chargeMap
plain-language theorem explainer
The charge quantum map defines an affine transformation from integers to reals with slope given by the quantum and zero offset. Mass gap routines and delta mappings cite this constructor when assembling charge-dependent transformations. It arises from direct record construction of the affine map structure.
Claim. The charge quantum map with value $q_e$ is the affine map $nmapsto q_e cdot n$ from $mathbb{Z}$ to $mathbb{R}$.
background
UnitMapping builds maps from the integer subgroup generated by delta (treated as an abstract placeholder) onto physical quantities. The affine map structure consists of a slope field and an offset field, encoding the linear map n mapsto slope cdot n + offset. This definition supplies the charge leg using the supplied quantum qe. The identical pattern appears upstream in the Scales module for charge, time, and action constructors.
proof idea
Direct structure constructor for the affine map structure. Slope receives the input qe and offset receives zero. No lemmas or tactics are applied.
why it matters
Downstream code invokes it inside mapDeltaCharge to produce delta-to-charge functions and inside the gap definition to compute logarithmic mass gaps from charge indices. It supplies the charge context constructor in the unit mapping layer that supports the Recognition Science mass formula on the phi ladder. No open questions are resolved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.