nobleGasBoilingPoint
plain-language theorem explainer
Boiling points of noble gases are assigned explicitly in Kelvin as a function of atomic number, with values 4.22 K for He, 27.07 K for Ne, 87.30 K for Ar, 119.93 K for Kr, 165.05 K for Xe and 211.4 K for Rn. Researchers modeling van der Waals trends inside Recognition Science cite these numbers to anchor the predicted monotonic increase down the group. The definition is a direct pattern match on atomic numbers with no lemmas or reductions.
Claim. The function $b : ℕ → ℝ$ returns the boiling point in Kelvin of the noble gas with atomic number $n$, where $b(2) = 4.22$, $b(10) = 27.07$, $b(18) = 87.30$, $b(36) = 119.93$, $b(54) = 165.05$, $b(86) = 211.4$, and $b(n) = 0$ otherwise.
background
The Van der Waals module treats boiling points as empirical anchors for dispersion forces generated by eight-tick ledger fluctuations that induce temporary dipoles. Polarizability grows with electron count, so interaction strength rises down the group and scales as $1/r^6$. The upstream shell definition supplies the energy scale: noncomputable def shell (n : Nat) : ℝ := Constants.E_coh * block_capacity n, with the identity that shell scale equals E_coh times capacity at each n.
proof idea
This is a direct definition by pattern matching on the six noble-gas atomic numbers, returning the listed Kelvin values or zero for all other inputs. No lemmas are invoked and no tactics are applied; the body is the data itself.
why it matters
The definition supplies the concrete values required by the six downstream ordering theorems that prove nobleGasBoilingPoint 2 < 10 < 18 < 36 < 54 < 86. It supplies the empirical input for the CH-013 claim that van der Waals strength increases with atomic size via polarizability. In the framework it links the eight-tick ledger mechanism directly to observable chemistry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.