btfr_constant_universal
plain-language theorem explainer
The theorem shows that baryonic masses defined via the deep-regime constant 1/(G a0) satisfy a strict fourth-power velocity scaling. Galaxy dynamics researchers cite it to account for the low intrinsic scatter in the observed baryonic Tully-Fisher relation. The proof is a direct algebraic substitution of the two mass equations, followed by clearing the common nonzero denominator and ring normalization.
Claim. If the baryonic masses satisfy $M_1 = v_1^4 / (G a_0)$ and $M_2 = v_2^4 / (G a_0)$ for positive real numbers $G$, $a_0$, $v_1$, $v_2$, then $M_1 / M_2 = (v_1 / v_2)^4$.
background
The module records the algebraic link between the ILG/RAR scaling and a BTFR-style power law. The empirical BTFR states that total baryonic mass $M_b$ correlates with asymptotic rotation velocity $v_f$ as $M_b proportional to v_f^beta$ with beta near 4 and scatter 0.1-0.2 dex. In the deep regime the RAR power-law form $a_obs = a_0^{alpha/2} a_baryon^{1-alpha/2}$ rearranges, for flat rotation curves, to the mass-velocity relation $M_b = v_f^4 / (G a_0)$. The constant $C = 1/(G a_0)$ is independent of galaxy mass, which explains the observed universality. Upstream results supply the collision-free ledger properties and structural isomorphisms used in the broader ILG construction, though the present step is purely algebraic.
proof idea
The proof substitutes the two mass hypotheses into the goal. It then records that $G a_0$ is nonzero from the positivity assumptions and that $v_2^4$ is nonzero. Field simplification cancels the common denominator, after which the ring tactic reduces the identity to a tautology.
why it matters
This result is invoked by btfr_cert to certify the deep-regime universal constant inside the BTFRCert structure. It thereby completes the mechanical verification that the BTFR power law emerges from the RAR interpolation without additional mass-dependent parameters. In the Recognition framework it supports the claim that the acceleration scale together with G fixes the deep-regime behavior, consistent with the phi-ladder constants. The module leaves open a fully structural derivation of the BTFR constant from the J-cost functional.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.