ringdownChannel
plain-language theorem explainer
Ringdown echoes are packaged as one typed QG falsifier channel: the observable is the successive-echo amplitude ratio, RS predicts φ^{-1} ≈ 0.618, and classical GR predicts zero. Strong-field and multi-channel QG falsifier citations use this record. The definition fills the signal-model fields and discharges inequality obligations by positivity of φ^{-1}.
Claim. The ringdown channel is the typed observation-channel signal model with name "Ringdown echoes", observable the successive-echo amplitude ratio $A_{n+1}/A_n$, RS prediction $\varphi^{-1}$, and null baseline $0$, together with proofs that $\varphi^{-1} \neq 0$ and $0 < |\varphi^{-1}-0|$.
background
This module builds typed signal models for the five observational channels on the quantum-gravity falsifier surface (PTA, EHT, S-star, Cassini, ringdown). Each channel is an ObservationChannelSignalModel: a name, a measured observable string, an RS real prediction, a null (GR/ΛCDM) baseline, and two inequality fields forcing the prediction off the baseline with positive absolute separation.
For ringdown, the observable is the amplitude ratio between successive echoes. Classical GR with no echoes sets the null baseline to zero. Recognition Science assigns the prediction $\varphi^{-1}$, the same golden-ratio inverse that appears as the Berry creation threshold in the broader framework.
The constants bundle supplies phi with a positivity lemma used below; no deeper Clifford or ledger structure is invoked at this definition site.
proof idea
Structure-instance definition, not a deep theorem. Two proof fields are filled by short tactic scripts.
rsPrediction_ne_null: assume $\varphi^{-1}=0$, obtain $0<\varphi^{-1}$ from inv_pos and phi_pos, then linarith for contradiction.
separation_pos: again use $0<\varphi^{-1}$, simplify $|\varphi^{-1}-0|$ via sub_zero and abs_of_pos, and return the same positivity fact.
why it matters
Closes the fifth slot in the QG falsifier channel list. Downstream, qgChannels collects it with PTA, EHT, S-star, and Cassini; strongFieldSignalModelWitness uses the strong-field siblings to assert RS deviations distinct from the GR zero baseline (ringdown supplies the same pattern: nonzero RS prediction against a zero null).
Doc-comment stress: no other quantum-gravity framework predicts this specific value $\varphi^{-1}\approx 0.618$ for the echo amplitude ratio. That pins a sharp, single-number falsifier against the classical no-echo baseline. Framework landmark: Berry creation threshold $\varphi^{-1}$.
Status is structural (definition with discharged inequality proofs, zero sorry).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.