nuclearPhysicsDepthCert
plain-language theorem explainer
This definition assembles a certificate confirming exactly five nuclear structure categories and the second magic number equal to eight. Nuclear physicists modeling binding energies via the Recognition Science phi-ladder would cite it to anchor the five-category decomposition. The construction directly supplies the two required fields from prior decide lemmas on cardinality and exponentiation.
Claim. The certificate requires that the cardinality of the nuclear structure category type equals 5 and that the second magic number equals $2^3$.
background
NuclearPhysicsDepthCert is a structure requiring two facts: the cardinality of the nuclear structure category type is 5, and the second magic number equals 8. The module sets the local context with five categories (single-particle, collective, rotation, vibration, cluster) and five force carriers (gluons, W+, W-, Z0, photon). Upstream, the cardinality theorem is proved by decide, and the equality to 2 cubed is likewise proved by decide.
proof idea
This is a definition that constructs the structure instance by assigning the five-categories field to the result of the cardinality theorem and the second-magic-cube field to the result of the equality theorem. Both upstream results are obtained via the decide tactic.
why it matters
This certificate anchors the nuclear depth analysis in Recognition Science by confirming the five-category structure and the 2^3 magic number. It aligns with the eight-tick octave in the forcing chain and supplies a Lean-verified fact for the B7 nuclear module. No downstream uses appear in the dependency graph.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.