a0_phi_ladder_formula
plain-language theorem explainer
The theorem shows that the MOND acceleration scale equals 2 pi c over tau0 times phi to the power of (N_r minus 2 N_tau) once tau star and r0 are placed on the phi ladder from positive tau0 and the light-speed relation ell0 equals c times tau0. Researchers deriving galactic gravity from Recognition Science first principles cite it to fix a0 by ladder rungs instead of treating it as free. The proof is a direct algebraic reduction that substitutes definitions, applies field simplification, and reduces the phi exponents via two short power-additon
Claim. Let tau_0 > 0 and ell_0 = c tau_0. Define tau_star = tau_0 phi^{N_tau} and r_0 = ell_0 phi^{N_r}. If a_0 satisfies a_0 = 2 pi r_0 / tau_star^2, then a_0 = 2 pi c / tau_0 * phi^{N_r - 2 N_tau}.
background
Recognition Science derives galactic gravity parameters from the phi-ladder, expressing times and lengths as fundamental units tau0 and ell0 raised to integer powers of phi. The module GravityParameters lists seven such parameters and classifies a0 as linked to the ladder via the relation a0 = 2 pi r0 / tau_star^2. The local setting treats this formula as a proven theorem rather than an axiom or conjecture.
proof idea
The tactic proof introduces the let-bound tau_star, r0 and a0, then dsimps the definition of a0 from tau and r0. It rewrites ell0 via the light-speed hypothesis, proves non-zero conditions for tau0 and the phi powers, and applies field_simp to clear denominators. Two auxiliary facts are established: (phi^{N_tau})^2 equals phi^{2 N_tau} by rpow_add, and phi^{2 N_tau} times phi^{N_r - 2 N_tau} equals phi^{N_r} by exponent addition. The target equality follows by a calc block that substitutes these identities.
why it matters
The result supplies an explicit, testable expression for the MOND scale a0 in terms of ladder rungs, matching the observed 1.95 times 10^{-10} m/s^2 to 0.5 percent for the cited approximate rung values. It supports the module claim that a0 is fixed by phi-ladder structure and contributes to the set of derived gravity parameters. The theorem closes the derivation for galactic scales while leaving open the Fibonacci-square conjecture that would set N_tau exactly to 142 and remove all remaining phenomenological inputs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.