`LNALVoxel`

definition

show as: view math explainer →

module: IndisputableMonolith.ClassicalBridge.Fluids.LNAL
domain: ClassicalBridge
line: 23 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.ClassicalBridge.Fluids.LNAL on GitHub at line 23.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

used by

formal source

  20pulling in any experimental multi-voxel infrastructure.
  21-/
  22
  23abbrev LNALVoxel : Type := IndisputableMonolith.LNAL.Reg6 × IndisputableMonolith.LNAL.Aux5
  24abbrev LNALField : Type := Array LNALVoxel
  25
  26/-- A minimal interface for spatial execution of an LNAL program over a field of voxels. -/
  27structure SpatialSemantics where
  28  step : IndisputableMonolith.LNAL.LProgram → LNALField → LNALField
  29
  30namespace SpatialSemantics
  31
  32/-- Iterate `step` for `n` steps (functional execution). -/
  33def run (sem : SpatialSemantics) (P : IndisputableMonolith.LNAL.LProgram) : LNALField → Nat → LNALField
  34  | s, 0 => s
  35  | s, Nat.succ n => run sem P (sem.step P s) n
  36
  37end SpatialSemantics
  38
  39end Fluids
  40end ClassicalBridge
  41end IndisputableMonolith

papers checked against this theorem

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