Merge pull request #365 from HEPLean/JTS/QM

feat: Update Curated Notes
HEPLean · Mar 3, 2025 · 927c1f4 · 927c1f4
2 parents ed20ca3 + c0b962a
commit 927c1f4
Show file tree

Hide file tree

Showing 7 changed files with 87 additions and 121 deletions.
diff --git a/.github/ISSUE_TEMPLATE/NoteDocString.yml b/.github/ISSUE_TEMPLATE/NoteDocString.yml
@@ -0,0 +1,24 @@
+name: Note doc string
+description: Improvements to docstrings from curated notes
+title: "[doc-string]: "
+body:
+  - type: markdown
+    attributes:
+      value: |
+        Thanks for taking the time to suggest an improvement!
+  - type: input
+    id: name
+    attributes:
+      label: Name of result
+      description: What is the name of the result you are suggesting an improvement for?
+      placeholder:
+    validations:
+      required: true
+  - type: textarea
+    id: improvement
+    attributes:
+      label: Improvement
+      description: What is the improvement you are suggesting?
+      placeholder:
+    validations:
+      required: true
diff --git a/docs/CuratedNotes/HarmonicOscillator.html b/docs/CuratedNotes/HarmonicOscillator.html
@@ -1,105 +1,4 @@
 ---
-layout: default
+layout: curatedNote
+data_source: harmonicOscillator
 ---
-<style>
-  body {
-    color: black;
-  }
-</style>
-
-<link rel="stylesheet" href="https://cdnjs.cloudflare.com/ajax/libs/highlight.js/11.9.0/styles/default.min.css">
-<script src="https://cdnjs.cloudflare.com/ajax/libs/highlight.js/11.9.0/highlight.min.js"></script>
-<script type="text/javascript" charset="UTF-8"
-  src="../assets/css/lean.min.js"></script>
-<script>hljs.highlightAll();</script>
-<!--- Toggle background color. -->
-<script>
-let isDefaultBackground = true;
-function toggleDyslexiaMode() {
-  document.body.style.backgroundColor = isDefaultBackground ? '#f4ecd8' : '#ffffff';
-  isDefaultBackground = !isDefaultBackground;
-}
-</script>
-<div style="text-align: right;">
-  <a href="#" onclick="toggleDyslexiaMode(); return false;" style="color: #2c5282; text-decoration: underline; cursor: pointer;">
-    Toggle background color
-  </a>
-</div>
-<!-- Note header (title, curators, notice etc.). -->
-<center><h1 style="font-size: 50px;">{{ site.data.harmonicOscillator.title }}</h1></center>
-<center><h2 style="font-size: 20px;">Note Authors: {{ site.data.harmonicOscillator.curators }}</h2></center>
-<!--  -->
-<style>
-  body {
-    font-family: "Times New Roman", Times, serif;
-  }
-</style>
-<br>
-<div style="border: 1px solid black; padding: 10px;">
-  <p>
-  These notes are created using an interactive theorem
-  prover called <a href="https://lean-lang.org">Lean</a>.
-  Lean formally checks definitions, theorems and proofs for correctness.
-  These notes are part of a much larger project called
-  <a href="https://github.com/HEPLean/PhysLean">PhysLean</a>, which aims to digitalize
-  physics into Lean. Please consider contributing to this project.
-  <br><br>
-  Please provide feedback or suggestions for improvements by creating a GitHub issue
-  <a href="https://github.com/HEPLean/HepLean/issues">here</a>.
-  </p>
-</div>
-<!-- Table of content. -->
-<hr>
-<center><h2 style="font-size: 30px;">Table of content</h2></center>
-<p>
-{% for entry in site.data.harmonicOscillator.parts %}
-{% if entry.type == "h1" %}
-  <a href="#section-{{ entry.sectionNo }}" style="color: #2c5282;">{{ entry.sectionNo }}. {{ entry.content }}</a><br>
-{% endif %}
-{% if entry.type == "h2" %}
-&nbsp;&nbsp;&nbsp;&nbsp;<a href="#section-{{ entry.sectionNo }}"  style="color: #2c5282;">{{ entry.sectionNo }}. {{ entry.content }}</a><br>
-{% endif %}
-{% endfor %}
-</p>
-<hr>
-<!-- Main body. -->
-<br>
-{% for entry in site.data.harmonicOscillator.parts %}
-  {% if entry.type == "h1" %}
-    <h1 id="section-{{ entry.sectionNo }}">{{ entry.sectionNo }}. {{ entry.content }}</h1>
-  {% endif %}
-  {% if entry.type == "h2" %}
-    <h2 id="section-{{ entry.sectionNo }}">{{ entry.sectionNo }}. {{ entry.content }} </h2>
-  {% endif %}
-  {% if entry.type == "p" %}
-    <p>{{ entry.content }}</p>
-  {% endif %}
-  {% if entry.type == "warning" %}
-  <div class="alert alert-danger" role="alert">
-    <b>Warning:</b> {{ entry.content }}
-  </div>
-  {% endif %}
-  {% if entry.type == "name" %}
-
-  <div style=" padding: 10px; border-radius: 4px;">
-     <b id="decl-{{ entry.declNo }}">
-      <a href="#decl-{{ entry.declNo }}" style="color: black;">
-      {% if entry.isDef %}Definition{% else %}
-      {% if entry.isThm %}Theorem{% else %}Lemma{% endif %}{% endif %} {{ entry.declNo }}</a></b>
-      (<a href = "{{ entry.link }}" style="color: #2c5282;">{{ entry.name }}</a>)<b>:</b>
-      {% if entry.status == "incomplete" %}🚧{% endif %}
-      <div style="margin-left: 1em;">{{ entry.docString | markdownify}}</div>
-    <details class="code-block-container">
-    <summary style="font-size: 0.8em; margin-left: 1em;">Show Lean code:</summary>
-    <pre style="background: none; margin: 0;"><code class="language-lean">{{ entry.declString }}</code></pre>
-    </details>
-  </div>
-  {% endif %}
-  {% if entry.type == "remark" %}
-  <div style="padding: 10px; border-radius: 4px; border: 1px solid #e8e6e6;">
-    <a href = "{{ entry.link }}" style="color: #2c5282;">Remark: {{ entry.name}} </a>
-  {{ entry.content|markdownify }}
-  </div>
-  <br>
-  {% endif %}
-{% endfor %}
diff --git a/docs/CuratedNotes/HiggsPotential.html b/docs/CuratedNotes/HiggsPotential.html
@@ -0,0 +1,4 @@
+---
+layout: curatedNote
+data_source: higgsPotential
+---
diff --git a/docs/CuratedNotes/WickTheorem.html b/docs/CuratedNotes/WickTheorem.html
@@ -0,0 +1,4 @@
+---
+layout: curatedNote
+data_source: perturbationTheory
+---
diff --git a/docs/CuratedNotes/index.html b/docs/CuratedNotes/index.html
@@ -4,17 +4,27 @@
 <div class="curated-notes">
   <h1 class="title">Curated Notes</h1>
   <div class="notes-container">
