rung_offset_is_two_8tick_cycles
plain-language theorem explainer
The rung offset in the Recognition Science phi-ladder equals two eight-tick cycles. Modelers of galactic gravity parameters would reference this identity when aligning mass rungs with observed rotation curves. The proof is a direct native computation confirming the constant definition matches the arithmetic expression.
Claim. The 16-rung offset in the phi-ladder equals two periods of the eight-tick octave: $16 = 2 times 8$.
background
The GravityParameters module derives galactic gravity parameters from the golden ratio phi, classifying each as derived, RS-basis, or phenomenological. rung_offset is introduced as the constant 16, described as the shift N_tau minus 16 that yields the conjectured galactic radius rung of 126. This setting rests on the eight-tick octave (period 2^3) and the phi-ladder mass formula yardstick times phi to the power of (rung minus 8 plus gap). Upstream definitions of rung appear in AnchorPolicy, RSBridge.Anchor, and Compat.Constants, each assigning integer rungs to sectors or particles without further structure.
proof idea
The proof is a one-line term that invokes native_decide to evaluate the equality between the defined constant 16 and the expression 2 * 8.
why it matters
This equality anchors the galactic gravity parameters to the eight-tick octave (T7) of the forcing chain. It supports derivation of alpha_gravity and upsilon_star within the same module while linking the phi-ladder mass formula to galactic scales. The offset is consistent with T8 fixing D equals 3 and the overall Recognition Composition Law structure, though no downstream theorems yet consume it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.