def definition def or abbrev

`step8`

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

formal statement (Lean)

  28def step8 {α : Type} (dyn : OneStepDynamics α) : α → α :=

Definition body.

  29  dyn.step^[8]
  30
  31/-- Iterating a one-step defect-nonincreasing map preserves defect monotonicity. -/

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

EightTickCertificate in IndisputableMonolith.NavierStokes.EightTickDynamics decl_use
eight_tick_certificate_propagates in IndisputableMonolith.NavierStokes.EightTickDynamics decl_use
step8_defect_nonincreasing in IndisputableMonolith.NavierStokes.EightTickDynamics decl_use
window_certificate_extends in IndisputableMonolith.NavierStokes.EightTickDynamics decl_use
windowDynamics in IndisputableMonolith.NavierStokes.EightTickDynamics decl_use

Lean names referenced from this declaration's body.

step in IndisputableMonolith.Complexity.CellularAutomata decl_use
one in IndisputableMonolith.Foundation.IntegersFromLogic decl_use
defect in IndisputableMonolith.Foundation.LawOfExistence decl_use
one in IndisputableMonolith.Foundation.RationalsFromLogic decl_use
map in IndisputableMonolith.Measurement.RSNative.Core decl_use
OneStepDynamics in IndisputableMonolith.NavierStokes.EightTickDynamics decl_use
one in IndisputableMonolith.QFT.SpinStatistics decl_use
one in IndisputableMonolith.RecogSpec.Core decl_use