test(sign-det): verify nested infinitesimal roots against pinned Z3

.github/workflows/ci.yml

@@ -191,7 +191,7 @@ jobs:
         if: steps.classify.outputs.docs_only != 'true'
         run: |
           python3 -m pip install --user -r scripts/conway/requirements.txt \
-            python-flint==0.9.0 sympy==1.14.0 gmpy2 cypari2 conway-polynomials matplotlib==3.11.1
+            python-flint==0.9.0 z3-solver==4.15.4.0 sympy==1.14.0 gmpy2 cypari2 conway-polynomials matplotlib==3.11.1
           python3 -m unittest scripts/oracle/test_hermite_bench_drivers.py
           python3 -m unittest scripts/oracle/test_matrix_carriers.py scripts/oracle/test_rank_bench.py scripts/oracle/test_rank_stages.py
           python3 -m unittest scripts/bench/test_rank_measure.py scripts/bench/test_rank_analyze.py

HexSignDet/README.md

@@ -216,8 +216,30 @@ performance milestone is claimed here. See the [specification](SPEC/hex-sign-det
 for the complete contract and [#10377](https://github.com/kim-em/hex-dev/issues/10377)
 for the remaining assignment.
 
+The extension conformance target uses the existing `RationalFn Rat` and
+`RationalFn (RationalFn Rat)` coefficient fields with explicit exact signs at
+successive positive infinitesimals. Its independent oracle is pinned to
+`z3-solver==4.15.4.0` and numeric runtime version `(4, 15, 4, 0)`;
+its RCF API constructs roots and compares them exactly. Every fixture records the ordered
+coefficient levels and starts a fresh oracle context. The corrected
+`(εx²−1)(εx³−1)` example exercises the two positive partial descriptors,
+completion, root order, selected signs and cross-polynomial re-encoding without
+a rational separator. Two-level fixtures isolate `δ` from `ε` and `ε+δ` using
+an endpoint `2δ`. Both coefficient levels reject changed context, head and
+derivative-query bindings, and reject a multi-query table presented as a leaf.
+These leaf-arity checks do not test an identity-preserving incomplete support
+forgery. The oracle enforces each case’s coefficient depth and the corrected
+Passmore polynomial, and checks all five descriptor-error reasons. It separately
+rejects forged counts, reordered roots, altered encodings and context metadata.
+These test-only sign callbacks do not implement the ordered-function provider;
+tower-generated coefficient proofs, nested semantic replay, literal DAG
+serialization and all Phase-4 measurements remain required.
+
 Build the library and its regression target with:
 
 ```sh
-lake build HexSignDet +HexSignDet.Conformance
+lake build HexSignDet +HexSignDet.Conformance hexsigndet_emit_infinitesimal
+.lake/build/bin/hexsigndet_emit_infinitesimal > conformance-fixtures/HexSignDet/infinitesimal.jsonl
+python3 scripts/oracle/sign_det_z3.py --check
+python3 -m unittest scripts.oracle.test_sign_det_z3
 ```

conformance-fixtures/HexSignDet/README.md

@@ -1,4 +1,4 @@
-# Rational sign-table and descriptor fixtures
+# Exact sign-table and descriptor fixtures
 
 `sign_det.jsonl` contains 101 cases emitted by `hexsigndet_emit_fixtures`.
 The 59 table records include ascending rational polynomial coefficients as exact
@@ -52,7 +52,29 @@ python3 scripts/oracle/sign_det_flint.py --check
 python3 -m unittest scripts.oracle.test_sign_det_flint
 ```
 
-These fixtures validate rational sign tables and the implemented descriptor
-operations, including cross-polynomial comparison and re-encoding.
-Extension-field and nested-context conformance remain required. None of these fixtures proves general
-root-sum/Thom semantics or supplies Phase-4 performance evidence.
+`infinitesimal.jsonl` contains 29 cases emitted by `hexsigndet_emit_infinitesimal`
+using the existing rational-function fields over one and two positive
+infinitesimals. The independent Z3 RCF oracle requires `z3-solver==4.15.4.0`
+and numeric runtime version `(4, 15, 4, 0)`. Each record creates a fresh context
+and reconstructs the serialized coefficients with exact arithmetic. The oracle
+enforces the coefficient depth of each case and the corrected Passmore
+polynomial `(εx²−1)(εx³−1)`, then computes roots, signs and order independently.
+The cases cover sign tables, invalid domains, all five descriptor-error reasons,
+completion, selected signs, comparisons and re-encoding. Negative replay checks
+change context, head and derivative-query bindings or present a multi-query
+table as a leaf; the latter checks leaf arity, not identity-preserving incomplete
+support. The 16 adversarial Python tests also reject substituted case inputs,
+omitted support with preserved totals, wrong root order and version drift.
+
+```sh
+lake build hexsigndet_emit_infinitesimal
+.lake/build/bin/hexsigndet_emit_infinitesimal > conformance-fixtures/HexSignDet/infinitesimal.jsonl
+python3 scripts/oracle/sign_det_z3.py --check
+python3 -m unittest scripts.oracle.test_sign_det_z3
+```
+
+These fixtures validate rational and nested-infinitesimal sign tables and the
+implemented descriptor operations, including comparison and re-encoding.
+The infinitesimal sign callbacks are test providers. General coefficient
+interpretation, nested semantic replay and root-sum/Thom correspondence proofs
+remain required. None of these fixtures supplies Phase-4 performance evidence.