Integer measurements of Boolean words

Rows and matrices use the existing integer-list/table representations. Evaluation is total: missing bits are false, extra bits are ignored, and each row uses its own stored length. Matrix equality compares the complete output list, so a target with the wrong length cannot match. On rectangular inputs this agrees with the ordinary integer matrix/Boolean-vector product.

The unrestricted representative scan in [OAI26c], Lemma 3.2, printed pp. 22–23, searches for a word having the requested measurements. Fixed-bit restrictions belong to the later scan. This module supplies evaluation and that representative search, not the full counting identity.

Main definitions

• Cslib.LinearAlgebra.BooleanMeasurements.evalBoolRow: one signed integer measurement.
• Cslib.LinearAlgebra.BooleanMeasurements.evalBoolMatrix: all measurements in row order.
• Cslib.LinearAlgebra.BooleanMeasurements.test: full measurement-list equality.
• Cslib.LinearAlgebra.BooleanMeasurements.search: an unrestricted representative, if one exists.
• Cslib.LinearAlgebra.BooleanMeasurements.searchCertificate: native search with raw bit words.

Main results

• Cslib.LinearAlgebra.BooleanMeasurements.evalBoolMatrix_getD_eq_sum: finite-matrix semantics.
• Cslib.LinearAlgebra.BooleanMeasurements.evalBoolRow_polyTime, Cslib.LinearAlgebra.BooleanMeasurements.evalBoolMatrix_polyTime: native evaluation costs.
• Cslib.LinearAlgebra.BooleanMeasurements.search_some, Cslib.LinearAlgebra.BooleanMeasurements.search_eq_none_iff_cube: search correctness.
• Cslib.LinearAlgebra.BooleanMeasurements.exists_computableInO_search: traversal-proportional time and independent polynomial workspace, including encoding conversions.
• Cslib.LinearAlgebra.BooleanMeasurements.polyBounded_searchCertificate_space, Cslib.LinearAlgebra.BooleanMeasurements.exists_polyBounded_searchCertificate_time: composable bounds on the exported certificate itself.

References

• OpenAI, The Exponential Time Hypothesis is False, Lemma 3.2, pp. 22–23.

def Cslib.LinearAlgebra.BooleanMeasurements.evalBoolRow (row : List ℤ) (y : List Bool) : ℤ

Evaluate one integer row. Missing bits are false; bits beyond the row are ignored.

def Cslib.LinearAlgebra.BooleanMeasurements.evalBoolMatrix (M : List (List ℤ)) (y : List Bool) : List ℤ

Evaluate every stored row, including ragged inputs, in the original row order.

theorem Cslib.LinearAlgebra.BooleanMeasurements.evalBoolRow_eq_sum (row : List ℤ) (y : List Bool) : evalBoolRow row y = ∑ j ∈ Finset.range row.length, row.getD j 0 * BitString.bitVal ℤ (y.getD j false)

Row evaluation is the integer dot product with the padded Boolean word.

@[simp]

theorem Cslib.LinearAlgebra.BooleanMeasurements.length_evalBoolMatrix (M : List (List ℤ)) (y : List Bool) : (evalBoolMatrix M y).length = M.length

Evaluation preserves the number of rows, also for malformed/ragged tables.

theorem Cslib.LinearAlgebra.BooleanMeasurements.evalBoolMatrix_getD (M : List (List ℤ)) (y : List Bool) (i : ℕ) : (evalBoolMatrix M y).getD i 0 = evalBoolRow (M.getD i []) y

Total lookup of an evaluated row agrees with evaluating the total row lookup.

theorem Cslib.LinearAlgebra.BooleanMeasurements.evalBoolMatrix_ne_of_length_ne (M : List (List ℤ)) (y : List Bool) (target : List ℤ) (h : M.length ≠ target.length) : evalBoolMatrix M y ≠ target

A target of the wrong length cannot be the matrix's complete measurement vector.

