anchor_charge_map_values
plain-language theorem explainer
The canonical charge-index map on the three charged Standard Model families evaluates to the fixed integers Z(lepton, −1) = 1332, Z(up, 2/3) = 276, and Z(down, −1/3) = 24. Mass-layer forcing arguments cite this as the concrete anchor output triple. The proof is a pure native decision procedure on the closed-form charge map.
Claim. The canonical mass-layer charge index satisfies $Z_{\mathrm{lepton}}(-1)=1332$, $Z_{\mathrm{up}}(2/3)=276$, and $Z_{\mathrm{down}}(-1/3)=24$.
background
The module packages partial O2/O3 closure into the mass-layer namespace. Two concrete facts are exposed: the smallest positive even integerization scale that integerizes SM charges is $k=6$ (parity-constrained class), and the canonical anchor charge map hits the family values $Z_{\mathrm{lepton}}=1332$, $Z_{\mathrm{up}}=276$, $Z_{\mathrm{down}}=24$.
Charge indices here are the integerized outputs of the topology-compatible family forms used downstream: leptons as $a\tilde{Q}^2+b\tilde{Q}^4$ and quarks as $c+a\tilde{Q}^2+b\tilde{Q}^4$, evaluated on the SM charges $-1$, $2/3$, and $-1/3$ in the lepton, up-quark, and down-quark sectors. The result is not yet full first-principles closure; it makes the current forcing progress consumable from Masses.*.
Upstream scaffolding includes the RS-native mass type and various canonical arithmetic/trace objects; none of those lemmas are invoked in the proof body, which is purely computational.
proof idea
One-line term proof by native_decide. Lean evaluates the closed-form charge-index definition on the three concrete sector/charge pairs and checks equality with the integer literals 1332, 276, and 24. No algebraic lemmas are applied.
why it matters
This is the second packaged fact of the Z-map forcing bridge. Its sole direct consumer is canonical_tuple_forced_from_anchor_outputs: if a topology-compatible family matches these three anchor outputs, then the coefficient triple is forced to $(a,b,c)=(1,1,4)$.
That bridge sits on the path toward zmap_canonical_tuple_forced_from_first_principles and the iff with first-principles satisfaction. In the broader RS mass story, these integers are the yardstick inputs that feed the phi-ladder mass formula (rung and gap structure). The module itself flags that full first-principles closure remains open; this theorem only freezes the numerical anchor side so coefficient forcing can proceed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.