N_r_conjecture_eq_126
plain-language theorem explainer
Fixes the conjectured galactic radius rung at exactly 126. Galaxy modelers working with Recognition Science phi-ladder mass formulas cite this to anchor radius calculations in the N_tau minus offset relation. The proof is a one-line native decision that evaluates the concrete natural-number definition directly.
Claim. The conjectured galactic radius rung satisfies $N_r = 126$, where $N_r$ is defined by subtracting the rung offset 16 from the conjectured tau rung $N_τ = 142$.
background
The GravityParameters module derives phenomenological galactic gravity parameters from Recognition Science first principles using the golden ratio φ. Parameters are classified as derived (such as α = 1 - 1/φ), having RS basis (C_ξ = 2φ^{-4}, p = 1 - αLock/4), or phenomenological, with Υ★ fixed at φ by convention. The module links a0 and r0 through the relation τ★ = √(2π r0 / a0) on the phi-ladder. N_r_conjecture supplies the radius rung value as N_tau_conjecture minus rung_offset.
proof idea
One-line term proof that invokes native_decide to evaluate the definition N_r_conjecture := N_tau_conjecture - rung_offset to the concrete natural number 126.
why it matters
This declaration anchors the radius rung in the phi-ladder for gravity calculations, completing the conjecture step N_r = N_τ - 16. It supports derivations of galactic acceleration and radius scales consistent with the eight-tick octave and D = 3 from the forcing chain. No downstream uses are recorded, leaving open its integration into full mass-formula proofs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.