def
definition
eightGateCoherent
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Spectra.SpectralLadder on GitHub at line 33.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
30def sum8 (x : ℕ → ℝ) (t0 : ℕ) : ℝ :=
31 (Finset.range 8).sum (fun k => x (t0 + k))
32
33def eightGateCoherent (x : ℕ → ℝ) (t0 : ℕ) : Prop :=
34 sum8 x t0 = 0
35
36end
37
38end SpectralLadder
39end Spectra
40end IndisputableMonolith