Runtime greedy parity-row search for CNF formulas

In §6 and Lemma 6.2 of [OAI26c] (pp. 40, 42), given an initial parity-check matrix where every passing nonsatisfying assignment violates at least m / P clauses, a deterministic greedy loop runs for 3n rounds, streaming all (2m)^P tuples γ ∈ ([m] × {0, 1})^P via Cslib.GenericRAM.IndexFold.run, materializing h_γ mod 2, and—whenever the candidate space is nonempty (0 < candidateTupleCount m P)—appending the first candidate in enumeration order minimizing countSys (rows ++ [h_γ]) (falling back to the length-m zero row List.replicate m false when candidateTupleCount m P = 0, i.e., m = 0 and P > 0).

Scope and fixed-counter quantifier

In the native certificate and complexity API (selectBestStepCertificate, selectBestTestRowCertificate, greedyParityRowsCertificate, computableInO_selectBestTestRow, computableInO_greedyParityRows, computableInPolySpace_greedyParityRows), the candidate counter countSys : List (List Bool) → ℕ and its certificate cCount : NativeCertificate countSys (encList encBits) encNat are fixed before the runtime inputs (m, P, rows) / (n, m, P, rows). Neither the original CNF formula φ nor an arbitrary encoded context is a runtime input to this machine: choosing a separate countSys per φ allows a different machine and polynomial bound per φ. Uniform composition with a variable-CNF Theorem 2.2 common-zero counter therefore requires a captured-context certificate interface—for example, a counter on (context, rows) whose encoded context is retained and charged throughout IndexFold and the outer 3n-round loop.

Main definitions

• Cslib.Logic.PL.CNF.candidateTupleCount, Cslib.Logic.PL.CNF.encodeTestTuple, Cslib.Logic.PL.CNF.decodeTestTuple, Cslib.Logic.PL.CNF.materializeTestRow: base-2m codec and length-m mod-2 parity-test row materializer.
• Cslib.Logic.PL.CNF.selectBestTestRow, Cslib.Logic.PL.CNF.greedyParityRows, Cslib.Logic.PL.CNF.selectBestTestRowCertificate, Cslib.Logic.PL.CNF.greedyParityRowsCertificate: streaming selector, 3n-round greedy loop, and fixed-counter native certificates.

Main results

• Cslib.Logic.PL.CNF.decodeTestTuple_encodeTestTuple, Cslib.Logic.PL.CNF.encodeTestTuple_decodeTestTuple, Cslib.Logic.PL.CNF.mem_map_decodeTestTuple_range, Cslib.Logic.PL.CNF.length_materializeTestRow, Cslib.Logic.PL.CNF.count_true_materializeTestRow_le, Cslib.Logic.PL.CNF.materializeTestRow_ofFn: base-2m bijection, weight ≤ P, and testRow.
• Cslib.Logic.PL.CNF.computableInPolyTime_candidateTupleCount, Cslib.Logic.PL.CNF.computableInPolyTime_decodeTestTuple, Cslib.Logic.PL.CNF.computableInPolyTime_materializeTestRow: plain polynomial-time certificates.
• Cslib.Logic.PL.CNF.exists_min_index_selectBestTestRow, Cslib.Logic.PL.CNF.countSys_selectBestTestRow_le, Cslib.Logic.PL.CNF.countSys_greedyParityRows_eq_card_sat, Cslib.Logic.PL.CNF.numPassing_greedyParityRows_fin: nonempty-space (0 < candidateTupleCount m P) tie-breaking, minimality, and Lemma 6.2 under hn : 1 ≤ Fintype.card V and hP : 1 ≤ P.
• Cslib.Logic.PL.CNF.computableInO_selectBestTestRow, Cslib.Logic.PL.CNF.computableInO_greedyParityRows, Cslib.Logic.PL.CNF.computableInPolySpace_greedyParityRows: fixed-counter native time and workspace bounds.

References

• OpenAI, The Exponential Time Hypothesis is False, §6, §6.2 Lemma 6.2, §6.3

Candidate-tuple count and base-2m tuple decoding

def Cslib.Logic.PL.CNF.candidateTupleCount (m P : ℕ) : ℕ

Number (2 * m) ^ P of ordered candidate lists γ ∈ ([m] × {0, 1})^P (Lemma 6.2, p. 42).

@[simp]

theorem Cslib.Logic.PL.CNF.candidateTupleCount_zero_right (m : ℕ) : candidateTupleCount m 0 = 1

