U1NormalizationVerdict
plain-language theorem explainer
Certificate proposition packaging the negative U(1) normalization verdict on the 3-cube: independent gauge-invariant photon modes equal 5 by two routes, the α seed uses the ledger passive-edge count 11 (not 5), and the genuine Maxwell seed 20π lies far below α⁻¹. Anyone auditing Alpha Genesis or the status of 4π·11 as identification versus theorem would cite it. It is a Prop structure whose fields are discharged by named equalities and inequalities elsewhere in the module.
Claim. A proposition asserting five facts together: the cycle rank of the 3-cube 1-skeleton equals $5$; cube edges minus gauge redundancy equals that cycle rank; passive field edges in dimension $D=3$ equal $11$; those passive edges are not equal to the cycle rank; and the gauge-invariant Maxwell seed $4\pi$ times the cycle rank is strictly less than the assembled inverse fine-structure constant $\alpha^{-1}$.
background
Alpha Genesis M11 quarantines a make-or-break question: can the seed $4\pi\cdot 11$ be promoted from a channel-budget identification to a theorem about U(1) coupling normalization on the cube $Q_3$? Foundation work already yields the U(1) group as a parity quotient of $\mathrm{Aut}(Q_3)$, but never reads $\alpha$ off a Maxwell action.
A gauge-invariant U(1) action counts independent plaquette strengths, i.e. the first Betti number $b_1=E-V+1$. With $D=3$, edges are $D\cdot 2^{D-1}=12$ and vertices $2^D=8$, so $b_1=5$. Equivalently, gauge fixing removes $V-1=7$ link phases, leaving $12-7=5$ physical modes. The seed instead uses passive field edges (total edges minus one active edge), which equals $11$ for $D=3$: a ledger recognition-channel count, not photon stiffness.
The assembled $\alpha^{-1}$ is the exponential resummation of that seed (canonical construction near $137.04$), while a genuine gauge-invariant seed would be $4\pi\cdot 5=20\pi\approx 62.8$.
proof idea
No proof body: this is a structure of type Prop whose five fields are named equalities and one strict inequality. An inhabitant is built by supplying the module lemmas that already prove each clause (cycle rank equals 5; physical link degrees of freedom equal cycle rank; passive edges equal 11; $11\neq 5$; gauge-invariant seed excluded below $\alpha^{-1}$). The structure only packages those results into a single certificate type.
why it matters
This is the typed verdict object for the M11 quarantine: the channel-budget reading $\alpha^{-1}=4\pi\cdot 11$ does not promote to a U(1) coupling-normalization theorem on the cube. Downstream, u1NormalizationVerdict is the concrete inhabitant that fills every field, so any later audit or export can depend on one Prop rather than five scattered lemmas.
Framework-wise it separates ledger numerology (the same $11$ appearing in $\Omega_\Lambda=11/16$, CKM structure, and related $\phi$-ladder counts) from gauge-invariant Maxwell stiffness ($5$, forced by $D=3$ cube topology and the eight-tick / $T8$ spatial setting). The genuine gauge seed $20\pi$ is excluded from the RS $\alpha^{-1}$ band near $137$, so the seed remains an identification, not a derived coupling. That keeps the OPEN infrared boundary-condition status of exact $\alpha^{-1}(0)$ honest rather than overclaimed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.