lower_z_more_remaining
plain-language theorem explainer
Within a shared period, an element with smaller atomic number Z1 has strictly larger distance to the next noble-gas closure than one with larger Z2. This encodes the across-period contraction of atomic radii predicted by Recognition Science phi-ladder scaling. Periodic-table modelers cite it to justify why radii shrink left to right. The proof is a one-line wrapper that unfolds the distance definition and invokes linear arithmetic.
Claim. Let $Z_1 < Z_2$ be atomic numbers sharing the same next noble-gas closure $N$, with $Z_1, Z_2$ both at or before $N$. Then the distance $N - Z_1$ exceeds $N - Z_2$.
background
Atomic radii follow phi-ladder scaling in the Chemistry.AtomicRadii module, with base radius proportional to phi raised to shell number. The nextClosure function returns the atomic number of the next noble gas after Z, defined piecewise as 2 for Z <= 2, 10 for Z <= 10, 18 for Z <= 18, and so on. distToNextClosure(Z) is defined as nextClosure(Z) - Z, giving the remaining steps to shell closure (zero at noble gases).
proof idea
The term proof applies simp to unfold distToNextClosure, reducing the goal to nextClosure Z1 - Z1 > nextClosure Z2 - Z2. The hypotheses Z1 < Z2 together with nextClosure Z1 = nextClosure Z2 then yield the strict inequality by subtraction, which omega discharges as a linear-arithmetic fact.
why it matters
This result formalizes the period trend stated in the module documentation: radii decrease across a period because increasing Z reduces remaining capacity to the next closure. It supplies the ordering principle used by sibling declarations such as normalizedRadius and shellRadiusProxy. In the broader Recognition Science setting it realizes the prediction that effective radius contracts with valence-electron count within each phi-scaled shell, consistent with the eight-tick octave structure for period lengths.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.