`IndisputableMonolith.CondensedMatter.TopologicalPhasesStructure`

IndisputableMonolith/CondensedMatter/TopologicalPhasesStructure.lean · 23 lines · 3 declarations

Explainer status: ready · generated 2026-05-14 19:21:39.472916+00:00

   1import Mathlib
   2import IndisputableMonolith.CondensedMatter.StronglyCorrelatedElectronsStructure
   3
   4namespace IndisputableMonolith
   5namespace CondensedMatter
   6namespace TopologicalPhasesStructure
   7
   8open StronglyCorrelatedElectronsStructure
   9
  10def topological_phases_from_ledger : Prop := strongly_correlated_electrons_from_ledger
  11
  12theorem topological_phases_structure : topological_phases_from_ledger :=
  13  strongly_correlated_electrons_structure
  14
  15/-- Topological-phase structure implies strongly-correlated-electron input. -/
  16theorem topological_phases_implies_strongly_correlated (h : topological_phases_from_ledger) :
  17    strongly_correlated_electrons_from_ledger :=
  18  h
  19
  20end TopologicalPhasesStructure
  21end CondensedMatter
  22end IndisputableMonolith
  23

source mirrored from github.com/jonwashburn/shape-of-logic