isMagic
plain-language theorem explainer
isMagic marks a nuclear index Z as magic for a given cost function x when some aligned 8-window sum of x vanishes at an s at most Z. Nuclear shell-structure calculations in the Recognition framework cite this predicate to locate closure points on the phi-ladder without adjustable parameters. The definition is a direct existential statement that invokes the isClosure predicate on the octave cost proxy.
Claim. Let $x : ℕ → ℝ$ be a valence-cost function and let $Z ∈ ℕ$. Then $Z$ is magic if there exists $s ≤ Z$ such that the aligned 8-window sum of $x$ centered at $s$ equals zero.
background
The Nuclear.Octave module works inside the octave structure imported from RRF.Core.Octave, whose State type and strain functional supply the abstract setting for nuclear levels. The sibling predicate isClosure is defined by sum8 x i0 = 0 and is described as the magic-number test: an index is closed when the 8-window total cost is neutral. The cost function x is assembled from levelEnergy, a fit-free proxy built on the phi-ladder. Upstream Z from Masses.Anchor supplies the integer map that converts sector and charge into the nuclear index used by the anchor relation.
proof idea
The definition is a one-line existential wrapper. It asserts the existence of an s ≤ Z such that isClosure x s holds, where isClosure itself reduces directly to the vanishing of the sum8 function over the aligned 8-window.
why it matters
isMagic supplies the display-level test for nuclear magic numbers inside the eight-tick octave (T7) and the phi-ladder mass formula. It connects the Recognition Composition Law to shell closures by requiring a neutral 8-window on the cost proxy. No downstream theorems are recorded yet, but the predicate is positioned to feed nuclear mass predictions once the levelEnergy assembly is certified.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.