btfr_slope_identity_iff
plain-language theorem explainer
The equivalence BTFRSlopeIdentity asserts that for positive reals M, Vflat, a0, G the baryonic mass satisfies M = Vflat^4 / (G a0) precisely when the product M (G a0) equals Vflat^4. Analysts of galactic rotation curves and the Baryonic Tully-Fisher Relation cite this algebraic identity to anchor the ILG enhancement factor in the SPARC dataset. The proof proceeds by a direct tactic script that establishes both directions of the biconditional via positivity of G a0 and cancellation of the nonzero term.
Claim. For all positive real numbers $M, V, a_0, G$, the equality $M = V^4 / (G a_0)$ holds if and only if $M (G a_0) = V^4$.
background
The module develops structural properties of the Information-Limited Gravity radial weight w(R) = 1 + C (R/r0)^α with α = 1 - 1/φ and C = φ^{-3/2}. BTFRSlopeIdentity encodes the algebraic relation underlying the baryonic Tully-Fisher relation, where Newtonian velocity squared is G M / R and the ILG version is w(R) times that. The definition is the proposition that M equals Vflat to the fourth over (G a0) exactly when their product recovers Vflat to the fourth, for positive parameters. This rests on the gravitational constant G derived in Constants as λ_rec² c³ / (π ħ) and on basic arithmetic facts such as mul_one from ArithmeticFromLogic. The surrounding theorems establish positivity and monotonicity of the enhancement factor, ensuring the modified velocity exceeds the Newtonian prediction at all radii.
proof idea
The proof opens by introducing the four positive parameters and deriving that G a0 is positive and nonzero. It then splits the biconditional into two implications. The forward direction rewrites the assumed equality and cancels the nonzero divisor. The reverse direction substitutes the product equality and simplifies using associativity and division by the nonzero term, invoking mul_one to reach the target.
why it matters
This identity supplies the slope relation required by the certificate theorem ilgAsymptoticEnhancementCert_holds, which packages the positivity, strict increase, and unboundedness of the ILG enhancement. It fills the algebraic step in Phase D9 of the RS_PhiLocked_SPARC_Prereg analysis, confirming that the BTFR slope remains locked under the φ-derived parameters. The result ties directly to the eight-tick octave and phi-ladder structure of Recognition Science by ensuring the velocity scaling matches the observed flat rotation curves without additional tuning.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.