Support forests and edge-word reflection

Abstract

Support counts and sound reflection of edge-word character moments.

Definition 1.1 (Endpoint set).

$$\forall (n:\mathbb{N}),\forall (S:\mathrm{Finset}\left(Sym2\left(\mathrm{Fin}\left(n\right)\right)\right)),endpointSet\left(S\right)=Finset.biUnion\left(S,Sym2.toFinset\right)$$

Formalization. D5/S3/Combinatorics/Graph/SupportForestMoments/SupportAndEdgeWordReflection.endpointSet (✓ std3).

Source. Repository-derived.

Commentary.

The union of the endpoint sets of the unordered edges. Loops, if supplied as raw symmetric pairs, contribute their one endpoint.

Definition 1.2 (Graph on the endpoints).

$$\forall (n:\mathbb{N}),\forall (S:\mathrm{Finset}\left(Sym2\left(\mathrm{Fin}\left(n\right)\right)\right)),endpointGraph\left(S\right)=SimpleGraph.induce\left(SimpleGraph.fromEdgeSet\left((S:\mathrm{Set}\left(Sym2\left(\mathrm{Fin}\left(n\right)\right)\right))\right),(endpointSet\left(S\right):\mathrm{Set}\left(\mathrm{Fin}\left(n\right)\right))\right)$$

Formalization. D5/S3/Combinatorics/Graph/SupportForestMoments/SupportAndEdgeWordReflection.endpointGraph (✓ std3).

Source. Repository-derived.

Commentary.

The graph from the supplied edge set is induced on exactly its endpoints. This induction changes the vertex carrier; it does not impose ambient inducedness.

Definition 1.3 (Support-subgraph count).

$$\forall (n:\mathbb{N}),\forall (h:\mathbb{N}),\forall (G:\mathrm{SimpleGraph}\left(\mathrm{Fin}\left(n\right)\right)),\forall (H:\mathrm{SimpleGraph}\left(\mathrm{Fin}\left(h\right)\right)),N_H\left(G,H\right)=Finset.card\left(Finset.filter\left(fun(S:\mathrm{Finset}\left(Sym2\left(\mathrm{Fin}\left(n\right)\right)\right))\mapsto \mathrm{Nonempty}\left((endpointGraph\left(S\right){\equiv }_{g}H)\right),Finset.powerset\left(SimpleGraph.edgeFinset\left(G\right)\right)\right)\right)$$

Formalization. D5/S3/Combinatorics/Graph/SupportForestMoments/SupportAndEdgeWordReflection.N_H (✓ std3).

Citation. Boris Shapiro (2026). The (n−2,2)-Spectrum of a Graph. URL: https://arxiv.org/abs/2605.17501v2.

Commentary.

Section 6.1, page 5: “For a finite simple graph H without isolated vertices, let N_H(G) denote the number of edge subsets S ⊆ E(G) for which the graph with edge set S and vertex set formed by the endpoints of S is isomorphic to H. No inducedness condition is imposed on the ambient graph G.” Vertices are Fin n and Fin h; each edge subset is counted once, independently of how many isomorphisms it admits.

Definition 1.4 (Fixed points).

$$\forall (n:\mathbb{N}),\forall (sigma:Equiv.Perm\left(\mathrm{Fin}\left(n\right)\right)),c1\left(sigma\right)=Finset.card\left(Finset.filter\left(fun(v:\mathrm{Fin}\left(n\right))\mapsto sigma\left(v\right)=v,(Finset.univ:\mathrm{Finset}\left(\mathrm{Fin}\left(n\right)\right))\right)\right)$$

Formalization. D5/S3/Combinatorics/Graph/SupportForestMoments/SupportAndEdgeWordReflection.c1 (✓ std3).

Citation. Boris Shapiro (2026). The (n−2,2)-Spectrum of a Graph. URL: https://arxiv.org/abs/2605.17501v2.

Commentary.

Section 6, page 4: “If σ ∈ Sₙ, let c₁(σ) be the number of fixed points of σ and let c₂(σ) be the number of two-cycles in its cycle decomposition.” The encoding names these counts c1 and c2. The finite filter tests equality of the permutation value and its input.

Definition 1.5 (Two-cycles).

