Shapiro Conjecture 1(iii): identity words on finite trees

Boris Shapiro, Transposition Cayley Spectra and Subgraph Counts, arXiv:2610.14373v1, Section 4.1, page 14, Conjecture 1(iii), states:

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.

Each edge acts by the transposition of its endpoints. Multiplication uses $(\sigma\rho)(v)=\sigma(\rho(v))$. Alternating occurrences of distinct letters are crossings; nested pairs are allowed. The one-vertex tree and empty word are included.

Statement echo

| Source clause | Lean counterpart | Fidelity | | --- | --- | --- | | Every finite tree | n : ℕ, T : SimpleGraph (Fin n), T.IsTree in claim | Relabeling of $[n]$; no bound on $n$ | | A word in the edges | w : List (Sym2 (Fin n)); every member belongs to T.edgeFinset | No nonedge letters | | Length twice the edge count | w.length = 2 * T.edgeFinset.card | Exact equality | | Uses every edge | Every member of T.edgeFinset belongs to w | Onto edge support | | Product is identity | (w.map edgeSwap).prod = 1 | Existing endpoint transposition; literal list product | | Every edge occurs twice | w.count a = 2 for each tree edge | Exact multiplicity | | Every vertex's incident subword is noncrossing | NoncrossingDoubleOccurrence of the order-preserving membership filter | Existing Crossing predicate on the position pairs | | If and only if | Both directions of result : claim | No dropped clause |

NoncrossingDoubleOccurrence displays the source convention literally: every occurring letter has two copies and distinct letters have no crossing position pairs. claim retains the preregistered body. The proofs reuse SupportAndEdgeWordReflection.edgeSwap and NoncrossingNonnestingGraphRecurrence.Crossing.

The theorem replaces the bounded verification of the local criterion by a uniform proof for all finite trees. It identifies the local obstruction to an identity word of minimal onto-support length.

The externally named target is preregistered in issue #22558. The source labels it a conjecture and checks trees with at most five edges. The literature screen in that issue covers the source, citation indexes, star-factorization results of Goulden–Jackson and Irving–Rattan, and Irving's planar-constellation correspondence. No explicit settlement of the fixed-tree criterion was located in that searched scope. Classical ingredients are not claimed as new. Literature completeness is ASSUMED-UNVERIFIED.

The following helper names are private declarations in D5.S3.Combinatorics.Graph.SupportForestMoments.ShapiroTreeIdentityWords.

ShapiroProbe.multiplicity_two uses acyclicity: an edge used exactly once would transport a vertex across the cut left by deleting that edge. Positivity of every edge count and the total length then force all counts to be two.

ShapiroList.interval_cancellation applies to any monoid with involutive labels and commuting labels at alternating pairs. It replaces a contiguous interval by its letters occurring exactly once, in their original order. The proof selects a repeated pair with a duplicate-free interior, commutes its label across that interior, cancels the pair, and uses strong induction.

ShapiroProbe.distinct_forest_fixed says that a product of distinct forest edges fixes a vertex exactly when no used edge is incident to that vertex. ShapiroLeaf.leaf_interval extracts a fixed-neighbor constraint from the two copies of a leaf edge. In ShapiroMain.identity_separated, cancellation and the distinct-edge criterion rule out crossings with that leaf edge; deleting the leaf edge gives the induction step. Conversely, vertex-disjoint edge transpositions commute, and interval cancellation proves sufficiency.

A finite tree and onto edge word of length twice its edge count for which identity product differs from the stated multiplicity-and-local condition would contradict the target. A cyclic graph is outside its hypotheses. Source-fidelity checks must retain alternating crossings while allowing nested pairs and the empty word.

The settling declaration is D5.S3.Combinatorics.Graph.SupportForestMoments.ShapiroTreeIdentityWords.result. It proves the complete claim. The axiom closure of every public declaration is contained in {propext, Classical.choice, Quot.sound}; some declarations may be axiom-free. The Scribe carries one Proved resolution claim on result.

Escape audit unfinished: issue #24676. The target is the public theorem result. The enrolled Boolean-iff template and dependent-family interface do not themselves provide a compiled source reconstruction, occurrence ties, variation, sensitivity, or observational dependence for this guarded dependent family. No Reg source or declared_validated registration is claimed.

Exact finite experiment

The source experiment is docs/reports/tree-identity-words/ in the-omega-institute/trureturing-experiments, at immutable commit 82686ecf6f80257b272bc14b5d427bb34ccb3ab1. The SHA-256 of check.py is 1f7bd589e624ef83cc5fec145cea34830c58bace8300fda30d91f935f3e6e16c. Command: git -C ../trureturing-experiments show 82686ecf6f80257b272bc14b5d427bb34ccb3ab1:docs/reports/tree-identity-words/check.py | python3 -; exit 0. It checks all 14 tree shapes with zero through five edges and all 688,148 double-occurrence words, reproduces the 13 published table values, counts all onto identity words by exact meet-in-the-middle enumeration, and independently checks every onto word through four edges.

For the cyclic boundary, the same pinned script's evaluate and local_noncrossing functions were evaluated using python3 -i /Users/auric/.sshx/2bc38f0950403d9de62688cf/attempt-1/experiment-check.py (the byte-identical script above); exit 0. The tested graph has edges $((0,1),(1,2),(0,2))$ and word $(0,1,2,0,1,2)$, with occurrence pairs $((0,3),(1,4),(2,5))$. The computed permutation is $(0,1,2)$, the identity, and the local noncrossing value is false. This is a finite computation only.

theorem: the named Conjecture 1(iii) is proved.

What the settlement shows

1. Proved, kernel-checked: result establishes the equivalence for every finite tree. The necessity mechanism is the leaf interval and distinct forest-edge support criterion; sufficiency uses commuting crossing labels.
2. Proved in prose using kernel-checked helpers: ShapiroMain.identity_separated, ShapiroProbe.multiplicity_two, and ShapiroProbe.distinct_forest_fixed assume only acyclicity, allowing isolated vertices. Together with ShapiroPattern.local_iff and ShapiroList.interval_cancellation, the same implications give the finite forest analogue: multiplicity two follows from onto support and length, identity implies separated alternating edges, the local condition is equivalent to separation, and commuting disjoint labels give identity. This assembled consequence is proved in prose using those helpers; the only exported settling theorem is for trees.
3. Proved, kernel-checked: ShapiroList.interval_cancellation is generic over a monoid. It requires involutive labels and commuting labels at every alternating pair in a double word, and applies to each contiguous interval.
4. Computed: acyclicity cannot be removed wholesale. The triangle instance in the experiment entry has identity product and fails the local condition. It is neither a tree counterexample nor a Lean-certified graph extension.
5. Open as a delivery boundary: no Lean Catalan enumeration is delivered. Shapiro states that (iii) implies the star formula (i), by counting noncrossing pairings and their edge labelings. That enumeration has classical antecedents; no novelty or open-status claim about (i) is made.
6. Open as a delivery boundary: the cycle formula (ii), inversion, and broader reconstruction are outside this settlement. Their mathematical status is not determined by this proof; separate repository results are not included in this resolution claim.

The settlement supplies the local criterion used in the source's implication to the star formula. It makes no further claim about the source's remaining problems.

Literature completeness, publication priority, and whether an unlocated explicit consequence of the constellation machinery supplies this exact criterion are ASSUMED-UNVERIFIED. The source-to-Lean correspondence is a fidelity judgment; kernel checking establishes the encoded proposition. The finite experiment establishes only its stated tested range.