SigmaLayer/NullSeamGeneralN: the third horn at every N (D3b)

Category: dynamical measurement — the general-N null-seam witness (specs/BACKLOG.md D3b; the two-cell witness is NullSeamWitness.lean).

The construction

N cells on the register circle, cut at the corpus's own cumulative Born positions loSum r i (BornFibrePartition.lean) of a positive weight vector r summing to 1. Each closed cell is realised as a closed ball cellArc r i around the existing cell midpoint cellMid r i (PointerWeights.lean), radius r i / 2, which hands the cell mass to AddCircle.volume_closedBall with no bespoke measure computation; the open cell is a rep-preimage (CircleFibre.lean), so measurability is free.

The landing amplitudes are plateau tents cellTent r i θ = max 0 (cellGap r − infDist θ (cellArc r i)) with cellGap = (min r)/2: value exactly cellGap on the whole closed cell, decaying outside, vanishing at distance cellGap. Off the seam the active cell's tent dominates strictly (it sits at the plateau, every other tent is strictly below it, and at most one other tent is nonzero — the separation estimates); at a seam point the two adjacent tents are equal — the kiss. The record criterion momentMap > ½ therefore reads: record i exactly on the open cell i, no record exactly on the N seam points.

The propagator's unitary is a single global formula — the rotation by π/2 in the plane spanned by the ready direction f₀ and the (normalised) amplitude vector a ⊥ f₀:

M(a) = I − f₀f₀ᵀ − aaᵀ + af₀ᵀ − f₀aᵀ,

orthogonal for every unit a with a₀ = 0 (seamRotation_mem), with first column a (the landing). Because M is a fixed polynomial in the amplitudes, continuity of the propagator reduces to continuity of the tents — there is no per-boundary gluing of plane rotations, and hence none of the monodromy trouble a piecewise-rotation design would have at the wrap.

Relation to the two-cell witness

