No prose has been written for this declaration yet. The Lean source and graph data below render
without it.
generate prose now
formal statement (Lean)
35def sumFirst (m : Nat) (s : Stream) : Nat :=
proof body
Definition body.
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`. -/
used by (10)
From the project-wide theorem graph. These declarations reference this one in their body.
depends on (7)
Lean names referenced from this declaration's body.
-
Z
in IndisputableMonolith.Masses.Anchor
decl_use
-
Stream
in IndisputableMonolith.Measurement
decl_use
-
sumFirst
in IndisputableMonolith.Measurement
decl_use
-
Z
in IndisputableMonolith.Physics.AnchorPolicyCertified
decl_use
-
Stream
in IndisputableMonolith.Streams
decl_use
-
sumFirst
in IndisputableMonolith.Streams
decl_use
-
Stream
in IndisputableMonolith.Streams.Blocks
decl_use