def
definition
listenNoopProgram
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.ClassicalBridge.Fluids.LNALSemantics on GitHub at line 36.
browse module
All declarations in this module, on Recognition.
explainer page
used by
formal source
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