module module moderate

`IndisputableMonolith.Verification.EPTAPTALikelihood`

Packages EPTA DR2 pulsar-timing spectral-index numbers as a concrete falsifier attachment for the quantum-gravity register. Records the observed gamma central value and interval, the Recognition Science target, and the naive residual versus half-width. Short lemmas prove positivity, that the RS target sits below the observed band, and that the residual exceeds the half-width. Downstream likelihood aggregation imports these constants and status facts.

claimFix EPTA DR2 spectral-index data: central $\gamma$, bounds $\gamma_L,\gamma_U$, half-width $w$, RS target $\gamma_{\mathrm{RS}}>0$, and naive residual $r=|\gamma-\gamma_{\mathrm{RS}}|$. The module asserts $w>0$, the observed interval is positive, $\gamma_{\mathrm{RS}}$ lies strictly below that interval, and $r>w$, together with a dataset-attachment status flag for the falsifier register.

background

Pulsar timing arrays constrain a stochastic gravitational-wave background through the spectral index $\gamma$ of the timing-residual power spectrum. EPTA DR2 supplies a representative central value and uncertainty band used here as an external observational anchor.

In the Recognition Science verification stack, the quantum-gravity master plan §7 falsifier register needs named dataset attachments with numeric sensitivity records. The upstream module FalsifierRegisterDatasets states that role: attach concrete datasets to every register row (structural theorem, zero sorry).

This module is the EPTA-specific slice: gamma central/lower/upper/half-width, an RS-native target on the same observable, the naive residual, and comparison lemmas that turn those floats into proved inequalities usable by the likelihood layer.

proof idea

Mostly a definition module: numeric defs for the EPTA gamma band, half-width, RS target, and naive residual. The proved facts are short positivity and order lemmas (half-width positive, RS target positive, observed interval positive, RS target below the gamma interval, residual strictly larger than half-width) plus a dataset-attachment status constant. No deep tactic scripts; inequalities follow by unfolding the numeric defs and applying standard real arithmetic.

why it matters in Recognition Science

Feeds the parent module FalsifierLikelihoodRegister, which aggregates Sessions 107--115 into the dataset-specific likelihood/status layer over the §7 falsifier register (also a structural theorem, zero sorry). Without EPTA numbers and the residual-versus-width comparison, the register cannot mark this PTA channel as tension, agreement, or under-sensitivity. Sits in the verification domain rather than the T0--T8 forcing chain: it is empirical closure machinery, not a derivation of $\phi$, $D=3$, or the eight-tick octave.

scope and limits

Does not derive the EPTA gamma measurement from RS first principles.
Does not claim a full PTA likelihood function or covariance model.
Does not update or reanalyze raw EPTA DR2 timing residuals.
Does not prove RS correct; only records target-versus-data residual status.
Does not attach non-EPTA PTA datasets (NANOGrav, PPTA, IPTA).

used by (1)

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

IndisputableMonolith.Verification.FalsifierLikelihoodRegister module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Verification.FalsifierRegisterDatasets module_import

declarations in this module (16)

def eptaGammaCentral L52
def eptaGammaLower L55
def eptaGammaUpper L58
def eptaGammaHalfWidth L61
def eptaRSTarget L64
def eptaNaiveResidual L67
theorem eptaGammaHalfWidth_pos L69
theorem eptaRSTarget_pos L73
theorem epta_gamma_interval_positive L80
theorem epta_rs_target_below_gamma_interval L88
theorem epta_naive_residual_gt_half_width L94
theorem epta_dataset_attachment_status L102
structure EPTAPTALikelihoodCert L110
def eptaPTALikelihoodCert L123
theorem eptaPTALikelihoodCert_inhabited L130
theorem epta_pta_likelihood_one_statement L135