LemmaStatement: AI-adaptedProof: AI-generatedPipeline-generatedjudge pass (gpt-6-luna)

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.

A finite initial segment of the naturals has its index as cardinality

Statement

For each $n \in N$ , let $I_{n} = {t \in N : t < n}$ . Then $I_{n} = n$ , so $I_{n}$ is finite and $∣ I_{n} ∣ = n$ .

Statement references

The natural numbers are the von Neumann naturals, and each natural number is the set of its predecessors.

The natural-number order is defined by addition.

For von Neumann naturals, strict order is membership.

Each natural n is finite and has cardinality n.

Dumas and McCarthy, Transition to Higher Mathematics, §1.2.

Facts & Assumptions

Given: $n \in N$ and $I_{n} = {t \in N : t < n}$ , using the additive order on $N$ .

[F1]

For every natural $n$ , $n = {t \in N : t < n}$ , and the additive strict order agrees with membership on von Neumann naturals. The natural numbers $N$ (von Neumann), Order on the natural numbers, On $N$ the order is membership: $m < n ⟺ m \in n$

[F2]

Every natural $n$ is finite and has cardinality $∣ n ∣ = n$ . The cardinality $∣ A ∣$ of a finite set

Proof

1.1givenF1

The final equality in [F1] says precisely that the set ${t \in N : t < n}$ is $n$ , so $I_{n} = n$ .

2.1step 1.1F2∎

By [F2], $n$ is finite and $∣ n ∣ = n$ . Substituting $I_{n} = n$ from step 1.1 gives that $I_{n}$ is finite and $∣ I_{n} ∣ = n$ .

Depends on

Used by

A finite POMDP family has exponentially many witnessed alpha vectors Example

Dependency tree · two levels

21 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

Bob Dumas and John E. McCarthy, Transition to Higher Mathematics, §1.2: Sets (standard reference, not scraped)