Reference · Signed rationals

rainbow.math.rational.signed.multiply-associative

Signed rationalssrc/rainbow/math/rational/signed/multiply_associative.clj0 definitions, 2 theorems

Associativity of signed multiplication, and the outer swap the LP column bound needs. signed/multiply-associative : (a*b)*c ~ a*(b*c) signed/multiply-swap-outer : (p*q)*r ~ (p*r)*q Both are genuine eight-monomial identities. Unfolded, `(a*b)*c ~ a*(b*c)` is the nnrat equivalence [(Pa*Pb + Na*Nb)*Pc + (Pa*Nb + Na*Pb)*Nc] + [Pa*(Pb*Nc + Nb*Pc) + Na*(Pb*Pc + Nb*Nc)] ~ [Pa*(Pb*Pc + Nb*Nc) + Na*(Pb*Nc + Nb*Pc)] + [(Pa*Pb + Na*Nb)*Nc + (Pa*Nb + Na*Pb)*Pc] whose two sides carry the same eight degree-three monomials in eight different bracketings and orders. Written by hand that is a few hundred lines of add-four-reorder / multiply-associative / congruence chaining; here each proof is a single call to `rainbow.math.rational.nnrat.ring`, which normalizes both sides to a canonical sorted sum of canonical monomials and refuses to emit anything if the multisets differ. `signed/multiply-swap-outer` is the specific reassociation that turns (A_ij * y_i) * x_j into (A_ij * x_j) * y_i, which is the step that was blocking the column-side discharge of signed LP weak duality. Native and axiom-free; chains the nnrat-ring law providers on D63.

Depends onmath.rational.signed.multiplymath.rational.nnrat.ring

signed/multiply-associative :
  (a b c : ℚ)
  → a · b · c = a · (b · c)

signed/multiply-swap-outer :
  (p q r : ℚ)
  → p · q · r = p · r · q