reflectedFraction_lt_one
plain-language theorem explainer
The reflected energy fraction at one φ-rung of the near-horizon barrier is strictly less than 1. Echo and gravity modelers cite it to guarantee a nonzero transmitted share and geometric damping of successive echoes. The proof is short linear arithmetic from the complete partition identity plus positivity of the transmitted fraction.
Claim. The single-rung reflected energy fraction equals $\varphi^{-2}$ and satisfies $\varphi^{-2} < 1$.
background
This module treats the near-horizon recognition structure as a φ-self-similar potential barrier. At each rung the incident 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}$ and the transmitted fraction as $\varphi^{-1}$.
Upstream, partition_complete states that reflected plus transmitted equals 1 (proved by unfolding the two defs and invoking the native φ-energy partition). transmittedFraction_pos records $0 < \varphi^{-1}$, which follows from positivity of φ. Together those facts force each share into $(0,1)$.
proof idea
Term-mode proof with one intermediate fact. First obtain $0 < \mathrm{transmittedFraction}$ from transmittedFraction_pos. Then apply linarith to that inequality together with partition_complete (reflected + transmitted = 1). The arithmetic immediately yields reflected < 1. No unfolding of φ-powers is required at this step.
why it matters
The module claims the QG-paper echo prediction is forced by substrate self-similarity, not dimensional analysis: single-rung $|R|^2 = \varphi^{-2}$ and amplitude $|R| = \varphi^{-1}$, with echo $n$ damped by $\varphi^{-n}$. Strict inequality reflected < 1 is the elementary bound that keeps the geometric series of successive echoes convergent and leaves a positive transmitted channel at every rung.
No downstream consumers are wired yet (used_by is empty), but sibling declarations (reflectionAmplitude, reflectionAmplitude_sq, echoDampingFactor, transmittedFraction_lt_one) sit on the same partition and will inherit the bound. In the broader RS chain this is local gravity scaffolding built on the forced φ of T6, not a new forcing step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.