QEC 265 declarations in 18 modules

FormalRV.QEC.Addressing

FormalRV/QEC/Addressing.lean

FormalRV.QEC.Addressing — the LOGICAL ADDRESSING layer. In a qLDPC block the `k` logical qubits are not physically separable; addressing a SUBSET `S` (e.g. {2,5,7} of a `[[144,12,12]]` block) for a PPM is a compilation concern. This file makes the split explicit: (a) the `LogicalBasis` is the TRUSTED address book the user provides (index `i ↦` physical support of X̄_i / Z̄_i; its `valid` / `pairs_delta` δ_ij invariant is what makes index `i` a genuine separable logical qubit); (b) `selectZ S` forms the addressed operator `∏_{i∈S} Z̄_i` (EASY — GF(2) sum of supports), and `addressedTargetZ` is the surgery `target_pauli`; (c) SYNTHESIZING the ancilla system + connection `f_X'` so that `ker(H_X'^T)` addresses exactly `S` is the HARD compilation (qianxu dynamic ancilla, `O(exp k)` gadgets) — done by the implementer, NOT here; (d) VERIFYING a provided gadget measures exactly the addressed product is DECIDABLE via `SurgeryGadget.targets_logical_correctly` (`row_combination span_witness merged_hx = addressedTargetZ S anc`) plus `surgery_readout_operator` / `surgery_eigenvalue`. So: the user provides the logical-Z definitions ⟹ addressed-PPM verification is decidable. Synthesis hard, verification easy. No Mathlib. Pure Bool / Nat / List + `decide`.

defselectZ

def selectZ {c k} (L : LogicalBasis c k) (S : List (Fin k)) : BoolVec

Support of `∏_{i∈S} Z̄_i`: the GF(2) sum of the selected logical-Z supports. `foldr` over `S` with base `zero_vec c.n`, so that `selectZ (i :: S) = vec_xor (lz i) (selectZ S)` holds definitionally.

defselectX

def selectX {c k} (L : LogicalBasis c k) (S : List (Fin k)) : BoolVec

Support of `∏_{i∈S} X̄_i`: the GF(2) sum of the selected logical-X supports.

defaddressedTargetZ

def addressedTargetZ {c k} (L : LogicalBasis c k) (S : List (Fin k))
    (ancilla_n : Nat) : BoolVec

The surgery `target_pauli` for measuring `∏_{i∈S} Z̄_i`: the addressed Z-support, zero-extended onto an `ancilla_n`-qubit ancilla block.

defaddressedTargetX

def addressedTargetX {c k} (L : LogicalBasis c k) (S : List (Fin k))
    (ancilla_n : Nat) : BoolVec

The surgery `target_pauli` for measuring `∏_{i∈S} X̄_i`: the addressed X-support, zero-extended onto an `ancilla_n`-qubit ancilla block.

theoremselectZ_nil

theorem selectZ_nil {c k} (L : LogicalBasis c k) :
    L.selectZ [] = zero_vec c.n

Addressing the empty subset yields the identity (zero support).

theoremselectZ_cons

theorem selectZ_cons {c k} (L : LogicalBasis c k) (i : Fin k)
    (S : List (Fin k)) :
    L.selectZ (i :: S) = vec_xor (L.lz i) (L.selectZ S)

Prepending index `i` to the address list XORs in `Z̄_i`'s support.

theoremselectX_nil

theorem selectX_nil {c k} (L : LogicalBasis c k) :
    L.selectX [] = zero_vec c.n

Addressing the empty subset (X side) yields the identity.

theoremselectX_cons

theorem selectX_cons {c k} (L : LogicalBasis c k) (i : Fin k)
    (S : List (Fin k)) :
    L.selectX (i :: S) = vec_xor (L.lx i) (L.selectX S)

Prepending index `i` to the address list XORs in `X̄_i`'s support.

theoremselectZ_single

theorem selectZ_single {c k} (L : LogicalBasis c k) (i : Fin k) :
    L.selectZ [i] = vec_xor (L.lz i) (zero_vec c.n)

Single-qubit addressing is `vec_xor` of the chosen support with zero. (The general `vec_xor a (zero_vec a.length) = a` cancellation needs a length-indexed induction in a later module; here the `rfl` form plus `decide`-checked instances at concrete bases suffice.)

theoremselectX_single

theorem selectX_single {c k} (L : LogicalBasis c k) (i : Fin k) :
    L.selectX [i] = vec_xor (L.lx i) (zero_vec c.n)

Single-qubit addressing on the X side.

example(example)

example : code422Logical.valid = true

The basis is a valid address book: each index is a genuine logical qubit (commutes with stabilizers, realises the δ_ij pairing).

example(example)

example :
    code422Logical.selectZ [0, 1]
      = vec_xor (code422Logical.lz 0) (code422Logical.lz 1)

Addressing the subset {0,1}: the operator is `Z̄₀Z̄₁`, whose support is the GF(2) sum `lz 0 ⊕ lz 1`.

example(example)

example : code422Logical.selectZ [0, 1] = [false, true, true, false]

The concrete support of `Z̄₀Z̄₁` on the `[[4,2,2]]` block: `lz0 ⊕ lz1 = [T,F,T,F] ⊕ [T,T,F,F] = [F,T,T,F]`.

example(example)

example : code422Logical.selectZ [0] = code422Logical.lz 0

Single-qubit addressing {0}: the operator is `Z̄₀`, support `lz 0`.

example(example)

example : (code422Logical.addressedTargetZ [0, 1] 2).length = 6

The surgery `target_pauli` for measuring `Z̄₀Z̄₁` with a 2-qubit ancilla block has length 4 + 2 = 6.

example(example)

example : code422Logical.selectX [0, 1] = [false, true, true, false]

The X-side addressed product `X̄₀X̄₁` on the same block: `lx0 ⊕ lx1 = [T,T,F,F] ⊕ [T,F,T,F] = [F,T,T,F]`.

theoremaddressing_demo

theorem addressing_demo :
    code422Logical.addressedTargetZ [0, 1] 2
      = [false, true, true, false, false, false]

Demo anchor for `#print axioms`: the addressed-{0,1} Z target on a 2-qubit ancilla block is the concrete length-6 vector.

FormalRV.QEC.CSSCode

FormalRV/QEC/CSSCode.lean

FormalRV.QEC.CSSCode — the unified CSS-code pivot type, and the level's SEMANTIC-CORRECTNESS theorem: *the stabilizer-measurement circuit implements the specified code.** Design: `notes/topic-qec-code-framework.md`. The pivot representation is the GF(2) check-matrix pair `(hx, hz)` (`BoolMat`), reusing the `FormalRV.Framework.LDPC` toolbox + `GF2Linear`. A code can be built in three "languages" (algebraic / check-matrix / stabilizer); they all lower to this `(hx, hz)` pair. ## The semantic-correctness goal of this level A CSS code is *specified* by its check matrices. Its stabilizer- measurement circuit measures, for each row, the Pauli operator obtained by lowering that row (X-rows ↦ X/I strings via `xStab`, Z-rows ↦ Z/I strings via `zStab`). "This circuit implements the specified code" means exactly: those measured operators form a *valid stabilizer code* (a pairwise-commuting generating set) and they ARE the code's stabilizers. The headline theorem `syndrome_circuit_implements_code` proves this holds IFF the CSS commutation condition `H_X H_Z^T = 0`: valid (toStabilizers c) c.n ↔ c.css_condition i.e. the construction yields a genuine stabilizer code precisely when the CSS condition holds — the circuit implements the code. Note (layering / future unification): `xStab`/`zStab` here are the canonical check-matrix→Pauli lowering; the surgery layer's `SurgeryReadout.xRow` / `SurgeryCorrect.zRow` are definitionally the same and should later be re-pointed to import these (kept separate now to avoid a QEC→LatticeSurgery import inversion / touching committed files). No Mathlib. Pure Bool / Nat / List.

structureCSSCode

structure CSSCode

A CSS code as its GF(2) check-matrix pair. Mirrors `bposd.css_code`. `hx`/`hz` are the X- and Z-stabilizer parity matrices, rows of length `n`.

defwell_shaped

def well_shaped (c : CSSCode) : Bool

Every row of `hx` and `hz` has length `n`.

defcss_condition

def css_condition (c : CSSCode) : Bool

CSS commutation: `H_X · H_Z^T = 0` over GF(2).

defvalid

def valid (c : CSSCode) : Bool

All structural invariants of a CSS code.

defis_qldpc_code

def is_qldpc_code (c : CSSCode) (Δ : Nat) : Bool

qLDPC degree bound on both check matrices.

defxStab

def xStab (l : BoolVec) : PauliString

An X-type check row lowered to an X/I `PauliString`.

defzStab

def zStab (l : BoolVec) : PauliString

A Z-type check row lowered to a Z/I `PauliString`.

deftoStabilizers

def toStabilizers (c : CSSCode) : StabilizerState

*The stabilizer-measurement circuit of the code**: the X-checks lowered via `xStab`, then the Z-checks via `zStab`. This is the sequence of Pauli measurements that the syndrome-extraction circuit performs (each ancilla+CNOT+measure gadget realises one of these).

deftoQECCode

def toQECCode (c : CSSCode) (k d : Nat) : Framework.QECCode

Project to the flat L4 resource container. `k` and `d` are supplied separately (distance is NOT derived — honest residue; `k` derivation needs GF(2) rank, a later module).

defofQECCodeChecked

def ofQECCodeChecked (q : Framework.QECCode) : Option CSSCode

Smart constructor from a `QECCode` carrying matrices, checking the CSS invariants.

theoremxbit_commutes

theorem xbit_commutes (x y : Bool) : Pauli.commutes (xbit x) (xbit y) = true

Single-qubit X/I operators always commute.

theoremzbit_commutes

theorem zbit_commutes (x y : Bool) : Pauli.commutes (zbit x) (zbit y) = true

Single-qubit Z/I operators always commute.

theoremxStab_commutes

theorem xStab_commutes (a b : BoolVec) : (xStab a).commutes (xStab b) = true

Any two X/I strings commute.

theoremzStab_commutes

theorem zStab_commutes (a b : BoolVec) : (zStab a).commutes (zStab b) = true

Any two Z/I strings commute.

theoremxz_anti_count

theorem xz_anti_count (a b : BoolVec) :
    ((a.map xbit).zip (b.map zbit)).countP (fun p => ! p.1.commutes p.2)
      = (a.zip b).countP (fun p => p.1 && p.2)

At each position the X-vs-Z anticommutation indicator equals the GF(2) overlap bit, so the symplectic anticommuting-position count over the lowered strings equals the overlap count over the raw supports.

theoremxStab_zStab_commutes

theorem xStab_zStab_commutes (a b : BoolVec) :
    (xStab a).commutes (zStab b) = ! dotBit a b

An X-row stabilizer commutes with a Z-row stabilizer IFF their supports are GF(2)-orthogonal (even overlap) — the symplectic pairing equals the GF(2) inner product `dotBit`.

theoremsyndrome_circuit_implements_code

theorem syndrome_circuit_implements_code (c : CSSCode) (hws : c.well_shaped = true) :
    StabilizerState.valid (c.toStabilizers) c.n = true ↔ c.css_condition = true

