kOf_fromZ
plain-language theorem explainer
Compatibility of nonnegative index extraction with the integer embedding into the δ-subgroup: for nonzero δ ∈ ℤ and any n ∈ ℤ, the k-index of the element n·δ equals the nonnegative conversion of n. Ledger unit mappings in Recognition Science cite this when normalizing coefficients for the phi-ladder and mass formulas. The proof is a one-line simp reduction that unfolds kOf and invokes the inversion toZ_fromZ.
Claim. For nonzero integer $δ$ and integer $n$, let $Δ_δ$ be the subgroup of $ℤ$ generated by $δ$, let $φ_δ(n) = n·δ$ be the embedding into $Δ_δ$, and let $k_δ(p)$ be the nonnegative integer $Int.toNat(k)$ where $k$ is the unique coefficient such that $p = k·δ$. Then $k_δ(φ_δ(n)) = Int.toNat(n)$.
background
LedgerUnits works with the subgroup $Δ_δ ⊆ ℤ$ generated by a fixed nonzero integer $δ$. The constructor fromZ δ n produces the element $n·δ ∈ Δ_δ$. The extractor kOf δ p returns $Int.toNat(toZ δ p)$, where toZ recovers the integer coefficient of p. The module specializes to $δ=1$ to obtain a clean order isomorphism with $ℤ$ itself. This lemma sits inside that arithmetic layer and depends on the prior inversion lemma toZ_fromZ, which states that toZ δ (fromZ δ n) = n exactly, together with the definition of kOf as the composition $Int.toNat ∘ toZ$. The upstream toNat from ArithmeticFromLogic supplies the forward reading of iteration counts that is reused here for nonnegative indices.
proof idea
One-line simp wrapper. It unfolds the definition of kOf and applies the already-proved lemma toZ_fromZ δ hδ, which directly replaces the inner toZ application by n and yields Int.toNat n.
why it matters
The result closes the round-trip for nonnegative indices inside each δ-subgroup, guaranteeing that the embedding fromZ followed by kOf recovers the original nonnegative part of n. It belongs to the arithmetic foundation that supports unit mappings and the phi-ladder constructions in the Recognition framework (T5 J-uniqueness through T8 D=3). No downstream theorems are recorded yet, but the lemma is required for consistent index handling in mass formulas and Berry creation thresholds.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.