structure
definition
AlphaPrecisionCert
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Constants.AlphaPrecision on GitHub at line 60.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
57
58/-! ## Certificate -/
59
60structure AlphaPrecisionCert where
61 seed_from_geometry : alpha_seed = 4 * Real.pi * 11
62 seed_positive : 0 < alpha_seed
63 curvature_positive : 0 < curvature_correction
64 gap_positive : ∀ w seed, 0 < w → 0 < seed → 0 < gap_correction w seed
65
66theorem alpha_precision_cert_exists : Nonempty AlphaPrecisionCert :=
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