Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passaudited 2026-09-14
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.

The primary obstruction class is independent of cellular choices

Statement

Changing cell orientations, lifts, whiskers, or transport coordinates changes θ(f) only by the canonical cellular-cochain isomorphism. If f0,f1:Xn∪A→Y are joined on Xn−1∪A by H, then, under the coefficient identification supplied by H,

δd(f0,H,f1)=θ(f0)−θ(f1).

Consequently the primary obstruction cohomology class depends only on the prior-stage map up to the stated homotopy and canonical coefficient identification.

Facts & Assumptions

[F1]

Reversing a cell orientation or changing its lift transforms the cellular generator and obstruction value by the matching sign or monodromy action, so the primary cochain is unchanged under the canonical basis identification (Primary cellular obstruction cochain).

[F2]

The obstruction cochain on the product CW pair is a cocycle (The primary obstruction cochain is a cocycle).

[F3]

With the interval-last orientation fixed in the difference-cochain definition, ∂(e×I)=(∂e)×I+(−1)dim⁡e(e×1−e×0) (Difference cochain between two cellular extensions).

[F4]

Homotopy-group basepoint transport depends only on the endpoint-fixed path class, composes along concatenated paths, and in degree one is conjugation by the transport path (Higher homotopy basepoint transport and moving homotopies).

[F5]

The coefficient system is a covariant functor whose transports compose along concatenated incidence paths (Homotopy-group local system along a cellular map).

Proof

Given: The cellular data and the maps f0,f1,H in the statement.

1.1F1F4F5

An orientation reversal multiplies both the cellular generator and the recorded obstruction value by −1, while a lift change applies the same deck transformation and inverse monodromy relation on the equivariant cellular Hom; these are exactly the canonical basis identifications in [F1]. If a whisker u from the attaching-sphere basepoint a to the chosen coordinate c is replaced by v:a→c, the comparison loop at c is uˉ∗v, not u∗vˉ (which is based at a). Writing fu and fv for their images in Y, the published convention gives Tu=βfu‾ and βγ∗η=βγβη, so Tu=βfu‾∗(fv)Tv. Thus this coordinate-loop transport carries the new recorded value to the old one; its inverse βvˉ∗u carries old to new. In the n=1 case the action is trivial by the standing coefficient hypothesis. Finally, changing transport coordinates means applying a stalkwise natural isomorphism of the fixed local system in [F5]. By the defining naturality square it intertwines transport along every incidence path. Applying it stalkwise therefore commutes with the cellular coboundary and sends each old obstruction value to its new coordinate. In all four cases the resulting canonical cellular-cochain isomorphism carries θ(f) and its cohomology class to their new-coordinate versions.

1.2F2

Give (X×I,A×I) the relative prism CW structure and put Zn=(Xn×∂I)∪(Xn−1×I)∪(A×I). The endpoint maps f0,f1 and H agree on overlaps, defining a map F:Zn→Y. Let PH be the homotopy-group coefficient system induced by F, with its endpoint restrictions identified along H. Then [F2] gives a relative obstruction cocycle Θ∈Ccelln+1(X×I,A×I;PH). Its values on horizontal (n+1)-cells are θ(f0) and θ(f1), while its signed restriction to vertical cells en×I is the difference cochain by definition.

2.1F2F3step 1.2

Evaluate δΘ=0 on en+1×I. Using [F3] and the defining sign d(en)=(−1)n+1Θ(en×I) gives 0=(−1)n+1(δd(en+1)+θ(f1)(en+1)−θ(f0)(en+1)). Hence δd=θ(f0)−θ(f1) on every cell.

3.1step 1.1step 2.1

Coboundaries vanish in cohomology, so Step 2.1 identifies [θ(f0)] and [θ(f1)] after the coefficient transport supplied by H. Combining this with Step 1.1 proves independence from every listed choice. The argument uses a supplied homotopy and supplied coordinates and makes no set-indexed selection. □

Depends on

Dependency tree · 2 levels

Sources