pith. machine review for the scientific record. sign in
theorem proved tactic proof

T2_substrate_strictly_decreasing

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  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

proof body

Tactic-mode proof.

  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. -/

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (21)

Lean names referenced from this declaration's body.