phiTetrahedralAngle
plain-language theorem explainer
The declaration defines the tetrahedral angle in radians as arccos of negative one third, the value that arises in Recognition Science cost minimization for four-fold symmetric structures. Researchers assembling the spiral-field propulsion geometry cite it as the fixed primitive for rotor paths and log-spiral scaffolds. The definition is a direct assignment of the closed-form arccos expression taken from the real numbers library.
Claim. The tetrahedral angle is defined by the equation $θ = arccos(-1/3)$ (in radians).
background
The Flight.Geometry module supplies the purely geometric layer of the spiral-field propulsion model. It introduces the φ-tetrahedral angle as the optimal angle for 4-fold symmetric structures under the Recognition Science cost-minimization framework, together with log-spiral rotor paths and step-ratio lemmas, all derived from the RS constant φ. The module states that no physical claims are made here; all geometry follows from the φ-lattice structure. The angle is noted to be mathematically identical to the sp³ hybridization angle in chemistry and to appear in any tetrahedral geometry.
proof idea
The definition is a direct one-line assignment of the closed-form expression Real.arccos(-1/3). No lemmas or tactics are invoked; the value is taken verbatim from the standard real-arithmetic library.
why it matters
This definition supplies the geometric primitive that feeds the FlightReport status summary for the spiral-field propulsion subtheory. It fills the tetrahedral-angle slot in the φ-lattice structures, consistent with the Recognition Science derivation of constants from the forcing chain and the phi fixed point. The angle is presented as emerging from first principles via the φ-lattice and is used downstream in the display-level report that lists proved theorems for the Flight subtheory.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.