angle_bias
plain-language theorem explainer
The theorem establishes that the tetrahedral bias proxy exceeds zero, confirming a positive preference for tetrahedral geometry over linear arrangements in the Recognition Science model. Chemists deriving optimal bond angles from J-cost minimization under phi-lattice constraints cite this result. The short tactic proof simplifies the definition, invokes the known inequality 1 less than phi, derives the reciprocal bound less than one, and applies positivity of subtraction.
Claim. $0 < 1 - 1/phi$, where $phi$ is the golden ratio constant satisfying the self-similar fixed point condition in Recognition Science.
background
The BondAngles module develops bond angles from the phi-lattice under the CH-014 heading. Tetrahedral bias is the dimensionless quantity 1 minus the reciprocal of phi, which quantifies deviation from linearity that favors tetrahedral geometry for four equivalent bonds. The module states that cos(theta) equals -1/(n-1) for n bonds, yielding -1/3 and theta approximately 109.47 degrees for the tetrahedral case, with a phi-connection via dodecahedron and inscribed tetrahedron.
proof idea
The tactic proof simplifies the bias definition to 1 minus one over phi. It obtains 1 less than phi from the Constants lemma one_lt_phi. Positivity of phi follows from lt_trans applied to a norm_num fact. The reciprocal inequality one over phi less than one is derived via div_lt_one. Finally sub_pos.mpr concludes the difference is positive.
why it matters
This declaration anchors the tetrahedral preference in the bond angle derivations of the Chemistry module. It supports the RS mechanism for minimizing J-cost while maintaining bond strength, connecting to the phi-lattice and dodecahedral relations in the module documentation. It aligns with forcing chain steps that fix phi as the self-similar point and D equals 3 dimensions, though the dependency graph lists no immediate parent theorems.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.