pith. sign in
module module high

IndisputableMonolith.Chemistry.BondAngles

show as:
view Lean formalization →

Chemistry.BondAngles supplies definitions for a dimensionless bias proxy favoring tetrahedral geometry plus cosine and angle functions for linear, trigonal, tetrahedral and octahedral cases. Flight.Geometry models cite it to obtain the phi-derived tetrahedral angle. The module contains only definitions with no theorems or proofs.

claimDimensionless bias proxy for tetrahedral preference $b_t$; optimal bond cosine $c$; tetrahedral angle $ heta_r$ (radians) and $ heta_d$ (degrees); cosine identities for linear, trigonal ($2\pi/3$), tetrahedral and octahedral geometries.

background

The module belongs to the Chemistry domain and imports Mathlib together with Compat (project-wide shims) and Constants (where the RS time quantum is defined as $\tau_0 = 1$ tick). Its central object is the dimensionless bias proxy for tetrahedral preference, accompanied by explicit cosine values and angle bounds for the standard molecular geometries.

These definitions sit upstream of any geometric construction that requires the tetrahedral angle derived from Recognition Science axioms. No physical content or energy relations are introduced.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the angle primitives required by Flight.Geometry, whose doc-comment describes the purely geometric layer of the spiral-field propulsion model built from the phi-tetrahedral angle and log-spiral paths under phi-scaling. It therefore closes the chemistry-to-geometry interface inside the Recognition framework.

scope and limits

used by (1)

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

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (15)