$$\forall (n:\mathbb{N}),\forall (sigma:Equiv.Perm\left(\mathrm{Fin}\left(n\right)\right)),c2\left(sigma\right)=Multiset.count\left(2,Equiv.Perm.cycleType\left(sigma\right)\right)$$

Formalization. D5/S3/Combinatorics/Graph/SupportForestMoments/SupportAndEdgeWordReflection.c2 (✓ std3).

Citation. Boris Shapiro (2026). The (n−2,2)-Spectrum of a Graph. URL: https://arxiv.org/abs/2605.17501v2.

Commentary.

Section 6, page 4: “If σ ∈ Sₙ, let c₁(σ) be the number of fixed points of σ and let c₂(σ) be the number of two-cycles in its cycle decomposition.” Mathlib’s cycleType omits fixed points and retains the other cycle lengths with multiplicity.

Definition 1.6 (The character).

$$\forall (n:\mathbb{N}),\forall (sigma:Equiv.Perm\left(\mathrm{Fin}\left(n\right)\right)),chi\left(sigma\right)=(Nat.choose\left(c1\left(sigma\right),2\right):\mathbb{Z})+(c2\left(sigma\right):\mathbb{Z})-(c1\left(sigma\right):\mathbb{Z})$$

Formalization. D5/S3/Combinatorics/Graph/SupportForestMoments/SupportAndEdgeWordReflection.chi (✓ std3).

Citation. Boris Shapiro (2026). The (n−2,2)-Spectrum of a Graph. URL: https://arxiv.org/abs/2605.17501v2.

Commentary.

Section 6, page 4, (6.1): chi^(n−2,2)(σ) = binom(c1(σ),2) + c2(σ) − c1(σ). Each natural count is cast to the integers; the subtraction is integer subtraction.

Definition 1.7 (Edge transposition).

$$\forall (n:\mathbb{N}),(edgeSwap:Sym2\left(\mathrm{Fin}\left(n\right)\right)\to Equiv.Perm\left(\mathrm{Fin}\left(n\right)\right))=Sym2.lift\left(⟨Equiv.swap,Equiv.swa{\mathrm{p}}_{\mathrm{comm}}⟩\right)$$

Formalization. D5/S3/Combinatorics/Graph/SupportForestMoments/SupportAndEdgeWordReflection.edgeSwap (✓ std3).

Citation. Boris Shapiro (2026). The (n−2,2)-Spectrum of a Graph. URL: https://arxiv.org/abs/2605.17501v2.

Commentary.

Section 6, page 4: “Let τ_e = (ij) denote the transposition corresponding to an edge e = ij.” Sym2.lift uses Equiv.swap_comm, so the transposition is independent of endpoint order.

Definition 1.8 (Edge-word moment).

$$\forall (n:\mathbb{N}),\forall (G:\mathrm{SimpleGraph}\left(\mathrm{Fin}\left(n\right)\right)),\forall (r:\mathbb{N}),M_{r2}\left(G,r\right)=(\sum _{w:\mathrm{Fin}\left(r\right)\to SimpleGraph.edgeFinset\left(G\right)}(chi\left(List.prod\left(List.ofFn\left(fun(i:\mathrm{Fin}\left(r\right))\mapsto edgeSwap\left(\mathrm{val}\left(w\left(i\right)\right)\right)\right)\right)\right)))$$

Formalization. D5/S3/Combinatorics/Graph/SupportForestMoments/SupportAndEdgeWordReflection.M_r2 (✓ std3).

Citation. Boris Shapiro (2026). The (n−2,2)-Spectrum of a Graph. URL: https://arxiv.org/abs/2605.17501v2.

Commentary.

Section 6, page 4, (6.2): M_r^(2)(G) is the sum over all edge words (e₁,…,e_r) of chi(τ_e₁⋯τ_e_r). List.ofFn lists indices in increasing order and List.prod preserves the displayed multiplication order. The definition uses this right side, as the source identifies it with the trace. The extension r = 0 is included in the evaluator; the inversion statement only uses r = 2, 3, 4.

Definition 1.9 (No isolated vertices).

$$\forall (n:\mathbb{N}),\forall (G:\mathrm{SimpleGraph}\left(\mathrm{Fin}\left(n\right)\right)),noIsolated\left(G\right)\iff (\forall (v:\mathrm{Fin}\left(n\right)),\exists (w:\mathrm{Fin}\left(n\right)),SimpleGraph.Adj\left(G,v,w\right))$$

