doc: add grounded roadmap for infinitary syntax, back-and-forth, and Scott analysis

[cameronfreer]

Summary

Adds TauCetiRoadmap/InfinitaryLogic/, a grounded roadmap for the first Tau Ceti infinitary-model-theory spine: (1) Lω₁ω / L∞ω syntax and semantics over FirstOrder.Language; (2) the finitary embedding toLω + realization compatibility; (3) back-and-forth / potential isomorphism — an explicit back-and-forth system of Mathlib FGEquivs with its basic API (potentialIso_of_equiv, PotentialIso.symm, PotentialIso.trans) and a one-way bridge from Mathlib's IsExtensionPair — and Karp; (4) the countable coded-formula proxy for the Scott-refinement formulas and refinement counting; (5) Scott's isomorphism theorem for countable relational languages (the v1 summit).

This roadmap does not cover admissible sets / Barwise compactness, invariant descriptive set theory (Silver / G₀ / Glimm–Effros, López–Escobar, Morley counting), EM / Erdős–Rado / Morley–Hanf, many-sorted model theory, or Lκλ; those are out of scope here and belong in separate roadmap PRs with their own grounded dependency paths. It also adds a "known WIP, ownership, and boundaries" section — now with links to the four in-flight Zulip threads and a stated rationale for the parallel-inductive prototype. The earlier revision made Layer 0's substitution/relabel/recursion API explicit and added per-layer dependency/acceptance checks; the latest revision corrects the PotentialIso definition (see the correction comment on this thread), pins its basic API, and brings the branch up to date with main. See the replies on the review thread.

Contents

• TauCetiRoadmap/InfinitaryLogic/README.md (narrowed roadmap), Suggested.lean (Layer 0/1 elaborating signatures, opened with the standard "README.md is definitive / not exhaustive" note), root index fix: correct stale and fabricated Mathlib paths in roadmap inventories #14, the Suggested import.

Verification

• Full lake build green (8521 jobs); Suggested.lean elaborates with only the six intended sorry targets (realize_toLω, potentialIso_of_equiv, PotentialIso.symm, PotentialIso.trans, potentialIso_of_isExtensionPair, countable_potentialIso_iff_iso) — all definitions carry real bodies (no def _ : Prop := sorry).
• Mathlib paths verified at the pin (mathlib 9caeba1 / Lean v4.31.0-rc1).

Migration source

Pinned at cameronfreer/infinitary-logic @a1932b9 — a migration source and API-warning map, not the specification; the README's "Migration source" section maps it onto the spine layers. The source's Scott theorem is unconditional (its CountableRefinementHypothesis is discharged sorry-free); its remaining frontier sorry (Erdős–Rado) sits in territory that is out of scope for this PR.

Attribution

Cameron Freer wrote this with assistance from GPT Pro, Claude Code, Codex, lean4-skills, and lean-lsp-mcp.

Thanks to @kim-em and @mrdouglasny for helpful reviews.

[kim-em]

I don't think this is quite at our "connected all the way to the ground" bar yet, and there are a couple of gaps I'd like closed before we merge:

• Layers 8–9 (the descriptive set theory). At the pinned Mathlib, there's no Borel hierarchy / pointclasses, no Borel codes, no E₀ / hyperfinite, and no Gandy–Harrington. The prose names some of this, but the target list goes from IsBorelEquivalence / BorelReducible straight to Silver / G₀ / Glimm–Effros without making the intervening infrastructure explicit. (Your migration source files GandyHarrington and SilverBurgess under Conditional/, which makes me wary of treating them as ready targets.) I think it's best if we drop these layers from the roadmap for now, and deal with them in a follow-up.
• Layer 4 (admissible sets / KP). You correctly say Mathlib has none and it "must be built here", but the targets jump to AdmissibleFragment / barwise_compactness. The admissible-set theory itself (KP, Σ-definability, A-finiteness, set-coded syntax) needs to be a target too, by the same rule.

Separately, there's a fair amount of related work already in motion that I think we'll need to coordinate with rather than route around:

• Your own #mathlib4 > ModelTheory: API for infinitary formulas of L_{∞,ω} thread — the single-core-vs-parallel-types question you raised there never got an answer, and this roadmap commits to parallel types. Worth citing it and saying why.
• #mathlib4 > Cantor-Bendixson analysis (Violeta is about to PR perfect-kernel / the ordinal-stabilization lemma your Scott rank needs) and #mathlib4 > Naming Suslin Spaces (the Effros theorem + AnalyticSpace, mathlib4#32742) overlap Layers 8–9.
• #mathlib4 > Many-sorted model theory (Mathias Stout's group, with Aaron Anderson) overlaps Layer 11.

Given how much of this is live, I suspect merging this roadmap may need to wait until Tau Ceti is public — coordinating with these efforts will be much easier once the Zulip channel is public.

