stepRatio_logSpiral_closed_form
plain-language theorem explainer
The lemma gives a closed-form expression for the step ratio of a log-spiral path: the ratio equals phi raised to kappa times delta theta over 2 pi, independent of the starting radius and angle. Flight-geometry researchers working on discrete pitch families cite it as the algebraic kernel that converts continuous spiral scaling into discrete multipliers. The proof unfolds the stepRatio definition, invokes the non-zero lemma for the spiral, splits the exponent via ring, applies rpow_add, and cancels common factors with field_simp.
Claim. Let $r_0, theta, Delta theta in mathbb{R}$ with $r_0 neq 0$, and let $P$ be a spiral-field parameter record whose kappa component is a real number. Then the step ratio along the log-spiral satisfies $r(theta + Delta theta)/r(theta) = phi^{kappa Delta theta / (2 pi)}$, where $phi$ denotes the Recognition Science constant.
background
The module supplies the purely geometric layer of the spiral-field model: phi-tetrahedral angles and log-spiral rotor paths whose radii scale by powers of phi. The function logSpiral r0 theta P returns r0 times phi raised to (kappa times theta over 2 pi); stepRatio is defined as the ratio of two such values, with a special case returning 1 when r0 equals zero. The upstream lemma logSpiral_ne_zero states that logSpiral r0 theta P is nonzero whenever r0 is nonzero, because phi to any real power remains positive.
proof idea
The tactic proof first unfolds stepRatio and applies logSpiral_ne_zero to discharge the zero-radius branch, then simplifies. It splits the combined exponent with a ring identity, invokes Real.rpow_add on the positive phi constant to factor the power, rewrites the factored form, and finishes with field_simp to cancel the common r0-powered term.
why it matters
This closed form is the direct parent of perTurn_ratio (the special case Delta theta equals 2 pi recovers phi to the kappa) and of kappa_one_step_ratio (the kappa equals 1 instance). It supplies the algebraic engine behind discrete pitch families in the Flight subtheory and sits inside the phi-scaling scaffold that descends from the self-similar fixed point T6. No open scaffolding remains; the lemma is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.