Documentation

LeanPool.PointwiseComposition.CategoricalRiceShapiro.Evaluator.Certificate

Supporting results for pointwise provable equality.

The raw evaluator certificate #

evalnGraphFormula names the graph of codeHistoryEvaluator as a Sigma-one semisentence, and evalnCertificateFormula reorders and shifts its arguments so that the four places read stage, index, input, output, with the output recorded as its successor. evalnCertificateFormula_eval_history_iff is the bridge between the two presentations; it is a substitution identity and needs no arithmetic theory.

evalnCertificateFormula_canonicalPartrecCompIndex_forward decomposes a certificate for a canonical composition index into a certificate for the inner index followed by one for the outer index, at the same stage. evalnCertificateFormula_canonicalPartrecCompIndex_reverse reconstructs the certificate for the composition index from two component certificates that are already at one supplied stage. evalnCertificateFormula_canonicalPartrecCompIndex_iff packages these two directions as an equivalence at one supplied stage. None of these theorems brings certificates supplied at unrelated stages to a common stage, and none concerns first-success minimality or standard-model semantics.

source
def PointwiseComposition.CategoricalRiceShapiro.Evaluator.evalnGraphFormula :
Σ₁.Semisentence 4

The graph of codeHistoryEvaluator, as a Sigma-one semisentence.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def PointwiseComposition.CategoricalRiceShapiro.Evaluator.evalnCertificateFormula :
    Σ₁.Semisentence 4

    The raw evaluator certificate: the graph formula with its places reordered to stage, index, input, output, the output shifted by one.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem PointwiseComposition.CategoricalRiceShapiro.Evaluator.evalnCertificateFormula_eval_history_iff {M : Type u_1} [FFL.ORingStructure M] (s qCode u y : M) :
      (FFL.FirstOrder.Semiformula.Evalb ![s, qCode, u, y]) ↑evalnCertificateFormula ↔ (FFL.FirstOrder.Semiformula.Evalb ![y + 1, s, qCode, u]) (FFL.FirstOrder.Arithmetic.code codeHistoryEvaluator)

      The certificate formula is the graph of codeHistoryEvaluator with the places reordered. This is a substitution identity: it holds in an arbitrary structure and needs no arithmetic theory.

      source
      theorem PointwiseComposition.CategoricalRiceShapiro.Evaluator.evalnCertificateFormula_canonicalPartrecCompIndex_forward {M : Type u_1} [FFL.ORingStructure M] [M↓[ℒₒᵣ] ⊧* 𝐏𝐀] (s u y : M) (fCode gCode : ℕ) (h : (FFL.FirstOrder.Semiformula.Evalb ![s, FFL.ORingStructure.numeral (PartialRecursive.canonicalPartrecCompIndex fCode gCode), u, y]) ↑evalnCertificateFormula) :
      ∃ (x : M), (FFL.FirstOrder.Semiformula.Evalb ![s, FFL.ORingStructure.numeral gCode, u, x]) ↑evalnCertificateFormula ∧ (FFL.FirstOrder.Semiformula.Evalb ![s, FFL.ORingStructure.numeral fCode, x, y]) ↑evalnCertificateFormula

      A certificate for a canonical composition index decomposes, at the same stage, into a certificate for the inner index and one for the outer index.

      𝐏𝐀 is the only theory assumption. The indices enter the statement through ORingStructure.numeral, which needs no theory, rather than through the numeral cast, whose NatCast instance is not reachable from 𝐏𝐀 by instance search; 𝐈Σ 1 is installed inside the proof and supplies 𝐈Σ₀, 𝐈𝐎𝐩𝐞𝐧 and 𝐏𝐀⁻ through Foundation's instance chain.

      source
      theorem PointwiseComposition.CategoricalRiceShapiro.Evaluator.evalnCertificateFormula_canonicalPartrecCompIndex_reverse {M : Type u_1} [FFL.ORingStructure M] [M↓[ℒₒᵣ] ⊧* 𝐏𝐀] (s u x y : M) (fCode gCode : ℕ) (hinner : (FFL.FirstOrder.Semiformula.Evalb ![s, FFL.ORingStructure.numeral gCode, u, x]) ↑evalnCertificateFormula) (houter : (FFL.FirstOrder.Semiformula.Evalb ![s, FFL.ORingStructure.numeral fCode, x, y]) ↑evalnCertificateFormula) :
      (FFL.FirstOrder.Semiformula.Evalb ![s, FFL.ORingStructure.numeral (PartialRecursive.canonicalPartrecCompIndex fCode gCode), u, y]) ↑evalnCertificateFormula

      Two component certificates at one supplied stage reconstruct the certificate for their canonical composition at that same stage.

      source
      theorem PointwiseComposition.CategoricalRiceShapiro.Evaluator.evalnCertificateFormula_canonicalPartrecCompIndex_iff {M : Type u_1} [FFL.ORingStructure M] [M↓[ℒₒᵣ] ⊧* 𝐏𝐀] (s u y : M) (fCode gCode : ℕ) :
      (FFL.FirstOrder.Semiformula.Evalb ![s, FFL.ORingStructure.numeral (PartialRecursive.canonicalPartrecCompIndex fCode gCode), u, y]) ↑evalnCertificateFormula ↔ ∃ (x : M), (FFL.FirstOrder.Semiformula.Evalb ![s, FFL.ORingStructure.numeral gCode, u, x]) ↑evalnCertificateFormula ∧ (FFL.FirstOrder.Semiformula.Evalb ![s, FFL.ORingStructure.numeral fCode, x, y]) ↑evalnCertificateFormula

      A certificate for a canonical composition index at a supplied stage is equivalent to an inner certificate followed by an outer certificate at that same stage.