londonDispersionProxy
plain-language theorem explainer
The proxy computes a London dispersion interaction between atoms of atomic numbers Z1 and Z2 at separation r, returning zero for non-positive r and otherwise the product of polarizabilities divided by r to the sixth. Chemists modeling noble-gas boiling-point trends within the Recognition framework would cite this expression when deriving the 1/r^6 scaling. The definition is a direct conditional that multiplies the outputs of the polarizability proxy and applies the inverse sixth-power law.
Claim. The London dispersion proxy is given by $f(Z_1,Z_2,r)=0$ if $r≤0$ and $f(Z_1,Z_2,r)=α(Z_1)α(Z_2)/r^6$ otherwise, where $α(Z)$ is the polarizability proxy that increases with the period of atomic number $Z$.
background
The Van der Waals module derives intermolecular forces from ledger fluctuations in the eight-tick cycle that create temporary dipoles. Polarizability grows with atomic size because outer shells contain more electrons; the polarizabilityProxy returns the real number equal to the period of Z. The module states that dispersion strength therefore increases down the noble-gas group and follows the classical dipole-dipole distance dependence of 1/r^6.
proof idea
One-line wrapper that applies polarizabilityProxy to each atomic number, multiplies the results, and divides by r^6, returning zero for non-positive r.
why it matters
This definition supplies the explicit 1/r^6 term required by the CH-013 Van der Waals derivation. It is invoked directly by the theorem london_decreases_with_distance, which establishes monotonic decay with separation. In the Recognition framework the expression realizes the prediction that interaction energy follows from 8-tick ledger fluctuations and supports the observed increase in noble-gas boiling points with polarizability.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.