NullSeamWitness.lean stands as the minimal exhibit (its (f₁,f₂)-plane rotation is the N = 2 kissing-crossing in bespoke form); this module proves the same closure shape for every N ≥ 2 and every weight vector: continuity, measure invariance, exact records off an N-point null seam, and exact Born mass r i per cell (nullSeamGeneralClosure). The scope notes of the two-cell module apply verbatim: the exactness is at the Dirac-calibrated ready point (the third horn's price — posMeasure_noRecord_pointer), and the cell split r plays the Born-weight role without a preparation in the arena.

Cumulative-position extras

loSum (BornFibrePartition.lean) carries the ordering lemmas (loSum_add_le_loSum, loSum_add_self_le_one); the two small identities below complete the tiling picture.

theorem CSD.RecordLayer.loSum_nonneg {N : ℕ} (r : Fin N → ℝ) (hr : ∀ (i : Fin N), 0 < r i) (i : Fin N) : 0 ≤ loSum r i

theorem CSD.RecordLayer.loSum_zero_val {N : ℕ} {i : Fin N} (r : Fin N → ℝ) (hi : ↑i = 0) : loSum r i = 0

theorem CSD.RecordLayer.loSum_succ_val {N : ℕ} (r : Fin N → ℝ) {i j : Fin N} (hij : ↑j = ↑i + 1) : loSum r j = loSum r i + r i

Consecutive cumulative positions: the cell for i ends where the cell for the next index begins.

theorem CSD.RecordLayer.loSum_last_add {N : ℕ} (r : Fin N → ℝ) (hsum : ∑ i : Fin N, r i = 1) {i : Fin N} (hi : ↑i + 1 = N) : loSum r i + r i = 1

The last cell ends at 1.

The canonical representative

theorem CSD.RecordLayer.coe_rep (θ : CircleFibre) : ↑(rep θ) = θ

theorem CSD.RecordLayer.rep_mem (θ : CircleFibre) : rep θ ∈ Set.Ioc 0 1

The tent half-width

noncomputable def CSD.RecordLayer.cellGap {N : ℕ} [NeZero N] (r : Fin N → ℝ) : ℝ

The tent half-width: half the smallest cell width. Every tent extends exactly cellGap beyond its cell, so tents of cells that do not share a boundary never overlap.

Equations

• CSD.RecordLayer.cellGap r = Finset.univ.inf' ⋯ r / 2

theorem CSD.RecordLayer.cellGap_pos {N : ℕ} [NeZero N] (r : Fin N → ℝ) (hr : ∀ (i : Fin N), 0 < r i) : 0 < cellGap r

theorem CSD.RecordLayer.two_cellGap_le {N : ℕ} [NeZero N] (r : Fin N → ℝ) (i : Fin N) : 2 * cellGap r ≤ r i

Circle lemmas beyond the two-cell toolkit

theorem CSD.RecordLayer.circle_dist_coe_eq {a b : ℝ} (h : |a - b| ≤ 1 / 2) : dist ↑a ↑b = |a - b|

On lifts within a half-period, the circle distance is exact.

theorem CSD.RecordLayer.circle_dist_coe_ge (a b : ℝ) : min |a - b| (1 - |a - b|) ≤ dist ↑a ↑b

The circle distance of two lifts is at least min |a−b| (1 − |a−b|).

The cells

noncomputable def CSD.RecordLayer.cellArc {N : ℕ} (r : Fin N → ℝ) (i : Fin N) : Set CircleFibre

Closed cell i: the closed ball of radius r i / 2 around the existing cell midpoint cellMid r i (PointerWeights.lean). Equal to the arc image of its lift interval (cellArc_eq_image).

Equations

• CSD.RecordLayer.cellArc r i = Metric.closedBall (CSD.RecordLayer.cellMid r i) (r i / 2)

noncomputable def CSD.RecordLayer.openCell {N : ℕ} (r : Fin N → ℝ) (i : Fin N) : Set CircleFibre

The open cell: the rep-preimage of the open CDF interval, so measurability is definitional (compare circleCell).

Equations

• CSD.RecordLayer.openCell r i = CSD.RecordLayer.rep ⁻¹' Set.Ioo (CSD.RecordLayer.loSum r i) (CSD.RecordLayer.loSum r i + r i)

noncomputable def CSD.RecordLayer.seamPoint {N : ℕ} (r : Fin N → ℝ) (i : Fin N) : CircleFibre

The seam point at the left end of cell i. The N of them are the cell boundaries (the right end of the last cell wraps to the left end of the first).

Equations

• CSD.RecordLayer.seamPoint r i = ↑(CSD.RecordLayer.loSum r i)

theorem CSD.RecordLayer.measurableSet_openCell {N : ℕ} {r : Fin N → ℝ} (i : Fin N) : MeasurableSet (openCell r i)

theorem CSD.RecordLayer.cellArc_eq_image {N : ℕ} {r : Fin N → ℝ} (hr : ∀ (i : Fin N), 0 < r i) (hsum : ∑ i : Fin N, r i = 1) (i : Fin N) : cellArc r i = (fun (s : ℝ) => ↑s) '' Set.Icc (loSum r i) (loSum r i + r i)

The closed cell is the arc image of its lift interval.

theorem CSD.RecordLayer.exists_rep_mem_cell {N : ℕ} [NeZero N] {r : Fin N → ℝ} (hsum : ∑ i : Fin N, r i = 1) (θ : CircleFibre) : ∃ (i : Fin N), rep θ ∈ Set.Ioc (loSum r i) (loSum r i + r i)

Every circle point lies in some closed cell (via its canonical representative, whose CDF interval is found by taking the largest cumulative position strictly below it).

theorem CSD.RecordLayer.openCell_subset_cellArc {N : ℕ} {r : Fin N → ℝ} (hr : ∀ (i : Fin N), 0 < r i) (hsum : ∑ i : Fin N, r i = 1) (i : Fin N) : openCell r i ⊆ cellArc r i

The open cell sits inside the closed cell.

theorem CSD.RecordLayer.volume_openCell {N : ℕ} {r : Fin N → ℝ} (hr : ∀ (i : Fin N), 0 < r i) (hsum : ∑ i : Fin N, r i = 1) (i : Fin N) : MeasureTheory.volume (openCell r i) = ENNReal.ofReal (r i)

The Born mass of an open cell is exactly its weight (the Ioo sibling of volume_circleCell, same measure-preserving route).

The tents

noncomputable def CSD.RecordLayer.cellTent {N : ℕ} [NeZero N] (r : Fin N → ℝ) (i : Fin N) (θ : CircleFibre) : ℝ

The plateau tent of cell i: value cellGap r on the whole closed cell, decaying with the distance outside, vanishing at distance cellGap r.

Equations

• CSD.RecordLayer.cellTent r i θ = max 0 (CSD.RecordLayer.cellGap r - Metric.infDist θ (CSD.RecordLayer.cellArc r i))

theorem CSD.RecordLayer.continuous_cellTent {N : ℕ} [NeZero N] {r : Fin N → ℝ} (i : Fin N) : Continuous (cellTent r i)

theorem CSD.RecordLayer.cellTent_nonneg {N : ℕ} [NeZero N] {r : Fin N → ℝ} (i : Fin N) (θ : CircleFibre) : 0 ≤ cellTent r i θ

theorem CSD.RecordLayer.cellTent_le {N : ℕ} [NeZero N] {r : Fin N → ℝ} (hr : ∀ (i : Fin N), 0 < r i) (i : Fin N) (θ : CircleFibre) : cellTent r i θ ≤ cellGap r

theorem CSD.RecordLayer.cellTent_of_mem {N : ℕ} [NeZero N] {r : Fin N → ℝ} (hr : ∀ (i : Fin N), 0 < r i) {i : Fin N} {θ : CircleFibre} (hθ : θ ∈ cellArc r i) : cellTent r i θ = cellGap r

On the closed cell the tent sits at its plateau.

theorem CSD.RecordLayer.cellArc_nonempty {N : ℕ} {r : Fin N → ℝ} (hr : ∀ (i : Fin N), 0 < r i) (i : Fin N) : (cellArc r i).Nonempty

theorem CSD.RecordLayer.cellTent_lt_of_notMem {N : ℕ} [NeZero N] {r : Fin N → ℝ} (hr : ∀ (i : Fin N), 0 < r i) {i : Fin N} {θ : CircleFibre} (hθ : θ ∉ cellArc r i) : cellTent r i θ < cellGap r

Off the closed cell the tent is strictly below its plateau.

theorem CSD.RecordLayer.cellTent_eq_zero {N : ℕ} [NeZero N] {r : Fin N → ℝ} {i : Fin N} {θ : CircleFibre} (h : cellGap r ≤ Metric.infDist θ (cellArc r i)) : cellTent r i θ = 0

Vanishing at distance cellGap.

theorem CSD.RecordLayer.infDist_lt_of_cellTent_pos {N : ℕ} [NeZero N] {r : Fin N → ℝ} {i : Fin N} {θ : CircleFibre} (h : 0 < cellTent r i θ) : Metric.infDist θ (cellArc r i) < cellGap r

Positivity means the cell is within tent reach.

Separation: at most one foreign tent is ever within reach

theorem CSD.RecordLayer.cellTent_pos_branches {N : ℕ} [NeZero N] {r : Fin N → ℝ} (hr : ∀ (i : Fin N), 0 < r i) (hsum : ∑ i : Fin N, r i = 1) {k : Fin N} {s : ℝ} (hpos : 0 < cellTent r k ↑s) : ∃ (t : ℝ), loSum r k ≤ t ∧ t ≤ loSum r k + r k ∧ (|s - t| < cellGap r ∨ 1 - |s - t| < cellGap r)

Tent-positivity at a lift, resolved into the two approach directions: if cell k's tent is positive at coe s, then s is within cellGap of the cell's lift interval either directly or around the wrap.

theorem CSD.RecordLayer.openCell_disjoint_cellArc {N : ℕ} {r : Fin N → ℝ} (hr : ∀ (i : Fin N), 0 < r i) (hsum : ∑ i : Fin N, r i = 1) {i k : Fin N} (hik : k ≠ i) {θ : CircleFibre} (hθ : θ ∈ openCell r i) : θ ∉ cellArc r k

The open cell meets no other closed cell.

theorem CSD.RecordLayer.cellTent_pos_left {N : ℕ} [NeZero N] {r : Fin N → ℝ} (hr : ∀ (i : Fin N), 0 < r i) (hsum : ∑ i : Fin N, r i = 1) {i k : Fin N} (hki : ↑k < ↑i) {s : ℝ} (hsi : loSum r i < s ∧ s < loSum r i + r i) (hpos : 0 < cellTent r k ↑s) : s < loSum r k + r k + cellGap r ∨ loSum r k + 1 - cellGap r < s

Foreign-tent approach bounds, cell to the left of the active one.

theorem CSD.RecordLayer.cellTent_pos_right {N : ℕ} [NeZero N] {r : Fin N → ℝ} (hr : ∀ (i : Fin N), 0 < r i) (hsum : ∑ i : Fin N, r i = 1) {i k : Fin N} (hik : ↑i < ↑k) {s : ℝ} (hsi : loSum r i < s ∧ s < loSum r i + r i) (hpos : 0 < cellTent r k ↑s) : loSum r k - cellGap r < s ∨ s < loSum r k + r k + cellGap r - 1

Foreign-tent approach bounds, cell to the right of the active one.

theorem CSD.RecordLayer.cellTent_pair_exclusion {N : ℕ} [NeZero N] {r : Fin N → ℝ} (hr : ∀ (i : Fin N), 0 < r i) (hsum : ∑ i : Fin N, r i = 1) {i k l : Fin N} (hk : k ≠ i) (hl : l ≠ i) (hkl : ↑k < ↑l) {θ : CircleFibre} (hθ : θ ∈ openCell r i) : ¬(0 < cellTent r k θ ∧ 0 < cellTent r l θ)

At most one foreign tent is within reach at any point of an open cell. The twelve position/branch combinations each contradict the cumulative ordering (loSum_add_le_loSum), the one-turn bound (loSum_add_self_le_one), or the width floor (two_cellGap_le).

The amplitude vector and the record criterion

noncomputable def CSD.RecordLayer.tentVec {N : ℕ} [NeZero N] (r : Fin N → ℝ) (θ : CircleFibre) : EuclideanSpace ℂ (Fin (N + 1))

The (unnormalised) landing amplitude vector: zero in the ready slot, tent i in record slot i.succ.

Equations

• CSD.RecordLayer.tentVec r θ = WithLp.toLp 2 fun (k : Fin (N + 1)) => Fin.cases 0 (fun (i : Fin N) => ↑(CSD.RecordLayer.cellTent r i θ)) k

theorem CSD.RecordLayer.tentVec_zero {N : ℕ} [NeZero N] {r : Fin N → ℝ} (θ : CircleFibre) : (tentVec r θ).ofLp 0 = 0

theorem CSD.RecordLayer.tentVec_succ {N : ℕ} [NeZero N] {r : Fin N → ℝ} (θ : CircleFibre) (i : Fin N) : (tentVec r θ).ofLp i.succ = ↑(cellTent r i θ)

theorem CSD.RecordLayer.exists_cellTent_plateau {N : ℕ} [NeZero N] {r : Fin N → ℝ} (hr : ∀ (i : Fin N), 0 < r i) (hsum : ∑ i : Fin N, r i = 1) (θ : CircleFibre) : ∃ (i : Fin N), cellTent r i θ = cellGap r

Every point sits on some closed cell's plateau.

theorem CSD.RecordLayer.tentVec_ne_zero {N : ℕ} [NeZero N] {r : Fin N → ℝ} (hr : ∀ (i : Fin N), 0 < r i) (hsum : ∑ i : Fin N, r i = 1) (θ : CircleFibre) : tentVec r θ ≠ 0

theorem CSD.RecordLayer.norm_sq_tentVec {N : ℕ} [NeZero N] {r : Fin N → ℝ} (θ : CircleFibre) : ‖tentVec r θ‖ ^ 2 = ∑ i : Fin N, cellTent r i θ ^ 2

The squared norm of the tent vector is the tent sum of squares.

The seam rotation

noncomputable def CSD.RecordLayer.seamRotationR {n : ℕ} (a : Fin (n + 1) → ℝ) : Matrix (Fin (n + 1)) (Fin (n + 1)) ℝ

The rotation by π/2 in the plane spanned by the ready direction f₀ and a unit amplitude vector a ⊥ f₀, over ℝ: first column a, first row −aᵀ (off the corner), the record block I − aaᵀ.

Equations

• CSD.RecordLayer.seamRotationR a = Matrix.of fun (k l : Fin (n + 1)) => if k = 0 then if l = 0 then 0 else -a l else if l = 0 then a k else (if k = l then 1 else 0) - a k * a l

@[simp]

theorem CSD.RecordLayer.seamRotationR_zero_zero {n : ℕ} (a : Fin (n + 1) → ℝ) : seamRotationR a 0 0 = 0

@[simp]

theorem CSD.RecordLayer.seamRotationR_zero_succ {n : ℕ} (a : Fin (n + 1) → ℝ) (m : Fin n) : seamRotationR a 0 m.succ = -a m.succ

@[simp]

theorem CSD.RecordLayer.seamRotationR_succ_zero {n : ℕ} (a : Fin (n + 1) → ℝ) (k : Fin n) : seamRotationR a k.succ 0 = a k.succ

@[simp]

theorem CSD.RecordLayer.seamRotationR_succ_succ {n : ℕ} (a : Fin (n + 1) → ℝ) (k l : Fin n) : seamRotationR a k.succ l.succ = (if k = l then 1 else 0) - a k.succ * a l.succ

theorem CSD.RecordLayer.seamRotationR_orthogonal {n : ℕ} (a : Fin (n + 1) → ℝ) (h0 : a 0 = 0) (hsum : ∑ k : Fin (n + 1), a k ^ 2 = 1) : (seamRotationR a).transpose * seamRotationR a = 1

Orthogonality of the seam rotation, for every unit amplitude vector with empty ready slot.

noncomputable def CSD.RecordLayer.seamRotation {n : ℕ} (a : Fin (n + 1) → ℝ) : Matrix (Fin (n + 1)) (Fin (n + 1)) ℂ

The seam rotation over ℂ: the real matrix, entrywise embedded.

Equations

• CSD.RecordLayer.seamRotation a = (CSD.RecordLayer.seamRotationR a).map Complex.ofReal

theorem CSD.RecordLayer.seamRotation_mem {n : ℕ} (a : Fin (n + 1) → ℝ) (h0 : a 0 = 0) (hsum : ∑ k : Fin (n + 1), a k ^ 2 = 1) : seamRotation a ∈ Matrix.unitaryGroup (Fin (n + 1)) ℂ

theorem CSD.RecordLayer.seamRotation_mulVec_single {n : ℕ} (a : Fin (n + 1) → ℝ) (h0 : a 0 = 0) : (Matrix.toEuclideanLin (seamRotation a)) (EuclideanSpace.single 0 1) = WithLp.toLp 2 fun (k : Fin (n + 1)) => ↑(a k)

The first column of the seam rotation is the amplitude vector.

The propagator

noncomputable def CSD.RecordLayer.tentTotal {N : ℕ} [NeZero N] (r : Fin N → ℝ) (θ : CircleFibre) : ℝ

The total tent weight (the amplitude normaliser).

Equations

• CSD.RecordLayer.tentTotal r θ = √(∑ j : Fin N, CSD.RecordLayer.cellTent r j θ ^ 2)

theorem CSD.RecordLayer.tentTotal_pos {N : ℕ} [NeZero N] {r : Fin N → ℝ} (hr : ∀ (i : Fin N), 0 < r i) (hsum : ∑ i : Fin N, r i = 1) (θ : CircleFibre) : 0 < tentTotal r θ

theorem CSD.RecordLayer.sq_tentTotal {N : ℕ} [NeZero N] {r : Fin N → ℝ} (θ : CircleFibre) : tentTotal r θ ^ 2 = ∑ j : Fin N, cellTent r j θ ^ 2

noncomputable def CSD.RecordLayer.seamAmp {N : ℕ} [NeZero N] (r : Fin N → ℝ) (θ : CircleFibre) : Fin (N + 1) → ℝ

The normalised landing amplitudes: empty ready slot, tent/total in the record slots.

Equations

• CSD.RecordLayer.seamAmp r θ k = Fin.cases 0 (fun (i : Fin N) => CSD.RecordLayer.cellTent r i θ / CSD.RecordLayer.tentTotal r θ) k

theorem CSD.RecordLayer.seamAmp_zero {N : ℕ} [NeZero N] {r : Fin N → ℝ} (θ : CircleFibre) : seamAmp r θ 0 = 0

theorem CSD.RecordLayer.seamAmp_succ {N : ℕ} [NeZero N] {r : Fin N → ℝ} (θ : CircleFibre) (i : Fin N) : seamAmp r θ i.succ = cellTent r i θ / tentTotal r θ

theorem CSD.RecordLayer.seamAmp_sq_sum {N : ℕ} [NeZero N] {r : Fin N → ℝ} (hr : ∀ (i : Fin N), 0 < r i) (hsum : ∑ i : Fin N, r i = 1) (θ : CircleFibre) : ∑ k : Fin (N + 1), seamAmp r θ k ^ 2 = 1

noncomputable def CSD.RecordLayer.nullSeamGenUU {N : ℕ} [NeZero N] {r : Fin N → ℝ} (hr : ∀ (i : Fin N), 0 < r i) (hsum : ∑ i : Fin N, r i = 1) (θ : CircleFibre) : ↥(Matrix.unitaryGroup (Fin (N + 1)) ℂ)

The propagator's unitary at register point θ.

Equations

• CSD.RecordLayer.nullSeamGenUU hr hsum θ = ⟨CSD.RecordLayer.seamRotation (CSD.RecordLayer.seamAmp r θ), ⋯⟩

noncomputable def CSD.RecordLayer.nullSeamGenEvolve {N : ℕ} [NeZero N] {r : Fin N → ℝ} (hr : ∀ (i : Fin N), 0 < r i) (hsum : ∑ i : Fin N, r i = 1) : CircleFibre × Pointer N → CircleFibre × Pointer N

The general-N null-seam propagator: register conserved, pointer rotated by the seam rotation at the register's amplitudes.

Equations

• CSD.RecordLayer.nullSeamGenEvolve hr hsum y = (y.1, CSD.RecordLayer.nullSeamGenUU hr hsum y.1 • y.2)

theorem CSD.RecordLayer.seamAmp_toLp_smul {N : ℕ} [NeZero N] {r : Fin N → ℝ} (θ : CircleFibre) : (WithLp.toLp 2 fun (k : Fin (N + 1)) => ↑(seamAmp r θ k)) = ↑(tentTotal r θ)⁻¹ • tentVec r θ

The amplitude vector is the tent vector, normalised.

theorem CSD.RecordLayer.nullSeamGenEvolve_ready {N : ℕ} [NeZero N] {r : Fin N → ℝ} (hr : ∀ (i : Fin N), 0 < r i) (hsum : ∑ i : Fin N, r i = 1) (θ : CircleFibre) : (nullSeamGenEvolve hr hsum (θ, readyState)).2 = Projectivization.mk ℂ (tentVec r θ) ⋯

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

Records: exactly the open cells

theorem CSD.RecordLayer.momentMap_tentVec {N : ℕ} [NeZero N] {r : Fin N → ℝ} (hr : ∀ (i : Fin N), 0 < r i) (hsum : ∑ i : Fin N, r i = 1) (θ : CircleFibre) (i : Fin N) : LF4.momentMap (Projectivization.mk ℂ (tentVec r θ) ⋯) i.succ = cellTent r i θ ^ 2 / ∑ j : Fin N, cellTent r j θ ^ 2

The landing moments are the normalised squared tents.

theorem CSD.RecordLayer.tentVec_record_iff {N : ℕ} [NeZero N] {r : Fin N → ℝ} (hr : ∀ (i : Fin N), 0 < r i) (hsum : ∑ i : Fin N, r i = 1) (θ : CircleFibre) (i : Fin N) : Projectivization.mk ℂ (tentVec r θ) ⋯ ∈ recordRegion i ↔ ∑ j ∈ Finset.univ.erase i, cellTent r j θ ^ 2 < cellTent r i θ ^ 2

The record criterion: outcome i is recorded iff cell i's tent strictly dominates all the others combined.

theorem CSD.RecordLayer.nullSeamGen_landing {N : ℕ} [NeZero N] {r : Fin N → ℝ} (hr : ∀ (i : Fin N), 0 < r i) (hsum : ∑ i : Fin N, r i = 1) {i : Fin N} {θ : CircleFibre} (hθ : θ ∈ openCell r i) : (nullSeamGenEvolve hr hsum (θ, readyState)).2 ∈ recordRegion i

★ Records on the open cells — exactly.

The seam: the kiss, and no record

theorem CSD.RecordLayer.seamPoint_mem_cellArc {N : ℕ} {r : Fin N → ℝ} (hr : ∀ (i : Fin N), 0 < r i) (hsum : ∑ i : Fin N, r i = 1) (i : Fin N) : seamPoint r i ∈ cellArc r i

theorem CSD.RecordLayer.coe_one_eq_coe_zero : ↑1 = ↑0

theorem CSD.RecordLayer.seamPoint_mem_left {N : ℕ} {r : Fin N → ℝ} (hr : ∀ (i : Fin N), 0 < r i) (hsum : ∑ i : Fin N, r i = 1) (hN : 1 < N) (i : Fin N) : ∃ (i' : Fin N), i' ≠ i ∧ seamPoint r i ∈ cellArc r i'

Every seam point also sits on its left neighbour's plateau — the kiss. Needs N ≥ 2 (with a single cell, the seam point's only cell is its own).

theorem CSD.RecordLayer.nullSeamGen_seam_no_record {N : ℕ} [NeZero N] {r : Fin N → ℝ} (hr : ∀ (i : Fin N), 0 < r i) (hsum : ∑ i : Fin N, r i = 1) (hN : 1 < N) (i j : Fin N) : (nullSeamGenEvolve hr hsum (seamPoint r i, readyState)).2 ∉ recordRegion j

★ No record at any seam point, for any outcome — the kiss: two tents sit at the plateau, so no tent strictly dominates.

The outcome sets are exactly the open cells

theorem CSD.RecordLayer.openCell_or_seam {N : ℕ} [NeZero N] {r : Fin N → ℝ} (hsum : ∑ i : Fin N, r i = 1) (θ : CircleFibre) : (∃ (i : Fin N), θ ∈ openCell r i) ∨ ∃ (i : Fin N), θ = seamPoint r i

Every register point is in an open cell or on the seam.

theorem CSD.RecordLayer.nullSeamGen_outcome {N : ℕ} [NeZero N] {r : Fin N → ℝ} (hr : ∀ (i : Fin N), 0 < r i) (hsum : ∑ i : Fin N, r i = 1) (hN : 1 < N) (i : Fin N) : {θ : CircleFibre | (nullSeamGenEvolve hr hsum (θ, readyState)).2 ∈ recordRegion i} = openCell r i

★ The outcome set for record i is exactly the open cell i.

theorem CSD.RecordLayer.nullSeamGen_born {N : ℕ} [NeZero N] {r : Fin N → ℝ} (hr : ∀ (i : Fin N), 0 < r i) (hsum : ∑ i : Fin N, r i = 1) (hN : 1 < N) (i : Fin N) : MeasureTheory.volume {θ : CircleFibre | (nullSeamGenEvolve hr hsum (θ, readyState)).2 ∈ recordRegion i} = ENNReal.ofReal (r i)

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

theorem CSD.RecordLayer.nullSeamGen_seam_null {N : ℕ} {r : Fin N → ℝ} : MeasureTheory.volume (Set.range (seamPoint r)) = 0

★ The seam is null — indeed N points.

★★ Continuity and measure invariance

theorem CSD.RecordLayer.continuous_tentTotal {N : ℕ} [NeZero N] {r : Fin N → ℝ} : Continuous (tentTotal r)

theorem CSD.RecordLayer.continuous_seamAmp {N : ℕ} [NeZero N] {r : Fin N → ℝ} (hr : ∀ (i : Fin N), 0 < r i) (hsum : ∑ i : Fin N, r i = 1) (k : Fin (N + 1)) : Continuous fun (θ : CircleFibre) => seamAmp r θ k

theorem CSD.RecordLayer.continuous_seamRotation_entry {N : ℕ} [NeZero N] {r : Fin N → ℝ} (hr : ∀ (i : Fin N), 0 < r i) (hsum : ∑ i : Fin N, r i = 1) (a b : Fin (N + 1)) : Continuous fun (θ : CircleFibre) => seamRotation (seamAmp r θ) a b

Entrywise continuity of the seam rotation over the register.

theorem CSD.RecordLayer.continuous_nullSeamGenEvolve_snd {N : ℕ} [NeZero N] {r : Fin N → ℝ} (hr : ∀ (i : Fin N), 0 < r i) (hsum : ∑ i : Fin N, r i = 1) : Continuous fun (y : CircleFibre × Pointer N) => nullSeamGenUU hr hsum y.1 • y.2

The pointer component of the propagator is continuous.

theorem CSD.RecordLayer.continuous_nullSeamGenEvolve {N : ℕ} [NeZero N] {r : Fin N → ℝ} (hr : ∀ (i : Fin N), 0 < r i) (hsum : ∑ i : Fin N, r i = 1) : Continuous (nullSeamGenEvolve hr hsum)

★★ The propagator is continuous on the whole arena.

noncomputable def CSD.RecordLayer.nullSeamGenMeasure {N : ℕ} (q₀ : Pointer N) : MeasureTheory.Measure (CircleFibre × Pointer N)

The arena's invariant measure: Haar on the register, Fubini–Study on the pointer (the same product as the two-cell witness's nullSeamMeasure).

