bounceRadius_mono
plain-language theorem explainer
The theorem establishes that the bounce radius at recognition rung N is strictly less than at rung N+1. Physicists modeling black hole echoes or quantum gravity from Recognition Science would cite this to guarantee that echo delays increase with rung gap. The proof is a short algebraic reduction that unfolds the power definition and applies the inequality 1 < φ together with positivity of powers.
Claim. $For all natural numbers $N$, $φ^N < φ^{N+1}$.
background
The bounce radius is defined as φ raised to the power N in RS-native units. This definition appears in the Gravity modules and is imported here to support quantum gravity claims. The module QuantumGravityFromRS supplies structural facts for five canonical quantum gravity approaches that RS subsumes, with the bounce radius given by ℓ_Planck × φ^(N/2) in the broader setting but simplified to φ^N in this file.
proof idea
The proof unfolds the definition of bounceRadius, obtains positivity of φ^N via pow_pos, rewrites the successor exponent, and closes with linarith using mul_lt_mul_of_pos_left applied to one_lt_phi.
why it matters
This result supplies the monotonicity fact required by quantumGravityCert, which certifies the five quantum gravity approaches together with positivity and echo delay facts. It directly implements the module's claim that echo delay is monotone in N, closing one of the three structural backing items listed in the module documentation. The argument rests on the phi fixed point and the phi-ladder structure from the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.