SigmaLayer/UntriggeredVolume: the untriggered flow preserves chart volume, and is unique

Category: 7-SigmaLayer (dynamical measurement) — specs/frozen-base-obstruction-scoping.md brick 2, the two gaps its own honest scope left open: measure preservation and uniqueness.

What this closes

Brick 2 (SigmaLayer/UntriggeredFlow.lean) built one Hamiltonian flow that records and back-reacts. Its readout half (SigmaLayer/UntriggeredReadout.lean) showed the record is faithful for every preparation μ — but said nothing about which μ the dynamics itself preserves, and every necessary condition in RecordLayer/MeasurementConstraints.lean takes measure preservation as its hypothesis. This module supplies it.

The whole argument is one observation: the time-t map is linear in the initial state, block-diagonal on Chart n = (Fin n → ℝ) × (Fin n → ℝ), and each block is a rank-one perturbation of the identity — a shear. Its determinant is (1 + t·c_k)(1 − t·c_k) = 1 by the matrix determinant lemma, because c k = 0.

• untriggeredLin — the time-t map as a linear endomorphism; untriggeredLin_apply identifies it with untriggeredCurve.
• det_untriggeredLin — its determinant is 1.
• ★★ untriggeredCurve_measurePreserving — therefore the flow preserves Lebesgue measure on the chart. This is MeasurePreserving in the corpus's own sense (ConstraintDynamics.flow_preserves, MeasurementRecord), so it plugs directly into the necessary conditions.
• ★ untriggered_no_exact_collapse — one such plug-in, MeasurementConstraints.no_exact_collapse instantiated on this flow: a positive-volume set of preparations cannot be driven into a null set. Collapse, on this flow too, is relocation of a null slice.
• ★ untriggeredCurve_unique — the same linearity makes the field Lipschitz, so brick 0's hamiltonianCurve_unique upgrades an integral curve to the integral curve. This is the claim brick 2's docstring promised and then withdrew; it is now proved.

Not reinvented

Everything measure-theoretic is Mathlib: Measure.map_linearMap_addHaar_eq_smul_addHaar (pushforward of a Haar measure by a linear map is |det⁻¹| times itself), LinearMap.det_prodMap (block-diagonal determinants multiply), LinearMap.det_toLin' and Matrix.det_one_add_replicateCol_mul_replicateRow (the matrix determinant lemma). The chart's Lebesgue measure is Haar by instance. No volume computation is done by hand.

⚠️ Honest scope

This is measure preservation of the chart flow, not Born. There is still no moment map in a Darboux chart, so nothing here weights outcomes; the readout half's caveat stands unchanged. It is a chart statement: Chart n is globally ℝ^{2n}, the arena is not, and the chart→arena transport remains open (⚠️ RESIDUE(R-016)). Which interaction an apparatus realises is a permanent boundary rather than open work (⚠️ RESIDUE(R-015)).

c k = 0 is a hypothesis throughout, as in untriggeredCurve_isHamiltonianCurve. Without it the block determinants are 1 ± t·c_k and the map is not volume-preserving — but then it is not the Hamiltonian flow either, so nothing is lost.

References

specs/frozen-base-obstruction-scoping.md (brick 2, remaining gaps); specs/future-work.md; SigmaLayer/UntriggeredFlow.lean (untriggeredCurve, interactionH); SigmaLayer/UntriggeredReadout.lean (the readout half); SigmaLayer/ChartIntegralCurve.lean (hamiltonianCurve_unique, lipschitzWith_momentumH_field — the idiom reused here); RecordLayer/MeasurementConstraints.lean (no_exact_collapse, the consumer); SigmaLayer/ConstraintDynamics.lean (flow_preserves, the predicate).

The time-t map is linear: the two blocks

noncomputable def CSD.SigmaLayer.posBlock {n : ℕ} (c : Fin n → ℝ) (k : Fin n) (t : ℝ) : Matrix (Fin n) (Fin n) ℝ

