def definition def or abbrev

`RSLatticeFRC`

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

formal statement (Lean)

  88def RSLatticeFRC (s : FiniteVolumeProfile) : Prop :=

Definition body.

  89  Jcost (normalizedRatio s) ≤ Real.sqrt s.siteCount
  90
  91/-- Weak lattice FRC: there exists some finite bound. -/

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

FRCBridgeCert in IndisputableMonolith.NavierStokes.FRCBridge decl_use
frc_holds_on_RS_lattice in IndisputableMonolith.NavierStokes.FRCBridge decl_use
LatticeRegularityCertificate in IndisputableMonolith.NavierStokes.FRCBridge decl_use
lattice_regular_via_direction_constancy in IndisputableMonolith.NavierStokes.FRCBridge decl_use

Lean names referenced from this declaration's body.