Tree endpoint moment certificates

Abstract

Actual rooted finite tree recurrence states and every-order positive Jacobi rigidity.

The coefficient field is arbitrary where stated. Algebraic pairing needs only a field; positivity and the tree norm statements use a linearly ordered field. All vertices and the selected port belong to the same actual finite graph. No spectral, positivity, cyclicity, contraction or oracle premise is added to that graph.

Definition 1.1 (The original spectral coordinate).

$$\forall K\in \mathrm{Type},[\mathrm{Field}\left(K\right)]\forall a\in K,\forall c\in K,\mathrm{affinePolynomial}\left(a,c\right)=C\left(c^{-1}\right)\cdot \left(X-C\left(a\right)\right)$$

Formalization. D5/S3/Combinatorics/SpectralGraph/TreeEndpointMomentCertificates.affinePolynomial (✓ std3).

Source. Repository-derived.

Commentary.

Here X denotes the polynomial indeterminate and scalars denote constant polynomials. The formula is c inverse times (X minus a).

Definition 1.2 (The fixed chain polynomials).

$$\forall K\in \mathrm{Type},[\mathrm{Field}\left(K\right)]\forall a\in K,\forall c\in K,\forall j\in \mathrm{Nat},\mathrm{chainPolynomial}\left(a,c,j\right)=\mathrm{comp}\left(\mathrm{ChebyshevS}\left(K,j\right),\mathrm{affinePolynomial}\left(a,c\right)\right)$$

Formalization. D5/S3/Combinatorics/SpectralGraph/TreeEndpointMomentCertificates.chainPolynomial (✓ std3).

Source. Repository-derived.

Commentary.

Mathlib Chebyshev.S has S minus one equal to zero, S zero equal to one, and S at j plus one equal to X times S at j minus S at j minus one. Thus this is precisely the original Q recurrence composed with (z-a)/c; no polynomial is fitted to the observed graph.

Definition 1.3 (Evaluation at the actual matrix).

$$\forall K\in \mathrm{Type},[\mathrm{Field}\left(K\right)]\forall V\in \mathrm{Type},[\mathrm{Fintype}\left(V\right)][\mathrm{DecidableEq}\left(V\right)]\forall M\in \mathrm{Matrix}\left(V,V,K\right),\forall o\in V,\forall p\in \mathrm{Polynomial}\left(K\right),\mathrm{polynomialVector}\left(M,o,p\right)=\mathrm{mulVec}\left(\mathrm{aeval}\left(M,p\right),\mathrm{unit}\left(o\right)\right)$$

Formalization. D5/S3/Combinatorics/SpectralGraph/TreeEndpointMomentCertificates.polynomialVector (✓ std3).

Source. Repository-derived.

Commentary.

Polynomial evaluation is in the matrix algebra; the resulting matrix acts on the selected unit coordinate.

Definition 1.4 (Chain states).

$$\forall K\in \mathrm{Type},[\mathrm{Field}\left(K\right)]\forall V\in \mathrm{Type},[\mathrm{Fintype}\left(V\right)][\mathrm{DecidableEq}\left(V\right)]\forall M\in \mathrm{Matrix}\left(V,V,K\right),\forall o\in V,\forall a\in K,\forall c\in K,\forall j\in \mathrm{Nat},\mathrm{chainVector}\left(M,o,a,c,j\right)=\mathrm{polynomialVector}\left(M,o,\mathrm{chainPolynomial}\left(a,c,j\right)\right)$$

Formalization. D5/S3/Combinatorics/SpectralGraph/TreeEndpointMomentCertificates.chainVector (✓ std3).

Source. Repository-derived.

Commentary.

The index is a natural number, beginning with the actual selected unit vector.

Definition 1.5 (All positive symmetric Jacobi matrices).

$$\forall K\in \mathrm{Type},[\mathrm{Field}\left(K\right)][\mathrm{LinearOrder}\left(K\right)]\forall n\in \mathrm{Nat},\forall J\in \mathrm{Matrix}\left(\mathrm{Fin}\left(n\right),\mathrm{Fin}\left(n\right),K\right),\mathrm{PositiveJacobi}\left(J\right)\iff \left(\mathrm{IsSymm}\left(J\right)\wedge \left(\left(\forall i\in \mathrm{Fin}\left(n\right),\forall j\in \mathrm{Fin}\left(n\right),\left(\mathrm{val}\left(i\right)+1<\mathrm{val}\left(j\right)\vee \mathrm{val}\left(j\right)+1<\mathrm{val}\left(i\right)\right)\Rightarrow J\left(i,j\right)=0\right)\wedge \left(\forall j\in \mathrm{Nat},j+1<n\Rightarrow 0<J\left(j,j+1\right)\right)\right)\right)$$

