The Pattern Seam · a finite game with a proof wall
The Forest That Refuses to Continue
Build a sequence of labelled trees while one rule stalks every move: no earlier tree may embed into a later one. The local test is exact. The small game can be exhausted. The audit then finds something more useful than agreement: the written definition and a printed small value do not match.
An embedding is not an ordinary subtree. Pick distinct target nodes with the same labels. For every pair of source nodes, their lowest common ancestor must map to the lowest common ancestor of their images. Target paths may have unused nodes. The optional root rule asks for one more thing: source root to target root.
label(u) = label(f(u))
f(lca(u,v)) = lca(f(u),f(v)) for every u,v
popular variant only: f(root(S)) = root(T)
Layer 1 · make one legal move
Grow a tree the past cannot enter
Your move number is also your node budget. Select a node, add a child, change its label, then submit. If an earlier tree embeds, the engine returns the exact node map and paints corresponding nodes the same colour.
Three labels. Unordered rooted trees. At move i, at most i nodes. The game stores at most ... accepted trees and the editor caps a tree at ... nodes.
The engine is preparing your first move.
This workbench proves only each comparison it performs. A long session cannot demonstrate eventual loss. General termination belongs to Kruskal's theorem.
Layer 2 · exhaust the convention
Ask the written definition what it says
This solver generates every unordered rooted labelled tree available at each move, canonicalizes child order, computes the complete embedding matrix, and visits every legal history. Change the alphabet or root rule. When the search is complete, open the terminal certificate: every possible next tree is listed beside an earlier tree that blocks it. When a history reaches the cutoff, the page reports only a lower bound.
Run the solver to build the certificate.
A longest legal sequence
Open the no-extension certificate
Each row is one possible tree on the next move. “Blocked by” names an earlier tree, and its map gives source node → target node. Together the rows prove that this displayed sequence cannot continue.
| possible next tree | blocked by | witness map |
|---|
The disagreement is now visible, not verbal. With two labels, one-to-one maps, equal labels, at most i nodes at move i, and no root condition, the live exhaustive answer is .... Requiring root-to-root does not turn that value into the often quoted answer: the search constructs a sequence of length ... before its cutoff. So the root rule alone cannot explain Friedman's printed TREE[2] = 2.
The check: the finite world rebuilt here
Canonical tree census, two labels
Exactly by size: .... Available through each move: ....
Complete relation
... trees give ... ordered embedding tests.
Search ceiling
The raw stage product is ...; illegal prefixes are pruned only after their exact witness is found.
Workbench ceiling
At the fixed editor caps, one submitted comparison has at most ... node-pair states; a matching side has at most ... branches.
Four exhaustive answers
...
Independent audit
The repository verifier uses parent-array enumeration and brute-force injections, executes this shipped engine in a VM, and mutation-tests the coupling.
Every free choice, truncation, and uncertainty
- Tree model: finite, unordered, rooted, non-plane trees. Labels are discrete colours and must be equal, not merely comparable.
- Embedding: injective and label-preserving, with every binary lowest common ancestor preserved. Edges may stretch through paths. “Root free” means no extra root-to-root condition. “Root fixed” adds that condition.
- Size indexing: move i admits any tree with at most i vertices. It does not mean exactly i.
- Depth truncation: the exhaustive solver generates only through ... vertices and only one or two labels. The root-free two-label search is terminal before the truncation. The root-fixed search reaches it and is explicitly reported as a lower bound. Nothing here computes the three-label value.
- Workbench truncation: at most ... nodes per edited tree and ... accepted trees. These are interface limits, not TREE bounds.
- Canonicalization: siblings are sorted by recursive signature. Their screen order carries no mathematics.
- Timing: elapsed milliseconds depend on the device and are never used as evidence.
- Uncertainty: Friedman's opened post prints TREE[2] = 2 but does not define “inf preserving embedding” inside that post. A separate ... Friedman manuscript defines such an embedding as one-to-one and infimum-preserving. Under those written conditions, this exhaustive audit gets a different answer. We do not silently guess an omitted convention.
- Proof theory: this finite audit does not independently formalize the systems in the proof-theory sources. Claims about Kruskal, ATR₀, ACA₀ + Π¹₂-BI, proof length, and Graham's number remain cited claims, not outputs of this browser computation.
Layer 3 · the open edge
Finite, computable, and nowhere near computed
Kruskal's general termination theorem is closed: Kruskal proved the well-quasi-order result for finite labelled trees in .... This page does not reprove it.
The exact third value is not supplied: we could not find a published exact value for Friedman's TREE[3], or a usable decimal interval for it, as of .... The opened Friedman post from ... gives a non-decimal lower comparison to proof-bounded Turing-machine halting times. That is not an estimate you can expand.
The live dispute is a source audit: Friedman's opened post prints TREE[2] = 2. Under the one-to-one infimum-preserving definition found in his separate manuscript, the root-free solver gets ..., with a complete no-extension certificate. The root-fixed solver reaches ... at the cutoff. We could not reconcile the printed 2 with these written conditions as of ....
The proof wall, stated without the folklore
Friedman's opened ... FOM post defines TREE[k] using the phrases infimum-preserving and label-preserving, with at most i vertices at move i. It prints TREE[1] = 1 and TREE[2] = 2. It also states the uniform finite assertion “for all k, TREE[k] exists,” and says the TREE function eventually dominates every function provably recursive in ACA₀ + Π¹₂-BI. It separately gives a proof-length lower bound for the fixed TREE[3]. Those are different claims, and the printed small value needs more convention than that post supplies.
Simpson's exposition reports Friedman's nonprovability result for the general tree theorem in ATR₀. It does not license the slogan “ATR₀ cannot prove this fixed numeral exists.” Likewise, TREE is computable in principle once finiteness is known. It is not Busy Beaver.
Whose theorem that is, precisely, because the credit is routinely collapsed onto the expositor. The nonprovability result is Friedman's, and it was obtained independently by Diana Schmidt in her 1979 Heidelberg habilitation. Simpson's 1985 chapter is the published exposition of Friedman's then-unpublished work, so the correct citation form is “cf. Simpson 1985”, not “Simpson proved”. The exact proof-theoretic strength was pinned later still, by Rathjen and Weiermann in 1993, at the small Veblen ordinal. This page did not reproduce any of those proofs and does not claim to: they are cited, while the census, the embeddings and the small exact answers below are computed here.
For the fixed-number comparison, cite the fixed-number source: Friedman's follow-up records n(3) < Graham's number < n(4) < TREE[3] for his convention. An asymptotic slogan alone would not prove that inequality.
Source status: the Friedman archive pages were opened. The Kruskal paper's indexed first page and the Simpson bibliographic abstract were inspected, while their publisher PDFs returned access errors. The full distinction is recorded in the research README.