IndisputableMonolith.Materials.MetamaterialBandGapFromPhiLadder

   1import Mathlib
   2import IndisputableMonolith.Constants
   3
   4/-!
   5# Photonic Metamaterial Band Gap on the Phi-Ladder
   6
   7Photonic metamaterials with golden-ratio lattice geometry (covered by
   8RS_PAT_018) exhibit a φ-laddered family of band gaps. The structural
   9prediction: the dimensionless gap-center frequency `ω_n / ω_0` lies on
  10the φ-ladder, with adjacent-rung ratios equal to exactly φ.
  11
  12This is the structural prediction underlying the patent. The empirical
  13observation: 1D Fibonacci photonic crystals exhibit a self-similar
  14gap-frequency cascade with the golden ratio as the fundamental scaling
  15constant (Maciá-Barber 2009, Wang et al. 2017).
  16
  17Lean status: 0 sorry, 0 axiom.
  18-/
  19
  20namespace IndisputableMonolith
  21namespace Materials
  22namespace MetamaterialBandGapFromPhiLadder
  23
  24open Constants
  25
  26noncomputable section
  27
  28/-- Reference band-gap center frequency (RS-native dimensionless 1). -/
  29def referenceFreq : ℝ := 1
  30
  31/-- Band-gap center at φ-ladder rung `k`. -/
  32def gapFreq (k : ℕ) : ℝ := referenceFreq * phi ^ k
  33
  34theorem gapFreq_pos (k : ℕ) : 0 < gapFreq k := by
  35  unfold gapFreq referenceFreq
  36  have : 0 < phi ^ k := pow_pos Constants.phi_pos k
  37  linarith [this]
  38
  39theorem gapFreq_succ_ratio (k : ℕ) :
  40    gapFreq (k + 1) = gapFreq k * phi := by
  41  unfold gapFreq
  42  rw [pow_succ]; ring
  43
  44theorem gapFreq_strictly_increasing (k : ℕ) :
  45    gapFreq k < gapFreq (k + 1) := by
  46  rw [gapFreq_succ_ratio]
  47  have hk : 0 < gapFreq k := gapFreq_pos k
  48  have hphi_gt_one : (1 : ℝ) < phi := by
  49    have := Constants.phi_gt_onePointFive; linarith
  50  have : gapFreq k * 1 < gapFreq k * phi :=
  51    mul_lt_mul_of_pos_left hphi_gt_one hk
  52  simpa using this
  53
  54theorem gapFreq_adjacent_ratio (k : ℕ) :
  55    gapFreq (k + 1) / gapFreq k = phi := by
  56  rw [gapFreq_succ_ratio]
  57  have hpos : 0 < gapFreq k := gapFreq_pos k
  58  field_simp [hpos.ne']
  59
  60structure MetamaterialBandGapCert where
  61  freq_pos : ∀ k, 0 < gapFreq k
  62  one_step_ratio : ∀ k, gapFreq (k + 1) = gapFreq k * phi
  63  strictly_increasing : ∀ k, gapFreq k < gapFreq (k + 1)
  64  adjacent_ratio_eq_phi : ∀ k, gapFreq (k + 1) / gapFreq k = phi
  65
  66/-- Metamaterial-band-gap-on-φ-ladder certificate. -/
  67def metamaterialBandGapCert : MetamaterialBandGapCert where
  68  freq_pos := gapFreq_pos
  69  one_step_ratio := gapFreq_succ_ratio
  70  strictly_increasing := gapFreq_strictly_increasing
  71  adjacent_ratio_eq_phi := gapFreq_adjacent_ratio
  72
  73end
  74end MetamaterialBandGapFromPhiLadder
  75end Materials
  76end IndisputableMonolith
  77