kernel_ratio_dimensionless

formal source

 175/-! ## Dimensional Analysis -/
 176
 177/-- Kernel ratio is scale-invariant: the ratio a/(k τ₀) is dimensionless. -/
 178theorem kernel_ratio_dimensionless (lam : ℝ) (hlam : lam ≠ 0) (k a tau0 : ℝ) :
 179    (lam * a) / ((lam * k) * tau0) = a / (k * tau0) := by
 180  field_simp [hlam]
 181
 182/-! ## Self-Similarity Derivation of α -/
 183
 184/-- Structure encoding the self-similarity assumption for α derivation. -/
 185structure SelfSimilarKernel where
 186  /-- The kernel exponent -/
 187  alpha : ℝ
 188  /-- Self-similarity: kernel at scale φ·a equals kernel at a scaled by φ^α -/
 189  self_similar : ∀ (P : KernelParams) (k a : ℝ), P.alpha = alpha →
 190    kernel P k (phi * a) = 1 + P.C * phi ^ alpha * (max 0.01 (a / (k * P.tau0))) ^ alpha
 191
 192/-- From self-similarity and the fixed-point equation φ² = φ + 1,
 193    we can derive constraints on α. This is a placeholder for the full derivation. -/
 194theorem alpha_from_self_similarity (hSS : SelfSimilarKernel)
 195    (h_constraint : hSS.alpha = (1 - 1 / phi) / 2) :
 196    hSS.alpha = alphaLock := by
 197  simp [h_constraint, alphaLock]
 198
 199/-! ## Causality bounds (Beltracchi 2026 resolution)
 200
 201Two pathologies of the literal Riemann–Liouville / Fourier-only ILG formulation
 202were identified by P. Beltracchi (April 2026 internal note):
 203
 2041. **Cumulative-time growth.** Reading the time-domain RL form
 205   `ρ_eff(t) = ρ(t) + C τ₀⁻ᵅ Iᵅ[ρ(t)]` literally for an isolated mass `M`,
 206   the gravitational acceleration grows as `t^α` without bound.
 207
 2082. **Infrared divergence.** The Fourier-space kernel