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

Mapping cone of a degree d circle map

Example

For dZ let fd:R/ZR/Z, fd([t])=[dt]. Its unreduced mapping cone has H0=Z,H1=Z/dZ,H2=ker(d:ZZ),Hj=0 (j>2), and π1Z/dZ. For d=0, π1=H1=H2=Z; for d=±1 the fundamental group and reduced homology vanish. All homology coefficients here are integers.

Facts & Assumptions

[F1]

The unreduced cone attaches the cone on the source circle to the target. Mapping cylinder and mapping cone

[F2]

Degree is the integral sphere-homology multiplier. Degree of a self map of an oriented sphere

[F3]

Local degree is the multiplier on the local oriented punctured-pair groups. Local degree at an isolated preimage

[F4]

Degree is the sum over a finite fibre. Global sphere degree is the sum of local degrees

[F5]

In dimension one identity, constant and reflection degrees are 1,0,−1. Degree of identity constant reflection and antipodal sphere maps

[F6]

The cellular boundary coefficient is the attaching incidence degree. Cellular boundary is the incidence degree matrix

[F7]

Cellular homology equals singular homology. Cellular homology computes singular homology

[F8]

An open path-connected cover with path-connected intersection gives the fundamental-group pushout. Seifert–van Kampen identifies the fundamental group with a group pushout

[F9]

The standard winding class identifies π1(R/Z) with Z. Deg:π1(R/Z,[0])(Z,+) is an isomorphism

Verification

Given: The spaces, maps, and hypotheses in the statement above.

1.1

The map h([t])=e2πit identifies the quotient circle with the unit circle: it is a continuous bijection, and inverse angular charts are continuous on arcs, including arcs crossing the quotient seam. Give it the counterclockwise orientation. Then hfdh1(z)=zd. For d>0 the fibre over 1 is e2πik/d, 0≤k<d. In positive angular coordinates at each preimage and at 1, the map is u↦du. Interpolating the positive coefficient d to 1 on a sufficiently small arc gives a homotopy of punctured pairs. Thus F3 identifies its local multiplier with that of an orientation-preserving circle rotation, namely +1 by the identity and rotation homotopy, or the singleton-fibre case of F4. For d<0 the same calculation reduces to angular reflection, whose degree is −1 by the circle clause of F5. Hence F4 gives degree d for every nonzero d. For d=0 the map is constant and F5 gives degree zero.

F2F3F4F5
1.2

For the fundamental group take U to be the target circle together with cone heights s<2/3, and V to be cone heights s>1/3 including its tip. They are open in the quotient, their union is the cone space, and their intersection is a circle times (1/3,2/3). U retracts to the target by decreasing height, V contracts to the tip by increasing height, and the intersection retracts to its circle. All are path-connected. Choose the basepoint at source [0], height 1/2 and transport to the target vertex along the height segment. The overlap generator maps to a^d in π1(U) by F9 and trivially in π1(V). Thus F8 gives the presentation aad=1=Z/dZ. This calculation does not infer H1 from π1.

F1F8F9
2.1

The cone on the source circle is the disk via [z,s](1s)z; its boundary at s=0 attaches by f_d. Thus the mapping cone has one vertex, one loop edge and one 2-cell. F2 and step 1.1 identify its attaching coefficient in F6 as d, so its cellular complex is 0ZdZ0Z0. Direct kernels and images give the stated H0,H1,H2 and vanishing above dimension two, and F7 identifies them with singular homology.

F1F2F6F7step 1.1
3.1

When d=0 the cellular map is zero, so H1=H2=Z and the group relation is empty. When d=±1 the cellular map is an isomorphism and the group relation kills a, giving the claimed vanishings. For instance d=−2 gives H1=π1=Z/2Z and H2=0. No inference of contractibility from these invariants is made.

step 2.1step 1.2

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

39 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