Pith. sign in
module module moderate

IndisputableMonolith.Gravity.QGObservableSignalModels

show as:
view Lean formalization →

Catalogue of typed observation-channel signal models for the quantum-gravity falsifier matrix. Each channel (PTA, EHT, S-star, Cassini, ringdown) carries a common structure tying RS signature scales to discriminators. Supplies separation and length facts plus PTA and strong-field witnesses. Imported by the unconditional master-theorem closure surface. Mostly definitions and short structural checks.

claimEach quantum-gravity observational channel is packaged as a typed signal model carrying the RS-predicted signature scale and discriminator data. The module fixes the finite list of channels (PTA stochastic background, EHT, S-star, Cassini, ringdown), records that the list has the expected length and that the channels are pairwise separated, and installs structural witnesses for the PTA and strong-field channels used by the master theorem.

background

Recognition Science gravity work organizes quantum-gravity tests as a falsifier matrix of observational channels. Each channel needs a common typed carrier so that predicted RS scales (phi-ladder rungs, eight-tick factorizations) can be compared against baselines without mixing units or hypotheses.

Upstream, the PTA structural track isolates the rung-44 positive scale $\varphi^{-44}$ as the RS signature for a stochastic background, distinct from a zero inflation baseline. The strong-field structural track does the analogous job for strong-field tests (Track 6.C). Both sit under the conditional master theorem (Track 7.A), which still takes channel inputs as arguments.

Constants and the baryon/phi-rung ladder supply the shared arithmetic: $\tau_0$ as the RS time quantum, and rung arithmetic through the eight-tick period. This module only names and packages those channel models; it does not re-derive the scales.

proof idea

Definition-first module. It introduces the observation-channel signal-model type, then constructs the five named channels (PTA, EHT, S-star, Cassini, ringdown) and the finite list of QG channels. Short lemmas record list length and pairwise separation. PTA and strong-field witness terms point at the structural discriminators from the PTA and strong-field modules. A certificate aggregates the package. No deep analytic argument; the load-bearing content is naming and wiring.

why it matters in Recognition Science

Gives the unconditional master-theorem closure a single import surface for every QG observation channel in the falsifier matrix. MasterTheoremUnconditional installs theorem-built witnesses for the five inputs that the older conditional master theorem accepted as arguments; this module is the channel-model half of that wiring.

Without a shared signal-model type, PTA rung-44 structure and strong-field discriminators cannot be fed uniformly into the master statement. The module therefore sits between Tracks 6.B/6.C (structural discriminators) and Track 7.A (master theorem), turning channel-specific algebra into a catalogue the unconditional route can cite. It does not itself discharge the master theorem.

scope and limits

used by (1)

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

depends on (5)

Lean names referenced from this declaration's body.

declarations in this module (15)