Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Degeneracy Graph Determinant: Factorization

Abstract

The full arbitrary-depth determinant is the signed literal sibling-difference product with source witness multiplicities.

SourceSiblingPair separates only ordered siblings under one parent. sourceExponent is the actual cardinality of SourcePairTailWitness, so all exponents are positive where the source requires them and the bottom exponent is one. sourceFactorProduct is the literal product over every level and sibling pair; sourceSquare_det_factorization combines the recurrence with the exact row/column enumeration sign and no unproved evaluation-equivalence proxy.

This owner is the canonical Lean resolution of the source determinant clauses (6.22)–(6.27), conditional only on the SourceTree sibling-injectivity hypothesis already present in the formal statement.

Definition 1.1 (SourceSiblingPair).

Lean statement: D5/S3/Quantum/Algebra/DegeneracyGraphDeterminantFactorization.SourceSiblingPair

Formalization. D5/S3/Quantum/Algebra/DegeneracyGraphDeterminantFactorization.SourceSiblingPair (✓ std3).

Source. Repository-derived.

Acknowledgement. Garreth Kemp and Sanjaye Ramgoolam (2026). Gauge-string duality, monomial bases and graph determinants. URL: https://arxiv.org/html/2603.05259v2.

Commentary.

This declaration is part of the final signed source factorization. It preserves literal ordered sibling pairs, actual SourcePairTailWitness cardinalities, and the explicit integer sign.

Definition 1.2 (sourceExponent).

Lean statement: D5/S3/Quantum/Algebra/DegeneracyGraphDeterminantFactorization.sourceExponent

Formalization. D5/S3/Quantum/Algebra/DegeneracyGraphDeterminantFactorization.sourceExponent (✓ std3).

Source. Repository-derived.

Acknowledgement. Garreth Kemp and Sanjaye Ramgoolam (2026). Gauge-string duality, monomial bases and graph determinants. URL: https://arxiv.org/html/2603.05259v2.

Commentary.

This declaration is part of the final signed source factorization. It preserves literal ordered sibling pairs, actual SourcePairTailWitness cardinalities, and the explicit integer sign.

Definition 1.3 (sourceFactorProduct).

Lean statement: D5/S3/Quantum/Algebra/DegeneracyGraphDeterminantFactorization.sourceFactorProduct

Formalization. D5/S3/Quantum/Algebra/DegeneracyGraphDeterminantFactorization.sourceFactorProduct (✓ std3).

Source. Repository-derived.

Acknowledgement. Garreth Kemp and Sanjaye Ramgoolam (2026). Gauge-string duality, monomial bases and graph determinants. URL: https://arxiv.org/html/2603.05259v2.

Commentary.

This declaration is part of the final signed source factorization. It preserves literal ordered sibling pairs, actual SourcePairTailWitness cardinalities, and the explicit integer sign.

Theorem 1.4 (sourceSquare_det_factorization).

Lean statement: D5/S3/Quantum/Algebra/DegeneracyGraphDeterminantFactorization.sourceSquare_det_factorization

Proof. Machine-checked in Lean as D5/S3/Quantum/Algebra/DegeneracyGraphDeterminantFactorization.sourceSquare_det_factorization (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Garreth Kemp and Sanjaye Ramgoolam (2026). Gauge-string duality, monomial bases and graph determinants. URL: https://arxiv.org/html/2603.05259v2.

Commentary.

This declaration is part of the final signed source factorization. It preserves literal ordered sibling pairs, actual SourcePairTailWitness cardinalities, and the explicit integer sign.

References