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

r0_eq_alt

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)

  88theorem r0_eq_alt (s : Anchor.Sector) : Anchor.r0 s = r0_alt s := by

proof body

Term-mode proof.

  89  cases s <;> simp only [Anchor.r0, r0_alt, Anchor.W, Anchor.E_total, Anchor.A,
  90    wallpaper_groups, cube_edges, active_edges_per_tick, D, Wz, Etz, Az]
  91  all_goals norm_num
  92
  93/-! ## Summary
  94
  95The theorems above prove that:
  961. B_pow and r0 in Anchor.lean are definitionally equal to the formulas
  97   derived from cube geometry and crystallography.
  982. No hardcoded magic numbers exist—all values trace to:
  99   - D = 3 (dimension)
 100   - cube_edges(3) = 12
 101   - passive_field_edges(3) = 11
 102   - wallpaper_groups = 17
 103   - active_edges_per_tick = 1
 104
 105This constitutes a formal proof that the sector constants are parameter-free.
 106-/
 107
 108end AnchorDerivation
 109end Masses
 110end IndisputableMonolith

depends on (30)

Lean names referenced from this declaration's body.