reflectionAmplitude
plain-language theorem explainer
The single-rung reflection amplitude on a φ-self-similar near-horizon barrier is fixed at φ^{-1}. Echo and QG analyses cite it as the geometric decay factor per rung reflection. The definition is the positive square root of the reflected energy fraction φ^{-2}, forced by the golden-ratio partition 1 = φ^{-1} + φ^{-2}.
Claim. The reflection amplitude at one rung of the $\varphi$-self-similar barrier is $|R| = \varphi^{-1}$. Equivalently, $|R| = \sqrt{\varphi^{-2}}$, the positive square root of the reflected energy fraction.
background
The module treats the near-horizon recognition structure as a φ-self-similar potential barrier. At each rung boundary, energy splits by the golden-ratio partition $1 = \varphi^{-1} + \varphi^{-2}$, which is exactly $\varphi^2 = \varphi + 1$. The reflected energy fraction is therefore $\varphi^{-2}$ and the transmitted fraction is $\varphi^{-1}$.
The reflection coefficient at a single rung is $|R|^2 = \varphi^{-2}$, so the amplitude is $|R| = \varphi^{-1}$. Round-trip phase across one rung is $\log\varphi$ per crossing; echo $n$ then carries amplitude $\varphi^{-n}$ and delay $n\cdot\Delta t_{\mathrm{echo}}$.
Sibling quantities in the same file name the partition pieces (reflectedFraction, transmittedFraction) and the damping factor used for successive echoes. The constant $\varphi$ is the RS self-similar fixed point (forcing chain T6).
proof idea
One-line definition: the real constant is set equal to $\varphi^{-1}$. No tactic proof. The surrounding doc-comment records the physical reading: amplitude squared equals the reflected energy fraction $\varphi^{-2}$, hence the amplitude is the positive root $\varphi^{-1}$. Downstream, reflectionAmplitude_sq discharges that identity by rewriting powers of $\varphi$.
why it matters
This constant is the scattering amplitude that the golden-ratio barrier is forced to carry. It is wired into PhiSelfSimilarBarrier (uniform reflection at every rung), into reflectionAmplitude_sq (amplitude squared equals reflected fraction), and into the equality echoDampingFactor_eq_reflectionAmplitude.
The certificate structure EchoReflectionCoefficientCert and the theorem echo_reflection_coefficient_forced package the full claim: successive echo amplitudes satisfy $A_{n+1}/A_n = \varphi^{-1}$, with no fitting parameter and no dimensional analysis. Module status is structural (0 sorry). Framework landmark: φ as the self-similar fixed point (T6) becomes the barrier scattering matrix via $\varphi^2 = \varphi + 1$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.