Bounded pilot · 16 August 2026

Compositional Foundations of Finite-Dimensional Classical Mechanics

Four papers ask one question: can finite-dimensional Hamiltonian mechanics be represented as an empirically interpreted compositional theory object, without conflating mathematical equivalence with physical equivalence? The pilot answers by exhibiting where the representation works, and by exhibiting the obstructions where it does not.

Thesis under investigation, not assumed: physics is the study of empirically realized compositional mathematical structures. The pilot was chartered to test this claim for precision, internal coherence, and compatibility with established finite-dimensional classical mechanics — and it reports that the thesis as stated is not itself a falsifiable physical hypothesis.
Founding thesis and charter, PRINCIPIA PHYSICA pilot context

4papers, PDF + LaTeX source
35typeset pages total
2representative formal companions
12epistemic labels on every claim
113labelled claim environments

What this pilot is, and what it is not

In scope

Finite-dimensional smooth classical systems: symplectic state spaces, observables, Hamiltonian dynamics, products and interconnection, symmetries, measurement maps, and empirical interpretation.

Boundary tests only

Field theory, infinite-dimensional analysis, general relativity, quantum mechanics, quantum field theory, theory-space geometry, and new experimental claims appear only as boundary tests. No new experimental claim is made anywhere in this pilot.

Three epistemic rules the papers are held to

Definitions, axioms, assumptions, conjectures, proved results, interpretations, and empirical statements are distinguished by label at the point of use.
Every substantial claim is proved, cited, an explicit empirical input, or marked conjectural.
Mathematical admissibility is never identified with physical realization.

Accepted outputs

The four papers

Three topic papers form a series; the fourth synthesizes them. Every paper is self-contained arXiv-style LaTeX with no external bibliography file; each carries its own embedded reference list. Both the compiled PDF and the exact LaTeX source that produced it are published here, with the SHA-256 recorded in the build receipt.

Paper I of III · 9 pages

Compositional Systems in Finite-Dimensional Classical Mechanics

A typed reconstruction of system, state, observable, process and composition. The symplectic product is monoidal but not cartesian: no projection, no diagonal. Centrally, “these two subsystems interact” is not an invariant of the triple (M,ω,H), so compositional structure is additional data fixed empirically by what an apparatus reads. Symplectic Hamiltonian systems are not closed under the operations physicists call composition; the closed class is the Dirac / port-Hamiltonian one.

PDF, Compositional Systems in Finite-Dimensional Classical Mechanics LaTeX source, Compositional Systems in Finite-Dimensional Classical Mechanics

PDF SHA-256
4a3ef75ce34accdd9674d4b7abb15c0708138cce4f154dd8d5d356d74716b1bf

Paper II of III · 9 pages

Hamiltonian Reconstruction as a Physical Theory Object

Finite-dimensional Hamiltonian mechanics reconstructed as a typed physical theory object, separating bare structure from an interpretation layer, with the results that make its slots well typed (nondegeneracy ⇔ uniqueness of the Hamiltonian vector field; Jacobi ⇔ closedness; conservation; Liouville; Noether). Three structural findings: dynamical composition is rigid, so “system ↦ dynamics” is no monoidal functor on the Cartesian product; interconnection is not morphism composition and its Lagrangian-relation replacement is partial, with four failure modes; and isomorphism underdetermines physical identity.

PDF, Hamiltonian Reconstruction as a Physical Theory Object LaTeX source, Hamiltonian Reconstruction as a Physical Theory Object

PDF SHA-256
05a68fd0b4375c30ee1f3938bbace49ea60801891dd47ae7acb3efd5df59c90a

Paper III of III · 10 pages

Empirical Realization, Observational Equivalence, and the Limits of Finite-Dimensional Classical Models

Two routinely conflated predicates are separated: mathematical admissibility, a unary predicate on symplectic model tuples, and empirical realization, a binary relation between models and finite-precision data records. They come apart both ways. Finite-precision observational equivalence is a tolerance relation — reflexive and symmetric but non-transitive, with transitive closure the total relation — so model space cannot be quotiented by it. Exact, complete data still leave an infinite-dimensional consistent family. The founding thesis as stated is shown not to be falsifiable, and the falsifiable sub-claim it contains is isolated.

PDF, Empirical Realization, Observational Equivalence, and the Limits of Finite-Dimensional Classical Models LaTeX source, Empirical Realization, Observational Equivalence, and the Limits of Finite-Dimensional Classical Models

PDF SHA-256
ae266285ea6dc962ed934a9483497312e8bc5f3fcc41f76b2bd6be6c5ae05b78

Synthesis · 7 pages

Synthesis, Obstructions, and an Empirical Contract

The three reconstructions are combined and the founding thesis is tested. A Hamiltonian theory object must include not only (M,ω,H) but selected preparations, observables, processes, decomposition, and a realization map. That enrichment prevents mathematical isomorphism from being mistaken for physical equivalence, and it exposes four obstructions. The usable residue of the thesis is an explicit empirical contract whose compositional clauses can fail — stated as six required entries, not as a slogan.

PDF, Synthesis, Obstructions, and an Empirical Contract LaTeX source, Synthesis, Obstructions, and an Empirical Contract

PDF SHA-256
5a6eda2e306dea2e90f451d84f883a13b9c670817e83ea1f6faf7270d5f8ea0b

The four obstructions the series exhibits

Canonical relations compose only partially; transversality can fail.
Interaction is not an invariant of (M,ω,H).
Symplectic Hamiltonian systems are not closed under ordinary interconnection.
Finite-precision observational equivalence is neither transitive nor a congruence.

Formal appendix

Representative formal companions

What these artifacts do and do not establish

The Lean and Haskell files below are representative formal companions to a single argument each. They are not a formalization of the papers, and they are not a proof of the founding thesis or of any complete result in the series. The Lean file formalizes the elementary metric content of one theorem — that finite-tolerance closeness is reflexive, symmetric, and not transitive — and deliberately does not encode empirical realization as a theorem. The Haskell file is an executable vocabulary: its types keep mathematical structure, empirical interpretation, and equivalence evidence apart, and it explicitly leaves smoothness, symplecticity, and Hamilton's equations as obligations on the values a user supplies. Reading either file as machine-checked support for the pilot's physical conclusions would be a misreading.

Lean 4.33.0 · 89 lines

Proofs.lean

Formalizes a pseudometric fragment, closeness at tolerance ε, and a concrete arithmetic witness — gravitational parameters 9.8, 9.9, 10.0 m s⁻² at a 0.2 m tolerance — showing that observational closeness fails transitivity. It also proves a conditional transitivity result: closeness is transitive under an explicit added gap hypothesis on the distance. That is a restriction, not a converse.

Checked with lean formal/lean/Proofs.lean, exit status 0, and scanned for sorry/admit placeholders with zero matches.

Read Proofs.lean

SHA-256
8b91f80211a76080156f176aa52cf60fae3bbb3fa09d97549bfa3bb1dd08384d

GHC 9.14.1 · 193 lines

Core.hs

An executable vocabulary for the appendix: observables, local flows that record leaving their domain rather than assuming completeness, bare models, procedures, interpretations, a non-interacting product and an explicit interaction, tolerance witnesses, and an equivalence certificate that refuses to call two models physically equivalent unless all four preservation flags hold — symplectic structure, Hamiltonian, dynamics and interpretation — and the list of known losses is empty.

Compiled with ghc -fno-code -Wall -Wextra -Werror plus further strictness flags, exit status 0, zero warnings.

Read Core.hs

SHA-256
41faecdc2dc68bc7e1f8b0d5b8d2e2a50e16ce466c18e841027a6af7f0439514

Epistemic contract

All twelve epistemic labels

The pilot contract requires that every claim carrying epistemic status in every paper is typed by one of twelve labels, all sharing a single counter so the type of a claim is visible where it is used. Counts below are occurrences of the corresponding environment across the four published LaTeX sources. Two further environments share that same counter and are not among the twelve: Counterexample (×10), which exhibits a witness against a claim, and Remark (×7), which carries no independent claim.

Definition ×14
Axiom ×5
Assumption ×14
Conjecture ×4
Lemma ×5
Proposition ×17
Theorem ×10
Corollary ×7
Interpretation ×6
Empirical statement ×7
Established physical result ×13
New result claimed by this work ×11

Assumptions and conjectures are not theorems; equivalence claims require an explicit preservation-and-loss analysis; and a mathematical construction is not physically realized until an empirical correspondence is supplied. Only eleven claims across the four papers are labelled New result claimed by this work, and of those the synthesis records that literature priority for the exact formulations of its two headline claims remains less certain than their correctness.

