actionMap
plain-language theorem explainer
actionMap supplies the affine map from integers to reals whose slope is the supplied reduced Planck constant ħ and whose offset is zero. It is invoked by mapDeltaAction and the time/charge siblings inside UnitMapping and RecogSpec.Scales to convert discrete deltas into physical increments. The definition is a direct record construction of the AffineMapZ structure.
Claim. The affine map $f:ℤ→ℝ$ defined by $f(n)=ℏ⋅n$.
background
AffineMapZ is the structure recording an affine map from ℤ to ℝ of the form n ↦ slope·n + offset. The UnitMapping module treats δ-generated subgroups as abstract integer placeholders for unit conversions among charge, time and action. Upstream, hbar is supplied either as the RS-native value φ^{-5} (Constants.hbar) or the CODATA numerical constant; the same module also imports LedgerFactorization and PhiForcingDerived structures that calibrate the underlying J-cost.
proof idea
One-line definition that directly constructs the AffineMapZ record with the parameter hbar as slope and literal zero as offset.
why it matters
Completes the action leg of the three affine maps (chargeMap, timeMap, actionMap) required by mapDeltaAction and its specializations mapDeltaAction_fromZ and mapDeltaAction_step. These feed the scale lemmas apply_timeMap and mapDeltaTime_fromZ_one in RecogSpec.Scales. The construction encodes the Recognition Science convention that action increments are measured in units of ħ = φ^{-5} while remaining agnostic about the forcing chain that produces that value.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.