Roadmap

Quantum mechanics works extraordinarily well. What it does not yet give us is a clear account of why a single experiment produces one definite outcome, why the observed frequencies follow the Born rule, and how those features might fit into a deeper deterministic picture.

Constraint-Surface Dynamics is a research programme built to tackle those questions in order. It does not try to solve everything at once. It starts with the narrowest question that can be made precise, closes that step, then moves to the next. The roadmap below shows that sequence, and where each stage actually stands.

The destination

The long-term goal is a complete geometric framework in which:

  • physical systems evolve deterministically on an underlying state space (Sigma)

  • observed probabilities arise from geometry and symmetry, not primitive randomness

  • the standard finite-dimensional quantum formalism is recovered as an effective layer

  • the framework can then be extended, carefully, toward continuum physics and field theory

That is the full ambition. The finite-dimensional part of it is now largely built.

Where the programme is now

The finite-dimensional reconstruction is machine-verified. Stages 1 to 4 below are complete in the Lean corpus, which stands at 438 files and roughly 104,000 lines. It is free of sorry, and every theorem reports only Lean's three foundational axioms under #print axioms, enforced per theorem by pinned checks in continuous integration. No mathematical result is imported as an axiom.

What that means concretely: Schrödinger evolution, the Born rule, measurement as a physical process, and the post-measurement state update are theorems of the geometric model rather than postulates.

The work now sits at the boundary between the finite-dimensional reconstruction and the continuum. Early continuous-variable modules exist. The field-theoretic extension does not.

The roadmap

1. Establish deterministic statistics

Question: how can a deterministic theory produce stable outcome frequencies?

If the ontic dynamics preserve volume, and repeated runs begin from a preparation region, long-run frequencies converge to normalised volume weights. Without this step, probability would have to be put in by hand.

Status: complete. Paper A, and LF1 in Lean.

2. Fix the probability rule

Question: why should those weights match the Born rule?

Symmetry and operational consistency identify the relevant projective-space measure and recover the quadratic probability rule in finite dimension. This is the step that turns generic geometric weights into the specific rule quantum mechanics uses.

Status: complete, and formalised. Paper B and TN1 at the paper level. LF2 gives the measure bridge and Born-weight wrapper in Lean, published April 2026. The stronger result came later: in LF4, Born weights are derived as Fubini-Study volume ratios by way of the moment map and Duistermaat-Heckman, for every dimension and for general POVM measurements.

3. Reconstruct finite-dimensional quantum mechanics

Question: can the standard finite-dimensional formalism be recovered from deterministic geometry?

The projection from ontic space to projective state space, the quantum-effective sector, and the operational architecture of finite-dimensional quantum mechanics.

Status: complete. This is the largest layer in the corpus. Composite systems are no longer an open item: the tensor product is derived rather than assumed, from locality and local tomography, with the reconstruction theorem giving the dimension result. The residual assumption is local tomography itself, which is stated openly and is not derivable, since general probabilistic theories that fail it exist.

Mixed states, POVMs, reduced states and sequential update are all inside the same framework.

4. Give a physical account of measurement and outcomes

Question: what physically determines the one outcome we actually observe?

Status: complete, and this is the part that changed most. Measurement is no longer only a conceptual proposal. An explicit volume-preserving interaction creates a record from an apparatus-ready state, the record persists, distinct outcomes exclude one another, and the resulting statistics are exactly Born. The Lüders rule, that is wavefunction collapse, falls out as a pushforward of the dynamics rather than being postulated. The apparatus never destroys information: what looks like collapse is relocation with storage.

No-signalling holds dynamically, in every basis. Mixed preparations reproduce Tr(rho E) through the same dynamics. The quantum eraser runs as a process, restoring fringes only before a record exists and never after.

A trade-off theorem sits underneath all of this, and it is one of the programme's more interesting results. A machine-checked no-go shows that continuity and records that are exact everywhere cannot both hold. Three witness families exist and each pays exactly one price: exact records without continuous flow, a smooth witness whose records and Born weights are exact only up to a stated tolerance, and a continuous witness exact except on a two-point seam. No horn is canonical. Whether a fourth combination is impossible is an open question, not a claim.

5. Build controlled continuum limits

Question: how can continuum-like quantum behaviour emerge from exact finite models?

Status: early work in progress. Continuous-variable modules exist covering the harmonic oscillator, its spectrum, Born weights in that setting, position, dispersion, approximate canonical commutation relations, field modes and mode locality. This is the current frontier rather than a completed stage.

6. The quantum-effective sector

Question: why do physically relevant Hamiltonians lie in the sector at all?

Status: this is a declared posit, and it stays one. Earlier versions of this page described the sector as an open problem to be solved. That is not the current position. The sector is posited openly, in the papers and in the formalisation, and deriving it from deeper dynamics is explicitly outside the programme's scope.

This is a scope decision, not an unfinished derivation. A machine-checked no-go in the corpus shows why deriving the sector from a single flow is not available. The reconstruction is conditional on the posit, and it says so.

7. Extend toward continuum physics and field theory

Question: can any of this survive the move to fields?

Status: not started, beyond the mode-level work in stage 5. No claim is made here.

What is done, and what is open

Done and machine-verified: the finite-dimensional reconstruction, stages 1 to 4. Schrödinger dynamics, the Born rule for general dimension and general measurements, measurement as a physical process with records, the Lüders update, entanglement and Bell, CGLMP and GHZ non-locality with no-signalling, contextuality, uncertainty, mixed states, quantum information theory, cryptographic protocols including Shor's algorithm, and quantum thermodynamics through Landauer's bound. Each carries an experimental counterpart in the empirical suite, which runs to over a hundred tests.

Open: the continuum limit, the field-theoretic extension, and the finer structural questions inside stage 5. The sector posit is not on this list, for the reason given above.

Why the roadmap is structured this way

Each stage is designed to be falsifiable on its own terms, and to be replaceable without collapsing the stages below it. That is also why the assumptions are stated as assumptions. The corpus carries a per-theorem axiom ledger, honest-scope notes in module headers, and an automated scan of its own prose for overclaims, because a reconstruction programme that quietly widens its claims is worth nothing.

The immediate next steps

Continuum limits, and publishing the technical layer that supports stages 3 and 4.

In one sentence

The finite-dimensional reconstruction is built and machine-verified on a posited sector, and the work now is whether it survives the move to the continuum.