partition_complete
plain-language theorem explainer
At one φ-rung of the near-horizon barrier, the reflected energy fraction plus the transmitted fraction equals one. Echo-amplitude and golden-ratio scattering arguments cite this as exact energy bookkeeping. The proof unfolds the two fraction definitions and rewrites to the identity φ^{-1}+φ^{-2}=1.
Claim. The reflected energy fraction $\varphi^{-2}$ and the transmitted energy fraction $\varphi^{-1}$ sum to one: $\varphi^{-2}+\varphi^{-1}=1$.
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 pieces fixed solely by the golden ratio. The defining equation $\varphi^2=\varphi+1$ rearranges, after dividing by $\varphi^2$, to the energy partition $1=\varphi^{-1}+\varphi^{-2}$.
Two named constants package those pieces: the reflected fraction is $\varphi^{-2}$, and the transmitted fraction is $\varphi^{-1}$. Upstream, the golden-ratio energy-partition theorem already proves $\varphi^{-1}+\varphi^{-2}=1$ from $\varphi\neq 0$, positivity of $\varphi$, and $\varphi^2=\varphi+1$ alone. No fitting parameter enters.
This declaration is the bookkeeping form of that identity once the fractions are defined as module constants: their sum must be unity, so the single-rung barrier neither creates nor destroys energy.
proof idea
Unfold both fraction definitions to $\varphi^{-2}$ and $\varphi^{-1}$. Commute addition so the sum order matches the upstream energy-partition lemma, then apply that lemma by exact. Three steps: unfold, rewrite commutativity of addition, discharge with the golden-ratio partition identity. No new arithmetic is proved here.
why it matters
This is the conservation step for the single-rung scattering data of the φ-barrier. Downstream, the strict bounds that each fraction is less than one follow by linear arithmetic from this identity plus positivity of the complementary fraction. Those bounds underwrite the geometric decay of successive echo amplitudes $|R|^n=\varphi^{-n}$ and the damping factor built later in the file.
In the Recognition framework the split is forced by the self-similar fixed point (T6) and the defining equation of φ; the module presents the reflection coefficient $|R|=\varphi^{-1}$ as a structural consequence, not a dimensional estimate. Status is fully proved (zero sorry). The same completeness idea appears abstractly as bipartition bookkeeping elsewhere in the gravity ledger, but the concrete parent uses here are the two fraction-less-than-one lemmas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.