---
slug: something-has-to-stop-the-loop
passed: 2026-10-18
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)
checked: 94            # source-record entries plus the 15 lines the checker added
confirmed: 52
wrong: 11              # 2 WRONG + 9 MINOR
unverifiable: 0
observed: 29
stale: 2
---
This pass was the assay line's source-first re-read of this layer (batch claude-1018b, tier B). A Claude agent (claude-sonnet-5-5) wrote a source record for the page's claims (research/assay-line/claude-1018b/something-has-to-stop-the-loop/N1-sources.json); a second Claude agent (claude-opus-5-5) read each entry against its source and added fifteen claims of its own (N2-claude.md, whose claim lines are carried here unchanged); a Claude fixer (claude-opus-5-5) then re-read every WRONG and STALE item at its source (the Haveliwala and Kamvar paper, the 1999 PageRank report, the SEP entry on provability logic, and the git history of the two member pages), decided each one in triage.json and made the fixes. Two WRONG statements were fixed on the page with dated Corrected lines: the theorem's "exactly when", which adds a converse the paper does not prove, and the claim that no published statement of PageRank fixes a dead-end convention, which the 1999 report's section 2.7 does. The two STALE descriptions of other layers are dated in one Updated line, and the layer's verifier, which had gone red when the quoted card was reworded, now checks the quotation against the card as published on 2026-07-11. One MINOR (an unmarked omission inside the SEP quotation) was fixed by restoring the source's words; the other eight MINOR lines are declined for tier B and stay on the page as written.

