Stability that scales with the coarse boundaries

Category: 7-SigmaLayer (the record layer — Paper C A7). BACKLOG #138 (out of #131 obligation (2)): the sharpening TwoWingStability.lean did not claim.

#103 bounded the microstates a record write relabels by N · δ, one boundary band per fine cell, and TwoWingStability.lean inherited that bound for the coarse two-wing reading without improving it. This file proves the bound the coarse reading deserves: one band per coarse boundary, where a coarse boundary is an index k whose decoded value differs from that of the cyclically next cell (IsCoarseBoundary, coarseBoundaryCount).

The argument

• Every microstate lies in a basin (★ exists_mem_globalBasin). The rates sum to one, so the arcs tile (0, 1] exactly, not merely almost everywhere: the none value of fineIndex and the 0 value of outcomeCode are never taken. This strengthens globalBasin_ae_total.
• A write of size δ ≤ 1 moves the representative by δ, wrapping at most once (rep_sigmaShift): either rep ↦ rep + δ or, past the top of the turn, rep ↦ rep + δ − 1 (rep_add_coe_of_one_lt, the wrap-around companion of rep_add_coe).
• A coarse relabelling crosses a coarse boundary within δ (★★ coarseCode_ne_subset). If the microstate sits in cell i and the written point in cell j with different coarse values, then along the cyclic path from i to j some consecutive pair of cells differs (exists_boundary_between, a discrete intermediate-value lemma), and the representative lies in the last δ before that boundary — read cyclically, so the band at a boundary T is (T − δ, T] ∪ (T + 1 − δ, 1] (cyclicBand), of epistemic measure at most δ (★ measure_cyclicBand_le).
• Hence ★★★ measure_coarseCode_ne_le: the microstates whose coarse reading a write of size δ ≤ 1 changes have epistemic measure at most #boundaries · δ; uniformly over the horizon (★★★ measure_exists_coarseCode_ne_le) and under a drift (★★★ measure_drift_coarseCode_ne_le).
• coarseBoundaryCount_le: the count is at most N, so #103's bound is the worst case; and ★★ coarseBoundaryCount_comp_le: a decoding that groups adjacent cells into m contiguous blocks has at most m boundaries, whatever the block values. For the two-wing record this is ★★★ measure_wingCode_ne_le_of_blocks: a contiguous decoding into the experiment's m = 4 joint outcomes is stable outside a set of measure 4 · δ, independent of the Hilbert dimension N.

Honest scope

• Writes of at most one turn (δ ≤ 1, ω · T ≤ 1). A longer write can wrap several times; the bound #boundaries · δ is then trivially true for any decoding with a boundary and the hypothesis is kept rather than discharged by that remark.
• Contiguity is a hypothesis on the decoding, stated as a factorisation w = v ∘ g through a monotone block map g : Fin N → Fin m. The row's worry stands: LF6.pointerDecode groups cells by the pointer half of an arbitrary index equivalence, which need not be contiguous, and for a non-contiguous decoding the count can be N. Nothing here chooses the equivalence.
• The row's first deliverable, "a write moves a microstate to the next cell or nowhere", is true only when the write is shorter than the next cell; the covering lemma above replaces it by the statement that holds for every δ ≤ 1.
• The write is the fibre translation sigmaShift, as in #103 and TwoWingStability.lean: the base and the symplectic partner are fixed; no base motion is composed with this, and this is not invariance and contains no mixing claim.

References: specs/BACKLOG.md #138, #131 obligation (2), #103; RecordLayer/MacrostateStability.lean (sigmaShift, cellTop, edgeBand, measure_edgeBand_le, measure_unstableSet_le), RecordLayer/TwoWingStability.lean (measure_wingCode_ne_le, the bound sharpened here), RecordLayer/TwoWingCoarsening.lean (fineIndex, wingCode), RecordLayer/CircleFibre.lean (rep_add_coe, volume_rep_preimage_Ioc), RecordLayer/NullSeamGeneralN.lean (loSum_succ_val, loSum_last_add), LF6/TwoWingRecord.lean (pointerDecode).

Every microstate lies in a basin

theorem CSD.RecordLayer.exists_mem_globalBasin {N : ℕ} (c : ContextField N) (x : LF4.KSigma N) : ∃ (i : Fin N), x ∈ globalBasin c i

★ Every microstate lies in a basin. The rates sum to one, so the arcs tile the whole turn: the fine code is never 0. Strengthens globalBasin_ae_total.

theorem CSD.RecordLayer.outcomeCode_ne_zero {N : ℕ} (c : ContextField N) (x : LF4.KSigma N) : outcomeCode c x ≠ 0

The fine code is never 0.

theorem CSD.RecordLayer.fineIndex_ne_none {N : ℕ} (c : ContextField N) (x : LF4.KSigma N) : fineIndex c x ≠ none

