IndisputableMonolith.Verification.GravityS2StrongFieldLikelihood

declarations in this module (14)

• def gravityS2FSPCentral L47
• def gravityS2FSPSigma L50
• def gravityS2RSTargetScale L53
• def gravityS2RSPredictedFSP L56
• def gravityS2Residual L59
• theorem gravityS2FSPSigma_pos L62
• theorem gravityS2RSTargetScale_pos L66
• theorem gravityS2_residual_lt_one_sigma L73
• theorem gravityS2_sigma_gt_rs_target L81
• theorem gravityS2_dataset_attachment_status L88
• structure GravityS2StrongFieldLikelihoodCert L96
• def gravityS2StrongFieldLikelihoodCert L108
• theorem gravityS2StrongFieldLikelihoodCert_inhabited L115
• theorem gravity_s2_strong_field_likelihood_one_statement L120