`halfRowSum_eq`

proved

show as: view math explainer →

module: IndisputableMonolith.CrossDomain.RegulatoryCeiling
domain: CrossDomain
line: 38 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.CrossDomain.RegulatoryCeiling on GitHub at line 38.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

formal source

  35/-- Sum of Q₃ half-rows: C(8,0)+C(8,1)+C(8,2)+C(8,3) = 93. -/
  36def halfRowSum : ℕ :=
  37  Nat.choose 8 0 + Nat.choose 8 1 + Nat.choose 8 2 + Nat.choose 8 3
  38theorem halfRowSum_eq : halfRowSum = 93 := by decide
  39
  40/-- Total Q₃ power set: Σ_k C(8,k) = 2^8 = 256. -/
  41theorem totalPowerSet :
  42    (Finset.range 9).sum (fun k => Nat.choose 8 k) = 256 := by decide
  43
  44structure RegulatoryCeilingCert where
  45  peak : Nat.choose 8 4 = 70
  46  peak_is_max : ∀ k, k ≤ 8 → Nat.choose 8 k ≤ Nat.choose 8 4
  47  fits_double_gap : Nat.choose 8 4 ≤ 2 * gap45
  48  exceeds_gap : Nat.choose 8 4 > gap45
  49  total_256 : (Finset.range 9).sum (fun k => Nat.choose 8 k) = 256
  50
  51def regulatoryCeilingCert : RegulatoryCeilingCert where
  52  peak := choose_8_4
  53  peak_is_max := choose_8_4_is_max
  54  fits_double_gap := peak_fits_double_gap
  55  exceeds_gap := peak_exceeds_single_gap
  56  total_256 := totalPowerSet
  57
  58end IndisputableMonolith.CrossDomain.RegulatoryCeiling

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.