Verification Eptaptalikelihood

The EPTA check

Pulsar timing arrays are galactic-scale detectors. By timing the radio pulses of many millisecond pulsars, astronomers look for a common signal, a stochastic gravitational-wave background, that would shift all the pulses together. The European Pulsar Timing Array's second data release (EPTA DR2) reported a spectral index for this background of about 3.83, with an asymmetric uncertainty that puts the value roughly between 3.11 and 4.65.

In Recognition Science, a ledger, a discrete record of recognition events, carries a structural prediction for this same background. The framework's target scale, expressed as log φ ≈ 0.481, is a positive number. The EPTA measurement interval is also entirely positive, which is the sign-level agreement the framework can currently claim.

The module EPTAPTALikelihood in the machine-checked library of formal theorems proves a scope-control record, not an empirical confirmation. Its central theorem, epta_pta_likelihood_one_statement, establishes five facts together: the EPTA interval is positive and ordered, the structural target is positive, the target lies below the EPTA interval, the naive residual between the central values exceeds the interval's half-width, and the dataset attachment is explicitly marked as not currently sensitive.

The plain-language meaning is a careful non-match. The structural target log φ ≈ 0.481 is about 3.35, which falls below the EPTA lower bound of 3.11. A naive comparison would therefore fail. The module proves this is not a falsification of the framework, because the dynamic RS prediction for the pulsar timing array spectral index is not yet formalized. The comparison is recorded as a dataset-accounting fact, with the mismatch stated honestly rather than smoothed over.

/-- EPTA DR2 representative spectral-index central value. -/
def eptaGammaCentral : ℝ := 3.83

theorem eptaRSTarget_pos : 0 < eptaRSTarget := by
  unfold eptaRSTarget ptaAttachment
  norm_num

/-- The RS structural target is below the EPTA `γ` interval. A naive
magnitude comparison would therefore fail. This is a scope-control
theorem, not a falsification theorem. -/
theorem epta_rs_target_below_gamma_interval :
    eptaRSTarget < eptaGammaLower := by
  unfold eptaRSTarget ptaAttachment eptaGammaLower
  norm_num

/-- The naive residual is larger than the half-width. -/
theorem epta_naive_residual_gt_half_width :
    eptaGammaHalfWidth < eptaNaiveResidual := by
  unfold eptaNaiveResidual eptaGammaCentral eptaRSTarget ptaAttachment
    eptaGammaHalfWidth eptaGammaUpper eptaGammaLower
  norm_num

/-- PTA dataset attachment is present, positive, and explicitly marked
not currently sensitive. -/
theorem epta_dataset_attachment_status :
    HasPositiveSensitivity ptaAttachment ∧
    HasPositiveTargetScale ptaAttachment ∧
    ptaAttachment.currentlySensitive = false :=
  ⟨pta_sensitivity_pos, pta_target_pos, rfl⟩

What this page does not claim

This module does not empirically confirm the RS structural prediction. The naive non-match is not a falsification of the framework. EPTA's γ is not the same physical parameter as the structural RS placeholder log φ.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Verification/EPTAPTALikelihood.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: