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.
injective f: V(S) → V(T)
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.
Bad-sequence workbenchmove loading
Selected node label
Edit the current move
Commit
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.
Exhaustive finite solverready
Alphabet
Root convention
...
longest legal sequence
...
trees through final stage
...
legal history nodes visited
...
candidate extensions tested
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 Friedman's printed 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. The connection between finite trees and ordinal notations behind his method was noticed independently by Diana Schmidt in her 1979 Heidelberg habilitation, which computed maximal order types; Simpson notes that she drew no nonprovability result from it, though Freund (2020) names both for the theorem. 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.
The claims record60 claims re-read against their sources, 18 October 2026
Written 2026-08-01. Claims re-read against their sources on 2026-10-18: 60 checked, 42 confirmed, 7 wrong, 1 unverifiable, 10 first-hand observations checked against their record. By the assay line (research/assay-line/claude-1018b/), Claude fixer (claude-opus-5-5) directed by claude-assaying-boyle-1014; source record by a Claude agent (claude-sonnet-5-5), checked by a Claude agent (claude-opus-5-5).
This pass was the Assay Office's assay line, batch claude-1018b, re-reading the published layer against its sources, source first: one Claude agent (claude-sonnet-5-5) built the source record (research/assay-line/claude-1018b/tree-three/N1-sources.json), a second (claude-opus-5-5) checked every entry against the opened sources (FOM 273 and 290, Friedman's 2000 OSU manuscript, Kruskal 1960, Simpson's Arch. math. Logik 25 (1985) paper, Freund arXiv:2003.02714, Rathjen and Weiermann 1993, Crossref, Wikipedia, the SEP proof-theory supplement E) and ran the verifier (277/277, mutations 12/12), and a third, the fixer, re-read the evidence for every WRONG item before deciding and fixing (decisions in research/assay-line/claude-1018b/tree-three/triage.json). Two statements were false and are corrected on the page with dated lines: the claim that Diana Schmidt obtained the nonprovability result independently (Simpson says she obtained none; what she noticed independently was the trees-to-ordinals connection), and "the often quoted answer" for Friedman's printed TREE[2] = 2 (Wikipedia gives TREE(2) = 3, this page's root-free result). The JSON-LD dateModified was moved to 2026-10-18. Three MINOR overstatements were listed and left. MINOR lines are counted in `wrong`.
Claims
CONFIRMED At move (i), the tree may have at most (i) vertices. https://fomarchive.ugent.be/2006-March/010279.html : fom-at-most-i: post 273 reads "where each T_i has at most i vertices"; also in the PROPOSITION.
CONFIRMED That result does not reproduce the value two printed in Harvey Friedman's opened 2006 post. https://fomarchive.ugent.be/2006-March/010279.html : fom-printed-two: "Note that TREE[1] = 1 and TREE[2] = 2."; header "Tue Mar 28 12:57:25 EST 2006".
MINOR Friedman's opened 2006 FOM post defines TREE[k] using the phrases infimum-preserving and label-preserving, with at most i vertices at move i. https://fomarchive.ugent.be/2006-March/010279.html : fom-phrases: the post's phrase is "inf preserving and label preserving embeddable" (twice); the word "infimum" occurs 0 times in the post, so "the phrases infimum-preserving" names a phrase the post does not use. Same wording in research/tree-three/README.md. Fix at public/strata/tree-three/index.html:316: "using the phrases inf preserving and label preserving".
CONFIRMED but the short 2006 post does not restate the definition, so the unresolved point is exactly named. https://fomarchive.ugent.be/2006-March/010279.html : fom-no-definition: read in full; "inf preserving" appears 2 times (the record says 3) and is never defined; no "defin" string in the post.
CONFIRMED It also states the uniform finite assertion "for all k, TREE[k] exists," https://fomarchive.ugent.be/2006-March/010279.html : fom-uniform: verbatim "One of our many finite forms of Kruskal's theorem asserts that for all k, TREE[k] exists."
CONFIRMED says the TREE function eventually dominates every function provably recursive in ACA₀ + Π¹₂-BI https://fomarchive.ugent.be/2006-March/010279.html : fom-dominates: "This function eventually dominates every provably recursive function of the system ACA_0 + Pi12-BI."
CONFIRMED It separately gives a proof-length lower bound for the fixed TREE[3]. https://fomarchive.ugent.be/2006-March/010279.html : fom-proof-length: the closer support is THEOREM # on the three-label PROPOSITION: "any such proof in ACA_0 + Pi12-BI must use at least 2^[1000] symbols"; the record's excerpt (THEOREM ##) is the halting-time comparison.
CONFIRMED gives a non-decimal lower comparison to proof-bounded Turing-machine halting times. https://fomarchive.ugent.be/2006-March/010279.html : fom-halting-comparison: "TREE[3] is greater than the halting time of any Turing machine initialized with a blank tape, which can be proved to halt in ACA_0 + Pi12-BI by a proof with at most 2^[1000] symbols."
CONFIRMED but does not define "inf preserving embedding" inside that post. https://fomarchive.ugent.be/2006-March/010279.html : fom-quoted-term: true, no definition in the post. The quoted term is the manuscript's exact phrase ("An inf preserving embedding from T1 into T2"), used as the concept's name; the post itself says "inf preserving and label preserving embeddable". The tool's offline flag is this naming, not a misquote of the post.
CONFIRMED Friedman's follow-up records n(3) < Graham's number < n(4) < TREE[3] for his convention. https://fomarchive.ugent.be/2006-March/010290.html : fom-graham: subject "[FOM] n(3) < Graham's number < n(4) < TREE[3]", Wed Mar 29 2006; body "So n(4) >> Graham's number." and "n(4) is too puny to even think about mentioning against TREE[3]". Note the page does not link this post.
CONFIRMED TREE is not Busy Beaver https://en.wikipedia.org/wiki/Busy_beaver : bb-uncomputable: "He proved that both of these functions were noncomputable, because they each grew faster than any computable function."
CONFIRMED Likewise, TREE is computable in principle once finiteness is known. https://en.wikipedia.org/w/index.php?title=Kruskal%27s_tree_theorem&action=raw : tree-finite: the source gives finiteness only; computability follows by exhaustive search over the finitely branching tree of bad sequences, which is finite by Kruskal and Konig. Correct mathematics, no quoted source.
CONFIRMED Simpson's 1985 chapter is the published exposition of Friedman's then-unpublished work https://sgslogic.net/t20/papers/nichtbeweisbarkeit-aml-1985.pdf : simpson-exposes: abstract "In this paper we exposit some as yet unpublished results of Harvey Friedman." This is Simpson's German companion paper (Arch. math. Logik 25 (1985) 45-65), not the chapter; Rathjen and Weiermann say the same of the chapter ("presents proof-theoretic results, due to H. Friedman").
CONFIRMED Simpson's exposition reports Friedman's nonprovability result for the general tree theorem in ATR₀. https://web.archive.org/web/2020/https://core.ac.uk/download/pdf/82187099.pdf : simpson-atr0: opened; Introduction: "It is shown there that Kruskal's theorem is not provable in ATR0." Simpson AML Satz 2.8: "(Friedman [8]). Kruskals Satz WQO(T) ist in ATR0 nicht beweisbar."
CONFIRMED Simpson's exposition reports Friedman's nonprovability result for the general tree theorem in ATR₀. https://arxiv.org/pdf/2003.02714 : simpson-atr0-freund: opened; "a classical result of D. Schmidt [18] and H. Friedman [19] shows that Kruskal's theorem cannot be proved in ATR0"; [19] is Simpson's chapter.
WRONG The nonprovability result is Friedman's, and it was obtained independently by Diana Schmidt in her 1979 Heidelberg habilitation. https://sgslogic.net/t20/papers/nichtbeweisbarkeit-aml-1985.pdf : schmidt-independent-simpson: the record's own excerpt contradicts the claim. Simpson, Einleitung p. 48 (OCR normalized): "Die Existenz einer solchen Verbindung wurde schon frueher, z.B. von Schmidt [27], bemerkt. Aber Schmidt bekam keine Nichtbeweisbarkeitsergebnisse." and Bemerkung 2.9, after Satz 2.8 (Kruskal not provable in ATR0): "Fuer eine genauere Berechnung gewisser dem Kruskalsatz zugeordneter Ordinalzahlen siehe auch Schmidt [27]. Die Arbeit [27] enthaelt aber keine Folgerungen wie z.B. Satz 2.8." The SEP supplement uses "independently" for the trees-to-ordinals connection, not the result: "The connection between finite trees and ordinal representations for ordinals <Γ0 was noticed by Friedman (cf. Simpson 1985) and independently by Diana Schmidt (1979)." (https://plato.stanford.edu/archives/spr2021/entries/proof-theory/appendix-e.html). Freund credits "D. Schmidt [18] and H. Friedman [19]" without "independently". Fix at public/strata/tree-three/index.html:318, e.g. "The nonprovability result is Friedman's; the connection between trees and ordinal notations behind it was noticed independently by Diana Schmidt in her 1979 Heidelberg habilitation, which computed the maximal order types (Simpson notes she drew no nonprovability conclusion; later authors credit both)." Same claim in research/tree-three/README.md (attribution section). Re-read by the fixer (pdftotext of the same PDF), confirmed; fixed.
MINOR The nonprovability result is Friedman's, and it was obtained independently by Diana Schmidt in her 1979 Heidelberg habilitation. https://arxiv.org/pdf/2003.02714 : schmidt-joint-freund: Freund names both for the result ("a classical result of D. Schmidt [18] and H. Friedman [19]") and nowhere says "independently"; it does not support the page's wording and cannot outweigh Simpson's explicit statement. Answered under schmidt-independent-simpson. Fixed with schmidt-independent-simpson (same sentence).
CONFIRMED in her 1979 Heidelberg habilitation. https://arxiv.org/pdf/2003.02714 : schmidt-1979: ref [18] "Diana Schmidt, Well-partial orderings and their maximal order types, Habilitationsschrift, Universitaet Heidelberg, 1979."; Simpson ref [27] "Habilitationsschrift, Heidelberg, 1979, 77 Seiten".
CONFIRMED The exact proof-theoretic strength was pinned later still, by Rathjen and Weiermann in 1993, at the small Veblen ordinal. https://web.archive.org/web/2020/https://core.ac.uk/download/pdf/82187099.pdf : rw-1993: opened; APAL 60 (1993) 49-88, abstract "we calibrate the exact proof-theoretic strength of Kruskal's theorem"; the paper calls the ordinal (theta Omega^omega 0) the "Ackermann ordinal", which is today's small Veblen ordinal (see svo-wiki). Freund: "The precise logical strength of Kruskal's theorem has been determined by M. Rathjen and A. Weiermann [17]."
CONFIRMED at the small Veblen ordinal. https://en.wikipedia.org/wiki/Kruskal%27s_tree_theorem : svo-wiki: "the proof-theoretic ordinal of the theorem equaling the small Veblen ordinal (sometimes confused with the smaller Ackermann ordinal)", citing Rathjen and Weiermann 1993.
CONFIRMED Goodstein sequences expose what Peano arithmetic cannot prove uniformly https://en.wikipedia.org/wiki/Goodstein%27s_theorem : goodstein: "Laurence Kirby and Jeff Paris showed in 1982 that Goodstein's theorem is unprovable in Peano arithmetic".
CONFIRMED Busy Beaver is uncomputable, while TREE is computable in principle once Kruskal gives finiteness https://en.wikipedia.org/wiki/Busy_beaver : bb-uncomputable2: as bb-uncomputable and tree-finite.
CONFIRMED we could not find a published exact value for Friedman's TREE[3], or a usable decimal interval for it, as of 2026-08-01 https://en.wikipedia.org/w/index.php?title=Kruskal%27s_tree_theorem&action=raw : no-tree3-value: a dated absence statement; the wikitext gives only "an extremely weak lower bound for TREE(3)", and the README limits the claim to "we could not find". Positive control: the same wikitext does yield TREE(1) and TREE(2) values.
CONFIRMED It does not license the slogan "ATR₀ cannot prove this fixed numeral exists." public/strata/tree-three/index.html : slogan: a slogan the page disowns, attributed to nobody; nothing to misquote.
CONFIRMED so the correct citation form is "cf. Simpson 1985", not "Simpson proved". https://plato.stanford.edu/archives/spr2021/entries/proof-theory/appendix-e.html : cf-simpson: a recommendation, not a quotation; the SEP supplement uses exactly this form: "Kruskal's Theorem is not provable in ATR0 (cf. Simpson 1985)."
CONFIRMED "A toy can reject one move. It does not prove a small exact case, and it cannot tell whether a source disagreement is really caused by the root convention." public/strata/tree-three/index.html : toy-dismissal: presented under "The sophisticated dismissal" as an anticipated objection, attributed to nobody.
CONFIRMED "name":"Well-Quasi-Ordering, the Tree Theorem, and Vazsonyi's Conjecture","author":"J. B. Kruskal","isPartOf":"Transactions of the American Mathematical Society 95(2)" https://api.crossref.org/works/10.1090/S0002-9947-1960-0111704-1 : cite-kruskal: Crossref title "Well-quasi-ordering, the Tree Theorem, and Vazsonyi's conjecture", J. B. Kruskal, vol 95, issue 2, pp. 210-225, issued 1960. The tool's "DOI MISMATCH (does not give the year 1960)" is an artefact: the JSON-LD gives no year to mismatch.
CONFIRMED "name":"Nonprovability of Certain Combinatorial Properties of Finite Trees","author":"Stephen G. Simpson","isPartOf":"Studies in Logic and the Foundations of Mathematics 117" https://api.crossref.org/works/10.1016/S0049-237X(09)70156-9 : cite-simpson: Crossref title matches, book chapter, 1985, pp. 87-117, container "Studies in Logic and the Foundations of Mathematics" / "Harvey Friedman's Research on the Foundations of Mathematics", no author or volume; author and vol. 117 from Freund ref [19], and FOM 273 cites the same book as "volume 117". The tool's year mismatch is the same artefact.
OBSERVED Source status: the Friedman archive pages were opened. research/tree-three/README.md : src-status: README "Opened in full" lists FOM 273 and 290; both return 200 today and read as the page says.
OBSERVED The Kruskal paper's indexed first page and the Simpson bibliographic abstract were inspected, while their publisher PDFs returned access errors. research/tree-three/README.md : src-access: README items 4 and 5 record "The AMS PDF request returned an access error" and "The ScienceDirect full text request returned an access error". (Archive.org copies of the Kruskal PDF open today; that does not contradict the author's observation.)
CONFIRMED The page names which source pages were opened, which publisher materials were accessible only through indexed metadata, and which claims remain citations rather than live computations. public/strata/tree-three/index.html : src-names: lines 300-302 ("Proof theory: ... remain cited claims") and 320 (source status). The README also says the manuscript was read only through indexed text; the page does not say so, a small gap.
OBSERVED Corrected 2026-09-28 (found by a scan of the site's pages for verdicts printed whatever the page computed) git show b08bee9d4c3:public/strata/tree-three/index.html : corrected-0928: commit b08bee9d4c3 (2026-09-28 19:09Z, "typed verdicts: nine pages (group 3)") adds the line and the bound() logic.
OBSERVED one label: 1 either way, complete; two labels: 3 complete root free, 4 at the cutoff root fixed recreated: node research/tree-three/verify-tree-three.mjs : four-answers: PASS 025-032 print 1/true, 1/true, 3/true, 4/false; 277/277, exit 0.
OBSERVED Measured, not assumed: with every file this layer ships emptied, it goes red. research/verifier-independence/verdicts.json : measured-emptied: row tree-three "dependence": "red", "depRed": 1.
OBSERVED Measured too: a defect placed in this page's running code turned it red. research/verifier-independence/verdicts.json : measured-defect: "code": 2, "codeRed": 1 (prose 2, proseRed 0).
CONFIRMED Last verified 1 August 2026, when it was written. git show 9ddc1e9045:scripts/check-placard.mjs : verified-date: lines 255-257 print "when it was written" with the layer date when no re-read record exists; frontmatter date 2026-08-01.
CONFIRMED This layer's check lifts this page's own source out of the HTML and runs it. research/tree-three/README.md : check-lifts: "extracts the engine between TREE_THREE_ENGINE_START and TREE_THREE_ENGINE_END, executes that exact shipped code in a Node VM"; verifier section "page exact census" passes.
CONFIRMED A move is a finite unordered rooted tree whose nodes carry discrete labels. research/tree-three/README.md : d-discrete: "Labels form a discrete alphabet."; engine uses parent and label arrays.
MINOR The browser checks this condition from the definition: labels agree, the node map is injective, and every lowest common ancestor is preserved. public/strata/tree-three/index.html : d-embed-def: the engine (embedding(), lines 480-545) does not test the definition; it tests an equivalent recursive criterion (labels agree, source children matched by bipartite matching to distinct child branches of the target). Only the verifier enumerates injective maps and checks every LCA, and only through four vertices; the workbench allows 12. The comparisons are right, the description overstates the method. Fix at src/content/strata/tree-three.md:20, e.g. "checks an equivalent recursive form of this condition, which the verifier compares with the definition itself by brute force through four vertices".
CONFIRMED When a move fails, the page shows the earlier tree and the complete witnessing node map. public/strata/tree-three/index.html : d-witness: reconstruct() builds the map; lines 692-694 paint both trees and print "map: i->j" for every source node.
CONFIRMED It generates every canonical unordered rooted tree with one or two labels through four vertices, precomputes the full embedding relation, and exhausts every legal history. public/strata/tree-three/index.html : d-gen: solverMaxStage: 4, generateForms, the full matrix at lines 556-558 and dfs over histories; verifier census [2,4,14,52] (PASS 064).
CONFIRMED The reader can switch one condition: whether the source root may land anywhere or must land at the target root. public/strata/tree-three/index.html : d-switch: "root may land anywhere" / "root must map to root" buttons; starts = rootPreserving ? [0] : all nodes (line 536).
OBSERVED Under the explicit one-to-one, label-equality, lowest-common-ancestor rules, the root-free two-label answer is three, with a complete terminal certificate. recreated: node research/tree-three/verify-tree-three.mjs : d-free3: PASS 029-030 (3, complete), PASS 043 "root-free terminal certificate row count: 72" (= 2+4+14+52), PASS 044 every candidate has a blocker.
OBSERVED The root-fixed search reaches a legal fourth move and is therefore reported only as a lower bound at the cutoff. recreated: node research/tree-three/verify-tree-three.mjs : d-fixed4: PASS 031-032 (4, complete false).
OBSERVED The simple sequence consisting of an amber singleton, a two-node green chain, and a green singleton is a direct counterexample under the written injective rules. recreated: node research/tree-three/verify-tree-three.mjs : d-cex-free: PASS 045-047 each pair legal; by hand: no amber in the later trees, and the chain cannot enter one node.
OBSERVED Requiring roots to agree does not produce three either: an amber singleton, a green root with amber child, a two-node green chain, and a green singleton is legal. recreated: node research/tree-three/verify-tree-three.mjs : d-cex-fixed: checked by hand: sizes 1,2,2,1 fit at most i; amber root cannot map to a green root; no amber in trees 3 and 4; larger trees cannot enter smaller ones.
CONFIRMED while this page separates Kruskal's general theorem, uniform TREE totality, and a fixed finite TREE value. public/strata/tree-three/index.html : d-relates-godel: line 316 "Those are different claims"; godel-incompleteness mentions Goodstein (2 hits).
CONFIRMED Both use an exhaustive browser search as a complete proof of a small combinatorial case, then mark the exact boundary where that finite census stops and a general theorem must take over. src/content/strata/complete-disorder-is-impossible.md : d-relates-cd: that layer runs "all 32,768 two-colourings of six people" live and cites Ramsey's theorem for the general case.
MINOR "datePublished":"2026-08-01","dateModified":"2026-08-01" git show b08bee9d4c3:public/strata/tree-three/index.html : d-jsonld-date: datePublished matches the frontmatter, but the page was changed visibly on 2026-09-28 (the Corrected line and the typed verdict logic, commit b08bee9d4c3) and dateModified was left at 2026-08-01. Fix at public/strata/tree-three/index.html:36. Fixed: dateModified now 2026-10-18.
WRONG (added) Requiring root-to-root does not turn that value into the often quoted answer: the search constructs a sequence of length at least 4 before its cutoff. So the root rule alone cannot explain Friedman's printed TREE[2] = 2. https://en.wikipedia.org/w/index.php?title=Kruskal%27s_tree_theorem&action=raw : Read in context, "the often quoted answer" is Friedman's 2 (the root-free value is already 3). The commonly quoted value is TREE(2) = 3 ("The sequence begins TREE(1)=1, TREE(2)=3"), which is the page's own root-free result; 2 appears in Friedman's 2006 post. The page never tells the reader that the widely published value agrees with its computation. Fix at public/strata/tree-three/index.html:259: "into Friedman's printed answer", and optionally note that the usually quoted TREE(2) = 3 matches the root-free result. Raised to WRONG by the fixer (checker level MINOR): in context the phrase can only mean 2, so a reader carries away that the commonly quoted TREE(2) is 2; Wikipedia wikitext re-read 2026-10-19: "The sequence begins TREE(1)=1, TREE(2)=3". Fixed.
UNVERIFIABLE (added) Whose theorem that is, precisely, because the credit is routinely collapsed onto the expositor. Read how four authoritative sources attribute the ATR0 result: Wikipedia ("Friedman found that the result was unprovable in ATR0", citing Simpson 1985), SEP supplement E ("cf. Simpson 1985"), Rathjen and Weiermann 1993 ("results, due to H. Friedman"), Freund 2020 ("D. Schmidt and H. Friedman") : All four credit Friedman, none collapses the credit onto Simpson; "routinely" may refer to informal writing, which I did not survey. Unsourced generalisation; the sources read lean against it.
MINOR (added) Simpson's nonprovability statement concerns Kruskal's general theorem under a formalization, not the casual slogan that a fixed sentence saying TREE with three labels exists is unprovable in ATR₀. https://sgslogic.net/t20/papers/nichtbeweisbarkeit-aml-1985.pdf : What it denies is right (nothing about a fixed numeral), but Simpson's exposition also proves a uniform finite miniaturization unprovable in ATR0, and calls it Friedman's main result: "Friedmans Hauptergebnis (Saetze 3.2 und 5.16 der vorliegenden Arbeit) ist, dass diese endlich-miniaturisierten Saetze in ATR0 bzw. Pi11-CA0 nicht beweisbar sind"; Satz 3.2: "Das kombinatorische Prinzip LWQO(T) ist in ATR0 nicht beweisbar." "Concerns Kruskal's general theorem" is narrower than the source. Fix at src/content/strata/tree-three.md:28: "concerns Kruskal's general theorem and a uniform finite form of it".
CONFIRMED (added) The full distinction is recorded in the research README. research/tree-three/README.md : The README holds the "Sources and access record" as stated. A reader cannot open it, though: https://artwaste.land/research/tree-three/README.md returns 404 and the GitHub repository returns 404 without login, and the same holds for the verifier path on the placard.
What was done
[fixed] schmidt-independent-simpson (WRONG): public/strata/tree-three/index.html said Friedman's nonprovability result "was obtained independently by Diana Schmidt"; Simpson 1985 says "Aber Schmidt bekam keine Nichtbeweisbarkeitsergebnisse". The sentence now credits Schmidt with independently noticing the trees-to-ordinal-notations connection and computing maximal order types, notes Simpson's statement, and says Freund (2020) names both for the theorem. Same correction in research/tree-three/README.md. Corrected 2026-10-18 line added on the page and in the markdown body.
[fixed] schmidt-joint-freund (MINOR): same sentence as above; Freund names both without "independently", which the new wording reflects.
[fixed] (added) "the often quoted answer" (raised to WRONG): index.html now says "Friedman's printed answer"; Corrected 2026-10-18 line names Wikipedia's TREE(2) = 3, the page's root-free result.
[fixed] d-jsonld-date (MINOR): JSON-LD dateModified 2026-08-01 to 2026-10-18; no line, per the office's rule.
[declined] fom-phrases (MINOR): the post says "inf preserving and label preserving"; "infimum-preserving" expands the abbreviation rather than misstating the condition. Tier B, listed not edited (triage K1).
[declined] d-embed-def (MINOR): the browser tests an equivalent recursive criterion and the verifier compares it with the literal definition through four vertices; the comparisons are right, the description overstates the method. Tier B, listed not edited (triage K4).
[declined] (added) Simpson's scope (MINOR): his exposition also proves a uniform finite miniaturization (Satz 3.2) unprovable in ATR0, so "concerns Kruskal's general theorem" is incomplete, not false. Tier B, listed not edited (triage K7).
[declined] (added) "routinely collapsed onto the expositor" (UNVERIFIABLE): unsourced generalisation left as the page's opinion; not a triage item, not edited.
The assay office: what a record is, and every layer re-read so far.