Formalization. D5/S3/Combinatorics/SpectralGraph/TreeEndpointMomentCertificates.PositiveJacobi (✓ std3).

Source. Repository-derived.

Commentary.

Every natural order is allowed. The matrix is symmetric, entries farther than one from the diagonal vanish, and every existing adjacent link is strictly positive. The diagonals are unrestricted. The positive-order hypothesis is supplied only where an endpoint vector is needed.

Definition 1.6 (Absent coordinates mean zero).

$$\forall K\in \mathrm{Type},[\mathrm{Field}\left(K\right)]\forall n\in \mathrm{Nat},\forall j\in \mathrm{Nat},\forall i\in \mathrm{Fin}\left(n\right),\mathrm{unitAt}\left(n,j\right)\left(i\right)=\mathrm{ite}\left(\mathrm{val}\left(i\right)=j,1,0\right)$$

Formalization. D5/S3/Combinatorics/SpectralGraph/TreeEndpointMomentCertificates.unitAt (✓ std3).

Source. Repository-derived.

Commentary.

The zero extension lets the rigidity proof treat short, exact and larger matrix orders in the same recurrence.

Definition 1.7 (Zero-extended diagonals).

$$\forall K\in \mathrm{Type},[\mathrm{Field}\left(K\right)]\forall n\in \mathrm{Nat},\forall J\in \mathrm{Matrix}\left(\mathrm{Fin}\left(n\right),\mathrm{Fin}\left(n\right),K\right),\forall j\in \mathrm{Nat},\mathrm{diagonalAt}\left(J,j\right)=\mathrm{ite}\left(j<n,J\left(j,j\right),0\right)$$

Formalization. D5/S3/Combinatorics/SpectralGraph/TreeEndpointMomentCertificates.diagonalAt (✓ std3).

Source. Repository-derived.

Commentary.

The displayed entry uses its natural-number index only in the branch where that index is in range.

Definition 1.8 (Zero-extended links).

$$\forall K\in \mathrm{Type},[\mathrm{Field}\left(K\right)]\forall n\in \mathrm{Nat},\forall J\in \mathrm{Matrix}\left(\mathrm{Fin}\left(n\right),\mathrm{Fin}\left(n\right),K\right),\forall j\in \mathrm{Nat},\mathrm{nextLink}\left(J,j\right)=\mathrm{ite}\left(j+1<n,J\left(j,j+1\right),0\right)$$

Formalization. D5/S3/Combinatorics/SpectralGraph/TreeEndpointMomentCertificates.nextLink (✓ std3).

Source. Repository-derived.

Commentary.

There is no fictitious terminal link: the value is zero when its second endpoint is absent.

Definition 1.9 (A locally saturated actual stem).

$$\forall V\in \mathrm{Type},\forall G\in \mathrm{SimpleGraph}\left(V\right),\forall o\in V,\forall z\in V,\forall p\in \mathrm{Walk}\left(G,o,z\right),\mathrm{IsStem}\left(p\right)\iff \left(\forall j\in \mathrm{Nat},j<\mathrm{length}\left(p\right)\Rightarrow \left(\forall x\in V,\mathrm{Adj}\left(G,\mathrm{getVert}\left(p,j\right),x\right)\iff \left(\left(0<j\wedge x=\mathrm{getVert}\left(p,j-1\right)\right)\vee x=\mathrm{getVert}\left(p,j+1\right)\right)\right)\right)$$

Formalization. D5/S3/Combinatorics/SpectralGraph/TreeEndpointMomentCertificates.IsStem (✓ std3).

Source. Repository-derived.

Commentary.

At every proper stem vertex, all actual neighbors are exactly the preceding vertex when present and the following vertex. This predicate alone does not assert existence; the tree theorem earns a simple path satisfying it.

Definition 1.10 (The actual terminal boundary).

