module module

`IndisputableMonolith.Constants.AlphaGenesis.MeasurementVerdict`

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

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Constants.AlphaGenesis module_import

depends on (5)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants.AlphaGenesis.LoopCertificate module_import
IndisputableMonolith.Constants.AlphaGenesis.ResidualTarget module_import
IndisputableMonolith.Constants.ExternalAnchors module_import
IndisputableMonolith.Numerics.Interval.AlphaBounds module_import
IndisputableMonolith.Numerics.Interval.W8Bounds module_import

declarations in this module (15)

def exp_taylor_12_at_048122 L39
def exp_error_12_at_048122 L44
lemma exp_048122_taylor_floor L48
lemma exp_048122_gt L53
theorem log_phi_lt_048122 L98
def exp_taylor_12_at_neg_0086705 L104
def exp_error_12_at_neg_0086705 L109
lemma exp_neg_0086705_taylor_floor L113
lemma exp_neg_0086705_gt L119
theorem exponentialLoad_lt_0086705 L166
theorem alphaInvGenesis_exceeds_CODATA_by_0007 L192
theorem alpha_inv_uncertainty_eq L223
theorem margin_0007_gt_30000_sigma L227
structure MeasurementVerdictCert L233
def measurementVerdictCert L238