Revision #1517 → #1787 · back to history
modifiedReal scalar field15ac0c6e76a4
| Field | From #1517 | To #1787 |
|---|
| anchors | [{"section":"Classical fields","snippet":"The simplest classical field is a real scalar field"},{"type":"math_alttext","value":"{\\displaystyle L=\\int d^{3}x\\,{\\mathcal {L}}=\\int d^{3}x\\,\\left[{\\frac {1}{2}}{\\dot {\\phi }}^{2}-{\\frac {1}{2}}(\\nabla \\phi )^{2}-{\\frac {1}{2}}m^{2}\\phi ^{2}\\right],}"},{"type":"math_alttext","value":"{\\displaystyle {\\frac {\\partial }{\\partial t}}\\left[{\\frac {\\partial {\\mathcal {L}}}{\\partial (\\partial \\phi /\\partial t)}}\\right]+\\sum _{i=1}^{3}{\\frac {\\partial }{\\partial x^{i}}}\\left[{\\frac {\\partial {\\mathcal {L}}}{\\partial (\\partial \\phi /\\partial x^{i})}}\\right]-{\\frac {\\partial {\\mathcal {L}}}{\\partial \\phi }}=0,}"},{"type":"math_alttext","value":"{\\displaystyle \\left({\\frac {\\partial ^{2}}{\\partial t^{2}}}-\\nabla ^{2}+m^{2}\\right)\\phi =0.}"}] | — |
modifiedKlein–Gordon equationc280c7286a94
| Field | From #1517 | To #1787 |
|---|
| anchors | [{"section":"Classical fields","snippet":"This is known as the Klein–Gordon equation"},{"type":"math_alttext","value":"{\\displaystyle L=\\int d^{3}x\\,{\\mathcal {L}}=\\int d^{3}x\\,\\left[{\\frac {1}{2}}{\\dot {\\phi }}^{2}-{\\frac {1}{2}}(\\nabla \\phi )^{2}-{\\frac {1}{2}}m^{2}\\phi ^{2}\\right],}"},{"type":"math_alttext","value":"{\\displaystyle {\\frac {\\partial }{\\partial t}}\\left[{\\frac {\\partial {\\mathcal {L}}}{\\partial (\\partial \\phi /\\partial t)}}\\right]+\\sum _{i=1}^{3}{\\frac {\\partial }{\\partial x^{i}}}\\left[{\\frac {\\partial {\\mathcal {L}}}{\\partial (\\partial \\phi /\\partial x^{i})}}\\right]-{\\frac {\\partial {\\mathcal {L}}}{\\partial \\phi }}=0,}"},{"type":"math_alttext","value":"{\\displaystyle \\left({\\frac {\\partial ^{2}}{\\partial t^{2}}}-\\nabla ^{2}+m^{2}\\right)\\phi =0.}"}] | — |
| note | A grep for Klein–Gordon finds nothing; this relativistic wave equation is not in Mathlib. | All `Klein` matches in Mathlib refer to the Klein four-group; the Klein–Gordon equation is not formalized. |
modifiedNormal mode decomposition3ddc5829ad0b
| Field | From #1517 | To #1787 |
|---|
| anchors | [{"section":"Classical fields","snippet":"so its solutions can be expressed as a sum of normal modes"},{"type":"math_alttext","value":"{\\displaystyle \\phi (\\mathbf {x} ,t)=\\int {\\frac {d^{3}p}{(2\\pi )^{3}}}{\\frac {1}{\\sqrt {2\\omega _{\\mathbf {p} }}}}\\left(a_{\\mathbf {p} }e^{-i\\omega _{\\mathbf {p} }t+i\\mathbf {p} \\cdot \\mathbf {x} }+a_{\\mathbf {p} }^{*}e^{i\\omega _{\\mathbf {p} }t-i\\mathbf {p} \\cdot \\mathbf {x} }\\right),}"},{"type":"math_alttext","value":"{\\displaystyle \\omega _{\\mathbf {p} }={\\sqrt {|\\mathbf {p} |^{2}+m^{2}}}.}"}] | — |
modifiedCreation and annihilation operators0f81cf85b97d
| Field | From #1517 | To #1787 |
|---|
| anchors | [{"section":"Canonical quantization","snippet":"are replaced by the annihilation operator"},{"type":"math_alttext","value":"{\\displaystyle {\\hat {x}}(t)={\\frac {1}{\\sqrt {2\\omega }}}{\\hat {a}}e^{-i\\omega t}+{\\frac {1}{\\sqrt {2\\omega }}}{\\hat {a}}^{\\dagger }e^{i\\omega t}.}"},{"type":"math_alttext","value":"{\\displaystyle \\left[{\\hat {a}},{\\hat {a}}^{\\dagger }\\right]=1.}"},{"type":"math_alttext","value":"{\\displaystyle {\\hat {H}}=\\hbar \\omega {\\hat {a}}^{\\dagger }{\\hat {a}}+{\\frac {1}{2}}\\hbar \\omega .}"},{"type":"math_alttext","value":"{\\displaystyle {\\hat {a}}|0\\rangle =0}"},{"type":"math_alttext","value":"{\\displaystyle |n\\rangle \\propto \\left({\\hat {a}}^{\\dagger }\\right)^{n}|0\\rangle .}"}] | — |
modifiedVacuum stateb2ce29f977e5
| Field | From #1517 | To #1787 |
|---|
| anchors | [{"section":"Canonical quantization","snippet":"which is the lowest energy state, is defined by"},{"type":"math_alttext","value":"{\\displaystyle {\\hat {x}}(t)={\\frac {1}{\\sqrt {2\\omega }}}{\\hat {a}}e^{-i\\omega t}+{\\frac {1}{\\sqrt {2\\omega }}}{\\hat {a}}^{\\dagger }e^{i\\omega t}.}"},{"type":"math_alttext","value":"{\\displaystyle \\left[{\\hat {a}},{\\hat {a}}^{\\dagger }\\right]=1.}"},{"type":"math_alttext","value":"{\\displaystyle {\\hat {H}}=\\hbar \\omega {\\hat {a}}^{\\dagger }{\\hat {a}}+{\\frac {1}{2}}\\hbar \\omega .}"},{"type":"math_alttext","value":"{\\displaystyle {\\hat {a}}|0\\rangle =0}"},{"type":"math_alttext","value":"{\\displaystyle |n\\rangle \\propto \\left({\\hat {a}}^{\\dagger }\\right)^{n}|0\\rangle .}"}] | — |
modifiedFock space6799fe2438c5
| Field | From #1517 | To #1787 |
|---|
| note | A grep for Fock space returns nothing; Fock space is not defined in Mathlib. | Grep finds no Fock-space matches in Mathlib. |
modifiedQuartic interaction termdb471a4a2a22
| Field | From #1517 | To #1787 |
|---|
| anchors | [{"section":"Canonical quantization","snippet":"a quartic interaction term could be introduced to the Lagrangian of the real scalar field"},{"type":"math_alttext","value":"{\\displaystyle {\\mathcal {L}}={\\frac {1}{2}}(\\partial _{\\mu }\\phi )\\left(\\partial ^{\\mu }\\phi \\right)-{\\frac {1}{2}}m^{2}\\phi ^{2}-{\\frac {\\lambda }{4!}}\\phi ^{4},}"}] | — |
modifiedFeynman path integral6cfd47ebaf18
| Field | From #1517 | To #1787 |
|---|
| anchors | [{"section":"Path integrals","snippet":"the above product of integrals becomes the Feynman path integral"},{"type":"math_alttext","value":"{\\displaystyle \\langle \\phi _{F}|e^{-iHT}|\\phi _{I}\\rangle =\\int d\\phi _{1}\\int d\\phi _{2}\\cdots \\int d\\phi _{N-1}\\,\\langle \\phi _{F}|e^{-iHT/N}|\\phi _{N-1}\\rangle \\cdots \\langle \\phi _{2}|e^{-iHT/N}|\\phi _{1}\\rangle \\langle \\phi _{1}|e^{-iHT/N}|\\phi _{I}\\rangle .}"},{"type":"math_alttext","value":"{\\displaystyle \\langle \\phi _{F}|e^{-iHT}|\\phi _{I}\\rangle =\\int {\\mathcal {D}}\\phi (t)\\,\\exp \\left\\{i\\int _{0}^{T}dt\\,L\\right\\},}"},{"type":"math_alttext","value":"{\\displaystyle \\phi (0)=\\phi _{I},\\quad \\phi (T)=\\phi _{F}.}"}] | — |
modifiedTwo-point correlation functionbe65d27f3870
| Field | From #1517 | To #1787 |
|---|
| anchors | [{"section":"Two-point correlation function","snippet":"and goes by multiple names, like the two-point propagator"},{"type":"math_alttext","value":"{\\displaystyle \\langle 0|T\\{\\phi (x)\\phi (y)\\}|0\\rangle \\quad {\\text{or}}\\quad \\langle \\Omega |T\\{\\phi (x)\\phi (y)\\}|\\Omega \\rangle }"}] | — |
modifiedFeynman propagatoraa246d701741
| Field | From #1517 | To #1787 |
|---|
| anchors | [{"section":"Two-point correlation function","snippet":"The free two-point function, also known as the Feynman propagator"},{"type":"math_alttext","value":"{\\displaystyle \\langle 0|T\\{\\phi (x)\\phi (y)\\}|0\\rangle \\equiv D_{F}(x-y)=\\lim _{\\epsilon \\to 0}\\int {\\frac {d^{4}p}{(2\\pi )^{4}}}{\\frac {i}{p_{\\mu }p^{\\mu }-m^{2}+i\\epsilon }}e^{-ip_{\\mu }(x^{\\mu }-y^{\\mu })}.}"}] | — |
modifiedWick's theoremde6a1455ff4a
| Field | From #1517 | To #1787 |
|---|
| anchors | [{"section":"Two-point correlation function","snippet":"Wick's theorem further reduce any"},{"type":"math_alttext","value":"{\\displaystyle {\\begin{aligned}\\langle 0|T\\{\\phi (x_{1})\\phi (x_{2})\\phi (x_{3})\\phi (x_{4})\\}|0\\rangle &=\\langle 0|T\\{\\phi (x_{1})\\phi (x_{2})\\}|0\\rangle \\langle 0|T\\{\\phi (x_{3})\\phi (x_{4})\\}|0\\rangle \\\\&+\\langle 0|T\\{\\phi (x_{1})\\phi (x_{3})\\}|0\\rangle \\langle 0|T\\{\\phi (x_{2})\\phi (x_{4})\\}|0\\rangle \\\\&+\\langle 0|T\\{\\phi (x_{1})\\phi (x_{4})\\}|0\\rangle \\langle 0|T\\{\\phi (x_{2})\\phi (x_{3})\\}|0\\rangle .\\end{aligned}}}"}] | — |
| note | The only "Wick" matches are an author's name; Wick's/Isserlis' theorem is not formalized in Mathlib. | Wick's/Isserlis' theorem is not formalized in Mathlib. |
modifiedConnected diagrams822a8746c72a
| Field | From #1517 | To #1787 |
|---|
| anchors | [{"section":"Feynman diagram","snippet":"Connected diagrams are those in which every vertex is connected to an external point through lines"},{"type":"math_alttext","value":"{\\displaystyle \\langle \\Omega |T\\{\\phi (x_{1})\\cdots \\phi (x_{n})\\}|\\Omega \\rangle }"}] | — |
modifiedRenormalized perturbation theory7c5c9bf0fbdf
| Field | From #1517 | To #1787 |
|---|
| anchors | [{"section":"Renormalization","snippet":"A different approach, called renormalized perturbation theory"},{"type":"math_alttext","value":"{\\displaystyle \\phi =Z^{1/2}\\phi _{r},}"},{"type":"math_alttext","value":"{\\displaystyle {\\mathcal {L}}={\\frac {1}{2}}(\\partial _{\\mu }\\phi _{r})(\\partial ^{\\mu }\\phi _{r})-{\\frac {1}{2}}m_{r}^{2}\\phi _{r}^{2}-{\\frac {\\lambda _{r}}{4!}}\\phi _{r}^{4}+{\\frac {1}{2}}\\delta _{Z}(\\partial _{\\mu }\\phi _{r})(\\partial ^{\\mu }\\phi _{r})-{\\frac {1}{2}}\\delta _{m}\\phi _{r}^{2}-{\\frac {\\delta _{\\lambda }}{4!}}\\phi _{r}^{4},}"},{"type":"math_alttext","value":"{\\displaystyle \\delta _{Z}=Z-1,\\quad \\delta _{m}=m^{2}Z-m_{r}^{2},\\quad \\delta _{\\lambda }=\\lambda Z^{2}-\\lambda _{r}}"}] | — |
modifiedQED beta functionbedcc55c8b10
| Field | From #1517 | To #1787 |
|---|
| anchors | [{"section":"Renormalization group","snippet":"namely the elementary charge e , has the following β function"},{"type":"math_alttext","value":"{\\displaystyle \\beta (e)\\equiv {\\frac {1}{\\Lambda }}{\\frac {de}{d\\Lambda }}={\\frac {e^{3}}{12\\pi ^{2}}}+O{\\mathord {\\left(e^{5}\\right)}},}"}] | — |
modifiedAsymptotic freedom (QCD)10012f54799f
| Field | From #1517 | To #1787 |
|---|
| anchors | [{"section":"Renormalization group","snippet":"a phenomenon known as asymptotic freedom"},{"type":"math_alttext","value":"{\\displaystyle \\beta (g)\\equiv {\\frac {1}{\\Lambda }}{\\frac {dg}{d\\Lambda }}={\\frac {g^{3}}{16\\pi ^{2}}}\\left(-11+{\\frac {2}{3}}N_{f}\\right)+O{\\mathord {\\left(g^{5}\\right)}},}"}] | — |
modifiedQED Lagrangian7c32227aed88
| Field | From #1517 | To #1787 |
|---|
| anchors | [{"section":"Other theories","snippet":"quantum electrodynamics contains a Dirac field ψ representing the electron field"},{"type":"math_alttext","value":"{\\displaystyle {\\mathcal {L}}={\\bar {\\psi }}\\left(i\\gamma ^{\\mu }\\partial _{\\mu }-m\\right)\\psi -{\\frac {1}{4}}F_{\\mu \\nu }F^{\\mu \\nu }-e{\\bar {\\psi }}\\gamma ^{\\mu }\\psi A_{\\mu },}"}] | — |
modifiedGauge symmetry2966ff5c7ef0
| Field | From #1517 | To #1787 |
|---|
| anchors | [{"section":"Gauge symmetry","snippet":"then the transformation is referred to as a gauge symmetry of the theory"},{"type":"math_alttext","value":"{\\displaystyle \\psi (x)\\to e^{i\\alpha (x)}\\psi (x),\\quad A_{\\mu }(x)\\to A_{\\mu }(x)+ie^{-1}e^{-i\\alpha (x)}\\partial _{\\mu }e^{i\\alpha (x)},}"}] | — |
modifiedU(1) gauge symmetry of QED5e2ea1adae7b
| Field | From #1517 | To #1787 |
|---|
| anchors | [{"section":"Gauge symmetry","snippet":"thus QED is said to have U(1) gauge symmetry"},{"type":"math_alttext","value":"{\\displaystyle \\psi (x)\\to e^{i\\alpha (x)}\\psi (x),\\quad A_{\\mu }(x)\\to A_{\\mu }(x)+ie^{-1}e^{-i\\alpha (x)}\\partial _{\\mu }e^{i\\alpha (x)},}"}] | — |
| mathlib.match_kind | — | invocation |
| note | The gauge group U(1) exists as `Circle` (and `Matrix.unitaryGroup`), but the gauge symmetry of QED itself is not formalized. | The gauge group U(1) exists as `Circle` (confirmed via decl_exists), but the gauge symmetry of QED itself is not formalized. |
modifiedSU(3) gauge symmetry of QCDad11cc17dbc9
| Field | From #1517 | To #1787 |
|---|
| anchors | [{"section":"Gauge symmetry","snippet":"is a non-Abelian gauge theory with an SU(3) gauge symmetry"},{"type":"math_alttext","value":"{\\displaystyle {\\mathcal {L}}=i{\\bar {\\psi }}^{i}\\gamma ^{\\mu }(D_{\\mu })^{ij}\\psi ^{j}-{\\frac {1}{4}}F_{\\mu \\nu }^{a}F^{a,\\mu \\nu }-m{\\bar {\\psi }}^{i}\\psi ^{i},}"},{"type":"math_alttext","value":"{\\displaystyle D_{\\mu }=\\partial _{\\mu }-igA_{\\mu }^{a}t^{a},}"},{"type":"math_alttext","value":"{\\displaystyle F_{\\mu \\nu }^{a}=\\partial _{\\mu }A_{\\nu }^{a}-\\partial _{\\nu }A_{\\mu }^{a}+gf^{abc}A_{\\mu }^{b}A_{\\nu }^{c},}"},{"type":"math_alttext","value":"{\\displaystyle \\psi ^{i}(x)\\to U^{ij}(x)\\psi ^{j}(x),\\quad A_{\\mu }^{a}(x)t^{a}\\to U(x)\\left[A_{\\mu }^{a}(x)t^{a}+ig^{-1}\\partial _{\\mu }\\right]U^{\\dagger }(x),}"},{"type":"math_alttext","value":"{\\displaystyle U(x)=e^{i\\alpha (x)^{a}t^{a}}.}"}] | — |
| mathlib.match_kind | — | invocation |
| note | The gauge group SU(3) exists as `Matrix.specialUnitaryGroup`, but QCD as a gauge theory with this symmetry is not formalized. | The gauge group SU(3) exists as `Matrix.specialUnitaryGroup` (confirmed via decl_exists), but QCD as a gauge theory with this symmetry is not formalized. |
modifiedNoether's theorem547e7a7a7f08
| Field | From #1517 | To #1787 |
|---|
| note | Mathlib has Noetherian rings but not the physics Noether's theorem relating symmetries to conservation laws. | All `Noether` matches in Mathlib refer to Noetherian rings/modules, not the physics theorem relating symmetries to conservation laws. |
modifiedLinear sigma model0534655ff205
| Field | From #1517 | To #1787 |
|---|
| anchors | [{"section":"Spontaneous symmetry-breaking","snippet":"consider a linear sigma model containing N real scalar fields"},{"type":"math_alttext","value":"{\\displaystyle {\\mathcal {L}}={\\frac {1}{2}}\\left(\\partial _{\\mu }\\phi ^{i}\\right)\\left(\\partial ^{\\mu }\\phi ^{i}\\right)+{\\frac {1}{2}}\\mu ^{2}\\phi ^{i}\\phi ^{i}-{\\frac {\\lambda }{4}}\\left(\\phi ^{i}\\phi ^{i}\\right)^{2},}"},{"type":"math_alttext","value":"{\\displaystyle \\phi ^{i}\\to R^{ij}\\phi ^{j},\\quad R\\in \\mathrm {O} (N).}"},{"type":"math_alttext","value":"{\\displaystyle \\phi _{0}^{i}\\phi _{0}^{i}={\\frac {\\mu ^{2}}{\\lambda }}.}"},{"type":"math_alttext","value":"{\\displaystyle \\phi _{0}^{i}=\\left(0,\\cdots ,0,{\\frac {\\mu }{\\sqrt {\\lambda }}}\\right).}"},{"type":"math_alttext","value":"{\\displaystyle \\phi ^{i}(x)=\\left(\\pi ^{1}(x),\\cdots ,\\pi ^{N-1}(x),{\\frac {\\mu }{\\sqrt {\\lambda }}}+\\sigma (x)\\right),}"},{"type":"math_alttext","value":"{\\displaystyle {\\mathcal {L}}={\\frac {1}{2}}\\left(\\partial _{\\mu }\\pi ^{k}\\right)\\left(\\partial ^{\\mu }\\pi ^{k}\\right)+{\\frac {1}{2}}\\left(\\partial _{\\mu }\\sigma \\right)\\left(\\partial ^{\\mu }\\sigma \\right)-{\\frac {1}{2}}\\left(2\\mu ^{2}\\right)\\sigma ^{2}-{\\sqrt {\\lambda }}\\mu \\sigma ^{3}-{\\sqrt {\\lambda }}\\mu \\pi ^{k}\\pi ^{k}\\sigma -{\\frac {\\lambda }{2}}\\pi ^{k}\\pi ^{k}\\sigma ^{2}-{\\frac {\\lambda }{4}}\\left(\\pi ^{k}\\pi ^{k}\\right)^{2},}"}] | — |
modifiedQFT in curved spacetime653916b0c35c
| Field | From #1517 | To #1787 |
|---|
| anchors | [{"section":"Other spacetimes","snippet":"For QFTs in curved spacetime on the other hand, a general metric"},{"type":"math_alttext","value":"{\\displaystyle A_{\\mu }A^{\\mu }=\\eta _{\\mu \\nu }A^{\\mu }A^{\\nu },\\quad \\partial _{\\mu }\\phi \\partial ^{\\mu }\\phi =\\eta ^{\\mu \\nu }\\partial _{\\mu }\\phi \\partial _{\\nu }\\phi ,}"},{"type":"math_alttext","value":"{\\displaystyle A_{\\mu }A^{\\mu }=g_{\\mu \\nu }A^{\\mu }A^{\\nu },\\quad \\partial _{\\mu }\\phi \\partial ^{\\mu }\\phi =g^{\\mu \\nu }\\partial _{\\mu }\\phi \\partial _{\\nu }\\phi ,}"},{"type":"math_alttext","value":"{\\displaystyle {\\mathcal {L}}={\\sqrt {|g|}}\\left({\\frac {1}{2}}g^{\\mu \\nu }\\nabla _{\\mu }\\phi \\nabla _{\\nu }\\phi -{\\frac {1}{2}}m^{2}\\phi ^{2}\\right),}"}] | — |
| note | No Lorentzian/curved-spacetime QFT is formalized; Mathlib's "Minkowski" refers to inequalities and geometry of numbers. | No Lorentzian/curved-spacetime QFT is formalized; Mathlib's `Minkowski` refers to inequalities and geometry of numbers. |
modifiedChern–Simons theoryf9d5915ae4ee
| Field | From #1517 | To #1787 |
|---|
| note | Chern–Simons theory is not formalized in Mathlib (the only "Chern" matches are Chernoff bounds). | Chern–Simons theory is not formalized in Mathlib (the only `Chern` matches are Chernoff bounds). |
addedDirac equatione9b34d250665
addedFaddeev–Popov gauge fixinga07284e15ddb
addedBRST quantizatione7b9d07c2e93
addedCPT theorem6c7be069d034
addedSpin–statistics theoremb2aeebfd7575
addedLagrangian density5150d4b19242
addedEuler–Lagrange equationd82bd021aea9
addedCanonical quantizationc7c7f03c30e3
addedNon-Abelian gauge theory156bab89d457