mapDeltaAction_fromZ
plain-language theorem explainer
The lemma establishes that the delta-action map applied to the integer embedding fromZ(δ, n) recovers exactly ħ ⋅ n. Researchers verifying consistency between discrete ledger units and continuous action parameters in Recognition Science cite it when checking that actionMap commutes with the subgroup embedding. The proof is a one-line wrapper that instantiates the general mapDelta_fromZ lemma with f := actionMap ħ and simplifies via the definitions of mapDeltaAction together with add_comm.
Claim. For nonzero integer δ, real ħ, and integer n, the action map applied to the subgroup element fromZ(δ, n) satisfies mapDeltaAction(δ, ħ, fromZ(δ, n)) = ħ ⋅ n.
background
The UnitMapping module treats DeltaSub δ as the abstract subgroup generated by a fixed nonzero integer δ, using ℤ only as a placeholder for discrete mappings. The constructor fromZ δ n produces the element n⋅δ inside this subgroup. mapDeltaAction δ hδ ħ is the specialization of the general mapDelta operator to the function actionMap ħ, which scales subgroup elements by the real parameter ħ. Upstream results supply the definition of ħ as φ^{-5} in RS-native units and the commutativity of addition in the underlying arithmetic.
proof idea
The term proof first obtains an instance of mapDelta_fromZ by substituting f := actionMap ħ. It then applies simpa, unfolding the definitions of mapDeltaAction and actionMap while invoking add_comm to discharge the resulting equality.
why it matters
The result closes a consistency check inside the unit-mapping layer, confirming that the action scaling commutes with the integer embedding. It supports the Recognition Science construction of ledger units by ensuring that discrete increments map to continuous action values without distortion. No downstream theorems are recorded, leaving the lemma as a local bridge between the subgroup abstraction and the ħ-scaled action map.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.