Alphabeta Math
CounterexampleConstruction: AI-generatedVerification: AI-adaptedPipeline-generatedprecheck passaudited 2026-09-27
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 isolated differential 2 on the integers cannot be cancelled

Statement refuted

In the two-term complex 0→Z→2Z→0, the nonzero differential entry 2 can serve as a Gaussian pivot: the two terms can be cancelled and replaced by the zero complex, which is homotopy equivalent to the original complex.

Facts & Assumptions

Given: The two-term cochain complex X∙ in the category of abelian groups with Xn=Z, Xn+1=Z, differential dn=⋅2, and Xj=0 for j∉{n,n+1}; and the claim that the two terms of X∙ can be cancelled, so that X∙ is homotopy equivalent to the zero complex.

[L1]

A pivot is required to be an isomorphism, with a two-sided inverse φ−1; the Schur complement a−bφ−1c is defined through that inverse (An invertible cochain differential block and its candidate reduction).

[L2]

The splitting theorem produces a homotopy equivalence between a complex and its reduction only when the pivot block of the decomposition is invertible; its contractible summand has differential the pivot itself (Gaussian elimination splits a contractible two-term complex).

[L3]

A complex is contractible when there is a family h with 1Cn=dn−1hn+hn+1dn for all n; a complex is homotopy equivalent to the zero complex exactly when it is contractible (Complexes, homotopies and contractibility in an additive category).

[L4]

The homology object of a chain complex is the cokernel of the boundary-to-cycle map Bm→Zm supplied by the factorization of the boundary inclusion through the cycle inclusion (Cycle and boundary subobjects of a complex, The boundary subobject factors through the cycle subobject, Homology object of a chain complex).

Counterexample

1.1

The entry 2 has no inverse in the category of abelian groups. If u:Z→Z satisfied 2u=1 or u⋅2=1, then evaluating at 1 gives 2u(1)=1 with u(1)∈Z, which is impossible because 1 is odd; equivalently Z has no element m with 2m=1. Since 2 is not invertible, it is not a pivot in the sense of [L1], and the Schur complement a−bφ−1c of the block (φ)=(2) is not defined on its own.

L1algebra
1.2

The complex nonetheless has nonzero homology. Reindexing by Cm:=X−m gives the chain complex Z→2Z concentrated in degrees −n and −n−1. There Z−n−1=ker⁡(d−n−1=0)=Z and B−n−1=im⁡(d−n)=im⁡(2)=2Z, so the boundary-to-cycle map is the inclusion 2Z↪Z and, by [L4], H−n−1≅Z/2Z≠0; this is the homology in cochain degree n+1 of X∙.

L4algebra
2.1

The complex is not contractible. If it were, [L3] would give a homomorphism hn+1:Z→Z with 1Xn=dn−1hn+hn+1dn=0+hn+1⋅2 in degree n, because dn−1=0 and dn=⋅2; evaluating at 1 would produce an integer hn+1(1) with 2hn+1(1)=1, which is impossible by step 1.1. Hence X∙ is not homotopy equivalent to the zero complex, and deleting both terms would not be a homotopy equivalence.

L3step 1.1algebra
3.1

Consequently the pivot hypothesis of [L1] and [L2] is genuinely needed: the deleted terms carry the nonzero homology object H−n−1≅Z/2Z of step 1.2, which the zero complex does not have, and no two-sided inverse of 2 exists in Z. The claim refuted is therefore false; the theorem's conclusion is not available here because its hypothesis fails. ∎

L2step 1.2step 2.1algebra

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

16 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