actionMap
plain-language theorem explainer
actionMap constructs an affine map from the integer subgroup to reals whose slope is the supplied reduced Planck constant ħ and whose offset is zero. Researchers assembling discrete action increments within the Recognition Science unit system cite it to complete the charge-time-action triad. The definition is realized by a direct record construction of AffineMapZ.
Claim. The action map is the affine function $nmapsto hbarcdot n$ from $mathbb{Z}$ to $mathbb{R}$, obtained by setting slope to the reduced Planck constant and offset to zero.
background
The UnitMapping module abstracts mappings over the subgroup generated by δ using integer placeholders for δ increments. AffineMapZ is the structure that records an affine function from ℤ to ℝ via its slope and offset fields. The action mapping requires an explicit Planck-like constant passed as the hbar parameter, consistent with the RS-native value ħ = φ^{-5}. Upstream results include the hbar definition in Constants as cLagLock * tau0 together with LedgerFactorization and SpectralEmergence structures that supply the discrete ledger context.
proof idea
This is a one-line definition that directly constructs the AffineMapZ record, assigning the input hbar to the slope field and zero to the offset field.
why it matters
This definition supplies the action scaling used by mapDeltaAction, mapDeltaAction_fromZ and mapDeltaAction_step inside UnitMapping, which feed the timeMap and chargeMap family in RecogSpec.Scales. It completes the unit-mapping triad required for the Recognition Composition Law and the eight-tick octave. It touches the open question of embedding the phi-ladder constants into the discrete δ increments.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.