theorem Cslib.LinearAlgebra.BooleanMeasurements.evalBoolMatrix_getD_eq_sum {M : List (List ℤ)} {r d : ℕ} (hM : IsTableShape r d M) (y : List Bool) (i : Fin r) : (evalBoolMatrix M y).getD (↑i) 0 = ∑ j : Fin d, rowEntry M ↑i ↑j * BitString.bitVal ℤ (y.getD (↑j) false)

On an (r,d) table, measurement i < r is the finite integer dot product. The word is still padded/truncated by the total convention; an exactly d-bit word needs no padding.

theorem Cslib.LinearAlgebra.BooleanMeasurements.evalBoolRow_polyTime : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : List ℤ × List Bool) => evalBoolRow p.1 p.2) (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin) Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encIntBin

One fixed native polynomial-time routine evaluates arbitrary signed rows and bit words.

theorem Cslib.LinearAlgebra.BooleanMeasurements.evalBoolMatrix_polyTime : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : List (List ℤ) × List Bool) => evalBoolMatrix p.1 p.2) (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin)) Turing.MultiTapeTM.encBits) (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin)

Evaluate a runtime matrix on a runtime Boolean word with polynomial native costs.

def Cslib.LinearAlgebra.BooleanMeasurements.test {C : Type} (matOf : C → List (List ℤ)) (targetOf : C → List ℤ) (p : C × List Bool) : Bool

Compare the complete measurement list to the target retained in the runtime context.

def Cslib.LinearAlgebra.BooleanMeasurements.search {C : Type} (matOf : C → List (List ℤ)) (targetOf : C → List ℤ) (p : C × ℕ) : Option (List Bool)

Search the unrestricted measurement fiber with the existing streaming first-match loop.

theorem Cslib.LinearAlgebra.BooleanMeasurements.search_some {C : Type} (matOf : C → List (List ℤ)) (targetOf : C → List ℤ) (p : C × ℕ) {y : List Bool} (h : search matOf targetOf p = some y) : y.length = p.2 ∧ evalBoolMatrix (matOf p.1) y = targetOf p.1

A returned representative has the requested width and exactly the requested measurements.

theorem Cslib.LinearAlgebra.BooleanMeasurements.length_search_le {C : Type} (matOf : C → List (List ℤ)) (targetOf : C → List ℤ) (p : C × ℕ) : ((Turing.MultiTapeTM.encOption Turing.MultiTapeTM.encBits) (search matOf targetOf p)).length ≤ p.2 + 1

The raw-bit optional representative has at most the declared width plus its option tag.

theorem Cslib.LinearAlgebra.BooleanMeasurements.search_eq_none_iff {C : Type} (matOf : C → List (List ℤ)) (targetOf : C → List ℤ) (p : C × ℕ) : search matOf targetOf p = none ↔ ∀ (y : List Bool), y.length = p.2 → evalBoolMatrix (matOf p.1) y ≠ targetOf p.1

Failure is equivalent to the unrestricted fiber being empty. This uses the total padding convention even for ragged matrices, rather than silently assuming rectangular input.

