Alphabeta Math
LemmaStatement: 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.

Disk-pair cohomology over an arbitrary commutative ring

Statement

For every commutative ring R and n0, Hq(Dn,Sn1;R){Rq=n,0qn. where S1=. The iterated connecting maps, with the ordered coordinate orientation, normalize the element corresponding to 1R. Every linear automorphism of the disk pair acts on the top group by multiplication by a unit. The calculation is choice-free.

Facts & Assumptions

Given: A commutative ring R and n0.

[F1]

Singular cohomology satisfies the Eilenberg Steenrod cohomology axioms gives choice-free homotopy invariance, dimension, exactness, excision, and finite additivity for singular cohomology.

[F2]

Mayer vietoris sequence in singular cohomology gives the natural two-open Mayer–Vietoris sequence.

[F3]

Long exact sequence of a pair in singular cohomology gives the natural disk/sphere pair sequence.

Proof

technique · direct suspension recursion and the pair sequence
1.1

For n=0, (D0,S1)=(,), so [F1]'s dimension axiom gives R in degree zero and zero in every other degree. Its distinguished element is 1R.

F1
1.2

The two points of S0 have H0(S0;R)=RR by finite additivity. The reduced group is the cokernel of the diagonal constants and is freely generated by (1,0) modulo the diagonal, hence is R; all other reduced groups vanish.

F1
2.1

Suppose m1 and the reduced cohomology of Sm1 is R in degree m1 and zero otherwise. Cover Sm by two slightly enlarged hemispheres. Each is contractible and their intersection deformation retracts onto the equator Sm1. In the Mayer–Vietoris sequence [F2], the map on degree-zero constants is the diagonal-difference map and the higher groups of the hemispheres vanish. Exactness therefore makes the connector an isomorphism H~q1(Sm1;R)H~q(Sm;R) in every q. Thus the asserted sphere calculation propagates from step 1.2.

F1F2step 1.2
3.1

For n1, Dn is contractible and Sn1 is nonempty. The pair sequence [F3], together with the sphere calculation of step 2.1, identifies Hq(Dn,Sn1;R) naturally with H~q1(Sn1;R). It is therefore R exactly at q=n and zero otherwise. Following 1R through the ordered hemisphere connectors fixes the stated coordinate generator; reversing one ordered coordinate reverses the first difference and hence negates that generator.

F1F2F3step 1.1step 1.2step 2.1
4.1

A linear automorphism is a homeomorphism of the pair, so functoriality in [F1] makes its top-degree action an R-module automorphism of the rank-one module calculated in step 3.1. Such an automorphism is multiplication by a unique unit: the image of 1 is u, and the inverse image supplies v with uv=1. At n=0 this is the identity. Empty boundary, zero ring, ranks zero and one, both hemisphere endpoints, repeated/degenerate cover pieces, and the two possible coordinate signs are all included above. Only a fixed finite cover and its canonical maps occur, so neither arbitrary additivity nor AC is used.

F1F2F3step 1.1step 1.2step 2.1step 3.1

Depends on

Used by

Dependency tree · two levels

18 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