@[simp]

theorem Cslib.Logic.PL.CNF.candidateTupleCount_zero_left {P : ℕ} (hP : 1 ≤ P) : candidateTupleCount 0 P = 0

theorem Cslib.Logic.PL.CNF.length_encNat_candidateTupleCount_le (m P : ℕ) : (Turing.MultiTapeTM.encNat (candidateTupleCount m P)).length ≤ P * (2 * m) + 1

The binary encoding of (2 * m) ^ P has bit-length at most P * (2 * m) + 1.

theorem Cslib.Logic.PL.CNF.computableInPolyTime_candidateTupleCount : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : ℕ × ℕ) => candidateTupleCount p.1 p.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) Turing.MultiTapeTM.encNat

candidateTupleCount m P is computable in polynomial time in binary from unary (m, P).

theorem Cslib.Logic.PL.CNF.computableInPolyTime_candidateTupleCount' {α : Type} {input : α ↪ List Bool} {m P : α → ℕ} (hm : Turing.MultiTapeTM.ComputableInPolyTime m input Turing.MultiTapeTM.encUnary) (hP : Turing.MultiTapeTM.ComputableInPolyTime P input Turing.MultiTapeTM.encUnary) : Turing.MultiTapeTM.ComputableInPolyTime (fun (a : α) => candidateTupleCount (m a) (P a)) input Turing.MultiTapeTM.encNat

def Cslib.Logic.PL.CNF.decodeTestTuple (m P j : ℕ) : List (ℕ × Bool)

Decode a binary candidate index j : ℕ in base 2 * m into ((e₁, c₁), …, (e_P, c_P)) via Cslib.Radix.digit without materializing (2 * m) ^ P lists ([OAI26c], §6, p. 40; Lemma 6.2, p. 42). At m = 0, digits default to 0 so clause indices remain bounded in unary.

def Cslib.Logic.PL.CNF.encodeTestTuple (m : ℕ) (γ : List (ℕ × Bool)) : ℕ

Little-endian base-2m encoder inverse to decodeTestTuple m P on lists with clause indices < m, defined via Nat.ofDigits (2 * m).

@[simp]

theorem Cslib.Logic.PL.CNF.decodeTestTuple_zero_right (m j : ℕ) : decodeTestTuple m 0 j = []

@[simp]

theorem Cslib.Logic.PL.CNF.length_decodeTestTuple (m P j : ℕ) : (decodeTestTuple m P j).length = P

theorem Cslib.Logic.PL.CNF.fst_lt_of_mem_decodeTestTuple {m P j : ℕ} (hm : 1 ≤ m) {p : ℕ × Bool} (hp : p ∈ decodeTestTuple m P j) : p.1 < m

Every pair (e, c) produced by decodeTestTuple m P j satisfies e < m when 1 ≤ m.

theorem Cslib.Logic.PL.CNF.encodeTestTuple_lt {m : ℕ} {γ : List (ℕ × Bool)} (hγ : ∀ p ∈ γ, p.1 < m) : encodeTestTuple m γ < candidateTupleCount m γ.length

Encoding any list γ with clause indices < m yields an index < (2 * m) ^ γ.length.

theorem Cslib.Logic.PL.CNF.decodeTestTuple_encodeTestTuple {m : ℕ} {γ : List (ℕ × Bool)} (hγ : ∀ p ∈ γ, p.1 < m) : decodeTestTuple m γ.length (encodeTestTuple m γ) = γ

Decoding the index of any valid list γ recovers γ exactly.

theorem Cslib.Logic.PL.CNF.encodeTestTuple_decodeTestTuple {m P j : ℕ} (hj : j < candidateTupleCount m P) : encodeTestTuple m (decodeTestTuple m P j) = j

Encoding the decoded tuple of any j < (2 * m) ^ P recovers j.

theorem Cslib.Logic.PL.CNF.mem_map_decodeTestTuple_range {m P : ℕ} (γ : Fin P → Fin m × Bool) : (List.ofFn fun (r : Fin P) => (↑(γ r).1, (γ r).2)) ∈ List.map (decodeTestTuple m P) (List.range (candidateTupleCount m P))

Completeness of decodeTestTuple m P over List.range ((2 * m) ^ P).

