zmap_canonical_tuple_satisfies_first_principles
plain-language theorem explainer
The canonical Z-map parameters (integerization scale 6, unit ordered coefficients, edge-direction count 4) satisfy every first-principles characterization condition used in the mass layer. Mass and verification authors cite it as the converse half of the canonical-tuple equivalence. The proof is a one-line re-export of the topological-derivation converse.
Claim. The scale $k=6$ integerizes all Standard Model charges; it is the smallest positive even scale with that property; the ordered coefficient pair $(1,1)$ is a complete ordered minimizer; and the edge-direction count equals $4$. Equivalently, the canonical tuple $(6,1,1,4)$ meets the full first-principles Z-map predicate.
background
The Masses Z-Map Forcing Bridge upstreams partial O2/O3 closure into the mass-layer namespace. Two concrete facts are packaged: (i) in the parity-constrained class, $k=6$ is the smallest positive even integerization scale for SM charges; (ii) the canonical anchor charge map evaluates to the expected family values $Z_{\mathrm{lepton}}=1332$, $Z_{\mathrm{up}}=276$, $Z_{\mathrm{down}}=24$.
First-principles characterization of a Z-map tuple $(k,a,b,c)$ asks that $k$ integerize all charges, that no smaller positive even scale does so, that $(a,b)$ be a complete ordered minimizer of the budget, and that $c$ equal the geometric edge-direction count. The canonical candidate is $(6,1,1,4)$.
The detailed converse lives in Verification.ZMapTopologicalDerivation; this module only re-exports it so mass-layer consumers need not import the verification stack.
proof idea
One-line term wrapper. It applies the identically named theorem in Verification.ZMapTopologicalDerivation, whose body assembles four conjuncts: the left half of six_smallest_positive_even_integerizer (integerization at 6 and minimality among positive even scales), the complete-ordered-minimizer fact for coefficients $(1,1)$, and the equality of the edge-direction count with $4$. No local algebra is redone here.
why it matters
This is the converse leg of the canonical-tuple characterization. Downstream, canonical_tuple_iff_first_principles combines it with the forcing direction zmap_canonical_tuple_forced_from_first_principles to obtain the biconditional: a tuple satisfies the first-principles predicate if and only if it equals $(6,1,1,4)$.
In the Recognition mass formula, charges sit on the $\varphi$-ladder via a yardstick times $\varphi^{\mathrm{rung}-8+\mathrm{gap}(Z)}$. Fixing the Z-map parameters from first principles (integerization scale, unit coefficients, geometric edge count) is the bridge from ledger geometry to concrete family $Z$ values. The module header is explicit that this is not yet full first-principles closure of the mass layer, only consumable O2/O3 progress under the adopted parity constraint.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.