choose84_gt_gap45
plain-language theorem explainer
The binomial coefficient C(8,4) exceeds 45. Recognition Science combinatorics researchers cite this to anchor the central binomial above the gap threshold. The proof proceeds via direct decision without lemmas or hypotheses.
Claim. The binomial coefficient $C(8,4)$ is strictly greater than 45.
background
CombinatoricsFromRS derives key identities from Recognition Science. It centers on binomial coefficients for the eight-tick structure 8 = 2^D with D=3. C(8,4) reaches its maximum of 70, exceeding gap45 by 25, where gap45 relates to nearby Catalan number 42 and Bell number 52. The module ties this to five combinatorial families for configDim D=5.
proof idea
This is a one-line wrapper that applies the decide tactic to the statement Nat.choose 8 4 > 45.
why it matters
The declaration supplies the choose84_gt component in combinatoricsCert. It certifies the combinatorial structure from RS, referencing the eight-tick octave and D=3. The module doc emphasizes C(8,4) = 70 = gap45 + 25 = gap45 + D^(D-1), supporting the overall certification.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.