Documentation

LeanPool.PointwiseComposition.FailureOfComposition.RangeAssignment

Supporting results for pointwise provable equality.

The range partial identity of a Sigma-one graph and its realization by an index of the fixed evaluator. The defining range equation holds in every PA model. PA-uniformly equivalent choices of realizing indices are pointwise equivalent over every PA extension.

source
def PointwiseComposition.FailureOfComposition.ConcreteIndices.rangeOfGraph (F : ProofSearch.Graph) :
ProofSearch.Graph

The partial identity on the range of a Sigma-one graph.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem PointwiseComposition.FailureOfComposition.ConcreteIndices.rangeOfGraph_eval {M : Type u_1} [FFL.ORingStructure M] (F : ProofSearch.Graph) (v : Fin 2 → M) :
    (FFL.FirstOrder.Semiformula.Evalb v) ↑(rangeOfGraph F) ↔ v 0 = v 1 ∧ ∃ (x : M), (FFL.FirstOrder.Semiformula.Evalb ![x, v 0]) ↑F
    source
    theorem PointwiseComposition.FailureOfComposition.ConcreteIndices.rangeOfGraph_functional (F : ProofSearch.Graph) :
    ProofSearch.Functional (rangeOfGraph F)

    Range partial identities are PA-provably functional, even if the source graph has not been assumed functional.

    source
    theorem PointwiseComposition.FailureOfComposition.ConcreteIndices.uniform_rangeOfGraph {F G : ProofSearch.Graph} (h : ProofSearch.Uniform 𝐏𝐀 F G) :
    ProofSearch.Uniform 𝐏𝐀 (rangeOfGraph F) (rangeOfGraph G)

    PA-uniform graph equality is preserved by taking the range partial identity.

    source
    def PointwiseComposition.FailureOfComposition.ConcreteIndices.rangeGraph (e : ℕ) :
    ProofSearch.Graph

    The range partial identity of a program in the fixed evaluator.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem PointwiseComposition.FailureOfComposition.ConcreteIndices.rangeGraph_eval {M : Type u_1} [FFL.ORingStructure M] (e : ℕ) (v : Fin 2 → M) :
      (FFL.FirstOrder.Semiformula.Evalb v) ↑(rangeGraph e) ↔ v 0 = v 1 ∧ ∃ (x : M), (FFL.FirstOrder.Semiformula.Evalb ![x, v 0]) ↑(ConcreteEvaluator.eventualGraph e)
      source
      theorem PointwiseComposition.FailureOfComposition.ConcreteIndices.rangeGraph_functional (e : ℕ) :
      ProofSearch.Functional (rangeGraph e)
      source
      noncomputable def PointwiseComposition.FailureOfComposition.ConcreteIndices.rangeIndex (e : ℕ) :
      ℕ

      Choose a range program using the proved Sigma-one graph realization theorem.

      Equations
      Instances For
        source
        theorem PointwiseComposition.FailureOfComposition.ConcreteIndices.rangeIndex_realizes (e : ℕ) :
        ProofSearch.Uniform 𝐏𝐀 (ConcreteEvaluator.eventualGraph (rangeIndex e)) (rangeGraph e)
        source
        theorem PointwiseComposition.FailureOfComposition.ConcreteIndices.rangeIndex_graph_equation {M : Type u_1} [FFL.ORingStructure M] [M↓[ℒₒᵣ] ⊧* 𝐏𝐀] (e : ℕ) (r w : M) :
        (FFL.FirstOrder.Semiformula.Evalb ![r, w]) ↑(ConcreteEvaluator.eventualGraph (rangeIndex e)) ↔ r = w ∧ ∃ (x : M), (FFL.FirstOrder.Semiformula.Evalb ![x, r]) ↑(ConcreteEvaluator.eventualGraph e)

        The selected range index satisfies the defining equation in every PA model.

        source
        theorem PointwiseComposition.FailureOfComposition.ConcreteIndices.rangeIndex_eval (e r w : ℕ) :
        w ∈ Kleene.eval (rangeIndex e) r ↔ r = w ∧ ∃ (x : ℕ), r ∈ Kleene.eval e x

        In the standard model this is the partial identity on the program's range.

        source
        theorem PointwiseComposition.FailureOfComposition.ConcreteIndices.rangeIndex_of_uniform {e : ℕ} {F : ProofSearch.Graph} (h : ProofSearch.Uniform 𝐏𝐀 (ConcreteEvaluator.eventualGraph e) F) :
        ProofSearch.Uniform 𝐏𝐀 (ConcreteEvaluator.eventualGraph (rangeIndex e)) (rangeOfGraph F)

        A PA-uniform description of a source graph transports to its selected range.

        source
        theorem PointwiseComposition.FailureOfComposition.ConcreteIndices.rangeOfGraph_empty :
        ProofSearch.Uniform 𝐏𝐀 (rangeOfGraph ProofSearch.empty) ProofSearch.empty

        The empty graph has empty range in PA.

        source
        theorem PointwiseComposition.FailureOfComposition.ConcreteIndices.rangeIndex_empty :
        ProofSearch.Uniform 𝐏𝐀 (ConcreteEvaluator.eventualGraph (rangeIndex ConcreteEmptyGraph.concreteEmptyIndex)) ProofSearch.empty

        The selected range of the concrete empty program is uniformly empty in PA.

        source
        theorem PointwiseComposition.FailureOfComposition.ConcreteIndices.rangeIndex_realization_unique {e r s : ℕ} (hr : ProofSearch.Uniform 𝐏𝐀 (ConcreteEvaluator.eventualGraph r) (rangeGraph e)) (hs : ProofSearch.Uniform 𝐏𝐀 (ConcreteEvaluator.eventualGraph s) (rangeGraph e)) :
        ProofSearch.Uniform 𝐏𝐀 (ConcreteEvaluator.eventualGraph r) (ConcreteEvaluator.eventualGraph s)

        Any two indices realizing the same range graph are PA-uniformly equivalent.

        source
        theorem PointwiseComposition.FailureOfComposition.ConcreteIndices.rangeIndex_choice_independent (T : FFL.FirstOrder.ArithmeticTheory) [𝐏𝐀 ≼ T] {e r : ℕ} (hr : ProofSearch.Uniform 𝐏𝐀 (ConcreteEvaluator.eventualGraph r) (rangeGraph e)) :
        PointwiseIndex T r (rangeIndex e)

        Replacing the selected range index by any PA-uniform realization leaves its pointwise class unchanged over every PA extension.