Greedy parity search with an encoded context

The selector and greedy program are those of GreedyParitySearch; this module supplies one native machine for a counter on (context, rows). The context is part of every live state and counter input. Its encoding is charged even when candidate enumeration or the outer loop is empty. This closes the fixed-counter interface gap without constructing the common-zero counter or the initial Tanner matrix of [OAI26c], §§6.2–6.3 (pp. 42–43).

Main definitions

• GreedyContext.selectCertificate: uniform context-dependent candidate selection.
• GreedyContext.greedyCertificate: the existing greedyParityRows on a runtime context.

Main results

• GreedyContext.computableInO_greedy: independent time and polynomial-workspace bounds.
• GreedyContext.count_greedy_eq_card_sat: the fixed-counter correctness theorem pointwise.

References

• OpenAI, The Exponential Time Hypothesis is False, §§6.2–6.3.

The certificate construction extends Anton Kovsharov's GreedyParitySearch implementation.

def Cslib.Logic.PL.CNF.GreedyContext.encInput {C : Type} (encC : C ↪ List Bool) : C × ℕ × ℕ × List (List Bool) ↪ List Bool

Full selector input: context, unary width and tuple length, and retained rows.

def Cslib.Logic.PL.CNF.GreedyContext.encGreedyInput {C : Type} (encC : C ↪ List Bool) : C × ℕ × ℕ × ℕ × List (List Bool) ↪ List Bool

Full greedy input: context, unary round parameter, width and tuple length, and rows.

noncomputable def Cslib.Logic.PL.CNF.GreedyContext.selectCertificate {C : Type} {encC : C ↪ List Bool} {count : C × List (List Bool) → ℕ} (cCount : GenericRAM.NativeCertificate count (Turing.MultiTapeTM.encPair encC (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits)) Turing.MultiTapeTM.encNat) : GenericRAM.NativeCertificate (fun (a : C × ℕ × ℕ × List (List Bool)) => selectBestTestRow (fun (rows : List (List Bool)) => count (a.1, rows)) a.2.1 a.2.2.1 a.2.2.2) (encInput encC) Turing.MultiTapeTM.encBits

One fixed native selector for all encoded contexts. Empty candidate spaces return the zero row, exactly as selectBestTestRow; otherwise its first-minimum semantics are unchanged.

noncomputable def Cslib.Logic.PL.CNF.GreedyContext.greedyCertificate {C : Type} {encC : C ↪ List Bool} {count : C × List (List Bool) → ℕ} (cCount : GenericRAM.NativeCertificate count (Turing.MultiTapeTM.encPair encC (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits)) Turing.MultiTapeTM.encNat) : GenericRAM.NativeCertificate (fun (a : C × ℕ × ℕ × ℕ × List (List Bool)) => greedyParityRows (fun (rows : List (List Bool)) => count (a.1, rows)) a.2.1 a.2.2.1 a.2.2.2.1 a.2.2.2.2) (encGreedyInput encC) (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits)

One fixed machine runs 3n greedy rounds for the runtime context. The context survives every candidate and round; the returned rows are the original greedyParityRows specialization.

theorem Cslib.Logic.PL.CNF.GreedyContext.count_greedy_eq_card_sat {C : Type} {V : Type u_1} [Fintype V] [DecidableEq V] (count : C × List (List Bool) → ℕ) (c : C) (φ : CNF V) {P : ℕ} (hn : 1 ≤ Fintype.card V) (hP : 1 ≤ P) {initRows : List (List Bool)} (hinit_len : ∀ r ∈ initRows, r.length = List.length φ) (hcount : ∀ (rows : List (List Bool)), (∀ r ∈ rows, r.length = List.length φ) → rows.length ≤ initRows.length + 3 * Fintype.card V → (∀ r ∈ rows, r ∈ initRows ∨ List.count true r ≤ P) → count (c, rows) = BitString.numPassing φ.violations (List.map (BitString.ofList (List.length φ)) rows)) (hinit : ∀ (σ : V → Bool), BitString.PassesTests φ.violations (List.map (BitString.ofList (List.length φ)) initRows) σ → eval σ φ = false → List.length φ ≤ P * BitString.weight (φ.violations σ)) : count (c, greedyParityRows (fun (rows : List (List Bool)) => count (c, rows)) (Fintype.card V) (List.length φ) P initRows) = {σ : V → Bool | eval σ φ = true}.card

The existing Lemma 6.2 correctness theorem, specialized at a runtime context. Positivity, initial support, and counter agreement on the stated bounded candidate systems are essential. This statement constructs neither that counter nor the initial rows.

