Pith. sign in
module module moderate

IndisputableMonolith.Cosmology.GravitationalWaveBackground3

show as:
view Lean formalization →

Defines the third RS packaging of a stochastic gravitational-wave background (SGWB) certificate: a nonnegative domain cost on a scale variable, a positive canonical threshold, and an inhabited certificate record. Cosmologists working in the Recognition ladder would cite it when tying GW background claims to the J-cost infrastructure. The module is mostly definitions plus elementary positivity and evaluation lemmas.

claimOn a real scale variable, a domain cost $C$ is introduced with $C\ge 0$ and an evaluation identity at a distinguished point; a canonical threshold $\theta>0$ is fixed; and an inhabited certificate record $\mathrm{SGWB3Cert}$ packages these data for the third SGWB formulation.

background

Recognition Science routes continuum claims through the J-cost $J(x)=(x+x^{-1})/2-1$ and the constants module (tick $\tau_0$, $\phi$-ladder units). Cosmology modules specialize that cost language to observable backgrounds rather than particle masses.

This file sits in the cosmology domain and imports only Constants and Cost. Sibling names indicate a local cost on a domain (scale or frequency proxy), its nonnegativity, a pointwise evaluation lemma, and a strictly positive canonical threshold used as a pass/fail cut for a stochastic GW background claim.

The certificate bundle SGWB3Cert is the module's public face: an inhabited record that freezes the cost, the threshold, and the elementary inequalities so downstream cosmology statements can assume a single named witness rather than re-proving positivity.

proof idea

Definition-first module. domainCost and canonicalThreshold are introduced as defs; domainCost_nonneg and canonicalThreshold_pos are short positivity arguments from the Cost import and arithmetic. domainCost_at_eq is an evaluation identity. SGWB3Cert / cert package the data; cert_inhabited supplies a concrete witness. No deep tactic development: structure is definitions plus elementary lemmas.

why it matters in Recognition Science

Gives cosmology a third, certificate-shaped handle on the stochastic gravitational-wave background inside the RS cost language, parallel to mass-ladder and coupling certificates elsewhere in the monolith. With no recorded downstream users yet, it is a leaf packaging layer: it freezes nonnegativity and a positive threshold so later SGWB amplitude or $\Omega_{\mathrm{GW}}$ claims can cite one inhabited record instead of ad-hoc inequalities.

It does not itself force $D=3$, the eight-tick octave, or the $\alpha$ band; those live in the T0–T8 forcing chain. Its role is local: bind GW-background bookkeeping to Cost and Constants so Recognition-native units stay consistent when cosmology is wired in.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (8)