choose_8_4_is_max
plain-language theorem explainer
Binomial coefficients C(8, k) for integer k from 0 to 8 attain their maximum at k = 4. Regulatory network modelers and combinatorial physicists cite the bound to limit consistent half-activated states to 70 under the gap-45 ceiling. The argument exhausts the possible values of k by interval splitting and verifies each inequality by decision.
Claim. For every natural number $k$ with $k ≤ 8$, the binomial coefficient satisfies $C(8, k) ≤ C(8, 4)$.
background
The Regulatory Ceiling module asserts that the maximum binomial coefficient on 8-element recognition states is C(8,4) = 70, the central entry of the binomial row. This caps the number of mutually consistent half-activated configurations in a regulatory module with 8 binary states before decoherence. The doubled gap-45 ceiling equals 90, and 70 lies strictly below it.
proof idea
The proof is a one-line wrapper that applies interval_cases to k under the hypothesis k ≤ 8 and then invokes decide on each resulting numerical inequality.
why it matters
This theorem supplies the peak_is_max field inside regulatoryCeilingCert, which certifies that the 70-peak fits under twice the gap-45 value. It realizes the C9 structural claim that C(8,4) is maximal on 8-element recognition states. The 8-element setting aligns with the eight-tick octave (period 2^3) in the unified forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.