Determinant expansion through a supplied finite path-system bijection

Proved

ProofsInTheBook.Chapter30.PathCountSystem.det_matrix_eq_total

by xiangyazi24 · Sep 12, 2026 · Mathlib c5ea003 (Lean v4.30.0)

combinatoricsconditional-identitydeterminantsfinite-sumslean4proofs-from-the-book

Let n be a natural number, let V have decidable equality, and let R be a commutative ring. Suppose a PathCountSystem is supplied: a vertex weight $v:V\to R$ ; finite types $P_{ij}$ with weights $a:P_{ij}\to R$ for every pair $i,j\in\{0,\ldots,n-1\}$ ; a bijection

E:\coprod_{\sigma\in S_n}\prod_i P_{\sigma(i),i}\;\longrightarrow\;\mathcal F_n(V);

and, for every choice $(\sigma,p)$ , the compatibility identity

w_v(E(\sigma,p))=\operatorname{sgn}(\sigma)\prod_i a(p_i).

Here $\mathcal F_n(V)$ is the defined disjoint union of pairwise vertex-disjoint list families and marked bad list data, and $w_v$ is its specified signed vertex-product weight. Set $M_{ij}=\sum_{p\in P_{ij}}a(p)$ . Assume explicitly that the entire type $\mathcal F_n(V)$ is finite.

Then

\det M=\sum_{F\in\mathcal F_n(V)}w_v(F).

This is a conditional algebraic identity for the supplied finite system and its weight-preserving bijection. The underlying lists have unrestricted length and no graph-edge, source, sink, or lattice-step constraints. For positive n and nonempty V, unrestricted list families are not a finite geometric path space. The source explicitly leaves bounded or geometric path infrastructure, grid applications, and the hook-length formula unresolved.

Preamble

import Mathlib
import Definitions.Def_ProofsInTheBook_Chapter30
open ProofsInTheBook.Chapter30
open Matrix BigOperators
open ProofsInTheBook.Chapter30.PathCountSystem
variable {n : ℕ} {V R : Type*} [DecidableEq V] [CommRing R]

Formal statement

theorem ProofsInTheBook.Chapter30.PathCountSystem.det_matrix_eq_total (S : PathCountSystem n V R) [Fintype (LGVFamily n V)] :
    S.matrix.det = ∑ F : LGVFamily n V, ProofsInTheBook.Chapter30.LGVFamily.signedWeight S.vertexWeight F := by sorry

Source

Exact repository declaration: https://github.com/xiangyazi24/proof_in_the_book/blob/88d88d141768cded75e782c525ef1bf04b8fe220/ProofsInTheBook/Chapter30.lean#L464. PathCountSystem hypotheses: https://github.com/xiangyazi24/proof_in_the_book/blob/88d88d141768cded75e782c525ef1bf04b8fe220/ProofsInTheBook/Chapter30.lean#L435. Explicit scope limitation: https://github.com/xiangyazi24/proof_in_the_book/blob/88d88d141768cded75e782c525ef1bf04b8fe220/ProofsInTheBook/Chapter30.lean#L578. Repository topic: “Lattice paths and determinants.” No edition-specific chapter mapping or geometric application is asserted.

View graph