Formalization. D5/S3/Combinatorics/Graph/SupportForestMoments/SupportAndEdgeWordReflection.noIsolated (✓ std3).

Source. Repository-derived.

Commentary.

Every vertex has an adjacent vertex; the empty vertex carrier satisfies this condition.

Definition 1.10 (Points in two-cycles).

$$\forall (alpha:Type),[\mathrm{Fintype}\left(alpha\right)],[\mathrm{DecidableEq}\left(alpha\right)],\forall (sigma:Equiv.Perm\left(alpha\right)),twoPoints\left(sigma\right)=Finset.sdiff\left(Equiv.Perm.support\left(sigma\right),Equiv.Perm.support\left(sigm{a}^2\right)\right)$$

Formalization. D5/S3/Combinatorics/Graph/SupportForestMoments/SupportAndEdgeWordReflection.twoPoints (✓ std3).

Source. Repository-derived.

Commentary.

A point lies in the support of the permutation but not in the support of its square precisely when its orbit has length two.

Theorem 1.11 (Counting points in two-cycles).

$$\forall (alpha:Type),[\mathrm{Fintype}\left(alpha\right)],[\mathrm{DecidableEq}\left(alpha\right)],\forall (sigma:Equiv.Perm\left(alpha\right)),Finset.card\left(twoPoints\left(sigma\right)\right)=2\cdot Multiset.count\left(2,Equiv.Perm.cycleType\left(sigma\right)\right)$$

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

Source. Repository-derived.

Commentary.

Cycle induction separates a cycle of length two from every other nontrivial cycle. Disjoint products give disjoint unions of these point sets and additive cycle multiplicities.

Theorem 1.12 (Enumerating support counts).

$$\forall (n:\mathbb{N}),\forall (h:\mathbb{N}),\forall (r:\mathbb{N}),\forall (t:\mathbb{N}),\forall (G:\mathrm{SimpleGraph}\left(\mathrm{Fin}\left(n\right)\right)),\forall (H:\mathrm{SimpleGraph}\left(\mathrm{Fin}\left(h\right)\right)),\forall (a:\mathrm{Fin}\left(t\right)\to \mathrm{Finset}\left(Sym2\left(\mathrm{Fin}\left(n\right)\right)\right)),(Function.Injective\left(a\right))\Rightarrow ((Finset.image\left(a,(Finset.univ:\mathrm{Finset}\left(\mathrm{Fin}\left(t\right)\right))\right)=Finset.powersetCard\left(r,SimpleGraph.edgeFinset\left(G\right)\right))\Rightarrow ((Finset.card\left(SimpleGraph.edgeFinset\left(H\right)\right)=r)\Rightarrow (N_H\left(G,H\right)=(\sum _{i:\mathrm{Fin}\left(t\right)}(\mathrm{ite}\left(\mathrm{Nonempty}\left((endpointGraph\left(a\left(i\right)\right){\equiv }_{g}H)\right),1,0\right))))))$$

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

Source. Repository-derived.

Commentary.

An injective enumeration of all r-edge subsets rewrites the support count as a sum of isomorphism indicators, provided H has r edges.

Theorem 1.13 (Matched support enumerations).

$$\forall (n:\mathbb{N}),\forall (h:\mathbb{N}),\forall (r:\mathbb{N}),\forall (t:\mathbb{N}),\forall (G:\mathrm{SimpleGraph}\left(\mathrm{Fin}\left(n\right)\right)),\forall (Gprime:\mathrm{SimpleGraph}\left(\mathrm{Fin}\left(n\right)\right)),\forall (H:\mathrm{SimpleGraph}\left(\mathrm{Fin}\left(h\right)\right)),\forall (a:\mathrm{Fin}\left(t\right)\to \mathrm{Finset}\left(Sym2\left(\mathrm{Fin}\left(n\right)\right)\right)),\forall (b:\mathrm{Fin}\left(t\right)\to \mathrm{Finset}\left(Sym2\left(\mathrm{Fin}\left(n\right)\right)\right)),(Function.Injective\left(a\right))\Rightarrow ((Function.Injective\left(b\right))\Rightarrow ((Finset.image\left(a,(Finset.univ:\mathrm{Finset}\left(\mathrm{Fin}\left(t\right)\right))\right)=Finset.powersetCard\left(r,SimpleGraph.edgeFinset\left(G\right)\right))\Rightarrow ((Finset.image\left(b,(Finset.univ:\mathrm{Finset}\left(\mathrm{Fin}\left(t\right)\right))\right)=Finset.powersetCard\left(r,SimpleGraph.edgeFinset\left(Gprime\right)\right))\Rightarrow ((\forall (i:\mathrm{Fin}\left(t\right)),endpointGraph\left(a\left(i\right)\right){\equiv }_{g}endpointGraph\left(b\left(i\right)\right))\Rightarrow ((Finset.card\left(SimpleGraph.edgeFinset\left(H\right)\right)=r)\Rightarrow (N_H\left(G,H\right)=N_H\left(Gprime,H\right)))))))$$

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

