GC-03.02 · Symbolic Model & Source

Companion symbolic Python construction for GC-03.02 · Tran Quang Hung’s Square Midpoint Circle Division (GC-03.02).

Programmatic Usage

from geometor.divine.catalog import build_construction

        model, cert = build_construction("GC-03.02")
        assert cert.ratio_expr == sp.GoldenRatio
        

Exact Builder Implementation

def build_tran_square_midpoints() -> ConstructionResult:
            """Tran Quang Hung's square midpoint circle construction (Buratino 1)."""
            m = new_catalog_model("tran-square-midpoints")
            A = m.set_point(-2, 2, classes=["given"], ID="A")
            B = m.set_point(2, 2, classes=["given"], ID="B")
            C = m.set_point(2, -2, ID="C")
            D = m.set_point(-2, -2, ID="D")
            F = m.set_point(0, 0, ID="F")

            M = m.set_point(0, 2, ID="M")
            N = m.set_point(2, 0, ID="N")
            P = m.set_point(0, -2, ID="P")
            Q = m.set_point(-2, 0, ID="Q")

            m.construct_polygon([A, B, C, D], ID="ABCD")
            ln_qn = m.construct_line(Q, N, classes=["golden"], ID="QN")
            ln_mp = m.construct_line(M, P, classes=["auxiliary"], ID="MP")
            m.construct_segment(A, P, classes=["auxiliary"], ID="AP")

            K = m.set_point(-1, 0, ID="K")
            c_ka = m.construct_circle(K, A, classes=["compass"], ID="cKA")
            X = m.intersect(c_ka, ln_qn, between=(F, N), classes=["golden"], ID="X")

            ln_ax = m.construct_line(A, X, classes=["auxiliary"], ID="AX")
            Z = m.intersect(ln_ax, ln_mp, classes=["golden"], ID="Z")
            _ = Z

            return make_result(m, ("F", "X"), ("X", "N"), ("F", "X", "N"))
        

Exact Symbolic Point Coordinates

All points in tran-square-midpoints are certified free of floating-point approximations over \(\mathbb{Q}(\phi)\):

Point

Exact \(x\)

Exact \(y\)

A

\(-2\)

\(2\)

B

\(2\)

\(2\)

C

\(2\)

\(-2\)

D

\(-2\)

\(-2\)

F

\(0\)

\(0\)

M

\(0\)

\(2\)

N

\(2\)

\(0\)

P

\(0\)

\(-2\)

Q

\(-2\)

\(0\)

K

\(-1\)

\(0\)

X

\(-1 + \sqrt{5}\)

\(0\)

Z

\(0\)

\(3 - \sqrt{5}\)

Certified Golden Ratio: FX / XN = GoldenRatio.