Equations

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

instance CSD.RecordLayer.instIsProbabilityMeasureProdCircleFibrePointerNullSeamGenMeasure {N : ℕ} (q₀ : Pointer N) : MeasureTheory.IsProbabilityMeasure (nullSeamGenMeasure q₀)

theorem CSD.RecordLayer.nullSeamGenEvolve_measurePreserving {N : ℕ} [NeZero N] {r : Fin N → ℝ} (hr : ∀ (i : Fin N), 0 < r i) (hsum : ∑ i : Fin N, r i = 1) (q₀ : Pointer N) : MeasureTheory.MeasurePreserving (nullSeamGenEvolve hr hsum) (nullSeamGenMeasure q₀) (nullSeamGenMeasure q₀)

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

★★ The third horn at every N, bundled

structure CSD.RecordLayer.NullSeamGenClosure {N : ℕ} [NeZero N] (r : Fin N → ℝ) (hr : ∀ (i : Fin N), 0 < r i) (hsum : ∑ i : Fin N, r i = 1) (hN : 1 < N) : Prop

The general-N third horn: continuous, measure-preserving dynamics on S¹ × ℂℙ^N whose records from the calibrated ready state are exact and correct off an N-point null seam, with exact Born mass r i per cell. The price is unchanged from the two-cell witness: Dirac calibration (posMeasure_noRecord_pointer prices the alternative).

