BTFRCert
plain-language theorem explainer
BTFRCert packages the assertion that the deep-regime BTFR exponent equals 4 together with the scaling M = v^4/(G a0) holding identically for any positive G and a0. Galaxy dynamicists and modified-gravity modelers cite the certificate when they require a Lean-verified statement of the asymptotic power-law form. The structure is assembled directly from the constant definition btfr_slope_deep = 4 and the algebraic identity that follows from the flat-rotation power law.
Claim. The structure asserts that the deep BTFR exponent equals 4 and that, for all positive real numbers $G$ and $a_0$ and all positive velocities $v_1, v_2$, the masses defined by $M_i = v_i^4 / (G a_0)$ satisfy $M_1/M_2 = (v_1/v_2)^4$.
background
The module derives the BTFR from the ILG modification of Newtonian gravity via the RAR power-law form $a_{obs} = a_0^{alpha/2} a_{baryon}^{1-alpha/2}$. In the deep regime this produces slope beta = 4/(1 + alpha/2). The upstream definition btfr_slope_deep fixes the asymptotic value at 4 for flat rotation curves. The certificate isolates the universal scaling that holds once this exponent is adopted, before a full structural emergence theorem with an independent constant is completed. From the module documentation the empirical BTFR states that baryonic mass correlates with asymptotic rotation velocity as $M_b propto v_f^beta$ with beta approximately 3.5-4.
proof idea
BTFRCert is a structure definition whose first field records the equality btfr_slope_deep = 4. The second field states the universal scaling property that follows identically from expressing masses via the fourth-power relation. No proof tactics are invoked; the structure simply packages the two properties for use by the downstream theorem btfr_cert.
why it matters
BTFRCert supplies the fields required by the theorem btfr_cert that constructs an explicit instance. It provides the mechanically checkable power-law wrapper described in the module while a fully structural BTFR emergence theorem with nontrivial constant remains in progress. The result sits inside the gravity module that extracts the BTFR from the ILG/RAR scaling, consistent with the Recognition Science derivation of constants and the phi-ladder mass formulas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.