*The stabilizer-measurement circuit implements the specified code.** For a well-shaped CSS code, the lowered measured operators `toStabilizers c` form a valid (pairwise-commuting) stabilizer code IFF the CSS commutation condition `H_X · H_Z^T = 0` holds. Equivalently: the syndrome-extraction circuit realises a genuine stabilizer code exactly when the specified check matrices are a valid CSS code, and the measured stabilizer group is exactly `{xStab(hxᵢ)} ∪ {zStab(hzⱼ)}`.

FormalRV.QEC.CodeDimension

FormalRV/QEC/CodeDimension.lean

FormalRV.QEC.CodeDimension — the logical-qubit count of a CSS code, DERIVED from its constructed parity matrices over GF(2): k = n − rank(H_X) − rank(H_Z). GENERAL / reusable: every qLDPC-code paper uses this to DERIVE `k` from the matrices (rather than asserting it). It lives in the framework `QEC/` layer — not in any one paper's folder — so each `Audit/<Paper>/` imports it as general machinery.

defderivedK

def derivedK (c : CSSCode) : Nat

Logical-qubit count derived from a CSS code's parity matrices over GF(2): `k = n − rank(H_X) − rank(H_Z)`.

FormalRV.QEC.FrontendAlgebraic

FormalRV/QEC/FrontendAlgebraic.lean

FormalRV.QEC.FrontendAlgebraic -- the ALGEBRAIC frontend of the QEC code-construction framework. Builds CSS qLDPC codes from polynomial / product data and lowers each construction to the unified CSSCode pivot (hx, hz). Every constructor produces an honest GF(2) check-matrix pair; the CSS commutation condition H_X * H_Z^T = 0 is then derived (by decide) on concrete smoke instances. Constructions: identMat, kron, hypergraphProduct, repCode, surfaceHGP, shiftMat, shiftPow, matXor, biCirculant, bivariateBicycle, circulant, circDagger. Capstone: surfaceHGP3_circuit_implements instantiates CSSCode.syndrome_circuit_implements_code on the distance-3 surface code. No Mathlib. Pure Bool / Nat / List + decide / native_decide.

defidentMat

def identMat (n : Nat) : BoolMat

The n x n GF(2) identity matrix.

defkron

def kron (A B : BoolMat) : BoolMat

Kronecker product of two GF(2) matrices. If A is rA x cA and B is rB x cB, the result is (rA*rB) x (cA*cB), block (i,k),(j,l) = A i j and B k l.

example(example)

example : kron [[true]] (identMat 3) = identMat 3

example(example)

example : (kron (identMat 2) (identMat 3)).length = 2 * 3

example(example)

example : kron (identMat 2) (identMat 2) = identMat 4

defhypergraphProduct

def hypergraphProduct (h1 h2 : BoolMat) (m1 n1 m2 n2 : Nat) : CSSCode

The CSS hypergraph product of classical parity-check matrices h1 : m1 x n1 and h2 : m2 x n2. n = n1*n2 + m1*m2 hx = [ h1 (x) I_n2 | I_m1 (x) h2^T ] hz = [ I_n1 (x) h2 | h1^T (x) I_m2 ] CSS condition hx*hz^T = 0 holds since (h1(x)I)(I(x)h2^T) + (I(x)h2^T)(h1(x)I) = h1(x)h2^T + h1(x)h2^T = 0 over GF(2). Dimensions are passed explicitly to avoid re-deriving them.

defrepCode

def repCode (d : Nat) : BoolMat

The (d-1) x d consecutive-ones parity check of the distance-d repetition code: row i (for 0 <= i < d-1) has 1s at columns i and i+1.

defsurfaceHGP

def surfaceHGP (d : Nat) : CSSCode

The unrotated surface code at distance d = HGP(repCode d, repCode d). Parameters [[d^2 + (d-1)^2, 1, d]]. Here repCode d is (d-1) x d, so m1 = m2 = d-1 and n1 = n2 = d.

example(example)

example : (surfaceHGP 3).n = 13

example(example)

example : (surfaceHGP 3).well_shaped = true

example(example)

example : (surfaceHGP 3).css_condition = true

defshiftMat

def shiftMat (l : Nat) : BoolMat

The l x l cyclic shift matrix S_l: row i has a 1 at column (i+1) mod l.

defshiftPow

def shiftPow (l k : Nat) : BoolMat

S_l^k as a matrix: entry (i, (i+k) mod l) is 1.

defmatXor

def matXor (A B : BoolMat) : BoolMat

Entrywise GF(2) sum (XOR) of two equal-shape matrices.

defbiCirculant

def biCirculant (l m : Nat) (terms : List (Nat × Nat)) : BoolMat

A bivariate monomial sum over F2[x,y]/(x^l+1, y^m+1) as a list of (i,j) exponent pairs. Monomial x^i y^j lowers to shiftPow l i (x) shiftPow m j (an lm x lm matrix); the sum is GF(2) XOR over all terms.

defbivariateBicycle

def bivariateBicycle (l m : Nat) (a b : List (Nat × Nat)) : CSSCode

A bivariate-bicycle (BB) code, a.k.a. LP(a, b) (Bravyi et al. 2024). A = biCirculant l m a, B = biCirculant l m b hx = [ A | B ], hz = [ B^T | A^T ], n = 2*l*m CSS condition holds since A and B are circulants over the same commutative ring, so A*B = B*A, hence A*B + B*A = 0 over GF(2), which is hx*hz^T.

example(example)

example : (bivariateBicycle 3 3 [(0, 0), (1, 0)] [(0, 0), (0, 1)]).n = 18

example(example)

example : (bivariateBicycle 3 3 [(0, 0), (1, 0)] [(0, 0), (0, 1)]).well_shaped = true

example(example)

example : (bivariateBicycle 3 3 [(0, 0), (1, 0)] [(0, 0), (0, 1)]).css_condition = true

example(example)

example : (bivariateBicycle 6 6 [(3, 0), (0, 1), (0, 2)] [(0, 3), (1, 0), (2, 0)]).n = 72

example(example)

example : (bivariateBicycle 6 6 [(3, 0), (0, 1), (0, 2)] [(0, 3), (1, 0), (2, 0)]).well_shaped = true

example(example)

example : (bivariateBicycle 6 6 [(3, 0), (0, 1), (0, 2)] [(0, 3), (1, 0), (2, 0)]).css_condition = true

abbrevCirc

abbrev Circ

A ring element of F2[x]/(x^l+1), represented by its exponent support.

defcirculant

def circulant (l : Nat) (p : Circ) : BoolMat

The l x l circulant matrix of a Circ: entry (i, j) is 1 iff (j - i) mod l is a member of the support.

defcircDagger

def circDagger (l : Nat) (p : Circ) : Circ

The conjugate p(x) to p(x_inv) on Circ: e to (l - e) mod l.

example(example)

example : circulant 3 [1] = shiftMat 3

example(example)

example : circDagger 3 [1] = [2]

example(example)

example : circulant 3 (circDagger 3 [1]) = transpose (circulant 3 [1]) 3

KEY FACT: the GF(2) transpose of a lifted circulant equals the lift of the ring conjugate. Verified on the smoke instances used below by `decide`; this is what makes the lifted-product CSS condition cancel over GF(2).

example(example)

example : circulant 4 (circDagger 4 [1, 2]) = transpose (circulant 4 [1, 2]) 4

defliftMat

def liftMat (ℓ : Nat) (A : List (List Circ)) : BoolMat

A polynomial matrix `A` (`r×n` over `R`) lifted to a GF(2) `BoolMat` (`r·ℓ × n·ℓ`): block `(a,c)` is `circulant ℓ (A[a][c])`. Each ring entry becomes an `ℓ×ℓ` circulant; row block `a` contributes `ℓ` GF(2) rows, each the column-concatenation of the corresponding circulant rows.

defpIdent

def pIdent (n : Nat) : List (List Circ)

The `n×n` identity over `R`: `1_R = [0]` (the constant `1 = x⁰`) on the diagonal, `0_R = []` off-diagonal.

defpDagger

def pDagger (ℓ : Nat) (A : List (List Circ)) : List (List Circ)

Conjugate transpose `A†` of a polynomial matrix: transpose the index grid and conjugate (`circDagger`) every ring entry.

defcircMul

def circMul (ℓ : Nat) (p q : Circ) : Circ

Multiplication in `R = F2[x]/(x^ℓ+1)`: convolution of exponent supports, exponents reduced mod `ℓ`, keeping terms of odd multiplicity (mod-2 sum).

defpKron

def pKron (ℓ : Nat) (A B : List (List Circ)) : List (List Circ)

Kronecker (tensor) product of two polynomial matrices over `R`: block `(i,k),(j,l)` is the ring product `A[i][j] · B[k][l]`.

defpHcat

def pHcat (L R : List (List Circ)) : List (List Circ)

Horizontal block concatenation of two same-row-count polynomial matrices.

defliftedProduct

def liftedProduct (ℓ : Nat) (A : List (List Circ)) (rA nA : Nat) : CSSCode

The qianxu lifted-product code `LP(A, A†)` for `A : rA × nA` over `R = F2[x]/(x^ℓ+1)` (each entry a `Circ`). The hypergraph product is taken over the ring with second factor `A†`, then lifted to GF(2): n = (rA² + nA²)·ℓ hx = lift [ A ⊗ I_{nA} | I_{rA} ⊗ A† ] hz = lift [ I_{nA} ⊗ A | A† ⊗ I_{rA} ] `css_condition` holds because `transpose (lift A†) = lift A`, so `hx · hzᵀ = lift(A ⊗ A† + A ⊗ A†) = 0` over GF(2) (oracle: `lpTiny`).

deflpTiny

def lpTiny : CSSCode

example(example)

example : lpTiny.n = (1 * 1 + 2 * 2) * 3

example(example)

example : lpTiny.well_shaped = true

example(example)

example : lpTiny.css_condition = true

example(example)

example : StabilizerState.valid (lpTiny.toStabilizers) lpTiny.n = true

Tiny-LP pipeline capstone: the lifted-product code's syndrome-measurement circuit implements it (the lowered stabilizer group is valid), because the construction is CSS.

theoremsurfaceHGP3_circuit_implements

theorem surfaceHGP3_circuit_implements :
    StabilizerState.valid ((surfaceHGP 3).toStabilizers) (surfaceHGP 3).n = true

The constructed distance-3 surface code syndrome circuit implements it. Instantiating CSSCode.syndrome_circuit_implements_code on the HGP-built surface code: because the construction is CSS (css_condition = true), the measured stabilizer group toStabilizers is a valid (pairwise-commuting) stabilizer code. Closes the ALGEBRAIC -> check-matrix -> circuit-implements-code chain end-to-end.

theoremtinyBB_circuit_implements

theorem tinyBB_circuit_implements :
    StabilizerState.valid
      ((bivariateBicycle 3 3 [(0, 0), (1, 0)] [(0, 0), (0, 1)]).toStabilizers)
      (bivariateBicycle 3 3 [(0, 0), (1, 0)] [(0, 0), (0, 1)]).n = true

The same end-to-end chain for the tiny bivariate-bicycle code: its syndrome circuit implements the constructed [[18, *, *]] BB code.

FormalRV.QEC.GF2Linear

FormalRV/QEC/GF2Linear.lean

