theorem proved decidable or rfl

`down_generation_spacing`

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

formal statement (Lean)

  82theorem down_generation_spacing :
  83    r_down "s" - r_down "d" = 11 ∧ r_down "b" - r_down "d" = 17 := by

proof body

Decided by rfl or decide.

  84  decide
  85
  86/-! ## Structural ratios that already match PDG order of magnitude
  87
  88These are theorems in `Masses.Verification`. We re-export them under
  89explicit row IDs so the scorecard can be read at a glance.
  90-/
  91
  92/-- P0-Q structural row: m_c / m_u = φ^11 (proved). -/

used by (2)

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

down_generation_spacing in IndisputableMonolith.Masses.QuarkVerification decl_use
quark_verification_cert_exists in IndisputableMonolith.Masses.QuarkVerification decl_use

depends on (10)

Lean names referenced from this declaration's body.

of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
of in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization decl_use
of in IndisputableMonolith.Foundation.PhiForcingDerived decl_use
of in IndisputableMonolith.Foundation.SpectralEmergence decl_use
of in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use
r_down in IndisputableMonolith.Masses.Anchor decl_use
r_down in IndisputableMonolith.Masses.AnchorPolicy decl_use
down_generation_spacing in IndisputableMonolith.Masses.QuarkVerification decl_use
that in IndisputableMonolith.NumberTheory.PhiLadderLattice decl_use
row in IndisputableMonolith.YM.Dobrushin decl_use