Supporting results for pointwise provable equality.

Fair search and disjunction for the concrete program numbering. The searched arithmetic tests are total history-evaluator computations, so a divergent candidate does not prevent the search from reaching a different candidate. All graph laws hold at arbitrary elements of every PA model.

def PointwiseComposition.FailureOfComposition.SigmaOneSearch.historyAt {n : ℕ} (c : ProgramGraph.PCode) (s x : Nat.ArithPart₁.Code n) : Nat.ArithPart₁.Code n

The history At construction in FailureOfComposition.SigmaOneSearch.

Equations

• One or more equations did not get rendered due to their size.

def PointwiseComposition.FailureOfComposition.SigmaOneSearch.successAt {n : ℕ} (c : ProgramGraph.PCode) (s x : Nat.ArithPart₁.Code n) : Nat.ArithPart₁.Code n

The success At construction in FailureOfComposition.SigmaOneSearch.

Equations

• One or more equations did not get rendered due to their size.

def PointwiseComposition.FailureOfComposition.SigmaOneSearch.existsTest (c : ProgramGraph.PCode) : Nat.ArithPart₁.Code 2

The exists Test construction in FailureOfComposition.SigmaOneSearch.

Equations

• One or more equations did not get rendered due to their size.

def PointwiseComposition.FailureOfComposition.SigmaOneSearch.unionTest (c d : ProgramGraph.PCode) : Nat.ArithPart₁.Code 2

The union Test construction in FailureOfComposition.SigmaOneSearch.

Equations

• One or more equations did not get rendered due to their size.

def PointwiseComposition.FailureOfComposition.SigmaOneSearch.candidateSearch (c : ProgramGraph.PCode) : ProgramGraph.PCode

Return the candidate from the least successful stage/candidate pair.

Equations

• One or more equations did not get rendered due to their size.

def PointwiseComposition.FailureOfComposition.SigmaOneSearch.existsProgram (c : ProgramGraph.PCode) : ProgramGraph.PCode

Existential projection, with output zero on its domain.

Equations

• PointwiseComposition.FailureOfComposition.SigmaOneSearch.existsProgram c = Nat.Partrec.Code.zero.comp (PointwiseComposition.FailureOfComposition.SigmaOneSearch.candidateSearch c)

def PointwiseComposition.FailureOfComposition.SigmaOneSearch.unionProgram (c d : ProgramGraph.PCode) : ProgramGraph.PCode

Disjunction, with output zero if either program returns zero.

Equations

• One or more equations did not get rendered due to their size.

def PointwiseComposition.FailureOfComposition.SigmaOneSearch.packedSuccess {M : Type u_1} [FFL.ORingStructure M] [M↓[ℒₒᵣ] ⊧* 𝐏𝐀] [M↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] (c : ProgramGraph.PCode) (x w : M) : Prop

A packed witness records a stage and a candidate accepted by c with output zero.

Equations

• One or more equations did not get rendered due to their size.

theorem PointwiseComposition.FailureOfComposition.SigmaOneSearch.computes_candidateSearch {M : Type u_1} [FFL.ORingStructure M] [M↓[ℒₒᵣ] ⊧* 𝐏𝐀] [M↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] (c : ProgramGraph.PCode) (x a : M) : ProgramGraph.Computes (candidateSearch c) x a ↔ ∃ (w : M), packedSuccess c x w ∧ (∀ r < w, ¬packedSuccess c x r) ∧ a = π₂ w

Exact witness-selection graph: select the candidate belonging to the least successful stage/candidate pair in the arithmetic model.

theorem PointwiseComposition.FailureOfComposition.SigmaOneSearch.candidateSearch_sound {M : Type u_1} [FFL.ORingStructure M] [M↓[ℒₒᵣ] ⊧* 𝐏𝐀] [M↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] (c : ProgramGraph.PCode) (x a : M) (h : ProgramGraph.Computes (candidateSearch c) x a) : ProgramGraph.Computes c ⟪a, x⟫ 0

Every returned candidate is accepted by the original semidecision program.

theorem PointwiseComposition.FailureOfComposition.SigmaOneSearch.candidateSearch_domain {M : Type u_1} [FFL.ORingStructure M] [M↓[ℒₒᵣ] ⊧* 𝐏𝐀] [M↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] (c : ProgramGraph.PCode) (x : M) : (∃ (a : M), ProgramGraph.Computes (candidateSearch c) x a) ↔ ∃ (a : M), ProgramGraph.Computes c ⟪a, x⟫ 0

Fair search terminates if and only if an accepted candidate exists.

theorem PointwiseComposition.FailureOfComposition.SigmaOneSearch.computes_existsProgram {M : Type u_1} [FFL.ORingStructure M] [M↓[ℒₒᵣ] ⊧* 𝐏𝐀] [M↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] (c : ProgramGraph.PCode) (x y : M) : ProgramGraph.Computes (existsProgram c) x y ↔ y = 0 ∧ ∃ (a : M), ProgramGraph.Computes c ⟪a, x⟫ 0

Existential quantification of a semidecision predicate, with output zero.

theorem PointwiseComposition.FailureOfComposition.SigmaOneSearch.candidateSearch_of_functional {M : Type u_1} [FFL.ORingStructure M] [M↓[ℒₒᵣ] ⊧* 𝐏𝐀] [M↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] (c : ProgramGraph.PCode) (x a : M) (hunique : ∀ (b d : M), ProgramGraph.Computes c ⟪b, x⟫ 0 → ProgramGraph.Computes c ⟪d, x⟫ 0 → b = d) : ProgramGraph.Computes (candidateSearch c) x a ↔ ProgramGraph.Computes c ⟪a, x⟫ 0

With at most one accepted candidate, witness selection realizes the full functional relation, rather than merely choosing some accepted candidate.

theorem PointwiseComposition.FailureOfComposition.SigmaOneSearch.computes_unionProgram {M : Type u_1} [FFL.ORingStructure M] [M↓[ℒₒᵣ] ⊧* 𝐏𝐀] [M↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] (c d : ProgramGraph.PCode) (x y : M) : ProgramGraph.Computes (unionProgram c d) x y ↔ y = 0 ∧ (ProgramGraph.Computes c x 0 ∨ ProgramGraph.Computes d x 0)

Fair disjunction of semidecision predicates, with output zero.