feat: 20 of March PR to make the branch up-to-date

.codespellignore

@@ -9,3 +9,4 @@ Breal
 ket
 rIn
 FRO
+Commun

.github/workflows/labels_from_comment.yml

@@ -0,0 +1,82 @@
+# This workflow allows any user to add or remove one of the labels in the array `labelArray`
+# by commenting on the PR or issue.
+# The script reacts to lines in the comment whose entire content is, up to whitespace,
+# the label name, optionally preceded by `-`.
+# For each label, the bot follows the instruction of the *last* line that matches the label.
+
+name: Label PR based on Comment
+
+on:
+  issue_comment:
+    types: [created]
+  pull_request_review:
+    types: [submitted]
+  pull_request_review_comment:
+    types: [created]
+
+# Limit permissions for GITHUB_TOKEN for the entire workflow
+permissions:
+  contents: read
+  pull-requests: write  # Only allow PR comments/labels
+  # All other permissions are implicitly 'none'
+
+jobs:
+  update-label:
+    env:
+      COMMENT: ${{ github.event.comment.body }}
+    runs-on: ubuntu-latest
+
+    steps:
+    - name: Add / remove label based on comment
+      run: |
+        labelArray=("awaiting-author" "blocked-by-mathlib-PR" "blocked-by-PR" "documentation" "easy" "help-wanted" "merge-conflict" "new-contributor" "please-adopt" "RFC" "WIP" "t-classical-mechanics" "t-condensed-matter" "t-cosmology" "t-electromagnetism" "t-mathematics" "t-meta" "t-optics" "t-particles" "t-quantum-field-theory" "t-quantum-mechanics" "t-relativity" "t-space-time" "t-statistical-mechanics" "t-string-theory" "t-thermodynamics" "t-units")
+
+        # we strip `\r` since line endings from GitHub contain this character
+        COMMENT="${COMMENT//$'\r'/}"
+
+        # trim leading/trailing whitespace and collapse "internal" whitespace
+        COMMENT="$(printf '%s' "${COMMENT}" | awk '{$1=$1};1')"
+
+        # for debugging, we print some information
+        printf '%s' "${COMMENT}" | hexdump -cC
+        printf 'Comment:"%s"\n' "${COMMENT}"
+
+        for i in "${!labelArray[@]}"; do
+          inComment=""
+          label="${labelArray[$i]}"
+          printf $'\nProcessing label \'%s\'\n' "${label}"
+          # extract the last line that, up to leading/trailing whitespace, matches the current label
+          inComment="$(printf '%s' "${COMMENT}" | grep "[-]\?${label}$" | tail -1)"
+          if [ -n "${inComment}" ]
+          then
+            printf $'Found \'%s\'\n' "${inComment}"
+            if [ "${inComment:0:1}" == "-" ]
+            then
+              printf $'Removing label \'%s\'\n' "${label}"
+              # we use curl rather than octokit/request-action so that the job won't fail
+              # (and send an annoying email) if the labels don't exist
+              curl --request DELETE \
+                --url "https://api.github.com/repos/${{ github.repository }}/issues/${{ github.event.issue.number }}/labels/${label}" \
+                --header 'authorization: Bearer ${{ secrets.GITHUB_TOKEN }}'
+              printf $'%s DELETE done\n' "${inComment}"
+
+            else
+              data="$(printf $'{"labels":["%s"]}' "${label}")"
+              printf $'Using data: %s\n' "${data}"
+              # we use curl rather than octokit/request-action so that the job won't fail
+              # (and send an annoying email) if the labels don't exist
+              curl --request POST \
+                --header 'Accept: application/vnd.github+json' \
+                --header 'authorization: Bearer ${{ secrets.GITHUB_TOKEN }}' \
+                --header 'X-GitHub-Api-Version: 2022-11-28' \
+                --url "https://api.github.com/repos/${{ github.repository }}/issues/${{ github.event.issue.number }}/labels" \
+                --data "${data}"
+              printf $'%s POST done\n' "${inComment}"
+
+            fi
+
+          else
+            printf $'Label \'%s\' not found.\n' "${label}"
+          fi
+
+        done

PhysLean/ClassicalMechanics/Basic.lean

@@ -3,11 +3,13 @@ Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
+module
+
 /-!
 
 # Classical mechanics
 
 This file is currently a stub.
 Please feel free to contribute!
 
--/
+-/@[expose] public section

PhysLean/ClassicalMechanics/DampedHarmonicOscillator/Basic.lean

@@ -3,9 +3,11 @@ Copyright (c) 2025 Nicola Bernini. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Nicola Bernini
 -/
