IndisputableMonolith.Foundation.RSCoupledAxis

   1import Mathlib
   2
   3/-!
   4# RS-Coupled Axes
   5
   6Infrastructure for cross-domain combination theorems.
   7
   8The main point is that two finite axes of the same cardinality are not
   9automatically independent. In RS they count as independent only when they are
  10tagged by different recognition primitives.
  11
  12Lean status: 0 sorry, 0 axiom.
  13-/
  14
  15namespace IndisputableMonolith
  16namespace Foundation
  17namespace RSCoupledAxis
  18
  19/-- The five RS primitives used to tag domain axes. -/
  20inductive RSPrimitive where
  21  | jCost
  22  | phiLadder
  23  | sigmaCharge
  24  | q3Lattice
  25  | gap45
  26  deriving DecidableEq, Repr, Fintype
  27
  28theorem rsPrimitive_count : Fintype.card RSPrimitive = 5 := by
  29  decide
  30
  31/-- A finite domain axis, tagged by the RS primitive that carries its meaning. -/
  32structure CoupledAxis (n : ℕ) where
  33  Ix : Type
  34  finite : Fintype Ix
  35  card_eq : @Fintype.card Ix finite = n
  36  primitive : RSPrimitive
  37
  38/-- RS-independence means the axes are carried by different primitives. -/
  39def independent {n m : ℕ} (A : CoupledAxis n) (B : CoupledAxis m) : Prop :=
  40  A.primitive ≠ B.primitive
  41
  42/-- Pairwise independent triple of same-size axes. -/
  43structure RSIndependentTriple (n : ℕ) where
  44  axis1 : CoupledAxis n
  45  axis2 : CoupledAxis n
  46  axis3 : CoupledAxis n
  47  indep12 : independent axis1 axis2
  48  indep13 : independent axis1 axis3
  49  indep23 : independent axis2 axis3
  50
  51/-- Pairwise independent disjoint sum of same-size axes. -/
  52structure RSDisjointSum3 (n : ℕ) where
  53  axis1 : CoupledAxis n
  54  axis2 : CoupledAxis n
  55  axis3 : CoupledAxis n
  56  indep12 : independent axis1 axis2
  57  indep13 : independent axis1 axis3
  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
  88