Documentation

Oseledets.Krieger.RefTower

The escape-symbol single-stage column code and the refining-tower assembly (C3, sub-problem B) #

This file builds the escape-symbol single-stage column alignment — the genuine repair of the two-sided bracketing defect (W7) flagged for Oseledets.Krieger.sentinelParseAt_itin_eq — and the refining-tower assembly that bundles a sequence of single-stage codes into a Oseledets.Krieger.RefiningTowerCode, hence sub-problem B's CodesTwoSidedMod0c.

The W7 defect this repairs #

Oseledets.Krieger.sentinelParseAt_itin_of_encode needs the previous column's terminating sentinel one coordinate below floor 0 of the current column (hprev). With a single skyscraper this FAILS on the bottom-most complete block of each first-return column: there, coordinate -1 is the top of the incomplete residual stub of the previous first-return column, which carries no sentinel. This is a positive-measure obstruction (the bottom blocks are a fixed positive fraction of the covered set, not a vanishing one).

The escape-symbol repair (Keane–Serafin 1998 §; Downarowicz §4.2.5; Shields §I.9) #

A reserved sentinel s : Fin k is placed so that every first-return column terminates in s (at its top floor — whether that top is the top of a complete N-block or the top of the residual stub). Then for every column base b, the coordinate e⁻¹ b (the top of the previous column) carries s, so hprev holds for the bottom block of every column too. This is exactly the device that makes every used column two-sided sentinel-bracketed.

This file isolates that repair as a clean, reusable abstract interface: a StageCode whose code spells sentinelEncode blocks on each column and places s at every column-bottom predecessor. On the well-tiled stage event the parser then recovers the cell index, via Oseledets.Krieger.sentinelParseAt_itin_of_encode with hprev discharged from the bracketing.

What is proved sorry-free here #

The honest residual (the adversarial verdict) #

What StageCode carries as hypotheses (spells, brackets) is precisely the genuinely-dynamical content the construction of one fixed measurable interleaving code must establish: that a single code : α → Fin k, on the refining sequence of Rokhlin towers, spells the sentinelEncode of each column's Q-name AND places s at every column terminator, simultaneously for all stages. Producing that one code (nested bases Bₘ₊₁ ⊆ Bₘ, the escape symbol carrying the finest column's name) and verifying spells/brackets measurably is the ≈ several-hundred-line inductive symbolic-dynamics residual. The structural reduction — escape-symbol bracketing ⟹ hprev ⟹ per-stage alignment ⟹ RefiningTowerCode — is proved here, unconditionally and sorry-free.

References #

The escape-symbol single-stage column code #

We isolate, as a clean abstract interface, exactly the data the refining-tower interleaving must supply at one stage so that on the well-tiled stage event the position-aware parser recovers the cell index. The two genuinely-dynamical hypotheses are:

StageCode.tiled then discharges the per-stage alignment via Oseledets.Krieger.sentinelParseAt_itin_of_encode.

source
structure Oseledets.Krieger.StageCode {α : Type u_1} {κ : Type u_2} {k : ℕ} [mα : MeasurableSpace α] (e : α ≃ᵐ α) (code : α → Fin k) (decode : List (Fin k) → ℕ → κ) (cellIndex : α → κ) (s : Fin k) (T : Set α) :
Type u_1

The escape-symbol single-stage column code interface. Bundles, for one fixed stage, the data the refining-tower interleaving construction supplies, isolated from the structural alignment:

  • N (≥ 1): the stage tower height; s: the reserved sentinel; emb: the data embedding;
  • base x / floor x: the column base point and within-column floor of x (x = e^{floor x} base x, floor x < N), valid on the stage event;
  • name x: the (N - 1)-length data word coding the column's Q-name;
  • spells: on the stage event, the code spells the sentinelEncode of name x along the column (hblk), and reading that block at the offset recovers the cell index;
  • brackets: the escape-symbol bracketing — the predecessor of the column base carries s.

This is precisely the per-stage residual of the refining-tower interleaving: the structural alignment sentinelParseAt_itin_of_encode is discharged from it without any further hypotheses.

  • N : ℕ

    The stage tower height.

  • hN : 1 ≤ self.N

    The height is positive.

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

    The data embedding placing data symbols into the non-sentinel letters.

  • base : α → α

    The column base point of x (valid on T).

  • floor : α → ℕ

    The within-column floor of x (valid on T).

  • name : α → List (Fin (k - 1))

    The (N - 1)-length data word coding the column's Q-name (valid on T).

  • at_floor (x : α) : x ∈ T → self.floor x < self.N ∧ x = (⇑e)^[self.floor x] (self.base x)

    On T, x sits at floor floor x < N of the column over base x.

  • name_length (x : α) : x ∈ T → (self.name x).length = self.N - 1

    On T, the data word has length N - 1.

  • spells (x : α) : x ∈ T → ∀ i < self.N, code ((⇑e)^[i] (self.base x)) = (sentinelEncode s self.emb (self.name x)).getD i s

    On T, the code spells the sentinelEncode block of the column's name along the column. The block is indexed with the junk-safe getD … s (no proof in the type); on T the index i < N is in range, so getD agrees with the genuine get used by sentinelParseAt_itin_of_encode.

  • decodes (x : α) : x ∈ T → decode (sentinelEncode s self.emb (self.name x)) (self.floor x) = cellIndex x

    On T, decoding the column block at the floor offset recovers the cell index.

  • brackets (x : α) : x ∈ T → code (e.symm (self.base x)) = s

    The escape-symbol bracketing. The predecessor of the column base carries the sentinel.

Instances For
    source
    theorem Oseledets.Krieger.StageCode.tiled {α : Type u_1} {κ : Type u_2} {k : ℕ} [mα : MeasurableSpace α] {e : α ≃ᵐ α} {code : α → Fin k} {decode : List (Fin k) → ℕ → κ} {cellIndex : α → κ} {s : Fin k} {T : Set α} (sc : StageCode e code decode cellIndex s T) (x : α) :
    x ∈ T → sentinelParseAt s decode (itin e code x) = cellIndex x

    The per-stage alignment from a StageCode (the W7 escape-symbol repair). On the well-tiled stage event T the position-aware parser of the fixed code recovers the cell index: sentinelParseAt s decode (itin e code x) = cellIndex x for every x ∈ T.

    The proof reads off x = e^{floor x} (base x) (at_floor), discharges the sentinel-placement hypotheses htop/hdata from the sentinelEncode structure via Oseledets.Krieger.sentinelParseAt_itin_of_encode, and discharges hprev from the escape-symbol bracketing brackets (code (e⁻¹ base) = s): the previous column's terminator sits exactly one coordinate below floor 0. The decode then recovers the cell index by decodes.

    The refining-tower assembly from a sequence of single-stage codes #

    A RefiningTowerCode is one fixed code, one cellIndex recovering Q mod 0, stage events T m with summable misses, and per-stage alignment. Given a sequence of StageCodes all sharing one fixed code, decode, cellIndex and sentinel s — the output of the interleaving — the per-stage alignment is StageCode.tiled at each m. The summable-misses field is supplied directly (∑ εₘ < ∞, εₘ = 2^{−(m+1)} in the Keane–Serafin construction).

    source
    noncomputable def Oseledets.Krieger.RefiningTowerCode.ofStages {α : Type u_1} {κ : Type u_2} {k : ℕ} [mα : MeasurableSpace α] {μ : MeasureTheory.Measure α} [Countable κ] [MeasurableSpace κ] [MeasurableSingletonClass κ] {e : α ≃ᵐ α} {Q : κ → Set α} (s : Fin k) (code : α → Fin k) (hcode : Measurable code) (decode : List (Fin k) → ℕ → κ) (cellIndex : α → κ) (hQ : ∀ (j : κ), Q j =ᵐ[μ] {x : α | cellIndex x = j}) (T : ℕ → Set α) (hsum : ∑' (m : ℕ), μ (T m)ᶜ ≠ ⊤) (stages : (m : ℕ) → StageCode e code decode cellIndex s (T m)) :
    RefiningTowerCode e μ Q k

    The refining-tower code from a sequence of single-stage codes. Bundles one fixed measurable code, one fixed cellIndex (recovering Q mod 0), stage events T m with summable misses, and — the genuinely-dynamical content — a StageCode at each stage m (all sharing the same code/decode/cellIndex/s), into a RefiningTowerCode. The per-stage alignment field stage_tiled is StageCode.tiled at each m; everything else is supplied verbatim.

    This is the clean exit the refining-tower interleaving plugs into: once one fixed code is built that, on each stage, spells sentinelEncode blocks and brackets every column with s (StageCode.spells/brackets), and the stage misses are summable, the full RefiningTowerCode — hence sub-problem B's CodesTwoSidedMod0c — is assembled.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem Oseledets.Krieger.RefiningTowerCode.codes_ofStages {α : Type u_1} {κ : Type u_2} {k : ℕ} [mα : MeasurableSpace α] {μ : MeasureTheory.Measure α} [Countable κ] [MeasurableSpace κ] [MeasurableSingletonClass κ] {e : α ≃ᵐ α} {Q : κ → Set α} (s : Fin k) (code : α → Fin k) (hcode : Measurable code) (decode : List (Fin k) → ℕ → κ) (cellIndex : α → κ) (hQ : ∀ (j : κ), Q j =ᵐ[μ] {x : α | cellIndex x = j}) (T : ℕ → Set α) (hsum : ∑' (m : ℕ), μ (T m)ᶜ ≠ ⊤) (stages : (m : ℕ) → StageCode e code decode cellIndex s (T m)) :
      CodesTwoSidedMod0c e Q (codePartition (ofStages s code hcode decode cellIndex hQ T hsum stages).toColumnLayoutData.code ⋯)

      A refining-tower code from a sequence of stages yields CodesTwoSidedMod0c. Composing RefiningTowerCode.ofStages with Oseledets.Krieger.RefiningTowerCode.codes closes sub-problem B's symbolic side: the cross-layer countable mod-0 code of Q by the code partition. The entire residual is concentrated in producing the single fixed interleaving code and its per-stage StageCodes.