mapDeltaCharge
plain-language theorem explainer
Defines the charge component of affine mappings from the subgroup generated by a nonzero integer δ to the reals by direct composition. Model builders constructing delta-based unit systems in Recognition Science cite this when assigning charges without numerical evaluation. The definition is realized as a one-line wrapper around mapDelta applied to chargeMap.
Claim. Let $h_δ$ witness that the integer $δ$ is nonzero and let $q_e ∈ ℝ$. The map $mapDeltaCharge(δ, h_δ, q_e)$ sends elements of the subgroup generated by $δ$ to $ℝ$ by composing the general affine map $mapDelta(δ, h_δ)$ with the charge assignment $chargeMap(q_e)$.
background
DeltaSub δ is the subgroup generated by δ, realized abstractly as ℤ solely to support mapping constructions. The UnitMapping module supplies such abstract placeholders for δ-to-charge, δ-to-time, and δ-to-action maps without committing to concrete numerics, per the module documentation. Upstream structures supply the physical contexts: NucleosynthesisTiers.of organizes nuclear densities on φ-tiers, MassToLight.via encodes recognition-weighted stellar assembly, LedgerFactorization.of calibrates the J-cost on the positive reals, and PhiForcingDerived.of encodes the J-cost itself.
proof idea
One-line wrapper that applies mapDelta δ hδ to the output of chargeMap qe.
why it matters
Supplies the charge leg of the abstract δ-mappings required by the unit-mapping layer. It completes the existence claim for affine charge maps stated in the declaration comment and aligns with the Recognition Science emphasis on J-cost and φ-ladder structures appearing in the upstream results. No downstream uses are recorded, leaving its integration into larger derivations open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.