$$\forall V\in \mathrm{Type},[\mathrm{Fintype}\left(V\right)][\mathrm{DecidableEq}\left(V\right)]\forall G\in \mathrm{SimpleGraph}\left(V\right),[\mathrm{DecidableRel}\left(\mathrm{Adj}\left(G\right)\right)]\forall o\in V,\forall z\in V,\forall p\in \mathrm{Walk}\left(G,o,z\right),\forall x\in V,\mathrm{mem}\left(x,\mathrm{forward}\left(p\right)\right)\iff \left(\mathrm{Adj}\left(G,z,x\right)\wedge \left(\mathrm{length}\left(p\right)=0\vee x\ne \mathrm{penultimate}\left(p\right)\right)\right)$$

Formalization. D5/S3/Combinatorics/SpectralGraph/TreeEndpointMomentCertificates.forward (✓ std3).

Source. Repository-derived.

Commentary.

Only the incoming edge is removed. A zero-length stem removes no edge, so its forward boundary is the actual root’s entire neighbor set.

Definition 1.11 (Rooted endpoint paths).

$$\forall V\in \mathrm{Type},\forall G\in \mathrm{SimpleGraph}\left(V\right),\forall o\in V,\mathrm{EndpointPath}\left(G,o\right)\iff \left(\exists n\in \mathrm{Nat},\exists e\in \mathrm{GraphIso}\left(G,\mathrm{pathGraph}\left(n+1\right)\right),e\left(o\right)=0\right)$$

Formalization. D5/S3/Combinatorics/SpectralGraph/TreeEndpointMomentCertificates.EndpointPath (✓ std3).

Source. Repository-derived.

Commentary.

A genuine graph isomorphism to a nonempty finite path sends the actual selected port to zero. This includes a singleton and excludes an interior port on a nontrivial path.

Definition 1.12 (The same actual graph law).

$$\forall K\in \mathrm{Type},[\mathrm{Field}\left(K\right)]\forall V\in \mathrm{Type},[\mathrm{DecidableEq}\left(V\right)]\forall G\in \mathrm{SimpleGraph}\left(V\right),[\mathrm{DecidableRel}\left(\mathrm{Adj}\left(G\right)\right)]\forall a\in K,\forall c\in K,\mathrm{uniformMatrix}\left(G,a,c\right)=a\cdot \mathrm{identity}\left(V\right)+c\cdot \mathrm{adjMatrix}\left(K,G\right)$$

Formalization. D5/S3/Combinatorics/SpectralGraph/TreeEndpointMomentCertificates.uniformMatrix (✓ std3).

Source. Repository-derived.

Commentary.

The adjacency matrix has unit edges and zero diagonal. The shift a is arbitrary, including zero and negative values.

Definition 1.13 (Squared recurrence norms).

$$\forall K\in \mathrm{Type},[\mathrm{Field}\left(K\right)]\forall V\in \mathrm{Type},[\mathrm{Fintype}\left(V\right)][\mathrm{DecidableEq}\left(V\right)]\forall M\in \mathrm{Matrix}\left(V,V,K\right),\forall o\in V,\forall a\in K,\forall c\in K,\forall j\in \mathrm{Nat},\mathrm{chainNorm}\left(M,o,a,c,j\right)=\mathrm{dotProduct}\left(\mathrm{chainVector}\left(M,o,a,c,j\right),\mathrm{chainVector}\left(M,o,a,c,j\right)\right)$$

Formalization. D5/S3/Combinatorics/SpectralGraph/TreeEndpointMomentCertificates.chainNorm (✓ std3).

Source. Repository-derived.

Commentary.

Over the rationals this dot product is the exact sum of squares defining the squared Euclidean length; no square-root normalization is used.

Definition 1.14 (Actual boundary indicators).

$$\forall K\in \mathrm{Type},[\mathrm{Field}\left(K\right)]\forall V\in \mathrm{Type},[\mathrm{DecidableEq}\left(V\right)]\forall s\in \mathrm{Finset}\left(V\right),\forall x\in V,\mathrm{indicatorVector}\left(s\right)\left(x\right)=\mathrm{ite}\left(\mathrm{mem}\left(x,s\right),1,0\right)$$

Formalization. D5/S3/Combinatorics/SpectralGraph/TreeEndpointMomentCertificates.indicatorVector (✓ std3).

Source. Repository-derived.

Commentary.

The value is one exactly on the given finite set of actual vertices.

Theorem 1.15 (Moments determine the needed Gram entries).

