def definition def or abbrev

`step_top_bottom`

show as: view Lean formalization →

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)

  77def step_top_bottom : ℚ := 31 / 4

proof body

Definition body.

  78
  79/-- Step from Bottom to Charm: 2.50 rungs. -/

used by (5)

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

hierarchy_coherence in IndisputableMonolith.Physics.Hierarchy decl_use
quark_hierarchy in IndisputableMonolith.Physics.Hierarchy decl_use
derived_parameters in IndisputableMonolith.Physics.ParticleSummary decl_use
res_bottom in IndisputableMonolith.Physics.QuarkMasses decl_use
residues_match_steps in IndisputableMonolith.Physics.QuarkMasses decl_use

depends on (1)

Lean names referenced from this declaration's body.

from in IndisputableMonolith.Foundation.PrimitiveDistinction decl_use