Publication checks — updated 10 September 2026
This revision covers eight FPRD publications: the new residual-access article, six earlier research articles, and the program overview. The textbook is deferred. Each revised article now begins with a concrete problem, an example, and an explanation of how the argument develops. Earlier statements and proofs remain available in the reading editions, with their existing reference and theorem anchors.
These checks were performed with AI assistance. They record particular inspections and calculations; they do not certify every theorem in the collection. The written arguments remain the basis for the mathematical claims.
Contents
Corrections
- Residual access: corrected an opening that could confuse the size of one residual with the number of distinct residuals across prefixes. Expanded the distinction between matching counts and matching a complete transition system. Added background on Ford and Ko and a worked terminal-marker example. Kim–Park’s methodological contribution remains explicit.
- Persistent stacks: corrected the Loff–Moreira–Reis journal pagination to 111 (2020), 1–21, consistent with the journal record. The author-version reference to Theorem 16 remains correct.
- Metric groups: completed the Bargetz–Bartoš–Kubiś–Luggin locator as RACSAM 118, article 118 (2024). Removed a statement that external specialist review was ongoing; this revision supplies no evidence of such a review.
- Unary coherence: identified the earlier separate checking process as an AI-assisted audit, avoiding the suggestion of a human specialist’s endorsement. Removed a stray bibliography counter.
- GapCVP: removed an empty certificate-file sentence left by the HTML import. Actual reproduction-package citations remain, with their historical commit identifiers.
- Added source links to previously unlinked bibliographies. References to current FPRD reading editions now link to those editions. Pinned historical evidence links retain their original targets.
Mathematical scope
| Publication | Arguments inspected or reconstructed in this pass | Limits |
|---|---|---|
| Remembering information and reaching it | Checked the expanded examples against the existing grammar, rank, terminal-marker and direct-simulation arguments. The companion combined audit records the earlier full reconstruction and exact scope of the conditional profile theorem. | Ko’s full communication proof is an external premise. Equal cardinalities and probability multisets do not assert equality of named residuals or update maps. |
| Program overview | Checked the finite-horizon interpretation, bracket example, and distinction between a quotient at one cut and one uniform recognition process. | This is not a fresh proof audit of every research packet cited by the overview. |
| Persistent stacks | Reconstructed simultaneous stack updates, immutable tails, empty-stack handling, two-stack tape zippers, and the bounded-radius simulation. | Classical machine-model simulations and the historical Lean run were not rerun or re-proved in full. Strict per-symbol timing remains essential. |
| GapCVP retuning | Reconstructed exponent elimination leading to the 1/28 frontier for the retained architecture; checked the 1/30 tuple and finite inequalities with exact arithmetic. Compared source interfaces with OpenAI’s -Hardness of the Euclidean Closest Vector Problem. | The frontier concerns this reduction architecture. Historical Lean certificates and repository artifacts were not rerun. |
| Metric-group regularity | Inspected the Boolean-group reduction, displacement and involution arguments, interval/category steps, nested digit readout, and boundary cancellation. | Finite rational checks do not establish the limiting construction. Later bounded-variation arguments were not reconstructed line by line in this pass. |
| Direct palindrome scaffold | Reconstructed occurrence updates, receipt recurrences, the fixed-layout source program, the simultaneous-record compiler, and the whole-client symbolic-normalization theorem. The exact external/internal/reset observation schedule was checked separately from the max-plus resource certificate. | The restored theorem is scoped to an abstract immutable source-record model. The local old-address ceilings 55 and 766 remain manual, the reviews share model dependencies, and there is no external specialist review, OCaml–Rocq refinement, or literal runtime-heap theorem. |
| Causal scaffold algebra | Inspected observational equivalence, generated residual quotients, guarded folding, causal support, and carrier geometry. Checked why an unreachable node can still be needed to replay a construction. Rechecked its direct-palindrome example against the companion’s later implementation and normalization work. | This does not certify every higher-dimensional coherence case or supply a uniform online normalization algorithm. Its generic compiler remains logically separate from the companion’s application theorem. |
| Unary coherence | Inspected fixed-root carrier coordinates, order-ideal rectangles, and the role of guarded local relations in the inductive argument. | Finite carrier-distance checks do not prove complete coherence. Old self-loop and context guards remain part of the theorem. |
The 10 September direct-palindrome audit identified one substantive open bridge and one underived numerical inventory. Later passes implemented the narrowed four-operation interface, proved its source semantics, supplied fixed-layout allocation and address certificates, and proved a whole-client normalization theorem that closes the qualitative source-to-plan bridge. This restores the direct theorem in its abstract model without promoting the manual local resource ceilings or shared-model reviews into external validation. The other rows retain the narrower results of the 5 September pass; this document is not a verification of every result in every publication.
Source checks
The citation pass compared author, title, version and publication details with primary papers, author pages and publisher records where accessible. A working link establishes access to a source, not the truth of its theorem. The citation inventory records individual entries and remaining access limitations.
For residual access, substantive interface checks concern Ford’s question and PEG operations, Ko’s Theorem 1.1 and coordinate-update accounting, Loff–Moreira–Reis’s Theorem 16, and Horváth–Nagy’s linear pumping lemma. Kim–Park remains the methodological source. Reproving the simulation does not remove their influence, and using Ko does not give an intrinsic lower-bound proof.
OpenAI’s -Hardness of the Euclidean Closest Vector Problem occupies printed pages 183–218, which differ from PDF viewer page numbers. Metric-article checks included Bargetz et al., Theorem 4.9, Chatyrko’s Baire-transfer statement, and Balcerzak–Holá–Holý’s equi-Lebesgue implication. The scaffold geometry was compared with the Ardila–Owen–Sullivant order-ideal/CAT(0) correspondence.
Two source details remain unresolved. The publisher’s archive lists the MT22 issue associated with the citation to A. Klene, but the article’s text and exact pages 30–37 could not be retrieved for confirmation. Pin’s author-hosted notes were inaccessible, so the historical 22 August retrieval and its exact snapshot have not been reverified. These are retained references, not newly verified source text. Dated GitLab reproduction packages also remain historical evidence: no GitLab access or artifact rerun was performed during this revision.
Kaplan–Tarjan’s final JACM paper was read through its catenable-steque theorem using the author-hosted journal PDF. The source establishes worst-case constant-cost operations on regular steques in its strict purely functional model. It does not state the stronger FPRD finite-record, allocation, old-address, or element-opacity bridge. Viennot et al. v3 separately explain that the 1999 paper gave prose algorithms without code and did not explicitly prove functional correctness or the constant-time claims. Their later OCaml and Rocq artifacts establish different properties and have no proved correspondence to each other.
Reproducible finite checks
Run check_publication_examples.py with Python 3. The recorded output gives the bounds and counts:
| Check | Cases |
|---|---|
| Palindrome occurrence updates | 16,382 |
| Palindrome receipt recurrences | 254 |
| Palindrome shadow cases | 5,446 |
| Persistent stack steps | 114,688 |
| Metric rational subadditivity pairs | 12,288 |
| Metric boundary cancellations | 8,192 |
| Carrier graph-distance pairs | 4,707 |
| Exact GapCVP parameter checks | 10 |
| Residual terminal-marker table rows | 8 |
All passed. The script uses finite words, rational arithmetic and small graphs to test these examples and identities. It is corroboration, not a replacement for unbounded arguments. The residual article’s combined audit and reproduction packet preserve its earlier grammar and conditioned-profile checks. The direct-palindrome normalization package records the theorem, three distinct shared-model reviews, and a manifest checker; that checker validates the declared finite observation schedule and arithmetic, not the manual local source bounds.
Editions
The residual-access Markdown, HTML, TeX and PDF are regenerated together. For the seven earlier publications, expanded web editions and downloadable HTML sources are current. The direct-palindrome and causal-algebra downloads now use corrected Draft 4 folios before preserved historical bodies; other buttons label retained PDFs and LaTeX sources as earlier editions. Archival content has not been silently replaced. The textbook’s reading edition is unchanged.