fluorine_gt_li
plain-language theorem explainer
The declaration establishes that fluorine has a higher electronegativity ranking than lithium under the valence-fraction definition. Chemists using Recognition Science models would cite it to confirm the predicted ordering where fluorine ranks highest among light elements. The proof reduces the claim to arithmetic by unfolding the ranking into valence and period quantities then normalizing the numbers.
Claim. Let $r(Z)$ be the electronegativity ranking of atomic number $Z$, given by the ratio of valence electrons to period length. Then $r(9) > r(3)$.
background
Electronegativity ranking is defined as the ratio of valence electrons to the length of the current period, serving as a proxy for an atom's proximity to shell closure. Valence electrons equal the atomic number minus the previous noble-gas closure, while period length is the difference between next and previous closures. The module sets this ranking inside the broader φ-ladder scaling picture, where electronegativity rises toward closure and falls down groups, matching the listed predictions that fluorine reaches the highest value.
proof idea
The proof is a one-line wrapper that unfolds the ranking definition together with valence-electrons, period-length, previous-closure and next-closure auxiliaries, then applies numerical normalization to confirm the inequality for atomic numbers 9 and 3.
why it matters
This theorem supplies the first concrete ordering instance supporting the module's claim that fluorine possesses the highest electronegativity because it lies closest to closure in a small shell. It belongs to the family of fluorine-greater-than statements that instantiate the across-period increase prediction. In the Recognition Science framework it supplies chemical evidence for shell-structure dependence tied to the eight-tick octave and φ-based mass ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.