rung_relationship
plain-language theorem explainer
The theorem states that the conjectured galactic radius rung equals the conjectured timescale rung minus 16. Galaxy modelers using Recognition Science cite it to close the link between spatial and temporal scales on the phi-ladder. The proof is a direct reflexivity step because the radius rung is defined from the timescale rung.
Claim. If the Fibonacci-square conjecture holds, the conjectured galactic radius rung $N_r$ satisfies $N_r = N_τ - 16$, where $N_τ = F_{12} - 2$.
background
The GravityParameters module derives galactic gravity parameters from φ, classifying each as DERIVED (algebraic from φ), HAS RS BASIS (numerical match with motivation), or PHENOMENOLOGICAL. The seven parameters include α = 1 - 1/φ, Υ★ = φ, C_ξ = 2φ^{-4}, p = 1 - αLock/4, A = 1 + αLock/2, and a0, r0 linked via τ★ = √(2π r0 / a0). The rung relationship appears in the module summary table under the conjectured N_τ = F_12 - 2 entry.
proof idea
The proof is a one-line term proof that applies reflexivity (rfl) directly to the definition of N_r_conjecture in terms of N_tau_conjecture.
why it matters
This theorem supplies the exact numerical relation between the two conjectured rungs, supporting the module claim that the model has zero phenomenological parameters once the Fibonacci-square conjecture is accepted. It fills the N_τ = F_12 - 2 row in the summary table and connects to the phi-ladder mass formula. The result touches the open validation of the Fibonacci-square selection for galactic timescales.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.