Documentation

Oseledets.Krieger.Bracket

The aligned-marker construction of a BracketedTowerSystem (C3, sub-problem B, closure) #

Oseledets.Krieger.Weave reduced sub-problem B of the unconditional Krieger theorem to producing a single BracketedTowerSystem e μ Q k: one fixed measurable master code : α → Fin k, self-bracketed on a refining sequence of Rokhlin towers with summable misses. The three genuinely hard fields are the self-bracketing conditions on the single code, simultaneously across the nested stages:

The crux (Keane–Serafin's nested alignment): a single point can be an interior floor of one stage and a marker (top / predecessor) of another, and then interior and top/pred would demand both code ≠ s and code = s at that point — a contradiction. The nesting eliminates this by aligning the markers: there is a single marker set M ⊆ α such that, for every stage m, the column tops and base-predecessors of stage m all lie in M, while every interior floor of every stage lies outside M. With such a coherent M the conflict is structurally excluded, and the master code is the piecewise map

code x = if x ∈ M then s else embLetter emb (dataLetter x) ,

placing the sentinel exactly on the marker set and a data letter off it.

What is built here, sorry-free #

This file isolates that coherent marker set as a clean hypothesis bundle — the aligned-tower castle AlignedTowerCastle — and discharges, unconditionally and sorry-free, the entire symbolic/measurable machinery that turns it into a BracketedTowerSystem (hence CodesTwoSidedMod0c):

The honest residual (the adversarial verdict) #

The reduction proved here is the structural exit: a coherent aligned marker set ⟹ a self- bracketed master code ⟹ BracketedTowerSystem ⟹ CodesTwoSidedMod0c. What AlignedTowerCastle carries as the field marker_top ∧ marker_pred ∧ interior_notMarker is exactly the genuinely-dynamical content the construction must deliver and which the repository's Oseledets.Krieger.rokhlin_tower API does not supply: a single measurable set M that is the top/predecessor marker for every refining stage while avoiding every stage's interior — i.e. the Kakutani–Rokhlin castle in which each column of tower m+1 is a concatenation of whole tower-m columns plus a marked remainder, so that the tower tops nest (N_{m+1} a multiple-plus of N_m).

rokhlin_tower produces, for each height N, an independent complete-block tower towerBase e A N over a fresh small base A; its column tops sit at arbitrary positions inside the orbit and are not aligned across distinct heights N. Consequently the marker set "column tops of tower m" is, in general, an interior floor of tower m', exactly the conflict the alignment is meant to exclude. Building M therefore needs a genuine nested castle refinement (stack whole tower-m columns to form tower m+1), for which Mathlib has no analogue and the repository has no lemma (verified: no nest/castle/stack/aligned-tower construction exists in Oseledets/Krieger/). This is the precise, non-fakeable dynamical residual of sub-problem B; AlignedTowerCastle is the faithful hypothesis boundary, sharper than BracketedTowerSystem in that the single carried datum is the coherent geometric marker set M, with all symbolic coding discharged here.

References #

The piecewise master code on a marker set #

Given a measurable marker set M ⊆ α (the coherent column-top / predecessor set of the nested castle), a sentinel s : Fin k, a data embedding emb, and a measurable data-letter map dataLetter : α → Fin (k - 1), the master code places the sentinel s exactly on M and the embedded data letter off M. The two reads markerCode_mem / markerCode_notMem are the only facts the self-bracketing proofs consume.

source
noncomputable def Oseledets.Krieger.markerCode {α : Type u_1} {k : ℕ} {s : Fin k} (M : Set α) (emb : Fin (k - 1) ↪ NonSentinel s) (dataLetter : α → Fin (k - 1)) (x : α) :
Fin k

The piecewise master code. On the marker set M it is the reserved sentinel s; off M it is the embedded data letter embLetter emb (dataLetter x) (a non-sentinel letter, in the range of embLetter emb). This is the code = s ⇔ marker placement that makes the column tops and base predecessors carry s while interior floors carry data.

Decidability of membership in M is supplied classically (Classical.propDecidable) so the code needs no DecidablePred instance to be carried alongside M; the piecewise value is independent of the decidability instance, so this is harmless. The classical instance is supplied by open Classical in on this definition.

Equations
Instances For
    source
    theorem Oseledets.Krieger.markerCode_mem {α : Type u_1} {k : ℕ} {s : Fin k} {M : Set α} {emb : Fin (k - 1) ↪ NonSentinel s} {dataLetter : α → Fin (k - 1)} {x : α} (hx : x ∈ M) :
    markerCode M emb dataLetter x = s

    On the marker set the master code is the sentinel s.

    source
    theorem Oseledets.Krieger.markerCode_notMem {α : Type u_1} {k : ℕ} {s : Fin k} {M : Set α} {emb : Fin (k - 1) ↪ NonSentinel s} {dataLetter : α → Fin (k - 1)} {x : α} (hx : x ∉ M) :
    markerCode M emb dataLetter x = embLetter emb (dataLetter x)

    Off the marker set the master code is the embedded data letter, hence in the range of embLetter emb (a non-sentinel letter).

    source
    theorem Oseledets.Krieger.markerCode_mem_range_of_notMem {α : Type u_1} {k : ℕ} {s : Fin k} {M : Set α} {emb : Fin (k - 1) ↪ NonSentinel s} {dataLetter : α → Fin (k - 1)} {x : α} (hx : x ∉ M) :
    markerCode M emb dataLetter x ∈ Set.range (embLetter emb)

    Off the marker set the master code lies in the range of embLetter emb.

    source
    theorem Oseledets.Krieger.measurable_markerCode {α : Type u_1} {k : ℕ} [mα : MeasurableSpace α] {s : Fin k} {M : Set α} (hM : MeasurableSet M) (emb : Fin (k - 1) ↪ NonSentinel s) {dataLetter : α → Fin (k - 1)} (hdata : Measurable dataLetter) :
    Measurable (markerCode M emb dataLetter)

    The piecewise master code is measurable. It is Measurable.piecewise over the measurable marker set M, gluing the constant s (on M) with the measurable embLetter emb ∘ dataLetter (off M).

    The aligned-tower castle #

    The genuinely-dynamical output of the Keane–Serafin nested construction, isolated as a hypothesis bundle that is sharper than BracketedTowerSystem: a refining sequence of Rokhlin towers (A m, N m, T m) together with one measurable marker set M whose alignment facts force every column top and every column-base predecessor of every stage into M, and every interior floor of every stage out of M. From these three alignment facts the self-bracketing of the piecewise master code markerCode M emb dataLetter is purely definitional (markerCode_mem / markerCode_notMem). The remaining fields (decodes, cell-index recovery, summable misses) are carried verbatim.

    source
    structure Oseledets.Krieger.AlignedTowerCastle {α : Type u_1} {κ : Type u_2} [mα : MeasurableSpace α] (e : α ≃ᵐ α) (μ : MeasureTheory.Measure α) (Q : κ → Set α) (k : ℕ) [Nonempty (Fin (k - 1))] :
    Type (max u_1 u_2)

    The aligned-tower castle (the Keane–Serafin nested-construction output, marker-set form). The single carried geometric datum is the coherent measurable marker set M; everything else is bookkeeping shared with BracketedTowerSystem.

    • s : Fin k

      The shared reserved sentinel.

    • emb : Fin (k - 1) ↪ NonSentinel self.s

      The shared data embedding (fixed across stages).

    • dataLetter : α → Fin (k - 1)

      The measurable data-letter map (read off Q along the column).

    • dataLetter_measurable : Measurable self.dataLetter

      The data-letter map is measurable.

    • M : Set α

      The coherent marker set — the aligned column-top / predecessor set of the nested castle. This is the single genuinely-dynamical datum the construction must deliver.

    • M_measurable : MeasurableSet self.M

      The marker set is measurable.

    • decode : List (Fin k) → ℕ → κ

      The shared position-aware decoder.

    • cellIndex : α → κ

      The shared measurable cell index.

    • cellIndex_recovers (j : κ) : Q j =ᵐ[μ] {x : α | self.cellIndex x = j}

      The cell index recovers each cell of Q mod 0.

    • A : ℕ → Set α

      The per-stage tower base sets.

    • A_measurable (m : ℕ) : MeasurableSet (self.A m)

      Each base is measurable.

    • N : ℕ → ℕ

      The per-stage tower heights.

    • hN (m : ℕ) : 1 ≤ self.N m

      Each tower height is positive.

    • T : ℕ → Set α

      The stage events T m.

    • cover (m : ℕ) : self.T m ⊆ coveredSet e (self.A m) (self.N m)

      Each stage event lies in its tower's covered set.

    • interior_notMarker (m : ℕ) (x : α) : x ∈ self.T m → ∀ i < self.N m - 1, (⇑e)^[i] (columnBase e (self.A m) (self.N m) x) ∉ self.M

      Alignment, interior. On T m, every interior column floor lies outside the marker set (so the master code reads a data letter there).

    • marker_top (m : ℕ) (x : α) : x ∈ self.T m → (⇑e)^[self.N m - 1] (columnBase e (self.A m) (self.N m) x) ∈ self.M

      Alignment, top. On T m, every column top lies in the marker set.

    • marker_pred (m : ℕ) (x : α) : x ∈ self.T m → e.symm (columnBase e (self.A m) (self.N m) x) ∈ self.M

      Alignment, predecessor. On T m, every column-base predecessor lies in the marker set.

    • decodes (m : ℕ) (x : α) : x ∈ self.T m → self.decode (sentinelEncode self.s self.emb (weaveName e (self.A m) (self.N m) self.s self.emb (markerCode self.M self.emb self.dataLetter) (columnBase e (self.A m) (self.N m) x))) (floorAddr e (self.A m) (self.N m) x) = self.cellIndex x

      Decoding stage m's read-off block at the floor offset recovers the cell index.

    • misses_summable : ∑' (m : ℕ), μ (self.T m)ᶜ ≠ ⊤

      The stage misses are summable.

    Instances For
      source
      noncomputable def Oseledets.Krieger.AlignedTowerCastle.toBracketedTowerSystem {α : Type u_1} {κ : Type u_2} {k : ℕ} [mα : MeasurableSpace α] {μ : MeasureTheory.Measure α} [Nonempty (Fin (k - 1))] {e : α ≃ᵐ α} {Q : κ → Set α} (C : AlignedTowerCastle e μ Q k) :
      BracketedTowerSystem e μ Q k

      The BracketedTowerSystem from an AlignedTowerCastle. The master code is the piecewise markerCode M emb dataLetter; measurability is measurable_markerCode. The three self-bracketing fields are discharged from the alignment facts via the piecewise reads:

      decodes, cell-index recovery and summable misses carry over verbatim. This is the cross-stage interleaving made definitional through one coherent marker set.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        theorem Oseledets.Krieger.AlignedTowerCastle.codes {α : Type u_1} {κ : Type u_2} {k : ℕ} [mα : MeasurableSpace α] {μ : MeasureTheory.Measure α} [Nonempty (Fin (k - 1))] [Countable κ] [MeasurableSpace κ] [MeasurableSingletonClass κ] {e : α ≃ᵐ α} {Q : κ → Set α} (C : AlignedTowerCastle e μ Q k) :
        CodesTwoSidedMod0c e Q (codePartition (RefiningTowerCode.ofStages C.toBracketedTowerSystem.toStageInput.s C.toBracketedTowerSystem.toStageInput.code ⋯ C.toBracketedTowerSystem.toStageInput.decode C.toBracketedTowerSystem.toStageInput.cellIndex ⋯ C.toBracketedTowerSystem.toStageInput.T ⋯ fun (m : ℕ) => StageInput.toStageCode e C.toBracketedTowerSystem.toStageInput m).toColumnLayoutData.code ⋯)

        Sub-problem B closed from an aligned-tower castle. An AlignedTowerCastle — a refining sequence of Rokhlin towers with one coherent measurable marker set aligning every column top and base-predecessor across stages while avoiding every interior floor, with summable misses — yields, via BracketedTowerSystem.codes, the cross-layer countable mod-0 code CodesTwoSidedMod0c e Q (…), the deliverable that slots into Oseledets.Krieger.KriegerCodingData.code_codes. The entire residual is now the existence of the aligned marker set M, i.e. the Kakutani–Rokhlin nested castle.