transmittedFraction_lt_one
plain-language theorem explainer
At each rung of the φ-self-similar near-horizon barrier, the transmitted energy fraction is strictly less than one. Black-hole echo and gravity analyses cite this to guarantee a nonzero reflected share at every boundary. The argument is a short linear-arithmetic step from positivity of the reflected fraction and completeness of the golden-ratio energy partition.
Claim. The transmitted energy fraction satisfies $T < 1$, where $T$ is the transmission share in the golden-ratio partition $1 = \varphi^{-1} + \varphi^{-2}$ (equivalently $T = \varphi^{-1}$ under the module conventions).
background
The module treats the near-horizon recognition structure as a φ-self-similar potential barrier. At each rung boundary, incident energy splits by the identity $1 = \varphi^{-1} + \varphi^{-2}$, which is exactly $\varphi^2 = \varphi + 1$. Under the module conventions the reflected energy fraction is $\varphi^{-2}$ and the transmitted fraction is $\varphi^{-1}$.
Two upstream facts in the same file pin the inequality: partition_complete states that reflected plus transmitted equals one, and reflectedFraction_pos states that the reflected share is strictly positive. The local setting is structural (zero sorry, no RS-internal axiom): the scattering split is forced by φ, not fitted.
proof idea
Term-mode proof by linear arithmetic. First record $0 < \mathrm{reflectedFraction}$ via reflectedFraction_pos. Feed that inequality together with partition_complete (reflected + transmitted = 1) into linarith, which discharges transmitted < 1. No unfolding of φ is required at this step.
why it matters
Guarantees that transmission never exhausts the incident energy at a single rung, so a reflected wave is always present. That is the elementary inequality behind the module's claim that the QG-paper echo train is forced by substrate self-similarity: $|R| = \varphi^{-1}$ comes from $\varphi^2 = \varphi + 1$ alone (T6 forces φ as the self-similar fixed point). No recorded downstream dependents yet; siblings such as reflectionAmplitude, reflectionAmplitude_sq, and echoDampingFactor build the geometric decay $\varphi^{-n}$ and the round-trip delay. The result is bookkeeping, but without it the barrier would not be a genuine reflector.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.