Encyclopedia Cosmology Cosmology Ptastochastic Gwstructural Rs Pta Phi Signature Pos

ARTICLE 3 claims 1 theorem 1 model

Cosmology Ptastochastic Gwstructural Rs Pta Phi Signature Pos

A machine-checked proof establishes that one number is positive, a small but exact step in a much larger, unfinished search for gravitational waves from the early universe.

The structural signature

Pulsar timing arrays like NANOGrav and EPTA listen for a faint background hum of gravitational waves, ripples in spacetime that could carry information from the universe's first moments. One proposed source is a chaotic, primordial process rather than a single dramatic event. The Recognition Science framework has a specific idea about the shape of that hum, and a machine-checked library of formal proofs now contains a proof of one small but exact piece of it.

The piece is a number. The framework's model of the early universe produces a characteristic phase delay for each rung of its structure, and that delay is the natural logarithm of the golden ratio, about 0.481. The declaration rs_pta_phi_signature_pos establishes that this number is strictly greater than zero. The proof itself is a simple real-number inequality: since the golden ratio is greater than one, its logarithm is positive.

Why does positivity matter? Standard inflationary cosmology predicts a nearly flat spectrum for these primordial gravitational waves, with a tilt very close to zero. The framework's signature, at about 0.481, is not just positive but orders of magnitude larger. This structural difference is the entire content of the declaration: it establishes a clean, formal distinction between the two predictions, without yet claiming that either one matches the data.

In Recognition Science, this declaration is a ledger, a discrete record of events, entry. It retires one of five open hypotheses in the framework's larger conditional master proof, a step toward a unified derivation. But the empirical work is untouched. The declaration says nothing about whether NANOGrav or EPTA data actually show this signature. That comparison remains a separate, future obligation.

The practical consequence is a sharper target. Astronomers know what a slow-roll inflation background looks like: nearly flat. The framework now has a formal, machine-checked statement of what its own alternative looks like: a specific, positive, much larger tilt. The next step is to point a telescope, or rather a timing array, at that difference.

THEOREM rs_pta_phi_signature_pos · IndisputableMonolith/Cosmology/PTAStochasticGWStructural.lean
theorem rs_pta_phi_signature_pos : 0 < rs_pta_phi_signature := by
  unfold rs_pta_phi_signature
  exact Real.log_pos one_lt_phi
MODEL rs_pta_distinct_inflation_prop · IndisputableMonolith/Cosmology/PTAStochasticGWStructural.lean
/-- The structural discriminator proposition: the RS PTA signature is
strictly positive, distinct from the inflationary slow-roll prediction
of approximately zero. -/
def rs_pta_distinct_inflation_prop : Prop :=
  0 < rs_pta_phi_signature

What this page does not claim

The declaration does not prove any empirical match with NANOGrav or EPTA data. It does not derive the full spectral shape of the gravitational wave background. It does not claim that the inflationary prediction is wrong, only that it is structurally distinct.

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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND