IndisputableMonolith.ClassicalBridge.Fluids.LNALSemantics

   1import Mathlib.Data.Fintype.Basic
   2import IndisputableMonolith.ClassicalBridge.Fluids.LNAL
   3import IndisputableMonolith.ClassicalBridge.Fluids.Galerkin2D
   4
   5namespace IndisputableMonolith.ClassicalBridge.Fluids
   6
   7open Real
   8open scoped InnerProductSpace
   9
  10/-!
  11# LNALSemantics (Milestone M2)
  12
  13This file provides:
  14- a minimal **spatial** semantics for running an LNAL program over an `LNALField`
  15  (an `Array (Reg6 × Aux5)`), and
  16- an explicit **encoding** of the 2D Galerkin Fourier state (`Galerkin2D`) into LNAL voxels.
  17
  18This is intentionally minimal (no neighbor graph / no coupling between voxels yet).
  19-/
  20
  21namespace LNALSemantics
  22
  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/-!
  57## Encoding Galerkin2D → LNALField
  58-/
  59
  60/-- Quantize a real coefficient to an integer magnitude (very coarse; placeholder for later). -/
  61noncomputable def coeffMag (x : ℝ) : Int :=
  62  Int.floor |x|
  63
  64/-- A sign/parity encoding for a real coefficient. -/
  65noncomputable def coeffSign (x : ℝ) : Int :=
  66  if x < 0 then (-1) else 1
  67
  68/-- Encode a single Galerkin coefficient (at one Fourier mode and one component) into an LNAL voxel. -/
  69noncomputable def encodeIndex {N : ℕ} (u : GalerkinState N) (i : (modes N) × Fin 2) : LNALVoxel :=
  70  let k : Mode2 := (i.1 : Mode2)
  71  let x : ℝ := u i
  72  let r6 : Reg6 :=
  73    { nuPhi := coeffMag x
  74      ell := k.1
  75      sigma := coeffSign x
  76      tau := k.2
  77      kPerp := Int.ofNat i.2.val
  78      phiE := decide (x < 0) }
  79  (r6, Aux5.zero)
  80
  81/-- Encode an entire 2D Galerkin state into an `LNALField`.
  82
  83We use `Fintype.equivFin` to give a deterministic indexing of the finite coefficient set
  84`(modes N) × Fin 2`, then store one coefficient per voxel.
  85-/
  86noncomputable def encodeGalerkin2D {N : ℕ} (u : GalerkinState N) : LNALField :=
  87  let e : Fin (Fintype.card ((modes N) × Fin 2)) ≃ ((modes N) × Fin 2) :=
  88    (Fintype.equivFin ((modes N) × Fin 2)).symm
  89  Array.ofFn (fun j => encodeIndex u (e j))
  90
  91end Encoding
  92
  93end IndisputableMonolith.ClassicalBridge.Fluids
  94