resonance_increases_stability
plain-language theorem explainer
If a positive length scale lies off the phi-ladder while another lies on it, system stability at the off-ladder scale is strictly lower. Biologists or coherence engineers modeling resonant geometries would cite the result to quantify stability gains from phi-alignment. The proof splits cases: resonant_minimization forces zero strain and unit stability for the resonant input, while Jcost_pos_of_ne_one plus div_lt_one shows positive strain and reduced stability for the non-resonant input.
Claim. Let $r>0$ and $s>0$. If $r$ is not equal to any integer power of the golden ratio while $s$ is, then the stability $1/(1+Q(r))$ is strictly less than $1/(1+Q(s))$, where $Q$ is geometric strain.
background
The module Phase 10.2 formalizes how recognition-resonant geometries (phi-spirals, octave-loops) affect biological stability. The golden ratio is the unique positive fixed point of the self-similar cost recursion, so scales aligned with it are resonant because they match the ledger's fundamental scaling law. ResonantScale(r) holds when there exists integer n with r equal to phi to the n. GeometricStrain(r) for r>0 equals Jcost of r divided by phi to the nearest rung, using floor of (log r over log phi plus one-half). SystemStability(r) is then one over one plus that strain.
proof idea
The tactic proof begins by applying resonant_minimization to the resonant scale, unfolding SystemStability, rewriting the zero strain, and simplifying to obtain stability exactly one. For the non-resonant scale it unfolds GeometricStrain, computes the nearest rung n, proves the ratio to phi^n differs from one, invokes Jcost_pos_of_ne_one to obtain positive J-cost, then uses linarith and div_lt_one to conclude the resulting stability is strictly below one.
why it matters
The declaration fills the coherence-stability link stated in the module doc-comment. It shows that alignment with the phi-ladder (T6 self-similar fixed point) raises stability to its maximum, supporting the Recognition framework claim that resonant geometries minimize cost. No downstream uses appear yet, but the result closes an applied step between the Cost module and coherence arguments. It leaves open the extension to time-dependent or multi-scale systems.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.