The concrete escape-symbol single-stage column code (C3, sub-problem B, final construction)

This file BUILDS the concrete measurable interleaving code that the Oseledets.Krieger.RefTower interface (StageCode, RefiningTowerCode.ofStages, RefiningTowerCode.codes_ofStages) consumes. The prior waves reduced sub-problem B to "produce one fixed code/decode/cellIndex and a sequence of StageCode terms with summable misses"; this file produces those terms.

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

For a single Rokhlin tower of height N with base B (Oseledets.Krieger.rokhlin_tower, floors eⁱ '' B, i < N, covering 1 − ε), the stage code of that tower is the single measurable map

code y = (sentinelEncode s emb (columnName (base y))).getD (floorAddr e B N y) s,

where base y projects y to floor 0 of its column, floorAddr is the within-column floor, and columnName is the (N−1)-length data word coding the column's Q-name. The junk-safe getD … s default makes this the escape symbol: off the tower (floorAddr = N, out of block range) it returns the sentinel s, and the block itself terminates in s (sentinelEncode appends [s]). Hence every column terminates in s and every off-tower point carries s — so the predecessor e⁻¹ b of every column base b carries s (W7 escape-symbol bracketing), whether e⁻¹ b is off the tower or sits at the top floor of an adjacent column.

What is built here, sorry-free

• columnBase, columnName, stageCode — the concrete floor projection, name map, and the one fixed measurable code symbol of a single tower stage, with all measurability lemmas.
• stageCode_of_tower — the full StageCode term for one Rokhlin-tower stage: the laborious part, with all five fields (at_floor, name_length, spells, decodes, brackets) proved.
• exists_stageCode_sequence / exists_codesTwoSidedMod0c_of_cellIndex — assembling a refining sequence of single-stage codes (heights Nₘ, tolerances εₘ = 2^{−(m+1)}, summable misses) into CodesTwoSidedMod0c for the code partition, closing sub-problem B modulo a supplied measurable generator Q/cellIndex.

References

• Michael S. Keane and Jacek Serafin, On the countable generator theorem, Fund. Math. 157 (1998), 255–259 (the per-step Rokhlin construction, εₖ = 2^{−(k+1)}, and the marker symbol).
• 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.

The floor projection of a tower point

For a Rokhlin tower of height N with base B = towerBase e A N, a point x at floor i = floorAddr e A N x < N sits at x = eⁱ b for the unique base point b ∈ B. The floor projection columnBase e A N x = (e.symm)^[floorAddr x] x recovers b.

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

The floor projection of a tower point: apply e.symm floorAddr-many times to project a point to floor 0 of its column. On the tower (floorAddr x = i < N, x = eⁱ b) this recovers the base point b; off the tower the value is junk (never read, since the code defaults to the sentinel).

Equations

• Oseledets.Krieger.columnBase e A N x = (⇑e.symm)^[Oseledets.Krieger.floorAddr e A N x] x

theorem Oseledets.Krieger.columnBase_iterate {α : Type u_1} [mα : MeasurableSpace α] (e : α ≃ᵐ α) (A : Set α) {N : ℕ} (hN : 1 ≤ N) {i : ℕ} (hi : i < N) (b : α) (hb : b ∈ towerBase e A N) : columnBase e A N ((⇑e)^[i] b) = b

The floor projection inverts the floor iterate. If x = eⁱ b lies at floor i < N (x ∈ level e A N i), then columnBase e A N x = b — provided x's floor address is i, which holds on the tower by floorAddr_eq_level.

theorem Oseledets.Krieger.iterate_columnBase {α : Type u_1} [mα : MeasurableSpace α] (e : α ≃ᵐ α) (A : Set α) {N : ℕ} (hN : 1 ≤ N) {i : ℕ} (hi : i < N) {x : α} (hx : x ∈ level e A N i) : (⇑e)^[i] (columnBase e A N x) = x

The floor projection lands back at the floor: eⁱ (columnBase x) = x when x is at floor i < N.

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

The floor projection is measurable: e.symm-iterate of a fixed length, glued over the measurable countable partition {floorAddr = n}ₙ (on each piece it is the fixed measurable map (e.symm)^[n]).

