theorem
proved
T2_substrate_strictly_decreasing
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.QuantumComputing.DecoherenceFromBIT on GitHub at line 84.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
-
of -
one_lt_phi -
power -
Constants -
of -
is -
of -
as -
is -
of -
for -
is -
of -
Z -
is -
and -
one_lt_phi -
one_lt_phi -
Z -
two -
T2_substrate
used by
formal source
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
109 have h_phi_ne_zero : Constants.phi ≠ 0 := ne_of_gt h_phi_pos
110 have h_pow_a_ne : Constants.phi ^ k_a ≠ 0 := pow_ne_zero k_a h_phi_ne_zero
111 have h_pow_b_ne : Constants.phi ^ k_b ≠ 0 := pow_ne_zero k_b h_phi_ne_zero
112 have hT_ne : T2_0 ≠ 0 := ne_of_gt hT
113 -- Step 1: rewrite the LHS as φ^k_b / φ^k_a.
114 have h_lhs : T2_0 / Constants.phi ^ k_a / (T2_0 / Constants.phi ^ k_b)