[aliromman]

Prove a finite separation bound and implement a funded dyadic detector for a selected rational orthogonal inverse-circuit endpoint. If d is the path dimension, q counts named calls, A/B is the reduced Cayley parameter, and C is the product of all scalar denominators, every nonzero endpoint has magnitude at least eta = 1/[C(3B)^(dq)]. The detector pays all scalar amplification, matrix-entry quantization and data truncation, obtains error at most eta/4, and decides zero/nonzero at threshold eta/2. It does not use the exact endpoint as its decision oracle.

The written proof, detector, and exact receipt define the result. This answers the numerical-detectability limitation of the exact orthogonal witness. The complete rational register grammar retains every role, true named inverses and old values on aliased queries. A zero at one chosen tuple is not a universal equality certificate.

The sufficient precision and detector bit sizes are polynomial in the explicit program, word, scalar and parameter sizes after the path word is supplied. This is not a new bit-complexity theorem for the upstream coefficient producer. Matrix construction and qd² dense replay products remain paid. No optimal guard, IEEE backend guarantee, native Clifford relation, physical tape tariff, supplier admission or complete kappa improvement is claimed. The selected frontier remains unchanged at conditional kappa 60403/20000000.

Base: ff3cc58e370d0f678e529246f8c73e8094e18fcf. Ali Romman's PR #5315, consumed at 9bebc267c4608e51fcc94a543b8e0d66077cdfbb, supplies the orthogonal construction, literal action and retained test oracles. @krzysztofwojt supplied the inverse compiler and shortest-word theorem in PR #5262; retained notices credit @zxv for PR #5235 and the dirty-echo/tensor/phase and rational-series lineage. Source pins retain exact predecessor bytes in this branch's ancestry. Cayley transforms, Hadamard's determinant inequality and forward-error propagation are classical. Prepared by Ali Romman with substantial OpenAI Codex assistance; Apache-2.0.

Python 3.12 and its standard library:

python3.12 -B scripts/research_package.py --package research/orthogonal-witness-precision

Both registered isolated, warning-strict normal and optimized modes pass with PASS_ORTHOGONAL_WITNESS_PRECISION. All 102 cases pass: 24 zero and 78 nonzero, with every returned coordinate checked against its error bound. The tests include 101 separate dense exact comparisons, seven rejection controls, cancelling grid points, tiny parameter/discrepancy 2^-80, scalar gains 2^100, dirty returns and aliases. The stress case has 65,536 lowest-degree words, dimension 17 and a sufficient 2,262-bit fractional grid. Four actual code mutations fail in both modes before receipt comparison.

Committed bytes, every declared source pin's direct ancestry, official export integrity and both read-only Git-free replays pass; all 23 exported files remain unchanged. No independent human/proof-kernel review, selected cold replay, native tape, Lean, Docker or complete kappa calculation was run. The full-history wrapper remains unpassed in this shallow checkout. An optimized sparse or native-compatible detector needs a separate caller contract and complete error/cost comparison.

Hosted run 39996997226 passed planning and the registered Linux replay for published head 26fe40cbca6972a0e392e9248a9cb8a84368530b. Hosted execution is separate from independent scientific review.

[jwr404]

Independent review (James Reed, with Claude Code). Head 26fe40cbca6972a0e392e9248a9cb8a84368530b.

Verdict: the separation bound and the error analysis are correct. The threshold detector decides the selected endpoint as claimed.

Proof check

• §1 Cayley denominators.

  • K_a is skew, so P_a = 2BI + AK_a = M_aᵀ, and O_a = M_a⁻¹ M_aᵀ is orthogonal.
  • Path (tridiagonal) columns of M_a have squared norm at most 4B² + 2A², which is below 9B² for A ≤ B/4. Hadamard then gives det M_a ≤ (3B)^d, and det M_a > 0 because K has purely imaginary spectrum.
  • By the adjugate, entries of O_a and O_a⁻¹ = O_aᵀ are integers over D_a.

  The common-denominator induction (multiply by D_a per call and by scalar denominators per assignment or query, old values read before writing) gives |f| ≥ 1/[C(3B)^(dq)] for a nonzero difference, with C and q counted over both programs. ✓

• §2 Error recursion.

  • Propagation and quantization. For the computed step, |Q(x) − Q̃(x̃)| ≤ |Q(x) − Q(x̃)| + |(Q − Q̃)(x̃)| ≤ β_i E_(i−1) + γ_i h G.
  • Truncation. The final truncation adds at most h.
  • Bank bound. The computed bank stays within G, because quantized entries are at most 1 (row sum at most d) and truncation toward zero never increases magnitude.
  • Sum over steps. Suffix products are at most G, so E ≤ m G (ΓG + 1) h, and the stated choice of p makes E ≤ η/4.

  The two cases |f̂| ≤ η/4 and |f̂| ≥ 3η/4 follow. ✓ Using the transposed truncated table for G_a⁻¹ is exactly the entrywise truncation of the true inverse, since O⁻¹ = Oᵀ. That is a nice detail.

Independent spot check

I wrote separate exact code that draws random tridiagonal skew K with d ≤ 6 and t = A/B ≤ 1/4, B ≤ 40. Across 185 such cases, every one satisfies:

• 1 ≤ det M ≤ (3B)^d;
• O = M⁻¹Mᵀ is exactly orthogonal;
• all entries |O_ij| ≤ 1;
• D·O_ij is an integer.

No violations.

The registered replay passes locally (PASS_REGISTERED_RESEARCH_PACKAGE). The scope is accurately stated: a zero at one chosen tuple is not a universal identity certificate, and no speed claim is made over exact replay.