IndisputableMonolith.CondensedMatter.HighTcSuperconductivityStructure

   1import Mathlib
   2import IndisputableMonolith.Constants
   3
   4namespace IndisputableMonolith
   5namespace CondensedMatter
   6namespace HighTcSuperconductivityStructure
   7
   8open Constants
   9
  10def high_tc_superconductivity_from_ledger : Prop := 1 < phi ∧ phi < 2
  11
  12theorem high_tc_superconductivity_structure : high_tc_superconductivity_from_ledger := by
  13  exact ⟨one_lt_phi, phi_lt_two⟩
  14
  15/-- High-Tc structure implies lower bound `1 < phi`. -/
  16theorem high_tc_implies_phi_gt_one (h : high_tc_superconductivity_from_ledger) : 1 < phi :=
  17  h.1
  18
  19/-- High-Tc structure implies upper bound `phi < 2`. -/
  20theorem high_tc_implies_phi_lt_two (h : high_tc_superconductivity_from_ledger) : phi < 2 :=
  21  h.2
  22
  23end HighTcSuperconductivityStructure
  24end CondensedMatter
  25end IndisputableMonolith
  26