CircleScroll.mmt

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 CircleScroll =
    meta ?MetaAnnotations?problemTheory ?CircleScroll/Problem ❙
    meta ?MetaAnnotations?solutionTheory ?CircleScroll/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." ❙
        dMA : Σ x:ℝ . ⊦ (d- M A) ≐ x
                  ❘ meta ?MetaAnnotations?label "dMA"
                  ❘ meta ?MetaAnnotations?description "The distance from the Midpoint M to the edge point A" ❙
    ❚

    theory Solution =
       include ?CircleScroll/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)"
       ❙

        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}. " ❙
    ❚
❚

 theory CircleAreaScroll =
    meta ?MetaAnnotations?problemTheory  ?CircleAreaScroll/Problem ❙
    meta ?MetaAnnotations?solutionTheory ?CircleAreaScroll/Solution ❙

    theory Problem =
        cir: circle
           ❘ meta ?MetaAnnotations?label "○C"
           ❘  meta ?MetaAnnotations?description s"the circle"
        ❙

        /T todo: why can't we compute the radius directly from cir? ❙
        radiusC: Σ x:ℝ . ⊦ radius cir ≐ x
               ❘ meta ?MetaAnnotations?label "r"
               ❘ meta ?MetaAnnotations?description s"radius of the circle ${lverb cir}"
        ❙
    ❚

    theory Solution =
        include ?CircleAreaScroll/Problem ❙
        deduceArea: Σ x:ℝ . ⊦  areaCirc cir ≐ x
                  ❘ =  ⟨ ( (πl radiusC) ⋅ ( πl radiusC) ) ⋅ pi_num , sketch "CircleArea Scroll"⟩
                  ❘ meta ?MetaAnnotations?label s"A(${lverb cir})"
                  ❘ meta ?MetaAnnotations?description s"The area of the circle ${lverb cir}"
        ❙

        meta ?MetaAnnotations?label "CircleAreaScroll" ❙
        meta ?MetaAnnotations?description s" This scroll is calculating the area of the circle ${lverb cir} via the formula A = ${lverb radiusC}⋅ ${lverb radiusC}⋅ pi" ❙
    ❚
 ❚