leanprover-community · zhikaip · Mar 9, 2026 · Mar 6, 2026 · Mar 7, 2026 · Mar 7, 2026
diff --git a/PhysLean.lean b/PhysLean.lean
diff --git a/PhysLean/ClassicalMechanics/Basic.lean b/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
diff --git a/PhysLean/ClassicalMechanics/DampedHarmonicOscillator/Basic.lean b/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

diff --git a/PhysLean/ClassicalMechanics/EulerLagrange.lean b/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]

diff --git a/PhysLean/ClassicalMechanics/HamiltonsEquations.lean b/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

diff --git a/PhysLean/ClassicalMechanics/HarmonicOscillator/Basic.lean b/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

diff --git a/PhysLean/ClassicalMechanics/HarmonicOscillator/ConfigurationSpace.lean b/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

diff --git a/PhysLean/ClassicalMechanics/HarmonicOscillator/Solution.lean b/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
 

diff --git a/PhysLean/ClassicalMechanics/Lagrangian/TotalDerivativeEquivalence.lean b/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

diff --git a/PhysLean/ClassicalMechanics/Mass/MassUnit.lean b/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.

diff --git a/PhysLean/ClassicalMechanics/Pendulum/CoplanarDoublePendulum.lean b/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

diff --git a/PhysLean/ClassicalMechanics/Pendulum/MiscellaneousPendulumPivotMotions.lean b/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
 

diff --git a/PhysLean/ClassicalMechanics/Pendulum/SlidingPendulum.lean b/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

diff --git a/PhysLean/ClassicalMechanics/RigidBody/Basic.lean b/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

diff --git a/PhysLean/ClassicalMechanics/RigidBody/SolidSphere.lean b/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

diff --git a/PhysLean/ClassicalMechanics/Scattering/RigidSphere.lean b/PhysLean/ClassicalMechanics/Scattering/RigidSphere.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.Meta.TODO.Basic
+module
+
+public import PhysLean.Meta.TODO.Basic
 /-!
 
 # Scattering off a perfectly rigid sphere
@@ -13,4 +15,6 @@ import PhysLean.Meta.TODO.Basic
 - Landau and Lifshitz, Mechanics, page 50, Section 18, Problem 1
 -/
 
+@[expose] public section
+
 TODO "L7OTP" "Derive the scattering cross section of a perfectly rigid sphere."
diff --git a/PhysLean/ClassicalMechanics/Vibrations/LinearTriatomic.lean b/PhysLean/ClassicalMechanics/Vibrations/LinearTriatomic.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.Meta.TODO.Basic
+module
+
+public import PhysLean.Meta.TODO.Basic
 /-!
 
 # Vibrations of a symmetric linear triatomic molecule
@@ -13,4 +15,6 @@ import PhysLean.Meta.TODO.Basic
 - Landau and Lifshitz, Mechanics, page 72, Section 24, Problem 1
 -/
 
+@[expose] public section
+
 TODO "L7O4I" "Derive the frequencies of vibaration of a symmetric linear triatomic molecule."
diff --git a/PhysLean/ClassicalMechanics/WaveEquation/Basic.lean b/PhysLean/ClassicalMechanics/WaveEquation/Basic.lean
@@ -3,8 +3,10 @@ Copyright (c) 2025 Zhi Kai Pong. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Zhi Kai Pong
 -/
-import PhysLean.SpaceAndTime.Space.CrossProduct
-import PhysLean.SpaceAndTime.TimeAndSpace.Basic
+module
+
+public import PhysLean.SpaceAndTime.Space.CrossProduct
+public import PhysLean.SpaceAndTime.TimeAndSpace.Basic
 /-!
 
 # Wave equation
@@ -39,6 +41,8 @@ By a plne wave we mean a function of the form `f(t, x) = f₀(⟪x, s⟫_ℝ - c
 
 -/
 
+@[expose] public section
+
 namespace ClassicalMechanics
 
 open Space

diff --git a/PhysLean/ClassicalMechanics/WaveEquation/HarmonicWave.lean b/PhysLean/ClassicalMechanics/WaveEquation/HarmonicWave.lean
@@ -3,7 +3,9 @@ Copyright (c) 2025 Zhi Kai Pong. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Zhi Kai Pong
 -/
-import PhysLean.ClassicalMechanics.WaveEquation.Basic
+module
+
+public import PhysLean.ClassicalMechanics.WaveEquation.Basic
 /-!
 
 # Harmonic Wave
@@ -15,6 +17,8 @@ the status of Fourier theory in Mathlib.
 
 -/
 
+@[expose] public section
+
 namespace ClassicalMechanics
 open Space
 

diff --git a/PhysLean/CondensedMatter/Basic.lean b/PhysLean/CondensedMatter/Basic.lean
@@ -3,6 +3,8 @@ 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
+
 /-!
 
 # Condensed Matter
@@ -18,4 +20,4 @@ Some directories which are NOT currently place holders are:
 - Quantum Mechanics
 - Relativity
 
--/
+-/@[expose] public section