$$\forall K\in \mathrm{Type},[\mathrm{Field}\left(K\right)]\forall V\in \mathrm{Type},[\mathrm{Fintype}\left(V\right)][\mathrm{DecidableEq}\left(V\right)]\forall W\in \mathrm{Type},[\mathrm{Fintype}\left(W\right)][\mathrm{DecidableEq}\left(W\right)]\forall M\in \mathrm{Matrix}\left(V,V,K\right),\forall J\in \mathrm{Matrix}\left(W,W,K\right),\mathrm{IsSymm}\left(M\right)\Rightarrow \left(\mathrm{IsSymm}\left(J\right)\Rightarrow \left(\forall o\in V,\forall z\in W,\forall a\in K,\forall c\in K,\forall d\in \mathrm{Nat},\forall i\in \mathrm{Nat},\forall j\in \mathrm{Nat},\left(\forall k\in \mathrm{Nat},k\le d\Rightarrow \left(M^k\right)\left(o,o\right)=\left(J^k\right)\left(z,z\right)\right)\Rightarrow \left(i+j\le d\Rightarrow \mathrm{dotProduct}\left(\mathrm{chainVector}\left(M,o,a,c,i\right),\mathrm{chainVector}\left(M,o,a,c,j\right)\right)=\mathrm{dotProduct}\left(\mathrm{chainVector}\left(J,z,a,c,i\right),\mathrm{chainVector}\left(J,z,a,c,j\right)\right)\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/SpectralGraph/TreeEndpointMomentCertificates.prefix_chain_pairing (✓ std3). ∎

Source. Repository-derived.

Commentary.

Expand matrix polynomial evaluation and use symmetry to identify the pairing of powers i and j with moment i+j. The degrees of the fixed chain polynomials are at most their indices. Equal moments through d therefore transfer every pairing with i+j at most d. This helper is consumed by the endpoint classification’s prefix-rigidity step.

Theorem 1.16 (Moments determine the needed diagonal pairings).

$$\forall K\in \mathrm{Type},[\mathrm{Field}\left(K\right)]\forall V\in \mathrm{Type},[\mathrm{Fintype}\left(V\right)][\mathrm{DecidableEq}\left(V\right)]\forall W\in \mathrm{Type},[\mathrm{Fintype}\left(W\right)][\mathrm{DecidableEq}\left(W\right)]\forall M\in \mathrm{Matrix}\left(V,V,K\right),\forall J\in \mathrm{Matrix}\left(W,W,K\right),\mathrm{IsSymm}\left(M\right)\Rightarrow \left(\mathrm{IsSymm}\left(J\right)\Rightarrow \left(\forall o\in V,\forall z\in W,\forall a\in K,\forall c\in K,\forall d\in \mathrm{Nat},\forall j\in \mathrm{Nat},\left(\forall k\in \mathrm{Nat},k\le d\Rightarrow \left(M^k\right)\left(o,o\right)=\left(J^k\right)\left(z,z\right)\right)\Rightarrow \left(2\cdot j+1\le d\Rightarrow \mathrm{dotProduct}\left(\mathrm{chainVector}\left(M,o,a,c,j\right),\mathrm{mulVec}\left(M,\mathrm{chainVector}\left(M,o,a,c,j\right)\right)\right)=\mathrm{dotProduct}\left(\mathrm{chainVector}\left(J,z,a,c,j\right),\mathrm{mulVec}\left(J,\mathrm{chainVector}\left(J,z,a,c,j\right)\right)\right)\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/SpectralGraph/TreeEndpointMomentCertificates.prefix_chain_diagonal (✓ std3). ∎

Source. Repository-derived.

Commentary.

Apply the same polynomial pairing to p_j and X p_j. The total degree is at most 2j+1. This helper is consumed by the same prefix-rigidity step.

Theorem 1.17 (Rigidity without an order bound).

$$\forall K\in \mathrm{Type},[\mathrm{Field}\left(K\right)][\mathrm{LinearOrder}\left(K\right)][\mathrm{IsStrictOrderedRing}\left(K\right)]\forall n\in \mathrm{Nat},\forall r\in \mathrm{Nat},0<n\Rightarrow \left(0<r\Rightarrow \left(\forall J\in \mathrm{Matrix}\left(\mathrm{Fin}\left(n\right),\mathrm{Fin}\left(n\right),K\right),\mathrm{PositiveJacobi}\left(J\right)\Rightarrow \left(\forall a\in K,\forall c\in K,0<c\Rightarrow \left(\left(\forall j\in \mathrm{Nat},j<r\Rightarrow \mathrm{dotProduct}\left(\mathrm{chainVector}\left(J,0,a,c,j\right),\mathrm{chainVector}\left(J,0,a,c,j\right)\right)=1\right)\Rightarrow \left(\left(\forall j\in \mathrm{Nat},j<r\Rightarrow \mathrm{dotProduct}\left(\mathrm{chainVector}\left(J,0,a,c,j\right),\mathrm{mulVec}\left(J,\mathrm{chainVector}\left(J,0,a,c,j\right)\right)\right)=a\right)\Rightarrow \left(r\le n\wedge \left(\left(\forall j\in \mathrm{Nat},j<r\Rightarrow \mathrm{diagonalAt}\left(J,j\right)=a\right)\wedge \left(\left(\forall j\in \mathrm{Nat},j+1<r\Rightarrow \mathrm{nextLink}\left(J,j\right)=c\right)\wedge \mathrm{dotProduct}\left(\mathrm{chainVector}\left(J,0,a,c,r\right),\mathrm{chainVector}\left(J,0,a,c,r\right)\right)={\left(c^{-1}\cdot \mathrm{nextLink}\left(J,r-1\right)\right)}^2\cdot \mathrm{ite}\left(r<n,1,0\right)\right)\right)\right)\right)\right)\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/SpectralGraph/TreeEndpointMomentCertificates.positive_jacobi_prefix_rigidity (✓ std3). ∎

Source. Repository-derived.

Commentary.

Inductively the required unit state forces the next coordinate to exist. Its positive coefficient divided by positive c has square one, hence equals one. The diagonal pairing fixes the next diagonal. Applying the recurrence once more gives the displayed last-link norm, with zero for an exact terminating order. This proves the order bound, all earlier coefficients, and the short, exact and larger-order alternatives over the reals as well as the rationals. No normalized representation or supplied stem is assumed. The classification consumes this result to exclude all rational competitor orders and to force the positive matrix.

Theorem 1.18 (Earn the first departure on the actual tree).

$$\forall K\in \mathrm{Type},[\mathrm{Field}\left(K\right)][\mathrm{LinearOrder}\left(K\right)][\mathrm{IsStrictOrderedRing}\left(K\right)]\forall V\in \mathrm{Type},[\mathrm{Fintype}\left(V\right)][\mathrm{DecidableEq}\left(V\right)]\forall G\in \mathrm{SimpleGraph}\left(V\right),[\mathrm{DecidableRel}\left(\mathrm{Adj}\left(G\right)\right)]\mathrm{IsTree}\left(G\right)\Rightarrow \left(\left(\forall x\in V,\mathrm{degree}\left(G,x\right)\le 3\right)\Rightarrow \left(\forall o\in V,\forall a\in K,\forall c\in K,0<c\Rightarrow \left(\exists z\in V,\exists p\in \mathrm{Walk}\left(G,o,z\right),\mathrm{IsPath}\left(p\right)\wedge \left(\mathrm{IsStem}\left(p\right)\wedge \left(1\le \mathrm{length}\left(p\right)+1\wedge \left(\mathrm{length}\left(p\right)+1\le \mathrm{card}\left(V\right)\wedge \left(\left(\forall i\in \mathrm{Nat},i<\mathrm{length}\left(p\right)+1\Rightarrow \left(\forall j\in \mathrm{Nat},j<\mathrm{length}\left(p\right)+1\Rightarrow \mathrm{dotProduct}\left(\mathrm{chainVector}\left(\mathrm{uniformMatrix}\left(G,a,c\right),o,a,c,i\right),\mathrm{chainVector}\left(\mathrm{uniformMatrix}\left(G,a,c\right),o,a,c,j\right)\right)=\mathrm{ite}\left(i=j,1,0\right)\right)\right)\wedge \left(\left(\forall j\in \mathrm{Nat},j<\mathrm{length}\left(p\right)+1\Rightarrow \mathrm{dotProduct}\left(\mathrm{chainVector}\left(\mathrm{uniformMatrix}\left(G,a,c\right),o,a,c,j\right),\mathrm{mulVec}\left(\mathrm{uniformMatrix}\left(G,a,c\right),\mathrm{chainVector}\left(\mathrm{uniformMatrix}\left(G,a,c\right),o,a,c,j\right)\right)\right)=a\right)\wedge \left(\mathrm{chainNorm}\left(\mathrm{uniformMatrix}\left(G,a,c\right),o,a,c,\mathrm{length}\left(p\right)+1\right)=\mathrm{card}\left(\mathrm{forward}\left(p\right)\right)\wedge \left(\left(\mathrm{card}\left(\mathrm{forward}\left(p\right)\right)=0\vee \left(\mathrm{card}\left(\mathrm{forward}\left(p\right)\right)=2\vee \mathrm{card}\left(\mathrm{forward}\left(p\right)\right)=3\right)\right)\wedge \left(\left(0<\mathrm{length}\left(p\right)\Rightarrow \mathrm{card}\left(\mathrm{forward}\left(p\right)\right)\ne 3\right)\wedge \left(\left(\mathrm{card}\left(\mathrm{forward}\left(p\right)\right)=0\Rightarrow \left(\exists e\in \mathrm{GraphIso}\left(G,\mathrm{pathGraph}\left(\mathrm{length}\left(p\right)+1\right)\right),e\left(o\right)=0\right)\right)\wedge \left(\left(\forall j\in \mathrm{Nat},j<\mathrm{length}\left(p\right)+1\Rightarrow \mathrm{chainVector}\left(\mathrm{uniformMatrix}\left(G,a,c\right),o,a,c,j\right)=\mathrm{unit}\left(\mathrm{getVert}\left(p,j\right)\right)\right)\wedge \mathrm{chainVector}\left(\mathrm{uniformMatrix}\left(G,a,c\right),o,a,c,\mathrm{length}\left(p\right)+1\right)=\mathrm{indicatorVector}\left(\mathrm{forward}\left(p\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/SpectralGraph/TreeEndpointMomentCertificates.tree_first_departure (✓ std3). ∎

Source. Repository-derived.

Commentary.

Choose a maximal simple locally saturated rooted stem among the finitely bounded possible lengths. Acyclicity keeps every forward neighbor off that stem. A single forward neighbor would extend it, so maximality excludes boundary size one. The degree bound leaves only zero, two or three; a positive-length stem has at most two forward neighbors. The actual recurrence states are exactly its distinct coordinate vectors, followed by its actual boundary indicator. Thus all earlier norms are one and the next norm is zero, two or three. If the boundary is empty, connectivity exhausts every actual vertex; the path-to-subgraph isomorphism becomes a genuine rooted isomorphism of the whole graph. The theorem supplies, rather than assumes, every stem, Gram and diagonal premise used by the classification.

References

• Truth anchor: D5/S3/Combinatorics/SpectralGraph/TreeEndpointMomentCertificates.EndpointPath
• Truth anchor: D5/S3/Combinatorics/SpectralGraph/TreeEndpointMomentCertificates.IsStem
• Truth anchor: D5/S3/Combinatorics/SpectralGraph/TreeEndpointMomentCertificates.PositiveJacobi
• Truth anchor: D5/S3/Combinatorics/SpectralGraph/TreeEndpointMomentCertificates.affinePolynomial
• Truth anchor: D5/S3/Combinatorics/SpectralGraph/TreeEndpointMomentCertificates.chainNorm
• Truth anchor: D5/S3/Combinatorics/SpectralGraph/TreeEndpointMomentCertificates.chainPolynomial
• Truth anchor: D5/S3/Combinatorics/SpectralGraph/TreeEndpointMomentCertificates.chainVector
• Truth anchor: D5/S3/Combinatorics/SpectralGraph/TreeEndpointMomentCertificates.diagonalAt
• Truth anchor: D5/S3/Combinatorics/SpectralGraph/TreeEndpointMomentCertificates.forward
• Truth anchor: D5/S3/Combinatorics/SpectralGraph/TreeEndpointMomentCertificates.indicatorVector
• Truth anchor: D5/S3/Combinatorics/SpectralGraph/TreeEndpointMomentCertificates.nextLink
• Truth anchor: D5/S3/Combinatorics/SpectralGraph/TreeEndpointMomentCertificates.polynomialVector
• Truth anchor: D5/S3/Combinatorics/SpectralGraph/TreeEndpointMomentCertificates.positive_jacobi_prefix_rigidity
• Truth anchor: D5/S3/Combinatorics/SpectralGraph/TreeEndpointMomentCertificates.prefix_chain_diagonal
• Truth anchor: D5/S3/Combinatorics/SpectralGraph/TreeEndpointMomentCertificates.prefix_chain_pairing
• Truth anchor: D5/S3/Combinatorics/SpectralGraph/TreeEndpointMomentCertificates.tree_first_departure
• Truth anchor: D5/S3/Combinatorics/SpectralGraph/TreeEndpointMomentCertificates.uniformMatrix
• Truth anchor: D5/S3/Combinatorics/SpectralGraph/TreeEndpointMomentCertificates.unitAt