def definition def or abbrev

`ratioInRange`

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

formal statement (Lean)

 130noncomputable def ratioInRange (pred : ModeRatioPrediction) (measured : ℝ) : Bool :=

proof body

Definition body.

 131  pred.ratio_low ≤ measured && measured ≤ pred.ratio_high
 132
 133/-! ## Healing Study Predictions -/
 134
 135/-- Distance-independent healing study protocol -/

depends on (4)

Lean names referenced from this declaration's body.

independent in IndisputableMonolith.ClassicalBridge.Fluids.LNALSemantics decl_use
ModeRatioPrediction in IndisputableMonolith.Experiments.Protocols decl_use
independent in IndisputableMonolith.Foundation.RSCoupledAxis decl_use
pred in IndisputableMonolith.RRF.Core.Vantage decl_use