IndisputableMonolith.Streams.Blocks

   1import Mathlib
   2
   3namespace IndisputableMonolith
   4
   5/-!
   6Pattern and Measurement layers: streams, windows, and aligned block sums.
   7This file ports the PatternLayer/MeasurementLayer cluster from the umbrella.
   8-/
   9
  10namespace PatternLayer
  11
  12open scoped BigOperators
  13open Finset
  14
  15/-- Boolean stream as an infinite display. -/
  16def Stream := Nat → Bool
  17
  18/-- A finite window/pattern of length `n`. -/
  19def Pattern (n : Nat) := Fin n → Bool
  20
  21/-- Integer functional `Z` counting ones in a finite window. -/
  22def Z_of_window {n : Nat} (w : Pattern n) : Nat :=
  23  ∑ i : Fin n, (if w i then 1 else 0)
  24
  25/-- The cylinder set of streams whose first `n` bits coincide with the window `w`. -/
  26def Cylinder {n : Nat} (w : Pattern n) : Set Stream :=
  27  { s | ∀ i : Fin n, s i.val = w i }
  28
  29/-- Periodic extension of an 8‑bit window. -/
  30def extendPeriodic8 (w : Pattern 8) : Stream := fun t =>
  31  let i : Fin 8 := ⟨t % 8, Nat.mod_lt _ (by decide)⟩
  32  w i
  33
  34/-- Sum of the first `m` bits of a stream. -/
  35def sumFirst (m : Nat) (s : Stream) : Nat :=
  36  ∑ i : Fin m, (if s i.val then 1 else 0)
  37
  38/-- If a stream agrees with a window on its first `n` bits, then the first‑`n` sum equals `Z`. -/
  39lemma sumFirst_eq_Z_on_cylinder {n : Nat} (w : Pattern n)
  40  {s : Stream} (hs : s ∈ Cylinder w) :
  41  sumFirst n s = Z_of_window w := by
  42  classical
  43  unfold sumFirst Z_of_window Cylinder at *
  44  have : (fun i : Fin n => (if s i.val then 1 else 0)) =
  45         (fun i : Fin n => (if w i then 1 else 0)) := by
  46    funext i; simpa [hs i]
  47  simpa [this]
  48
  49/-- For an 8‑bit window extended periodically, the first‑8 sum equals `Z`. -/
  50lemma sumFirst8_extendPeriodic_eq_Z (w : Pattern 8) :
  51  sumFirst 8 (extendPeriodic8 w) = Z_of_window w := by
  52  classical
  53  unfold sumFirst Z_of_window extendPeriodic8
  54  have hmod : ∀ i : Fin 8, (i.val % 8) = i.val := by
  55    intro i; exact Nat.mod_eq_of_lt i.isLt
  56  have hfun :
  57    (fun i : Fin 8 => (if w ⟨i.val % 8, Nat.mod_lt _ (by decide)⟩ then 1 else 0))
  58    = (fun i : Fin 8 => (if w i then 1 else 0)) := by
  59      funext i; simp [hmod i]
  60  have := congrArg (fun f => ∑ i : Fin 8, f i) hfun
  61  simpa using this
  62
  63end PatternLayer
  64
  65namespace MeasurementLayer
  66
  67open scoped BigOperators
  68open Finset PatternLayer
  69
  70/-- Sum of one 8‑tick sub‑block starting at index `j*8`. -/
  71def subBlockSum8 (s : Stream) (j : Nat) : Nat :=
  72  ∑ i : Fin 8, (if s (j * 8 + i.val) then 1 else 0)
  73
  74/-- Aligned block sum over `k` copies of the 8‑tick window (so instrument length `T=8k`). -/
  75def blockSumAligned8 (k : Nat) (s : Stream) : Nat :=
  76  ∑ j : Fin k, subBlockSum8 s j.val
  77
  78/-- On any stream lying in the cylinder of an 8‑bit window, the aligned
  79    first block sum (j=0; T=8k alignment) equals the window integer `Z`. -/
  80lemma firstBlockSum_eq_Z_on_cylinder (w : Pattern 8) {s : Stream}
  81  (hs : s ∈ PatternLayer.Cylinder w) :
  82  subBlockSum8 s 0 = Z_of_window w := by
  83  classical
  84  have hsum : subBlockSum8 s 0 = PatternLayer.sumFirst 8 s := by
  85    unfold subBlockSum8 PatternLayer.sumFirst
  86    simp [Nat.zero_mul, zero_add]
  87  simpa [hsum] using
  88    (PatternLayer.sumFirst_eq_Z_on_cylinder (n:=8) w (s:=s) hs)
  89
  90/-- Alias (T=8k, first block): if `s` is in the cylinder of `w`, then the
  91    aligned block sum over the first 8‑tick block equals `Z(w)`. -/
  92lemma blockSum_equals_Z_on_cylinder_first (w : Pattern 8) {s : Stream}
  93  (hs : s ∈ PatternLayer.Cylinder w) :
  94  blockSumAligned8 1 s = Z_of_window w := by
  95  classical
  96  simp [blockSumAligned8, firstBlockSum_eq_Z_on_cylinder w (s:=s) hs]
  97
  98/-- On periodic extensions of a window, each 8‑sub‑block sums to `Z`. -/
  99lemma subBlockSum8_periodic_eq_Z (w : Pattern 8) (j : Nat) :
 100  subBlockSum8 (extendPeriodic8 w) j = Z_of_window w := by
 101  classical
 102  unfold subBlockSum8 Z_of_window extendPeriodic8
 103  have hmod : ∀ i : Fin 8, ((j * 8 + i.val) % 8) = i.val := by
 104    intro i
 105    have hi : i.val < 8 := i.isLt
 106    have h0 : (j * 8) % 8 = 0 := by simpa using Nat.mul_mod j 8 8
 107    calc
 108      (j * 8 + i.val) % 8
 109          = ((j * 8) % 8 + i.val % 8) % 8 := by
 110                simpa [Nat.add_comm, Nat.add_left_comm, Nat.add_assoc, Nat.mul_comm]
 111                  using (Nat.add_mod (j*8) i.val 8)
 112      _   = (0 + i.val) % 8 := by simpa [h0, Nat.mod_eq_of_lt hi]
 113      _   = i.val % 8 := by simp
 114      _   = i.val := by simpa [Nat.mod_eq_of_lt hi]
 115  have hfun :
 116    (fun i : Fin 8 => (if w ⟨(j*8 + i.val) % 8, Nat.mod_lt _ (by decide)⟩ then 1 else 0))
 117    = (fun i : Fin 8 => (if w i then 1 else 0)) := by
 118      funext i; simp [hmod i]
 119  have := congrArg (fun f => ∑ i : Fin 8, f i) hfun
 120  simpa using this
 121
 122/-- For `s = extendPeriodic8 w`, summing `k` aligned 8‑blocks yields `k * Z(w)`. -/
 123lemma blockSumAligned8_periodic (w : Pattern 8) (k : Nat) :
 124  blockSumAligned8 k (extendPeriodic8 w) = k * Z_of_window w := by
 125  classical
 126  unfold blockSumAligned8
 127  have hconst : ∀ j : Fin k, subBlockSum8 (extendPeriodic8 w) j.val = Z_of_window w := by
 128    intro j; simpa using subBlockSum8_periodic_eq_Z w j.val
 129  have hsum : (∑ _j : Fin k, Z_of_window w) = k * Z_of_window w := by
 130    simpa using
 131      (Finset.card_univ : Fintype.card (Fin k) = k) ▸
 132      (by simpa using (Finset.sum_const_natural (s:=Finset.univ) (a:=Z_of_window w)))
 133  have hmap := congrArg (fun f => ∑ j : Fin k, f j) (funext hconst)
 134  simpa using hmap.trans hsum
 135
 136/-- Averaged (per‑window) observation equals `Z` on periodic extensions. -/
 137def observeAvg8 (k : Nat) (s : Stream) : Nat :=
 138  blockSumAligned8 k s / k
 139
 140/-- DNARP Eq. (blockSum=Z at T=8k): on the periodic extension of an 8‑bit window,
 141    the per‑window averaged observation equals the window integer `Z`. -/
 142lemma observeAvg8_periodic_eq_Z {k : Nat} (hk : k ≠ 0) (w : Pattern 8) :
 143  observeAvg8 k (extendPeriodic8 w) = Z_of_window w := by
 144  classical
 145  unfold observeAvg8
 146  have hsum := blockSumAligned8_periodic w k
 147  have : (k * Z_of_window w) / k = Z_of_window w := by
 148    exact Nat.mul_div_cancel_left (Z_of_window w) (Nat.pos_of_ne_zero hk)
 149  simpa [hsum, this]
 150
 151end MeasurementLayer
 152
 153/-! ## Examples (witnesses) -/
 154namespace Examples
 155
 156open PatternLayer MeasurementLayer
 157
 158/-- Example 8‑bit window: ones at even indices (Z=4). -/
 159def sampleW : PatternLayer.Pattern 8 := fun i => decide (i.1 % 2 = 0)
 160
 161-- Example checks (can be evaluated in an interactive session)
 162-- #eval PatternLayer.Z_of_window sampleW
 163-- #eval MeasurementLayer.observeAvg8 3 (PatternLayer.extendPeriodic8 sampleW)
 164
 165end Examples
 166
 167end IndisputableMonolith
 168