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

gap_weight_unique

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)

  47theorem gap_weight_unique :
  48  ∃! w : ℝ, w = w8_from_eight_tick := by

proof body

Term-mode proof.

  49  use w8_from_eight_tick
  50  constructor
  51  · rfl
  52  · intro y hy; exact hy
  53
  54/-- The gap weight is positive (derived from the closed form). -/

depends on (10)

Lean names referenced from this declaration's body.