rung_offset_is_perfect_square
plain-language theorem explainer
The declaration confirms that the 16-rung offset used in gravity parameter placement equals 16, or equivalently 4 squared. Modelers building Recognition Science galactic gravity fits would reference it to fix the ladder starting point for parameters such as alpha_gravity and upsilon_star. The proof reduces to a single native_decide call that evaluates the constant definition directly.
Claim. The 16-rung offset equals $4^2$.
background
The module GravityParameters derives galactic gravity quantities from the Recognition Science phi-ladder. Parameters are classified as DERIVED (mathematically proven from phi), HAS RS BASIS (formula matches observations with physical motivation), or PHENOMENOLOGICAL. The seven parameters include alpha (1 - 1/phi), C_xi (2 phi^{-4}), p (1 - alphaLock/4), A (1 + alphaLock/2), upsilon_star (phi), and linked a0, r0 via tau_star. The upstream definition states: 'The 16-rung offset is 2^4 = 4² (second non-trivial perfect square).' rung_offset itself is the constant 16.
proof idea
One-line wrapper that applies native_decide to the constant definition of rung_offset.
why it matters
The result anchors the gravity parameter ladder inside the phi-ladder framework, ensuring consistent placement for derived quantities such as alpha_gravity and upsilon_star. It supports the module's classification of a0_phi_ladder_formula as a proven theorem. No downstream theorems currently depend on it, leaving its role as a fixed computational checkpoint rather than an active inference step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.