SigmaLayer/PiecewiseHamiltonian: the classification of the measurement dynamics

Category: dynamical measurement / classification (the decision resolving the reopened Hamiltonian-origin row, 2026-08-02).

⚠️ Correction 2026-08-02 (second external review) — the pieces are NOT globally Hamiltonian

The original docstring read each rigid translation as "generated by the linear Hamiltonian hᵢ = shearAmt(i)·p_R". That reading is wrong on the compact torus: with ω = dq ∧ dp, the translation field X = a·∂/∂q has ι_X ω = a·dp, which is closed but not exact on T² (∮ dp = 1 ≠ 0 around the p-cycle) — so for a ≠ 0 there is no globally defined generating function. The pieces are rigid symplectic (locally Hamiltonian) translations — measure-preserving, continuous, volume-exact — but not flows of global Hamiltonians. The correct classification of this witness is therefore "piecewise rigid symplectic torus translation with null seam set", not "piecewise Hamiltonian flow". Every Lean theorem below is unaffected (none mentions a Hamiltonian); the module and theorem names are retained for pin stability, with this correction as their reading. The Hamiltonian-origin row is reopened with the review-recommended route — a compact Kähler pointer ℂℙ^K, where unitary rotations are globally Hamiltonian (H¹(ℂℙ^K) = 0, moment maps exist) and the flux obstruction vanishes. See specs/BACKLOG.md.

The decision

ShearDiscontinuity.lean proved the measurement propagator is not continuous, reopening the Hamiltonian-origin row with two recorded routes. The decision (author, 2026-08-02): route (2) — CSD measurement dynamics is classified as piecewise Hamiltonian with a null seam set. Corridor regularisation (route 1) stays recorded in specs/BACKLOG.md as an optional later strengthening, not an obligation.

What "piecewise Hamiltonian with null seam set" means, machine-checked

Three facts, each a theorem:

1. The pieces are rigid symplectic translations (see the correction above — not globally Hamiltonian) (shearEvolve_eq_translation_on_basin + shearEvolve_continuousOn_basin): on each basin cylinder Bᵢ × T²_R the propagator is the rigid register translation by shearAmt i — a symplectic, measure-preserving translation. (The original hᵢ = shearAmt(i)·p_R reading is withdrawn — the flux correction above.) Continuity holds piecewise — ContinuousOn, proved.
2. The seam set is null (seam_null): the points lying in no basin cylinder have measure zero for every preparation and every (s-finite) register measure — the pieces cover the arena up to a null set (globalBasin_ae_total lifted through the product).
3. The seams cannot be removed (no_everywhere_correlation, MeasurementConstraints.lean): any exact-record dynamics must be discontinuous somewhere — a continuous propagator cannot carry a connected ready set into ≥ 2 disjoint open pointer regions. So the classification is not an apology for a defective witness; it is the general shape forced on exact-record measurement dynamics. Piecewise-smooth Hamiltonian systems with singular sets are standard objects (billiards, impact systems); CSD's measurement dynamics now carries that classification explicitly.

shear_piecewise_hamiltonian bundles (1) and (2) as one statement.

Honest boundary

The identification of each piece's translation with "the flow of hᵢ = shearAmt(i)·p_R" is carried as prose (the standard reading of a rigid torus translation); Lean exhibits the translation and its continuity, not a symplectic form — that spelling is the §2a gap. What is no longer claimed anywhere: that the full propagator is a time slice of a single continuous Hamiltonian flow (shearEvolve_not_continuous refutes it).

References

SigmaLayer/ShearDiscontinuity.lean (shearEvolve_not_continuous — why the classification is needed); SigmaLayer/MeasurementConstraints.lean (no_everywhere_correlation — why the seams are forced); SigmaLayer/GlobalBasin.lean (globalBasin_ae_total — why they are null); SigmaLayer/ShearWitness.lean (shearEvolve, pshift, shearAmt); specs/BACKLOG.md; specs/reconstruction-status.md §2a.

theorem CSD.RecordLayer.shearEvolve_eq_translation_on_basin {N : ℕ} [NeZero N] (c : ContextField N) (i : Fin N) (s t : ℝ) {x : LF4.KSigma N × LF4.KTorus} (hx : x.1 ∈ globalBasin c i) : shearEvolve (basinIndex c) s t x = (x.1, pshift ((elapsed t - elapsed s) * shearAmt N i) x.2)

The pieces are rigid translations. On the basin-i cylinder, the propagator is exactly the register translation by (elapsed t − elapsed s)·shearAmt i — no dependence on the point beyond its basin membership.

theorem CSD.RecordLayer.shearEvolve_continuousOn_basin {N : ℕ} [NeZero N] (c : ContextField N) (i : Fin N) (s t : ℝ) : ContinuousOn (shearEvolve (basinIndex c) s t) (globalBasin c i ×ˢ Set.univ)

Each piece is continuous — the restriction of a globally continuous rigid translation.

theorem CSD.RecordLayer.seam_null {N : ℕ} (c : ContextField N) (p : LF4.CPN N) (ν : MeasureTheory.Measure LF4.KTorus) [MeasureTheory.SFinite ν] : ((epistemicMeasure p).prod ν) {x : LF4.KSigma N × LF4.KTorus | ∀ (i : Fin N), x.1 ∉ globalBasin c i} = 0

The seam set is null. The points lying in no basin cylinder carry measure zero, for every preparation and every s-finite register measure: the symplectic pieces cover the arena up to a null set. (Not "Hamiltonian pieces": the module header's flux correction proves each piece is symplectic but not the flow of any global Hamiltonian. Wording corrected 2026-08-04 — it had carried the withdrawn reading forward.)

theorem CSD.RecordLayer.shear_piecewise_hamiltonian {N : ℕ} [NeZero N] (c : ContextField N) (p : LF4.CPN N) (ν : MeasureTheory.Measure LF4.KTorus) [MeasureTheory.SFinite ν] (s t : ℝ) : (∀ (i : Fin N), ContinuousOn (shearEvolve (basinIndex c) s t) (globalBasin c i ×ˢ Set.univ)) ∧ ((epistemicMeasure p).prod ν) {x : LF4.KSigma N × LF4.KTorus | ∀ (i : Fin N), x.1 ∉ globalBasin c i} = 0

★ The piecewise-Hamiltonian classification (decision 2026-08-02, resolving the reopened Hamiltonian-origin row): the measurement propagator is continuous on every basin cylinder — where it is an explicit rigid translation (symplectic, locally Hamiltonian — see the flux correction in the module header) — and the seam set outside the cylinders is null. Together with shearEvolve_not_continuous (the seams are real) and no_everywhere_correlation (they are forced for every exact-record dynamics), this is the "piecewise rigid symplectic translation with null seam set"** classification, machine-checked. ⚠️ The theorem NAME says "hamiltonian" and is a known misnomer, retained for pin stability per the header; the flux obstruction (ι_Xω = a·dp closed-not-exact on T²) means no global generator exists. What the statement literally proves is ContinuousOn per basin cylinder plus a null seam set — no generator, no symplectic form, no flow identification appears in it. Docstring corrected 2026-08-04; the name is declared as an exception in scripts/check-claims.sh check (7).