Documentation

LeanPool.PointwiseComposition.FailureOfComposition.GeneratedIndexTransport

Supporting results for pointwise provable equality.

The least composition congruence on indices agrees with the least congruence on their functional arithmetic graphs. Realization and composition are used at the level of PA proofs, including for the chosen inverse representatives.

source
def PointwiseComposition.FailureOfComposition.ProgramIndices.GeneratedRel (A : Arithmetization) (T : FFL.FirstOrder.ArithmeticTheory) (e d : ℕ) :
Prop

The Generated Rel construction in FailureOfComposition.ProgramIndices.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def PointwiseComposition.FailureOfComposition.ProgramIndices.generatedSetoid (A : Arithmetization) (T : FFL.FirstOrder.ArithmeticTheory) :
    Setoid ℕ

    The generated Setoid construction in FailureOfComposition.ProgramIndices.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      noncomputable def PointwiseComposition.FailureOfComposition.ProgramIndices.realizationIndex (A : Arithmetization) (F : ProofSearch.FunctionalGraph) :
      ℕ

      Select an index whose arithmetic graph PA proves equal to the given graph.

      Equations
      Instances For
        source
        theorem PointwiseComposition.FailureOfComposition.ProgramIndices.realizationIndex_uniform (A : Arithmetization) (F : ProofSearch.FunctionalGraph) :
        ProofSearch.Uniform 𝐏𝐀 (A.graph (realizationIndex A F)) ↑F
        source
        theorem PointwiseComposition.FailureOfComposition.ProgramIndices.realizationIndex_pointwise (A : Arithmetization) (T : FFL.FirstOrder.ArithmeticTheory) [𝐏𝐀 ≼ T] (F G : ProofSearch.FunctionalGraph) (h : ProofSearch.Pointwise T ↑F ↑G) :
        PointwiseIndex A T (realizationIndex A F) (realizationIndex A G)
        source
        theorem PointwiseComposition.FailureOfComposition.ProgramIndices.realizationIndex_roundtrip (A : Arithmetization) (T : FFL.FirstOrder.ArithmeticTheory) [𝐏𝐀 ≼ T] (e : ℕ) :
        PointwiseIndex A T (realizationIndex A ⟨A.graph e, ⋯⟩) e
        source
        theorem PointwiseComposition.FailureOfComposition.ProgramIndices.realizationIndex_composition (A : Arithmetization) (T : FFL.FirstOrder.ArithmeticTheory) [𝐏𝐀 ≼ T] (F G : ProofSearch.FunctionalGraph) :
        PointwiseIndex A T (realizationIndex A (ProofSearch.functionalComp F G)) (A.compIndex (realizationIndex A F) (realizationIndex A G))
        source
        theorem PointwiseComposition.FailureOfComposition.ProgramIndices.generatedRel_implies_graph (A : Arithmetization) (T : FFL.FirstOrder.ArithmeticTheory) [𝐏𝐀 ≼ T] {e d : ℕ} (h : GeneratedRel A T e d) :
        GeneratedCongruence.Rel T ⟨A.graph e, ⋯⟩ ⟨A.graph d, ⋯⟩

        The graph interpretation preserves the generated relation despite being a composition homomorphism only up to a PA-provable graph equation.

        source
        theorem PointwiseComposition.FailureOfComposition.ProgramIndices.graph_implies_generatedRel (A : Arithmetization) (T : FFL.FirstOrder.ArithmeticTheory) [𝐏𝐀 ≼ T] {e d : ℕ} (h : GeneratedCongruence.Rel T ⟨A.graph e, ⋯⟩ ⟨A.graph d, ⋯⟩) :
        GeneratedRel A T e d

        Realization transports the graph congruence back to indices. The chosen realizers differ from the original indices by generating relations already.

        source
        theorem PointwiseComposition.FailureOfComposition.ProgramIndices.generatedRel_iff_graph (A : Arithmetization) (T : FFL.FirstOrder.ArithmeticTheory) [𝐏𝐀 ≼ T] (e d : ℕ) :
        GeneratedRel A T e d ↔ GeneratedCongruence.Rel T ⟨A.graph e, ⋯⟩ ⟨A.graph d, ⋯⟩