Documentation

CsdLean4.SigmaLayer.UniqueErgodicity

SigmaLayer/UniqueErgodicity: the ergodic face of SO-1/L7, sharpened #

Category: 7-SigmaLayer (the projective-sector layer (Paper C)).

This module defines unique ergodicity (absent from Mathlib) and connects it to the SigmaLayer target scaffold IsErgodicForOutcomeRegions / BornFromFlow (SigmaLayer/TheoremTargets.lean), precisely locating the ergodic face of the SO-1/L7 frontier.

What this establishes (and, honestly, what it does NOT) #

What is NOT proved here — and why. The target BornFromFlow (TheoremTargets.lean) is the pointwise (a.e.) statement (1/n) ∑_{k<n} 𝟙_region(Φ_k x) → μL(region). Deriving it from IsErgodicForOutcomeRegions requires the pointwise (Birkhoff) ergodic theorem, which Mathlib does not have (it has only the von Neumann mean ergodic theorem, ContinuousLinearMap.tendsto_birkhoffAverage_orthogonalProjection, and the Birkhoff-sum definitions). So this module supplies the ergodicity side of the reduction and names the remaining gap; it does not close BornFromFlow.

Two proved facts bound what this route can ever buy — this is boundary-marking, not a route CSD takes:

  1. A single projective unitary flow is provably NOT ergodic, and NOT uniquely ergodic, w.r.t. μ_FS: it conserves the Born coordinates and fixes eigen-rays, giving distinct invariant measures (SigmaLayer/SectorPostulateNoGo.lean flow_admits_invariant_ne_fubiniStudy; LF4/TypicalityForcing.lean obsFlow_not_ergodic, obsFlow_not_uniquely_ergodic). So UniquelyErgodic is provably FALSE for the Schrödinger-type flows the sector currently carries — a candidate flow satisfying it must be non-unitary (de-isolation / fibre-mixing).
  2. CSD's typicality is forced by the law of large numbers over fresh i.i.d. preparations, NOT by single-trajectory time averages (specs/active-todo.md, framing correction 2026-06-29, Papers A & B). The ergodic / single-trajectory account is the optional stronger reading, not the mechanism. So even a full pointwise Birkhoff theorem would sharpen SO-1's bracketing, not close the SO-1 residue (which is the sector/symmetry ORIGIN, G-from-D1).

References: SigmaLayer/TheoremTargets.lean (BornFromFlow, IsErgodicForOutcomeRegions), SigmaLayer/SectorPostulateNoGo.lean, LF4/TypicalityForcing.lean, LF4/KahlerVolumeForced.lean (IsForcedKahlerVolume — the positive companion: μ_FS forced by the full U(N) symmetry), specs/connectivity-manifest.md (L7/SO-1), specs/reconstruction-status.md (T3 frontier).

source
def CSD.SigmaLayer.UniquelyErgodic {α : Type u_1} [MeasurableSpace α] (f : α → α) (μ : MeasureTheory.Measure α) :
Prop

Unique ergodicity. μ is the UNIQUE f-invariant probability measure: f preserves μ, μ is a probability measure, and any f-invariant probability measure equals μ. This is the standard definition (absent from Mathlib); the classic inhabitant is an irrational rotation.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem CSD.SigmaLayer.UniquelyErgodic.ergodic {α : Type u_1} [MeasurableSpace α] {f : α → α} {μ : MeasureTheory.Measure α} (h : UniquelyErgodic f μ) :
    Ergodic f μ

    Unique ergodicity implies ergodicity. If μ is the only f-invariant probability measure, the invariant-probability-measure set is the singleton {μ}, so μ is trivially an extreme point of it, hence ergodic (Ergodic.of_mem_extremePoints).

    source
    theorem CSD.SigmaLayer.isErgodicForOutcomeRegions_of_ergodic {Sigma : Type u_2} [MeasurableSpace Sigma] (D : ConstraintDynamics Sigma) (h : Ergodic (D.flow 1) ↑D.muL) :
    IsErgodicForOutcomeRegions D

    Ergodicity of the time-1 flow map discharges the scaffold. IsErgodicForOutcomeRegions D (every time-1-invariant measurable set is μL-null or co-null) is exactly Mathlib's PreErgodic.measure_self_or_compl_eq_zero for Φ_1 on μL.

    source
    theorem CSD.SigmaLayer.isErgodicForOutcomeRegions_of_uniquelyErgodic {Sigma : Type u_2} [MeasurableSpace Sigma] (D : ConstraintDynamics Sigma) (h : UniquelyErgodic (D.flow 1) ↑D.muL) :
    IsErgodicForOutcomeRegions D

    Unique ergodicity of the time-1 flow map discharges the scaffold (a fortiori, via UniquelyErgodic.ergodic). This is the exact hypothesis under which BornFromFlow would follow from the (Mathlib-absent) pointwise Birkhoff theorem — and which the unitary no-gos provably exclude for the current flows.