stepRatio
plain-language theorem explainer
The radial ratio along a logarithmic spiral between angles separated by an increment is computed from the base radius, starting angle, and integer pitch parameter. Researchers working on phi-scaled flow geometries and turbine designs would reference this when establishing scale invariance or per-turn multipliers. The implementation evaluates the spiral radius function at the two angles and forms their quotient, returning unity if the initial radius is zero.
Claim. For base radius $r_0$, angle $θ$, angular increment $Δθ$, and spiral parameter record $P$ holding integer pitch $κ$, the ratio is $r(θ + Δθ)/r(θ)$ when $r(θ) ≠ 0$ and equals 1 otherwise, where the spiral radius satisfies $r(θ) = r_0 φ^{κ θ / (2π)}$.
background
The Spiral Wavefields module supplies a scaffold for variational ansatz of logarithmic spiral fields under phi-scaling together with an eight-tick gating constraint; only basic structures and helpers are defined, with no proofs required for compilation. The parameter record holds a single integer pitch value. The spiral radius function is given explicitly by base scale times phi raised to the power of (pitch times angle) over two pi. Upstream, the cost from MultiplicativeRecognizerL4 is the derived cost of its comparator on positive ratios, while the cost from ObserverForcing is the J-cost of a recognition event. The anchor r0 supplies phi-exponent offsets per sector that originate from wallpaper and cube geometry.
proof idea
As a definition it directly constructs the ratio by evaluating the spiral radius function at the incremented angle and at the original angle, then dividing unless the base evaluation vanishes, in which case it returns 1. It depends on the sibling spiral radius function and the parameter record for the pitch value but invokes no lemmas or tactics.
why it matters
It supplies the core radial ratio used by the closed-form identity in Flight.Geometry and by the per-turn multiplier lemma, which in turn support the master theorem on the phi-spiral engine in Flight.TeslaTurbine. This fills the discrete pitch computation step in the Recognition framework, linking to the self-similar fixed point phi from the forcing chain and to the eight-tick octave. It leaves open the full embedding of J-cost minimization inside the spiral ansatz.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.