canonicalLoopExcitation
plain-language theorem explainer
Maps the three fermion generations to cumulative independent Q₃ loop-layer counts 0, 1, 2. Anyone proving the unique minimal one-new-loop-per-generation excitation cites this profile. It is a pure pattern-match definition: ground state excites nothing; each later generation adds exactly one loop layer, exhausting the three-loop budget at generation three.
Claim. The canonical loop-excitation profile assigns to each charged generation a natural number: generation 1 maps to $0$, generation 2 to $1$, and generation 3 to $2$. Equivalently, it is the cumulative count of independent $Q_3$ loop layers excited by that generation under the minimal one-new-layer-per-step rule.
background
The module Generation Torsion Bridge is the geometric source of truth for charged-generation torsion ${0, 11, 17}$. Those integers come from $D=3$ cube combinatorics: ground state has no geometric coupling; the second generation is edge-dressed by the passive-edge count $E_{\mathrm{passive}}(3)=11$; the third is face+edge-dressed by $W_{\mathrm{endo}}(3)=11+6=17$. The module certifies that this schedule agrees with every other torsion representation in the codebase and is the unique solution of an explicit structural predicate CubeAdmissibleTorsion.
Independent of the torsion integers themselves, the module also tracks how generations couple to independent loop layers of the 3-cube $Q_3$. The three-loop budget of $Q_3$ is the natural ceiling: at most three independent loops can be excited. The present definition records the cumulative excitation count under the minimal-step rule (ground: none; each later generation activates exactly one new independent loop layer).
Generation is the three-valued type of charged fermion generations used throughout the mass and ledger layers. Downstream, a structure MinimalLoopExcitation packages the four axioms that a profile $\ell:\mathrm{Generation}\to\mathbb{N}$ must satisfy to be a minimal one-new-loop-per-step excitation.
proof idea
No proof: this is a definition by cases on the three constructors of Generation. First generation returns $0$, second returns $1$, third returns $2$. The mathematical content is the assignment itself; all theorems about it are proved elsewhere by rfl against these three clauses.
why it matters
This profile is the witness for the unique minimal loop-excitation schedule on three generations. Downstream, canonicalLoopExcitation_minimal shows it satisfies the four MinimalLoopExcitation axioms (ground level zero, second and third each add one, third exhausts the cube's three-loop budget). minimalLoopExcitation_unique then proves any other profile obeying those axioms equals this one by cases on generation. Together they yield one_new_independent_loop_per_generation_step: there exists a unique minimal loop-excitation profile.
In the broader Recognition framework this sits under the $D=3$ forcing (T8) and the eight-tick / $Q_3$ geometry that organises generation structure. It does not itself derive the torsion integers ${0,11,17}$; those come from cube edge/face counts. It does supply the discrete excitation ladder that justifies treating generations as successive independent loop activations rather than arbitrary labels. The remaining open premise of the module (the structural coupling rule ground / passive-edge / face+edge, not yet forced from the RCL alone) is orthogonal: this definition only fixes the loop-count side of that story.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.