T2_substrate_pos

formal source

  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]
  93  exact div_lt_div_of_pos_left hT h_pow_pos h_lt
  94
  95/-! ## §3. The cross-class ratio is a φ-power -/
  96
  97/-- **STRUCTURAL THEOREM (F1)**: the ratio of decoherence times
  98    between two substrate classes at Z-rungs `k_a` and `k_b` is
  99    `φ^(k_b - k_a)` (treating the integer subtraction as `k_b - k_a`
 100    when `k_b ≥ k_a`).
 101
 102    Stated here with `k_b ≥ k_a` for non-negativity. -/
 103theorem T2_ratio_is_phi_power
 104    (T2_0 : ℝ) (k_a k_b : ℕ) (hT : 0 < T2_0) (h_le : k_a ≤ k_b) :
 105    T2_substrate T2_0 k_a / T2_substrate T2_0 k_b
 106      = Constants.phi ^ (k_b - k_a) := by
 107  unfold T2_substrate
 108  have h_phi_pos := Constants.phi_pos