def definition def or abbrev

`coeffMag`

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

formal statement (Lean)

  61noncomputable def coeffMag (x : ℝ) : Int :=

Definition body.

  62  Int.floor |x|
  63
  64/-- A sign/parity encoding for a real coefficient. -/

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

A in IndisputableMonolith.Foundation.IntegrationGap decl_use
for in IndisputableMonolith.Foundation.UniversalForcingSelfReference decl_use
parity in IndisputableMonolith.LedgerPostingAdjacency decl_use
A in IndisputableMonolith.Masses.Anchor decl_use
A in IndisputableMonolith.Modal.Actualization decl_use