theorem Cslib.Logic.PL.CNF.exists_fin_of_lt_candidateTupleCount {m P j : ℕ} (hj : j < candidateTupleCount m P) : ∃ (γ : Fin P → Fin m × Bool), decodeTestTuple m P j = List.ofFn fun (r : Fin P) => (↑(γ r).1, (γ r).2)

Every valid candidate index j < (2 * m) ^ P decodes to a typed γ : Fin P → Fin m × Bool.

theorem Cslib.Logic.PL.CNF.computableInPolyTime_decodeTestTuple : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : (ℕ × ℕ) × ℕ) => decodeTestTuple p.1.1 p.1.2 p.2) (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) Turing.MultiTapeTM.encNat) (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBool))

decodeTestTuple m P j is computable in polynomial time from unary (m, P) and binary j.

theorem Cslib.Logic.PL.CNF.computableInPolyTime_decodeTestTuple' {α : Type} {input : α ↪ List Bool} {m P j : α → ℕ} (hm : Turing.MultiTapeTM.ComputableInPolyTime m input Turing.MultiTapeTM.encUnary) (hP : Turing.MultiTapeTM.ComputableInPolyTime P input Turing.MultiTapeTM.encUnary) (hj : Turing.MultiTapeTM.ComputableInPolyTime j input Turing.MultiTapeTM.encNat) : Turing.MultiTapeTM.ComputableInPolyTime (fun (a : α) => decodeTestTuple (m a) (P a) (j a)) input (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBool))

Mod-2 row materialization

def Cslib.Logic.PL.CNF.materializeTestRow (m : ℕ) (γ : List (ℕ × Bool)) : List Bool

Materialize the length-m binary row h_γ from a test list γ, summing coefficients c_r modulo 2 (xor) across occurrences of e ([OAI26c], §6, p. 40; Lemma 6.2, p. 42).

@[simp]

theorem Cslib.Logic.PL.CNF.length_materializeTestRow (m : ℕ) (γ : List (ℕ × Bool)) : (materializeTestRow m γ).length = m

theorem Cslib.Logic.PL.CNF.materializeTestRow_ofFn {m P : ℕ} (γ : Fin P → Fin m × Bool) : materializeTestRow m (List.ofFn fun (r : Fin P) => (↑(γ r).1, (γ r).2)) = List.ofFn (BitString.testRow γ)

Exact bridge to Cslib.BitString.testRow on γ : Fin P → Fin m × Bool.

theorem Cslib.Logic.PL.CNF.count_true_materializeTestRow_le (m : ℕ) (γ : List (ℕ × Bool)) : List.count true (materializeTestRow m γ) ≤ γ.length

Every materialized row has at most γ.length ones (fewer when repeated indices cancel).

theorem Cslib.Logic.PL.CNF.count_true_materializeTestRow_decodeTestTuple_le (m P j : ℕ) : List.count true (materializeTestRow m (decodeTestTuple m P j)) ≤ P

Every decoded candidate row for (m, P) has Hamming weight at most P.

theorem Cslib.Logic.PL.CNF.computableInPolyTime_materializeTestRow : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : ℕ × List (ℕ × Bool)) => materializeTestRow p.1 p.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBool))) Turing.MultiTapeTM.encBits

materializeTestRow is computable in polynomial time from unary m and (e, c) pairs.

theorem Cslib.Logic.PL.CNF.computableInPolyTime_materializeTestRow' {α : Type} {input : α ↪ List Bool} {m : α → ℕ} {γ : α → List (ℕ × Bool)} (hm : Turing.MultiTapeTM.ComputableInPolyTime m input Turing.MultiTapeTM.encUnary) (hγ : Turing.MultiTapeTM.ComputableInPolyTime γ input (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBool))) : Turing.MultiTapeTM.ComputableInPolyTime (fun (a : α) => materializeTestRow (m a) (γ a)) input Turing.MultiTapeTM.encBits

Streaming (2m)^P min-count selector and 3n-round greedy loop

@[reducible, inline]

abbrev Cslib.Logic.PL.CNF.SelectBestAcc : Type

Live streaming accumulator: (m, P), rows, and optional (bestRow, bestVal).

def Cslib.Logic.PL.CNF.selectBestStep (countSys : List (List Bool) → ℕ) (state : ℕ × SelectBestAcc) : SelectBestAcc

Callback body of IndexFold.run for candidate index j, replacing the incumbent only on strict improvement candVal < best.2 ([OAI26c], Lemma 6.2, p. 42).

