LemmaStatement: AI-adaptedProof: AI-generatedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-07

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Compatible recursion attempts

Statement

Let $R$ be well-founded and setlike on $X$ , and let a definable rule $G (x, h)$ assign a unique set whenever $x \in X$ and $h$ is a set function on ${pred}_{R} (x)$ . An attempt is a set function $f$ on a predecessor-closed set $D \subseteq X$ satisfying $f (z) = G (z, f ↾ {pred}_{R} (z))$ for every $z \in D$ .

Any two attempts agree on the intersection of their domains. If for every $y R x$ an attempt exists on the canonical cone $C (y)$ , there is a unique attempt on $C (x)$ .

Facts & Assumptions

Given: Work in ZF unless the statement explicitly weakens or supplements it; fix the objects and hypotheses of the statement.

[F1]

Let $R$ be well-founded and setlike on a definable class $X$ . If a definable property $P$ is progressive, meaning that for every $x \in X$ , $[\forall y R x P (y)] \Rightarrow P (x)$ , then $P (x)$ holds for all $x \in X$ . Set parameters in $P$ are allowed. This holds without Foundation. (Induction on well-founded setlike relations)

[F2]

For every setlike relation $R$ on a definable class $X$ and $x \in X$ , there is a least predecessor-closed set $C (x) \subseteq X$ containing $x$ . It consists exactly of nodes reachable from $x$ by a finite sequence of predecessor steps. Well-foundedness is not needed. (Finite predecessor closures are sets)

Proof

1.1

The intersection of two attempt domains is predecessor-closed. At a point of the intersection, agreement at all predecessors makes their restricted functions equal; functionality of $G$ then makes their values equal. Well-founded induction on this intersection proves agreement throughout.

2.1

For each $y R x$ , the attempt on $C (y)$ is unique by step 1.1. Since the predecessor set is a set, Replacement collects these uniquely specified attempts. Their union $h$ is a function on $D = ⋃_{y R x} C (y)$ by agreement on overlaps. Its domain is predecessor-closed and it satisfies the attempt equation, because each point and all its predecessors lie in a constituent cone.

F2step 1.1

3.1

There is no finite R-cycle: the finitely many nodes of such a cycle would form a nonempty set with no minimal member. Thus $x \notin D$ . The finite-path description gives $C (x) = D \cup {x}$ . Extend $h$ by the single pair $(x, G (x, h ↾ {pred}_{R} (x)))$ . The extension obeys the rule at $x$ , and it does not alter any predecessor restriction of a point in $D$ . It is an attempt on $C (x)$ , unique by step 1.1. If the predecessor set is empty, the same construction starts with $h = \emptyset$ .

F2step 1.1step 2.1given∎

Depends on

Used by

Recursion on well-founded setlike relations Theorem

Dependency tree · two levels

4 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Marks, Set Theory, Berkeley edition — Theorem 6.6 proof p.31. (standard reference, not scraped)