gauge_redundancy_eq_7
plain-language theorem explainer
The U(1) gauge redundancy on the 3-cube equals 7: one phase per vertex minus the global phase. Anyone tracking the Alpha Genesis U(1) normalization test cites this to separate ledger channel counts from gauge-invariant photon modes. The proof unfolds the definition as vertex count minus one and discharges the arithmetic by native decision.
Claim. The U(1) gauge redundancy on the cube graph equals $7$, that is, the number of vertices minus one: $V-1=8-1=7$.
background
This module runs the make-or-break test: can the $\alpha$ seed $4\pi\cdot 11$ promote from a ledger identification to a genuine U(1) coupling normalization on the cube $Q_3$? A gauge-invariant Maxwell action on the cube counts independent plaquette field strengths, i.e. the cycle rank $b_1=E-V+1=12-8+1=5$. Gauge fixing removes one U(1) phase per vertex, minus the global phase that acts trivially.
Gauge redundancy is defined as the cube vertex count minus one. For the 3-cube one has $V=8$ and $E=12$, so the redundancy is $7$ and the physical link modes are $12-7=5$. The seed's $11=E-1$ removes only the single active edge, not these seven gauge redundancies.
proof idea
One-line term-style proof: unfold the definition of gauge redundancy (cube vertices minus one) and finish by native_decide, which evaluates the concrete natural-number arithmetic $8-1=7$.
why it matters
Feeds the parent theorem that physical link modes equal the cycle rank: $E-(V-1)=12-7=5$. Those two routes to the gauge-invariant photon count agree. The module's negative verdict then contrasts this $5$ with the seed channel count $11=E-1$, so $11$ is a ledger recognition-channel count, not a gauge-invariant photon stiffness. 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 the RS band $(137.030,137.039)$. The channel-budget reading of $\alpha^{-1}=4\pi\cdot 11$ therefore does not promote to a U(1) coupling-normalization theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.