def Cslib.Logic.PL.CNF.selectBestTestRow (countSys : List (List Bool) → ℕ) (m P : ℕ) (rows : List (List Bool)) : List Bool

Stream j ∈ 0 .. (2 * m) ^ P - 1 via Cslib.GenericRAM.IndexFold.run: when the candidate space is nonempty (0 < candidateTupleCount m P), select the first candidate parity-test row in enumeration order attaining the minimum of countSys (rows ++ [h_γ]); if candidateTupleCount m P = 0 (m = 0, P > 0), return the total fallback length-m zero row List.replicate m false.

def Cslib.Logic.PL.CNF.greedyParityRowsAt (countSys : List (List Bool) → ℕ) (m P : ℕ) (initRows : List (List Bool)) (i : ℕ) : List (List Bool)

Prefix sequence of rows after i greedy rounds from initRows.

def Cslib.Logic.PL.CNF.greedyParityRows (countSys : List (List Bool) → ℕ) (n m P : ℕ) (initRows : List (List Bool)) : List (List Bool)

Append 3 * n greedily selected parity-test rows of list length P and width m, starting from initRows ([OAI26c], Lemma 6.2, p. 42).

@[simp]

theorem Cslib.Logic.PL.CNF.greedyParityRowsAt_zero (countSys : List (List Bool) → ℕ) (m P : ℕ) (initRows : List (List Bool)) : greedyParityRowsAt countSys m P initRows 0 = initRows

theorem Cslib.Logic.PL.CNF.greedyParityRowsAt_succ (countSys : List (List Bool) → ℕ) (m P : ℕ) (initRows : List (List Bool)) (i : ℕ) : greedyParityRowsAt countSys m P initRows (i + 1) = greedyParityRowsAt countSys m P initRows i ++ [selectBestTestRow countSys m P (greedyParityRowsAt countSys m P initRows i)]

Prefix invariant, tie-breaking, and minimality

theorem Cslib.Logic.PL.CNF.exists_min_index_selectBestTestRow (countSys : List (List Bool) → ℕ) {m P : ℕ} (rows : List (List Bool)) (hpos : 0 < candidateTupleCount m P) : ∃ jStar < candidateTupleCount m P, selectBestTestRow countSys m P rows = materializeTestRow m (decodeTestTuple m P jStar) ∧ (∀ j < candidateTupleCount m P, countSys (rows ++ [materializeTestRow m (decodeTestTuple m P jStar)]) ≤ countSys (rows ++ [materializeTestRow m (decodeTestTuple m P j)])) ∧ ∀ j < jStar, countSys (rows ++ [materializeTestRow m (decodeTestTuple m P jStar)]) < countSys (rows ++ [materializeTestRow m (decodeTestTuple m P j)])

Enumeration-order tie-breaking characterization of selectBestTestRow when (2 * m) ^ P > 0: jStar < (2 * m) ^ P attains the minimum count and strictly beats every j < jStar.

@[simp]

theorem Cslib.Logic.PL.CNF.length_selectBestTestRow (countSys : List (List Bool) → ℕ) (m P : ℕ) (rows : List (List Bool)) : (selectBestTestRow countSys m P rows).length = m

theorem Cslib.Logic.PL.CNF.count_true_selectBestTestRow_le (countSys : List (List Bool) → ℕ) (m P : ℕ) (rows : List (List Bool)) : List.count true (selectBestTestRow countSys m P rows) ≤ P

The selected parity-test row has Hamming weight (count true) at most P.

theorem Cslib.Logic.PL.CNF.countSys_selectBestTestRow_le (countSys : List (List Bool) → ℕ) {m P : ℕ} (rows : List (List Bool)) (γ : Fin P → Fin m × Bool) : countSys (rows ++ [selectBestTestRow countSys m P rows]) ≤ countSys (rows ++ [List.ofFn (BitString.testRow γ)])

Minimality over all test tuples γ : Fin P → Fin m × Bool.

theorem Cslib.Logic.PL.CNF.exists_fin_selectBestTestRow (countSys : List (List Bool) → ℕ) {m P : ℕ} (rows : List (List Bool)) (hpos : 0 < candidateTupleCount m P) : ∃ (γ : Fin P → Fin m × Bool), selectBestTestRow countSys m P rows = List.ofFn (BitString.testRow γ)

Whenever (2 * m) ^ P > 0, selectBestTestRow equals List.ofFn (testRow γ) for some γ.

Row counts, widths, weights, and CNF bridge for greedyParityRows