Source. Repository-derived.

Commentary.

Two injective exhaustive enumerations paired by endpoint-graph isomorphisms give equal counts for every r-edge model H.

Definition 1.14 (Radix digit).

$$\forall (b:\mathbb{N}),\forall (p:\mathbb{N}),\forall (i:\mathbb{N}),digit\left(b,p,i\right)=Nat.mod\left(Nat.div\left(p,b^i\right),b\right)$$

Formalization. D5/S3/Combinatorics/Graph/SupportForestMoments/SupportAndEdgeWordReflection.digit (✓ std3).

Source. Repository-derived.

Commentary.

Nat.div is integer quotient and Nat.mod is the remainder, including Lean’s total conventions at base zero.

Definition 1.15 (Packing radix digits).

$$\forall (b:\mathbb{N}),\forall (n:\mathbb{N}),\forall (f:\mathbb{N}\to \mathbb{N}),pack\left(b,n,f\right)=Nat.ofDigits\left(b,List.map\left(f,List.range\left(n\right)\right)\right)$$

Formalization. D5/S3/Combinatorics/Graph/SupportForestMoments/SupportAndEdgeWordReflection.pack (✓ std3).

Source. Repository-derived.

Commentary.

Nat.ofDigits reads the finite digit list in little-endian order.

Theorem 1.16 (Decoding a bounded digit).

$$\forall (b:\mathbb{N}),\forall (n:\mathbb{N}),(0<b)\Rightarrow (\forall (f:\mathbb{N}\to \mathbb{N}),(\forall (j:\mathbb{N}),(j<n)\Rightarrow (f\left(j\right)<b))\Rightarrow (\forall (i:\mathbb{N}),(i<n)\Rightarrow (digit\left(b,pack\left(b,n,f\right),i\right)=f\left(i\right))))$$

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

Source. Repository-derived.

Commentary.

For positive base and digits below the base, integer quotient and remainder recover each digit at an index below the packed length.

Definition 1.17 (Endpoint isomorphism from relabelling).

$$\forall (n:\mathbb{N}),\forall (S:\mathrm{Finset}\left(Sym2\left(\mathrm{Fin}\left(n\right)\right)\right)),\forall (Sprime:\mathrm{Finset}\left(Sym2\left(\mathrm{Fin}\left(n\right)\right)\right)),\forall (q:Equiv.Perm\left(\mathrm{Fin}\left(n\right)\right)),\forall (hq:Finset.image\left(Sym2.map\left(q\right),S\right)=Sprime),(endpointIs{o}_{image}\left(S,Sprime,q,hq\right):endpointGraph\left(S\right){\equiv }_{g}endpointGraph\left(Sprime\right))\wedge (\forall (v:\{x:\mathrm{Fin}\left(n\right)|x\in endpointSet\left(S\right)\}),\mathrm{val}\left(endpointIs{o}_{image}\left(S,Sprime,q,hq\right)\left(v\right)\right)=q\left(\mathrm{val}\left(v\right)\right))$$

Formalization. D5/S3/Combinatorics/Graph/SupportForestMoments/SupportAndEdgeWordReflection.endpointIso_image (✓ std3).

Source. Repository-derived.

Commentary.

The image hypothesis transports endpoint membership. The isomorphism sends each endpoint vertex v to q(v), using q.subtypeEquiv; its adjacency proof is the membership transport for unordered pairs.

Definition 1.18 (Counting a Boolean predicate).

