IndisputableMonolith.Constants.PlanckScaleMatching

declarations in this module (35)

• def J L45
• theorem J_eq_Jcost L48
• theorem J_exp_eq_cosh L51
• def J_bit_val L60
• theorem J_bit_eq_cosh L63
• theorem J_bit_pos L71
• theorem J_bit_explicit L80
• theorem J_bit_eq_phi_minus L88
• theorem J_bit_bounds L102
• def cube_faces L113
• theorem Q3_faces L116
• def cube_vertices L119
• theorem Q3_vertices L122
• def J_curv L132
• theorem J_curv_zero L135
• theorem J_curv_nonneg L138
• def lambda_rec_from_Jbit L148
• theorem lambda_rec_from_Jbit_pos L151
• theorem extremum_condition L156
• theorem extremum_unique L163
• def solid_angle_per_octant L175
• def num_octants L178
• def total_solid_angle L181
• theorem octants_cover_sphere L184
• def ell_P L192
• theorem ell_P_pos L195
• def lambda_rec_SI L208
• theorem lambda_rec_SI_pos L211
• theorem lambda_rec_over_ell_P L223
• theorem one_over_sqrt_pi_approx L241
• theorem planck_gate_identity L251
• theorem planck_gate_normalized L260
• structure PlanckScaleMatchingCert L287
• def planck_scale_matching_cert L298
• def planck_scale_matching_report L305