def definition def or abbrev

`certificateWithinTolerance`

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

formal statement (Lean)

 158def certificateWithinTolerance (c : ResidueCert) : Prop :=

proof body

Definition body.

 159  let theoretical := gap (ZOf c.f)
 160  (c.lo : ℝ) - anchorTolerance ≤ theoretical ∧
 161  theoretical ≤ (c.hi : ℝ) + anchorTolerance
 162
 163/-! ## Summary Statistics -/
 164
 165/-- The lepton certificates cluster around F(1332) ≈ 13.95. -/

depends on (12)

Lean names referenced from this declaration's body.

gap in IndisputableMonolith.Gap45.Derivation decl_use
gap in IndisputableMonolith.Masses.AnchorPolicy decl_use
gap in IndisputableMonolith.Masses.RSBridge.Anchor decl_use
ResidueCert in IndisputableMonolith.Masses.RSBridge.Anchor decl_use
ZOf in IndisputableMonolith.Masses.RSBridge.Anchor decl_use
F in IndisputableMonolith.Physics.AnchorPolicy decl_use
F in IndisputableMonolith.Physics.LeptonGenerations.TauStepDerivation decl_use
F in IndisputableMonolith.Pipelines decl_use
Statistics in IndisputableMonolith.QFT.SpinStatistics decl_use
gap in IndisputableMonolith.RSBridge.Anchor decl_use
ResidueCert in IndisputableMonolith.RSBridge.Anchor decl_use
ZOf in IndisputableMonolith.RSBridge.Anchor decl_use