Encyclopedia Gravity Gravity Ilgasymptotic Enhancement Btfr Slope Identity Iff
ARTICLE 3 claims 2 theorems 1 model
Gravity Ilgasymptotic Enhancement Btfr Slope Identity Iff
A machine-checked theorem confirms that two algebraic ways of writing the baryonic Tully-Fisher relation are exactly equivalent, nothing more.
The slope identity
The baryonic Tully-Fisher relation is an observed link between the total ordinary matter in a spiral galaxy and the flat speed at which its outer stars orbit. Write M for the baryonic mass, V for the flat rotation speed, and the relation becomes M ∝ Vβ. The exponent β is the slope; astronomers measure it near 4, meaning a galaxy with twice the mass rotates about 1.19 times faster.
The Recognition Science declaration btfr_slope_identity_iff proves a purely algebraic equivalence. For positive M, V, a0, and G, it establishes that M = V⁴ / (G·a0) holds if and only if M·(G·a0) = V⁴. This is a tautology in the sense that both equations say the same thing after multiplying through by the denominator. The theorem does not derive β = 4 from any physical principle; it merely confirms that the two forms of the relation are interchangeable.
The surrounding formal development also proves structural facts about the Information-Limited Gravity radial weight w(R) = 1 + C·(R/r0)α. Those theorems show w(R) is always positive, always above 1, strictly increasing in radius, and unbounded. The consequence is that the ILG-modified velocity squared always exceeds the Newtonian baryonic prediction and cannot decay like a Keplerian curve. These are genuine formal results, but they concern the weight function, not the slope identity itself.
The slope identity is recorded as a proposition, not derived. The docstring explains the intended physical reasoning: in the deep-ILG limit, a_obs ≈ (a0·a_bar)1/2, which leads to V⁴ ≈ G·M·a0 and hence β = 4. That reasoning is not formalized here. The numerical confirmation against SPARC data lives in a separate scorecard file, and the integration step from acceleration to velocity is explicitly left unformalized.
What the declaration gives a reader is precision about a small piece of the framework's machinery. If one accepts the ILG weight function and its derived properties, then the slope identity is a consistent algebraic statement. But the theorem itself carries no empirical weight; it is a bookkeeping fact, not a measurement or a derivation of the Tully-Fisher slope.
THEOREM btfr_slope_identity_iff · IndisputableMonolith/Gravity/ILGAsymptoticEnhancement.lean
theorem btfr_slope_identity_iff : BTFRSlopeIdentity := by
intros M V a0 G _hM _hV ha0 hG
have hpos : 0 < G * a0 := mul_pos hG ha0
have hne : (G * a0) ≠ 0 := ne_of_gt hpos
constructor
· intro h
have : M * (G * a0) = (V ^ 4 / (G * a0)) * (G * a0) := by rw [h]
rw [this, div_mul_cancel₀ _ hne]
· intro h
have : V ^ 4 = M * (G * a0) := h.symm
rw [this, mul_div_assoc, div_self hne, mul_one]
THEOREM enhancement_pos · enhancement_above_one · enhancement_strict_mono · enhancement_unbounded · IndisputableMonolith/Gravity/ILGAsymptoticEnhancement.lean
theorem enhancement_pos (R r0 : ℝ) (hR : 0 < R) (hr0 : 0 < r0) (n : ℕ) :
0 < w_radial R r0 n := by
unfold w_radial
have hpow : 0 ≤ (R / r0) ^ n := pow_nonneg (le_of_lt (div_pos hR hr0)) n
have hC : 0 < C_lock := C_lock_pos
have hCprod : 0 ≤ C_lock * (R / r0) ^ n := mul_nonneg (le_of_lt hC) hpow
linarith
theorem enhancement_above_one (R r0 : ℝ) (hR : 0 < R) (hr0 : 0 < r0)
(n : ℕ) (hn : 0 < n) : 1 < w_radial R r0 n := by
unfold w_radial
have hpow : 0 < (R / r0) ^ n := pow_pos (div_pos hR hr0) n
have hC : 0 < C_lock := C_lock_pos
have h : 0 < C_lock * (R / r0) ^ n := mul_pos hC hpow
linarith
theorem enhancement_strict_mono (R₁ R₂ r0 : ℝ) (hR₁ : 0 < R₁)
(hR₂ : R₁ < R₂) (hr0 : 0 < r0) (n : ℕ) (hn : 0 < n) :
w_radial R₁ r0 n < w_radial R₂ r0 n := by
unfold w_radial
have hC : 0 < C_lock := C_lock_pos
-- (R₁ / r0) ^ n < (R₂ / r0) ^ n
have hd1 : 0 < R₁ / r0 := div_pos hR₁ hr0
have hd_lt : R₁ / r0 < R₂ / r0 := by
have hinv : 0 < r0⁻¹ := inv_pos.mpr hr0
have : R₁ * r0⁻¹ < R₂ * r0⁻¹ := mul_lt_mul_of_pos_right hR₂ hinv
simpa [div_eq_mul_inv] using this
have hpow_lt : (R₁ / r0) ^ n < (R₂ / r0) ^ n :=
pow_lt_pow_left₀ hd_lt (le_of_lt hd1) (Nat.pos_iff_ne_zero.mp hn)
have hmul_lt : C_lock * (R₁ / r0) ^ n < C_lock * (R₂ / r0) ^ n := by
exact mul_lt_mul_of_pos_left hpow_lt hC
linarith
/-- For any positive lower threshold `M`, there exists a radius `R*` at
which the enhancement exceeds `M`. This formalises "asymptotic
divergence" of `w` along the witness sequence. -/
theorem enhancement_unbounded (r0 : ℝ) (hr0 : 0 < r0) (n : ℕ) (hn : 0 < n)
(M : ℝ) (hM : 0 < M) :
∃ R : ℝ, 0 < R ∧ M < w_radial R r0 n := by
unfold w_radial
-- choose R := r0 * (M / C_lock)^(1/n) + r0 ...
-- Simpler: pick R so that (R/r0)^n > M / C_lock, then C_lock*(R/r0)^n > M, so w > 1+M > M.
have hC : 0 < C_lock := C_lock_pos
-- Choose target u = max(1, M/C_lock + 1) for (R/r0)^n.
set u := M / C_lock + 1 with hu_def
have hu_pos : 0 < u := by
have : 0 < M / C_lock := div_pos hM hC
have : 0 < M / C_lock + 1 := by linarith
simpa [hu_def] using this
-- Pick R = r0 * u (so (R/r0)^1 = u, then (R/r0)^n ≥ u for u ≥ 1, n ≥ 1).
-- We need u ≥ 1 to make (·)^n monotone past 1.
refine ⟨r0 * (u + 1), ?pos, ?bound⟩
· have : 0 < u + 1 := by linarith
exact mul_pos hr0 this
· -- (R/r0) = u + 1 > 1
have hratio : (r0 * (u + 1)) / r0 = u + 1 := by
field_simp
have hge : 1 ≤ u + 1 := by linarith
-- (u+1)^n ≥ u + 1 for n ≥ 1
have hn_ne : n ≠ 0 := Nat.pos_iff_ne_zero.mp hn
have hpow_ge : u + 1 ≤ (u + 1) ^ n := by
have h₁ : (u + 1) ^ 1 = u + 1 := by ring
have h₂ : (u + 1) ^ 1 ≤ (u + 1) ^ n :=
pow_le_pow_right₀ hge (Nat.one_le_iff_ne_zero.mpr hn_ne)
simpa [h₁] using h₂
have hd_pow : (u + 1) ≤ ((r0 * (u + 1)) / r0) ^ n := by
simp [hratio]; exact hpow_ge
have : M < C_lock * (u + 1) := by
have hCu : C_lock * u = C_lock * (M / C_lock + 1) := by simp [hu_def]
have hexp : C_lock * (M / C_lock + 1) = M + C_lock := by
field_simp
have : C_lock * u = M + C_lock := by simp [hCu, hexp]
have hadd : M + C_lock < C_lock * (u + 1) := by
have hexp2 : C_lock * (u + 1) = C_lock * u + C_lock := by ring
rw [hexp2]
linarith
linarith
have hCprod : C_lock * (u + 1) ≤ C_lock * ((r0 * (u + 1)) / r0) ^ n :=
mul_le_mul_of_nonneg_left hd_pow (le_of_lt hC)
linarith
MODEL BTFRSlopeIdentity · IndisputableMonolith/Gravity/ILGAsymptoticEnhancement.lean
def BTFRSlopeIdentity : Prop :=
∀ (M Vflat a0 G : ℝ), 0 < M → 0 < Vflat → 0 < a0 → 0 < G →
(M = Vflat ^ 4 / (G * a0) ↔ M * (G * a0) = Vflat ^ 4)
What this page does not claim
The theorem does not derive the value β = 4 from physical principles. The theorem does not confirm the slope against astronomical data. The theorem does not prove that the ILG weight function applies to real galaxies.
Verify this page
Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:
$ lake env lean IndisputableMonolith/Gravity/ILGAsymptoticEnhancement.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)
A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.
Derived articles
This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red:
- How does the unformalized integration from acceleration to velocity proceed in the framework?
- What does the SPARC scorecard show for the numerical value of the BTFR slope?
- Does the ILG radial weight function itself follow from the forcing chain or is it an input?
- How does the framework's β = 4 compare to the measured scatter in the Tully-Fisher relation?
MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND
THEOREM btfr_slope_identity_iff · IndisputableMonolith/Gravity/ILGAsymptoticEnhancement.lean
theorem btfr_slope_identity_iff : BTFRSlopeIdentity := by intros M V a0 G _hM _hV ha0 hG have hpos : 0 < G * a0 := mul_pos hG ha0 have hne : (G * a0) ≠ 0 := ne_of_gt hpos constructor · intro h have : M * (G * a0) = (V ^ 4 / (G * a0)) * (G * a0) := by rw [h] rw [this, div_mul_cancel₀ _ hne] · intro h have : V ^ 4 = M * (G * a0) := h.symm rw [this, mul_div_assoc, div_self hne, mul_one]The declaration btfr_slope_identity_iff proves a purely algebraic equivalence. btfr_slope_identity_iff · IndisputableMonolith/Gravity/ILGAsymptoticEnhancement.leanTHEOREM enhancement_pos · enhancement_above_one · enhancement_strict_mono · enhancement_unbounded · IndisputableMonolith/Gravity/ILGAsymptoticEnhancement.lean
theorem enhancement_pos (R r0 : ℝ) (hR : 0 < R) (hr0 : 0 < r0) (n : ℕ) : 0 < w_radial R r0 n := by unfold w_radial have hpow : 0 ≤ (R / r0) ^ n := pow_nonneg (le_of_lt (div_pos hR hr0)) n have hC : 0 < C_lock := C_lock_pos have hCprod : 0 ≤ C_lock * (R / r0) ^ n := mul_nonneg (le_of_lt hC) hpow linariththeorem enhancement_above_one (R r0 : ℝ) (hR : 0 < R) (hr0 : 0 < r0) (n : ℕ) (hn : 0 < n) : 1 < w_radial R r0 n := by unfold w_radial have hpow : 0 < (R / r0) ^ n := pow_pos (div_pos hR hr0) n have hC : 0 < C_lock := C_lock_pos have h : 0 < C_lock * (R / r0) ^ n := mul_pos hC hpow linariththeorem enhancement_strict_mono (R₁ R₂ r0 : ℝ) (hR₁ : 0 < R₁) (hR₂ : R₁ < R₂) (hr0 : 0 < r0) (n : ℕ) (hn : 0 < n) : w_radial R₁ r0 n < w_radial R₂ r0 n := by unfold w_radial have hC : 0 < C_lock := C_lock_pos -- (R₁ / r0) ^ n < (R₂ / r0) ^ n have hd1 : 0 < R₁ / r0 := div_pos hR₁ hr0 have hd_lt : R₁ / r0 < R₂ / r0 := by have hinv : 0 < r0⁻¹ := inv_pos.mpr hr0 have : R₁ * r0⁻¹ < R₂ * r0⁻¹ := mul_lt_mul_of_pos_right hR₂ hinv simpa [div_eq_mul_inv] using this have hpow_lt : (R₁ / r0) ^ n < (R₂ / r0) ^ n := pow_lt_pow_left₀ hd_lt (le_of_lt hd1) (Nat.pos_iff_ne_zero.mp hn) have hmul_lt : C_lock * (R₁ / r0) ^ n < C_lock * (R₂ / r0) ^ n := by exact mul_lt_mul_of_pos_left hpow_lt hC linarith/-- For any positive lower threshold `M`, there exists a radius `R*` at which the enhancement exceeds `M`. This formalises "asymptotic divergence" of `w` along the witness sequence. -/ theorem enhancement_unbounded (r0 : ℝ) (hr0 : 0 < r0) (n : ℕ) (hn : 0 < n) (M : ℝ) (hM : 0 < M) : ∃ R : ℝ, 0 < R ∧ M < w_radial R r0 n := by unfold w_radial -- choose R := r0 * (M / C_lock)^(1/n) + r0 ... -- Simpler: pick R so that (R/r0)^n > M / C_lock, then C_lock*(R/r0)^n > M, so w > 1+M > M. have hC : 0 < C_lock := C_lock_pos -- Choose target u = max(1, M/C_lock + 1) for (R/r0)^n. set u := M / C_lock + 1 with hu_def have hu_pos : 0 < u := by have : 0 < M / C_lock := div_pos hM hC have : 0 < M / C_lock + 1 := by linarith simpa [hu_def] using this -- Pick R = r0 * u (so (R/r0)^1 = u, then (R/r0)^n ≥ u for u ≥ 1, n ≥ 1). -- We need u ≥ 1 to make (·)^n monotone past 1. refine ⟨r0 * (u + 1), ?pos, ?bound⟩ · have : 0 < u + 1 := by linarith exact mul_pos hr0 this · -- (R/r0) = u + 1 > 1 have hratio : (r0 * (u + 1)) / r0 = u + 1 := by field_simp have hge : 1 ≤ u + 1 := by linarith -- (u+1)^n ≥ u + 1 for n ≥ 1 have hn_ne : n ≠ 0 := Nat.pos_iff_ne_zero.mp hn have hpow_ge : u + 1 ≤ (u + 1) ^ n := by have h₁ : (u + 1) ^ 1 = u + 1 := by ring have h₂ : (u + 1) ^ 1 ≤ (u + 1) ^ n := pow_le_pow_right₀ hge (Nat.one_le_iff_ne_zero.mpr hn_ne) simpa [h₁] using h₂ have hd_pow : (u + 1) ≤ ((r0 * (u + 1)) / r0) ^ n := by simp [hratio]; exact hpow_ge have : M < C_lock * (u + 1) := by have hCu : C_lock * u = C_lock * (M / C_lock + 1) := by simp [hu_def] have hexp : C_lock * (M / C_lock + 1) = M + C_lock := by field_simp have : C_lock * u = M + C_lock := by simp [hCu, hexp] have hadd : M + C_lock < C_lock * (u + 1) := by have hexp2 : C_lock * (u + 1) = C_lock * u + C_lock := by ring rw [hexp2] linarith linarith have hCprod : C_lock * (u + 1) ≤ C_lock * ((r0 * (u + 1)) / r0) ^ n := mul_le_mul_of_nonneg_left hd_pow (le_of_lt hC) linarithThe surrounding formal development proves structural facts about the Information-Limited Gravity radial weight w(R) = 1 + C·(R/r0)<sup>α</sup>. enhancement_pos · enhancement_above_one · enhancement_strict_mono · enhancement_unbounded · IndisputableMonolith/Gravity/ILGAsymptoticEnhancement.leanMODEL BTFRSlopeIdentity · IndisputableMonolith/Gravity/ILGAsymptoticEnhancement.lean
def BTFRSlopeIdentity : Prop := ∀ (M Vflat a0 G : ℝ), 0 < M → 0 < Vflat → 0 < a0 → 0 < G → (M = Vflat ^ 4 / (G * a0) ↔ M * (G * a0) = Vflat ^ 4)The slope identity is recorded as a proposition, not derived. BTFRSlopeIdentity · IndisputableMonolith/Gravity/ILGAsymptoticEnhancement.lean