Pith. sign in
module module moderate

IndisputableMonolith.Verification.EHTM87StrongFieldLikelihood

show as:
view Lean formalization →

Dataset and residual layer for EHT M87* strong-field checks: ring diameter, shadow and circularity fractional sigmas, RS target scale, and residual-versus-sigma inequalities. Verification and gravity-track authors cite it when wiring M87* into the §7 falsifier likelihood register. Content is mostly named constants plus short positivity and residual bounds.

claimFix the EHT M87* ring-diameter central value and uncertainty (microarcseconds), shadow and circularity fractional sigmas, and an RS target scale. Define shadow and circularity residuals relative to that scale, and record that both residuals lie strictly below their fractional sigmas (with positivity of the scale and sigmas).

background

Track 6.C of the quantum-gravity master plan treats strong-field structural discriminators: observables that can separate Recognition Science gravity predictions from GR baselines without committing to a full dynamical simulation stack. The upstream module StrongFieldStructural closes that structural form (0 sorry, 0 RS-internal axiom).

This module attaches the concrete EHT M87* numbers used in that track: ring diameter in microarcseconds, fractional uncertainties for shadow size and circularity, and an RS-native target scale against which residuals are measured. It sits beside FalsifierRegisterDatasets, which binds named datasets and sensitivity records to every row of the master-plan §7 falsifier register.

Notation is observational: central value and $\sigma$ in $\mu\mathrm{as}$, dimensionless fractional sigmas, and residual $= |\mathrm{data}-\mathrm{RS\ target}|$ style comparisons used later as likelihood inputs.

proof idea

Definition-heavy module. Named defs pin the published EHT M87* ring diameter, its uncertainty, shadow/circularity fractional sigmas, and the RS target scale. Residual defs are arithmetic comparisons to that scale. The proved facts are short positivity lemmas (sigmas and scale $> 0$) and two residual bounds (shadow and circularity residual strictly less than the corresponding fractional sigma), each a direct numerical inequality rather than a deep derivation.

why it matters in Recognition Science

Feeds FalsifierLikelihoodRegister, which aggregates Sessions 107--115 into the dataset-specific likelihood/status layer over the quantum-gravity master plan §7 falsifier register. Without pinned M87* numbers and residual-versus-sigma facts, the strong-field row cannot be scored as pass/fail or likelihood-weighted against other falsifiers.

In the broader RS program this is verification infrastructure for Track 6.C, not a derivation of $D=3$, $\varphi$, or the forcing chain. It closes the observational attachment so structural strong-field claims can be audited against a real EHT target rather than a placeholder.

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)