PhiSelfSimilarBarrier
plain-language theorem explainer
A φ-self-similar barrier is a positive-length stack of rung boundaries at scales ℓ_n = ℓ_0 · φ^n, each forced to the same reflection amplitude φ^{-1} by self-similarity. Echo and near-horizon gravity work cites it as the data package for geometric decay of successive echoes. It is a structure definition: two fields (rung count with positivity, and uniform reflection equal to φ^{-1}) with no proof body.
Claim. A $\varphi$-self-similar barrier is a pair $(n,\mathrm{unif})$ where $n\in\mathbb{N}$ satisfies $n>0$ and the reflection amplitude at every rung equals $\varphi^{-1}$ (the uniform self-similar value).
background
The module models the near-horizon recognition structure as a φ-self-similar potential barrier. Energy at each rung boundary splits by the golden-ratio partition $1=\varphi^{-1}+\varphi^{-2}$, which is exactly $\varphi^2=\varphi+1$. The single-rung reflection coefficient is therefore $|R|^2=\varphi^{-2}$, so the amplitude is $|R|=\varphi^{-1}$.
That amplitude is packaged upstream as reflectionAmplitude := phi⁻¹. Round-trip phase across one φ-rung is $\log\varphi$ per crossing; echo $n$ then carries amplitude $\varphi^{-n}$ and delay $n\cdot\Delta t_{\mathrm{echo}}$. The structure here records a finite barrier: how many such rungs, and the self-similarity constraint that every rung uses the same amplitude.
Local status is structural (no sorry, no RS-internal axiom). The claim is definitional packaging, not a derived identity; the identity $|R|=\varphi^{-1}$ is already fixed by the partition law before this structure is introduced.
proof idea
No proof: this is a structure definition. It declares three fields: a natural number of rungs, a positivity proof obligation on that count, and an equality asserting that the module-level reflection amplitude equals $\varphi^{-1}$. Downstream constructors discharge positivity by norm_num and the uniformity field by rfl against the definition of the amplitude.
why it matters
This is the carrier type for the module's echo theorems. barrier_total_reflection takes a barrier $B$ and concludes that the echo amplitude after $B$'s rung count is $\varphi^{-n}$, by pure unfolding of the geometric product of identical factors. singleRungBarrier is the canonical one-rung instance used as the base case.
In the Recognition framework this sits under the gravity/echo story: the QG-paper echo prediction is presented as forced by substrate self-similarity at golden-ratio spacing, not by dimensional fitting. The uniform amplitude field is the Lean face of that claim. Landmark contact is T6 (φ as the self-similar fixed point) and the mass/rung ladder language: barriers are counted in rungs, and each rung multiplies by $\varphi^{-1}$.
It does not close open gravity gaps elsewhere in the tree; it only standardizes the barrier hypothesis so the total-reflection identity is a one-line rfl.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.