phi_energy_partition
plain-language theorem explainer
At a φ-self-similar barrier, energy splits as φ^{-1} (transmitted) plus φ^{-2} (reflected), summing to 1. Gravity and QG-echo workers cite this as the forced single-rung partition. The proof is a short algebraic reduction from the defining identity φ² = φ + 1, using invertibility of φ and nlinarith.
Claim. For the golden ratio $\varphi>0$ one has $\varphi^{-1}+\varphi^{-2}=1$. Equivalently, dividing the defining relation $\varphi^{2}=\varphi+1$ by $\varphi^{2}$ yields the complete energy partition into transmitted fraction $\varphi^{-1}$ and reflected fraction $\varphi^{-2}$.
background
The module models the near-horizon recognition structure as a φ-self-similar potential barrier. At each rung boundary, incident energy splits into a reflected piece and a transmitted piece; the module asserts that the only scale-consistent split is the golden-ratio partition
$$1=\varphi^{-1}+\varphi^{-2}.$$
Here $\varphi$ is the unique positive root of $x^{2}-x-1=0$, so $\varphi^{2}=\varphi+1$ (the lemma phi_sq_eq). The same identity appears throughout the RS constants layer and in the recognition-event-horizon development. Invertibility $\varphi\neq 0$ follows at once from positivity.
The partition is therefore not an extra physical assumption: it is the defining equation of φ rewritten in reciprocal powers. Downstream the reflected fraction is identified with $\varphi^{-2}$ and the transmitted fraction with $\varphi^{-1}$.
proof idea
Record $\varphi\neq 0$ and the key identity $\varphi^{2}=\varphi+1$. Cancel to obtain $\varphi\cdot\varphi^{-1}=1$, and rewrite the second power as $\varphi^{2}\cdot\varphi^{-2}=1$ via the integer-power addition law. Feed both cancellations, together with non-negativity of the square $(\varphi(\varphi^{-1}+\varphi^{-2})-\varphi)^{2}$, into nlinarith; the linear arithmetic engine closes $\varphi^{-1}+\varphi^{-2}=1$. No analysis beyond the field axioms and the defining quadratic is required.
why it matters
This identity is the algebraic heart of the echo-reflection package. It is invoked verbatim by partition_complete (reflected + transmitted = 1), by the certificate constructor echoReflectionCoefficientCert, and by the main structural theorem echo_reflection_coefficient_forced, whose doc-comment states that the amplitude ratio $A_{n+1}/A_n=\varphi^{-1}$ is forced by the partition and ultimately by $\varphi^{2}=\varphi+1$.
In the broader RS chain the result sits under T6 (φ forced as the self-similar fixed point). The module status line emphasizes that the QG-paper echo prediction is therefore a structural consequence of substrate self-similarity at golden-ratio spacing, not a dimensional-analysis estimate or a fitted damping factor. Closing this single algebraic step removes any free parameter from the single-rung scattering matrix.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.