Pith. sign in
module module high

IndisputableMonolith.Spiral.SpiralField

show as:
view Lean formalization →

SpiralField supplies the logarithmic spiral paths, J-cost functions, step ratios, and eight-gate neutrality predicates for Recognition Science flight models. It is imported by the Geometry, Schedule, and TeslaTurbine modules in the Flight domain. The module is a pure definitions collection built on the RS constant φ and the time quantum from Constants, with no internal theorems.

claimThe module defines the log-spiral $r(\theta) = a \phi^{\theta/(2\pi)}$ under $\phi$-scaling, the J-cost $J(x) = (x + x^{-1})/2 - 1$, per-turn multipliers, and eight-gate neutrality scores on the phi-ladder.

background

Recognition Science derives geometry from the forcing chain (T5 J-uniqueness, T6 phi fixed point, T7 eight-tick octave). The Constants module supplies the RS time quantum $\tau_0 = 1$ tick. SpiralField introduces sibling definitions: Params for spiral parameters, logSpiral for the geometric path, Jcost as the recognition cost function, stepRatio and sampledCost for discretization, eightGateNeutral and neutralityScore for the 8-window predicates, perTurnMultiplier, and ELStationary.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module feeds the purely geometric layer of Flight.Geometry (phi-tetrahedral angles and log-spiral rotor paths), the 8-tick control surface of Flight.Schedule, and the spiral engine model of Flight.TeslaTurbine. It supplies the phi-derived primitives required by the Recognition Science propulsion scaffold.

scope and limits

used by (3)

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

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (9)