An Explicit Membership Graph Outside G₂

Abstract

Cuts in arbitrary words reconstruct their two-letter projections. The explicit membership graph on 24 points and all their subsets has no two-uniform representation.

This construction addresses the unnumbered explicit-graph request in the source conclusion. It does not address Conjecture 31, minimum size or connectedness. The literature note attests the question and definitions, not a published answer. Novelty is suspected only within the supplied September 15, 2026 search scope; worldwide priority remains ASSUMED-UNVERIFIED.

All words are finite lists. Projection and representation use decidable equality on V; cuts need it only on B, reconstruction needs none, and the reconstruction theorem assumes it on A and B. Sum(A,B) is the tagged disjoint union, with injections inl and inr. Unit has the single element . Empty lists are written []. The left restriction L(w) is filterMap(getLeft?,w), retaining each left letter in its original order. The renaming rho(b) sends inl(a) to inl(a) and inr() to inr(b). Its domain is Sum(A,Unit), and it is injective. Natural pred is truncated subtraction by one. The displayed proj, cuts and Rec abbreviate twoProjection, leftCuts and reconstruct. Finset(Fin(24)) is the full power set of the 24 points.

Definition 1.1 (The actual two-letter projection).

$$\forall V:\mathrm{Type},\forall a:V,\forall b:V,\forall w:\mathrm{List}\left(V\right),\mathrm{proj}\left(a,b,w\right)=\mathrm{filter}\left(z\mapsto (z=a\vee z=b),w\right)$$

Formalization. D5/S1/Words/GraphRepresentation/ExplicitNonTwoUniform.twoProjection (✓ std3).

Citation. Duncan Adamson, Amanita Dietz, Pamela Fleischmann, Annika Huch, and Silas Cato Sacher (2026). 2-word-π-representable Graphs. URL: https://arxiv.org/abs/2605.27183v1.

Commentary.

The filter keeps exactly the letters equal to either specified vertex, preserving order and repetitions. This is the source projection, not an alternation pattern or a union of graph representations.

Definition 1.2 (Two words, each two-uniform).

$$\forall V:\mathrm{Type},\forall G:\mathrm{SimpleGraph}\left(V\right),(InG2\left(G\right))⟺(\exists w,v:\mathrm{List}\left(V\right),(\forall z:V,\mathrm{count}\left(z,w\right)=2)\wedge ((\forall z:V,\mathrm{count}\left(z,v\right)=2)\wedge (\forall x:V,\forall y:V,x\ne y⟹(\mathrm{Adj}\left(G,x,y\right))⟺(\mathrm{proj}\left(x,y,w\right)=\mathrm{proj}\left(x,y,v\right)))))$$

Formalization. D5/S1/Words/GraphRepresentation/ExplicitNonTwoUniform.InG2 (✓ std3).

Citation. Duncan Adamson, Amanita Dietz, Pamela Fleischmann, Annika Huch, and Silas Cato Sacher (2026). 2-word-π-representable Graphs. URL: https://arxiv.org/abs/2605.27183v1.

Commentary.

Both occurrence conditions quantify over every vertex. Since two is positive, both word alphabets equal the vertex type. The edge equivalence is required for every distinct pair; SimpleGraph already excludes loops and is symmetric.

Definition 1.3 (Cuts counted in the original word).

$$\begin{array}{c}\forall A,B:\mathrm{Type},b,c:B,a:A,w:\mathrm{List}\left(\mathrm{Sum}\left(A,B\right)\right)\\ \mathrm{cuts}\left(b,[]\right)=[]\\ \mathrm{cuts}\left(b,(\mathrm{inl}\left(a\right))::w\right)=\mathrm{map}\left(\mathrm{succ},\mathrm{cuts}\left(b,w\right)\right)\\ \mathrm{cuts}\left(b,(\mathrm{inr}\left(b\right))::w\right)=(0)::\mathrm{cuts}\left(b,w\right)\\ c\ne b⟹\mathrm{cuts}\left(b,(\mathrm{inr}\left(c\right))::w\right)=\mathrm{cuts}\left(b,w\right)\end{array}$$

Formalization. D5/S1/Words/GraphRepresentation/ExplicitNonTwoUniform.leftCuts (✓ std3).

Source. Repository-derived.

