Superlogarithmic real blocky rank
Lax100002.Main · concepts/Lax100002/Main.lean · lax-100002
Natural Language Statement
Theorem
The square zero-one family has blocky rank greater than a logarithm times an iterated logarithm.
Concept map
Preparing this local graph with the browser’s fonts…
Evidence
This concept declares 11 statements. Each proof establishes one of them relative to its assumptions.
1 blockyRank_gt_of_power_rows proven
2 hadamard_rows_tendsto_atTop proven
3 hadamardGenerator_binary_distance proven
4 hadamardGenerator_real_distance proven
5 squareHadamardMatrix_blockyRank_gt proven
6 squareHadamardMatrix_eventually_gt_logb_two proven
7 squareHadamardMatrix_gt_logb_two proven
8 squareHadamardMatrix_log_loglog_bound proven
9 squareHadamardMatrix_logb_two_superlogarithmic proven
10 squareHadamardMatrix_spec proven
11 squareHadamardMatrix_superlogarithmic proven
In the paper
- page 1 of this submission's paper
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 Lax100002.Definitions |
| 7 | import Mathlib.Analysis.Asymptotics.Lemmas |
| 8 | import Mathlib.Analysis.SpecialFunctions.Log.Base |
| 9 | import Mathlib.InformationTheory.Hamming |
| 10 | |
| 11 | /-! |
| 12 | --- |
| 13 | title: Superlogarithmic real blocky rank |
| 14 | type: theorem |
| 15 | --- |
| 16 | The square zero-one family has blocky rank greater than a logarithm times an iterated logarithm. |
| 17 | -/ |
| 18 | |
| 19 | namespace Lax100002.Main |
| 20 | |
| 21 | open Lax100002.Definitions Matrix Filter Asymptotics |
| 22 | |
| 23 | /-- The blocky rank exceeds the parameter product for every parameter at least twenty. -/ |
| 24 | axiom squareHadamardMatrix_blockyRank_gt (v : ℕ) (hv : 20 ≤ v) : |
| 25 | v * codeDimension v < blockyRank (squareHadamardMatrix v) |
| 26 | |
| 27 | /-- The square matrix has zero-one entries and blocky rank above the parameter product. -/ |
| 28 | axiom squareHadamardMatrix_spec (v : ℕ) (hv : 20 ≤ v) : |
| 29 | (∀ i j, squareHadamardMatrix v i j = 0 ∨ squareHadamardMatrix v i j = 1) ∧ |
| 30 | v * codeDimension v < blockyRank (squareHadamardMatrix v) |
| 31 | |
| 32 | /-- The blocky rank exceeds one quarter of the logarithm times the shifted iterated logarithm. -/ |
| 33 | axiom squareHadamardMatrix_log_loglog_bound (v : ℕ) (hv : 20 ≤ v) : |
| 34 | Real.logb 2 (Fintype.card (HadamardRows v) : ℝ) * |
| 35 | (Real.logb 2 (Real.logb 2 (Fintype.card (HadamardRows v) : ℝ)) - 1) / 4 < |
| 36 | (blockyRank (squareHadamardMatrix v) : ℝ) |
| 37 | |
| 38 | /-- The blocky rank exceeds the base-two logarithm of the dimension. -/ |
| 39 | axiom squareHadamardMatrix_gt_logb_two (v : ℕ) (hv : 20 ≤ v) : |
| 40 | Real.logb 2 (Fintype.card (HadamardRows v) : ℝ) < |
| 41 | (blockyRank (squareHadamardMatrix v) : ℝ) |
| 42 | |
| 43 | /-- The natural logarithm of the dimension is little-o of the blocky rank. -/ |
| 44 | axiom squareHadamardMatrix_superlogarithmic : |
| 45 | (fun v : ℕ => Real.log (Fintype.card (HadamardRows v) : ℝ)) =o[atTop] |
| 46 | (fun v : ℕ => (blockyRank (squareHadamardMatrix v) : ℝ)) |
| 47 | |
| 48 | /-- The base-two logarithm of the dimension is little-o of the blocky rank. -/ |
| 49 | axiom squareHadamardMatrix_logb_two_superlogarithmic : |
| 50 | (fun v : ℕ => Real.logb 2 (Fintype.card (HadamardRows v) : ℝ)) =o[atTop] |
| 51 | (fun v : ℕ => (blockyRank (squareHadamardMatrix v) : ℝ)) |
| 52 | |
| 53 | /-- The blocky rank eventually exceeds the base-two logarithm of the dimension. -/ |
| 54 | axiom squareHadamardMatrix_eventually_gt_logb_two : |
| 55 | ∀ᶠ v : ℕ in atTop, |
| 56 | Real.logb 2 (Fintype.card (HadamardRows v) : ℝ) < |
| 57 | (blockyRank (squareHadamardMatrix v) : ℝ) |
| 58 | |
| 59 | /-- The distance bound rules out every blocky decomposition of the stated size. -/ |
| 60 | axiom blockyRank_gt_of_power_rows |
| 61 | {Row Col : Type*} [Fintype Row] [Fintype Col] |
| 62 | (v h : ℕ) (hv : 20 ≤ v) (hh : codeDimension v ≤ h) |
| 63 | (A : Matrix Row Col ℝ) |
| 64 | (hRow : Fintype.card Row = 2 ^ h) |
| 65 | (hCol : Fintype.card Col = (2 ^ codeDimension v / 2) * codeDimension v) |
| 66 | (hd : ∀ x : Col → ℝ, x ≠ 0 → |
| 67 | Fintype.card Row / 4 ≤ hammingNorm (A *ᵥ x)) : |
| 68 | v * codeDimension v < blockyRank A |
| 69 | |
| 70 | /-- Every nonzero binary message has at least a quarter of the output coordinates nonzero. -/ |
| 71 | axiom hadamardGenerator_binary_distance (v : ℕ) : |
| 72 | ∀ x : HadamardColumns v → ZMod 2, x ≠ 0 → |
| 73 | Fintype.card (HadamardRows v) / 4 ≤ |
| 74 | hammingNorm ((hadamardGenerator v).map (Int.castRingHom (ZMod 2)) *ᵥ x) |
| 75 | |
| 76 | /-- Every nonzero real message has at least a quarter of the output coordinates nonzero. -/ |
| 77 | axiom hadamardGenerator_real_distance (v : ℕ) : |
| 78 | ∀ x : HadamardColumns v → ℝ, x ≠ 0 → |
| 79 | Fintype.card (HadamardRows v) / 4 ≤ |
| 80 | hammingNorm ((hadamardGenerator v).map (Int.castRingHom ℝ) *ᵥ x) |
| 81 | |
| 82 | /-- The square dimensions tend to infinity. -/ |
| 83 | axiom hadamard_rows_tendsto_atTop : |
| 84 | Tendsto (fun v : ℕ => Fintype.card (HadamardRows v)) atTop atTop |
| 85 | |
| 86 | end Lax100002.Main |
| 87 |
Builds on
Used by
none