+    <!-- Harmonic Oscillator -->
     <div class="note-card">
       <h2 style="text-align: center;">Quantum Harmonic Oscillator</h2>
       <p class="description">The formalization of the quantum harmonic oscillator.</p>
       <a href="HarmonicOscillator" class="note-link">Read More →</a>
     </div>
+    <!-- End Harmonic Oscillator -->
+    <!-- Wick's theorem -->
     <div class="note-card">
-      <h2 style="text-align: center;">Proof of Wick's theorem</h2>
-
+      <h2 style="text-align: center;">Wick's theorem</h2>
       <p class="description">The formalization of the proof of Wick's theorem in perturbation theory.</p>
-      <a href="PerturbationTheory" class="note-link">Read More →</a>
+      <a href="WickTheorem" class="note-link">Read More →</a>
+    </div>
+    <!-- End Wick's theorem -->
+    <!-- Higgs potential -->
+    <div class="note-card">
+      <h2 style="text-align: center;">Higgs potential 🚧</h2>
+      <p class="description">The formalization of properties of the Higgs potential.</p>
+      <a href="HiggsPotential" class="note-link">Read More →</a>
     </div>
+    <!-- End Wick's theorem -->
   </div>
 </div>
 

diff --git a/docs/CuratedNotes/PerturbationTheory.html → docs/_layouts/curatedNote.html b/docs/CuratedNotes/PerturbationTheory.html → docs/_layouts/curatedNote.html
@@ -1,6 +1,9 @@
 ---
 layout: default
+data_source: harmonicOscillator  # Default value, can be overridden
 ---