Acknowledgement. Duncan Adamson, Amanita Dietz, Pamela Fleischmann, Annika Huch, and Silas Cato Sacher (2026). 2-word-π-representable Graphs. URL: https://arxiv.org/abs/2605.27183v1.

Commentary.

Each left letter increments every later cut. An occurrence of b contributes a zero cut before the cuts of the remaining suffix, while other right letters are deleted. Thus the list records, in occurrence order, the number of preceding left letters at every b. Right letters between occurrences are ignored. Consecutive b markers may have the same cut.

Definition 1.4 (Insert markers at absolute cuts).

$$\begin{array}{c}\forall A:\mathrm{Type},a:A,r:\mathrm{List}\left(A\right),n:\mathbb{N},c:\mathrm{List}\left(\mathbb{N}\right)\\ \mathrm{Rec}\left(r,[]\right)=\mathrm{map}\left(\mathrm{inl},r\right)\\ \mathrm{Rec}\left(r,(0)::c\right)=(\mathrm{inr}\left(\ast \right))::\mathrm{Rec}\left(r,c\right)\\ \mathrm{Rec}\left([],(n+1)::c\right)=[]\\ \mathrm{Rec}\left((a)::r,(n+1)::c\right)=(\mathrm{inl}\left(a\right))::\mathrm{Rec}\left(r,(n)::\mathrm{map}\left(\mathrm{pred},c\right)\right)\end{array}$$

Formalization. D5/S1/Words/GraphRepresentation/ExplicitNonTwoUniform.reconstruct (✓ std3).

Source. Repository-derived.

Acknowledgement. Duncan Adamson, Amanita Dietz, Pamela Fleischmann, Annika Huch, and Silas Cato Sacher (2026). 2-word-π-representable Graphs. URL: https://arxiv.org/abs/2605.27183v1.

Commentary.

With no cuts, retain the left list. A zero cut inserts a marker without consuming a left letter, so tied cuts give consecutive markers. A positive cut consumes one left letter and decrements every remaining cut. The branch with an empty left list and a positive first cut returns the empty list; it is unreachable for cuts of actual words. Recursion decreases the sum of the two input lengths.

Theorem 1.5 (Reconstruction for every word).

