SigmaLayer/NullSeamWitness: the third horn — continuous, exact Born, null seam

Category: dynamical measurement — the "Cantor-horn" candidate brick recorded against the fourth external review (2026-08-03), delivered — and simpler than the devil's-staircase sketch that motivated it.

The idea

no_everywhere_correlation kills {continuity + everywhere-exact records}. The two formalised horns paid for that with seams (piecewise) or with an ε-corridor of Born error (smooth witness). The reviewer observed a third option was not excluded: continuous dynamics with records exact off a null seam and exact Born. This module exhibits it — and the mechanism is not a Cantor function. The transition between two record regions dodges the record gap by crossing where the record regions kiss: the moment regions {m₁ > ½} and {m₂ > ½} share the boundary state m₁ = m₂ = ½, and a rotation in the (f₁, f₂)-plane travels from one region to the other touching the complement at exactly one projective point. Sweeping that crossing angle continuously in the register coordinate θ — crossing π/4 exactly at the two cell-boundary points — gives:

• ★★ nullSeamClosure — a continuous (continuous_nullSeamEvolve), measure-preserving (nullSeamEvolve_measurePreserving) skew-unitary propagator on S¹ × ℂℙ² whose landing from the calibrated ready state is in the correct record region for every θ off a two-point seam (nullSeam_landing_neg/pos, nullSeam_seam_null), with exact Born weights r and 1 − r (nullSeam_born_left/right) — no ε.

The seam profile is nullSeamSign θ = infDist θ I₁ − infDist θ I₂ (the two closed cell arcs): continuous, negative exactly on the open first cell, positive exactly on the open second, zero exactly at the two boundary points — circle-intrinsic, no fundamental-domain lift, no case analysis at the wrap point.

