kappa_discreteness
Shifting the stiffness kappa in a SpiralField.Params record by an integer d multiplies the per-turn multiplier by phi to the power d. Workers modeling discrete pitch families in log-spiral rotor geometry cite the result to justify quantized multiplicative steps. The proof is a short tactic sequence that first pulls positivity of phi from the constants module then applies simp to the perTurnMultiplier definition together with rpow_add and integer casting.
claimLet $P$ be a spiral-field parameter record with stiffness parameter $κ$. For any integer $d$, the per-turn multiplier at stiffness $κ + d$ equals the per-turn multiplier at $κ$ multiplied by $φ^d$, where $φ$ is the golden-ratio constant.
background
The Flight.Geometry module supplies the purely geometric layer for spiral-field propulsion: the phi-tetrahedral angle and log-spiral rotor paths whose step ratios are derived from the Recognition Science constant phi. SpiralField.Params is the parameter record holding the stiffness kappa (along with auxiliary geometric values). The perTurnMultiplier function returns phi raised to the supplied kappa value. Upstream results include the positivity lemma for phi and the minimal Params structures imported from ILG and CPM modules.
proof idea
The tactic proof first obtains positivity of phi via the Constants.phi_pos lemma. It then calls simp on the perTurnMultiplier definition, the real exponentiation additivity rule rpow_add, the positivity hypothesis, and the integer-to-real cast additivity Int.cast_add.
why it matters in Recognition Science
The lemma encodes the discrete pitch families idea inside the spiral geometry scaffold and is referenced by the FlightReport display summary. It fills the step that quantizes per-turn growth in multiplicative phi-powers, consistent with the phi fixed-point construction. No open scaffolding questions are closed here.
scope and limits
- Does not prove physical realizability of any rotor path.
- Does not treat non-integer shifts of kappa.
- Does not incorporate material or energetic constraints.
formal statement (Lean)
143lemma kappa_discreteness (P : SpiralField.Params) (d : ℤ) :
144 SpiralField.perTurnMultiplier { kappa := P.kappa + d }
proof body
Tactic-mode proof.
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