  67theorem average_per_pattern :
  68    crossDomainModuleCount * 10 = 270 := by decide  -- 27 = 27 = 5.4 × 5
  69
  70structure MetaTheoremCountCert where
  71  count : crossDomainModuleCount = 27
  72  count_is_cube : crossDomainModuleCount = 3^3
  73  patterns_covered : patternsCovered = 5
  74  count_in_spectrum_range :
  75    25 ≤ crossDomainModuleCount ∧ crossDomainModuleCount ≤ 45
  76
  77def metaTheoremCountCert : MetaTheoremCountCert where
  78  count := count_eq
  79  count_is_cube := count_is_D_cubed
  80  patterns_covered := patterns_match_D
  81  count_in_spectrum_range := count_in_spectrum
  82
  83end IndisputableMonolith.CrossDomain.MetaTheoremCount

papers checked against this theorem

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