r0_from_tau_a0
plain-language theorem explainer
The definition computes the galactic length scale r₀ directly from the acceleration scale a₀ and timescale τ★. It is cited in consistency verifications for Recognition Science gravity models that link observed galactic parameters to the derived timescale constraint. The implementation is a one-line algebraic rearrangement inverting τ★ = √(2π r₀ / a₀).
Claim. The length scale satisfies $r_0 = a_0 τ_★^2 / (2π)$, where $τ_★$ is the characteristic timescale and $a_0$ the acceleration scale.
background
The GravityParameters module derives galactic gravity parameters from the golden ratio φ. The table lists a₀ and r₀ as linked parameters via the relation τ★ = √(2π r₀ / a₀). This definition supplies the explicit inversion for r₀ given τ★ and a₀. The module distinguishes fully derived quantities such as Υ★ = φ from these linked scales.
proof idea
The declaration is a direct definition implementing the algebraic inversion of the timescale constraint. No lemmas are applied; it is a one-line expression using standard real arithmetic.
why it matters
This definition supports the consistency theorem tau_constraint_consistency that verifies forward and inverse mappings between a₀, r₀, and τ★. It fills the linked-parameter slot in the module's seven-parameter table. Within Recognition Science it connects phenomenological galactic scales to the φ-derived constants without new axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.