rungOf
plain-language theorem explainer
rungOf extracts the integer coefficient n from an element p of the subgroup generated by δ by delegating directly to toZ. Mass ladder derivations and unit-mapping lemmas cite this when converting between rung indices and δ-subgroup elements. The definition is a one-line alias to the toZ projection.
Claim. Let $Delta_δ = {x ∈ ℤ | ∃ n ∈ ℤ, x = n δ}$. For $p ∈ Delta_δ$, rungOf(δ, p) returns the integer n such that p = n δ, via the coefficient map toZ.
background
DeltaSub δ is the subgroup of ℤ consisting of all integer multiples of δ. The module specializes to δ = 1 to obtain a clean order isomorphism with ℤ. toZ extracts the coefficient by selecting the witness n from the existential property of p. This construction reappears in RecogSpec.Scales and UnitMapping to support consistent rung indexing across ledger and mass modules.
proof idea
The definition is a one-line wrapper that applies toZ to the supplied δ and subgroup element p.
why it matters
rungOf feeds rungOf_fromZ and rungOf_step, which establish the isomorphism for nonzero δ, and is used by rungOf in Masses.KernelTypes and Derivation in Ribbons. It supplies the integer rung coordinate required by the mass formula yardstick · φ^(rung − 8 + gap(Z)) on the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.