pith. machine review for the scientific record. sign in
def definition def or abbrev

encodeIndex

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  69noncomputable def encodeIndex {N : ℕ} (u : GalerkinState N) (i : (modes N) × Fin 2) : LNALVoxel :=

proof body

Definition body.

  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-/

used by (4)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (21)

Lean names referenced from this declaration's body.