$$\forall (n:\mathbb{N}),\forall (p:\mathbb{N}\to Bool),countNat\left(n,p\right)=List.length\left(List.filter\left(p,List.range\left(n\right)\right)\right)$$

Formalization. D5/S3/Combinatorics/Graph/SupportForestMoments/SupportAndEdgeWordReflection.countNat (✓ std3).

Source. Repository-derived.

Commentary.

Filter the natural numbers below n, then take the list length.

Definition 1.19 (Character on a natural-number action).

$$\forall (n:\mathbb{N}),\forall (p:\mathbb{N}\to \mathbb{N}),natChi\left(n,p\right)=(Nat.choose\left(countNat\left(n,fun(v:\mathbb{N})\mapsto BEq.beq\left(p\left(v\right),v\right)\right),2\right):\mathbb{Z})+(Nat.div\left(countNat\left(n,fun(v:\mathbb{N})\mapsto Bool.and\left(\mathrm{bne}\left(p\left(v\right),v\right),BEq.beq\left(p\left(p\left(v\right)\right),v\right)\right)\right),2\right):\mathbb{Z})-(countNat\left(n,fun(v:\mathbb{N})\mapsto BEq.beq\left(p\left(v\right),v\right)\right):\mathbb{Z})$$

Formalization. D5/S3/Combinatorics/Graph/SupportForestMoments/SupportAndEdgeWordReflection.natChi (✓ std3).

Source. Repository-derived.

Commentary.

The displayed expression is the literal body of natChi. The two local counts test fixed points and nonfixed points fixed by the square. Dividing the latter by two uses Nat.div; both counts and the quotient are cast to integers.

Definition 1.20 (Word action on natural numbers).

$$(\forall (x:\mathbb{N}),natProd\left([],x\right)=x)\wedge (\forall (u:\mathbb{N}),\forall (v:\mathbb{N}),\forall (w:\mathrm{List}\left(\mathbb{N}\times \mathbb{N}\right)),\forall (x:\mathbb{N}),natProd\left(List.cons\left((u,v),w\right),x\right)=Equiv.swapCore\left(u,v,natProd\left(w,x\right)\right))$$

Formalization. D5/S3/Combinatorics/Graph/SupportForestMoments/SupportAndEdgeWordReflection.natProd (✓ std3).

Source. Repository-derived.

Commentary.

The list head acts after the tail, matching multiplication of permutations.

Definition 1.21 (Recursive edge-word evaluator).

$$\forall (n:\mathbb{N}),\forall (edges:\mathrm{List}\left(\mathbb{N}\times \mathbb{N}\right)),\forall (w:\mathrm{List}\left(\mathbb{N}\times \mathbb{N}\right)),(evalMoment\left(n,edges,0,w\right)=natChi\left(n,natProd\left(w\right)\right))\wedge (\forall (r:\mathbb{N}),evalMoment\left(n,edges,r+1,w\right)=List.sum\left(List.map\left(fun(e:\mathbb{N}\times \mathbb{N})\mapsto evalMoment\left(n,edges,r,List.append\left(w,[e]\right)\right),edges\right)\right))$$

Formalization. D5/S3/Combinatorics/Graph/SupportForestMoments/SupportAndEdgeWordReflection.evalMoment (✓ std3).

Source. Repository-derived.

Commentary.

At depth zero evaluate the accumulated word. At positive depth append each edge once and sum the recursive values. Repeated edges and all edge orders are included.

Theorem 1.22 (Sum over a function by its first value).

$$\forall (m:\mathbb{N}),\forall (alpha:Type),\forall (beta:Type),[\mathrm{Fintype}\left(alpha\right)],[\mathrm{AddCommMonoid}\left(beta\right)],\forall (f:(\mathrm{Fin}\left(m+1\right)\to alpha)\to beta),(\sum _{w:\mathrm{Fin}\left(m+1\right)\to alpha}(f\left(w\right)))=(\sum _{a:alpha}((\sum _{w:\mathrm{Fin}\left(m\right)\to alpha}(f\left(Fin.cons\left(a,w\right)\right)))))$$

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

Source. Repository-derived.

Commentary.

The equivalence Fin.consEquiv decomposes a function on Fin(m + 1) into its first value and its restriction to the remaining m coordinates. Summation over this product gives the two nested sums.

