rung_offset
plain-language theorem explainer
The rung offset is the fixed natural number 16 subtracted from the tau conjecture to locate the galactic radius rung. Galactic dynamics researchers cite this constant when scaling the phi-ladder to observed rotation curves. The definition is a direct constant assignment that enables downstream algebraic verifications of its power-of-two and perfect-square properties.
Claim. Define the rung offset by the equation $r := 16$ where $r$ is a natural number.
background
The GravityParameters module derives galactic gravity parameters from the Recognition Science phi framework. Parameters are classified as derived from phi, having an RS basis, or phenomenological, with the rung offset appearing in the linked a0 and r0 scaling via the tau star relation. The phi-ladder supplies rung counts for mass and length scales, and the eight-tick octave (period 2^3) supplies the structural period that 16 respects as two full cycles.
proof idea
Direct definition that assigns the constant 16 with no computation or lemmas applied.
why it matters
This definition supplies the exact offset subtracted in the N_r_conjecture to produce the galactic radius rung 126. It anchors the rung_relationship theorem and feeds the three verification theorems that establish the offset as 2^4, 4^2, and two eight-tick cycles. The placement ties directly to the T7 eight-tick octave landmark and the phi-ladder mass formula used for galactic scaling.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.