kOf_fromNat
plain-language theorem explainer
The lemma states that the nonnegative k-index extracted from the natural-number embedding into the δ-subgroup recovers the original index m. Ledger-unit and arithmetic-mapping work in Recognition Science cites it to simplify index calculations inside DeltaSub. The proof is a one-line simp wrapper that unfolds kOf, fromNat, the toZ_fromZ round-trip, and the Int.toNat cast on naturals.
Claim. Let δ ∈ ℤ with δ ≠ 0 and let m ∈ ℕ. Let Δ_δ be the subgroup of ℤ generated by δ. Let ι_δ(m) be the element obtained by embedding m via fromZ δ (Int.ofNat m). Let k_δ(p) be Int.toNat(toZ δ p) for p ∈ Δ_δ. Then k_δ(ι_δ(m)) = m.
background
LedgerUnits works inside the subgroup Δ_δ of ℤ generated by a fixed nonzero integer δ; the case δ = 1 yields an order isomorphism to ℤ. The embedding fromNat δ m is defined by fromZ δ (Int.ofNat m), placing the nonnegative integer m·δ inside Δ_δ. The extractor kOf δ p is defined as Int.toNat(toZ δ p), recovering the coefficient of the generator. Upstream, ArithmeticFromLogic.fromNat builds the orbit by iterated steps, while the lemma toZ_fromZ δ hδ n asserts toZ δ (fromZ δ n) = n, supplying the round-trip used here.
proof idea
One-line simp wrapper. It rewrites the goal by the definitions of kOf and fromNat, applies the round-trip lemma toZ_fromZ δ hδ, and reduces the resulting Int.toNat (Int.ofNat m) via Int.toNat_natCast.
why it matters
Supplies the basic compatibility between the nonnegative index map and the natural-number embedding inside LedgerUnits. It supports downstream index arithmetic that appears in unit-mapping lemmas and in the construction of the phi-ladder mass formulas. No direct parent theorem is listed among the used-by edges, but the result closes a routine gap in the δ-subgroup representation that the eight-tick octave and D = 3 constructions rely upon for consistent nonnegative counting.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.