TenFoldCombinationsCert

formal source

  78/-- Two 5-fold halves of a 10-fold: decimal = 2 × 5 (half-halves). -/
  79theorem ten_as_two_halves : (10 : ℕ) = 5 + 5 := by decide
  80
  81structure TenFoldCombinationsCert where
  82  finger_10 : HasTenFold Finger
  83  digit_10 : HasTenFold DecimalDigit
  84  lumSac_10 : HasTenFold LumbarSacralVert
  85  dBlock_10 : HasTenFold DBlockElement
  86  ten_factoring : (10 : ℕ) = 2 * 5
  87  ten_as_halves : (10 : ℕ) = 5 + 5
  88  squared_100 : ∀ (A B : Type) [Fintype A] [Fintype B],
  89    HasTenFold A → HasTenFold B → Fintype.card (A × B) = 100
  90
  91def tenFoldCombinationsCert : TenFoldCombinationsCert where
  92  finger_10 := finger_is_10
  93  digit_10 := digit_is_10
  94  lumSac_10 := lumSac_is_10
  95  dBlock_10 := dBlock_is_10
  96  ten_factoring := ten_eq_two_D
  97  ten_as_halves := ten_as_two_halves
  98  squared_100 := fun _ _ _ _ => tenfold_squared
  99
 100end IndisputableMonolith.CrossDomain.TenFoldCombinations