Dynamical stability of record macrostates

Category: 7-SigmaLayer (the record layer — Paper C A7). BACKLOG #103, the physics half of #38's candidate (5).

RecordMacrostate.lean (#102) built the macroscopic coordinate: the record string of a finite indexed family of contexts, with no-signalling and the Born chain law both verified for it. What makes a coordinate macroscopic is not its construction but its stability, and #103 opened with the warning that stability here cannot mean invariance — finite unitary dynamics on Σ's base is almost periodic and supplies no mixing (not_hasCorrelationDecay_blockPop_of_unitary). The brick chosen is therefore the measure-theoretic one, in two halves that pull in opposite directions and are both proved:

• the macroscopic law is exactly invariant. ★★★ map_recordString_sigmaShift: a record write translates the record coordinate of the fibre, so it preserves the epistemic measure (★ measurePreserving_sigmaShift), and therefore the distribution of the record string is unchanged — for every write size, with no error term;
• the pointwise assignment is robust to first order in the write. ★★★ measure_recordString_ne_le: the set of microstates whose record string a write of size δ changes has epistemic measure at most k · N · δ for a family of k contexts over N outcomes. So the records do move — but only on a set that shrinks linearly with the write (★ tendsto_measure_recordString_ne), which is the honest sense in which the cells are stable.

The mechanism is arithmetic on the fibre, and the whole file rests on one lemma:

• ★ rep_add_coe (in CircleFibre.lean) — a translation that does not wrap adds to the canonical representative. A write therefore pushes a microstate towards the upper endpoint of its own arc, and the only microstates it can relabel are the ones within δ of that endpoint;
• robustBasin, edgeBand — the δ-interior of a basin and the last δ of its arc, with ★ globalBasin_subset_robustBasin_union_edgeBand splitting every basin into the two;
• ★★ sigmaShift_mem_globalBasin — the margin lemma: a write of size δ cannot move a microstate out of a basin it is δ-robustly inside — and hence ★★ outcomeCode_sigmaShift, ★★★ recordString_sigmaShift, ★★ recordMacro_sigmaShift at the macrostate level;
• measure_edgeBand_le — the band's measure is at most δ, by volume_rep_preimage_Ioc;
• ★★ measure_robustBasin_ge — robustness is controlled by the Born weight: rate p i − δ ≤ μ(δ-interior of the basin of i). A record whose Born weight is large is robust to writes far larger than a record whose weight is small, and a cell of weight below δ is given no robustness at all. That is the sense in which macroscopic records are the stable ones;
• ★★ measure_robustBasin_ge_one_sub — the majority half, conditional on concentration: once the context's weights concentrate (1 − ε ≤ rate p i) the shared-and-robust cell carries all but ε + δ. By globalBasin_prob a cell's measure is exactly its Born weight, so no cell is overwhelming unless the weights are — "overwhelmingly many microstates share the record" is a property of the preparation and the context, not of the coordinate, and that is the honest reading of #103's second half;
• ★★★ measure_exists_recordString_ne_le and ★★★ measure_drift_recordString_ne_le — the bound is uniform over a whole horizon: the exceptional set is the same one for every write in [0, δ], so for a drift of the record coordinate at rate ω the record string survives the entire interval [0, T] outside a set of measure k · N · ω · T. This is "persistence over a horizon" in the words of #103, obtained without a second argument.

Honest scope

⚠️ This is not invariance and contains no mixing claim. No cell is shown to be an invariant set, no flow is shown to mix, and nothing here contradicts not_hasCorrelationDecay_blockPop_of_unitary: the exact statement is invariance of the law plus an O(δ) bound on the microstates that get relabelled. The two are compatible precisely because the law is a pushforward and the relabelling is a pointwise fact.

⚠️ Only the record coordinate moves. sigmaShift fixes the base and the symplectic partner of the fibre. A flow that moves the base changes the arcs themselves, and a ContextField is only assumed measurable, so its arcs may move discontinuously with the base: that case is not covered here. It is BACKLOG #104, landed the same day as BaseMotionStability.lean, which carries the margin argument over with a hypothesis bounding the arcs' displacement — no metric on the base required.

⚠️ The write below is a constant translation, so nothing in this file is stated for the base-dependent write of CV/RecordInfluence.lean's recordStroke. That is a limit of this file and not an obstruction: MeasurableSingletonClass (LF4.CPN N) is available at the pin, so the epistemic measure is concentrated on the fibre over its preparation and a base-dependent write agrees with a constant one almost everywhere. BaseMotionStability.lean (#104) proves exactly that (ae_fst_eq, map_sigmaMove_id) and covers the base-dependent case.

⚠️ The majority half is conditional, and its hypothesis is not supplied. measure_robustBasin_ge_one_sub assumes the concentration 1 − ε ≤ rate p i; nothing here derives it, and by globalBasin_prob it cannot be derived from the coordinate, since a cell's measure is its Born weight. Where such a rate field comes from — pointer states, decoherence, or the dynamics — is BACKLOG #105. ⚠️ It is not the same thing as fs_chebyshev_concentration (Thermo/CanonicalTypicality.lean, a polynomial rate) or the conditional time-averaged equilibration of Thermo/Equilibration.lean: those are statements about base statistics, they live at a different place in Σ, and no theorem below joins them to the fibre bound proved here.

⚠️ The bound degrades with the family and the alphabet and is not claimed uniform in k or N: it is k · N · δ, each factor from a union bound (one band per outcome, one context per index), and no better constant is claimed. In particular records of small Born weight are genuinely fragile — measure_robustBasin_ge is vacuous once δ exceeds the weight — and that is a feature of the construction, not a gap in the proof.

⚠️ No dynamics of Σ is derived. Translation of the record coordinate is the dynamics the record medium has in this corpus (measurePreserving_fibreShift), not a flow derived from an interaction Hamiltonian; nothing here claims it is the physical evolution.

References: records-to-spacetime-scoping.md ST-3; future-work.md; RecordMacrostate.lean (#102), MacroProjection.lean (#99), CircleFibre.lean, GlobalBasin.lean, CV/RecordInfluence.lean (fibreShift); specs/BACKLOG.md #103, #104, #105, #38, #100.

A record write as a translation of the record coordinate

def CSD.RecordLayer.sigmaShift {N : ℕ} (δ : ℝ) (x : LF4.KSigma N) : LF4.KSigma N

A record write of size δ: translation of the record coordinate of Σ's fibre, leaving the base and the symplectic partner untouched. This is the dynamics the record medium has — the recordStroke of CV/RecordInfluence.lean acts on the fibre exactly this way.

Equations

• CSD.RecordLayer.sigmaShift δ x = (x.1, x.2.1 + ↑δ, x.2.2)

@[simp]

theorem CSD.RecordLayer.sigmaShift_fst {N : ℕ} (δ : ℝ) (x : LF4.KSigma N) : (sigmaShift δ x).1 = x.1

@[simp]

theorem CSD.RecordLayer.sigmaShift_record {N : ℕ} (δ : ℝ) (x : LF4.KSigma N) : (sigmaShift δ x).2.1 = x.2.1 + ↑δ

@[simp]

theorem CSD.RecordLayer.sigmaShift_partner {N : ℕ} (δ : ℝ) (x : LF4.KSigma N) : (sigmaShift δ x).2.2 = x.2.2

@[simp]

theorem CSD.RecordLayer.sigmaShift_zero {N : ℕ} : sigmaShift 0 = id

theorem CSD.RecordLayer.sigmaShift_sigmaShift {N : ℕ} (δ₁ δ₂ : ℝ) (x : LF4.KSigma N) : sigmaShift δ₁ (sigmaShift δ₂ x) = sigmaShift (δ₂ + δ₁) x

Writes compose by adding their sizes: the family sigmaShift is a one-parameter group.

theorem CSD.RecordLayer.measurable_sigmaShift {N : ℕ} (δ : ℝ) : Measurable (sigmaShift δ)

theorem CSD.RecordLayer.measurePreserving_torusShift (δ : ℝ) : MeasureTheory.MeasurePreserving (Prod.map (fun (θ : AddCircle 1) => θ + ↑δ) id) MeasureTheory.volume MeasureTheory.volume

★ A record write preserves the epistemic measure. The base is a point and the record coordinate carries Haar measure, which translation preserves. This is what makes the macroscopic law exactly invariant (map_recordString_sigmaShift) however large the write.

theorem CSD.RecordLayer.measurePreserving_sigmaShift {N : ℕ} (δ : ℝ) (p : LF4.CPN N) : MeasureTheory.MeasurePreserving (sigmaShift δ) (epistemicMeasure p) (epistemicMeasure p)

The arc a context assigns, its robust interior and its boundary band

noncomputable def CSD.RecordLayer.cellTop {N : ℕ} (c : ContextField N) (i : Fin N) (x : LF4.KSigma N) : ℝ

The upper endpoint of the arc a context assigns to outcome i, read at a microstate's own base point. A write pushes the record coordinate towards it, so it is the only endpoint the stability bounds have to watch.

Equations

• CSD.RecordLayer.cellTop c i x = CSD.RecordLayer.loSum (c.rate x.1) i + c.rate x.1 i

@[simp]

theorem CSD.RecordLayer.cellTop_sigmaShift {N : ℕ} (c : ContextField N) (δ : ℝ) (i : Fin N) (x : LF4.KSigma N) : cellTop c i (sigmaShift δ x) = cellTop c i x

theorem CSD.RecordLayer.cellTop_le_one {N : ℕ} (c : ContextField N) (i : Fin N) (x : LF4.KSigma N) : cellTop c i x ≤ 1

theorem CSD.RecordLayer.measurable_cellTop {N : ℕ} (c : ContextField N) (i : Fin N) : Measurable (cellTop c i)

theorem CSD.RecordLayer.measurable_repRecord {N : ℕ} : Measurable fun (x : LF4.KSigma N) => rep x.2.1

theorem CSD.RecordLayer.mem_globalBasin_iff {N : ℕ} (c : ContextField N) (i : Fin N) (x : LF4.KSigma N) : x ∈ globalBasin c i ↔ loSum (c.rate x.1) i < rep x.2.1 ∧ rep x.2.1 ≤ cellTop c i x

The basin, written out as two inequalities on the record coordinate — the form every margin argument below consumes.

noncomputable def CSD.RecordLayer.robustBasin {N : ℕ} (c : ContextField N) (δ : ℝ) (i : Fin N) : Set (LF4.KSigma N)

The δ-robust interior of a basin: the microstates of the basin whose record coordinate is at distance at least δ from the arc's upper endpoint, the endpoint a write pushes towards.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CSD.RecordLayer.edgeBand {N : ℕ} (c : ContextField N) (δ : ℝ) (i : Fin N) : Set (LF4.KSigma N)

The δ-boundary band of a basin: the last δ of its arc, the only part of the basin a write of size δ can push out.

Equations

• CSD.RecordLayer.edgeBand c δ i = {x : CSD.LF4.KSigma N | CSD.RecordLayer.cellTop c i x - δ < CSD.RecordLayer.rep x.2.1 ∧ CSD.RecordLayer.rep x.2.1 ≤ CSD.RecordLayer.cellTop c i x}

theorem CSD.RecordLayer.measurableSet_robustBasin {N : ℕ} (c : ContextField N) (δ : ℝ) (i : Fin N) : MeasurableSet (robustBasin c δ i)

theorem CSD.RecordLayer.measurableSet_edgeBand {N : ℕ} (c : ContextField N) (δ : ℝ) (i : Fin N) : MeasurableSet (edgeBand c δ i)

theorem CSD.RecordLayer.robustBasin_subset_globalBasin {N : ℕ} (c : ContextField N) {δ : ℝ} (hδ : 0 ≤ δ) (i : Fin N) : robustBasin c δ i ⊆ globalBasin c i

theorem CSD.RecordLayer.robustBasin_mono {N : ℕ} (c : ContextField N) {δ δ' : ℝ} (h : δ' ≤ δ) (i : Fin N) : robustBasin c δ i ⊆ robustBasin c δ' i

theorem CSD.RecordLayer.globalBasin_subset_robustBasin_union_edgeBand {N : ℕ} (c : ContextField N) (δ : ℝ) (i : Fin N) : globalBasin c i ⊆ robustBasin c δ i ∪ edgeBand c δ i

★ Every basin splits into its robust interior and its boundary band. The dichotomy the measure bounds run on: a microstate of the basin either has margin δ to the upper endpoint, or lies in the last δ of the arc.

The margin lemma

theorem CSD.RecordLayer.sigmaShift_mem_globalBasin {N : ℕ} (c : ContextField N) {δ : ℝ} (hδ : 0 ≤ δ) (i : Fin N) {x : LF4.KSigma N} (hx : x ∈ robustBasin c δ i) : sigmaShift δ x ∈ globalBasin c i

★★ The margin lemma. A record write of size δ cannot move a microstate out of a basin it is δ-robustly inside: the write adds δ to the record coordinate's representative (rep_add_coe, available because the shifted representative is still inside one turn), and the margin is exactly what keeps the sum below the arc's upper endpoint.

theorem CSD.RecordLayer.outcomeCode_sigmaShift {N : ℕ} (c : ContextField N) {δ : ℝ} (hδ : 0 ≤ δ) {i : Fin N} {x : LF4.KSigma N} (hx : x ∈ robustBasin c δ i) : outcomeCode c (sigmaShift δ x) = outcomeCode c x

★★ A record write does not change the outcome a context assigns to a microstate robustly inside one of its basins.

theorem CSD.RecordLayer.recordString_sigmaShift {N k : ℕ} (c : Fin k → ContextField N) {δ : ℝ} (hδ : 0 ≤ δ) {x : LF4.KSigma N} (hx : ∀ (j : Fin k), ∃ (i : Fin N), x ∈ robustBasin (c j) δ i) : recordString c (sigmaShift δ x) = recordString c x

★★★ A record write leaves the whole record string intact on a microstate that is robustly inside a basin of every context of the family. The macrostate of #102 is unchanged — not because the cell is invariant, but because the microstate had margin.

theorem CSD.RecordLayer.recordString_sigmaShift_of_le {N k : ℕ} (c : Fin k → ContextField N) {δ s : ℝ} (hs0 : 0 ≤ s) (hs : s ≤ δ) {x : LF4.KSigma N} (hx : ∀ (j : Fin k), ∃ (i : Fin N), x ∈ robustBasin (c j) δ i) : recordString c (sigmaShift s x) = recordString c x

The margin bought at size δ covers every smaller write, since the robust interior only grows as the margin demanded shrinks. This is why one exceptional set serves a whole horizon.

theorem CSD.RecordLayer.recordMacro_sigmaShift {N k : ℕ} (c : Fin k → ContextField N) {δ : ℝ} (hδ : 0 ≤ δ) {x : LF4.KSigma N} (hx : ∀ (j : Fin k), ∃ (i : Fin N), x ∈ robustBasin (c j) δ i) : (recordMacro c).toFun (sigmaShift δ x) = (recordMacro c).toFun x

★★ The macrostate of #102 itself is preserved, stated on recordMacro so that it is literally the macroscopic coordinate of candidate (5) that the write leaves alone.

The measure of the boundary band

theorem CSD.RecordLayer.volume_rep_preimage_Ioc_le (a b : ℝ) : MeasureTheory.volume (rep ⁻¹' Set.Ioc a b) ≤ ENNReal.ofReal (b - a)

★ Any rep-preimage of an interval has measure at most the interval's length, with no containment hypothesis at all: the representative's range (0, 1] clips the overhang at both ends. The boundary bands of the stability bounds are intervals that need not sit inside one turn, so this is the form they consume.

theorem CSD.RecordLayer.measure_edgeBand_le {N : ℕ} (c : ContextField N) (δ : ℝ) (i : Fin N) (p : LF4.CPN N) : (epistemicMeasure p) (edgeBand c δ i) ≤ ENNReal.ofReal δ

The boundary band is small. Its slice over the preparation is the last δ of one arc, so its epistemic measure is at most δ — the single quantitative input to every bound below.

theorem CSD.RecordLayer.measure_robustBasin_ge {N : ℕ} (c : ContextField N) {δ : ℝ} (hδ : 0 ≤ δ) (i : Fin N) (p : LF4.CPN N) : ENNReal.ofReal (c.rate p i - δ) ≤ (epistemicMeasure p) (robustBasin c δ i)

★★ Robustness is controlled by the Born weight. The δ-robust interior of the basin of i has epistemic measure at least rate p i − δ. A record of large Born weight survives writes far larger than one of small weight, and a cell of weight below δ is granted no robustness at all: the macroscopic records — the heavy ones — are the stable ones, quantitatively.

theorem CSD.RecordLayer.measure_robustBasin_ge_one_sub {N : ℕ} (c : ContextField N) {δ ε : ℝ} (hδ : 0 ≤ δ) (i : Fin N) (p : LF4.CPN N) (hconc : 1 - ε ≤ c.rate p i) : ENNReal.ofReal (1 - ε - δ) ≤ (epistemicMeasure p) (robustBasin c δ i)

★★ The overwhelming-majority half, conditional on concentration. If a context's weights concentrate at the preparation — 1 − ε ≤ rate p i, which is what a pointer-like apparatus is supposed to produce — then the microstates that share outcome i and are robust to writes of size δ carry all but ε + δ of the epistemic measure. This is "overwhelmingly many microstates share the record" with the concentration as an explicit hypothesis: by globalBasin_prob the cell of outcome i has measure exactly rate p i, so no cell is overwhelming unless the Born weights are — a property of the preparation and the context, never of the coordinate. Supplying that hypothesis from the dynamics is BACKLOG #105; fs_chebyshev_concentration is a statement about base statistics and is not it.

The microstates a write can relabel

noncomputable def CSD.RecordLayer.unstableSet {N : ℕ} (c : ContextField N) (δ : ℝ) : Set (LF4.KSigma N)

The microstates a write of size δ can relabel, for one context: those outside every basin (a null set) and those in some basin's boundary band.

Equations

• CSD.RecordLayer.unstableSet c δ = (⋃ (i : Fin N), CSD.RecordLayer.globalBasin c i)ᶜ ∪ ⋃ (i : Fin N), CSD.RecordLayer.edgeBand c δ i

theorem CSD.RecordLayer.exists_robustBasin_of_notMem_unstableSet {N : ℕ} (c : ContextField N) (δ : ℝ) {x : LF4.KSigma N} (hx : x ∉ unstableSet c δ) : ∃ (i : Fin N), x ∈ robustBasin c δ i

Outside the unstable set a microstate has margin δ in some basin — the converse direction the measure bounds need.

theorem CSD.RecordLayer.measure_unstableSet_le {N : ℕ} (c : ContextField N) (δ : ℝ) (p : LF4.CPN N) : (epistemicMeasure p) (unstableSet c δ) ≤ ↑N * ENNReal.ofReal δ

The unstable set of one context has measure at most N · δ: one band per outcome, plus the null set where no basin contains the microstate (globalBasin_ae_total).

Quantitative stability of the record macrostate

theorem CSD.RecordLayer.measure_recordString_ne_le {N k : ℕ} (c : Fin k → ContextField N) {δ : ℝ} (hδ : 0 ≤ δ) (p : LF4.CPN N) : (epistemicMeasure p) {x : LF4.KSigma N | recordString c (sigmaShift δ x) ≠ recordString c x} ≤ ↑k * (↑N * ENNReal.ofReal δ)

★★★ Quantitative stability of record macrostates. The microstates whose record string a write of size δ changes have epistemic measure at most k · N · δ, for a family of k contexts over N outcomes. This is the measure-theoretic statement #103 asked for: the cells are not invariant, but the set of microstates that cross a cell boundary shrinks linearly with the write.

theorem CSD.RecordLayer.measure_exists_recordString_ne_le {N k : ℕ} (c : Fin k → ContextField N) (δ : ℝ) (p : LF4.CPN N) : (epistemicMeasure p) {x : LF4.KSigma N | ∃ s ∈ Set.Icc 0 δ, recordString c (sigmaShift s x) ≠ recordString c x} ≤ ↑k * (↑N * ENNReal.ofReal δ)

★★★ One exceptional set serves the whole horizon. The microstates whose record string is changed by some write of size at most δ have the same bound: the margin bought at δ covers every smaller write, so no second argument and no union over times is needed.

theorem CSD.RecordLayer.measure_drift_recordString_ne_le {N k : ℕ} (c : Fin k → ContextField N) {ω : ℝ} (hω : 0 ≤ ω) (T : ℝ) (p : LF4.CPN N) : (epistemicMeasure p) {x : LF4.KSigma N | ∃ t ∈ Set.Icc 0 T, recordString c (sigmaShift (ω * t) x) ≠ recordString c x} ≤ ↑k * (↑N * ENNReal.ofReal (ω * T))

★★★ Persistence over a horizon. Under a drift of the record coordinate at rate ω, the record string of the family survives the entire interval [0, T] outside a set of epistemic measure at most k · N · ω · T. This is #103's "persistence over a horizon", with the horizon appearing only through the total drift.

theorem CSD.RecordLayer.tendsto_measure_recordString_ne {N k : ℕ} (c : Fin k → ContextField N) (p : LF4.CPN N) : Filter.Tendsto (fun (δ : ℝ) => (epistemicMeasure p) {x : LF4.KSigma N | recordString c (sigmaShift δ x) ≠ recordString c x}) (nhdsWithin 0 (Set.Ici 0)) (nhds 0)

★ The relabelled set vanishes as the write shrinks. The qualitative form of the bound: in the limit of small writes the record macrostate is stable almost everywhere.

Exact invariance of the macroscopic law

theorem CSD.RecordLayer.map_recordString_sigmaShift {N k : ℕ} (c : Fin k → ContextField N) (δ : ℝ) (p : LF4.CPN N) : MeasureTheory.Measure.map (fun (x : LF4.KSigma N) => recordString c (sigmaShift δ x)) (epistemicMeasure p) = MeasureTheory.Measure.map (recordString c) (epistemicMeasure p)

★★★ The macroscopic law is exactly invariant under a record write. The write preserves the epistemic measure, so the distribution of the record string is unchanged — for every write size, with no error term and no margin hypothesis. Together with measure_recordString_ne_le this is the honest content of "the record macrostates are stable": the macroscopic statistics do not move at all, while the macrostate of an individual microstate moves only on a set of measure O(δ).