sixteen_is_2_fourth
plain-language theorem explainer
Sixteen equals two to the fourth power in the natural numbers. Researchers examining the Recognition Science cardinality spectrum cite this as an explicit witness that 16 belongs to the structured set generated from the cube primitives 2 and 3. The proof reduces to a single decision procedure that confirms the arithmetic identity.
Claim. $16 = 2^4$ in the natural numbers.
background
The module collects witnesses showing that cardinalities across the RS stack form the spectrum {2, 3, 4, 5, 6, 7, 8, 10, 12, 15, 16, 45, 70, 125, 216, 256, 3125, ...}. Each entry decomposes via multiplication, summation, or powers of the cube-generators {2, 3}, the configDim 5, and gap45. Sixteen appears here as the fourth power of the generator 2.
proof idea
The proof is a one-line wrapper that applies the decide tactic to verify the arithmetic equality directly.
why it matters
This supplies one concrete decomposition inside the C21 cardinality spectrum, confirming that the listed numbers arise from RS primitives rather than arbitrarily. It supports the module claim that the spectrum is structured, feeding the broader argument that RS produces a non-random numerical pattern from small generators.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.