galactic_ratio_rational
plain-language theorem explainer
galactic_ratio_rational supplies the fixed rational 41971608 * 10^24 / 73 as proxy for the galactic timescale ratio τ★/τ₀ ≈ 5.75e29. Researchers verifying Recognition Science predictions for galactic dynamics cite it when establishing that the phi-rung index N_galactic lies strictly between 140 and 145. The declaration is a direct rational literal requiring no lemmas or reduction steps.
Claim. Let r = 41971608 × 10^{24} / 73 ∈ ℚ. This rational serves as the working numerical proxy for the dimensionless ratio τ★ / τ₀ ≈ 5.75 × 10^{29}.
background
The Numerics.Interval.GalacticBounds module constructs interval enclosures for powers of the golden ratio φ to locate the galactic ratio. galactic_ratio_rational is the concrete rational constant imported from Constants and used to bound φ^N for N near 140-145. Upstream results define φ as the self-similar fixed point satisfying the Recognition Composition Law J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y).
proof idea
The declaration is a direct definition of the rational literal 41971608 * 10^24 / 73. No lemmas are invoked; downstream proofs simply unfold the identifier and apply norm_num to obtain the required comparisons against phi-power intervals.
why it matters
This constant anchors the parent theorems N_galactic_approx and tau_star_is_phi_rung, which place τ★ on the phi-ladder at rung 142. It supplies the numerical bridge to the Recognition Science T7 eight-tick octave structure for galactic periods. The open question it touches is the precision with which the exact physical ratio matches this rational proxy.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.