kOf_step_succ
plain-language theorem explainer
The lemma shows that the coefficient extractor applied to the (m+1)-fold multiple of a nonzero integer generator δ equals the coefficient of the m-fold multiple plus one. Workers on discrete subgroups and quantization steps in Recognition Science cite it when confirming that the natural-number indexing produces unit increments in the coefficient. The proof is a one-line term simplification that unfolds the relevant definitions and reduces by reflexivity.
Claim. For nonzero integer $δ$ and natural number $m$, let $x_n$ denote the $n$-fold sum of $δ$ in the subgroup it generates. Then the integer coefficient of $x_{m+1}$ equals the coefficient of $x_m$ plus one.
background
The LedgerUnits module examines the additive subgroup of ℤ generated by a fixed nonzero δ, with the case δ = 1 yielding a clean order isomorphism to the naturals. The fromNat construction (imported from ArithmeticFromLogic) builds this subgroup element by iterated addition of δ, so fromNat δ m corresponds to the m-fold sum. The kOf function extracts the unique integer multiplier for each such element, consistent with the module's quantization remark that every element carries a unique coefficient. Upstream structures from PhiForcingDerived and SpectralEmergence supply the discrete tier context in which these integer steps appear.
proof idea
The proof is a term-mode one-liner. It invokes simp only on the definitions of kOf and fromNat, the toZ_fromZ recovery of the integer from the subgroup element, and the natural-number addition rules Int.natCast_add and Int.natCast_one, then closes immediately by rfl.
why it matters
The result supplies a basic inductive step for the quantization claim that every element of the δ-subgroup possesses a unique integer coefficient. It sits inside the ledger-units construction that supports the Recognition Science forcing chain (T0–T8) and the Recognition Composition Law by guaranteeing orderly discrete increments. No downstream uses are recorded, yet the lemma directly enables the order-isomorphism specialization to δ = 1 noted in the module documentation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.