The cross-stage interleaving of one fixed measurable code (C3, sub-problem B, closure)

Oseledets.Krieger.StageBuild reduced sub-problem B of the unconditional Krieger theorem to producing a single StageInput e μ Q k: one fixed measurable code : α → Fin k that, on each refining tower stage m's event T m, agrees with that stage's concrete stageCode e (A m) (N m) (nm m) s (emb m) — the hard fields being code_floor and code_pred.

This file performs the cross-stage interleaving: it builds a StageInput from one master code code, discharging code_floor/code_pred/decodes by a coherence device that makes the per-stage agreement definitional.

The coherence device (Keane–Serafin nested refinement, made definitional)

The genuine crux (cf. Oseledets.Krieger.RefTower): summable misses ∑ₘ μ (T m)ᶜ < ∞ force the T m to overlap heavily, and on T m ∩ T m' the fixed code equals both stageCode_m and stageCode_{m'}, so the per-stage codes must be consistent. Keane–Serafin (On the countable generator theorem, Fund. Math. 157 (1998), 255–259) resolve this by nesting the towers so each stage's column code refines the previous one's; the one fixed code is the coherent limit.

We package the output of that nesting as the hypothesis bundle BracketedTowerSystem: one master code and a refining sequence of towers on which code is self-bracketed — interior column floors carry non-sentinel symbols, every column top and every column-base predecessor carries the escape symbol s. Then, crucially, defining each stage's name map nm m as the read-off of the master code along the column (weaveName) makes stageCode_m agree with code on T m by construction:

• stageCode_m (eⁱ b) = (sentinelEncode s (emb m) (weaveName … b)).getD i s, and for a self-bracketed column this getD is, at interior i, emb (decode (code (eⁱ b))) = code (eⁱ b), the embedding emb being a bijection onto the non-sentinel letters, so it inverts the read-off; at the top i = N m − 1 it is the terminator s = code (e^{N m−1} b).

So code_floor/code_pred hold definitionally from self-bracketing — the cross-stage consistency is absorbed into the single statement "code is self-bracketed on every stage", which is exactly what the nested Keane–Serafin construction delivers (one code, bracketing every refining column with s). This is the honest reduction: it turns the several per-stage agreements into one self-bracketing property of one code.

What is built here, sorry-free

• embLetter / embLetterInv — the data-letter map of the embedding and its Function.invFun inverse (a left inverse on the range), used to read off and re-encode the master code.
• weaveName / weaveName_length — the per-stage name map (the master code read off the column, inverted through emb) and its length.
• getD_sentinelEncode_weaveName_interior — the interior block read of the read-off name.
• stageCode_weaveName_eq — the coherence lemma: on a self-bracketed column, stageCode with weaveName equals the master code. This is what makes code_floor definitional.
• BracketedTowerSystem — the bundle: one master code, refining towers, the self-bracketing of code on every stage, summable misses, and the cell-index recovery.
• BracketedTowerSystem.toStageInput / BracketedTowerSystem.codes — assemble a full StageInput from a BracketedTowerSystem, discharging every field; hence CodesTwoSidedMod0c via StageInput.codes.

The honest residual

