EHTM87StrongFieldLikelihoodCert
plain-language theorem explainer
Certificate bundle for the EHT M87* strong-field likelihood attachment: positive shadow (17%) and circularity (10%) sensitivities, positive RS target scale φ^{-44}, residuals below both sigmas, and the target strictly below both sensitivity floors, so the dataset is marked not currently sensitive. Verification and falsifier-register authors cite it when wiring the M87* row into the aggregate likelihood register. It is a pure structure of positivity and inequality fields; inhabitation is discharged by sibling lemmas elsewhere in the module.
Claim. A certificate packing eight facts about the EHT M87* strong-field attachment: the shadow fractional sensitivity $\sigma_{\mathrm{sh}}=0.17$ and circularity sensitivity $\sigma_{\mathrm{c}}=0.10$ are positive; the RS target scale $\tau$ (structurally $\varphi^{-44}$) is positive; the shadow and circularity residuals $|0-\tau|$ each lie strictly below their $\sigma$; $\tau$ itself lies strictly below both $\sigma_{\mathrm{sh}}$ and $\sigma_{\mathrm{c}}$ (not currently sensitive); and the dataset attachment has positive sensitivity, positive target scale, and $\mathrm{currentlySensitive}=\mathrm{false}$.
background
This module attaches a dataset-specific likelihood-style certificate to the §7 strong-field falsifier row, using the Event Horizon Telescope first image of M87*: ring diameter $42\pm 3,\mu\mathrm{as}$, circularity deviation $\le 10%$, and shadow-size consistency with Kerr at roughly the $17%$ level. The RS structural target is a tiny positive fractional deviation from pure GR/Kerr, represented by $\varphi^{-44}$ via the shared strong-field attachment.
Sibling defs fix the numerical floors: shadow fractional sigma $0.17$, circularity fractional sigma $0.10$, and target scale equal to strongFieldAttachment.rsTargetScale. Residuals are $|0-\tau|$ on each channel (central Kerr-consistent deviation taken as zero). Upstream predicates HasPositiveSensitivity and HasPositiveTargetScale require $0 < D.\mathrm{sensitivity}$ and a positive RS target on a DatasetAttachment.
The local claim is deliberately a consistency / non-sensitivity test: the target sits inside the quoted EHT scales, yet far below both floors, so the attachment is marked not currently sensitive. Status: structural theorem, zero sorry, zero new RS-internal axioms.
proof idea
No proof body: this is a structure (certificate type), not a theorem. Each field is a Prop recording positivity of the two EHT fractional sigmas and of the RS target, residual-below-sigma inequalities on shadow and circularity channels, target-below-sigma non-sensitivity on both channels, and the three-way dataset status conjunction.
Inhabitation is supplied downstream by ehtM87StrongFieldLikelihoodCert, which fills the fields from the sibling lemmas ehtM87ShadowFractionalSigma_pos, ehtM87CircularityFractionalSigma_pos, ehtM87RSTargetScale_pos, ehtM87_shadow_residual_lt_sigma, ehtM87_circularity_residual_lt_sigma, and the dataset-attachment status theorem. Nonempty then follows by packing that witness.
why it matters
Closes the EHT M87* third dataset-specific likelihood certificate for the strong-field falsifier row. Downstream, ehtM87StrongFieldLikelihoodCert inhabits the structure; ehtM87StrongFieldLikelihoodCert_inhabited exposes Nonempty; and eht_m87_strong_field_likelihood_one_statement flattens the residual, non-sensitivity, and attachment-status facts into a single conjunction.
The aggregate FalsifierLikelihoodRegisterCert consumes this (alongside OmegaLambda/Planck, Cassini, gravity-S2, and related rows) so the falsifier likelihood register can cite a uniform certificate shape per dataset. Framework role: honest non-sensitivity bookkeeping for a strong-field observable, not a mass or coupling derivation. The RS target $\varphi^{-44}$ is the structural scale under test; the certificate records that present EHT precision cannot yet resolve it. No open sorry remains in this module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.