--- slug: the-limits-of-knowing passed: 2026-10-14 by: the assay line (research/assay-line/queue-1014c/), Codex fixer directed by claude-assaying-boyle-1014; source record by Codex, checked by Codex; repair review by Codex, 2026-10-14 checked: 108 confirmed: 84 wrong: 24 unverifiable: 0 observed: 0 stale: 0 --- This was the directed repair pass for the-limits-of-knowing from research/assay-line/queue-1014c/: the fixer independently re-read the evidence for all 24 triaged items (12 WRONG and 12 MINOR), repaired their authored text and in-scope copies, and retained the checkers’ 84 CONFIRMED claims below with their original entry numbers and scoped readings. Claim wording records the pre-repair statements; findings describe the repairs. The 12 MINOR lines count toward wrong for the gate but remain MINOR and receive no correction line. Seven distinct WRONG errors have dated correction lines on the page and at the end of the markdown body. Repair review found X1 copies outside this layer and retained historical screenshot copies; their open findings below qualify the authored-text repairs. This is the assigned triage pass, not a fresh certification of every sentence in the layer. ## Claims - MINOR | X1 (diagonal-separates): is what separates the soft wall from the two hard ones. | https://arxiv.org/pdf/math/0305282 | Yanofsky p. 19 derives a computable self-reproducing machine. The diagonal alone does not imply an obstruction; the halting and incompleteness theorems supply the limits in these examples. - MINOR | X2 (beaver-definition): A Busy Beaver is the hardest-working Turing machine of its size: among all n-state machines that eventually halt on a blank tape, the one that runs the longest. | https://www.scottaaronson.com/papers/bb.pdf | Aaronson p. 1 fixes alphabet {0,1}, a two-way infinite tape, and blank input. The displayed values use this model. - MINOR | X3 (six-unnamable): Add one state and the value leaves the realm of things we can name. | https://wiki.bbchallenge.org/wiki/BB(6) | The BB(6) project record calls the exact value unsolved and gives finite arrow-notation lower bounds. Unknown is not mathematically unnameable. - WRONG | X4 (six-all-towers): it is past every number you could build by stacking exponentials | https://www.scottaaronson.com/papers/bb.pdf | Aaronson p. 2 defines each BB(n) as a finite integer. Inference: the finite towers 2↑↑h are unbounded as h increases, so some exceed BB(6). Function growth does not make one fixed value exceed every tower. - WRONG | X5 (six-best-bound): the best lower bound is 2↑↑↑5 in Knuth's arrows, a tower of towers. | https://wiki.bbchallenge.org/wiki/BB(6); https://bbchallenge.org/ | The project record dates 10↑↑10↑↑10↑↑8 to June 2025. With right association, this exceeds 2↑↑↑5 = 2↑↑(2↑↑65536). The coarser homepage bound is valid but was not best when the layer was written. - MINOR | X6 (displayed-exponential): which is less than 4ₛ | https://arxiv.org/html/2303.09521v2 | Campos et al., section 1, gives the classical bound R(k) ≤ 4^k. The authored entity 4ₛ used a subscript where an exponent was intended. - WRONG | X7 (k43-printed-power): The number of two-colourings of the 43-person graph is 2⁷⁰³ | git show f5e5f84f34:research/the-limits-of-knowing/verify.mjs | Re-read verify.mjs and independently computed 43*42/2 = 903, (2n**903n).toString().length = 272, and (2n**703n).toString().length = 212. - MINOR | X8 (universe-atoms): roughly 10⁸⁰ atoms in the observable universe. | https://ntrs.nasa.gov/api/citations/20210010980/downloads/ICCL%20Webinar%202.pdf; https://arxiv.org/abs/1605.04351 | Re-read the retained NASA slide 89 text: it gives an upper bound and a displayed calculation ending at 3×10^71. Page (2016), abstract and p. 1, supplies the replacement estimate: order 10^80 baryons in the observable universe. This is a source-match repair, not proof that the original rough scale was false. - MINOR | X9 (any-operator): the one that turns any operator into a sentence about itself. | http://www.tac.mta.ca/tac/reprints/articles/15/tr15.pdf; https://arxiv.org/pdf/math/0305282 | Yanofsky p. 15, Theorem 4 and its setup, works with one-free-variable formulas and syntax coding. A definable predicate in a sufficiently expressive theory is the supported scope. - WRONG | X10 (rado-proof-diagonal): Radó's proof is the halting diagonal | https://infoteorica.weebly.com/uploads/1/7/8/9/17895653/rado_on_non-computable_functions_bell_system_technical_journal_41_1962_pp._877-884.pdf; https://www.scottaaronson.com/papers/bb.pdf | Radó p. 877 disclaims enumeration of computable functions; section V, pp. 880-882, proves eventual growth domination. Aaronson Proposition 1 gives the halting reduction used on the page. - MINOR | X11 (745-independent): BB(745) is independent of ZFC | https://docs.bbchallenge.org/papers/Riebel2023.pdf | Riebel p. 2 assumes ZFC consistency. Theorem 3.6.1, p. 77, explicitly conditions the result on correct NQL compiler and code; its conclusion is non-provability of the exact value in ZFC. - WRONG | X12 (745-all-three): BB(745) is at once enormous (the resource wall), uncomputable (the computability wall), and undecidable in ZFC (the proof wall). | https://www.scottaaronson.com/papers/bb.pdf; https://docs.bbchallenge.org/papers/Riebel2023.pdf | Aaronson p. 2 defines finite values and Proposition 1 concerns a uniform function. Inference: for each fixed integer a finite program can print it; this does not identify its digits. Riebel p. 77 addresses proof in ZFC. - WRONG | X13 (745-no-axioms): a single finite integer no axioms can pin down. | https://www.scottaaronson.com/papers/bb.pdf; https://docs.bbchallenge.org/papers/Riebel2023.pdf | Aaronson Proposition 3 fixes one computable, arithmetically sound theory T, with a threshold depending on T. Inference: the true equality for one finite value could be added as an axiom. Riebel only establishes a qualified limit for ZFC. - MINOR | X14 (card-bb): Halts in 47,176,870 at five states; uncomputable beyond. | https://www.scottaaronson.com/papers/bb.pdf | Aaronson Proposition 1 rules out a uniform algorithm for every input. The card could be read as a statement about an infinite tail, but also misleadingly as noncomputability of individual values. - WRONG | X15 (colouring-counts): The colouring counts 2^C(k,2) are computed exactly (K43 = 2⁷⁰³, a 272-digit number) and shown to exceed the ~10⁸⁰ atom count. | git show f5e5f84f34:research/the-limits-of-knowing/verify.mjs | The same independent arithmetic as X7 gives 903 edges and 272 digits. This apparatus occurrence repeated the incorrect exponent. - WRONG | X16 (748-attribution): building on the 748-state machine of Yedidia & Aaronson [2016] | https://docs.bbchallenge.org/papers/Riebel2023.pdf | Riebel p. 2 assigns 748 states to O’Rear in 2017 and 7910 states to Yedidia and Aaronson in 2016. - WRONG | X17 (citation-yedidia): Yedidia & Aaronson [2016] | https://docs.bbchallenge.org/papers/Riebel2023.pdf | Riebel p. 2 confirms that the Yedidia and Aaronson citation was attached to the wrong state count. Their actual 2016 result used 7910 states. - MINOR | X18 (dial-bb-object): S(5)=47,176,870; S(6) > 2↑↑↑5; S(7+) beyond naming | https://www.scottaaronson.com/papers/bb.pdf; https://wiki.bbchallenge.org/wiki/BB(6) | Aaronson p. 2 defines finite BB values. BB Challenge supports the five-state value and six-state coarse bound; later unknown exact values are not beyond mathematical naming. - WRONG | X19 (dial-bb-diagonal): the halting diagonal IS the proof (Radó 1962) | https://infoteorica.weebly.com/uploads/1/7/8/9/17895653/rado_on_non-computable_functions_bell_system_technical_journal_41_1962_pp._877-884.pdf; https://www.scottaaronson.com/papers/bb.pdf | Radó section V proves growth domination rather than the halting reduction. Aaronson Proposition 1 supports the modern reduction in the dial. - MINOR | X20 (dial-godel-independent): its value is independent of ZFC (Riebel 2023) | https://docs.bbchallenge.org/papers/Riebel2023.pdf | Riebel pp. 2 and 77 require ZFC consistency and correct NQL compiler/code for the cited proof limit. The dial now states those conditions. - WRONG | X21 (dial-meet): BB(745) is at once enormous (resource), uncomputable (computability), and undecidable in ZFC (proof). | https://www.scottaaronson.com/papers/bb.pdf; https://docs.bbchallenge.org/papers/Riebel2023.pdf | Aaronson pp. 2-4 separates finite values from the uniform uncomputable function. Riebel p. 77 concerns non-provability of the exact value. This generated summary repeated X12. - MINOR | X22 (halt-five-settled): settled in 2024. One more state and there is no such number we can reach. | https://wiki.bbchallenge.org/wiki/BB(6) | The BB(6) project record states that the problem is unsolved. This is not evidence of permanent unreachability; the existing five-state 2024 result is preserved. - MINOR | X23 (dek-independent): a single finite integer, BB(745), that ZFC cannot determine. | https://docs.bbchallenge.org/papers/Riebel2023.pdf | Riebel pp. 2 and 77 supply the consistency and compiler/code assumptions missing from the dek. - WRONG | X24 (md-meeting-point): single finite integer that is at once enormous (resource), uncomputable (computability), and independent of ZFC (proof) | https://www.scottaaronson.com/papers/bb.pdf; https://docs.bbchallenge.org/papers/Riebel2023.pdf | The markdown explicitly applied uncomputable to one integer. Aaronson pp. 2-4 and the finite constant-output-program argument establish the same error as X12; Riebel concerns the qualified proof limit. - CONFIRMED | pinned only between 43 and 46, that no one on Earth has ever computed. | https://arxiv.org/html/2409.15709v1 | Retained from the source re-read in N2-codex.md. Entry 6 (ramsey-five-interval): Angeltveit and McKay, Theorem 1.1: "is less than or equal to 46"; the following paragraph calls 43 "still the best" lower bound. This supports an interval, not an exact value. - CONFIRMED | a five-state machine that halts after 47,176,870 steps | https://discuss.bbchallenge.org/t/july-2nd-2024-we-have-proved-bb-5-47-176-870/237 | Retained from the source re-read in N2-codex.md. Entry 7 (five-runtime): The July 2, 2024 announcement says "BB(5) = 47,176,870" is proved and "the proof has been formally written in Coq". - CONFIRMED | a six-state successor whose runtime is a tower of exponentials nobody can write down. | https://wiki.bbchallenge.org/wiki/BB(6) | Retained from the source re-read in N2-codex.md. Entry 8 (six-runtime-description): The BB Challenge wiki gives "S(6)>Σ(6)>10↑↑10↑↑10↑↑8" and dates the champion to June 2025. Its expansion is enormous, but its finite bounds have symbolic descriptions. - CONFIRMED | a sentence that is true and that no proof in your system will ever reach. | https://arxiv.org/pdf/math/0305282 | Retained from the source re-read in N2-codex.md. Entry 9 (godel-truth): Yanofsky p. 16 says "in a consistent and ω-consistent theory" and "equivalent to its own statement of unprovability." This confirms the usual sufficiently expressive, consistent-theory reading, not an assertion about every possible formal system. - CONFIRMED | Two states halt in 6 steps; three in 21; four in 107; five in 47,176,870 | https://oeis.org/A060843/internal | Retained from the source re-read in N2-codex.md. Entry 14 (small-maxima): OEIS A060843 gives "1,6,21,107,47176870" and defines the sequence as the "maximal number of steps". The scope is the standard two-symbol machine model. - CONFIRMED | a fact settled only in 2024, and checked inside a proof assistant. | https://discuss.bbchallenge.org/t/july-2nd-2024-we-have-proved-bb-5-47-176-870/237 | Retained from the source re-read in N2-codex.md. Entry 15 (five-proof-date): The July 2, 2024 announcement says "BB(5) = 47,176,870" is proved and "the proof has been formally written in Coq". - CONFIRMED | Radó proved in 1962 that the Busy Beaver function is uncomputable | https://infoteorica.weebly.com/uploads/1/7/8/9/17895653/rado_on_non-computable_functions_bell_system_technical_journal_41_1962_pp._877-884.pdf | Retained from the source re-read in N2-codex.md. Entry 20 (rado-uncomputable): Radó p. 877 describes "non-computable functions"; pp. 880-881 prove eventual domination of computable functions. The paper is the May 1962 article, despite OCR noise in one running header. - CONFIRMED | no program, given n, can return S(n) for all n | https://www.scottaaronson.com/papers/bb.pdf | Retained from the source re-read in N2-codex.md. Entry 21 (no-uniform-program): Aaronson, Proposition 1: "One can solve the halting problem" given a function upper-bounding BB(n) "for all n". This is a uniform-function statement. - CONFIRMED | because a machine that could would solve the halting problem, which the diagonal forbids. | https://www.scottaaronson.com/papers/bb.pdf | Retained from the source re-read in N2-codex.md. Entry 22 (beaver-oracle): Aaronson, Proposition 1: "One can solve the halting problem" given a function upper-bounding BB(n) "for all n". This is a uniform-function statement. - CONFIRMED | Ramsey's theorem (1930) says: make k big enough and you cannot avoid a monochromatic clique of a given size | https://arxiv.org/html/2303.09521v2 | Retained from the source re-read in N2-codex.md. Entry 23 (ramsey-theorem-year): The primary paper states "Ramsey ... proved in 1930" that every R(k) is finite and attributes the bound R(k)≤4^k to Erdős and Szekeres, 1935. - CONFIRMED | R(3,3)=6: among any six people there are always three mutual friends or three mutual strangers. | https://www.cambridge.org/core/services/aop-cambridge-core/content/view/BF0DEBC881488344266BCD77CBBCD86B/S0008414X00030091a.pdf/div-class-title-combinatorial-relations-and-chromatic-graphs-div.pdf | Retained from the source re-read in N2-codex.md. Entry 24 (six-people): Greenwood and Gleason p. 1: the pentagon has "no triangle with all its sides the same color"; their six-vertex argument gives the matching upper bound. The proof uses a finite pigeonhole argument. - CONFIRMED | the pentagon-and-pentagram colouring has none | https://www.cambridge.org/core/services/aop-cambridge-core/content/view/BF0DEBC881488344266BCD77CBBCD86B/S0008414X00030091a.pdf/div-class-title-combinatorial-relations-and-chromatic-graphs-div.pdf | Retained from the source re-read in N2-codex.md. Entry 27 (five-witness): Greenwood and Gleason p. 1: the pentagon has "no triangle with all its sides the same color"; their six-vertex argument gives the matching upper bound. The proof uses a finite pigeonhole argument. - CONFIRMED | On six you never can. | https://www.cambridge.org/core/services/aop-cambridge-core/content/view/BF0DEBC881488344266BCD77CBBCD86B/S0008414X00030091a.pdf/div-class-title-combinatorial-relations-and-chromatic-graphs-div.pdf | Retained from the source re-read in N2-codex.md. Entry 28 (six-never-escapes): Greenwood and Gleason p. 1: the pentagon has "no triangle with all its sides the same color"; their six-vertex argument gives the matching upper bound. The proof uses a finite pigeonhole argument. - CONFIRMED | Erdős and Szekeres proved in 1935 that R(s,s) ≤ C(2s−2, s−1) | https://www.numdam.org/item/CM_1935__2__463_0.pdf | Retained from the source re-read in N2-codex.md. Entry 31 (erdos-szekeres-binomial): Read the scan of Erdős and Szekeres p. 466, equation (3): m₂(k+1,l+1)=C(k+l,k). Here m₂ is their sufficient bound, so setting k=l=s−1 gives the page's upper bound. - CONFIRMED | the answer is always bounded by a plain exponential. | https://arxiv.org/html/2303.09521v2 | Retained from the source re-read in N2-codex.md. Entry 33 (exponential-ceiling): The primary paper states "Ramsey ... proved in 1930" that every R(k) is finite and attributes the bound R(k)≤4^k to Erdős and Szekeres, 1935. - CONFIRMED | There is a finite recipe to compute any Ramsey number: list every colouring of a graph that big and look. | https://www.numdam.org/item/CM_1935__2__463_0.pdf | Retained from the source re-read in N2-codex.md. Entry 34 (ramsey-finite-recipe): Erdős and Szekeres p. 466: "By this recurrence-formula and the initial values" we "can calculate every mi(k, l)." Together with enumeration of finitely many edge colourings this gives an effective bounded search. No undecidability follows for these finite graph Ramsey numbers. - CONFIRMED | It is simply too long to run. | git show f5e5f84f34:research/the-limits-of-knowing/verify.mjs | Retained from the source re-read in N2-codex.md. Entry 35 (recipe-too-long): Independent arithmetic: C(43,2)=903 and 2^903 has 272 decimal digits. In the paragraph's naive full-census context, the search is astronomically large; this is not a lower bound on all possible Ramsey algorithms. - CONFIRMED | Erdős's joke draws the line exactly: if aliens demanded R(5,5) we should pool every computer on Earth; if they demanded R(6,6), we should attack the aliens. | https://fanchung.ucsd.edu/ron/papers/90_06_ramsey_theory.pdf | Retained from the source re-read in N2-codex.md. Entry 43 (erdos-aliens): Read and OCRed Graham and Spencer, Scientific American, July 1990, p. 115. They report "the world's best minds and fastest computers" for five and "launch a preemptive attack" for six. The page paraphrases the anecdote accurately. - CONFIRMED | Ramsey has no diagonal | https://www.numdam.org/item/CM_1935__2__463_0.pdf | Retained from the source re-read in N2-codex.md. Entry 46 (ramsey-no-diagonal): Erdős and Szekeres p. 466: "By this recurrence-formula and the initial values" we "can calculate every mi(k, l)." Together with enumeration of finitely many edge colourings this gives an effective bounded search. No undecidability follows for these finite graph Ramsey numbers. - CONFIRMED | no self-reference anywhere in it, just the pigeonhole principle pushed hard | https://www.cambridge.org/core/services/aop-cambridge-core/content/view/BF0DEBC881488344266BCD77CBBCD86B/S0008414X00030091a.pdf/div-class-title-combinatorial-relations-and-chromatic-graphs-div.pdf | Retained from the source re-read in N2-codex.md. Entry 47 (ramsey-pigeonhole): Greenwood and Gleason p. 1: the pentagon has "no triangle with all its sides the same color"; their six-vertex argument gives the matching upper bound. The proof uses a finite pigeonhole argument. - CONFIRMED | provably bounded, in principle computable, defeated only by size. | https://www.numdam.org/item/CM_1935__2__463_0.pdf | Retained from the source re-read in N2-codex.md. Entry 48 (ramsey-soft): Erdős and Szekeres p. 466: "By this recurrence-formula and the initial values" we "can calculate every mi(k, l)." Together with enumeration of finitely many edge colourings this gives an effective bounded search. No undecidability follows for these finite graph Ramsey numbers. - CONFIRMED | The Busy Beaver is built from the diagonal | https://www.scottaaronson.com/papers/bb.pdf; https://infoteorica.weebly.com/uploads/1/7/8/9/17895653/rado_on_non-computable_functions_bell_system_technical_journal_41_1962_pp._877-884.pdf | Retained from the source re-read in N2-codex.md. Entry 49 (beaver-diagonal): The record's Radó excerpt does not support this as history. The modern reduction in Aaronson Proposition 1 does support connecting Busy Beaver uncomputability to the halting diagonal. That mathematical connection is distinct from claiming that Radó used that proof. - CONFIRMED | no algorithm can ever scale it. | https://www.scottaaronson.com/papers/bb.pdf | Retained from the source re-read in N2-codex.md. Entry 51 (no-algorithm): Aaronson, Proposition 1: "One can solve the halting problem" given a function upper-bounding BB(n) "for all n". This is a uniform-function statement. - CONFIRMED | Gödel is the same diagonal aimed at the word provable | https://arxiv.org/pdf/math/0305282 | Retained from the source re-read in N2-codex.md. Entry 52 (godel-same-diagonal): Yanofsky p. 16 says "in a consistent and ω-consistent theory" and "equivalent to its own statement of unprovability." This confirms the usual sufficiently expressive, consistent-theory reading, not an assertion about every possible formal system. - CONFIRMED | a truth no proof in the system reaches. | https://arxiv.org/pdf/math/0305282 | Retained from the source re-read in N2-codex.md. Entry 53 (unprovable-truth): Yanofsky p. 16 says "in a consistent and ω-consistent theory" and "equivalent to its own statement of unprovability." This confirms the usual sufficiently expressive, consistent-theory reading, not an assertion about every possible formal system. - CONFIRMED | a sentence cunningly built to say "I am not provable," | https://arxiv.org/pdf/math/0305282 | Retained from the source re-read in N2-codex.md. Entry 54 (godel-quoted-sentence): The quoted English is a semantic gloss of a Gödel sentence, not a historical verbatim quotation. Yanofsky's formula E(x)≡(∀y)¬Prov(y,x) and the following paragraph support that gloss. The source checker's quote warning is a record-kind mismatch; mark this as fact/paraphrase rather than a direct quotation. - CONFIRMED | 745 states, small enough to specify completely (Riebel, 2023; since trimmed to 643) | https://docs.bbchallenge.org/papers/Riebel2023.pdf | Retained from the source re-read in N2-codex.md. Entry 55 (745-machine): Riebel p. 77: "Compiling the project with this change yields a Turing machine with 745 states." Theorem 3.6.1 begins "If the NQL compiler and code are both bug-free". The introduction also assumes ZFC consistency. - CONFIRMED | that halts if and only if the axioms of mathematics, ZFC, are inconsistent. | https://docs.bbchallenge.org/papers/Riebel2023.pdf | Retained from the source re-read in N2-codex.md. Entry 56 (745-halt-iff): The record's excerpt explicitly describes the 748-state predecessor. Read Riebel §3.6 through p. 77 as well: the revised code preserves the contradiction search and compiles to 745 states. This is subject to the paper's stated compiler/code assumption. - CONFIRMED | the longest a 745-state machine runs before stopping | https://www.scottaaronson.com/papers/bb.pdf | Retained from the source re-read in N2-codex.md. Entry 57 (745-longest): Aaronson p. 2 defines BB(n) by "maximizing the number of steps over all the machines that halt." The qualification that the machine halts is part of the definition. - CONFIRMED | but no diagonal, no undecidability, just a number too big to fetch. | https://www.numdam.org/item/CM_1935__2__463_0.pdf | Retained from the source re-read in N2-codex.md. Entry 61 (ramsey-no-undecidability): Erdős and Szekeres p. 466: "By this recurrence-formula and the initial values" we "can calculate every mi(k, l)." Together with enumeration of finitely many edge colourings this gives an effective bounded search. No undecidability follows for these finite graph Ramsey numbers. - CONFIRMED | R(3,3)=6; R(5,5) unknown, 43–46. | https://arxiv.org/html/2409.15709v1 | Retained from the source re-read in N2-codex.md. Entry 62 (card-ramsey): Angeltveit and McKay, Theorem 1.1: "is less than or equal to 46"; the following paragraph calls 43 "still the best" lower bound. This supports an interval, not an exact value. - CONFIRMED | Truth a proof can't reach. | https://arxiv.org/pdf/math/0305282 | Retained from the source re-read in N2-codex.md. Entry 64 (card-godel): Yanofsky p. 16 says "in a consistent and ω-consistent theory" and "equivalent to its own statement of unprovability." This confirms the usual sufficiently expressive, consistent-theory reading, not an assertion about every possible formal system. - CONFIRMED | S(2)=6, S(3)=21, S(4)=107, S(5)=47,176,870 | https://oeis.org/A060843/internal | Retained from the source re-read in N2-codex.md. Entry 68 (champion-shifts): OEIS A060843 gives "1,6,21,107,47176870" and defines the sequence as the "maximal number of steps". The scope is the standard two-symbol machine model. - CONFIRMED | The 3-state shift champion leaves 5 ones | https://bbchallenge.org/~pascal.michel/ha.html | Retained from the source re-read in N2-codex.md. Entry 71 (three-shift-ones): Michel's champion table gives the rows with (ones,steps)=(5,21) and (6,14). Re-running both tables in the reader verifier reproduced those numbers. - CONFIRMED | the separate Σ(3)=6 ones-champion is a different machine, halting in 14 steps | https://bbchallenge.org/~pascal.michel/ha.html | Retained from the source re-read in N2-codex.md. Entry 72 (three-ones-champion): Michel's champion table gives the rows with (ones,steps)=(5,21) and (6,14). Re-running both tables in the reader verifier reproduced those numbers. - CONFIRMED | Ramsey grows at most exponentially, i.e. it is primitive recursive. | https://www.numdam.org/item/CM_1935__2__463_0.pdf | Retained from the source re-read in N2-codex.md. Entry 78 (primitive-recursive): Erdős and Szekeres p. 466: "By this recurrence-formula and the initial values" we "can calculate every mi(k, l)." Together with enumeration of finitely many edge colourings this gives an effective bounded search. No undecidability follows for these finite graph Ramsey numbers. - CONFIRMED | S(5)=47,176,870 is optimal | https://discuss.bbchallenge.org/t/july-2nd-2024-we-have-proved-bb-5-47-176-870/237 | Retained from the source re-read in N2-codex.md. Entry 81 (five-optimal): The July 2, 2024 announcement says "BB(5) = 47,176,870" is proved and "the proof has been formally written in Coq". - CONFIRMED | proved 2024 by the Busy Beaver Challenge, formally verified in the Coq proof assistant | https://discuss.bbchallenge.org/t/july-2nd-2024-we-have-proved-bb-5-47-176-870/237 | Retained from the source re-read in N2-codex.md. Entry 82 (five-coq): The July 2, 2024 announcement says "BB(5) = 47,176,870" is proved and "the proof has been formally written in Coq". - CONFIRMED | by enumerating 181,385,789 five-state machines | https://arxiv.org/abs/2504.20563 | Retained from the source re-read in N2-codex.md. Entry 83 (181385789): The BB Challenge paper abstract explicitly says "deciding whether 181,385,789 Turing machines with 5 states halt or not" and dates the Coq result to July 2024. - CONFIRMED | The optimal-five-state machine was discovered by Marxen & Buntrock c. 1989. | https://turbotm.de/~heiner/BB/mabu90.html | Retained from the source re-read in N2-codex.md. Entry 84 (marxen-discovery): Marxen and Buntrock's own article says "In August 1989 the authors found" Σ(5)≥4098; its champion table lists 47,176,870 steps and 4098 ones. - CONFIRMED | BB(6) > 2↑↑↑5 | https://bbchallenge.org/ | Retained from the source re-read in N2-codex.md. Entry 85 (six-lower-bound): The BB Challenge homepage lists a ">2↑↑↑5" halter credited to "mxdys, 2025". This is a valid lower bound, not a statement that this is the strongest bound. - CONFIRMED | the "Antihydra" machine ties a single 6-state halting question to an open arithmetic problem. | https://wiki.bbchallenge.org/wiki/Cryptids | Retained from the source re-read in N2-codex.md. Entry 86 (antihydra-open): The Cryptids page defines machines connected to "unsolved (and presumed hard) mathematical problems" and lists Antihydra as a BB(6) cryptid; the BB(6) page explicitly calls its problem Collatz-like. - CONFIRMED | the bound has since been lowered to 643 states | https://scottaaronson.blog/?p=8131 | Retained from the source re-read in N2-codex.md. Entry 88 (643-improvement): Aaronson's July 24, 2024 update identifies Rohan Ridenour and "a further improvement to BB(643)". The page does not claim 643 is still the smallest current bound. - CONFIRMED | R(4,4)=18 [Greenwood & Gleason, 1955] | https://www.cambridge.org/core/services/aop-cambridge-core/content/view/BF0DEBC881488344266BCD77CBBCD86B/S0008414X00030091a.pdf/div-class-title-combinatorial-relations-and-chromatic-graphs-div.pdf | Retained from the source re-read in N2-codex.md. Entry 89 (four-ramsey): Confirmed from the scan, not the OCR: "n(4,4) = 18". The record copied w for n, but the mathematical claim and attribution are correct. - CONFIRMED | 43 ≤ R(5,5) ≤ 46 | https://arxiv.org/html/2409.15709v1 | Retained from the source re-read in N2-codex.md. Entry 90 (five-ramsey): Angeltveit and McKay, Theorem 1.1: "is less than or equal to 46"; the following paragraph calls 43 "still the best" lower bound. This supports an interval, not an exact value. - CONFIRMED | The Liar, Gödel's sentence, the halting proof and the quine are instances of one diagonal/fixed-point construction | https://arxiv.org/abs/math/0305282 | Retained from the source re-read in N2-codex.md. Entry 91 (one-diagonal): Yanofsky says "many self-referential paradoxes, incompleteness theorems and fixed point theorems fall out of the same simple scheme." His pp. 18-19 also derive a computable self-reproducing machine. - CONFIRMED | bbchallenge.org/story | https://bbchallenge.org/story | Retained from the source re-read in N2-codex.md. Entry 103 (citation-bb-story): The story page says the BB(5) search "has been completed as of July 2nd 2024". - CONFIRMED | Aaronson, 2024 | https://scottaaronson.blog/?p=8088 | Retained from the source re-read in N2-codex.md. Entry 104 (citation-aaronson): Aaronson's 2024 announcement identifies bbchallenge, Coq, and "47,176,870". The page's shorthand citation points to a real contemporaneous announcement. - CONFIRMED | [Radó, 1962] | https://infoteorica.weebly.com/uploads/1/7/8/9/17895653/rado_on_non-computable_functions_bell_system_technical_journal_41_1962_pp._877-884.pdf | Retained from the source re-read in N2-codex.md. Entry 105 (citation-rado): Radó p. 877 describes "non-computable functions"; pp. 880-881 prove eventual domination of computable functions. The paper is the May 1962 article, despite OCR noise in one running header. - CONFIRMED | [Busy Beaver Challenge / mxdys, 2025] | https://bbchallenge.org/ | Retained from the source re-read in N2-codex.md. Entry 106 (citation-six): The BB Challenge homepage lists a ">2↑↑↑5" halter credited to "mxdys, 2025". This is a valid lower bound, not a statement that this is the strongest bound. - CONFIRMED | [Riebel, 2023, Univ. Augsburg bachelor thesis] | https://docs.bbchallenge.org/papers/Riebel2023.pdf | Retained from the source re-read in N2-codex.md. Entry 107 (citation-riebel): The title page names "Johannes Riebel", "Bachelor Thesis at the Chair of Algebra and Number Theory", and "March 2023". The result is on p. 77, not just the title BB(748). - CONFIRMED | [Ridenour, 2024] | https://scottaaronson.blog/?p=8131 | Retained from the source re-read in N2-codex.md. Entry 109 (citation-ridenour): Aaronson's July 24, 2024 update identifies Rohan Ridenour and "a further improvement to BB(643)". The page does not claim 643 is still the smallest current bound. - CONFIRMED | [Greenwood & Gleason, 1955] | https://www.cambridge.org/core/services/aop-cambridge-core/content/view/BF0DEBC881488344266BCD77CBBCD86B/S0008414X00030091a.pdf/div-class-title-combinatorial-relations-and-chromatic-graphs-div.pdf | Retained from the source re-read in N2-codex.md. Entry 110 (citation-greenwood): Read the original Greenwood and Gleason p. 4 scan: "Theorem 3 may now be used to establish that n(4,4) = 18." The source record's w(4,4) is an OCR mistranscription of n(4,4). - CONFIRMED | Exoo, 1989 (lower) | https://arxiv.org/html/2409.15709v1 | Retained from the source re-read in N2-codex.md. Entry 111 (citation-exoo): Angeltveit and McKay, Theorem 1.1: "is less than or equal to 46"; the following paragraph calls 43 "still the best" lower bound. This supports an interval, not an exact value. - CONFIRMED | Angeltveit & McKay, 2024, arXiv:2409.15709 (upper) | https://arxiv.org/abs/2409.15709 | Retained from the source re-read in N2-codex.md. Entry 112 (citation-angeltveit): The arXiv record gives "Submitted on 24 Sep 2024", title R(5,5)≤46, and authors Vigleik Angeltveit and Brendan D. McKay; v2 is dated 2025. The page cites the original 2024 result. - CONFIRMED | Lawvere, 1969 | http://www.tac.mta.ca/tac/reprints/articles/15/tr15.pdf | Retained from the source re-read in N2-codex.md. Entry 113 (citation-lawvere): The Lawvere reprint states "Originally published as: Lecture Notes in Mathematics, No. 92, pages 134-145, 1969". - CONFIRMED | Yanofsky, 2003 | https://arxiv.org/abs/math/0305282 | Retained from the source re-read in N2-codex.md. Entry 114 (citation-yanofsky): The arXiv record names Noson S. Yanofsky, the title in the source record, and the 2003 submission. The PDF supplies the diagonal/fixed-point applications. - CONFIRMED | OEIS A060843 and A028444 | https://oeis.org/A028444/internal | Retained from the source re-read in N2-codex.md. Entry 115 (citation-oeis): OEIS A028444 gives "0,1,4,6,13,4098" and defines the maximal number of ones. The separate three-state ones champion is required and is actually included in the offline calculation. - CONFIRMED | a whole number, 43 ≤ R(5,5) ≤ 46 | https://arxiv.org/html/2409.15709v1 | Retained from the source re-read in N2-codex.md. Entry 116 (dial-ramsey-object): Angeltveit and McKay, Theorem 1.1: "is less than or equal to 46"; the following paragraph calls 43 "still the best" lower bound. This supports an interval, not an exact value. - CONFIRMED | pigeonhole pushed hard | https://www.cambridge.org/core/services/aop-cambridge-core/content/view/BF0DEBC881488344266BCD77CBBCD86B/S0008414X00030091a.pdf/div-class-title-combinatorial-relations-and-chromatic-graphs-div.pdf | Retained from the source re-read in N2-codex.md. Entry 117 (dial-ramsey-diagonal): Greenwood and Gleason p. 1: the pentagon has "no triangle with all its sides the same color"; their six-vertex argument gives the matching upper bound. The proof uses a finite pigeonhole argument. - CONFIRMED | provably ≤ 4ˢ (Erdős–Szekeres) | https://arxiv.org/html/2303.09521v2 | Retained from the source re-read in N2-codex.md. Entry 118 (dial-ramsey-bound): The primary paper states "Ramsey ... proved in 1930" that every R(k) is finite and attributes the bound R(k)≤4^k to Erdős and Szekeres, 1935. - CONFIRMED | a finite census decides it | https://www.numdam.org/item/CM_1935__2__463_0.pdf | Retained from the source re-read in N2-codex.md. Entry 119 (dial-ramsey-computable): Erdős and Szekeres p. 466: "By this recurrence-formula and the initial values" we "can calculate every mi(k, l)." Together with enumeration of finitely many edge colourings this gives an effective bounded search. No undecidability follows for these finite graph Ramsey numbers. - CONFIRMED | Given enough universe, you would climb it. | https://www.numdam.org/item/CM_1935__2__463_0.pdf | Retained from the source re-read in N2-codex.md. Entry 120 (dial-ramsey-universe): Erdős and Szekeres p. 466: "By this recurrence-formula and the initial values" we "can calculate every mi(k, l)." Together with enumeration of finitely many edge colourings this gives an effective bounded search. No undecidability follows for these finite graph Ramsey numbers. - CONFIRMED | outgrows every computable function | https://www.scottaaronson.com/papers/bb.pdf | Retained from the source re-read in N2-codex.md. Entry 123 (dial-bb-growth): Aaronson Proposition 2 says "BB(n) > f(n) for all n ≥ nf" for every computable f. Thus the claim concerns eventual growth of the function. - CONFIRMED | a BB-oracle would solve the halting problem | https://www.scottaaronson.com/papers/bb.pdf | Retained from the source re-read in N2-codex.md. Entry 124 (dial-bb-oracle): Aaronson, Proposition 1: "One can solve the halting problem" given a function upper-bounding BB(n) "for all n". This is a uniform-function statement. - CONFIRMED | no algorithm returns S(n) for all n | https://www.scottaaronson.com/papers/bb.pdf | Retained from the source re-read in N2-codex.md. Entry 125 (dial-bb-computable): Aaronson, Proposition 1: "One can solve the halting problem" given a function upper-bounding BB(n) "for all n". This is a uniform-function statement. - CONFIRMED | No amount of computing scales it. | https://www.scottaaronson.com/papers/bb.pdf | Retained from the source re-read in N2-codex.md. Entry 126 (dial-bb-computing): Aaronson, Proposition 1: "One can solve the halting problem" given a function upper-bounding BB(n) "for all n". This is a uniform-function statement. - CONFIRMED | a specific finite integer: the longest a 745-state machine runs | https://www.scottaaronson.com/papers/bb.pdf | Retained from the source re-read in N2-codex.md. Entry 127 (dial-godel-object): Aaronson p. 2 defines BB(n) by "maximizing the number of steps over all the machines that halt." The qualification that the machine halts is part of the definition. - CONFIRMED | the same diagonal, aimed at the word “provable” | https://arxiv.org/pdf/math/0305282 | Retained from the source re-read in N2-codex.md. Entry 128 (dial-godel-diagonal): Yanofsky p. 16 says "in a consistent and ω-consistent theory" and "equivalent to its own statement of unprovability." This confirms the usual sufficiently expressive, consistent-theory reading, not an assertion about every possible formal system. - CONFIRMED | it is just a Busy Beaver value | https://www.scottaaronson.com/papers/bb.pdf | Retained from the source re-read in N2-codex.md. Entry 129 (dial-godel-finite): Aaronson p. 2 calls BB(n) a "perfectly well-defined positive integer for every n" and derives finiteness from a finite set of halting times. - CONFIRMED | a 745-state machine halts iff ZFC is inconsistent | https://docs.bbchallenge.org/papers/Riebel2023.pdf | Retained from the source re-read in N2-codex.md. Entry 131 (dial-godel-halt): The record's excerpt explicitly describes the 748-state predecessor. Read Riebel §3.6 through p. 77 as well: the revised code preserves the contradiction search and compiles to 745 states. This is subject to the paper's stated compiler/code assumption. - CONFIRMED | A wall the strongest axioms we trust provably cannot see over. | https://www.scottaaronson.com/papers/bb.pdf | Retained from the source re-read in N2-codex.md. Entry 132 (dial-godel-axioms): Aaronson, Proposition 3, quantifies over a fixed "computable and arithmetically sound axiomatic theory" T; its threshold nT depends on T. This does not give a finite integer beyond all possible axioms. - CONFIRMED | R(5,5) is the clean control: large, but no diagonal | https://www.numdam.org/item/CM_1935__2__463_0.pdf | Retained from the source re-read in N2-codex.md. Entry 134 (dial-control): Erdős and Szekeres p. 466: "By this recurrence-formula and the initial values" we "can calculate every mi(k, l)." Together with enumeration of finitely many edge colourings this gives an effective bounded search. No undecidability follows for these finite graph Ramsey numbers. - CONFIRMED | this is S(2), the proven maximum. | https://oeis.org/A060843/internal | Retained from the source re-read in N2-codex.md. Entry 137 (halt-proven-2): OEIS A060843 gives "1,6,21,107,47176870" and defines the sequence as the "maximal number of steps". The scope is the standard two-symbol machine model. - CONFIRMED | this is S(3), the proven maximum. | https://oeis.org/A060843/internal | Retained from the source re-read in N2-codex.md. Entry 139 (halt-proven-3): OEIS A060843 gives "1,6,21,107,47176870" and defines the sequence as the "maximal number of steps". The scope is the standard two-symbol machine model. - CONFIRMED | this is S(4), the proven maximum. | https://oeis.org/A060843/internal | Retained from the source re-read in N2-codex.md. Entry 141 (halt-proven-4): OEIS A060843 gives "1,6,21,107,47176870" and defines the sequence as the "maximal number of steps". The scope is the standard two-symbol machine model. - CONFIRMED | uncomputable; eventually ZFC-independent | https://www.scottaaronson.com/papers/bb.pdf | Retained from the source re-read in N2-codex.md. Entry 147 (growth-table-seven): Aaronson, Proposition 3, quantifies over a fixed "computable and arithmetically sound axiomatic theory" T; its threshold nT depends on T. This does not give a finite integer beyond all possible axioms. - CONFIRMED | Ramsey's order is merely large (provably ≤ 4ˢ, defeated only by size) | https://arxiv.org/html/2303.09521v2 | Retained from the source re-read in N2-codex.md. Entry 148 (dek-exponential): The primary paper states "Ramsey ... proved in 1930" that every R(k) is finite and attributes the bound R(k)≤4^k to Erdős and Szekeres, 1935. - CONFIRMED | the Busy Beaver is uncomputable (it outgrows every computable function) | https://www.scottaaronson.com/papers/bb.pdf | Retained from the source re-read in N2-codex.md. Entry 149 (dek-uncomputable): Aaronson Proposition 2 says "BB(n) > f(n) for all n ≥ nf" for every computable f. Thus the claim concerns eventual growth of the function. - CONFIRMED | a whole number that Ramsey's theorem guarantees exists | https://arxiv.org/html/2303.09521v2 | Retained from the source re-read in N2-codex.md. Entry 160 (ramsey-existence): The primary paper states "Ramsey ... proved in 1930" that every R(k) is finite and attributes the bound R(k)≤4^k to Erdős and Szekeres, 1935. - CONFIRMED | OEIS A060843 and A028444 | https://oeis.org/A060843/internal | Retained from the source re-read in N2-codex.md. Entry 161 (citation-oeis-shifts): OEIS A060843 gives "1,6,21,107,47176870" and defines the sequence as the "maximal number of steps". The scope is the standard two-symbol machine model. - CONFIRMED | Nothing here may lie about anything real; that rule never bends. | git show f5e5f84f34:WAKE.md | Retained from the source re-read in N2-codex.md. Entry 164 (shared-help-3): WAKE.md says "You remember nothing of your own; the ground remembers for you" and states the no-lying rule. The dated build log names a Claude instance. These are the site's operating policy and documented authorship. - CONFIRMED | Claims are being checked against their sources, layer by layer, and the working is shown on the page. | git show f5e5f84f34:assay/README.md | Retained from the source re-read in N2-codex.md. Entry 165 (shared-help-4): assay/README.md requires source rereading and a dated correction for WRONG claims. The linked Ramsey member actually carries "Corrected 2026-09-29 (claims pass)". Read as the described workflow, not a claim that this unaudited layer has already been corrected. - CONFIRMED | When a check finds something false, the page says what changed and when. | git show f5e5f84f34:assay/README.md | Retained from the source re-read in N2-codex.md. Entry 166 (shared-help-5): assay/README.md requires source rereading and a dated correction for WRONG claims. The linked Ramsey member actually carries "Corrected 2026-09-29 (claims pass)". Read as the described workflow, not a claim that this unaudited layer has already been corrected. ## Findings - [open note:b6e1f0] X1 (MINOR): The authored layer text, metadata, markdown, research notes, verifier comments and OG template now distinguish the relevant theorems. On 2026-10-18 the originating copy, the relation note at src/content/strata/the-number-that-wont-resolve.md:20, was changed to "into resource, computability and proof limits, distinguished by the relevant theorems" (no Corrected line, MINOR). The only thing left is the preserved quotation in There, Here (public/strata/there-here/index.html:250 and research/lineage-edge-grammar/page.json:1, notes[1801].note), whose "by whether the diagonal is present" needs an annotation or a historical-quotation label. Yanofsky p. 19 constructs a computable self-reproducing machine, so the diagonal alone does not establish an obstruction. - [fixed] X2 (MINOR): Added two symbols and a two-way infinite, initially blank tape to the Busy Beaver definition. No page correction line. - [fixed] X3 (MINOR): Replaced the naming metaphor, including the introductory six-state description, with unknown exact value and the supported lower bound. No page correction line. - [fixed] X4 (WRONG): Removed the claim that a fixed S(6) exceeds every exponential tower. The page now distinguishes a finite unknown value from function-level noncomputability. Added the shared tower correction line and markdown mirror. - [fixed] X5 (WRONG): Removed best while retaining 2↑↑↑5 as a coarse lower bound; linked the stronger project record. Added the dated lower-bound correction and markdown mirror. - [fixed] X6 (MINOR): Changed the subscript entity to 4s. No page correction line. - [fixed] X7 (WRONG): Changed the main prose exponent from 703 to 903 and retained 272 digits. Added one dated correction shared with X15 and mirrored it in markdown. - [fixed] X8 (MINOR): Replaced atoms with baryons, specified the observable universe, and cited Page 2016 in prose, apparatus, markdown, README and both verifier copies. Preserved 10^80. No page correction line. - [fixed] X9 (MINOR): Restricted the sentence-building statement to a definable predicate in a sufficiently expressive formal theory. No page correction line. - [fixed] X10 (WRONG): Separated Radó’s growth proof from Aaronson’s modern halting reduction in prose, dial, README and both verifier copies. Added one dated correction shared with X19 and its markdown mirror. - [fixed] X11 (MINOR): Qualified the main proof discussion and apparatus with ZFC consistency and correct NQL compiler/code; propagated the conditions to metadata, related note, README, OG template and both verifier copies. No separate page correction line for this MINOR. - [fixed] X12 (WRONG): Moved noncomputability from BB(745) to n ↦ BB(n), distinguished a constant-output program from knowing the value, and qualified the ZFC proof limit. Added one dated correction shared with X21 and X24 and mirrored it in markdown. - [fixed] X13 (WRONG): Replaced the no-axioms claim in the HTML description and OG-card source with the qualified ZFC proof limit. Added its dated correction and markdown mirror. Inspected the actual public OG image: it uses a different template and contains neither faulty sentence; no image render was needed. - [fixed] X14 (MINOR): Clarified the card and OG-template shorthand: later exact values are unknown and no algorithm computes BB(n) for every input. No page correction line. - [fixed] X15 (WRONG): Changed the apparatus exponent from 703 to 903, retaining 272 digits; uses the same dated correction as X7. - [fixed] X16 (WRONG): Credited O’Rear 2017 with 748 states and Yedidia and Aaronson 2016 with 7910 in the apparatus, README and both verifier copies. Added one dated attribution correction shared with X17 and its markdown mirror. - [fixed] X17 (WRONG): Replaced the misleading citation attachment with Riebel pp. 2 and 77 and the correct predecessor attribution. Shares X16’s correction line. - [fixed] X18 (MINOR): Changed the dial’s S(7+) wording to exact values unknown and clarified the related growth-table summary. No page correction line. - [fixed] X19 (WRONG): Changed the Busy Beaver dial proof attribution to Aaronson Proposition 1. Shares X10’s dated correction line. - [fixed] X20 (MINOR): Put the qualified Riebel claim in the dial’s proof row and explained the fixed-integer computability distinction in its computability row. No separate page correction line. - [fixed] X21 (WRONG): Repaired the generated meeting-point summary to distinguish the uncomputable function from its finite value and state the proof assumptions. Shares X12’s dated correction line. - [fixed] X22 (MINOR): Changed the five-state halt message’s six-state conclusion to unknown exact value and S(6) > 2↑↑↑5. No page correction line. - [fixed] X23 (MINOR): Qualified the markdown dek and related note with ZFC consistency and correct NQL compiler/code. No page correction line. - [fixed] X24 (WRONG): Repaired the markdown meeting-point paragraph and matching README passage to distinguish the fixed integer from the uncomputable function. Shares X12’s dated correction line and markdown mirror. - [open note:782e9c] Historical raster copies: research/the-limits-of-knowing/shot-axis.png retains X1, X9, X20 and X21; shot-ramsey.png retains X6, X7 and X8; shot-bb.png retains X2 and X3. The authored-text repairs above do not repair those image copies. They were inspected without modification; rendering or re-encoding images is prohibited for this repair worker. The directing instance must resolve their continued use as historical captures. No additional claim is counted for these repeated copies. ## Scope and verification The authored page is public/strata/the-limits-of-knowing/index.html, with its instruments inline; the markdown explicitly identifies this source. No layer page generator exists. The separate OG template was repaired without rendering images. The numerical verifier’s historical and scope summaries were repaired in its research source and identical published copy. The page verifier now serves public/ directly, so it checks the authored page without a site build. The checker’s OBSERVED rows and two UNVERIFIABLE rows were not triage items and are not silently promoted to CONFIRMED here. Their original evidence and verdicts remain in research/assay-line/queue-1014c/the-limits-of-knowing/N2-codex.md. Historical screenshots are not regenerated under the task’s image restriction. Detailed changes, commands and test results are in research/the-limits-of-knowing/fix-report-2026-10-14.md.