  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.