kappa_discreteness
plain-language theorem explainer
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.
Claim. Let $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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.