choose_8_4
plain-language theorem explainer
Binomial coefficient C(8,4) equals 70 and marks the peak value for the regulatory ceiling on 8-element recognition states. Cross-domain modelers of gene regulation cite the bound to limit mutually consistent half-activated configurations before decoherence. The proof is a direct computational check via the decide tactic.
Claim. $C(8,4) = 70$
background
The Regulatory Ceiling module treats 8-element recognition states as arising from the eight-tick octave in three spatial dimensions. The central binomial coefficient supplies the maximum number of mutually consistent half-activated configurations on these states, with the explicit numerical claim that this maximum is 70 and satisfies 70 < 2 * gap45 = 90. Upstream enumerations supply the concrete 8-element sets (kinship systems) and 7-element lists (narrative plots, ore classes) that fix the combinatorial arena for the 8-state models.
proof idea
The declaration is a one-line wrapper that applies the decide tactic to evaluate Nat.choose 8 4 directly.
why it matters
The theorem supplies the peak field to regulatoryCeilingCert, which certifies that the binomial maximum fits under the doubled gap-45 ceiling for wave 62. It instantiates the eight-tick octave (T7) together with D = 3 from the forcing chain, furnishing a concrete numerical bound for regulatory complexity across domains. The combinatorial claim is closed with no remaining scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.