Add the interval arithmetic and grid solvers for Ross-Selinger synthesis

[ciaranra]

Phase 2a of Clifford+T synthesis: the interval arithmetic and grid-candidate machinery for Ross-Selinger Rz approximation. Builds on the pecos-synth crate (#603); the norm equation, factoring, and the synthesize_rz driver are subsequent work. Governed by the phase-2 specification (v4, three math-review rounds) in the project design vault.

Contents

interval.rs -- dyadic fixed-point intervals over BigInt with sign-aware outward rounding (floor/ceil division on signed values, never %), octant-reduced cos/sin enclosures with Lagrange remainders added outward, the exact 65-bit half-angle from an Angle64 fraction (theta in (-pi, pi], so theta/2 in (-pi/2, pi/2]), a 1024-bit pi constant with documented provenance, sqrt enclosures, and a shared precision-retry policy that surfaces SynthError::Inconclusive { precision } at the caller's ceiling rather than looping.

grid.rs -- the closed epsilon-cap per RS Eq. 13-14; an enclosing ellipse of the cap with in-comment proofs of BOTH containment and a uniform area bound (C = 3; ratio limits 3pi/4, 2, 2sqrt2 across the regimes), which is what RS Prop. 5.17 / Thm. 5.18 need for efficient enumeration; Appendix-A uprighting with pinned residual choices; the 1D solver per RS Prop. 4.5 with a fully SYMBOLIC normalization count (exact dyadic-vs-Z[sqrt2] comparisons -- no interval arithmetic in the loop condition); both candidate branches with the shifted branch's k = lde(u') and recovery via delta^{-1} = (omega - i)/sqrt2; RS Lemma 5.5 coset enumeration; and exact closed-cap filtering with an exact ring path for pi/2-grid targets (there z lies in Z[omega]; the shifted branch's dot >= d|delta| is decided by a sign split and one squaring against |delta|^2 = 2 + sqrt2).

Everything is pub(crate); the only public additions are the SynthError::Inconclusive variant and nothing else. No floating point exists in either module.

Review history

An adversarial math review (web-verified against RS) initially returned DO-NOT-MERGE on two totality defects: valid inputs could become permanently Inconclusive at the 1D normalization endpoint (width exactly 1 -- two inexact enclosures of the same irrational never resolve) and at exact closed-cap boundary candidates (e.g. theta = pi/2, epsilon = 3/8, u = (119/128) z). Both are fixed by the exact symbolic paths above, each with a verbatim regression. The same review independently re-derived the ellipse (confirming C = 3), the delta-inverse identity, and the pi constant via its own Chudnovsky computation. A closure round confirmed all findings resolved (MERGE-WITH-FOLLOWUPS); its one follow-up -- an impractically large tolerance exponent could eagerly allocate a ~512 MiB numerator instead of erroring -- is fixed here by capping log_denominator at 4096 with a regression.

A mutation test also exposed that a broken endpoint comparison would HANG the normalization loop rather than fail; the loop now carries a defensive iteration bound (bits + precision + 8 -> ExponentOverflow), and the same mutant now fails fast.

Verification

• 38 tests, including: brute-force cross-checks of the 1D solver (set AND order) and of both 2D branches against bounded scans that do NOT derive their search region from the ellipse; sampled ellipse containment plus the area bound across an epsilon ladder covering both regimes (h ~ 1.01, h ~ 1.98); the three reviewer reproducers; determinism of the full candidate stream.
• Mutations killed: flipped outward-rounding direction; shifted-branch k swapped to lde(u); exact-cap threshold off by one ulp; endpoint inclusivity flipped (fails fast via the loop bound).
• In-crate --locked clippy with -D warnings, workspace check, fmt, pre-commit -- clean.

Driver-facing note

RS Lemmas 7.2/9.6 assume epsilon < 2 sin(pi/16); this layer accepts any 0 < epsilon < 2 and documents that the later synthesize_rz driver owns the Clifford shortcut above that threshold.