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

phi_critical_numeric

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)

  43theorem phi_critical_numeric : 0.09 < phi_critical_energy ∧ phi_critical_energy < 0.12 := by

proof body

Tactic-mode proof.

  44  rw [phi_critical_value]
  45  have hphi_inv : phi⁻¹ = phi - 1 := by
  46    have hne : phi ≠ 0 := phi_pos.ne'
  47    have hsq := phi_sq_eq
  48    field_simp at hsq ⊢
  49    nlinarith [phi_pos]
  50  rw [hphi_inv]
  51  have h1 := phi_gt_onePointSixOne
  52  have h2 := phi_lt_onePointSixTwo
  53  constructor <;> linarith
  54
  55/-- **FALSIFIABLE PREDICTION**: Superconducting materials with phi-structured
  56    lattices will show critical temperatures T_c ~ 80-120 K when the coherence
  57    energy E_coh matches phi^(-5) ~ 0.09 eV. This predicts optimal doping
  58    occurs at carrier density n ~ 1/phi^2 ~ 0.38 per unit cell. -/

depends on (12)

Lean names referenced from this declaration's body.