The position block of the time-t map, x ↦ x + t (c ⬝ x) e_k, as the rank-one perturbation of the identity 1 + (t e_k) cᵀ.

Equations

• CSD.SigmaLayer.posBlock c k t = 1 + Matrix.vecMulVec (t • Pi.single k 1) c

noncomputable def CSD.SigmaLayer.momBlock {n : ℕ} (c : Fin n → ℝ) (k : Fin n) (t : ℝ) : Matrix (Fin n) (Fin n) ℝ

The momentum block, y ↦ y − t y_k c, as 1 − (t c) e_kᵀ.

Equations

• CSD.SigmaLayer.momBlock c k t = 1 + Matrix.vecMulVec (-(t • c)) (Pi.single k 1)

theorem CSD.SigmaLayer.vecMulVec_mulVec_apply {n : ℕ} (u v x : Fin n → ℝ) (j : Fin n) : (Matrix.vecMulVec u v).mulVec x j = u j * v ⬝ᵥ x

A rank-one matrix acting on a vector: (u vᵀ) x = (v ⬝ x) u, entrywise.

theorem CSD.SigmaLayer.posBlock_mulVec {n : ℕ} (c : Fin n → ℝ) (k : Fin n) (t : ℝ) (x : Fin n → ℝ) : (posBlock c k t).mulVec x = fun (j : Fin n) => if j = k then x k + t * ∑ i : Fin n, c i * x i else x j

theorem CSD.SigmaLayer.momBlock_mulVec {n : ℕ} (c : Fin n → ℝ) (k : Fin n) (t : ℝ) (y : Fin n → ℝ) : (momBlock c k t).mulVec y = fun (j : Fin n) => y j - t * (c j * y k)

noncomputable def CSD.SigmaLayer.untriggeredLin {n : ℕ} (c : Fin n → ℝ) (k : Fin n) (t : ℝ) : Chart n →ₗ[ℝ] Chart n

The time-t map of the untriggered flow, as a linear endomorphism of the chart.

Equations

• CSD.SigmaLayer.untriggeredLin c k t = (Matrix.toLin' (CSD.SigmaLayer.posBlock c k t)).prodMap (Matrix.toLin' (CSD.SigmaLayer.momBlock c k t))

theorem CSD.SigmaLayer.untriggeredLin_apply {n : ℕ} (c : Fin n → ℝ) (k : Fin n) (t : ℝ) (z : Chart n) : (untriggeredLin c k t) z = untriggeredCurve c k z t

The linear map is the flow: untriggeredLin c k t z = untriggeredCurve c k z t.

The determinant is one

theorem CSD.SigmaLayer.det_posBlock {n : ℕ} (c : Fin n → ℝ) (k : Fin n) (hck : c k = 0) (t : ℝ) : (posBlock c k t).det = 1

The position shear has unit determinant: det (1 + (t e_k) cᵀ) = 1 + t·c_k = 1.

theorem CSD.SigmaLayer.det_momBlock {n : ℕ} (c : Fin n → ℝ) (k : Fin n) (hck : c k = 0) (t : ℝ) : (momBlock c k t).det = 1

The momentum shear has unit determinant: det (1 − (t c) e_kᵀ) = 1 − t·c_k = 1.

theorem CSD.SigmaLayer.det_untriggeredLin {n : ℕ} (c : Fin n → ℝ) (k : Fin n) (hck : c k = 0) (t : ℝ) : LinearMap.det (untriggeredLin c k t) = 1

The time-t map has determinant one. Block-diagonal, so the determinants multiply.

★★ Measure preservation

instance CSD.SigmaLayer.instIsAddHaarMeasureVolumeChart {n : ℕ} : MeasureTheory.volume.IsAddHaarMeasure

Lebesgue measure on the chart is a Haar measure: the product of the two Haar measures on the position and momentum blocks. (Instance search does not find the Measure.prod instance through volume on the product by itself; this registers it for Chart n.)

