recognitionAxisCount
plain-language theorem explainer
Assigns each compact gauge factor its recognition-axis count from the 3-cube completion: color gets 3, weak isospin 2, hypercharge phase 1. Anyone citing the cube-to-SM gauge bridge or the (3,2,1) vs Lie-rank (2,1,1) split uses this map. The body is a three-clause pattern match, not a derived proof.
Claim. The recognition-axis count is the function on compact gauge factors with $\mathrm{SU}(3)\mapsto 3$, $\mathrm{SU}(2)\mapsto 2$, and $\mathrm{U}(1)\mapsto 1$.
background
The module records the first bridge from the forced $B_3$ cube layer counts to the Standard Model compact gauge skeleton. Cube work already yields three axis permutations, a two-fold even sign-flip completion, and a one-fold parity quotient. The compact-completion rule sends those counts to color, weak isospin, and hypercharge phase respectively.
Compact gauge factors are the three-constructor type with values for $\mathrm{SU}(3)$, $\mathrm{SU}(2)$, and $\mathrm{U}(1)$. Recognition-axis count is kept separate from Lie rank: axes total $(3,2,1)$ sum to 6 (cube faces), while ranks are $(2,1,1)$ sum to 4. This file is not yet the full hypercharge or fermion-representation derivation.
proof idea
Definition by exhaustive pattern match on the three compact factors: color returns 3, weak isospin returns 2, hypercharge phase returns 1. No lemmas or tactics; the values are the cube-layer counts written as a lookup.
why it matters
This map is the numeric content of the cube-to-gauge bridge (planning item P0-S2-01). Downstream, the certificate structure packages the three equalities as part of the completion certificate; the theorems that recognition-axis counts are exactly $(3,2,1)$ and that their sum equals the 3-cube face count both reduce by deciding against this definition.
In the Recognition framework it is the clean separation between recognition axes (total 6) and Lie rank (total 4) before any deeper representation theory. It does not yet force hypercharge embeddings or fermion charges; it only pins the factor skeleton that later steps must fill.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.