twoFiftySix_decomp
plain-language theorem explainer
The equality 256 = 2^(2^3) holds in the natural numbers as one instance of spectrum-member decomposition under the Recognition Generators framework. Cross-domain researchers cite this when confirming that 256 reduces to the binary generator via iterated exponentiation on the set {2,3,5}. The proof is a one-line decision procedure that evaluates the expression directly.
Claim. $256 = 2^{2^3}$ where 2 is the binary-face generator.
background
The module proves decompositions for every integer in the RS cardinality spectrum using the generators G = {2, 3, 5} and the operations addition, multiplication, exponentiation and choose. The binary-face generator is defined as the constant 2. The module documentation explicitly lists the target decomposition 256 = 2^8 = 2^(2^3) among the enumerated spectrum members.
proof idea
The proof is a one-line wrapper that applies the decide tactic to evaluate the numerical equality by direct computation.
why it matters
This result instantiates the structural meta-claim of the Recognition Generators module that every spectrum member reduces to a polynomial expression in {2, 3, 5}. It supplies the concrete case 256 = 2^(2^3) required for the completeness statement over the enumerated spectrum members. No downstream theorems depend on it in the current graph.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.