Theorem 1.23 (Soundness of the evaluator).

$$\forall (n:\mathbb{N}),\forall (m:\mathbb{N}),\forall (e:\mathrm{Fin}\left(m\right)\to \mathrm{Fin}\left(n\right)\times \mathrm{Fin}\left(n\right)),\forall (r:\mathbb{N}),\forall (w:\mathrm{List}\left(\mathrm{Fin}\left(n\right)\times \mathrm{Fin}\left(n\right)\right)),evalMoment\left(n,List.map\left(fun(i:\mathrm{Fin}\left(m\right))\mapsto (\mathrm{val}\left(Prod.fst\left(e\left(i\right)\right)\right),\mathrm{val}\left(Prod.snd\left(e\left(i\right)\right)\right)),List.finRange\left(m\right)\right),r,List.map\left(fun(a:\mathrm{Fin}\left(n\right)\times \mathrm{Fin}\left(n\right))\mapsto (\mathrm{val}\left(Prod.fst\left(a\right)\right),\mathrm{val}\left(Prod.snd\left(a\right)\right)),w\right)\right)=(\sum _{v:\mathrm{Fin}\left(r\right)\to \mathrm{Fin}\left(m\right)}(chi\left(List.prod\left(List.map\left(fun(a:\mathrm{Fin}\left(n\right)\times \mathrm{Fin}\left(n\right))\mapsto Equiv.swap\left(Prod.fst\left(a\right),Prod.snd\left(a\right)\right),w\right)\right)\cdot List.prod\left(List.ofFn\left(fun(i:\mathrm{Fin}\left(r\right))\mapsto Equiv.swap\left(Prod.fst\left(e\left(v\left(i\right)\right)\right),Prod.snd\left(e\left(v\left(i\right)\right)\right)\right)\right)\right)\right)))$$

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

Source. Repository-derived.

Commentary.

Induction on the remaining word length identifies the recursive sum with the sum over functions Fin r → Fin m. Natural-number actions agree with the corresponding permutations on Fin n, including repeated or equal endpoints.

Theorem 1.24 (Two-prefix decomposition).

$$\forall (n:\mathbb{N}),\forall (m:\mathbb{N}),\forall (e:\mathrm{Fin}\left(m\right)\to \mathbb{N}\times \mathbb{N}),\forall (r:\mathbb{N}),\forall (w:\mathrm{List}\left(\mathbb{N}\times \mathbb{N}\right)),evalMoment\left(n,List.map\left(e,List.finRange\left(m\right)\right),r+2,w\right)=(\sum _{i:\mathrm{Fin}\left(m\right)}((\sum _{j:\mathrm{Fin}\left(m\right)}(evalMoment\left(n,List.map\left(e,List.finRange\left(m\right)\right),r,List.append\left(w,[e\left(i\right),e\left(j\right)]\right)\right)))))$$

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

Source. Repository-derived.

Commentary.

Two applications of the evaluator recursion expose the first two edge choices as finite sums, leaving the remaining r choices recursive.

Definition 1.25 (Moment indexed by an edge enumeration).

$$\forall (n:\mathbb{N}),\forall (m:\mathbb{N}),\forall (e:\mathrm{Fin}\left(m\right)\to Sym2\left(\mathrm{Fin}\left(n\right)\right)),\forall (r:\mathbb{N}),wordMoment\left(e,r\right)=(\sum _{w:\mathrm{Fin}\left(r\right)\to \mathrm{Fin}\left(m\right)}(chi\left(List.prod\left(List.ofFn\left(fun(i:\mathrm{Fin}\left(r\right))\mapsto edgeSwap\left(e\left(w\left(i\right)\right)\right)\right)\right)\right)))$$

Formalization. D5/S3/Combinatorics/Graph/SupportForestMoments/SupportAndEdgeWordReflection.wordMoment (✓ std3).

Source. Repository-derived.

Commentary.

The index function chooses unordered edges; the list of their transpositions has length r and is multiplied in increasing index order.

Theorem 1.26 (Reindexing graph edge words).

