halfRowSum
halfRowSum defines the sum of binomial coefficients binom(8,0) through binom(8,3) as a natural number equaling 93. This counts the lower half of configurations in an 8-element recognition state space for regulatory ceiling analysis. Cross-domain models in Recognition Science cite it when bounding consistent states below the doubled gap-45 threshold of 90. The definition is a direct enumeration of four binomial terms.
claimDefine $S = {8 choose 0} + {8 choose 1} + {8 choose 2} + {8 choose 3}$.
background
The Regulatory Ceiling module studies binomial coefficients over 8-element recognition states arising from the eight-tick octave. The half-row sum aggregates the lower terms (k from 0 to 3) to represent half-activated configurations. The module states that C(8,4) equals 70 and satisfies 70 less than twice gap45, so the doubled peak still fits under the gap-45 ceiling. This supports the prediction that a regulatory module with 8 binary states maintains at most 70 mutually consistent half-activated configurations before decoherence.
proof idea
The definition is a direct one-line expression that adds the four results of the binomial coefficient function applied to (8,0), (8,1), (8,2), and (8,3).
why it matters in Recognition Science
It supplies the numerical value required by the companion theorem halfRowSum_eq that confirms the sum equals 93. This supports the module's structural claim that C(8,4) is the maximum binomial coefficient and lies below 2 times gap45. In the Recognition Science framework the construction aligns with the eight-tick octave and the bound on consistent states in 8-element systems, informing gene-regulation predictions.
scope and limits
- Does not prove the sum equals 93; that is the separate theorem halfRowSum_eq.
- Does not define or reference the gap45 constant.
- Does not compute the central coefficient C(8,4) or the full power-set total.
- Does not extend the sum to state spaces of size other than 8.
Lean usage
theorem halfRowSum_eq : halfRowSum = 93 := by decideformal statement (Lean)
36def halfRowSum : ℕ :=
proof body
Definition body.
37 Nat.choose 8 0 + Nat.choose 8 1 + Nat.choose 8 2 + Nat.choose 8 3