Prenex normal form theorem over $\mathsf{I\Sigma_1}$

Every Hierarchy 𝚺 1 formula is 𝗜𝚺₁-provably equivalent to a formula of the form ∃¹ θ with θ in Hierarchy 𝚺 0, and dually for Hierarchy 𝚷 1 and ∀¹ θ.

theorem FFL.FirstOrder.Arithmetic.ISigma1.hasPrenex {n : ℕ} {φ : ArithmeticSemisentence n} (h : Hierarchy 𝚺 1 φ) : ∃ (φ' : Prenex 𝚺 1 Empty n), 𝗜𝚺₁ ⊢ ∀¹* (φ 🡘 ↑φ')

theorem FFL.FirstOrder.Arithmetic.ISigma1.exists_matrix_provable {n : ℕ} {φ : ArithmeticSemisentence n} (h : Hierarchy 𝚺 1 φ) : ∃ (θ : 𝚺₀.Semisentence (n + 1)), 𝗜𝚺₁ ⊢ ∀¹* (φ 🡘 ∃¹ ↑θ)

theorem FFL.FirstOrder.Arithmetic.ISigma1.exists_matrix_provable_pi {n : ℕ} {φ : ArithmeticSemisentence n} (h : Hierarchy 𝚷 1 φ) : ∃ (θ : 𝚺₀.Semisentence (n + 1)), 𝗜𝚺₁ ⊢ ∀¹* (φ 🡘 ∀¹ ↑θ)

theorem FFL.FirstOrder.Arithmetic.ISigma1.exists_matrix_provable_of_sentence {σ : ArithmeticSentence} (h : Hierarchy 𝚺 1 σ) : ∃ (θ : 𝚺₀.Semisentence 1), 𝗜𝚺₁ ⊢ σ 🡘 ∃¹ ↑θ