phiTetrahedralAngle
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not derive the angle from the forcing chain T0-T8.
- Does not prove that the angle minimizes any Recognition cost function.
- Does not connect the angle to the eight-tick octave or to D=3.
- Does not supply numerical approximations or error bounds.
formal statement (Lean)
33noncomputable def phiTetrahedralAngle : ℝ := Real.arccos (-(1 / 3 : ℝ))
proof body
Definition body.
34
35/-- Rotor pitch family: integral log-spiral pitch `kappa : ℤ`. -/