Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Degeneracy Graph Determinant: Recurrence

Abstract

Occupied-degree reindexing turns the arbitrary-depth source square into a block-triangular pruning recurrence.

The recurrence owner supplies the canonical bottom and column equivalences, the actual pruning matrix, its low-block and triangular identities, and the signed determinant recurrence. No determinant sign is hidden in an ordering convention: fiber orientation and pruning permutation signs are explicit declarations.

Definition 1.1 (OccupiedDegree).

Lean statement: D5/S3/Quantum/Algebra/DegeneracyGraphDeterminantRecurrence.OccupiedDegree

Formalization. D5/S3/Quantum/Algebra/DegeneracyGraphDeterminantRecurrence.OccupiedDegree (✓ 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 the exact occupied-degree and pruning recurrence used to reindex the source square. The construction retains actual parent fibers and carries the induced row and column permutations explicitly.

Definition 1.2 (DegreeParent).

Lean statement: D5/S3/Quantum/Algebra/DegeneracyGraphDeterminantRecurrence.DegreeParent

Formalization. D5/S3/Quantum/Algebra/DegeneracyGraphDeterminantRecurrence.DegreeParent (✓ 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 the exact occupied-degree and pruning recurrence used to reindex the source square. The construction retains actual parent fibers and carries the induced row and column permutations explicitly.

Definition 1.3 (bottomDegreeEquiv).

Lean statement: D5/S3/Quantum/Algebra/DegeneracyGraphDeterminantRecurrence.bottomDegreeEquiv

Formalization. D5/S3/Quantum/Algebra/DegeneracyGraphDeterminantRecurrence.bottomDegreeEquiv (✓ 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 the exact occupied-degree and pruning recurrence used to reindex the source square. The construction retains actual parent fibers and carries the induced row and column permutations explicitly.

Definition 1.4 (columnDegree).

Lean statement: D5/S3/Quantum/Algebra/DegeneracyGraphDeterminantRecurrence.columnDegree

Formalization. D5/S3/Quantum/Algebra/DegeneracyGraphDeterminantRecurrence.columnDegree (✓ 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 the exact occupied-degree and pruning recurrence used to reindex the source square. The construction retains actual parent fibers and carries the induced row and column permutations explicitly.

Definition 1.5 (columnDegreeFiberEquiv).

Lean statement: D5/S3/Quantum/Algebra/DegeneracyGraphDeterminantRecurrence.columnDegreeFiberEquiv

Formalization. D5/S3/Quantum/Algebra/DegeneracyGraphDeterminantRecurrence.columnDegreeFiberEquiv (✓ 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 the exact occupied-degree and pruning recurrence used to reindex the source square. The construction retains actual parent fibers and carries the induced row and column permutations explicitly.

Definition 1.6 (columnDegreeEquiv).

Lean statement: D5/S3/Quantum/Algebra/DegeneracyGraphDeterminantRecurrence.columnDegreeEquiv

Formalization. D5/S3/Quantum/Algebra/DegeneracyGraphDeterminantRecurrence.columnDegreeEquiv (✓ 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 the exact occupied-degree and pruning recurrence used to reindex the source square. The construction retains actual parent fibers and carries the induced row and column permutations explicitly.

Definition 1.7 (degreeParentEquiv).

Lean statement: D5/S3/Quantum/Algebra/DegeneracyGraphDeterminantRecurrence.degreeParentEquiv

Formalization. D5/S3/Quantum/Algebra/DegeneracyGraphDeterminantRecurrence.degreeParentEquiv (✓ 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 the exact occupied-degree and pruning recurrence used to reindex the source square. The construction retains actual parent fibers and carries the induced row and column permutations explicitly.

Definition 1.8 (pruneBottomEquiv).

Lean statement: D5/S3/Quantum/Algebra/DegeneracyGraphDeterminantRecurrence.pruneBottomEquiv

Formalization. D5/S3/Quantum/Algebra/DegeneracyGraphDeterminantRecurrence.pruneBottomEquiv (✓ 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 the exact occupied-degree and pruning recurrence used to reindex the source square. The construction retains actual parent fibers and carries the induced row and column permutations explicitly.

Definition 1.9 (bottomColumnEquiv).

Lean statement: D5/S3/Quantum/Algebra/DegeneracyGraphDeterminantRecurrence.bottomColumnEquiv

Formalization. D5/S3/Quantum/Algebra/DegeneracyGraphDeterminantRecurrence.bottomColumnEquiv (✓ 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 the exact occupied-degree and pruning recurrence used to reindex the source square. The construction retains actual parent fibers and carries the induced row and column permutations explicitly.

Definition 1.10 (bottomFiberOrderEquiv).

Lean statement: D5/S3/Quantum/Algebra/DegeneracyGraphDeterminantRecurrence.bottomFiberOrderEquiv

Formalization. D5/S3/Quantum/Algebra/DegeneracyGraphDeterminantRecurrence.bottomFiberOrderEquiv (✓ 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 the exact occupied-degree and pruning recurrence used to reindex the source square. The construction retains actual parent fibers and carries the induced row and column permutations explicitly.

Theorem 1.11 (NewtonE_inv_reindex_fibers).

Lean statement: D5/S3/Quantum/Algebra/DegeneracyGraphDeterminantRecurrence.NewtonE_inv_reindex_fibers

Proof. Machine-checked in Lean as D5/S3/Quantum/Algebra/DegeneracyGraphDeterminantRecurrence.NewtonE_inv_reindex_fibers (✓ 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 the exact occupied-degree and pruning recurrence used to reindex the source square. The construction retains actual parent fibers and carries the induced row and column permutations explicitly.

Definition 1.12 (ancestorPrefix).

Lean statement: D5/S3/Quantum/Algebra/DegeneracyGraphDeterminantRecurrence.ancestorPrefix

Formalization. D5/S3/Quantum/Algebra/DegeneracyGraphDeterminantRecurrence.ancestorPrefix (✓ 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 the exact occupied-degree and pruning recurrence used to reindex the source square. The construction retains actual parent fibers and carries the induced row and column permutations explicitly.

Definition 1.13 (PruningIndex).

Lean statement: D5/S3/Quantum/Algebra/DegeneracyGraphDeterminantRecurrence.PruningIndex

Formalization. D5/S3/Quantum/Algebra/DegeneracyGraphDeterminantRecurrence.PruningIndex (✓ 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 the exact occupied-degree and pruning recurrence used to reindex the source square. The construction retains actual parent fibers and carries the induced row and column permutations explicitly.

Definition 1.14 (pruningRowEquiv).

Lean statement: D5/S3/Quantum/Algebra/DegeneracyGraphDeterminantRecurrence.pruningRowEquiv

Formalization. D5/S3/Quantum/Algebra/DegeneracyGraphDeterminantRecurrence.pruningRowEquiv (✓ 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 the exact occupied-degree and pruning recurrence used to reindex the source square. The construction retains actual parent fibers and carries the induced row and column permutations explicitly.

Definition 1.15 (pruningColumnEquiv).

Lean statement: D5/S3/Quantum/Algebra/DegeneracyGraphDeterminantRecurrence.pruningColumnEquiv

Formalization. D5/S3/Quantum/Algebra/DegeneracyGraphDeterminantRecurrence.pruningColumnEquiv (✓ 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 the exact occupied-degree and pruning recurrence used to reindex the source square. The construction retains actual parent fibers and carries the induced row and column permutations explicitly.

Definition 1.16 (NewtonPruningMatrix).

Lean statement: D5/S3/Quantum/Algebra/DegeneracyGraphDeterminantRecurrence.NewtonPruningMatrix

Formalization. D5/S3/Quantum/Algebra/DegeneracyGraphDeterminantRecurrence.NewtonPruningMatrix (✓ 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 the exact occupied-degree and pruning recurrence used to reindex the source square. The construction retains actual parent fibers and carries the induced row and column permutations explicitly.

Definition 1.17 (pruningDegree).

Lean statement: D5/S3/Quantum/Algebra/DegeneracyGraphDeterminantRecurrence.pruningDegree

Formalization. D5/S3/Quantum/Algebra/DegeneracyGraphDeterminantRecurrence.pruningDegree (✓ 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 the exact occupied-degree and pruning recurrence used to reindex the source square. The construction retains actual parent fibers and carries the induced row and column permutations explicitly.

Theorem 1.18 (NewtonPruningMatrix_apply_low).

Lean statement: D5/S3/Quantum/Algebra/DegeneracyGraphDeterminantRecurrence.NewtonPruningMatrix_apply_low

Proof. Machine-checked in Lean as D5/S3/Quantum/Algebra/DegeneracyGraphDeterminantRecurrence.NewtonPruningMatrix_apply_low (✓ 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 the exact occupied-degree and pruning recurrence used to reindex the source square. The construction retains actual parent fibers and carries the induced row and column permutations explicitly.

Theorem 1.19 (NewtonPruningMatrix_blockTriangular).

Lean statement: D5/S3/Quantum/Algebra/DegeneracyGraphDeterminantRecurrence.NewtonPruningMatrix_blockTriangular

Proof. Machine-checked in Lean as D5/S3/Quantum/Algebra/DegeneracyGraphDeterminantRecurrence.NewtonPruningMatrix_blockTriangular (✓ 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 the exact occupied-degree and pruning recurrence used to reindex the source square. The construction retains actual parent fibers and carries the induced row and column permutations explicitly.

Definition 1.20 (SourceSquare).

Lean statement: D5/S3/Quantum/Algebra/DegeneracyGraphDeterminantRecurrence.SourceSquare

Formalization. D5/S3/Quantum/Algebra/DegeneracyGraphDeterminantRecurrence.SourceSquare (✓ 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 the exact occupied-degree and pruning recurrence used to reindex the source square. The construction retains actual parent fibers and carries the induced row and column permutations explicitly.

Definition 1.21 (pruningBlockEquiv).

Lean statement: D5/S3/Quantum/Algebra/DegeneracyGraphDeterminantRecurrence.pruningBlockEquiv

Formalization. D5/S3/Quantum/Algebra/DegeneracyGraphDeterminantRecurrence.pruningBlockEquiv (✓ 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 the exact occupied-degree and pruning recurrence used to reindex the source square. The construction retains actual parent fibers and carries the induced row and column permutations explicitly.

Theorem 1.22 (NewtonPruningMatrix_diagonal_block_reindex).

Lean statement: D5/S3/Quantum/Algebra/DegeneracyGraphDeterminantRecurrence.NewtonPruningMatrix_diagonal_block_reindex

Proof. Machine-checked in Lean as D5/S3/Quantum/Algebra/DegeneracyGraphDeterminantRecurrence.NewtonPruningMatrix_diagonal_block_reindex (✓ 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 the exact occupied-degree and pruning recurrence used to reindex the source square. The construction retains actual parent fibers and carries the induced row and column permutations explicitly.

Theorem 1.23 (det_NewtonPruningMatrix_blocks).

Lean statement: D5/S3/Quantum/Algebra/DegeneracyGraphDeterminantRecurrence.det_NewtonPruningMatrix_blocks

Proof. Machine-checked in Lean as D5/S3/Quantum/Algebra/DegeneracyGraphDeterminantRecurrence.det_NewtonPruningMatrix_blocks (✓ 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 the exact occupied-degree and pruning recurrence used to reindex the source square. The construction retains actual parent fibers and carries the induced row and column permutations explicitly.

Definition 1.24 (pruningPermutation).

Lean statement: D5/S3/Quantum/Algebra/DegeneracyGraphDeterminantRecurrence.pruningPermutation

Formalization. D5/S3/Quantum/Algebra/DegeneracyGraphDeterminantRecurrence.pruningPermutation (✓ 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 the exact occupied-degree and pruning recurrence used to reindex the source square. The construction retains actual parent fibers and carries the induced row and column permutations explicitly.

Theorem 1.25 (sourceSquare_det_recurrence_mathlib).

Lean statement: D5/S3/Quantum/Algebra/DegeneracyGraphDeterminantRecurrence.sourceSquare_det_recurrence_mathlib

Proof. Machine-checked in Lean as D5/S3/Quantum/Algebra/DegeneracyGraphDeterminantRecurrence.sourceSquare_det_recurrence_mathlib (✓ 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 the exact occupied-degree and pruning recurrence used to reindex the source square. The construction retains actual parent fibers and carries the induced row and column permutations explicitly.

Definition 1.26 (sourceSiblingVandermonde).

Lean statement: D5/S3/Quantum/Algebra/DegeneracyGraphDeterminantRecurrence.sourceSiblingVandermonde

Formalization. D5/S3/Quantum/Algebra/DegeneracyGraphDeterminantRecurrence.sourceSiblingVandermonde (✓ 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 the exact occupied-degree and pruning recurrence used to reindex the source square. The construction retains actual parent fibers and carries the induced row and column permutations explicitly.

Definition 1.27 (fiberOrientationSign).

Lean statement: D5/S3/Quantum/Algebra/DegeneracyGraphDeterminantRecurrence.fiberOrientationSign

Formalization. D5/S3/Quantum/Algebra/DegeneracyGraphDeterminantRecurrence.fiberOrientationSign (✓ 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 the exact occupied-degree and pruning recurrence used to reindex the source square. The construction retains actual parent fibers and carries the induced row and column permutations explicitly.

Definition 1.28 (pruningRecurrenceSign).

Lean statement: D5/S3/Quantum/Algebra/DegeneracyGraphDeterminantRecurrence.pruningRecurrenceSign

Formalization. D5/S3/Quantum/Algebra/DegeneracyGraphDeterminantRecurrence.pruningRecurrenceSign (✓ 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 the exact occupied-degree and pruning recurrence used to reindex the source square. The construction retains actual parent fibers and carries the induced row and column permutations explicitly.

Theorem 1.29 (sourceSquare_det_pruning_recurrence).

Lean statement: D5/S3/Quantum/Algebra/DegeneracyGraphDeterminantRecurrence.sourceSquare_det_pruning_recurrence

Proof. Machine-checked in Lean as D5/S3/Quantum/Algebra/DegeneracyGraphDeterminantRecurrence.sourceSquare_det_pruning_recurrence (✓ 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 the exact occupied-degree and pruning recurrence used to reindex the source square. The construction retains actual parent fibers and carries the induced row and column permutations explicitly.

References