Alphabeta Math
TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-26
How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

  • Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
  • AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
  • AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

det⁡(∣M(Ai,Ej)∣)i,j=∑π∈Srsgn⁡(π)⋅#{non-intersecting π-systems}

Statement

Fix a natural number r≥1, start points (Ai)i<r and end points (Ei)i<r in Z2. Put

mi,j:=∣M(Ai,Ej)∣,

the number of monotone lattice paths from Ai to Ej. Then

det⁡(mi,j)0≤i,j<r=∑π∈Srsgn⁡(π)⋅#Nπ(A,E),

where Nπ(A,E) is the set of non-intersecting π-systems (Path systems between two families of lattice points, and non-intersecting systems).

If the configuration is compatible, meaning that every monotone path Ai→Ej meets every monotone path Ak→Eℓ whenever i<k and j>ℓ, then only the identity permutation contributes and

det⁡(mi,j)0≤i,j<r=#Nid(A,E).

Facts & Assumptions

Given: a natural number r≥1, start points (Ai)i<r, end points (Ei)i<r, and the matrix M=(mi,j)0≤i,j<r with mi,j:=∣M(Ai,Ej)∣.

[F1]

For r≥1, the determinant is det⁡(M)=∑σ∈Srsgn⁡(σ)∏i<rmσ(i),i (For n≥1, the determinant over a commutative ring by the Leibniz formula, and ∣det⁡A∣ for a real matrix).

[L1]

There is a sign-reversing involution on the intersecting systems (Tail-swapping is a sign-reversing involution on the intersecting systems).

[F3]

The sign is multiplicative, so 1=sgn⁡(σσ−1)=sgn⁡(σ)sgn⁡(σ−1) and hence sgn⁡(σ−1)=sgn⁡(σ) (The sign is a homomorphism Sn→{+1,−1}, surjective exactly when n≥2).

Proof

technique · direct
1.1F1F3algebra

Expanding by [F1] and reindexing the finite sum by π=σ−1 gives det⁡(M)=∑π∈Srsgn⁡(π)∏i<rmi,π(i). Indeed [F3] gives sgn⁡(σ−1)=sgn⁡(σ) and, after putting j=σ(i), the product ∏i<rmσ(i),i becomes ∏j<rmj,σ−1(j).

2.1F2step 1.1

For each permutation π, the product ∏i<rmi,π(i) is exactly the number of π-systems by [F2], so det⁡(M)=∑π∈Srsgn⁡(π)⋅#Sπ(A,E).

3.1L1step 2.1

Split each finite set Sπ(A,E) into its non-intersecting part and its intersecting part. The intersecting systems cancel in pairs under the involution of [L1], because paired terms carry opposite signs and equal absolute values. Therefore the sum of step 2.1 reduces to ∑π∈Srsgn⁡(π)⋅#Nπ(A,E).

4.1givenstep 3.1∎

In the compatible case, every non-identity permutation π has an inversion i<k with π(i)>π(k), and the compatibility hypothesis says that every path Ai→Eπ(i) meets every path Ak→Eπ(k); so every π-system is intersecting and Nπ(A,E)=∅. Only the identity permutation remains, and the determinant counts the non-intersecting systems joining Ai to Ei.

Remarks

  • This is the lattice-path form of the Lindstrom-Gessel-Viennot lemma. The general acyclic-digraph statement needs digraph machinery that this page does not build, so the theorem is stated exactly in the form the page uses.

Depends on

Used by

Dependency tree · two levels

48 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources