twoFiftySix_is_power_of_2cube
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 in Recognition Science
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.
scope and limits
- Does not derive 256 from the Recognition Composition Law or J-uniqueness.
- Does not connect the cardinality to spatial dimension D=3 beyond the exponent.
- Does not supply a physical model for the power-set interpretation of 256.
- Does not prove that every spectrum member admits an equally simple proof.
formal statement (Lean)
88theorem twoFiftySix_is_power_of_2cube : (256 : ℕ) = 2 ^ (2^3) := by decide
proof body
Term-mode proof.
89
90/-- 360 = 8·45 (full turn = tick × gap). -/