PathCHSNormClosedForm

Abstract

Complete homogeneous symmetric functions of finite path spectra.

Theorem 1.1 (The path matrix is Hermitian).

$$\forall n\in \mathbb{N},\mathrm{Matrix}.\mathrm{IsHermitian}\left(\mathrm{Matrix}.\mathrm{of}\left(\mathrm{fun}(i:\mathrm{Fin}\left(n\right))\mapsto \mathrm{fun}(j:\mathrm{Fin}\left(n\right))\mapsto \mathrm{if}(((i:\mathbb{N})+1=(j:\mathbb{N}))\vee ((j:\mathbb{N})+1=(i:\mathbb{N})))\mathrm{then}(1:\mathbb{R})\mathrm{else}0\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Graph/PathCHS/PathCHSNormClosedForm.pathAdjHermitian (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Ángel Chávez, Sarah Fullerton, Matilda LaFortune, Keyron Linarez, Nethmin Liyanage, Justin Son and Tyler Ting (2023). Extremal polynomial norms of graphs. DOI: 10.48550/arXiv.2311.04689. URL: https://arxiv.org/abs/2311.04689v3.

Commentary.

The entry with indices i and j equals the entry with indices j and i. The matrix is the adjacency matrix of the path with vertices Fin n.

Definition 1.2 (Complete homogeneous symmetric value).

$$\forall n\in \mathbb{N},\forall d\in \mathbb{N},\mathrm{chs}\left(n,d\right)=\mathrm{MvPolynomial}.\mathrm{eval}\left(\mathrm{Matrix}.\mathrm{IsHermitian}.\mathrm{eigenvalues}\left(\mathrm{pathAdjHermitian}\left(n\right)\right),\mathrm{MvPolynomial}.\mathrm{hsymm}\left(\mathrm{Fin}\left(n\right),\mathbb{R},d\right)\right)$$

Formalization. D5/S3/Combinatorics/Graph/PathCHS/PathCHSNormClosedForm.chs (✓ std3).

Citation. Ángel Chávez, Sarah Fullerton, Matilda LaFortune, Keyron Linarez, Nethmin Liyanage, Justin Son and Tyler Ting (2023). Extremal polynomial norms of graphs. DOI: 10.48550/arXiv.2311.04689. URL: https://arxiv.org/abs/2311.04689v3.

Commentary.

Page 2, Equation (1.1): “∑{d=0}^{∞} h_d(x₁, x₂, …, x_n) t^d = ∏{i=1}^{n} 1/(1 − x_i t).” The polynomial hsymm is evaluated at the real eigenvalues of the path adjacency matrix.

Definition 1.3 (The complete homogeneous symmetric norm).

$$\forall n\in \mathbb{N},\forall d\in \mathbb{N},\mathrm{chsNorm}\left(n,d\right)=\mathrm{chs}{\left(n,d\right)}^{\frac{(1:\mathbb{R})}{(d:\mathbb{R})}}$$

Formalization. D5/S3/Combinatorics/Graph/PathCHS/PathCHSNormClosedForm.chsNorm (✓ std3).

Citation. Ángel Chávez, Sarah Fullerton, Matilda LaFortune, Keyron Linarez, Nethmin Liyanage, Justin Son and Tyler Ting (2023). Extremal polynomial norms of graphs. DOI: 10.48550/arXiv.2311.04689. URL: https://arxiv.org/abs/2311.04689v3.

Commentary.

Page 2, Theorem 1.4: “Suppose d ≥ 2 is even. The following function defines a norm on H_n: ‖A‖_d = h_d(λ₁, λ₂, …, λ_n)^{1/d}.” Natural d is cast to ℝ in the reciprocal exponent.

Definition 1.4 (Finite second-difference expression).

$$\forall n\in \mathbb{N},\forall m\in \mathbb{N},\mathrm{pathFormula}\left(n,m\right)=\sum _{k\in \mathrm{Finset}.\mathrm{range}\left(\mathrm{Nat}.\mathrm{div}\left(m,n+1\right)+1\right)}((D5.S0.\mathrm{Conventions}.\mathrm{IntegerIndexBinomial}.\mathrm{binom}\left(2\cdot m+n-1,(m:\mathbb{Z})-(k:\mathbb{Z})\cdot \left((n:\mathbb{Z})+1\right)\right):\mathbb{Z})-2\cdot (D5.S0.\mathrm{Conventions}.\mathrm{IntegerIndexBinomial}.\mathrm{binom}\left(2\cdot m+n-1,(m:\mathbb{Z})-(k:\mathbb{Z})\cdot \left((n:\mathbb{Z})+1\right)-1\right):\mathbb{Z})+(D5.S0.\mathrm{Conventions}.\mathrm{IntegerIndexBinomial}.\mathrm{binom}\left(2\cdot m+n-1,(m:\mathbb{Z})-(k:\mathbb{Z})\cdot \left((n:\mathbb{Z})+1\right)-2\right):\mathbb{Z}))$$

Formalization. D5/S3/Combinatorics/Graph/PathCHS/PathCHSNormClosedForm.pathFormula (✓ std3).

Source. Repository-derived.

Acknowledgement. Ángel Chávez, Sarah Fullerton, Matilda LaFortune, Keyron Linarez, Nethmin Liyanage, Justin Son and Tyler Ting (2023). Extremal polynomial norms of graphs. DOI: 10.48550/arXiv.2311.04689. URL: https://arxiv.org/abs/2311.04689v3.

Commentary.

The upper index is 2m+n−1. Nat.div is natural-number quotient. Each binomial value is cast to ℤ before subtraction.

Definition 1.5 (Problem 1 for path norms).

$$\mathrm{claim}=\left(\forall n\in \mathbb{N},\forall m\in \mathbb{N},(1\le n)\to (2\le m)\to (\mathrm{chs}\left(n,2\cdot m\right)=(\mathrm{pathFormula}\left(n,m\right):\mathbb{R}))\wedge (\mathrm{chsNorm}\left(n,2\cdot m\right)=(\mathrm{pathFormula}\left(n,m\right):\mathbb{R}{)}^{\frac{(1:\mathbb{R})}{(2\cdot m:\mathbb{R})}})\right)$$

Formalization. D5/S3/Combinatorics/Graph/PathCHS/PathCHSNormClosedForm.claim (✓ std3).

Source. Repository-derived.

Acknowledgement. Ángel Chávez, Sarah Fullerton, Matilda LaFortune, Keyron Linarez, Nethmin Liyanage, Justin Son and Tyler Ting (2023). Extremal polynomial norms of graphs. DOI: 10.48550/arXiv.2311.04689. URL: https://arxiv.org/abs/2311.04689v3.

Commentary.

Page 14, Section 5, Problem 1: “The path of order n has m = n − 1 edges. Proposition 5.14 (a) therefore implies that ‖P_n‖₂ = √(n − 1). However, computing ‖P_n‖_d for d ≥ 4 seems unattainable at the moment. We leave this is an interesting open problem. Problem 1. Compute ‖P_n‖_d for d ≥ 4.” Here n ≥ 1 and d=2m with m ≥ 2; both the symmetric polynomial and its real root are specified.

Theorem 1.6 (A geometric series times its denominator).

$$\forall R\in \mathrm{Type},[\mathrm{CommRing}\left(R\right)]\forall a\in R,\mathrm{PowerSeries}.\mathrm{mk}\left(\mathrm{fun}(k:\mathbb{N})\mapsto a^k\right)\cdot (1-\mathrm{PowerSeries}.C\left(a\right)\cdot \mathrm{PowerSeries}.X)=1$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Graph/PathCHS/PathCHSNormClosedForm.geometric_mul_linear (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Ángel Chávez, Sarah Fullerton, Matilda LaFortune, Keyron Linarez, Nethmin Liyanage, Justin Son and Tyler Ting (2023). Extremal polynomial norms of graphs. DOI: 10.48550/arXiv.2311.04689. URL: https://arxiv.org/abs/2311.04689v3.

Commentary.

Rescaling the geometric series gives the inverse of 1−aX over any commutative ring.

Theorem 1.7 (The symmetric-polynomial generating function).

$$\forall I\in \mathrm{Type},\forall R\in \mathrm{Type},[\mathrm{Fintype}\left(I\right)][\mathrm{DecidableEq}\left(I\right)][\mathrm{CommRing}\left(R\right)]\forall a\in I\to R,\mathrm{PowerSeries}.\mathrm{mk}\left(\mathrm{fun}(d:\mathbb{N})\mapsto \mathrm{MvPolynomial}.\mathrm{eval}\left(a,\mathrm{MvPolynomial}.\mathrm{hsymm}\left(I,R,d\right)\right)\right)\cdot \prod _{i:I}(1-\mathrm{PowerSeries}.C\left(a\left(i\right)\right)\cdot \mathrm{PowerSeries}.X)=1$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Graph/PathCHS/PathCHSNormClosedForm.hsymm_series_product (✓ std3). ∎

Citation. Ángel Chávez, Sarah Fullerton, Matilda LaFortune, Keyron Linarez, Nethmin Liyanage, Justin Son and Tyler Ting (2023). Extremal polynomial norms of graphs. DOI: 10.48550/arXiv.2311.04689. URL: https://arxiv.org/abs/2311.04689v3.

Commentary.

Equation (1.1), page 2, gives the generating function. Grouping monomials by total degree gives the reciprocal product of the linear factors over a commutative ring.

Theorem 1.8 (Ring homomorphisms and constant-weight continuants).

$$\forall R\in \mathrm{Type},\forall S\in \mathrm{Type},[\mathrm{CommRing}\left(R\right)][\mathrm{CommRing}\left(S\right)]\forall f\in R\to +\ast S,\forall x\in R,\forall n\in \mathbb{N},f\left(D5.S3.\mathrm{Combinatorics}.\mathrm{NarayanaStrip}.\mathrm{CiglerStripProductAlgebra}.\mathrm{cont}\left(\mathrm{Function}.\mathrm{const}\left(\mathbb{N},x\right),1,1,n\right)\right)=D5.S3.\mathrm{Combinatorics}.\mathrm{NarayanaStrip}.\mathrm{CiglerStripProductAlgebra}.\mathrm{cont}\left(\mathrm{Function}.\mathrm{const}\left(\mathbb{N},f\left(x\right)\right),1,1,n\right)$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Graph/PathCHS/PathCHSNormClosedForm.continuant_map (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Ángel Chávez, Sarah Fullerton, Matilda LaFortune, Keyron Linarez, Nethmin Liyanage, Justin Son and Tyler Ting (2023). Extremal polynomial norms of graphs. DOI: 10.48550/arXiv.2311.04689. URL: https://arxiv.org/abs/2311.04689v3.

Commentary.

A ring homomorphism preserves the initial values and the second-order recurrence.

Theorem 1.9 (The zero-weight continuant).

$$\forall R\in \mathrm{Type},[\mathrm{CommRing}\left(R\right)]\forall n\in \mathbb{N},D5.S3.\mathrm{Combinatorics}.\mathrm{NarayanaStrip}.\mathrm{CiglerStripProductAlgebra}.\mathrm{cont}\left(\mathrm{Function}.\mathrm{const}\left(\mathbb{N},(0:R)\right),1,1,n\right)=1$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Graph/PathCHS/PathCHSNormClosedForm.continuant_zero (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Ángel Chávez, Sarah Fullerton, Matilda LaFortune, Keyron Linarez, Nethmin Liyanage, Justin Son and Tyler Ting (2023). Extremal polynomial norms of graphs. DOI: 10.48550/arXiv.2311.04689. URL: https://arxiv.org/abs/2311.04689v3.

Commentary.

At zero weight every term of the continuant is one.

Theorem 1.10 (The reciprocal path continuant).

$$\forall n\in \mathbb{N},\mathrm{PowerSeries}.\mathrm{mk}\left(\mathrm{fun}(d:\mathbb{N})\mapsto \mathrm{chs}\left(n,d\right)\right)\cdot D5.S3.\mathrm{Combinatorics}.\mathrm{NarayanaStrip}.\mathrm{CiglerStripProductAlgebra}.\mathrm{cont}\left(\mathrm{Function}.\mathrm{const}\left(\mathbb{N},(\mathrm{PowerSeries}.X:\mathrm{PowerSeries}\left(\mathbb{R}\right){)}^2\right),1,1,n\right)=1$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Graph/PathCHS/PathCHSNormClosedForm.path_hsymm_series (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Ángel Chávez, Sarah Fullerton, Matilda LaFortune, Keyron Linarez, Nethmin Liyanage, Justin Son and Tyler Ting (2023). Extremal polynomial norms of graphs. DOI: 10.48550/arXiv.2311.04689. URL: https://arxiv.org/abs/2311.04689v3.

Commentary.

The product over adjacency eigenvalues is the path determinant. Its reciprocal generates the symmetric polynomials.

Theorem 1.11 (Even-degree values).

$$\forall n\in \mathbb{N},\forall m\in \mathbb{N},\mathrm{chs}\left(n,2\cdot m\right)=(\mathrm{pathFormula}\left(n,m\right):\mathbb{R})$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Graph/PathCHS/PathCHSNormClosedForm.chs_formula (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Ángel Chávez, Sarah Fullerton, Matilda LaFortune, Keyron Linarez, Nethmin Liyanage, Justin Son and Tyler Ting (2023). Extremal polynomial norms of graphs. DOI: 10.48550/arXiv.2311.04689. URL: https://arxiv.org/abs/2311.04689v3.

Commentary.

For x(1+q)²=q, the recurrence identity (1+q)ⁿ cont(x;1,1;n)(1−q)=1−qⁿ⁺¹ holds at every order n. It supplies the reciprocal-continuant substitution; the Catalan coefficient transform then gives a binomial second difference and a geometric series of reflections.

Theorem 1.12 (Closed form for every even path norm).

$$\forall n\in \mathbb{N},\forall m\in \mathbb{N},(1\le n)\to (2\le m)\to (\mathrm{chs}\left(n,2\cdot m\right)=(\mathrm{pathFormula}\left(n,m\right):\mathbb{R}))\wedge (\mathrm{chsNorm}\left(n,2\cdot m\right)=(\mathrm{pathFormula}\left(n,m\right):\mathbb{R}{)}^{\frac{(1:\mathbb{R})}{(2\cdot m:\mathbb{R})}})$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Graph/PathCHS/PathCHSNormClosedForm.result (✓ std3). ∎

Resolves. Problems/chavez-2023-path-chs-norm-closed-form (proved) by D5/S3/Combinatorics/Graph/PathCHS/PathCHSNormClosedForm.result.

Source. Repository-derived.

Acknowledgement. Ángel Chávez, Sarah Fullerton, Matilda LaFortune, Keyron Linarez, Nethmin Liyanage, Justin Son and Tyler Ting (2023). Extremal polynomial norms of graphs. DOI: 10.48550/arXiv.2311.04689. URL: https://arxiv.org/abs/2311.04689v3.

Commentary.

The second-difference expression gives the complete homogeneous symmetric value and hence its real root.

Theorem 1.13 (Degree of the monic Chebyshev polynomial).

$$\forall K\in \mathrm{Type},[\mathrm{Field}\left(K\right)][\mathrm{CharZero}\left(K\right)]\forall n\in \mathbb{N},\mathrm{Polynomial}.\mathrm{natDegree}\left(\mathrm{Polynomial}.\mathrm{Chebyshev}.S\left(K,(n:\mathbb{Z})\right)\right)=n$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Graph/PathCHS/PathCHSNormClosedForm.chebS_degree (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Ángel Chávez, Sarah Fullerton, Matilda LaFortune, Keyron Linarez, Nethmin Liyanage, Justin Son and Tyler Ting (2023). Extremal polynomial norms of graphs. DOI: 10.48550/arXiv.2311.04689. URL: https://arxiv.org/abs/2311.04689v3.

Commentary.

The identity with the second-kind Chebyshev polynomial after scaling the variable gives degree n.

References

• Truth anchor: D5/S3/Combinatorics/Graph/PathCHS/PathCHSNormClosedForm.chebS_degree
• Truth anchor: D5/S3/Combinatorics/Graph/PathCHS/PathCHSNormClosedForm.chs
• Truth anchor: D5/S3/Combinatorics/Graph/PathCHS/PathCHSNormClosedForm.chsNorm
• Truth anchor: D5/S3/Combinatorics/Graph/PathCHS/PathCHSNormClosedForm.chs_formula
• Truth anchor: D5/S3/Combinatorics/Graph/PathCHS/PathCHSNormClosedForm.claim
• Truth anchor: D5/S3/Combinatorics/Graph/PathCHS/PathCHSNormClosedForm.continuant_map
• Truth anchor: D5/S3/Combinatorics/Graph/PathCHS/PathCHSNormClosedForm.continuant_zero
• Truth anchor: D5/S3/Combinatorics/Graph/PathCHS/PathCHSNormClosedForm.geometric_mul_linear
• Truth anchor: D5/S3/Combinatorics/Graph/PathCHS/PathCHSNormClosedForm.hsymm_series_product
• Truth anchor: D5/S3/Combinatorics/Graph/PathCHS/PathCHSNormClosedForm.pathAdjHermitian
• Truth anchor: D5/S3/Combinatorics/Graph/PathCHS/PathCHSNormClosedForm.pathFormula
• Truth anchor: D5/S3/Combinatorics/Graph/PathCHS/PathCHSNormClosedForm.path_hsymm_series
• Truth anchor: D5/S3/Combinatorics/Graph/PathCHS/PathCHSNormClosedForm.result
• Dependency: D5/S0/Conventions/IntegerIndexBinomial
• Dependency: D5/S1/Recurrence/Invariants/CompositionalIterateCongruence
• Dependency: D5/S3/Combinatorics/NarayanaStrip/CiglerStripProductContinuants
• Dependency: D5/S3/Combinatorics/Nonnesting/CatalanLagrangeBridge
• Dependency: D5/S3/Quantum/FockSpace/ForbiddenNeighbourDeterminant