Foundational reformulation

Foundational Reformulation is a seven-publication research program. It asks how much of geometry, quantum theory, and kinetic theory can be reconstructed from categorical locality and representation data, and which extra assumptions must be supplied.

Read the publication site or inspect the public source repository.

The program keeps the realization branches separate. A shared vocabulary does not make them one theorem. The claim register records what the repository proves, what it proves only from named assumptions, what it checks computationally, what is obstructed, and what remains open.

The papers carry the mathematical arguments. Lean checks exact formal subclaims and dependency records. Haskell exercises finite models and adversarial cases. Neither executable layer stands in for the analytic, geometric, or physical results stated in the manuscripts.

Publications

The program contains six source papers and a synthesis.

Part	Publication	Repository artifacts
I	Categorical Locality Before Spacetime: Axioms for Physical Contexts, Composition, and Descent	PDF, TeX, review
II	Condensed Physical Contexts: Topological, Distributional, and Infinite-Dimensional Structures Without Primitive Geometry	PDF, TeX, review
III	Representation-Theoretic Emergence of Measurement, Symmetry, and Observable Structure	PDF, TeX, review
IV	Lorentzian Geometry as a Realization: Coframes, Connections, Curvature, and Einstein Dynamics	PDF, TeX, review
V	Quantum Mechanics from Categorical Representations and Compositional Measurement	PDF, TeX, review
VI	Statistical Mechanics and the Boltzmann Equation from Categorical Coarse-Graining	PDF, TeX, review
Synthesis	Representation Before Geometry: A Categorical-Condensed Foundation for Geometry, Quantum Theory, and Statistical Physics	PDF, TeX, review

The paper manifest fixes the seven slugs, titles, and part labels. Acceptance of a paper review does not upgrade a scientific claim. Status changes require evidence for the exact registered statement.

How the program fits together

Papers I through III define the common language and its limits:

1. Paper I introduces physical contexts, composition, coverage, compatibility, and descent without taking a manifold or metric as primitive.
2. Paper II gives a controlled condensed realization for selected record fields. It keeps faithful realization separate from solidification and analytic localization.
3. Paper III studies compact-group reconstruction, observable interfaces, algebraic state averaging, outcome labels, and reference data. Probability and spacetime measurement remain separate inputs.

Papers IV through VI are separate downstream branches:

• Paper IV gives a conditional Lorentzian realization ladder. It distinguishes causal rigidity, the EPS route, clocks, metric scale, connections, curvature, action principles, boundary terms, and matter conservation.
• Paper V introduces an explicit operational bridge before applying finite quantum reconstruction results. It keeps CDP, Jordan-algebraic comparison, Born-rule representation, instruments, and interpretations at their proper scopes.
• Paper VI separates finite marginalization and collision algebra from propagation of chaos, scaling limits, collision-tree analysis, and kinetic partial differential equations.

The synthesis checks whether a proposed composition uses current evidence, compatible interfaces, named assumptions, and current reviews. Its authoring target is intentionally scoped to separate realizations. A theorem that all three branches arise from one common physical model would require a new joint model certificate.

Scientific status

The repository uses five uppercase labels. These words are part of the data model, not editorial shorthand.

Status	Meaning
PROVED	A complete mathematical proof is present, and its dependency audit reveals no hidden axiom or admitted bridge.
CONDITIONAL	A complete proof is present from named assumptions.
COMPUTATIONAL	Executable finite or numerical evidence is present.
OBSTRUCTED	A stated obstruction rules out the target under the current assumptions.
OPEN	The repository does not establish the target.

At the six-paper integration commit, the claim register contains 42 claims: 29 OPEN, 4 PROVED, 5 CONDITIONAL, 1 COMPUTATIONAL, and 3 OBSTRUCTED. The assumption ledger contains 78 assumptions, of which 77 are UNVALIDATED and 1 is ESTABLISHED at its exact syntactic scope. The counterexample register contains 49 active obstructions or failure witnesses.

Those counts can be reproduced directly from the closed Markdown tables:

awk -F'|' '
  /^\| (P[1-6]-C[0-9]+[a-z]?|PS-C[0-9]+) / {
    gsub(/^[[:space:]]+|[[:space:]]+$/, "", $5)
    claims += 1
    statuses[$5] += 1
  }
  END {
    print claims, "claims"
    for (status in statuses) print status, statuses[status]
  }
' research/claim-register.md

awk -F'|' '
  /^\| (P[1-6]-A[0-9]+|PS-A[0-9]+) / {
    gsub(/^[[:space:]]+|[[:space:]]+$/, "", $7)
    assumptions += 1
    states[$7] += 1
  }
  END {
    print assumptions, "assumptions"
    for (state in states) print state, states[state]
  }
' research/assumption-ledger.md

rg -c '^\| CE-(P[1-6]|PS)-[0-9]+ ' research/counterexample-register.md

The source ledger states exactly what each reference supports. A citation can constrain or motivate a claim, but it is not project evidence by association. The terminology guide and prior-art map keep names and comparison routes stable across papers.

