mapDeltaAction
The definition constructs an affine map sending elements of the subgroup generated by nonzero integer δ to real numbers via scaling by the supplied ħ parameter. Researchers building discrete-to-continuous maps in Recognition Science unit systems cite it when embedding integer steps into action quantities. It is realized as a direct one-line composition of the generic mapDelta operator with the actionMap function.
claimFor nonzero integer $δ$, the map $ΔSub(δ) → ℝ$ is given by $Δ ↦ ħ · k$ where $k ∈ ℤ$ is the integer coefficient of $Δ$ in the subgroup generated by $δ$.
background
DeltaSub δ is the subgroup of ℤ generated by δ, implemented here as the full ℤ to serve as an abstract placeholder for mapping. The ħ parameter is supplied explicitly and drawn from Constants as the RS-native reduced Planck constant ħ = φ^{-5}. The UnitMapping module supplies affine maps for discrete steps and depends on the generic mapDelta from RecogSpec.Scales together with the local actionMap definition.
proof idea
The definition is a one-line wrapper that applies mapDelta δ hδ to the function actionMap hbar.
why it matters in Recognition Science
This supplies the concrete ħ-dependent action map used by the downstream lemmas mapDeltaAction_fromZ and mapDeltaAction_step, which establish the scaling mapDeltaAction δ hδ hbar (fromZ δ n) = ħ · n and the unit step difference of ħ. It fills the explicit mapping role in the unit-mapping layer, connecting discrete subgroups to action quantities consistent with ħ = φ^{-5} in the Recognition framework.
scope and limits
- Does not define or expand the actionMap function.
- Does not handle the case δ = 0.
- Does not perform numerical evaluation or connect to J-cost.
- Does not reference the forcing chain T0-T8 or RCL.
formal statement (Lean)
72noncomputable def mapDeltaAction (δ : ℤ) (hδ : δ ≠ 0) (hbar : ℝ) : DeltaSub δ → ℝ :=
proof body
Definition body.
73 mapDelta δ hδ (actionMap hbar)
74