tripleProductCard

formal source

  58  indep23 : independent axis2 axis3
  59
  60/-- Product of the cardinalities of three same-size RS-independent axes. -/
  61def tripleProductCard {n : ℕ} (T : RSIndependentTriple n) : ℕ :=
  62  @Fintype.card T.axis1.Ix T.axis1.finite *
  63    @Fintype.card T.axis2.Ix T.axis2.finite *
  64    @Fintype.card T.axis3.Ix T.axis3.finite
  65
  66/-- The tensor-product count of three same-size RS-independent axes is n^3. -/
  67theorem triple_card {n : ℕ} (T : RSIndependentTriple n) :
  68    tripleProductCard T = n * n * n := by
  69  unfold tripleProductCard
  70  rw [T.axis1.card_eq, T.axis2.card_eq, T.axis3.card_eq]
  71
  72/-- Cardinality of the disjoint sum of three same-size RS-independent axes. -/
  73theorem disjoint_sum_card {n : ℕ} (S : RSDisjointSum3 n) :
  74    @Fintype.card S.axis1.Ix S.axis1.finite +
  75      @Fintype.card S.axis2.Ix S.axis2.finite +
  76      @Fintype.card S.axis3.Ix S.axis3.finite = 3 * n := by
  77  rw [S.axis1.card_eq, S.axis2.card_eq, S.axis3.card_eq]
  78  ring
  79
  80/-- The gap-45 complexity ceiling. -/
  81def gap45 : ℕ := 45
  82
  83theorem gap45_eq : gap45 = 45 := rfl
  84
  85end RSCoupledAxis
  86end Foundation
  87end IndisputableMonolith