def definition def or abbrev

`stepAt`

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

formal statement (Lean)

1012noncomputable def stepAt {d : Nat} [AtomicTick (AccountRS d)] (sideAt : Nat → Side) (t : Nat) (L : LedgerState d) :
1013    LedgerState d :=

Definition body.

1014  post L (accountAt (d := d) t) (sideAt t)
1015

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

stepAt_isPostingStep in IndisputableMonolith.LedgerPostingAdjacency decl_use
stepAt_oneBitDiff in IndisputableMonolith.LedgerPostingAdjacency decl_use

Lean names referenced from this declaration's body.

AtomicTick in IndisputableMonolith.Chain decl_use
LedgerState in IndisputableMonolith.Foundation.VariationalDynamics decl_use
LedgerState in IndisputableMonolith.Information.InformationIsLedger decl_use
LedgerState in IndisputableMonolith.Information.Thermodynamics decl_use
accountAt in IndisputableMonolith.LedgerPostingAdjacency decl_use
AccountRS in IndisputableMonolith.LedgerPostingAdjacency decl_use
LedgerState in IndisputableMonolith.LedgerPostingAdjacency decl_use
post in IndisputableMonolith.LedgerPostingAdjacency decl_use
Side in IndisputableMonolith.LedgerPostingAdjacency decl_use
LedgerState in IndisputableMonolith.QFT.GaugeInvariance decl_use
AtomicTick in IndisputableMonolith.Recognition decl_use
L in IndisputableMonolith.Recognition decl_use
L in IndisputableMonolith.Recognition.Cycle3 decl_use
AtomicTick in IndisputableMonolith.RRF.Core.Recognition decl_use