FormalRV.QEC.GF2Linear — GF(2) linear-algebra primitives over the `BoolVec`/`BoolMat` carrier of `LDPCMatrix`. This is the missing primitive flagged by the code-framework design (`notes/topic-qec-code-framework.md`): everything downstream — the CSS commutation condition `H_X H_Z^T = 0`, the logical-qubit count `k = n − rank H_X − rank H_Z`, kernel/logical extraction — needs GF(2) linear algebra absent from `LDPCMatrix.lean`. This file provides the inner-product / orthogonality layer (the part the CSS condition needs); rank/echelon/nullspace are a later module. Extends the SAME namespace `FormalRV.Framework.LDPC` as `LDPCMatrix`. No Mathlib. Pure Bool / Nat / List + `decide`.

defdotBit

def dotBit (a b : BoolVec) : Bool

GF(2) inner product bit of two vectors: `1` (`true`) iff the number of positions where BOTH are `1` is odd. This is `Σ_i a_i·b_i mod 2`. `dotBit a b = false` means `a` and `b` are orthogonal over GF(2).

deftranspose

def transpose (mat : BoolMat) (ncols : Nat) : BoolMat

GF(2) transpose of a matrix with `ncols` columns: row `j` of the result is column `j` of `mat`.

defmat_mul_transpose

def mat_mul_transpose (a b : BoolMat) : BoolMat

The GF(2) product `A · Bᵀ`, as a `BoolMat`: entry `(i, j)` is the inner product of row `i` of `A` with row `j` of `B`.

deforthogonal

def orthogonal (a b : BoolMat) : Bool

`orthogonal a b = true` iff every row of `a` is GF(2)-orthogonal to every row of `b`, i.e. `A · Bᵀ = 0`. This is the CSS commutation test `H_X · H_Z^T = 0`.

theoremorthogonal_iff

theorem orthogonal_iff (a b : BoolMat) :
    orthogonal a b = true ↔
      ∀ ra ∈ a, ∀ rb ∈ b, dotBit ra rb = false

`orthogonal a b = true` iff every (row-of-`a`, row-of-`b`) pair is GF(2)-orthogonal — the per-pair unfolding used downstream.

example(example)

example : dotBit [true, false, true] [true, true, true] = false

example(example)

example : dotBit [true, true, false] [true, true, true] = false

example(example)

example : dotBit [true, false, false] [true, true, true] = true

example(example)

example :
    orthogonal
      [ [false, false, false, true,  true,  true,  true ]
      , [false, true,  true,  false, false, true,  true ]
      , [true,  false, true,  false, true,  false, true ] ]
      [ [false, false, false, true,  true,  true,  true ]
      , [false, true,  true,  false, false, true,  true ]
      , [true,  false, true,  false, true,  false, true ] ] = true

FormalRV.QEC.GF2Linearity

FormalRV/QEC/GF2Linearity.lean

FormalRV.QEC.GF2Linearity — LINEARITY of the GF(2) inner product, the cornerstone of a PARAMETRIC nullspace-correctness proof for the logical-operator finder. GOAL (task a, fully-clean / no-`native_decide` route demanded by the strengthened verifier `ShorLPContract`): prove that every operator the finder computes lies in the relevant kernel — `z_in_ker_hx` / `x_in_ker_hz` for lp16/lp20 — PARAMETRICALLY, with no `decide`/`native_decide` at 2610/4350 columns. The whole development reduces to GF(2) linear algebra over `BoolVec`, whose ATOM is the linearity of `dotBit`: `dotBit (a ⊕ c) b = dotBit a b ⊕ dotBit c b`. Every later step (a vector orthogonal to a set of rows is orthogonal to their GF(2) span; `reduceVec` differs from its input by a span element; the kernel-basis vectors are orthogonal to the echelon rows; rows are preserved in the rowspace) is an application of this atom plus bookkeeping. This file proves the atom, axiom-free, by a parity induction. ## Path to `kernelBasis_in_ker` (the remaining chain, each step built on `dotBit_vec_xor`) 1. `dotBit_vec_xor` — linearity (THIS FILE, proven). 2. `dotBit_row_combination` — `v ⊥ every row of M → v ⊥ (any GF(2) combination of M)`. 3. `reduceVec_sub_in_span` — `reduceVec P v = v ⊕ (combination of P)`. 4. `rowReduce_rows_in_span` — every original row ∈ rowspace of the echelon pivots. 5. `kernelBasis_orthogonal` — each `kernelBasis M n` vector ⊥ every echelon row. 6. `kernelBasis_in_ker` — (4)+(5)+(2): each `kernelBasis M n` vector ⊥ every row of M. 7. `logicalZ_in_ker_hx` — instantiate at `M = c.hx` ⇒ `z_in_ker_hx c.logical`. Steps 2–7 are the documented continuation; they introduce NO `decide`-at-scale. No Mathlib heavy machinery, no `sorry`, no `axiom`.

theoremvec_xor_cons

theorem vec_xor_cons (x y : Bool) (xs ys : BoolVec) :
    vec_xor (x :: xs) (y :: ys) = (x != y) :: vec_xor xs ys

`vec_xor` on cons cells: the head is the per-bit XOR `(x != y)`, the tail recurses.

theoremcount_xor_parity

theorem count_xor_parity (a c b : BoolVec) (hac : a.length = c.length) (hab : a.length = b.length) :
    ((vec_xor a c).zip b).countP (fun p => p.1 && p.2) % 2
      = (((a.zip b).countP (fun p => p.1 && p.2)) + ((c.zip b).countP (fun p => p.1 && p.2))) % 2

The GF(2) overlap count of `(a ⊕ c)` with `b` is, MOD 2, the sum of the overlap counts of `a` with `b` and of `c` with `b`. (Per position `(x≠y)∧z ≡ (x∧z)+(y∧z) (mod 2)`, lifted by induction.) Equal-length lists.

theoremparity_add

theorem parity_add (m n : Nat) :
    decide ((m + n) % 2 = 1) = xor (decide (m % 2 = 1)) (decide (n % 2 = 1))

`(m+n)` is odd iff exactly one of `m`, `n` is — i.e. parity is XOR-additive.

theoremdotBit_vec_xor

theorem dotBit_vec_xor (a c b : BoolVec) (hac : a.length = c.length) (hab : a.length = b.length) :
    dotBit (vec_xor a c) b = xor (dotBit a b) (dotBit c b)

*`dotBit` is GF(2)-LINEAR in its left argument:** `dotBit (a ⊕ c) b = dotBit a b ⊕ dotBit c b` (for equal-length vectors). This is the atom every step of the parametric nullspace-correctness proof reduces to.

FormalRV.QEC.GF2Rank

FormalRV/QEC/GF2Rank.lean

FormalRV.QEC.GF2Rank — GF(2) Gaussian elimination over `BoolMat`. This is the rank / rowspace-membership layer flagged as the one RESIDUE in `Logical.lean`: deciding whether a declared logical operator is a product of stabilizers* (i.e. lies INSIDE the stabilizer group) needs a GF(2) rank computation absent from `GF2Linear.lean` (which provides only the inner-product / orthogonality layer). We build a textbook GF(2) row reduction: fold the rows of a matrix, reducing each against the pivots collected so far, and keeping it as a new pivot iff it stays nonzero. `rank` = number of pivots. `inRowspace mat v` = `v` reduces to all-zero against the echelon pivots. The MATHEMATICAL key fact this layer exposes: every element of the GF(2) rowspace of the Steane Hamming matrix has EVEN weight, so the weight-7 all-ones logical operator is OUTSIDE the stabilizer rowspace — precisely the property that distinguishes a genuine logical (in N(S)\S) from a stabilizer. Correctness here is `decide`-verified at the instance level (the smoke tests below are the oracle), not proven parametrically. That is sufficient for the per-instance audit: the smokes pin the algorithm to the mathematically-true answers. Extends the SAME namespace `FormalRV.Framework.LDPC` as `GF2Linear`. No Mathlib. Pure Bool / Nat / List + `decide`.

defleadIdx

def leadIdx (v : BoolVec) : Option Nat

The first column index where `v` is `true` (its "leading 1"), or `none` if `v` is all-zero.

defreduceVec

def reduceVec (pivots : BoolMat) (v : BoolVec) : BoolVec

Reduce `v` against a list of echelon `pivots`: for each pivot `p` whose leading column `j` is also set in `v`, xor `p` into `v`, clearing that column. When `pivots` is in row-echelon form (distinct leading columns, each pivot's leading bit clear in every later pivot), the result is `v`'s canonical remainder modulo the rowspace of `pivots`.

defrowReduce

def rowReduce (mat : BoolMat) : BoolMat

GF(2) Gaussian elimination. Folds over `mat`'s rows, building a pivot list; each row is first reduced against the current pivots, and kept as a new pivot iff the remainder is nonzero. The returned `BoolMat` is the list of nonzero pivot rows (one per independent direction).

defrank

def rank (mat : BoolMat) : Nat

GF(2) rank = number of pivots in the echelon form.

definRowspace

def inRowspace (mat : BoolMat) (v : BoolVec) : Bool

`v` is in the GF(2) rowspace of `mat` iff it reduces to all-zero against `mat`'s echelon pivots.

defsteaneH

def steaneH : BoolMat

The Steane `[7,4]` Hamming parity-check matrix (`hx = hz` for Steane).

example(example)

example : rank steaneH = 3

example(example)

example : inRowspace steaneH [false, false, false, true, true, true, true] = true

example(example)

example :
    inRowspace steaneH
      (vec_xor [false, false, false, true, true, true, true]
               [false, true,  true,  false, false, true, true]) = true

example(example)

example : inRowspace steaneH [true, true, true, true, true, true, true] = false

example(example)

example : rank (steaneH ++ [[true, true, true, true, true, true, true]]) = 4

FormalRV.QEC.GateSyndromeWorkedExample

FormalRV/QEC/GateSyndromeWorkedExample.lean

FormalRV.QEC.GateSyndrome — GATE-LEVEL WORKED INSTANCE. The physical syndrome-extraction circuit of the [[4,2,2]] code — explicit ancilla+CNOT+measure gates — measures exactly the code's stabilizers {X₀X₁X₂X₃, Z₀Z₁Z₂Z₃} (each check via CliffordConj's `measGadgetConj`/`xMeasGadgetConj`, the set valid by `CSSCode.syndrome_circuit_implements_code`), and its resource count (physical qubits 6, CNOTs 8, cycles 2) follows from the per-check costs. This is the bottom rung of the physical→PPM→logical→Shor stack, made concrete and resource-counted; the full-Hilbert faithfulness of the Heisenberg picture is the cited Gottesman–Knill bridge. No Mathlib. Pure Bool / Nat / List + decide.

example(example)

example : measGadgetConj [0, 1, 2, 3] 4
      ⟨Phase.plus, [Pauli.I, Pauli.I, Pauli.I, Pauli.I, Pauli.Z]⟩
    = ⟨Phase.plus, [Pauli.Z, Pauli.Z, Pauli.Z, Pauli.Z, Pauli.Z]⟩

The Z-check `ZZZZ` is measured by CNOT(0→4),CNOT(1→4),CNOT(2→4), CNOT(3→4); measure Z₄. Heisenberg picture: Z₄ ↦ Z₀Z₁Z₂Z₃Z₄.

example(example)

example : xMeasGadgetConj [0, 1, 2, 3] 4
      ⟨Phase.plus, [Pauli.I, Pauli.I, Pauli.I, Pauli.I, Pauli.X]⟩
    = ⟨Phase.plus, [Pauli.X, Pauli.X, Pauli.X, Pauli.X, Pauli.X]⟩

