IndisputableMonolith.Verification.EHTM87StrongFieldLikelihood

declarations in this module (19)

• def ehtM87RingDiameterCentralMicroas L47
• def ehtM87RingDiameterSigmaMicroas L50
• def ehtM87ShadowFractionalSigma L53
• def ehtM87CircularityFractionalSigma L56
• def ehtM87RSTargetScale L59
• def ehtM87ShadowResidual L62
• def ehtM87CircularityResidual L66
• theorem ehtM87ShadowFractionalSigma_pos L69
• theorem ehtM87CircularityFractionalSigma_pos L73
• theorem ehtM87RSTargetScale_pos L78
• theorem ehtM87_shadow_residual_lt_sigma L85
• theorem ehtM87_circularity_residual_lt_sigma L92
• theorem ehtM87_shadow_sigma_gt_rs_target L99
• theorem ehtM87_circularity_sigma_gt_rs_target L105
• theorem ehtM87_dataset_attachment_status L112
• structure EHTM87StrongFieldLikelihoodCert L120
• def ehtM87StrongFieldLikelihoodCert L137
• theorem ehtM87StrongFieldLikelihoodCert_inhabited L147
• theorem eht_m87_strong_field_likelihood_one_statement L152