Alphabeta Math
TheoremStatement: AI-adaptedProof: AI-adaptedPipeline-generatedaudited 2026-09-10
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 (X,x0), cubical concatenation makes πn(X,x0) a group for n≥1, with identity the constant class and inverse given by reversal of coordinate 1. It is abelian for n≥2.

Facts & Assumptions

[F1]

Concatenation and pasted homotopies are continuous and well-defined in a fixed coordinate. Cubical concatenation is well defined on higher homotopy classes

[F2]

The one-coordinate loop laws use endpoint-fixed reparametrizations; the formulas are replayed below. Loop classes form the group π1(X,x0) under concatenation

[F3]

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.

1.1F1F2

For any continuous ϕ:I→I fixing endpoints, a((1−t)s+tϕ(s),u) is a boundary-fixed homotopy from a to its reparametrization. The coordinate formula is jointly continuous, not merely continuous separately in u. Taking ϕR(s)=min⁡(2s,1) and ϕL(s)=max⁡(2s−1,0) gives a∗e≃a≃e∗a. These are the loop-law formulas of F2 with u retained as a parameter.

2.1F1F2step 1.1

For w=(a∗b)∗c, set ϕ(s)=s/2 on [0,1/2], s−1/4 on [1/2,3/4], and 2s−1 on [3/4,1]. The pieces agree and fix endpoints. Substitution gives w(ϕ(s),u)=(a∗(b∗c))(s,u) on all three intervals. Step 1.1 therefore proves associativity on classes.

3.1F1F2F3step 1.1step 2.1

The map equal to a(2s(1−t),u) for s≤1/2 and a(2(1−s)(1−t),u) for s≥1/2 pastes continuously. It fixes the exterior boundary, begins at a∗a− and ends at e. Applying the same formula to a− contracts a−∗a. Together with steps 1.1–2.1 and F1 this verifies the group axioms of F3.

4.1F1step 1.1step 3.1∎

For n≥2 let ∗ and ∘ concatenate in coordinates 1 and 2. Each has the same two-sided unit by step 1.1. Pasting four quarter-cubes gives (a∘b)∗(c∘d)=(a∗c)∘(b∗d) on representatives. Therefore on classes a∗b=(a∘e)∗(e∘b)=(a∗e)∘(e∗b)=a∘b, whereas a∗b=(e∘a)∗(b∘e)=(e∗b)∘(a∗e)=b∘a. Hence the common operation commutes. For n=1 there is no second coordinate, and no commutativity claim is made.

Depends on

Dependency tree · 2 levels

Sources