mapDeltaCharge
The declaration defines an affine mapping from the integer subgroup generated by nonzero δ to real-valued charges. Researchers building abstract unit systems in Recognition Science cite it when assigning charges to delta-subgroups without numerical evaluation. It is realized as a one-line wrapper composing the general mapDelta with chargeMap at the supplied qe.
claimThe function maps elements of the subgroup generated by nonzero integer δ to real numbers via the affine charge map at scale q_e, yielding mapDeltaCharge(δ, h_δ, q_e) : Δ_δ → ℝ.
background
In the UnitMapping module, DeltaSub δ is defined as the integers ℤ and functions as an abstract placeholder for the subgroup generated by a nonzero integer δ. This setup permits defining mappings for physical quantities while remaining independent of concrete scales. The sibling chargeMap supplies the electric-charge scaling factor qe drawn from the anchor policy.
proof idea
The definition is a one-line wrapper that applies mapDelta δ hδ to the output of chargeMap qe.
why it matters in Recognition Science
This definition completes the charge leg of the affine unit-mapping family inside the Recognition framework, sitting alongside the timeMap and actionMap siblings. It supports the abstract subgroup approach required for consistent ledger factorization and phi-forcing derivations without committing to numerical constants. No downstream uses are recorded, leaving its role as a modular building block for later unit constructions.
scope and limits
- Does not compute or fix any numerical value for qe or the resulting charges.
- Does not extend the mapping beyond the abstract integer subgroup Δ_δ.
- Does not impose or verify any physical units or dimensions on the output.
formal statement (Lean)
64noncomputable def mapDeltaCharge (δ : ℤ) (hδ : δ ≠ 0) (qe : ℝ) : DeltaSub δ → ℝ :=
proof body
Definition body.
65 mapDelta δ hδ (chargeMap qe)
66
67/-- Existence of affine δ→time mapping via τ0. -/