Streams

Streams and windows

A stream, a discrete record of events over time, is here an infinite sequence of bits: a function from natural numbers to booleans, written Stream := Nat → Bool. A finite window, or pattern, of length n is a function from the first n positions to booleans, Pattern n := Fin n → Bool. The integer functional Z counts the ones in such a window: Z_of_window w = ∑ i, if w i then 1 else 0. This is the basic vocabulary for describing what a stream looks like over a finite stretch.

The framework proves elementary but load-bearing facts about these objects. The count of ones in any window is never negative, and the count in an empty window is zero. A cylinder set is the set of streams whose first n bits match a given window; the empty window's cylinder is the whole space of streams. The key construction is periodic extension: given an 8-bit window, extendPeriodic8 repeats it forever, so the stream at time t equals the window at position t mod 8. The framework proves this extension is genuinely periodic, with period 8: the stream at t+8 equals the stream at t.

Two results tie the pieces together. First, if a stream lies in a window's cylinder, then the sum of its first n bits equals the window's Z count. Second, for an 8-bit window extended periodically, the sum of the first 8 bits equals Z of that window. These are simple identities, but they are the bridge between a finite pattern and the infinite display it generates: the periodic stream's initial segment exactly reproduces the window's count.

The classical setting for these objects is symbolic dynamics, where a stream is a bi-infinite or one-sided sequence over a finite alphabet, and a cylinder set is the basic open set of sequences sharing a fixed finite block. The framework's ledger, the record of recognition events, is modeled as such a stream, and the 8-bit window is the natural unit because the framework's forcing chain fixes an eight-tick cycle. This framework supplies the formal plumbing: it defines the stream, the window, the count, the cylinder, and the periodic extension, and it proves the consistency lemmas that let later arguments treat an 8-bit pattern as a self-repeating stream.

In plain language, the framework says: if you fix a block of eight bits and repeat it forever, the infinite sequence you get has exactly the count you started with, and it agrees with the block on its first eight positions. That is not deep mathematics, but it is the kind of foundation a machine-checked library needs before it can talk about recognition cycles as streams. The payoff is that the framework's eight-tick cycle can be treated as an infinite periodic stream, with finite windows as its observable slices.

/-- Boolean stream as an infinite display. -/
def Stream := Nat → Bool

lemma Z_of_window_nonneg {n : Nat} (w : Pattern n) : 0 ≤ Z_of_window w := by
  unfold Z_of_window
  apply Finset.sum_nonneg
  intro i _
  split <;> decide

lemma extendPeriodic8_period (w : Pattern 8) (t : Nat) :
  extendPeriodic8 w (t + 8) = extendPeriodic8 w t := by
  dsimp [extendPeriodic8]
  have hmod : (t + 8) % 8 = t % 8 := by
    rw [Nat.add_mod]
    simp
  have h8 : 0 < 8 := by decide
  have hfin : (⟨(t + 8) % 8, Nat.mod_lt _ h8⟩ : Fin 8)
            = ⟨t % 8, Nat.mod_lt _ h8⟩ := by
    apply Fin.mk_eq_mk.mpr
    exact hmod
  rw [hfin]

/-- If a stream agrees with a window on its first `n` bits, then the first‑`n` sum equals `Z`. -/
lemma sumFirst_eq_Z_on_cylinder {n : Nat} (w : Pattern n)
  {s : Stream} (hs : s ∈ Cylinder w) :
  sumFirst n s = Z_of_window w := by
  unfold sumFirst Z_of_window Cylinder at *
  have : (fun i : Fin n => (if s i.val then 1 else 0)) =
         (fun i : Fin n => (if w i then 1 else 0)) := by
    funext i; simp [hs i]
  simp [this]

/-- For an 8‑bit window extended periodically, the first‑8 sum equals `Z`. -/
lemma sumFirst8_extendPeriodic_eq_Z (w : Pattern 8) :
  sumFirst 8 (extendPeriodic8 w) = Z_of_window w := by
  classical
  unfold sumFirst Z_of_window extendPeriodic8
  have hmod : ∀ i : Fin 8, (i.val % 8) = i.val := by
    intro i; exact Nat.mod_eq_of_lt i.isLt
  have h8 : 0 < 8 := by decide
  have hfun :
    (fun i : Fin 8 => (if w ⟨i.val % 8, Nat.mod_lt _ h8⟩ then 1 else 0))
    = (fun i : Fin 8 => (if w i then 1 else 0)) := by
      funext i; simp [hmod i]
  -- Now the two sums are definitionally equal by hfun.
  have := congrArg (fun f => ∑ i : Fin 8, f i) hfun
  simpa using this

What this page does not claim

This framework does not derive the eight-tick cycle; it only provides the stream formalism. No claim is made that all recognition events form a periodic stream. The framework does not define probability or measure on streams.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Streams.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: