From 02f8c1b7bfb9d39d365fa00b8b7daea4b923c8aa Mon Sep 17 00:00:00 2001
From: Paul-Walcher <paulwalcher12@gmail.com>
Date: Sat, 11 May 2024 16:56:04 +0200
Subject: [PATCH] Better circle scroll

---
 source/Scrolls/MuchBetterCircleScroll.mmt | 61 +++++++++++++++++++++++
 1 file changed, 61 insertions(+)
 create mode 100644 source/Scrolls/MuchBetterCircleScroll.mmt

diff --git a/source/Scrolls/MuchBetterCircleScroll.mmt b/source/Scrolls/MuchBetterCircleScroll.mmt
new file mode 100644
index 0000000..5cef9d7
--- /dev/null
+++ b/source/Scrolls/MuchBetterCircleScroll.mmt
@@ -0,0 +1,61 @@
+namespace http://mathhub.info/FrameIT/frameworld ❚
+fixmeta ?FrameworldMeta ❚
+
+/T This scrolls infers a 2D circle from three dedicated 3D points (the circle's supposed center,
+   one of the supposed circle itself, one in the plane the circle should lie in).
+❚
+theory MuchBetterCircleScroll =
+    meta ?MetaAnnotations?problemTheory ?MuchBetterCircleScroll/Problem ❙
+    meta ?MetaAnnotations?solutionTheory ?MuchBetterCircleScroll/Solution ❙
+
+    // the three special points M, A and  B ❙
+    theory Problem =
+        M : point ❘ meta ?MetaAnnotations?label "M"
+                  ❘ meta ?MetaAnnotations?description "The circle's center" ❙
+        A : point ❘ meta ?MetaAnnotations?label "A"
+                  ❘ meta ?MetaAnnotations?description "A point on the circle" ❙
+        B : point ❘ meta ?MetaAnnotations?label "B"
+                  ❘ meta ?MetaAnnotations?description "A point within the plane the circle should lie in." ❙
+        radiusC: Σ x:ℝ . ⊦ (d- M A ≐ x) ∨ (d- A M)
+               ❘ meta ?MetaAnnotations?label "r"
+               ❘ meta ?MetaAnnotations?description s"radius of the circle ${lverb cir}"
+        ❙
+    ❚
+
+    theory Solution =
+        include ?MuchBetterCircleScroll/Problem ❙
+
+        deduceC: circle
+              ❘ = ( pointsToC M A B )
+              ❘ meta ?MetaAnnotations?label s"○${lverb M}"
+              ❘ meta ?MetaAnnotations?description "Circle"
+        ❙
+
+        deduceR:  Σ x:ℝ . ⊦ ( circleRadius deduceC) ≐ x
+              ❘ =  ⟨ d- M A , sketch "deduce Radius"⟩
+              ❘ meta ?MetaAnnotations?label s"r${lverb deduceC}"
+              ❘ meta ?MetaAnnotations?description s"radius of ${lverb deduceC} (radius fact)"  b
+        ❙
+
+        deduceR2:  Σ x:ℝ . ⊦ ( d- A M ) ≐ x 
+                ❘ =  ⟨ d- A M , sketch "deduce Radius2"⟩
+                ❘ meta ?MetaAnnotations?label s"${lverb A M}"
+                ❘ meta ?MetaAnnotations?description s"radius of ${lverb deduceC} (distance fact)"
+        ❙
+
+        midOnCircle: ⊦ M VonC deduceC
+                   ❘ = midOnC deduceC M
+                   ❘ meta ?MetaAnnotations?label s"${lverb M}∈${lverb deduceC}"
+                   ❘ meta ?MetaAnnotations?description s"proof of M being on the circle ${lverb deduceC}"
+        ❙
+
+        edgeOnCircle: ⊦ A VonC deduceC
+                    ❘ meta ?MetaAnnotations?label s"${lverb A}∈${lverb deduceC}"
+                    ❘ meta ?MetaAnnotations?description s"proof of A being on the circle ${lverb deduceC}"
+        ❙
+
+        // the description verbalizes CircleCircumference, hence must come after its declaration ❙
+        meta ?MetaAnnotations?label "CircleScroll" ❙
+        meta ?MetaAnnotations?description s"Calculating a circle defined by the middle ${lverb M}, an edge point ${lverb A} and a point on the circle plane ${lverb B}. " ❙
+    ❚
+❚
\ No newline at end of file
-- 
GitLab