IndisputableMonolith.Gravity.FullEFEWithDarkEnergy

declarations in this module (20)

• def covDeriv02 L54
• theorem covDeriv02_smul L64
• theorem minkowski_metric_compatible L83
• theorem vacuum_stress_conserved L97
• theorem flat_vacuum_stress_conserved L111
• theorem Omega_Lambda_RS_pos L123
• def Lambda_RS L129
• theorem Lambda_RS_pos L133
• theorem Lambda_RS_zero L138
• def rho_vac L141
• theorem rho_vac_pos L143
• def vacuum_pressure L147
• theorem vacuum_eos L150
• def rs_efe_data_with_lambda L158
• theorem lambda_efe_kappa L165
• theorem lambda_efe_dimension L168
• theorem lambda_efe_lambda_pos L171
• theorem recovers_baseline_lambda L175
• structure DarkEnergyEFECert L186
• def darkEnergyEFECert L202