def definition def or abbrev

`Window`

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

formal statement (Lean)

  50def Window (n : ℕ) := Fin n → CellState

Definition body.

  51
  52/-! ## Local Update Rules -/
  53
  54/-- Neighborhood radius for the CA -/

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

costCompose_right_cancel in IndisputableMonolith.Algebra.CostAlgebra decl_use
paired_preserves_balance in IndisputableMonolith.Algebra.LedgerAlgebra decl_use
PBMDeviceSpec in IndisputableMonolith.Applied.PhotobiomodulationDevice decl_use
encodeClause in IndisputableMonolith.Complexity.CellularAutomata decl_use
beat_fraction_irreducible in IndisputableMonolith.Gap45.RecognitionBarrier decl_use
is in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom decl_use
mock_orders_exactly_odd_primes_lt_8 in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom decl_use
instant in IndisputableMonolith.Measurement.RSNative.Core decl_use
Measurement in IndisputableMonolith.Measurement.RSNative.Core decl_use
stop in IndisputableMonolith.Measurement.RSNative.Core decl_use
Window in IndisputableMonolith.Measurement.RSNative.Core decl_use
PrimeTailBound in IndisputableMonolith.NumberTheory.RiemannHypothesis.ErrorBudget decl_use
L3_scope in IndisputableMonolith.Papers.ClaimBoundaries decl_use

Lean names referenced from this declaration's body.

CellState in IndisputableMonolith.Complexity.CellularAutomata decl_use
Neighborhood in IndisputableMonolith.Complexity.CellularAutomata decl_use
radius in IndisputableMonolith.Complexity.CellularAutomata decl_use
for in IndisputableMonolith.Foundation.UniversalForcingSelfReference decl_use
Window in IndisputableMonolith.Measurement.RSNative.Core decl_use