Operational vs Semantic Equality: A Machine-Checked Separation of Completion and Finite Attainment in the Gregory-Leibniz Construction of Pi

Abstract

This work develops a finite-attainment framework for distinguishing mathematical completion from finite operational realization. The foundational significance is that completion is treated as an extension of the mathematical domain rather than as a hidden terminal event of the finite generating process. This provides a contemporary formal setting for revisiting the distinction between potential construction and actual completion that historically underlies the Hilbert–Brouwer divide, without denying the internal coherence of classical real analysis or completed Euclidean geometry.--------------------------------Research classification. Mathematics; pure mathematics; foundations of mathematics; philosophy of mathematics; mathematical logic; mathematical analysis; real analysis; Euclidean geometry; formal methods; formal verification; formalized mathematics; interactive theorem proving; machine-checked mathematics. Research question. This preprint studies the foundational distinction between exact equality in a completed semantic domain and exact attainment at a finite stage of the generating process. The traditional real number pi and the Gregory-Leibniz construction of pi are used as the concrete machine-checked test case. No alternative value of pi is introduced or used.