rung
plain-language theorem explainer
The constant rung is defined as the natural number 1. Researchers modeling the phi-ladder in Recognition Science cite this base index for scale-dependent calculations across masses, acoustics, and applied devices. It supplies the default rung offset in downstream energy and strain formulas. The definition is a direct constant assignment with no computation or lemmas.
Claim. The base rung index on the recognition ladder is the natural number $1$.
background
Compat.Constants supplies project-wide constants and minimal structural lemmas for the Recognition Science framework. The rung definition provides a default index of 1 for phi-ladder calculations that appear in mass formulas and energy ladders. Upstream results define specialized rung maps, including the OreClass mapping (silicate to 0, metallic_Fe to 4) and the Fermion assignment (electron to 2, up quark to 4). The module doc states these constants support the overall structure of the phi-energy ladder.
proof idea
This is a direct definition that assigns the constant value 1. No lemmas or tactics are invoked.
why it matters
This supplies the reference rung value used by parent results such as hearingLossPenalty_zero, GeometricStrain, E_base_pos, and settlementLevelCount_eq. It fills the base case for the phi-ladder in the mass formula yardstick * phi^(rung - 8 + gap(Z)) and supports applications in the eight-tick octave and D = 3 spatial structure. The definition anchors the default offset for the phi-energy ladder E(n) = E_base * phi^n.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.