module module

`IndisputableMonolith.Verification.AlphaCorrectionAnalysis`

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

depends on (5)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Constants.Alpha module_import
IndisputableMonolith.Constants.AlphaDerivation module_import
IndisputableMonolith.Constants.ExternalAnchors module_import
IndisputableMonolith.Numerics.Interval.AlphaBounds module_import

declarations in this module (12)

def required_correction L49
theorem correction_positive L53
theorem correction_window_from_current_bounds L59
theorem correction_positive_of_alphaInv_lt L69
def candidate_1 L81
def candidate_2 L86
def candidate_3 L92
def candidate_4 L97
theorem candidate_1_bounds L104
theorem candidate_2_value L148
structure CorrectionAnalysis L169
def analysis L183