The fine index is never none.

The written representative: forward by δ, wrapping at most once

theorem CSD.RecordLayer.rep_add_coe_of_one_lt {θ : CircleFibre} {δ : ℝ} (h1 : 1 < rep θ + δ) (h2 : rep θ + δ ≤ 2) : rep (θ + ↑δ) = rep θ + δ - 1

The wrap-around companion of rep_add_coe: when the shifted representative overshoots the turn by less than one, it drops by exactly 1.

theorem CSD.RecordLayer.rep_sigmaShift {N : ℕ} {δ : ℝ} (hδ0 : 0 ≤ δ) (hδ1 : δ ≤ 1) (x : LF4.KSigma N) : rep x.2.1 + δ ≤ 1 ∧ rep (sigmaShift δ x).2.1 = rep x.2.1 + δ ∨ 1 < rep x.2.1 + δ ∧ rep (sigmaShift δ x).2.1 = rep x.2.1 + δ - 1

A write of at most one turn moves the representative by δ, wrapping at most once.

Cell endpoints

theorem CSD.RecordLayer.cellTop_nonneg {N : ℕ} (c : ContextField N) (k : Fin N) (x : LF4.KSigma N) : 0 ≤ cellTop c k x

The upper endpoint of a cell is non-negative.

theorem CSD.RecordLayer.cellTop_mono {N : ℕ} (c : ContextField N) (x : LF4.KSigma N) {i k : Fin N} (h : ↑i ≤ ↑k) : cellTop c i x ≤ cellTop c k x

Cell tops are monotone in the index.

theorem CSD.RecordLayer.cellTop_le_loSum_of_lt {N : ℕ} (c : ContextField N) (x : LF4.KSigma N) {k j : Fin N} (h : ↑k < ↑j) : cellTop c k x ≤ loSum (c.rate x.1) j

A cell's top is at most the lower endpoint of every later cell.

theorem CSD.RecordLayer.cellTop_eq_one {N : ℕ} (c : ContextField N) (x : LF4.KSigma N) {k : Fin N} (h : ↑k + 1 = N) : cellTop c k x = 1

The last cell ends at the top of the turn.

The cyclic successor and the coarse boundaries

def CSD.RecordLayer.nextIdx {N : ℕ} (k : Fin N) : Fin N

The cyclic successor of an index: k + 1, or 0 after the last.

Equations

• CSD.RecordLayer.nextIdx k = if h : ↑k + 1 < N then ⟨↑k + 1, h⟩ else ⟨0, ⋯⟩

theorem CSD.RecordLayer.nextIdx_of_lt {N : ℕ} {k : Fin N} (h : ↑k + 1 < N) : nextIdx k = ⟨↑k + 1, h⟩

theorem CSD.RecordLayer.nextIdx_of_last {N : ℕ} {k : Fin N} (h : ↑k + 1 = N) : nextIdx k = ⟨0, ⋯⟩

def CSD.RecordLayer.IsCoarseBoundary {N : ℕ} {κ : Type u_1} (w : Fin N → κ) (k : Fin N) : Prop

A coarse boundary of a decoding w: an index whose value differs from the cyclically next one.

Equations

• CSD.RecordLayer.IsCoarseBoundary w k = (w k ≠ w (CSD.RecordLayer.nextIdx k))

noncomputable def CSD.RecordLayer.coarseBoundaries {N : ℕ} {κ : Type u_1} (w : Fin N → κ) : Finset (Fin N)

The coarse boundaries of a decoding, as a finite set.

Equations

• CSD.RecordLayer.coarseBoundaries w = Finset.filter (CSD.RecordLayer.IsCoarseBoundary w) Finset.univ

noncomputable def CSD.RecordLayer.coarseBoundaryCount {N : ℕ} {κ : Type u_1} (w : Fin N → κ) : ℕ

The number of coarse boundaries of a decoding.

Equations

• CSD.RecordLayer.coarseBoundaryCount w = (CSD.RecordLayer.coarseBoundaries w).card

theorem CSD.RecordLayer.mem_coarseBoundaries {N : ℕ} {κ : Type u_1} {w : Fin N → κ} {k : Fin N} : k ∈ coarseBoundaries w ↔ IsCoarseBoundary w k

theorem CSD.RecordLayer.coarseBoundaryCount_le {N : ℕ} {κ : Type u_1} (w : Fin N → κ) : coarseBoundaryCount w ≤ N

There are at most N coarse boundaries: #103's count is the worst case.

theorem CSD.RecordLayer.exists_ne_succ_of_ne {κ : Type u_1} (f : ℕ → κ) {a b : ℕ} (hab : a ≤ b) (h : f a ≠ f b) : ∃ (k : ℕ), a ≤ k ∧ k < b ∧ f k ≠ f (k + 1)

