mapDeltaAction
plain-language theorem explainer
The definition supplies an affine map from the integer subgroup generated by nonzero δ to the reals, parameterized by an explicit ħ to scale actions. Researchers constructing discrete unit mappings in Recognition Science reference it when building consistent action increments across steps. It is realized as a direct composition of the general delta mapping with the action map function.
Claim. Let $Δ_δ$ be the subgroup of integers generated by nonzero $δ ∈ ℤ$. The map $Δ_δ → ℝ$ is obtained by composing the delta-subgroup mapping operator with the action map scaled by $ℏ$, producing an affine function whose increments equal $ℏ$ per generator step.
background
In this module DeltaSub δ is introduced as the set of integers ℤ, serving as an abstract placeholder for the subgroup generated by δ. This choice keeps the interface lightweight for affine mappings and avoids the explicit multiple structure {x : ℤ // ∃ n, x = n·δ} used in LedgerUnits and RecogSpec.Scales. The action map is instantiated with the supplied ħ, which enters as the scaling factor for actions.
proof idea
The definition is a one-line wrapper that applies the mapDelta operator to the actionMap function instantiated with the supplied ħ value.
why it matters
This definition supports the lemmas mapDeltaAction_fromZ and mapDeltaAction_step that establish evaluation at generators and unit increments of ħ. It fills the affine δ-to-action slot in the unit-mapping layer, consistent with the Recognition Science treatment of ħ as φ^{-5} and the need for explicit parameter passing when scaling physical quantities across different δ steps.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.