phi_critical_numeric

formal source

  40  unfold phi_critical_energy J_cost
  41  rfl
  42
  43theorem phi_critical_numeric : 0.09 < phi_critical_energy ∧ phi_critical_energy < 0.12 := by
  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. -/
  59theorem sc_prediction : 80 < T_critical ∧ T_critical < 120 := by
  60  unfold T_critical
  61  rw [phi_critical_value]
  62  have hphi_inv : phi⁻¹ = phi - 1 := by
  63    have hne : phi ≠ 0 := phi_pos.ne'
  64    have hsq := phi_sq_eq
  65    field_simp at hsq ⊢
  66    nlinarith [phi_pos]
  67  rw [hphi_inv]
  68  have h1 := phi_gt_onePointSixOne
  69  have h2 := phi_lt_onePointSixTwo
  70  constructor <;> nlinarith
  71
  72end IndisputableMonolith.CondensedMatter.JCostPhaseTransition