structure definition def or abbrev

`ResidueCert`

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

formal statement (Lean)

 134structure ResidueCert where
 135  f  : Fermion
 136  lo : ℚ
 137  hi : ℚ
 138  lo_le_hi : lo ≤ hi
 139
 140def ResidueCert.valid (c : ResidueCert) : Prop :=

proof body

Definition body.

 141  (c.lo : ℝ) ≤ gap (ZOf c.f) ∧ gap (ZOf c.f) ≤ (c.hi : ℝ)
 142
 143/-! ### Generation indexing (three disjoint families) -/
 144
 145/-- Generation index (0,1,2) assigned by rung/sector ordering. -/

used by (16)

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

ResidueCert in IndisputableMonolith.RSBridge.Anchor decl_use
ResidueCert in IndisputableMonolith.RSBridge.Anchor decl_use
allCerts in IndisputableMonolith.RSBridge.ResidueData decl_use
cert_b in IndisputableMonolith.RSBridge.ResidueData decl_use
cert_c in IndisputableMonolith.RSBridge.ResidueData decl_use
cert_d in IndisputableMonolith.RSBridge.ResidueData decl_use
cert_e in IndisputableMonolith.RSBridge.ResidueData decl_use
certificateWithinTolerance in IndisputableMonolith.RSBridge.ResidueData decl_use
cert_mu in IndisputableMonolith.RSBridge.ResidueData decl_use
cert_s in IndisputableMonolith.RSBridge.ResidueData decl_use
cert_t in IndisputableMonolith.RSBridge.ResidueData decl_use
cert_tau in IndisputableMonolith.RSBridge.ResidueData decl_use
cert_u in IndisputableMonolith.RSBridge.ResidueData decl_use
leptonCerts in IndisputableMonolith.RSBridge.ResidueData decl_use
quarkCerts in IndisputableMonolith.RSBridge.ResidueData decl_use
StabilityCert in IndisputableMonolith.RSBridge.ResidueData decl_use

depends on (21)

Lean names referenced from this declaration's body.

rung in IndisputableMonolith.Compat.Constants decl_use
rung in IndisputableMonolith.Engineering.AsteroidOreSpectroscopy decl_use
Generation in IndisputableMonolith.Foundation.SpectralEmergence decl_use
Generation in IndisputableMonolith.Foundation.UniversalForcing.BiologyRealization decl_use
gap in IndisputableMonolith.Gap45.Derivation decl_use
gap in IndisputableMonolith.Masses.AnchorPolicy decl_use
rung in IndisputableMonolith.Masses.AnchorPolicy decl_use
Fermion in IndisputableMonolith.Masses.RSBridge.Anchor decl_use
gap in IndisputableMonolith.Masses.RSBridge.Anchor decl_use
rung in IndisputableMonolith.Masses.RSBridge.Anchor decl_use
ZOf in IndisputableMonolith.Masses.RSBridge.Anchor decl_use
Fermion in IndisputableMonolith.Masses.SMVerification decl_use
Generation in IndisputableMonolith.Physics.CKM decl_use
Generation in IndisputableMonolith.Physics.ThreeGenerations decl_use
Generation in IndisputableMonolith.RecogSpec.RSLedger decl_use
Fermion in IndisputableMonolith.RSBridge.Anchor decl_use
gap in IndisputableMonolith.RSBridge.Anchor decl_use
ResidueCert in IndisputableMonolith.RSBridge.Anchor decl_use
ResidueCert in IndisputableMonolith.RSBridge.Anchor decl_use
rung in IndisputableMonolith.RSBridge.Anchor decl_use
ZOf in IndisputableMonolith.RSBridge.Anchor decl_use