The X-check `XXXX` is measured by CNOT(4→0),…,CNOT(4→3); measure X₄. Heisenberg picture: X₄ ↦ X₀X₁X₂X₃X₄.

example(example)

example : code422.toStabilizers
    = [⟨Phase.plus, [Pauli.X, Pauli.X, Pauli.X, Pauli.X]⟩,
       ⟨Phase.plus, [Pauli.Z, Pauli.Z, Pauli.Z, Pauli.Z]⟩]

`code422.toStabilizers = [xStab [T,T,T,T], zStab [T,T,T,T]] = [X₀X₁X₂X₃, Z₀Z₁Z₂Z₃]`.

example(example)

example : StabilizerState.valid code422.toStabilizers code422.n = true

The lowered stabilizer group of `code422` is a valid (pairwise- commuting, well-sized) stabilizer code — the syndrome circuit implements it, since `code422` is CSS.

theoremcode422_syndrome_circuit_valid

theorem code422_syndrome_circuit_valid :
    StabilizerState.valid code422.toStabilizers code422.n = true

Named witness for the validity claim, for the axiom audit.

structurePhysResources

structure PhysResources

Physical-layer resource tally of a gate-level syndrome circuit: data qubits, syndrome ancillae, CNOTs, and measurement cycles.

defphysQubits

def physQubits (r : PhysResources) : Nat

Total physical qubits = data + ancilla.

defrowWeight

def rowWeight (row : BoolVec) : Nat

The weight of a check row = number of `true` (supported) entries.

defsyndromeCost

def syndromeCost (c : CSSCode) : PhysResources

Resource cost of the gate-level syndrome circuit of a CSS code: one ancilla per check, one CNOT per stabilizer-support entry (Σ row weights), one measurement cycle per check.

example(example)