theorem Cslib.LinearAlgebra.BooleanMeasurements.test_polyTime {C : Type} {encC : C ↪ List Bool} {matOf : C → List (List ℤ)} {targetOf : C → List ℤ} (hM : Turing.MultiTapeTM.ComputableInPolyTime matOf encC (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin))) (ht : Turing.MultiTapeTM.ComputableInPolyTime targetOf encC (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin)) : Turing.MultiTapeTM.ComputableInPolyTime (test matOf targetOf) (Turing.MultiTapeTM.encPair encC Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool

The equality test is uniformly polynomial in the complete retained context and candidate word encodings, using the supplied polynomial matrix/target projections.

theorem Cslib.LinearAlgebra.BooleanMeasurements.search_eq_none_iff_cube {C : Type} (matOf : C → List (List ℤ)) (targetOf : C → List ℤ) (p : C × ℕ) : search matOf targetOf p = none ↔ ∀ (y : BitString p.2), evalBoolMatrix (matOf p.1) (List.ofFn y) ≠ targetOf p.1

Empty-fiber completeness stated on the ordinary finite Boolean cube.

theorem Cslib.LinearAlgebra.BooleanMeasurements.exists_computableInO_search {C : Type} {encC : C ↪ List Bool} {matOf : C → List (List ℤ)} {targetOf : C → List ℤ} (hM : Turing.MultiTapeTM.ComputableInPolyTime matOf encC (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin))) (ht : Turing.MultiTapeTM.ComputableInPolyTime targetOf encC (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin)) : ∃ (overhead : C × ℕ → ℕ) (workspace : C × ℕ → ℕ), Turing.MultiTapeTM.PolyBounded (fun (p : C × ℕ) => ((Turing.MultiTapeTM.encPair encC Turing.MultiTapeTM.encUnary) p).length) overhead ∧ Turing.MultiTapeTM.PolyBounded (fun (p : C × ℕ) => ((Turing.MultiTapeTM.encPair encC Turing.MultiTapeTM.encUnary) p).length) workspace ∧ Turing.MultiTapeTM.ComputableInO (search matOf targetOf) (Turing.MultiTapeTM.encPair encC Turing.MultiTapeTM.encUnary) (Turing.MultiTapeTM.encOption Turing.MultiTapeTM.encBits) (fun (p : C × ℕ) => (2 ^ p.2 + 1) * overhead p) workspace

The fixed native representative search has traversal-proportional time and polynomial charged workspace in the full runtime context/width encoding, including both codec boundaries.

noncomputable def Cslib.LinearAlgebra.BooleanMeasurements.searchCertificate {C : Type} {encC : C ↪ List Bool} {matOf : C → List (List ℤ)} {targetOf : C → List ℤ} (hM : Turing.MultiTapeTM.ComputableInPolyTime matOf encC (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin))) (ht : Turing.MultiTapeTM.ComputableInPolyTime targetOf encC (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin)) : GenericRAM.NativeCertificate (search matOf targetOf) (Turing.MultiTapeTM.encPair encC Turing.MultiTapeTM.encUnary) (Turing.MultiTapeTM.encOption Turing.MultiTapeTM.encBits)

Native representative search with the consumer's raw-bit option encoding, selecting the independent resource bounds above once, before any runtime context/width input. Both codec boundaries are included.

theorem Cslib.LinearAlgebra.BooleanMeasurements.polyBounded_searchCertificate_space {C : Type} {encC : C ↪ List Bool} {matOf : C → List (List ℤ)} {targetOf : C → List ℤ} (hM : Turing.MultiTapeTM.ComputableInPolyTime matOf encC (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin))) (ht : Turing.MultiTapeTM.ComputableInPolyTime targetOf encC (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin)) : Turing.MultiTapeTM.PolyBounded (fun (p : C × ℕ) => ((Turing.MultiTapeTM.encPair encC Turing.MultiTapeTM.encUnary) p).length) (searchCertificate hM ht).space

The exported certificate's actual charged workspace is polynomial in the full input.

theorem Cslib.LinearAlgebra.BooleanMeasurements.exists_polyBounded_searchCertificate_time {C : Type} {encC : C ↪ List Bool} {matOf : C → List (List ℤ)} {targetOf : C → List ℤ} (hM : Turing.MultiTapeTM.ComputableInPolyTime matOf encC (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin))) (ht : Turing.MultiTapeTM.ComputableInPolyTime targetOf encC (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin)) : ∃ (overhead : C × ℕ → ℕ), Turing.MultiTapeTM.PolyBounded (fun (p : C × ℕ) => ((Turing.MultiTapeTM.encPair encC Turing.MultiTapeTM.encUnary) p).length) overhead ∧ ∀ (p : C × ℕ), (searchCertificate hM ht).time p = (2 ^ p.2 + 1) * overhead p

The exported certificate's actual time has a fixed polynomial factor times the traversal count. Its encoded output is charged to its separate polynomial workspace bound.