theorem proved term proof

`high_tc_implies_phi_gt_one`

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

formal statement (Lean)

  16theorem high_tc_implies_phi_gt_one (h : high_tc_superconductivity_from_ledger) : 1 < phi :=

Term-mode proof.

  17  h.1
  18
  19/-- High-Tc structure implies upper bound `phi < 2`. -/

Lean names referenced from this declaration's body.

high_tc_superconductivity_from_ledger in IndisputableMonolith.CondensedMatter.HighTcSuperconductivityStructure decl_use