SigmaLayer/NullSeamLift: the third horn on an even-dimensional arena

Category: dynamical measurement — specs/BACKLOG.md B2.

NullSeamWitness.lean builds the third measurement horn on S¹ × ℂℙ². That arena has real dimension 1 + 4 = 5 — odd — so it admits no symplectic structure, which is why its invariant measure had to be renamed nullSeamMeasure (the original nullSeamLiouville was the corpus's second odd-dimension slip; scripts/check-claims.sh check (7) now enforces the parity question).

This module removes that obstruction by giving the register its conjugate coordinate: the arena becomes T² × ℂℙ², real dimension 2 + 4 = 6. The construction is otherwise unchanged — the crossing angle still reads θ₁, and θ₂ is carried along untouched, exactly as a conjugate variable should be when the Hamiltonian does not depend on it.

What transfers, and how

Everything, and cheaply, because the lift is a product with the identity:

• continuous_nullSeamEvolveLift, nullSeamEvolveLift_measurePreserving — continuity and invariance of (vol ⊗ vol) ⊗ μ_FS.
• nullSeamLift_landing_neg / _pos — records exact and correct off the seam.
• nullSeamLift_seam_null — the seam is (two points) × T¹, still null.
• ★ nullSeamLift_born_left / _right — exact Born r and 1 − r, now measured on an even-dimensional register: the outcome sets are cylinders S ×ˢ univ, so their measure is vol S · 1 by Measure.prod_prod.
• ★★ nullSeamLiftClosure — the third horn, restated on the even-dimensional arena.

What this does and does not earn

Earned: the parity obstruction is gone. T² and ℂℙ² are each even-dimensional Kähler factors, so the product admits a symplectic structure, and the invariant measure is the corresponding volume — the name nullSeamLiftMeasure no longer asserts something the space cannot carry.

⚠️ NOT earned, and deliberately not claimed: the symplectic form itself is still not constructed. Mathlib has no symplectic-manifold API (verified 2026-08-04), so "this measure is the Liouville volume of ω^3/3!" remains the same §2a-scoped statement as everywhere else in the corpus (MATHLIB-GAPS.md, A4). Even dimension is necessary, not sufficient, and the guard's parity ledger records this arena as even without asserting the form. The horn's other prices are unchanged: exactness is at the Dirac-calibrated ready pointer, and "Born" is still carried by the free cell-split parameter r rather than by a preparation's moment map (NullSeamWitness.lean's scope note).

References

specs/BACKLOG.md B2 (this row), A4 (the blocked arrow); SigmaLayer/NullSeamWitness.lean (the construction lifted here); docs/TOUR.md §"Which horn is the right one?" (the trilemma).

@[reducible, inline]

abbrev CSD.RecordLayer.SeamArenaLift : Type

The even-dimensional seam arena: T² × ℂℙ², real dimension 2 + 4 = 6.

Equations

• CSD.RecordLayer.SeamArenaLift = ((CSD.RecordLayer.CircleFibre × CSD.RecordLayer.CircleFibre) × CSD.RecordLayer.Pointer 2)

noncomputable def CSD.RecordLayer.nullSeamEvolveLift (r : ℝ) : SeamArenaLift → SeamArenaLift

The lifted propagator: the crossing acts through θ₁ exactly as before; θ₂, the register's conjugate coordinate, is carried along untouched — which is what a conjugate variable does when the generator does not depend on it. Written as a reindexing of the unlifted map so that every transfer below is a one-liner.

Equations

• CSD.RecordLayer.nullSeamEvolveLift r y = (y.1, (CSD.RecordLayer.nullSeamEvolve r (y.1.1, y.2)).2)

@[simp]

theorem CSD.RecordLayer.nullSeamEvolveLift_fst (r : ℝ) (y : SeamArenaLift) : (nullSeamEvolveLift r y).1 = y.1

theorem CSD.RecordLayer.nullSeamEvolveLift_snd (r : ℝ) (y : SeamArenaLift) : (nullSeamEvolveLift r y).2 = (nullSeamEvolve r (y.1.1, y.2)).2

The lifted pointer component is the unlifted one at θ₁.

theorem CSD.RecordLayer.continuous_seamReindex : Continuous fun (y : SeamArenaLift) => (y.1.1, y.2)

The reindexing onto the unlifted arena.

Continuity and invariance

theorem CSD.RecordLayer.continuous_nullSeamEvolveLift (r : ℝ) : Continuous (nullSeamEvolveLift r)

The lifted propagator is continuous.

noncomputable def CSD.RecordLayer.nullSeamLiftMeasure (q₀ : Pointer 2) : MeasureTheory.Measure SeamArenaLift

The even-dimensional arena's invariant measure: Haar on T², Fubini–Study on ℂℙ². Unlike the S¹ × ℂℙ² version this arena is even-dimensional, so the name carries no parity defect — though the symplectic form itself is still not constructed (§2a).

Equations

• CSD.RecordLayer.nullSeamLiftMeasure q₀ = (MeasureTheory.volume.prod MeasureTheory.volume).prod (Matrix.UnitaryGroup.fubiniStudyMeasure q₀)

