theorem proved decidable or rfl

`up_generation_spacing`

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

formal statement (Lean)

  77theorem up_generation_spacing :
  78    r_up "c" - r_up "u" = 11 ∧ r_up "t" - r_up "u" = 17 := by

Decided by rfl or decide.

  79  decide
  80
  81open Integers in

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

quark_verification_cert_exists in IndisputableMonolith.Masses.QuarkVerification decl_use
up_generation_spacing in IndisputableMonolith.Masses.QuarkVerification decl_use

Lean names referenced from this declaration's body.

r_up in IndisputableMonolith.Masses.Anchor decl_use
r_up in IndisputableMonolith.Masses.AnchorPolicy decl_use
up_generation_spacing in IndisputableMonolith.Masses.QuarkVerification decl_use