mapDeltaCharge
plain-language theorem explainer
The definition constructs an affine map from the integer subgroup generated by nonzero δ to real-valued charges by composing the general delta mapper with the charge assignment at energy scale qe. Researchers handling abstract unit conversions for charges in Recognition Science models would cite it when treating delta subgroups as placeholders for physical mappings. The implementation is a direct one-line composition of mapDelta and chargeMap with no added computation.
Claim. Let $Δ_δ$ denote the subgroup generated by nonzero integer $δ$. For energy scale $q_e$, the charge map is the function $Δ_δ → ℝ$ obtained by applying the affine $δ$-mapping to the charge assignment function at $q_e$.
background
In the UnitMapping module the local setting treats DeltaSub δ as the abstract subgroup generated by δ, implemented simply as ℤ to serve as a placeholder for mapping purposes only. Sibling definitions supply the general mapDelta together with chargeMap from anchor policies, allowing charge to be handled uniformly with time and action mappings.
proof idea
One-line wrapper that applies mapDelta δ hδ to the output of chargeMap qe.
why it matters
The definition supplies the charge-specific case inside the unit-mapping layer that supports ledger factorizations and mass-to-light derivations. It connects to upstream structures on J-cost minimization and spectral emergence while remaining free of numerics, consistent with the abstract delta-subgroup convention.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.