logSpiral
plain-language theorem explainer
logSpiral supplies the explicit radius function for a logarithmic spiral whose growth is governed by the golden ratio φ raised to an angle-dependent exponent. Flight geometry modules cite it to define rotor paths and step ratios on the φ-lattice. The definition is a direct algebraic expression using the phi constant and the kappa parameter from Params.
Claim. $r(θ) = r_0 ⋅ φ^{(κ ⋅ θ)/(2π)}$ where $κ$ is the integer parameter in the structure Params and $φ$ denotes the golden-ratio constant.
background
The SpiralField module supplies a variational ansatz for logarithmic spiral fields under φ-scaling together with an eight-tick gating constraint; the file contains only basic structures and helpers. Params is the local structure carrying the single integer field kappa that sets the spiral pitch. Upstream results supply the phi constant from the Constants bundle and the J-cost definitions from MultiplicativeRecognizerL4 and ObserverForcing that motivate the geometric construction.
proof idea
The definition is a direct one-line computation that multiplies the base radius r0 by phi raised to the real exponent (kappa ⋅ θ) / (2 ⋅ π) via Real.rpow.
why it matters
logSpiral is the kernel for the rotorPath abbreviation and the stepRatio closed-form lemma in Flight.Geometry; those in turn feed the SpiralArray construction in VirtualRotor. It realizes the φ-scaling fixed point (T6) inside the spiral domain and supplies the discrete pitch families needed for the eight-tick octave geometry. No open scaffolding remains attached to this definition.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.