The position-aware sentinel parser for Krieger's column code (C3, sub-problem B)

This file repairs and sharpens the bi-infinite sentinel parser of Oseledets.Krieger.ColumnCode. The parser there, sentinelParse s dec w = dec (blockContent s w), decodes the content of the sentinel block containing coordinate 0. The dynamical-recovery field that SentinelColumnCode then demands is

recovers : ∀ j, Q j =ᵐ[μ] {x | sentinelParse s decode (itin e code x) = j},

i.e. the parser, fed the two-sided itinerary of a point x, must recover which Q-cell x itself lies in. We show this is impossible for a generic countable generator Q: sentinelParse is position-blind. The block content is the same list of symbols for every point on the same tower column, while distinct floors of one column lie in genuinely different Q-cells (a generator's cells cut across the floors). Formally, the two-sided itinerary intertwines the dynamics with the one-step shift shift w n = w (n+1) (itin_apply_e), and sentinelParse is invariant under that shift inside a block (sentinelParse_shift_eq): so the parser returns the same label at x and at e x whenever both sit in one column, and no decode can make the parser event coincide with the non-e-invariant cell Q j.

The fix: carry the within-block offset

The classical Krieger/Downarowicz decoder reads off the Q-name at coordinate 0 by (i) locating the sentinel-marked column boundaries, (ii) determining the offset of coordinate 0 inside the column, and (iii) reading the symbol at that offset. Step (ii) — the offset — is available from the stream (blockOffset s w = bwdSentinel s (-1) w, the distance back to the column's lower sentinel), but sentinelParse discards it. The corrected parser

sentinelParseAt s dec w = dec (blockContent s w) (blockOffset s w),

with dec : List (Fin k) → ℕ → κ taking the block content and the offset, keeps the offset channel. It is still measurable (the offset is measurable_bwdSentinel, the content is the ColumnCode decomposition), and — crucially — it is not shift-invariant: the offset increases by one under the one-step shift (blockOffset_shift), so sentinelParseAt does distinguish x from e x (sentinelParseAt_can_separate). The repaired residual bundle SentinelColumnCodeAt uses it, and SentinelColumnCodeAt.toColumnCodeData shows it yields a full Oseledets.Krieger.ColumnCodeData exactly as before, but now with a recovery field that is satisfiable by the floor-address column code.

Main definitions

• shift — the one-step shift w ↦ (n ↦ w (n+1)) of a bi-infinite stream.
• blockOffset s w — the offset of coordinate 0 inside its sentinel block (= bwdSentinel s (-1)).
• sentinelParseAt s dec w — the position-aware parser, dec (blockContent s w) (blockOffset).
• SentinelColumnCodeAt — the repaired residual bundle (code symbol + position-aware decode + satisfiable a.e. recovery).

Main results

• sentinelParse_shift_eq — the obstruction: the old parser is shift-invariant inside a block.
• parse_event_cannot_separate — the old parser returns the same label at x and e x (the reason SentinelColumnCode.recovers is unsatisfiable for a generic generator).
• blockOffset_shift — the offset increases by one under the shift (the repaired position channel).
• measurable_sentinelParseAt — the position-aware parser is measurable.
• sentinelParseAt_can_separate — the position-aware parser can distinguish x from e x.
• SentinelColumnCodeAt.toColumnCodeData / .codes — the repaired bundle yields a full ColumnCodeData, hence the cross-layer mod-0 code.
• floorAddr / measurable_floorAddr — the measurable floor-address map of a Rokhlin tower (the within-column floor index), the first dynamical field of the code symbol (point (1) of the Recovery note).

References

• Tomasz Downarowicz, Entropy in Dynamical Systems, Cambridge (2011), §4.2 (Lemma 4.2.5).
• Paul C. Shields, The Ergodic Theory of Discrete Sample Paths, GSM 13, AMS (1996), §I.9.
• Wolfgang Krieger, On entropy and generators of measure-preserving transformations, Trans. Amer. Math. Soc. 149 (1970), 453–464.

The one-step shift of a bi-infinite stream and its window/sentinel calculus

def Oseledets.Krieger.shift {k : ℕ} (w : ℤ → Fin k) : ℤ → Fin k

The one-step shift of a bi-infinite stream: shift w n = w (n + 1). The two-sided itinerary intertwines the dynamics e with this shift (itin_apply_e): itin e c (e x) = shift (itin e c x).

Equations

• Oseledets.Krieger.shift w n = w (n + 1)

theorem Oseledets.Krieger.window_shift {k : ℕ} (w : ℤ → Fin k) (b : ℤ) (L : ℕ) : window (shift w) b L = window w (b + 1) L

window commutes with the shift: window (shift w) b L = window w (b + 1) L.

theorem Oseledets.Krieger.bwdSentinel_shift {k : ℕ} (s : Fin k) (w : ℤ → Fin k) (h0 : w 0 ≠ s) (hbwd : ∃ (m : ℕ), w (-1 - ↑m) = s) : bwdSentinel s (-1) (shift w) = bwdSentinel s (-1) w + 1

Under w 0 ≠ s and a backward sentinel, the backward sentinel distance increases by one under the shift.

theorem Oseledets.Krieger.fwdSentinel_shift {k : ℕ} (s : Fin k) (w : ℤ → Fin k) (h0 : w 0 ≠ s) (hfwd : ∃ (m : ℕ), w (0 + ↑m) = s) : fwdSentinel s 0 (shift w) + 1 = fwdSentinel s 0 w

Under w 0 ≠ s and a forward sentinel, the forward sentinel distance decreases by one under the shift.

The obstruction: the position-blind parser cannot recover coordinate 0's cell

theorem Oseledets.Krieger.blockContent_shift_eq {k : ℕ} (s : Fin k) (w : ℤ → Fin k) (h0 : w 0 ≠ s) (hbwd : ∃ (m : ℕ), w (-1 - ↑m) = s) (hfwd : ∃ (m : ℕ), w (0 + ↑m) = s) : blockContent s (shift w) = blockContent s w

The block content is shift-invariant inside a block. If coordinate 0 of the stream w is not a sentinel and there are sentinels in both directions (the generic tiled case), then the sentinel block around coordinate 0 of w and that of the one-step shift shift w are the same list of symbols. The block re-anchors by one coordinate, but its content is identical: this is the position-blindness of blockContent.

theorem Oseledets.Krieger.sentinelParse_shift_eq {κ : Type u_2} {k : ℕ} (s : Fin k) (dec : List (Fin k) → κ) (w : ℤ → Fin k) (h0 : w 0 ≠ s) (hbwd : ∃ (m : ℕ), w (-1 - ↑m) = s) (hfwd : ∃ (m : ℕ), w (0 + ↑m) = s) : sentinelParse s dec (shift w) = sentinelParse s dec w

The old parser is shift-invariant inside a block. Consequently sentinelParse s dec returns the same κ-label at w and at its one-step shift shift w whenever coordinate 0 is not a sentinel and the stream is tiled in both directions.

theorem Oseledets.Krieger.itin_apply_e {α : Type u_1} {k : ℕ} [mα : MeasurableSpace α] (e : α ≃ᵐ α) (c : α → Fin k) (x : α) : itin e c (e x) = shift (itin e c x)

The two-sided itinerary intertwines e with the one-step shift: itin e c (e x) = shift (itin e c x).

theorem Oseledets.Krieger.parse_event_cannot_separate {α : Type u_1} {κ : Type u_2} {k : ℕ} [mα : MeasurableSpace α] (s : Fin k) (dec : List (Fin k) → κ) (e : α ≃ᵐ α) (c : α → Fin k) (x : α) (h0 : itin e c x 0 ≠ s) (hbwd : ∃ (m : ℕ), itin e c x (-1 - ↑m) = s) (hfwd : ∃ (m : ℕ), itin e c x (0 + ↑m) = s) : sentinelParse s dec (itin e c (e x)) = sentinelParse s dec (itin e c x)

The obstruction at the dynamical level. For a point x whose itinerary stream is tiled (a forward and backward sentinel exist) and whose coordinate 0 is not a sentinel, the position-blind parser returns the same label at x and at e x: sentinelParse s dec (itin e c (e x)) = sentinelParse s dec (itin e c x). Since the floors x and e x of one tower column lie in genuinely different cells of a generator Q, the parser event {x | sentinelParse s dec (itin e c x) = j} cannot equal Q j a.e. for a generic generator — the recovers field of Oseledets.Krieger.SentinelColumnCode is unsatisfiable.

The fix: the position-aware parser

noncomputable def Oseledets.Krieger.blockOffset {k : ℕ} (s : Fin k) (w : ℤ → Fin k) : ℕ

The within-block offset of coordinate 0. The distance from coordinate 0 back to the lower sentinel of its block, bwdSentinel s (-1) w. Equivalently -blockStart s w. In the tiled case it is exactly the floor index of x within its tower column, the piece of information the position-blind blockContent discards.

Equations

• Oseledets.Krieger.blockOffset s w = Oseledets.Krieger.bwdSentinel s (-1) w

@[simp]

theorem Oseledets.Krieger.blockOffset_def {k : ℕ} (s : Fin k) (w : ℤ → Fin k) : blockOffset s w = bwdSentinel s (-1) w

theorem Oseledets.Krieger.blockOffset_shift {k : ℕ} (s : Fin k) (w : ℤ → Fin k) (h0 : w 0 ≠ s) (hbwd : ∃ (m : ℕ), w (-1 - ↑m) = s) : blockOffset s (shift w) = blockOffset s w + 1

The offset increases by one under the shift (the repaired position channel). If coordinate 0 is not a sentinel and a backward sentinel exists, then blockOffset s (shift w) = blockOffset s w + 1 — matching the fact that e x sits one floor higher in its column than x. This is exactly the information that distinguishes x from e x, lost by the position-blind parser and restored here.

theorem Oseledets.Krieger.measurableSet_blockOffset_eq {k : ℕ} (s : Fin k) (o : ℕ) : MeasurableSet {w : ℤ → Fin k | blockOffset s w = o}

The block-offset level set is measurable (it is a level set of the measurable backward sentinel distance).

noncomputable def Oseledets.Krieger.sentinelParseAt {κ : Type u_2} {k : ℕ} (s : Fin k) (dec : List (Fin k) → ℕ → κ) (w : ℤ → Fin k) : κ

The position-aware bi-infinite sentinel parser. Given a block-decode map dec : List (Fin k) → ℕ → κ taking the block content and the within-block offset of coordinate 0, the parser reads off both blockContent s w and blockOffset s w, and decodes: sentinelParseAt s dec w = dec (blockContent s w) (blockOffset s w). Unlike sentinelParse, it has access to where coordinate 0 sits inside its column, so it can recover the Q-cell of x itself (not merely the column name).

Equations

• Oseledets.Krieger.sentinelParseAt s dec w = dec (Oseledets.Krieger.blockContent s w) (Oseledets.Krieger.blockOffset s w)

theorem Oseledets.Krieger.measurableSet_parseAt_eq {κ : Type u_2} {k : ℕ} [MeasurableSpace κ] [MeasurableSingletonClass κ] (s : Fin k) (dec : List (Fin k) → ℕ → κ) (j : κ) : MeasurableSet {w : ℤ → Fin k | dec (blockContent s w) (blockOffset s w) = j}

Each position-aware parser preimage is measurable. For a target label j : κ, the set {w | dec (blockContent s w) (blockOffset s w) = j} is the countable union, over block starts b : ℤ, lengths L : ℕ, contents l : List (Fin k), and offsets o : ℕ with dec l o = j, of the cylinder {blockStart = b} ∩ {blockLen = L} ∩ {window b L = l} ∩ {blockOffset = o}. Each factor is measurable (measurableSet_blockStart_eq, measurableSet_blockLen_eq, measurableSet_window_eq, measurableSet_blockOffset_eq) and the index types are countable.

theorem Oseledets.Krieger.measurable_sentinelParseAt {κ : Type u_2} {k : ℕ} [Countable κ] [MeasurableSpace κ] [MeasurableSingletonClass κ] (s : Fin k) (dec : List (Fin k) → ℕ → κ) : Measurable (sentinelParseAt s dec)

The position-aware sentinel parser is measurable. The codomain κ is Countable with MeasurableSingletonClass, so measurable_to_countable' reduces to measurability of each preimage, supplied by measurableSet_parseAt_eq.

theorem Oseledets.Krieger.sentinelParseAt_can_separate {κ : Type u_2} {k : ℕ} (s : Fin k) (dec : List (Fin k) → ℕ → κ) (w : ℤ → Fin k) (h0 : w 0 ≠ s) (hbwd : ∃ (m : ℕ), w (-1 - ↑m) = s) (hfwd : ∃ (m : ℕ), w (0 + ↑m) = s) : sentinelParseAt s dec (shift w) = dec (blockContent s w) (blockOffset s w + 1)

The position-aware parser can separate x from e x — it is not shift-invariant. Whereas sentinelParse returns the same label at x and e x (parse_event_cannot_separate), sentinelParseAt reads the offset, which increases by one under the shift (blockOffset_shift), so it evaluates dec at offsets blockOffset s w and blockOffset s w + 1 on the same block content. A decoder that reads off the symbol at the offset position therefore recovers the distinct Q-cells of the two floors. This is the capability the repaired recovers field relies on.

The repaired residual bundle

structure Oseledets.Krieger.SentinelColumnCodeAt {α : Type u_1} {κ : Type u_2} [mα : MeasurableSpace α] [Countable κ] [MeasurableSpace κ] [MeasurableSingletonClass κ] (e : α ≃ᵐ α) (μ : MeasureTheory.Measure α) (Q : κ → Set α) (k : ℕ) : Type (max u_1 u_2)

The repaired column-code residual. Identical to Oseledets.Krieger.SentinelColumnCode except that the decoder is position-aware — decode : List (Fin k) → ℕ → κ reads both the block content and the within-block offset of coordinate 0. The recovery field uses the position-aware parser sentinelParseAt, and is satisfiable by the floor-address column code (the floors of a column carry distinct offsets, so decode block offset can return the genuine Q-cell of x), unlike SentinelColumnCode.recovers.

• sentinel : Fin k

  The reserved sentinel letter of the Fin k alphabet.

• code : α → Fin k

  The measurable code symbol c : α → Fin k of the column coding.

• code_measurable : Measurable self.code

  The code symbol is measurable.

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

  The position-aware per-block decode map (block content and offset of coordinate 0).

• recovers (j : κ) : Q j =ᵐ[μ] {x : α | sentinelParseAt self.sentinel self.decode (itin e self.code x) = j}

  A.e. correctness of the position-aware sentinel parse.

noncomputable def Oseledets.Krieger.SentinelColumnCodeAt.toColumnCodeData {α : Type u_1} {κ : Type u_2} {k : ℕ} [mα : MeasurableSpace α] {μ : MeasureTheory.Measure α} [Countable κ] [MeasurableSpace κ] [MeasurableSingletonClass κ] {e : α ≃ᵐ α} {Q : κ → Set α} (data : SentinelColumnCodeAt e μ Q k) : ColumnCodeData e μ Q k

The repaired residual yields a full ColumnCodeData. The decoder field is filled by the measurable position-aware parser sentinelParseAt sentinel decode (measurable_sentinelParseAt), and the recovery field is the supplied a.e. correctness.

Equations

• data.toColumnCodeData = { code := data.code, code_measurable := ⋯, decoder := Oseledets.Krieger.sentinelParseAt data.sentinel data.decode, decoder_measurable := ⋯, recovers := ⋯ }

theorem Oseledets.Krieger.SentinelColumnCodeAt.codes {α : Type u_1} {κ : Type u_2} {k : ℕ} [mα : MeasurableSpace α] {μ : MeasureTheory.Measure α} [Countable κ] [MeasurableSpace κ] [MeasurableSingletonClass κ] {e : α ≃ᵐ α} {Q : κ → Set α} (data : SentinelColumnCodeAt e μ Q k) : CodesTwoSidedMod0c e Q (codePartition data.code ⋯)

A SentinelColumnCodeAt yields the cross-layer countable mod-0 code of Q by its code partition — the deliverable that slots into Oseledets.Krieger.KriegerCodingData.code_codes.

The measurable floor-address map of a Rokhlin tower

The first dynamical field of a SentinelColumnCodeAt — the code symbol c : α → Fin k — is built from the floor-address map of a Rokhlin tower (Oseledets.Krieger.rokhlin_tower): the index of the floor a point sits on within its column. We construct it here as a measurable ℕ-valued map (junk value N off the tower), which is exactly the within-column offset the position-aware parser (blockOffset) consumes. This is the self-contained, reusable piece point (1) of the Recovery module note asked for (and is reused by KeaneSerafinLevels for sub-problem A).

def Oseledets.Krieger.level {α : Type u_1} [mα : MeasurableSpace α] (e : α ≃ᵐ α) (A : Set α) (N i : ℕ) : Set α

The floor levels of the tower: level e A N i = eⁱ '' (towerBase e A N).

Equations

• Oseledets.Krieger.level e A N i = (⇑e)^[i] '' Oseledets.Krieger.towerBase e A N

theorem Oseledets.Krieger.measurableSet_level {α : Type u_1} [mα : MeasurableSpace α] (e : α ≃ᵐ α) {A : Set α} (hA : MeasurableSet A) (N i : ℕ) : MeasurableSet (level e A N i)

noncomputable def Oseledets.Krieger.floorAddr {α : Type u_1} [mα : MeasurableSpace α] (e : α ≃ᵐ α) (A : Set α) (N : ℕ) (x : α) : ℕ

The floor-address map of a Rokhlin tower: the least i < N with x ∈ eⁱ '' B, or N if x is off the tower. By level disjointness (pairwise_disjoint_levels) this least index is the unique one, so the map is the genuine floor address. It feeds the per-column block read of the code symbol c (point (1) of the Recovery note), and its value is the within-block offset of the position-aware parser on the corresponding itinerary.

Equations

• Oseledets.Krieger.floorAddr e A N x = if h : ∃ i < N, x ∈ Oseledets.Krieger.level e A N i then Nat.find h else N

theorem Oseledets.Krieger.floorAddr_spec {α : Type u_1} [mα : MeasurableSpace α] (e : α ≃ᵐ α) (A : Set α) (N : ℕ) {x : α} (h : ∃ i < N, x ∈ level e A N i) : floorAddr e A N x < N ∧ x ∈ level e A N (floorAddr e A N x)

On the tower, floorAddr picks an index < N and x lies in that level.

theorem Oseledets.Krieger.floorAddr_eq_level {α : Type u_1} [mα : MeasurableSpace α] (e : α ≃ᵐ α) (A : Set α) {N : ℕ} (hN : 1 ≤ N) {i : ℕ} (hi : i < N) : {x : α | floorAddr e A N x = i} = level e A N i

The floor-address level set, for i < N, is exactly the i-th level (using disjointness: the least admissible index is the unique one).

theorem Oseledets.Krieger.floorAddr_eq_N {α : Type u_1} [mα : MeasurableSpace α] (e : α ≃ᵐ α) (A : Set α) (N : ℕ) : {x : α | floorAddr e A N x = N} = (coveredSet e A N)ᶜ

The off-tower level set is the complement of the covered set.

theorem Oseledets.Krieger.measurable_floorAddr {α : Type u_1} [mα : MeasurableSpace α] (e : α ≃ᵐ α) {A : Set α} (hA : MeasurableSet A) {N : ℕ} (hN : 1 ≤ N) : Measurable (floorAddr e A N)

The floor-address map is measurable. A ℕ-valued map whose level sets are the tower levels (for i < N, floorAddr_eq_level), the covered-set complement (for i = N, floorAddr_eq_N), or empty (for i > N); each is measurable, and ℕ is countable.