mapDeltaAction
plain-language theorem explainer
mapDeltaAction defines the affine map from the δ-generated subgroup to real action values by composing the generic delta mapper with actionMap at a supplied ħ. Researchers establishing discrete action increments in Recognition Science unit conversions cite it when scaling integer steps. The definition is a direct composition inheriting affine structure from mapDelta.
Claim. Define the function $f : Δ_δ → ℝ$ by $f(x) := mapDelta(δ, h_δ, actionMap(ħ))(x)$, where $Δ_δ$ is the subgroup of ℤ generated by nonzero integer $δ$.
background
In UnitMapping, DeltaSub δ is defined as ℤ and serves as an abstract placeholder for the subgroup generated by δ. The generic mapDelta is supplied by RecogSpec.Scales while actionMap is a sibling definition providing the target scaling. Upstream, ħ appears in Constants as the RS-native value ħ = E_coh · τ₀ = φ^{-5} · 1, with parallel CODATA definitions in other modules.
proof idea
This definition is a one-line wrapper that applies mapDelta to the actionMap function at the supplied ħ parameter.
why it matters
It is invoked by the lemmas mapDeltaAction_fromZ and mapDeltaAction_step, which establish that the map sends fromZ δ n to ħ · n and has constant differences of ħ. This supplies the action-specific case of delta mapping, supporting consistent units in the Recognition framework where ħ = φ^{-5} in native units.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.