per_turn_at_kappa_one
plain-language theorem explainer
The theorem confirms that the per-turn compression ratio for a κ=1 logarithmic spiral equals the golden ratio φ. Fluid dynamicists optimizing bladeless turbine designs would cite this to fix the baseline compression step in φ-scaled models. The proof is a direct one-line application of the real exponentiation identity that any number to the first power equals itself.
Claim. For the logarithmic spiral with pitch parameter κ=1, the per-turn compression ratio satisfies $φ^1 = φ$, where φ is the golden ratio.
background
In the Tesla turbine model the fluid path is a logarithmic spiral whose pitch κ determines the per-turn compression ratio φ^κ. The module treats disc spacing as proportional to φ times boundary-layer thickness to minimize J-cost of the velocity profile across gaps, with integer κ=1 yielding the minimal non-trivial stable step φ ≈ 1.618. This rests on upstream φ-spiral lemmas from Flight.Geometry and Spiral.SpiralField that define the log-spiral geometry and link it to the self-similar fixed point of the forcing chain.
proof idea
The proof is a one-line wrapper that applies the real exponentiation identity rpow_one directly to φ.
why it matters
This isolates the κ=1 case as the golden compression step, listed among the key results that feed the master certificate tesla_turbine_master. It aligns with the phi-ladder and eight-tick octave structures, where integer exponents mark discrete rungs of compression. The result closes the trivial pitch case without touching open questions on multi-stage stability or viscous flow.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.