rsKernelParams_C

formal source

 165    (rsKernelParams tau0 h).alpha = alphaLock := rfl
 166
 167/-- The RS-canonical C equals φ^(-3/2). -/
 168@[simp] theorem rsKernelParams_C (tau0 : ℝ) (h : 0 < tau0) :
 169    (rsKernelParams tau0 h).C = phi ^ (-(3 : ℝ) / 2) := rfl
 170
 171/-- The eight-tick C equals 49/162. -/
 172@[simp] theorem eightTickKernelParams_C (tau0 : ℝ) (h : 0 < tau0) :
 173    (eightTickKernelParams tau0 h).C = 49 / 162 := rfl
 174
 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