alkali_halogen_ionic
plain-language theorem explainer
Alkali metals paired with halogens satisfy the ionic bond condition because their electronegativity proxies differ by more than the 0.02 threshold. Researchers deriving chemical bonding rules from atomic shell closure in Recognition Science would reference this result. The proof reduces the statement to thirty explicit numerical comparisons by exhaustive case analysis on the six alkali and five halogen atomic numbers, each verified by norm_num after unfolding the electronegativity proxy definition.
Claim. For all natural numbers $Z_a$ and $Z_h$ such that $Z_a$ belongs to the alkali metal list and $Z_h$ belongs to the halogen list, the absolute difference between the electronegativity proxy of $Z_a$ and that of $Z_h$ exceeds the ionic threshold, so the pair forms an ionic bond.
background
In the IonicBond module, alkali membership holds for the explicit list of six atomic numbers while halogen membership holds precisely when the distance to closure equals one. The electronegativity proxy is the real-valued function that multiplies the reciprocal of one plus the distance to next closure by the reciprocal of the shell number, where shell number equals the period plus one. The module documentation frames ionic bonding as electron transfer driven by the eight-tick shell closure mechanism, with net energy set by ionization cost minus electron affinity gain and stabilized by lattice Madelung energy.
proof idea
The tactic proof first simplifies the target to the electronegativity difference exceeding the threshold. It then extracts non-zero facts for both atomic numbers from the list membership hypotheses. Exhaustive rcases on the six alkali cases and five halogen cases expands every electronegativity proxy expression; norm_num then discharges each of the resulting thirty concrete real inequalities.
why it matters
The theorem supplies the basic ionic formation rule inside the chemistry module and directly instantiates the eight-tick closure drive stated in the module documentation. It thereby links electronegativity ordering to the T7 octave and the phi-ladder radii used throughout Recognition Science. No downstream theorems yet consume the result, leaving open its use in the lattice energy proxies such as madelungNaCl.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.