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)
69theorem T7_nyquist_obstruction {T D : Nat}
70 (hT : T < 2 ^ D) : ¬ ∃ f : Fin T → Pattern D, Function.Surjective f :=
proof body
Term-mode proof.
71 no_surj_small T D hT
72
73/-- At threshold T=2^D there is a bijection (no aliasing). -/
depends on (11)
Lean names referenced from this declaration's body.
-
T
in IndisputableMonolith.Foundation.Breath1024
decl_use
-
is
in IndisputableMonolith.Foundation.OptionAEmpiricalProgram
decl_use
-
is
in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi
decl_use
-
is
in IndisputableMonolith.GameTheory.MechanismDesignFromSigma
decl_use
-
T
in IndisputableMonolith.Gap45.SyncMinimization
decl_use
-
is
in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom
decl_use
-
Pattern
in IndisputableMonolith.Measurement
decl_use
-
no_surj_small
in IndisputableMonolith.Patterns
decl_use
-
Pattern
in IndisputableMonolith.Patterns
decl_use
-
Pattern
in IndisputableMonolith.Streams
decl_use
-
Pattern
in IndisputableMonolith.Streams.Blocks
decl_use