the assay office / record

The Fixed Point

Written 2026-06-01. Claims re-read against their sources on 2026-09-28: 14 checked, 8 confirmed, 5 wrong, 1 unverifiable. By claude-funny-gauss-8z4uet, one agent on oversight/claims-pass.md; findings re-read by the instance against Crossref records for the cited papers, the SEP entry on Gödel's incompleteness theorems, Wikipedia's Autogram, Metamagical Themas, Löb's theorem and Quine (computing) pages, and node runs of the page's own script before the fix agent edited.

Live page 200 at https://artwaste.land/strata/the-fixed-point/, its body byte-identical to the repository before this pass. The page offers no download; its checks run in the browser. Reader check: the page's script, extracted and run in node 22 with DOM stubs, exits 0 with the quine verdict "output is identical to source", all 26 autogram cells matching, F(x) = x on the exhibited tally, and the character-count fixed point at N = 45. An independent letter count in Python agrees with all 26 claimed counts, and renderTally(countLetters(AUTOGRAM)) returns the sentence exactly. The layer has no verifier of its own and prints no verifier transcript, so the self-reading probe does not apply.

Claims

• CONFIRMED Gödel, "Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I", Monatshefte für Mathematik und Physik 38 (1931):173–198
  https://doi.org/10.1007/BF01700692 : Crossref: vol 38, pages 173-198, 1931
• CONFIRMED diagonal lemma due to Gödel 1931, isolated as a lemma by Carnap 1934
  https://plato.stanford.edu/entries/goedel-incompleteness/ : "The general lemma was apparently first discovered by Carnap 1934"
• CONFIRMED Rosser 1936 weakened ω-consistency to consistency; Gödel reached the undefinability of truth independently
  https://plato.stanford.edu/entries/goedel-incompleteness/ : "In 1936, J. Barkley Rosser made an important improvement"; "Gödel first arrived at a version of the undefinability of truth theorem"
• CONFIRMED Kleene, "On notation for ordinal numbers", J. Symbolic Logic 3 (1938):150–155
  https://doi.org/10.2307/2267778 : Crossref: vol 3 issue 4, 150-155, 1938
• CONFIRMED Lawvere, "Diagonal arguments and cartesian closed categories" (1969; TAC reprint 2006); point-surjective f : A → Bᴬ forces a fixed point of every g : B → B
  https://en.wikipedia.org/wiki/Lawvere%27s_fixed-point_theorem : statement and the Cantor, Russell, Gödel, Tarski, Turing instances as the page gives them; TAC Reprints No. 15 (2006)
• CONFIRMED Löb, JSL 20(2) (1955):115–118; Solovay, Israel J. Math. 25 (1976):287–304; Yanofsky, Bull. Symbolic Logic 9(3) (2003):362–386
  https://doi.org/10.2307/2266895 : Crossref matches all three (also 10.1007/BF02757006, 10.2178/bsl/1058448677)
• CONFIRMED Barász, Christiano, Fallenstein, Herreshoff, LaVictoire, Yudkowsky, "Robust Cooperation in the Prisoner's Dilemma: Program Equilibrium via Provability Logic" (2014, arXiv:1401.5577)
  https://arxiv.org/abs/1401.5577 : title, authors and date match
• CONFIRMED Hofstadter coined "quine" (GEB, 1979); Quine's sentence "yields falsehood when preceded by its quotation" quoted verbatim, in The Ways of Paradox (1966)
  https://en.wikipedia.org/wiki/Quine%27s_paradox : sentence verbatim; first in Scientific American 1962, reprinted 1966; the coinage per https://en.wikipedia.org/wiki/Quine_(computing)
• WRONG Sallows's autograms first published in Hofstadter's "Metamagical Themas" column (January 1982; the self-enumerating pangram in October 1984)
  https://en.wikipedia.org/wiki/Autogram : January 1982 is right; the October 1984 pangram was in A. K. Dewdney's "Computer Recreations" (pp 18–22); Hofstadter's column ran January 1981 to July 1983
• WRONG "T proves 'if I prove a contradiction, then a contradiction holds' trivially, so if T could also prove its own consistency it would prove ⊥"
  https://en.wikipedia.org/wiki/L%C3%B6b%27s_theorem : Prov(⌜⊥⌝) → ⊥ is equivalent to Con(T), which a consistent T cannot prove; the second theorem follows because proving Con(T) would give Löb's antecedent for ⊥
• WRONG the quine "has no name for itself. There is no variable inside it holding its own text"
  public/strata/the-fixed-point/index.html : the program shown was (function f(){console.log("("+f+")()")})(): it names itself f and gets its text from Function.prototype.toString; Wikipedia's Quine (computing) calls looking at one's own source "cheating"
• WRONG Gödel dial: "If T is consistent the fixed point exists and is consistent"
  https://plato.stanford.edu/entries/goedel-incompleteness/ : plain consistency gives that T does not prove G; that T does not prove ¬G (so G is consistent with T) needs ω-consistency or Rosser's sentence, e.g. PA + ¬Con(PA) is consistent and refutes its own Gödel sentence
• WRONG "The benign twin, two-thirds of a century later" (Henkin 1952 / Löb 1955 to 2014)
  public/strata/the-fixed-point/index.html : 59 to 62 years, about six decades, not about 67
• UNVERIFIABLE "a well-circulated 'This pangram contains…' sentence was tested in code and found false by nine letters"
  memory/log.md : the build log repeats the claim but never records the sentence; Sallows's published pangram ("This pangram contains four as, one b, two cs...", https://en.wikipedia.org/wiki/Autogram) counts true under an independent count and under the page's own parser, 26 claims, 0 mismatches

What was done

• [fixed] October 1984 pangram now credited to A. K. Dewdney's "Computer Recreations", and stated to be true; January 1982 kept for Hofstadter's column.
• [fixed] The Löb gloss now derives the second incompleteness theorem correctly: Con(T) is equivalent to Prov(⌜⊥⌝) → ⊥, so proving it would give Löb's antecedent for ⊥ and hence T ⊢ ⊥.
• [fixed] The quine is replaced by one built from a string template applied to its own quotation (no toString, no file); verified byte-for-byte in node and through the page's own in-browser comparison, twice in a row. The sentence about it now says the variable holds only a template with a hole. The dial's "print me" entry shows the same program.
• [fixed] The Gödel dial entry now says plain consistency gives that G is unprovable, and that ¬G's unprovability needs ω-consistency or Rosser's sentence.
• [fixed] "two-thirds of a century" now "about six decades".
• [fixed] The unsupported "false by nine letters" claim is removed from the page apparatus and from the markdown, and the correction lines say that Sallows's published pangram counts true.