perTurn_ratio

formal source

 122
 123Mathematically: `r(θ+2π)/r(θ) = φ^kappa`.
 124-/
 125lemma perTurn_ratio
 126    (r0 θ : ℝ) (P : SpiralField.Params) (hr0 : r0 ≠ 0) :
 127    SpiralField.stepRatio r0 θ (2 * Real.pi) P = SpiralField.perTurnMultiplier P := by
 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-/
 143lemma kappa_discreteness (P : SpiralField.Params) (d : ℤ) :
 144    SpiralField.perTurnMultiplier { kappa := P.kappa + d }
 145      = SpiralField.perTurnMultiplier P * Real.rpow IndisputableMonolith.Constants.phi (d : ℝ) := by
 146  -- `φ > 0` so we can use `Real.rpow_add`.
 147  have hφpos : 0 < IndisputableMonolith.Constants.phi := IndisputableMonolith.Constants.phi_pos
 148  -- Expand both sides and use `rpow_add` on the exponent `(κ + d)`.
 149  simp [SpiralField.perTurnMultiplier, Real.rpow_add, hφpos, Int.cast_add]
 150
 151end SpiralLemmas
 152
 153end Geometry
 154end Flight
 155end IndisputableMonolith