stepRatio_logSpiral_closed_form
The lemma gives a closed-form expression for the step ratio of a log-spiral path: the ratio equals phi raised to kappa times delta theta over 2 pi, independent of the starting radius and angle. Flight-geometry researchers working on discrete pitch families cite it as the algebraic kernel that converts continuous spiral scaling into discrete multipliers. The proof unfolds the stepRatio definition, invokes the non-zero lemma for the spiral, splits the exponent via ring, applies rpow_add, and cancels common factors with field_simp.
claimLet $r_0, theta, Delta theta in mathbb{R}$ with $r_0 neq 0$, and let $P$ be a spiral-field parameter record whose kappa component is a real number. Then the step ratio along the log-spiral satisfies $r(theta + Delta theta)/r(theta) = phi^{kappa Delta theta / (2 pi)}$, where $phi$ denotes the Recognition Science constant.
background
The module supplies the purely geometric layer of the spiral-field model: phi-tetrahedral angles and log-spiral rotor paths whose radii scale by powers of phi. The function logSpiral r0 theta P returns r0 times phi raised to (kappa times theta over 2 pi); stepRatio is defined as the ratio of two such values, with a special case returning 1 when r0 equals zero. The upstream lemma logSpiral_ne_zero states that logSpiral r0 theta P is nonzero whenever r0 is nonzero, because phi to any real power remains positive.
proof idea
The tactic proof first unfolds stepRatio and applies logSpiral_ne_zero to discharge the zero-radius branch, then simplifies. It splits the combined exponent with a ring identity, invokes Real.rpow_add on the positive phi constant to factor the power, rewrites the factored form, and finishes with field_simp to cancel the common r0-powered term.
why it matters in Recognition Science
This closed form is the direct parent of perTurn_ratio (the special case Delta theta equals 2 pi recovers phi to the kappa) and of kappa_one_step_ratio (the kappa equals 1 instance). It supplies the algebraic engine behind discrete pitch families in the Flight subtheory and sits inside the phi-scaling scaffold that descends from the self-similar fixed point T6. No open scaffolding remains; the lemma is fully proved.
scope and limits
- Does not assert physical realizability of any rotor path.
- Does not cover the r0 equals zero definitional branch.
- Does not derive the value of kappa from axioms.
- Does not address non-logarithmic spiral families.
Lean usage
have h := stepRatio_logSpiral_closed_form r0 theta Delta theta P hr0formal statement (Lean)
68lemma stepRatio_logSpiral_closed_form
69 (r0 θ Δθ : ℝ) (P : SpiralField.Params) (hr0 : r0 ≠ 0) :
70 SpiralField.stepRatio r0 θ Δθ P
71 = Real.rpow IndisputableMonolith.Constants.phi ((P.kappa : ℝ) * Δθ / (2 * Real.pi)) := by
proof body
Tactic-mode proof.
72 classical
73 -- Unfold the definition and discharge the `if` branch *before* unfolding `logSpiral`.
74 unfold SpiralField.stepRatio
75 have hr0path : SpiralField.logSpiral r0 θ P ≠ 0 :=
76 logSpiral_ne_zero (r0:=r0) (θ:=θ) (P:=P) hr0
77 simp [hr0path]
78
79 -- Now we are proving the ratio identity:
80 -- r(θ+Δθ)/r(θ) = φ^{κΔθ/(2π)}.
81 have hφpos : 0 < IndisputableMonolith.Constants.phi := IndisputableMonolith.Constants.phi_pos
82 simp [SpiralField.logSpiral]
83 -- Split the exponent using `rpow_add`.
84 have hexp :
85 ((P.kappa : ℝ) * (θ + Δθ) / (2 * Real.pi))
86 = ((P.kappa : ℝ) * θ / (2 * Real.pi)) + ((P.kappa : ℝ) * Δθ / (2 * Real.pi)) := by
87 ring
88 have hadd :
89 Real.rpow IndisputableMonolith.Constants.phi ((P.kappa : ℝ) * (θ + Δθ) / (2 * Real.pi))
90 =
91 Real.rpow IndisputableMonolith.Constants.phi ((P.kappa : ℝ) * θ / (2 * Real.pi))
92 * Real.rpow IndisputableMonolith.Constants.phi ((P.kappa : ℝ) * Δθ / (2 * Real.pi)) := by
93 simpa [hexp] using
94 (Real.rpow_add hφpos
95 ((P.kappa : ℝ) * θ / (2 * Real.pi))
96 ((P.kappa : ℝ) * Δθ / (2 * Real.pi)))
97 have hA_ne :
98 Real.rpow IndisputableMonolith.Constants.phi ((P.kappa : ℝ) * θ / (2 * Real.pi)) ≠ 0 := by
99 exact ne_of_gt (Real.rpow_pos_of_pos hφpos _)
100 have haddPow :
101 IndisputableMonolith.Constants.phi ^ ((P.kappa : ℝ) * (θ + Δθ) / (2 * Real.pi))
102 =
103 IndisputableMonolith.Constants.phi ^ ((P.kappa : ℝ) * θ / (2 * Real.pi))
104 * IndisputableMonolith.Constants.phi ^ ((P.kappa : ℝ) * Δθ / (2 * Real.pi)) := by
105 simpa using hadd
106 -- Cancel the common factors.
107 rw [haddPow]
108 field_simp [hr0, hA_ne, mul_assoc, mul_left_comm, mul_comm]
109
110/-- The step ratio is invariant under scaling the base radius `r0`.
111
112This follows immediately from the closed-form identity.
113-/