Pith. sign in
module module high

IndisputableMonolith.Chemistry.BondAngles

show as:
view Lean formalization →

BondAngles supplies dimensionless bias proxies and cosine expressions for molecular bond angles, centered on tetrahedral preference derived from the RS phi constant. Flight geometry modelers cite these when constructing phi-tetrahedral scaffolds for log-spiral paths. The module is a collection of direct definitions and algebraic identities with no tactic proofs.

claimDefines functions such as $\text{tetra_bias}(x)$, $\text{angle_bias}$, $\text{optimalBondCosine}$, $\text{tetrahedral_cosine}$, $\text{tetrahedralAngleRadians}$, and $\text{tetra_angle_bounds}$ that encode dimensionless tetrahedral preference and angle cosines in RS units.

background

The module imports Constants (where $\tau_0 = 1$ tick) and Compat for project shims. It introduces bias proxies that quantify deviation from ideal angles using the self-similar fixed point $\phi$ from the forcing chain. Sibling definitions include linear_cosine, trigonal_cosine, and octahedral_formula_cosine, all expressed as algebraic reductions of the Recognition Composition Law applied to angular defects.

proof idea

This is a definition module, no proofs. Each declaration is an abbrev or def that directly encodes the cosine or bias formula; no lemmas or tactics are applied beyond Mathlib arithmetic.

why it matters in Recognition Science

Supplies the angle primitives required by the Flight.Geometry module, whose doc states it provides the purely geometric layer of the spiral-field propulsion model with the $\phi$-tetrahedral angle derived from Recognition Science axioms. No physical claims appear here; all geometry follows from the RS constant $\phi$.

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)