IndisputableMonolith.Verification.EPTAPTALikelihood
Module packaging EPTA DR2 pulsar-timing spectral-index numbers against the Recognition Science target for the nanohertz gravitational-wave background. It records the observed gamma interval, the RS prediction, the naive residual, and elementary positivity/ordering lemmas that certify the residual exceeds half-width. Downstream likelihood aggregation cites these constants when scoring the quantum-gravity falsifier register.
claimFix the EPTA DR2 representative spectral index $\gamma_{\mathrm{EPTA}}$ with central value, lower/upper bounds, and half-width $w$, together with the RS target $\gamma_{\mathrm{RS}}>0$. The module asserts $w>0$, that the observed interval lies in the positive reals, that $\gamma_{\mathrm{RS}}$ lies strictly below that interval, and that the naive residual $|\gamma_{\mathrm{EPTA}}-\gamma_{\mathrm{RS}}|$ exceeds $w$, plus a dataset-attachment status flag for the falsifier register.
background
Pulsar timing arrays constrain the spectral index of a stochastic nanohertz gravitational-wave background. EPTA DR2 supplies a representative central value and uncertainty band for that index. In the Recognition Science verification stack, each such observational band is attached as a named numerical record to a row of the quantum-gravity master-plan §7 falsifier register.
The parent dataset module states it "attaches concrete named datasets and numerical sensitivity records to every row" of that register, with structural-theorem status (zero sorry, zero RS-internal axiom). This module is the EPTA-specific slice: gamma central/lower/upper/half-width, an RS target on the same scale, and the residual that compares them.
Elementary lemmas then certify that the half-width and RS target are positive, that the reported gamma interval is positive, that the RS target sits below the interval, and that the residual exceeds half-width—facts needed before any likelihood score is formed.
proof idea
Definition-and-lemma module, not a single deep theorem. Numeric constants are introduced as plain definitions (central value, bounds, half-width, RS target, naive residual). Short positivity and comparison lemmas discharge the arithmetic inequalities by direct computation or rewriting against those constants. A final attachment-status declaration records how this dataset row sits in the falsifier register. No multi-step tactic scripts beyond unfolding and norm_num-style checks.
why it matters in Recognition Science
Feeds the Falsifier Likelihood Register, which "aggregates Sessions 107--115: the dataset-specific likelihood/status layer over the quantum-gravity master plan §7 falsifier register." Without a certified EPTA residual and interval geometry, that aggregator cannot score the PTA spectral-index falsifier row.
In the broader RS program this is observational hygiene, not a forcing-chain step: it does not derive $J$, $\varphi$, the eight-tick octave, or $D=3$. It only pins whether the RS nanohertz prediction sits inside or outside the EPTA DR2 band, so the register can mark pass, tension, or fail once likelihoods are combined.
scope and limits
- Does not derive the RS spectral-index target from the forcing chain or RCL.
- Does not reanalyze raw EPTA TOAs; only packages published representative numbers.
- Does not compute a full likelihood or posterior, only residual vs half-width facts.
- Does not claim tension with NANOGrav, PPTA, or IPTA bands.
- Does not address non-power-law or anisotropic GW background models.
used by (1)
depends on (1)
declarations in this module (16)
-
def
eptaGammaCentral -
def
eptaGammaLower -
def
eptaGammaUpper -
def
eptaGammaHalfWidth -
def
eptaRSTarget -
def
eptaNaiveResidual -
theorem
eptaGammaHalfWidth_pos -
theorem
eptaRSTarget_pos -
theorem
epta_gamma_interval_positive -
theorem
epta_rs_target_below_gamma_interval -
theorem
epta_naive_residual_gt_half_width -
theorem
epta_dataset_attachment_status -
structure
EPTAPTALikelihoodCert -
def
eptaPTALikelihoodCert -
theorem
eptaPTALikelihoodCert_inhabited -
theorem
epta_pta_likelihood_one_statement