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.
A C4 coboundary changes the pentagonator and is gauged away
Example
Write additively, with elements . Define the normalized 3-cochain Let , with the multiplicative coboundary convention in A normalized 3-cochain gives the gauge equivalence of 2Vect_G^omega.
Facts & Assumptions
Given: The group , the normalized cochain , and the group-cochain convention in the A-page gauge theorem.
A normalized 3-cochain gives the gauge equivalence of 2Vect_G^omega: A normalized coboundary changes the pentagonator by a monoidal 2-equivalence; its value is
Group and abelian group: A group has associative multiplication, identity, and inverses.
Verification
The cochain is normalized because it equals whenever any input is . At in , the five factors in [F1] are respectively , , , , and . Thus , so the resulting 4-cochain is not the constant cochain.
If , the first two factors in are equal with opposite exponents and the remaining three have an input , so all remaining normalized values are . If , the second and third factors cancel and the other factors are normalized; if , the third and fourth factors cancel and the other factors are normalized; if , the fourth and fifth factors cancel and the other factors are normalized. Thus is normalized. Applying the degree-four coboundary to this expression gives a product of the 30 composites from the six degree-four faces and five degree-three faces. For each , the simplicial face identity pairs two occurrences with opposite exponents; the interior face identities use associativity in , and the endpoint identities delete the same first or last entry. All 15 pairs cancel, so and is a 4-cocycle.
Theorem [F1] applies to and with cochain (whose coboundary is ), and gives a monoidal 2-equivalence . The example checks a nonconstant representative and its coherent untwisting; it does not assert a nonzero class in .
Depends on
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
8 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
- Décoppet and Yu, Fiber 2-Functors and Tambara-Yamagami Fusion 2-Categories, §2.1 (standard reference, not scraped)
- Douglas and Reutter, Fusion 2-Categories and a State-Sum Invariant for 4-Manifolds, Construction 2.1.16 (standard reference, not scraped)