Real blocky rank and a square zero-one family
Lax100002.Definitions · concepts/Lax100002/Definitions.lean · lax-100002
Natural Language Statement
Definition
A blocky pattern labels disjoint rectangles. Real blocky rank is the minimum number of such patterns in a real linear combination. Singleton rectangles prove that this minimum exists. The square family evaluates basis monomials in a binary finite field and appends zero columns.
Concept map
Preparing this local graph with the browser’s fonts…
Lean source
| 1 | /- |
| 2 | Copyright (c) 2026 Anonymous. All rights reserved. |
| 3 | Released under Apache 2.0 license as described in the file LICENSE. |
| 4 | Authors: ChatGPT (OpenAI) |
| 5 | -/ |
| 6 | import Mathlib.Algebra.BigOperators.Fin |
| 7 | import Mathlib.Data.Matrix.Basis |
| 8 | import Mathlib.Data.Matrix.Block |
| 9 | import Mathlib.Data.Nat.Find |
| 10 | import Mathlib.Data.Fintype.EquivFin |
| 11 | import Mathlib.Data.Real.Basic |
| 12 | import Mathlib.FieldTheory.Finite.GaloisField |
| 13 | import Mathlib.Logic.Equiv.Fin.Basic |
| 14 | |
| 15 | /-! |
| 16 | --- |
| 17 | title: Real blocky rank and a square zero-one family |
| 18 | type: definition |
| 19 | --- |
| 20 | A blocky pattern labels disjoint rectangles. Real blocky rank is the minimum |
| 21 | number of such patterns in a real linear combination. Singleton rectangles |
| 22 | prove that this minimum exists. The square family evaluates basis monomials |
| 23 | in a binary finite field and appends zero columns. |
| 24 | -/ |
| 25 | |
| 26 | namespace Lax100002.Definitions |
| 27 | |
| 28 | open scoped BigOperators |
| 29 | |
| 30 | universe u v w x y |
| 31 | |
| 32 | /-- Disjoint rectangles, described by their row and column labels. -/ |
| 33 | structure BlockyPattern (Row : Type u) (Col : Type v) (Label : Type w) where |
| 34 | rowLabel : Row → Option Label |
| 35 | colLabel : Col → Option Label |
| 36 | |
| 37 | /-- The zero-one matrix specified by a blocky pattern. -/ |
| 38 | noncomputable def BlockyPattern.matrix {Row : Type u} {Col : Type v} {Label : Type w} |
| 39 | (B : BlockyPattern Row Col Label) : Matrix Row Col ℝ := by |
| 40 | classical |
| 41 | exact fun i j => match B.rowLabel i with |
| 42 | | none => 0 |
| 43 | | some a => if B.colLabel j = some a then 1 else 0 |
| 44 | |
| 45 | /-- A Boolean matrix whose ones form disjoint row-and-column rectangles. |
| 46 | There can be at most one nonempty rectangle per row, so the finite label |
| 47 | space below is sufficient for the usual notion of a blocky matrix. -/ |
| 48 | def IsBlocky {Row : Type u} {Col : Type v} [Fintype Row] [Fintype Col] |
| 49 | (A : Matrix Row Col ℝ) : Prop := |
| 50 | ∃ B : BlockyPattern Row Col (Fin (Fintype.card Row + Fintype.card Col)), B.matrix = A |
| 51 | |
| 52 | /-- An `r`-term real blocky decomposition. Coefficients may have either sign. -/ |
| 53 | def HasBlockyDecomposition {Row : Type u} {Col : Type v} |
| 54 | [Fintype Row] [Fintype Col] (A : Matrix Row Col ℝ) (r : ℕ) : Prop := |
| 55 | ∃ (coeff : Fin r → ℝ) (B : Fin r → Matrix Row Col ℝ), |
| 56 | (∀ t, IsBlocky (B t)) ∧ A = ∑ t, coeff t • B t |
| 57 | |
| 58 | variable {Row : Type u} {Col : Type v} [Fintype Row] [Fintype Col] |
| 59 | |
| 60 | /-- The all-zero matrix is blocky. -/ |
| 61 | theorem isBlocky_zero : IsBlocky (0 : Matrix Row Col ℝ) := by |
| 62 | refine ⟨⟨fun _ => none, fun _ => none⟩, ?_⟩ |
| 63 | rfl |
| 64 | |
| 65 | /-- A singleton one is a blocky matrix. -/ |
| 66 | theorem isBlocky_single [DecidableEq Row] [DecidableEq Col] (i : Row) (j : Col) : |
| 67 | IsBlocky (Matrix.single i j (1 : ℝ)) := by |
| 68 | classical |
| 69 | let a : Fin (Fintype.card Row + Fintype.card Col) := |
| 70 | (Fintype.equivFin Row i).castAdd (Fintype.card Col) |
| 71 | refine ⟨⟨fun r => if r = i then some a else none, |
| 72 | fun c => if c = j then some a else none⟩, ?_⟩ |
| 73 | ext r c |
| 74 | by_cases hr : r = i |
| 75 | · subst r |
| 76 | by_cases hc : c = j |
| 77 | · subst c |
| 78 | simp [BlockyPattern.matrix] |
| 79 | · simp [BlockyPattern.matrix, hc, Ne.symm hc] |
| 80 | · simp [BlockyPattern.matrix, hr, Ne.symm hr] |
| 81 | |
| 82 | /-- Singleton rectangles weighted by their entries decompose every matrix. -/ |
| 83 | theorem exists_blockyDecomposition (A : Matrix Row Col ℝ) : |
| 84 | ∃ r, HasBlockyDecomposition A r := by |
| 85 | classical |
| 86 | let e := Fintype.equivFin (Row × Col) |
| 87 | refine ⟨Fintype.card (Row × Col), |
| 88 | (fun t => A (e.symm t).1 (e.symm t).2), |
| 89 | (fun t => Matrix.single (e.symm t).1 (e.symm t).2 (1 : ℝ)), ?_, ?_⟩ |
| 90 | · intro t |
| 91 | exact isBlocky_single _ _ |
| 92 | · have hsum : A = ∑ p : Row × Col, |
| 93 | A p.1 p.2 • Matrix.single p.1 p.2 (1 : ℝ) := by |
| 94 | simpa [Fintype.sum_prod_type] using Matrix.matrix_eq_sum_single A |
| 95 | exact hsum.trans (e.symm.sum_comp |
| 96 | (fun p : Row × Col => A p.1 p.2 • Matrix.single p.1 p.2 (1 : ℝ))).symm |
| 97 | |
| 98 | /-- The least number of blocky matrices whose real linear span contains `A`. -/ |
| 99 | noncomputable def blockyRank (A : Matrix Row Col ℝ) : ℕ := by |
| 100 | classical |
| 101 | exact Nat.find (exists_blockyDecomposition A) |
| 102 | |
| 103 | /-- The dimension of the binary extension field at parameter `v`. -/ |
| 104 | def codeDimension (v : ℕ) : ℕ := 2 ^ (2 * v) |
| 105 | |
| 106 | /-- The field dimension is always positive. -/ |
| 107 | theorem codeDimension_pos (v : ℕ) : 0 < codeDimension v := |
| 108 | Nat.pow_pos (by decide) |
| 109 | |
| 110 | /-- The field in which the message polynomial is evaluated. -/ |
| 111 | abbrev BinaryCodeField (v : ℕ) := GaloisField 2 (codeDimension v) |
| 112 | |
| 113 | noncomputable instance binaryCodeFieldFintype (v : ℕ) : Fintype (BinaryCodeField v) := |
| 114 | Fintype.ofFinite _ |
| 115 | |
| 116 | /-- A standard mathlib basis over the binary prime field. -/ |
| 117 | noncomputable def binaryCodeBasis (v : ℕ) : |
| 118 | Module.Basis (Fin (codeDimension v)) (ZMod 2) (BinaryCodeField v) := |
| 119 | Module.finBasisOfFinrankEq (ZMod 2) (BinaryCodeField v) |
| 120 | (GaloisField.finrank 2 (by simp [codeDimension])) |
| 121 | |
| 122 | variable {F : Type*} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] |
| 123 | variable {t : ℕ} (b : Module.Basis (Fin t) (ZMod 2) F) (h : Fin t) |
| 124 | |
| 125 | /-- Each matrix column is the encoding of one basis monomial. -/ |
| 126 | noncomputable def binaryHadamardMatrix (k : ℕ) : |
| 127 | Matrix (F × F) (Fin k × Fin t) (ZMod 2) := |
| 128 | fun p q => b.repr (p.2 * (b q.2 * p.1 ^ (q.1 : ℕ))) h |
| 129 | |
| 130 | /-- Lift each binary entry to the corresponding integer zero or one. -/ |
| 131 | noncomputable def integerHadamardMatrix (k : ℕ) : Matrix (F × F) (Fin k × Fin t) ℤ := |
| 132 | fun p q => (binaryHadamardMatrix b h k p q).val |
| 133 | |
| 134 | abbrev HadamardRows (v : ℕ) := BinaryCodeField v × BinaryCodeField v |
| 135 | |
| 136 | abbrev HadamardColumns (v : ℕ) := |
| 137 | Fin (Fintype.card (BinaryCodeField v) / 2) × Fin (codeDimension v) |
| 138 | |
| 139 | /-- Row `(α, β)`, column `(j, s)` contains the first binary coordinate of |
| 140 | `β * b_s * α^j`, viewed as an integer zero or one. -/ |
| 141 | noncomputable def hadamardGenerator (v : ℕ) : Matrix (HadamardRows v) (HadamardColumns v) ℤ := by |
| 142 | classical |
| 143 | exact |
| 144 | integerHadamardMatrix (binaryCodeBasis v) ⟨0, codeDimension_pos v⟩ |
| 145 | (Fintype.card (BinaryCodeField v) / 2) |
| 146 | |
| 147 | /-- Append zero columns to an by matrix and index both sides by positions below . |
| 148 | The construction uses mathlib's `Matrix.fromBlocks` and standard equivalences. -/ |
| 149 | def padToSquare {K : Type*} [Zero K] {N m : ℕ} |
| 150 | (A : Matrix (Fin N) (Fin m) K) (hm : m ≤ N) : Matrix (Fin N) (Fin N) K := |
| 151 | (Matrix.fromBlocks A (0 : Matrix (Fin N) (Fin (N - m)) K) |
| 152 | (0 : Matrix (Fin 0) (Fin m) K) (0 : Matrix (Fin 0) (Fin (N - m)) K)).submatrix |
| 153 | (Equiv.sumEmpty (Fin N) (Fin 0)).symm |
| 154 | (finSumFinEquiv.trans (finCongr (Nat.add_sub_of_le hm))).symm |
| 155 | |
| 156 | theorem binaryCodeField_card (v : ℕ) : Fintype.card (BinaryCodeField v) = 2 ^ codeDimension v := by |
| 157 | calc |
| 158 | Fintype.card (BinaryCodeField v) = Fintype.card (Fin (codeDimension v) → ZMod 2) := |
| 159 | Fintype.card_congr (binaryCodeBasis v).equivFun.toEquiv |
| 160 | _ = 2 ^ codeDimension v := by simp |
| 161 | |
| 162 | theorem hadamardRows_card (v : ℕ) : |
| 163 | Fintype.card (HadamardRows v) = 2 ^ (2 * codeDimension v) := by |
| 164 | simp only [HadamardRows, Fintype.card_prod, binaryCodeField_card, two_mul, pow_add] |
| 165 | |
| 166 | theorem hadamardColumns_card (v : ℕ) : |
| 167 | Fintype.card (HadamardColumns v) = (2 ^ codeDimension v / 2) * codeDimension v := by |
| 168 | simp [HadamardColumns, binaryCodeField_card] |
| 169 | |
| 170 | theorem hadamardColumns_card_le_rows (v : ℕ) : |
| 171 | Fintype.card (HadamardColumns v) ≤ Fintype.card (HadamardRows v) := by |
| 172 | rw [hadamardColumns_card, hadamardRows_card, |
| 173 | show 2 * codeDimension v = codeDimension v + codeDimension v by omega, pow_add] |
| 174 | exact Nat.mul_le_mul (Nat.div_le_self _ _) |
| 175 | (Nat.le_of_lt (codeDimension v).lt_two_pow_self) |
| 176 | |
| 177 | /-- Reindex the integer zero-one generator over the reals, then append zeros. -/ |
| 178 | noncomputable def squareHadamardMatrix (v : ℕ) : |
| 179 | Matrix (Fin (Fintype.card (HadamardRows v))) |
| 180 | (Fin (Fintype.card (HadamardRows v))) ℝ := by |
| 181 | classical |
| 182 | exact |
| 183 | padToSquare (((hadamardGenerator v).map (Int.castRingHom ℝ)).submatrix |
| 184 | (Fintype.equivFin (HadamardRows v)).symm |
| 185 | (Fintype.equivFin (HadamardColumns v)).symm) (hadamardColumns_card_le_rows v) |
| 186 | |
| 187 | end Lax100002.Definitions |
| 188 |