package rocq-pi-leibniz

A constructive pi for the constructive Cauchy reals of the Rocq standard library ([ConstructiveCauchyReals]), realized by the alternating Leibniz series, with the strong irrationality separation theorem

Theorem pi_leibniz_strong_irrational : forall a b : Q, b <> 0 -> CReal_appart pi_leibniz (inject_Q (a / b)).

together with its premise-free companion

Theorem pi_leibniz_appart_all_Q : forall q : Q, CReal_appart pi_leibniz (inject_Q q).

pi is apart, in the sense of [CReal_appart], from every embedded rational constant; the apartness witness comes with an explicit positive margin and an explicit convergence modulus for the realizer.

Every witness is explicitly constructed and the statements are [Set]-valued throughout, so the witnesses are extractable: the extracted OCaml carries zero [Obj.magic]. Both main statements are premise-free and closed under the global context ([Print Assumptions] reports "Closed under the global context"; the [coqchk -o] assumption summary is all-none). Sample points run in the REPL with [vm_compute]: for [q = 22 # 7] the escape-witness triple computes to [(22 # 7, 5 # 8, 3%nat) : Q * Q * nat].

The content modules compile green on Rocq 9.1 locally and across the CI matrix of the hosting standard-library submission (Alpine build and Rocq 9.2 / 9.3 / master Nix bundles; 180/180 checks passed at the submitted head), as an integral part of the standard-library tree.