chargeMap
plain-language theorem explainer
The charge assignment definition supplies rational electric charges for standard model fermions by string label. Mass gap calculations in the AnchorPolicy module invoke it to adjust the phi-ladder exponent for each particle. The implementation consists of a direct case split on the input string with no auxiliary lemmas.
Claim. The function that returns the electric charge in units of the elementary charge: leptons receive $-1$, up-type quarks receive $2/3$, down-type quarks receive $-1/3$, and all other labels receive $0$.
background
Within the AnchorPolicy module, mass predictions are built on a phi-ladder whose effective rung incorporates a gap correction that depends on the particle's electric charge. The gap term is computed from the charge value together with the sector index and the constant phi. Upstream results supply the generation torsion tau from the Anchor module and the scalar coefficient mu from the Ndim projector; sibling definitions such as rung and predict_mass then consume the charge value to produce numerical mass estimates.
proof idea
The definition is realized by exhaustive pattern matching on the string argument. It returns the conventional charge for each named lepton or quark family and defaults to zero for any unrecognized label. No tactics or lemmas are applied.
why it matters
This definition supplies the charge input required by the gap function, which adjusts the exponent in the mass formula yardstick times phi to the power of (rung minus 8 plus gap). It thereby connects the standard model charge assignments to the Recognition Science mass ladder and to downstream affine mappings in RecogSpec.Scales and UnitMapping. The placement supports the overall derivation of particle masses from the phi-ladder and the eight-tick octave structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.