Paper

Superlogarithmic Real Blocky Rank

5 pages · 12 marked passages · pdflatex · download PDF · lax-100002

thm✓Lax100002.Main

Superlogarithmic real blocky rank

The square zero-one family has blocky rank greater than a logarithm times an iterated logarithm.

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

Loading the paper…