Supporting results for pointwise provable equality.

The tag-5 induction case of certificate persistence

Constructor number 5 is composition. evalnCertificateFormula_natCode_persist_of_tag_five concerns a standard index q with partrecCodeTag q = 5. It proves that the raw evaluator certificate for q persists from a stage s to every stage t ≥ s, assuming the same persistence for every standard index p < q, whatever the constructor number of p. The theory assumptions are 𝐏𝐀 and 𝐈𝐎𝐩𝐞𝐧.

A private helper rewrites q as the canonical composition index canonicalPartrecCompIndex (partrecCodePayload₁ q) (partrecCodePayload₂ q), relating bodd.toNat to % 2 through Nat.mod_two_of_bodd; a second helper places both payloads strictly below q. At that index, evalnCertificateFormula_canonicalPartrecCompIndex_forward reduces the certificate at stage s to an inner certificate for the second payload and an outer certificate for the first. The induction hypothesis gives both at stage t, and evalnCertificateFormula_canonicalPartrecCompIndex_reverse reconstructs the certificate for the canonical index at stage t.

The file states one induction case. It proves neither the cases for the other constructor numbers nor persistence for all standard indices.

theorem PointwiseComposition.CategoricalRiceShapiro.Evaluator.evalnCertificateFormula_natCode_persist_of_tag_five {M : Type u_1} [FFL.ORingStructure M] [M↓[ℒₒᵣ] ⊧* 𝐏𝐀] [M↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] (q : ℕ) (hq : ArithmeticCode.partrecCodeTag q = 5) (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

Tag-5 induction case of certificate persistence. For a standard index q of constructor number 5, persistence of the certificate for q from stage s to any later stage t follows from persistence for every strictly smaller standard index, whatever its constructor number.