`stepRatio_logSpiral_closed_form`

proved

show as: view math explainer →

module: IndisputableMonolith.Flight.Geometry
domain: Flight
line: 68 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Flight.Geometry on GitHub at line 68.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

  65We assume `r0 ≠ 0` to avoid the definitional `if r₀ = 0 then 1` branch
  66in `SpiralField.stepRatio`.
  67-/
  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
  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

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.