choose84_doubled
plain-language theorem explainer
The binomial identity asserts that the number of 4-subsets of an 8-set equals twice the number of 3-subsets of a 7-set. Workers counting configurations inside the eight-tick structure of Recognition Science reference this relation when locating the peak binomial coefficient at three dimensions. The proof is a direct numerical check performed by the decide tactic.
Claim. $C(8,4) = 2 C(7,3)$
background
The module extracts combinatorial identities tied to the eight-tick octave 8 = 2^D with D = 3. It records that C(8,4) = 70 is the maximum binomial coefficient at D = 3 and equals gap45 + D^(D-1). The present theorem supplies the elementary relation C(8,4) = 2 C(7,3) that follows from the definition of binomial coefficients.
proof idea
The proof is a one-line wrapper that applies the decide tactic to verify the numerical equality.
why it matters
The identity anchors the combinatorial layer of Recognition Science by confirming relations inside the eight-tick structure at D = 3. It supports the module's claim that C(8,4) = 70 is the peak binomial and contributes to the five canonical families for configDim D = 5. No downstream theorems are listed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.