twoFiftySix_decomp
plain-language theorem explainer
The equality shows 256 equals the binary-face generator raised to that generator cubed. Recognition Science spectrum work cites this to confirm 256 belongs to the set generated by {2,3,5} under the listed operations. The proof is a direct decision procedure that evaluates the numerical identity.
Claim. $256 = 2^{(2^3)}$ where 2 denotes the binary-face generator.
background
The module proves that every integer in the RS cardinality spectrum reduces to a polynomial expression in the generators {2,3,5} using addition, multiplication, exponentiation and binomial coefficients. G2 is fixed as the binary-face generator equal to 2. The module documentation lists 256 explicitly as one such member via the decomposition 256 = 2^8 = 2^(2^3).
proof idea
The declaration is a one-line wrapper that applies the decide tactic to verify the equality in the natural numbers.
why it matters
This entry completes one case in the C27 enumeration of spectrum members under the {2,3,5} generators. It aligns with the eight-tick octave (T7) because 256 = 2^8. No downstream theorems are recorded.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.