Documentation

LeanPool.PointwiseComposition.FailureOfComposition.RangeWitness

Supporting results for pointwise provable equality.

A zero-output probe separates external pointwise equality from equality of range partial identities. Every standard input may have its own PA proof of divergence, while the range at input zero tests an internal existential over all possible probe inputs. No passage from these individual proofs to a universal proof is assumed.

source
def PointwiseComposition.FailureOfComposition.ConcreteIndices.probeGraph (P : Σ₁.Semisentence 1) :
ProofSearch.Graph

The zero-output probe for a Sigma-one predicate on possible witnesses.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem PointwiseComposition.FailureOfComposition.ConcreteIndices.probeGraph_eval {M : Type u_1} [FFL.ORingStructure M] (P : Σ₁.Semisentence 1) (v : Fin 2 → M) :
    (FFL.FirstOrder.Semiformula.Evalb v) ↑(probeGraph P) ↔ (FFL.FirstOrder.Semiformula.Evalb ![v 0]) ↑P ∧ v 1 = 0
    source
    theorem PointwiseComposition.FailureOfComposition.ConcreteIndices.probeGraph_functional (P : Σ₁.Semisentence 1) :
    ProofSearch.Functional (probeGraph P)

    A probe has at most one output, whether or not its predicate holds.

    source
    noncomputable def PointwiseComposition.FailureOfComposition.ConcreteIndices.probeIndex (P : Σ₁.Semisentence 1) :
    ℕ

    A concrete program index supplied by the proved Sigma-one realization theorem.

    Equations
    Instances For
      source
      theorem PointwiseComposition.FailureOfComposition.ConcreteIndices.probeIndex_realizes (P : Σ₁.Semisentence 1) :
      ProofSearch.Uniform 𝐏𝐀 (ConcreteEvaluator.eventualGraph (probeIndex P)) (probeGraph P)
      source
      theorem PointwiseComposition.FailureOfComposition.ConcreteIndices.probeIndex_graph_equation {M : Type u_1} [FFL.ORingStructure M] [M↓[ℒₒᵣ] ⊧* 𝐏𝐀] (P : Σ₁.Semisentence 1) (x y : M) :
      (FFL.FirstOrder.Semiformula.Evalb ![x, y]) ↑(ConcreteEvaluator.eventualGraph (probeIndex P)) ↔ (FFL.FirstOrder.Semiformula.Evalb ![x]) ↑P ∧ y = 0

      The equation holds for all inputs of every PA model, including nonstandard ones.

      source
      def PointwiseComposition.FailureOfComposition.ConcreteIndices.absenceSentence (P : Σ₁.Semisentence 1) :
      FFL.FirstOrder.ArithmeticSentence

      The internal assertion that the probe predicate has no witness.

      Equations
      Instances For
        source
        @[simp]
        theorem PointwiseComposition.FailureOfComposition.ConcreteIndices.absenceSentence_eval {M : Type u_1} [FFL.ORingStructure M] (P : Σ₁.Semisentence 1) :
        (FFL.FirstOrder.Semiformula.Evalb ![]) (absenceSentence P) ↔ ∀ (p : M), ¬(FFL.FirstOrder.Semiformula.Evalb ![p]) ↑P
        source
        theorem PointwiseComposition.FailureOfComposition.ConcreteIndices.probeGraph_pointwise_empty (T : FFL.FirstOrder.ArithmeticTheory) [𝐏𝐀 ≼ T] (P : Σ₁.Semisentence 1) (href : ∀ (n : ℕ), 𝐏𝐀 ⊢ ∼↑P/[↑n]) :
        ProofSearch.Pointwise T (probeGraph P) ProofSearch.empty

        Separate numeralwise refutations suffice for external pointwise equality.

        source
        theorem PointwiseComposition.FailureOfComposition.ConcreteIndices.probeIndex_pointwise_empty (T : FFL.FirstOrder.ArithmeticTheory) [𝐏𝐀 ≼ T] (P : Σ₁.Semisentence 1) (href : ∀ (n : ℕ), 𝐏𝐀 ⊢ ∼↑P/[↑n]) :
        PointwiseIndex T (probeIndex P) ConcreteEmptyGraph.concreteEmptyIndex
        source
        theorem PointwiseComposition.FailureOfComposition.ConcreteIndices.range_probe_at_zero {M : Type u_1} [FFL.ORingStructure M] (P : Σ₁.Semisentence 1) :
        (FFL.FirstOrder.Semiformula.Evalb ![0, 0]) ↑(rangeOfGraph (probeGraph P)) ↔ ∃ (p : M), (FFL.FirstOrder.Semiformula.Evalb ![p]) ↑P

        The range at zero records the internal existential over all probe inputs.

        source
        theorem PointwiseComposition.FailureOfComposition.ConcreteIndices.range_probe_empty_implies_absence (P : Σ₁.Semisentence 1) :
        𝐏𝐀 ⊢ ProofSearch.eqAt (rangeOfGraph (probeGraph P)) ProofSearch.empty 0 ⇒ₗ absenceSentence P

        Equality of the probe's range with the empty graph at the one input zero already implies the internally quantified absence sentence.

        source
        theorem PointwiseComposition.FailureOfComposition.ConcreteIndices.range_probeIndex_not_pointwise_empty (T : FFL.FirstOrder.ArithmeticTheory) [𝐏𝐀 ≼ T] (P : Σ₁.Semisentence 1) (hnot : T ⊬ absenceSentence P) :
        ¬PointwiseIndex T (rangeIndex (probeIndex P)) (rangeIndex ConcreteEmptyGraph.concreteEmptyIndex)
        source
        theorem PointwiseComposition.FailureOfComposition.ConcreteIndices.range_counterexample_of_instance_refutations (T : FFL.FirstOrder.ArithmeticTheory) [𝐏𝐀 ≼ T] (P : Σ₁.Semisentence 1) (href : ∀ (n : ℕ), 𝐏𝐀 ⊢ ∼↑P/[↑n]) (hnot : T ⊬ absenceSentence P) :
        PointwiseIndex T (probeIndex P) ConcreteEmptyGraph.concreteEmptyIndex ∧ ¬PointwiseIndex T (rangeIndex (probeIndex P)) (rangeIndex ConcreteEmptyGraph.concreteEmptyIndex)

        A concrete pair of equivalent program indices whose range indices differ.

        source
        def PointwiseComposition.FailureOfComposition.ConcreteIndices.NoIndexQuotientRange (T : FFL.FirstOrder.ArithmeticTheory) [𝐏𝐀 ≼ T] :
        Prop

        The selected range assignment has no operation on the pointwise quotient.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          theorem PointwiseComposition.FailureOfComposition.ConcreteIndices.no_index_quotient_range_of_counterexample (T : FFL.FirstOrder.ArithmeticTheory) [𝐏𝐀 ≼ T] (u z : ℕ) (huz : PointwiseIndex T u z) (hr : ¬PointwiseIndex T (rangeIndex u) (rangeIndex z)) :
          NoIndexQuotientRange T

          A pair of equivalent indices with distinct range classes prevents descent.

          source
          theorem PointwiseComposition.FailureOfComposition.ConcreteIndices.no_quotient_range_of_instance_refutations (T : FFL.FirstOrder.ArithmeticTheory) [𝐏𝐀 ≼ T] (P : Σ₁.Semisentence 1) (href : ∀ (n : ℕ), 𝐏𝐀 ⊢ ∼↑P/[↑n]) (hnot : T ⊬ absenceSentence P) :
          NoIndexQuotientRange T

          No operation on the pointwise quotient induces the chosen range assignment.

          source
          theorem PointwiseComposition.FailureOfComposition.ConcreteIndices.no_quotient_range_of_correct_assignment (T : FFL.FirstOrder.ArithmeticTheory) [𝐏𝐀 ≼ T] (h : NoIndexQuotientRange T) (ρ : ℕ → ℕ) (hρ : ∀ (e : ℕ), ProofSearch.Uniform 𝐏𝐀 (ConcreteEvaluator.eventualGraph (ρ e)) (rangeGraph e)) :
          ¬∃ (R : Quotient (indexSetoid T) → Quotient (indexSetoid T)), ∀ (e : ℕ), R ⟦e⟧ = ⟦ρ e⟧

          Non-descent persists for every choice of PA-correct range indices.