IndisputableMonolith.ClassicalBridge.Fluids.LNAL

   1import Mathlib
   2import IndisputableMonolith.LNAL.VM
   3
   4namespace IndisputableMonolith
   5namespace ClassicalBridge
   6namespace Fluids
   7
   8/-!
   9# Fluids Bridge: LNAL spatial interface
  10
  11The existing LNAL core (`IndisputableMonolith/LNAL/VM.lean`) defines the single-voxel VM.
  12For fluids we need a **spatial** semantics (a whole field of voxels).
  13
  14This file defines a minimal, *bridge-local* interface:
  15
  16- the spatial state is an array of `(Reg6 × Aux5)` voxels
  17- a `SpatialSemantics` gives a one-step update given an `LProgram`.
  18
  19We keep this separate from `LNAL/MultiVoxelVM.lean` so the bridge can evolve without
  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
  42