rotorPath
plain-language theorem explainer
RotorPath aliases the log-spiral radial function on the φ lattice for rotor geometry. A researcher modeling the geometric scaffold of the spiral-field propulsion layer would cite it to invoke the scaled path r(θ) without repeating the exponential form. The declaration is a direct one-line alias with no additional content or proof obligations.
Claim. The rotor radial path is the function satisfying $r(θ) = r_0 · φ^{(κ·θ)/(2π)}$ for parameters $r_0$, $θ$, and $κ$ drawn from the spiral-field definition.
background
The Flight.Geometry module supplies the purely geometric layer of the spiral-field propulsion model, consisting of the φ-tetrahedral angle, log-spiral rotor paths, and associated step-ratio lemmas, all derived from the RS constant φ with no physical claims asserted. The upstream logSpiral definition supplies the concrete expression: def logSpiral (r0 : ℝ) (θ : ℝ) (P : Params) : ℝ := r0 * Real.rpow phi ((P.kappa : ℝ) * θ / (2 * Real.pi)). The module imports Constants, SpiralField, and BondAngles to anchor the φ-scaling and lattice conventions.
proof idea
This is a one-line abbreviation that directly aliases the logSpiral definition from the SpiralField module.
why it matters
The declaration supplies the explicit rotor path expression inside the φ-lattice geometry scaffold of the flight model. It sits downstream of the logSpiral construction and the r0 sector offsets, feeding the broader Recognition Science framework landmarks of φ self-similarity and the eight-tick octave without introducing new axioms or physical assertions. No downstream uses are recorded in the current graph.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.