IndisputableMonolith.NavierStokes.PhiOptimalCascade

   1import Mathlib
   2import IndisputableMonolith.Constants
   3import IndisputableMonolith.NavierStokes.PhiLadderCutoff
   4
   5/-!
   6# φ as the Unique Optimal Cascade Ratio
   7
   8This module formalizes a simplified variational model for the φ-ladder.
   9The idea is to measure the failure of a geometric ratio `r > 1` to satisfy the
  10self-similar closure relation `r^2 = r + 1`. The canonical cost of that defect
  11is minimized exactly at `r = φ`.
  12-/
  13
  14namespace IndisputableMonolith
  15namespace NavierStokes
  16namespace PhiOptimalCascade
  17
  18open Constants
  19open PhiLadderCutoff
  20
  21noncomputable section
  22
  23/-- Self-similarity defect ratio for a geometric cascade. -/
  24def selfSimilarityDefect (r : ℝ) : ℝ :=
  25  r ^ 2 / (r + 1)
  26
  27/-- Simplified cascade cost: the J-cost of the self-similarity defect. -/
  28def simplifiedCascadeCost (r : ℝ) : ℝ :=
  29  Jcost (selfSimilarityDefect r)
  30
  31theorem selfSimilarityDefect_pos {r : ℝ} (hr : 1 < r) :
  32    0 < selfSimilarityDefect r := by
  33  unfold selfSimilarityDefect
  34  positivity
  35
  36theorem selfSimilarityDefect_phi : selfSimilarityDefect phi = 1 := by
  37  unfold selfSimilarityDefect
  38  have hphi1 : phi + 1 ≠ 0 := by linarith [phi_pos]
  39  rw [phi_sq_eq]
  40  field_simp [hphi1]
  41
  42theorem simplifiedCascadeCost_phi : simplifiedCascadeCost phi = 0 := by
  43  unfold simplifiedCascadeCost
  44  rw [selfSimilarityDefect_phi]
  45  exact Jcost_one
  46
  47theorem selfSimilarityDefect_eq_one_iff {r : ℝ} (hr : 1 < r) :
  48    selfSimilarityDefect r = 1 ↔ r ^ 2 = r + 1 := by
  49  unfold selfSimilarityDefect
  50  have hr1 : r + 1 ≠ 0 := by linarith
  51  constructor
  52  · intro h
  53    field_simp [hr1] at h
  54    linarith
  55  · intro h
  56    rw [h]
  57    field_simp [hr1]
  58
  59theorem positive_root_unique_above_one {r : ℝ} (hr : 1 < r)
  60    (hroot : r ^ 2 = r + 1) : r = phi := by
  61  have hroot0 : r ^ 2 - r - 1 = 0 := by nlinarith [hroot]
  62  have hphi0 : phi ^ 2 - phi - 1 = 0 := by nlinarith [phi_sq_eq]
  63  by_contra hneq
  64  rcases lt_or_gt_of_ne hneq with hlt | hgt
  65  · have hmono : r ^ 2 - r - 1 < phi ^ 2 - phi - 1 := by
  66      nlinarith [hr, one_lt_phi, hlt]
  67    nlinarith
  68  · have hmono : phi ^ 2 - phi - 1 < r ^ 2 - r - 1 := by
  69      nlinarith [hr, one_lt_phi, hgt]
  70    nlinarith
  71
  72theorem simplifiedCascadeCost_eq_zero_iff {r : ℝ} (hr : 1 < r) :
  73    simplifiedCascadeCost r = 0 ↔ r = phi := by
  74  have hpos : 0 < selfSimilarityDefect r := selfSimilarityDefect_pos hr
  75  constructor
  76  · intro h
  77    have hdefect : selfSimilarityDefect r = 1 :=
  78      (Jcost_eq_zero_iff hpos).mp h
  79    exact positive_root_unique_above_one hr ((selfSimilarityDefect_eq_one_iff hr).mp hdefect)
  80  · intro h
  81    rw [h]
  82    exact simplifiedCascadeCost_phi
  83
  84theorem simplifiedCascadeCost_nonneg {r : ℝ} (hr : 1 < r) :
  85    0 ≤ simplifiedCascadeCost r := by
  86  unfold simplifiedCascadeCost
  87  exact Jcost_nonneg (selfSimilarityDefect_pos hr)
  88
  89/-- φ is the unique minimizer of the simplified cascade cost on `(1, ∞)`. -/
  90theorem phi_is_unique_optimal_ratio {r : ℝ} (hr : 1 < r) :
  91    simplifiedCascadeCost phi ≤ simplifiedCascadeCost r ∧
  92    (simplifiedCascadeCost r = simplifiedCascadeCost phi ↔ r = phi) := by
  93  have hnonneg : 0 ≤ simplifiedCascadeCost r := simplifiedCascadeCost_nonneg hr
  94  constructor
  95  · simpa [simplifiedCascadeCost_phi] using hnonneg
  96  · constructor
  97    · intro heq
  98      have hz : simplifiedCascadeCost r = 0 := by
  99        simpa [simplifiedCascadeCost_phi] using heq
 100      exact (simplifiedCascadeCost_eq_zero_iff hr).mp hz
 101    · intro h
 102      rw [h]
 103
 104end
 105
 106end PhiOptimalCascade
 107end NavierStokes
 108end IndisputableMonolith
 109