theorem proved term proof

`bottom_down_equal_Z`

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

formal statement (Lean)

  70theorem bottom_down_equal_Z : ZOf .d = ZOf .b := by

proof body

Term-mode proof.

  71  obtain ⟨hd, _, hb⟩ := ZOf_down_quarks
  72  rw [hd, hb]
  73
  74/-! ## Generation rung spacing (proved directly from Integers definitions) -/
  75
  76open Integers in

depends on (14)

Lean names referenced from this declaration's body.

rung in IndisputableMonolith.Compat.Constants decl_use
rung in IndisputableMonolith.Engineering.AsteroidOreSpectroscopy decl_use
from in IndisputableMonolith.Foundation.PrimitiveDistinction decl_use
Generation in IndisputableMonolith.Foundation.SpectralEmergence decl_use
Generation in IndisputableMonolith.Foundation.UniversalForcing.BiologyRealization decl_use
rung in IndisputableMonolith.Masses.AnchorPolicy decl_use
ZOf_down_quarks in IndisputableMonolith.Masses.QuarkScoreCard decl_use
rung in IndisputableMonolith.Masses.RSBridge.Anchor decl_use
ZOf in IndisputableMonolith.Masses.RSBridge.Anchor decl_use
Generation in IndisputableMonolith.Physics.CKM decl_use
Generation in IndisputableMonolith.Physics.ThreeGenerations decl_use
Generation in IndisputableMonolith.RecogSpec.RSLedger decl_use
rung in IndisputableMonolith.RSBridge.Anchor decl_use
ZOf in IndisputableMonolith.RSBridge.Anchor decl_use