IndisputableMonolith.Unification.RecognitionBandGeometry

   1import Mathlib
   2import IndisputableMonolith.Constants
   3
   4namespace IndisputableMonolith
   5namespace Unification
   6namespace RecognitionBandGeometry
   7
   8open Constants
   9
  10noncomputable section
  11
  12/-- The lower cognitive band boundary: `ρ_min = 1/φ²`. -/
  13def rhoBandLower : ℝ := phi⁻¹ ^ 2
  14
  15/-- The upper cognitive band boundary: `ρ_upper = 1/φ`. -/
  16def rhoBandUpper : ℝ := phi⁻¹
  17
  18theorem rhoBandLower_eq : rhoBandLower = phi⁻¹ ^ 2 := by
  19  rfl
  20
  21theorem rhoBandUpper_eq : rhoBandUpper = phi⁻¹ := by
  22  rfl
  23
  24theorem rhoBandUpper_pos : 0 < rhoBandUpper := by
  25  unfold rhoBandUpper
  26  exact inv_pos.mpr phi_pos
  27
  28theorem rhoBandUpper_lt_one : rhoBandUpper < 1 := by
  29  unfold rhoBandUpper
  30  exact inv_lt_one_of_one_lt₀ one_lt_phi
  31
  32theorem rhoBandLower_pos : 0 < rhoBandLower := by
  33  unfold rhoBandLower
  34  have h : 0 < phi⁻¹ := inv_pos.mpr phi_pos
  35  positivity
  36
  37theorem rhoBandLower_lt_one : rhoBandLower < 1 := by
  38  unfold rhoBandLower
  39  have hpos : 0 < phi⁻¹ := inv_pos.mpr phi_pos
  40  have hlt : phi⁻¹ < 1 := inv_lt_one_of_one_lt₀ one_lt_phi
  41  nlinarith
  42
  43theorem rhoBandLower_lt_rhoBandUpper : rhoBandLower < rhoBandUpper := by
  44  unfold rhoBandLower rhoBandUpper
  45  have hpos : 0 < phi⁻¹ := inv_pos.mpr phi_pos
  46  have hlt : phi⁻¹ < 1 := inv_lt_one_of_one_lt₀ one_lt_phi
  47  nlinarith
  48
  49/-- `1 - 1/φ = 1/φ²`, the golden complement relation. -/
  50theorem one_sub_phi_inv_eq_phi_inv_sq : 1 - phi⁻¹ = phi⁻¹ ^ 2 := by
  51  have hphi : phi ≠ 0 := phi_ne_zero
  52  have hphi_sq : phi ^ 2 = phi + 1 := phi_sq_eq
  53  field_simp [hphi]
  54  nlinarith [sq_pos_of_pos phi_pos, hphi_sq]
  55
  56/-- The two band boundaries sum to one. -/
  57theorem bandBoundaries_sum_to_one : rhoBandLower + rhoBandUpper = 1 := by
  58  unfold rhoBandLower rhoBandUpper
  59  have hphi : phi ≠ 0 := phi_ne_zero
  60  have hphi_sq : phi ^ 2 = phi + 1 := phi_sq_eq
  61  field_simp [hphi]
  62  nlinarith [sq_pos_of_pos phi_pos, hphi_sq]
  63
  64theorem one_sub_rhoBandLower_eq_rhoBandUpper : 1 - rhoBandLower = rhoBandUpper := by
  65  linarith [bandBoundaries_sum_to_one]
  66
  67theorem one_sub_rhoBandUpper_eq_rhoBandLower : 1 - rhoBandUpper = rhoBandLower := by
  68  linarith [bandBoundaries_sum_to_one]
  69
  70/-- At the lower boundary, `ρ/(1-ρ) = 1/φ`. -/
  71theorem bandLower_ratio : rhoBandLower / (1 - rhoBandLower) = phi⁻¹ := by
  72  rw [one_sub_rhoBandLower_eq_rhoBandUpper]
  73  unfold rhoBandLower rhoBandUpper
  74  field_simp [phi_ne_zero]
  75
  76/-- At the upper boundary, `ρ/(1-ρ) = φ`. -/
  77theorem bandUpper_ratio : rhoBandUpper / (1 - rhoBandUpper) = phi := by
  78  rw [one_sub_rhoBandUpper_eq_rhoBandLower]
  79  unfold rhoBandLower rhoBandUpper
  80  field_simp [phi_ne_zero]
  81
  82theorem bandBoundaries_product : rhoBandLower * rhoBandUpper = phi⁻¹ ^ 3 := by
  83  unfold rhoBandLower rhoBandUpper
  84  ring
  85
  86end
  87end RecognitionBandGeometry
  88end Unification
  89end IndisputableMonolith
  90