Reference · Matrices

rainbow.math.linear.matrix.associativity-counterexample

Matrices src/rainbow/math/linear/matrix/associativity_counterexample.clj3 definitions, 5 theorems

A checked counterexample to unrestricted native matrix associativity. With A = [[]], B = [], and C = [[0]], both adjacent pairs are composable, yet (A*B)*C evaluates to [[0]] while A*(B*C) evaluates to [[]]. Thus the nonempty-middle premise of matrix/multiply-associative-nonempty-middle is mathematically necessary for the total row-list encoding, not merely a proof artifact. Native and axiom-free on D63.

Depends onmath.linear.matrix.composable-transpose

matrix/associativity-counterexample-left

DefinitionSource, line 65

matrix/associativity-counterexample-left :
  → List (List ℚ)

List = data/Listℚ = signed/SignedRational

matrix/associativity-counterexample-middle

DefinitionSource, line 71

matrix/associativity-counterexample-middle :
  → List (List ℚ)

List = data/Listℚ = signed/SignedRational

matrix/associativity-counterexample-right

DefinitionSource, line 77

matrix/associativity-counterexample-right :
  → List (List ℚ)

List = data/Listℚ = signed/SignedRational

matrix/associativity-counterexample-left-middle-composable

TheoremWorked exampleNo axiomsSource, line 86

matrix/associativity-counterexample-left-middle-composable :
  → matrix/composable matrix/associativity-counterexample-left matrix/associativity-counterexample-middle

matrix/associativity-counterexample-middle-right-composable

TheoremWorked exampleNo axiomsSource, line 102

matrix/associativity-counterexample-middle-right-composable :
  → matrix/composable matrix/associativity-counterexample-middle matrix/associativity-counterexample-right

matrix/associativity-counterexample-left-evaluates

TheoremWorked exampleNo axiomsSource, line 112

matrix/associativity-counterexample-left-evaluates :
  → matrix/equivalent (multiply) [[0]]
  where multiply := matrix/multiply (matrix/multiply matrix/associativity-counterexample-left matrix/associativity-counterexample-middle) matrix/associativity-counterexample-right

0 = signed/zero

matrix/associativity-counterexample-right-evaluates

TheoremWorked exampleNo axiomsSource, line 129

matrix/associativity-counterexample-right-evaluates :
  → matrix/equivalent (multiply) [[]]
  where multiply := matrix/multiply matrix/associativity-counterexample-left (matrix/multiply matrix/associativity-counterexample-middle matrix/associativity-counterexample-right)

matrix/associativity-counterexample-not-associative

TheoremWorked exampleNo axiomsSource, line 157

matrix/associativity-counterexample-not-associative :
  (x₁ : matrix/equivalent (multiply) (multiply₁))
  → proposition/falsity
  where multiply := matrix/multiply (matrix/multiply matrix/associativity-counterexample-left matrix/associativity-counterexample-middle) matrix/associativity-counterexample-right
  where multiply₁ := matrix/multiply matrix/associativity-counterexample-left (matrix/multiply matrix/associativity-counterexample-middle matrix/associativity-counterexample-right)