Supporting results for pointwise provable equality.

Persistence for constructor 7 of the existing Mathlib-index history evaluator. The subsidiary-index premise is discharged by the external induction on indices; the same-index recursive lookup is handled by PA induction on the source stage.

theorem PointwiseComposition.CategoricalRiceShapiro.Evaluator.evalnCertificateFormula_tag_seven_iff {M : Type u_1} [FFL.ORingStructure M] [M↓[ℒₒᵣ] ⊧* 𝐏𝐀] [M↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] (q : ℕ) (hq : ArithmeticCode.partrecCodeTag q = 7) (s u y : M) (hs : 0 < s) : (FFL.FirstOrder.Semiformula.Evalb ![s, ↑q, u, y]) ↑evalnCertificateFormula ↔ u < s ∧ ∃ (x : M), (FFL.FirstOrder.Semiformula.Evalb ![s, ↑(ArithmeticCode.partrecCodePayload q), u, x]) ↑evalnCertificateFormula ∧ (0 < x ∧ (FFL.FirstOrder.Semiformula.Evalb ![s - 1, ↑q, ⟪π₁ u, π₂ u + 1⟫, y]) ↑evalnCertificateFormula ∨ x = 0 ∧ y = π₂ u)

The complete tag-7 equation for the existing raw computation formula, valid at arbitrary stages and arguments of every model of PA.

theorem PointwiseComposition.CategoricalRiceShapiro.Evaluator.evalnCertificateFormula_natCode_persist_of_tag_seven {M : Type u_1} [FFL.ORingStructure M] [M↓[ℒₒᵣ] ⊧* 𝐏𝐀] [M↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] (q : ℕ) (hq : ArithmeticCode.partrecCodeTag q = 7) (ih : ∀ p < q, ∀ (s t u y : M), s ≤ t → (FFL.FirstOrder.Semiformula.Evalb ![s, ↑p, u, y]) ↑evalnCertificateFormula → (FFL.FirstOrder.Semiformula.Evalb ![t, ↑p, u, y]) ↑evalnCertificateFormula) (s t u y : M) : s ≤ t → (FFL.FirstOrder.Semiformula.Evalb ![s, ↑q, u, y]) ↑evalnCertificateFormula → (FFL.FirstOrder.Semiformula.Evalb ![t, ↑q, u, y]) ↑evalnCertificateFormula

Constructor-7 persistence of the accepted computation formula. The only premise is persistence for strictly smaller standard program indices.