lennardJonesPotential
plain-language theorem explainer
The declaration defines the Lennard-Jones potential as a real-valued function of parameters ε, σ and separation r. Researchers modeling intermolecular forces within Recognition Science cite it to quantify London dispersion between atoms, especially noble gases whose boiling points rise with polarizability. The definition is a direct piecewise implementation that returns zero for non-positive r and applies the algebraic form 4ε[(σ/r)^12 − (σ/r)^6] otherwise.
Claim. The Lennard-Jones potential is $U(r) = 4ε[(σ/r)^{12} − (σ/r)^6]$ for $r > 0$ and $U(r) = 0$ otherwise.
background
Van der Waals forces in this module arise from ledger fluctuations in the eight-tick cycle that induce temporary dipoles, with polarizability growing for larger atoms and producing the characteristic 1/r^6 attraction. The module states that interaction energy follows the London dispersion form and that noble-gas boiling points increase down the group as a direct consequence. Upstream the has class supplies a spectral-peak model ω_k = ω_0 · φ^k used for ranking mineral classes by rung, providing a spectroscopic anchor for the same phi-scaling that appears in the chemistry layer.
proof idea
The definition is a primitive piecewise expression: it returns the constant 0 when r ≤ 0 and otherwise evaluates the closed-form expression 4 * ε * ((σ / r) ^ 12 - (σ / r) ^ 6). No lemmas or tactics are invoked; the body is the complete implementation.
why it matters
This definition supplies the explicit potential required by the CH-013 van der Waals derivation. It feeds the sibling results on noble-gas boiling-point trends that increase from He to Rn, consistent with the eight-tick octave and polarizability growth. The r^{-6} term matches the dipole-dipole mathematics predicted by ledger fluctuations, while the r^{-12} repulsion encodes Pauli exclusion at short range. No open scaffolding questions are attached.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.