theorem Cslib.Logic.PL.CNF.GreedyContext.computableInO_select {C : Type} {encC : C ↪ List Bool} {count : C × List (List Bool) → ℕ} (cCount : GenericRAM.NativeCertificate count (Turing.MultiTapeTM.encPair encC (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits)) Turing.MultiTapeTM.encNat) (hSpace : Turing.MultiTapeTM.PolyBounded (fun (r : C × List (List Bool)) => ((Turing.MultiTapeTM.encPair encC (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits)) r).length) cCount.space) (R : C × ℕ × ℕ × List (List Bool) → ℕ) (hR : ∀ (a : C × ℕ × ℕ × List (List Bool)), ∀ j ≤ candidateTupleCount a.2.1 a.2.2.1, cCount.time (a.1, a.2.2.2 ++ [materializeTestRow a.2.1 (decodeTestTuple a.2.1 a.2.2.1 j)]) ≤ R a) : ∃ (poly : ℕ → ℕ), PolynomiallyBounded poly ∧ Turing.MultiTapeTM.ComputableInO (fun (a : C × ℕ × ℕ × List (List Bool)) => selectBestTestRow (fun (r : List (List Bool)) => count (a.1, r)) a.2.1 a.2.2.1 a.2.2.2) (encInput encC) Turing.MultiTapeTM.encBits (fun (a : C × ℕ × ℕ × List (List Bool)) => (candidateTupleCount a.2.1 a.2.2.1 + 1) * (poly ((encInput encC) a).length + R a)) fun (a : C × ℕ × ℕ × List (List Bool)) => poly ((encInput encC) a).length

Uniform selector time and polynomial workspace, measured in the full context/input encoding. The counter-time premise includes j = (2m)^P: the native iterator uses inclusive prefix maxima, so this endpoint is charged even though that candidate is not executed.

theorem Cslib.Logic.PL.CNF.GreedyContext.computableInO_greedy {C : Type} {encC : C ↪ List Bool} {count : C × List (List Bool) → ℕ} (cCount : GenericRAM.NativeCertificate count (Turing.MultiTapeTM.encPair encC (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits)) Turing.MultiTapeTM.encNat) (hSpace : Turing.MultiTapeTM.PolyBounded (fun (r : C × List (List Bool)) => ((Turing.MultiTapeTM.encPair encC (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits)) r).length) cCount.space) (R : C × ℕ × ℕ × ℕ × List (List Bool) → ℕ) (hR : ∀ (a : C × ℕ × ℕ × ℕ × List (List Bool)), ∀ i ≤ 3 * a.2.1, ∀ j ≤ candidateTupleCount a.2.2.1 a.2.2.2.1, cCount.time (a.1, greedyParityRowsAt (fun (r : List (List Bool)) => count (a.1, r)) a.2.2.1 a.2.2.2.1 a.2.2.2.2 i ++ [materializeTestRow a.2.2.1 (decodeTestTuple a.2.2.1 a.2.2.2.1 j)]) ≤ R a) : ∃ (poly : ℕ → ℕ), PolynomiallyBounded poly ∧ Turing.MultiTapeTM.ComputableInO (fun (a : C × ℕ × ℕ × ℕ × List (List Bool)) => greedyParityRows (fun (r : List (List Bool)) => count (a.1, r)) a.2.1 a.2.2.1 a.2.2.2.1 a.2.2.2.2) (encGreedyInput encC) (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits) (fun (a : C × ℕ × ℕ × ℕ × List (List Bool)) => (3 * a.2.1 + 1) * (candidateTupleCount a.2.2.1 a.2.2.2.1 + 1) * (poly ((encGreedyInput encC) a).length + R a)) fun (a : C × ℕ × ℕ × ℕ × List (List Bool)) => poly ((encGreedyInput encC) a).length

One uniform machine and polynomial for all encoded contexts, with independent native time O((3n + 1) ((2m)^P + 1) (poly(L) + R)) and workspace O(poly(L)), where L is the full context/input encoding length. The binary clock, retained rows/context, incumbent count, and final output are charged; workspace is not multiplied by either loop length.

The inclusive resource maxima require hR also at i = 3n and j = (2m)^P. These are resource obligations on extra endpoint candidates, not extra calls in the executable program. In particular, their row-length bound can exceed the correctness theorem's candidate bound by one. Polynomial counter workspace is a separate, global joint-input assumption; counter time need not be polynomial. This supplies the context interface for [OAI26c], §6.3, not its common-zero counter.

theorem Cslib.Logic.PL.CNF.GreedyContext.computableInPolySpace_greedy {C : Type} {encC : C ↪ List Bool} {count : C × List (List Bool) → ℕ} (cCount : GenericRAM.NativeCertificate count (Turing.MultiTapeTM.encPair encC (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits)) Turing.MultiTapeTM.encNat) (hSpace : Turing.MultiTapeTM.PolyBounded (fun (r : C × List (List Bool)) => ((Turing.MultiTapeTM.encPair encC (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits)) r).length) cCount.space) : Turing.MultiTapeTM.ComputableInPolySpace (fun (a : C × ℕ × ℕ × ℕ × List (List Bool)) => greedyParityRows (fun (r : List (List Bool)) => count (a.1, r)) a.2.1 a.2.2.1 a.2.2.2.1 a.2.2.2.2) (encGreedyInput encC) (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits)

Whenever cCount uses polynomial workspace, greedyParityRows runs in polynomial space.