Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-13
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.

Factor reversal gives the commutativity chain homotopy

Statement

Let X be a space and R a commutative unital ring. Put A=AW:C(X×X;R)C(X;R)RC(X;R) and let τ(x,y)=(y,x). On homogeneous tensors put W(ab)=(1)pqba(a=p, b=q). Then WAτ# and A are naturally chain homotopic. In particular WDX and DX, with DX=AΔ#, are naturally chain homotopic. No AC is required.

Facts & Assumptions

[F1]

Alexander--Whitney and shuffle are natural chain-homotopy inverses provides natural maps A,S and specified natural homotopies for AS1 and SA1, over R.

[F2]

The singular chain cross product on generators expresses S as the signed sum of monotone lattice paths.

Proof

Given: The signed tensor differential d(ab)=dab+(1)padb. Take the supplied homotopies dU+Ud=AS1 and dV+Vd=SA1.

1.1

The coefficients of dba and bda in dW(ab) are respectively (1)pq and (1)pq+q. In Wd(ab) they are (1)p+p(q1) and (1)(p1)q, respectively. Each corresponding pair agrees modulo two, so dW=Wd. Also W2=1. Terms involving da or db in degree zero are absent, so the calculation includes p=0 and q=0.

given
1.2

A shuffle path has p horizontal and q vertical steps. Its permutation sign is (1)N, where N counts vertical steps occurring before horizontal steps. Interchanging the two types of steps replaces N by pqN, since each horizontal/vertical pair contributes to exactly one of the counts. It therefore changes the sign by (1)pq. The affine simplex of the swapped path is the original one followed by factor interchange. Matching paths bijectively in the finite shuffle sums gives τ#S=SW. This is a signed-shuffle calculation, not merely naturality for maps of the two factors.

F2given
2.1

Put B=WAτ# and L=WUW. These are natural (with simultaneous maps of X), and step 1.2 gives BS=WASW. Thus dL+Ld=W(AS1)W=BS1. The map B is a chain map by step 1.1, [F1], and the fact that postcomposition commutes with face boundary. Define K=LABV. Using the two supplied homotopy equations yields dK+Kd=(BS1)AB(SA1)=BA. This is an explicitly specified natural homotopy.

F1step 1.1step 1.2given
3.1

Since τΔ=Δ, precomposing step 2.1 with the chain map Δ# gives d(KΔ#)+(KΔ#)=WDXDX. In degree zero the twists have sign +1 and the maps agree on vertices. If X is empty or R=0, all maps have zero complexes as domain and codomain. Degenerate singular simplices and one-point spaces use the same shuffle paths and homotopies; nothing was normalized away. The construction uses finite signed sums and the supplied homotopies, not a selection of new fillers, so it is choice-free.

F1F2step 2.1

Depends on

Used by

Dependency tree · two levels

10 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