smallest_positive_even_integerization_scale
plain-language theorem explainer
The natural number 6 is the smallest positive even scale that multiplies every Standard Model electric charge to an integer. Mass-layer and Z-map forcing work cite it to lock the parity-constrained integerization scale used downstream of the anchor charge map. The proof is a one-line term re-export of the topological derivation lemma that already proves both integerization at 6 and minimality among positive even scales.
Claim. The scale $k=6$ integerizes all Standard Model charges: for every charge $Q$ there is an integer $n$ with $6Q=n$. Moreover, every positive even natural number $k$ that integerizes all such charges satisfies $k\ge 6$.
background
The Masses Z-Map Forcing Bridge module lifts partial O2/O3 closure into the canonical mass-layer namespace. It records two concrete facts: the integerization-scale closure in the parity-constrained class, and the evaluation of the canonical anchor charge map to the family values $Z_{\mathrm{lepton}}=1332$, $Z_{\mathrm{up}}=276$, $Z_{\mathrm{down}}=24$.
Integerization of a scale $k$ means that for every Standard Model charge $Q$ in the fixed charge list there exists an integer $n$ with $k\cdot Q=n$ over the rationals. The upstream predicate packages exactly that universal quantification. The note on the source lemma records that $k=3$ also integerizes, but is odd; the present statement restricts to the even class adopted for the mass-layer bridge.
The local setting is therefore not full first-principles Z-map closure. It makes the currently forced even scale directly consumable from Masses.* without reopening the topological derivation.
proof idea
One-line term wrapper. The body is exactly the upstream theorem that $6$ is the smallest positive even integerization scale for SM charges, which itself splits as a constructor: the left conjunct is the direct integerization lemma at $6$, and the right conjunct is a minimality argument over positive even $k$ that integerize the charge list.
why it matters
This declaration is the mass-namespace entry point for the integerization-scale half of the Z-map forcing bridge. The module packages it so that later mass-layer arguments (canonical color offset, anchor charge map values, ordered min-budget forcing of unit coefficients, and the first-principles Z-map tuple siblings) can cite a single proved fact rather than reach back into the verification layer.
In the broader Recognition framework it fixes the discrete clearing scale that sits under the charge-to-rung side of the mass formula (yardstick times a $\phi$-ladder exponent). It does not yet finish first-principles closure of the full Z-map tuple; the module text is explicit that only partial O2/O3 progress is being upstreamed. No downstream consumers are wired yet in the graph, so its immediate role is namespace hygiene and a stable citation target for the parity-constrained scale $k=6$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.