Alphabeta Math
False statementConstruction: AI-adaptedVerification: AI-adaptedPipeline-generated
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.

Every exact couple is a long exact sequence with no extra grading data

Statement

False: An ungraded long exact sequence, without additional grading and repeated-object data, determines the specified homological exact-couple spectral sequence.

Facts & Assumptions

[F1]

Exact couple requires the bigraded objects and degrees degi=(1,1), degj=(0,0), degk=(1,0) in an initial couple, in addition to three exactness conditions.

[F2]

Abelian-group model for spectral-sequence computations proves that multiplication by 2 on Z is injective, with image 2Z and cokernel Z/2.

Refutation

Given: The ungraded long exact sequence with nonzero terms L0=Z, L1=Z, L2=Z/2, maps L0L1 multiplication by 2 and L1L2 reduction modulo 2, and Ln=0 for every other integer n. All other maps are zero.

1.1

This sequence is exact: multiplication by 2 is injective, its image is the kernel of reduction, and reduction is surjective. Exactness at every zero term is equality of zero subgroups.

F2
2.1

For each c{0,1} define Dp,q(c)=Z and Ep,q(c)=Z/2 when p+q=c, and zero otherwise. Let i be multiplication by 2 on supported components, j reduction on supported components, and k the zero map to its prescribed target Dp1,q(c). All off-support maps are zero. The shift (1,1) preserves support, and j has degree (0,0). At supported D, imi=2Z=kerj and imk=0=keri; at supported E, imj=E=kerk. At off-support targets each required image and kernel is zero, including any zero map from a supported source. Thus these are initial exact couples with exactly the degrees in [F1].

F1F2step 1.1
3.1

To specify the underlying long exact sequences without dropping zero terms, fix any integer a. Following i,j,k in the c-couple gives, for every integer m, the consecutive terms Da,cam(c)iDa+1,cam1(c)jEa+1,cam1(c)kDa,cam1(c). The last term is the first term for m+1. Assign the first three terms sequence positions 3m,3m+1,3m+2. Their total bidegree is cm, so they are nonzero exactly when m=0. Forgetting bidegrees therefore gives exactly the sequence L of step 1.1, for both c=0 and c=1, for every a. In particular the zero target of each supported k remains a zero term. No sum of the indexed families is being taken.

step 1.1step 2.1
4.1

The two E1 pages differ: E0,0(0)=Z/2 whereas E0,0(1)=0. Hence they cannot be isomorphic by bidegree-zero maps. Even the displayed collection of underlying long exact sequences is identical in the two constructions, while their specified first spectral pages are different. Thus the ungraded sequence does not determine the specified homological exact-couple spectral sequence; bidegree allocation is essential extra data. This asserts neither failure of ungraded exactness nor a convergence statement, and uses no choice.

F1F2step 3.1

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

3 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