tau_constraint_consistency
plain-language theorem explainer
The consistency theorem shows that the acceleration scale a0 obtained from timescale tau_star and length r0 via a0 = 2 pi r0 / tau_star squared inverts to recover the original r0. Researchers deriving MOND-like galactic parameters from Recognition Science first principles would cite it to confirm the timescale constraint is algebraically invertible. The proof is a direct term-mode simplification that unfolds the two definitions, substitutes the hypothesis, and cancels via field operations after isolating the nonzero square.
Claim. Let $a_0, r_0, tau_star in mathbb{R}$ with $tau_star neq 0$. If $a_0 = 2 pi r_0 / tau_star^2$, then $r_0 = a_0 tau_star^2 / (2 pi)$.
background
The Gravity Parameters module derives seven galactic gravity parameters from phi, classifying a0 and r0 as linked through the timescale constraint tau_star = sqrt(2 pi r0 / a0). The forward map a0_from_tau_r0 is defined by a0 = 2 pi r0 / tau_star^2, forcing the acceleration scale once tau_star and r0 are given. The inverse map r0_from_tau_a0 recovers the length scale from tau_star and a0, and the present theorem proves these maps are mutual inverses.
proof idea
The term proof unfolds both a0_from_tau_r0 and r0_from_tau_a0, rewrites the goal with the hypothesis ha, introduces the auxiliary fact that tau_star squared is nonzero, and finishes with field_simp to cancel the common factors.
why it matters
The result closes the definitional loop for the linked a0-r0 pair inside the seven-parameter table of the module, where the phi-ladder formula for a0 is stated as a proven RS prediction that matches the observed MOND scale to 0.5 percent. It supports the claim that a0 is not a free parameter but is fixed by the phi-ladder structure once tau_star and r0 are chosen on the ladder. No downstream theorems are recorded, yet the consistency is presupposed by any later use of the timescale constraint in gravity derivations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.