first_principles_zmap_tuple
plain-language theorem explainer
Bundled predicate on a scale k and integer coefficients (a,b,c) that packages the first-principles constraints for the Z-map charge tuple: positive even integerization scale, minimality among such scales, and ordered-minimizer conditions on the coefficients. Mass-layer and verification code cite it as the single Prop standing for those constraints. The body is a one-line re-export of the verification-lane definition.
Claim. For $k \in \mathbb{N}$ and $a,b,c \in \mathbb{Z}$, the first-principles Z-map tuple predicate holds when $k>0$, $k$ is even, $k$ integerizes all Standard Model charges, $k$ is minimal among positive even integerizing scales, and $(a,b)$ (with the remaining coefficient constraint on $c$) form a complete ordered minimizer of the charge budget.
background
The Masses Z-Map Forcing bridge re-exports partial O2/O3 closure into the mass-layer namespace. Two concrete facts sit behind it: $k=6$ is the smallest positive even scale that integerizes SM charges, and the canonical anchor charge map evaluates to $Z_{\mathrm{lepton}}=1332$, $Z_{\mathrm{up}}=276$, $Z_{\mathrm{down}}=24$. Full first-principles closure is not claimed yet; the module only makes current forcing progress consumable from Masses.*.
The upstream verification definition bundles those constraints into one Prop on $(k,a,b,c)$: positivity and evenness of $k$, the integerization predicate, minimality of $k$ in that class, and the complete ordered-minimizer condition on the coefficient pair (with the remaining slot for $c$). Sibling facts in this module already force unit coefficients under ordered min-budget hypotheses and record the anchor charge values.
Downstream, the same predicate is the left-hand side of the iff that pins the unique canonical tuple $(k,a,b,c)=(6,1,1,4)$.
proof idea
One-line definitional wrapper. The body is pure abbreviation: it names the verification-lane predicate Verification.ZMapTopologicalDerivation.first_principles_zmap_tuple on the same arguments $(k,a,b,c)$. No tactics, no local lemmas, no new proof obligations.
why it matters
Gives the mass layer a stable name for the bundled first-principles Z-map constraints without forcing every consumer to import the verification derivation module. The immediate parent is the upstreamed iff theorem canonical_tuple_iff_first_principles, which states that the predicate holds exactly when $(k,a,b,c)=(6,1,1,4)$. The same iff lives in the verification module and is the forcing statement that closes the canonical tuple.
In the broader Recognition picture this sits on the mass side of the phi-ladder: the integerization scale and unit coefficients feed the yardstick times $\varphi^{\mathrm{rung}-8+\mathrm{gap}(Z)}$ mass formula once anchor charges are fixed. The module doc is explicit that this is partial O2/O3 progress, not full first-principles closure of the Z-map lane.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.