btfr_cert
plain-language theorem explainer
The declaration certifies that the deep-regime baryonic Tully-Fisher relation has exact exponent 4 together with a universal prefactor 1/(G a0) independent of baryonic mass. Galaxy-dynamics modelers would cite it to account for the observed low scatter in the BTFR under ILG scaling. The proof is a term-mode record construction that directly supplies the exponent identity and the universal-constant theorem to the BTFRCert structure.
Claim. The deep-regime BTFR satisfies exponent exactly 4 and the universal scaling property: for all $G,a_0>0$ and all positive velocities $v_1,v_2$, if $M_1=v_1^4/(G a_0)$ and $M_2=v_2^4/(G a_0)$ then $M_1/M_2=(v_1/v_2)^4$.
background
The module records the algebraic link between the ILG/RAR scaling and the empirical BTFR $M_bpropto v_f^beta$. In the deep regime the RAR form reduces to $a_obs=a_baryon$ with the flat-curve constraint $a_obs=v_f^2/r$ and $a_baryon=GM_b/r^2$, yielding the exact relation $M_b=v_f^4/(G a_0)$. The structure BTFRCert packages two required properties: the slope equality $beta_deep=4$ and the universality of the prefactor $1/(G a_0)$ (independent of $M_b$). Upstream, btfr_deep_regime_exponent establishes the slope by reflexivity while btfr_constant_universal proves the ratio identity under the stated positivity hypotheses.
proof idea
The proof is a term-mode record construction that supplies btfr_deep_regime_exponent to the deep_exponent field and btfr_constant_universal to the deep_universal field of BTFRCert.
why it matters
This certificate supplies the mechanically verified power-law wrapper for BTFR emergence while a fully structural derivation with nontrivial constant independent of $M_b$ remains in progress. It feeds the gravity-emergence development by confirming the observed BTFR scaling from the ILG deep-regime limit. In the Recognition Science setting it aligns with the forcing-chain derivation of three-dimensional gravity and the RAR acceleration scale, closing the algebraic check for the tight observed relation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.