IndisputableMonolith.Unification.ConstantsPredictionsProved

declarations in this module (16)

• theorem alpha_positive L34
• theorem alpha_lt_0_1 L39
• theorem alpha_bounds L94
• theorem c_eq_one L102
• theorem c_positive L105
• theorem boltzmann_analog_formula L112
• theorem boltzmann_analog_positive L116
• theorem boltzmann_analog_lt_half L121
• theorem boltzmann_analog_bounds L161
• theorem phi_inverse_formula L169
• theorem phi_plus_inverse_eq_sqrt5 L176
• theorem phi_sq_gt_2_5 L192
• theorem phi_sq_lt_2_7 L199
• structure ConstantsPredictionsCert L216
• theorem constants_predictions_cert_exists L228
• theorem constants_calculated_proofs_summary L247