[aliromman]

This construction gives every false complete rational dirty linear identity with true named-generator inverses a positive-definite witness in dimension at most r+q. The generators can be arbitrarily close to identity. Each generator and its actual inverse has spectral condition number at most two. This closes the conditioning gap left by the inverse frontend and the earlier polynomial SPD construction. It does not change the complete kappa calculation or the selected frontier; a native-family adapter and physical admission remain absent.

The proof, exact receipt, source pins and literal checker are pinned to this reviewed head. Base: canonical main ff3cc58e370d0f678e529246f8c73e8094e18fcf, priority revision 7.

A nonzero Magnus coefficient of length D<r+q gives a symmetric labelled path in dimension d=D+1. With A_a=(1-e)I+(e/2)S_a, the endpoint has a nonzero leading term c(e/2)^D. Higher inverse-series terms can cancel a particular parameter. A common-denominator argument bounds the numerator degree by L=q_forward+d*q_inverse, counting both programs. One of L+1 rational grid points in any requested interval (0,e0], e0<=1/4, must therefore work. The generator spectra lie in [1-2e,1]; inverse spectra lie in [1,1/(1-2e)]. Only the generators are required to be contractions.

The grammar retains every independent input and every final role, including dirty helpers and self-source queries. It permits rational linear instructions and inverses of named square generators. Inverses of operator sums and additional commutation, Clifford, involution or native relations are outside scope. The public checker executes the complete program with exact tridiagonal inverse solves. It does not import the coefficient producer and does not certify shortestness or a positive equality case.

Verification uses Python 3.12 and the standard library:

python3.12 -B scripts/research_package.py --package research/spd-inverse-circuit-witness

Expected final marker:

PASS_REGISTERED_RESEARCH_PACKAGE research/spd-inverse-circuit-witness outcome=completed

Both registered modes pass: 160 reduced-group-word differential cases, including 40 equivalent and 120 different programs; 137 full replays against separate dense inverses; all eight source dirty-sandwich deletions; 154 exact inverse basis checks; and fourteen rejecting controls. Four cancellation fixtures force the final grid point, including G^-1-4/3 where the first point is zero and the second gives -4/21. The pinned inverse commutator gives discrepancy -1/35 in dimension three. A circuit with 2^32 lowest-degree words uses 66 realization states and a dimension-33 witness.

Four actual code mutations fail in normal and optimized modes before source-hash or receipt checks: wrong inverse action, a one-point grid, wrong query source, and discarded dirty returns. Committed bytes, every declared source-pin ancestry, export integrity and both read-only Git-free replays pass; all 19 exported regular files remain unchanged. The validation record records the boundaries. Hosted CI passed both planning and the focused replay at this exact head. The full-history wrapper was not run successfully in this shallow checkout; proof-kernel review, independent human review, selected cold replay and a native caller were not run.

Credit @krzysztofwojt for PR #5262, consumed at 6f92ccf1e61c4668c8ee687bd1df8b42932b8759: its proof supplies the inverse realization and coefficient bound. The consumed code, proof, notices and fixtures are retained byte-exact in this branch's ancestry. Its source notice retains @zxv's PR #5235, classical rational-series/Magnus/weighted-automata credit and the earlier dirty-echo, tensor and phase lineage. Ali Romman's PR #5268 supplies the related polynomial SPD construction; this result replaces its highest-degree step with a rational root grid. No new general PIT algorithm or global literature priority is claimed.

Prepared by Ali Romman with substantial OpenAI Codex assistance; Apache-2.0. Exact coefficient growth and runtime integer-text limits remain practical constraints, and a nonzero discrepancy can be too small for floating-point detection. The next open task is a source-bound native inverse-word adapter with every extra operator relation stated explicitly.