pith. machine review for the scientific record. sign in
module module high

IndisputableMonolith.Flight.Geometry

show as:
view Lean formalization →

Flight.Geometry supplies the φ-tetrahedral angle arccos(-1/3) together with logarithmic-spiral ratios for RS propulsion models. Researchers formalizing virtual rotors, Tesla-turbine analogs, or Searl candidates cite it for the exact angle and scaling invariants. The module consists of direct definitions plus elementary lemmas on invariance and discreteness.

claim$θ_{tet} = arccos(-1/3) ≈ 109.47°$ (tetrahedral angle from J-cost minimization); stepRatio and perTurn_ratio for φ-scaled logarithmic spirals under eight-tick gating.

background

The module sits in the Flight domain and imports Constants (τ₀ = 1 tick), Spiral.SpiralField (variational logarithmic spirals with φ-scaling and eight-tick gating), and Chemistry.BondAngles (tetrahedral angle derived by minimizing J-cost for four equivalent bonds around a central atom). It defines phiTetrahedralAngle as the exact arccos(-1/3) that matches the sp³ hybridization angle and arises from the φ-lattice. Additional objects include RotorPitch, rotorPath, stepRatio_logSpiral_closed_form, and kappa_discreteness.

proof idea

This is a definition module, no proofs. It contains direct definitions of the angle and spiral parameters together with short lemmas establishing logSpiral_ne_zero, stepRatio_invariant_under_r0, and perTurn_ratio.

why it matters in Recognition Science

Supplies the geometric primitives required by the Flight subtheory and is imported by Flight, GravityBridge, Report, VirtualRotor, TeslaTurbine, and the Searl candidate. It realizes the tetrahedral angle from the BondAngles derivation (CH-014) as a concrete building block for φ-spiral engines and connects directly to the eight-tick octave and φ-scaling constraints.

scope and limits

used by (6)

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

depends on (3)

Lean names referenced from this declaration's body.

declarations in this module (8)