Add the norm equation and factoring layer for Ross-Selinger synthesis

[ciaranra]

Phase 2b of Clifford+T synthesis: the norm-equation and factoring layer. Builds on the exact rings and Matsumoto-Amano synthesis (#603) and the interval/grid machinery (#643). The synthesize_rz driver is the next and final phase. Governed by the phase-2 specification in the project design vault.

Contents

diophantine.rs -- solves t^dagger t = xi over D[omega] for a grid candidate's xi, returning one of three resolutions with deliberately asymmetric evidence rules:

• Solved { t } -- only ever constructed after an exact t^dagger t == xi check in the rings, on every path including xi = 0.
• Unsolvable -- requires PROOF: either strict double positivity fails (RS Definition C.1, needs no factoring, so it is checked first), or an odd exponent of a proved Z[sqrt2] prime over a proved rational prime p = 7 (mod 8) (RS Lemmas C.19/C.21/C.23).
• Exhausted -- everything else, including any obstruction resting on merely PROBABLE primality.

That asymmetry is the design's core: a wrong t is caught by the exact gate at the return boundary, but a wrongly DISCARDED candidate is invisible to it forever, so probable primality may be used constructively and may never obstruct.

The scaled equation is solved UP TO ASSOCIATES. Demanding an exact s^dagger s = xi' after the RS Lemma C.25 scaling is unsatisfiable for odd scaling exponents -- scaling by sqrt2 can destroy double positivity (xi = (2+sqrt2)/2 is solvable by t = delta/sqrt2, yet sqrt2 xi = 1+sqrt2 has negative bullet embedding, and every nonzero dagger norm is doubly positive). The leftover unit after delta^-l unscaling is doubly positive, hence exactly lambda^2k, and is square-rooted exactly per RS Lemma C.2 and the proof of C.16. The counterexample is a regression test.

factor.rs -- sieve below 2^16, Brent-cycle Pollard rho over an explicit heap worklist, deterministic 12-base Miller-Rabin below 2^64 (valid because psi_12 > 2^64, Sorenson-Webster Theorem 1.1) and seeded probable-prime rounds above it, Tonelli-Shanks with a canonical [0, p/2] root, and domain-separated seed streams via nth_derived_seed. Every loop carries a budget; there are no wall-clock budgets and no floating point anywhere in the crate.

Supporting exact gcds, canonical associates (absolute embedding ratio normalized into [1, lambda^2)), and quotient rounding were added to the Z[sqrt2] and Z[omega] rings. Everything is pub(crate); this PR adds no public API.

Review history

An adversarial review of the packet against the specification, before any code existed, found seven defects -- including one INHERITED FROM THE SPEC: it demanded the exact scaled solve described above as unsatisfiable. Three prior review rounds on that spec had missed it. The spec was corrected first (vault marker F15), then the packet.

An adversarial review of the implementation returned REVISE with four findings, all reproduced or confirmed against the code before being acted on:

1. canonical_associate bounded its normalization loop by field norm -- unsound, because every unit lambda^k has field norm 1 while normalization takes |k| steps. gcd(lambda^100, 0) panicked. The bound now derives from coordinate bit length, and exhaustion returns None rather than asserting.
2. Recursive factoring gave stack depth linear in a repeated factor's exponent; it is now an explicit heap worklist with per-node budgets and traversal order preserved (per-integer budgets are the specified semantics and are unchanged).
3. Denominator scaling bypassed every budget and walked lambda^l linearly; scaling exponents are now capped at 4096 (following the tolerance-exponent precedent from Add the interval arithmetic and grid solvers for Ross-Selinger synthesis #643) and all powers use exponentiation by squaring.
4. primality_rounds == 0 returned Probable having tested nothing; zero rounds are now rejected at parameter validation.

The same review independently confirmed the mathematics against RS Appendix C, audited every Unsolvable return and every discard path for silent factor loss (none found), and ran 12,000 generated norms and 277,050 modular-root cases against brute force.

Verification

• 63 tests. Seven mutations killed, re-run after the final fixes: removing the exact verification gate; returning Unsolvable on probable-prime evidence; skipping the double-positivity check; flattening the odd-exponent bullet parity; removing zero-round validation; removing the scale cap; restoring the unsound field-norm bound.
• The reviewer's panic reproducer (gcd(lambda^k, 0) for k up to 500) no longer panics.
• In-crate --locked clippy with -D warnings, workspace check, fmt, pre-commit -- all clean, run cold.

[ciaranra]

A second adversarial review, scoped to the fix commit 3b1cba7d7 alone, returned SHIP with no must-fixes. It was explicitly walled off from the settled material (Appendix C mathematics, the proof-boundary and discard-path audit, the exact t^dagger t == xi gate) so the round spent its budget on the ~200 previously unreviewed lines.

The load-bearing question was whether the replacement normalization bound in canonical_associate is genuinely sound, rather than a second instance of the defect it replaced. The review supplied a derivation: for nonzero z with maximum coordinate bit length B, each complex embedding satisfies |sigma(z)| < 2^(B+2); the product of the two squared embedding magnitudes is the nonzero integral field norm and so is at least 1; hence either ratio is below 2^(4B+8). Each normalization step moves that ratio by lambda^4 > 2, so fewer than 4B+8 steps suffice against an implemented budget of 8(B+8). Verified independently: lambda^4 = 33.970563, and 8(B+8) - (4B+8) = 4B+56 > 0 for all B >= 0. Zero never reaches canonicalization -- gcd intercepts it.

Also confirmed: the worklist reproduces the recursive depth-first order (larger child pushed first), leaving seed-stream consumption and per-node budgets unchanged, and Pollard-Brent returns only 1 < d < n so both children strictly decrease and trivial-factor cycling cannot occur; the squaring helpers are correct at exponents 0, 1, and negative, with the scale cap enforced before any large allocation; and validation covers every production path into probable-primality classification.

One low-severity item is deliberately deferred rather than fixed here. FactorParams::validate runs before the exact zero result and the proof-independent positivity rejection, so primality_rounds == 0 turns those into Exhausted even though neither can reach probable-primality classification; and FactorError::Exhausted conflates invalid configuration with a consumed search budget. Both are safe (no false Unsolvable is reachable) and the layer is crate-private. The proper fix is a distinct InvalidParameters variant, which belongs with the phase-2c driver that will own the public parameter surface.