peak_exceeds_single_gap
plain-language theorem explainer
The theorem asserts that the central binomial coefficient for an 8-element set exceeds the gap-45 threshold. Cross-domain regulatory models cite it to bound consistent configurations in Q3 recognition states before decoherence sets in. The proof is a direct computational verification that evaluates the inequality outright.
Claim. The central binomial coefficient satisfies $C(8,4) >$ gap-45.
background
The CrossDomain.RegulatoryCeiling module treats the regulatory ceiling for Q3, the 8-element recognition state space whose structure is supplied by the spectral emergence result. That upstream structure forces the SU(3) x SU(2) x U(1) gauge content, exactly three particle generations, and 24 chiral fermion flavors. gap45 is the single-gap threshold calibrated from the J-cost function (strictly convex with minimum at unity) and the ledger factorization of positive reals. The local setting is the eight-tick dynamics in which each recognition step updates at most eight neighbors.
proof idea
The proof is a term-mode application of the decide tactic that reduces the concrete numerical comparison between the binomial coefficient and the gap threshold to a decidable proposition.
why it matters
The result supplies the exceeds_gap field inside the regulatoryCeilingCert definition, completing the C9 structural claim that the peak of 70 still lies below the doubled gap-45 ceiling of 90. It aligns with the eight-tick octave (T7) and the emergence of D=3 spatial dimensions while supporting the gene-regulation prediction for at most 70 mutually consistent half-activated states in an 8-binary-state module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.