perTurn_ratio
plain-language theorem explainer
The per-turn ratio lemma recovers the full-rotation multiplier as the special case of the log-spiral step ratio when the angular increment equals 2π. Researchers modeling discrete pitch families or φ-scaled rotor paths in Recognition Science cite it to reduce periodic geometry to the kappa exponent. The proof applies the closed-form step-ratio lemma and cancels the 2π factors in the exponent via direct simplification.
Claim. For nonzero real $r_0$, real angle $θ$, and spiral-field parameters $P$, the step ratio over a full turn satisfies $r(θ + 2π)/r(θ) = φ^κ$, where $κ$ is the kappa parameter of $P$.
background
Flight.Geometry supplies the purely geometric layer of the spiral-field model: φ-tetrahedral angles and log-spiral rotor paths whose scaling is fixed by the Recognition Science constant φ. All results here are math-only; no physical propulsion claims appear. The key upstream fact is the closed-form step-ratio lemma, which states that SpiralField.stepRatio r0 θ Δθ P equals Real.rpow phi ((P.kappa : ℝ) * Δθ / (2 * Real.pi)) whenever r0 ≠ 0. This lemma supplies the explicit φ-power dependence on angular increment that the present result specializes.
proof idea
One-line wrapper that applies stepRatio_logSpiral_closed_form with Δθ set to 2 * Real.pi. The proof then discharges the nonzero denominator 2π, simplifies the exponent (P.kappa * 2π / 2π) to kappa, and rewrites the right-hand side via the definition of perTurnMultiplier.
why it matters
This lemma sits inside the φ-geometry scaffold that feeds FlightReport and the broader discrete-pitch-families construction. It directly instantiates the per-turn multiplier as the Δθ = 2π case of the log-spiral closed form, thereby linking the eight-tick octave structure (T7) and the self-similar fixed point φ (T6) to concrete rotor-path ratios. The result closes a small but necessary reduction step before discreteness statements about integer shifts in kappa can be stated.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.