rungOf_step
plain-language theorem explainer
The rung level on the δ-generated subgroup of integers increases by one under the successor map fromZ. Researchers modeling discrete phi-ladders for mass or energy tiers in Recognition Science cite this step property. The proof is a one-line wrapper that applies the successor lemma for the inverse map toZ and simplifies via the rungOf definition.
Claim. For nonzero integer $δ$ and integer $n$, the rung level satisfies rung level of $δ$ at embedding of $n+1$ equals rung level of $δ$ at embedding of $n$ plus one.
background
LedgerUnits treats the subgroup of ℤ generated by nonzero δ, with fromZ the embedding n ↦ n·δ and toZ its inverse isomorphism. rungOf extracts the discrete rung index on the phi-ladder associated to the embedded unit. The module specializes to δ = 1 for a clean order isomorphism between the subgroup and ℤ. Upstream results supply structures for nuclear densities at phi-tiers and recognition-weighted mass-to-light ratios that rely on these discrete levels.
proof idea
The proof is a one-line wrapper that applies the toZ_succ lemma establishing the successor property for the toZ map, then simplifies using the definition of rungOf.
why it matters
This supplies the incremental step for rung levels along the phi-ladder, supporting the mass formula with yardstick · phi^(rung - 8 + gap(Z)). It contributes to applications of the Recognition Composition Law in ledger factorizations and the eight-tick octave structure. No downstream uses are recorded, leaving its role as a basic property in the discrete units layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.