rung_offset_is_power_of_2
plain-language theorem explainer
The declaration verifies that the 16-rung offset equals 2 to the fourth power. Gravity modelers working in Recognition Science would cite it to fix the phi-ladder position when deriving parameters such as alpha_gravity and upsilon_star. The verification is a direct numerical check on the constant definition.
Claim. The 16-rung offset satisfies $16 = 2^4$.
background
The GravityParameters module derives galactic gravity parameters from Recognition Science. It lists seven quantities, some proven from phi (such as alpha = 1 - 1/phi) and others with RS basis or phenomenological status. The rung offset appears as the shift in the phi-ladder used for mass scaling formulas of the form yardstick times phi to the (rung minus 8 plus gap). Upstream, rung_offset is introduced as the constant 16, described as the 16-rung offset equal to 2^4 or the second non-trivial perfect square.
proof idea
The proof is a one-line wrapper that applies native_decide to the equality between the defined natural number 16 and the power 2^4.
why it matters
The result fixes the ladder offset inside the gravity parameters module, supporting later derivations of upsilon_star = phi and alpha_gravity. It aligns with the eight-tick octave structure from the forcing chain (T7) by choosing a power-of-two rung count. No downstream theorems currently reference it, and no open scaffolding questions are closed here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.