IndisputableMonolith.Verification.DarkEnergyWPlanckLikelihood

declarations in this module (14)

• def planckW0Central L50
• def planckW0Sigma L53
• def rsW0Baseline L56
• def rsW1DeviationTarget L59
• def darkEnergyWResidual L62
• theorem planckW0Sigma_pos L65
• theorem rsW1DeviationTarget_pos L69
• theorem darkEnergyW_residual_le_one_sigma L77
• theorem darkEnergyW_sigma_gt_rs_z1_target L84
• theorem darkEnergyW_dataset_attachment_status L91
• structure DarkEnergyWPlanckLikelihoodCert L99
• def darkEnergyWPlanckLikelihoodCert L111
• theorem darkEnergyWPlanckLikelihoodCert_inhabited L118
• theorem dark_energy_w_planck_likelihood_one_statement L123