reflectionAmplitude_sq
plain-language theorem explainer
The square of the single-rung reflection amplitude equals the reflected energy fraction at a φ-self-similar barrier. Both sides are fixed by the golden ratio alone: amplitude φ^{-1} and energy fraction φ^{-2}. Cite this when packaging the forced echo damping law or the echo-reflection certificate. The proof is a short integer-power rewrite of (φ^{-1})^2 to φ^{-2}.
Claim. The single-rung reflection amplitude squared equals the reflected energy fraction: $(\varphi^{-1})^2 = \varphi^{-2}$, where the amplitude is $\varphi^{-1}$ and the reflected fraction is $\varphi^{-2}$.
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 the defining relation $\varphi^2 = \varphi + 1$. The module therefore sets the reflected energy fraction to $\varphi^{-2}$ and the reflection amplitude to $\varphi^{-1}$, so that amplitude squared recovers the energy fraction with no free parameter.
Upstream, the two sides are the plain definitions: amplitude is the real reciprocal of φ, and the reflected fraction is the integer power $\varphi^{-2}$. The present identity is the elementary bridge between those two quantities.
proof idea
Both sides unfold immediately: left-hand side is $(\varphi^{-1})^2$, right-hand side is $\varphi^{-2}$. Rewrite the square as an integer power via the standard zpow identities (natural cast of the exponent 2, inverse as $zpow$ of $-1$, and multiplication of exponents). A final norm_num checks that the exponents match. No analytic estimates or external lemmas beyond integer-power algebra.
why it matters
This identity is one of the four conjuncts of the main forced-echo theorem: the constant amplitude ratio $A_{n+1}/A_n = \varphi^{-1}$ is packaged together with the partition $1 = \varphi^{-1}+\varphi^{-2}$, the amplitude-squared equality, and positivity/bound constraints. It is also recorded directly in the module certificate structure.
In the Recognition framework the result closes the amplitude-to-energy step of the QG-paper echo prediction. The scattering matrix of the barrier is forced by the self-similar fixed point of φ (T6) alone; no dimensional analysis or fit enters. Fully proved, zero sorry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.