def
definition
halfRowSum
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.CrossDomain.RegulatoryCeiling on GitHub at line 36.
browse module
All declarations in this module, on Recognition.
explainer page
used by
formal source
33theorem peak_exceeds_single_gap : Nat.choose 8 4 > gap45 := by decide
34
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