InvolutionCancellation

Finite sign-reversing cancellation and its determinant application (ZF)

Open in Workbench View on GitHub

1-- Finite sign-reversing cancellation and its determinant application (ZF).2-- Copyright (c) 2026 Grant Passmore.3-- Released under the Apache License 2.0. See LICENSE in the repository root.4-- Authors: Grant Passmore56module InvolutionCancellation7import Grace.Cumulus.Algebra.Ring.DeterminantCancellation89section Rings10variable (D A add zero neg mul one w t : Set)11notation ring R := (A, add, zero, neg, mul, one)12hypothesis ring : IsCommRing(R)1314theorem paired_sum15  requires finite : Finite(D)16  requires weights : w : D → A17  requires involution : InvolutionOn(t, D)18  requires opposite : ∀ a ∈ D, w(t(a)) = R[-w(a)]19  requires fixed : ∀ a ∈ D, t(a) = a → w(a) = R[0]20  shows finiteRingSum(D, A, add, zero, neg, mul, one, w) = R[0]21proof22  exact finiteRingSum.involution with *2324theorem paired_sum_without_fixed_points25  requires finite : Finite(D)26  requires weights : w : D → A27  requires involution : InvolutionOn(t, D)28  requires opposite : ∀ a ∈ D, w(t(a)) = R[-w(a)]29  requires free : ∀ a ∈ D, t(a) ≠ a30  shows finiteRingSum(D, A, add, zero, neg, mul, one, w) = R[0]31proof32  exact finiteRingSum.involution_free with *3334theorem paired_determinant (n : Nat) (M : Set)35  requires matrix : RingMatrix(n, R, M)36  requires involution : InvolutionOn(t, permutations(n))37  requires free : ∀ p ∈ permutations(n), t(p) ≠ p38  requires signs : ∀ p ∈ permutations(n), permutationSign(n, A, add, zero, neg, mul, one, t(p)) = R[-permutationSign(n, A, add, zero, neg, mul, one, p)]39  requires products : ∀ p ∈ permutations(n), finiteRingProduct(n, A, add, zero, neg, mul, one, permutationEntries(n, A, M, t(p))) = finiteRingProduct(n, A, add, zero, neg, mul, one, permutationEntries(n, A, M, p))40  shows determinant(n, R, M) = R[0]41proof42  exact determinant.cancel_pairs with *4344end Rings45