Pith. sign in
module module high

IndisputableMonolith.Verification.EHTM87StrongFieldLikelihood

show as:
view Lean formalization →

Dataset and residual layer for EHT M87* strong-field checks against Recognition Science targets. It records the measured ring diameter in microarcseconds, fractional sigmas for shadow size and circularity, the RS target scale, and short proved residual-within-sigma inequalities. Downstream likelihood registers import these constants when scoring Track 6.C falsifiers. Content is numeric definitions plus positivity and comparison lemmas.

claimRecords the EHT M87* ring-diameter central value $d_{\mathrm{M87}}$ and uncertainty $\sigma_d$ (microarcseconds), fractional shadow and circularity sigmas $\sigma_{\mathrm{sh}},\sigma_{\mathrm{circ}}$, RS target scale $s_{\mathrm{RS}}>0$, residuals $r_{\mathrm{sh}},r_{\mathrm{circ}}$, and proves $r_{\mathrm{sh}}<\sigma_{\mathrm{sh}}$ and $r_{\mathrm{circ}}<\sigma_{\mathrm{circ}}$.

background

Track 6.C of the quantum-gravity master plan is the strong-field structural discriminator: compare Recognition Science geometric targets to horizon-scale imaging observables without introducing RS-internal axioms. The upstream StrongFieldStructural module states that status as a closed structural theorem (0 sorry).

FalsifierRegisterDatasets attaches named observational datasets and sensitivity records to every row of the master-plan §7 falsifier register. This module is the M87*-specific attachment: EHT ring-diameter central value and sigma in microarcseconds, fractional sigmas for shadow diameter and circularity, and an RS target scale used to form residuals.

Sibling declarations also prove positivity of the fractional sigmas and target scale, then that each residual lies strictly inside its assigned sigma. Those inequalities are the local pass/fail witnesses consumed by the likelihood layer.

proof idea

Definition-heavy module, not a single deep theorem. Numeric defs fix the EHT M87* ring diameter, its uncertainty, fractional shadow and circularity sigmas, the RS target scale, and the two residuals. Short lemma proofs discharge positivity of the sigmas and target, then residual-strictly-less-than-sigma comparisons by unfolding the constants and applying ordinary real arithmetic. No tactic search beyond that; the scientific content is the pinned dataset and the residual inequalities.

why it matters in Recognition Science

Feeds IndisputableMonolith.Verification.FalsifierLikelihoodRegister, which aggregates Sessions 107--115 as the dataset-specific likelihood and status layer over the quantum-gravity master plan §7 falsifier register. Without these M87* numbers and residual lemmas, the strong-field Track 6.C row cannot be scored against EHT shadow size and circularity. Closes the observational attachment side of the structural strong-field discriminator (upstream StrongFieldStructural) for the M87* target, keeping the falsifier path concrete and machine-checkable.

scope and limits

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (19)