instance CSD.RecordLayer.instIsProbabilityMeasureSeamArenaLiftNullSeamLiftMeasure (q₀ : Pointer 2) : MeasureTheory.IsProbabilityMeasure (nullSeamLiftMeasure q₀)

theorem CSD.RecordLayer.nullSeamEvolveLift_measurePreserving (r : ℝ) (q₀ : Pointer 2) : MeasureTheory.MeasurePreserving (nullSeamEvolveLift r) (nullSeamLiftMeasure q₀) (nullSeamLiftMeasure q₀)

Measure invariance — a skew product over the whole register torus: both register coordinates are conserved, and every slice acts by an FS-preserving unitary.

Records, seam, and exact Born

theorem CSD.RecordLayer.nullSeamLift_landing_neg (r : ℝ) (hr0 : 0 < r) (hr1 : r < 1) (y : CircleFibre × CircleFibre) (hy : nullSeamSign r y.1 < 0) : (nullSeamEvolveLift r (y, readyState)).2 ∈ recordRegion 0

Records in the open first cell, exactly — inherited pointwise.

theorem CSD.RecordLayer.nullSeamLift_landing_pos (r : ℝ) (hr0 : 0 < r) (hr1 : r < 1) (y : CircleFibre × CircleFibre) (hy : 0 < nullSeamSign r y.1) : (nullSeamEvolveLift r (y, readyState)).2 ∈ recordRegion 1

Records in the open second cell, exactly.

theorem CSD.RecordLayer.nullSeamLift_outcome_cylinder (r : ℝ) (j : Fin 2) : {y : CircleFibre × CircleFibre | (nullSeamEvolveLift r (y, readyState)).2 ∈ recordRegion j} = {θ : CircleFibre | (nullSeamEvolve r (θ, readyState)).2 ∈ recordRegion j} ×ˢ Set.univ

The lifted outcome set is a cylinder over the unlifted one.

theorem CSD.RecordLayer.nullSeamLift_seam_null (r : ℝ) (hr0 : 0 < r) (hr1 : r < 1) : MeasureTheory.volume {y : CircleFibre × CircleFibre | nullSeamSign r y.1 = 0} = 0

★ The seam is still null — now (two points) × T¹.

theorem CSD.RecordLayer.nullSeamLift_born_left (r : ℝ) (hr0 : 0 < r) (hr1 : r < 1) : MeasureTheory.volume {y : CircleFibre × CircleFibre | (nullSeamEvolveLift r (y, readyState)).2 ∈ recordRegion 0} = ENNReal.ofReal r

★ Exact Born, first outcome, on the even-dimensional register.

theorem CSD.RecordLayer.nullSeamLift_born_right (r : ℝ) (hr0 : 0 < r) (hr1 : r < 1) : MeasureTheory.volume {y : CircleFibre × CircleFibre | (nullSeamEvolveLift r (y, readyState)).2 ∈ recordRegion 1} = ENNReal.ofReal (1 - r)

★ Exact Born, second outcome.

★★ The third horn, on an even-dimensional arena

structure CSD.RecordLayer.NullSeamLiftClosure (r : ℝ) : Prop

The third horn, parity obstruction removed. Same construction, same prices; the arena is now T² × ℂℙ², real dimension 6, a product of Kähler factors. What is not claimed: the symplectic form itself (§2a-scoped, MATHLIB-GAPS.md A4).

• continuity : Continuous (nullSeamEvolveLift r)

  Continuous on the whole even-dimensional arena.

• invariant (q₀ : Pointer 2) : MeasureTheory.MeasurePreserving (nullSeamEvolveLift r) (nullSeamLiftMeasure q₀) (nullSeamLiftMeasure q₀)

  The product measure is invariant.

• landing_left (y : CircleFibre × CircleFibre) : nullSeamSign r y.1 < 0 → (nullSeamEvolveLift r (y, readyState)).2 ∈ recordRegion 0

  Correct record in the open first cell.

• landing_right (y : CircleFibre × CircleFibre) : 0 < nullSeamSign r y.1 → (nullSeamEvolveLift r (y, readyState)).2 ∈ recordRegion 1

  Correct record in the open second cell.

• seam_null : MeasureTheory.volume {y : CircleFibre × CircleFibre | nullSeamSign r y.1 = 0} = 0

  The seam is null.

• born_left : MeasureTheory.volume {y : CircleFibre × CircleFibre | (nullSeamEvolveLift r (y, readyState)).2 ∈ recordRegion 0} = ENNReal.ofReal r

  Exact Born, first outcome.

• born_right : MeasureTheory.volume {y : CircleFibre × CircleFibre | (nullSeamEvolveLift r (y, readyState)).2 ∈ recordRegion 1} = ENNReal.ofReal (1 - r)

  Exact Born, second outcome.

theorem CSD.RecordLayer.nullSeamLiftClosure (r : ℝ) (hr0 : 0 < r) (hr1 : r < 1) : NullSeamLiftClosure r

★★ The lifted third horn exists, for every cell split.