Pith. sign in
module module moderate

IndisputableMonolith.Gravity.PTAStructural

show as:
view Lean formalization →

Structural module fixing the Recognition Science stochastic PTA gravitational-wave signature at the rung-44 φ-ladder scale, and proving it is positive, lies in a stated observable band, and is distinct from the zero and inflationary baselines. Gravity and QG-falsifier authors cite it when wiring PTA channels into the master theorem. The argument is arithmetic comparison of φ-powers against fixed numerical bands and baseline constants.

claimAt rung $44$ on the $\varphi$-ladder the module fixes an RS PTA stochastic-background signature $S_{\mathrm{PTA}}$, an observable band $B_{\mathrm{PTA}}$, and an inflationary PTA baseline family $I_{\mathrm{PTA}}$, and records $S_{\mathrm{PTA}}>0$, $S_{\mathrm{PTA}}\in B_{\mathrm{PTA}}$, $S_{\mathrm{PTA}}\neq 0$, and $I_{\mathrm{PTA}}\notin B_{\mathrm{PTA}}$.

background

Pulsar timing arrays constrain a nanohertz stochastic gravitational-wave background. In Recognition Science the same background is read as a discrete rung on the φ-ladder rather than a continuous inflationary spectrum. The module sits in the Gravity domain and imports the RS constants (including the native time quantum), the baryon/φ-rung ladder arithmetic from Cosmology.PhiRungLadder, and the conditional Gravity MasterTheorem surface.

The ladder supplies the discrete scale at which the PTA signature is evaluated: rung 44. Sibling declarations name a positive RS stochastic φ-signature, a zero inflationary stochastic baseline, an observable numerical band for the RS prediction, and an inflationary PTA family baseline. The local claim is structural distinguishability: the RS value is nonzero, sits inside the RS band, and the inflationary family does not.

proof idea

Definition-plus-comparison module, not a deep analytic derivation. It introduces the RS PTA stochastic φ-signature at rung 44, the zero inflation baseline, and the RS observable band as concrete constants or φ-ladder expressions. Positivity and inequality lemmas then show the RS signature is strictly positive and unequal to the inflation-zero baseline. Separate facts place the RS signature inside the observable band and place the inflationary PTA family outside that band. A packaged witness and a proposition-level distinctness statement bundle those comparisons for downstream import. No differential equation or waveform integral is solved here; the work is arithmetic and band membership.

why it matters in Recognition Science

PTA is one of the typed observational channels on the quantum-gravity falsifier surface. Downstream, QGObservableSignalModels installs per-channel signal models with an observable, an RS prediction or band, and a classical/alternative baseline; this module supplies the PTA stochastic half of that pair. MasterTheoremUnconditional imports it when discharging inputs that the older conditional master theorem took as hypotheses, so the PTA distinctness witness becomes part of the zero-argument closure route.

Within the framework landmarks this is a gravity-track observable consequence of the φ-ladder (T6 self-similarity and the discrete rung structure), not a re-derivation of J-uniqueness or D=3. It turns the rung-44 scale into a referee-checkable separation between RS and inflationary PTA stochastic backgrounds.

scope and limits

used by (2)

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

depends on (3)

Lean names referenced from this declaration's body.

declarations in this module (18)