cube_cycle_rank_eq_5
plain-language theorem explainer
The cycle rank of the cube graph Q₃ equals 5: independent U(1) plaquette field strengths are b₁ = E − V + 1 = 12 − 8 + 1. Anyone citing the Alpha-Genesis U(1) normalization verdict or the forced-closure package needs this equality. The proof unfolds the definition and discharges the arithmetic by native decision.
Claim. The cycle rank of the 3-cube 1-skeleton equals five: $b_1(Q_3) = E - V + 1 = 12 - 8 + 1 = 5$.
background
Module Alpha Genesis M11 asks whether the α seed $4\pi\cdot 11$ can be promoted from a ledger channel-budget identification to a genuine U(1) coupling-normalization theorem on the cube $Q_3$. A gauge-invariant Maxwell action counts independent plaquette field strengths, i.e. the first Betti number of the 1-skeleton.
The definition cube_cycle_rank is exactly that count: $E - V + 1$ with the cube edge and vertex cardinalities. Equivalently one may count six faces minus the single global Bianchi/closure relation $\prod F = 1$. The module records a sharp negative verdict: the seed's 11 is a passive-edge ledger count, not this gauge-invariant photon degree-of-freedom count.
Upstream, the definition itself states: independent plaquette field strengths equal the cycle rank $b_1 = E - V + 1$, and for $Q_3$ that is $12 - 8 + 1 = 5$.
proof idea
One-line term-mode proof. Unfold the definition of the cycle rank (edges minus vertices plus one) and finish by native_decide, which evaluates the concrete natural-number arithmetic $12 - 8 + 1 = 5$ at compile time. No intermediate lemmas are required beyond the definition.
why it matters
This equality is the combinatorial core of the U(1) normalization quarantine. Downstream it is packaged into u1NormalizationVerdict as the fact that the gauge DOF count is 5, and it feeds forcedClosure_holds in KappaGammaIrreducibility (forced-closure facts hold for every kinetic normalization $\kappa_\gamma$).
Sibling theorems rebuild the same 5 two ways: faces-minus-Bianchi (gauge_dof_via_faces) and physical link modes $E - (V-1)$ (physical_link_dof_eq_cycle_rank). The mismatch $11 \neq 5$ (seed_channel_count_ne_gauge_dof) then shows the ledger seed is not a gauge-invariant photon stiffness. The would-be gauge-invariant seed $4\pi\cdot 5 = 20\pi \approx 62.8$ is excluded from $\alpha^{-1}$ by a wide margin (well below the RS band $(137.030, 137.039)$).
In the broader framework this closes a make-or-break test: $\alpha^{-1} = 4\pi\cdot 11$ remains a striking ledger number (also appearing in $\Omega_\Lambda = 11/16$ and related counts) but does not promote to a cube Maxwell normalization theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.