chargeMap
The chargeMap definition maps standard model particle names to their electric charges in rational units of the elementary charge. Mass spectrum calculations cite it to supply the charge index Q for rung and gap computations on the phi-ladder. The implementation is a direct case analysis over a finite set of string labels returning -1, 2/3, -1/3 or 0.
claimThe function maps a particle label to its electric charge $q$ in units of the elementary charge, with $q=-1$ for the labels e, mu, tau; $q=2/3$ for u, c, t; $q=-1/3$ for d, s, b; and $q=0$ otherwise.
background
In the AnchorPolicy module particle masses are obtained from the phi-ladder via rung and gap functions that require a rational charge Q. The supplied chargeMap returns this Q for each named fermion. Upstream the tau definition from Anchor supplies generation torsion values (0 for gen 0, 11 for gen 1, 17 for gen 2) while the mu projector from Cost.Ndim supplies the scalar coefficient in the quadratic relation A² = μ A. The local setting therefore uses charge to compute the gap as (log(1 + (Z sector Q)/phi))/log phi where Z is the charge index.
proof idea
The definition is a direct pattern match on the input string name. It returns the fixed rational for each listed lepton or quark label and zero for every other string. No lemmas or tactics are applied; the body is a pure enumeration.
why it matters in Recognition Science
This definition supplies the charge argument to the gap function in the same module, which feeds the mass formula yardstick * phi^(rung - 8 + gap(Z)). It is used downstream by apply_chargeMap in RecogSpec.Scales and by mapDeltaCharge in UnitMapping. The construction is consistent with the Recognition Science mass ladder and the eight-tick octave (T7) that fixes D = 3 spatial dimensions.
scope and limits
- Does not assign charges to non-standard-model particles.
- Does not incorporate color or weak isospin charges.
- Does not distinguish particles from antiparticles.
- Does not accept generation or sector as explicit inputs.
Lean usage
noncomputable def exampleGap := gap .lepton (chargeMap := chargeMap) (name := 'e')formal statement (Lean)
17noncomputable def chargeMap (name : String) : ℚ :=
proof body
Definition body.
18 match name with
19 | "e" | "mu" | "tau" => -1
20 | "u" | "c" | "t" => 2 / 3
21 | "d" | "s" | "b" => -1 / 3
22 | _ => 0
23