• continuity : Continuous (nullSeamGenEvolve hr hsum)

  The propagator is continuous on the whole arena.

• invariant (q₀ : Pointer N) : MeasureTheory.MeasurePreserving (nullSeamGenEvolve hr hsum) (nullSeamGenMeasure q₀) (nullSeamGenMeasure q₀)

  Measure invariance at every Fubini–Study base point.

• landing (i : Fin N) (θ : CircleFibre) : θ ∈ openCell r i → (nullSeamGenEvolve hr hsum (θ, readyState)).2 ∈ recordRegion i

  Correct record on every open cell — exactly.

• seam_kiss (i j : Fin N) : (nullSeamGenEvolve hr hsum (seamPoint r i, readyState)).2 ∉ recordRegion j

  No record at any seam point, for any outcome — the kiss.

• seam_null : MeasureTheory.volume (Set.range (seamPoint r)) = 0

  The seam is null.

• born (i : Fin N) : MeasureTheory.volume {θ : CircleFibre | (nullSeamGenEvolve hr hsum (θ, readyState)).2 ∈ recordRegion i} = ENNReal.ofReal (r i)

  Exact Born, every outcome.

theorem CSD.RecordLayer.nullSeamGenClosure {N : ℕ} [NeZero N] (r : Fin N → ℝ) (hr : ∀ (i : Fin N), 0 < r i) (hsum : ∑ i : Fin N, r i = 1) (hN : 1 < N) : NullSeamGenClosure r hr hsum hN

★★ The third horn exists at every N ≥ 2 and every weight vector — D3b discharged.

theorem CSD.RecordLayer.nullSeamGenClosure_uniform {N : ℕ} [NeZero N] (hN : 1 < N) : NullSeamGenClosure (fun (x : Fin N) => (↑N)⁻¹) ⋯ ⋯ hN

The uniform witness: N cells of weight 1/N each — non-vacuity of the closure at every N ≥ 2.