@[simp]

theorem Cslib.Logic.PL.CNF.length_greedyParityRowsAt (countSys : List (List Bool) → ℕ) (m P : ℕ) (initRows : List (List Bool)) (i : ℕ) : (greedyParityRowsAt countSys m P initRows i).length = initRows.length + i

@[simp]

theorem Cslib.Logic.PL.CNF.length_greedyParityRows (countSys : List (List Bool) → ℕ) (n m P : ℕ) (initRows : List (List Bool)) : (greedyParityRows countSys n m P initRows).length = initRows.length + 3 * n

theorem Cslib.Logic.PL.CNF.length_of_mem_greedyParityRowsAt (countSys : List (List Bool) → ℕ) {m P : ℕ} {initRows : List (List Bool)} (hinit : ∀ r ∈ initRows, r.length = m) (i : ℕ) {r : List Bool} (hr : r ∈ greedyParityRowsAt countSys m P initRows i) : r.length = m

theorem Cslib.Logic.PL.CNF.length_of_mem_greedyParityRows (countSys : List (List Bool) → ℕ) {n m P : ℕ} {initRows : List (List Bool)} (hinit : ∀ r ∈ initRows, r.length = m) {r : List Bool} (hr : r ∈ greedyParityRows countSys n m P initRows) : r.length = m

theorem Cslib.Logic.PL.CNF.length_encList_greedyParityRowsAt (countSys : List (List Bool) → ℕ) (m P : ℕ) (initRows : List (List Bool)) (i : ℕ) : ((Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits) (greedyParityRowsAt countSys m P initRows i)).length = ((Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits) initRows).length + i * (2 * m + 1)

theorem Cslib.Logic.PL.CNF.countSys_greedyParityRows_eq_card_sat {V : Type u_1} [Fintype V] [DecidableEq V] (φ : CNF V) {P : ℕ} (hn : 1 ≤ Fintype.card V) (hP : 1 ≤ P) {countSys : List (List Bool) → ℕ} {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) → countSys 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 σ)) : countSys (greedyParityRows countSys (Fintype.card V) (List.length φ) P initRows) = {σ : V → Bool | eval σ φ = true}.card

Exact bridge from greedyParityRows to CNF.numPassing_greedy ([OAI26c], Lemma 6.2). Under hn : 1 ≤ Fintype.card V and hP : 1 ≤ P, when initRows has row width φ.length, countSys computes numPassing φ.violations on width-φ.length candidate row lists of length at most initRows.length + 3 * Fintype.card V whose appended rows have weight ≤ P, and initRows satisfies Lemma 6.1's φ.length ≤ P * weight (φ.violations σ) bound, 3 * Fintype.card V greedy rounds yield countSys finalRows = #{σ : V → Bool | φ.eval σ = true}. Positivity is material: for V = Fin 0, φ = [[]], P = 1, initRows = [], and countSys given by numPassing, the agreement and support conditions hold, yet 0 rounds leave count 1 while #sat = 0.

theorem Cslib.Logic.PL.CNF.numPassing_greedyParityRows_fin {n P : ℕ} (φ : CNF (Fin n)) (hn : 1 ≤ n) (hP : 1 ≤ P) (initRows : List (List Bool)) (hinit_len : ∀ r ∈ initRows, r.length = List.length φ) (hinit : ∀ (σ : Fin n → Bool), BitString.PassesTests φ.violations (List.map (BitString.ofList (List.length φ)) initRows) σ → eval σ φ = false → List.length φ ≤ P * BitString.weight (φ.violations σ)) : have countSys := fun (rows : List (List Bool)) => BitString.numPassing φ.violations (List.map (BitString.ofList (List.length φ)) rows); have finalRows := greedyParityRows countSys n (List.length φ) P initRows; countSys finalRows = {σ : Fin n → Bool | eval σ φ = true}.card ∧ {σ : Fin n → Bool | BitString.PassesTests φ.violations (List.map (BitString.ofList (List.length φ)) finalRows) σ ∧ eval σ φ = false}.card = 0

Concrete Fin n specialization of Lemma 6.2: under hn : 1 ≤ n and hP : 1 ≤ P, 3 * n greedy rounds yield N(A) = #F and D(A) = 0.

Encodings for native IndexFold certificates

def Cslib.Logic.PL.CNF.encSelectBestAcc : SelectBestAcc ↪ List Bool

