gauge_redundancy
plain-language theorem explainer
On the 3-cube, U(1) gauge redundancy is V−1 = 7: one phase per vertex minus the global phase that acts trivially on links. Anyone counting physical photon modes from the 12 edges cites this. It is a one-line definition from the forced dimension D=3 and the hypercube vertex count 2^D.
Claim. The U(1) gauge redundancy on the link variables of the $D$-cube is $V-1$, where $V=2^D$ is the number of vertices. With the forced spatial dimension $D=3$, this is $8-1=7$: one local phase per vertex, quotiented by the global phase that acts trivially.
background
Module Alpha Genesis M11 asks whether the $\alpha$ seed $4\pi\cdot 11$ can be promoted from a ledger channel-budget identification to a genuine U(1) coupling normalization on the cube $Q_3$. Foundation work already derives the U(1) group as a parity quotient of $\mathrm{Aut}(Q_3)$, but does not fix the Maxwell stiffness.
Spatial dimension is forced to $D=3$ (T8/T9). The $D$-hypercube then has $V=2^D$ vertices and $E=D\cdot 2^{D-1}$ edges; for $D=3$ one has $V=8$, $E=12$. A U(1) connection lives on the edges. Gauge transformations assign a phase to each vertex; the global (constant) phase multiplies every link by a coboundary that is identically 1, so it is pure redundancy.
Thus the count of independent gauge parameters is $V-1$. The module contrasts this with the cycle rank $b_1=E-V+1=5$ (independent plaquette strengths) and with the ledger seed count $11=E-1$ (passive edges), which is not gauge-invariant.
proof idea
Pure definition: unfold to $\mathrm{cube_vertices}(D)-1$. Upstream, $D:=3$ and $\mathrm{cube_vertices}(d):=2^d$, so the value is $2^3-1=7$. No tactics; the companion theorem gauge_redundancy_eq_7 discharges the numeral by native_decide after unfolding.
why it matters
This is the gauge-fixing half of the photon DOF count on $Q_3$. Downstream, physical_link_dof_eq_cycle_rank shows $E-(V-1)=12-7=5$ equals the cycle rank $b_1$, so two independent routes agree on five gauge-invariant link modes. ForcedClosure packages that equality (and $11\neq 5$) as $\kappa_\gamma$-independent combinatorial facts. U1NormalizationVerdict then records the negative make-or-break result: a true Maxwell seed would be $4\pi\cdot 5=20\pi\approx 62.8$, excluded from $\alpha^{-1}\in(137.030,137.039)$, so the seed $4\pi\cdot 11$ remains a ledger channel count, not a derived U(1) normalization. Ties the alpha pipeline to the eight-vertex cube forced by T7/T8 ($2^3$ ticks, $D=3$).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.