FR-12: a labeled Hadamard counting counterexample
Recorded by the registry's curators from GitHub; the authors did not submit it here.
George Stepaniants
Proves a complete negative answer to the original labeled real Hadamard counting conjecture. A genuine finite matrix subtype and an injective restricted doubling construction give m! H(m)^2 ≤ H(2m), the exact source power-of-two lower bound, and a counterexample for every positive real constant.
Claims
LEAN VERIFIED
OP-00076 — Counting real Hadamard matrices
Files and sources
- Paper
- OpenProblemsInNLA @ e375a6f, FR-12/lean/ ↗
- Lean bundle
- submissions/bundles/openproblemsinnla-fr-12-lean.tar.gz
- Toolchain
- leanprover/lean4:v4.33.1
- Posted on GitHub
- 12 September 2026
Verification PASSED
- Attempt
- 2
- Toolchain
- leanprover/lean4:v4.33.1
- Auditor
- v1 · modal
- lake build
- succeeded
- Kernel replay
- succeeded
- Duration
- 0:01:25.332534
Declarations audited
| Declaration | Kind | Axioms | Unused hypotheses | Canonical |
|---|---|---|---|---|
| NLA.FR12.not_countingConjecture | theorem · Prop | propext, Classical.choice, Quot.sound | none | matched |
| RegistryProblems.Problem_OP_00076 | definition | propext, Classical.choice, Quot.sound | none | no canonical statement |
NLA.FR12.not_countingConjecture
Not NLA.FR12.CountingConjecture
RegistryProblems.Problem_OP_00076
Prop
Build log
RegistryProblems: built against the registry's copy at 38ca23a44fc2b159a0c944d5c9af39a80eb601c2 rather than the pinned 545a5d18ad3917d52192c41ce172ec4b41945751. Statements are checked by content, not revision. ✔ [2154/2161] Built NLA.FR12.Definitions (3.6s) ✔ [2155/2161] Built NLA.FR12.Semantics (2.7s) ✔ [2156/2161] Built NLA.FR12.Doubling (2.9s) ✔ [2157/2161] Built NLA.FR12.Growth (2.0s) ℹ [2158/2161] Built NLA.FR12.Proof (3.5s) info: NLA/FR12/Proof.lean:20:0: 'NLA.FR12.counting_semantics_proved' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/FR12/Proof.lean:22:0: 'NLA.FR12.injective_doubling_proved' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/FR12/Proof.lean:24:0: 'NLA.FR12.factorial_doubling_proved' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/FR12/Proof.lean:26:0: 'NLA.FR12.power_two_nonempty_proved' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/FR12/Proof.lean:28:0: 'NLA.FR12.power_two_lower_bound_proved' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/FR12/Proof.lean:30:0: 'NLA.FR12.counterexample_proved' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/FR12/Proof.lean:32:0: 'NLA.FR12.not_countingConjecture_proved' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [2159/2161] Built Solution (3.3s) info: Solution.lean:60:0: 'NLA.FR12.counting_semantics' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:62:0: 'NLA.FR12.injective_doubling' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:64:0: 'NLA.FR12.factorial_doubling' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:66:0: 'NLA.FR12.power_two_nonempty' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:68:0: 'NLA.FR12.power_two_lower_bound' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:70:0: 'NLA.FR12.counterexample' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:72:0: 'NLA.FR12.not_countingConjecture' depends on axioms: [propext, Classical.choice, Quot.sound] ✔ [2160/2161] Built RegistryRecord (3.1s) Build completed successfully (2161 jobs).