totalPowerSet
The sum of binomial coefficients C(8,k) for k from 0 to 8 equals 256, confirming the power set cardinality of an 8-element set. Researchers modeling regulatory ceilings in Recognition Science cite this to bound total configurations in 8-state systems before decoherence. The proof is a direct evaluation via the decide tactic on the finite sum.
claim$sum_{k=0}^{8} binom{8}{k} = 256$
background
The CrossDomain.RegulatoryCeiling module analyzes the regulatory ceiling on Q3, an 8-element recognition state space. It shows the central binomial coefficient C(8,4) equals 70 and remains below the doubled gap-45 ceiling of 90, yielding a prediction that an 8-state regulatory module supports at most 70 mutually consistent half-activated configurations. The module doc states: 'Structural claim: the maximum binomial coefficient on 8-element recognition states is C(8,4) = 70.'
proof idea
The proof is a one-line wrapper that applies the decide tactic to evaluate the finite sum of binomial coefficients directly.
why it matters in Recognition Science
This theorem supplies the total_256 field inside the RegulatoryCeilingCert structure, which certifies the regulatory ceiling for gene regulation models. It anchors the eight-tick octave (T7) in the forcing chain by confirming the power set size 2^8 for the 8-state system. The module predicts decoherence limits for binary regulatory states and feeds the downstream certification that 70 fits under the gap-45 bound.
scope and limits
- Does not prove maximality of C(8,4) or any other binomial coefficient.
- Does not extend the equality to sets of size other than 8.
- Does not incorporate J-cost, defectDist, or phi-ladder mass formulas.
- Does not address Berry creation thresholds or alpha-band constraints.
Lean usage
example : (Finset.range 9).sum (fun k => Nat.choose 8 k) = 256 := totalPowerSetformal statement (Lean)
41theorem totalPowerSet :
42 (Finset.range 9).sum (fun k => Nat.choose 8 k) = 256 := by decide
proof body
43