-import PhysLean.Meta.Informal.SemiFormal
-import PhysLean.ClassicalMechanics.EulerLagrange
-import PhysLean.ClassicalMechanics.HamiltonsEquations
+module
+
+public import PhysLean.Meta.Informal.SemiFormal
+public import PhysLean.ClassicalMechanics.EulerLagrange
+public import PhysLean.ClassicalMechanics.HamiltonsEquations
 /-!
 
 # The Damped Harmonic Oscillator
@@ -59,6 +61,8 @@ References for the damped harmonic oscillator include:
 
 -/
 
+@[expose] public section
+
 namespace ClassicalMechanics
 open Real
 open ContDiff

PhysLean/ClassicalMechanics/EulerLagrange.lean

@@ -3,7 +3,9 @@ Copyright (c) 2025 Tomas Skrivan. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Tomas Skrivan, Joseph Tooby-Smith
 -/
-import PhysLean.Mathematics.VariationalCalculus.HasVarGradient
+module
+
+public import PhysLean.Mathematics.VariationalCalculus.HasVarGradient
 /-!
 
 # Euler-Lagrange equations
@@ -14,6 +16,8 @@ and prove the that the variational derivative of the action functional
 
 -/
 
+@[expose] public section
+
 open MeasureTheory ContDiff InnerProductSpace Time
 
 variable {X} [NormedAddCommGroup X] [InnerProductSpace ℝ X] [CompleteSpace X]

PhysLean/ClassicalMechanics/HamiltonsEquations.lean

@@ -3,7 +3,9 @@ Copyright (c) 2025 Tomas Skrivan. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Tomas Skrivan, Joseph Tooby-Smith
 -/
-import PhysLean.Mathematics.VariationalCalculus.HasVarGradient
+module
+
+public import PhysLean.Mathematics.VariationalCalculus.HasVarGradient
 /-!
 
 # Hamilton's equations
@@ -23,6 +25,8 @@ applied to `(p, q)`.
 
 -/
 
+@[expose] public section
+
 open MeasureTheory ContDiff InnerProductSpace Time
 
 namespace ClassicalMechanics

PhysLean/ClassicalMechanics/HarmonicOscillator/Basic.lean

@@ -3,10 +3,12 @@ Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith, Lode Vermeulen
 -/
-import PhysLean.Meta.Informal.SemiFormal
-import PhysLean.ClassicalMechanics.EulerLagrange
-import PhysLean.ClassicalMechanics.HamiltonsEquations
-import PhysLean.ClassicalMechanics.HarmonicOscillator.ConfigurationSpace
+module
+
+public import PhysLean.Meta.Informal.SemiFormal
+public import PhysLean.ClassicalMechanics.EulerLagrange
+public import PhysLean.ClassicalMechanics.HamiltonsEquations
+public import PhysLean.ClassicalMechanics.HarmonicOscillator.ConfigurationSpace
 /-!
 
 # The Classical Harmonic Oscillator
@@ -81,6 +83,8 @@ References for the classical harmonic oscillator include:
 
 -/
 
+@[expose] public section
+
 namespace ClassicalMechanics
 open Real
 open Space

PhysLean/ClassicalMechanics/HarmonicOscillator/ConfigurationSpace.lean

@@ -3,15 +3,19 @@ Copyright (c) 2026 Nicola Bernini. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Nicola Bernini
 -/
-import Mathlib.Geometry.Manifold.Diffeomorph
-import PhysLean.SpaceAndTime.Time.Basic
+module
+
+public import Mathlib.Geometry.Manifold.Diffeomorph
+public import PhysLean.SpaceAndTime.Time.Basic
 /-!
 # Configuration space of the harmonic oscillator
 
 The configuration space is defined as a one-dimensional smooth manifold,
 modeled on `ℝ`, with a chosen coordinate.
 -/
 
+@[expose] public section
+
 namespace ClassicalMechanics
 
 namespace HarmonicOscillator

PhysLean/ClassicalMechanics/HarmonicOscillator/Solution.lean

@@ -3,9 +3,11 @@ Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith, Lode Vermeulen
 -/
-import Mathlib.Analysis.CStarAlgebra.Classes
-import PhysLean.ClassicalMechanics.HarmonicOscillator.Basic
-import PhysLean.Units.Basic
+module
+
+public import Mathlib.Analysis.CStarAlgebra.Classes
+public import PhysLean.ClassicalMechanics.HarmonicOscillator.Basic
+public import PhysLean.Units.Basic
 /-!
 
 # Solutions to the classical harmonic oscillator
@@ -53,6 +55,8 @@ References for the classical harmonic oscillator include:
 
 -/
 
+@[expose] public section
+
 namespace ClassicalMechanics
 open Real Time ContDiff
 

