apply_chargeMap
The lemma establishes that the affine map built from charge quantum qe multiplies any integer n by qe. Workers on charge-scaled quantities in the Recognition Science mass ladder invoke it to simplify integer applications. The proof reduces immediately by the simp tactic unfolding apply and chargeMap.
claimLet $q_e$ be a real number and $n$ an integer. Then the application of the charge map with slope $q_e$ to $n$ equals $q_e$ times $n$.
background
The RecogSpec.Scales module develops binary scales and φ-exponential wrappers. chargeMap constructs an AffineMapZ whose slope is the supplied real charge quantum qe and whose offset is zero. The apply operation on such a map is the standard evaluation slope times the integer argument plus offset. Upstream chargeMap definitions in AnchorPolicy assign fixed rationals to particle names while the UnitMapping version supplies the same AffineMapZ constructor for charge and time contexts.
proof idea
The proof is a one-line simp tactic that unfolds the definitions of apply and chargeMap, reducing the goal to the arithmetic identity qe * n = qe * n.
why it matters in Recognition Science
The lemma supplies the direct computational rule for charge maps inside the scales module, allowing charge scaling to act by multiplication on integer rungs. It supports the mass formula yardstick * phi^(rung-8+gap(Z)) by making charge factors immediate. No downstream theorems are recorded, yet the declaration closes the interface between charge quanta and the binary scale constructions.
scope and limits
- Does not define chargeMap or AffineMapZ.
- Does not extend the map to non-integer arguments.
- Does not insert phi-exponential or time factors.
- Does not assign specific particle charges.
formal statement (Lean)
158@[simp] lemma apply_chargeMap (qe : ℝ) (n : ℤ) :
159 apply (chargeMap qe) n = qe * (n : ℝ) := by simp [apply, chargeMap]
proof body
160