Schrodinger from records

The Schrodinger equation is not postulated here. Preserving record statistics forces unitarity, unitarity plus continuity forces a Hamiltonian, and the exponential form is a theorem at the end of a chain.

proved in corpus · proved here, no imported axiomsLean sigmaFlow_schrodinger_form

In plain terms

Here is the problem. Reconstructions of quantum mechanics usually spend their effort on probability and quietly assume the dynamics: states evolve by the Schrodinger equation because that is the theory being reconstructed. If the arena picture is doing real work, the dynamics should be earned too.

The corpus's route earns it from records. Suppose the arena's dynamics preserves record statistics -- the pairwise outcome frequencies that experiments actually accumulate. A rigidity theorem going back to Wigner says a map preserving those statistics must be unitary or antiunitary; a selection argument kills the antiunitary branch along a continuous flow; a phase-lifting step and a continuity theorem of Stone's type then deliver a self-adjoint generator.

The endpoint is the exponential form of the Schrodinger equation, derived -- with the premise being about statistics of records, not about Hilbert-space structure. The chain is assembled from separate theorems rather than proved in one stroke, and the final link carries real hypotheses: a smoothness condition, and a coboundary condition on the phase that the corpus shows is unavoidable rather than convenient.

In CSD

The W-series is the dynamics spine: the projected sector flow is conjugation by a one-parameter unitary group, proved from the descent structure rather than assumed, with the record-level premise conversion making the hypothesis operational -- transition probabilities ARE record observables, so preserving record statistics and preserving transition probabilities are the same predicate, by theorem.

The honest scope is tracked mechanically: the sector-linkage guard enforces that the descent equation is genuinely consumed, and the connectivity manifest -- not this page -- is the single source of truth for which end-to-end connective claims are backed.

Mathematically

sigmaFlow_schrodinger_form: for sector data with a projectable flow, the projected dynamics is exp(-itH)-conjugation on rays. Read the hypotheses, because they are where the content sits. The theorem takes the projected flow as ALREADY given by a unitary family, so Wigner rigidity and the Bargmann branch discriminator stand upstream supplying that premise rather than inside this statement; it then takes a cocycle for the family, a unit-modulus phase satisfying a coboundary condition, an anti-Hermitian generator, and a C^1 derivative hypothesis. The coboundary condition is not a convenience -- the corpus proves it necessary, so the phase lift exists exactly when it holds. What the capstone adds over the ray-level form is that it genuinely consumes the sector fields, the flow, the projection and projectability, rather than restating a result about an already-projected map. The record-level conversion equates the operational premise with the geometric one and re-derives the flow theorem from record statistics, with the invariance of the Fubini-Study measure obtained with U(N) in the proof and never in the statement.

Module
CsdLean4/LF4/PhaseLift.lean
Related
schrodinger equation, wigner rigidity, stone theorem, bargmann
Referenced
Wikipedia

Source links are pinned to a commit, so they do not drift. The anchors above are checked mechanically against the Lean tree on every build. The mathematics is not, and cannot be: that is a human responsibility and it rests with the author.

Part of Constraint-Surface Dynamics · Formalised in csd-lean4.

Privacy policy