$$\forall A:\mathrm{Type},\forall B:\mathrm{Type},\forall a:A,\forall b:B,\forall w:\mathrm{List}\left(\mathrm{Sum}\left(A,B\right)\right),\mathrm{proj}\left(\mathrm{inl}\left(a\right),\mathrm{inr}\left(b\right),w\right)=\mathrm{map}\left(\mathrm{rho}\left(b\right),\mathrm{proj}\left(\mathrm{inl}\left(a\right),\mathrm{inr}\left(\ast \right),\mathrm{Rec}\left(L\left(w\right),\mathrm{cuts}\left(b,w\right)\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S1/Words/GraphRepresentation/ExplicitNonTwoUniform.projection_eq_reconstruction (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Duncan Adamson, Amanita Dietz, Pamela Fleischmann, Annika Huch, and Silas Cato Sacher (2026). 2-word-π-representable Graphs. URL: https://arxiv.org/abs/2605.27183v1.

Commentary.

Induct on the original word. A left head shifts all cuts by one; the reconstructor consumes that same head and restores the original cuts. A right head equal to b inserts a zero cut and hence a marker. A different right head changes neither side. Projecting and renaming gives the displayed identity. There is no uniformity, cut-separation or word-order hypothesis.

Definition 1.6 (The literal membership graph).

$$\begin{array}{c}V=\mathrm{Sum}\left(\mathrm{Fin}\left(24\right),\mathrm{Finset}\left(\mathrm{Fin}\left(24\right)\right)\right)\\ U24:\mathrm{SimpleGraph}\left(V\right)\\ \forall a,b:\mathrm{Fin}\left(24\right),S,T:\mathrm{Finset}\left(\mathrm{Fin}\left(24\right)\right)\\ (\mathrm{Adj}\left(U24,\mathrm{inl}\left(a\right),\mathrm{inr}\left(S\right)\right))⟺(a\in S)\\ (\mathrm{Adj}\left(U24,\mathrm{inr}\left(S\right),\mathrm{inl}\left(a\right)\right))⟺(a\in S)\\ (\neg \mathrm{Adj}\left(U24,\mathrm{inl}\left(a\right),\mathrm{inl}\left(b\right)\right))\wedge (\neg \mathrm{Adj}\left(U24,\mathrm{inr}\left(S\right),\mathrm{inr}\left(T\right)\right))\end{array}$$

Formalization. D5/S1/Words/GraphRepresentation/ExplicitNonTwoUniform.U24 (✓ std3).

Source. Repository-derived.

Acknowledgement. Duncan Adamson, Amanita Dietz, Pamela Fleischmann, Annika Huch, and Silas Cato Sacher (2026). 2-word-π-representable Graphs. URL: https://arxiv.org/abs/2605.27183v1.

Commentary.

The carrier is the tagged union V of Fin(24) and all finite subsets of Fin(24). Adjacency is membership across the two tags, in either direction, and false within either part. These equations directly provide symmetry and looplessness. V is finite with 24 + 2^24 = 16,777,240 vertices. The vertex inr(emptyset) is isolated and is permitted by the source definition.

Theorem 1.7 (No pair of two-uniform words represents U₂₄).

$$\neg \exists w,v:\mathrm{List}\left(V\right),(\forall z:V,\mathrm{count}\left(z,w\right)=2)\wedge ((\forall z:V,\mathrm{count}\left(z,v\right)=2)\wedge (\forall x:V,\forall y:V,x\ne y⟹(\mathrm{Adj}\left(U24,x,y\right))⟺(\mathrm{proj}\left(x,y,w\right)=\mathrm{proj}\left(x,y,v\right))))$$

Proof. Machine-checked in Lean as D5/S1/Words/GraphRepresentation/ExplicitNonTwoUniform.u24_not_in_g2 (✓ std3). ∎

Resolves. Problems/adamson-explicit-graph-outside-g2 (proved) by D5/S1/Words/GraphRepresentation/ExplicitNonTwoUniform.u24_not_in_g2.

Source. Repository-derived.

Acknowledgement. Duncan Adamson, Amanita Dietz, Pamela Fleischmann, Annika Huch, and Silas Cato Sacher (2026). 2-word-π-representable Graphs. URL: https://arxiv.org/abs/2605.27183v1.

Commentary.

Assume the displayed representation. Each left restriction has length 48, because each of the 24 left letters occurs twice. Each subset occurs twice, so its cut list has length two, and every cut is between zero and 48. Choose these two cuts in each word to obtain a signature in (Fin(49) × Fin(49))². The domain has 2^24 = 16,777,216 elements, whereas the signature space has 49^4 = 5,764,801. The existing pigeonhole theorem therefore gives distinct subsets S,T with equal signatures. Apply reconstruction separately to w and v for each left letter a. Injectivity of rho(S) and rho(T) shows that equality of the two a/S projections is equivalent to equality of the two a/T projections. Hence a belongs to S exactly when it belongs to T. Finite-set extensionality gives S=T, contradicting distinctness. The two left restrictions may have different orders throughout this proof.

The pigeonhole step directly reuses D5/S0/Diagonal/PigeonholeFiber.finite_reading_has_fiber. Count identities, finite cardinalities, marker injectivity and membership extensionality are local steps, not separate new theorems. The live new content in both theorem proofs is reconstruction from cuts. The argument is structural for arbitrary words; the concluding finite arithmetic does not enumerate words or graphs.

References

• Truth anchor: D5/S0/Diagonal/PigeonholeFiber.finite_reading_has_fiber
• Truth anchor: D5/S1/Words/GraphRepresentation/ExplicitNonTwoUniform.InG2
• Truth anchor: D5/S1/Words/GraphRepresentation/ExplicitNonTwoUniform.U24
• Truth anchor: D5/S1/Words/GraphRepresentation/ExplicitNonTwoUniform.leftCuts
• Truth anchor: D5/S1/Words/GraphRepresentation/ExplicitNonTwoUniform.projection_eq_reconstruction
• Truth anchor: D5/S1/Words/GraphRepresentation/ExplicitNonTwoUniform.reconstruct
• Truth anchor: D5/S1/Words/GraphRepresentation/ExplicitNonTwoUniform.twoProjection
• Truth anchor: D5/S1/Words/GraphRepresentation/ExplicitNonTwoUniform.u24_not_in_g2
• Dependency: D5/S0/Diagonal/PigeonholeFiber