Binary encoding of the live streaming accumulator ((m, P), (rows, bestOpt)).

def Cslib.Logic.PL.CNF.encSelectBestIn : ℕ × ℕ × List (List Bool) ↪ List Bool

Input encoding for selectBestTestRow (and outer-loop state): unary (m, P) and rows.

def Cslib.Logic.PL.CNF.encGreedyIn : ℕ × ℕ × ℕ × List (List Bool) ↪ List Bool

Input encoding for greedyParityRows: unary (n, m, P) and framed bit-rows initRows.

Native IndexFold certificates and ComputableInO / ComputableInPolySpace bounds

def Cslib.Logic.PL.CNF.candRowOfState (s : ℕ × SelectBestAcc) : List Bool

Candidate test row decoded and materialized from an IndexFold state (j, acc).

theorem Cslib.Logic.PL.CNF.computableInPolyTime_candRowOfState : Turing.MultiTapeTM.ComputableInPolyTime candRowOfState (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encNat encSelectBestAcc) Turing.MultiTapeTM.encBits

def Cslib.Logic.PL.CNF.augCandidateRows (s : ℕ × SelectBestAcc) : List (List Bool)

Existing parity-test rows extended with the candidate row at IndexFold state s.

theorem Cslib.Logic.PL.CNF.computableInPolyTime_augCandidateRows : Turing.MultiTapeTM.ComputableInPolyTime augCandidateRows (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encNat encSelectBestAcc) (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits)

def Cslib.Logic.PL.CNF.finishSelectBestStep (p : (ℕ × SelectBestAcc) × ℕ) : SelectBestAcc

Update SelectBestAcc after evaluating the candidate score p.2 at IndexFold state p.1.

theorem Cslib.Logic.PL.CNF.computableInPolyTime_finishSelectBestStep : Turing.MultiTapeTM.ComputableInPolyTime finishSelectBestStep (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encNat encSelectBestAcc) Turing.MultiTapeTM.encNat) encSelectBestAcc

noncomputable def Cslib.Logic.PL.CNF.selectBestStepCertificate {countSys : List (List Bool) → ℕ} (cCount : GenericRAM.NativeCertificate countSys (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encNat) : GenericRAM.NativeCertificate (selectBestStep countSys) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encNat encSelectBestAcc) encSelectBestAcc

Native callback certificate for one candidate step selectBestStep countSys.

