Identity edge words on finite trees

Abstract

Leaf intervals characterize identity words on every finite tree.

Definition 1.1 (Noncrossing double occurrence words).

$$\forall (n:\mathbb{N}),\forall (w:\mathrm{List}\left(Sym2\left(\mathrm{Fin}\left(n\right)\right)\right)),\mathrm{NoncrossingDoubleOccurrence}\left(w\right)\iff ((\forall (a:Sym2\left(\mathrm{Fin}\left(n\right)\right)),(a\in w)\Rightarrow (List.count\left(a,w\right)=2))\wedge (\forall (i:\mathrm{Fin}\left(List.length\left(w\right)\right)),\forall (j:\mathrm{Fin}\left(List.length\left(w\right)\right)),\forall (k:\mathrm{Fin}\left(List.length\left(w\right)\right)),\forall (l:\mathrm{Fin}\left(List.length\left(w\right)\right)),(w[i]=w[j])\Rightarrow ((w[k]=w[l])\Rightarrow ((w[i]\ne w[k])\Rightarrow (\neg NoncrossingNonnestingGraphRecurrence.Crossing\left((i,j),(k,l)\right))))))$$

Formalization. D5/S3/Combinatorics/Graph/SupportForestMoments/ShapiroTreeIdentityWords.NoncrossingDoubleOccurrence (✓ std3).

Citation. Boris Shapiro (2026). Transposition Cayley Spectra and Subgraph Counts. URL: https://arxiv.org/abs/2610.14373v1.

Commentary.

Page 14, Conjecture 1(iii): “For a tree T, a word of length 2|E(T)| in the edges of T using every edge has product 1 if and only if every edge occurs exactly twice and, for every vertex x of T, the subword formed by the edges incident to x is a non-crossing double occurrence word.” For this term, every occurring letter has two copies. The existing Crossing predicate compares the position pairs (i,j) and (k,l); it forbids both alternating orders. Nested pairs and the empty word are allowed.

Definition 1.2 (Shapiro’s local tree criterion).

$$claim\iff (\forall (n:\mathbb{N}),\forall (T:\mathrm{SimpleGraph}\left(\mathrm{Fin}\left(n\right)\right)),\forall (w:\mathrm{List}\left(Sym2\left(\mathrm{Fin}\left(n\right)\right)\right)),(SimpleGraph.IsTree\left(T\right))\Rightarrow ((\forall (a:Sym2\left(\mathrm{Fin}\left(n\right)\right)),(a\in w)\Rightarrow (a\in SimpleGraph.edgeFinset\left(T\right)))\Rightarrow ((List.length\left(w\right)=2\cdot Finset.card\left(SimpleGraph.edgeFinset\left(T\right)\right))\Rightarrow ((\forall (a:Sym2\left(\mathrm{Fin}\left(n\right)\right)),(a\in SimpleGraph.edgeFinset\left(T\right))\Rightarrow (a\in w))\Rightarrow (List.prod\left(List.map\left(SupportAndEdgeWordReflection.edgeSwap,w\right)\right)=1\iff ((\forall (a:Sym2\left(\mathrm{Fin}\left(n\right)\right)),(a\in SimpleGraph.edgeFinset\left(T\right))\Rightarrow (List.count\left(a,w\right)=2))\wedge (\forall (x:\mathrm{Fin}\left(n\right)),\mathrm{NoncrossingDoubleOccurrence}\left(List.filter\left(fun(a:Sym2\left(\mathrm{Fin}\left(n\right)\right))\mapsto \mathrm{decide}\left(x\in a\right),w\right)\right))))))))$$

Formalization. D5/S3/Combinatorics/Graph/SupportForestMoments/ShapiroTreeIdentityWords.claim (✓ std3).

Citation. Boris Shapiro (2026). Transposition Cayley Spectra and Subgraph Counts. URL: https://arxiv.org/abs/2610.14373v1.

Commentary.

Page 14, Conjecture 1(iii): “For a tree T, a word of length 2|E(T)| in the edges of T using every edge has product 1 if and only if every edge occurs exactly twice and, for every vertex x of T, the subword formed by the edges incident to x is a non-crossing double occurrence word.” Fin n relabels the source’s vertex set [n]. Sym2 represents unordered endpoint pairs. SimpleGraph.IsTree supplies connectedness and acyclicity; the two membership hypotheses say that the word contains only tree edges and uses every tree edge. List.prod multiplies the endpoint transpositions in list order, with (sigma * rho)(v) = sigma(rho(v)). List.filter retains the original order and tests decidable endpoint membership. The length is twice the edge count, including the empty word on the one-vertex tree.

Theorem 1.3 (The local tree criterion holds).

$$\forall (n:\mathbb{N}),\forall (T:\mathrm{SimpleGraph}\left(\mathrm{Fin}\left(n\right)\right)),\forall (w:\mathrm{List}\left(Sym2\left(\mathrm{Fin}\left(n\right)\right)\right)),(SimpleGraph.IsTree\left(T\right))\Rightarrow ((\forall (a:Sym2\left(\mathrm{Fin}\left(n\right)\right)),(a\in w)\Rightarrow (a\in SimpleGraph.edgeFinset\left(T\right)))\Rightarrow ((List.length\left(w\right)=2\cdot Finset.card\left(SimpleGraph.edgeFinset\left(T\right)\right))\Rightarrow ((\forall (a:Sym2\left(\mathrm{Fin}\left(n\right)\right)),(a\in SimpleGraph.edgeFinset\left(T\right))\Rightarrow (a\in w))\Rightarrow (List.prod\left(List.map\left(SupportAndEdgeWordReflection.edgeSwap,w\right)\right)=1\iff ((\forall (a:Sym2\left(\mathrm{Fin}\left(n\right)\right)),(a\in SimpleGraph.edgeFinset\left(T\right))\Rightarrow (List.count\left(a,w\right)=2))\wedge (\forall (x:\mathrm{Fin}\left(n\right)),\mathrm{NoncrossingDoubleOccurrence}\left(List.filter\left(fun(a:Sym2\left(\mathrm{Fin}\left(n\right)\right))\mapsto \mathrm{decide}\left(x\in a\right),w\right)\right)))))))$$

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

Resolves. Problems/shap2610 (proved) by D5/S3/Combinatorics/Graph/SupportForestMoments/ShapiroTreeIdentityWords.result.

Source. Repository-derived.

Acknowledgement. Boris Shapiro (2026). Transposition Cayley Spectra and Subgraph Counts. URL: https://arxiv.org/abs/2610.14373v1.

Commentary.

Deleting a tree edge separates its endpoints, so an identity word cannot use that edge once. The prescribed total length forces multiplicity two. For a leaf edge, the permutation between its two copies fixes its other endpoint. Cancellation replaces that interval by its singleton letters. A product of distinct forest-edge transpositions fixes exactly the vertices outside those edges, which excludes a crossing with the leaf edge. Induction proves necessity. For sufficiency, crossing edges have disjoint endpoints, their transpositions commute, and repeated pairs cancel.

References

• Truth anchor: D5/S3/Combinatorics/Graph/SupportForestMoments/ShapiroTreeIdentityWords.NoncrossingDoubleOccurrence
• Truth anchor: D5/S3/Combinatorics/Graph/SupportForestMoments/ShapiroTreeIdentityWords.claim
• Truth anchor: D5/S3/Combinatorics/Graph/SupportForestMoments/ShapiroTreeIdentityWords.result
• Dependency: D5/S1/Words/Patterns/NoncrossingNonnestingGraphRecurrence
• Dependency: D5/S3/Combinatorics/Graph/SupportForestMoments/SupportAndEdgeWordReflection