OctaveRung
plain-language theorem explainer
OctaveRung supplies the integer index for octave levels within the RRF core structure. Researchers constructing hierarchical models of scaled physical patterns cite this alias to index families of octaves. The declaration is a direct type alias to the integers with no reduction steps or lemmas.
Claim. The octave rung index is the set of all integers $Z$.
background
In the RRF Core module an octave is a scale of manifestation. The same underlying pattern can appear at different octaves, related by scaling (φⁿ in the full theory). The module supplies the abstract octave structure without physical constants, with φ-scaling treated as a hypothesis in separate files. Upstream results supply rung assignments in constants and nucleosynthesis tiers that place physical quantities on discrete φ-tiers, together with J-cost structures from ledger factorization.
proof idea
The declaration is a direct type alias to the integers. No lemmas or tactics are invoked.
why it matters
The alias feeds the OctaveFamily structure that indexes octaves by rung. It supports the T7 eight-tick octave and the phi-ladder for scaling hierarchies. Physical mapping of the integer rungs remains open in the Hypotheses section.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.