diff --git a/Complexity.lean b/Complexity.lean index 09d6303a1..e7fd4eb86 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -961,6 +961,9 @@ public import Complexity.Computability.Circuit.Frontier.TensorNetwork.FastContra public import Complexity.Computability.Circuit.Frontier.TensorNetwork.FastContractionShape public import Complexity.Computability.Circuit.Frontier.TensorNetwork.FastContractionSize public import Complexity.Computability.Circuit.Frontier.TensorNetwork.FastContractionStep +public import Complexity.Computability.Circuit.Frontier.TensorNetwork.IncidenceEntry +public import Complexity.Computability.Circuit.Frontier.TensorNetwork.IncidenceEntryCertificate +public import Complexity.Computability.Circuit.Frontier.TensorNetwork.IncidenceEntryPolyTime public import Complexity.Computability.Circuit.Frontier.TensorNetwork.IncidenceNetwork public import Complexity.Computability.Circuit.Frontier.TensorNetwork.IncidenceNetworkBounds public import Complexity.Computability.Circuit.Frontier.TensorNetwork.IncidenceNetworkSize @@ -991,6 +994,7 @@ public import Complexity.Computability.Circuit.Frontier.TensorNetwork.TruncatedE public import Complexity.Computability.Circuit.Frontier.TensorNetwork.TruncatedPolyTime public import Complexity.Computability.Circuit.Frontier.TensorNetwork.TruncatedPolynomialEntries public import Complexity.Computability.Circuit.Frontier.TensorNetwork.TruncatedResources +public import Complexity.Computability.Circuit.Frontier.TensorNetwork.TruncatedRing public import Complexity.Computability.Circuit.Frontier.TensorNetwork.VertexDesc public import Complexity.Computability.Circuit.Frontier.TwoSidedWitness public import Complexity.Computability.Circuit.Frontier.Unconditional @@ -3202,6 +3206,7 @@ public import Complexity.Foundations.Data.BitString.AgreeExpect public import Complexity.Foundations.Data.BitString.Basic public import Complexity.Foundations.Data.BitString.Binary public import Complexity.Foundations.Data.BitString.Block +public import Complexity.Foundations.Data.BitString.Combination public import Complexity.Foundations.Data.BitString.Convolution public import Complexity.Foundations.Data.BitString.Counter public import Complexity.Foundations.Data.BitString.CoverCoding diff --git a/Complexity/Computability/Circuit/Frontier/TensorNetwork/IncidenceEntry.lean b/Complexity/Computability/Circuit/Frontier/TensorNetwork/IncidenceEntry.lean new file mode 100644 index 000000000..72df582a5 --- /dev/null +++ b/Complexity/Computability/Circuit/Frontier/TensorNetwork/IncidenceEntry.lean @@ -0,0 +1,264 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: candidate + +public import Complexity.Computability.Circuit.Frontier.TensorNetwork.IncidenceNetwork +public import Complexity.Computability.Circuit.Frontier.TensorNetwork.TruncatedRing +public import Complexity.Computability.Circuit.Frontier.TensorNetwork.VertexDesc +public import Complexity.Computability.PolyTime.ParityFactorEval +public import Complexity.Foundations.Data.BitString.Combination +public import Complexity.Foundations.Data.BitString.Enumeration + +/-! +# The entries of the incidence network of Lemma D.2 + +The incidence network of Lemma D.2 of [OpenAI2026ETH] (pp. 55–56, +`Cslib.Circuits.Frontier.IncidenceNetwork.network`) has three kinds of vertices: a row for each +test group, a column for each variable group, and fixed tables for padding. This file gives the +entry procedure `incEntry` of all three, with values in `B_{P,ℓ} = (ℤ / 2 ^ P)[V] / (V ^ ℓ)` as +coefficient lists (`GaloisRingArith` at the modulus `truncFl ℓ`, see +`Complexity/Computability/Circuit/Frontier/TensorNetwork/TruncatedRing.lean`), and the encoding +`encDesc` of the descriptors. + +**Indices.** The ports of a group vertex are the index wires of its blocks, in order. A block of +`N` incidences with `d` selected has `blockWires = ⌈log₂ C(N, d)⌉` wires. The entry reads the +bits block by block (`blockIndices`), each chunk as an index `ι` in little-endian order +(`BitString.lsbValue`). An index `ι < C(N, d)` names the weight-`d` subset of the block's +incidences at the `true` positions of the combination of rank `ι` +(`Cslib.BitString.unrankCombination`, `selectBlock`). The selected incidences of all +blocks are `selected`. + +**Rows** (`rowEntry`, p. 56). For the test group with tests `t`, an index `ι ≥ C(N, d)` in any +block gives the entry `0`. Otherwise let `S_t` be the variables selected for test `t`. The entry +is `∏_t c_t(S_t)` with `c_t(S) = ∑_{T ⊆ S} (-1) ^ (|S| - |T|) B(m_t(T); V)`, where `m_t(T)` is the +number of monomials of test `t` inside `T` (`monomialsIn`) and `B(y; V)` is the parity factor +`Polynomial.parityFactor ℓ y`, whose coefficient list modulo `2 ^ P` is `factorCoeffs` (from +`parityLinearCoeffs`, the linear remainders `e_j` of Lemma 5.1). The product of the subset sums +is one sum over the subsets of all selected incidences of the group: a word `w` on them +(`chosenBy`) contributes `(-1) ^ (|sel| - |w|) ∏_t B(m_t(T_t(w)); V)` (`rowTerm`, `rowBody`), and +the entry is the sum over all `2 ^ |sel|` words (`rowSum`), which the native machine streams. + +**Columns** (`colEntry`). For the variable group with variables `X_h`, the entry is the constant +`2 ^ u` modulo `2 ^ P`, for `u` the number of variables of `X_h` selected by no test +(`unselectedCount`). Columns read invalid indices too; the rows make those terms zero. + +**Tables** are read by `tableEntry`. + +The correctness of the contraction against the incidence expansion and the native certificate are +separate. + +## Main definitions + +* `Cslib.Circuits.Frontier.IncidenceNetwork.blockIndices`: the indices of the blocks. +* `Cslib.Circuits.Frontier.IncidenceNetwork.selected`: the selected incidences. +* `Cslib.Circuits.Frontier.IncidenceNetwork.factorCoeffs`: the parity factor in `B_{P,ℓ}`. +* `Cslib.Circuits.Frontier.IncidenceNetwork.rowEntry`, `colEntry`: the group entries. +* `Cslib.Circuits.Frontier.IncidenceNetwork.incEntry`: the entry procedure. +* `Cslib.Circuits.Frontier.IncidenceNetwork.encDesc`: the encoding of the descriptors. + +## References + +* [OpenAI, *The Exponential Time Hypothesis is False*][OpenAI2026ETH], Lemma 5.1 (p. 36) and + Lemma D.2 (pp. 54–56). +-/ + +public section + +namespace Cslib.Circuits.Frontier.IncidenceNetwork + +open GaloisRingArith Cslib.BitString Cslib.GenericRAM Turing.MultiTapeTM + +/-! ### Reading the indices -/ + +/-- **The number of index wires of a block** of `N` incidences with `d` selected: +`⌈log₂ C(N, d)⌉`. -/ +@[expose] def blockWires (b : Block) : ℕ := Nat.clog 2 (b.1.length.choose b.2) + +/-- One step of reading the indices: the next `blockWires b` bits, read little-endian. -/ +@[expose] def indexStep (st : List Bool × List ℕ) (b : Block) : List Bool × List ℕ := + (st.1.drop (blockWires b), st.2 ++ [lsbValue (st.1.take (blockWires b))]) + +/-- **The indices of the blocks**, read from consecutive chunks of the bits. -/ +@[expose] def blockIndices (blocks : List Block) (bs : List Bool) : List ℕ := + (blocks.foldl indexStep (bs, [])).2 + +/-- **The incidences of a block selected by an index**: those at the `true` positions of the +combination of that rank. -/ +@[expose] def selectBlock (b : Block) (ι : ℕ) : List (ℕ × ℕ) := + ((b.1.zip (unrankCombination b.1.length b.2 ι)).filter (·.2)).map (·.1) + +/-- **The selected incidences** of the blocks at the indices. -/ +@[expose] def selected (blocks : List Block) (idx : List ℕ) : List (ℕ × ℕ) := + (blocks.zip idx).flatMap fun (b, ι) => selectBlock b ι + +/-- **Valid indices**: the index of every block of `N` incidences with `d` selected is below +`C(N, d)`. -/ +@[expose] def validIndices (blocks : List Block) (idx : List ℕ) : Bool := + (blocks.zip idx).all fun ((incs, d), ι) => decide (ι < incs.length.choose d) + +/-! ### Rows -/ + +/-- **The parity factor `B(x; V)` in `B_{P,ℓ}`** at a natural `x`: coefficient `j < ℓ` is +`(a_j + b_j x) (x (x - 1)) ^ j` modulo `2 ^ P`, for the linear remainders `a_j + b_j Y` of +`parityLinearCoeffs ℓ`. -/ +@[expose] def factorCoeffs (P ℓ x : ℕ) : List ℕ := + (List.range ℓ).map fun j => + ((((parityLinearCoeffs ℓ).getD j (0, 0)).1 % ((2 ^ P : ℕ) : ℤ)).toNat + + (((parityLinearCoeffs ℓ).getD j (0, 0)).2 % ((2 ^ P : ℕ) : ℤ)).toNat * x) * + (x * (x - 1)) ^ j % 2 ^ P + +/-- **The monomials of a test inside its chosen variables**: the number of monomials of `test` +all of whose variables `v` have `(t, v)` chosen. -/ +@[expose] def monomialsIn (test : List (List ℕ)) (t : ℕ) (chosen : List (ℕ × ℕ)) : ℕ := + test.countP fun M => M.all fun v => decide ((t, v) ∈ chosen) + +/-- **The product of the parity factors** of the tests at the chosen incidences, in `B_{P,ℓ}`: +`∏_t B(m_t; V)`, for `m_t` the monomials of test `t` inside its chosen variables. -/ +@[expose] def rowTerm (P ℓ : ℕ) (tests : List (List (List ℕ))) (chosen : List (ℕ × ℕ)) : + List ℕ := + (List.range tests.length).foldl + (fun acc t => mul P (truncFl ℓ) acc (factorCoeffs P ℓ (monomialsIn (tests.getD t []) t chosen))) + (one (truncFl ℓ)) + +/-- The incidences chosen by a word on the selected incidences: those at its `true` positions. -/ +@[expose] def chosenBy (sel : List (ℕ × ℕ)) (w : List Bool) : List (ℕ × ℕ) := + ((sel.zip w).filter (·.2)).map (·.1) + +/-- The descriptor of a row: the precision `P`, the truncation order `ℓ`, the tests of its group +and its blocks. -/ +abbrev RowDesc : Type := ℕ × ℕ × List (List (List ℕ)) × List Block + +/-- The context of the sum of a row: `P`, `ℓ`, the tests and the selected incidences. -/ +abbrev RowCtx : Type := ℕ × ℕ × List (List (List ℕ)) × List (ℕ × ℕ) + +/-- **One term of the sum of a row**, at a word `w` on the selected incidences: add +`(-1) ^ (|sel| - |w|) ∏_t B(m_t; V)` to the accumulator, keeping the context. -/ +@[expose] def rowBody : (ℕ × List Bool) × RowCtx × List ℕ → RowCtx × List ℕ + | ((_, w), (P, ℓ, tests, sel), acc) => + ((P, ℓ, tests, sel), + if (sel.length - w.count true) % 2 = 0 then + add P (truncFl ℓ) acc (rowTerm P ℓ tests (chosenBy sel w)) + else + sub P (truncFl ℓ) acc (rowTerm P ℓ tests (chosenBy sel w))) + +/-- **The sum of a row** over all words on its selected incidences, in enumeration order. -/ +@[expose] def rowSum : RowCtx → List ℕ + | (P, ℓ, tests, sel) => + ((enumList sel.length).foldl (fun st w => rowBody ((sel.length, w), st)) + ((P, ℓ, tests, sel), zero (truncFl ℓ))).2 + +/-- The context of a row at the bits on its ports: its `P`, `ℓ` and tests, and the incidences +selected by the indices. -/ +@[expose] def rowContext : RowDesc → List Bool → RowCtx + | (P, ℓ, tests, blocks), bs => (P, ℓ, tests, selected blocks (blockIndices blocks bs)) + +/-- **The entry of a row**: zero (the empty list) at an invalid index, and the sum of the row +otherwise. -/ +@[expose] def rowEntry : RowDesc → List Bool → List ℕ + | (P, ℓ, tests, blocks), bs => + if validIndices blocks (blockIndices blocks bs) then + rowSum (rowContext (P, ℓ, tests, blocks) bs) + else [] + +/-! ### Columns -/ + +/-- The descriptor of a column: the precision `P`, the variables of its group and its blocks. -/ +abbrev ColDesc : Type := ℕ × List ℕ × List Block + +/-- The number of variables selected by no incidence. -/ +@[expose] def unselectedCount (vars : List ℕ) (sel : List (ℕ × ℕ)) : ℕ := + vars.countP fun v => decide (v ∉ sel.map Prod.snd) + +/-- **The entry of a column**: the constant `2 ^ u` modulo `2 ^ P`, for `u` the number of its +variables selected by no incidence. -/ +@[expose] def colEntry : ColDesc → List Bool → List ℕ + | (P, vars, blocks), bs => + [2 ^ unselectedCount vars (selected blocks (blockIndices blocks bs)) % 2 ^ P] + +/-! ### The entry procedure -/ + +/-- **The entry procedure of the incidence network**: rows, columns and tables. -/ +@[expose] def incEntry : Desc → List Bool → List ℕ + | .inl row, bs => rowEntry row bs + | .inr (.inl col), bs => colEntry col bs + | .inr (.inr table), bs => tableEntry table bs + +@[simp] theorem incEntry_inl (row : RowDesc) (bs : List Bool) : + incEntry (.inl row) bs = rowEntry row bs := rfl + +@[simp] theorem incEntry_inr_inl (col : ColDesc) (bs : List Bool) : + incEntry (.inr (.inl col)) bs = colEntry col bs := rfl + +@[simp] theorem incEntry_inr_inr (table : List ℕ) (bs : List Bool) : + incEntry (.inr (.inr table)) bs = tableEntry table bs := rfl + +/-! ### Encoding -/ + +/-- The encoding of a block: its incidences in binary and its selected number in unary. -/ +abbrev encBlock : Block ↪ List Bool := encPair (encList (encPair encNat encNat)) encUnary + +/-- The encoding of a row descriptor: `P` and `ℓ` in unary, then the tests and the blocks. -/ +abbrev encRowDesc : RowDesc ↪ List Bool := + encPair encUnary (encPair encUnary (encPair (encList (encList (encList encNat))) + (encList encBlock))) + +/-- The encoding of a column descriptor: `P` in unary, then the variables and the blocks. -/ +abbrev encColDesc : ColDesc ↪ List Bool := + encPair encUnary (encPair (encList encNat) (encList encBlock)) + +/-- **The encoding of the descriptors**: a tag, then a row, a column or a table. -/ +abbrev encDesc : Desc ↪ List Bool := encSum encRowDesc (encSum encColDesc (encList encNat)) + +/-! ### Basic facts -/ + +/-- The rows of an invalid index have entry zero. -/ +theorem rowEntry_of_not_valid {P ℓ : ℕ} {tests : List (List (List ℕ))} {blocks : List Block} + {bs : List Bool} (h : validIndices blocks (blockIndices blocks bs) = false) : + rowEntry (P, ℓ, tests, blocks) bs = [] := by + simp [rowEntry, h] + +@[simp] theorem length_factorCoeffs (P ℓ x : ℕ) : (factorCoeffs P ℓ x).length = ℓ := by + simp [factorCoeffs] + +theorem lt_of_mem_factorCoeffs {P ℓ x y : ℕ} (hy : y ∈ factorCoeffs P ℓ x) : y < 2 ^ P := by + obtain ⟨j, -, rfl⟩ := List.mem_map.mp hy + exact Nat.mod_lt _ (Nat.two_pow_pos P) + +/-- The indices of the blocks: one per block. -/ +theorem length_blockIndices (blocks : List Block) (bs : List Bool) : + (blockIndices blocks bs).length = blocks.length := by + have h (st : List Bool × List ℕ) : + (blocks.foldl indexStep st).2.length = st.2.length + blocks.length := by + induction blocks generalizing st with + | nil => simp + | cons b blocks ih => + rw [List.foldl_cons, ih] + simp only [indexStep, List.length_append, List.length_cons, List.length_nil] + omega + simpa [blockIndices] using h (bs, []) + +/-- A block selects at most its incidences. -/ +theorem length_selectBlock_le (b : Block) (ι : ℕ) : (selectBlock b ι).length ≤ b.1.length := by + rw [selectBlock, List.length_map] + exact (List.length_filter_le _ _).trans (by simp) + +/-- The selected incidences are at most the incidences of the blocks. -/ +theorem length_selected_le (blocks : List Block) (idx : List ℕ) : + (selected blocks idx).length ≤ (blocks.map fun b => b.1.length).sum := by + induction blocks generalizing idx with + | nil => simp [selected] + | cons b blocks ih => + cases idx with + | nil => simp [selected] + | cons ι idx => + have := ih idx + simp only [selected, List.zip_cons_cons, List.flatMap_cons, List.length_append, + List.map_cons, List.sum_cons] at this ⊢ + exact Nat.add_le_add (length_selectBlock_le b ι) this + +end Cslib.Circuits.Frontier.IncidenceNetwork diff --git a/Complexity/Computability/Circuit/Frontier/TensorNetwork/IncidenceEntryCertificate.lean b/Complexity/Computability/Circuit/Frontier/TensorNetwork/IncidenceEntryCertificate.lean new file mode 100644 index 000000000..c06b2f4a1 --- /dev/null +++ b/Complexity/Computability/Circuit/Frontier/TensorNetwork/IncidenceEntryCertificate.lean @@ -0,0 +1,361 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: candidate + +public import Complexity.Computability.Circuit.Frontier.TensorNetwork.IncidenceEntryPolyTime +public import Complexity.Computability.GenericRAM.Native.BooleanFold +public import Complexity.Computability.GenericRAM.Native.Combinators +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.BigO.Sum +import Complexity.Computability.Machines.Turing.MultiTape.Internal.PolyTimeOptionPrimitives +import Complexity.Computability.Machines.Turing.MultiTape.Internal.PolyTimePrimitives + +/-! +# The native certificate of the entries of the incidence network + +One native machine evaluates every entry of the incidence network of Lemma D.2 of +[OpenAI2026ETH] (`Cslib.Circuits.Frontier.IncidenceNetwork.incEntry`, p. 56) +(`IncidenceNetwork.incCertificate`). A row runs the streaming Boolean fold +`Cslib.GenericRAM.BooleanFold` over the `2 ^ |sel|` words on its selected incidences, one +polynomial-time term each (`IncidenceNetwork.rowSumCertificate`); everything else is +polynomial-time. So on a descriptor and bits of encoded length `m`, with `N` incidences in the +blocks of a row descriptor (`IncidenceNetwork.descInc`, none for other descriptors), the machine +takes time at most `c (m + 1) ^ c 2 ^ N` and space at most `c (m + 1) ^ c` +(`IncidenceNetwork.exists_incCertificate_le`). The source evaluates a test-group entry in +`2 ^ λ ^ O(1)` bit operations and polynomial space (p. 56), summing one test at a time over the +`2 ^ |S_i|` subsets; here one sum runs over the subsets of all selected incidences of the group, +so the exponent is bounded by the incidences of the group. + +## Main definitions + +* `Cslib.Circuits.Frontier.IncidenceNetwork.rowSumCertificate`: the sum of a row. +* `Cslib.Circuits.Frontier.IncidenceNetwork.rowCertificate`: the entries of rows. +* `Cslib.Circuits.Frontier.IncidenceNetwork.incCertificate`: the entry procedure. +* `Cslib.Circuits.Frontier.IncidenceNetwork.descInc`: the incidences of a row descriptor. + +## Main results + +* `Cslib.Circuits.Frontier.IncidenceNetwork.exists_incCertificate_le`: time and space. + +## References + +* [OpenAI, *The Exponential Time Hypothesis is False*][OpenAI2026ETH], Lemma D.2 (p. 56). +-/ + +public section + +namespace Cslib.Circuits.Frontier.IncidenceNetwork + +open Turing.MultiTapeTM Cslib.GenericRAM GaloisRingArith Cslib.BitString + +/-! ### The sum of a row -/ + +/-- The number of selected incidences of a context, in unary. -/ +theorem rowDim_polyTime : + ComputableInPolyTime (fun ((_, _, _, sel) : RowCtx) => sel.length) encRowCtx encUnary := + ((ComputableInPolyTime.length_list (encPair encNat encNat)).comp + ((ComputableInPolyTime.snd _ _).comp ((ComputableInPolyTime.snd _ _).comp + (ComputableInPolyTime.snd _ _)))).of_enc_eq fun (_, _, _, _) => rfl + +/-- The initial state of the sum of a row: the context and zero. -/ +theorem rowInit_polyTime : + ComputableInPolyTime + (fun ((P, ℓ, tests, sel) : RowCtx) => ((P, ℓ, tests, sel), zero (truncFl ℓ))) encRowCtx + encRowState := by + have hℓ := (ComputableInPolyTime.fst encUnary (encPair (encList (encList (encList encNat))) + (encList (encPair encNat encNat)))).comp (ComputableInPolyTime.snd encUnary + (encPair encUnary (encPair (encList (encList (encList encNat))) + (encList (encPair encNat encNat))))) + have hfl := truncFl_polyTime.comp hℓ + have hz := computableInPolyTime_tabulate (g := fun (_ : RowCtx) (_ : ℕ) => 0) + ((ComputableInPolyTime.length_list encNat).comp hfl) (ComputableInPolyTime.const 0) + exact (ComputableInPolyTime.id'.prod (hz.of_enc_eq fun _ => rfl)).of_enc_eq + fun (_, _, _, _) => rfl + +/-- The streaming fold of the sum of a row. -/ +noncomputable def rowLoopCertificate := + BooleanFold.certificate (encIn := encRowCtx) (encB := encRowState) + (dimension := fun ((_, _, _, sel) : RowCtx) => sel.length) + (initial := fun ((P, ℓ, tests, sel) : RowCtx) => ((P, ℓ, tests, sel), zero (truncFl ℓ))) + (body := rowBody) + (NativeCertificate.ofPolyTime rowDim_polyTime) (NativeCertificate.ofPolyTime rowInit_polyTime) + (NativeCertificate.ofPolyTime rowBody_polyTime) + +/-- The streaming fold computes the sum of a row. -/ +private theorem run_rowBody (P ℓ : ℕ) (tests : List (List (List ℕ))) (sel : List (ℕ × ℕ)) : + (BooleanFold.run rowBody sel.length ((P, ℓ, tests, sel), zero (truncFl ℓ))).2.2.2 = + rowSum (P, ℓ, tests, sel) := by + rw [BooleanFold.run_accumulator] + rfl + +/-- **The native certificate of the sum of a row.** -/ +noncomputable def rowSumCertificate : NativeCertificate rowSum encRowCtx (encList encNat) := + rowLoopCertificate.snd.snd.snd.congr fun (P, ℓ, tests, sel) => run_rowBody P ℓ tests sel + +/-- A term keeps the context. -/ +theorem fst_rowBody (n : ℕ) (w : List Bool) (ctx : RowCtx) (acc : List ℕ) : + (rowBody ((n, w), ctx, acc)).1 = ctx := by + obtain ⟨_, _, _, _⟩ := ctx + rfl + +/-- A term leaves a reduced accumulator: `ℓ` coefficients below `2 ^ P`. -/ +theorem reduced_rowBody (n : ℕ) (w : List Bool) (P ℓ : ℕ) (tests : List (List (List ℕ))) + (sel : List (ℕ × ℕ)) (acc : List ℕ) : + (rowBody ((n, w), (P, ℓ, tests, sel), acc)).2.length = ℓ ∧ + ∀ x ∈ (rowBody ((n, w), (P, ℓ, tests, sel), acc)).2, x < 2 ^ P := by + simp only [rowBody] + split_ifs + · exact ⟨by simp, fun x hx => lt_of_mem_add hx⟩ + · exact ⟨by simp [sub], fun x hx => lt_of_mem_add hx⟩ + +/-- Every prefix of the sum of a row keeps the context and a reduced accumulator. -/ +theorem foldl_rowBody {α : Type*} (P ℓ : ℕ) (tests : List (List (List ℕ))) + (sel : List (ℕ × ℕ)) (n : ℕ) (word : α → List Bool) (l : List α) (acc : List ℕ) + (hlen : acc.length = ℓ) (hlt : ∀ x ∈ acc, x < 2 ^ P) : + (l.foldl (fun st i => rowBody ((n, word i), st)) ((P, ℓ, tests, sel), acc)).1 = + (P, ℓ, tests, sel) ∧ + (l.foldl (fun st i => rowBody ((n, word i), st)) ((P, ℓ, tests, sel), acc)).2.length = ℓ ∧ + ∀ x ∈ (l.foldl (fun st i => rowBody ((n, word i), st)) ((P, ℓ, tests, sel), acc)).2, + x < 2 ^ P := by + induction l generalizing acc with + | nil => exact ⟨rfl, hlen, hlt⟩ + | cons i l ih => + rw [List.foldl_cons] + have h := reduced_rowBody n (word i) P ℓ tests sel acc + have hst : rowBody ((n, word i), ((P, ℓ, tests, sel), acc)) = + ((P, ℓ, tests, sel), (rowBody ((n, word i), ((P, ℓ, tests, sel), acc))).2) := + Prod.ext (fst_rowBody _ _ _ _) rfl + rw [hst] + exact ih _ h.1 h.2 + +/-- The bound on the states of the sum of a row. -/ +theorem length_encRowState_le (P ℓ : ℕ) (tests : List (List (List ℕ))) (sel : List (ℕ × ℕ)) + (acc : List ℕ) (hlen : acc.length = ℓ) (hlt : ∀ x ∈ acc, x < 2 ^ P) : + (encRowState ((P, ℓ, tests, sel), acc)).length ≤ + 2 * (encRowCtx (P, ℓ, tests, sel)).length + 1 + + (encRowCtx (P, ℓ, tests, sel)).length * + (2 * (encRowCtx (P, ℓ, tests, sel)).length + 1) := by + have h1 := GaloisRingArith.length_encList_le hlen hlt + have hP : P ≤ (encRowCtx (P, ℓ, tests, sel)).length := by + simp only [length_encPair, encUnary_apply, List.length_replicate] + omega + have hℓ : ℓ ≤ (encRowCtx (P, ℓ, tests, sel)).length := by + simp only [length_encPair, encUnary_apply, List.length_replicate] + omega + have h0 : (encRowState ((P, ℓ, tests, sel), acc)).length = + 2 * (encRowCtx (P, ℓ, tests, sel)).length + 1 + (encList encNat acc).length := + length_encPair _ + have := Nat.mul_le_mul hℓ (Nat.add_le_add_right (Nat.mul_le_mul_left 2 hP) 1) + omega + +/-- **The sum of a row in time `(2 ^ |sel| + 1)` times a polynomial and polynomial space.** -/ +theorem rowSumCertificate_bounds : + PolyBounded (fun ctx => (encRowCtx ctx).length) rowSumCertificate.space ∧ + ∃ T : RowCtx → ℕ, PolyBounded (fun ctx => (encRowCtx ctx).length) T ∧ + ∀ (P ℓ : ℕ) (tests : List (List (List ℕ))) (sel : List (ℕ × ℕ)), + rowSumCertificate.time (P, ℓ, tests, sel) ≤ + (2 ^ sel.length + 1) * T (P, ℓ, tests, sel) := by + have h := BooleanFold.certificate_bounds (encIn := encRowCtx) (encB := encRowState) + (dimension := fun ((_, _, _, sel) : RowCtx) => sel.length) + (initial := fun ((P, ℓ, tests, sel) : RowCtx) => ((P, ℓ, tests, sel), zero (truncFl ℓ))) + (body := rowBody) + (cn := NativeCertificate.ofPolyTime rowDim_polyTime) + (ci := NativeCertificate.ofPolyTime rowInit_polyTime) + (cb := NativeCertificate.ofPolyTime rowBody_polyTime) + (NativeCertificate.ofPolyTime_isPolynomial _) (NativeCertificate.ofPolyTime_isPolynomial _) + (NativeCertificate.ofPolyTime_isPolynomial _) + (B := fun ctx => 2 * (encRowCtx ctx).length + 1 + + (encRowCtx ctx).length * (2 * (encRowCtx ctx).length + 1)) + ((((PolyBounded.const 2).mul .self).add (.const 1)).add + (PolyBounded.self.mul (((PolyBounded.const 2).mul .self).add (.const 1)))) + (fun (P, ℓ, tests, sel) j _ => by + rw [BooleanFold.prefix_accumulator] + have hz : (zero (truncFl ℓ)).length = ℓ := by simp + have hz' : ∀ x ∈ zero (truncFl ℓ), x < 2 ^ P := fun x hx => by + simp only [zero, List.mem_map] at hx + obtain ⟨_, -, rfl⟩ := hx + exact Nat.two_pow_pos _ + obtain ⟨h1, h2, h3⟩ := foldl_rowBody P ℓ tests sel sel.length (lowBits sel.length) + (List.range j) _ hz hz' + have heq : List.foldl (fun acc i => rowBody ((sel.length, lowBits sel.length i), acc)) + ((P, ℓ, tests, sel), zero (truncFl ℓ)) (List.range j) = + ((P, ℓ, tests, sel), (List.foldl (fun acc i => rowBody ((sel.length, + lowBits sel.length i), acc)) ((P, ℓ, tests, sel), zero (truncFl ℓ)) + (List.range j)).2) := + Prod.ext h1 rfl + rw [heq] + exact length_encRowState_le P ℓ tests sel _ h2 h3) + exact ⟨h.1, h.2.imp fun _ hT => ⟨hT.1, fun P ℓ tests sel => hT.2 (P, ℓ, tests, sel)⟩⟩ + +/-! ### Rows -/ + +/-- **The native certificate of the entries of rows.** -/ +noncomputable def rowCertificate : + NativeCertificate (fun q : RowDesc × List Bool => rowEntry q.1 q.2) + (encPair encRowDesc encBits) (encList encNat) := + (NativeCertificate.branch (NativeCertificate.ofPolyTime rowValid_polyTime) + (rowSumCertificate.comp (NativeCertificate.ofPolyTime rowContext_polyTime)) + (NativeCertificate.const [])).congr fun ((_, _, _, _), _) => rfl + +/-- The incidences of the blocks of a row descriptor. -/ +@[expose] def rowInc : RowDesc → ℕ + | (_, _, _, blocks) => (blocks.map fun b => b.1.length).sum + +/-- **The entries of rows in time `2 ^ N` times a polynomial and polynomial space**, for `N` the +incidences of the blocks. -/ +theorem rowCertificate_bounds : + PolyBounded (fun q => (encPair encRowDesc encBits q).length) rowCertificate.space ∧ + ∃ T : RowDesc × List Bool → ℕ, + PolyBounded (fun q => (encPair encRowDesc encBits q).length) T ∧ + ∀ q, rowCertificate.time q ≤ 2 ^ rowInc q.1 * T q := by + obtain ⟨hS, Tl, hTl, hle⟩ := rowSumCertificate_bounds + have hv := NativeCertificate.ofPolyTime_isPolynomial rowValid_polyTime + have hc := NativeCertificate.ofPolyTime_isPolynomial rowContext_polyTime + have hlen := rowContext_polyTime.polyBounded_length + refine ⟨(((hv.2.add hc.2).add (hS.comp hlen)).add .self).mono fun q => ?_, + fun q => (NativeCertificate.ofPolyTime rowValid_polyTime).time q + + (NativeCertificate.ofPolyTime rowContext_polyTime).time q + + (encPair encRowDesc encBits q).length + 2 * Tl (rowContext q.1 q.2), + (((hv.1.add hc.1).add .self).add ((PolyBounded.const 2).mul (hTl.comp hlen))), + fun q => ?_⟩ + · have hsp : rowCertificate.space q = (NativeCertificate.ofPolyTime rowValid_polyTime).space q + + if validIndices q.1.2.2.2 (blockIndices q.1.2.2.2 q.2) then + (NativeCertificate.ofPolyTime rowContext_polyTime).space q + + rowSumCertificate.space (rowContext q.1 q.2) + else (encPair encRowDesc encBits q).length := rfl + rw [hsp] + split_ifs <;> omega + · obtain ⟨⟨P, ℓ, tests, blocks⟩, bs⟩ := q + have htm : rowCertificate.time ((P, ℓ, tests, blocks), bs) = + (NativeCertificate.ofPolyTime rowValid_polyTime).time ((P, ℓ, tests, blocks), bs) + + if validIndices blocks (blockIndices blocks bs) then + (NativeCertificate.ofPolyTime rowContext_polyTime).time ((P, ℓ, tests, blocks), bs) + + rowSumCertificate.time (P, ℓ, tests, selected blocks (blockIndices blocks bs)) + else (encPair encRowDesc encBits ((P, ℓ, tests, blocks), bs)).length := rfl + rw [htm] + dsimp only [rowContext] + have hdim : (selected blocks (blockIndices blocks bs)).length ≤ rowInc (P, ℓ, tests, blocks) := + length_selected_le _ _ + have h2 : 2 ^ (selected blocks (blockIndices blocks bs)).length ≤ + 2 ^ rowInc (P, ℓ, tests, blocks) := + Nat.pow_le_pow_right (by norm_num) hdim + have h1 : 1 ≤ 2 ^ rowInc (P, ℓ, tests, blocks) := Nat.one_le_two_pow + have hl := hle P ℓ tests (selected blocks (blockIndices blocks bs)) + have h3 := Nat.mul_le_mul_right (Tl (P, ℓ, tests, selected blocks (blockIndices blocks bs))) + (Nat.add_le_add h2 h1) + split_ifs + · nlinarith + · nlinarith + +/-! ### All descriptors -/ + +/-- The entries of columns and tables, from a descriptor that is not a row. -/ +@[expose] def restEntry (q : Desc × List Bool) : List ℕ := + (((q.1.getRight?).getD (.inr [])).getLeft?).elim + (tableEntry ((((q.1.getRight?).getD (.inr [])).getRight?).getD []) q.2) + (fun col => colEntry col q.2) + +/-- The entries of columns and tables are polynomial-time. -/ +theorem restEntry_polyTime : + ComputableInPolyTime restEntry (encPair encDesc encBits) (encList encNat) := by + have hright := (ComputableInO.getRight?_deg encRowDesc (encSum encColDesc (encList encNat)) + ).computableInPolyTime.comp (ComputableInPolyTime.fst encDesc encBits) + have hr := ComputableInPolyTime.optionGetDWithInput hright (ComputableInPolyTime.const (.inr [])) + have hleft := + (ComputableInO.getLeft?_deg encColDesc (encList encNat)).computableInPolyTime.comp hr + have htab := + (ComputableInO.getRight?_deg encColDesc (encList encNat)).computableInPolyTime.comp hr + have htab' := ComputableInPolyTime.optionGetDWithInput htab (ComputableInPolyTime.const []) + have hfallback := tableEntry_polyTime.comp (htab'.prod (ComputableInPolyTime.snd encDesc encBits)) + have hbody := colEntry_polyTime.comp ((ComputableInPolyTime.snd _ _).prod + ((ComputableInPolyTime.snd encDesc encBits).comp (ComputableInPolyTime.fst _ _))) + exact (ComputableInPolyTime.optionElimWithInput hleft hfallback hbody).of_enc_eq fun _ => rfl + +/-- The row descriptor of a descriptor, the default for others, with the bits. -/ +theorem leftInput_polyTime : + ComputableInPolyTime (fun q : Desc × List Bool => ((q.1.getLeft?).getD default, q.2)) + (encPair encDesc encBits) (encPair encRowDesc encBits) := by + have hleft := (ComputableInO.getLeft?_deg encRowDesc (encSum encColDesc (encList encNat)) + ).computableInPolyTime.comp (ComputableInPolyTime.fst encDesc encBits) + exact (ComputableInPolyTime.optionGetDWithInput hleft (ComputableInPolyTime.const default)).prod + (ComputableInPolyTime.snd encDesc encBits) + +/-- Whether a descriptor is a row. -/ +theorem isRow_polyTime : + ComputableInPolyTime (fun q : Desc × List Bool => (q.1.getLeft?).isSome) + (encPair encDesc encBits) encBool := + ((ComputableInO.getLeft?_deg encRowDesc (encSum encColDesc (encList encNat)) + ).computableInPolyTime.comp (ComputableInPolyTime.fst encDesc encBits)).optionIsSome + +/-- **The native certificate of the entry procedure of the incidence network.** -/ +noncomputable def incCertificate : + NativeCertificate (fun q : Desc × List Bool => incEntry q.1 q.2) (encPair encDesc encBits) + (encList encNat) := + (NativeCertificate.branch (NativeCertificate.ofPolyTime isRow_polyTime) + (rowCertificate.comp (NativeCertificate.ofPolyTime leftInput_polyTime)) + (NativeCertificate.ofPolyTime restEntry_polyTime)).congr fun q => by + rcases q with ⟨row | col | t, bs⟩ <;> rfl + +/-- **The incidences of a descriptor**: those of the blocks of a row, and none otherwise. -/ +@[expose] def descInc : Desc → ℕ + | .inl row => rowInc row + | .inr _ => 0 + +/-- **Time and space of the entry procedure.** On a descriptor and bits of encoded length `m`, the +certificate takes time at most `c (m + 1) ^ c 2 ^ N`, for `N` the incidences of the descriptor, +and space at most `c (m + 1) ^ c`. -/ +theorem exists_incCertificate_le : ∃ c : ℕ, ∀ q : Desc × List Bool, + incCertificate.time q ≤ c * ((encPair encDesc encBits q).length + 1) ^ c * 2 ^ descInc q.1 ∧ + incCertificate.space q ≤ c * ((encPair encDesc encBits q).length + 1) ^ c := by + obtain ⟨hS, T, hT, hle⟩ := rowCertificate_bounds + have hi := NativeCertificate.ofPolyTime_isPolynomial isRow_polyTime + have hl := NativeCertificate.ofPolyTime_isPolynomial leftInput_polyTime + have hr := NativeCertificate.ofPolyTime_isPolynomial restEntry_polyTime + have hlen := leftInput_polyTime.polyBounded_length + obtain ⟨c₁, d₁, h₁⟩ := ((((hi.1.add hl.1).add hr.1).add (hT.comp hlen))).exists_le + obtain ⟨c₂, d₂, h₂⟩ := ((((hi.2.add hl.2).add hr.2).add (hS.comp hlen))).exists_le + refine ⟨c₁ + c₂ + d₁ + d₂ + 1, fun q => ?_⟩ + obtain ⟨m, hm⟩ : ∃ m, (encPair encDesc encBits q).length = m := ⟨_, rfl⟩ + have hpow (c d : ℕ) (hc : c ≤ c₁ + c₂ + d₁ + d₂ + 1) (hd : d ≤ c₁ + c₂ + d₁ + d₂ + 1) : + c * (m + 1) ^ d ≤ (c₁ + c₂ + d₁ + d₂ + 1) * (m + 1) ^ (c₁ + c₂ + d₁ + d₂ + 1) := + Nat.mul_le_mul hc (Nat.pow_le_pow_right (by omega) hd) + have h1 := h₁ q + have h2 := h₂ q + rw [hm] at h1 h2 + rw [hm] + have hp1 := hpow c₁ d₁ (by omega) (by omega) + have hp2 := hpow c₂ d₂ (by omega) (by omega) + have htm : incCertificate.time q = (NativeCertificate.ofPolyTime isRow_polyTime).time q + + if (q.1.getLeft?).isSome then + (NativeCertificate.ofPolyTime leftInput_polyTime).time q + + rowCertificate.time ((q.1.getLeft?).getD default, q.2) + else (NativeCertificate.ofPolyTime restEntry_polyTime).time q := rfl + have hsp : incCertificate.space q = (NativeCertificate.ofPolyTime isRow_polyTime).space q + + if (q.1.getLeft?).isSome then + (NativeCertificate.ofPolyTime leftInput_polyTime).space q + + rowCertificate.space ((q.1.getLeft?).getD default, q.2) + else (NativeCertificate.ofPolyTime restEntry_polyTime).space q := rfl + rw [htm, hsp] + rcases q with ⟨row | rest, bs⟩ + · have hrow := hle (row, bs) + have hd : descInc (Sum.inl row) = rowInc row := rfl + simp only [Sum.getLeft?_inl, Option.isSome_some, Option.getD_some, ↓reduceIte, hd] at h1 h2 ⊢ + have h2p : 1 ≤ 2 ^ rowInc row := Nat.one_le_two_pow + constructor + · calc _ ≤ 2 ^ rowInc row * ((NativeCertificate.ofPolyTime isRow_polyTime).time (.inl row, bs) + + (NativeCertificate.ofPolyTime leftInput_polyTime).time (.inl row, bs) + + (NativeCertificate.ofPolyTime restEntry_polyTime).time (.inl row, bs) + + T (row, bs)) := by nlinarith + _ ≤ 2 ^ rowInc row * (c₁ * (m + 1) ^ d₁) := Nat.mul_le_mul_left _ h1 + _ ≤ _ := by rw [Nat.mul_comm]; exact Nat.mul_le_mul_right _ hp1 + · omega + · have hd : descInc (Sum.inr rest) = 0 := rfl + simp only [Sum.getLeft?_inr, Option.isSome_none, Bool.false_eq_true, ↓reduceIte, hd, + pow_zero, mul_one] at h1 h2 ⊢ + exact ⟨by omega, by omega⟩ + +end Cslib.Circuits.Frontier.IncidenceNetwork diff --git a/Complexity/Computability/Circuit/Frontier/TensorNetwork/IncidenceEntryPolyTime.lean b/Complexity/Computability/Circuit/Frontier/TensorNetwork/IncidenceEntryPolyTime.lean new file mode 100644 index 000000000..c0f3602e9 --- /dev/null +++ b/Complexity/Computability/Circuit/Frontier/TensorNetwork/IncidenceEntryPolyTime.lean @@ -0,0 +1,410 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: candidate + +public import Complexity.Computability.Circuit.Frontier.TensorNetwork.IncidenceEntry +import Complexity.Computability.GenericRAM.Native.SubsetPairFold +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.BitString +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Int.BinaryDiv +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.List +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Membership +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat.Binary +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat.BinaryDiv +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat.BinaryLog +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat.Choose +import Complexity.Computability.Machines.Turing.MultiTape.Internal.EqualityPrimitives +import Complexity.Computability.Machines.Turing.MultiTape.Internal.PolyTimeListLookup +import Complexity.Computability.Machines.Turing.MultiTape.Internal.PolyTimeListMap +import Complexity.Computability.Machines.Turing.MultiTape.Internal.PolyTimeListPrimitives +import Complexity.Computability.Machines.Turing.MultiTape.Internal.PolyTimeLoops +import Complexity.Computability.Machines.Turing.MultiTape.Internal.PolyTimeNatFrontends +import Complexity.Computability.Machines.Turing.MultiTape.Internal.PolyTimeOptionPrimitives +import Complexity.Foundations.Data.BitString.Binary +import Mathlib.Data.List.GetD + +/-! +# The polynomial-time steps of the entries of the incidence network + +The entry procedure of the incidence network of Lemma D.2 of [OpenAI2026ETH] (p. 56, +`Cslib.Circuits.Frontier.IncidenceNetwork.incEntry`) is polynomial-time apart from the sum of a +row over the `2 ^ |sel|` words on its selected incidences. This file proves the polynomial-time +steps, with precisions, truncation orders and selected numbers in unary: reading the indices +(`blockIndices_polyTime`), unranking and selecting (`selected_polyTime`), the validity test +(`validIndices_polyTime`), the context of a row (`rowContext_polyTime`), one term of the sum of a +row (`rowBody_polyTime`), and the entries of columns (`colEntry_polyTime`). The source states these +costs: "Each term costs polynomially many bit operations" and "The variable-side entries and checks +for invalid wire indices take polynomial time" (p. 56). + +## Main results + +* `Cslib.Circuits.Frontier.IncidenceNetwork.blockIndices_polyTime`, + `Cslib.Circuits.Frontier.IncidenceNetwork.selected_polyTime`, + `Cslib.Circuits.Frontier.IncidenceNetwork.validIndices_polyTime`: decoding. +* `Cslib.Circuits.Frontier.IncidenceNetwork.rowContext_polyTime`, + `Cslib.Circuits.Frontier.IncidenceNetwork.rowValid_polyTime`: the context and validity of a row. +* `Cslib.Circuits.Frontier.IncidenceNetwork.factorCoeffs_polyTime`, + `Cslib.Circuits.Frontier.IncidenceNetwork.rowTerm_polyTime`, + `Cslib.Circuits.Frontier.IncidenceNetwork.rowBody_polyTime`: one term of a row. +* `Cslib.Circuits.Frontier.IncidenceNetwork.colEntry_polyTime`: the entries of columns. + +## References + +* [OpenAI, *The Exponential Time Hypothesis is False*][OpenAI2026ETH], Lemma D.2 (pp. 55–56). +-/ + +public section + +namespace Cslib.Circuits.Frontier.IncidenceNetwork + +open Turing.MultiTapeTM Cslib.GenericRAM GaloisRingArith Cslib.BitString + +section PolyTime + +open ComputableInPolyTime + +/-! ### Decoding -/ + +/-- A block has at most as many index wires as incidences: `C(N, d) ≤ 2 ^ N`. -/ +theorem blockWires_le (b : Block) : blockWires b ≤ b.1.length := + Nat.clog_le_of_le_pow (Nat.choose_le_two_pow _ _) + +/-- The number of index wires of a block is polynomial-time, in unary. -/ +theorem blockWires_polyTime : ComputableInPolyTime blockWires encBlock encUnary := + binary_clog_two.comp (binary_choose' + ((length_list (encPair encNat encNat)).comp (fst _ _)) (snd _ _)) + +/-- One step of reading the indices is polynomial-time. -/ +theorem indexStep_polyTime : + ComputableInPolyTime (fun p : (List Bool × List ℕ) × Block => indexStep p.1 p.2) + (encPair (encPair encBits (encList encNat)) encBlock) (encPair encBits (encList encNat)) := by + have hst := fst (encPair encBits (encList encNat)) encBlock + have hb := snd (encPair encBits (encList encNat)) encBlock + have hw := blockWires_polyTime.comp hb + have hbits := (fst encBits (encList encNat)).comp hst + have hacc := (snd encBits (encList encNat)).comp hst + have hval := bitsBinaryValue.comp (bitsReverse.comp (bitsTakeWithInput hbits hw)) + exact ((bitsDropWithInput hbits hw).prod (listAppend' hacc (cons' hval (const [])))).of_enc_eq + fun p => by simp only [indexStep, lsbValue_eq_binaryValue_reverse, Function.comp_apply] + +/-- A step of reading the indices adds at most `2 N + 1` bits for a block of `N` incidences. -/ +theorem length_indexStep_le (st : List Bool × List ℕ) (b : Block) : + (encPair encBits (encList encNat) (indexStep st b)).length ≤ + (encPair encBits (encList encNat) st).length + 2 * b.1.length + 1 := by + have hval : (encNat (lsbValue (st.1.take (blockWires b)))).length ≤ b.1.length := by + change (lsbValue _).bits.length ≤ _ + rw [Nat.size_eq_bits_len] + refine (Nat.size_le.mpr ((lsbValue_lt _).trans_le + (Nat.pow_le_pow_right (by norm_num) ?_))).trans le_rfl + exact (List.length_take_le _ _).trans (blockWires_le b) + simp only [indexStep, length_encPair, encBits_apply, length_encList, List.map_append, + List.sum_append, List.length_drop, List.map_cons, List.map_nil, List.sum_cons, List.sum_nil] + omega + +/-- **Reading the indices of the blocks is polynomial-time.** -/ +theorem blockIndices_polyTime : + ComputableInPolyTime (fun q : List Block × List Bool => blockIndices q.1 q.2) + (encPair (encList encBlock) encBits) (encList encNat) := by + let encQ := encPair (encList encBlock) encBits + let encS := encPair encBits (encList encNat) + have hinit : ComputableInPolyTime (fun q : List Block × List Bool => (q.2, ([] : List ℕ))) + encQ encS := (snd (encList encBlock) encBits).prod (const []) + have hlist : ComputableInPolyTime (fun q : List Block × List Bool => q.1) encQ + (encList encBlock) := fst (encList encBlock) encBits + have hp1 : ComputableInPolyTime + (fun p : ((List Block × List Bool) × (List Bool × List ℕ)) × Block => p.1.2) + (encPair (encPair encQ encS) encBlock) encS := + (snd encQ encS).comp (fst (encPair encQ encS) encBlock) + have hp2 : ComputableInPolyTime + (fun p : ((List Block × List Bool) × (List Bool × List ℕ)) × Block => p.2) + (encPair (encPair encQ encS) encBlock) encBlock := + snd (encPair encQ encS) encBlock + have hstep := indexStep_polyTime.comp (hp1.prod hp2) + have hgrowth : ∀ (q : List Block × List Bool) (st : List Bool × List ℕ) (b : Block), + b ∈ q.1 → (encS (indexStep st b)).length ≤ (encS st).length + (2 * (encQ q).length + 1) := by + intro q st b hb + have h1 : (encS (indexStep st b)).length ≤ (encS st).length + 2 * b.1.length + 1 := + length_indexStep_le st b + have h2 : b.1.length ≤ (encQ q).length := by + have h4 := length_le_encList_of_mem encBlock hb + have h3 : b.1.length ≤ (encBlock b).length := by + have h5 := sum_length_le_length_encList (encPair encNat encNat) b.1 + have h6 : b.1.length ≤ (b.1.map fun a => (encPair encNat encNat a).length).sum := by + refine (List.length_map (f := fun a => (encPair encNat encNat a).length) + (as := b.1)).symm.le.trans ?_ + exact List.length_le_sum_of_one_le _ fun x hx => by + obtain ⟨a, -, rfl⟩ := List.mem_map.mp hx + simp only [length_encPair] + omega + simp only [encBlock, length_encPair] + omega + simp only [encQ, length_encPair] + omega + omega + have hfold := foldlWithInput_of_bounded_growth (encA := encBlock) (encL := encList encBlock) + (encB := encS) (step := fun _ st b => indexStep st b) hinit + ⟨hlist, hstep, inferInstance, inferInstance⟩ + (growth := fun q => 2 * (encQ q).length + 1) + ⟨((PolyBounded.const 2).mul .self).add (.const 1), hgrowth⟩ + exact ((snd encBits (encList encNat)).comp hfold).of_enc_eq fun q => + congrArg (encList encNat) (show blockIndices q.1 q.2 = _ from rfl) + +/-- **Selecting the incidences of a block at an index is polynomial-time.** -/ +theorem selectBlock_polyTime : + ComputableInPolyTime (fun q : Block × ℕ => selectBlock q.1 q.2) + (encPair encBlock encNat) (encList (encPair encNat encNat)) := by + have hb := fst encBlock encNat + have hι := snd encBlock encNat + have hinc := (fst (encList (encPair encNat encNat)) encUnary).comp hb + have hN := (length_list (encPair encNat encNat)).comp hinc + have hd := (snd (encList (encPair encNat encNat)) encUnary).comp hb + have hmask := SubsetPairFold.unrankCombination_polyTime.comp ((hN.prod hd).prod hι) + have hzip := (zip (encPair encNat encNat) encBool).comp (hinc.prod (bitsToList.comp hmask)) + have htest : ComputableInPolyTime + (fun p : (Block × ℕ) × ((ℕ × ℕ) × Bool) => p.2.2) + (encPair (encPair encBlock encNat) (encPair (encPair encNat encNat) encBool)) encBool := + (snd (encPair encNat encNat) encBool).comp (snd _ _) + have hfilter := filterWithInput (test := fun (_ : Block × ℕ) (p : (ℕ × ℕ) × Bool) => p.2) + hzip htest + have hmap := (map (fst (encPair encNat encNat) encBool)).comp hfilter + exact hmap.of_enc_eq fun q => rfl + +/-- **The selected incidences are polynomial-time**, from the blocks and the indices. -/ +theorem selected_polyTime : + ComputableInPolyTime (fun q : List Block × List ℕ => selected q.1 q.2) + (encPair (encList encBlock) (encList encNat)) (encList (encPair encNat encNat)) := by + have hzip := zip encBlock encNat + have hf := selectBlock_polyTime.comp + (snd (encPair (encList encBlock) (encList encNat)) (encPair encBlock encNat)) + exact (flatMapWithInput hzip hf).of_enc_eq fun q => rfl + +/-- **The validity test is polynomial-time.** -/ +theorem validIndices_polyTime : + ComputableInPolyTime (fun q : List Block × List ℕ => validIndices q.1 q.2) + (encPair (encList encBlock) (encList encNat)) encBool := by + have hzip := zip encBlock encNat + have hp := snd (encPair (encList encBlock) (encList encNat)) (encPair encBlock encNat) + have hb := (fst encBlock encNat).comp hp + have hι := (snd encBlock encNat).comp hp + have hN := (length_list (encPair encNat encNat)).comp + ((fst (encList (encPair encNat encNat)) encUnary).comp hb) + have hd := (snd (encList (encPair encNat encNat)) encUnary).comp hb + have htest := binary_lt' hι (binary_choose' hN hd) + exact (allWithInput hzip htest).of_enc_eq fun q => rfl + +/-- The encoding of the context of a row: `P` and `ℓ` in unary, then the tests and the selected +incidences. -/ +abbrev encRowCtx : RowCtx ↪ List Bool := + encPair encUnary (encPair encUnary (encPair (encList (encList (encList encNat))) + (encList (encPair encNat encNat)))) + +/-- **The context of a row is polynomial-time.** -/ +theorem rowContext_polyTime : + ComputableInPolyTime (fun q : RowDesc × List Bool => rowContext q.1 q.2) + (encPair encRowDesc encBits) encRowCtx := by + have hrow := fst encRowDesc encBits + have hbs := snd encRowDesc encBits + have hP := (fst _ _).comp hrow + have hr1 := (snd _ _).comp hrow + have hℓ := (fst _ _).comp hr1 + have hr2 := (snd _ _).comp hr1 + have htests := (fst _ _).comp hr2 + have hblocks := (snd (encList (encList (encList encNat))) (encList encBlock)).comp hr2 + have hsel := selected_polyTime.comp (hblocks.prod (blockIndices_polyTime.comp (hblocks.prod hbs))) + exact (hP.prod (hℓ.prod (htests.prod hsel))).of_enc_eq fun ((_, _, _, _), _) => rfl + +/-- **The validity test of a row is polynomial-time.** -/ +theorem rowValid_polyTime : + ComputableInPolyTime + (fun (((_, _, _, blocks), bs) : RowDesc × List Bool) => + validIndices blocks (blockIndices blocks bs)) + (encPair encRowDesc encBits) encBool := by + have hblocks := (snd (encList (encList (encList encNat))) (encList encBlock)).comp + ((snd _ _).comp ((snd _ _).comp (fst encRowDesc encBits))) + exact (validIndices_polyTime.comp + (hblocks.prod (blockIndices_polyTime.comp (hblocks.prod (snd encRowDesc encBits))))).of_enc_eq + fun ((_, _, _, _), _) => rfl + +/-! ### One term of a row -/ + +/-- **The parity factor in `B_{P,ℓ}` is polynomial-time**, with `P` and `ℓ` in unary and the +count in binary. -/ +theorem factorCoeffs_polyTime : + ComputableInPolyTime (fun (((P, ℓ), x) : (ℕ × ℕ) × ℕ) => factorCoeffs P ℓ x) + (encPair (encPair encUnary encUnary) encNat) (encList encNat) := by + let encQ := encPair (encPair encUnary encUnary) encNat + have hq := fst encQ encUnary + have hj := snd encQ encUnary + have hP := (fst encUnary encUnary).comp ((fst (encPair encUnary encUnary) encNat).comp hq) + have hℓ := (snd encUnary encUnary).comp ((fst (encPair encUnary encUnary) encNat).comp hq) + have hx := (snd (encPair encUnary encUnary) encNat).comp hq + have hab := (listGetD (encA := encPair encIntBin encIntBin) (encL := encList (encPair encIntBin + encIntBin)) (0, 0)).comp ((parityLinearCoeffs_polytime.comp hℓ).prod hj) + have hm := binary_two_pow.comp hP + have ha := intBin_emodNat' ((fst encIntBin encIntBin).comp hab) hm + have hb := intBin_emodNat' ((snd encIntBin encIntBin).comp hab) hm + have hlin := binary_add.comp (ha.prod (binary_mul' hb hx)) + have hh := binary_mul' hx (binary_sub' hx (const 1)) + have hterm := binary_mul' hlin (binary_pow' hh hj) + have hg := computableInPolyTime_mod_two_pow hterm hP + have hℓ₀ := (snd encUnary encUnary).comp (fst (encPair encUnary encUnary) encNat) + exact (computableInPolyTime_tabulate (g := fun (q : (ℕ × ℕ) × ℕ) (j : ℕ) => + ((((parityLinearCoeffs q.1.2).getD j (0, 0)).1 % ((2 ^ q.1.1 : ℕ) : ℤ)).toNat + + (((parityLinearCoeffs q.1.2).getD j (0, 0)).2 % ((2 ^ q.1.1 : ℕ) : ℤ)).toNat * q.2) * + (q.2 * (q.2 - 1)) ^ j % 2 ^ q.1.1) hℓ₀ hg).of_enc_eq fun ((_, _), _) => rfl + +/-- The input of `monomialsIn`: the test, its position and the chosen incidences. -/ +abbrev encMonomialsIn : (List (List ℕ) × ℕ) × List (ℕ × ℕ) ↪ List Bool := + encPair (encPair (encList (encList encNat)) encUnary) (encList (encPair encNat encNat)) + +/-- **Counting the monomials inside the chosen variables is polynomial-time**, in unary. -/ +theorem monomialsIn_polyTime : + ComputableInPolyTime (fun (((test, t), chosen) : (List (List ℕ) × ℕ) × List (ℕ × ℕ)) => + monomialsIn test t chosen) encMonomialsIn encUnary := by + have htest := (fst (encList (encList encNat)) encUnary).comp + (fst (encPair (encList (encList encNat)) encUnary) (encList (encPair encNat encNat))) + -- The inner test: `(t, v) ∈ chosen`. + let encM := encPair encMonomialsIn (encList encNat) + have hq := fst encMonomialsIn (encList encNat) + have hinner : ComputableInPolyTime + (fun p : ((List (List ℕ) × ℕ) × List (ℕ × ℕ)) × List ℕ => p.2) encM + (encList encNat) := snd encMonomialsIn (encList encNat) + have hv := snd encM encNat + have hq' := hq.comp (fst encM encNat) + have ht := (unary_to_binary.comp ((snd (encList (encList encNat)) encUnary).comp + ((fst (encPair (encList (encList encNat)) encUnary) (encList (encPair encNat encNat))).comp + hq'))) + have hchosen := (snd (encPair (encList (encList encNat)) encUnary) + (encList (encPair encNat encNat))).comp hq' + have hmem := decide_mem (encA := encPair encNat encNat) hchosen (ht.prod hv) + have hall := allWithInput (test := fun (p : ((List (List ℕ) × ℕ) × List (ℕ × ℕ)) × List ℕ) + (v : ℕ) => decide ((p.1.1.2, v) ∈ p.1.2)) hinner hmem + exact (countPWithInput (test := fun (q : (List (List ℕ) × ℕ) × List (ℕ × ℕ)) (M : List ℕ) => + M.all fun v => decide ((q.1.2, v) ∈ q.2)) htest hall).of_enc_eq fun ((_, _), _) => rfl + +/-- The input of `rowTerm`: `P`, `ℓ` and the tests, then the chosen incidences. -/ +abbrev encRowTerm : (ℕ × ℕ × List (List (List ℕ))) × List (ℕ × ℕ) ↪ List Bool := + encPair (encPair encUnary (encPair encUnary (encList (encList (encList encNat))))) + (encList (encPair encNat encNat)) + +/-- `truncFl ℓ` is polynomial-time from `ℓ` in unary. -/ +theorem truncFl_polyTime : ComputableInPolyTime truncFl encUnary (encList encNat) := + (replicate (hcount := id') (hvalue := const 0)).of_enc_eq fun _ => rfl + +/-- **The product of the parity factors of the tests is polynomial-time.** -/ +theorem rowTerm_polyTime : + ComputableInPolyTime + (fun (((P, ℓ, tests), chosen) : (ℕ × ℕ × List (List (List ℕ))) × List (ℕ × ℕ)) => + rowTerm P ℓ tests chosen) encRowTerm (encList encNat) := by + have hctx := fst (encPair encUnary (encPair encUnary (encList (encList (encList encNat))))) + (encList (encPair encNat encNat)) + have hP := (fst _ _).comp hctx + have hℓ := (fst _ _).comp ((snd _ _).comp hctx) + have htests := (snd encUnary (encList (encList (encList encNat)))).comp ((snd _ _).comp hctx) + have hchosen := snd (encPair encUnary (encPair encUnary (encList (encList (encList encNat))))) + (encList (encPair encNat encNat)) + have hfl := truncFl_polyTime.comp hℓ + -- One step: multiply by the factor of test `t`. + let encS := encPair (encPair encRowTerm (encList encNat)) encUnary + have hx := (fst encRowTerm (encList encNat)).comp (fst (encPair encRowTerm (encList encNat)) + encUnary) + have hacc := (snd encRowTerm (encList encNat)).comp (fst (encPair encRowTerm (encList encNat)) + encUnary) + have ht := snd (encPair encRowTerm (encList encNat)) encUnary + have htest := (listGetD (encA := encList (encList encNat)) + (encL := encList (encList (encList encNat))) []).comp ((htests.comp hx).prod ht) + have hcount := monomialsIn_polyTime.comp ((htest.prod ht).prod (hchosen.comp hx)) + have hfac := factorCoeffs_polyTime.comp + ((((hP.comp hx).prod (hℓ.comp hx))).prod (unary_to_binary.comp hcount)) + have hstep := computableInPolyTime_mul (hP.comp hx) (hfl.comp hx) hacc hfac + have hone := computableInPolyTime_one hfl + have hPb := hP.polyBounded_length + have hℓb := hℓ.polyBounded_length + have hfold := foldlWithInput_of_bounded_growth (encA := encUnary) (encL := encList encUnary) + (step := fun (x : (ℕ × ℕ × List (List (List ℕ))) × List (ℕ × ℕ)) acc t => + mul x.1.1 (truncFl x.1.2.1) acc + (factorCoeffs x.1.1 x.1.2.1 (monomialsIn (x.1.2.2.getD t []) t x.2))) hone + ⟨range.comp ((length_list (encList (encList encNat))).comp htests), hstep, inferInstance, + inferInstance⟩ + (growth := fun x => (encUnary x.1.2.1).length * (2 * (encUnary x.1.1).length + 1)) + ⟨hℓb.mul (((PolyBounded.const 2).mul hPb).add (.const 1)), fun x acc t _ => by + have h := length_encList_le (length_mul x.1.1 (truncFl x.1.2.1) acc + (factorCoeffs x.1.1 x.1.2.1 (monomialsIn (x.1.2.2.getD t []) t x.2))) + fun _ h => lt_of_mem_mul h + simp only [length_truncFl, encUnary_apply, List.length_replicate] at h ⊢ + nlinarith⟩ + exact hfold.of_enc_eq fun ((_, _, _), _) => rfl + +/-- **The incidences chosen by a word are polynomial-time.** -/ +theorem chosenBy_polyTime : + ComputableInPolyTime (fun q : List (ℕ × ℕ) × List Bool => chosenBy q.1 q.2) + (encPair (encList (encPair encNat encNat)) encBits) (encList (encPair encNat encNat)) := by + have hzip := (zip (encPair encNat encNat) encBool).comp + ((fst (encList (encPair encNat encNat)) encBits).prod + (bitsToList.comp (snd (encList (encPair encNat encNat)) encBits))) + have htest : ComputableInPolyTime + (fun p : (List (ℕ × ℕ) × List Bool) × ((ℕ × ℕ) × Bool) => p.2.2) + (encPair (encPair (encList (encPair encNat encNat)) encBits) + (encPair (encPair encNat encNat) encBool)) encBool := + (snd (encPair encNat encNat) encBool).comp (snd _ _) + have hfilter := filterWithInput + (test := fun (_ : List (ℕ × ℕ) × List Bool) (p : (ℕ × ℕ) × Bool) => p.2) hzip htest + exact ((map (fst (encPair encNat encNat) encBool)).comp hfilter).of_enc_eq fun q => rfl + +/-- The encoding of the state of the sum of a row: the context and the accumulator. -/ +abbrev encRowState : RowCtx × List ℕ ↪ List Bool := encPair encRowCtx (encList encNat) + +/-- **One term of the sum of a row is polynomial-time.** -/ +theorem rowBody_polyTime : + ComputableInPolyTime rowBody (encPair (encPair encUnary encBits) encRowState) + encRowState := by + have hw := (snd encUnary encBits).comp (fst (encPair encUnary encBits) encRowState) + have hst := snd (encPair encUnary encBits) encRowState + have hctx := (fst encRowCtx (encList encNat)).comp hst + have hacc := (snd encRowCtx (encList encNat)).comp hst + have hP := (fst _ _).comp hctx + have hr1 := (snd _ _).comp hctx + have hℓ := (fst _ _).comp hr1 + have hr2 := (snd _ _).comp hr1 + have htests := (fst _ _).comp hr2 + have hsel := (snd (encList (encList (encList encNat))) (encList (encPair encNat encNat))).comp + hr2 + have hchosen := chosenBy_polyTime.comp (hsel.prod hw) + have hterm := rowTerm_polyTime.comp ((hP.prod (hℓ.prod htests)).prod hchosen) + have hfl := truncFl_polyTime.comp hℓ + have hadd := computableInPolyTime_add hP hfl hacc hterm + have hsub := computableInPolyTime_sub hP hfl hacc hterm + have hdiff := unary_to_binary.comp (unary_sub.comp + (((length_list (encPair encNat encNat)).comp hsel).prod (bitsCountWithInput hw (const true)))) + have hcond := (binary_mod.comp (hdiff.prod (const 2))).beq (const 0) + exact (hctx.prod (ite hcond hadd hsub)).of_enc_eq fun ((_, _), (_, _, _, _), _) => by + simp only [rowBody, Function.comp_apply, beq_iff_eq] + +/-- **The entries of columns are polynomial-time.** -/ +theorem colEntry_polyTime : + ComputableInPolyTime (fun q : ColDesc × List Bool => colEntry q.1 q.2) + (encPair encColDesc encBits) (encList encNat) := by + have hcol := fst encColDesc encBits + have hbs := snd encColDesc encBits + have hP := (fst _ _).comp hcol + have hr := (snd _ _).comp hcol + have hvars := (fst (encList encNat) (encList encBlock)).comp hr + have hblocks := (snd (encList encNat) (encList encBlock)).comp hr + have hsel := selected_polyTime.comp (hblocks.prod (blockIndices_polyTime.comp (hblocks.prod hbs))) + have hsnd := (map (snd encNat encNat)).comp + (hsel.comp (fst (encPair encColDesc encBits) encNat)) + have hmem := decide_not (decide_mem (encA := encNat) hsnd + (snd (encPair encColDesc encBits) encNat)) + have hu := countPWithInput (test := fun (q : ColDesc × List Bool) (v : ℕ) => + decide (v ∉ (selected q.1.2.2 (blockIndices q.1.2.2 q.2)).map Prod.snd)) hvars hmem + have hval := computableInPolyTime_mod_two_pow (binary_two_pow.comp hu) hP + exact (cons' hval (const [])).of_enc_eq fun ((_, _, _), _) => rfl + +end PolyTime + +end Cslib.Circuits.Frontier.IncidenceNetwork diff --git a/Complexity/Computability/Circuit/Frontier/TensorNetwork/TruncatedRing.lean b/Complexity/Computability/Circuit/Frontier/TensorNetwork/TruncatedRing.lean new file mode 100644 index 000000000..1516c7e28 --- /dev/null +++ b/Complexity/Computability/Circuit/Frontier/TensorNetwork/TruncatedRing.lean @@ -0,0 +1,174 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: candidate + +public import Complexity.Computability.Circuit.Frontier.TensorNetwork.Truncated +public import Complexity.Computability.PolyTime.GaloisRingArithmetic +import Complexity.Foundations.Data.Polynomial.CoeffList +import Mathlib.Algebra.Polynomial.Degree.Support +import Mathlib.Data.List.GetD + +/-! +# `B_{P,ℓ}` as a ring of coefficient lists + +Theorem D.1 of [OpenAI2026ETH] (p. 53) contracts networks with entries in +`B_{P,ℓ} = (ℤ / 2 ^ P)[V] / (V ^ ℓ)`. This ring is the ring `GaloisRingArith.Ring P fl` of +coefficient-list arithmetic modulo `2 ^ P` and a monic polynomial, for the monic polynomial +`V ^ ℓ`, whose lower coefficients `truncFl ℓ` are all zero (`monicOf_truncFl`). So the +coefficient-list operations of `GaloisRingArith` (`add`, `mul`, `neg`, `sub`, `one`, `zero`), +with their correctness (`GaloisRingArith.val_mul`, …) and polynomial-time certificates +(`GaloisRingArith.computableInPolyTime_mul`, …), are arithmetic in `B_{P,ℓ}`; no separate +multiplication of truncated coefficient lists is needed. + +The bridge to the contraction over `ℕ[V]` is the ring map `truncNatHom P ℓ : ℕ[X] → B_{P,ℓ}`. +It sends the polynomial of a coefficient list to its value (`truncNatHom_ofCoeffList`), and two +polynomials have the same image exactly when their coefficients below `ℓ` agree modulo `2 ^ P` +(`truncNatHom_eq_iff`). So the image of the contraction over `ℕ[V]` is the contraction of the +values of the entries in `B_{P,ℓ}` (`truncNatHom_polyContraction`). The same holds over `ℤ[X]` +(`truncRingHom`, `truncRingHom_eq_iff`), where the incidence expansion of Lemma D.2 (pp. 54–56) +lives. + +## Main definitions + +* `Cslib.Circuits.Frontier.truncFl`: the lower coefficients of `V ^ ℓ`. +* `Cslib.Circuits.Frontier.truncRingHom`, `Cslib.Circuits.Frontier.truncNatHom`: the maps + `ℤ[X] → B_{P,ℓ}` and `ℕ[X] → B_{P,ℓ}`. + +## Main results + +* `Cslib.Circuits.Frontier.monicOf_truncFl`: the monic polynomial is `V ^ ℓ`. +* `Cslib.Circuits.Frontier.truncRingHom_eq_iff`, `Cslib.Circuits.Frontier.truncNatHom_eq_iff`: + equality in `B_{P,ℓ}` is agreement of the coefficients below `ℓ` modulo `2 ^ P`. +* `Cslib.Circuits.Frontier.truncNatHom_ofCoeffList`: a coefficient list maps to its value. +* `Cslib.Circuits.Frontier.DescribedNetwork.truncNatHom_polyContraction`: the contraction over + `ℕ[V]` maps to the contraction of the values. + +## References + +* [OpenAI, *The Exponential Time Hypothesis is False*][OpenAI2026ETH], Theorem D.1 (p. 53) and + Lemma D.2 (pp. 54–56). +-/ + +public section + +namespace Cslib.Circuits.Frontier + +open Polynomial Finset GaloisRingArith + +/-- **The lower coefficients of `V ^ ℓ`**: `ℓ` zeros. With this modulus, +`GaloisRingArith.Ring P (truncFl ℓ)` is `B_{P,ℓ} = (ℤ / 2 ^ P)[V] / (V ^ ℓ)`. -/ +@[expose] def truncFl (ℓ : ℕ) : List ℕ := List.replicate ℓ 0 + +@[simp] theorem length_truncFl (ℓ : ℕ) : (truncFl ℓ).length = ℓ := List.length_replicate + +theorem getD_truncFl (ℓ i : ℕ) : (truncFl ℓ).getD i 0 = 0 := by + unfold truncFl + by_cases h : i < ℓ + · rw [List.getD_eq_getElem _ _ (by simpa using h)] + simp + · rw [List.getD_eq_default _ _ (by simpa using h)] + +/-- The monic polynomial with lower coefficients `truncFl ℓ` is `V ^ ℓ`. -/ +theorem monicOf_truncFl (ℓ : ℕ) : monicOf (truncFl ℓ) = X ^ ℓ := by + rw [monicOf, length_truncFl, add_eq_left] + refine sum_eq_zero fun i _ => ?_ + rw [getD_truncFl] + simp + +variable {P ℓ : ℕ} + +/-- The defining polynomial of `B_{P,ℓ}` is `V ^ ℓ` over `ℤ / 2 ^ P`. -/ +theorem map_monicOf_truncFl : + (monicOf (truncFl ℓ)).map (Int.castRingHom (ZMod (2 ^ P))) = X ^ ℓ := by + rw [monicOf_truncFl, Polynomial.map_pow, map_X] + +/-- **The map `ℤ[V] → B_{P,ℓ}`**: reduce the coefficients modulo `2 ^ P`, then modulo `V ^ ℓ`. -/ +noncomputable def truncRingHom (P ℓ : ℕ) : ℤ[X] →+* Ring P (truncFl ℓ) := + (AdjoinRoot.mk _).comp (mapRingHom (Int.castRingHom (ZMod (2 ^ P)))) + +theorem truncRingHom_X : truncRingHom P ℓ X = AdjoinRoot.root _ := by + simp [truncRingHom] + +theorem truncRingHom_C (z : ℤ) : truncRingHom P ℓ (C z) = (z : Ring P (truncFl ℓ)) := by + simp [truncRingHom] + +/-- **Equality in `B_{P,ℓ}`** of the images of two integer polynomials is agreement of their +coefficients below `ℓ` modulo `2 ^ P`. -/ +theorem truncRingHom_eq_iff {p q : ℤ[X]} : + truncRingHom P ℓ p = truncRingHom P ℓ q ↔ ∀ j < ℓ, p.coeff j ≡ q.coeff j [ZMOD 2 ^ P] := by + rw [truncRingHom, RingHom.comp_apply, RingHom.comp_apply, AdjoinRoot.mk_eq_mk, + map_monicOf_truncFl, X_pow_dvd_iff] + refine forall₂_congr fun j _ => ?_ + rw [coeff_sub, sub_eq_zero, coe_mapRingHom, coeff_map, coeff_map, eq_intCast, eq_intCast, + ZMod.intCast_eq_intCast_iff, Nat.cast_pow, Nat.cast_ofNat] + +/-- `V ^ ℓ = 0` in `B_{P,ℓ}`. -/ +theorem root_pow_truncFl : (AdjoinRoot.root _ : Ring P (truncFl ℓ)) ^ ℓ = 0 := by + have h := root_pow_length (p := P) (fl := truncFl ℓ) + rw [length_truncFl] at h + rw [h, neg_eq_zero] + refine sum_eq_zero fun i _ => ?_ + rw [getD_truncFl] + simp + +/-- **The map `ℕ[V] → B_{P,ℓ}`**, through `ℤ[V]`. -/ +noncomputable def truncNatHom (P ℓ : ℕ) : ℕ[X] →+* Ring P (truncFl ℓ) := + (truncRingHom P ℓ).comp (mapRingHom (Nat.castRingHom ℤ)) + +/-- **Equality in `B_{P,ℓ}`** of the images of two natural polynomials is agreement of their +coefficients below `ℓ` modulo `2 ^ P`. -/ +theorem truncNatHom_eq_iff {p q : ℕ[X]} : + truncNatHom P ℓ p = truncNatHom P ℓ q ↔ ∀ j < ℓ, p.coeff j % 2 ^ P = q.coeff j % 2 ^ P := by + rw [truncNatHom, RingHom.comp_apply, RingHom.comp_apply, truncRingHom_eq_iff] + refine forall₂_congr fun j _ => ?_ + simp only [coe_mapRingHom, coeff_map, Nat.coe_castRingHom] + rw [show (2 : ℤ) ^ P = ((2 ^ P : ℕ) : ℤ) by push_cast; rfl, Int.natCast_modEq_iff] + rfl + +/-- **A coefficient list maps to its value**: the image of `ofCoeffList c` in `B_{P,ℓ}` is +`GaloisRingArith.val P (truncFl ℓ) c`. -/ +theorem truncNatHom_ofCoeffList (c : List ℕ) : + truncNatHom P ℓ (ofCoeffList c) = GaloisRingArith.val P (truncFl ℓ) c := by + have hterm (i : ℕ) : truncNatHom P ℓ (C (c.getD i 0) * X ^ i) = + ((c.getD i 0 : ℕ) : Ring P (truncFl ℓ)) * AdjoinRoot.root _ ^ i := by + simp [truncNatHom, truncRingHom] + have hsum : ofCoeffList c = ∑ i ∈ range (c.length + 1), C (c.getD i 0) * X ^ i := by + conv_lhs => rw [as_sum_range' (ofCoeffList c) (c.length + 1) + ((natDegree_ofCoeffList_le c).trans_lt (by omega))] + simp only [coeff_ofCoeffList, ← C_mul_X_pow_eq_monomial] + rw [hsum, map_sum, GaloisRingArith.val, length_truncFl] + simp only [hterm] + -- Both sums agree with the sum below `max |c| ℓ`. + have hzero : ∀ i, ¬ (i < c.length ∧ i < ℓ) → + ((c.getD i 0 : ℕ) : Ring P (truncFl ℓ)) * AdjoinRoot.root _ ^ i = 0 := by + intro i hi + by_cases hc : i < c.length + · have hℓ : ℓ ≤ i := by omega + rw [← Nat.add_sub_cancel' hℓ, pow_add, root_pow_truncFl, zero_mul, mul_zero] + · rw [List.getD_eq_default _ _ (by omega)] + simp + rw [← sum_subset (range_subset_range.mpr (Nat.min_le_left (c.length + 1) ℓ)) fun i _ hi => + hzero i (by simp only [mem_range] at hi; omega), + ← sum_subset (range_subset_range.mpr (Nat.min_le_right (c.length + 1) ℓ)) fun i _ hi => + hzero i (by simp only [mem_range] at hi; omega)] + +namespace DescribedNetwork + +variable {T : Type*} + +/-- **The contraction over `ℕ[V]` in `B_{P,ℓ}`** is the contraction of the values of the +entries. -/ +theorem truncNatHom_polyContraction (entry : T → List Bool → List ℕ) (G : DescribedNetwork T) : + truncNatHom P ℓ (G.polyContraction entry) = + G.contraction fun t bs => GaloisRingArith.val P (truncFl ℓ) (entry t bs) := by + rw [polyContraction, map_contraction] + simp only [truncNatHom_ofCoeffList] + +end DescribedNetwork + +end Cslib.Circuits.Frontier diff --git a/Complexity/Computability/GenericRAM/Native/SubsetPairFold.lean b/Complexity/Computability/GenericRAM/Native/SubsetPairFold.lean index 47f638d44..8db08ada0 100644 --- a/Complexity/Computability/GenericRAM/Native/SubsetPairFold.lean +++ b/Complexity/Computability/GenericRAM/Native/SubsetPairFold.lean @@ -10,6 +10,7 @@ module public import Complexity.Init public import Complexity.Computability.GenericRAM.Native.IndexFold public import Complexity.Foundations.Combinatorics.SubsetPairCount +public import Complexity.Foundations.Data.BitString.Combination public import Complexity.Foundations.Data.BitString.Support import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Plain import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Iteration @@ -358,68 +359,25 @@ private theorem findBucket_of_le {n q j : ℕ} (hj : subsetPairCount n q ≤ j) have hnot : ¬(j < subsetPairCount n q) := by omega simp only [hnot, ↓reduceIte] at hspec; simp only [Internal.findBucket, hspec] -private def pureUnrankComb : ℕ → ℕ → ℕ → List Bool - | 0, _, _ => [] - | m + 1, k, r => - if r < m.choose k then false :: pureUnrankComb m k r - else true :: pureUnrankComb m (k - 1) (r - m.choose k) - private theorem foldl_unrankCombStep_eq {N m : ℕ} (hm : m ≤ N) (k r : ℕ) (acc : List Bool) : ((List.range m).reverse.foldl (Internal.unrankCombStep (pascalTable N)) ((k, r), acc)).2 = - acc ++ pureUnrankComb m k r := by + acc ++ unrankCombination m k r := by induction m generalizing k r acc with - | zero => simp [pureUnrankComb] + | zero => simp [unrankCombination] | succ m ih => rw [List.range_succ, List.reverse_append, List.reverse_singleton, List.singleton_append, - List.foldl_cons, pureUnrankComb] + List.foldl_cons, unrankCombination] have hm_le : m ≤ N := by omega simp only [Internal.unrankCombStep, getD_pascalTable_eq_choose hm_le k]; split_ifs · rw [ih hm_le k r (acc ++ [false]), List.append_assoc, List.singleton_append] · rw [ih hm_le (k - 1) (r - m.choose k) (acc ++ [true]), List.append_assoc, List.singleton_append] -private theorem unrankComb_eq_pure (n k r : ℕ) : - Internal.unrankComb n k r (pascalTable n) = pureUnrankComb n k r := by +/-- The table-driven unranker computes `Cslib.BitString.unrankCombination`. -/ +theorem unrankComb_eq_unrankCombination (n k r : ℕ) : + Internal.unrankComb n k r (pascalTable n) = unrankCombination n k r := by simpa only [Internal.unrankComb, List.nil_append] using foldl_unrankCombStep_eq le_rfl k r [] -private theorem length_pureUnrankComb (m k r : ℕ) : (pureUnrankComb m k r).length = m := by - induction m generalizing k r with - | zero => rfl - | succ m ih => simp only [pureUnrankComb]; split_ifs <;> simp [ih] - -private theorem count_true_pureUnrankComb {m k r : ℕ} (hr : r < m.choose k) : - (pureUnrankComb m k r).count true = k := by - induction m generalizing k r with - | zero => cases k with | zero => rfl | succ k => simp at hr - | succ m ih => - simp only [pureUnrankComb]; split_ifs with hlt - · simp [ih hlt] - · cases k with - | zero => simp only [Nat.choose_zero_right] at hr hlt; omega - | succ k => - rw [Nat.choose_succ_succ, Nat.succ_eq_add_one] at hr - simp [ih (by omega : r - m.choose (k + 1) < m.choose k)] - -private theorem pureUnrankComb_injective {m k r₁ r₂ : ℕ} - (hr₁ : r₁ < m.choose k) (hr₂ : r₂ < m.choose k) - (heq : pureUnrankComb m k r₁ = pureUnrankComb m k r₂) : r₁ = r₂ := by - induction m generalizing k r₁ r₂ with - | zero => - cases k with - | zero => simp only [Nat.choose_zero_right, Nat.lt_one_iff] at hr₁ hr₂; omega - | succ k => simp at hr₁ - | succ m ih => - simp only [pureUnrankComb] at heq; split_ifs at heq with h₁ h₂ h₂ - · simp only [List.cons.injEq, true_and] at heq; exact ih h₁ h₂ heq - · simp at heq - · simp at heq - · simp only [List.cons.injEq, true_and] at heq - cases k with - | zero => simp only [Nat.choose_zero_right] at hr₁ h₁; omega - | succ k => - rw [Nat.choose_succ_succ, Nat.succ_eq_add_one] at hr₁ hr₂ - have := ih (by omega : r₁ - m.choose (k + 1) < m.choose k) (by omega) heq; omega - private def pureScatter : List Bool → ℕ → List Bool | [], _ => [] | b :: bs, mask => @@ -480,7 +438,7 @@ theorem unrankSubsetPair_of_le {n q j : ℕ} (hj : subsetPairCount n q ≤ j) : (unrankSubsetPair n q j).1.length = n := by by_cases hj : j < subsetPairCount n q · obtain ⟨_, _, hfb, -⟩ := findBucket_of_lt hj - simp [unrankSubsetPair, hfb, unrankComb_eq_pure, length_pureUnrankComb] + simp [unrankSubsetPair, hfb, unrankComb_eq_unrankCombination, length_unrankCombination] · rw [unrankSubsetPair_of_le (by omega)]; simp /-- The second indicator `indU` returned by `unrankSubsetPair n q j` has exact length `n`. -/ @@ -489,8 +447,8 @@ theorem unrankSubsetPair_of_le {n q j : ℕ} (hj : subsetPairCount n q ≤ j) : dsimp only [DecodedPair.indU, DecodedPair.innerSign] by_cases hj : j < subsetPairCount n q · obtain ⟨_, _, hfb, -⟩ := findBucket_of_lt hj - simp [unrankSubsetPair, hfb, scatterMask_eq_pure, length_pureScatter, unrankComb_eq_pure, - length_pureUnrankComb] + simp [unrankSubsetPair, hfb, scatterMask_eq_pure, length_pureScatter, + unrankComb_eq_unrankCombination, length_unrankCombination] · rw [unrankSubsetPair_of_le (by omega)]; simp /-- Pointwise containment: every `true` position of `indU` is also `true` in `indE`. -/ @@ -511,8 +469,8 @@ theorem count_true_fst_unrankSubsetPair_le (n q j : ℕ) : · obtain ⟨s, offset, hfb, hs_le, hoff_lt, -⟩ := findBucket_of_lt hj have hr_lt : offset / 2 ^ s < n.choose s := by rw [Nat.div_lt_iff_lt_mul (by positivity), Nat.mul_comm]; exact hoff_lt - simp only [unrankSubsetPair, hfb, Option.elim_some, unrankComb_eq_pure, - count_true_pureUnrankComb hr_lt]; exact hs_le + simp only [unrankSubsetPair, hfb, Option.elim_some, unrankComb_eq_unrankCombination, + count_true_unrankCombination hr_lt]; exact hs_le · rw [unrankSubsetPair_of_le (by omega)]; simp [List.count_replicate] /-- The third component `negSign` is `decide (Odd (indE.count true - indU.count true))`. -/ @@ -561,17 +519,20 @@ private theorem unrankPair_injective {n q j₁ j₂ : ℕ} rw [Nat.div_lt_iff_lt_mul (by positivity), Nat.mul_comm]; exact hoff₂ simp only [unrankSubsetPair, hfb₁, hfb₂, Option.elim_some] at hE hU have hs_eq : s₁ = s₂ := by - simpa only [unrankComb_eq_pure, count_true_pureUnrankComb hr₁, - count_true_pureUnrankComb hr₂] using congrArg (List.count true) hE + simpa only [unrankComb_eq_unrankCombination, count_true_unrankCombination hr₁, + count_true_unrankCombination hr₂] using congrArg (List.count true) hE subst hs_eq have hr_eq : off₁ / 2 ^ s₁ = off₂ / 2 ^ s₁ := by - simp only [unrankComb_eq_pure] at hE; exact pureUnrankComb_injective hr₁ hr₂ hE + simp only [unrankComb_eq_unrankCombination] at hE + exact unrankCombination_injective hr₁ hr₂ hE have hm₁ : off₁ % 2 ^ s₁ < 2 ^ (Internal.unrankComb n s₁ (off₁ / 2 ^ s₁) (pascalTable n)).count true := by - rw [unrankComb_eq_pure, count_true_pureUnrankComb hr₁]; exact Nat.mod_lt off₁ (by positivity) + rw [unrankComb_eq_unrankCombination, count_true_unrankCombination hr₁] + exact Nat.mod_lt off₁ (by positivity) have hm₂ : off₂ % 2 ^ s₁ < 2 ^ (Internal.unrankComb n s₁ (off₁ / 2 ^ s₁) (pascalTable n)).count true := by - rw [unrankComb_eq_pure, count_true_pureUnrankComb hr₁]; exact Nat.mod_lt off₂ (by positivity) + rw [unrankComb_eq_unrankCombination, count_true_unrankCombination hr₁] + exact Nat.mod_lt off₂ (by positivity) rw [← hE] at hU; simp only [scatterMask_eq_pure] at hU have hm_eq := pureScatter_injective hm₁ hm₂ hU have hd₁ := Nat.div_add_mod off₁ (2 ^ s₁); have hd₂ := Nat.div_add_mod off₂ (2 ^ s₁) @@ -831,9 +792,12 @@ private theorem computableInPolyTime_findBucket : (by omega) hj_le hn_le) exact hfold.snd' -private theorem computableInPolyTime_unrankComb : +/-- The table-driven unranker is polynomial-time, from `(n, k)` in unary, the rank in binary and +the table. -/ +@[fun_prop, program_certificate] theorem unrankComb_polyTime : ComputableInPolyTime - (fun p : ((ℕ × ℕ) × ℕ) × List (List ℕ) => Internal.unrankComb p.1.1.1 p.1.1.2 p.1.2 p.2) + (fun ((((n, k), rank), table) : ((ℕ × ℕ) × ℕ) × List (List ℕ)) => + Internal.unrankComb n k rank table) (encPair (encPair encParams encNat) (encList (encList encNat))) encBits := by let encTab := encList (encList encNat); let encIn := encPair (encPair encParams encNat) encTab let encSt := encPair (encPair encUnary encNat) encBits @@ -911,7 +875,7 @@ private theorem computableInPolyTime_scatterMask : have hq_fst := fst encIn (encPair encUnary encNat) have hq_snd := snd encIn (encPair encUnary encNat) have hq_pow := binary_two_pow.comp hq_snd.fst' - have hq_indE := computableInPolyTime_unrankComb.comp + have hq_indE := unrankComb_polyTime.comp ((((hn_in.comp hq_fst).prod hq_snd.fst').prod (binary_div.comp (hq_snd.snd'.prod hq_pow))).prod (htab.comp hq_fst)) have hq_indU := computableInPolyTime_scatterMask.comp @@ -921,6 +885,15 @@ private theorem computableInPolyTime_scatterMask : have hq_sign := (binary_mod.comp ((unary_to_binary.comp hq_diff).prod (const 2))).beq (const 1) exact optionElimWithInput hfb hfall (hq_indE.prod (hq_indU.prod hq_sign)) +/-- **Unranking combinations is polynomial-time**, from `(m, k)` in unary and the rank in +binary. -/ +@[fun_prop, program_certificate] theorem unrankCombination_polyTime : + ComputableInPolyTime (fun (((m, k), rank) : (ℕ × ℕ) × ℕ) => unrankCombination m k rank) + (encPair encParams encNat) encBits := + (unrankComb_polyTime.comp + (id'.prod (pascalTable_polyTime.comp (fst encParams encNat).fst'))).of_enc_eq + fun ((m, k), rank) => congrArg encBits (unrankComb_eq_unrankCombination m k rank).symm + end PlainProofs /-- Native certificate for `pascalTable`, selected via `NativeCertificate.ofPolyTime`. -/ diff --git a/Complexity/Foundations/Data/BitString/Combination.lean b/Complexity/Foundations/Data/BitString/Combination.lean new file mode 100644 index 000000000..57a4671d0 --- /dev/null +++ b/Complexity/Foundations/Data/BitString/Combination.lean @@ -0,0 +1,87 @@ +/- +Copyright (c) 2026 Anton Kovsharov. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Anton Kovsharov +-/ + +module +-- upstream: candidate + +public import Complexity.Init +public import Mathlib.Data.Nat.Choose.Basic + +/-! +# Unranking combinations + +The weight-`k` indicators of length `m`, ordered lexicographically with `false` first, are +numbered `0, …, C(m, k) - 1`. `Cslib.BitString.unrankCombination m k r` is the indicator of rank +`r`: its first bit is `false` exactly when `r` is below the `C(m - 1, k)` indicators that start +with `false`. + +## Main definitions + +* `Cslib.BitString.unrankCombination`: the weight-`k` indicator of length `m` of a given rank. + +## Main results + +* `Cslib.BitString.length_unrankCombination`: the indicator has length `m`. +* `Cslib.BitString.count_true_unrankCombination`: a rank below `C(m, k)` gives weight `k`. +* `Cslib.BitString.unrankCombination_injective`: distinct ranks below `C(m, k)` give distinct + indicators. +-/ + +@[expose] public section + +namespace Cslib.BitString + +/-- **The combination of rank `r`** among the weight-`k` indicators of length `m`, in the +lexicographic order with `false` first. A rank `r < C(m, k)` gives an indicator of weight `k` +(`count_true_unrankCombination`), and distinct ranks give distinct indicators +(`unrankCombination_injective`). -/ +def unrankCombination : ℕ → ℕ → ℕ → List Bool + | 0, _, _ => [] + | m + 1, k, r => + if r < m.choose k then false :: unrankCombination m k r + else true :: unrankCombination m (k - 1) (r - m.choose k) + +@[simp] theorem length_unrankCombination (m k r : ℕ) : (unrankCombination m k r).length = m := by + induction m generalizing k r with + | zero => rfl + | succ m ih => simp only [unrankCombination]; split_ifs <;> simp [ih] + +/-- A rank below `C(m, k)` unranks to an indicator of weight `k`. -/ +theorem count_true_unrankCombination {m k r : ℕ} (hr : r < m.choose k) : + (unrankCombination m k r).count true = k := by + induction m generalizing k r with + | zero => cases k with | zero => rfl | succ k => simp at hr + | succ m ih => + simp only [unrankCombination]; split_ifs with hlt + · simp [ih hlt] + · cases k with + | zero => simp only [Nat.choose_zero_right] at hr hlt; omega + | succ k => + rw [Nat.choose_succ_succ, Nat.succ_eq_add_one] at hr + simp [ih (by omega : r - m.choose (k + 1) < m.choose k)] + +/-- Distinct ranks below `C(m, k)` unrank to distinct indicators. -/ +theorem unrankCombination_injective {m k r₁ r₂ : ℕ} + (hr₁ : r₁ < m.choose k) (hr₂ : r₂ < m.choose k) + (heq : unrankCombination m k r₁ = unrankCombination m k r₂) : r₁ = r₂ := by + induction m generalizing k r₁ r₂ with + | zero => + cases k with + | zero => simp only [Nat.choose_zero_right, Nat.lt_one_iff] at hr₁ hr₂; omega + | succ k => simp at hr₁ + | succ m ih => + simp only [unrankCombination] at heq; split_ifs at heq with h₁ h₂ h₂ + · simp only [List.cons.injEq, true_and] at heq; exact ih h₁ h₂ heq + · simp at heq + · simp at heq + · simp only [List.cons.injEq, true_and] at heq + cases k with + | zero => simp only [Nat.choose_zero_right] at hr₁ h₁; omega + | succ k => + rw [Nat.choose_succ_succ, Nat.succ_eq_add_one] at hr₁ hr₂ + have := ih (by omega : r₁ - m.choose (k + 1) < m.choose k) (by omega) heq; omega + +end Cslib.BitString diff --git a/ComplexityTests/Computability/Circuit/Frontier/TensorNetworkIncidenceEntry.lean b/ComplexityTests/Computability/Circuit/Frontier/TensorNetworkIncidenceEntry.lean new file mode 100644 index 000000000..1bae630ab --- /dev/null +++ b/ComplexityTests/Computability/Circuit/Frontier/TensorNetworkIncidenceEntry.lean @@ -0,0 +1,124 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: local-only (test driver) + +public import Complexity.Computability.Circuit.Frontier.TensorNetwork.IncidenceEntryCertificate + +/-! +# Tests for the entries of the incidence network of Lemma D.2 + +A block of the two incidences `(0, 0), (0, 1)` with one selected has one index wire: the index +`0` selects `(0, 1)` and the index `1` selects `(0, 0)`, in the lexicographic order of the +combinations. At the index `1`, a column of the variables `0, 1, 2` with that block has two +unselected variables, so its entry is `2 ^ 2` modulo `2 ^ 3`. A block of three incidences of test +`1` with two selected has `⌈log₂ 3⌉ = 2` wires; the index `3` is invalid, so the row has entry +zero. + +**A valid row.** The tests `x₀ + x₁` and `x₂ + x₂ x₃` form one group (`J = 1`). At precision +`P = 4`, truncation order `ℓ = 2` and three selected incidences, their row is the row vertex of the +incidence network, with the four incidences `(0, 0), (0, 1), (1, 2), (1, 3)` in one block and two +index wires. For `ℓ = 2` the parity factor is `B(y; V) = (1 - y) + (2 y - 1) y (y - 1) V`, since +`parityLinearCoeffs 2 = [(1, -1), (-1, 2)]`: `B(0) = 1`, `B(1) = 0` and `B(2) = -1 + 6 V`. The +entry is `∏_t ∑_{T ⊆ S_t} (-1) ^ (|S_t| - |T|) B(m_t(T))`, for `m_t(T)` the monomials of test `t` +inside `T`. +* The index `3` selects `S₀ = {x₀, x₁}` and `S₁ = {x₂}`. Test `0` has `m₀(T) = 0, 1, 1, 2` on + `T = ∅, {x₀}, {x₁}, {x₀, x₁}`, and test `1` has `m₁(T) = 0, 1` on `T = ∅, {x₂}`. So the entry is + `(B(0) - 2 B(1) + B(2)) (B(1) - B(0)) = 6 V · (-1) = -6 V`, that is `10 V` modulo `16`. +* The index `0` selects `S₀ = {x₁}` and `S₁ = {x₂, x₃}`, with `m₁(T) = 0, 1, 0, 2` on + `T = ∅, {x₂}, {x₃}, {x₂, x₃}`. The entry is `(B(1) - B(0)) (B(0) - B(1) - B(0) + B(2))`, + which is `(-1) (-1 + 6 V) = 1 - 6 V`, that is `1 + 10 V`. +* The index `2` selects `S₁ = {x₃}`, inside which test `1` has no monomial, so the entry is `0`. + +The tests check these coefficients, and the product of the per-test subset sums in `B_{4,2}`. The +signs matter: summing the subsets without signs would give `6 V` and `1 + 6 V`. +-/ + +@[expose] public section + +namespace ComplexityTests.TensorNetworkIncidenceEntry + +open Cslib.Circuits.Frontier Cslib.Circuits.Frontier.IncidenceNetwork + +/-- A block of two incidences of test `0`, one selected. -/ +abbrev b₁ : Block := ([(0, 0), (0, 1)], 1) + +/-- A block of three incidences of test `1`, two selected. -/ +abbrev b₂ : Block := ([(1, 0), (1, 1), (1, 2)], 2) + +example : blockWires b₁ = 1 := by decide +example : blockWires b₂ = 2 := by decide +example : blockIndices [b₁, b₂] [true, false, true] = [1, 2] := by decide +example : selectBlock b₁ 0 = [(0, 1)] := by decide +example : selectBlock b₁ 1 = [(0, 0)] := by decide +example : selected [b₁, b₂] [1, 2] = [(0, 0), (1, 0), (1, 1)] := by decide +example : validIndices [b₁, b₂] [1, 2] = true := by decide +example : validIndices [b₁, b₂] [1, 3] = false := by decide + +-- The column of the variables `0, 1, 2`: the index `1` selects variable `0`. +example : colEntry (3, [0, 1, 2], [b₁]) [true] = [4] := by decide + +-- An invalid index gives the row entry zero. +example : rowEntry (2, 1, [[[0]]], [b₂]) [true, true] = [] := + rowEntry_of_not_valid (by decide) + +/-! ### A valid row -/ + +/-- The tests `x₀ + x₁` and `x₂ + x₂ x₃`. -/ +abbrev sys : List (List (List ℕ)) := [[[0], [1]], [[2], [2, 3]]] + +/-- The block of their incidences, three selected. -/ +abbrev blk : Block := ([(0, 0), (0, 1), (1, 2), (1, 3)], 3) + +/-- Their row at precision `4` and truncation order `2`. -/ +abbrev row : RowDesc := (4, 2, sys, [blk]) + +-- It is the row vertex of the incidence network with one group, on the index wires `0, 1`. +example : rowVertex 4 2 1 sys [3] 0 = ([0, 1], .inl row) := rfl + +-- The bits read the indices little-endian, and every index is valid. +example : blockIndices [blk] [true, true] = [3] := by decide +example : blockIndices [blk] [false, true] = [2] := by decide +example : validIndices [blk] [3] = true := by decide +example : selected [blk] [3] = [(0, 0), (0, 1), (1, 2)] := by decide +example : selected [blk] [0] = [(0, 1), (1, 2), (1, 3)] := by decide +example : selected [blk] [2] = [(0, 0), (0, 1), (1, 3)] := by decide + +-- The parity factor `B(y; V) = (1 - y) + (2 y - 1) y (y - 1) V` modulo `2 ^ 4`. +example : Cslib.parityLinearCoeffs 2 = [(1, -1), (-1, 2)] := by decide +example : factorCoeffs 4 2 0 = [1, 0] := by decide +example : factorCoeffs 4 2 1 = [0, 0] := by decide +example : factorCoeffs 4 2 2 = [15, 6] := by decide + +-- The index `3`: `-6 V`. +example : rowEntry row [true, true] = [0, 10] := by decide + +-- The index `3` is the product of the per-test subset sums `B(0) - 2 B(1) + B(2)` and +-- `B(1) - B(0)` in `B_{4,2}`. +open Cslib.GaloisRingArith in +example : rowEntry row [true, true] = + mul 4 (truncFl 2) + (add 4 (truncFl 2) + (sub 4 (truncFl 2) (sub 4 (truncFl 2) (factorCoeffs 4 2 0) (factorCoeffs 4 2 1)) + (factorCoeffs 4 2 1)) + (factorCoeffs 4 2 2)) + (sub 4 (truncFl 2) (factorCoeffs 4 2 1) (factorCoeffs 4 2 0)) := by decide + +-- The index `0`: `1 - 6 V`. +example : rowEntry row [false, false] = [1, 10] := by decide + +-- The index `2`: test `1` has no monomial inside `{x₃}`. +example : rowEntry row [false, true] = [0, 0] := by decide + +-- The certificate bound is not vacuous: its constant exists. +example : ∃ c : ℕ, ∀ q : Desc × List Bool, + incCertificate.time q ≤ c * ((Turing.MultiTapeTM.encPair encDesc + Turing.MultiTapeTM.encBits q).length + 1) ^ c * 2 ^ descInc q.1 := + let ⟨c, h⟩ := exists_incCertificate_le + ⟨c, fun q => (h q).1⟩ + +end ComplexityTests.TensorNetworkIncidenceEntry