theorem CSD.SigmaLayer.untriggeredCurve_measurePreserving {n : ℕ} (c : Fin n → ℝ) (k : Fin n) (hck : c k = 0) (t : ℝ) : MeasureTheory.MeasurePreserving (fun (z : Chart n) => untriggeredCurve c k z t) MeasureTheory.volume MeasureTheory.volume

★★ The untriggered flow preserves chart volume. A unit-determinant linear map pushes Lebesgue measure to itself (Measure.map_linearMap_addHaar_eq_smul_addHaar). This is MeasurePreserving in the corpus's own sense — the hypothesis every necessary condition in RecordLayer/MeasurementConstraints.lean takes.

theorem CSD.SigmaLayer.volume_untriggered_preimage {n : ℕ} (c : Fin n → ℝ) (k : Fin n) (hck : c k = 0) (t : ℝ) {A : Set (Chart n)} (hA : MeasurableSet A) : MeasureTheory.volume ((fun (z : Chart n) => untriggeredCurve c k z t) ⁻¹' A) = MeasureTheory.volume A

Volume flows without compression or dilation: the set of initial states carried into a measurable A has exactly the volume of A.

theorem CSD.SigmaLayer.untriggered_no_exact_collapse {n : ℕ} (c : Fin n → ℝ) (k : Fin n) (hck : c k = 0) (t : ℝ) {C T : Set (Chart n)} (hT : MeasureTheory.NullMeasurableSet T MeasureTheory.volume) (hTnull : MeasureTheory.volume T = 0) (hsub : C ⊆ (fun (z : Chart n) => untriggeredCurve c k z t) ⁻¹' T) (hCpos : MeasureTheory.volume C ≠ 0) : False

★ no_exact_collapse on the untriggered flow. A positive-volume set of preparations cannot be driven into a null set of states: on this flow too, collapse can only be relocation of a null slice, never contraction of a positive-measure one. The first consumer of untriggeredCurve_measurePreserving, showing it plugs into the existing constraints.

★ The field is linear, so the flow is the flow

noncomputable def CSD.SigmaLayer.untriggeredField {n : ℕ} (c : Fin n → ℝ) (k : Fin n) : Chart n →L[ℝ] Chart n

The Hamiltonian field of the coupling as a continuous linear map, z ↦ ((Σᵢ cᵢ xᵢ) e_k, −y_k c).

Equations

• CSD.SigmaLayer.untriggeredField c k = ((CSD.SigmaLayer.posCLM c).smulRight (Pi.single k 1)).prod ((CSD.SigmaLayer.momCoord k).smulRight (-c))

theorem CSD.SigmaLayer.hamiltonianField_interactionH {n : ℕ} (c : Fin n → ℝ) (k : Fin n) : hamiltonianField (interactionH c k) = ⇑(untriggeredField c k)

The field of interactionH is untriggeredField — linear, hence Lipschitz.

theorem CSD.SigmaLayer.lipschitzWith_interactionH_field {n : ℕ} (c : Fin n → ℝ) (k : Fin n) : LipschitzWith ‖untriggeredField c k‖₊ (hamiltonianField (interactionH c k))

The coupling's field is Lipschitz, with constant the operator norm.

theorem CSD.SigmaLayer.untriggeredCurve_unique {n : ℕ} (c : Fin n → ℝ) (k : Fin n) (hck : c k = 0) (z₀ : Chart n) {γ : ℝ → Chart n} (hγ : IsHamiltonianCurve (interactionH c k) γ) (h₀ : γ 0 = z₀) : γ = untriggeredCurve c k z₀

★ The untriggered curve is THE integral curve. Any integral curve of the coupling through z₀ at time 0 is untriggeredCurve c k z₀ — the uniqueness brick 2's honest scope left open, discharged from linearity via brick 0.