From b46ddeaf1ae4b4594057ab4f7b0cea4d80c9b2d0 Mon Sep 17 00:00:00 2001 From: Nicola Bernini Date: Tue, 30 Jun 2026 12:22:08 +0200 Subject: [PATCH 1/2] feat: Close the smallest pendulum configuration-space sorryful definitions --- .../Pendulum/SlidingPendulum.lean | 20 +++++++++++++++---- 1 file changed, 16 insertions(+), 4 deletions(-) diff --git a/Physlib/ClassicalMechanics/Pendulum/SlidingPendulum.lean b/Physlib/ClassicalMechanics/Pendulum/SlidingPendulum.lean index 688ef0b51..17a9845f4 100644 --- a/Physlib/ClassicalMechanics/Pendulum/SlidingPendulum.lean +++ b/Physlib/ClassicalMechanics/Pendulum/SlidingPendulum.lean @@ -5,7 +5,7 @@ Authors: Shlok Vaibhav Singh -/ module -public import Physlib.Meta.Linters.Sorry +public import Mathlib.Data.Real.Basic /-! # Sliding Pendulum ### Tag: LnL_1.5.2 @@ -63,9 +63,21 @@ namespace ClassicalMechanics namespace SlidingPendulum -/-- The configuration space of the sliding pendulum system. -/ -@[sorryful] -def ConfigurationSpace : Type := sorry +/-! +## A. Configuration space +-/ + +/-- +The configuration space of the sliding pendulum system. + +The generalized coordinates are the horizontal position of the support mass and the angle +that the string makes with the vertical. +-/ +structure ConfigurationSpace where + /-- The horizontal position `x₁` of the support mass. -/ + supportPosition : ℝ + /-- The angle `φ` that the string makes with the vertical. -/ + angle : ℝ end SlidingPendulum From 8640cf64588366614c82acdb40a62422e966deee Mon Sep 17 00:00:00 2001 From: Nicola Bernini Date: Wed, 1 Jul 2026 09:49:08 +0200 Subject: [PATCH 2/2] Use Real.Angle for sliding pendulum angle Co-authored-by: Claude Opus 4.8 --- Physlib/ClassicalMechanics/Pendulum/SlidingPendulum.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Physlib/ClassicalMechanics/Pendulum/SlidingPendulum.lean b/Physlib/ClassicalMechanics/Pendulum/SlidingPendulum.lean index 17a9845f4..cbbbd721d 100644 --- a/Physlib/ClassicalMechanics/Pendulum/SlidingPendulum.lean +++ b/Physlib/ClassicalMechanics/Pendulum/SlidingPendulum.lean @@ -5,7 +5,7 @@ Authors: Shlok Vaibhav Singh -/ module -public import Mathlib.Data.Real.Basic +public import Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle /-! # Sliding Pendulum ### Tag: LnL_1.5.2 @@ -77,7 +77,7 @@ structure ConfigurationSpace where /-- The horizontal position `x₁` of the support mass. -/ supportPosition : ℝ /-- The angle `φ` that the string makes with the vertical. -/ - angle : ℝ + angle : Real.Angle end SlidingPendulum