mapDeltaAction_step
plain-language theorem explainer
The lemma shows that advancing the index by one unit inside the subgroup generated by any nonzero integer δ increases the mapped action value by exactly ħ. Researchers deriving discrete action spectra from the Recognition framework would cite it when constructing the action component of the unit ladder. The proof is a direct specialization of the general mapDelta_step result to the affine action map.
Claim. Let δ be a nonzero integer, ħ a real number, and n an integer. Let S_δ be the subgroup generated by δ. Let fromZ_δ(k) denote the element k·δ inside S_δ. Let actionMap_ħ be the affine map sending the underlying index to ħ times that index. Then actionMap_ħ(fromZ_δ(n+1)) − actionMap_ħ(fromZ_δ(n)) = ħ.
background
The UnitMapping module treats DeltaSub δ as an abstract placeholder subgroup generated by a fixed nonzero integer δ, using integers solely for mapping purposes. The constructor fromZ δ n produces the element n·δ inside this subgroup. The actionMap ħ is the affine map with slope ħ and zero offset, so the mapped action scales directly with the integer index. The parameter ħ stands for the reduced Planck constant in RS-native units, ħ = φ^{-5}.
proof idea
One-line term-mode wrapper. It applies the general mapDelta_step lemma (which proves the increment property for any affine map f) after substituting f := actionMap ħ, then simplifies the resulting expression using the definitions of mapDeltaAction and actionMap.
why it matters
The result supplies the discrete step for action in the unit-mapping layer that feeds into Recognition Science quantization. It aligns with the framework's assignment ħ = φ^{-5} and supports later constructions that combine action increments with the Recognition Composition Law and the eight-tick octave. No parent theorems are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.