`independent`

definition

show as: view math explainer →

module: IndisputableMonolith.ClassicalBridge.Fluids.LNALSemantics
domain: ClassicalBridge
line: 32 · 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 32.

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

  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|

papers checked against this theorem

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