reflectedFraction
plain-language theorem explainer
The single-rung reflected energy fraction on the near-horizon φ-barrier is fixed at φ^{-2}. Echo and QG analyses cite it as |R|² in the golden-ratio partition 1 = φ^{-1} + φ^{-2}. The declaration is a bare definition: the real constant φ raised to the integer power -2. Downstream lemmas then prove positivity, completeness of the split, and that the amplitude squared recovers this value.
Claim. Define the reflected energy fraction at one rung by $R_{\mathrm{frac}} := \varphi^{-2}$, where $\varphi$ is the golden ratio.
background
The module models the near-horizon recognition structure as a φ-self-similar potential barrier. At each rung boundary, incident energy splits into reflected and transmitted parts by the golden-ratio partition
$$1 = \varphi^{-1} + \varphi^{-2},$$
which is exactly the defining relation $\varphi^2 = \varphi + 1$. The module states that the single-rung reflection coefficient is $|R|^2 = \varphi^{-2}$ and the reflected amplitude is $|R| = \varphi^{-1}$, with no free fit parameter.
Here $\varphi$ is the RS constant (self-similar fixed point from the forcing chain). The companion transmitted fraction is defined as $\varphi^{-1}$. Integer powers of $\varphi$ are the natural language of the φ-ladder; the exponent $-2$ is one rung of reflection in that discrete structure.
proof idea
Definitional, not a proved theorem. The body is the single term $\varphi^{(-2:\mathbb{Z})}$ as a real. No tactics, no lemmas. Later results unfold this name and rewrite with the energy-partition identity or with $zpow$ algebra (for example when showing amplitude squared equals the reflected fraction).
why it matters
This constant is the scattering weight that makes the echo story forced rather than phenomenological. It is the reflected half of the partition used by partition_complete ($R_{\mathrm{frac}} + T_{\mathrm{frac}} = 1$), and the target of reflectionAmplitude_sq ($|R|^2 = R_{\mathrm{frac}}$). Positivity and strict upper bounds (reflectedFraction_pos, reflectedFraction_lt_one) rest on it, as does the transmitted-side comparison.
The certificate structure and the forced theorem package the same content: amplitude ratio $A_{n+1}/A_n = \varphi^{-1}$, partition identity, and amplitude squared equal to this fraction, all with no dimensional analysis. In the framework this is the gravity-side reading of φ from T6 (self-similar fixed point): the defining equation of φ is literally the barrier S-matrix entry for one rung.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.