kOf_step_succ
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not prove coefficient uniqueness for elements outside the image of fromNat.
- Does not treat the excluded case δ = 0.
- Does not link the coefficient to physical constants or φ-ladder rungs.
- Does not address non-additive group structures.
formal statement (Lean)
101lemma kOf_step_succ (δ : ℤ) (hδ : δ ≠ 0) (m : Nat) :
102 kOf δ (fromNat δ (m+1)) = kOf δ (fromNat δ m) + 1 := by
proof body
Term-mode proof.
103 simp only [kOf, fromNat, toZ_fromZ δ hδ, Int.natCast_add, Int.natCast_one]
104 rfl
105
106/-- Quantization: every element of the δ-subgroup has a unique integer coefficient. -/