fluorine_gt_b
plain-language theorem explainer
Fluorine (Z=9) has higher electronegativity ranking than boron (Z=5) under the Recognition Science definition. Chemists using the phi-ladder model for period-wise trends would cite this when confirming that EN rises toward shell closure. The proof is a one-line term wrapper that unfolds the ranking, valence, and closure functions then reduces the inequality by norm_num.
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(5)$.
background
Electronegativity ranking is defined as valenceElectrons(Z) divided by periodLength(Z). Valence electrons equal Z minus the previous noble-gas closure; period length is the difference between next and previous closures. These functions encode shell structure so that higher valence fraction within a period signals stronger electron attraction, approximating the classical Mulliken relation via distance to closure.
proof idea
The proof is a one-line term wrapper. It applies simp to unfold enRanking together with valenceElectrons, periodLength, prevClosure and nextClosure, then invokes norm_num to compare the resulting concrete rationals.
why it matters
The result supplies a concrete instance of the module prediction that EN increases across a period as atoms approach noble-gas closure. It supports sibling statements such as en_increases_across_period and group_17_en_order. In the larger Recognition Science setting it ties chemical ordering to the same phi-ladder and eight-tick octave used for mass and force derivations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.