at_dist_one
plain-language theorem explainer
The theorem asserts that the distance to the next noble gas closure at atomic number 85 equals one. Chemists applying Recognition Science phi-ladder scaling to atomic radii would cite this when confirming shell completion for astatine. The proof is a direct term-mode evaluation via native_decide on the arithmetic definition of distToNextClosure.
Claim. The distance from atomic number 85 to the next noble gas shell closure equals 1, where the distance function is defined as nextClosure(Z) minus Z.
background
In the Recognition Science treatment of atomic structure, radii follow phi-ladder scaling with shell number. The function distToNextClosure(Z) gives the atomic-number distance to the next noble gas, defined as nextClosure(Z) - Z. Noble gases occur exactly where valenceElectrons(Z) equals periodLength(Z), marking complete shells. The module establishes period trends (radii decrease with rising Z) and group trends (radii increase with new shells), plus lanthanide contraction from d/f filling.
proof idea
The proof is a one-line term wrapper that applies native_decide to evaluate the definition of distToNextClosure at 85, confirming the value 1 since the next closure lies at 86.
why it matters
This result verifies a concrete instance of shell closure inside the Chemistry.AtomicRadii module, supporting the RS prediction that noble gases exhibit local radius maxima. It aligns with the phi-ladder mechanism and the eight-tick octave structure for periodic organization. No downstream theorems are recorded, leaving the verification as a standalone check on the periodic-table primitives.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.