choose84_eq_70
plain-language theorem explainer
The binomial coefficient C(8,4) equals 70. Researchers working on combinatorial counts tied to the eight-tick octave cite this equality when confirming the peak value at D=3. The proof evaluates the expression directly with the decide tactic.
Claim. $C(8,4) = 70$
background
The module extracts combinatorial identities from Recognition Science, centering on C(8,k) for k from 0 to 8 where 8 equals the 8-tick octave 2^D with D=3. It lists C(8,4)=70 as the maximum binomial coefficient at D=3, satisfying the relation 70 = gap45 + 25 with 25 = D^{D-1}. This identity supports the five canonical combinatorial families (permutations, combinations, partitions, paths, Young tableaux) that correspond to configDim D=5.
proof idea
The proof is a one-line wrapper that applies the decide tactic to evaluate the binomial coefficient directly.
why it matters
This theorem supplies the choose84 field inside the combinatoricsCert definition, which bundles the five combinatorial families and the C(8,4)=70 identity. It anchors the combinatorial side of the eight-tick octave (T7) and spatial dimension D=3 (T8) in the forcing chain. The module positions the result alongside Catalan and Bell numbers near gap-45.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.