The discrete intermediate-value lemma: a sequence that differs between a and b ≥ a differs between some consecutive pair in between.

theorem CSD.RecordLayer.exists_boundary_between {N : ℕ} {κ : Type u_1} (w : Fin N → κ) {i j : Fin N} (hij : ↑i ≤ ↑j) (h : w i ≠ w j) : ∃ (k : Fin N), ↑i ≤ ↑k ∧ ↑k < ↑j ∧ IsCoarseBoundary w k

Between two indices with different values lies a coarse boundary.

The cyclic boundary band

def CSD.RecordLayer.wrapBand {N : ℕ} (c : ContextField N) (δ : ℝ) (k : Fin N) : Set (LF4.KSigma N)

The part of a boundary band that wraps past the top of the turn: the representatives within δ of the boundary T through 1, i.e. in (T + 1 − δ, 1].

Equations

• CSD.RecordLayer.wrapBand c δ k = {x : CSD.LF4.KSigma N | CSD.RecordLayer.cellTop c k x + 1 - δ < CSD.RecordLayer.rep x.2.1}

def CSD.RecordLayer.cyclicBand {N : ℕ} (c : ContextField N) (δ : ℝ) (k : Fin N) : Set (LF4.KSigma N)

The cyclic boundary band at the top of cell k: the representatives within δ before the boundary, read around the circle.

Equations

• CSD.RecordLayer.cyclicBand c δ k = CSD.RecordLayer.edgeBand c δ k ∪ CSD.RecordLayer.wrapBand c δ k

theorem CSD.RecordLayer.measurableSet_wrapBand {N : ℕ} (c : ContextField N) (δ : ℝ) (k : Fin N) : MeasurableSet (wrapBand c δ k)

theorem CSD.RecordLayer.measurableSet_cyclicBand {N : ℕ} (c : ContextField N) (δ : ℝ) (k : Fin N) : MeasurableSet (cyclicBand c δ k)

theorem CSD.RecordLayer.cyclicBand_mono {N : ℕ} (c : ContextField N) {s δ : ℝ} (h : s ≤ δ) (k : Fin N) : cyclicBand c s k ⊆ cyclicBand c δ k

A smaller write has a smaller band.

theorem CSD.RecordLayer.measure_cyclicBand_le {N : ℕ} (c : ContextField N) (δ : ℝ) (k : Fin N) (p : LF4.CPN N) : (epistemicMeasure p) (cyclicBand c δ k) ≤ ENNReal.ofReal δ

★ The cyclic band is small: its epistemic measure is at most δ, however the band wraps. The two pieces have measures min T δ and (δ − T)₊, which sum to δ.

A coarse relabelling crosses a coarse boundary within δ

noncomputable def CSD.RecordLayer.coarseCode {N : ℕ} {κ : Type u_1} (c : ContextField N) (u : Fin N → κ) (x : LF4.KSigma N) : Option κ

The coarse code of a microstate under a decoding u: the fine index, decoded. The two-wing code wingCode is this with u = w.

Equations

• CSD.RecordLayer.coarseCode c u x = Option.map u (CSD.RecordLayer.fineIndex c x)

theorem CSD.RecordLayer.wingCode_eq_coarseCode {N : ℕ} {Ω₁ : Type u_2} {Ω₂ : Type u_3} (c : ContextField N) (w : Fin N → Ω₁ × Ω₂) : wingCode c w = coarseCode c w

theorem CSD.RecordLayer.coarseCode_eq_some {N : ℕ} {κ : Type u_1} (c : ContextField N) (u : Fin N → κ) {x : LF4.KSigma N} {i : Fin N} (hx : x ∈ globalBasin c i) : coarseCode c u x = some (u i)

theorem CSD.RecordLayer.coarseCode_ne_subset {N : ℕ} {κ : Type u_1} (c : ContextField N) (u : Fin N → κ) {δ : ℝ} (hδ0 : 0 ≤ δ) (hδ1 : δ ≤ 1) : {x : LF4.KSigma N | coarseCode c u (sigmaShift δ x) ≠ coarseCode c u x} ⊆ ⋃ k ∈ coarseBoundaries u, cyclicBand c δ k

★★ A write that changes the coarse reading puts the microstate in a cyclic band at a coarse boundary. Along the cyclic path from the microstate's cell to the written point's cell some consecutive pair of cells decodes differently, and the representative lies within δ before that boundary, read around the circle.

★★★ The bounds

theorem CSD.RecordLayer.measure_coarseCode_ne_le {N : ℕ} {κ : Type u_1} (c : ContextField N) (u : Fin N → κ) {δ : ℝ} (hδ0 : 0 ≤ δ) (hδ1 : δ ≤ 1) (p : LF4.CPN N) : (epistemicMeasure p) {x : LF4.KSigma N | coarseCode c u (sigmaShift δ x) ≠ coarseCode c u x} ≤ ↑(coarseBoundaryCount u) * ENNReal.ofReal δ

