kOf
plain-language theorem explainer
kOf extracts a nonnegative natural-number index from any element of the δ-generated subgroup of the integers by first recovering its integer coefficient and then truncating to Nat. Ledger-unit constructions and scale lemmas cite this map to turn signed deltas into rung labels. The definition is a direct composition of the coefficient selector toZ with Int.toNat.
Claim. For an integer generator δ and an element p of the subgroup {x ∈ ℤ | ∃ n ∈ ℤ, x = n·δ}, the nonnegative index is defined by k(δ,p) := Int.toNat(n), where n is the integer coefficient recovered from p.
background
LedgerUnits works inside the subgroup DeltaSub δ of ℤ, defined as the set of all integer multiples of a fixed generator δ. The auxiliary map toZ recovers the unique coefficient n such that the representative of p equals n·δ. Upstream, toNat from ArithmeticFromLogic converts a logic natural number into an ordinary Nat by counting iteration steps.
proof idea
kOf is a one-line wrapper that applies toZ to the subgroup element and then passes the result to Int.toNat.
why it matters
The definition supplies the nonnegative k-index used by the downstream lemmas kOf_fromNat, kOf_fromZ and kOf_step_succ. Those lemmas establish the arithmetic of rung labels on the δ-subgroup. In the Recognition framework the map converts signed deltas into the natural-number indices required by the phi-ladder mass formula and the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.