IndisputableMonolith.Cost.FrequencyLadder

   1import Mathlib
   2import IndisputableMonolith.Constants
   3import IndisputableMonolith.Cost.JcostCore
   4
   5/-!
   6# φ-Ladder Frequency Bridge
   7
   8## Gap B Closure
   9
  10The J-cost function J(r) = ½(r + r⁻¹) − 1 evaluates the cost of any
  11positive ratio r. The golden ratio φ is the unique positive fixed point
  12of the self-similar recursion r = 1 + 1/r (i.e., r² = r + 1).
  13
  14This module proves that φ is the **minimal-cost non-trivial ratio**:
  15among all r > 1 satisfying the self-similarity equation, φ is the unique
  16positive root. Therefore, for any oscillating system at frequency f,
  17the first φ-harmonic f × φ is the minimal-cost resonance above f.
  18
  19This justifies the step in BodyCosmosResonance where we define
  20f_phi_rung1 := Mode1 × φ as the first φ-ladder harmonic.
  21-/
  22
  23namespace IndisputableMonolith
  24namespace Cost
  25namespace FrequencyLadder
  26
  27open Real
  28open IndisputableMonolith.Constants
  29
  30/-! ## J-Cost on Frequency Ratios -/
  31
  32/-- The J-cost of a frequency ratio r = f₂/f₁. -/
  33noncomputable def frequencyRatioCost (r : ℝ) : ℝ := Jcost r
  34
  35/-- J-cost of unit ratio is zero: equal frequencies have no cost. -/
  36theorem frequencyRatioCost_unit : frequencyRatioCost 1 = 0 := by
  37  unfold frequencyRatioCost Jcost; simp
  38
  39/-- J-cost is non-negative for positive ratios. -/
  40theorem frequencyRatioCost_nonneg {r : ℝ} (hr : 0 < r) :
  41    0 ≤ frequencyRatioCost r :=
  42  Jcost_nonneg hr
  43
  44/-! ## φ as Minimal-Cost Non-Trivial Ratio -/
  45
  46/-- A self-similar ratio satisfies r² = r + 1 (the defining equation of φ). -/
  47def IsSelfSimilarRatio (r : ℝ) : Prop := r ^ 2 = r + 1
  48
  49/-- φ is a self-similar ratio. -/
  50theorem phi_is_self_similar : IsSelfSimilarRatio phi := phi_sq_eq
  51
  52/-- φ is the UNIQUE positive self-similar ratio.
  53    Proof: r² = r + 1 and φ² = φ + 1 give (r−φ)(r+φ) = r−φ,
  54    so (r−φ)(r+φ−1) = 0. Since r > 0 and φ > 1, r+φ−1 > 0,
  55    so r = φ. -/
  56theorem phi_unique_self_similar {r : ℝ} (hr_pos : 0 < r)
  57    (hr_ss : IsSelfSimilarRatio r) : r = phi := by
  58  unfold IsSelfSimilarRatio at hr_ss
  59  have hphi_sq := phi_sq_eq
  60  have hphi_pos := phi_pos
  61  have hphi_gt1 := one_lt_phi
  62  have hdiff : (r - phi) * (r + phi - 1) = 0 := by nlinarith
  63  rcases mul_eq_zero.mp hdiff with h | h
  64  · linarith
  65  · exfalso; nlinarith
  66
  67/-- φ is the cost fixed point: φ = 1 + 1/φ.
  68    Follows directly from φ² = φ + 1. -/
  69theorem phi_cost_fixed_point : phi = 1 + 1 / phi := by
  70  have hsq := phi_sq_eq
  71  have hne := phi_ne_zero
  72  field_simp at hsq ⊢; linarith
  73
  74/-! ## The φ-Harmonic Theorem -/
  75
  76/-- For any positive frequency f, the first φ-harmonic is f × φ.
  77    This is the minimal-cost non-trivial resonance above f.
  78
  79    The forcing chain:
  80    1. J(r) is the cost of ratio r (from T5)
  81    2. Self-similar ratios (r² = r + 1) are the scale-invariant resonances
  82    3. φ is the unique positive self-similar ratio (from T6)
  83    4. Therefore f × φ is the unique first φ-harmonic of f -/
  84structure PhiHarmonicForced (f : ℝ) where
  85  harmonic : ℝ
  86  harmonic_eq : harmonic = f * phi
  87  ratio_is_phi : harmonic / f = phi
  88  ratio_self_similar : IsSelfSimilarRatio (harmonic / f)
  89  ratio_unique : ∀ r > 0, IsSelfSimilarRatio r → r = phi
  90
  91/-- The φ-harmonic is forced for any positive frequency. -/
  92noncomputable def phi_harmonic_forced {f : ℝ} (hf : 0 < f) : PhiHarmonicForced f where
  93  harmonic := f * phi
  94  harmonic_eq := rfl
  95  ratio_is_phi := by rw [mul_div_cancel_left₀ _ (ne_of_gt hf)]
  96  ratio_self_similar := by
  97    rw [mul_div_cancel_left₀ _ (ne_of_gt hf)]
  98    exact phi_is_self_similar
  99  ratio_unique := fun r hr_pos hr_ss => phi_unique_self_similar hr_pos hr_ss
 100
 101end FrequencyLadder
 102end Cost
 103end IndisputableMonolith
 104