# Provenance and Verification Supplement for *Ramsey’s Theorem for Pairs in Pincus’s Model XI*

**Frank Gilson**

**Version 1.2, 21 October 2026**

## 1. Purpose and provenance

This supplement records the provenance and principal verification steps behind the accompanying note *Ramsey’s Theorem for Pairs in Pincus’s Model XI*. It is not part of the proof. Its purpose is to make visible the role of AI-assisted research, the checks performed on the mathematical argument and its sources, and the historical search concerning Ramsey’s theorem in Howard–Rubin model \(N48\).

The note grew out of a longer investigation of weak choice principles and transfer from permutation models to ZF. An earlier manuscript contained the \(N48\) result together with several other results. The present note was rewritten from scratch around the single model-specific theorem and its immediate ZF consistency consequence.

OpenAI’s ChatGPT was used extensively for mathematical exploration, proof development, literature searching, source verification, and drafting. Anthropic’s Claude was used as an adversarial reviewer of proofs, citations, and exposition. Claude Opus 5.5 was used in the final review cycle. Earlier Claude reviews are not assigned a model version because the version was not independently recorded. Meta AI, accessed through the free tier at meta.ai with no model version displayed, was used in reviewing the predecessor manuscript and portions of the \(N48\) argument and its sources. Apodex, accessed through apodex.ai in Deep Solve mode, was also used to audit the predecessor manuscript and source claims.

These machine reviews are not presented as independent human peer review.

## 2. Relation to the proof in the note

The proof adapts the stabilizer strategy used by Tachtsis for Mostowski’s linearly ordered permutation model. Pincus’s model has additional color predicates. The adaptation therefore moves one point of a finite support only within its color class and within a gap determined by the remaining fixed support. Homogeneity of the ordered colored structure then produces the orbit on which the stabilizer acts transitively on unordered pairs.

The complete argument is given in §2 of the note and is not repeated here. During its development, particular attention was given to the behavior of least supports under automorphisms, distinctness of the resulting orbit elements, pair transitivity, the treatment of the fixed-point case, and the internal status of the sets and relations used in the proof.

## 3. Source verification

The locations listed below were checked against the source texts during the AI-assisted source audits.

| Source | Location checked | Role in the note |
|---|---|---|
| Pincus, *The dense linear ordering principle* (1997) | Proposition 2.1, p. 449 | Supplies the countable homogeneous ordered colored structure, extension of finite ordered-colored partial isomorphisms, density of the order, and occurrence of each color between distinct points. |
| Pincus (1997) | Lemma 2.2 and surrounding discussion, p. 449 | Supplies support intersection and the least finite supports used in the orbit argument. |
| Pincus (1997) | pp. 450–451 | Establishes the dense linear ordering principle in the model and the failure of \(\mathrm{Part}_{\infty}\). |
| Pincus (1997) | §3, pp. 452–455 | Establishes the Prime Ideal Theorem in the model. |
| Pincus (1997) | pp. 447–448, including Theorem 3 on p. 448 | Gives the transfer classifications used in the consistency corollary, including the boundability of \(\neg\mathrm{Part}_{\infty}\), the placement of DO and PI in the relevant classes, and closure under conjunction. |
| Blass, *Ramsey’s theorem in the hierarchy of choice principles* (1977) | pp. 388–389 | Establishes that ordinary Ramsey’s theorem is injectively boundable in Pincus’s sense. |
| Pincus, *Adding dependent choice* (1977a) | §4, especially pp. 136–137 | Gives the transfer construction and its restatement for a Fraenkel–Mostowski model whose well-founded universe satisfies ZFE + GCH. |
| Pincus (1977a) | glossary, p. 145 | Defines \(E\) as “The universe has a well ordering.” |
| Pincus, *Adding dependent choice to the prime ideal theorem* (1977b) | pp. 547–565 | Supplies the extension of the transfer theory to the Prime Ideal Theorem. |
| Tachtsis, *On Ramsey’s theorem and the existence of infinite chains or infinite anti-chains in infinite posets* (2016) | Theorem 2.4 | Proves Ramsey’s theorem in Mostowski’s linearly ordered permutation model and provides the strategic predecessor for the argument used here. |

The consistency corollary uses Pincus’s later description of Class III in conjunction with the 1977 transfer results. Pincus’s transfer construction assumes a well-founded universe satisfying ZFE + GCH. The note explains why passing to the constructible universe supplies this background without increasing the relative consistency strength.

## 4. Howard–Rubin \(N48\), Form 17, and the implication data

Howard and Rubin list the model in Part III of *Consequences of the Axiom of Choice* under the heading

> \(N48\): Pincus’ Model XI.

A PDF copy of Howard and Rubin was used for the check of the \(N48\) entry. Claude transcribed from page images the complete lists of forms recorded true and false in \(N48\). ChatGPT independently extracted the same lists from the PDF’s machine-readable text. The two readings agreed on every entry: 172 forms in the true list and 69 in the false list, excluding the parenthetical duplicate occurrence of Form 383.

