echoReflectionCoefficientCert
plain-language theorem explainer
Packages the golden-ratio echo barrier facts into a single certificate: energy splits as φ^{-1}+φ^{-2}=1, reflected amplitude is φ^{-1}, successive echo amplitudes decay by exactly that factor, and the per-rung phase is positive. Gravity and QG-echo readers cite it as the closed structural claim that |R|=φ^{-1} needs no free parameter. The body is a field-by-field assembly of already-proved lemmas plus two short positivity/bound facts from φ>1.
Claim. There exists a certificate recording: the golden-ratio energy partition $\phi^{-1}+\phi^{-2}=1$; the single-rung reflection amplitude equals $\phi^{-1}$; its square equals the reflected energy fraction; for every $n$, the ratio of successive echo amplitudes is $\phi^{-1}$; that amplitude is positive and strictly less than $1$; and the phase accumulated per $\phi$-rung is positive.
background
The module treats the near-horizon recognition structure as a φ-self-similar potential barrier. At each rung the energy splits by the golden-ratio partition $1=\phi^{-1}+\phi^{-2}$, which is exactly $\phi^2=\phi+1$ rewritten. The reflected fraction is therefore $\phi^{-2}$ and the reflected amplitude is $\phi^{-1}$; successive echoes form a geometric sequence with that common ratio, and the round-trip phase per rung is $\log\phi$.
Upstream, phi_energy_partition proves the split from $\phi^2=\phi+1$ alone. echo_ratio_constant shows $A_{n+1}/A_n=\phi^{-1}$ by unfolding the geometric definition of echo amplitude. reflectionAmplitude_sq ties amplitude squared to the reflected fraction, and phasePerRung_pos uses $\phi>1$ (from one_lt_phi) to get a positive log phase. The certificate structure simply names these obligations as fields.
proof idea
Field-wise witness construction, not a new argument. partition is filled by phi_energy_partition. amplitude_eq is definitional (rfl). amplitude_sq and ratio_constant are the named theorems reflectionAmplitude_sq and echo_ratio_constant. Positivity of the amplitude is inv_pos applied to phi_pos. The strict bound amplitude $<1$ unfolds reflectionAmplitude and applies inv_lt_one_of_one_lt₀ to one_lt_phi. Phase positivity is phasePerRung_pos.
why it matters
This is the packaged form of the module's structural theorem: the QG-paper echo prediction is forced by φ-self-similarity, not dimensional analysis. The certificate's doc states that $A_{n+1}/A_n=\phi^{-1}$ follows from $1=\phi^{-1}+\phi^{-2}$, itself equivalent to $\phi^2=\phi+1$, so the golden ratio's defining equation is the barrier scattering matrix. Downstream, echoReflectionCoefficientCert_inhabited uses this value to prove the certificate type is nonempty. In the broader RS chain it sits on T6 (φ as the self-similar fixed point) and supplies the concrete gravity-side amplitude and delay skeleton (geometric decay $\phi^{-n}$, delay proportional to $\log\phi$) without introducing free parameters.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.