EchoReflectionCoefficientCert
plain-language theorem explainer
Certificate bundling the forced echo reflection law: successive amplitudes satisfy A_{n+1}/A_n = φ^{-1}, from the golden-ratio energy partition 1 = φ^{-1} + φ^{-2}. Anyone citing the RS gravitational-wave echo prediction uses this pack. Fields record the partition, |R| = φ^{-1}, |R|^2 equal to the reflected fraction, geometric decay, and positivity bounds. Companion constructor inhabits it from prior lemmas; no free parameters.
Claim. A certificate asserting: the golden-ratio energy partition $\varphi^{-1}+\varphi^{-2}=1$; single-rung reflection amplitude $|R|=\varphi^{-1}$ with $|R|^2$ equal to the reflected energy fraction $\varphi^{-2}$; successive echo amplitudes in constant ratio $A_{n+1}/A_n=\varphi^{-1}$ for all $n$; $0<|R|<1$; and strictly positive per-rung phase $\log\varphi$.
background
The module treats the near-horizon recognition structure as a φ-self-similar potential barrier. At each rung boundary, energy splits between reflected and transmitted parts by the golden-ratio partition $1=\varphi^{-1}+\varphi^{-2}$, equivalent to $\varphi^2=\varphi+1$. Module status is structural theorem: zero sorry, zero RS-internal axiom.
Local defs fix the scattering data: reflected fraction $\varphi^{-2}$, transmitted fraction $\varphi^{-1}$, reflection amplitude $|R|=\varphi^{-1}$ (so $|R|^2$ recovers the reflected fraction), and echo amplitude at step $n$ proportional to $(\varphi^{-1})^n$. Phase per rung is $\log\varphi$, the log of the scale ratio when crossing from $\ell$ to $\varphi\ell$.
Upstream echo-amplitude defs (this module, BHEchoAmplitudes, and GravitationalWaveEchoFromRS) all encode the same geometric decay $\varphi^{-n}$. The partition identity is the algebraic content of φ's minimal equation; no dimensional analysis enters.
proof idea
This declaration is a structure (certificate type), not a proved theorem. Its fields are Prop-valued obligations naming the partition identity, amplitude equality and square relation, constant amplitude ratio, positivity and upper bound on the reflection amplitude, and positivity of phase per rung.
Inhabitation is separate: the companion value echoReflectionCoefficientCert fills each field by named lemmas (phi_energy_partition, reflectionAmplitude_sq, echo_ratio_constant, phi_pos, and the one-line bound from $1<\varphi$). The nonempty theorem is then a one-constructor wrapper around that value. No new algebra is proved inside the structure itself.
why it matters
This is the master cert for the module's claim that the QG-paper echo prediction is forced, not fitted. Downstream, echoReflectionCoefficientCert builds a concrete inhabitant and echoReflectionCoefficientCert_inhabited records Nonempty, so later gravity or GW developments can assume the whole pack at once.
Framework link: φ is the self-similar fixed point (forcing chain T6). The defining equation $\varphi^2=\varphi+1$ becomes the barrier scattering matrix: $|R|=\varphi^{-1}$, geometric echo train $A_n\propto\varphi^{-n}$, delay set by $\log\varphi$ per rung. Module doc: "the golden ratio's defining equation IS the barrier's scattering matrix."
Closes the structural side of the echo story inside Gravity.EchoReflectionCoefficient; observational comparison and full waveform templates sit outside this cert.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.