def definition def or abbrev

`tick_within_epoch`

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

formal statement (Lean)

  57def tick_within_epoch (t : Tick) : Fin 8 :=

proof body

Definition body.

  58  ⟨t.index % 8, Nat.mod_lt _ (by norm_num)⟩
  59
  60/-! ## Ledger State and Temporal Progression -/
  61
  62/-- A ledger state at a given tick. The state space is indexed by ticks,
  63    not by a continuous time parameter. -/

depends on (16)

Lean names referenced from this declaration's body.

State in IndisputableMonolith.ClassicalBridge.Fluids.CPM2D decl_use
tick in IndisputableMonolith.Constants decl_use
tick in IndisputableMonolith.Constants.RSNativeUnits decl_use
A in IndisputableMonolith.Foundation.IntegrationGap decl_use
is in IndisputableMonolith.Foundation.OptionAEmpiricalProgram decl_use
is in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi decl_use
Tick in IndisputableMonolith.Foundation.TimeEmergence decl_use
is in IndisputableMonolith.GameTheory.MechanismDesignFromSigma decl_use
A in IndisputableMonolith.Masses.Anchor decl_use
Tick in IndisputableMonolith.Masses.Ribbons decl_use
Tick in IndisputableMonolith.Masses.Ribbons.Tick decl_use
is in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom decl_use
Tick in IndisputableMonolith.Measurement.RSNative.Core decl_use
A in IndisputableMonolith.Modal.Actualization decl_use
State in IndisputableMonolith.NavierStokes.DiscreteVorticity decl_use
and in IndisputableMonolith.NumberTheory.CirclePhaseLift decl_use