`voxelStep`

definition

show as: view math explainer →

module: IndisputableMonolith.ClassicalBridge.Fluids.LNALSemantics
domain: ClassicalBridge
line: 26 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.ClassicalBridge.Fluids.LNALSemantics on GitHub at line 26.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

  23open IndisputableMonolith.LNAL
  24
  25/-- One-voxel execution: run a single LNAL step on a `(Reg6 × Aux5)` voxel. -/
  26def voxelStep (P : LProgram) (v : LNALVoxel) : LNALVoxel :=
  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). -/
  32def independent : SpatialSemantics :=
  33  { step := fun P field => field.map (voxelStep P) }
  34
  35/-- A trivial "do nothing" LNAL program: `LISTEN noop` at every instruction pointer. -/
  36@[simp] def listenNoopProgram : LProgram :=
  37  fun _ => LInstr.listen ListenMode.noop
  38
  39@[simp] lemma voxelStep_listenNoopProgram (v : LNALVoxel) :
  40    voxelStep listenNoopProgram v = v := by
  41  rcases v with ⟨r6, a5⟩
  42  simp [voxelStep, listenNoopProgram, lStep]
  43
  44@[simp] lemma independent_step_listenNoopProgram (field : LNALField) :
  45    independent.step listenNoopProgram field = field := by
  46  -- `LISTEN noop` does not change `(reg6, aux5)` for any voxel, so the spatial step is `Array.map id`.
  47  simpa [independent] using
  48    (Array.map_id'' (f := voxelStep listenNoopProgram) (h := by intro v; simp) field)
  49
  50end LNALSemantics
  51
  52namespace Encoding
  53
  54open IndisputableMonolith.LNAL
  55
  56/-!

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.