omega_BIT_band

formal source

  59  linarith
  60
  61/-- The BIT carrier frequency is in the band `(7.5, 8.1)`. -/
  62theorem omega_BIT_band : (7.5 : ℝ) < omega_BIT ∧ omega_BIT < 8.1 := by
  63  unfold omega_BIT
  64  have h1 := Constants.phi_gt_onePointFive  -- φ > 1.5
  65  have h2 := Constants.phi_lt_onePointSixTwo -- φ < 1.62
  66  refine ⟨?_, ?_⟩
  67  · nlinarith
  68  · nlinarith
  69
  70/-! ## §2. Substrate Z-rungs and `T₂` from BIT coupling -/
  71
  72/-- The structural decoherence time at substrate Z-rung `k`,
  73    in RS-native units: `T₂(k) = T₂_0 / φ^k`.  Higher Z-rung →
  74    stronger BIT coupling → faster decoherence. -/
  75def T2_substrate (T2_0 : ℝ) (k : ℕ) : ℝ := T2_0 / Constants.phi ^ k
  76
  77/-- `T₂_substrate` is positive when `T₂_0` is positive. -/
  78theorem T2_substrate_pos (T2_0 : ℝ) (k : ℕ) (hT : 0 < T2_0) :
  79    0 < T2_substrate T2_0 k := by
  80  unfold T2_substrate
  81  exact div_pos hT (pow_pos Constants.phi_pos k)
  82
  83/-- `T₂_substrate` is strictly decreasing in `k`. -/
  84theorem T2_substrate_strictly_decreasing (T2_0 : ℝ) (k : ℕ) (hT : 0 < T2_0) :
  85    T2_substrate T2_0 (k + 1) < T2_substrate T2_0 k := by
  86  unfold T2_substrate
  87  have h_pow_pos : 0 < Constants.phi ^ k := pow_pos Constants.phi_pos k
  88  have h_pow_succ_pos : 0 < Constants.phi ^ (k + 1) := pow_pos Constants.phi_pos (k + 1)
  89  have h_phi := Constants.one_lt_phi
  90  have h_lt : Constants.phi ^ k < Constants.phi ^ (k + 1) := by
  91    rw [pow_succ]
  92    nlinarith [h_pow_pos, h_phi]