def
definition
observeAvg8
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Streams.Blocks on GitHub at line 137.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
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