This is sufficiently far outside my own expertise that I'm not the right person to give it a final sign-off. We'll need to find another reviewer with real model-theory / DST background (waiting for release should help there too — several of the people in the threads above would be ideal). :-)

[mrdouglasny]

Structural review — TauCetiRoadmap #41

Roadmap: Infinitary logic, Scott analysis, and the descriptive set theory of countable models
Author: cameronfreer · PR: FormalFrontier/TauCetiRoadmap#41 · Head: 221cde7
Reviewers (purely AI, independent): Claude Opus 4.8 · Gemini 3.1 Pro · Codex / GPT‑5.4
Date: 2026‑06‑27 · Type: structural review (not a proof review)

---

Verdict (unanimous)

Structurally excellent and house‑pattern‑perfect — but scoped as a multi‑year program, not a single roadmap. Cut v1 to Layers 0–2 (+ relationalization) and split the remainder into dependent sibling roadmaps. The roadmap would pass a TauCeti review on quality; it should be restructured for scope and hidden dependencies before it is handed to the pod, or the agents will hit the unscaffolded admissible‑set and effective‑DST walls mid‑run.

All three reviewers reached this independently — the agreement is itself a confidence signal.

---

What all three agree on

Strengths

• Exemplary house‑pattern + generality discipline — every required section; unbundled instances ([L.IsRelational], [Countable M], [Countable (Σ n, L.Relations n)] carried separately); ω₁ = Ordinal.omega 1 with no bespoke subtype; intrinsic spec with the existing Lean formalization pinned only as a secondary migration source.
• Correct core architecture — parallel infinitary inductive (not an extension of finitary BoundedFormula); the FormulaCode countable proxy that turns "countably many Scott formulas" into a theorem; universe‑w Karp.
• Honest about the source's real gaps — flags that the migration source's hard cases live in its Conditional/ directory (Hanf transfer, Gandy–Harrington).
• Consume/build split is factually correct — Codex verified against live Mathlib docs that BoundedFormula's iSup/iInf really are [Finite]‑restricted and that IsRelational / Symbols / FGEquiv / IsExtensionPair / standard‑Borel / analytic‑sets genuinely exist to consume. No bogus "Mathlib already has it" claims.

The core finding: scope → split

It bundles four separate disciplines (infinitary model theory · admissible‑set theory/KP · partition calculus · descriptive set theory) into one linear roadmap.

• Consensus minimal v1 = Layers 0–2 (syntax → Karp → Scott), with relationalization (Layer 11) pulled up (it depends only on 0–2, and users want Scott for function/algebraic languages early).
• Everything else → dependent sibling roadmaps. Gemini groups into ~3–4 (Core / Partition / DST / eject admissible sets); Codex splits finely (A–M). Same shape, different granularity.
• Spin off Layer 6 (Erdős–Rado / partition calculus) as standalone, Mathlib‑upstreamable combinatorics.
• Eject Layer 4 (Barwise / admissible sets) to a dedicated Kripke–Platek roadmap — the KP / Δ₀‑set‑theory API does not exist in Mathlib and the roadmap allocates zero layers to it.

Under‑scoped layers (difficulty hidden as bullets)

L4 (admissible sets — no Mathlib KP), L9 (Silver / G₀ / Glimm–Effros — three deep dichotomies needing effective DST / Gandy–Harrington scaffolded nowhere), L8, L13. Codex adds L0 (under‑scoped for its blast radius — binding/substitution/universes/recursion principles every later theorem inherits) and L3.

Critical‑path single points of failure

1. refinement_countable / BFEquiv_iff_agree_codes — the entire Scott summit rides on this one bridge. Vet the FormulaCode encoding by hand before any agent starts (avoid dependent‑type‑transport hell).
2. Silver → Morley counting — cannot proceed without a real Borel‑equivalence‑relation library that does not yet exist.

---

Distinct contributions by reviewer

Gemini 3.1 Pro

• The "effective‑DST iceberg": L9/L13 silently need lightface / Gandy–Harrington machinery absent from both Mathlib and Layers 0–8.
• Universe‑clash warning for BoundedFormulaInf (universe‑indexed) vs model universes — Mathlib's FirstOrder.Language already struggles with universe bumping; infinitary conjunctions make it perilous.
• Eject admissible sets to a KP roadmap; move relationalization up.

Codex / GPT‑5.4

• "No forward references is mostly aspirational" — L8–10 silently depend on more DST than listed; L4 on a whole KP development; L12 (Lκλ) may force a different syntax architecture back onto Layer 0 (a real hidden forward‑dependency the ordering claim misses).
• Layer 0 under‑scoped for its blast radius.
• Replace the "coded proxy or direct game‑counting" ambiguity with one chosen route; demote the other to a provenance note.
• Add a per‑milestone dependency table (prior milestones + Mathlib imports + new infra) and per‑layer compile‑before‑summit examples.
• Name‑audit against Mathlib conventions before implementation (flagged LInfEquivW).
• Add bridge lemmas: Countable (Σ n, L.Relations n) ↔ L.card ≤ ℵ₀, and Countable M ↔ Structure.CG (to mesh with equiv_between_cg).

