Cosmology Ptastochastic Gwstructural Pta Stochastic Gw One Statement

The structural discriminator

Pulsar timing arrays like NANOGrav and EPTA search for a stochastic gravitational-wave background, a faint sea of ripples in spacetime from many distant sources. Standard slow-roll inflation, the leading theory of the early universe, predicts that this background's spectrum is nearly flat, with a tensor tilt n_t close to zero. The Recognition Science framework's ledger, a discrete record of recognition events, predicts a different signature: a per-rung phase delay of log φ ≈ 0.481, where φ is the golden ratio.

The theorem pta_stochastic_gw_one_statement establishes a purely structural discriminator. It proves that this framework signature is strictly positive, 0 < log φ, and therefore distinct from the inflationary prediction of approximately zero. The proof is a simple real-number inequality, following from the fact that φ > 1. This is the extent of the theorem's reach: it shows the two predictions are mathematically different, not that one matches observations.

The declaration also provides a formal witness that satisfies one hypothesis in the framework's master theorem for quantum gravity. This retires that hypothesis from the conditional list, meaning the master theorem now has one fewer unproven assumption. The witness is a machine-checked object, but it only certifies the algebraic inequality, not any physical claim about the cosmos.

In Recognition Science, this is a step toward a full prediction. The specific spectral shape of the background from the φ-rung primordial structure remains future work. The empirical match against NANOGrav or EPTA datasets is a separate obligation, not yet met. The theorem's value is narrow but solid: it proves the framework's prediction is not trivially identical to the standard one.

theorem rs_pta_phi_signature_pos : 0 < rs_pta_phi_signature := by
  unfold rs_pta_phi_signature
  exact Real.log_pos one_lt_phi

/-- **TRACK 6.B ONE-STATEMENT** (structural form). The RS PTA spectral
signature `log φ` is strictly positive, distinct from the inflationary
slow-roll prediction `n_t ≈ 0`. The master theorem hypothesis input
`PTAStochasticGWDistinctFromInflation` is inhabited by
`ptaDistinctFromInflationWitness`. Empirical match against NANOGrav /
EPTA datasets remains a separate falsifier-register obligation. -/
theorem pta_stochastic_gw_one_statement :
    (0 < rs_pta_phi_signature) ∧
    (rs_pta_distinct_inflation_prop) ∧
    (Nonempty Gravity.MasterTheorem.PTAStochasticGWDistinctFromInflation) :=
  ⟨rs_pta_phi_signature_pos,
   rs_pta_distinct_inflation_prop_holds,
   ⟨ptaDistinctFromInflationWitness⟩⟩

theorem rs_pta_distinct_inflation_prop_holds :
    rs_pta_distinct_inflation_prop :=
  rs_pta_phi_signature_pos

/-- **Inhabitant for the master theorem hypothesis input**
`PTAStochasticGWDistinctFromInflation` (from `Gravity.MasterTheorem`,
Session 97). This witness retires the PTA hypothesis from the conditional
master theorem `rs_quantum_gravity_master_conditional`. -/
def ptaDistinctFromInflationWitness :
    Gravity.MasterTheorem.PTAStochasticGWDistinctFromInflation where
  rs_pta_distinct_inflation := rs_pta_distinct_inflation_prop
  holds := rs_pta_distinct_inflation_prop_holds

What this page does not claim

The theorem does not claim any empirical match to pulsar-timing-array data. The theorem does not derive the full spectral shape of the gravitational-wave background. The theorem does not prove that the inflationary prediction is wrong, only that it is different from the framework's.

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/Cosmology/PTAStochasticGWStructural.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: