fluorine_gt_c
plain-language theorem explainer
The theorem shows fluorine (Z=9) outranks carbon (Z=6) in the Recognition Science electronegativity ordering. Periodic-table modelers and chemists testing RS-derived shell trends would cite it for second-period comparisons. The proof is a one-line wrapper that unfolds the ranking definition into explicit arithmetic and evaluates the inequality by normalization.
Claim. Let $r(Z)$ be the electronegativity ranking $r(Z) = v(Z)/p(Z)$, where $v(Z)$ counts valence electrons beyond the prior noble-gas core and $p(Z)$ is the length of the current period. Then $r(9) > r(6)$.
background
The module treats electronegativity as a shell-filling fraction derived from noble-gas closures. The ranking function is defined as valence electrons divided by period length, so that atoms closer to the next closure receive higher scores within the same shell. Period length itself is nextClosure(Z) minus prevClosure(Z), with the closure functions supplying the discrete shell boundaries 2, 10, 18, 36, 54. These definitions come directly from the PeriodicTable module and implement the RS claim that EN increases across a period as atoms approach closure.
proof idea
The proof is a one-line wrapper. It applies simp to expand enRanking, valenceElectrons, periodLength, prevClosure and nextClosure into their explicit arithmetic expressions, then invokes norm_num to reduce the resulting numerical comparison 7/8 > 4/8 to a verified inequality.
why it matters
The result supplies one concrete instance of the ordering predictions listed in the module header, confirming that EN rises toward fluorine in the second period. It therefore supports the broader RS mechanism EN ~ distToNextClosure^{-1} and is consistent with the eight-tick octave structure of shell closures. No downstream theorems currently depend on it, but the sibling declarations en_increases_across_period and group_17_en_order rely on the same ranking function.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.