`phiRungScale_pos`

proved

show as: view math explainer →

module: IndisputableMonolith.NavierStokes.PhiLadderCutoff
domain: NavierStokes
line: 80 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.NavierStokes.PhiLadderCutoff on GitHub at line 80.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

formal source

  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⟩
 108
 109/-- Cascade depth is monotone in Reynolds number. -/
 110theorem cascadeDepth_mono {re₁ re₂ : ℝ} (h1 : 1 < re₁) (h2 : re₁ ≤ re₂) :

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.