SeedNormalizationReading
plain-language theorem explainer
A Prop structure packaging the three inputs under which the α seed 4π·11 reads as a U(1) coupling normalization. Two are model conventions (Heaviside–Lorentz α = e²/(4π) and bare charge e² = 1); the load-bearing third is that photon stiffness is the ledger passive-edge count 11, not the gauge-invariant cycle rank 5. Anyone citing the α-genesis quarantine verdict uses this bundle. As a structure definition there is no proof body; the inhabited instance is separate.
Claim. A reading of the fine-structure seed $4\pi\cdot 11$ as a U(1) coupling normalization is the conjunction of three propositions: (i) the Heaviside–Lorentz convention $\alpha = e^2/(4\pi)$; (ii) the bare charge unit $e^2 = 1$ (J-cost Hessian normalized to 1); (iii) the stiffness identification that the passive-edge ledger channel count in spatial dimension $D=3$ is unequal to the cube cycle rank $b_1 = E-V+1$ (which equals 5 on $Q_3$).
background
Module AlphaGenesis.U1Normalization runs a make-or-break quarantine: 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.GaugeFromCube already yields the U(1) group as a parity quotient of $\mathrm{Aut}(Q_3)$, but never touches the α pipeline. A genuine normalization would read inverse coupling off a gauge-invariant Maxwell action: $\alpha^{-1}=(4\pi)\cdot(\mathrm{stiffness})/e^2$.
Spatial dimension is forced to $D=3$. Passive field edges equal total cube edges minus the single active edge, giving 11 for $D=3$; that is the seed's stiffness. By contrast, independent plaquette field strengths of a U(1) gauge field on the cube 1-skeleton are the cycle rank $b_1=E-V+1=12-8+1=5$ (equivalently six faces minus one Bianchi relation). Gauge fixing removes $V-1=7$ link redundancies and again leaves five physical link modes.
The seed's 11 removes only the active edge, not the seven gauge redundancies. So 11 is a ledger recognition-channel count, not a gauge-invariant photon stiffness. The two disagree: $11\neq 5$.
proof idea
No proof body: this is a structure of type Prop with three fields. The first two fields are typed as True (pure model conventions, discharged by trivial). The third field is the inequality passive_field_edges D ≠ cube_cycle_rank, i.e. ledger channel count versus gauge cycle rank on the D=3 cube. Inhabitation is deferred to the downstream instance, which fills the third field by the already-proved mismatch lemma seed_channel_count_ne_gauge_dof.
why it matters
This structure is the honest packaging of the negative quarantine verdict for α genesis. Downstream, seedNormalizationReading inhabits it and certifies the reading as an identification that holds, not a derivation: a genuine gauge-invariant Maxwell seed on the cube would be $4\pi\cdot 5=20\pi\approx 62.8$, excluded from $\alpha^{-1}$ by a wide margin (below 63, while the RS α band sits above 137.030).
In the broader framework the same ledger 11 reappears in $\Omega_\Lambda=11/16$, CKM structure, $\eta_B=\varphi^{-44}$, and $44=4\cdot 11$, so the seed remains a cross-consistent recognition number. What this declaration blocks is any claim that the seed is forced by U(1) Maxwell counting on $Q_3$. The T8/T9 forcing of $D=3$ and the passive-edge count stay intact; only the gauge-normalization promotion fails.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.