peak_exceeds_single_gap
plain-language theorem explainer
The central binomial coefficient on 8 states exceeds the single gap45 threshold while remaining below the doubled ceiling. Cross-domain applications in gene regulation and Q3 state counting cite this bound to limit consistent half-activated configurations. The proof is a direct numerical verification by the decide tactic.
Claim. $\binom{8}{4} > \text{gap45}$
background
The RegulatoryCeiling module treats 8-element recognition states arising from the Q3 structure, which forces SU(3) x SU(2) x U(1) gauge content together with exactly three generations and 24 chiral fermions. gap45 is the single-gap threshold such that twice this value equals 90; the module shows that the peak count of 70 lies strictly between gap45 and 2*gap45. Upstream results supply the J-cost convexity from PhysicsComplexityStructure and the discrete phi-tier structure from NucleosynthesisTiers that calibrate the regulatory bounds.
proof idea
Term-mode proof consisting of a single decide tactic that evaluates the binomial coefficient and gap45 numerically to confirm the inequality.
why it matters
Supplies the exceeds_gap component of RegulatoryCeilingCert, which bundles the peak, its maximality, double-gap fit, single-gap exceedance, and total power set. This completes the certificate for the regulatory ceiling on Q3 and supports the gene-regulation prediction that at most 70 mutually consistent configurations are sustainable on 8 binary states. It aligns with the eight-tick octave (T7) of the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.