Prove rectangular selected-minor Cauchy-Binet identity

[PerAlexandersson]

Parent

Prerequisite for #292 and Karlin, Total Positivity, Vol. I, Chapter V, Section 1, Proposition 1.2.

Required theorem

Add a Mathlib-shaped theorem in the determinant shim expressing the determinant of a selected square minor of a rectangular product L * A as the sum over q-element subsets of the intermediate finite index type. Use the canonical increasing enumeration Set.powersetCard.ofFinEmbEquiv.symm.

Proposed name: Matrix.det_submatrix_mul_eq_sum_powersetCard.

Required proof route

Expand the determinant and matrix product, group intermediate maps by image subset and permutation, move the permutation sign between factors, and reassemble the two determinants. This is the finite Cauchy-Binet composition formula used by Karlin.

Acceptance criteria

• General over a commutative ring.
• Handles rectangular matrices and arbitrary selected row/column maps.
• No sorry, axiom, or theorem-shaped Prop definition.
• Lives in the Mathlib-shaped determinant compatibility layer.
• Includes focused coverage of empty, square-middle, and genuinely rectangular cases.
• Full CI is green.

Mathlib currently has Matrix.det_mul only for square factors with the same middle index and Matrix.submatrix_mul only when the middle reindexing is bijective, so neither proves this result.

[PerAlexandersson]

Implemented the algebraic half in PR #294 as Matrix.det_submatrix_mul_eq_sum_perm_fun, in a new Mathlib-shaped determinant/CauchyBinet module. It expands a selected minor of a rectangular product into the Leibniz sum over permutations and all intermediate maps, over any commutative ring. Axle accepted the exact proof with no errors or warnings in request 10d0da84-033f-4884-baa1-20d2ea9d96b7. No final Cauchy-Binet placeholder was added. The remaining exact obligation is to cancel noninjective-map contributions and group injective maps by the canonical ordered enumeration of their image subset.

[PerAlexandersson]

PR #294 now adds Matrix.det_submatrix_mul_eq_sum_fun_det, reassembling the permutation sum for each intermediate map as an actual determinant, and Matrix.det_submatrix_eq_zero_of_not_injective_right, which kills every noninjective map by repeated columns. Axle accepted the exact proofs in requests 036e7e42-7b1d-420d-9fb7-80285bab2910 and d63d0a78-bdb3-4946-b3c7-0ddbfead2e2a. The remaining Cauchy-Binet obligation is purely injective: factor each map through its canonical ordered image and a permutation, transfer the permutation sign to the right determinant, and group by Set.powersetCard.

[PerAlexandersson]

Mandatory cleanup cycle: moved Matrix.det_submatrix_eq_zero_of_not_injective_right from the Cauchy-Binet module to the lower-level determinant Basic shim and generalized it from Fin indices to arbitrary row/column types with an arbitrary finite decidable square selector type. Axle accepted the generalized statement and unchanged proof body with no errors or warnings in request 9960659e-b085-47b2-965e-b14b67adb60f. The Cauchy-Binet module now owns only product-expansion-specific results.

[PerAlexandersson]

PR #294 now adds Set.powersetCard.exists_orderEmb_comp_perm_eq_of_injective. Every injective map from Fin q into an arbitrary linear order is factored through the canonical increasing enumeration of its image subset and a permutation of Fin q. Axle accepted the exact generalized proof with no errors or warnings in request a607d401-c8c3-4342-a5a3-32a600a8ce3e. Together with the noninjective determinant-zero lemma, the remaining Cauchy-Binet work is now permutation-sign transport through the right determinant and grouping by the image subset.

[PerAlexandersson]

PR #294 now adds Set.powersetCard.orderEmb_comp_perm_injective, proving uniqueness of the ordered-image/permutation representation. The proof recovers the subset from the function range and then recovers the permutation using injectivity of the canonical order embedding. Axle accepted the exact theorem and private range helpers with no errors or warnings in request 55dffbd5-1267-4854-84da-27301f95f558. Together with the existence theorem, the finite reindexing is bijective. Remaining: package the equivalence, apply Matrix.det_permute/det_permute', and reassemble the right determinant for each subset.

[PerAlexandersson]

Mandatory cleanup cycle: hoisted the private range_orderEmbOfPowersetCard helper before both ordered-image factorization proofs and replaced the existence theorem's duplicate inline range calculation with the shared helper. Axle accepted the refactored proof with no errors or warnings in request 02328ef6-b939-40da-a1b0-6dc18b0dd548. No public statement or mathematical route changed.

[PerAlexandersson]

PR #294 now packages the factorization as Set.powersetCard.orderEmbPermEquivEmbedding and adds Set.powersetCard.sum_embedding_eq_sum_orderEmb_perm, explicitly reindexing finite sums over embeddings as nested sums over ordered image subsets and permutations. Axle accepted both declarations with no Lean errors or warnings in request 743aaa9c-fe11-4c92-adbc-74a821afe483; its advisory stubs are the existence/uniqueness theorems already proved on the branch. Remaining: restrict the all-functions sum to embeddings using noninjective determinant vanishing, then collapse each permutation sum via Matrix.det_permute' and Matrix.det_apply.

[PerAlexandersson]

Implemented the rectangular selected-minor Cauchy--Binet identity on PR #294 in commit fecbbec.

New declaration:

Matrix.det_submatrix_mul_eq_sum_powersetCard

The proof follows the source composition route: expand over all intermediate maps, eliminate noninjective maps via zero determinants, reindex injective maps by ordered image and permutation, then collapse each permutation sum using determinant alternation. The two new private bridges and the complete composition were checked in Axle; no local Lake build was run in this proof run.