coeffSign

formal source

  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