actionMap
The actionMap definition constructs the affine map n ↦ ħ n from ℤ to ℝ by setting slope to the supplied ħ and offset to zero. Recognition Science researchers cite it when building the action leg of the charge-time-action triad for discrete-to-continuous mappings. The definition is a direct record constructor for the AffineMapZ structure with no further computation.
claimThe affine map from $ℤ$ to $ℝ$ given by $n ↦ ħ n$, realized as the structure with slope $ħ$ and offset $0$.
background
AffineMapZ is the structure of affine maps from ℤ to ℝ of the form n ↦ slope · n + offset. The module treats δ as an abstract generator of a subgroup and uses integers solely as placeholders for the mapping. Upstream constants supply ħ = φ^{-5} in RS-native units while ledger factorization and spectral emergence structures supply the surrounding context for action as the third coordinate in the unit triad.
proof idea
The definition is a direct record constructor that instantiates AffineMapZ with the supplied hbar value as slope and zero offset. No lemmas or tactics are invoked.
why it matters in Recognition Science
This definition supplies the action component required by mapDeltaAction, mapDeltaAction_fromZ and mapDeltaAction_step inside the same module. It parallels the timeMap definition in RecogSpec.Scales and completes the charge-time-action family used for δ-step mappings. It directly implements the framework requirement that action be scaled by the native ħ = φ^{-5}.
scope and limits
- Does not derive or compute a numerical value for ħ.
- Does not extend the domain beyond integers.
- Does not impose positivity or other constraints on the slope.
- Does not perform unit conversion beyond the affine form.
Lean usage
mapDeltaAction δ hδ hbar (LedgerUnits.fromZ δ n)formal statement (Lean)
61def actionMap (hbar : ℝ) : AffineMapZ := { slope := hbar, offset := 0 }
proof body
Definition body.
62
63/-- Existence of affine δ→charge mapping (no numerics). -/