MatrixGap.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Size of a binary row kernel

An r-row linear constraint on ℓ binary coordinates leaves a kernel with at least 2^(ℓ-r) elements. This does not require independent constraint rows. The exponent uses natural subtraction, so the assertion also covers r > ℓ. The argument is rank--nullity followed by the exact finite-field cardinality formula; it does not use any inverse theorem or rank-level inequality.

def OAI.MaxCutGames.FromMatrixGap.reduction line 20
Source documentation
Choose the parity error only after the matrix tuple length is fixed, then compose the actual raw-input, matrix-test, and final graph machines.
```
def reduction {ε δ : ℝ} (P : ParameterSelection.OuterParameters ε δ)
    (M : Decoder.MatrixGap.Parameters P.pStar) :
    MachineOutputContract.BinaryGapReduction ε δ := by
…
```
Mentions: OAI.MaxCutGames.ParameterSelection.OuterParameters, OAI.MaxCutGames.Decoder.MatrixGap.Parameters

theorem OAI.MaxCutGames.Inverse.binary_kernel_finrank_lower line 77

Source documentation

Even dependent binary row constraints remove at most one dimension per row.

theorem binary_kernel_finrank_lower {ℓ r : ℕ}
    (A : (Fin ℓ → ZMod 2) →ₗ[ZMod 2] (Fin r → ZMod 2)) :
    ℓ - r ≤ Module.finrank (ZMod 2) A.ker := by
…

theorem OAI.MaxCutGames.Inverse.binary_kernel_card_lower line 93

Source documentation

The cardinality of the binary row kernel is at least 2^(ℓ-r).

theorem binary_kernel_card_lower {ℓ r : ℕ}
    (A : (Fin ℓ → ZMod 2) →ₗ[ZMod 2] (Fin r → ZMod 2)) :
    2 ^ (ℓ - r) ≤ Nat.card A.ker := by
…