perTurnMultiplier
plain-language theorem explainer
The perTurnMultiplier definition supplies the multiplicative growth factor per full revolution of a logarithmic spiral whose pitch is set by integer kappa. Flight geometry lemmas cite it to recover the ratio r(θ+2π)/r(θ) and to establish discrete pitch families under φ-scaling. The definition is a direct one-line application of the real power function to the golden ratio.
Claim. Let $P$ be a parameter record containing an integer pitch index $κ$. The per-turn multiplier is defined by $φ^κ$, where $φ$ denotes the golden ratio.
background
The SpiralField module supplies a variational scaffold for logarithmic spiral fields under φ-scaling together with an eight-tick gating constraint. Its Params structure stores the single integer field kappa; the associated radius formula is $r(θ)=r0·φ^{(κ·θ)/(2π)}$. The golden ratio is taken from the imported Constants bundle, while upstream cost functions from MultiplicativeRecognizerL4 and ObserverForcing supply the J-cost background against which the spiral ansatz is later evaluated.
proof idea
One-line definition that applies Real.rpow to IndisputableMonolith.Constants.phi with the real cast of P.kappa.
why it matters
kappa_discreteness, perTurn_ratio and spiral_pitch_one_is_phi all invoke this definition to obtain their statements about discrete pitch families and the special case κ=1. It supplies the concrete φ-scaling map required by the spiral wavefield ansatz, linking directly to the self-similar fixed point T6 and the eight-tick octave T7 of the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.