bounceRadius_succ_ratio
plain-language theorem explainer
Adjacent-rung bounce radius scales exactly by the golden ratio φ. LIGO/Virgo catalog analysts cite this when scaling predicted echo delays across successive mass rungs in the recognition lattice. The proof is a one-line wrapper that unfolds the bounceRadius definition and rewrites with the power-successor identity.
Claim. For every natural number $N$, the bounce radius at rung $N+1$ equals the bounce radius at rung $N$ multiplied by the golden ratio $φ$.
background
The module catalogs LIGO/Virgo merger events under the recognition-lattice bounce model. Bounce radius and echo delay are defined for every rung $N ≥ 1$, with the delay given by twice the radius times log φ. The local setting requires both quantities to remain strictly positive and to obey the adjacent-rung ratio φ.
proof idea
The proof unfolds the definition of bounceRadius and rewrites using the successor rule for exponentiation (pow_succ).
why it matters
The result is collected into bhEchoesCert, which bundles the four positivity and ratio certificates for the catalog. It supplies the scaling step required by the black-hole echoes predictions and instantiates the phi-ladder self-similarity from the forcing chain. The declaration touches the open question of whether a null echo result on any high-SNR event with $N ≥ 1$ would falsify the bounce mechanism.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.