singleRungBarrier
plain-language theorem explainer
Canonical one-rung instance of a φ-self-similar near-horizon barrier: a single scale boundary with uniform reflection amplitude φ^{-1}. Gravity and echo-timing work cites it as the base case of the geometric cascade. The instance is a structure fill-in: numRungs = 1, positivity by norm_num, and the uniform-reflection field by reflexivity against the fixed amplitude.
Claim. The single-rung barrier is the $\varphi$-self-similar barrier with $n=1$ rungs: $0 < 1$, and the reflection amplitude at that rung equals $\varphi^{-1}$ (the same value forced at every rung by self-similarity).
background
The module treats the near-horizon recognition structure as a $\varphi$-self-similar potential barrier. Rung boundaries sit at scales $\ell_n = \ell_0 \cdot \varphi^n$. Self-similarity forces every boundary to share one reflection amplitude.
Energy at a rung splits by the golden-ratio partition $1 = \varphi^{-1} + \varphi^{-2}$, equivalent to $\varphi^2 = \varphi + 1$. The single-rung reflection coefficient is therefore $|R|^2 = \varphi^{-2}$ and the amplitude is $|R| = \varphi^{-1}$, with no free fit parameter.
PhiSelfSimilarBarrier packages a positive rung count together with the equality reflectionAmplitude = phi⁻¹. The present definition is the minimal concrete inhabitant of that structure.
proof idea
Structure instance, not a multi-step proof. Set numRungs := 1. Discharge numRungs_pos by norm_num (the literal $0 < 1$). Discharge uniformReflection by rfl, since the structure field is definitionally the already-fixed amplitude $\varphi^{-1}$.
why it matters
Gives the base case of the echo cascade in the QG paper: one reflection contributes amplitude $\varphi^{-1}$ and one factor of the round-trip phase $\log\varphi$. Multi-rung barriers then multiply amplitudes to $\varphi^{-n}$ with delay $n\cdot\Delta t_{\rm echo}$.
That matches the module claim that the echo prediction is forced by substrate self-similarity at golden-ratio spacing, not dimensional analysis. The partition $1=\varphi^{-1}+\varphi^{-2}$ is the scattering content of $\varphi^2=\varphi+1$ (T6 fixed point in the forcing chain).
No downstream theorems currently depend on this name; siblings such as reflected/transmitted fractions and the damping factor sit beside it as the quantitative layer built on the same barrier structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.