structure definition def or abbrev

`StabilityCert`

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

formal statement (Lean)

 136structure StabilityCert (f : Fermion) where
 137  cert : ResidueCert
 138  cert_matches : cert.f = f
 139  cert_valid : cert.valid
 140
 141/-! ## Connection to AnchorPolicy -/
 142
 143/-- The canonical anchor from AnchorPolicy. -/

depends on (10)

Lean names referenced from this declaration's body.

canonical in IndisputableMonolith.Foundation.ArithmeticOf decl_use
from in IndisputableMonolith.Foundation.PrimitiveDistinction decl_use
canonical in IndisputableMonolith.Gap45.Beat decl_use
AnchorPolicy in IndisputableMonolith.Masses.AnchorPolicy decl_use
Fermion in IndisputableMonolith.Masses.RSBridge.Anchor decl_use
ResidueCert in IndisputableMonolith.Masses.RSBridge.Anchor decl_use
Fermion in IndisputableMonolith.Masses.SMVerification decl_use
canonical in IndisputableMonolith.NavierStokes.RM2U.NonParasitism decl_use
Fermion in IndisputableMonolith.RSBridge.Anchor decl_use
ResidueCert in IndisputableMonolith.RSBridge.Anchor decl_use