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 collapse with a noncanonical extension choice
Example
The finite filtration has two graded pieces , but its target is not . Over a field, a finite vector-space filtration splits under AC, yet its complements need not be natural; already has complements moved by automorphisms. Both filtrations can occur in collapsed first-quadrant sequences.
Facts & Assumptions
Given: The two displayed filtered modules.
Collapse retains the extension between its graded quotients (UCT and Kunneth collapse retains an extension problem).
Under AC finite vector-space filtrations split; finite-dimensional individual filtrations need only finite choice, and a shear can prevent naturality (Collapsed vector-space spectral sequences split noncanonically).
Verification
Put in cochain degree one, with zero differential, , and . The associated graded is at and , zero elsewhere. Every differential is zero, so all pages equal this graded object, and actual cohomology is with exactly the displayed finite filtration. A section of would send the element of order two to an element killed by two lifting the odd coset. Its only lifts are and , both of order four. Thus no section exists; equivalently has order-four elements while does not. This is F1's extension obstruction with no choice assumption.
Similarly place in degree one, , with zero differential. Its stationary entries are at the same two positions, and its finite image filtration gives the actual abutment. Each line is a complement, since its intersection with is zero and every vector is the sum of elements in those two lines. Conversely every complement has this form by normalizing the second coordinate of a nonzero vector in it. The shear , sends to and fixes no complement, while inducing identity on both graded pieces. Hence existence and even an explicit choice do not give naturality.
In arbitrary dimension F2 uses AC for bases and complements, followed by only finitely many filtration splittings. In the displayed two-dimensional example the formula already supplies complements in ZF. In both cases the full target has zero/full filtration endpoints , so convergence has no hidden issue; the unresolved question from page data alone is the extension or its choice of section. With just one nonzero quotient this particular extension obstruction disappears.
Depends on
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
10 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
- Weibel, Section 5.2 (standard reference, not scraped)