mapDelta
mapDelta sends each element of the δ-generated integer subgroup to a real by applying an affine map after extracting the integer coefficient via toZ. Researchers constructing charge, time, and action maps in the Recognition Science ledger cite it to embed abstract subgroups into physical units. The definition is a direct one-line functional composition that multiplies the projected integer by the slope and adds the offset.
claimFor nonzero integer $δ$ and affine map $f$ with slope $m$ and offset $b$, the function maps each $p$ in the subgroup generated by $δ$ to $m · k + b$, where $k ∈ ℤ$ satisfies $p = k · δ$ and is recovered by the projection toZ.
background
DeltaSub δ is the set of all integers that are integer multiples of δ. The projection toZ extracts the unique coefficient k such that the input equals k · δ, using classical choice. AffineMapZ is the structure consisting of a real slope and real offset that defines the linear map n ↦ slope · n + offset on integers.
proof idea
The definition is a direct lambda that applies the affine map to the integer projection: for input p it returns f.slope multiplied by the cast of (LedgerUnits.toZ δ p) to reals, then adds f.offset. No lemmas are invoked; it is a straightforward functional definition relying on the upstream toZ projection.
why it matters in Recognition Science
This supplies the uniform mapping operation used by mapDeltaCharge, mapDeltaAction, and mapDelta_diff in the same module, and by apply_timeMap in RecogSpec.Scales. It realizes the affine embedding of δ-subgroups into real-valued physical quantities (charge qe, time τ0, action ħ) that the Recognition framework requires for its unit system.
scope and limits
- Does not assign concrete numerical values to slope or offset.
- Does not handle the case δ = 0.
- Does not supply an inverse map from reals back to the subgroup.
- Does not invoke Recognition Science constants or the J-function.
Lean usage
example (δ : ℤ) (hδ : δ ≠ 0) (f : AffineMapZ) (p : DeltaSub δ) : ℝ := mapDelta δ hδ f pformal statement (Lean)
31noncomputable def mapDelta (δ : ℤ) (hδ : δ ≠ 0) (f : AffineMapZ) : DeltaSub δ → ℝ :=
proof body
Definition body.
32 fun p => f.slope * ((LedgerUnits.toZ δ p) : ℝ) + f.offset
33