example : syndromeCost code422
    = { data_qubits

code422: 4 data, 2 ancilla (1 per check), 8 CNOTs (4+4 = Σ weights), 2 measurement cycles.

example(example)

example : physQubits (syndromeCost code422) = 6

The [[4,2,2]] syndrome circuit uses 6 physical qubits.

FormalRV.QEC.Instances

FormalRV/QEC/Instances.lean

FormalRV.QEC.Instances — the qianxu code corpus as concrete `CSSCode` values, with `decide`/`native_decide`-checked structural smokes. Each entry is a genuine GF(2) check-matrix pair built through the `FrontendAlgebraic` constructors (no axiomatized parameters): the small codes verify the CSS commutation condition `H_X · H_Z^T = 0` outright; the large lifted-product codes are verified CSS by the tiny-LP oracle plus the ring algebra (`liftedProduct`), with the full-matrix `css_condition` left as an HONEST RESIDUE at that scale. SCOPE NOTE: code DISTANCE is OUT OF SCOPE — these are constructions plus CSS commutation, not distance proofs. Codes: `code422` — the `[[4,2,2]]` code (with a verified logical basis) `surface3`, `surface5` — unrotated surface codes (HGP) `bb18` — bivariate-bicycle `[[248, 10, 18]]` (qianxu) `lp16`, `lp20`, `lp24`, `lpproc` — qianxu lifted-product seeds No Mathlib. Pure Bool / Nat / List + decide / native_decide.

defcode422

def code422 : CSSCode

The `[[4,2,2]]` detection code: a single weight-4 `X`-stabilizer `XXXX` and a single weight-4 `Z`-stabilizer `ZZZZ` on 4 qubits. Encodes 2 logical qubits, detects 1 error.

example(example)

example : code422.well_shaped = true

All rows have length 4.

example(example)

example : code422.css_condition = true

CSS commutation: `XXXX · ZZZZ` overlap = 4 (even), so they commute.

defcode422Logical

def code422Logical : LogicalBasis code422 2

A logical basis for `[[4,2,2]]`, `k = 2`. Standard supports: X̄₀ = XXII, Z̄₀ = XIXI (read as Z), X̄₁ = XIXI, Z̄₁ = XXII. Each commutes with both stabilizers (weight-2 overlap with the weight-4 checks is even) and realises the δ_ij pairing: overlap(X̄ᵢ, Z̄ⱼ) is odd iff i = j.

example(example)

example : code422Logical.valid = true

The declared `[[4,2,2]]` logical basis is valid (commutes with all stabilizers and realises the δ_ij pairing).

example(example)

example : StabilizerState.valid (code422.toStabilizers) 4 = true

Pipeline capstone: the `[[4,2,2]]` syndrome-measurement circuit implements it (the lowered stabilizer group is valid), since it is CSS.

defsurface3

def surface3 : CSSCode

The unrotated distance-3 surface code, `[[13, 1, 3]]`.

defsurface5

def surface5 : CSSCode

The unrotated distance-5 surface code, `[[41, 1, 5]]`.

example(example)

example : surface3.n = 13

example(example)

example : surface3.well_shaped = true

example(example)

example : surface3.css_condition = true

example(example)

example : surface5.n = 41

example(example)

example : surface5.well_shaped = true

example(example)

example : surface5.css_condition = true

defbb18

def bb18 : CSSCode

The bivariate-bicycle `[[248, 10, 18]]` qLDPC code from qianxu.

example(example)

example : bb18.n = 248

example(example)

example : bb18.css_condition = true

CSS commutation for the BB `[[248, 10, 18]]` code. `native_decide` (the `248`-column orthogonality check is too large for kernel `decide`).

defA_lp16

def A_lp16 : List (List Circ)

LP seed for the `[[2610, 744, ≤16]]` code (qianxu App. A), `3×7` over ℓ=45.

defA_lp20

def A_lp20 : List (List Circ)

LP seed for the `ℓ=75` lifted-product code (qianxu App. A), `3×7`.

defA_lp24

def A_lp24 : List (List Circ)

LP seed for the `ℓ=91` lifted-product code (qianxu App. A), `3×7`.

deflp16

def lp16 : CSSCode

The lifted-product code on `A_lp16` over `R = F2[x]/(x^45+1)`.

deflp20

def lp20 : CSSCode

The lifted-product code on `A_lp20` over `R = F2[x]/(x^75+1)`.

deflp24

def lp24 : CSSCode

The lifted-product code on `A_lp24` over `R = F2[x]/(x^91+1)`.

example(example)

example : lp16.n = (3 * 3 + 7 * 7) * 45

example(example)

example : lp20.n = (3 * 3 + 7 * 7) * 75

example(example)

example : lp24.n = (3 * 3 + 7 * 7) * 91

defA_lpproc

def A_lpproc : List (List Circ)

LP seed for the `lpproc` processing-block code (qianxu), `3×5` over ℓ=33. First row and column are the constant `1 = x⁰ = [0]`.

deflpproc

def lpproc : CSSCode

The lifted-product `lpproc` code over `R = F2[x]/(x^33+1)`.

example(example)

example : lpproc.n = (3 * 3 + 5 * 5) * 33

FormalRV.QEC.LDPCMatrix

FormalRV/QEC/LDPCMatrix.lean

FormalRV.Framework.LDPCMatrix — GF(2) matrix primitives for LDPC lattice surgery. We need a handful of GF(2) (binary-field) matrix operations to verify the structural constraints of qLDPC surgery gadgets per qianxu Appendix C: vector XOR (= addition in GF(2)) linear combination of matrix rows by a Bool selection vector horizontal concatenation of two row blocks vertical concatenation dimension and parity-check-matrix consistency We represent a GF(2) matrix as `List (List Bool)` with no Mathlib dependency. All ops are decidable on concrete matrices. ## Why this matters for surgery verification A surgery gadget's merged-code parity matrix `H̃_X` is built by block concatenation of the data code's `H_X`, the ancilla's `H_X'`, and the connection matrix `f_X'`. The framework verifies that the target logical `P̄` lies in the row span of `H̃_X` — a one-line equality `row_combination span_witness merged_hx = target_pauli` over GF(2). This is the structural correctness condition (the "kernel of H_X'^T" condition in the paper, restated as a row-span membership of the merged matrix).

abbrevBoolVec

abbrev BoolVec

Row vector as a `List Bool`. `true` ↦ 1, `false` ↦ 0.

abbrevBoolMat

abbrev BoolMat

Matrix as a `List` of rows. Each row is a `BoolVec` of the same length (matrix-shape consistency is checked separately by `matrix_well_shaped`).

defvec_xor

def vec_xor : BoolVec → BoolVec → BoolVec
  | [],          _           => []
  | _,           []          => []
  | h1 :: t1,    h2 :: t2    => (h1 != h2) :: vec_xor t1 t2

Component-wise XOR (= GF(2) sum) of two equal-length vectors. On unequal lengths, truncates to the shorter — but in our use the caller is responsible for matching lengths.

defzero_vec

def zero_vec (n : Nat) : BoolVec

The all-zero vector of length `n`.

defrow_combination

def row_combination (sel : BoolVec) (mat : BoolMat) : BoolVec

Linear combination of the rows of `mat` selected by the Bool vector `sel`. Row `i` is XOR'ed into the accumulator iff `sel[i] = true`. Returns the zero vector if `sel` is shorter than `mat` (truncates). This is the GF(2) version of `selᵀ · mat` (vector-matrix multiplication) producing a row vector.

defhcat

def hcat (left right : BoolMat) : BoolMat

Horizontal concatenation of two same-row-count matrices, producing a wider matrix.

defvcat

def vcat (top bot : BoolMat) : BoolMat

Vertical concatenation of two same-column-count matrices, producing a taller matrix.

defmatrix_has_n_cols

def matrix_has_n_cols (mat : BoolMat) (n : Nat) : Bool

Every row of `mat` has length exactly `n`.

defmatrix_well_shaped

def matrix_well_shaped (mat : BoolMat) : Bool

The matrix is well-shaped iff every row has the same length (which we read off the first row).

defmax_column_weight

def max_column_weight (mat : BoolMat) (n_cols : Nat) : Nat

Maximum number of `true` entries in any column of `mat`. Used to check the qLDPC degree bound on the merged code.

defmax_row_weight

def max_row_weight (mat : BoolMat) : Nat

Maximum number of `true` entries in any row of `mat`.

defis_qldpc

def is_qldpc (mat : BoolMat) (n_cols Δ : Nat) : Bool

The matrix is qLDPC (parameter `Δ`) iff every row and every column has weight ≤ `Δ`.

example(example)

example : vec_xor [true, false, true] [false, true, true] = [true, true, false]

example(example)

example :
    row_combination [true, false, true]
      [ [true,  false, false]
      , [false, true,  false]
      , [false, false, true] ]
      = [true, false, true]

example(example)

example :
    row_combination [true, true]
      [ [true,  false, false]
      , [false, true,  false] ]
      = [true, true, false]

example(example)

example :
    hcat [[true, false]] [[true]] = [[true, false, true]]

example(example)

example :
    vcat [[true, false]] [[false, true]]
      = [[true, false], [false, true]]

example(example)

example :
    matrix_has_n_cols [[true, false], [false, true]] 2 = true

example(example)

example :
    matrix_has_n_cols [[true, false], [false]] 2 = false

example(example)

example :
    max_row_weight [[true, false, true], [false, false, false]] = 2

example(example)

example :
    max_column_weight [[true, false, true], [true, false, true]] 3 = 2

example(example)

example :
    is_qldpc [[true, false, true], [true, true, false]] 3 2 = true

example(example)

example :
    is_qldpc [[true, true, true]] 3 2 = false

FormalRV.QEC.LPCssCondition

FormalRV/QEC/LPCssCondition.lean

FormalRV.QEC.LPCssCondition — toward a PARAMETRIC (native-free) proof that the lifted- product LP codes (lp16/lp20) satisfy the CSS condition `H_X H_Z^T = 0`. Track (b) of the validity programme: the strengthened verifier's no-native acceptance forbids `decide`/`native_decide` on the 2610/4350-column matrices, so `code.valid` (= well_shaped ∧ css_condition) must be proven algebraically. The CSS cancellation of the lifted product rests on ONE structural fact — the GF(2) transpose of a lifted circulant block equals the lift of the ring conjugate: circulant ℓ (circDagger ℓ p) = transpose (circulant ℓ p) ℓ currently only `decide`-verified on instances. This file proves it GENERICALLY (for reduced exponent supports `p`, which the real seeds satisfy), via the modular-negation bijection `e ↦ (ℓ−e) mod ℓ`. Remaining toward `liftedProduct_css_condition` (documented continuation): lift the block identity through `liftMat` (`transpose (lift A†) = lift A`), then the ring-level cancellation `A⊗A† + A⊗A† = 0` via `circMul` commutativity. Needs `Mathlib.Tactic.SplitIfs`. No `sorry`, no `axiom`, no `native_decide`.

theoremsubMod

theorem subMod (a b ℓ : Nat) (hb : b < ℓ) (ha : a < ℓ) :
    (a + ℓ - b) % ℓ = if b ≤ a then a - b else a + ℓ - b

`(a + ℓ − b) mod ℓ` for `a, b < ℓ`: `a − b` if `b ≤ a`, else `a + ℓ − b`.

theoremnegMod

theorem negMod (e ℓ : Nat) (he : e < ℓ) : (ℓ - e) % ℓ = if e = 0 then 0 else ℓ - e

`(ℓ − e) mod ℓ` for `e < ℓ`: `0` if `e = 0`, else `ℓ − e` (modular negation).

theoremdagger_contains

theorem dagger_contains (ℓ : Nat) (p : Circ) (hp : ∀ e ∈ p, e < ℓ)
    (i j : Nat) (hi : i < ℓ) (hj : j < ℓ) :
    (circDagger ℓ p).contains ((j + ℓ - i % ℓ) % ℓ) = p.contains ((i + ℓ - j % ℓ) % ℓ)

*Entrywise core of the conjugate-transpose identity.** For reduced `p` (entries `< ℓ`) and `i, j < ℓ`, the conjugated support contains the `(i,j)`-circulant offset iff the original support contains the transposed `(j,i)` offset — the modular-negation bijection `e ↦ (ℓ−e) mod ℓ`.

theoremmap_range_getD

private theorem map_range_getD {α : Type _} (n i : Nat) (f : Nat → α) (d : α) (hi : i < n) :
    ((List.range n).map f).getD i d = f i

`getD` of a mapped range at an in-bounds index.

theoremcirculant_circDagger_eq_transpose

theorem circulant_circDagger_eq_transpose (ℓ : Nat) (p : Circ) (hp : ∀ e ∈ p, e < ℓ) :
    circulant ℓ (circDagger ℓ p) = transpose (circulant ℓ p) ℓ

*The GF(2) transpose of a lifted circulant equals the lift of the ring conjugate** (`circulant ℓ (circDagger ℓ p) = transpose (circulant ℓ p) ℓ`), GENERICALLY for reduced `p`. This is the cancellation fact behind the lifted-product CSS condition; previously only `decide`-verified on instances.

theoremsum_map_add

private theorem sum_map_add (l : List Nat) (A B : Nat → Nat) :
    (l.map (fun x => A x + B x)).sum = (l.map A).sum + (l.map B).sum

Sum of a pointwise-added map splits.

theoremcountP_eq_sum_ite

private theorem countP_eq_sum_ite (q : List Nat) (P : Nat → Bool) :
    q.countP P = (q.map (fun j => if P j then 1 else 0)).sum

`countP` as a sum of `0/1` indicators.

theoremsum_countP_swap

private theorem sum_countP_swap (p q : List Nat) (g : Nat → Nat → Bool) :
    (p.map (fun i => q.countP (fun j => g i j))).sum
      = (q.map (fun j => p.countP (fun i => g i j))).sum

*Fubini for `countP` over a product**: the double count is symmetric in the two lists.

theoremcircMul_comm

theorem circMul_comm (ℓ : Nat) (p q : Circ) : circMul ℓ p q = circMul ℓ q p

*The ring `R = F₂[x]/(xˡ+1)` is COMMUTATIVE**: `circMul ℓ p q = circMul ℓ q p`. The multiset of pairwise-sum exponents is symmetric (`i + j = j + i`), so each residue's odd-multiplicity test agrees — by `filter_congr` + the Fubini swap. This is the commutativity behind the lifted-product CSS cancellation `A⊗A† + A⊗A† = 0`.

theoremsum_replicate

private theorem sum_replicate (n a : Nat) : (List.replicate n a).sum = n * a

Sum of a constant-`a` replicate.

theoremcirculant_row_length

theorem circulant_row_length (ℓ : Nat) (e : Circ) (r : Nat) (hr : r < ℓ) :
    ((circulant ℓ e).getD r []).length = ℓ

A circulant's `r`-th row (for `r < ℓ`) has length `ℓ` (the matrix is `ℓ×ℓ`).

theoremliftRow_length

theorem liftRow_length (ℓ : Nat) (pr : List Circ) (r : Nat) (hr : r < ℓ) :
    ((pr.map (fun e => circulant ℓ e)).flatMap (fun blk => blk.getD r [])).length
      = pr.length * ℓ

One lifted row of a polynomial row `pr` (the `r`-th rows of its circulant blocks, concatenated) has length `(#blocks)·ℓ = pr.length·ℓ`.

theoremliftMat_row_length

theorem liftMat_row_length (ℓ : Nat) (A : List (List Circ)) (C : Nat)
    (hrect : ∀ pr ∈ A, pr.length = C) :
    ∀ row ∈ liftMat ℓ A, row.length = C * ℓ

*Every row of `liftMat ℓ A` has length `C·ℓ`** when `A` is rectangular with `C` columns — the shape invariant feeding `well_shaped` for the lifted product, and the block decomposition needed for the transpose homomorphism.

theoremgetElem?_flatMap_uniform

theorem getElem?_flatMap_uniform {α β : Type} (f : α → List β) (ℓ : Nat) :
    ∀ (l : List α), (∀ a ∈ l, (f a).length = ℓ) →
      ∀ (b s : Nat) (a : α), s < ℓ → l[b]? = some a →
        (l.flatMap f)[b * ℓ + s]? = (f a)[s]?

*Uniform-block `getElem?`**: for `f` producing length-`ℓ` lists and `s < ℓ`, the `(b·ℓ+s)`-th element of `l.flatMap f` is the `s`-th element of `f`(the `b`-th block). By induction over `l`, using the append `getElem?` lemmas.

theoremliftMat_entry

theorem liftMat_entry (ℓ : Nat) (A : List (List Circ)) (C : Nat)
    (hrect : ∀ pr ∈ A, pr.length = C)
    (a r b s : Nat) (ha : a < A.length) (hr : r < ℓ) (hb : b < C) (hs : s < ℓ) :
    ((liftMat ℓ A)[a * ℓ + r]?.getD []).getD (b * ℓ + s) false
      = ((circulant ℓ ((A[a]?.getD []).getD b [])).getD r []).getD s false

*The `(a·ℓ+r, b·ℓ+s)` entry of `liftMat ℓ A` is `circulant(A[a][b])[r][s]`** — the block `(a,b)` is the `ℓ×ℓ` circulant of the ring entry `A[a][b]`, read at `(r,s)`. Proved by decomposing both flatMap levels with `getElem?_flatMap_uniform`. This is the bridge that turns the transpose homomorphism into a per-entry application of `circulant_circDagger_eq_transpose`.

theorempKron_row_length

theorem pKron_row_length (ℓ : Nat) (A B : List (List Circ)) (cA cB : Nat)
    (hA : ∀ arow ∈ A, arow.length = cA) (hB : ∀ brow ∈ B, brow.length = cB) :
    ∀ row ∈ pKron ℓ A B, row.length = cA * cB

A `pKron` row has length `(#cols A)·(#cols B)` for rectangular `A`, `B`.

theorempHcat_row_length

theorem pHcat_row_length (L R : List (List Circ)) (cL cR : Nat)
    (hL : ∀ row ∈ L, row.length = cL) (hR : ∀ row ∈ R, row.length = cR) :
    ∀ row ∈ pHcat L R, row.length = cL + cR

A `pHcat` row has length `cL + cR` for rectangular sides.

theorempIdent_row_length

theorem pIdent_row_length (n : Nat) : ∀ row ∈ pIdent n, row.length = n

Each `pIdent n` row has length `n`.

theorempDagger_row_length

theorem pDagger_row_length (ℓ : Nat) (A : List (List Circ)) :
    ∀ row ∈ pDagger ℓ A, row.length = A.length

Each `pDagger ℓ A` row has length `A.length` (the conjugate transpose flips dimensions).

theoremmatrix_has_n_cols_of

theorem matrix_has_n_cols_of (M : BoolMat) (n : Nat) (h : ∀ row ∈ M, row.length = n) :
    matrix_has_n_cols M n = true

A matrix whose every row has length `n` passes `matrix_has_n_cols`.

theoremliftedProduct_well_shaped

theorem liftedProduct_well_shaped (ℓ : Nat) (A : List (List Circ)) (rA nA : Nat)
    (hA_rows : A.length = rA) (hA_cols : ∀ row ∈ A, row.length = nA) :
    (liftedProduct ℓ A rA nA).well_shaped = true

*`well_shaped` for the lifted product `LP(A, A†)`, PARAMETRICALLY** (native-free). Every `H_X`/`H_Z` row has length `n = (rA² + nA²)·ℓ`: both check matrices are `liftMat` of a `pHcat` of two `pKron`s with column counts `nA·nA` and `rA·rA`, and `liftMat_row_length` multiplies by `ℓ`. This is the first half of `code.valid` for lp16/lp20, with NO `decide`/`native_decide` at the 2610/4350-column scale.

theoremcirculant_getD_row

theorem circulant_getD_row (ℓ : Nat) (p : Circ) (r : Nat) (hr : r < ℓ) :
    (circulant ℓ p).getD r [] = (List.range ℓ).map (fun s => p.contains ((s + ℓ - r % ℓ) % ℓ))

The explicit `r`-th row of `circulant ℓ p` (`r < ℓ`): `s ↦ p.contains((s+ℓ−r) mod ℓ)`.

theoremcirculant_rows_zip

theorem circulant_rows_zip (ℓ : Nat) (p q : Circ) (r r' : Nat) (hr : r < ℓ) (hr' : r' < ℓ) :
    (((circulant ℓ p).getD r []).zip ((circulant ℓ q).getD r' [])).countP (fun x => x.1 && x.2)
      = ((List.range ℓ).filter
          (fun s => p.contains ((s + ℓ - r) % ℓ) && q.contains ((s + ℓ - r') % ℓ))).length

The GF(2) overlap count of two circulant rows is the number of columns `s` where both circulants are set — `#{s < ℓ : (s−r)∈p ∧ (s−r')∈q}`. (The next step rewrites this count as a `circMul ℓ p (circDagger ℓ q)` convolution coefficient via the `s ↦ (s−r)` bijection.)

FormalRV.QEC.LPInstancesValid

FormalRV/QEC/LPInstancesValid.lean

FormalRV.QEC.LPInstancesValid — the PARAMETRIC `liftedProduct_well_shaped` instantiated at the ACTUAL paper codes lp16 / lp20 / lp24, NATIVE-FREE. `Instances.lean` flags `well_shaped`/`css_condition` for these codes as residues "infeasible to elaborate" at the ~2600/4350/5278-column scale (only the `n`-count is discharged there). But the well_shaped half is NOT scale-bound: `liftedProduct_well_shaped` (proved parametrically in `LPCssCondition.lean`) needs only the 3×7 SEED's shape, which is a tiny `decide`. So `well_shaped` for the real codes follows with NO `decide`/`native_decide` on the big matrices — the parametric proof paying off on the paper instances. This closes the `well_shaped` half of `code.valid` (the verifier's `hCSS`) for lp16/lp20/lp24. (`css_condition` remains the in-progress half — see `LPCssCondition.lean` §9.) No `sorry`, no `axiom`, no `native_decide`.

theoremlp16_well_shaped

theorem lp16_well_shaped : lp16.well_shaped = true

*`lp16` ([[2610,744,16]]) is well-shaped — native-free.** From the parametric `liftedProduct_well_shaped`; the only `decide`s are on the 3×7 seed `A_lp16`'s shape (`length = 3`, rows `length = 7`), NOT the 2610-column check matrices.

theoremlp20_well_shaped

theorem lp20_well_shaped : lp20.well_shaped = true

*`lp20` ([[4350,1224,20]]) is well-shaped — native-free.**

theoremlp24_well_shaped

theorem lp24_well_shaped : lp24.well_shaped = true

*`lp24` ([[5278,1480,24]]) is well-shaped — native-free.**

theoremlp_codes_well_shaped

theorem lp_codes_well_shaped :
    lp16.well_shaped = true ∧ lp20.well_shaped = true ∧ lp24.well_shaped = true

The well_shaped half of `code.valid` holds for all three real LP memory codes, with no `decide`/`native_decide` at the 2600–5300-column scale.

FormalRV.QEC.Logical

FormalRV/QEC/Logical.lean

FormalRV.QEC.Logical — the LOGICAL-OPERATOR layer of the QEC code-construction framework. This level lets a user DEFINE a code's logical operators — especially the logical Z̄ — and fix the logical-qubit INDEX `i : Fin k` within a code block, with a fully DECIDABLE validity predicate. A CSS code (`FormalRV.QEC.CSSCode`) is specified by its check matrices `(hx, hz)`. Those pin the *stabilizer* group, but NOT which Pauli operators play the role of the encoded logical X̄_i / Z̄_i. A user must declare those. This file is the type + decidable contract for that declaration: `LogicalBasis c k` — the user's declared `lx`/`lz` supports, indexed by the logical-qubit index `Fin k`. `LogicalBasis.valid` — a `Bool` that holds iff the declared operators commute with every stabilizer and satisfy the symplectic δ_ij pairing (X̄_i anticommutes Z̄_j iff i = j). a worked, `decide`-checked instance: the Steane [[7,1,3]] code. connectors producing the `BoolVec` a `SurgeryGadget.target_pauli` must equal when measuring a logical Z̄_i / X̄_i. RESIDUE (flagged honestly): `valid` captures commute-with-stabilizers plus the δ_ij pairing. It does NOT check *independence modulo stabilizers* — i.e. that no declared logical is a product of stabilizers (which would make it act trivially) — because that needs a GF(2) rank / nullspace computation living in a later module (`GF2Linear` provides the inner-product layer; rank/echelon is deferred). When `k` equals the code's true logical dimension and the δ_ij pairing holds, the δ pairing already forces the declared logicals to be genuinely independent nontrivial logical operators, so `valid` is sufficient for the worked small instances here; the rank check is the one residue at this layer. No Mathlib. Pure Bool / Nat / List + `decide`.

structureLogicalBasis

structure LogicalBasis (c : CSSCode) (k : Nat)

A user-declared logical basis for a CSS code `c` with `k` logical qubits. `lx i` / `lz i` are the GF(2) supports (length `c.n`) of the logical X̄_i / Z̄_i operators — the i-th logical qubit's operators. This is how a user "defines the logical Z operation" and fixes the logical-qubit INDEX within the code block.

defxbar

def xbar {c k} (L : LogicalBasis c k) (i : Fin k) : PauliString

The logical X̄_i operator as an X/I `PauliString`, via the canonical check-matrix→Pauli lowering `CSSCode.xStab`.

defzbar

def zbar {c k} (L : LogicalBasis c k) (i : Fin k) : PauliString

The logical Z̄_i operator as a Z/I `PauliString`, via the canonical check-matrix→Pauli lowering `CSSCode.zStab`.

defx_in_ker_hz

def x_in_ker_hz {c k} (L : LogicalBasis c k) : Bool

X̄_i commutes with every Z-check: `lx i` ⟂ every row of `hz` (even overlap, `dotBit = false`).

defz_in_ker_hx

def z_in_ker_hx {c k} (L : LogicalBasis c k) : Bool

Z̄_j commutes with every X-check: `lz j` ⟂ every row of `hx` (even overlap, `dotBit = false`).

defpairs_delta

def pairs_delta {c k} (L : LogicalBasis c k) : Bool

Symplectic pairing δ_ij: X̄_i anticommutes Z̄_j iff `i = j`. `dotBit (lx i) (lz j)` is the GF(2) overlap bit = the symplectic anticommutation indicator (see `CSSCode.xStab_zStab_commutes`).

defvalid

def valid {c k} (L : LogicalBasis c k) : Bool

Headline decidable validity. Independence-mod-stabilizers (GF(2) rank) is deferred to a later module; this captures commute-with-stabilizers (`x_in_ker_hz` ∧ `z_in_ker_hx`) plus the δ_ij pairing (`pairs_delta`), which already pins the declared `lx`/`lz` as genuine independent logical operators when `k` matches the code's true logical dimension.

deftoSurgeryTargetZ

def toSurgeryTargetZ {c k} (L : LogicalBasis c k) (i : Fin k) (ancilla_n : Nat) : BoolVec

The surgery `target_pauli` for measuring logical Z̄_i: the i-th Z-logical support, zero-extended onto an `ancilla_n`-qubit ancilla block. This is exactly the vector a `SurgeryGadget.target_pauli` must equal (its `targets_logical_correctly` row-span identity is qianxu's kernel condition ⟨ℒ⟩ = f_X'ᵀ ker(H_X'ᵀ) with this target).

deftoSurgeryTargetX

def toSurgeryTargetX {c k} (L : LogicalBasis c k) (i : Fin k) (ancilla_n : Nat) : BoolVec

The surgery `target_pauli` for measuring logical X̄_i: the i-th X-logical support, zero-extended onto an `ancilla_n`-qubit ancilla block.

defsteaneCSS

def steaneCSS : CSSCode

The Steane [[7,1,3]] CSS code. Both `hx` and `hz` are the three weight-4 rows of the `[7,4]` Hamming parity-check matrix.

example(example)

example : steaneCSS.well_shaped = true

The Steane code is well-shaped (all rows length 7).

example(example)

example : steaneCSS.css_condition = true

The Steane code satisfies the CSS commutation condition `H_X H_Z^T = 0` (every pair of weight-4 Hamming rows overlaps in an even number of positions).

defsteaneLogical

def steaneLogical : LogicalBasis steaneCSS 1

A logical basis for Steane, `k = 1`. The single logical qubit uses the all-ones weight-7 vector for BOTH X̄ and Z̄: overlap with each weight-4 Hamming row = 4 (even) ⇒ commutes with every X- and Z-check; overlap of X̄ with Z̄ = 7 (odd) ⇒ they anticommute, giving δ_00.

theoremsteaneLogical_valid

theorem steaneLogical_valid : steaneLogical.valid = true

*Worked-instance validity**: the declared Steane logical basis is valid (commutes with all stabilizers and realises the δ_ij pairing).

example(example)

example : (steaneLogical.toSurgeryTargetZ 0 2).length = 9

Smoke: the Z̄_0 surgery target, zero-extended onto a 2-qubit ancilla block, has length 7 + 2 = 9.

example(example)

example : (steaneLogical.toSurgeryTargetX 0 2).length = 9

Smoke: the X̄_0 surgery target on the same ancilla block also has length 9.

FormalRV.QEC.LogicalFinder

FormalRV/QEC/LogicalFinder.lean

FormalRV.QEC.LogicalFinder — DETERMINE the logical operators of a CSS code from its check matrices, DEFINING its logical qubits. John (2026-06-03): "the first thing we must solve is to determine all Logical Z of these codes, otherwise the logical qubits/index is not even defined and there is no way to compile [a PPM]." Right — `LogicalBasis` was hand-filled; there was no algorithm to FIND the logicals. This module adds the missing GF(2) NULLSPACE (`GF2Rank` had only rank / rowspace-membership) and the logical-operator finder: logical Z of a CSS code = ker(H_X) / rowspace(H_Z) (k = n − rank H_X − rank H_Z) logical X of a CSS code = ker(H_Z) / rowspace(H_X) Each computed logical Z commutes with every X-check (in ker H_X) and is NOT a Z-stabilizer (outside rowspace H_Z) — a genuine element of N(S)\S. The k logical Z operators ARE the k logical-qubit names: logical qubit `i` is the one measured by `logicalZ c |>.get i`. General (any CSS code), `decide`-verified on a real bivariate-bicycle code (qianxu's LP family) at 18 qubits + Steane + [[4,2,2]]. No Mathlib. No `sorry`, no `axiom`.

defrref

def rref (mat : BoolMat) : BoolMat

Reduced row echelon form: echelon-reduce, then back-substitute each pivot against the others (clears bits above pivots), giving distinct pivot columns each set in exactly one row.

defkernelBasis

def kernelBasis (mat : BoolMat) (n : Nat) : List BoolVec

A basis of the GF(2) KERNEL of `mat` over `n` columns: one null vector per FREE (non-pivot) column. `kernelBasis` has dimension `n − rank mat`.

defgf2dot

def gf2dot (u v : BoolVec) : Bool

GF(2) inner product (parity of the overlap).

deflogicalBasis

def logicalBasis (stab coStab : BoolMat) (n : Nat) : List BoolVec

Logical operators: a basis of `ker(stab)` reduced MODULO `rowspace(coStab)` — the `k` generators of N(S)\S in this sector.

deflogicalZ

def logicalZ (c : FormalRV.QEC.CSSCode) : List BoolVec

The logical Z operators of a CSS code = ker(H_X) / rowspace(H_Z). These DEFINE the logical qubits: logical qubit `i` is named by `(logicalZ c).get i`.

deflogicalX

def logicalX (c : FormalRV.QEC.CSSCode) : List BoolVec

The logical X operators of a CSS code = ker(H_Z) / rowspace(H_X).

defnumLogicals

def numLogicals (c : FormalRV.QEC.CSSCode) : Nat

The number of logical qubits, DERIVED as the count of logical Z operators found.

deflogicalZ_genuine

def logicalZ_genuine (c : FormalRV.QEC.CSSCode) : Bool

Every computed logical Z is GENUINE: it commutes with all X-checks (in ker H_X) and is not a Z-stabilizer (outside rowspace H_Z).

deflogicalX_genuine

def logicalX_genuine (c : FormalRV.QEC.CSSCode) : Bool

Every computed logical X is genuine (in ker H_Z, outside rowspace H_X).

defbbSmall

def bbSmall : FormalRV.QEC.CSSCode

A small bivariate-bicycle code `[[18, 2, d]]` (qianxu's LP family, l=m=3): genuine BB structure, k=2 (high-rate), `decide`-tractable.

theorembbSmall_2_logical_qubits

theorem bbSmall_2_logical_qubits : numLogicals bbSmall = 2

*The BB code has exactly 2 logical qubits, DETERMINED from its matrices** — its two logical Z operators are computed, not asserted.

theorembbSmall_logicalZ_genuine

theorem bbSmall_logicalZ_genuine : logicalZ_genuine bbSmall = true

*Every computed logical Z of the BB code is genuine** (commutes with all X-checks, is not a Z-stabilizer) — so the 2 logical qubits are well-defined.

theorembbSmall_logicalX_genuine

theorem bbSmall_logicalX_genuine : logicalX_genuine bbSmall = true

…and likewise the logical X operators.

theoremsteane_1_logical

theorem steane_1_logical : numLogicals FormalRV.QEC.steaneCSS = 1 ∧ logicalZ_genuine FormalRV.QEC.steaneCSS = true

Steane [[7,1,3]]: the finder returns exactly 1 logical qubit, genuine.

theoremcode422_2_logical

theorem code422_2_logical : numLogicals code422 = 2 ∧ logicalZ_genuine code422 = true

[[4,2,2]]: the finder returns exactly 2 logical qubits, genuine.

defgf2Inverse

def gf2Inverse (M : BoolMat) (k : Nat) : Option BoolMat

GF(2) `k×k` matrix inverse via Gaussian elimination on `[M | I]` (`none` if singular).

defpairingMatrix

def pairingMatrix (lx lz : List BoolVec) : BoolMat

The `k×k` symplectic pairing matrix `M_ij = gf2dot(X̄_i, Z̄_j)`.

defrelabel

def relabel (Minv : BoolMat) (lx : List BoolVec) (n : Nat) : List BoolVec

Relabel a basis `lx` by a `k×k` matrix `Minv` over `n` columns: `lx'_i = ⊕_l Minv_il · lx_l`.

defpairedLogicalX

def pairedLogicalX (c : FormalRV.QEC.CSSCode) : List BoolVec

The logical X basis RELABELLED to pair symplectically with `logicalZ c`.

defbbSmallLogicalBasis

def bbSmallLogicalBasis : FormalRV.QEC.LogicalBasis bbSmall 2

A computed `LogicalBasis` for the BB code `[[18,2,d]]`: Z̄_i from `logicalZ`, X̄_i from the symplectically-paired `pairedLogicalX` — both DERIVED from the check matrices, defining the 2 logical qubits.

theorembbSmallLogicalBasis_valid

theorem bbSmallLogicalBasis_valid : bbSmallLogicalBasis.valid = true

*The BB code's computed logical basis is VALID**: each X̄/Z̄ commutes with the stabilizers and the symplectic form is `δ_ij` — the 2 logical qubits are well-defined, computed from the matrices (not asserted). Kernel-clean by decide.

FormalRV.QEC.LogicalGenuine

FormalRV/QEC/LogicalGenuine.lean

FormalRV.QEC.LogicalGenuine — a VALID logical basis is GENUINE (its operators are real logical operators, not stabilizers), proven PARAMETRICALLY with NO rank / NO `decide` at scale — using only the GF(2)-linearity cornerstone. This dissolves the "homological-dimension wall" for COMPILATION CORRECTNESS. The strengthened verifier (`ShorLPContract`) demands the logical qubits be genuine; the obvious route was `k = n − rank H_X − rank H_Z` (a rank at 4350 columns, forbidden by the no-native acceptance). But genuineness does NOT need the rank: if a basis is `valid` (`x_in_ker_hz ∧ z_in_ker_hx ∧ pairs_delta`), the symplectic δ-pairing ALONE forces each logical to lie OUTSIDE the stabilizer rowspace — proven here via `dotBit_row_combination` (orthogonality to a set of rows propagates to their whole GF(2) span, by linearity). Consequence: a `valid` basis of `k` operators is `k` genuine, independent logical qubits, with NO claim about (and no computation of) the total logical dimension. A correct compilation runs on exactly those `k` qubits. No Mathlib heavy machinery, no `sorry`, no `axiom`.

theoremdotBit_row_combination

theorem dotBit_row_combination (n : Nat) (sel : BoolVec) (mat : BoolMat) (v : BoolVec)
    (hn : v.length = n) (hmat : ∀ r ∈ mat, r.length = n)
    (hrows : ∀ r ∈ mat, dotBit r v = false) :
    dotBit (row_combination sel mat) v = false

*A vector orthogonal to every row of a matrix is orthogonal to every GF(2) combination of those rows** (the rowspace). By induction on the selection, using the linearity cornerstone `dotBit_vec_xor`. No `decide` at scale.

theoremvalid_logical_not_Zstabilizer

theorem valid_logical_not_Zstabilizer (c : CSSCode) (k : Nat) (L : LogicalBasis c k)
    (hv : L.valid = true) (hlx : ∀ i : Fin k, (L.lx i).length = c.n)
    (hhz : ∀ r ∈ c.hz, r.length = c.n) (j : Fin k) (w : BoolVec) :
    L.lz j ≠ row_combination w c.hz

*No Z-logical of a valid basis is a Z-stabilizer.** If `L.lz j` were a GF(2) combination of Z-checks, then (by `dotBit_row_combination` and `x_in_ker_hz`) it would be orthogonal to `L.lx j`, contradicting the symplectic `pairs_delta` (`dotBit(X̄ⱼ,Z̄ⱼ)=1`). Parametric; no rank, no `decide` at scale.

theoremvalid_logical_not_Xstabilizer

theorem valid_logical_not_Xstabilizer (c : CSSCode) (k : Nat) (L : LogicalBasis c k)
    (hv : L.valid = true) (hlz : ∀ i : Fin k, (L.lz i).length = c.n)
    (hhx : ∀ r ∈ c.hx, r.length = c.n) (j : Fin k) (w : BoolVec) :
    L.lx j ≠ row_combination w c.hx

*No X-logical of a valid basis is an X-stabilizer** (the exact dual, via `z_in_ker_hx`).

theoremvalid_basis_genuine

theorem valid_basis_genuine (c : CSSCode) (k : Nat) (L : LogicalBasis c k) (hv : L.valid = true)
    (hlx : ∀ i : Fin k, (L.lx i).length = c.n) (hlz : ∀ i : Fin k, (L.lz i).length = c.n)
    (hhx : ∀ r ∈ c.hx, r.length = c.n) (hhz : ∀ r ∈ c.hz, r.length = c.n) :
    (∀ (j : Fin k) (w : BoolVec), L.lz j ≠ row_combination w c.hz)
    ∧ (∀ (j : Fin k) (w : BoolVec), L.lx j ≠ row_combination w c.hx)

*A valid logical basis is GENUINE — parametrically, with no rank computation.** Every logical operator is neither a stabilizer of its own type (Z̄ⱼ not a Z-stabilizer, X̄ⱼ not an X-stabilizer): they are real elements of N(S)\S. So a `valid` basis of `k` operators certifies `k` genuine logical qubits WITHOUT computing `n − rank − rank` — the route that makes lp16/lp20 logical-qubit genuineness reachable without `native_decide`.

FormalRV.QEC.LogicalMeasurementGeneral

FormalRV/QEC/LogicalMeasurementGeneral.lean

FormalRV.QEC.LogicalMeasurementGeneral — SCALE-FREE logical-measurement semantics: prove the LP-code measurement correctness GENERICALLY (∀ CSS code, from `LogicalBasis.valid`), so bbSmall / lp16 / lp20 are instances and there is NO `decide` on the stabilizer state at scale. John: "use some smarter way to avoid the scalability issue." Right — the residue was that the LP-code Gottesman semantics were proven by `decide` at 18 qubits, so lp16/lp20 only appeared as plugged-in numbers. The fix is a PARAMETRIC proof: the non-disturbance of a logical-Z measurement is a general stabilizer-algebra fact that follows from the GF(2) commutation data already packaged in `LogicalBasis.valid` (`z_in_ker_hx`, `pairs_delta`), via `apply_PPM_pos_preserves_mem_of_commutes` — by structure, NOT by enumeration. Consequently the SEMANTIC theorems below mention no fixed code and no `decide`: • a single logical-Z PPM preserves every stabilizer and every OTHER logical (∀ code); • the FULL modexp (any-length logical-Z sequence) preserves every stabilizer (∀ code). The only per-code obligation is `z_in_ker_hx` — a sparse GF(2) orthogonality predicate (linear, far cheaper than a rank/`decide` on the full stabilizer state, and for the structured LP codes it follows from the polynomial orthogonality by construction). No Mathlib heavy machinery, no `sorry`, no `axiom`.

theoremdotBit_comm

theorem dotBit_comm (a b : BoolVec) : dotBit a b = dotBit b a

The GF(2) inner product `dotBit` is symmetric.

defcodeStateWithLogicals

def codeStateWithLogicals (c : CSSCode) (k : Nat) (L : LogicalBasis c k) : StabilizerState

The stabilizer state of a CSS code together with all `k` logical-X generators (the logical qubits in an X-eigenstate) — the state on which a logical-Z measurement acts. Generic in the code `c` and logical basis `L`.

theoremstab_commutes_zbar

theorem stab_commutes_zbar (c : CSSCode) (k : Nat) (L : LogicalBasis c k)
    (hzk : L.z_in_ker_hx = true) (i : Fin k) (g : PauliString)
    (hg : g ∈ c.hx.map CSSCode.xStab ++ c.hz.map CSSCode.zStab) :
    g.commutes (L.zbar i) = true

*Every stabilizer commutes with the measured logical Z̄_i** — from `z_in_ker_hx` (Z̄_i ⟂ all X-checks) and the fact that Z/I strings always commute with Z-checks. Generic; no `decide`.

theoremxbar_commutes_zbar

theorem xbar_commutes_zbar (c : CSSCode) (k : Nat) (L : LogicalBasis c k)
    (hpd : L.pairs_delta = true) (i j : Fin k) (hij : j ≠ i) :
    (L.xbar j).commutes (L.zbar i) = true

*Logical X̄_j (j ≠ i) commutes with the measured logical Z̄_i** — from `pairs_delta` (the symplectic form is δ_ij). Generic; no `decide`.

theoremlogicalZ_preserves_stabilizers

theorem logicalZ_preserves_stabilizers (c : CSSCode) (k : Nat) (L : LogicalBasis c k)
    (hzk : L.z_in_ker_hx = true) (i : Fin k) (g : PauliString)
    (hg : g ∈ c.hx.map CSSCode.xStab ++ c.hz.map CSSCode.zStab) :
    g ∈ apply_PPM_pos (codeStateWithLogicals c k L) (L.zbar i)

*A logical-Z measurement preserves every stabilizer — for ANY CSS code.** From `z_in_ker_hx` and `apply_PPM_pos_preserves_mem_of_commutes`. No `decide`, no fixed code: bbSmall / lp16 / lp20 are all instances.

theoremlogicalZ_preserves_other_logicals

theorem logicalZ_preserves_other_logicals (c : CSSCode) (k : Nat) (L : LogicalBasis c k)
    (hpd : L.pairs_delta = true) (i j : Fin k) (hij : j ≠ i) :
    L.xbar j ∈ apply_PPM_pos (codeStateWithLogicals c k L) (L.zbar i)

*A logical-Z measurement preserves every OTHER logical qubit — for ANY CSS code.** From `pairs_delta`. No `decide`.

theoremfull_modexp_preserves_code_general

theorem full_modexp_preserves_code_general (c : CSSCode) (k : Nat) (L : LogicalBasis c k)
    (hzk : L.z_in_ker_hx = true) (ps : List PauliString)
    (hps : ∀ P ∈ ps, ∃ i : Fin k, P = L.zbar i)
    (g : PauliString) (hg : g ∈ c.hx.map CSSCode.xStab ++ c.hz.map CSSCode.zStab) :
    g ∈ measureChecks ps (codeStateWithLogicals c k L)

*THE FULL MODEXP, SCALE-FREE.** For ANY CSS code `c` with a logical basis whose `z_in_ker_hx` holds, and ANY sequence `ps` of logical-Z measurements (the full ≈10⁹-PPM modexp included), EVERY stabilizer survives the whole computation `measureChecks ps`. Proved by induction on `ps` (via `mem_measureChecks_of_commutesAll`) from the generic per-PPM commutation — NO `decide`, NO fixed code, NO scale ceiling. lp16 [[2610,…]] and lp20 [[4350,…]] are covered by this single theorem; the only per-code obligation is the sparse GF(2) predicate `z_in_ker_hx`.

theoremfull_modexp_preserves_code_of_valid

theorem full_modexp_preserves_code_of_valid (c : CSSCode) (k : Nat) (L : LogicalBasis c k)
    (hv : L.valid = true) (ps : List PauliString)
    (hps : ∀ P ∈ ps, ∃ i : Fin k, P = L.zbar i)
    (g : PauliString) (hg : g ∈ c.hx.map CSSCode.xStab ++ c.hz.map CSSCode.zStab) :
    g ∈ measureChecks ps (codeStateWithLogicals c k L)

The full-modexp code-preservation specialised to a code whose `LogicalBasis` is valid: validity (which includes `z_in_ker_hx`) is the ONLY per-code input.

FormalRV.QEC.LogicalValidity

FormalRV/QEC/LogicalValidity.lean

FormalRV.QEC.LogicalValidity — the NON-TRIVIALITY / independence layer that closes the one RESIDUE flagged in `Logical.lean`. `LogicalBasis.valid` (in `Logical.lean`) checks that a declared logical basis COMMUTES with every stabilizer and realises the symplectic δ_ij pairing. But commuting with the stabilizers is necessary, NOT sufficient, for being a genuine logical operator: a stabilizer itself commutes with every stabilizer. A genuine logical lies in N(S)\S — it must ALSO lie OUTSIDE the stabilizer group, i.e. it is not a product of stabilizers. This file adds that GF(2)-rank condition using `GF2Rank.inRowspace` / `GF2Rank.rank`: `outsideStabZ` / `outsideStabX` — every declared logical is NOT in the rowspace of the corresponding check matrix (not a product of checks). `independentModStabZ` / `independentModStabX` — the `k` logical supports raise the stabilizer rank by exactly `k` (they are mutually independent modulo the stabilizers). `is_logical_basis` — the COMPLETE N(S)\S condition: `valid` ∧ outside ∧ independent. DISCRIMINATING DEMO: a declared "logical Z" that is actually a row of `hz` (a stabilizer) passes `valid` (it commutes with everything) but is correctly REJECTED by `outsideStabZ` / `is_logical_basis`. All verification here is `decide` at the worked Steane instance. No Mathlib. Pure Bool / Nat / List + `decide`.

defoutsideStabZ

def outsideStabZ {c k} (L : LogicalBasis c k) : Bool

Every Z̄_i is OUTSIDE the Z-stabilizer group: `lz i` is not in the GF(2) rowspace of `hz` (not a product of Z-checks).

defoutsideStabX

def outsideStabX {c k} (L : LogicalBasis c k) : Bool

Every X̄_j is OUTSIDE the X-stabilizer group: `lx j` is not in the GF(2) rowspace of `hx` (not a product of X-checks).

defindependentModStabZ

def independentModStabZ {c k} (L : LogicalBasis c k) : Bool

The `k` logical-Z supports raise the Z-stabilizer rank by exactly `k`: they are mutually independent modulo the stabilizers (a basis-level strengthening of `outsideStabZ`).

defindependentModStabX

def independentModStabX {c k} (L : LogicalBasis c k) : Bool

The `k` logical-X supports raise the X-stabilizer rank by exactly `k`.

defis_logical_basis

def is_logical_basis {c k} (L : LogicalBasis c k) : Bool

A GENUINE logical basis: `valid` (commute with all stabilizers + δ_ij symplectic pairing) AND every declared logical is OUTSIDE the stabilizer group AND the logicals are mutually independent modulo stabilizers. Together these are the complete `N(S)\S` membership condition — they rule out a "logical" that is secretly a stabilizer (commutes, but acts trivially on the code space).

theoremsteaneLogical_outsideStabZ

theorem steaneLogical_outsideStabZ : steaneLogical.outsideStabZ = true

The all-ones Steane Z̄ is OUTSIDE the Z-stabilizer group (weight 7, odd — not in the even-weight Hamming rowspace).

theoremsteaneLogical_outsideStabX

theorem steaneLogical_outsideStabX : steaneLogical.outsideStabX = true

The all-ones Steane X̄ is OUTSIDE the X-stabilizer group.

theoremsteaneLogical_independentModStabZ

theorem steaneLogical_independentModStabZ : steaneLogical.independentModStabZ = true

The single Steane Z̄ is independent modulo the Z-stabilizers: appending it raises the rank from 3 to 4.

theoremsteaneLogical_independentModStabX

theorem steaneLogical_independentModStabX : steaneLogical.independentModStabX = true

The single Steane X̄ is independent modulo the X-stabilizers.

theoremsteaneLogical_is_logical_basis

theorem steaneLogical_is_logical_basis : steaneLogical.is_logical_basis = true

*HEADLINE (positive)**: the all-ones Steane logical basis is a GENUINE logical operator — it satisfies the complete N(S)\S condition.

deffakeLogical

def fakeLogical : LogicalBasis steaneCSS 1

A FAKE logical basis whose declared "logical Z" is actually the FIRST ROW of the Steane `hz` — i.e. a genuine Z-STABILIZER, not a logical. Its X̄ is kept as the real all-ones logical (so only the Z side is the trap).

theoremfakeLogical_z_in_ker_hx

theorem fakeLogical_z_in_ker_hx : fakeLogical.z_in_ker_hx = true

The fake "logical Z" still COMMUTES with every X-stabilizer (it IS a Z-check row, so it lies in the kernel of every X-check — even overlap). This is exactly the commutation test that is "already checked elsewhere": it is FOOLED by a stabilizer, returning `true`.

theoremfakeLogical_valid_false

theorem fakeLogical_valid_false : fakeLogical.valid = false

The full `valid` predicate happens to also reject THIS particular fake via its δ-pairing clause: a weight-4 Z-stabilizer cannot anticommute with the weight-7 all-ones X̄ (even overlap ⇒ they commute), so `pairs_delta` — and hence `valid` — is `false`. The whole point of this file is that even WITHOUT relying on that δ accident, the GF(2)-rank layer independently rejects the fake (next theorem).

theoremfakeLogical_outsideStabZ_false

theorem fakeLogical_outsideStabZ_false : fakeLogical.outsideStabZ = false

The discriminating rejection: the fake "logical Z" is a row of `hz`, hence INSIDE the stabilizer rowspace, so `outsideStabZ` correctly returns `false` — independently of the commutation/δ checks.

theoremfakeLogical_independentModStabZ_false

theorem fakeLogical_independentModStabZ_false :
    fakeLogical.independentModStabZ = false

It is also NOT independent modulo the stabilizers (appending a stabilizer row does not raise the rank).

theoremfakeLogical_is_logical_basis_false

theorem fakeLogical_is_logical_basis_false :
    fakeLogical.is_logical_basis = false

*HEADLINE (negative)**: a stabilizer masquerading as a logical is correctly REJECTED by the complete condition. This is the discriminating test: `valid` alone (commute-with-stabilizers) is FOOLED, but `is_logical_basis` (which enforces N(S)\S via the GF(2)-rank layer) is NOT.

FormalRV.QEC.QECCodeInstances

FormalRV/QEC/QECCodeInstances.lean

FormalRV.Framework.QECCodeInstances — concrete QEC code instances (identifiers for implementer submissions). Codes provided: Steane [[7, 1, 3]] Surface code at distances d = 3, 5, 7, 11, 25 (non-rotated count: [[d², 1, d]]) Bivariate-bicycle qLDPC [[144, 18, 12]] (Cain–Xu et al. 2026 space-efficient memory code variant) Each code carries `(n, k, d)`; concrete parity matrices `hx`, `hz` are filled in per-submission (`steane_713_parity` below for the demonstrative Steane case). ## L4 → L3 contract: implementer-supplied, not framework-derived Per John's directive (2026-05-25): the cycle-level logical error rate is an INPUT to the framework, justified by the implementer through their lower-level code analysis (Monte Carlo, analytic ansatz, decoder model, etc.). The framework does NOT compute it from `p_g` and `d`; that would presuppose a specific code family + subthreshold formula, which is the implementer's responsibility. Concretely: the implementer supplies `HardwareErrorParams` with per-syscall error rates already computed; the framework composes them via union bound. No Mathlib dependency; pure Nat for `decide`.

defsteane_713

def steane_713 : QECCode

Steane [[7, 1, 3]] code. CSS, distance 3, 7 physical qubits per logical. Smallest demonstrative QEC code.

defsurface_d3

def surface_d3 : QECCode

Surface code distance 3, [[9, 1, 3]] (non-rotated).

defsurface_d5

def surface_d5 : QECCode

Surface code distance 5, [[25, 1, 5]].

defsurface_d7

def surface_d7 : QECCode

Surface code distance 7, [[49, 1, 7]].

defsurface_d11

def surface_d11 : QECCode

Surface code distance 11, [[121, 1, 11]]. Typical Gidney-Ekerå 2021 / Gidney 2025 working distance for RSA-2048 surface-code resource estimates.

defsurface_d25

def surface_d25 : QECCode

Surface code distance 25, [[625, 1, 25]]. Hot-storage distance for Gidney 2025 yoked-surface architecture.

deflp_144_18_12

def lp_144_18_12 : QECCode

Cain–Xu et al. 2026 space-efficient lifted-product `[[2610, 744, ≤ 16]]` qLDPC code. Used in qianxu's RSA-2048 estimate; encodes many logical qubits per code block. For per-logical analysis we use the per-logical perspective: each logical qubit costs `n / k ≈ 3.5` physical qubits on this code, much smaller than surface code. Here we provide the [[144, 18, 12]] bivariate-bicycle variant (smaller demonstrative instance from Bravyi et al. 2024).

defsteane_713_with_parity

def steane_713_with_parity : QECCode

Steane [[7, 1, 3]] code WITH concrete parity matrices. Used for the demonstrative Cuccaro-on-Steane submission.