Gravity Qgobservable Signal Models Qg Channels Length

The five observation channels

In physics, a quantum gravity theory must say what an experiment would actually see. The Recognition Science framework organizes this into a typed signal model: for each observational channel, it records the measured quantity, the framework's predicted value, the standard baseline from general relativity or inflation, the current measurement precision, and the threshold a future experiment must cross to falsify the prediction. The declaration qgChannels_length is the simple bookkeeping fact that this collection contains exactly five such channels.

The five channels are named for their experiments. The PTA channel predicts a stochastic gravitational-wave background amplitude at a specific scale, where pure inflation predicts zero. The EHT channel predicts a shadow-radius deviation from the Kerr black hole template. The S-star channel predicts a periapsis timing residual near the galactic center. The Cassini channel predicts a time-delay residual beyond the standard parametrized post-Newtonian framework. The fifth, ringdown echo algebra, is quarantined: it carries a formula but is explicitly not part of the physical strong-field witness, because no horizon-consistent echo mechanism has been derived.

The theorem qgChannels_length does not prove that any of these predictions are correct. It proves only that the list has length five, a fact that follows by definition. A separate theorem, all_channels_separated, proves that each channel's prediction differs from its baseline by a positive amount. The strongest physical claim, assembled in the master theorem, uses only the three horizon-exterior channels (EHT, S-star, Cassini) for its strong-field witness, and it proves these are distinct from the GR zero baseline. The ringdown channel is deliberately excluded from that witness.

What the declaration does not claim is broader than what it proves. It does not claim that any experiment has detected these signals, nor that the predicted values are within reach of current instruments. It does not claim that the ringdown formula is a valid black-hole prediction. It does not even claim that the framework's predicted values are physically realized; it claims only that the predictions are algebraically separated from the baselines, so that a future experiment could in principle distinguish them.

In Recognition Science, the value of this bookkeeping is that it forces the framework to name its falsifiers. Each channel carries a futureThreshold, the measurement precision that would decide between the framework's prediction and the standard baseline. The declaration qgChannels_length is the smallest piece of that machinery: it fixes the count, so that the list of tests is closed and auditable. The reader can now see exactly which experiments the framework commits to, and which it does not.

theorem qgChannels_length : qgChannels.length = 5 := rfl

/-- Every channel in the collection has a positive separation between RS
prediction and null baseline. -/
theorem all_channels_separated :
    ∀ c ∈ qgChannels, 0 < |c.rsPrediction - c.nullBaseline| :=
  fun c _ => c.separation_pos

/-- 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⟩

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⟩

What this page does not claim

No experiment has detected any of the predicted signals, and no claim is made about current detection status. The ringdown echo formula is not a valid black-hole prediction until a horizon-consistent mechanism is derived. The algebraic separation of predictions from baselines does not imply the predictions are physically realized.

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: