rar_is_universal
plain-language theorem explainer
rar_is_universal establishes that the ratio of observed accelerations between any two galaxies equals the ratio of their baryonic accelerations raised to the fixed power 1 - α/2, whenever a0 and α are the same global constants. Galaxy modelers using the ILG framework cite it to confirm the RAR takes a universal power-law form independent of individual galaxy details. The proof substitutes the explicit power-law expression for each galaxy and cancels the shared a0 factors via algebraic identities on real exponents.
Claim. Let $a_0 > 0$ and let $a_1 > 0$, $a_2 > 0$ be the baryonic accelerations of two galaxies. Then the ratio of their ILG-derived observed accelerations satisfies $a_1^{1 - α/2} / a_2^{1 - α/2} = (a_1 / a_2)^{1 - α/2}$, where the observed acceleration is defined by the weight function $w(a_0, a, α) = C · (a_0 / a)^{α/2}$ so that $a_{obs} = w · a$.
background
The module derives the radial acceleration relation from the ILG weight function. Observed acceleration is defined by a_obs_ilg a0 a_baryon α := w_accel a0 a_baryon α * a_baryon, where w_accel scales as (a0 / a_baryon)^{α/2}. The companion definition rar_power_law supplies the explicit closed form a_obs = a0^{α/2} * a_baryon^{1 - α/2} (up to a global constant). MODULE_DOC states that under RS parameter locks α equals alphaLock ≈ 0.191, yielding the exponent 1 - α/2 ≈ 0.905. Upstream results supply the underlying J-cost and ledger structures that fix the functional form of the weight.
proof idea
The tactic proof applies rar_power_law to both galaxies, producing identical a0^{α/2} prefactors. It then isolates the ratio of the remaining a_baryon^p terms (with p := 1 - α/2), proves the a0 factors cancel by mul_div_mul_left after showing a0^{α/2} ≠ 0, and rewrites the quotient via Real.div_rpow on the positive reals. The final simp step folds the rewritten ratio back into the target expression.
why it matters
This theorem confirms that the RAR power-law form is identical for every galaxy once a0 and α are fixed globally, completing the derivation begun in the ILG weight function. It directly supports the main claim in MODULE_DOC that a_obs = C · a0^{α/2} · a_baryon^{1 - α/2} with exponent ≈ 0.8. The result sits inside the Gravity.RAREmergence module and aligns with the Recognition Science forcing chain that locks α through the eight-tick octave and phi-ladder. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.