pith. machine review for the scientific record. sign in
structure definition def or abbrev high

Params

show as:
view Lean formalization →

The Params structure supplies the integer pitch parameter kappa for logarithmic spiral fields under phi scaling. Researchers modeling discrete rotor pitches or spiral wavefields in flight geometry cite this record. It is introduced as a bare structure with Repr and DecidableEq instances to support downstream algebraic manipulations of the per-turn multiplier.

claimA record consisting of a single integer field $k$ that parametrizes the logarithmic spiral radius $r(θ) = r_0 · φ^{(k · θ)/(2π)}$.

background

The Spiral.SpiralField module supplies a variational ansatz for logarithmic spiral fields under φ-scaling and an eight-tick gating constraint. This file defines only basic structures and helpers; no proofs are required to compile. The integer kappa is drawn from upstream phi-ladder conventions such as the exponent offsets in Masses.Anchor.r0 and the power definitions in Materials.ThermalConductivityRegimesFromPhiLadder.kappa.

proof idea

This is a structure definition that introduces the kappa field directly. The deriving clauses supply automatic instances for representation and decidable equality. No lemmas or tactics are invoked.

why it matters in Recognition Science

This declaration supplies the core parameter for the RotorPitch abbrev and feeds lemmas such as kappa_discreteness, perTurn_ratio, and stepRatio_logSpiral_closed_form in Flight.Geometry. It realizes the discrete pitch families idea by tying spiral growth to integer multiples on the phi-ladder, consistent with T7 eight-tick octave and the Recognition Science phi-scaling. It touches the open question of closure under the Recognition Composition Law.

scope and limits

formal statement (Lean)

  21structure Params where
  22  kappa : ℤ
  23  deriving Repr, DecidableEq
  24
  25/- Log-spiral radius with base scale r0>0 and angle θ (radians):
  26   r(θ) = r0 · φ^{(κ · θ)/(2π)}. -/

used by (37)

From the project-wide theorem graph. These declarations reference this one in their body.

… and 7 more

depends on (9)

Lean names referenced from this declaration's body.