★★★ Stability that scales with the coarse boundaries. The microstates whose coarse reading a write of size δ ≤ 1 changes have epistemic measure at most #boundaries · δ.

theorem CSD.RecordLayer.measure_exists_coarseCode_ne_le {N : ℕ} {κ : Type u_1} (c : ContextField N) (u : Fin N → κ) {δ : ℝ} (hδ1 : δ ≤ 1) (p : LF4.CPN N) : (epistemicMeasure p) {x : LF4.KSigma N | ∃ s ∈ Set.Icc 0 δ, coarseCode c u (sigmaShift s x) ≠ coarseCode c u x} ≤ ↑(coarseBoundaryCount u) * ENNReal.ofReal δ

★★★ One exceptional set serves the whole horizon: a smaller write has a smaller band.

theorem CSD.RecordLayer.measure_drift_coarseCode_ne_le {N : ℕ} {κ : Type u_1} (c : ContextField N) (u : Fin N → κ) {ω T : ℝ} (hω : 0 ≤ ω) (hωT : ω * T ≤ 1) (p : LF4.CPN N) : (epistemicMeasure p) {x : LF4.KSigma N | ∃ t ∈ Set.Icc 0 T, coarseCode c u (sigmaShift (ω * t) x) ≠ coarseCode c u x} ≤ ↑(coarseBoundaryCount u) * ENNReal.ofReal (ω * T)

★★★ Persistence over a horizon, scaling with the coarse boundaries. Under a drift of the record coordinate at rate ω for a total of at most one turn, the coarse reading survives all of [0, T] outside a set of measure #boundaries · ω · T.

Contiguous decodings have few boundaries

theorem CSD.RecordLayer.nextIdx_image_ne {N m : ℕ} {g : Fin N → Fin m} (hg : Monotone g) {k k' : Fin N} (hk : g k ≠ g (nextIdx k)) (hk' : g k' ≠ g (nextIdx k')) (hlt : ↑k < ↑k') : g (nextIdx k) ≠ g (nextIdx k')

Under a monotone block map, the images of the cyclic successors of two distinct boundaries differ: strictly increasing values between non-wrapping boundaries, and the wrap boundary's successor image g 0 lies below every other successor image.

theorem CSD.RecordLayer.coarseBoundaryCount_comp_le {N : ℕ} {κ : Type u_1} {m : ℕ} (v : Fin m → κ) (g : Fin N → Fin m) (hg : Monotone g) : coarseBoundaryCount (v ∘ g) ≤ m

★★ A decoding that groups adjacent cells into m contiguous blocks has at most m coarse boundaries, whatever values the blocks carry. The successor image is injective on the boundaries.

theorem CSD.RecordLayer.measure_wingCode_ne_le_of_blocks {N : ℕ} {Ω₁ : Type u_2} {Ω₂ : Type u_3} (c : ContextField N) {m : ℕ} (g : Fin N → Fin m) (hg : Monotone g) (v : Fin m → Ω₁ × Ω₂) {δ : ℝ} (hδ0 : 0 ≤ δ) (hδ1 : δ ≤ 1) (p : LF4.CPN N) : (epistemicMeasure p) {x : LF4.KSigma N | wingCode c (v ∘ g) (sigmaShift δ x) ≠ wingCode c (v ∘ g) x} ≤ ↑m * ENNReal.ofReal δ

★★★ The two-wing record under a contiguous decoding is stable in proportion to its outcome count, not the Hilbert dimension. If the decoding groups adjacent cells into m blocks, the microstates whose two-wing reading a write of size δ ≤ 1 changes have epistemic measure at most m · δ. For the experiment's four joint outcomes, m = 4, whatever N is.

theorem CSD.RecordLayer.measure_drift_wingCode_ne_le_of_blocks {N : ℕ} {Ω₁ : Type u_2} {Ω₂ : Type u_3} (c : ContextField N) {m : ℕ} (g : Fin N → Fin m) (hg : Monotone g) (v : Fin m → Ω₁ × Ω₂) {ω T : ℝ} (hω : 0 ≤ ω) (hωT : ω * T ≤ 1) (p : LF4.CPN N) : (epistemicMeasure p) {x : LF4.KSigma N | ∃ t ∈ Set.Icc 0 T, wingCode c (v ∘ g) (sigmaShift (ω * t) x) ≠ wingCode c (v ∘ g) x} ≤ ↑m * ENNReal.ofReal (ω * T)

★★★ Persistence of the two-wing record over a horizon, in proportion to the outcome count.