stepRatio_invariant_under_r0
The step ratio for a log-spiral path is unchanged when the base radius is scaled by any nonzero real factor. Propulsion modelers working with φ-scaled rotors cite the result to eliminate absolute size from pitch calculations. The proof is a one-line wrapper that applies the closed-form step-ratio expression to both radii and simplifies.
claimFor nonzero reals $c$ and $r_0$, and any parameters $P$, the step ratio satisfies stepRatio$(c r_0, θ, Δθ, P) =$ stepRatio$(r_0, θ, Δθ, P)$.
background
The Flight.Geometry module supplies the purely geometric layer for spiral-field propulsion, built on the Recognition Science constant φ. It defines log-spiral rotor paths whose radial growth is governed by a pitch parameter kappa drawn from SpiralField.Params. The upstream lemma stepRatio_logSpiral_closed_form supplies the explicit formula stepRatio = φ^(kappa · Δθ / (2π)) once r0 ≠ 0, showing that the ratio depends only on angular step and pitch.
proof idea
The proof is a one-line wrapper that invokes stepRatio_logSpiral_closed_form once for the scaled radius c·r0 and once for the original r0, then applies simp to equate the two identical closed-form expressions.
why it matters in Recognition Science
The lemma is cited inside the master theorem tesla_turbine_master to establish that step ratio depends only on pitch and angle, not base radius. It thereby completes one of the six geometric properties required for the φ-spiral engine model and aligns with the self-similar scaling fixed point in the T0–T8 forcing chain.
scope and limits
- Does not derive the closed-form expression for the step ratio.
- Requires both the scaling factor c and base radius r0 to be nonzero reals.
- Applies only to the log-spiral definition inside SpiralField.
- Does not address physical forces, material properties, or non-log-spiral paths.
Lean usage
apply stepRatio_invariant_under_r0formal statement (Lean)
114lemma stepRatio_invariant_under_r0
115 (c r0 θ Δθ : ℝ) (P : SpiralField.Params) (hc : c ≠ 0) (hr0 : r0 ≠ 0) :
116 SpiralField.stepRatio (c * r0) θ Δθ P = SpiralField.stepRatio r0 θ Δθ P := by
proof body
Term-mode proof.
117 have hcr0 : c * r0 ≠ 0 := mul_ne_zero hc hr0
118 simp [stepRatio_logSpiral_closed_form (r0:=c*r0) (θ:=θ) (Δθ:=Δθ) (P:=P) hcr0,
119 stepRatio_logSpiral_closed_form (r0:=r0) (θ:=θ) (Δθ:=Δθ) (P:=P) hr0]
120
121/-- Per-turn multiplier recovered as the special case `Δθ = 2π`.
122
123Mathematically: `r(θ+2π)/r(θ) = φ^kappa`.
124-/