chargeMap
This definition constructs the affine map from integers to reals that realizes charge quantization, sending each index n to qe times n. Researchers mapping discrete charge sectors to continuous values in mass formulas and scale constructions cite it when building delta-to-charge functions. The definition is realized by direct record construction of the affine map structure with the supplied slope and zero offset.
claimThe charge map is the affine function $nmapsto q_e n$ from $mathbb{Z}$ to $mathbb{R}$, where $q_e$ denotes the charge quantum.
background
The AffineMapZ structure encodes affine maps from integers to reals of the form $n mapsto s cdot n + o$. This module treats such maps as context constructors, with the charge constructor using quantum $q_e$ and the time constructor using $tau_0$. The module itself works with the subgroup generated by the abstract placeholder $delta$, represented via integers for mapping purposes only. Upstream, the identical structure appears in RecogSpec.Scales and the charge assignment function in AnchorPolicy matches particle names to values such as $-1$ for leptons and $pm 1/3$ for quarks.
proof idea
This is a one-line definition that constructs the AffineMapZ record with slope equal to the input $q_e$ and offset equal to zero.
why it matters in Recognition Science
The definition supplies the charge component of the unit mapping used by mapDeltaCharge to produce delta-to-charge functions and by gap to compute logarithmic gaps on the phi ladder. It fills the charge constructor role in the context for discrete-to-continuous mappings. It connects directly to the charge quantum appearing in downstream gap calculations that employ the phi-based scaling.
scope and limits
- Does not assign numerical values to the charge quantum $q_e$.
- Does not define the corresponding maps for time or action.
- Does not perform numerical evaluation or approximation of any mapped value.
- Does not incorporate particle names or sector-specific charge assignments.
Lean usage
mapDelta δ hδ (chargeMap qe)formal statement (Lean)
57def chargeMap (qe : ℝ) : AffineMapZ := { slope := qe, offset := 0 }