def definition def or abbrev

`voxelStep`

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

formal statement (Lean)

  26def voxelStep (P : LProgram) (v : LNALVoxel) : LNALVoxel :=

proof body

Definition body.

  27  let s0 : LState := LState.init v.1 v.2
  28  let s1 : LState := lStep P s0
  29  (s1.reg6, s1.aux5)
  30
  31/-- Minimal spatial semantics: voxels evolve independently (no neighbor interaction yet). -/

used by (8)

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

independent in IndisputableMonolith.ClassicalBridge.Fluids.LNALSemantics decl_use
independent_step_listenNoopProgram in IndisputableMonolith.ClassicalBridge.Fluids.LNALSemantics decl_use
voxelStep_listenNoopProgram in IndisputableMonolith.ClassicalBridge.Fluids.LNALSemantics decl_use
decodeCoeff_voxelStep_foldMinusOne_encodeIndex in IndisputableMonolith.ClassicalBridge.Fluids.Simulation2D decl_use
SimulationHypothesis in IndisputableMonolith.ClassicalBridge.Fluids.Simulation2D decl_use
voxelStep_foldMinusOneProgram in IndisputableMonolith.ClassicalBridge.Fluids.Simulation2D decl_use
voxelStep_foldPlusOne_encodeIndex in IndisputableMonolith.ClassicalBridge.Fluids.Simulation2D decl_use
voxelStep_foldPlusOneProgram in IndisputableMonolith.ClassicalBridge.Fluids.Simulation2D decl_use

depends on (5)

Lean names referenced from this declaration's body.

LNALVoxel in IndisputableMonolith.ClassicalBridge.Fluids.LNAL decl_use
evolve in IndisputableMonolith.Thermodynamics.SecondLaw decl_use
init in IndisputableMonolith.VM.State decl_use
LState in IndisputableMonolith.VM.State decl_use
lStep in IndisputableMonolith.VM.State decl_use