topological_phases_structure
plain-language theorem explainer
Topological phases structure holds by direct reduction to the strongly correlated electrons structure within the ledger framework for condensed matter. Physicists modeling topological insulators or fractional quantum Hall states would cite this result to connect phase topology to electron correlations. The proof is a one-line term application of the upstream strongly_correlated_electrons_structure theorem.
Claim. The proposition that topological phases follow from the ledger equals the proposition that strongly correlated electrons follow from the ledger: topological phases from ledger holds because strongly correlated electrons from ledger holds.
background
In module CondensedMatter.TopologicalPhasesStructure, topological_phases_from_ledger is defined as the Prop strongly_correlated_electrons_from_ledger. This sits inside the Recognition Science ledger construction for condensed matter, where structures are chained from upstream electron and glass-transition inputs. The upstream theorem strongly_correlated_electrons_structure asserts strongly_correlated_electrons_from_ledger via glass_transition_structure. Related phase definitions appear in depends-on edges: EightTick.phase gives the eight discrete phases kπ/4 for k in Fin 8, and RiemannHypothesis.Wedge.phase supplies the unimodular complex exponential e^{i w}.
proof idea
The proof is a one-line term wrapper that directly applies the theorem strongly_correlated_electrons_structure. No tactics or additional reductions are used; the term supplies the required Prop by the upstream equality of the two ledger propositions.
why it matters
This theorem supplies the topological-phases entry point in the condensed-matter ledger chain and feeds the implication toward strongly correlated electrons. It aligns with the T7 eight-tick octave and the overall forcing chain T0-T8 that derives D=3 spatial dimensions. No downstream uses are recorded, so the declaration functions as a structural bridge rather than an active lemma in further proofs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.