No prose has been written for this declaration yet. The Lean source and graph data below render
without it.
generate prose now
formal statement (Lean)
172def QuarkAbsoluteMassResidual : Prop :=
proof body
Definition body.
173 ∀ (f : Fermion),
174 sectorOf f = Sector.up →
175 Verification.rs_mass_MeV Anchor.Sector.UpQuark (RSBridge.rung f)
176 = M0 * Real.exp (((RSBridge.rung f : ℝ) - 8 + gap (ZOf f)) *
177 Real.log Constants.phi)
178
179/-! ## ScoreCard certificate
180
181A single record bundling every theorem-grade row of this Phase 0
182deliverable. -/
183
used by (3)
From the project-wide theorem graph. These declarations reference this one in their body.
depends on (37)
Lean names referenced from this declaration's body.
-
of
in IndisputableMonolith.Astrophysics.NucleosynthesisTiers
decl_use
-
rung
in IndisputableMonolith.Compat.Constants
decl_use
-
Constants
in IndisputableMonolith.CPM.LawOfExistence
decl_use
-
rung
in IndisputableMonolith.Engineering.AsteroidOreSpectroscopy
decl_use
-
of
in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization
decl_use
-
A
in IndisputableMonolith.Foundation.IntegrationGap
decl_use
-
of
in IndisputableMonolith.Foundation.PhiForcingDerived
decl_use
-
of
in IndisputableMonolith.Foundation.SpectralEmergence
decl_use
-
gap
in IndisputableMonolith.Gap45.Derivation
decl_use
-
Phase
in IndisputableMonolith.Information.ChurchTuringPhysicsStructure
decl_use
-
of
in IndisputableMonolith.Information.PhysicsComplexityStructure
decl_use
-
A
in IndisputableMonolith.Masses.Anchor
decl_use
-
Sector
in IndisputableMonolith.Masses.Anchor
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
-
M0
in IndisputableMonolith.Masses.RSBridge.Anchor
decl_use
-
rung
in IndisputableMonolith.Masses.RSBridge.Anchor
decl_use
-
Sector
in IndisputableMonolith.Masses.RSBridge.Anchor
decl_use
-
sectorOf
in IndisputableMonolith.Masses.RSBridge.Anchor
decl_use
-
ZOf
in IndisputableMonolith.Masses.RSBridge.Anchor
decl_use
-
Sector
in IndisputableMonolith.Masses.RungConstructor.Basic
decl_use
-
sectorOf
in IndisputableMonolith.Masses.RungConstructor.Basic
decl_use
-
Fermion
in IndisputableMonolith.Masses.SMVerification
decl_use
-
rs_mass_MeV
in IndisputableMonolith.Masses.Verification
decl_use
-
A
in IndisputableMonolith.Modal.Actualization
decl_use
-
RSBridge
in IndisputableMonolith.RecogSpec.RSBridge
decl_use
-
Phase
in IndisputableMonolith.RRF.Hypotheses.EightTick
decl_use
-
Fermion
in IndisputableMonolith.RSBridge.Anchor
decl_use
… and 7 more