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

Integral homology of a finite cyclic group

Example

For Cm=ggm=1, m1, with trivial integral coefficients, H0(Cm;Z)=Z, H2j+1(Cm;Z)=Z/mZ for j0, and H2j(Cm;Z)=0 for j1. In particular multiplication by m kills positive homology.

Facts & Assumptions

Given: m is a positive integer; coefficients are trivial integers; the derived-functor convention carries DC and supplied resolutions.

[F1]

The order of a finite group annihilates its positive integral homology. (Positive integral homology is annihilated by the group order).

[F2]

Group homology is the homology obtained by tensoring the supplied projective resolution with the right trivial module (Group homology as a derived functor).

[F3]

Under DC, any two projective resolutions of the same object are chain-homotopy equivalent over that object (Projective resolutions of the same object are homotopy equivalent over that object).

Verification

1.1

Put R=ZCm and N=1+g++gm1. Use one copy of R in each nonnegative degree, augmentation ϵ(aigi)=ai, differential multiplication by g1 in odd degrees and by N in positive even degrees. Since (g1)N=gm1=0 and ϵ(g1)=0, this is an augmented chain complex.

algebra
2.1

For a=i=0m1aigi, the coefficient of gi in (g1)a is ai1ai (indices modulo m). Thus its kernel consists exactly of constant coefficient vectors, namely ZN. Also Na=(iai)N, so the image of multiplication by N is ZN and its kernel is kerϵ. If ai=0, then a=i=1m1ai(gi1)=(g1)i=1m1ai(1++gi1). Hence kerϵ=(g1)R, proving exactness in every degree. This also covers m=1: the two maps are zero and identity and the displayed sums are empty.

step 1.1algebra
3.1

Each term is free, so step 2.1 makes this complex PZ a projective resolution of the trivial left R-module. Let PsupZ be the supplied resolution used in [F2]. By [F3], P and Psup are chain-homotopy equivalent over Z. The additive functor ZR carries the comparison maps and their homotopies to comparison maps and homotopies, so H(ZRP)H(ZRPsup)=H(Cm;Z). Tensoring P makes multiplication by g1 zero and multiplication by N multiplication by m. Thus degree zero is Z, every odd degree has kernel Z modulo mZ, and every positive even degree has kernel of m:ZZ, which is zero.

F2F3step 2.1algebra
4.1

Multiplication by m on Z/mZ is zero, and on the zero groups it is zero. This explicitly verifies the conclusion of F1. Degree zero is excluded: m10 in Z. For m=1 all positive groups vanish.

F1step 3.1algebra

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

11 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