theorem proved term proof

`r_up_values`

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

formal statement (Lean)

  56theorem r_up_values : r_up "u" = 4 ∧ r_up "c" = 15 ∧ r_up "t" = 21 := by

proof body

Term-mode proof.

  57  simp only [r_up, tau, Anchor.E_passive, Anchor.W, passive_field_edges,
  58             cube_edges, active_edges_per_tick, D, wallpaper_groups]
  59  omega
  60

depends on (13)

Lean names referenced from this declaration's body.

active_edges_per_tick in IndisputableMonolith.Constants.AlphaDerivation decl_use
cube_edges in IndisputableMonolith.Constants.AlphaDerivation decl_use
passive_field_edges in IndisputableMonolith.Constants.AlphaDerivation decl_use
wallpaper_groups in IndisputableMonolith.Constants.AlphaDerivation decl_use
wallpaper_groups in IndisputableMonolith.Constants.AlphaHigherOrder decl_use
E_passive in IndisputableMonolith.Masses.Anchor decl_use
r_up in IndisputableMonolith.Masses.Anchor decl_use
tau in IndisputableMonolith.Masses.Anchor decl_use
W in IndisputableMonolith.Masses.Anchor decl_use
r_up in IndisputableMonolith.Masses.AnchorPolicy decl_use
W in IndisputableMonolith.Physics.LeptonGenerations.TauStepDerivation decl_use
E_passive in IndisputableMonolith.Physics.MassTopology decl_use
W in IndisputableMonolith.Physics.MassTopology decl_use