RungPhaseDiscriminator
plain-language theorem explainer
Packages five inequalities on the RS per-rung phase delay log φ: it lies strictly in (0, 1/2) and is unequal to 1/2, 3/4, and 1. Gravity and QG ringdown analysts cite it to separate RS echo timing from LQG half-quantum and quarter-period proxies. Structure definition only; inhabitance is assembled elsewhere from proved φ-bounds.
Claim. A certificate that the RS per-rung phase delay $\delta=\log\varphi$ satisfies $0<\delta<1/2$, and moreover $\delta\neq 1/2$, $\delta\neq 3/4$, and $\delta\neq 1$ (separating RS from the LQG half-quantum, a quarter-period proxy, and the unit delay).
background
Track 6 of the gravity program aggregates theorem-grade discriminators between Recognition Science and canonical quantum-gravity alternatives (LQG, string, no-echo Hawking). This module closes the binding criterion: three or more φ-derived discriminators with named observational channels, zero sorry and no RS-internal axioms.
The quantity under test is the per-rung phase delay, identified with $\log\varphi$ (from the black-hole echo/bounce development). In RS units the golden ratio $\varphi$ is forced as the self-similar fixed point (forcing chain T6), so $\log\varphi$ is a pure number fixed once and for all. The comparison points are the LQG half-quantum $1/2$, the quarter-period proxy $3/4$, and the unit delay $1$. Related eight-tick phases $k\pi/4$ supply the discrete angular grid against which continuous rung delay is contrasted.
Upstream, Session 90 already proved $\log\varphi<1/2$ (and positivity of $\log\varphi$ is elementary). The structure merely names the five Prop fields a live certificate must discharge.
proof idea
No proof body: this is a structure definition whose five fields are propositions about rungPhaseDelay ($=\log\varphi$). Inhabitance is not claimed here. The companion constructor fills the fields by quoting the proved bounds $\log\varphi<1/2$ and $0<\log\varphi$, then obtains the three disequalities by contradiction from the strict inequality (if equal to $1/2$ then not strictly below; the $3/4$ and $1$ cases are immediate from the same upper bound).
why it matters
Third leg of the master discriminator matrix. Downstream, the matrix cert requires a leading-log entropy discriminator, an echo-damping discriminator, and this rung-phase discriminator; the inhabited matrix is the Track 6 success object distinguishing RS from LQG, string, uniform discreteness, and no-echo semiclassical gravity.
Observationally the channel is black-hole ringdown / echo timing: a measured per-rung delay inside $(0,1/2)$ and away from $1/2$ favors RS over LQG half-quantum quantization. Framework landmarks in play are T6 (φ forced) and the eight-tick octave (T7), which fix the discrete phase grid the continuous delay is compared against. The structure itself closes no open analytic gap; it only freezes the interface the already-proved φ inequalities must satisfy.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.