Documentation

LeanPool.PointwiseComposition.FailureOfComposition.HistoryObstruction

Supporting results for pointwise provable equality.

The composition obstruction from unprovable diagonal history divergence.

source
def PointwiseComposition.FailureOfComposition.HistoryWitnesses.historyZeroFormula (d : ℕ) :
Σ₁.Semisentence 1

The history Zero Formula construction in FailureOfComposition.HistoryWitnesses.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def PointwiseComposition.FailureOfComposition.HistoryWitnesses.historyPositiveFormula (d : ℕ) :
    Σ₁.Semisentence 1

    The history Positive Formula construction in FailureOfComposition.HistoryWitnesses.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem PointwiseComposition.FailureOfComposition.HistoryWitnesses.history_positive_iff {M : Type u_1} [FFL.ORingStructure M] [M↓[ℒₒᵣ] ⊧* 𝐏𝐀] [M↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] (d : ℕ) (s : M) :
      (∃ (z : M), 0 < z ∧ (FFL.FirstOrder.Semiformula.Evalb ![s, z]) ↑(historyGraph d)) ↔ ∃ (y : M), (FFL.FirstOrder.Semiformula.Evalb ![s, ↑d, ↑d, y]) ↑CategoricalRiceShapiro.Evaluator.evalnCertificateFormula
      source
      theorem PointwiseComposition.FailureOfComposition.HistoryWitnesses.diagonalHistory_iff {M : Type u_1} [FFL.ORingStructure M] [M↓[ℒₒᵣ] ⊧* 𝐏𝐀] [M↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] (d : ℕ) :
      (FFL.FirstOrder.Semiformula.Evalb ![]) (ConcreteEvaluator.diagonalHistoryFormula/[↑d]) ↔ ∃ (s : M) (z : M), 0 < z ∧ (FFL.FirstOrder.Semiformula.Evalb ![s, z]) ↑(historyGraph d)
      source
      theorem PointwiseComposition.FailureOfComposition.HistoryWitnesses.history_zero_iff_no_positive {M : Type u_1} [FFL.ORingStructure M] [M↓[ℒₒᵣ] ⊧* 𝐏𝐀] [M↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] (d : ℕ) (s : M) :
      (FFL.FirstOrder.Semiformula.Evalb ![s, 0]) ↑(historyGraph d) ↔ ¬∃ (z : M), 0 < z ∧ (FFL.FirstOrder.Semiformula.Evalb ![s, z]) ↑(historyGraph d)
      source
      theorem PointwiseComposition.FailureOfComposition.HistoryWitnesses.guard_pointwise_identity (T : FFL.FirstOrder.ArithmeticTheory) [𝐏𝐀 ≼ T] (d : ℕ) (hdiv : ¬(FFL.FirstOrder.Semiformula.Evalb ![d]) ConcreteEvaluator.diagonalHistoryFormula) :
      ProofSearch.Pointwise T (guardGraph d) ProofSearch.identity
      source
      theorem PointwiseComposition.FailureOfComposition.HistoryWitnesses.search_empty_implies_absence (d : ℕ) :
      𝐏𝐀 ⊢ ProofSearch.eqAt (searchGraph d) ProofSearch.empty 0 ⇒ₗ ∼ConcreteEvaluator.diagonalHistoryFormula/[↑d]
      source
      theorem PointwiseComposition.FailureOfComposition.HistoryWitnesses.graph_noncongruence_of_history_divergence (T : FFL.FirstOrder.ArithmeticTheory) [𝐏𝐀 ≼ T] (d : ℕ) (hdiv : ¬(FFL.FirstOrder.Semiformula.Evalb ![d]) ConcreteEvaluator.diagonalHistoryFormula) (hnot : T ⊬ ∼ConcreteEvaluator.diagonalHistoryFormula/[↑d]) :
      ProofSearch.Pointwise T (guardGraph d) ProofSearch.identity ∧ ¬ProofSearch.Pointwise T (ProofSearch.comp (guardGraph d) (searchGraph d)) (ProofSearch.comp ProofSearch.identity (searchGraph d))