From ee2938db29771f9e5b3fd81af659441122a4c96b Mon Sep 17 00:00:00 2001
From: Paul-Walcher <paulwalcher12@gmail.com>
Date: Mon, 17 Jun 2024 14:49:36 +0200
Subject: [PATCH] Added Sphere

---
 source/DefaultSituationSpace.mmt |  2 +-
 source/MetaTheories.mmt          |  1 +
 source/Scrolls/SphereScroll.mmt  | 30 +++++++++++++++++++++++-------
 source/Scrolls/SphereType.mmt    | 12 ------------
 4 files changed, 25 insertions(+), 20 deletions(-)
 delete mode 100644 source/Scrolls/SphereType.mmt

diff --git a/source/DefaultSituationSpace.mmt b/source/DefaultSituationSpace.mmt
index 88876ef..254e098 100644
--- a/source/DefaultSituationSpace.mmt
+++ b/source/DefaultSituationSpace.mmt
@@ -14,7 +14,6 @@ theory DefaultSituationSpace =
 		include ?CircleLineAngleToAngleScroll❙
 
         include ?Midpoint ❙
-        include ?Test ❙
         include ?CircleScroll ❙
         
 		include ?BouncingScroll ❙
@@ -30,6 +29,7 @@ theory DefaultSituationSpace =
         include ?CuboidScroll ❙
         include ?TriangleScroll ❙
         include ?SimpleCircleScroll ❙
+        include ?SphereScroll ❙
         
 
 
diff --git a/source/MetaTheories.mmt b/source/MetaTheories.mmt
index 6bc7cb5..2a9f201 100644
--- a/source/MetaTheories.mmt
+++ b/source/MetaTheories.mmt
@@ -338,6 +338,7 @@ theory FrameworldMeta =
   include ?RectangleType ❙
   include ?CuboidType ❙
   include ?CircleType ❙
+  include ?SphereType ❙
 
  // include ☞http://mathhub.info/MitM/core/arithmetics?RealArithmetics ❙
 
diff --git a/source/Scrolls/SphereScroll.mmt b/source/Scrolls/SphereScroll.mmt
index 9ebdb1d..ceb193e 100644
--- a/source/Scrolls/SphereScroll.mmt
+++ b/source/Scrolls/SphereScroll.mmt
@@ -1,6 +1,16 @@
 namespace http://mathhub.info/FrameIT/frameworld ❚
 fixmeta ?FrameworldMeta ❚
 
+theory SphereType =
+  
+  include ☞http://mathhub.info/MitM/core/geometry?3DGeometry ❙
+  include ?FrameITBasics ❙
+
+  sphereType : type ❘ # Sphere ❙
+  sphereCons : point ⟶ point  ⟶ Sphere  ❘ # SphereCons 1 2 ❙
+  
+❚
+
 
 theory SphereScroll =
     meta ?MetaAnnotations?problemTheory  ?SphereScroll/Problem ❙
@@ -8,13 +18,18 @@ theory SphereScroll =
 
     theory Problem =
         
-        C: circle
-         ❘ meta ?MetaAnnotations?label "C"
-         ❘ meta ?MetaAnnotations?description "center-circle"
+        M: point
+         ❘ meta ?MetaAnnotations?label "M"
+         ❘ meta ?MetaAnnotations?description "Midpoint of the sphere"
         ❙
         T: point
          ❘ meta ?MetaAnnotations?label "T"
-         ❘ meta ?MetaAnnotations?description "The top point above the center circle. Has to be parallel to the normal or the normal"
+         ❘ meta ?MetaAnnotations?description "Point on the edge of the sphere"
+        ❙
+
+        dMT: Σ x:ℝ . ⊦ (d- M T) ≐ x
+         ❘ meta ?MetaAnnotations?label MT"
+         ❘ meta ?MetaAnnotations?description "The distance between the mid- and edgepoint (i.e. the radius)"
         ❙
 
 
@@ -23,12 +38,13 @@ theory SphereScroll =
         
     ❚
     theory Solution =
+
         include ?SphereScroll/Problem ❙
         meta ?MetaAnnotations?label "Sphere" ❙
-        meta ?MetaAnnotations?description s"Takes a circle and a point parallel to the normal, then constructs a Sphere." ❙
+        meta ?MetaAnnotations?description s"Takes a point as midpoint and an edgepoint, then constructs a Sphere." ❙
         
-        ConstructedRectangle : Rectangle
-                ❘ = ( SphereCons C T )
+        ConstructedSphere : Sphere
+                ❘ = ( SphereCons M T )
                 ❘ meta ?MetaAnnotations?label s"Sphere"
                 ❘ meta ?MetaAnnotations?description s"The constructed Sphere."
         ❙
diff --git a/source/Scrolls/SphereType.mmt b/source/Scrolls/SphereType.mmt
deleted file mode 100644
index 8646497..0000000
--- a/source/Scrolls/SphereType.mmt
+++ /dev/null
@@ -1,12 +0,0 @@
-namespace http://mathhub.info/FrameIT/frameworld ❚
-fixmeta ?FrameworldMeta ❚
-
-theory SphereType =
-  
-  include ☞http://mathhub.info/MitM/core/geometry?3DGeometry ❙
-  include ?FrameITBasics ❙
-
-  sphereType : type ❘ # Sphere ❙
-  sphereCons : circle ⟶ point  ⟶ Sphere  ❘ # SphereCons 1 2 ❙
-  
-❚
\ No newline at end of file
-- 
GitLab