Finite-search implementation of the revised normalization

def GenLimit.FiniteWitness.Simplified.samplePoints (S : Finset ℕ) (k : ℕ) : Finset ℕ

Executable first-k selection from the observed finite set.

Equations

• GenLimit.FiniteWitness.Simplified.samplePoints S k = {x ∈ S | {y ∈ S | y < x}.card < k}

theorem GenLimit.FiniteWitness.Simplified.samplePoints_eq (S : Finset ℕ) (k : ℕ) : samplePoints S k = firstPoints (↑S) k

def GenLimit.FiniteWitness.Simplified.codeWords (b : ℕ) : Finset (List ℕ)

Decode a finite initial segment of the fixed word codes.

Equations

• GenLimit.FiniteWitness.Simplified.codeWords b = Finset.image (fun (i : ℕ) => (Encodable.decode i).getD []) (Finset.range (b + 1))

theorem GenLimit.FiniteWitness.Simplified.mem_codeWords {q : List ℕ} {b : ℕ} (h : Encodable.encode q ≤ b) : q ∈ codeWords b

def GenLimit.FiniteWitness.Simplified.testCandidate (F : List ℕ → ℕ) (S : Finset ℕ) (p : List ℕ) (k : ℕ) (q : List ℕ) : Prop

Test a strict history extension that covers the next checkpoint and outputs outside the sample.

Equations

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

@[instance_reducible]

instance GenLimit.FiniteWitness.Simplified.instDecidableTestCandidate (F : List ℕ → ℕ) (S : Finset ℕ) (p : List ℕ) (k : ℕ) (q : List ℕ) : Decidable (testCandidate F S p k q)

Equations

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

theorem GenLimit.FiniteWitness.Simplified.testCandidate_iff (F : List ℕ → ℕ) (S : Finset ℕ) (p : List ℕ) (k : ℕ) (q : List ℕ) : testCandidate F S p k q ↔ Candidate naturalCheckpoints F S p k q

def GenLimit.FiniteWitness.Simplified.candidateCodes (F : List ℕ → ℕ) (S : Finset ℕ) (p : List ℕ) (k : ℕ) : Finset (List ℕ)

Search the bounded code interval for candidates extending the current history.

Equations

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

theorem GenLimit.FiniteWitness.Simplified.pick_candidate_eq {F : List ℕ → ℕ} (hF : Fresh F) {S : Finset ℕ} (hS : S.Nonempty) {p : List ℕ} (hp : p.toFinset ⊆ S) (k : ℕ) (hex : ∃ (q : List ℕ), Candidate naturalCheckpoints F S p k q) : pickWord (candidateCodes F S p k) = leastCode (Candidate naturalCheckpoints F S p k) hex

def GenLimit.FiniteWitness.Simplified.executableRun (F : List ℕ → ℕ) (S : Finset ℕ) : ℕ → List ℕ

Iterate finite candidate selection for the revised normalization.

Equations

• One or more equations did not get rendered due to their size.
• GenLimit.FiniteWitness.Simplified.executableRun F S 0 = []

theorem GenLimit.FiniteWitness.Simplified.executableRun_eq {F : List ℕ → ℕ} (hF : Fresh F) {S : Finset ℕ} (hS : S.Nonempty) (k : ℕ) : executableRun F S k = sampleRun naturalCheckpoints F S k

def GenLimit.FiniteWitness.Simplified.executableNormalized (F : List ℕ → ℕ) (S : Finset ℕ) : ℕ

Evaluate the history function after as many search steps as sample elements.

Equations

• GenLimit.FiniteWitness.Simplified.executableNormalized F S = F (GenLimit.FiniteWitness.Simplified.executableRun F S S.card)

theorem GenLimit.FiniteWitness.Simplified.executableNormalized_eq {F : List ℕ → ℕ} (hF : Fresh F) (S : Finset ℕ) : executableNormalized F S = normalized naturalCheckpoints F S

def GenLimit.FiniteWitness.Simplified.executableNormalization (G : Generic.Generator ℕ) (S : Finset ℕ) : ℕ

Apply the revised finite-search normalization after repairing repeated outputs.

Equations

• GenLimit.FiniteWitness.Simplified.executableNormalization G S = GenLimit.FiniteWitness.Simplified.executableNormalized (GenLimit.FiniteWitness.maxRepair G) S

theorem GenLimit.FiniteWitness.Simplified.executable_universal_normalization (G : Generic.Generator ℕ) (L : Set ℕ) : L.Infinite → (∀ (stream : Generic.Stream ℕ), Generic.Presents stream L → ∃ (N : ℕ), ∀ n ≥ N, Generic.CorrectAt G L stream n) → Locks (executableNormalization G) L

A terminating executable program for the new construction, not the old bounded one.