noncomputable def Cslib.Logic.PL.CNF.selectBestTestRowCertificate {countSys : List (List Bool) → ℕ} (cCount : GenericRAM.NativeCertificate countSys (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encNat) : GenericRAM.NativeCertificate (fun (a : ℕ × ℕ × List (List Bool)) => selectBestTestRow countSys a.1 a.2.1 a.2.2) encSelectBestIn Turing.MultiTapeTM.encBits

Native streaming machine certificate for selectBestTestRow via IndexFold.certificate, for a fixed counter (countSys, cCount) supplied before runtime inputs (m, P, rows).

noncomputable def Cslib.Logic.PL.CNF.greedyParityRowsCertificate {countSys : List (List Bool) → ℕ} (cCount : GenericRAM.NativeCertificate countSys (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encNat) : GenericRAM.NativeCertificate (fun (a : ℕ × ℕ × ℕ × List (List Bool)) => greedyParityRows countSys a.1 a.2.1 a.2.2.1 a.2.2.2) encGreedyIn (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits)

Native machine certificate for the 3 * n-round greedyParityRows procedure for a fixed counter (countSys, cCount).

Here countSys and cCount are fixed before the runtime inputs (n, m, P, rows) encoded by encGreedyIn; neither the original CNF nor an arbitrary encoded context is an input to this machine, and choosing a separate countSys per φ allows a different machine and polynomial per φ. Uniform composition with a variable-CNF Theorem 2.2 counter requires a captured-context certificate interface (such as a counter on (context, rows) retaining and charging context throughout the loop).

Live-state length bounds and ComputableInO / ComputableInPolySpace theorems

theorem Cslib.Logic.PL.CNF.length_encSelectBestAcc_run_le (countSys : List (List Bool) → ℕ) (m P k : ℕ) (rows : List (List Bool)) {V : ℕ} (hV : ∀ j < k, (Turing.MultiTapeTM.encNat (countSys (rows ++ [materializeTestRow m (decodeTestTuple m P j)]))).length ≤ V) : (encSelectBestAcc (GenericRAM.IndexFold.run (selectBestStep countSys) k ((m, P), rows, none)).2).length ≤ 6 * m + 2 * P + 2 * ((Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits) rows).length + V + 6

Live accumulator length bound during IndexFold.run (selectBestStep countSys), independent of the number k of visited candidates.

theorem Cslib.Logic.PL.CNF.computableInO_selectBestTestRow {countSys : List (List Bool) → ℕ} (cCount : GenericRAM.NativeCertificate countSys (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encNat) (hSpace : Turing.MultiTapeTM.PolyBounded (fun (r : List (List Bool)) => ((Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits) r).length) cCount.space) (R : ℕ × ℕ × List (List Bool) → ℕ) (hR : ∀ (a : ℕ × ℕ × List (List Bool)), ∀ j ≤ candidateTupleCount a.1 a.2.1, cCount.time (a.2.2 ++ [materializeTestRow a.1 (decodeTestTuple a.1 a.2.1 j)]) ≤ R a) : ∃ (poly : ℕ → ℕ), PolynomiallyBounded poly ∧ Turing.MultiTapeTM.ComputableInO (fun (a : ℕ × ℕ × List (List Bool)) => selectBestTestRow countSys a.1 a.2.1 a.2.2) encSelectBestIn Turing.MultiTapeTM.encBits (fun (a : ℕ × ℕ × List (List Bool)) => (candidateTupleCount a.1 a.2.1 + 1) * (poly (encSelectBestIn a).length + R a)) fun (a : ℕ × ℕ × List (List Bool)) => poly (encSelectBestIn a).length

Fixed-counter per-round ComputableInO time and polynomial-workspace bound for selectBestTestRow (with countSys and cCount fixed before runtime inputs (m, P, rows)).

theorem Cslib.Logic.PL.CNF.computableInO_greedyParityRows {countSys : List (List Bool) → ℕ} (cCount : GenericRAM.NativeCertificate countSys (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encNat) (hSpace : Turing.MultiTapeTM.PolyBounded (fun (r : List (List Bool)) => ((Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits) r).length) cCount.space) (R : ℕ × ℕ × ℕ × List (List Bool) → ℕ) (hR : ∀ (a : ℕ × ℕ × ℕ × List (List Bool)), ∀ i ≤ 3 * a.1, ∀ j ≤ candidateTupleCount a.2.1 a.2.2.1, cCount.time (greedyParityRowsAt countSys a.2.1 a.2.2.1 a.2.2.2 i ++ [materializeTestRow a.2.1 (decodeTestTuple a.2.1 a.2.2.1 j)]) ≤ R a) : ∃ (poly : ℕ → ℕ), PolynomiallyBounded poly ∧ Turing.MultiTapeTM.ComputableInO (fun (a : ℕ × ℕ × ℕ × List (List Bool)) => greedyParityRows countSys a.1 a.2.1 a.2.2.1 a.2.2.2) encGreedyIn (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits) (fun (a : ℕ × ℕ × ℕ × List (List Bool)) => (3 * a.1 + 1) * (candidateTupleCount a.2.1 a.2.2.1 + 1) * (poly (encGreedyIn a).length + R a)) fun (a : ℕ × ℕ × ℕ × List (List Bool)) => poly (encGreedyIn a).length

Fixed-counter 3n-round ComputableInO time and polynomial-workspace bound for greedyParityRows. For fixed countSys and cCount (supplied before runtime inputs (n, m, P, rows)), runs in time O((3 * n + 1) * ((2 * m) ^ P + 1) * (poly(|input|) + R)) and polynomial workspace O(poly(|input|)), never storing (2 * m) ^ P lists or counts ([OAI26c], §6.3, p. 43).

theorem Cslib.Logic.PL.CNF.computableInPolySpace_greedyParityRows {countSys : List (List Bool) → ℕ} (cCount : GenericRAM.NativeCertificate countSys (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encNat) (hSpace : Turing.MultiTapeTM.PolyBounded (fun (r : List (List Bool)) => ((Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits) r).length) cCount.space) : Turing.MultiTapeTM.ComputableInPolySpace (fun (a : ℕ × ℕ × ℕ × List (List Bool)) => greedyParityRows countSys a.1 a.2.1 a.2.2.1 a.2.2.2) encGreedyIn (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits)

For a fixed counter (countSys, cCount) using polynomial workspace, greedyParityRows runs in polynomial space on runtime inputs (n, m, P, rows).