perTurn_ratio
The lemma recovers the per-turn radial growth factor of a log-spiral as exactly φ raised to the kappa parameter of the spiral field. Modelers constructing discrete pitch families in φ-scaled geometries would cite it to specialize the general step ratio to a full revolution. The proof is a direct specialization of the closed-form step ratio lemma at Δθ = 2π followed by algebraic cancellation of the angle in the exponent.
claimFor nonzero initial radius $r_0$, angle $θ$, and spiral parameters $P$, the radial step ratio over a full turn satisfies $r(θ + 2π)/r(θ) = φ^κ$, where $κ$ denotes the kappa component of $P$.
background
The Flight.Geometry module supplies the purely geometric layer for spiral-field models, deriving log-spiral rotor paths from the Recognition Science constant φ. The central upstream result is the closed-form step ratio lemma, which states that the ratio equals φ raised to (kappa · Δθ / 2π) for r0 ≠ 0; its doc-comment calls this expression the mathematical kernel behind discrete pitch families. The per-turn multiplier is the direct specialization of that expression at Δθ = 2π, yielding φ^κ.
proof idea
The proof applies the closed-form step ratio lemma with Δθ set to 2π. It establishes that 2π is nonzero by factoring out the constant 2 and using π ≠ 0, then cancels the angle factor in the exponent via mul_div_cancel_right₀. The resulting expression is substituted into the definition of the per-turn multiplier.
why it matters in Recognition Science
This lemma is referenced by the FlightReport summary string in the Flight subtheory. It realizes the special case of the discrete pitch families idea, where per-turn growth occurs in multiplicative steps of φ^d. The result anchors the angular period 2π inside the φ-ladder geometry derived from the forcing chain.
scope and limits
- Does not constrain kappa to integer values.
- Does not incorporate forces or propulsion dynamics.
- Does not extend beyond log-spiral paths.
- Does not address stability under perturbations.
formal statement (Lean)
125lemma perTurn_ratio
126 (r0 θ : ℝ) (P : SpiralField.Params) (hr0 : r0 ≠ 0) :
127 SpiralField.stepRatio r0 θ (2 * Real.pi) P = SpiralField.perTurnMultiplier P := by
proof body
Tactic-mode proof.
128 -- Use the closed-form step ratio, then cancel `(2π)` in the exponent.
129 have h :=
130 stepRatio_logSpiral_closed_form (r0:=r0) (θ:=θ) (Δθ:=(2 * Real.pi)) (P:=P) hr0
131 have hden : (2 * Real.pi : ℝ) ≠ 0 := by
132 have h2 : (2 : ℝ) ≠ 0 := by norm_num
133 exact mul_ne_zero h2 Real.pi_ne_zero
134 have hexp : ((P.kappa : ℝ) * (2 * Real.pi) / (2 * Real.pi)) = (P.kappa : ℝ) := by
135 simpa using (mul_div_cancel_right₀ (P.kappa : ℝ) hden)
136 simpa [SpiralField.perTurnMultiplier, hexp] using h
137
138/-- Discreteness of `kappa`: shifting `kappa` by an integer shifts the per-turn multiplier by a φ-power.
139
140This captures the “discrete pitch families” idea: per-turn growth is quantized in multiplicative
141steps of `φ^{d}` for `d : ℤ`.
142-/