peak_3_2_ratio

formal source

  60  k_peak_adjacent_ratio k_0 1 h
  61
  62/-- The third-to-second peak ratio is `φ`. -/
  63theorem peak_3_2_ratio (k_0 : ℝ) (h : 0 < k_0) :
  64    k_peak k_0 3 / k_peak k_0 2 = phi :=
  65  k_peak_adjacent_ratio k_0 2 h
  66
  67/-- The third-to-first peak ratio is `φ²`. -/
  68theorem peak_3_1_ratio (k_0 : ℝ) (h : 0 < k_0) :
  69    k_peak k_0 3 / k_peak k_0 1 = phi ^ 2 := by
  70  unfold k_peak
  71  have h_phi_ne : phi ≠ 0 := ne_of_gt phi_pos
  72  have h_k0_ne : k_0 ≠ 0 := ne_of_gt h
  73  field_simp
  74
  75/-- The peak ratios are independent of the base scale `k_0`. -/
  76theorem peak_ratios_scale_invariant
  77    (k_0 k_0' : ℝ) (n m : ℕ) (h : 0 < k_0) (h' : 0 < k_0') :
  78    k_peak k_0 (n + m) / k_peak k_0 n = k_peak k_0' (n + m) / k_peak k_0' n := by
  79  unfold k_peak
  80  have h_phi_ne : phi ≠ 0 := ne_of_gt phi_pos
  81  have h_k0_ne : k_0 ≠ 0 := ne_of_gt h
  82  have h_k0'_ne : k_0' ≠ 0 := ne_of_gt h'
  83  have h_pow_n_ne : phi ^ n ≠ 0 := pow_ne_zero n h_phi_ne
  84  -- Both sides simplify to phi^m.
  85  have h_lhs : k_0 * phi ^ (n + m) / (k_0 * phi ^ n) = phi ^ m := by
  86    rw [pow_add]; field_simp
  87  have h_rhs : k_0' * phi ^ (n + m) / (k_0' * phi ^ n) = phi ^ m := by
  88    rw [pow_add]; field_simp
  89  rw [h_lhs, h_rhs]
  90
  91/-- **STRUCTURE FORMATION FROM BIT MASTER CERTIFICATE (Track F4).** -/
  92structure StructureFormationFromBITCert where
  93  k_pos : ∀ k_0 n, 0 < k_0 → 0 < k_peak k_0 n