Formal and executable scope

Lean and Haskell serve different purposes.

Layer	What it checks	What it does not establish
Lean	Exact finite algebra, typed interfaces, local theorems, status records, and dependency implications	The imported reconstruction theorems, existence of the physical realization bridges, or the joint physical model
Haskell	Finite constructions, malformed-input rejection, numerical tolerances, conservation checks, marginalization, and generated test cases	A mathematical proof, an infinite-system limit, a spacetime reconstruction, or a quantum reconstruction theorem
Papers and ledgers	Scientific statements, assumptions, literature hypotheses, counterexamples, and review state	Machine-checked formal proofs unless a claim points to a specific formal artifact

lake build means that the Lean project compiles. It does not by itself make a claim PROVED. The same boundary applies to the synthesis declarations that apply caller-supplied implications. Haskell tests receive the COMPUTATIONAL label only at the finite scope named in the claim register.

Reproduce the checks

Prerequisites

• Lean 4 is selected by lean-toolchain, currently v4.32.1. lakefile.lean pins mathlib to its matching release.
• GHC is fixed to 9.14.1 by cabal.project. The dependency closure is in cabal.project.freeze.
• The papers require a TeX installation with latexmk, BibTeX, and the packages imported by preamble.tex.
• The synthesis dependency graph uses Node.js and has no package installation step.

Fetch the Lean cache once, then compile the library and run every formal test with warnings treated as errors:

lake exe cache get
lake build

for file in FoundationalReformulationTest/*.lean; do
  lake env lean -DwarningAsError=true "$file"
done

Build the Haskell library, run the full test suite, and execute the finite demonstration:

cabal build all --ghc-options='-Wall -Wcompat -Werror'
cabal test all --test-show-details=direct
cabal run foundational-reformulation-demo

With the pinned GHC toolchain, the integrated suite reports 90 examples and 0 failures. QuickCheck runs 100 generated cases for each property in the default test configuration.

Build and validate the static research site:

npm run check

This runs the site contract tests, generates all seven publication pages plus the supporting routes, and rejects broken local links, missing semantic landmarks, unresolved math fallbacks, or incomplete responsive styles.

To rebuild one manuscript, run latexmk from the LaTeX directory and copy the result into the canonical PDF directory:

paper_slug=categorical-locality

(
  cd papers/latex
  latexmk -pdf -interaction=nonstopmode -halt-on-error "${paper_slug}.tex"
)

cp "papers/latex/${paper_slug}.pdf" "papers/pdf/${paper_slug}.pdf"
pdfinfo "papers/pdf/${paper_slug}.pdf" | rg '^Pages:'

Substitute any slug from papers/manifest.json.

Dependency graph release gate

The synthesis includes a generated, content-addressed graph at research/dependency-graph.v1.json. The generator reads the paper manifest, claim and assumption tables, source records, evidence artifacts, semantic terms, interfaces, and canonical reviews. The validator rejects stale artifacts, broken reciprocal links, unresolved identifiers, hard dependency cycles, incompatible interface types or terms, unsupported claim statuses, and tampered target closures.

Run the gate from the repository root after every change to a paper, ledger, review, formal artifact, or dependency edge:

node scripts/build-dependency-graph.mjs
node --test scripts/test-dependency-graph-validator.mjs
node scripts/validate-dependency-graph.mjs \
  --target TARGET-SYNTHESIS-AUTHORING \
  --tex papers/latex/synthesis.tex

The release candidate passes only when all 16 validator tests pass, the target reports PASS (SEPARATE_REALIZATIONS), and the validator ends with OVERALL: PASS. Regenerate and commit the graph after the final merge so its hashes refer to the exact released artifacts.

SAME_REALIZATION is a stronger scope. It must fail unless the graph contains relevant joint-model evidence and the target closure includes it. Separate branch certificates cannot be relabeled as a joint realization.

Repository map

Path	Contents
papers/latex/	Manuscript sources, shared preamble, and bibliography
papers/pdf/	Canonical compiled manuscripts
reviews/	Immutable review rounds, canonical reviews, and compliance audits
research/	Claims, assumptions, sources, counterexamples, terminology, prior art, and the synthesis graph
FoundationalReformulation/	Lean source modules
FoundationalReformulationTest/	Warning-as-error Lean test files
src/Foundational/	Haskell library modules
test/Spec.hs	Hspec and QuickCheck suite
site/	Static site generator, repair passes, validator, assets, and tests
coordination/	Decisions, open questions, review conflicts, and verification history

For a scientific change, update the claim and assumption records before changing the prose around them. Keep old IDs stable. If a statement changes materially, add a successor instead of reusing the old ID. Any artifact change that affects a reviewed claim makes the old review stale.

Publication endpoints

Purpose	Verified endpoint
Project website	foundational-reformulation.vercel.app
Public source repository	YonedaAI/foundational-reformulation
Versioned archive or DOI record	Not yet assigned

The website and repository links above were checked during release. No archive or DOI is claimed until a versioned record has been deposited and resolved.