structure 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)

  70structure Window where
  71  /-- Start tick. -/
  72  t0 : Nat
  73  /-- Window length in ticks (0 = instantaneous). -/
  74  len : Nat
  75  deriving DecidableEq
  76
  77namespace Window
  78

used by (13)

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
Window 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
PrimeTailBound in IndisputableMonolith.NumberTheory.RiemannHypothesis.ErrorBudget decl_use
L3_scope in IndisputableMonolith.Papers.ClaimBoundaries decl_use

depends on (3)

Lean names referenced from this declaration's body.

Window in IndisputableMonolith.Complexity.CellularAutomata decl_use
tick in IndisputableMonolith.Constants decl_use
tick in IndisputableMonolith.Constants.RSNativeUnits decl_use