rung_sum_equals_one
plain-language theorem explainer
Integer cancellation identity: one minus the dimension gap plus the dimension gap equals one. Cited only as rung bookkeeping that links the defined assignments whose difference is the gap; it carries no dynamical content. The proof is a one-line omega discharge of trivial ℤ arithmetic.
Claim. Let $D=3$ be the forced spatial dimension and write $\Delta$ for the dimension gap at $D$. Then as an equality in $\mathbb{Z}$, $1 - \Delta + \Delta = 1$.
background
This module records exact arithmetic identities that relate imported Standard Model degree-of-freedom counts to combinatorial quantities built from $D=3$. After external review it was re-scoped: the identities are kernel-checked re-expressions, not derivations of the SM spectrum.
$D$ is the spatial dimension forced upstream (T8 / DimensionForcing), fixed here as the natural number 3. The dimension gap $\Delta$ is the combinatorial gap quantity at that $D$ (imported from GapDerivation); the local doc glosses the concrete bookkeeping as $(1-45)+45=1$, i.e. the defined rung pair whose difference is the gap.
The surrounding section is an interpretive 7/8 identity-tick picture (one balanced tick per eight-tick cycle). That picture is explicitly marked HYPOTHESIS: the 7/8 thermal weight itself is the imported Fermi/Bose integral, not derived from tick occupancy here.
proof idea
Pure cancellation in $\mathbb{Z}$. After casting the dimension gap to integers, the goal is $1 - \Delta + \Delta = 1$. The omega tactic closes it immediately; no lemmas about $D$, the gap formula, or physics are invoked.
why it matters
Sits in the Fermion DOF / dimension-gap bridge as pure rung bookkeeping. The doc-comment is explicit: it "proves no physical mechanism" and only links the DEFINED rung assignments (glossed as $-44$ and $45$). It does not feed any downstream theorem in the current graph (used_by is empty).
In the broader Recognition chain it touches the same $D=3$ and eight-tick ($2^D=8$) landmarks used elsewhere in the module, but only as ambient constants. The honest split in the module doc still applies: SM representations, $g_f=90$, and the 7/8 thermal weight remain imported; what is proved here is arithmetic on those counts. This lemma is the most trivial of those checks.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.