Tier8Cert
plain-language theorem explainer
Empty certificate carrier for Tier-8 nuclear physics claims in Recognition Science. Its verification predicate packages four arithmetic identities: magic numbers from the eight-tick shell, alpha-particle double closure, 3D cube edge/face counts, and the fusion-window period. Nuclear-physics certification work cites this bundle. The companion proof discharges every conjunct by numeric simplification of cube geometry and powers of two.
Claim. A unit certificate type whose verification predicate asserts four nuclear identities: magic-number relations $2=2^1$, $8=2^3$, $20=2^3+3\cdot 2^2$; alpha-particle double closed shell $2=2$ and $4=2\cdot 2$; three-dimensional hypercube counts $\mathrm{edges}(3)=12$ and $\mathrm{faces}(3)=6$; and eight-tick fusion period $8=2^3$. The predicate holds for every certificate instance.
background
Tier 8 is the nuclear-physics certification layer of the Recognition Science monolith. The module bundles machine-checked claims on magic numbers, binding structure, alpha stability, and nucleosynthesis windows, with zero sorry and zero axioms.
The eight-tick octave (forcing-chain T7) is the fundamental evolution period: one octave equals $2^3$ ticks. Magic numbers ${2,8,20,\ldots}$ are read off shell capacities built from powers of two and the same octave. Spatial dimension $D=3$ (forcing-chain T8) fixes the 3-cube: edges $D\cdot 2^{D-1}=12$ and faces $2D=6$, which the certificate treats as the geometric skeleton of 3D nuclear structure.
Upstream definitions supply the arithmetic: cube_edges d = d * 2^(d-1), cube_faces d = 2*d, and the tick/octave constants. The alpha-particle claim is the double closed shell $N=Z=2$, written as the trivial identities $2=2$ and $4=2\cdot 2$.
proof idea
The structure itself is an empty carrier (no fields). The real content is the simp-normalized verification predicate: a four-way conjunction of pure Nat equalities.
The companion theorem verified_any proves the predicate for every certificate by a single refine that splits the nested conjunctions, then simp unfolding cube_edges, cube_faces, and D, followed by norm_num on each residual arithmetic goal. No external lemmas beyond those definitions are required; every conjunct is a closed numeric identity.
why it matters
This certificate is the Lean-side seal for the Tier-8 nuclear package listed in the module doc: magic numbers from 8-tick shells, alpha-particle stability as double closed shell, $D=3$ forcing 3D nuclear geometry, and fusion windows fixed by the octave period.
It sits on the forcing-chain landmarks T7 (eight-tick octave, period $2^3$) and T8 ($D=3$ spatial dimensions). The cube edge/face counts are the same hypercube combinatorics used in the alpha-derivation stack, so the nuclear layer reuses the geometric constants already forced for electromagnetism.
No downstream consumers are wired yet (used_by is empty). The module explicitly leaves open individual per-nucleus binding energies, neutron-lifetime channel dynamics, and double-beta matrix elements; those remain outside the certificate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.