IndisputableMonolith.Foundation.SIBridgeClosure

declarations in this module (33)

• def c_SI L90
• def hbar_SI L94
• def G_SI L98
• theorem c_SI_pos L100
• theorem hbar_SI_pos L101
• theorem G_SI_pos L102
• def c_RS L107
• def hbar_RS L111
• def G_RS L115
• theorem c_RS_pos L117
• theorem phi_pow_5_pos L119
• theorem hbar_RS_pos L121
• theorem G_RS_pos L125
• theorem hbar_RS_mul_G_RS L130
• structure SIBridge L142
• def c_constraint L155
• def hbar_constraint L159
• def G_constraint L164
• def IsClosedBridge L168
• theorem aL_eq_of_c_constraint L174
• theorem aM_aT_eq_of_c_hbar L186
• theorem aT_aM_eq_of_c_G L209
• theorem a_T_sq_eq L238
• def tau_Planck L277
• theorem tau_Planck_pos L279
• theorem a_T_eq L287
• theorem tau0_eq_sqrt_pi_planck_time L295
• def tau0_predicted_seconds L308
• theorem tau0_predicted_seconds_pos L310
• theorem si_bridge_closed_under_three_constraints L317
• structure SIBridgeClosureCert L335
• def siBridgeClosureCert L350
• theorem siBridgeClosureCert_inhabited L357