def definition def or abbrev

`jBudgetUpdate`

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

formal statement (Lean)

  41def jBudgetUpdate (s : LState) : LState :=

proof body

Definition body.

  42  let boundary := s.base.winIdx8 = 0
  43  let winJPrev := if boundary then s.winJ else s.winJPrev
  44  let winJ := if boundary then 0 else s.winJ + 1
  45  { s with winJ := winJ, winJPrev := winJPrev }
  46
  47/-- Wrapped small-step that preserves legacy semantics while tracking vNext counters. -/

used by (1)

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

lStep in IndisputableMonolith.VM.State decl_use

depends on (3)

Lean names referenced from this declaration's body.

step in IndisputableMonolith.Complexity.CellularAutomata decl_use
that in IndisputableMonolith.NumberTheory.PhiLadderLattice decl_use
LState in IndisputableMonolith.VM.State decl_use