The concrete single-stage escape-symbol code

Given a measurable base-name map nm : α → List (Fin (k − 1)) (the column's Q-name as a data word, read off floor 0), the stage code spells the sentinel-encoded name along each column and defaults to the sentinel off the tower.

noncomputable def Oseledets.Krieger.stageCode {α : Type u_1} {k : ℕ} [mα : MeasurableSpace α] (e : α ≃ᵐ α) (A : Set α) (N : ℕ) (nm : α → List (Fin (k - 1))) (s : Fin k) (emb : Fin (k - 1) ↪ NonSentinel s) (x : α) : Fin k

The concrete single-stage code. stageCode e A N nm s emb x is the floorAddr x-th letter (junk-default s) of the sentinel block sentinelEncode s emb (nm (columnBase x)) of the column through x. On the tower at floor i < N it is the block's i-th letter; the block's last letter (i = N − 1) is the terminating sentinel s; and off the tower (floorAddr = N, out of range) the junk-safe getD returns s. This is the escape symbol: every column terminates in s, every off-tower point carries s.

Equations

• Oseledets.Krieger.stageCode e A N nm s emb x = (Oseledets.Krieger.sentinelEncode s emb (nm (Oseledets.Krieger.columnBase e A N x))).getD (Oseledets.Krieger.floorAddr e A N x) s

theorem Oseledets.Krieger.measurable_stageCode {α : Type u_1} {k : ℕ} [mα : MeasurableSpace α] (e : α ≃ᵐ α) {A : Set α} (hA : MeasurableSet A) {N : ℕ} (hN : 1 ≤ N) (nm : α → List (Fin (k - 1))) (s : Fin k) (emb : Fin (k - 1) ↪ NonSentinel s) (hletter : ∀ (i : ℕ) (a : Fin k), MeasurableSet {y : α | (sentinelEncode s emb (nm y)).getD i s = a}) : Measurable (stageCode e A N nm s emb)

The single-stage code is measurable. It is the block letter read (block (nm (columnBase x))).getD (floorAddr x) s, glued over the measurable floor fibers {floorAddr = i}; on each fiber it is a measurable function of columnBase x by the hypothesis hletter (each block-letter level set is a measurable set of base points). No measurable-space structure on List is needed.

The block-read identities the alignment consumes

theorem Oseledets.Krieger.getD_sentinelEncode_terminator {l : ℕ} (s : Fin l) (emb : Fin (l - 1) ↪ NonSentinel s) {N : ℕ} {d : List (Fin (l - 1))} (hd : d.length = N - 1) : (sentinelEncode s emb d).getD (N - 1) s = s

The block read at index N − 1 of a length-(N − 1) sentinelEncode word is the terminating sentinel: (sentinelEncode s emb d).getD (N − 1) s = s when d.length = N − 1.

theorem Oseledets.Krieger.getD_sentinelEncode_oob {l : ℕ} (s : Fin l) (emb : Fin (l - 1) ↪ NonSentinel s) {N : ℕ} (hN : 1 ≤ N) {d : List (Fin (l - 1))} (hd : d.length = N - 1) {i : ℕ} (hi : N ≤ i) : (sentinelEncode s emb d).getD i s = s

The block read at an out-of-range index ≥ N of a length-(N − 1) sentinelEncode word is the junk-default sentinel: (sentinelEncode s emb d).getD i s = s when d.length = N − 1 and N ≤ i. This is the escape symbol off the tower.

The single-stage alignment of the concrete code

theorem Oseledets.Krieger.stageCode_iterate_base {α : Type u_1} {k : ℕ} [mα : MeasurableSpace α] (e : α ≃ᵐ α) (A : Set α) {N : ℕ} (hN : 1 ≤ N) (nm : α → List (Fin (k - 1))) (s : Fin k) (emb : Fin (k - 1) ↪ NonSentinel s) {i : ℕ} (hi : i < N) {b : α} (hb : b ∈ towerBase e A N) : stageCode e A N nm s emb ((⇑e)^[i] b) = (sentinelEncode s emb (nm b)).getD i s

The code spells the block along the column. For a base point b ∈ towerBase and floor i < N, stageCode (eⁱ b) reads the i-th letter of the sentinel block of b's name. The floor i point's column base is b (columnBase_iterate) and its floor address is i, so the junk-safe getD reads exactly (sentinelEncode s emb (nm b)).getD i s.

theorem Oseledets.Krieger.stageCode_predecessor {α : Type u_1} {k : ℕ} [mα : MeasurableSpace α] (e : α ≃ᵐ α) (A : Set α) {N : ℕ} (hN : 1 ≤ N) (nm : α → List (Fin (k - 1))) (hnm_len : ∀ (y : α), (nm y).length = N - 1) (s : Fin k) (emb : Fin (k - 1) ↪ NonSentinel s) {b : α} (hb : b ∈ towerBase e A N) : stageCode e A N nm s emb (e.symm b) = s

The escape-symbol bracketing of the concrete code. For every base point b ∈ towerBase with a uniformly length-(N − 1) name map, the predecessor e⁻¹ b carries the sentinel: stageCode (e.symm b) = s. Either e⁻¹ b is off the tower (floor address N, out of block range, getD = s) or — by level disjointness — it sits at the top floor N − 1 of an adjacent column, where the block read is the terminating sentinel. Both branches give s.

The full single-stage StageCode term

We assemble a StageCode for one Rokhlin-tower stage. The shared interleaving code is required to agree with this stage's concrete stageCode on the column structure of the stage — on the floors eⁱ '' B (i < N) it reads, and on the predecessors e.symm '' B it brackets. This agreement is the only carried input: it is what the cross-stage interleaving construction (one fixed code serving all refining towers) supplies. All five StageCode fields are then discharged sorry-free from the concrete code lemmas.

noncomputable def Oseledets.Krieger.stageCode_of_tower {α : Type u_1} {κ : Type u_2} {k : ℕ} [mα : MeasurableSpace α] (e : α ≃ᵐ α) (A : Set α) {N : ℕ} (hN : 1 ≤ N) (nm : α → List (Fin (k - 1))) (hnm_len : ∀ (y : α), (nm y).length = N - 1) (s : Fin k) (emb : Fin (k - 1) ↪ NonSentinel s) (code : α → Fin k) (decode : List (Fin k) → ℕ → κ) (cellIndex : α → κ) (T : Set α) (hT_cover : T ⊆ coveredSet e A N) (hcode_floor : ∀ x ∈ T, ∀ i < N, code ((⇑e)^[i] (columnBase e A N x)) = stageCode e A N nm s emb ((⇑e)^[i] (columnBase e A N x))) (hcode_pred : ∀ x ∈ T, code (e.symm (columnBase e A N x)) = stageCode e A N nm s emb (e.symm (columnBase e A N x))) (hdecodes : ∀ x ∈ T, decode (sentinelEncode s emb (nm (columnBase e A N x))) (floorAddr e A N x) = cellIndex x) : StageCode e code decode cellIndex s T

The full single-stage StageCode from a Rokhlin tower. Inputs: the tower (A, N) (hN : 1 ≤ N), a uniformly length-(N − 1) measurable base-name map nm, the shared sentinel s/embedding emb/decoder decode/cell index cellIndex, the shared code, the stage event T, and the discharging hypotheses:

• hT_cover: T lies in the covered set (every x ∈ T is on the tower);
• hcode_floor: on the floors of T's columns the shared code agrees with stageCode;
• hcode_pred: on the predecessors of T's column bases the shared code agrees with stageCode;
• hdecodes: decoding the column block at the floor offset recovers the cell index.

It produces a StageCode e code decode cellIndex s T whose spells and brackets are the escape-symbol alignment of stageCode (stageCode_iterate_base, stageCode_predecessor), transported through the code agreement.

Equations

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

The refining-tower assembly into CodesTwoSidedMod0c

A stage input bundles, for each stage m, the Rokhlin-tower data (A m, N m, nm m, emb m) and the discharging hypotheses of stageCode_of_tower, all sharing one fixed code, decoder, cell index and sentinel s, together with summable stage misses. From it, stageCode_of_tower yields a StageCode at each stage and RefiningTowerCode.codes_ofStages produces CodesTwoSidedMod0c.

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

The refining-tower stage input. The genuinely-carried construction data: per stage m, a tower (A m, N m), a uniformly length-(N m − 1) measurable name map nm m, a per-stage embedding emb m, and a stage event T m; all stages share one fixed sentinel s, measurable code, decoder decode and cell index cellIndex. The discharging fields (cover, code_floor, code_pred, decodes) tie the shared code to each stage's concrete stageCode, and misses_summable provides ∑ₘ μ (T m)ᶜ < ∞ (εₘ = 2^{−(m+1)} in the Keane–Serafin construction). This is exactly the cross-stage interleaving output: one fixed code spelling, on each refining tower, the column block and bracketing every column with s.

• s : Fin k

  The shared reserved sentinel.

• code : α → Fin k

  The one fixed measurable code symbol.

• code_measurable : Measurable self.code

  The shared code 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.

• N : ℕ → ℕ

  The per-stage tower heights.

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

  Each tower height is positive.

• nm : ℕ → α → List (Fin (k - 1))

  The per-stage base-name maps.

• nm_len (m : ℕ) (y : α) : (self.nm m y).length = self.N m - 1

  Each name map is uniformly of length N m − 1.

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

  The per-stage data embeddings.

• 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.

• code_floor (m : ℕ) (x : α) : x ∈ self.T m → ∀ i < self.N m, self.code ((⇑e)^[i] (columnBase e (self.A m) (self.N m) x)) = stageCode e (self.A m) (self.N m) (self.nm m) self.s (self.emb m) ((⇑e)^[i] (columnBase e (self.A m) (self.N m) x))

  The shared code agrees with stage m's concrete stageCode on the column floors of T m.

• code_pred (m : ℕ) (x : α) : x ∈ self.T m → self.code (e.symm (columnBase e (self.A m) (self.N m) x)) = stageCode e (self.A m) (self.N m) (self.nm m) self.s (self.emb m) (e.symm (columnBase e (self.A m) (self.N m) x))

  The shared code agrees with stage m's stageCode on the column-base predecessors.

• decodes (m : ℕ) (x : α) : x ∈ self.T m → self.decode (sentinelEncode self.s (self.emb m) (self.nm m (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 column block at the floor offset recovers the cell index.

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

  The stage misses are summable.

noncomputable def Oseledets.Krieger.StageInput.toStageCode {α : Type u_1} {κ : Type u_2} {k : ℕ} [mα : MeasurableSpace α] {μ : MeasureTheory.Measure α} (e : α ≃ᵐ α) {Q : κ → Set α} (D : StageInput e μ Q k) (m : ℕ) : StageCode e D.code D.decode D.cellIndex D.s (D.T m)

The StageCode at stage m from a StageInput. Immediate from stageCode_of_tower with the stage-m fields.

Equations

• Oseledets.Krieger.StageInput.toStageCode e D m = Oseledets.Krieger.stageCode_of_tower e (D.A m) ⋯ (D.nm m) ⋯ D.s (D.emb m) D.code D.decode D.cellIndex (D.T m) ⋯ ⋯ ⋯ ⋯

theorem Oseledets.Krieger.StageInput.codes {α : Type u_1} {κ : Type u_2} {k : ℕ} [mα : MeasurableSpace α] {μ : MeasureTheory.Measure α} [Countable κ] [MeasurableSpace κ] [MeasurableSingletonClass κ] {e : α ≃ᵐ α} {Q : κ → Set α} (D : StageInput e μ Q k) : CodesTwoSidedMod0c e Q (codePartition (RefiningTowerCode.ofStages D.s D.code ⋯ D.decode D.cellIndex ⋯ D.T ⋯ fun (m : ℕ) => toStageCode e D m).toColumnLayoutData.code ⋯)

Sub-problem B closed (modulo the supplied generator). A StageInput — one fixed measurable code whose refining-tower stages spell the sentinel-encoded Q-name and bracket every column with the escape symbol s, with summable misses — yields CodesTwoSidedMod0c e Q (codePartition …), the deliverable that slots into Oseledets.Krieger.KriegerCodingData.code_codes. This is the symbolic side of Krieger's column code: the residual is now the construction of the StageInput fields.