resonant_minimization
plain-language theorem explainer
Resonant scales, defined as exact integer powers of the golden ratio φ, yield zero geometric strain. Researchers modeling biological coherence or stability under Recognition Science would cite this when establishing that φ-ladder alignments eliminate deviation cost. The tactic proof unfolds the existential definition to an integer exponent, reduces the floor-log expression via rpow and log-positivity lemmas, confirms the floor identity by linear arithmetic, and applies the J-cost unit lemma.
Claim. If $r > 0$ and $r = φ^n$ for some integer $n$, then the geometric strain $Q_geom(r) = 0$.
background
The Coherence Technology module formalizes how recognition-resonant geometries (φ-spirals, octave loops) affect biological stability. The golden ratio φ is the unique positive fixed point of the self-similar cost recursion. A length scale r is resonant precisely when it lies on the φ-ladder, i.e., equals φ raised to an integer power. Geometric strain at r is the J-cost of the ratio of r to its nearest resonant neighbor, obtained by taking the floor of (log r / log φ + 1/2) as the proxy rung index.
proof idea
The proof introduces the resonant hypothesis, cases on the integer n via rcases, unfolds GeometricStrain, and simplifies the positive-r conditional. It establishes the log identity Real.log (phi ^ n) / Real.log phi = n by rpow and log-positivity from one_lt_phi, then proves floor(n + 1/2) = n by floor_eq_iff and linarith. The final rewrite applies Jcost_unit0 to obtain zero.
why it matters
This theorem supplies the zero-strain base case that feeds the downstream resonance_increases_stability result, which concludes that resonant scales raise system stability. It occupies the coherence-technology phase by linking φ-ladder membership directly to minimal J-cost, consistent with the self-similar fixed point (T6) and the eight-tick octave structure in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.