IndisputableMonolith.Cosmology.OmegaLambdaDerivation

declarations in this module (24)

• def N_modes_total L70
• def N_modes_saturated L73
• def tick_addressing L76
• def omega_raw L79
• theorem omega_raw_eq L82
• theorem omega_raw_val L87
• def em_correction L99
• theorem em_correction_small L103
• theorem em_correction_pos2 L115
• def omega_lambda L128
• theorem omega_lambda_lt_686 L131
• theorem omega_lambda_gt_683 L138
• theorem omega_lambda_interval L145
• def omega_lambda_planck2018 L149
• def omega_lambda_planck_err L152
• theorem rs_consistent_with_planck L156
• def gray_code_flip_counts L172
• theorem gray_flip_total L175
• theorem q3_mode_count L178
• theorem tick_addressing_is_power2 L181
• theorem omega_lambda_one_measured_input L195
• theorem omega_lambda_canonical_form L202
• structure OmegaLambdaCert L210
• theorem omegaLambdaCert L223