ESTABLISHED
Uniform locality
The analytic first arrow
Uniform interaction norms, not profiniteness, give parameter-independent Lieb-Robinson bounds. Thermodynamic dynamics also require a uniform vanishing tail.
Condensed mathematics × quantum matter
Where does a topological phase become a theorem?
A six-paper research program tracks the exact obligations between local Hamiltonians, uniform gaps, stabilized phases, and an invertible condensed phase spectrum.
The five-stage program
A spectral flow with its gap exposed
The coral notch marks the gapless transition locus. It is a boundary to analyze, not a categorical shortcut.
The arrows define the research program. They are not assertions of equivalence.
Claim-status ledger
What is proved, and what is not
Conditions stay in the scope column. Epistemic labels use the corpus-wide vocabulary exactly.
IDStatusClaimScope
A.1ESTABLISHEDUniform interaction norms imply uniform Lieb-Robinson estimates.Under the stated summability and convolution hypotheses on F.
A.2ESTABLISHEDC(S,A) carries pointwise positivity and the supremum C*-norm.For compact Hausdorff S and a fixed C*-algebra A.
A.3ESTABLISHEDA uniformly gapped locus supports stable spectral flow.Requires a common gap and the relevant locality/stability assumptions.
C.1OPENControlled microscopic systems map to effective invariants.Established in selected free and low-dimensional settings, not universally.
P.1PROPOSEDThe stabilized invertible sector defines a condensed spectrum.Descent, coherences, and comparison maps remain research obligations.
Five papers + synthesis
The research corpus
Read each paper as HTML, open the canonical PDF, and inspect its matching executable and formal artifacts.
ESTABLISHED
Condensed observables
Positivity, C*-norms, and descent
Section algebras preserve fiberwise positivity and the supremum C*-norm while separating analytic structure from bare condensed algebra.
PROPOSED
Thermodynamic gaps
Witnesses, images, and stability
A quantitative gap witness is data; the qualitative uniformly gapped locus is its propositional image, conditional on analytic input.
OPEN
Microscopic → effective
Three maps, not one equivalence
Functional calculus gives a controlled free-fermion map to K-theory, while scaling, classification, and inverse realization remain distinct.
OPEN
Physical realizability
From abstract class to lattice witness
Kitaev, BDI, and AKLT models verify concrete low-dimensional rows without claiming every bordism or homotopy class is realizable.
PROPOSED
Phase spectrum program
Conditional assembly and claim-status ledger
The synthesis keeps the five-stage program precise: solid analytic inputs, conditional categorical assembly, and no unproved spectrum comparison.
Executable research record
Claims paired with things you can inspect
Haskell files
Finite witnesses and contract checks that reject known false inferences.
Lean modules
Library interfaces that formalize the program without overstating results.
Review tracks
AGY paper review and independent Claude code review for each paper.