twoFiftySix_is_power_of_2cube
plain-language theorem explainer
256 equals 2 raised to the power of 2 cubed in the natural numbers. Researchers working on the Recognition Science cardinality spectrum cite this witness to place 256 inside the structured list generated from the cube generators 2 and 3 together with the eight-tick period. The proof is a one-line decision procedure that confirms the arithmetic identity directly.
Claim. $256 = 2^{2^3}$ in the natural numbers.
background
The CrossDomain.CardinalitySpectrum module collects explicit numerical witnesses showing that cardinalities of canonical RS domain types form a structured spectrum rather than an arbitrary collection. The listed values decompose via multiplication, summation, or exponentiation from the small cube-generators {2, 3}, the configuration dimension 5, and the gap of 45. The eight-tick octave supplies the period 2^3 that appears in several exponents, including the one for 256 = 2^8.
proof idea
The proof is a one-line wrapper that invokes the decide tactic on the equality 256 = 2^(2^3). No lemmas from the upstream tick or gap definitions are required because the arithmetic is decidable.
why it matters
This supplies a concrete member of the RS cardinality spectrum, confirming that 256 = 2^8 fits the pattern generated from the cube generators and the eight-tick octave (T7). It supports the module claim that every listed cardinality admits a decomposition into RS primitives. The declaration has no recorded downstream uses and touches no open scaffolding questions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.