noble_gas_bp_full_ordering
plain-language theorem explainer
The declaration establishes the complete increasing sequence of boiling points for the six noble gases from helium to radon. A chemist working in the Recognition Science framework would cite it to confirm the predicted polarizability trend from ledger fluctuations. The proof is a term-mode wrapper that directly composes five pairwise increase lemmas, each reduced by simplification on the explicit point values.
Claim. $ bp(2) < bp(10) < bp(18) < bp(36) < bp(54) < bp(86) $ where $ bp(Z) $ is the boiling point in kelvin of the noble gas with atomic number $ Z $, using the values assigned by the noble gas boiling point function.
background
The Van der Waals module models intermolecular forces via ledger fluctuations in the 8-tick octave that induce temporary dipoles, with polarizability rising for atoms with more electrons. The function nobleGasBoilingPoint : ℕ → ℝ supplies the explicit values 4.22 K (He, Z=2), 27.07 K (Ne, Z=10), 87.30 K (Ar, Z=18), 119.93 K (Kr, Z=36), 165.05 K (Xe, Z=54), and the corresponding value for radon (Z=86). Upstream results supply the five pairwise increase theorems, each proved by direct simplification and numerical comparison on these values.
proof idea
The term proof uses refine to build a five-element conjunction, then supplies each conjunct by exact application of the corresponding pairwise lemma: noble_gas_bp_increases_he_ne, noble_gas_bp_increases_ne_ar, noble_gas_bp_increases_ar_kr, noble_gas_bp_increases_kr_xe, and noble_gas_bp_increases_xe_rn.
why it matters
The theorem completes the numerical ordering required by the CH-013 derivation, confirming that van der Waals strength increases down the noble gas group as polarizability grows. It anchors the chemistry predictions inside the Recognition Science framework where the eight-tick ledger and T5 J-uniqueness generate the dispersion forces. No downstream theorems are recorded, leaving the result as a terminal verification step for the noble gas trend.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.