i_dist_one
plain-language theorem explainer
The declaration asserts that the distance from atomic number 53 to the next noble gas closure equals one. Researchers modeling atomic radii via RS shell structure would reference this instance when checking period-end distances. It follows immediately from evaluating the distToNextClosure definition at that specific atomic number.
Claim. The distance to the next noble gas closure for atomic number 53 equals 1, where the distance function subtracts the current atomic number from the atomic number of the subsequent closed shell.
background
In the Recognition Science treatment of atomic radii, shell structure is encoded through distances to noble gas closures. The function distToNextClosure(Z) computes nextClosure(Z) - Z, giving the number of elements until the next complete shell. This supports the predicted trends: radii decrease across a period as Z increases toward closure, and increase down a group with new shells. The module derives radii from φ-ladder scaling, with base radius proportional to φ raised to shell number, adjusted by screening. Upstream, distToNextClosure is defined directly from the nextClosure function in the PeriodicTable module.
proof idea
The proof applies native_decide to evaluate the concrete natural number computation for Z=53. This reduces the equality to a direct arithmetic check against the definition distToNextClosure(Z) = nextClosure(Z) - Z.
why it matters
This instance verifies the shell closure distance for iodine, immediately preceding xenon at Z=54. It anchors the RS predictions for atomic radii in the fifth period, where the model expects contraction toward the noble gas. While not yet referenced by downstream results, it exemplifies the concrete checks needed to connect the φ-ladder to observed periodic trends.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.