BracketedTowerSystem isolates exactly the genuinely-dynamical content the nested construction must deliver: one measurable code, self-bracketed on a refining sequence of towers with summable misses. Its existence is the inductive symbolic-dynamics construction (nested bases A (m+1) ⊆ A m, heights N m ↑ ∞, the escape symbol carrying the finest column's Q-name) — the ≈ several-hundred-line heart of Keane–Serafin. The reduction proved here is the structural exit: self-bracketed master code ⟹ StageInput ⟹ CodesTwoSidedMod0c, unconditionally and sorry-free.

References

• Michael S. Keane and Jacek Serafin, On the countable generator theorem, Fund. Math. 157 (1998), 255–259 (the inductive refining construction εₖ = 2^{−(k+1)}, marker symbol).
• Tomasz Downarowicz, Entropy in Dynamical Systems, Cambridge (2011), §4.2 (Lemma 4.2.5): the refining-tower column-coding limit with a reserved marker.
• Paul C. Shields, The Ergodic Theory of Discrete Sample Paths, GSM 13, AMS (1996), §I.9.

The letter map of a data embedding and its inverse

For a data embedding emb : Fin (k - 1) ↪ NonSentinel s, write embLetter emb j : Fin k for the non-sentinel letter emb j viewed in the full alphabet. The stage's name word reads the master code off the column and inverts it through embLetter: the i-th data letter is Function.invFun (embLetter emb) (code (eⁱ b)). On a self-bracketed column the interior letters are non-sentinels in the range of emb, so embLetter inverts them exactly.

def Oseledets.Krieger.embLetter {k : ℕ} {s : Fin k} (emb : Fin (k - 1) ↪ NonSentinel s) (j : Fin (k - 1)) : Fin k

The letter map of a data embedding: emb j viewed as a letter of the full alphabet Fin k. It is injective (emb is, and the subtype coercion is).

Equations

• Oseledets.Krieger.embLetter emb j = ↑(emb j)

theorem Oseledets.Krieger.embLetter_injective {k : ℕ} {s : Fin k} (emb : Fin (k - 1) ↪ NonSentinel s) : Function.Injective (embLetter emb)

theorem Oseledets.Krieger.embLetter_ne_sentinel {k : ℕ} {s : Fin k} (emb : Fin (k - 1) ↪ NonSentinel s) (j : Fin (k - 1)) : embLetter emb j ≠ s

noncomputable def Oseledets.Krieger.embLetterInv {k : ℕ} [Nonempty (Fin (k - 1))] {s : Fin k} (emb : Fin (k - 1) ↪ NonSentinel s) (a : Fin k) : Fin (k - 1)

The inverse of the letter map (Function.invFun). On the range of embLetter it recovers the data symbol; this is a left/right inverse where applicable (embLetter_embLetterInv_of_mem_range). Needs Nonempty (Fin (k - 1)) (i.e. 2 ≤ k, a genuine requirement: the alphabet must carry a sentinel plus at least one data letter) for the junk default of Function.invFun.

Equations

• Oseledets.Krieger.embLetterInv emb a = Function.invFun (Oseledets.Krieger.embLetter emb) a

theorem Oseledets.Krieger.embLetter_embLetterInv_of_mem_range {k : ℕ} [Nonempty (Fin (k - 1))] {s : Fin k} (emb : Fin (k - 1) ↪ NonSentinel s) {a : Fin k} (ha : a ∈ Set.range (embLetter emb)) : embLetter emb (embLetterInv emb a) = a

On the range of embLetter, embLetter ∘ embLetterInv is the identity: if a = embLetter emb j for some j, then embLetter emb (embLetterInv emb a) = a.

The read-off name map of the master code

noncomputable def Oseledets.Krieger.weaveName {α : Type u_1} {k : ℕ} [mα : MeasurableSpace α] [Nonempty (Fin (k - 1))] (e : α ≃ᵐ α) (_A : Set α) (N : ℕ) (s : Fin k) (emb : Fin (k - 1) ↪ NonSentinel s) (code : α → Fin k) (b : α) : List (Fin (k - 1))

The read-off name map. For tower (A, N) and master code code, the name word of a base point b reads code off the first N - 1 interior floors of the column over b, inverting each letter through embLetter: weaveName … b = List.ofFn (fun i : Fin (N - 1) ↦ embLetterInv emb (code (eⁱ b))). On a self-bracketed column (interior letters non-sentinel and in the range of emb), encoding this word reproduces code along the column — the definitional coherence.

Equations

• Oseledets.Krieger.weaveName e _A N s emb code b = List.ofFn fun (i : Fin (N - 1)) => Oseledets.Krieger.embLetterInv emb (code ((⇑e)^[↑i] b))

@[simp]

theorem Oseledets.Krieger.weaveName_length {α : Type u_1} {k : ℕ} [mα : MeasurableSpace α] [Nonempty (Fin (k - 1))] (e : α ≃ᵐ α) (A : Set α) (N : ℕ) (s : Fin k) (emb : Fin (k - 1) ↪ NonSentinel s) (code : α → Fin k) (b : α) : (weaveName e A N s emb code b).length = N - 1

theorem Oseledets.Krieger.getD_sentinelEncode_weaveName_interior {α : Type u_1} {k : ℕ} [mα : MeasurableSpace α] [Nonempty (Fin (k - 1))] (e : α ≃ᵐ α) (A : Set α) (N : ℕ) (s : Fin k) (emb : Fin (k - 1) ↪ NonSentinel s) (code : α → Fin k) (b : α) {i : ℕ} (hi : i < N - 1) : (sentinelEncode s emb (weaveName e A N s emb code b)).getD i s = embLetter emb (embLetterInv emb (code ((⇑e)^[i] b)))

The interior block read of a read-off name. For i < N - 1, the i-th letter of the sentinel encoding of weaveName … b is embLetter emb (embLetterInv emb (code (eⁱ b))) — the master code at floor i, inverted then re-embedded. On a self-bracketed column this round-trips to code (eⁱ b) (embLetter_embLetterInv_of_mem_range); the round-trip is isolated here.

The coherence lemma: stageCode of the read-off name equals the master code

The heart of the file. On a self-bracketed column over b — interior floors carry non-sentinel letters in the range of emb, and the top floor N - 1 carries the sentinel s — the stage code stageCode … (weaveName …) evaluated at any column floor i < N equals the master code at that floor. The interior floors invert through embLetter (range membership ⟹ embLetter ∘ embLetterInv = id); the top floor reads the terminating sentinel s, which the self-bracketing equates to code. This makes StageInput.code_floor definitional.

theorem Oseledets.Krieger.stageCode_weaveName_eq {α : Type u_1} {k : ℕ} [mα : MeasurableSpace α] [Nonempty (Fin (k - 1))] (e : α ≃ᵐ α) (A : Set α) {N : ℕ} (hN : 1 ≤ N) (s : Fin k) (emb : Fin (k - 1) ↪ NonSentinel s) (code : α → Fin k) {b : α} (hb : b ∈ towerBase e A N) (hinterior : ∀ i < N - 1, code ((⇑e)^[i] b) ∈ Set.range (embLetter emb)) (htop : code ((⇑e)^[N - 1] b) = s) {i : ℕ} (hi : i < N) : stageCode e A N (weaveName e A N s emb code) s emb ((⇑e)^[i] b) = code ((⇑e)^[i] b)

The coherence lemma. Let b ∈ towerBase e A N, and suppose code is self-bracketed on the column over b: every interior floor letter code (eⁱ b) (i < N - 1) lies in the range of embLetter emb, and the top floor satisfies code (e^{N-1} b) = s. Then for every floor i < N, stageCode e A N (weaveName e A N s emb code) s emb (eⁱ b) = code (eⁱ b).

The bracketed refining-tower system and the StageInput it produces

The genuinely-dynamical output of the Keane–Serafin nested construction, isolated as a hypothesis bundle: one master measurable code, a refining sequence of towers (A m, N m) on whose columns code is self-bracketed, with summable misses and a cell-index recovery. Self-bracketing — interior floors non-sentinel/in range, every column top and base predecessor carrying s — is exactly the property the escape symbol of the nested construction guarantees. From it the StageInput fields code_floor/code_pred are definitional (stageCode_weaveName_eq / stageCode_predecessor).

structure Oseledets.Krieger.BracketedTowerSystem {α : 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 bracketed refining-tower system (the Keane–Serafin nested-construction output). One master code self-bracketed on a refining sequence of towers. The shared embedding emb is fixed across stages (the cross-stage coherence is carried by self-bracketing of the single code, not by varying emb).

• s : Fin k

  The shared reserved sentinel.

• code : α → Fin k

  The one fixed measurable master code.

• code_measurable : Measurable self.code

  The master code is measurable.

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

  The shared data embedding (fixed across stages).

• 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, with each base measurable.

• 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 (m : ℕ) (x : α) : x ∈ self.T m → ∀ i < self.N m - 1, self.code ((⇑e)^[i] (columnBase e (self.A m) (self.N m) x)) ∈ Set.range (embLetter self.emb)

  Self-bracketing, interior. On T m, every interior column floor carries a non-sentinel letter in the range of emb (so the read-off name inverts to the master code).

• top (m : ℕ) (x : α) : x ∈ self.T m → self.code ((⇑e)^[self.N m - 1] (columnBase e (self.A m) (self.N m) x)) = self.s

  Self-bracketing, top. On T m, every column top floor N m − 1 carries the sentinel.

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

  Self-bracketing, predecessor. On T m, every column-base predecessor carries the sentinel.

• 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 self.code (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.

noncomputable def Oseledets.Krieger.BracketedTowerSystem.toStageInput {α : Type u_1} {κ : Type u_2} {k : ℕ} [mα : MeasurableSpace α] {μ : MeasureTheory.Measure α} [Nonempty (Fin (k - 1))] {e : α ≃ᵐ α} {Q : κ → Set α} (B : BracketedTowerSystem e μ Q k) : StageInput e μ Q k

The StageInput from a BracketedTowerSystem. Every field is discharged: the name maps are the read-off weaveName, code_floor is the coherence lemma stageCode_weaveName_eq (using the self-bracketing interior/top), and code_pred is stageCode_predecessor reconciled with the master code via the self-bracketing pred. This is the cross-stage interleaving, made definitional: one master code, self-bracketed on every refining tower, serves all stages.

Equations

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

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

Sub-problem B closed from a bracketed refining-tower system. A BracketedTowerSystem — one master measurable code, self-bracketed on a refining sequence of towers with summable misses — yields, via StageInput.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 a BracketedTowerSystem, i.e. the Keane–Serafin nested construction of one self-bracketed code.