Reals: a constructive pi for the constructive Cauchy reals with a strong irrationality separation theorem (Leibniz series) #315

Hi, I would like to propose adding a concrete pi instance to theories/Reals/Cauchy/, on top of the escape-window separation engine proposed in #312/#313 (a PR follows this issue).

What. A constructive realizer pi_leibniz : CReal for pi, together with a strong irrationality statement: pi is apart, in the sense of CReal_appart, from every embedded rational constant, with explicit witnesses:

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

The premise b <> 0 only says that a / b is a rational number; the underlying statement is premise-free:

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

Why here. As far as we know, the constructive Cauchy reals of ConstructiveCauchyReals currently carry no concrete construction of pi (the pi of Rtrigo belongs to the classical reals). The engine of #312/#313 reduces "a concrete constructive real is apart from every rational" to supplying a family of positive escape-window widths that decays slower than the resolution 2 * 2^(-n) of CReal. The alternating Leibniz series for pi comes with exactly such a family at the purely rational level (for the antecedent device — computing pi from alternating series with easy error bounds — see O'Connor 2008 and Krebbers and Spitters 2013, in the tradition of exact real arithmetic; both aim at efficient computation rather than at separation statements): this proposal supplies that family, converts it into a CReal modulus, and loads the engine, so that the strong irrationality of pi follows from the engine theorem with no further analytic input. Quantitative separation of pi from the rationals is classical (Mahler 1953); the present development strengthens the classical effective bound into constructive, machine-checked, extraction-ready per-rational witnesses.

Proposed files (five new files in theories/Reals/Cauchy/; working names — happy to rename the family to match the directory's ConstructiveCauchy* style):

The total is 21,129 lines (counts of the files as prepared for submission at the time of writing; the accompanying PR gives the final per-file counts).

Method.

• Window bounds at the rational level. The partial sums 4 * S(2k+2) of the Leibniz series 4 * (1 - 1/3 + 1/5 - 1/7 + ...) satisfy explicit two-sided bounds: even and odd partial sums interlace, the absolute steps 1/(2k+1) decrease monotonically with computable gaps, and the distance from any rational q to the partial-sum sequence is eventually bounded below by an explicit positive margin c.
• From window bounds to a CReal modulus. pi_leibniz samples the partial sums at exponentially growing depth: its value at index -n is the partial sum at depth 2^n. The alternating tail bound |S_k - S_n| <= |t_n|, combined with this depth floor, places every sampling point within the resolution 2^k and yields the cauchy component of the CReal record.
• Loading the engine. The margin c, a threshold N0 beyond which the window widths fall below c, and an index n0 satisfying N0 <= n0 and N <= 2^n0 (for the window order N of the margin step) produce a witness of creal_escape_window pi_leibniz e for the pi-specific window family e; the final step applies creal_escape_window_apart and is not proved again.

Properties.

• Assumption-free: Print Assumptions reports Closed under the global context for both main statements, and coqchk -o reports an empty assumption context over the whole dependency closure.
• All statements are in sort Set (sigma witnesses and the CReal_appart sum), mirroring the design of CRealLt and of the engine; the only Prop occurrences are Qlt predicates inside sigma types. The extracted OCaml contains zero Obj.magic.
• The proofs are explicit chains of rational-order lemmas; no automation tactic closes the main statements (lia appears only in small integer and rational literal bookkeeping steps, as in the engine file). Self-contained: the five files require only Stdlib modules, in the style of the engine file, plus ConstructiveCauchyRealsSep; no existing file is modified.
• Computational sanity checks accompany the PR: vm_compute-level probes verify the window inequalities at sample points (the resolution coupling at depth 3; the escape inequality for q = 22/7 at depth 8). In the pi instance the apartness witnesses are constructed by proof and are opaque through Qed; the computable escape-index-selector property concerns the engine itself (Add escape-window separation engine for the constructive Cauchy reals #313).

Scope. This proposal delivers the apartness form (CReal_appart), matching the engine's conclusion shape. An equation-level transport is left open: the equality on CReal in the host library is a Prop-valued double negation, and a Set-level pointwise equation layer does not transfer verbatim. Only the pi instance is included: the method is constant-agnostic, but further constants are left to future work, and only the Leibniz-series realizer is proposed (a geometric construction of pi via cosine zeros exists in the wider development and is deliberately out of scope).

Relation to #312/#313. This proposal is a concrete instance of the abstract criterion of #312/#313: PiSeparation.v loads the engine with a pi-specific window family, and the final step applies creal_escape_window_apart unchanged; no credit is claimed for the criterion itself. The accompanying PR is stacked on the current head of #313 and declares this dependency.

Happy to adjust naming, statement shape, granularity (single file versus the five-file layout proposed here), or file placement per maintainer preference.

Developed as part of the same independent constructive-formalization campaign as #312/#313; the abstract escape-window criterion is due to #312/#313 and is reused here unchanged.