rungOf_fromZ
plain-language theorem explainer
The lemma establishes that the rung index of the element n·δ in the subgroup generated by nonzero integer δ equals the coefficient n. Researchers handling mass ladders or unit mappings in Recognition Science would cite it to simplify coefficient extractions. The proof is a direct one-line simpa reduction that unfolds the rung index definition and applies the prior toZ extraction identity.
Claim. For nonzero integer $δ$ and integer $n$, the rung index of the element $n·δ$ in the subgroup generated by $δ$ equals $n$.
background
DeltaSub δ is the subgroup of ℤ consisting of all integer multiples of δ. The map fromZ δ n constructs the element n·δ inside this subgroup. The rung index function applied to an element p in DeltaSub δ returns the unique integer coefficient k such that p = k·δ, implemented via the toZ extraction.
proof idea
One-line wrapper that applies simpa, unfolding the rung index definition and substituting the toZ extraction identity for the given δ and nonzero hypothesis.
why it matters
This identity ensures consistent rung extraction in the phi-ladder mass formulas, where masses scale as yardstick times phi to the power of (rung minus 8 plus gap). It closes the round-trip between integer coefficients and subgroup elements in the LedgerUnits module, supporting the general δ case before specializing to δ=1 for the order isomorphism. No open questions are touched.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.