four_decomp
plain-language theorem explainer
The equality 4 equals the square of the binary-face generator holds in the natural numbers. Cross-domain decompositions of the Recognition Science spectrum cite this when confirming that listed cardinalities reduce to operations on the set {2,3,5}. The proof is a direct decision procedure after substitution of the generator definition.
Claim. $4 = 2^2$ where 2 is the binary-face generator.
background
The module establishes that every integer in the RS cardinality spectrum reduces to a small set of operations on the generators G = {2,3,5}, labeled binary face, spatial dimension, and configDim. Operations include addition, multiplication, exponentiation, and binomial coefficients. The explicit example 4 = 2² appears in the module documentation as one of the spectrum members enumerated in C21.
proof idea
One-line wrapper that applies the decide tactic to the equality after unfolding the definition of the binary-face generator.
why it matters
This decomposition feeds the recognitionGeneratorsCert that certifies the full set of generators and their distinctness. It directly implements the C27 meta-claim that no spectrum member lies outside polynomials in {2,3,5}. The result sits inside the cross-domain layer that supports the forcing chain from T0 to T8 and the phi-ladder mass formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.