Matrix Tree Theorem (0 sorry version)

[junaid-hasan]

It looks like Matrix Tree Theorem is done!

There are 0 sorries, and 0 warnings.

In a future PR I might add a more human written version. The current version was possible via

• Aristotle
• Pi Coding Agent
• DeepSeek V4 Pro
• CauchyBinet was recently proved by an autoformalization by group at Meta.

It costed around $10 in API cost and used about 250 Million tokens (most were cached input so at cheaper rates). Also the cost is higher because in earlier runs I tried to use DeepSeek only and wasted a ton of tokens. I feel using Aristotle at the start would have made it much more efficient. However aristotle uses the grind tactic at a lot of places which makes it hard for a human to understand. This presents an opportunity for future readibility improvements.

I will add followup comments explaining the code and the lemmas and how they work.

[junaid-hasan]

Module Dependency Graph

                            ┌──────────────────────┐
                            │   SpanningTree.lean  │
                            │ (SpanningTree type,  │
                            │  Finite/Fintype inst)│
                            └──────────┬───────────┘
                                       │
          ┌────────────────────────────┤
          │                            │
┌─────────┴──────────────┐  ┌─────────┴────────────┐
│   SignIncMatrix.lean   │  │    TreeDet.lean      │
│ (signedIncMatrix,      │  │ (treeParent,         │
│  factor L_G = B·Bᵀ,    │  │  edgeEmbedding,      │
│  reducedSignedInc      │  │  perm_eq_id_of_...,  │
│  Matrix)               │  │  signedInc_det_tree) │
└─────────┬──────────────┘  └─────────┬────────────┘
          │                           │
          │              ┌────────────┤
          │              │            │
┌─────────┴──────────────┤  ┌─────────┴────────────┐
│   CauchyBinet.lean     │  │  NonTreeDet.lean     │
│ (cauchyBinet theorem,  │  │ (det_zero_of_sum_    │
│  det_mul_aux_nonsquare,│  │  rows_eq_zero,       │
│  sum_injective_eq_...) │  │  signedInc_det_      │
└─────────┬──────────────┘  │  nontree)            │
          │                 └─────────┬────────────┘
          │                           │
          └───────────┬───────────────┘
                      │
          ┌───────────┴───────────────┐
          │     MatrixTreeThm.lean    │
          │                           │
          │ cauchyBinet_det_sq        │
          │ cauchyBinet_reindex_sq    │
          │ det_mul_transpose_        │
          │   cauchyBinet             │
          │ exists_perm_of_image_eq   │
          │ det_submatrix_sq_eq_of_   │
          │   comp_perm               │
          │ spanningTree_equiv_       │
          │   edgeFinset              │
          │ cauchyBinet_term_tree /   │
          │   nontree                 │
          │ cauchyBinet_sum_eq_       │
          │   spanningTree_card       │
          │                           │
          │ ★ matrix_tree_theorem ★   │
          └───────────────────────────┘