mapDeltaAction_step
The mapDeltaAction_step lemma shows that the action map increments by exactly ħ when the index in the δ-generated subgroup advances by one. Researchers constructing discrete unit mappings for action in Recognition Science would cite this for step consistency. The proof is a one-line wrapper that substitutes actionMap hbar into the general mapDelta_step lemma and simplifies the definitions.
claimLet $A$ be the affine map with slope $ħ$ applied to the subgroup generated by nonzero integer $δ$. Then $A(δ·(n+1)) - A(δ·n) = ħ$ for any integer $n$.
background
The UnitMapping module treats the subgroup generated by a fixed nonzero integer δ as an abstract integer lattice for defining mappings. The function fromZ δ n embeds the integer n into this subgroup as the element n·δ. The actionMap hbar is the affine map with slope ħ and zero offset, where ħ comes from Constants as φ^{-5} in RS-native units.
proof idea
The proof is a one-line wrapper that applies mapDelta_step with f set to actionMap hbar and then uses simpa on the definitions of mapDeltaAction and actionMap.
why it matters in Recognition Science
This lemma guarantees that the action map respects the discrete steps of the δ-subgroup, supplying the increment property needed for quantized action in the Recognition framework. It builds directly on the general mapDelta_step result and the affine actionMap definition, supporting later constructions of charge and time maps in the same module.
scope and limits
- Does not compute numerical values of action or ħ.
- Does not specify the physical scale or origin of δ.
- Does not extend the mapping beyond the integer lattice generated by δ.
- Does not address continuous or non-discrete limits.
formal statement (Lean)
116lemma mapDeltaAction_step (δ : ℤ) (hδ : δ ≠ 0)
117 (hbar : ℝ) (n : ℤ) :
118 mapDeltaAction δ hδ hbar (LedgerUnits.fromZ δ (n+1)) - mapDeltaAction δ hδ hbar (LedgerUnits.fromZ δ n)
119 = hbar := by
proof body
Term-mode proof.
120 simpa [mapDeltaAction, actionMap] using
121 (mapDelta_step (δ:=δ) (hδ:=hδ) (f:=actionMap hbar) (n:=n))
122