logSpiral_ne_zero
plain-language theorem explainer
The lemma establishes that the log-spiral function in the spiral field model is nonzero whenever the initial radius r0 is nonzero. Researchers deriving closed-form step ratios for discrete pitch families cite it to ensure the ratio expression is well-defined. The proof unfolds the spiral definition, invokes positivity of the golden ratio to obtain a positive power, and applies the multiplicative nonzero property.
Claim. Let $r_0, θ ∈ ℝ$ with $r_0 ≠ 0$ and let $P$ be a spiral-field parameter set containing scaling factor $κ$. Then the log-spiral $r_0 · φ^{(κ θ)/(2π)} ≠ 0$, where $φ$ is the golden ratio.
background
The Flight.Geometry module develops the purely geometric layer of the spiral-field model: the φ-tetrahedral angle and log-spiral rotor paths under φ-scaling. All constructions remain mathematical; no physical claims appear. The log-spiral is the product of initial radius with a real power of φ whose exponent is linear in the angle and the parameter κ. Upstream, positivity of φ is supplied by the Constants module.
proof idea
The tactic proof opens with classical, unfolds the logSpiral definition, obtains 0 < φ from phi_pos, deduces that the real power is positive (hence nonzero) via rpow_pos_of_pos, and concludes with mul_ne_zero applied to r0 and the power term.
why it matters
It directly supports the stepRatio_logSpiral_closed_form lemma, which supplies the closed-form step ratio depending only on Δθ and κ and serves as the kernel for discrete pitch families. The result is referenced in the FlightReport summary. Within Recognition Science it secures well-definedness of the φ-geometry scaffold, consistent with self-similar scaling from the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.