Haskell
Executable finite checks and counterexample contracts. They are not numerical simulations of the thermodynamic limit.
Executable research record
Code makes each theorem contract inspectable.
Haskell files test finite witnesses and reject invalid implications. Lean modules encode theorem interfaces and status boundaries. Reviews remain visible beside both.
Lean
Formal library representations and interfaces. Their status modules keep proved statements separate from open obligations.
Reviews
AGY reviews the papers. Claude independently reviews code and the formal artifacts.
Paper I
Uniform locality
Established under explicit F-norm hypotheses
Executable package
Lean
Canonical reviews
Paper II
Condensed observables
Established objectwise; categorical scope is explicit
Paper III
Thermodynamic gaps
Proposed packaging with established conditional analytic inputs
Executable package
Lean
Canonical reviews
Paper IV
Microscopic → effective
Controlled in free settings; a universal equivalence is open
Executable package
Lean
Canonical reviews
Paper V
Physical realizability
Explicit witnesses exist; general surjectivity is open
Executable package
Canonical reviews
Paper S
Phase spectrum program
Proposed spectrum; conditional assembly theorem
Executable package
Canonical reviews
Corpus-level audits