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 one-variable BV algebra and a classical master solution
Example
Let with and . Define and let . Then is a BV algebra in the degree- convention. The element satisfies the classical master equation and its Hamiltonian differential is
Facts & Assumptions
Given: The BV definition, odd-Poisson theorem, CME convention, and square-zero consequence in BV algebra with a degree-one generator, The derived BV bracket is an odd Poisson bracket, Classical and formal quantum master equations, and A classical master solution defines a square-zero differential.
BV algebra with a degree-one generator: the order condition is , with and .
Classical and formal quantum master equations: for , the classical master equation is .
A classical master solution defines a square-zero differential: any degree-zero classical master solution induces the square-zero map .
Verification
Every element is with and ; the polynomial quotient multiplication is associative and the assigned degrees make it graded commutative. For homogeneous factors, the ordinary product rule gives the Leibniz rule for ; direct expansion gives , , and , so is a degree- graded derivation. Thus has degree , , and .
For a homogeneous derivation , ; the composition identity gives . Commuting once more yields , a multiplication operator. Multiplication operators gradedly commute, so the third commutator with is zero and [F1]'s order condition holds.
Direct substitution in [F1] gives because , , and . Hence and ; also and depend only on , so by the same formula. Thus satisfies the CME [F2].
Step 2.2 gives , which is independent of and is killed by . Therefore directly, in agreement with [F3].
Depends on
Used by
Nothing in the library uses this result yet.
Dependency tree · one level
4 results within one dependency step 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
- Ezra Getzler, Batalin–Vilkovisky algebras and two-dimensional topological field theories, arXiv:hep-th/9212043v3 (standard reference, not scraped)
- Albert Schwarz, Geometry of Batalin–Vilkovisky quantization, arXiv:hep-th/9205088v1 (standard reference, not scraped)