Documentation

LeanPool.PointwiseComposition.FailureOfComposition.ConcreteConstructorGraphs

Supporting results for pointwise provable equality.

Constructor equations for the concrete evaluator over arbitrary models of PA. Shared decoder and forward pairing helpers come from production PairPersistence; the public results remove fuel and synchronize component computations using unconditional persistence.

source
theorem PointwiseComposition.FailureOfComposition.ConcreteEvaluator.evalnCertificateFormula_tag_four_iff {M : Type u_1} [FFL.ORingStructure M] [M↓[ℒₒᵣ] ⊧* 𝐏𝐀] [M↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] (q : ℕ) (hq : CategoricalRiceShapiro.ArithmeticCode.partrecCodeTag q = 4) (s u y : M) :
(FFL.FirstOrder.Semiformula.Evalb ![s, ↑q, u, y]) ↑CategoricalRiceShapiro.Evaluator.evalnCertificateFormula ↔ ∃ (a : M) (b : M), (FFL.FirstOrder.Semiformula.Evalb ![s, ↑(CategoricalRiceShapiro.ArithmeticCode.partrecCodePayload₁ q), u, a]) ↑CategoricalRiceShapiro.Evaluator.evalnCertificateFormula ∧ (FFL.FirstOrder.Semiformula.Evalb ![s, ↑(CategoricalRiceShapiro.ArithmeticCode.partrecCodePayload₂ q), u, b]) ↑CategoricalRiceShapiro.Evaluator.evalnCertificateFormula ∧ y = ⟪a, b⟫

At a common stage, pairing computes the pair of its component outputs.

source
def PointwiseComposition.FailureOfComposition.ConcreteEvaluator.canonicalPartrecPairIndex (fCode gCode : ℕ) :
ℕ

Mathlib's pairing constructor, in its fixed natural-number encoding.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem PointwiseComposition.FailureOfComposition.ConcreteEvaluator.canonicalPartrecPairIndex_eq (f g : ℕ) :
    canonicalPartrecPairIndex f g = 4 * Nat.pair f g + 4
    source
    theorem PointwiseComposition.FailureOfComposition.ConcreteEvaluator.canonicalPartrecPairIndex_tag (f g : ℕ) :
    CategoricalRiceShapiro.ArithmeticCode.partrecCodeTag (canonicalPartrecPairIndex f g) = 4
    source
    theorem PointwiseComposition.FailureOfComposition.ConcreteEvaluator.canonicalPartrecPairIndex_payload (f g : ℕ) :
    CategoricalRiceShapiro.ArithmeticCode.partrecCodePayload (canonicalPartrecPairIndex f g) = Nat.pair f g
    source
    theorem PointwiseComposition.FailureOfComposition.ConcreteEvaluator.canonicalPartrecPairIndex_left (f g : ℕ) :
    CategoricalRiceShapiro.ArithmeticCode.partrecCodePayload₁ (canonicalPartrecPairIndex f g) = f
    source
    theorem PointwiseComposition.FailureOfComposition.ConcreteEvaluator.canonicalPartrecPairIndex_right (f g : ℕ) :
    CategoricalRiceShapiro.ArithmeticCode.partrecCodePayload₂ (canonicalPartrecPairIndex f g) = g
    source
    theorem PointwiseComposition.FailureOfComposition.ConcreteEvaluator.eventualGraph_pair_eval {M : Type u_1} [FFL.ORingStructure M] [M↓[ℒₒᵣ] ⊧* 𝐏𝐀] [M↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] (f g : ℕ) (u y : M) :
    (FFL.FirstOrder.Semiformula.Evalb ![u, y]) ↑(eventualGraph (canonicalPartrecPairIndex f g)) ↔ ∃ (a : M) (b : M), (FFL.FirstOrder.Semiformula.Evalb ![u, a]) ↑(eventualGraph f) ∧ (FFL.FirstOrder.Semiformula.Evalb ![u, b]) ↑(eventualGraph g) ∧ y = ⟪a, b⟫

    Pairing equation with component stages synchronized internally in PA.

    source
    theorem PointwiseComposition.FailureOfComposition.ConcreteEvaluator.encode_pair_eq (f g : Nat.Partrec.Code) :
    Encodable.encode (f.pair g) = canonicalPartrecPairIndex (Encodable.encode f) (Encodable.encode g)

    The natural encoding of a pair constructor is the canonical pairing index.

    source
    theorem PointwiseComposition.FailureOfComposition.ConcreteEvaluator.evalnCertificateFormula_pair_iff {M : Type u_1} [FFL.ORingStructure M] [M↓[ℒₒᵣ] ⊧* 𝐏𝐀] [M↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] (f g : Nat.Partrec.Code) (s u y : M) :
    (FFL.FirstOrder.Semiformula.Evalb ![s, ↑(Encodable.encode (f.pair g)), u, y]) ↑CategoricalRiceShapiro.Evaluator.evalnCertificateFormula ↔ ∃ (a : M) (b : M), (FFL.FirstOrder.Semiformula.Evalb ![s, ↑(Encodable.encode f), u, a]) ↑CategoricalRiceShapiro.Evaluator.evalnCertificateFormula ∧ (FFL.FirstOrder.Semiformula.Evalb ![s, ↑(Encodable.encode g), u, b]) ↑CategoricalRiceShapiro.Evaluator.evalnCertificateFormula ∧ y = ⟪a, b⟫

    Same-stage pairing equation in terms of the actual syntax constructors.

    source
    theorem PointwiseComposition.FailureOfComposition.ConcreteEvaluator.eventualGraph_pair_code_eval {M : Type u_1} [FFL.ORingStructure M] [M↓[ℒₒᵣ] ⊧* 𝐏𝐀] [M↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] (f g : Nat.Partrec.Code) (u y : M) :
    (FFL.FirstOrder.Semiformula.Evalb ![u, y]) ↑(eventualGraph (Encodable.encode (f.pair g))) ↔ ∃ (a : M) (b : M), (FFL.FirstOrder.Semiformula.Evalb ![u, a]) ↑(eventualGraph (Encodable.encode f)) ∧ (FFL.FirstOrder.Semiformula.Evalb ![u, b]) ↑(eventualGraph (Encodable.encode g)) ∧ y = ⟪a, b⟫

    Eventual pairing equation for Mathlib's actual syntax constructors.