draining

source/Library/gearbox.mmt

@@ -15,7 +15,7 @@ theory cogwheels =
   include ?temp ❙
   // fixed planar cogwheels de-dimensionalized ❙
   theory cogwheel_theory =
-    center : ℝ ×ℝ ❘ # c ❙ // planar geometry ❙
+    center : ℝ×ℝ ❘ # c ❙ // planar geometry ❙
     radius : ℝ ❘ # r ❙
     numteeth : ℕ ❙
     angle : ℝ ❙
@@ -24,6 +24,7 @@ theory cogwheels =
   theory rotating_cogwheel_theory =
     include ?cogwheels/cogwheel_theory ❙
     angular_velocity : ℝ ❘ # ω ❙
+    angular_force : ℝ ❘ # f ❙
   ❚
   rotating_cogwheel = Mod ☞?cogwheels/rotating_cogwheel_theory ❙
 ❚
@@ -35,11 +36,17 @@ theory gearbox =
   interlocking = [x:cogwheel,y:cogwheel] dist (x.center) (y.center) ≐ (x.radius) + (y.radius) ❙
 
   interlocking_cogwheels : ⊦ ∀[x : rotating_cogwheel] ∀[y : rotating_cogwheel]
-        interlocking x y ⇒ (x.angular_velocity)/(x.radius) ≐ (y.angular_velocity)/(y.radius) ❙
+        interlocking x y ⇒ (x.angular_velocity)/(x.radius) ≐ - (y.angular_velocity)/(y.radius)❙
+
+coaxial : rotating_cogwheel ⟶ rotating_cogwheel ⟶ prop ❘ = [x,y] x.center ≐ y.center❙
+
+coaxial_cogwheels :  ⊦ ∀[x] ∀[y] coaxial x y ⇒ x.angular_velocity ≐ y.angular_velocity ❙
 
   compute_av : {RC : rotating_cogwheel, C : cogwheel} ⊦ interlocking RC C ⟶ ℝ ❘
-        = [RC,C,p] ((RC.angular_velocity)/(RC.radius)) ⋅ (C.radius) ❘ # avc 1 2 %I3 ❙
+        = [RC,C,p] - ((RC.angular_velocity)/(RC.radius)) ⋅ (C.radius) ❘ # avc 1 2 %I3 ❙
 
+  //proof_av : {RC : rotating_cogwheel, C : cogwheel, p ⊦ interlocking RC C} ⊦ compute_av RC C p ❘
+        = [RC, C, p] impE p (forallE (forallE interlocking_cogwheels)) ❙
 ❚