group_17_en_order
plain-language theorem explainer
The theorem establishes that shell numbers increase strictly across fluorine (Z=9), chlorine (Z=17), and bromine (Z=35). Chemists using Recognition Science to model electronegativity would cite this ordering to ground the claim that electron attraction weakens with larger shells. The proof is a one-line native_decide evaluation of the period-derived shell numbers.
Claim. Let $n(Z)$ denote the shell number of atomic number $Z$. Then $n(9) < n(17) ∧ n(17) < n(35)$.
background
Shell number is defined as periodOf Z + 1 and serves as a 1-indexed proxy for atomic radius scaling, with raw radius given by φ raised to the shell number. Higher shells therefore correspond to larger base radii. The module sets electronegativity as inversely proportional to distance to next shell closure, modulated by this shell number, so that EN is expected to fall as shells enlarge down any group.
proof idea
The proof is a term-mode native_decide that directly evaluates the two inequalities once shellNumber is expanded to periodOf Z + 1.
why it matters
The result supplies the concrete ordering needed to support the module's prediction that EN decreases down a group because larger shells reduce attraction. It belongs to the family of statements that instantiate the φ-ladder scaling for chemistry and sits alongside sibling results such as enRanking and en_increases_across_period. No downstream theorems yet depend on it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.