mapDelta_fromZ
plain-language theorem explainer
The lemma shows that mapDelta applied to the integer embedding LedgerUnits.fromZ(δ, n) recovers the affine evaluation slope · n + offset. Researchers specializing unit mappings for charge, time, and action in Recognition Science cite this when reducing subgroup projections to explicit linear forms. The proof is a one-line simplification that unfolds mapDelta and invokes the inversion lemma toZ_fromZ.
Claim. Let δ ∈ ℤ with δ ≠ 0, let f be the affine map ℤ → ℝ given by n ↦ s · n + o, and let n ∈ ℤ. Then mapDelta(δ, f, fromZ(δ, n)) = s · n + o, where fromZ embeds n into the δ-subgroup and mapDelta composes f with the projection of the subgroup element back to ℤ.
background
The UnitMapping module treats the subgroup generated by a fixed nonzero integer δ as an abstract placeholder for unit mappings. AffineMapZ is the structure with fields slope : ℝ and offset : ℝ, so that the associated map is n ↦ slope · n + offset. The function mapDelta, defined in RecogSpec.Scales, takes a projection toZ from the δ-subgroup to ℤ together with an AffineMapZ and returns the corresponding real-valued map on the subgroup.
proof idea
The proof is a one-line wrapper. It opens with the classical tactic, then applies simp using the definition of mapDelta together with the lemma toZ_fromZ(δ, hδ). This substitutes the projection result n directly into the affine expression.
why it matters
This lemma supplies the explicit evaluation rule used by the downstream lemmas mapDeltaTime_fromZ and mapDeltaAction_fromZ, which specialize the same pattern to the time and action maps. It completes the concrete computation layer that converts integer indices on the δ-subgroup into the real-valued physical quantities (τ0, ħ) without requiring the full phi-ladder at this stage.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.