transmittedFraction
plain-language theorem explainer
The single-rung transmitted energy fraction is fixed at φ^{-1}. Gravity and black-hole echo modelers cite it as the complementary piece of the golden-ratio barrier split. It is a one-line definition, not a derived equality.
Claim. The transmitted energy fraction at one rung of the $\varphi$-self-similar near-horizon barrier is defined to be $\varphi^{-1}$.
background
The module treats the near-horizon recognition structure as a $\varphi$-self-similar potential barrier. At each rung boundary, incident energy splits into reflected and transmitted parts by the golden-ratio partition
$$1 = \varphi^{-1} + \varphi^{-2},$$
which is exactly the defining relation $\varphi^2 = \varphi + 1$.
Here $\varphi$ is the unique positive root of that equation (the RS self-similar fixed point forced at T6). The companion definition sets the reflected fraction to $\varphi^{-2}$; the present constant is the complementary transmitted share $\varphi^{-1}$. No free scattering parameter is introduced: the barrier's energy partition is identified with the algebraic identity of $\varphi$.
proof idea
Pure definitional abbreviation: the real constant is set equal to the multiplicative inverse of $\varphi$ (imported from Constants). There is no proof body beyond the assignment.
why it matters
This constant is the transmitted half of the forced golden-ratio energy split that the module claims is identical to the barrier scattering matrix. Downstream, partition_complete rewrites the sum of reflected and transmitted fractions and invokes the identity $\varphi^{-1}+\varphi^{-2}=1$; positivity and strict upper bounds (transmittedFraction_pos, transmittedFraction_lt_one, and the reflected analogues) then follow by elementary arithmetic from that partition. Those facts underwrite the geometric echo train: amplitude $\varphi^{-n}$ after $n$ rung reflections, with no fitted reflectivity. The construction sits inside the RS gravity story that the QG echo prediction is a structural consequence of $\varphi$-self-similarity rather than dimensional analysis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.