def definition def or abbrev

`coeffSign`

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

formal statement (Lean)

  65noncomputable def coeffSign (x : ℝ) : Int :=

Definition body.

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

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

encodeIndex in IndisputableMonolith.ClassicalBridge.Fluids.LNALSemantics decl_use
coeffMag_foldPlusOneStep in IndisputableMonolith.ClassicalBridge.Fluids.Simulation2D decl_use
coeffSign_foldPlusOneStep in IndisputableMonolith.ClassicalBridge.Fluids.Simulation2D decl_use
decide_lt_zero_foldPlusOneStep in IndisputableMonolith.ClassicalBridge.Fluids.Simulation2D decl_use
foldMinusOneDecodedStep in IndisputableMonolith.ClassicalBridge.Fluids.Simulation2D decl_use
foldPlusOneStep in IndisputableMonolith.ClassicalBridge.Fluids.Simulation2D decl_use

Lean names referenced from this declaration's body.