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

alpha_precision_cert_exists

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)

  66theorem alpha_precision_cert_exists : Nonempty AlphaPrecisionCert :=

proof body

Term-mode proof.

  67  ⟨{ seed_from_geometry := alpha_seed_eq
  68     seed_positive := alpha_seed_positive
  69     curvature_positive := curvature_correction_positive
  70     gap_positive := gap_correction_positive }⟩
  71
  72end
  73
  74end IndisputableMonolith.Constants.AlphaPrecision

depends on (7)

Lean names referenced from this declaration's body.