$$\forall (n:\mathbb{N}),\forall (m:\mathbb{N}),\forall (G:\mathrm{SimpleGraph}\left(\mathrm{Fin}\left(n\right)\right)),\forall (e:\mathrm{Fin}\left(m\right)\to Sym2\left(\mathrm{Fin}\left(n\right)\right)),(Finset.image\left(e,(Finset.univ:\mathrm{Finset}\left(\mathrm{Fin}\left(m\right)\right))\right)=SimpleGraph.edgeFinset\left(G\right))\Rightarrow ((Function.Injective\left(e\right))\Rightarrow (\forall (r:\mathbb{N}),M_{r2}\left(G,r\right)=wordMoment\left(e,r\right)))$$

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

Source. Repository-derived.

Commentary.

An injective exhaustive edge enumeration supplies an equivalence with the graph’s edge subtype. The induced equivalence on word functions reindexes the finite sum.

References

• Truth anchor: D5/S3/Combinatorics/Graph/SupportForestMoments/SupportAndEdgeWordReflection.M_r2
• Truth anchor: D5/S3/Combinatorics/Graph/SupportForestMoments/SupportAndEdgeWordReflection.N_H
• Truth anchor: D5/S3/Combinatorics/Graph/SupportForestMoments/SupportAndEdgeWordReflection.N_H_of_enumeration
• Truth anchor: D5/S3/Combinatorics/Graph/SupportForestMoments/SupportAndEdgeWordReflection.c1
• Truth anchor: D5/S3/Combinatorics/Graph/SupportForestMoments/SupportAndEdgeWordReflection.c2
• Truth anchor: D5/S3/Combinatorics/Graph/SupportForestMoments/SupportAndEdgeWordReflection.chi
• Truth anchor: D5/S3/Combinatorics/Graph/SupportForestMoments/SupportAndEdgeWordReflection.countNat
• Truth anchor: D5/S3/Combinatorics/Graph/SupportForestMoments/SupportAndEdgeWordReflection.counts_eq_of_iso_enumerations
• Truth anchor: D5/S3/Combinatorics/Graph/SupportForestMoments/SupportAndEdgeWordReflection.digit
• Truth anchor: D5/S3/Combinatorics/Graph/SupportForestMoments/SupportAndEdgeWordReflection.digit_pack
• Truth anchor: D5/S3/Combinatorics/Graph/SupportForestMoments/SupportAndEdgeWordReflection.edgeSwap
• Truth anchor: D5/S3/Combinatorics/Graph/SupportForestMoments/SupportAndEdgeWordReflection.endpointGraph
• Truth anchor: D5/S3/Combinatorics/Graph/SupportForestMoments/SupportAndEdgeWordReflection.endpointIso_image
• Truth anchor: D5/S3/Combinatorics/Graph/SupportForestMoments/SupportAndEdgeWordReflection.endpointSet
• Truth anchor: D5/S3/Combinatorics/Graph/SupportForestMoments/SupportAndEdgeWordReflection.evalMoment
• Truth anchor: D5/S3/Combinatorics/Graph/SupportForestMoments/SupportAndEdgeWordReflection.evalMoment_sound
• Truth anchor: D5/S3/Combinatorics/Graph/SupportForestMoments/SupportAndEdgeWordReflection.evalMoment_two_fin
• Truth anchor: D5/S3/Combinatorics/Graph/SupportForestMoments/SupportAndEdgeWordReflection.moment_reindex
• Truth anchor: D5/S3/Combinatorics/Graph/SupportForestMoments/SupportAndEdgeWordReflection.natChi
• Truth anchor: D5/S3/Combinatorics/Graph/SupportForestMoments/SupportAndEdgeWordReflection.natProd
• Truth anchor: D5/S3/Combinatorics/Graph/SupportForestMoments/SupportAndEdgeWordReflection.noIsolated
• Truth anchor: D5/S3/Combinatorics/Graph/SupportForestMoments/SupportAndEdgeWordReflection.pack
• Truth anchor: D5/S3/Combinatorics/Graph/SupportForestMoments/SupportAndEdgeWordReflection.sum_fin_cons
• Truth anchor: D5/S3/Combinatorics/Graph/SupportForestMoments/SupportAndEdgeWordReflection.twoPoints
• Truth anchor: D5/S3/Combinatorics/Graph/SupportForestMoments/SupportAndEdgeWordReflection.twoPoints_card
• Truth anchor: D5/S3/Combinatorics/Graph/SupportForestMoments/SupportAndEdgeWordReflection.wordMoment