PhysLean/ClassicalMechanics/Lagrangian/TotalDerivativeEquivalence.lean

@@ -3,7 +3,9 @@ Copyright (c) 2025 Rein Zustand. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Rein Zustand
 -/
-import PhysLean.Mathematics.VariationalCalculus.HasVarGradient
+module
+
+public import PhysLean.Mathematics.VariationalCalculus.HasVarGradient
 /-!
 
 # Equivalent Lagrangians under Total Derivatives
@@ -51,6 +53,8 @@ This is because:
 
 -/
 
+@[expose] public section
+
 namespace ClassicalMechanics
 
 open InnerProductSpace

PhysLean/ClassicalMechanics/Mass/MassUnit.lean

@@ -3,8 +3,10 @@ Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
-import Mathlib.Geometry.Manifold.Diffeomorph
-import PhysLean.SpaceAndTime.Time.Basic
+module
+
+public import Mathlib.Geometry.Manifold.Diffeomorph
+public import PhysLean.SpaceAndTime.Time.Basic
 /-!
 
 # Units on Mass
@@ -24,6 +26,8 @@ existence of the mass unit of kilograms, and construct all other mass units from
 
 -/
 
+@[expose] public section
+
 open NNReal
 
 /-- The choices of translationally-invariant metrics on the mass-manifold.

PhysLean/ClassicalMechanics/Pendulum/CoplanarDoublePendulum.lean

@@ -3,8 +3,10 @@ Copyright (c) 2025 Shlok Vaibhav Singh. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Shlok Vaibhav Singh
 -/
-import PhysLean.Meta.Informal.Basic
-import PhysLean.Meta.Sorry
+module
+
+public import PhysLean.Meta.Informal.Basic
+public import PhysLean.Meta.Sorry
 /-!
 # Coplanar Double Pendulum
 ### Tag: LnL_1.5.1
@@ -62,6 +64,8 @@ so that the Lagrangian becomes:
 $$
 -/
 
+@[expose] public section
+
 namespace ClassicalMechanics
 
 namespace CoplanarDoublePendulum

PhysLean/ClassicalMechanics/Pendulum/MiscellaneousPendulumPivotMotions.lean

@@ -3,6 +3,8 @@ Copyright (c) 2025 Shlok Vaibhav Singh. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Shlok Vaibhav Singh
 -/
+module
+
 /-!
 # Miscellaneous Pendulum Pivot Motions
 ### Tag: LnL_1.5.3
@@ -139,7 +141,7 @@ Ignoring the total time derivate term, the final lagrangian becomes:
 $$
 L = \tfrac{1}{2} m l^2\dot{\phi}^2 + m g l \cos\phi - m a l \gamma^2 \cos\phi\cos(\gamma t)
 $$
--/
+-/@[expose] public section
 
 namespace ClassicalMechanics
 

PhysLean/ClassicalMechanics/Pendulum/SlidingPendulum.lean

@@ -3,7 +3,9 @@ Copyright (c) 2025 Shlok Vaibhav Singh. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Shlok Vaibhav Singh
 -/
-import PhysLean.Meta.Sorry
+module
+
+public import PhysLean.Meta.Sorry
 /-!
 # Sliding Pendulum
 ### Tag: LnL_1.5.2
@@ -55,6 +57,8 @@ $$
 
 -/
 
+@[expose] public section
+
 namespace ClassicalMechanics
 
 namespace SlidingPendulum

PhysLean/ClassicalMechanics/RigidBody/Basic.lean

@@ -3,8 +3,10 @@ Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
-import PhysLean.SpaceAndTime.Space.Derivatives.Curl
-import Mathlib.Geometry.Manifold.Algebra.SmoothFunctions
+module
+
+public import PhysLean.SpaceAndTime.Space.Derivatives.Curl
+public import Mathlib.Geometry.Manifold.Algebra.SmoothFunctions
 /-!
 
 # Rigid bodies
@@ -21,6 +23,8 @@ In this module we will define the basic properties of a rigid body, including
 - Landau and Lifshitz, Mechanics, page 100, Section 32
 -/
 
+@[expose] public section
+
 open Manifold
 
 TODO "MEX5S" "The definition of a rigid body is currently defined via linear maps

PhysLean/ClassicalMechanics/RigidBody/SolidSphere.lean

@@ -3,7 +3,9 @@ Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
-import PhysLean.ClassicalMechanics.RigidBody.Basic
+module
+
+public import PhysLean.ClassicalMechanics.RigidBody.Basic
 /-!
 
 # The solid sphere as a rigid body
@@ -13,6 +15,8 @@ center of mass and inertia tensor.
 
 -/
 
+@[expose] public section
+
 open Manifold
 open MeasureTheory
 namespace RigidBody