reflectedFraction_pos
plain-language theorem explainer
The reflected energy fraction at one rung of the near-horizon φ-barrier equals φ^{-2} and is strictly positive. Anyone citing the golden-ratio energy partition or the echo amplitude ladder needs this positivity. The proof is a one-line wrapper: integer powers of φ stay positive because φ > 0.
Claim. Let $\varphi$ be the golden ratio. The reflected energy fraction at a single rung, $\varphi^{-2}$, satisfies $0 < \varphi^{-2}$.
background
In the Echo Reflection Coefficient module the near-horizon recognition structure is 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 fraction is defined as $\varphi^{-2}$ (integer power). The companion transmitted fraction is $\varphi^{-1}$. Both enter the scattering picture: single-rung reflection coefficient $|R|^2 = \varphi^{-2}$, amplitude $|R| = \varphi^{-1}$, and geometric echo decay $\varphi^{-n}$ after $n$ reflections.
Positivity of the reflected piece is the elementary half of the claim that both partition weights are positive; it is used immediately to bound the transmitted weight strictly below one.
proof idea
One-line wrapper. The definition is $\mathrm{reflectedFraction} = \varphi^{-2}$. Apply Mathlib's zpow_pos to the known fact $\varphi > 0$ (from Constants); the integer exponent $-2$ is irrelevant once the base is positive. No case split or arithmetic beyond that lemma.
why it matters
Closes the positivity half of the golden-ratio energy partition that the module treats as the barrier's scattering matrix. Downstream, transmittedFraction_lt_one invokes this fact and partition_complete with linarith to get transmission strictly less than one, so the barrier is not fully transparent.
That bound feeds the structural claim that black-hole echo amplitudes decay geometrically as $\varphi^{-n}$ with no free fitting parameter: the reflection weight is forced by $\varphi^2 = \varphi + 1$ alone (T6 self-similarity of φ). Without reflected-fraction positivity the partition inequalities and the echo-damping story do not start.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.