`voxelStep_listenNoopProgram`

proved

show as: view math explainer →

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

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

formal source

  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 :=

papers checked against this theorem

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