Claude

• The L10(a) vs L10(b) seam: the bounded‑Scott‑height dichotomy (counting_dichotomy_of_bounded_scottHeight) needs only Borel‑iso + Silver‑for‑Borel and is reachable even if the effective track slips; full Morley (morley_counting) and G₀ need the harder machinery. State this as the milestone boundary so the DST track has a reachable sub‑summit.
• House‑pattern compliance audit; per‑layer ⚠ API‑warning quality is unusually high.

---

Recommended actions (consensus, ordered)

1. Retitle/cut v1 to "Core Lω₁ω & Scott Analysis" = Layers 0–2 + 11, with an explicit "not in scope for v1: Barwise, Hanf, Morley counting, Lκλ, effective."
2. Promote the coded‑formula bridge to its own named milestone group with acceptance examples — it is a subproject, not a bullet.
3. Spin off Erdős–Rado (standalone combinatorics) and eject admissible sets (dedicated KP roadmap).
4. Pick one counting route (proxy or game‑counting); the other becomes a provenance note.
5. Add a dependency table per milestone and examples that compile using only prior layers.
6. Name‑audit against Mathlib conventions before the pod starts.
7. Vet the Layer‑0 syntax + FormulaCode encoding by hand before any agent touches it — every later theorem inherits those choices, and L12 may otherwise force a redesign.

---

Methodology note

Purely AI review, three independent models given the same artifact (the full roadmap README at head 221cde7) and the same structural rubric (library‑building, generality bar, unbundled hypotheses, correct Mathlib reuse, dependency ordering, naming/placement). Codex additionally ran a live Mathlib‑docs verification pass on the consume/build claims. No proofs were attempted; this assesses roadmap structure only. Convergence across all three on the scope/split diagnosis is the headline.

[cameronfreer]

Thanks, @kim-em and @mrdouglasny -- these reviews are helpful. I've narrowed this PR rather than trying to patch the whole long-range program in place.

The active roadmap now contains just the spine of results along the way to Scott isomorphism:

• Lω₁ω / L∞ω syntax and semantics;
• the finitary embedding and realization lemmas;
• back-and-forth / potential isomorphism / Karp;
• the coded-formula proxy and refinement-counting bridge;
• Scott rank, Scott sentences, and Scott's isomorphism theorem.

Everything beyond this is removed from the roadmap entirely (admissible sets / Barwise, invariant DST, Silver / G₀ / Glimm–Effros, Morley counting, EM / Erdős–Rado / Morley–Hanf, many-sorted, Lκλ, effective Scott analysis, and relationalization of functions/constants). These can be grouped into their roadmap PRs later with appropriate grounding details and checks for WIP.

I also folded in some review points that still apply to what remains:

• Layer 0's recursion/substitution/relabeling/universe API is now explicit
• FormulaCode is the chosen counting route
• there's a per-layer dependency/acceptance table
• the bridge-lemma names are target shapes pending a Mathlib name audit.

[cameronfreer]

@kim-em wrote:

Given how much of this is live, I suspect merging this roadmap may need to wait until Tau Ceti is public — coordinating with these efforts will be much easier once the Zulip channel is public.

This is sufficiently far outside my own expertise that I'm not the right person to give it a final sign-off. We'll need to find another reviewer with real model-theory / DST background (waiting for release should help there too — several of the people in the threads above would be ideal). :-)

Sounds good; happy to wait! =]

[cameronfreer]

Important correction since the previous review: PotentialIso was defined using Mathlib's global IsExtensionPair predicate, which quantifies over all finitely generated partial equivalences and is strictly stronger than classical potential isomorphism. For example, (ℕ, <) is isomorphic to itself, but the partial equivalence 1 ↦ 0 cannot be extended to include 0 in its domain — so with the old definition, karp_theorem and countable_potentialIso_iff_iso were both false as stated (only the one direction previously written in Lean, PotentialIso → iso, was true, which is why the file compiled).

PotentialIso is now defined by the existence of a nonempty back-and-forth system S, with potentialIso_of_isExtensionPair retaining the one-way S = univ bridge to Mathlib's vocabulary. The countable milestone is now the correct iff countable_potentialIso_iff_iso, and the basic API is pinned alongside (potentialIso_of_equiv, PotentialIso.symm, PotentialIso.trans, with both halves of the transitivity back-and-forth recorded in the docstring). The counterexample is documented in the definition's docstring and a Layer-1 API warning in the README. Full lake build is green.

---

🤖 written by Claude, reviewed by Codex, directed by Cameron