Pith. sign in
module module high

IndisputableMonolith.Flight.Geometry

show as:
view Lean formalization →

The Flight.Geometry module supplies the φ-tetrahedral angle and related spiral path definitions for use in propulsion models. Flight and gravity-bridge developers cite these primitives when constructing rotor geometries and 4-fold symmetric structures. It is a pure definition module whose objects are pulled directly from upstream J-cost minimization and φ-scaling constraints.

claimThe central object is the tetrahedral angle $\theta = \arccos(-1/3)$ obtained by minimizing J-cost for four equivalent bonds; auxiliary objects include logarithmic spiral step ratios and rotor pitch under eight-tick periodicity.

background

This module belongs to the Flight domain and imports the φ-lattice bond-angle derivation from Chemistry.BondAngles, the RS time quantum from Constants, and the spiral-field ansatz from Spiral.SpiralField. The tetrahedral angle is presented as the geometry that minimizes recognition cost for 4-fold symmetry and is identical to the sp³ hybridization angle. SpiralField supplies the variational structures for logarithmic spirals gated by φ-scaling and the eight-tick constraint.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The definitions feed the Flight facade and its downstream modules (GravityBridge, Report, VirtualRotor, TeslaTurbine, Searl). They supply the angular and path primitives required by the spiral-field propulsion scaffold whose intent is to keep lemmas provable while isolating physical hypotheses.

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)