echoDampingDiscriminator_holds
plain-language theorem explainer
Packages the RS per-echo amplitude damping ratio $1/\varphi$ as a full discriminator against uniform-discreteness ($1/2$), no-damping ($1$), and no-echo ($0$). Ringdown-echo observers and Track-6 auditors cite it when separating RS from classical Hawking and lattice alternatives. Proof is a structure inhabitant: three strict inequalities are reused directly; three disequalities follow by contradiction via linarith.
Claim. The RS echo-amplitude damping ratio $r = 1/\varphi$ satisfies $r > 1/2$, $r < 1$, and $r > 0$, and therefore $r \neq 1/2$, $r \neq 0$, and $r \neq 1$. These six facts assemble into one inhabited discriminator certificate against uniform-discreteness, undamped, and no-echo alternatives.
background
Gravity Track 6 closes three theorem-grade discriminators between Recognition Science and canonical quantum-gravity alternatives (LQG, string, classical/uniform discreteness, no-echo Hawking). The binding success criterion demands three or more $\varphi$-derived discriminators with named observational channels. This module aggregates already-proved $\varphi$-rational inequalities into a single matrix certificate.
The second discriminator is the per-echo amplitude damping ratio. In RS the ratio equals $1/\varphi \in (0.617, 0.622)$, taken from the black-hole echo-from-bounce development. Classical Hawking predicts no echoes (effective ratio $0$ or undefined); a uniform-discreteness alternative would sit at $1/2$; an undamped cavity would sit at $1$.
The structure EchoDampingDiscriminator packages the six comparison facts (three strict inequalities and three disequalities) that separate $1/\varphi$ from those three alternatives. Upstream lemmas already prove $1/\varphi > 1/2$, $1/\varphi < 1$, and $0 < 1/\varphi$.
proof idea
One-line structure inhabitant. The three inequality fields are filled by the existing lemmas echoDampingRatio_above_half, echoDampingRatio_lt_one, and echoDampingRatio_pos.
Each disequality field is a short contradiction: assume equality, rewrite the matching strict inequality, then linarith discharges the absurd numerical comparison. No new analytic content is introduced; the def only packages prior bounds into the discriminator interface.
why it matters
Feeds the parent certificate discriminatorMatrixCert, which composes the three sub-discriminators (leading-log entropy coefficient, echo damping, per-rung phase delay) into the Track-6 matrix. That matrix is the module's closure object against LQG, string, and classical no-echo programs.
Framework landmark: the damping value is exactly $1/\varphi$, the reciprocal of the self-similar fixed point forced at T6. Observational channel is black-hole ringdown echo trains; a measured amplitude ratio near $0.618$ rather than $0$, $1/2$, or $1$ favors RS. The certificate supplies the explicit numerical margins needed for falsification protocols already outlined in the module doc.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.