mapDelta_step
plain-language theorem explainer
The lemma shows that the difference in mapDelta under an affine map f between consecutive elements fromZ δ (n+1) and fromZ δ n equals the slope of f. Researchers establishing incremental changes for time and action unit mappings cite it. The proof is a direct calc block that simplifies the definition then reduces via ring and arithmetic lemmas.
Claim. Let δ be a nonzero integer, f an affine map ℤ → ℝ with slope s and offset o, and n an integer. Then mapDelta(δ, f, fromZ(δ, n+1)) − mapDelta(δ, f, fromZ(δ, n)) = s, where fromZ(δ, k) denotes the element k·δ in the subgroup generated by δ.
background
The UnitMapping module treats mappings over the subgroup generated by a fixed nonzero integer δ as an abstract placeholder. AffineMapZ is the structure with slope and offset fields, representing the map sending index k to slope·k + offset. The function fromZ δ n constructs the corresponding subgroup element. This lemma depends on toZ_fromZ, which recovers the original index n from fromZ δ n, allowing mapDelta to be expressed in terms of the index. Upstream results include add_assoc, add_comm, and mul_add from ArithmeticFromLogic, supplying the ring identities used in the final step.
proof idea
The proof opens with classical and a calc block. The first equality applies simp [mapDelta, toZ_fromZ] to replace both terms with slope times the cast index plus offset. Ring cancels the offsets. Simpa [Int.cast_add, Int.cast_one] rewrites the cast of n+1. The final simp applies mul_add, sub_eq_add_neg, add_comm, add_left_comm, and add_assoc to reduce to the slope.
why it matters
This lemma supplies the algebraic core for mapDeltaTime_step and mapDeltaAction_step, which establish that consecutive increments equal the base units tau0 and hbar. It supports consistent integer-lattice mappings of physical quantities in the Recognition Science unit system, consistent with the scales in the forcing chain (T5–T8). No open question is directly addressed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.