## Claims
- CONFIRMED | Both start from a sentence that talks about itself - but they end in opposite places. ... no consistent theory can settle it. ... (the page's opening blockquote) | git show 84c2d96e88f:src/content/strata/the-importance-that-points-at-itself.md | [importance-card-then] Line 17 of that commit is the page's blockquote word for word (the original has an em dash where the record writes " - "); the same text was still the card at 881d6d962f4 (2026-08-01) and bd364907873 (2026-08-16), so the quotation was exact when this layer shipped on 2026-08-10.
- STALE | breaks the system open: no consistent theory can settle it. (quoted as "the note on that edge", the card as it stands) | src/content/strata/the-importance-that-points-at-itself.md | [importance-card-now] True when written. Changed 2026-09-29 (cc0848acb08) to "breaks the system open: the consistent system it describes cannot prove it.", after that layer's own claims pass marked the old clause MINOR. The page still prints the old text, and its own verifier now fails on it: "FAIL the quotation is verbatim, em dash and all" and "FAIL and it really does contain the em dash we are forbidden to remove".
- CONFIRMED | the relates: card of The Importance That Points at Itself, published 2026-07-11 | src/content/strata/the-importance-that-points-at-itself.md | [importance-card-date] "date: 2026-07-11"; commit 84c2d96e88f is dated 2026-07-11.
- MINOR | Suppose that all occurrences of the propositional variable p ... such that GL ⊢ B ↔ A(B). Moreover, the fixed point is unique, ... (presented as a verbatim SEP quotation) | https://plato.stanford.edu/entries/logic-provability/ | [dejongh-sambin-quote] Section 2.2 has a sentence between those two that the page drops with no ellipsis: "such that \[ \GL \vdash B \leftrightarrow A(B). \] This formula \(B\) is called a fixed point of \(A(p)\). Moreover, the fixed point is unique". The first omission ("for example A(p) = ¬□p, or ...") is marked with an ellipsis; this one is not. Meaning unchanged. The tool's NOT FOUND is the LaTeX markup, not a misquote.
- MINOR | On the coin the machines coordinate at 71 per cent, close to the human rate Schelling reports. | https://gamef21.classes.ryansafner.com/readings/Schelling-1960-Ch3.pdf | [schelling-quote-nonwiki] Primary, p. 55 footnote (OCR of the scan): "In the writer's sample, 36 persons concerted on "heads" in problem 1, and only 6 chose "tails."" Schelling reports counts (a share of 85.7 per cent), not a match rate; the comparable pairwise statistic computed from his counts is (36*35+6*5)/(42*41) = 74.9 per cent, which is close to 71.4. The-focal-point now makes exactly this distinction. N1's secondary (MPRA 23474, Abitbol 2009) quotes the same counts.
- WRONG | The theorem here is Haveliwala and Kamvar's (2003): the second eigenvalue of the Google matrix satisfies abs(λ₂) ≤ d, with equality exactly when the underlying walk has two or more closed classes. | https://nlp.stanford.edu/pubs/secondeigenvalue.pdf | [hk-theorem] The paper proves only the "if": "Theorem 2. Further, if P has at least two irreducible closed subsets ..., then the second eigenvalue of A is given by λ2 = c." The converse is false: a single periodic closed class also gives abs(λ₂) = d (P = [[0,1],[1,0]], d = 0.85: A has eigenvalues 1 and -0.85). The page's own figures need only the "if" plus its measured 0.512667.
- CONFIRMED | exactly the damping factor, the equality case of a 2003 theorem hit on the nose (dek) | https://nlp.stanford.edu/pubs/secondeigenvalue.pdf | [hk-dek] Theorem 2: at least two irreducible closed subsets gives λ2 = c; the self-loop rule has 47.
- CONFIRMED | its own verifier already notes operationally that the error decay ratio equals abs(λ₂) and that the theorem bounds it by d | public/checks/verify-the-importance-that-points-at-itself.mjs | [hk-bound-importance-verifier] Lines 225-226 (pipes written abs()): "Convergence rate: the measured error-decay ratio equals abs(lambda2), and the theorem (Haveliwala-Kamvar 2003) says abs(lambda2) <= d. Verify it operationally."
- CONFIRMED | Haveliwala, T. and Kamvar, S. (2003), "The Second Eigenvalue of the Google Matrix", Stanford technical report. | https://nlp.stanford.edu/pubs/ | [hk-citation] Listing: "Taher H. Haveliwala and Sepandar D. Kamvar. 2003. The Second Eigenvalue of the Google Matrix. Stanford University Technical Report." The PDF's title and authors match.
- CONFIRMED | De Jongh and Sambin, independently, in 1975: | https://plato.stanford.edu/entries/logic-provability/ | [dejongh-sambin-1975] "the fixed point theorem, which D. de Jongh and G. Sambin independently proved in 1975".
- CONFIRMED | de Jongh and Sambin, 1975, a self-reference guarded inside the provability operator has a fixed point unique up to provable equivalence (relates note) | https://plato.stanford.edu/entries/logic-provability/ | [dejongh-sambin-unique] Section 2.2: occurrences "under the scope of the provability operator"; "Moreover, the fixed point is unique, or more accurately, if there is another formula C such that GL ⊢ C ↔ A(C), then we must have GL ⊢ B ↔ C".
- CONFIRMED | Sambin, G. (1976), "An Effective Fixed Point Theorem in Intuitionistic Diagonalizable Algebras", Studia Logica 35: 345 to 361. | https://api.crossref.org/works/10.1007/bf02123402 | [sambin-citation] Crossref: title "An effective fixed-point theorem in intuitionistic diagonalizable algebras", Studia Logica 35(4) 345-361, 1976, Giovanni Sambin. SEP's bibliography adds a subtitle; the page's short title is fine.
- CONFIRMED | "An Effective Fixed Point Theorem in Intuitionistic Diagonalizable Algebras", Studia Logica 35: 345 to 361. | https://api.crossref.org/works/10.1007/bf02123402 | [sambin-citation-full] Same record as the line above.
- CONFIRMED | Work in GL, the modal logic whose □ reads "is provable in Peano arithmetic" and whose one non-trivial axiom is Löb's, and which Solovay (1976) proved captures exactly the principles of provability that arithmetic can prove about itself. | https://plato.stanford.edu/entries/logic-provability/ | [gl-solovay] "The logic GL results from adding the following axiom to the basic modal logic K: □(□A → A) → □A"; Solovay 1976: "GL ⊢ A if and only if for all realizations f, PA ⊢ f(A)". "One non-trivial axiom" is a fair gloss of K plus one axiom.
- CONFIRMED | Solovay, R. M. (1976), "Provability Interpretations of Modal Logic", Israel J. Math. 25: 287 to 304. | https://api.crossref.org/works/10.1007/bf02757006 | [solovay-citation] Crossref: Israel Journal of Mathematics 25(3-4) 287-304, 1976, Robert M. Solovay.
- CONFIRMED | GL is exactly the provability logic of Peano arithmetic. | https://plato.stanford.edu/entries/logic-provability/ | [solovay-gl-pa] Section 4.2, the arithmetical completeness theorem with its soundness converse.
- CONFIRMED | The finite frames the tableau agrees with are the standard semantics for GL (Segerberg 1971, completeness for finite transitive irreflexive frames) | https://plato.stanford.edu/entries/logic-provability/ | [segerberg-semantics] "Segerberg showed that GL is complete even with respect to the more restricted class of finite transitive irreflexive trees".
- MINOR | Segerberg, K. (1971), An Essay in Classical Modal Logic. Completeness of GL for finite transitive irreflexive frames, which is what makes the enumeration a legitimate refuter. | https://plato.stanford.edu/entries/logic-provability/ | [segerberg-citation] The attribution is right; the reason is the wrong direction. A countermodel is a legitimate refutation because of soundness, which SEP gives separately: "GL is modally sound with respect to the class of possible worlds models on transitive conversely well-founded frames, because all axioms and rules of GL are valid on such models." Completeness is what makes the enumeration able, in principle, to refute every non-theorem.
- CONFIRMED | Segerberg, K. (1971), An Essay in Classical Modal Logic. | https://plato.stanford.edu/entries/logic-provability/ | [segerberg-bib] Bibliography: "Segerberg, K., 1971, An Essay in Classical Modal Logic, Uppsala".
- CONFIRMED | The encyclopedia states that same fixed point in the same words, which makes it a check on this page's prover from outside this page. | https://plato.stanford.edu/entries/logic-provability/ | [godel-sentence-fixedpoint] "suppose that A(p) = ¬□p. Then the fixed point produced by such an algorithm is ¬□⊥ ... if a sufficiently strong formal theory T ... does not prove a contradiction"; the page: "¬□⊥: the statement that the theory does not prove a contradiction".
- MINOR | □p → p, the antecedent of Löb's axiom, returns more than one and not everything (also the relates note: "two for Löb's antecedent") | https://plato.stanford.edu/entries/logic-provability/ | [loeb-antecedent] The axiom is "□(□A → A) → □A"; its antecedent is □(□p → p), not □p → p. □p → p is the premise of Löb's theorem (the rule form) or the formula under the box. The count (2 of 9: ⊤ and ¬□⊥) is right per data.json logic.definitions "reflect".
- CONFIRMED | There is a real body of work that does build the bridge, in which a "later" modality gives guarded recursive definitions unique solutions by Banach's theorem on complete ultrametric spaces, and in which Löb's axiom is the guarded fixed point principle | https://arxiv.org/pdf/1208.3596v2 | [nakano-bridge] Read by pdftotext: "Nakano presented a simple type theory with guarded recursive types [30] which can be modelled using complete bounded ultrametric spaces"; "Theorem 2.9 (Internal Banach Fixed-Point Theorem)"; "an associated Löb rule for induction, (▷φ → φ) → φ". This is the LMCS 2012 journal version of the LICS 2011 paper.
- CONFIRMED | Nakano's "A Modality for Recursion" (2000) | https://api.crossref.org/works/10.1109/lics.2000.855774 | [nakano-citation] Crossref: "A modality for recursion", H. Nakano, Proceedings Fifteenth Annual IEEE Symposium on Logic in Computer Science, pp. 255-266 (LICS 2000); Crossref carries no date, 2000 is the symposium.
- CONFIRMED | Birkedal, L., Møgelberg, R. E., Schwinghammer, J. and Støvring, K. (2011), "First Steps in Synthetic Guarded Domain Theory" | https://api.crossref.org/works/10.1109/lics.2011.16 | [birkedal-citation] Crossref: "First Steps in Synthetic Guarded Domain Theory: Step-Indexing in the Topos of Trees", LICS 2011, pp. 55-64, the four authors in that order.
- CONFIRMED | with probability 1 − d at each step they give up and jump to a word chosen at random instead | http://infolab.stanford.edu/~backrub/google.html | [brin-page-surfer] Supported by the formula "PR(A) = (1-d) + d (PR(T1)/C(T1) + ... + PR(Tn)/C(Tn))" and by Wikipedia ("The probability that they instead jump to any random page is 1 - d"). The record's excerpt also carries Brin and Page's prose sentence "the d damping factor is the probability at each page the "random surfer" will get bored", which on its own says the opposite; it is the paper's known slip, and the page follows the formula.
- CONFIRMED | A random reader starts at a word, follows a word out of its definition, follows a word out of that one, and keeps going; | https://en.wikipedia.org/wiki/PageRank | [surfer-wikipedia] Random-surfer model, "an imaginary surfer who is randomly clicking on links"; the page applies it to its own graph.
- CONFIRMED | This is the standard stochasticity adjustment, and it is not part of the definition of PageRank; it is a repair applied before the definition can run. | https://en.wikipedia.org/wiki/PageRank | [dangling-patch] "pages with no outbound links are assumed to link out to all other pages in the collection"; Brin and Page's defining formula has no such term.
- CONFIRMED | Somebody has to say what happens next, and every published treatment says something different: | https://web.archive.org/web/2015/http://ilpubs.stanford.edu:8090/422/1/1999-66.pdf | [dangling-published] Read by pdftotext (the tool got a 214-character redirect): section "2.7 Dangling Links": "Because dangling links do not affect the ranking of any other page directly, we simply remove them from the system until all the PageRanks are calculated." Against Wikipedia's link-to-all patch, two published treatments that differ.
- CONFIRMED | Webster's Revised Unabridged Dictionary (1913, public domain) | https://gcide.gnu.org.ua/ | [webster-1913] GCIDE: "derived from Webster's Revised Unabridged Dictionary Version published 1913 by the C. & G. Merriam Co. Springfield, Mass. Under the direction of Noah Porter". The record's Gutenberg #29765 is titled only "Webster's Unabridged Dictionary" and carries no 1913 tags (0 hits for "1913" in its first 3 MB; positive control "Defn:" 11,127 hits); the dictionary layer itself names #661-673 and GCIDE.
- CONFIRMED | Webster's Revised Unabridged Dictionary (1913), public domain, via Project Gutenberg and the GCIDE lineage, as sliced and shipped by the dictionary layer. | research/the-dictionary-that-eats-itself/README.md | [webster-corpus-line] README lines 106-107: "Webster's Revised Unabridged Dictionary (1913) ... Project Gutenberg eBooks #661-673 and its derivative GCIDE. Public domain"; GCIDE's page confirms the 1913 lineage.
- CONFIRMED | which it formalises as a minimum feedback vertex set and which is NP-hard | https://en.wikipedia.org/wiki/Feedback_vertex_set | [fvs-nphard] "Whether there exists a feedback vertex set of size at most k is an NP-complete problem", so the minimisation is NP-hard.
- CONFIRMED | Harnad's symbol grounding problem | https://en.wikipedia.org/wiki/Symbol_grounding_problem | [harnad-sgp] "In his 1990 paper, Stevan Harnad ..."; the dictionary layer cites Harnad, Physica D 42:335-346 (1990).
- CONFIRMED | Schelling's coordination problem: two strangers who cannot communicate must choose the same thing, so each should choose what they expect the other to expect them to choose. | https://en.wikipedia.org/wiki/Focal_point_(game_theory) | [schelling-problem] Lead: a focal point is "a solution that people tend to choose by default in the absence of communication"; introduced by Schelling in The Strategy of Conflict (1960).
- CONFIRMED | What narrows them, in Schelling's account, is salience, which is not in the game. | https://en.wikipedia.org/wiki/Focal_point_(game_theory) | [schelling-salience] Grand Central example: no higher payoff, "its tradition as a meeting place raises its salience".
- CONFIRMED | The equation has exactly one solution, x = ½, sitting there the whole time. | public/strata/something-has-to-stop-the-loop/index.html | [x-1-minus-x] Arithmetic redone: x = 1 − x gives 2x = 1; iterating from 0 gives 1, 0, 1, 0.
- CONFIRMED | A page matters if pages that matter point to it. | http://infolab.stanford.edu/~backrub/google.html | [pagerank-def] Section 2.1.2 is the better excerpt: "a page can have a high PageRank if there are many pages that point to it, or if there are some pages that point to it and have a high PageRank."
- OBSERVED | The member's own figures are reproduced before anything new is computed: 1,200 nodes, 5,607 lookups, Kernel 755, Core 724, second component 3, 471 components, 98.6 per cent stay-in-Core, 47 sinks, greedy grounding set 465. | recreated: node research/something-has-to-stop-the-loop/verify.mjs in a scratch archive of 9ddc1e9045 (325 passed, 2 FAILED, neither on this) | [d-reproduced] data.json "reproduced"; cross-check.py independently: nodes 1200, edges 5607, components 471, Core 724, second SCC 3, 47 sinks.
- OBSERVED | Under the standard patch there is one closed class at every setting of the dial, all the way to d = 1 with the teleport switched off entirely | recreated: verify.mjs and cross-check.py ("closed classes, dangling mass spread uniformly got 1 want 1") | [d-closed] data.json closedBy.uniform.closedClasses 1, every uniform grid row closedClasses 1.
- OBSERVED | the measured second eigenvalue is 0.850000000 at d = 0.85 | recreated: cross-check.py ("abs(lambda2) selfloop d=0.85 got 0.85") and verify.mjs | [d-lambda-selfloop] data.json 0.8499999999947296.
- OBSERVED | it is 0.512667, six tenths of the bound | recreated: cross-check.py ("abs(lambda2) uniform d=0.85 got 0.512667 want 0.512667", pipes written abs()) | [d-lambda-uniform] 0.512667 / 0.85 = 0.603, six tenths.
- OBSERVED | with 2 of the six pairs at an L¹ distance of 2.000, the maximum, meaning those two share no word at all | recreated: verify.mjs ("two of the six pairs share nothing at all") | [d-pairs] data.json startPairs: path-data 2, new-data 1.9999999999999925; disjointPairs 2.
- OBSERVED | That removes 48 words and leaves 1,152. | recreated: verify.mjs | [d-pruned] data.json pruned removed 48, remaining 1152, closedClasses 1, largestClosed 724, isExactlyTheCore true.
- OBSERVED | it carries 91.31 per cent of the answer at d = 0.85 rather than all of it | recreated: cross-check.py ("Core mass at d=0.85 got 0.913104") | [d-core-mass] data.json coreMassByD 0.85 = 0.9131035.
- OBSERVED | 724 words that only define each other, which 98.6 per cent of lookups out of a Core word never leave | recreated: verify.mjs; public/strata/the-dictionary-that-eats-itself/index.html | [d-stay-in-core] data.json stayInCorePct 98.6; the dictionary page: "98.6% lands you on another word inside the Core".
- OBSERVED | Take the top 465 words by importance under the standard patch at d = 0.85 and intersect them with that layer's greedy grounding set of the same size: (308, 66.2%, 38.8%, Jaccard 0.495) | recreated: verify.mjs; arithmetic redone | [d-overlap] 308/465 = 66.24%; 465*465/1200 = 180.19 = 38.75%; 308/(930-308) = 0.495.
- OBSERVED | 157 of the words you would have to ground are not in the top 465 by importance at all. | recreated: arithmetic on research/something-has-to-stop-the-loop/data.json | [d-157] 465 − 308 = 157.
- CONFIRMED | the minimum grounding sets are exactly three, all of size two: {cause, act}, {cause, power}, {act, make} | public/strata/the-dictionary-that-eats-itself/index.html | [d-six-word] "Three different pairs of words: {cause, act}, {cause, power}, {act, make}"; "Exact only on the six-word subgraph, by brute force over all vertex subsets."
- OBSERVED | Order those six by importance on the full graph and the top two are act, make, which is one of the three. | recreated: verify.mjs | [d-six-order] data.json curatedRanks act 1, make 10, power 14, cause 23, effect 39, result 205; topTwoIsMinimum true.
- OBSERVED | 142 distinct formulas of size 5 or less collapse, under this logic, to exactly 9 things | recreated: verify.mjs (recomputes G.enumerateFormulas and G.equivalenceClasses, lines 246-248) | [d-142-9] data.json formulasEnumerated 142, equivalenceClasses 9.
- OBSERVED | Frames enumerated: 23 at three worlds or fewer, 242 at four, 4,473 at five. | recreated: verify.mjs; https://oeis.org/A001035 | [d-frames] Independent check: labelled posets on n points are 1, 3, 19, 219, 4231 (A001035), cumulative 23, 242, 4473.
- OBSERVED | the tableau and the four-world enumeration agree on 4,000 of 4000, with 0 cases where the tableau called a formula valid that a small frame refutes | recreated: verify.mjs | [d-agree] data.json agreement tested 4000, agree 4000, tableauValidFrameRefuted 0, seed 20260810.
- OBSERVED | And the tableau is held to 8 textbook facts that it could fail, 4 of which it must call false: | recreated: verify.mjs | [d-controls] 8 controls, expect false on T, D, ¬□⊥, □□⊥→□⊥; each verdict is also textbook-correct for GL.
- OBSERVED | ¬p, the liar, returns none, and no bound on the search changes that. | recreated: verify.mjs; research/something-has-to-stop-the-loop/data.json | [d-solver-table] answers 0 at size five and 0 at six; and no formula F has GL ⊢ F ↔ ¬F, since GL is consistent.
- OBSERVED | p, the truth-teller, returns every class in the space ... and rises when you raise the bound. | recreated: verify.mjs; research/something-has-to-stop-the-loop/data.json | [d-truth-teller] answers 9 at size five, 12 at six.
- OBSERVED | at the default bound it is ⊤ and ¬□⊥, the sentence saying the theory is consistent. | recreated: verify.mjs; research/something-has-to-stop-the-loop/data.json | [d-loeb-answers] representatives ⊤, ¬□⊥ (three at size six).
- OBSERVED | □□□□□¬p is guarded, so exactly one answer exists, and at size five the search returns nothing at all: the answer is □□□□□⊥, which is one symbol too big for the space. | recreated: verify.mjs; research/something-has-to-stop-the-loop/data.json | [d-deep-preset] answers 0 at five, 1 at six (□□□□□⊥, six symbols).
- OBSERVED | Ask ¬□¬p repeatedly from ⊤ and the iterates run ¬□⊥, ¬□□⊥, ¬□□□⊥, … and never repeat. | recreated: verify.mjs; research/something-has-to-stop-the-loop/data.json | [d-stopping] iterationSeq ⊤, ¬□⊥, ¬□□⊥, ...; by hand A(¬□ⁿ⊥) = ¬□ⁿ⁺¹⊥, and ⊥ solves it since ¬□¬⊥ = ¬□⊤ = ⊥.
- OBSERVED | On the coin the machines coordinate at 71 per cent | research/second-space/focal-points/_focal.json | [d-ladder-coin] coin pMatch 0.7142857 (6 heads, 1 tails: 15 of 21 pairs).
- MINOR | As the choice space opens the agreement falls away, and on a free single word it is zero: every model that answered wrote a different one. | research/second-space/focal-points/_focal.json | [d-ladder-word] "answered": 7, "n": 6. The seventh, Nemotron-3 Nano 30B, answered with leaked reasoning and committed no word. The focal-point layer itself now says "every one of the 6 models that committed wrote a different word". pMatch 0 is right.
- OBSERVED | Seven models from three makers answered; per game the count is six or seven | research/second-space/focal-points/_focal.json | [d-models] nModels 7, nMakers 3; per-game n is 6 or 7.
- OBSERVED | the models were put to the game on 2026-07-12, the date on the raw session file kept beside it | git show 9ddc1e9045:research/second-space/focal-points/_raw-2026-07-12.json | [d-run-date] the file exists at 9ddc1e9045; data.json runDate 2026-07-12; facts.md F7 explains why _focal.json's own date field is not used.
- CONFIRMED | Figures read from research/second-space/focal-points/_focal.json, which that layer's own verifier writes | research/something-has-to-stop-the-loop/build-data.mjs | [d-focal-file] "const FOCAL_PATH = 'research/second-space/focal-points/_focal.json';"
- CONFIRMED | and builds the graph by slicing that layer's own parse code out of that layer's own verifier rather than copying it. | research/something-has-to-stop-the-loop/build-data.mjs | [d-build-slice] sliceOut between "const STOP = new Set(" and "// exact minimum feedback vertex set"; verify.mjs does the same with new Function.
- CONFIRMED | finds components with Kosaraju rather than Tarjan, solves for the answer by Gauss-Seidel rather than power iteration | research/something-has-to-stop-the-loop/cross-check.py | [d-cross-kosaraju] "Kosaraju, not Tarjan"; "the answer, by Gauss-Seidel rather than power iteration" (line 156).
- CONFIRMED | where numpy is importable, by dense eigendecomposition of the whole 1,200 by 1,200 operator | research/something-has-to-stop-the-loop/cross-check.py | [d-cross-numpy] lines 228-245; skipped here (no numpy), as the script says.
- CONFIRMED | engine/loop.mjs and engine/gl.mjs are inlined into this page verbatim and imported by the verifier, which asserts the inlined text is byte-identical to the files. | research/something-has-to-stop-the-loop/verify.mjs | [d-inline] header: "byte-identical to their sources"; those checks passed in the run.
- OBSERVED | 39 checks, including that an input outside the closed fragment is refused rather than quietly answered. | git show 9ddc1e9045:memory/log.d/2026-08-10T1900Z-something-has-to-stop-the-loop.md | [o-39-checks] line 96: "`verify-page.mjs` **39/39**"; verify-page.mjs line 133: "an atom outside the closed fragment is refused". Not re-run (needs a browser and a built site).
- CONFIRMED | the 1,200 most frequent single-word content headwords of Webster's Revised Unabridged Dictionary (1913, public domain), each reduced to its first-sense gloss trimmed to thirty tokens | public/strata/the-dictionary-that-eats-itself/index.html | [d-dict-corpus] "The shipped lexicon is the 1,200 most-frequent single-word content headwords of Webster's Revised Unabridged Dictionary (1913, public domain), each reduced to its first-sense gloss trimmed to 30 tokens."
- CONFIRMED | not grounded primitives but artefacts of the 1,200-word slice, words like data, user, computer, whose real defining words fell outside the cut | public/strata/the-dictionary-that-eats-itself/index.html | [d-dict-sinks] "data, user, computer, server, photo… ... modern terms whose real defining words (digital, machine, network) simply fell outside this 1,200-word slice. They aren't primitive. They are holes in the sample."
- CONFIRMED | the largest strongly connected component of the definition graph, 724 words | public/strata/the-dictionary-that-eats-itself/index.html | [d-dict-core] "Core = largest SCC"; "the 724-word component where every word has a path to and from every other".
- CONFIRMED | It never says how many there are. | src/content/strata/godel-incompleteness.md | [d-dict-nohow] Searched that md and public/strata/godel-incompleteness/index.html: "how many" 0, "unique" 0, "only one" 0; positive control "diagonal" 8 hits, "there is a sentence" 1.
- CONFIRMED | It shows that self-reference always manufactures a fixed point and sorts the results by what becomes of them: forbidden, undetermined, unprovable, self-fulfilling, merely true. | public/strata/the-fixed-point/index.html | [d-fixed-sorts] "The sentence always exists"; "whether the fixed point is forbidden (the Liar), out of reach of proof (Gödel), self-fulfilling (Löb), undetermined (the Truth-teller), or merely rare and findable (the autogram)"; same at a454f36641f (2026-07-31).
- STALE | it asks whether a diagonal is present, this asks how many fixed points the diagonal has (also the relates note: "that portal asks whether a diagonal is present in a given wall") | git show 26148524b64:public/strata/the-limits-of-knowing/index.html | [d-limits] True when written: on 2026-08-10 that page said "For each, ask one question: is the diagonal in it? ... The answer is what sorts the walls." Corrected 2026-10-15 (d235d95bf1a, 7 WRONG fixed): it now asks "which theorem makes the wall?" and says the diagonal's "presence alone does not establish an obstruction". N1's excerpt is the new text, which does not support the claim.
- OBSERVED | Seven models from three makers answered | research/second-space/focal-points/_focal.json | [d-focal-ladder-card] "nModels": 7, "nMakers": 3.
- OBSERVED | have glosses that mention no other word in the vocabulary. (47 of the 1,200 words) | recreated: cross-check.py ("words that define nothing got 47 want 47") | [d-dangling-47] data.json dangling.count 47.
- OBSERVED | Four starting distributions are run every time: flat, and all the mass on each of new, path and data. | research/something-has-to-stop-the-loop/data.json | [d-starts] starts (flat), new, path, data; startIndices 0, 1199, 40 are new, path, data.
- OBSERVED | the four starts agree to about 2 × 10⁻¹⁵ | recreated: verify.mjs | [d-spread-uniform] uniform d 0.85 spread 1.69e-15; d 1 spread 2.56e-15.
- OBSERVED | the four starts reach four different answers | recreated: verify.mjs | [d-spread-selfloop-d1] selfloop d 1 spread 2; supports 47 (flat), 15 (new), 1 (path), 1 (data).
- CONFIRMED | It does not run a random walk on any of it. | public/strata/the-dictionary-that-eats-itself/index.html | [d-dict-no-walk] Raw HTML and md: "PageRank" 0, "random walk" 0, "stationary" 0, "damping" 0, "teleport" 0; positive control "Tarjan" 11 hits.
- WRONG | (added) that in the numeric setting the answer is the number of closed classes, which on this dictionary is one or forty-seven depending on a convention for forty-seven words that no published statement of PageRank contains | https://web.archive.org/web/2015/http://ilpubs.stanford.edu:8090/422/1/1999-66.pdf | Page, Brin, Motwani and Winograd's own statement of PageRank has a section "2.7 Dangling Links" that fixes a convention: "we simply remove them from the system until all the PageRanks are calculated". Wikipedia's statement fixes another ("pages with no outbound links are assumed to link out to all other pages"). The page's body agrees with them, not with this sentence: "every published treatment says something different" and "This is the standard stochasticity adjustment".
- MINOR | (added) Brin, S. and Page, L. (1998), "The Anatomy of a Large-Scale Hypertextual Web Search Engine". The circular definition, the damping factor, and rank sinks. | http://infolab.stanford.edu/~backrub/google.html | The Anatomy text has no rank sinks: "sink" 0 hits, "dangling" 0 (positive control "damping factor" 3, "recursively" 1). Rank sinks are in Page et al., "The PageRank Citation Ranking": "The loop forms a sort of trap which we call a rank sink" (1999-66 PDF, section 2.4).
- MINOR | (added) guarded self-reference returns one every time, the liar returns none, and the truth-teller returns all nine (dek; the relates note to godel-incompleteness says "one for every guarded definition") | research/something-has-to-stop-the-loop/data.json | The page's own guarded preset □□□□□¬p returns 0 at the default size-five bound (logic.definitions "deep": answers 0, answersAtSix 1). The body qualifies it correctly ("at every bound large enough to hold it"); the dek and the note drop the qualifier.
- MINOR | (added) reads the dictionary layer's lexicon.json, checks it byte-for-byte against the copy inlined in that layer's shipped page | research/something-has-to-stop-the-loop/build-data.mjs | Lines 38-43 parse both, un-escaping &lt; and &gt; first, and compare JSON.stringify of the parsed objects ("const sameLexicon = JSON.stringify(inlineLexicon) === JSON.stringify(lexicon)"). verify.mjs line 58 names it correctly: "the shipped lexicon and lexicon.json are the same object". facts.md: "required to be the same object". The same object, not the same bytes.
- MINOR | (added) Every row is recomputed by verify.mjs and again, with different code and in two cases a different algorithm, by cross-check.py. | research/something-has-to-stop-the-loop/cross-check.py | The table renders all 15 grid rows (page.template.html line 786, D.grid.map). cross-check.py recomputes abs(λ₂) for 6 of them (uniform and self-loop at d 0.5, 0.85, 0.95, lines 217-221), closed-class counts per convention, and the stationary vector only at uniform d = 0.85. The leak rows, d = 0.99 and d = 1, and the asks, spread and mass columns are not re-derived in Python. Run output: 20/20.
- CONFIRMED | (added) The count of closed classes is the multiplicity of the eigenvalue 1 | https://nlp.stanford.edu/pubs/secondeigenvalue.pdf | Proof of Lemma 2: "the multiplicity of the eigenvalue 1 for P is equal to the number of irreducible closed subsets of P".
- CONFIRMED | (added) Brin, S. and Page, L. (1998), "The Anatomy of a Large-Scale Hypertextual Web Search Engine" (the citation itself) | https://api.crossref.org/works/10.1016/S0169-7552(98)00110-X | Crossref: "The anatomy of a large-scale hypertextual Web search engine", Brin and Page, Computer Networks and ISDN Systems 30: 107-117, April 1998; the infolab copy carries the same title and authors.
- CONFIRMED | (added) Vincent-Lamarre, P., Blondin Massé, A., Lopes, M., Lord, M., Marcotte, O. and Harnad, S. (2016), "The Latent Structure of Dictionaries", Topics in Cognitive Science 8(3): 625 to 659. | https://api.crossref.org/works/10.1111/tops.12211 | Crossref: same title, Topics in Cognitive Science 8(3) 625-659, 2016, the six authors in that order.
- CONFIRMED | (added) Schelling, T. (1960), The Strategy of Conflict. The focal point. | https://en.wikipedia.org/wiki/Focal_point_(game_theory) | "introduced by the American economist Thomas Schelling in his book The Strategy of Conflict (1960)"; chapter 3 scan, p. 55, holds the focal-point experiments.
- CONFIRMED | (added) the classical fact is that you can always build one: for any property you like there is a sentence asserting that property of itself. The Sentence That Says It Can't Be Proved makes that construction operable, and it is careful to claim only that such a sentence exists. | public/strata/godel-incompleteness/index.html | "The diagonal lemma proves that for any property P expressible in arithmetic (a formula with one free variable, of any complexity), there is a sentence G for which the system itself proves that G holds exactly when G's own Gödel number has property P"; the layer's title is "The Sentence That Says It Can't Be Proved".
- CONFIRMED | (added) The dictionary layer hands its Core to Harnad's symbol grounding problem and is careful that the inference is contested | public/strata/the-dictionary-that-eats-itself/index.html | "it is not a theorem ... it is an argument, and it is still contested. In 1990 Stevan Harnad posed the symbol grounding problem".
- CONFIRMED | (added) Its own card relates it to No Fix From Inside, a portal that already holds the grounding argument | src/content/strata/the-dictionary-that-eats-itself.md | relates "- to: no-fix-from-inside", note "you can't repair a symbol system's grounding from inside the symbols".
- CONFIRMED | (added) the minimum grounding set ... which it formalises as a minimum feedback vertex set ..., so that layer ships a greedy upper bound | public/strata/the-dictionary-that-eats-itself/index.html | "That set is a minimum feedback vertex set"; "That greedy set is an upper bound only".
- CONFIRMED | (added) Its truth-teller card and this page's nine classes are the same phenomenon met from two directions (relates: "Its truth-teller, unforced in both directions") | public/strata/the-fixed-point/index.html | Operator-dial card: "The Truth-teller. Consistent either way and grounded in nothing. ... Its truth value is unforced in both directions." Present on 2026-07-31 (a454f36641f) and at 9ddc1e9045.
- CONFIRMED | (added) That layer put the game to free models, alone and unable to signal | public/strata/the-focal-point/index.html | "We put 7 free models from 3 distinct lineages into Schelling's game ... each asked, alone and with no way to signal the others, to make a choice designed to match an unknown partner AI."

## Findings
- [fixed] WRONG "with equality exactly when the underlying walk has two or more closed classes": Haveliwala and Kamvar (2003) prove only that direction ("Theorem 2. Further, if P has at least two irreducible closed subsets ..., then the second eigenvalue of A is given by λ2 = c"), and the converse fails for a single periodic closed class. Now "with equality whenever" in the prose, the live readout string, the inlined engine comment (engine/loop.mjs and the page), the labels in verify.mjs and cross-check.py, and facts.md; dated Corrected line on the page and in the markdown.
- [fixed] WRONG "a convention for forty-seven words that no published statement of PageRank contains": the 1999 PageRank report (Page, Brin, Motwani and Winograd), section 2.7 "Dangling Links", says "we simply remove them from the system until all the PageRanks are calculated". Now "that PageRank's defining equation leaves open and published treatments settle differently"; its copies ("a rule ... that nobody writes down" in the dek, "an unwritten rule" in the meta, og, twitter, plain and markdown descriptions) now say the rule is outside the equation. Dated Corrected line on the page and in the markdown.
- [fixed] MINOR the SEP quotation of the de Jongh and Sambin theorem dropped "This formula B is called a fixed point of A(p)." between "GL ⊢ B ↔ A(B)." and "Moreover" with no ellipsis; the source's sentence is restored inside the quotation (no line on the page, the office's rule for MINOR).
- [dated] STALE the opening blockquote quotes the importance layer's card as published on 2026-07-11 ("no consistent theory can settle it", with its em dash); that card was reworded on 2026-09-29 (cc0848acb08). The quotation is left as the 2026-07-11 text it cites, the page's Updated 2026-10-18 line says the card has changed and what it says now, and verify.mjs now compares the blockquote with the 2026-07-11 text and requires that line while the card differs (it had two FAILs on the reworded card).
- [dated] STALE "it asks whether a diagonal is present" (page) and "that portal asks whether a diagonal is present in a given wall" (relates note): true of The Limits of Knowing on 2026-08-10 ("For each, ask one question: is the diagonal in it?"), which since 2026-10-15 (d235d95bf1a) asks "which theorem makes the wall?". Dated in the same Updated 2026-10-18 line.
- [declined] MINOR "close to the human rate Schelling reports": Schelling reports counts (36 heads, 6 tails), not a match rate; the pairwise rate his counts imply is 74.9 per cent, near 71. Loose, not false; tier B, listed.
- [declined] MINOR Segerberg's completeness is named as "what makes the enumeration a legitimate refuter"; soundness is what makes a countermodel legitimate, completeness what makes the refuter able to find every non-theorem. The citation is right; tier B, listed.
- [declined] MINOR "□p → p, the antecedent of Löb's axiom" (and "two for Löb's antecedent"): the axiom's antecedent is □(□p → p); □p → p is the hypothesis of Löb's theorem in rule form. The count of two is right; tier B, listed.
- [declined] MINOR "every model that answered wrote a different one": seven answered and six committed a word; pMatch 0 is right. Tier B, listed.
- [declined] MINOR the Anatomy paper is credited with "rank sinks", which are in the 1999 PageRank report, section 2.4. Same authors' adjacent paper, one of three annotated topics; tier B, listed.
- [declined] MINOR "guarded self-reference returns one every time" (dek) and "one for every guarded definition" (relates note): the page's □□□□□¬p preset returns 0 at the default size-five bound; the body carries the qualifier. Tier B, listed.
- [declined] MINOR "checks it byte-for-byte": build-data.mjs compares the two parsed objects (JSON.stringify), the same object rather than the same bytes; the verifier names it correctly. Tier B, listed.
- [declined] MINOR "Every row is recomputed by verify.mjs and again ... by cross-check.py": verify.mjs asserts every row; cross-check.py re-derives abs(λ₂) on 6 of the 15 rows, the closed-class counts and one stationary vector. An overclaim about the page's own checking; tier B, listed.