phiRungScale

formal source

  74/-! ## The φ-Ladder Cascade -/
  75
  76/-- The scale at φ-rung n, relative to the voxel scale ℓ₀. -/
  77def phiRungScale (n : ℕ) : ℝ := phi ^ n
  78
  79/-- φ-rung scales are positive. -/
  80theorem phiRungScale_pos (n : ℕ) : 0 < phiRungScale n :=
  81  pow_pos phi_pos n
  82
  83/-- φ-rung scales are strictly increasing: m < n → φᵐ < φⁿ. -/
  84theorem phiRungScale_strictMono : StrictMono phiRungScale := by
  85  intro a b hab
  86  exact pow_lt_pow_right₀ one_lt_phi hab
  87
  88/-- φ-rung scale at n+1 equals φ times the scale at n. -/
  89theorem phiRungScale_succ (n : ℕ) :
  90    phiRungScale (n + 1) = phi * phiRungScale n := by
  91  unfold phiRungScale; rw [pow_succ]; ring
  92
  93/-! ## Cascade Depth -/
  94
  95/-- The cascade depth: N_d = ⌊(3/4) · ln(Re) / ln(φ)⌋. -/
  96def cascadeDepth (re : ℝ) : ℕ :=
  97  if 1 < re then
  98    Nat.floor ((3/4 : ℝ) * Real.log re / Real.log phi)
  99  else 0
 100
 101/-- The cascade depth is zero for Re ≤ 1. -/
 102theorem cascadeDepth_le_one {re : ℝ} (h : re ≤ 1) : cascadeDepth re = 0 := by
 103  unfold cascadeDepth; simp [not_lt.mpr h]
 104
 105/-- The cascade depth is always a concrete natural number. -/
 106theorem cascadeDepth_finite (re : ℝ) : ∃ N : ℕ, cascadeDepth re = N :=
 107  ⟨cascadeDepth re, rfl⟩