Form 17 is Ramsey’s theorem for pairs. It occurs in neither list.

A separate computational check concerned the implication data distributed with the Choiceless Grapher. The repository contains an implication matrix supplied by Paul Howard, together with form data extending beyond the 1998 catalog. The matrix used here has 431 forms, numbered 0 through 430, and therefore should not be identified with the printed 1998 Table 1 itself.

Positive direct implications were taken to be entries having code 1. ChatGPT and Claude independently computed the transitive closure from this matrix. Both computations gave the same 45 forms from which Form 17 is reachable:

\[
\{1,2,3,4,7,8,9,17,20,39,40,41,43,44,71,86,87,100,101,113,129,
152,161,168,174,181,192,202,214,255,256,257,258,259,260,261,262,
264,286,325,345,347,359,407,426\}.
\]

None of these forms is among the forms recorded true in \(N48\).

The reverse closure was also computed. In the raw matrix, Form 17 reaches

\[
\{0,10,17,18,73,80,124,132,216,249,288,342,358,373,374,389,423\}.
\]

None is recorded false in \(N48\). Under the Choiceless Grapher’s effective-form convention the descendant set has 15 forms, and its intersection with the \(N48\)-false list is again empty.

These calculations are historical and consistency checks only. They are not used in the proof that \(N48\models\mathrm{RT}^2_2\).

## 5. Literature search

A literature search was conducted to determine whether ordinary Ramsey’s theorem for pairs had already been proved for Pincus’s Model XI or Howard–Rubin \(N48\).

The search included Howard and Rubin’s catalog, Pincus’s 1997 paper, Tachtsis’s 2016 work on Ramsey’s theorem in permutation models, Brot–Cao–Fernández-Bretón’s 2021 work on Ramsey-theoretic finiteness without Choice, Banerjee–Gopaulsingh–Molnár’s 2024 work on rainbow and canonical Ramsey theorems without Choice, and Venkataramani’s 2026 work on Ramsey-theoretic finiteness and related separations.

Tachtsis proves the corresponding ordinary Ramsey result for Mostowski’s linearly ordered model rather than for \(N48\). The other papers examined concern different models, different Ramsey principles, or different finiteness phenomena.

No prior statement that \(N48\) satisfies ordinary Ramsey’s theorem for pairs was found. This search does not establish originality.

## 6. Verification history

The result first appeared as one theorem inside a broader manuscript about weak choice and transfer from permutation models to ZF. During development of that manuscript and of the present note, the proof and its citations underwent repeated machine-assisted review.

The reviews concentrated on the points most likely to affect the argument: the transformation of least supports under automorphisms, the reason a non-singleton orbit has support outside the coloring support, distinctness of the orbit elements obtained by moving one support point, pair transitivity, the treatment of the fixed-point set, and the transfer classification of the final conjunction.

Source review led to several corrections in attribution and exposition. In particular, the final transfer discussion distinguishes the 1977a transfer theorem from the separate 1977b extension involving the Prime Ideal Theorem. It also states explicitly the GCH hypothesis and Pincus’s axiom \(E\), and uses the source locations verified during preparation of the manuscript.

The historical check of Form 17 was also strengthened in stages. The \(N48\) true and false lists were independently read from the same PDF in two ways: from page images and from its machine-readable text. The implication closure was independently recomputed from the Choiceless Grapher matrix. The final description above distinguishes the later Choiceless Grapher data from the 1998 printed catalog.

The final-cycle Claude reviews were carried out with Claude Opus 5.5. Earlier Claude reviews, Meta AI reviews, and Apodex reviews are recorded without model-version claims where the version was not displayed or otherwise verified.

## 7. Scope and limitations

This supplement records checks performed during preparation of the note. It does not constitute formal verification, and agreement among AI systems is not a substitute for independent human review.

The implication computation establishes a property of the later implication dataset distributed with the Choiceless Grapher. It does not by itself reconstruct the historical state of every entry in the printed 1998 Table 1.

The literature search establishes only that no prior occurrence of the result was found in the sources searched. It does not establish originality.

The mathematical claims of the paper are intended to stand on the proofs and cited sources in the paper itself. This supplement is provided so that readers can see how those claims were developed and checked, and so that the role of AI assistance is explicit rather than implicit.

## Additional references

- I. M. Dimitriou, *Choiceless Grapher (Jeffrey)*, software repository, GitHub, `ioannad/jeffrey`, commit `75d800d` (21 May 2025). Implication data supplied by P. Howard.
- B. Venkataramani, *Ramsey-Theoretic Finiteness in Choiceless Set Theory: The Gower’s Collapse and Rainbow and Canonical Separations*, arXiv:2607.22196v1 [math.LO], 24 July 2026.