Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-05
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.

The simplicial-to-singular chain map commutes with boundaries

Statement

For every simplicial complex K equipped with a total order on its vertices and every n≥1, ∂singΦn=Φn−1∂simp:Cnsimp(K)→Cn−1sing(∣K∣;Z). In degree 0, both boundaries are zero maps to 0.

Facts & Assumptions

Given: A simplicial complex K with a total order on its vertices and an integer n≥0.

[L1]

Φn sends an oriented simplex to the sign of its increasing representative times the corresponding affine characteristic singular simplex (The degreewise simplicial-to-singular homomorphisms).

[L2]

The singular boundary is the alternating sum of affine face restrictions (The singular boundary operator).

[L3]

The simplicial boundary is the alternating sum of the oriented codimension-one faces (Simplicial chain groups and the boundary operator).

Proof

technique · direct
1.1L2L3given

If n=0, then both ∂sing and ∂simp are zero maps in degree 0, so the degree-zero claim is immediate.

1.2L1given

Assume n≥1 and let σ=[v0,…,vn] be the increasing representative of an oriented simplex of K. By [L1], the singular chain Φn(σ) is the affine characteristic simplex χ[v0,…,vn]. Restricting along the face map δi therefore produces the affine characteristic simplex of the face [v0,…,v^i,…,vn], listed in the induced increasing order.

2.1L1L2L3step 1.1step 1.2algebra∎

Applying [L2] and [L3] to step 1.2 gives ∂singΦn(σ)=∑i=0n(−1)iΦn−1([v0,…,v^i,…,vn])=Φn−1∂simp(σ) for the increasing representative. The same overall orientation sign ε(τ) from [L1] multiplies both sides for an arbitrary oriented simplex τ, so the identity holds on every generator and hence on all simplicial chains by linearity; step 1.1 handles degree 0.

Depends on

Used by

Dependency tree · two levels

7 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