Adversarial review

Review evidence

All four review records are published unedited, including the two that did not accept. The synthesis review is kept in its original rejecting form; the recovery receipt records what was rebuilt in response rather than the review being rewritten after the fact. Note that the topic-series review was carried out against the pre-acceptance drafts, so the item numbers it cites are the drafts' numbering; the accepted papers published here were renumbered, and the reviewed results appear under different numbers.

Review records, as published in this bundle
Record	Verdict	Content
topic-series-review.json	ACCEPT	No blocking findings, no required changes. Three claim assessments supported: structural lemmas for Hamiltonian fields and Jacobi identities; the absence of Cartesian structure in the symplectic relation category; and finite-precision equivalence as a non-transitive tolerance relation. Seven counterexamples catalogued across the series.
synthesis-review.json	REJECT	Three blocking findings at the time of review: the synthesis paper, the Lean draft, and the Haskell draft were all unwritten after a native-team execution failure. This is the original record, retained as-is.
website-self-review.json	CHANGES REQUIRED	The unrepaired first-pass review of this website, published as written. Ten findings — one blocker, three major, six minor — raised by the build process and by two independent bounded reviewers, one for accessibility and navigation, one for research communication. Verdict `changes-required`, `accepted: false`. It is published beside the second-pass record, not replaced by it.
website-review.json	SITE	The second-pass review of this website, after every finding above was repaired in a single fix pass and re-checked. This record lists each finding, its fix, and the re-run check output.

How the rejection was resolved

The three blocked artifacts were rebuilt and re-verified: the synthesis paper now compiles to 7 pages, the Lean companion checks with no placeholders, and the Haskell companion compiles under strict warnings-as-errors. The recovery receipt records three repair agents with non-overlapping ownership, zero unresolved compiler or verifier errors, and a respected bounded review-and-fix limit. The rejecting review is not superseded or edited — it is published alongside the receipt that answers it.

Verification

Receipts

Each receipt records the tool, the exact command, and the observed exit status for a build or check that actually ran. Nothing here is a claim about correctness of the physics; these are records of mechanical checks.

Verification receipts published with this bundle
Receipt	Tools	Recorded result
latex.json	`latexmk 4.88`, pdfTeX 1.40.29, `pdfinfo 26.08.0`	All four papers built with exit status 0; 9 + 9 + 10 + 7 pages; per-paper SHA-256 for both source and PDF; no matching diagnostics in the final logs.
formal.json	Lean 4.33.0, GHC 9.14.1	Lean check exit 0 with zero `sorry`/`admit` matches; Haskell compile exit 0 with zero warnings under `-Werror`.
recovery.json	Three native repair agents	Non-overlapping ownership, all agents completed, zero unresolved compiler or verifier errors, bounded fix limit respected.
website.json	Chosen at build time; listed in the file itself	The tools actually used to build and validate this site, each with the command run and the exit status observed: HTML5 conformance, CSS grammar, an automated WCAG audit, a measured responsive-layout probe, image dimensions, and resolution of every relative link to a local target.

Everything in this bundle

Stated plainly

Limitations retained

These are carried forward from the synthesis paper rather than dropped in presentation. A limitation that survives review is part of the result.

No novel empirical prediction is produced anywhere in this pilot.
No total category of canonical relations is constructed; composition remains partial.
No universal interconnection operation is given.
No uniqueness theorem for reconstruction is proved; exact data do not in general identify a unique Hamiltonian.
Long-range forces, dissipation, singular constraints, and incomplete flows defeat common idealizations used in the scope.
Eleven claims across the four papers are labelled new. Of these, the synthesis records that literature priority for the exact formulations of its two headline claims is less certain than their correctness.
The Lean and Haskell files are representative companions to one argument each, not a formalization of the papers and not machine-checked support for the thesis.
Scope is finite-dimensional classical mechanics. Field theory, general relativity, and quantum theory appear only as boundary tests.

Colophon

This site is static and self-contained: one HTML file, one stylesheet, no JavaScript, no external fonts, no analytics, no network requests. Every link on this page resolves to a file inside this bundle. It can be read from a local checkout with no build step.

To inspect it locally, serve the website/ directory with any static server — for example python3 -m http.server — or open website/index.html directly in a browser.