[hy7pc8gfmf-dotcom]

Referral chain: stdlib#316 (proux01's referral) -> #227 -> this draft.

This is a discussion-stage draft — not requesting merge yet. It accompanies #227 ("Constructive pi with extractable separation witnesses") by making the CoRN-native form of the separation engine concrete and CI-testable; happy to rework the scope, or to hold the whole thing, per maintainer preference.

---

Escape-window separation for the fast constructive reals

This PR adds reals/fast/CrnEscapeSep.v (287 lines), an abstract
irrationality criterion for the fast constructive reals CR.

Main statements (premise-free at top level, no axioms, no classical
logic):

• crn_escape_window x e : Set — the escape property: every rational
  q eventually escapes the window of width e n around the
  2^(-n) approximation of x, while e n dominates twice the
  dyadic resolution at the same index.

• crn_escape_window_apart : crn_escape_window x e -> forall q, CRapartT x ('q) — x is apart from every embedded rational, with
  an extractable side certificate: CRapartT is the disjoint sum
  that exhibits on which side of q the number x lies, and each
  component carries a positive rational distance witness
  (CRltT = CRpos (y - x)).

Compared with the corresponding construction for the standard
library's CReal, the engine is shorter: the positivity witness of
CRpos_char is a single positive rational value, so the Archimedean
index pushdown disappears; the witness is the quarter of the escape
margin, and the coherence of the approximation function transports
the escape inequality across precisions.

Relation to CRpi: this criterion is the separation half of a
second, independent route to pi. The alternating Leibniz series
construction (developed on the standard-library side, referred in
issue #227) instantiates the escape family and thereby yields, for
every rational q, an explicit computable margin with
c < |p_m - q| for all large m — extractable separation
witnesses complementing the equality route CRpi provides.

Build: picked up automatically by SCons and configure/make
(reals is already listed in dirs_to_compile/DIRECTORIES).
_CoqProject carries no per-file lines at HEAD, so no registration
edit is needed; should maintainers prefer explicit IDE registration,
a one-line addition can follow. No new external dependencies
(MathClasses and the stdlib QArith/Qabs/Qpower only).

License: GPL-2.0-or-later (header included), converted one-way
from the LGPL-2.1 standard-library sibling per LGPL-2.1 §3.