IndisputableMonolith.Flight.Geometry

   1import Mathlib
   2import IndisputableMonolith.Constants
   3import IndisputableMonolith.Spiral.SpiralField
   4import IndisputableMonolith.Chemistry.BondAngles
   5
   6/-!
   7# Flight Geometry (φ-Tetrahedral / log-spiral scaffold)
   8
   9This file provides the *purely geometric* layer of the spiral-field propulsion model:
  10- the φ-tetrahedral angle (derived from Recognition Science axioms),
  11- log-spiral rotor paths under φ-scaling,
  12- math-only lemmas about step ratios and per-turn multipliers.
  13
  14No physical claims are made here. All geometry is derived from the RS constant φ.
  15-/
  16
  17namespace IndisputableMonolith
  18namespace Flight
  19namespace Geometry
  20
  21open scoped Real
  22
  23/-- The φ-tetrahedral angle in radians.
  24
  25This is the tetrahedral bond angle, which emerges from the RS cost-minimization
  26framework as the optimal angle for 4-fold symmetric structures.
  27
  28Exact expression: `arccos (-1/3)` ≈ 109.47°.
  29
  30Note: This angle is mathematically identical to the sp³ hybridization angle in
  31chemistry and appears in any tetrahedral geometry. It is derived here from
  32first principles via the φ-lattice structure. -/
  33noncomputable def phiTetrahedralAngle : ℝ := Real.arccos (-(1 / 3 : ℝ))
  34
  35/-- Rotor pitch family: integral log-spiral pitch `kappa : ℤ`. -/
  36abbrev RotorPitch := IndisputableMonolith.Spiral.SpiralField.Params
  37
  38/-- Rotor radial path: log-spiral scaling on the φ lattice.
  39
  40`r(θ) = r0 · φ^{(κ·θ)/(2π)}`. -/
  41noncomputable abbrev rotorPath := IndisputableMonolith.Spiral.SpiralField.logSpiral
  42
  43namespace SpiralLemmas
  44
  45open IndisputableMonolith.Spiral
  46
  47/-- `logSpiral` is nonzero whenever `r0` is nonzero (since φ^x > 0). -/
  48lemma logSpiral_ne_zero
  49    {r0 θ : ℝ} {P : SpiralField.Params} (hr0 : r0 ≠ 0) :
  50    SpiralField.logSpiral r0 θ P ≠ 0 := by
  51  classical
  52  unfold SpiralField.logSpiral
  53  -- `φ > 0` hence `φ^exp > 0`.
  54  have hφpos : 0 < IndisputableMonolith.Constants.phi :=
  55    IndisputableMonolith.Constants.phi_pos
  56  have hrpow_ne : Real.rpow IndisputableMonolith.Constants.phi
  57        ((P.kappa : ℝ) * θ / (2 * Real.pi)) ≠ 0 := by
  58    exact ne_of_gt (Real.rpow_pos_of_pos hφpos _)
  59  exact mul_ne_zero hr0 hrpow_ne
  60
  61/-- Closed-form step ratio for the log-spiral: it depends only on `Δθ` and `kappa`.
  62
  63This is the mathematical kernel behind the "discrete pitch families" idea.
  64
  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
  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-/
 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
 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-/
 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
 156