mapDeltaAction_step
plain-language theorem explainer
mapDeltaAction_step proves that advancing one integer step in the embedding of the δ-subgroup produces an action increment of exactly ħ under the defined mapping. Researchers building ledger-to-physical unit conversions in Recognition Science would cite it to confirm step preservation for action. The argument is a direct one-line reduction to the general affine step lemma after substituting the slope-ħ map definition.
Claim. Let nonzero integer δ, real ħ, integer n. Then the difference between the action map applied to the embedded element n+1 and to n in the subgroup generated by δ equals ħ, where the action map is the affine function of slope ħ applied after embedding k ↦ k·δ.
background
The UnitMapping module constructs mappings from the abstract subgroup generated by a fixed nonzero integer δ (using integers as placeholder) to physical quantities such as action. The embedding fromZ δ n sends integer k to the subgroup element k·δ. actionMap ħ is the affine map with slope ħ and offset zero, passed explicitly because action requires a Planck-scale constant. ħ denotes the reduced Planck constant in RS-native units (φ^{-5}·1). The lemma depends on the general step property for any affine map on this subgroup.
proof idea
The proof is a one-line term wrapper. It rewrites the left-hand side via the definitions of mapDeltaAction and actionMap, then applies the general mapDelta_step lemma instantiated at f equal to the action map of slope ħ.
why it matters
The result verifies that the action mapping yields consistent ħ increments on consecutive subgroup elements, independent of δ. It contributes to the unit-mapping layer that aligns ledger units with derived RS constants such as ħ = φ^{-5}. No downstream uses are recorded, yet the lemma closes a consistency check within the module that supports the broader forcing-chain construction of physical units.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.