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.
Higher homotopy classes form groups and are abelian above degree one
Statement
For every based space , cubical concatenation makes a group for , with identity the constant class and inverse given by reversal of coordinate 1. It is abelian for .
Facts & Assumptions
Concatenation and pasted homotopies are continuous and well-defined in a fixed coordinate. Cubical concatenation is well defined on higher homotopy classes
The one-coordinate loop laws use endpoint-fixed reparametrizations; the formulas are replayed below. Loop classes form the group under concatenation
A group has an associative operation, a two-sided identity and inverses. Group and abelian group
Proof
Given: The spaces, maps, and hypotheses in the statement above.
For any continuous fixing endpoints, is a boundary-fixed homotopy from a to its reparametrization. The coordinate formula is jointly continuous, not merely continuous separately in u. Taking and gives . These are the loop-law formulas of F2 with u retained as a parameter.
For , set on , on , and on . The pieces agree and fix endpoints. Substitution gives on all three intervals. Step 1.1 therefore proves associativity on classes.
The map equal to for and for pastes continuously. It fixes the exterior boundary, begins at and ends at e. Applying the same formula to contracts . Together with steps 1.1–2.1 and F1 this verifies the group axioms of F3.
For let and concatenate in coordinates 1 and 2. Each has the same two-sided unit by step 1.1. Pasting four quarter-cubes gives on representatives. Therefore on classes , whereas . Hence the common operation commutes. For n=1 there is no second coordinate, and no commutativity claim is made.