a0_from_tau_r0
plain-language theorem explainer
Galactic dynamics models in Recognition Science use the relation a0 = 2π r0 / τ★² to connect the characteristic timescale and length scale to the acceleration parameter. This definition is invoked in proofs that express a0 on the φ-ladder and verify consistency between forward and inverse mappings. The implementation is a single-line algebraic expression with no lemmas required.
Claim. The acceleration scale satisfies $a_0 = 2π r_0 / τ_★^2$, where $τ_★$ is the characteristic timescale and $r_0$ the reference length scale.
background
The GravityParameters module derives phenomenological galactic gravity parameters from Recognition Science first principles. Each parameter is classified as DERIVED (mathematically proven from φ), HAS RS BASIS (formula matches observations with physical motivation), or PHENOMENOLOGICAL. The table lists α as DERIVED via 1 - 1/φ, C_ξ via 2φ^{-4}, p via 1 - αLock/4, A via 1 + αLock/2, Υ★ as φ by convention, and a0, r0 as LINKED via the timescale constraint τ★ = √(2π r0 / a0). Upstream, the scale function from LargeScaleStructureFromRS defines scale(k) := φ^k, while r0 from Masses.Anchor assigns φ-exponent offsets per sector such as 4(W) - 6 for leptons.
proof idea
This is a direct definition implementing the algebraic formula 2 * Real.pi * r0 / tau_star ^ 2. No lemmas are applied; it is a one-line expression.
why it matters
This definition supplies the core relation used by the theorem a0_phi_ladder_formula, which expresses a0 in terms of φ powers on the ladder as a0 = 2π c_light / tau0 * φ^(N_r - 2 N_tau), and by tau_constraint_consistency, which verifies the inverse mapping r0 = r0_from_tau_a0. It fills the LINKED status for a0, r0 in the module's table of seven parameters. In the Recognition framework it supports derivation of gravity parameters from φ, consistent with the eight-tick octave and D = 3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.