Supporting results for pointwise provable equality.

Success and totality of an evaluator cell

This module states two kinds of result, with different assumptions.

The success theorems describe a cell that has already reported a positive value: the encoded Option is x + 1 when the computation returned x. eval_codeOptionBind_succ_iff and eval_codeCompEvaluatorCell_succ_iff use 𝐏𝐀⁻. eval_codePairEvaluatorCell_succ_iff characterises the two successful lookups and their Cantor-pair result over 𝐈𝐎𝐩𝐞𝐧; its proof uses the public eval_codePair API at that fragment. None asserts that a cell has a value at all.

Over 𝐏𝐀, eval_codeEvaluatorCell_exists_of_values asserts exactly that: from values for the table and the argument alone, the whole cell has a value. The cell is a nested eager conditional, so the proof evaluates all five branches — base, pairing, composition, primitive recursion and minimization — together with every lookup and every option continuation inside them, whichever branch the tag comparisons end up selecting. It asserts existence only and identifies no value.

theorem PointwiseComposition.CategoricalRiceShapiro.Evaluator.eval_codeOptionBind_succ_iff {M : Type u_1} [FFL.ORingStructure M] [M↓[ℒₒᵣ] ⊧* 𝐏𝐀⁻] {n : ℕ} (dopt : Nat.ArithPart₁.Code n) (dk : Nat.ArithPart₁.Code (n + 1)) (y : M) (v : Fin n → M) : (FFL.FirstOrder.Semiformula.Evalb ((y + 1) :> v)) (FFL.FirstOrder.Arithmetic.code (ArithmeticCode.codeOptionBind dopt dk)) ↔ ∃ (x : M), (FFL.FirstOrder.Semiformula.Evalb ((x + 1) :> v)) (FFL.FirstOrder.Arithmetic.code dopt) ∧ (FFL.FirstOrder.Semiformula.Evalb ((y + 1) :> x :> v)) (FFL.FirstOrder.Arithmetic.code dk)

A successful bind on an encoded option: the bound code succeeds with some value, and the body succeeds at that value.

theorem PointwiseComposition.CategoricalRiceShapiro.Evaluator.eval_codePairEvaluatorCell_succ_iff {M : Type u_1} [FFL.ORingStructure M] [M↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] {r : ℕ} (dtable dk dcf dcg dn : Nat.ArithPart₁.Code r) (y : M) (v : Fin r → M) : (FFL.FirstOrder.Semiformula.Evalb ((y + 1) :> v)) (FFL.FirstOrder.Arithmetic.code (codePairEvaluatorCell dtable dk dcf dcg dn)) ↔ ∃ (a : M) (b : M), (FFL.FirstOrder.Semiformula.Evalb ((a + 1) :> v)) (FFL.FirstOrder.Arithmetic.code (codeTableLookup dtable dk dcf dn)) ∧ (FFL.FirstOrder.Semiformula.Evalb ((b + 1) :> a :> v)) (FFL.FirstOrder.Arithmetic.code (codeTableLookup (ArithmeticCode.codeLift dtable) (ArithmeticCode.codeLift dk) (ArithmeticCode.codeLift dcg) (ArithmeticCode.codeLift dn))) ∧ y = ⟪a, b⟫

Success of the pairing branch: the first index succeeds on the argument, the second index succeeds on the same argument, and the cell reports the Cantor pair of the two results.

theorem PointwiseComposition.CategoricalRiceShapiro.Evaluator.eval_codeCompEvaluatorCell_succ_iff {M : Type u_1} [FFL.ORingStructure M] [M↓[ℒₒᵣ] ⊧* 𝐏𝐀⁻] {r : ℕ} (dtable dk dcf dcg dn : Nat.ArithPart₁.Code r) (y : M) (v : Fin r → M) : (FFL.FirstOrder.Semiformula.Evalb ((y + 1) :> v)) (FFL.FirstOrder.Arithmetic.code (codeCompEvaluatorCell dtable dk dcf dcg dn)) ↔ ∃ (x : M), (FFL.FirstOrder.Semiformula.Evalb ((x + 1) :> v)) (FFL.FirstOrder.Arithmetic.code (codeTableLookup dtable dk dcg dn)) ∧ (FFL.FirstOrder.Semiformula.Evalb ((y + 1) :> x :> v)) (FFL.FirstOrder.Arithmetic.code (codeTableLookup (ArithmeticCode.codeLift dtable) (ArithmeticCode.codeLift dk) (ArithmeticCode.codeLift dcf) ArithmeticCode.codeHead))

Success of the composition branch: the inner index succeeds on the argument, and the outer index succeeds on that intermediate value.

Totality of an evaluator cell

theorem PointwiseComposition.CategoricalRiceShapiro.Evaluator.eval_codePrecEvaluatorCell_exists {M : Type u_1} [FFL.ORingStructure M] [M↓[ℒₒᵣ] ⊧* 𝐏𝐀] {r : ℕ} (dtable dk' dq dcf dcg dn : Nat.ArithPart₁.Code r) (table k' qv cf cg index : M) (v : Fin r → M) (htable : (FFL.FirstOrder.Semiformula.Evalb (table :> v)) (FFL.FirstOrder.Arithmetic.code dtable)) (hk' : (FFL.FirstOrder.Semiformula.Evalb (k' :> v)) (FFL.FirstOrder.Arithmetic.code dk')) (hq : (FFL.FirstOrder.Semiformula.Evalb (qv :> v)) (FFL.FirstOrder.Arithmetic.code dq)) (hcf : (FFL.FirstOrder.Semiformula.Evalb (cf :> v)) (FFL.FirstOrder.Arithmetic.code dcf)) (hcg : (FFL.FirstOrder.Semiformula.Evalb (cg :> v)) (FFL.FirstOrder.Arithmetic.code dcg)) (hn : (FFL.FirstOrder.Semiformula.Evalb (index :> v)) (FFL.FirstOrder.Arithmetic.code dn)) : ∃ (z : M), (FFL.FirstOrder.Semiformula.Evalb (z :> v)) (FFL.FirstOrder.Arithmetic.code (codePrecEvaluatorCell dtable dk' dq dcf dcg dn))

The primitive-recursion cell has a value. Both arms of its eager conditional are evaluated: the step lookup with its continuation, and the base lookup.

theorem PointwiseComposition.CategoricalRiceShapiro.Evaluator.eval_codeEvaluatorCell_exists_of_values {M : Type u_2} [FFL.ORingStructure M] [M↓[ℒₒᵣ] ⊧* 𝐏𝐀] {r : ℕ} (dtable dn : Nat.ArithPart₁.Code r) (table index : M) (v : Fin r → M) (htable : (FFL.FirstOrder.Semiformula.Evalb (table :> v)) (FFL.FirstOrder.Arithmetic.code dtable)) (hindex : (FFL.FirstOrder.Semiformula.Evalb (index :> v)) (FFL.FirstOrder.Arithmetic.code dn)) : ∃ (z : M), (FFL.FirstOrder.Semiformula.Evalb (z :> v)) (FFL.FirstOrder.Arithmetic.code (codeEvaluatorCell dtable dn))

An evaluator cell has a value at any table and argument values.

The cell is a nested eager conditional, so every one of its five branches is evaluated before the tag comparisons select one, and each branch in turn supplies every lookup and every option continuation it contains. Only existence is asserted: nothing here decodes the table, the index, or the program, and no value is identified.