Add independently verified real-quadratic order

[kaoru0822-kitauji]

Summary

• add arithmetic.real_quadratic.order.compute for two bounded canonical values a+b*sqrt(d) with one shared positive square-free radicand
• retain the exact difference, order, sign basis, and squared-magnitude certificate in a typed result
• add operator-authorized arithmetic.real_quadratic.order.verify, replayed in a clean process with standard-library Fraction and integer squares and no SymPy or producer import
• keep the scope deliberately below general algebraic-field arithmetic and matrix spectral computation

Grace-style reproduction

Primary source: Zhekai Pang, Counterexamples to a multivariable matrix Young conjecture, arXiv:2607.11866v1 (2026), Theorem 1, m=4: https://arxiv.org/abs/2607.11866

Frozen proof-critical scalar subproblem:

L = 3*sqrt(3)/8, R = 1/2 + sqrt(3)/20, so
L-R = -1/2 + 13*sqrt(3)/40 > 0, certified by
1/4 < 507/1600.

The authenticated Codex CLI arms used gpt-5.4-mini, low reasoning, one run per arm, the same task/schema/oracle, and isolated non-editable installs.

Arm	Result
installed main at 6df30e45	mathematics passed, evidence failed; 7 math.find calls, 0 math.run calls, and all producer/verifier fields were absent
this branch	mathematics and evidence passed; direct discovery of the new operation, one producer run (COMPUTED), one independent verifier run (VERIFIED), record artifact://sha256/dd0a28b19009e1bc4608c588ecc2797e8d4b7f0ffb19232ef7c645ea070530a4

Frozen input hashes:

• task: 9a7931639f7d30c29b14498c9cc47f1a413e21465fdc386ce0035aea7063d6e5
• output schema: 5f3de7ef08dfc9620b99c3d8deabb33d558980529a004e460116ace5b135e9d4
• independent oracle: 8ac04cd7a184a362cf183da3d8ed02122d136bd3ae5ebd888d16ea8fe0fcfb29
• policy: COMPUTE_VERIFY_NO_RETRIEVAL, digest sha256:0749b72e4263a380432feb9973b0fda9d5ed2b04d29417a1262bfc45134c71c6
• baseline catalog: sha256:98488060424b44551f7e0d920f6c59a2e76890315a7c34ef5076f1644fd6c23f
• treatment catalog: sha256:81e61b33f46e7ebce8dd68a0203389850609393565829588136bb42b7c9b1fa5

The treatment verifies only the supplied scalar comparison, not Pang's general theorem. This is a bounded slice motivated by #939 and does not claim the general simple-algebraic-field surface discussed in #916.

Validation

Planner: make test-plan BASE=origin/main.

Passed on the final tree:

• make lint typecheck
• make docs-linkcheck
• make test-unit (872 passed)
• make test-domain (324 passed)
• make test-composition (319 passed, 2 skipped)
• make test-storage (126 passed)
• make test-mcp (52 passed; rerun after replacing a now-recognized arithmetic unknown-domain sentinel)
• make test-e2e (7 passed, 1 Lean-runtime skip)
• focused producer/verifier, contract-bound, checker-installation, and portfolio tests

Two unrelated host-specific selected-lane cases remain for hosted CI to adjudicate:

• make test-component: 788 passed, 3 skipped; the existing macOS one-second DRAT timeout-marker race failed when the marker file was not created before process termination
• make test-process: 243 passed, 1 skipped; macOS Bash 3.2 lacks mapfile

Hosted CI is expected to run these lanes in the supported Linux environment.

[morluto]

Second-pass architecture review: draft looks sound. The capability is intentionally narrow, typed, exact, and domain-owned; the producer remains COMPUTED and the standard-library replay is a separate operator-authorized verification path. It also avoids turning the motivating theorem into a workflow or overbroad algebraic-field abstraction. I would proceed after the stated hosted Linux lanes.

[morluto]

Post-cutover architecture audit

Disposition: retain the reusable mathematical core, rewrite the operation.

Make the parent field identity structural: a real-quadratic value must carry the same positive square-free radicand as its coefficients, and comparison must reject values from different parents. Prefer a reusable RealQuadraticValue plus a compare/sign operation over a theorem-shaped result with duplicated difference/order/certificate representations.

The domain function can return a small sealed result containing comparison and the minimal exact sign witness; a separate checker may replay that claim without SymPy. Rebase onto current main, remove generic assurance/relationship/version machinery, and keep the Pang example, equal/negative cases, square-free validation, and incompatible-radicand failures.

[morluto]

Post-#1256/#1265 review: keep the capability, but substantially revise the implementation before merge. It is not already present on current main.

The mathematical operation is useful and well-scoped: exact order in one real quadratic field with an independently replayable certificate. The branch, however, puts the semantic kernel in domains/arithmetic/quadratic.py, operates directly on wire/Pydantic request/result values, and binds SymPy there. The current dependency direction wants the supported mathematical function/value under jacobian.math, with backend conversion private, then one OperationSpec adapting the boundary request to that semantic function.

Recommended restack:

• make the real-quadratic value/ordering semantics domain-owned under the current public math surface;
• keep exactly one canonical semantic input representation and a private SymPy adapter if needed;
• let the capability request/result models be wire/boundary projections rather than the mathematical implementation itself;
• keep the independent checker as a separate operation; do not restore result assurance/relationship metadata.

So: revise, not supersede. Preserve the math/tests, but use this as a clean example of the new operation budget rather than adding another legacy-style domain mini-stack.

[morluto]

Superseded by #1287. The replacement puts exact a+b*sqrt(d) values and squared-magnitude order semantics in a provider-independent math module, exposes one thin arithmetic operation, and uses a dedicated Fraction checker. It does not introduce a general algebraic-field framework or generic assurance metadata.

[morluto]

Superseded by #1287 after the ownership-model rewrite. The original real-quadratic capability, reproduction, and verification work here remains credited to @kaoru0822-kitauji; #1287 is a current-tree port/rework, not a rejection or reassignment of this contribution.

[morluto]

Superseded by #1287, which carries the clean post-#1276 semantic port and explicitly credits @kaoru0822-kitauji for the original investigation, reproduction, and implementation work. Closing this older branch so there is one authoritative implementation.