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.
The minimal-walk functions are coherent and finite-to-one
Statement
For every , the function is finite-to-one. If , then
is finite. Thus is coherent on the common domains of its members.
Facts & Assumptions
Given: Ordinals and the fixed minimal-walk data.
Minimal-walk weights, labelled lower traces, and the functions e-beta identifies with the maximum of the finite local weights over .
Concatenation and limit control for minimal-walk traces proves trace concatenation once the finite initial intersections above the splice have stabilized.
Proof
Fix and set . We prove that has no limit point at or below .
Let be a limit ordinal. The two traces and are finite. Local finiteness makes each finite for a trace node . Choose above every member of all these intersections, and let be the maximum of and their finitely many cardinalities. Cofinality of permits enlarging so that whenever .
For , no trace node above has a -point in . Hence the walks toward first follow the walks toward and then the walk from to ; this is the same splice calculation as [F2]. Moreover, every local weight on either upper segment is its stabilized value , whereas the lower segment contains the weight .
Taking the maxima in [F1] therefore gives for every . Such is not in , so is not a limit point of . Zero and successor ordinals are not limit points from below, so has no limit point at or below .
If were infinite, its well-order would recursively give a strictly increasing -sequence from . Its supremum is a nonzero limit ordinal and every final segment below meets , contradicting step 3.1. Hence is finite.
The set lies in , so every fiber of is finite. Taking, for example, , the disagreement set between and also lies in and is finite.
Step 5.1 proves finite-to-one behavior and coherence simultaneously. It also covers , where the domain and disagreement set are empty, and , where disagreement is empty.
Depends on
Used by
Dependency tree · two levels
6 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
- Moore, A solution to the L space problem, Section 2, Fact 5 and proof, printed p. 9 (standard reference, not scraped)