IndisputableMonolith.Cosmology.DarkEnergyWofZStructural

declarations in this module (30)

• def w_LCDM_value L78
• theorem w_LCDM_value_eq_neg_one L80
• def phi_neg_44 L87
• theorem phi_neg_44_pos L89
• def w_RS_linear L112
• theorem w_RS_linear_at_zero L115
• theorem w_RS_linear_eq_LCDM_at_zero L119
• theorem w_RS_linear_distinct_from_LCDM_at_positive_z L127
• theorem w_RS_linear_distinct_from_LCDM_abs L135
• theorem w_RS_linear_deviation_magnitude L143
• def falsifierThreshold L151
• theorem falsifierThreshold_pos L155
• theorem w_RS_linear_abs_deviation_eq_threshold L162
• theorem LCDM_abs_deviation_from_w_RS_linear_eq_threshold L170
• theorem measured_near_LCDM_not_RS_linear L181
• theorem exact_LCDM_measurement_not_RS_linear L193
• def redshift_half L201
• def redshift_one L204
• theorem redshift_half_pos L206
• theorem redshift_one_pos L210
• theorem w_RS_linear_at_redshift_half L215
• theorem w_RS_linear_at_redshift_one L221
• theorem falsifierThreshold_at_redshift_half L227
• theorem falsifierThreshold_at_redshift_one L233
• theorem named_redshift_falsifier_bands L239
• theorem falsifier_band_at_redshift L255
• structure DarkEnergyWofZStructuralCert L267
• def darkEnergyWofZStructuralCert L292
• theorem darkEnergyWofZStructuralCert_inhabited L305
• theorem dark_energy_w_of_z_one_statement L323