Gravity Qgobservable Signal Models Qg Observable Signal Models One Statement

Observable signal models

Gravitational physics offers several places where a new theory might leave a measurable trace. The Recognition Science framework's library of formal theorems organizes five such places into typed observation-channel signal models. Each model pairs an observable, the measured physical quantity, with a predicted value and a null baseline, the value standard physics expects. The theorem qg_observable_signal_models_one_statement establishes that all five channels are present, that each prediction is provably distinct from its baseline, and that only three of the five serve as physical evidence.

The five channels are the pulsar timing array (PTA) stochastic background, the Event Horizon Telescope (EHT) shadow radius, S-star orbits near the galactic center, Cassini time-delay, and ringdown echo algebra. For the first four, the framework predicts a positive deviation from the standard baseline. The PTA channel predicts a stochastic gravitational-wave background amplitude at the rung-44 scale, where pure inflation predicts zero. The EHT channel predicts a shadow-radius deviation from Kerr general relativity, where GR predicts zero. The S-star channel predicts a periapsis timing residual, and the Cassini channel predicts a time-delay residual. Each of these four channels carries a proof that the prediction and baseline are separated by more than zero.

The ringdown channel is different. The framework retains a formula for the successive-amplitude ratio of black-hole ringdown echoes, but it is quarantined. The theorem explicitly marks it as not a physical strong-field witness because no horizon-consistent mechanism for echoes has been derived. The physical witness for strong-field gravity uses only the EHT, S-star, and Cassini channels. This separation is not an oversight; it is a deliberate structural choice encoded in the theorem's statement.

What the theorem does not claim is as important as what it proves. It does not claim that any of these predictions are correct, only that they are distinct from the standard baselines. It does not claim that the ringdown formula is physically realized. It does not claim that any measurement has been made. The theorem is a structural statement about the framework's own predictions, not an empirical result.

/-- **OBSERVATION-CHANNEL SIGNAL MODELS ONE-STATEMENT.**  Five typed channels
(PTA, EHT, S-star, Cassini, ringdown algebra) each carry formula-level RS
values, GR/inflation null baselines, and proved algebraic separation.  The
physical strong-field master-theorem witness uses EHT, S-star, and Cassini
only; ringdown is quarantined until a horizon-consistent mechanism is derived. -/
theorem qg_observable_signal_models_one_statement :
    qgChannels.length = 5 ∧
    (∀ c ∈ qgChannels, 0 < |c.rsPrediction - c.nullBaseline|) ∧
    ringdownChannelStatus.physical_strong_field_witness = false ∧
    Nonempty MasterTheorem.PTAStochasticGWDistinctFromInflation ∧
    Nonempty MasterTheorem.StrongFieldTestsDistinctFromGR :=
  ⟨qgChannels_length,
   all_channels_separated,
   rfl,
   ⟨ptaSignalModelWitness⟩,
   ⟨strongFieldSignalModelWitness⟩⟩

theorem ringdownChannelStatus_not_physical_witness :
    ringdownChannelStatus.phi_ratio_formula_carried = true ∧
    ringdownChannelStatus.physical_strong_field_witness = false ∧
    ringdownChannelStatus.horizon_consistent_mechanism_open = true :=
  ⟨rfl, rfl, rfl⟩

/-- The signal-model strong-field witness: the three horizon-exterior
strong-field channels have positive RS deviations distinct from the GR zero
baseline.  Ringdown is deliberately excluded by
`ringdownChannelStatus_not_physical_witness`. -/
noncomputable def strongFieldSignalModelWitness :
    MasterTheorem.StrongFieldTestsDistinctFromGR where
  rs_strong_field_distinct_GR_only :=
    (ehtChannel.rsPrediction ≠ ehtChannel.nullBaseline) ∧
    (sStarChannel.rsPrediction ≠ sStarChannel.nullBaseline) ∧
    (cassiniChannel.rsPrediction ≠ cassiniChannel.nullBaseline)
  holds :=
    ⟨ehtChannel.rsPrediction_ne_null,
     sStarChannel.rsPrediction_ne_null,
     cassiniChannel.rsPrediction_ne_null⟩

What this page does not claim

The theorem does not claim any prediction has been measured or confirmed. The theorem does not claim the ringdown echo formula is physically real. The theorem does not claim the standard baselines are wrong.

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/Gravity/QGObservableSignalModels.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: