Reference · Finite sums

rainbow.math.sums.permutation-invariant

Finite sumssrc/rainbow/math/sums/permutation_invariant.clj0 definitions, 3 theorems

Nonlinear two-coordinate sums are invariant under a binary permutation matrix. Selection is derived from one-hot columns, not supplied as an external decoder.

signed/one-hot-preserves-binary-operation :
  (pi-selector pi-first pi-second : ℕ → ℚ) (pi-operation : ℚ → ℚ → ℚ) (pi-size : ℕ)
  (pi-respects : ∀ (pi-a : ℚ), ∀ (pi-b : ℚ), ∀ (pi-c : ℚ), ∀ (pi-d : ℚ), ∀ (pi-ac : pi-a = pi-c), ∀ (pi-bd : pi-b = pi-d), pi-operation pi-a pi-b = pi-operation pi-c pi-d)
  (pi-nonnegative : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx pi-size), 0 ≤ pi-selector idx)
  (pi-binary : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx pi-size), proposition/disjunction (pi-selector idx = 0) (pi-selector idx = 1))
  (pi-unit : signed/expr-sum-value pi-selector pi-size = 1)
  → pi-operation (signed/expr-sum-value (fun pi-job => pi-selector pi-job · pi-first pi-job) pi-size) (signed/expr-sum-value (fun pi-job => pi-selector pi-job · pi-second pi-job) pi-size) = signed/expr-sum-value (fun pi-job => pi-selector pi-job · (fun pi-job₁ => pi-operation (pi-first pi-job₁) (pi-second pi-job₁)) pi-job) pi-size

signed/permutation-row-weight-conservation :
  (pi-matrix : ℕ → ℕ → ℚ) (pi-values : ℕ → ℚ) (pi-size : ℕ)
  (pi-rows : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx pi-size), signed/expr-sum-value (fun rj => pi-matrix idx rj) pi-size = 1)
  → signed/expr-sum-value (fun pi-k => signed/expr-sum-value (fun pi-job => (fun pi-job₁ => pi-matrix pi-job₁ pi-k) pi-job · pi-values pi-job) pi-size) pi-size = signed/expr-sum-value (fun pi-i => pi-values pi-i) pi-size

signed/permutation-binary-operation-sum-invariant :
  (pi-matrix : ℕ → ℕ → ℚ) (pi-first pi-second : ℕ → ℚ) (pi-operation : ℚ → ℚ → ℚ)
  (pi-size : ℕ)
  (pi-respects : ∀ (pi-a : ℚ), ∀ (pi-b : ℚ), ∀ (pi-c : ℚ), ∀ (pi-d : ℚ), ∀ (pi-ac : pi-a = pi-c), ∀ (pi-bd : pi-b = pi-d), pi-operation pi-a pi-b = pi-operation pi-c pi-d)
  (pi-nonnegative : ∀ (ai : ℕ), ∀ (ai-bound : nat/strict-below ai pi-size), ∀ (aj : ℕ), ∀ (aj-bound : nat/strict-below aj pi-size), 0 ≤ pi-matrix ai aj)
  (pi-binary : ∀ (pi-row : ℕ), ∀ (pi-rb : nat/strict-below pi-row pi-size), ∀ (pi-col : ℕ), ∀ (pi-cb : nat/strict-below pi-col pi-size), proposition/disjunction (pi-matrix pi-row pi-col = 0) (pi-matrix pi-row pi-col = 1))
  (pi-rows : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx pi-size), signed/expr-sum-value (fun rj => pi-matrix idx rj) pi-size = 1)
  (pi-cols : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx pi-size), signed/expr-sum-value (fun ci => pi-matrix ci idx) pi-size = 1)
  → signed/expr-sum-value (fun pi-k => pi-operation (signed/expr-sum-value (fun pi-job => (fun pi-job₁ => pi-matrix pi-job₁ pi-k) pi-job · pi-first pi-job) pi-size) (signed/expr-sum-value (fun pi-job => (fun pi-job₁ => pi-matrix pi-job₁ pi-k) pi-job · pi-second pi-job) pi-size)) pi-size = signed/expr-sum-value (fun pi-job => pi-operation (pi-first pi-job) (pi-second pi-job)) pi-size