seventy_decomp
plain-language theorem explainer
The identity 70 equals the binomial coefficient of 8 choose 4 holds when 8 and 4 are written as powers of the binary generator 2. Researchers verifying the Recognition Science cardinality spectrum would cite this to confirm 70 fits the pattern of binomial coefficients generated from {2, 3, 5}. The proof is a direct computational check via the decide tactic on the binomial evaluation.
Claim. $70 = {2^3} choose {2^2}$
background
The RecognitionGenerators module defines the generators G = {2, 3, 5} with G2 as the binary face set to 2. Spectrum members are reduced via addition, multiplication, exponentiation and binomial coefficients, with the module proving all enumerated cases from C21 reduce to polynomials in these generators. The declaration depends only on the G2 definition.
proof idea
The proof is a one-line wrapper that invokes the decide tactic to evaluate the binomial coefficient and confirm numerical equality.
why it matters
This declaration supplies one concrete decomposition in the module's list, supporting the structural meta-claim that every RS spectrum integer is generated by operations on {2, 3, 5}. It aligns with the eight-tick octave (2^3) and the overall forcing chain by confirming cardinality consistency without introducing new axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.