⚠️ Naming corrected 2026-08-03 (fifth external review, and the reviewer is right). The invariant measure here was originally called nullSeamLiouville. (Corrected 2026-08-04 (independent Opus review of HEAD). — the global rename rewrote this sentence too, so the correction read as a no-op: it named the new name as the old one. Exactly the class of defect it was describing.) S¹ × ℂℙ² has real dimension 5 — odd — so it carries no symplectic structure and the word "Liouville" was unearned. The measure (Haar ⊗ Fubini–Study) is genuinely invariant and every theorem below stands unchanged; only the name and the surrounding prose overclaimed. It is now nullSeamMeasure, and invariance is stated as measure-preservation. Earning the symplectic word means lifting the register S¹ to the full T² and working on T² × ℂℙ² (even dimension) — recorded in BACKLOG.md, not done here. (This is the corpus's second odd-dimension slip; the first is recorded in the fibred-Σ correction.)

⚠️ Scope note 2026-08-04: "Born" here is carried by the cell split r, a free parameter of the construction. Unlike every other horn (pointer_born_lower reads c.rate p j; join_sector_born reads ∑ ‖⟨eⱼ,ψ⟩‖²), this module contains no preparation, no ray and no moment map. That is adequate for what the horn claims — an existence result against a no-go (no_everywhere_correlation) that is itself preparation-free, and every r ∈ (0,1) is some preparation's Born weight — but the identification of r with a Born weight is stated here, not formalised.

The price — and the trilemma

⚠️ Honest scope. The exactness statements are at the Dirac-calibrated ready point q = [f₀] — this is the third horn's price, and it is real: with a positive-width ready region {m₀ > 1 − δ}, states near the crossing angle land near the kissing state, and because the stroke is a homeomorphism their image is an open neighbourhood of it — which necessarily meets the interior of the no-record set, giving that set positive measure (posMeasure_noRecord_of_isOpenMap, SigmaLayer/SharpenedNoGo.lean). A Dirac calibration escapes precisely because a point has no neighbourhood to spare, which is how this witness threads the kissing state exactly. ⚠️ Corrected 2026-08-04: this note previously said the seam fattens "to a positive-measure set of order the calibration width". The order is a quantitative claim that the topological argument does not give and that is not proved anywhere; it needed an estimate on how far the landing moments move with the ready state. Positive measure stands; O(δ) was an over-assertion. The corpus already prices Dirac calibration: collapse_accuracy_bound. The honest classification is therefore a trilemma — each horn pays exactly one of: seams (piecewise witness, discontinuous propagator), ε-Born (smooth witness, positive-measure ready state), Dirac calibration (this witness, exact records a.e. and exact Born). Whether a fourth combination (continuous + positive-width ready + exact-Born-and-a.e.-records) is impossible is a candidate sharpened no-go, recorded, not claimed. Updated 2026-08-05: on the pointer's moment-region geometry this is now a theorem — posMeasure_noRecord_pointer (SigmaLayer/NoRecordGeometry.lean): continuity + open-map + open preconnected positive-width ready + two-outcome correlation force a positive-measure no-record set, so exact-a.e. records force Dirac calibration. General exhaustiveness over all arenas remains research, not claimed. Further scope: two cells and a ℂℙ² pointer (the horn is an existence claim; general N DONE 2026-08-12 — NullSeamGeneralN.lean, nullSeamGenClosure: every N ≥ 2 and every weight vector, via plateau tents and a single amplitude-polynomial rotation); the terminal stroke is exhibited as a continuous skew-unitary map (time-ramping through pointerRamp/smoothPointerRamp is the same mechanical wrapping as brick 4 and is not duplicated); no protocol packaging.

References

specs/BACKLOG.md (the Cantor-horn row — this discharges it; fourth external review 2026-08-03); docs/TOUR.md §"Which horn is the right one?" (updated to the trilemma); SigmaLayer/PointerArena.lean (Pointer, recordRegion, readyState, momentMap_add_le_one — the kissing geometry), SigmaLayer/PointerWeights.lean (the continuity-descent and skew-product idioms this reuses), SigmaLayer/ShearDiscontinuity. lean (shearEvolve_not_continuous — what the first horn pays), SigmaLayer/PointerBorn.lean (the ε the second horn pays), SigmaLayer/Measurement.lean (collapse_accuracy_bound — the price tag on the third).

Circle toolkit: lifts, half-diameter, coe-distance

theorem CSD.RecordLayer.abs_sub_round_le_abs (c : ℝ) : |c - ↑(round c)| ≤ |c|

Round is the nearest integer: subtracting it can only shrink the absolute value.

theorem CSD.RecordLayer.exists_norm_lift (z : CircleFibre) : ∃ (c : ℝ), ↑c = z ∧ |c| = ‖z‖ ∧ |c| ≤ 1 / 2

Every point of the unit circle has a lift realising its norm, of size at most ½.

theorem CSD.RecordLayer.circle_dist_le_half (z w : CircleFibre) : dist z w ≤ 1 / 2

The unit circle has diameter ½.

theorem CSD.RecordLayer.circle_dist_coe_le (a b : ℝ) : dist ↑a ↑b ≤ |a - b|

Distance on the circle is dominated by the distance of any pair of lifts.

The two cell arcs and the seam profile

def CSD.RecordLayer.seamArcL (r : ℝ) : Set CircleFibre

The first closed cell arc: the image of [0, r].

Equations

• CSD.RecordLayer.seamArcL r = (fun (s : ℝ) => ↑s) '' Set.Icc 0 r

def CSD.RecordLayer.seamArcR (r : ℝ) : Set CircleFibre

The second closed cell arc: the image of [r, 1].

Equations

• CSD.RecordLayer.seamArcR r = (fun (s : ℝ) => ↑s) '' Set.Icc r 1

theorem CSD.RecordLayer.isClosed_seamArcL (r : ℝ) : IsClosed (seamArcL r)

theorem CSD.RecordLayer.isClosed_seamArcR (r : ℝ) : IsClosed (seamArcR r)

theorem CSD.RecordLayer.seamArc_union (r : ℝ) (hr0 : 0 ≤ r) (hr1 : r ≤ 1) : seamArcL r ∪ seamArcR r = Set.univ

theorem CSD.RecordLayer.seamArc_inter (r : ℝ) (hr0 : 0 < r) (hr1 : r < 1) : seamArcL r ∩ seamArcR r = {↑0, ↑r}

The two closed arcs meet exactly at the two boundary points.

noncomputable def CSD.RecordLayer.nullSeamSign (r : ℝ) (θ : CircleFibre) : ℝ

The seam profile: signed by which closed arc is nearer. Continuous, circle-intrinsic, negative exactly on the open first cell, positive exactly on the open second, zero exactly at the two boundary points.

Equations

• CSD.RecordLayer.nullSeamSign r θ = Metric.infDist θ (CSD.RecordLayer.seamArcL r) - Metric.infDist θ (CSD.RecordLayer.seamArcR r)

theorem CSD.RecordLayer.continuous_nullSeamSign (r : ℝ) : Continuous (nullSeamSign r)

theorem CSD.RecordLayer.seamArcL_nonempty (r : ℝ) (hr0 : 0 < r) : (seamArcL r).Nonempty

theorem CSD.RecordLayer.seamArcR_nonempty (r : ℝ) (hr1 : r < 1) : (seamArcR r).Nonempty

theorem CSD.RecordLayer.nullSeamSign_neg_iff (r : ℝ) (hr0 : 0 < r) (hr1 : r < 1) (θ : CircleFibre) : nullSeamSign r θ < 0 ↔ θ ∈ seamArcL r \ seamArcR r

Negativity region: exactly the first arc minus the seam points.

theorem CSD.RecordLayer.nullSeamSign_pos_iff (r : ℝ) (hr0 : 0 < r) (hr1 : r < 1) (θ : CircleFibre) : 0 < nullSeamSign r θ ↔ θ ∈ seamArcR r \ seamArcL r

Positivity region: exactly the second arc minus the seam points.

theorem CSD.RecordLayer.nullSeamSign_eq_zero_iff (r : ℝ) (hr0 : 0 < r) (hr1 : r < 1) (θ : CircleFibre) : nullSeamSign r θ = 0 ↔ θ = ↑0 ∨ θ = ↑r

The seam is exactly the two boundary points.

theorem CSD.RecordLayer.abs_nullSeamSign_le (r : ℝ) (hr0 : 0 < r) (hr1 : r < 1) (θ : CircleFibre) : |nullSeamSign r θ| ≤ 1 / 2

The seam profile is bounded by the circle's half-diameter.

The crossing angle and the record criterion

noncomputable def CSD.RecordLayer.nullSeamAngle (r : ℝ) (θ : CircleFibre) : ℝ

The crossing angle: π/4 exactly on the seam, < π/4 in the first cell, > π/4 in the second — always inside (0, π/2).

Equations

• CSD.RecordLayer.nullSeamAngle r θ = Real.pi / 4 + CSD.RecordLayer.nullSeamSign r θ

theorem CSD.RecordLayer.nullSeamAngle_mem (r : ℝ) (hr0 : 0 < r) (hr1 : r < 1) (θ : CircleFibre) : nullSeamAngle r θ ∈ Set.Ioo 0 (Real.pi / 2)

theorem CSD.RecordLayer.cos_sq_gt_half_iff {χ : ℝ} (hχ : χ ∈ Set.Ioo 0 (Real.pi / 2)) : 1 / 2 < Real.cos χ ^ 2 ↔ χ < Real.pi / 4

The record criterion at the crossing angle: cos²χ > ½ ↔ χ < π/4 inside the window.

theorem CSD.RecordLayer.sin_sq_gt_half_iff {χ : ℝ} (hχ : χ ∈ Set.Ioo 0 (Real.pi / 2)) : 1 / 2 < Real.sin χ ^ 2 ↔ Real.pi / 4 < χ

The complementary criterion: sin²χ > ½ ↔ χ > π/4 inside the window.

The witness unitary

noncomputable def CSD.RecordLayer.nullSeamMat (χ : ℝ) : Matrix (Fin 3) (Fin 3) ℂ

The witness matrix at crossing angle χ: sends the ready direction f₀ to cos χ · f₁ + sin χ · f₂ — the record-to-record crossing through the kissing state.

Equations

• CSD.RecordLayer.nullSeamMat χ = !![0, 0, 1; ↑(Real.cos χ), -↑(Real.sin χ), 0; ↑(Real.sin χ), ↑(Real.cos χ), 0]

theorem CSD.RecordLayer.nullSeamMat_mem (χ : ℝ) : nullSeamMat χ ∈ Matrix.unitaryGroup (Fin 3) ℂ

noncomputable def CSD.RecordLayer.nullSeamUU (r : ℝ) (θ : CircleFibre) : ↥(Matrix.unitaryGroup (Fin 3) ℂ)

The witness unitary family over the register circle.

Equations

• CSD.RecordLayer.nullSeamUU r θ = ⟨CSD.RecordLayer.nullSeamMat (CSD.RecordLayer.nullSeamAngle r θ), ⋯⟩

noncomputable def CSD.RecordLayer.nullSeamEvolve (r : ℝ) : CircleFibre × Pointer 2 → CircleFibre × Pointer 2

The null-seam propagator: register conserved, pointer rotated by the crossing unitary at the register's crossing angle.

Equations

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

Landing at the calibrated ready point

noncomputable def CSD.RecordLayer.nullSeamVec (χ : ℝ) : EuclideanSpace ℂ (Fin 3)

The landing vector: cos χ · f₁ + sin χ · f₂.

Equations

• CSD.RecordLayer.nullSeamVec χ = !₂[0, ↑(Real.cos χ), ↑(Real.sin χ)]

theorem CSD.RecordLayer.nullSeamVec_ne_zero {χ : ℝ} (hχ : χ ∈ Set.Ioo 0 (Real.pi / 2)) : nullSeamVec χ ≠ 0

theorem CSD.RecordLayer.norm_nullSeamVec (χ : ℝ) : ‖nullSeamVec χ‖ = 1

theorem CSD.RecordLayer.nullSeamMat_mulVec (χ : ℝ) : (Matrix.toEuclideanLin (nullSeamMat χ)) (EuclideanSpace.single 0 1) = nullSeamVec χ

The witness matrix sends the ready vertex vector to the landing vector.

theorem CSD.RecordLayer.nullSeamEvolve_ready (r : ℝ) (hr0 : 0 < r) (hr1 : r < 1) (θ : CircleFibre) : (nullSeamEvolve r (θ, readyState)).2 = Projectivization.mk ℂ (nullSeamVec (nullSeamAngle r θ)) ⋯

The landing identity: the propagator sends the calibrated ready state to the crossing ray.

theorem CSD.RecordLayer.momentMap_nullSeamVec (χ : ℝ) (hχ : χ ∈ Set.Ioo 0 (Real.pi / 2)) (i : Fin 3) : LF4.momentMap (Projectivization.mk ℂ (nullSeamVec χ) ⋯) i = ‖(nullSeamVec χ).ofLp i‖ ^ 2

The landing moments: m₁ = cos²χ, m₂ = sin²χ.

★ Records off the seam, both outcomes, exactly

theorem CSD.RecordLayer.nullSeam_landing_neg (r : ℝ) (hr0 : 0 < r) (hr1 : r < 1) (θ : CircleFibre) (hθ : nullSeamSign r θ < 0) : (nullSeamEvolve r (θ, readyState)).2 ∈ recordRegion 0

★ In the open first cell, the landing carries record 0 — exactly.

theorem CSD.RecordLayer.nullSeam_landing_pos (r : ℝ) (hr0 : 0 < r) (hr1 : r < 1) (θ : CircleFibre) (hθ : 0 < nullSeamSign r θ) : (nullSeamEvolve r (θ, readyState)).2 ∈ recordRegion 1

★ In the open second cell, the landing carries record 1 — exactly.

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

★ The seam is null — indeed two points.

★ Exact Born

theorem CSD.RecordLayer.nullSeam_outcome_left (r : ℝ) (hr0 : 0 < r) (hr1 : r < 1) : {θ : CircleFibre | (nullSeamEvolve r (θ, readyState)).2 ∈ recordRegion 0} = {θ : CircleFibre | nullSeamSign r θ < 0}

The record-0 outcome set is exactly the negativity region.

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

★ Exact Born, left cell: the record-0 outcome set has measure exactly r.

theorem CSD.RecordLayer.nullSeam_outcome_right (r : ℝ) (hr0 : 0 < r) (hr1 : r < 1) : {θ : CircleFibre | (nullSeamEvolve r (θ, readyState)).2 ∈ recordRegion 1} = {θ : CircleFibre | 0 < nullSeamSign r θ}

The record-1 outcome set is exactly the positivity region.

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

★ Exact Born, right cell: the record-1 outcome set has measure exactly 1 − r.

★★ Continuity and measure invariance

theorem CSD.RecordLayer.continuous_nullSeamMat_entry (r : ℝ) (a b : Fin 3) : Continuous fun (θ : CircleFibre) => nullSeamMat (nullSeamAngle r θ) a b

Entrywise continuity of the witness family over the register.

theorem CSD.RecordLayer.continuous_nullSeamEvolve_snd (r : ℝ) : Continuous fun (y : CircleFibre × Pointer 2) => nullSeamUU r y.1 • y.2

The pointer component of the null-seam propagator is continuous.

theorem CSD.RecordLayer.continuous_nullSeamEvolve (r : ℝ) : Continuous (nullSeamEvolve r)

★★ The null-seam propagator is continuous on the whole arena — the property the piecewise horn provably cannot have.

noncomputable def CSD.RecordLayer.nullSeamMeasure (q₀ : Pointer 2) : MeasureTheory.Measure (CircleFibre × Pointer 2)

The null-seam arena's invariant measure: Haar on the register, Fubini–Study on the pointer. Not called Liouville: S¹ × ℂℙ² is odd-dimensional, hence not symplectic (naming corrected 2026-08-03, fifth review).

Equations

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

instance CSD.RecordLayer.instIsProbabilityMeasureProdCircleFibrePointerOfNatNatNullSeamMeasure (q₀ : Pointer 2) : MeasureTheory.IsProbabilityMeasure (nullSeamMeasure q₀)

theorem CSD.RecordLayer.nullSeamEvolve_measurePreserving (r : ℝ) (q₀ : Pointer 2) : MeasureTheory.MeasurePreserving (nullSeamEvolve r) (nullSeamMeasure q₀) (nullSeamMeasure q₀)

★★ Measure invariance — a skew product: register conserved, every register slice acts by an FS-preserving unitary.

★★ The third horn, bundled

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

The third horn: continuous, measure-preserving dynamics whose records from the calibrated ready state are exact and correct off a two-point seam, with exact Born weights. The price is the Dirac calibration — see the module docstring's trilemma.

• continuity : Continuous (nullSeamEvolve r)

  The propagator is continuous on the whole arena.

• invariant (q₀ : Pointer 2) : MeasureTheory.MeasurePreserving (nullSeamEvolve r) (nullSeamMeasure q₀) (nullSeamMeasure q₀)

  Measure invariance at every Fubini–Study base point.

• landing_left (θ : CircleFibre) : nullSeamSign r θ < 0 → (nullSeamEvolve r (θ, readyState)).2 ∈ recordRegion 0

  Correct record in the open first cell — exactly.

• landing_right (θ : CircleFibre) : 0 < nullSeamSign r θ → (nullSeamEvolve r (θ, readyState)).2 ∈ recordRegion 1

  Correct record in the open second cell — exactly.

• seam_null : MeasureTheory.volume {θ : CircleFibre | nullSeamSign r θ = 0} = 0

  The seam is null.

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

  Exact Born, first outcome.

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

  Exact Born, second outcome.

theorem CSD.RecordLayer.nullSeamClosure (r : ℝ) (hr0 : 0 < r) (hr1 : r < 1) : NullSeamClosure r

★★ The third horn exists — for every cell split r ∈ (0, 1).