abbrev definition def or abbrev

`blockSumAligned8`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  38abbrev blockSumAligned8 (k : Nat) (s : Stream) : Nat := MeasurementLayer.blockSumAligned8 k s

Definition body.

  39
  40/-- Averaged (per-window) observation over aligned blocks. -/

From the project-wide theorem graph. These declarations reference this one in their body.

blockSumAligned8_periodic in IndisputableMonolith.Measurement decl_use
blockSumAligned8 in IndisputableMonolith.Streams.Blocks decl_use
blockSumAligned8_periodic in IndisputableMonolith.Streams.Blocks decl_use
blockSum_equals_Z_on_cylinder_first in IndisputableMonolith.Streams.Blocks decl_use
observeAvg8 in IndisputableMonolith.Streams.Blocks decl_use

Lean names referenced from this declaration's body.