Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck pass
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.

Cellular boundary is the incidence degree matrix

Statement

Let X be a CW complex. For n≥1, in the integral cellular chain groups with the chosen cell orientations, dneαn=∑β[eαn:eβn−1]eβn−1.

Facts & Assumptions

Given: A CW complex X, integral cellular chains, and the chosen cell orientations; the differential is as in Cellular boundary from three consecutive skeleta.

Proof

technique · direct
1.1given

Project the three-skeleton connecting map defining dn to the summand of a fixed (n−1)-cell.

2.1step 1.1

For n≥2, first pass from Xn−1 to Xn−1/Xn−2 as required by the relative target of the cellular boundary, and then collapse all summand spheres except that of eβn−1. Equivalently, collapse the entire complement Xn−1∖eβn−1, including Xn−2. Naturality of the connecting homomorphism for the characteristic disk identifies the coefficient with the composite from its oriented boundary sphere to this quotient sphere. This is precisely the reduced-homology endomorphism in Incidence number of two CW cells, so its degree is [eαn:eβn−1].

3.1step 1.1step 2.1∎

For n=1, use a characteristic interval compatible with the chosen edge generator. Its connecting homomorphism is the singular boundary [v+]−[v−]. For each chosen vertex generator ev=εv[v], the identity [v]=εvev gives coefficient εv(1{v+=v}−1{v−=v}), exactly the incidence number of Incidence number of two CW cells. This includes negatively chosen zero-cell generators and gives zero when both endpoints coincide. The boundary is an element of a direct sum, so only finitely many coefficients are nonzero; equality of all its projections therefore proves the formula for every n≥1; separately, d0=0 by definition.

Depends on

Used by

Dependency tree · two levels

6 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