lj_minimum_approx
plain-language theorem explainer
The theorem shows that the Lennard-Jones minimum distance r_min satisfies 1.1 < r_min/σ < 1.15 for every σ > 0. Modelers of intermolecular forces in chemistry would cite the bound when approximating equilibrium separations in dispersion interactions. The proof unfolds the definition to isolate 2^{1/6}, splits the claim into two inequalities, and verifies each by direct sixth-power comparison together with the monotonicity of the real power function.
Claim. For every real number σ > 0, if r denotes the distance at which the Lennard-Jones potential reaches its minimum, then 1.1 < r/σ < 1.15.
background
The Lennard-Jones minimum distance is defined by the expression 2^{1/6} σ. The surrounding module derives van der Waals forces from ledger fluctuations in the eight-tick ledger that induce temporary dipoles, with interaction energy scaling as 1/r^6. The upstream definition states: 'The LJ potential has a minimum at r = 2^(1/6) * σ ≈ 1.122σ.' This numerical bound supplies a concrete interval around the exact factor 2^{1/6} for use in chemical approximations.
proof idea
The tactic proof first simplifies the ratio ljMinimumDistance σ / σ to 2^{1/6} by unfolding the definition and canceling σ. It then splits the conjunction and handles each side separately. For the lower bound it shows 1.1^6 < 2 by norm_num, applies Real.rpow_lt_rpow with the monotonicity of the sixth-root function, and simplifies the resulting expression via mul_one. The upper bound proceeds symmetrically by showing 2 < 1.15^6 and again invoking rpow_lt_rpow.
why it matters
The result supplies a verified numerical envelope for the Lennard-Jones minimum inside the van der Waals derivation (CH-013). It supports the module's claim that dispersion strength increases with polarizability and therefore with atomic size down the noble-gas group. The bound is consistent with the eight-tick ledger mechanism that produces the 1/r^6 London term; no downstream theorem yet consumes it directly, leaving the numerical interval available for later empirical checks against measured boiling points.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.