IndisputableMonolith.Verification.AlphaResolutionPass2

declarations in this module (18)

• def deltaAlphaInv_required L31
• def deltaAlphaInv_geometric L37
• theorem deltaAlphaInv_geometric_eq_required L42
• def alphaInv_corrected L47
• theorem alphaInv_corrected_eq_CODATA L51
• theorem additive_closure_unique_for_exact_alignment L58
• theorem exists_unique_exact_alignment_closure L71
• def deltaAlphaInv_ppm L79
• theorem deltaAlphaInv_ppm_eq_mismatch L83
• theorem corrected_residual_zero L88
• theorem corrected_in_CODATA_3sigma L94
• theorem curvature_exponent_forced_in_power_family L103
• theorem curvature_denominator_forced_at_pi5 L110
• theorem curvature_numerator_forced_at_pi5 L116
• theorem curvature_tuple_uniqueness_bundle_for_delta_kappa L122
• theorem curvature_structural_tuple_uniqueness_bundle_for_delta_kappa L134
• def closure_term_derived_from_geometry L152
• theorem closure_status L155