+
+
 <style>
   body {
     color: black;
@@ -26,8 +29,9 @@
   </a>
 </div>
 <!-- Note header (title, curators, notice etc.). -->
-<center><h1 style="font-size: 50px;">{{ site.data.perturbationTheory.title }}</h1></center>
-<center><h2 style="font-size: 20px;">Note Authors: {{ site.data.perturbationTheory.curators }}</h2></center>
+{% assign data = site.data[page.data_source] %}
+<center><h1 style="font-size: 50px;">{{ data.title }}</h1></center>
+<center><h2 style="font-size: 20px;">Note Authors: {{ data.curators }}</h2></center>
 <!--  -->
 <style>
   body {
@@ -41,7 +45,7 @@
   prover called <a href="https://lean-lang.org">Lean</a>.
   Lean formally checks definitions, theorems and proofs for correctness.
   These notes are part of a much larger project called
-  <a href="https://github.com/HEPLean/HepLean">HepLean</a>, which aims to digitalize
+  <a href="https://github.com/HEPLean/PhysLean">PhysLean</a>, which aims to digitalize
   physics into Lean. Please consider contributing to this project.
   <br><br>
   Please provide feedback or suggestions for improvements by creating a GitHub issue
@@ -52,7 +56,7 @@
 <hr>
 <center><h2 style="font-size: 30px;">Table of content</h2></center>
 <p>
-{% for entry in site.data.perturbationTheory.parts %}
+{% for entry in data.parts %}
 {% if entry.type == "h1" %}
   <a href="#section-{{ entry.sectionNo }}" style="color: #2c5282;">{{ entry.sectionNo }}. {{ entry.content }}</a><br>
 {% endif %}
@@ -64,7 +68,7 @@
 <hr>
 <!-- Main body. -->
 <br>
-{% for entry in site.data.perturbationTheory.parts %}
+{% for entry in data.parts %}
   {% if entry.type == "h1" %}
     <h1 id="section-{{ entry.sectionNo }}">{{ entry.sectionNo }}. {{ entry.content }}</h1>
   {% endif %}
@@ -84,7 +88,8 @@ <h2 id="section-{{ entry.sectionNo }}">{{ entry.sectionNo }}. {{ entry.content }
   <div style=" padding: 10px; border-radius: 4px;">
      <b id="decl-{{ entry.declNo }}">
       <a href="#decl-{{ entry.declNo }}" style="color: black;">
-      {% if entry.isDef %}Definition{% else %}Theorem{% endif %} {{ entry.declNo }}</a></b>
+      {% if entry.isDef %}Definition{% else %}
+      {% if entry.isThm %}Theorem{% else %}Lemma{% endif %}{% endif %} {{ entry.declNo }}</a></b>
       (<a href = "{{ entry.link }}" style="color: #2c5282;">{{ entry.name }}</a>)<b>:</b>
       {% if entry.status == "incomplete" %}🚧{% endif %}
       <div style="margin-left: 1em;">{{ entry.docString | markdownify}}</div>

diff --git a/scripts/MetaPrograms/notes.lean b/scripts/MetaPrograms/notes.lean
@@ -290,7 +290,6 @@ def perturbationTheory : Note where
     .name ``FieldSpecification.FieldOpAlgebra.wicks_theorem_normal_order .complete
     ]
 
-
 def harmonicOscillator : Note where
   title := "The Quantum Harmonic Oscillator in Lean 4"
   curators := ["Joseph Tooby-Smith"]
@@ -343,14 +342,35 @@ def harmonicOscillator : Note where
     .name ``QuantumMechanics.OneDimension.HarmonicOscillator.fourierIntegral_zero_of_mem_orthogonal .complete,
     .name ``QuantumMechanics.OneDimension.HarmonicOscillator.eigenfunction_completeness .complete,
     ]
+
+def higgsPotential : Note where
+  title := "The Higgs potential in Lean 4 🚧"
+  curators := ["Joseph Tooby-Smith"]
+  parts := [
+    .warning "This note is under construction (03-March-2025).",
+    .h1 "Introduction",
+    .p "The Higgs potential is a key part of the Standard Model of particle physics.
+      It is a scalar potential which is used to give mass to the elementary particles.
+      The Higgs potential is a polynomial of degree four in the Higgs field.",
+    .h1 "The Higgs field",
+    .name ``StandardModel.HiggsVec .incomplete,
+  ]
+
+def notesToMake : List (Note × String) := [
+    (perturbationTheory, "perturbationTheory"),
+    (harmonicOscillator, "harmonicOscillator"),
+    (higgsPotential, "higgsPotential")]
+
+def makeYML (nt : Note × String) : IO UInt32 := do
+  let n := nt.1
+  let s := nt.2
+  let ymlString ← CoreM.withImportModules #[`PhysLean] (n.toYML).run'
+  let fileOut : System.FilePath := {toString := s!"./docs/_data/{s}.yml"}
+  IO.FS.writeFile fileOut ymlString
+  IO.println (s!"YML file made for {n.title}.")
+  pure 0
+
 unsafe def main (_ : List String) : IO UInt32 := do
   initSearchPath (← findSysroot)
-  let ymlString ← CoreM.withImportModules #[`PhysLean] (perturbationTheory.toYML).run'
-  let fileOut : System.FilePath := {toString := "./docs/_data/perturbationTheory.yml"}
-  IO.println (s!"YML file made for perturbation theory.")
-  IO.FS.writeFile fileOut ymlString
-  let ymlString2 ← CoreM.withImportModules #[`PhysLean] (harmonicOscillator.toYML).run'
-  let fileOut2 : System.FilePath := {toString := "./docs/_data/harmonicOscillator.yml"}
-  IO.println (s!"YML file made for harmonic oscillator.")
-  IO.FS.writeFile fileOut2 ymlString2
+  let _ ← notesToMake.mapM makeYML
   pure 0