Skip to content

Further attempt to fix math rendering #17

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
KellyJDavis merged 1 commit into from
Jun 23, 2026
Merged

Further attempt to fix math rendering #17

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 2 additions & 1 deletion home_page/_layouts/default.html
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -17,6 +17,7 @@
{% else %}
<link rel="stylesheet" href="{{ 'assets/css/style.css?v=' | append: site.github.build_revision | relative_url }}">
{% endif %}
{% include mathjax.html %}
{% include head-custom.html %}
</head>

Expand Down Expand Up @@ -47,4 +48,4 @@ <h2 class="project-tagline">{{ page.description | default: site.description | de
</main>
</body>

</html>
</html>
9 changes: 5 additions & 4 deletions home_page/index.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -12,6 +12,7 @@ meta-twitter:card: summary
meta-twitter:title: AQFT in Lean
meta-viewport: width=device-width, initial-scale=1
title: Formalising AQFT in Lean
usemathjax: true
---

# AQFT in Lean
Expand Down Expand Up @@ -95,7 +96,7 @@ Only the content of Chapter 10 is formalised in Lean. This comprises:

**GNS Construction**
- Cauchy–Schwarz inequality for states
- Equivalence of the two descriptions of the left-ideal \$\$\mathcal{N}\$\$; \$\$\mathcal{N}\$\$ is a closed linear subspace
- Equivalence of the two descriptions of the left-ideal $$\mathcal{N}$$; $$\mathcal{N}$$ is a closed linear subspace
- Full GNS Construction Theorem (Hilbert space, \*-representation, cyclic vector, faithfulness, uniqueness up to unitary equivalence)
- Separating vector of a faithful state

Expand Down Expand Up @@ -127,9 +128,9 @@ Only the content of Chapter 10 is formalised in Lean. This comprises:
- Einstein Causality in a representation, curved spacetime (Theorem 93)

**KMS condition**
- Boundary coincidence for \$\$a = 1\$\$
- \$\$i\beta\$\$-periodic entire extension (strip Schwarz reflection)
- Strip-Liouville holds for \$\$\beta > 0\$\$
- Boundary coincidence for $$a = 1$$
- $$i\beta$$-periodic entire extension (strip Schwarz reflection)
- Strip-Liouville holds for $$\beta > 0$$
- KMS states are invariant (Theorem 83)
- Uniqueness on the strip from boundary values; uniqueness of the KMS correlation function
- A Killing flow induces a one-parameter automorphism group
Expand Down