cubeGeoTorsion_first
plain-language theorem explainer
The first charged fermion generation is assigned geometric torsion zero by the Q₃ cube schedule. Mass and generation-bridge arguments cite this as the ground-state base case of the torsion triple {0,11,17}. The proof is pure definitional reflexivity on the first branch of the cube-combinatorial torsion map.
Claim. Under the cube-geometric torsion assignment on charged generations, the first generation has torsion equal to $0$.
background
The module fixes charged-generation torsion from $D=3$ cube combinatorics alone, with no raw integer literals in the definition. Generations are ordered ground / edge-dressed / face+edge-dressed. The schedule is $\tau_1=0$, $\tau_2=E_{\mathrm{passive}}(D)$ (cube edges minus one), $\tau_3=W_{\mathrm{endo}}(D)=E_{\mathrm{passive}}+F$ (passive edges plus faces), which at $D=3$ yields ${0,11,17}$.
Upstream, cube-geometric torsion is the map sending the first generation to $0$, the second to the integer of passive field edges at $D$, and the third to the endogenous winding $W_{\mathrm{endo}}(D)$. Its doc-comment stresses that every branch is a cube-combinatorial function of $D$.
This sits inside the broader Recognition mass ladder and generation story: $D=3$ is forced (T8), and the eight-tick octave (T7) supplies the discrete timing against which generation structure is read. The remaining premise is the structural coupling rule (which cube features dress which generation), not yet derived from the Recognition Composition Law alone.
proof idea
One-line definitional proof. The cube-geometric torsion map is defined by pattern-match with first-generation branch equal to $0$; rfl closes the equality. The lemma is marked @[simp] so downstream rewrites discharge the ground case automatically.
why it matters
This is the ground vertex of the geometric source-of-truth for charged-generation torsion. The module's job is to replace hardcoded numerals ${0,11,17}$ by cube arithmetic and then match every other codebase representation (anchor integers, RecogSpec generation torsion, and the CubeAdmissibleTorsion uniqueness predicate).
No downstream dependents are recorded for this particular simp lemma, but the sibling equalities (second and third generation values, pointwise match to $\tau$ and to generationTorsion) rest on the same definition; the first-generation case is the trivial base of that bridge.
Framework landmarks: T8 forces $D=3$, so the edge and face counts that feed the second and third branches are fixed; the first branch remains the undressed ground state with torsion zero. The open gap the module records is that the ground/passive-edge/face+edge assignment rule is still a structural premise until a derivation from the RCL or the CW-filtration route in ExcitationOrdering closes it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.