pith. machine review for the scientific record. sign in
theorem proved term proof

r_down_values

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)

  61theorem r_down_values : r_down "d" = 4 ∧ r_down "s" = 15 ∧ r_down "b" = 21 := by

proof body

Term-mode proof.

  62  simp only [r_down, tau, Anchor.E_passive, Anchor.W, passive_field_edges,
  63             cube_edges, active_edges_per_tick, D, wallpaper_groups]
  64  omega
  65
  66/-! ## Sector Parameter Verification
  67
  68The up-quark sector has B_pow = -1, r0 = 35.
  69Effective exponent: -5 + 35 + r = 30 + r.
  70Scale: 2^(-1) / 10^6 = 1 / (2 × 10^6).
  71
  72The down-quark sector has B_pow = 23, r0 = -5.
  73Effective exponent: -5 + (-5) + r = -10 + r.
  74Scale: 2^23 / 10^6 = 8388608 / 10^6. -/
  75

depends on (20)

Lean names referenced from this declaration's body.