fluorine_gt_be
plain-language theorem explainer
The theorem establishes that the electronegativity ranking for fluorine exceeds that for beryllium under the valence-fraction definition. Chemists applying Recognition Science scaling to periodic trends would cite it to confirm the predicted rise in ranking across the second period. The proof reduces the claim to arithmetic by unfolding the periodic functions and evaluating the resulting numbers.
Claim. Let $r(Z)$ denote the electronegativity ranking of element $Z$, defined as the ratio of valence electrons to period length. Then $r(9) > r(4)$.
background
Electronegativity is modeled here via a simplified ranking that tracks distance to shell closure. The enRanking function returns the ratio of valence electrons (electrons past the prior noble-gas core) to the length of the current period. Period length itself is the difference between consecutive noble-gas closures given by nextClosure and prevClosure.
proof idea
The proof is a one-line term wrapper that applies simp to unfold enRanking together with valenceElectrons, periodLength, prevClosure and nextClosure, then invokes norm_num to discharge the resulting numerical inequality.
why it matters
The result fills the concrete ordering prediction that fluorine ranks highest among light elements because it sits closest to the next closure. It supports the module's claim that EN rises across a period as atoms approach shell completion, consistent with the Recognition Science mechanism of EN scaling with inverse distance to closure. No downstream theorems depend on it yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.