ljMinimumDistance
plain-language theorem explainer
The definition sets the Lennard-Jones equilibrium separation to 2^{1/6} σ. Chemists modeling dispersion forces in noble gases cite it when scaling intermolecular potentials from the 8-tick ledger. It is introduced as a direct algebraic formula with no lemmas or reductions required.
Claim. The equilibrium separation in the Lennard-Jones potential is $r = 2^{1/6} σ$.
background
The Van der Waals module derives weak intermolecular attractions from temporary dipole fluctuations induced by 8-tick ledger asymmetries. Polarizability grows with electron count and atomic size, producing London dispersion that scales as 1/r^6. The module imports constants and periodic table data to link these effects to observed boiling-point increases down the noble-gas group.
proof idea
The definition is a direct algebraic expression: 2 raised to the power 1/6 multiplied by the input parameter σ.
why it matters
This definition supplies the distance scale used by the downstream theorem lj_minimum_approx, which bounds the scaled minimum between 1.1 and 1.15. It completes the distance-dependence step in the RS mechanism for van der Waals forces, connecting the 8-tick ledger to 1/r^6 attraction. The parent results are the noble-gas boiling-point monotonicity statements that follow from increasing polarizability.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.