kappa_one_step_ratio
plain-language theorem explainer
The result states that the step ratio along a logarithmic spiral with pitch parameter exactly 1 equals the golden ratio raised to the normalized angular increment. Turbine designers optimizing boundary-layer compression in bladeless rotors would invoke it to obtain per-turn factors of φ without recomputing the spiral integral. The proof is a direct specialization of the general closed-form lemma for arbitrary kappa, instantiated at kappa=1 and discharged by simplification.
Claim. For $r_0,θ,Δθ∈ℝ$ with $r_0≠0$, the step ratio of the logarithmic spiral with pitch parameter $κ=1$ satisfies stepRatio$(r_0,θ,Δθ)=φ^{Δθ/(2π)}$, where $φ$ denotes the golden ratio.
background
The TeslaTurbine module models fluid flow between closely spaced discs as a logarithmic spiral whose pitch $κ$ controls radial compression per angular turn. The stepRatio function (imported from Flight.Geometry) returns the radial scaling factor after an angular increment $Δθ$ under a given SpiralField.Params record; when $κ=1$ the per-turn compression is exactly $φ$. The upstream lemma stepRatio_logSpiral_closed_form supplies the closed form SpiralField.stepRatio $r_0 θ Δθ P = φ^{(P.kappa)·Δθ/(2π)}$ once $r_0≠0$ eliminates the degenerate branch. MODULE_DOC records that integer $κ=1$ is the minimal non-trivial stable compression step under the Recognition Composition Law.
proof idea
One-line wrapper that applies the upstream lemma stepRatio_logSpiral_closed_form to the concrete parameter record {kappa:=1} and the hypothesis $r_0≠0$, then uses simpa to rewrite the resulting equality into the target form.
why it matters
This theorem supplies the explicit per-turn compression factor required by the φ-spiral engine description in MODULE_DOC, directly supporting the claim that $κ=1$ yields ratio $φ$ and thereby the Fibonacci disc-count optimality listed among the key results. It closes the link between the general log-spiral closed form (Flight.Geometry) and the concrete engineering parameters (disc spacing, pitch) that minimize J-cost. The result sits inside the T6 phi-forcing step of the unified chain and is a prerequisite for any downstream totalCompressionRatio calculation across multiple turns.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.