Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Degeneracy Graph Determinant: Source Model

Abstract

The arbitrary-depth source tree, threshold columns, leaf-path evaluation, and determinant input are formalized with parent-dependent fibers and sibling-only labels.

This owner records the complete public inventory of the source model. SourceTree carries all levels and coherent ancestor maps; Survives and sourceThreshold implement the recursive threshold rule; Columns and RawM are the literal source column and leaf-path evaluation objects. Labels are required to be injective only within a sibling block, so unrelated parents may reuse labels. The downstream owners consume this exact inventory in import order.

The formal target is Kemp–Ramgoolam, Gauge-string duality, monomial bases and graph determinants, arXiv:2603.05259v2, Sections 2, 3, 6, and 7. The source calls the arbitrary-depth monomial basis and determinant statements conjectures; this delivery resolves the exact clauses only through the stated Lean declarations. Neidinger 2019 and Sauer 2004 are recorded in the Library note as conditional global-grid comparisons, not as proofs of this parent-dependent case.

Definition 1.1 (SourceTree).

Lean statement: D5/S3/Quantum/Algebra/DegeneracyGraphDeterminant.SourceTree

Formalization. D5/S3/Quantum/Algebra/DegeneracyGraphDeterminant.SourceTree (✓ 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 public declaration is part of the source-faithful arbitrary-depth graph model. Its displayed type is projected directly from the Lean declaration; no global grid, uniform fiber, or depth restriction is added.

Definition 1.2 (sourcePositiveComposition).

Lean statement: D5/S3/Quantum/Algebra/DegeneracyGraphDeterminant.sourcePositiveComposition

Formalization. D5/S3/Quantum/Algebra/DegeneracyGraphDeterminant.sourcePositiveComposition (✓ 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 public declaration is part of the source-faithful arbitrary-depth graph model. Its displayed type is projected directly from the Lean declaration; no global grid, uniform fiber, or depth restriction is added.

Definition 1.3 (Survives).

Lean statement: D5/S3/Quantum/Algebra/DegeneracyGraphDeterminant.Survives

Formalization. D5/S3/Quantum/Algebra/DegeneracyGraphDeterminant.Survives (✓ 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 public declaration is part of the source-faithful arbitrary-depth graph model. Its displayed type is projected directly from the Lean declaration; no global grid, uniform fiber, or depth restriction is added.

Definition 1.4 (survivalSet).

Lean statement: D5/S3/Quantum/Algebra/DegeneracyGraphDeterminant.survivalSet

Formalization. D5/S3/Quantum/Algebra/DegeneracyGraphDeterminant.survivalSet (✓ 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 public declaration is part of the source-faithful arbitrary-depth graph model. Its displayed type is projected directly from the Lean declaration; no global grid, uniform fiber, or depth restriction is added.

Definition 1.5 (survivingChildren).

Lean statement: D5/S3/Quantum/Algebra/DegeneracyGraphDeterminant.survivingChildren

Formalization. D5/S3/Quantum/Algebra/DegeneracyGraphDeterminant.survivingChildren (✓ 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 public declaration is part of the source-faithful arbitrary-depth graph model. Its displayed type is projected directly from the Lean declaration; no global grid, uniform fiber, or depth restriction is added.

Theorem 1.6 (survives_step_iff).

Lean statement: D5/S3/Quantum/Algebra/DegeneracyGraphDeterminant.survives_step_iff

Proof. Machine-checked in Lean as D5/S3/Quantum/Algebra/DegeneracyGraphDeterminant.survives_step_iff (✓ 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 public declaration is part of the source-faithful arbitrary-depth graph model. Its displayed type is projected directly from the Lean declaration; no global grid, uniform fiber, or depth restriction is added.

Definition 1.7 (Exponents).

Lean statement: D5/S3/Quantum/Algebra/DegeneracyGraphDeterminant.Exponents

Formalization. D5/S3/Quantum/Algebra/DegeneracyGraphDeterminant.Exponents (✓ 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 public declaration is part of the source-faithful arbitrary-depth graph model. Its displayed type is projected directly from the Lean declaration; no global grid, uniform fiber, or depth restriction is added.

Definition 1.8 (sourceThreshold).

Lean statement: D5/S3/Quantum/Algebra/DegeneracyGraphDeterminant.sourceThreshold

Formalization. D5/S3/Quantum/Algebra/DegeneracyGraphDeterminant.sourceThreshold (✓ 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 public declaration is part of the source-faithful arbitrary-depth graph model. Its displayed type is projected directly from the Lean declaration; no global grid, uniform fiber, or depth restriction is added.

Definition 1.9 (sourceS).

Lean statement: D5/S3/Quantum/Algebra/DegeneracyGraphDeterminant.sourceS

Formalization. D5/S3/Quantum/Algebra/DegeneracyGraphDeterminant.sourceS (✓ 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 public declaration is part of the source-faithful arbitrary-depth graph model. Its displayed type is projected directly from the Lean declaration; no global grid, uniform fiber, or depth restriction is added.

Definition 1.10 (Columns).

Lean statement: D5/S3/Quantum/Algebra/DegeneracyGraphDeterminant.Columns

Formalization. D5/S3/Quantum/Algebra/DegeneracyGraphDeterminant.Columns (✓ 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 public declaration is part of the source-faithful arbitrary-depth graph model. Its displayed type is projected directly from the Lean declaration; no global grid, uniform fiber, or depth restriction is added.

Definition 1.11 (RawM).

Lean statement: D5/S3/Quantum/Algebra/DegeneracyGraphDeterminant.RawM

Formalization. D5/S3/Quantum/Algebra/DegeneracyGraphDeterminant.RawM (✓ 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 public declaration is part of the source-faithful arbitrary-depth graph model. Its displayed type is projected directly from the Lean declaration; no global grid, uniform fiber, or depth restriction is added.

Definition 1.12 (Bottom).

Lean statement: D5/S3/Quantum/Algebra/DegeneracyGraphDeterminant.Bottom

Formalization. D5/S3/Quantum/Algebra/DegeneracyGraphDeterminant.Bottom (✓ 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 public declaration is part of the source-faithful arbitrary-depth graph model. Its displayed type is projected directly from the Lean declaration; no global grid, uniform fiber, or depth restriction is added.

Definition 1.13 (Penultimate).

Lean statement: D5/S3/Quantum/Algebra/DegeneracyGraphDeterminant.Penultimate

Formalization. D5/S3/Quantum/Algebra/DegeneracyGraphDeterminant.Penultimate (✓ 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 public declaration is part of the source-faithful arbitrary-depth graph model. Its displayed type is projected directly from the Lean declaration; no global grid, uniform fiber, or depth restriction is added.

Definition 1.14 (bottomFiber).

Lean statement: D5/S3/Quantum/Algebra/DegeneracyGraphDeterminant.bottomFiber

Formalization. D5/S3/Quantum/Algebra/DegeneracyGraphDeterminant.bottomFiber (✓ 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 public declaration is part of the source-faithful arbitrary-depth graph model. Its displayed type is projected directly from the Lean declaration; no global grid, uniform fiber, or depth restriction is added.

Definition 1.15 (occupiedPenultimate).

Lean statement: D5/S3/Quantum/Algebra/DegeneracyGraphDeterminant.occupiedPenultimate

Formalization. D5/S3/Quantum/Algebra/DegeneracyGraphDeterminant.occupiedPenultimate (✓ 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 public declaration is part of the source-faithful arbitrary-depth graph model. Its displayed type is projected directly from the Lean declaration; no global grid, uniform fiber, or depth restriction is added.

Definition 1.16 (retainedVertex).

Lean statement: D5/S3/Quantum/Algebra/DegeneracyGraphDeterminant.retainedVertex

Formalization. D5/S3/Quantum/Algebra/DegeneracyGraphDeterminant.retainedVertex (✓ 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 public declaration is part of the source-faithful arbitrary-depth graph model. Its displayed type is projected directly from the Lean declaration; no global grid, uniform fiber, or depth restriction is added.

Definition 1.17 (reachesOccupied).

Lean statement: D5/S3/Quantum/Algebra/DegeneracyGraphDeterminant.reachesOccupied

Formalization. D5/S3/Quantum/Algebra/DegeneracyGraphDeterminant.reachesOccupied (✓ 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 public declaration is part of the source-faithful arbitrary-depth graph model. Its displayed type is projected directly from the Lean declaration; no global grid, uniform fiber, or depth restriction is added.

Theorem 1.18 (survives_reachesOccupied).

Lean statement: D5/S3/Quantum/Algebra/DegeneracyGraphDeterminant.survives_reachesOccupied

Proof. Machine-checked in Lean as D5/S3/Quantum/Algebra/DegeneracyGraphDeterminant.survives_reachesOccupied (✓ 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 public declaration is part of the source-faithful arbitrary-depth graph model. Its displayed type is projected directly from the Lean declaration; no global grid, uniform fiber, or depth restriction is added.

Theorem 1.19 (survives_descendant).

Lean statement: D5/S3/Quantum/Algebra/DegeneracyGraphDeterminant.survives_descendant

Proof. Machine-checked in Lean as D5/S3/Quantum/Algebra/DegeneracyGraphDeterminant.survives_descendant (✓ 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 public declaration is part of the source-faithful arbitrary-depth graph model. Its displayed type is projected directly from the Lean declaration; no global grid, uniform fiber, or depth restriction is added.

Definition 1.20 (appendThreshold).

Lean statement: D5/S3/Quantum/Algebra/DegeneracyGraphDeterminant.appendThreshold

Formalization. D5/S3/Quantum/Algebra/DegeneracyGraphDeterminant.appendThreshold (✓ 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 public declaration is part of the source-faithful arbitrary-depth graph model. Its displayed type is projected directly from the Lean declaration; no global grid, uniform fiber, or depth restriction is added.

Definition 1.21 (prune).

Lean statement: D5/S3/Quantum/Algebra/DegeneracyGraphDeterminant.prune

Formalization. D5/S3/Quantum/Algebra/DegeneracyGraphDeterminant.prune (✓ 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 public declaration is part of the source-faithful arbitrary-depth graph model. Its displayed type is projected directly from the Lean declaration; no global grid, uniform fiber, or depth restriction is added.

Theorem 1.22 (prune_survives_iff).

Lean statement: D5/S3/Quantum/Algebra/DegeneracyGraphDeterminant.prune_survives_iff

Proof. Machine-checked in Lean as D5/S3/Quantum/Algebra/DegeneracyGraphDeterminant.prune_survives_iff (✓ 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 public declaration is part of the source-faithful arbitrary-depth graph model. Its displayed type is projected directly from the Lean declaration; no global grid, uniform fiber, or depth restriction is added.

Definition 1.23 (liftExponents).

Lean statement: D5/S3/Quantum/Algebra/DegeneracyGraphDeterminant.liftExponents

Formalization. D5/S3/Quantum/Algebra/DegeneracyGraphDeterminant.liftExponents (✓ 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 public declaration is part of the source-faithful arbitrary-depth graph model. Its displayed type is projected directly from the Lean declaration; no global grid, uniform fiber, or depth restriction is added.

Definition 1.24 (restrictExponents).

Lean statement: D5/S3/Quantum/Algebra/DegeneracyGraphDeterminant.restrictExponents

Formalization. D5/S3/Quantum/Algebra/DegeneracyGraphDeterminant.restrictExponents (✓ 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 public declaration is part of the source-faithful arbitrary-depth graph model. Its displayed type is projected directly from the Lean declaration; no global grid, uniform fiber, or depth restriction is added.

Definition 1.25 (liftColumn).

Lean statement: D5/S3/Quantum/Algebra/DegeneracyGraphDeterminant.liftColumn

Formalization. D5/S3/Quantum/Algebra/DegeneracyGraphDeterminant.liftColumn (✓ 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 public declaration is part of the source-faithful arbitrary-depth graph model. Its displayed type is projected directly from the Lean declaration; no global grid, uniform fiber, or depth restriction is added.

Definition 1.26 (restrictColumn).

Lean statement: D5/S3/Quantum/Algebra/DegeneracyGraphDeterminant.restrictColumn

Formalization. D5/S3/Quantum/Algebra/DegeneracyGraphDeterminant.restrictColumn (✓ 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 public declaration is part of the source-faithful arbitrary-depth graph model. Its displayed type is projected directly from the Lean declaration; no global grid, uniform fiber, or depth restriction is added.

Definition 1.27 (lastExponentSliceEquiv).

Lean statement: D5/S3/Quantum/Algebra/DegeneracyGraphDeterminant.lastExponentSliceEquiv

Formalization. D5/S3/Quantum/Algebra/DegeneracyGraphDeterminant.lastExponentSliceEquiv (✓ 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 public declaration is part of the source-faithful arbitrary-depth graph model. Its displayed type is projected directly from the Lean declaration; no global grid, uniform fiber, or depth restriction is added.

Theorem 1.28 (column_last_occupied).

Lean statement: D5/S3/Quantum/Algebra/DegeneracyGraphDeterminant.column_last_occupied

Proof. Machine-checked in Lean as D5/S3/Quantum/Algebra/DegeneracyGraphDeterminant.column_last_occupied (✓ 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 public declaration is part of the source-faithful arbitrary-depth graph model. Its displayed type is projected directly from the Lean declaration; no global grid, uniform fiber, or depth restriction is added.

Definition 1.29 (depthOneExponents).

Lean statement: D5/S3/Quantum/Algebra/DegeneracyGraphDeterminant.depthOneExponents

Formalization. D5/S3/Quantum/Algebra/DegeneracyGraphDeterminant.depthOneExponents (✓ 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 public declaration is part of the source-faithful arbitrary-depth graph model. Its displayed type is projected directly from the Lean declaration; no global grid, uniform fiber, or depth restriction is added.

Definition 1.30 (depthOneColumnsEquiv).

Lean statement: D5/S3/Quantum/Algebra/DegeneracyGraphDeterminant.depthOneColumnsEquiv

Formalization. D5/S3/Quantum/Algebra/DegeneracyGraphDeterminant.depthOneColumnsEquiv (✓ 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 public declaration is part of the source-faithful arbitrary-depth graph model. Its displayed type is projected directly from the Lean declaration; no global grid, uniform fiber, or depth restriction is added.

Definition 1.31 (depthOneBottomOrder).

Lean statement: D5/S3/Quantum/Algebra/DegeneracyGraphDeterminant.depthOneBottomOrder

Formalization. D5/S3/Quantum/Algebra/DegeneracyGraphDeterminant.depthOneBottomOrder (✓ 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 public declaration is part of the source-faithful arbitrary-depth graph model. Its displayed type is projected directly from the Lean declaration; no global grid, uniform fiber, or depth restriction is added.

Definition 1.32 (fiberOrder).

Lean statement: D5/S3/Quantum/Algebra/DegeneracyGraphDeterminant.fiberOrder

Formalization. D5/S3/Quantum/Algebra/DegeneracyGraphDeterminant.fiberOrder (✓ 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 public declaration is part of the source-faithful arbitrary-depth graph model. Its displayed type is projected directly from the Lean declaration; no global grid, uniform fiber, or depth restriction is added.

Definition 1.33 (bottomParent).

Lean statement: D5/S3/Quantum/Algebra/DegeneracyGraphDeterminant.bottomParent

Formalization. D5/S3/Quantum/Algebra/DegeneracyGraphDeterminant.bottomParent (✓ 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 public declaration is part of the source-faithful arbitrary-depth graph model. Its displayed type is projected directly from the Lean declaration; no global grid, uniform fiber, or depth restriction is added.

Definition 1.34 (bottomInFiber).

Lean statement: D5/S3/Quantum/Algebra/DegeneracyGraphDeterminant.bottomInFiber

Formalization. D5/S3/Quantum/Algebra/DegeneracyGraphDeterminant.bottomInFiber (✓ 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 public declaration is part of the source-faithful arbitrary-depth graph model. Its displayed type is projected directly from the Lean declaration; no global grid, uniform fiber, or depth restriction is added.

Definition 1.35 (fiberRank).

Lean statement: D5/S3/Quantum/Algebra/DegeneracyGraphDeterminant.fiberRank

Formalization. D5/S3/Quantum/Algebra/DegeneracyGraphDeterminant.fiberRank (✓ 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 public declaration is part of the source-faithful arbitrary-depth graph model. Its displayed type is projected directly from the Lean declaration; no global grid, uniform fiber, or depth restriction is added.

Definition 1.36 (fiberNewton).

Lean statement: D5/S3/Quantum/Algebra/DegeneracyGraphDeterminant.fiberNewton

Formalization. D5/S3/Quantum/Algebra/DegeneracyGraphDeterminant.fiberNewton (✓ 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 public declaration is part of the source-faithful arbitrary-depth graph model. Its displayed type is projected directly from the Lean declaration; no global grid, uniform fiber, or depth restriction is added.

Definition 1.37 (NewtonE).

Lean statement: D5/S3/Quantum/Algebra/DegeneracyGraphDeterminant.NewtonE

Formalization. D5/S3/Quantum/Algebra/DegeneracyGraphDeterminant.NewtonE (✓ 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 public declaration is part of the source-faithful arbitrary-depth graph model. Its displayed type is projected directly from the Lean declaration; no global grid, uniform fiber, or depth restriction is added.

Definition 1.38 (fiberValues).

Lean statement: D5/S3/Quantum/Algebra/DegeneracyGraphDeterminant.fiberValues

Formalization. D5/S3/Quantum/Algebra/DegeneracyGraphDeterminant.fiberValues (✓ 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 public declaration is part of the source-faithful arbitrary-depth graph model. Its displayed type is projected directly from the Lean declaration; no global grid, uniform fiber, or depth restriction is added.

Definition 1.39 (fiberEvaluation).

Lean statement: D5/S3/Quantum/Algebra/DegeneracyGraphDeterminant.fiberEvaluation

Formalization. D5/S3/Quantum/Algebra/DegeneracyGraphDeterminant.fiberEvaluation (✓ 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 public declaration is part of the source-faithful arbitrary-depth graph model. Its displayed type is projected directly from the Lean declaration; no global grid, uniform fiber, or depth restriction is added.

Definition 1.40 (fiberCoefficient).

Lean statement: D5/S3/Quantum/Algebra/DegeneracyGraphDeterminant.fiberCoefficient

Formalization. D5/S3/Quantum/Algebra/DegeneracyGraphDeterminant.fiberCoefficient (✓ 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 public declaration is part of the source-faithful arbitrary-depth graph model. Its displayed type is projected directly from the Lean declaration; no global grid, uniform fiber, or depth restriction is added.

Theorem 1.41 (fiberRank_order).

Lean statement: D5/S3/Quantum/Algebra/DegeneracyGraphDeterminant.fiberRank_order

Proof. Machine-checked in Lean as D5/S3/Quantum/Algebra/DegeneracyGraphDeterminant.fiberRank_order (✓ 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 public declaration is part of the source-faithful arbitrary-depth graph model. Its displayed type is projected directly from the Lean declaration; no global grid, uniform fiber, or depth restriction is added.

Theorem 1.42 (det_NewtonE).

Lean statement: D5/S3/Quantum/Algebra/DegeneracyGraphDeterminant.det_NewtonE

Proof. Machine-checked in Lean as D5/S3/Quantum/Algebra/DegeneracyGraphDeterminant.det_NewtonE (✓ 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 public declaration is part of the source-faithful arbitrary-depth graph model. Its displayed type is projected directly from the Lean declaration; no global grid, uniform fiber, or depth restriction is added.

Theorem 1.43 (det_NewtonE_ne_zero).

Lean statement: D5/S3/Quantum/Algebra/DegeneracyGraphDeterminant.det_NewtonE_ne_zero

Proof. Machine-checked in Lean as D5/S3/Quantum/Algebra/DegeneracyGraphDeterminant.det_NewtonE_ne_zero (✓ 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 public declaration is part of the source-faithful arbitrary-depth graph model. Its displayed type is projected directly from the Lean declaration; no global grid, uniform fiber, or depth restriction is added.

References