rungOf_step
plain-language theorem explainer
The lemma shows that advancing the integer index by one under the isomorphism from ℤ to the δ-subgroup of ℤ increases the associated rung by precisely one. Researchers constructing discrete mass or energy tiers on the phi-ladder in Recognition Science would cite this step property. The proof is a one-line simplification that applies the successor lemma for the inverse map and unfolds the rung definition.
Claim. For nonzero integer $δ$ and integer $n$, if $m_n$ denotes the element of the subgroup generated by $δ$ that corresponds to $n$ under the isomorphism, then the rung of $m_{n+1}$ equals the rung of $m_n$ plus one.
background
The LedgerUnits module equips the subgroup of ℤ generated by nonzero $δ$ with maps realizing a group isomorphism to ℤ, via the correspondence $n ↦ n·δ$. The rung function extracts the discrete level of each such element, aligning with the mass formula that locates quantities at phi-powered positions on the ladder. This rests on upstream structures including nuclear density tiers and J-cost definitions that interpret the physical content of these levels.
proof idea
The proof is a one-line wrapper that applies the successor lemma for the inverse map to the parameters $δ$, $hδ$, $n$ and simplifies the resulting equality using the definition of the rung function.
why it matters
This increment property maintains consistent ordering when stepping through discrete ledger units and supports the phi-ladder in the mass formula. It supplies a basic step in the forcing chain by ensuring the rung map respects successor, contributing to the discrete structure needed for T7 eight-tick octave and T8 spatial dimensions. No immediate downstream theorems are recorded, leaving open its precise integration into derivations of constants such as the alpha band.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.