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 chain needing different subdivision depths on its simplices
Example
For the cover , of , the finite real chain with and has simplices of different least subdivision depths: zero for and one for .
Facts & Assumptions
Given: These two paths and this ordered cover.
Smooth subdivision consists of affine domain pieces (Barycentric subdivision and prism preserve smooth singular chains).
In dimension one the subdivision cone gives the two oriented halves (Barycentric subdivision operator).
Proof
The image of is , so it is already small. The image of is in neither nor , since and . Thus its least depth is positive. Both paths extend smoothly to all real parameters.
The cone convention [F2] gives , where and . Their images are respectively and . Thus is small and the least depth of is exactly one. Since both halves of the constant path are the same constant path, . Consequently is small.
This exhibits different least depths within a finite chain, while the common bound one works for the entire chain. The two terms of are distinct basis maps, so the nonsmall does not cancel before subdivision. Zero coefficients or the empty chain would have no such obligation. Endpoint inclusions above are strict relative to the cover thresholds, and the degenerate constant path has been computed rather than discarded. No choice is used.
Depends on
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
9 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
- DG-16 design; Hatcher/Park control (standard reference, not scraped)