def
definition
galactic_constraint
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Gravity.GravityParameters on GitHub at line 196.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
193
194/-- The "galactic constraint number": 2N_τ - N_r ≈ 158.5
195 This determines the acceleration scale exponent. -/
196def galactic_constraint : ℝ := 2 * N_tau_galactic - N_r_galactic
197
198/-- The φ-ladder rung for the galactic memory timescale (integer approximation). -/
199def N_galactic : ℝ := 142
200
201/-- The timescale constraint linking a₀ and r₀.
202 Given τ★ and r₀, the acceleration scale is forced. -/
203def a0_from_tau_r0 (tau_star r0 : ℝ) : ℝ := 2 * Real.pi * r0 / tau_star ^ 2
204
205/-- The timescale constraint linking a₀ and r₀.
206 Given τ★ and a₀, the length scale is forced. -/
207def r0_from_tau_a0 (tau_star a0 : ℝ) : ℝ := a0 * tau_star ^ 2 / (2 * Real.pi)
208
209theorem tau_constraint_consistency (tau_star r0 a0 : ℝ)
210 (hτ : tau_star ≠ 0) (ha : a0 = a0_from_tau_r0 tau_star r0) :
211 r0 = r0_from_tau_a0 tau_star a0 := by
212 unfold a0_from_tau_r0 r0_from_tau_a0 at *
213 rw [ha]
214 have hτ2 : tau_star ^ 2 ≠ 0 := pow_ne_zero 2 hτ
215 field_simp [hτ2]
216
217/-- **THEOREM: φ-Ladder Formula for a₀**
218
219 In φ-ladder coordinates, a₀ is determined by the rungs:
220 a₀ = 2π·c/τ₀ · φ^(N_r - 2N_τ)
221
222 **Derivation**:
223 If τ★ = τ₀·φ^N_τ and r₀ = ℓ₀·φ^N_r (where ℓ₀ = c·τ₀), then:
224
225 a₀ = 2π r₀/τ★² = 2π·(ℓ₀·φ^N_r)/(τ₀·φ^N_τ)²
226 = 2π·(c·τ₀·φ^N_r)/(τ₀²·φ^(2N_τ))