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.
Relative homotopy classes and groups
Definition
Let , with carrying its subspace topology, and . Set and let be the union of the other faces of . A relative representative is a continuous map with and . Two representatives are equivalent if connected by a continuous homotopy satisfying these same conditions at every time. Reversal of time and pasting in time give the equivalence relation, with constant homotopies giving reflexivity. Its classes form , pointed by the constant map.
For , and : representatives are paths from a variable point of to . This is a pointed set, with no group operation asserted. Relative is not defined. For , concatenation uses coordinate 1 as in Higher homotopy group by based cubes, leaving the distinguished last coordinate untouched. The group law is established below. If this is the absolute cubical definition.