canonical_tuple_iff_first_principles
plain-language theorem explainer
The bundled first-principles constraints on the Z-map integerization scale and charge coefficients force the unique canonical tuple $(k,a,b,c)=(6,1,1,4)$. Mass-layer workers cite this to pin the Z-map lane without entering the verification module. The proof is a one-line re-export of the topological-derivation characterization.
Claim. For $k\in\mathbb{N}$ and $a,b,c\in\mathbb{Z}$, the bundled first-principles Z-map predicate on $(k,a,b,c)$ holds if and only if $k=6$, $a=1$, $b=1$, and $c=4$.
background
In the mass layer, Standard Model charges are integerized by a positive even scale $k$ together with integer coefficients $(a,b,c)$ that define the Z-map. The module packages partial O2/O3 forcing into the mass namespace: $k=6$ is the smallest positive even scale that integerizes SM charges, and the canonical anchor map yields $Z_{\mathrm{lepton}}=1332$, $Z_{\mathrm{up}}=276$, $Z_{\mathrm{down}}=24$.
The bundled first-principles predicate packages positivity and evenness of $k$, full integerization of SM charges, minimality of $k$ among such scales, the complete ordered-minimizer condition on $(a,b)$, and a residual constraint on $c$. That predicate is defined in the Z-map topological derivation module and re-exported here for mass-layer use. The present statement is the corresponding iff characterization: the bundle holds exactly on the canonical tuple.
proof idea
One-line term wrapper that applies the matching characterization already proved in the Z-map topological derivation module. Upstream, the biconditional is proved by constructor. The forward direction unpacks positivity, evenness, integerization, scale-minimality, ordered-minimizer on $(a,b)$, and the residual $c$-constraint, then invokes the forcing lemma that those conjuncts imply $(k,a,b,c)=(6,1,1,4)$. The reverse direction checks that the canonical values satisfy the bundle.
why it matters
Places the unique forced Z-map tuple into the mass-layer namespace so mass formulas can cite a local name rather than the verification path. The same characterization is the reference point inside the topological derivation module. It closes the integerization-scale and coefficient-forcing half of the O2/O3 program described in the module doc: not full first-principles mass closure yet, but the scale $k=6$ and coefficients $(1,1,4)$ are now pinned for consumers of the phi-ladder mass formula (yardstick times $\varphi^{\mathrm{rung}-8+\mathrm{gap}(Z)}$). The result is mass-lane infrastructure rather than a step of the T0–T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.