peak_fits_double_gap
Binomial coefficient C(8,4) satisfies C(8,4) ≤ 2 * gap45. Regulatory ceiling modelers cite it to bound the number of consistent half-activated configurations in 8-element recognition systems. The proof is a one-line wrapper that invokes the decide tactic to confirm the numerical inequality holds.
claim$C(8,4) ≤ 2 · gap_{45}$
background
The Regulatory Ceiling module (C9) treats the maximum binomial coefficient on 8-element recognition states, establishing that C(8,4) = 70 remains below the doubled gap-45 threshold. gap45 is the gap value tied to the half-ladder embedding from RungFractions, where half(k) = k/2, with parallel half definitions appearing in SpinStatistics for spin 1/2 and in RecogSpec.Core for PhiClosed at half values. The local setting states: 'It is 70 < 2 · gap45 = 90, so doubled it still fits under the gap-45 ceiling.' This supports the prediction that an 8-state regulatory module maintains at most 70 mutually consistent half-activated configurations before decoherence.
proof idea
The declaration is a one-line wrapper that applies the decide tactic to verify the inequality by direct numerical computation.
why it matters in Recognition Science
The result is referenced inside regulatoryCeilingCert to complete the certification that bundles the peak value, its maximality, the double-gap fit, the single-gap exceedance, and the total power set. It realizes the regulatory ceiling claim for the eight-tick octave structure, bounding half-activated states in recognition systems. The theorem touches the framework prediction for gene regulation limits on 8 binary states.
scope and limits
- Does not prove that C(8,4) is the maximum binomial coefficient.
- Does not derive or compute the value of gap45.
- Applies only to the specific case of 8 elements and gap45.
- Does not address regulatory modules with state counts other than 8.
Lean usage
example : Nat.choose 8 4 ≤ 2 * gap45 := peak_fits_double_gapformal statement (Lean)
30theorem peak_fits_double_gap : Nat.choose 8 4 ≤ 2 * gap45 := by decide
proof body
Term-mode proof.
31
32/-- Peak exceeds gap45 itself (unlike the half-rows). -/