minimalLoopExcitation_unique
plain-language theorem explainer
Any generation-indexed natural-number profile that starts at ground level zero and adds exactly one independent Q₃ loop layer per generation step equals the canonical schedule (0,1,2). Mass and torsion derivations that need a unique minimal excitation ladder cite this. The proof is pointwise case analysis on the three generations, chaining the additive step axioms down to the ground axiom.
Claim. Let $\ell$ assign a natural number to each of the three fermion generations. If $\ell$ is a minimal loop excitation (ground generation at level $0$, each later generation activates exactly one new independent loop layer, and the third generation exhausts the independent-loop budget of the $3$-cube), then $\ell$ equals the canonical profile sending first, second, third generation to $0$, $1$, $2$ respectively.
background
The Generation Torsion Bridge module is the authoritative geometric derivation of charged-generation torsion ${0,11,17}$ from $Q_3$ cube combinatorics. Gen 1 is ground ($\tau=0$), Gen 2 is passive-edge dressed ($E_{\mathrm{passive}}(3)=11$), Gen 3 is face+edge dressed ($W_{\mathrm{endo}}(3)=17$). The module certifies agreement with Anchor and RecogSpec representations and upgrades hardcoded numerals to an explicit structural premise with uniqueness.
A generation is one of three modes (first, second, third) from parity patterns across dimensions. The canonical loop-excitation profile counts cumulative independent $Q_3$ loop-layers excited by each generation: $0$, $1$, $2$. The predicate MinimalLoopExcitation packages the structural rule: ground level zero, each step adds one layer, and the third generation plus one equals the independent-loop count of the $3$-cube.
That coupling rule (ground / passive-edge / face+edge) remains a structural premise about how fermion generations meet cube features, not yet a pure consequence of the Recognition Composition Law. Uniqueness under the premise is what this theorem supplies.
proof idea
Apply function extensionality on the generation argument, then case-split on the three constructors.
- First generation: immediate from the ground-level field of the hypothesis.
- Second: rewrite $\ell(\mathrm{second})=\ell(\mathrm{first})+1$ by the second-adds-one field, substitute ground level $0$, and simplify against the canonical definition.
- Third: chain third-adds-one, then second-adds-one, then ground level, obtaining $(0+1)+1$, and match the canonical value $2$ by simplification.
No external lemmas beyond the structure fields and the definition of the canonical profile are required; the unused exhausts-cube-loops field is not needed for equality to the canonical map.
why it matters
This is the uniqueness half of the existence-uniqueness package for minimal loop excitation. The immediate parent is one_new_independent_loop_per_generation_step, which packages $\exists!$ by exhibiting the canonical profile as a witness and invoking this theorem for uniqueness.
In the broader bridge, the loop-layer schedule is the combinatorial skeleton behind generation torsion: one new independent loop per generation step on $Q_3$ aligns with the edge-before-face CW filtration and with the geometric torsion values forced by cube arithmetic (T8 forces $D=3$). The module still treats the ground/edge/face coupling assignment as a structural premise rather than an RCL consequence; uniqueness under that premise closes the "hardcoded numerals" gap for the excitation ladder itself.
Downstream mass and torsion work that needs a single admissible loop-count profile on three generations lands here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.