ExampleConstruction: AI-generatedVerification: AI-generatedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-14

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 minimal walk and its lower trace

Example

Use the normalized successor values $C_{η + 1} = {0, η}$ and put

$C_{ω} = {2 n : n < ω} = {0, 2, 4, 6, \dots} .$

For $α = 5$ , $β = ω$ , and $γ = ω + 2$ , the three relevant minimal walks are

$ω + 2, ω + 1, ω, 6, 5; ω + 2, ω + 1, ω; ω, 6, 5.$

Their upper traces satisfy

$Tr (5, ω + 2) = {ω + 2, ω + 1, ω, 6} = Tr (ω, ω + 2) \cup Tr (5, ω) .$

The lower-trace running-max lists are respectively $(0, 0, 4, 4)$ , $(0, 0)$ , and $(4, 4)$ . Thus

$L (5, ω + 2) = {0, 4} = L (ω, ω + 2) \cup L (5, ω),$

and the strict separation hypothesis is visibly $L (ω, ω + 2) = {0} < {4} = L (5, ω)$ .

Facts & Assumptions

Given: Extend the displayed fragment to the normalized locally finite $C$ -sequence fixed on the companion page.

[F1]

C-sequences and the upper and lower traces of minimal walks on omega-one chooses at each stage the least member of $C_{ζ}$ at or above the target, excludes the final target from the upper trace, and records lower traces by running maxima of $C_{ζ} \cap α$ .

[F2]

Concatenation and limit control for minimal-walk traces gives trace concatenation when $L (β, γ) < L (α, β)$ .

Verification

technique · direct calculation

1.1

The displayed $C_{ω}$ is cofinal in $ω$ , contains $0$ , and has finite intersection with every $m < ω$ . Together with $C_{η + 1} = {0, η}$ , it meets every local requirement of [F1] used in this calculation.

F1Given

2.1

Aiming at $5$ , the least points at or above the target are $ω + 1$ in $C_{ω + 2}$ , $ω$ in $C_{ω + 1}$ , $6$ in $C_{ω}$ , and $5$ in $C_{6}$ . Aiming at $ω$ , the first two choices are $ω + 1$ and $ω$ ; aiming at $5$ from $ω$ , the choices are $6$ and $5$ . This proves the three displayed walks and, after deleting their terminal points, the three asserted upper traces.

F1step 1.1

3.1

For target $5$ , the successive intersections along the long walk are $C_{ω + 2} \cap 5 = {0}$ , $C_{ω + 1} \cap 5 = {0}$ , $C_{ω} \cap 5 = {0, 2, 4}$ , and $C_{6} \cap 5 = {0}$ . Their cumulative maxima are $(0, 0, 4, 4)$ . For target $ω$ , the two intersections are both ${0}$ , giving $(0, 0)$ ; for target $5$ from $ω$ , the intersections are ${0, 2, 4}$ and ${0}$ , giving $(4, 4)$ .

F1step 1.1step 2.1

4.1

Passing from the running-max lists to their trace sets gives $L (ω, ω + 2) = {0} < {4} = L (5, ω)$ and $L (5, ω + 2) = {0, 4}$ . Hence [F2] applies and its upper- and lower-trace unions agree exactly with the direct computations. No maximum of an empty set occurs, all three targets are strict lower endpoints, and multiplicities were retained until the final set calculation.

F1F2step 2.1step 3.1∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

5 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.