lemma proved term proof

`eight_tick_min`

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

formal statement (Lean)

  64lemma eight_tick_min {T : Nat}
  65  (pass : Fin T → Pattern 3) (covers : Function.Surjective pass) : 8 ≤ T := by

proof body

Term-mode proof.

  66  simpa using (min_ticks_cover (d := 3) (T := T) pass covers)
  67
  68/-- Nyquist-style obstruction: if T < 2^D, no surjection to D-bit patterns. -/

used by (7)

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

eight_tick_uniqueness in IndisputableMonolith.Foundation.SimplicialLedger decl_use
impulse_after_octaves_mono_decay in IndisputableMonolith.Geology.VolcanicForcingAsJCostImpulse decl_use
octavePeriod_eq_eight in IndisputableMonolith.Geology.VolcanicForcingAsJCostImpulse decl_use
octavePeriod_is_minimal_cover in IndisputableMonolith.Geology.VolcanicForcingAsJCostImpulse decl_use
volcanicForcingAsJCostImpulseCert in IndisputableMonolith.Geology.VolcanicForcingAsJCostImpulse decl_use
eight_tick_minimal in IndisputableMonolith.NavierStokes.EightTickDynamics decl_use
grayCover_eight_tick_min in IndisputableMonolith.Patterns.GrayCycle decl_use

depends on (7)

Lean names referenced from this declaration's body.

T in IndisputableMonolith.Foundation.Breath1024 decl_use
T in IndisputableMonolith.Gap45.SyncMinimization decl_use
Pattern in IndisputableMonolith.Measurement decl_use
min_ticks_cover in IndisputableMonolith.Patterns decl_use
Pattern in IndisputableMonolith.Patterns decl_use
Pattern in IndisputableMonolith.Streams decl_use
Pattern in IndisputableMonolith.Streams.Blocks decl_use