Add independently verified real-quadratic order

docs/reference/domain-operation-library.md

@@ -155,10 +155,11 @@ checks fraction-field equality by independent polynomial cross multiplication;
 pointwise denominator-definedness remains outside its scope. See
 [Rational-function identities](capabilities/polynomial/rational-function-identities.md).
 
-Some polynomial, matrix, graph, geometry, probability, topology, poset, and
-combinatorics results have a separate verification capability. The producer
-first returns a result artifact in `EXPLORE` mode. A verification request then
-supplies that exact `result_uri` to the matching `VERIFY` capability.
+Some arithmetic, polynomial, matrix, graph, geometry, probability, topology,
+poset, and combinatorics results have a separate verification capability. The
+producer first returns an exact result in `EXPLORE` mode. A verification request
+then supplies that result, inline or by artifact URI as declared by the
+contract, to the matching `VERIFY` capability.
 
 Domain-owned `ExactReplayCheckerDeclaration` values name the request model,
 certificate format, and checker function, but they carry no authority.
@@ -188,6 +189,13 @@ installed runtime.
 
 Bounded portfolio examples show the intended boundary:
 
+- `arithmetic.real_quadratic.order.compute` compares two bounded canonical
+  values `a+b*sqrt(d)` with one shared positive square-free radicand. It returns
+  the exact difference, order, and squared rational/radical magnitudes without
+  claiming general number-field arithmetic or matrix spectral computation.
+  `arithmetic.real_quadratic.order.verify` independently replays the comparison
+  with standard-library fractions and integer squares, without importing the
+  SymPy producer.
 - `graph.hamiltonian_path.decide` returns either a complete spanning path
   witness or a negative decision after exhausting its order-18 state space.
   `graph.hamiltonian_path.verify` checks a positive witness directly and

src/jacobian/contracts/arithmetic.py

@@ -8,11 +8,17 @@
 
 from __future__ import annotations
 
+from fractions import Fraction
+from math import isqrt
 from typing import Annotated, Literal, Self
 
-from pydantic import Field, StringConstraints, model_validator
+from pydantic import Field, StrictInt, StringConstraints, model_validator
 
-from jacobian.contracts.exact import CanonicalInteger
+from jacobian.contracts.exact import (
+    CanonicalInteger,
+    CanonicalRational,
+    require_bounded_rational,
+)
 from jacobian.contracts.results import ContractModel
 
 # ---------------------------------------------------------------------------
@@ -22,6 +28,8 @@
 _MAX_BASE = 10_000
 _MAX_NONNEGATIVE = 1_000
 MAX_BASE_DIGITS = 1_024
+MAX_REAL_QUADRATIC_RADICAND = 1_000_000
+MAX_REAL_QUADRATIC_DIGITS = 256
 
 # A positional digit is a small non-negative canonical integer string.  The
 # max length of 4 comfortably covers every base up to ``_MAX_BASE`` (10_000).
@@ -74,6 +82,88 @@ class IntegerNthRootRequest(ContractModel):
     degree: int = Field(ge=1, le=_MAX_NONNEGATIVE)
 
 
+# ---------------------------------------------------------------------------
+# Requests — real quadratic order
+# ---------------------------------------------------------------------------
+
+
+def _is_square_free(value: int) -> bool:
+    for divisor in range(2, isqrt(value) + 1):
+        if value % (divisor * divisor) == 0:
+            return False
+    return True
+
+
+def _fraction_order(left: Fraction, right: Fraction) -> Literal["LT", "EQ", "GT"]:
+    if left < right:
+        return "LT"
+    if left > right:
+        return "GT"
+    return "EQ"
+
+
+def _quadratic_sign(
+    rational_part: Fraction,
+    radical_coefficient: Fraction,
+    radicand: int,
+) -> Literal[-1, 0, 1]:
+    if radical_coefficient == 0:
+        if rational_part < 0:
+            return -1
+        if rational_part > 0:
+            return 1
+        return 0
+    if rational_part == 0:
+        return -1 if radical_coefficient < 0 else 1
+    if (rational_part > 0) == (radical_coefficient > 0):
+        return -1 if rational_part < 0 else 1
+    rational_square = rational_part * rational_part
+    radical_square = radical_coefficient * radical_coefficient * radicand
+    if rational_square == radical_square:
+        raise ValueError("square-free quadratic magnitudes cannot tie")
+    dominant = (
+        radical_coefficient if radical_square > rational_square else rational_part
+    )
+    return -1 if dominant < 0 else 1
+
+
+class RealQuadraticValue(ContractModel):
+    """One canonical real value ``a + b*sqrt(d)`` with square-free ``d``."""
+
+    rational_part: CanonicalRational
+    radical_coefficient: CanonicalRational
+    radicand: StrictInt = Field(ge=2, le=MAX_REAL_QUADRATIC_RADICAND)
+
+    @model_validator(mode="after")
+    def require_bounded_canonical_quadratic(self) -> Self:
+        require_bounded_rational(
+            self.rational_part,
+            max_digits=MAX_REAL_QUADRATIC_DIGITS,
+            label="real-quadratic rational part",
+        )
+        require_bounded_rational(
+            self.radical_coefficient,
+            max_digits=MAX_REAL_QUADRATIC_DIGITS,
+            label="real-quadratic radical coefficient",
+        )
+        if not _is_square_free(self.radicand):
+            raise ValueError("real-quadratic radicand must be square-free")
+        return self
+
+
+class RealQuadraticOrderRequest(ContractModel):
+    """Two values in one explicitly shared real quadratic field."""
+
+    left: RealQuadraticValue
+    right: RealQuadraticValue
+
+    @model_validator(mode="after")
+    def require_shared_radicand(self) -> Self:
+        if self.left.radicand != self.right.radicand:
+            raise ValueError("real-quadratic comparison requires one shared radicand")
+        return self
+
+
 # ---------------------------------------------------------------------------
 # Structured results — integer
 # ---------------------------------------------------------------------------
@@ -114,3 +204,76 @@ def require_canonical_digits(self) -> Self:
         if self.sign != 0 and self.digits[0] == "0":
             raise ValueError("nonzero positional digits cannot have a leading zero")
         return self
+
+
+# ---------------------------------------------------------------------------
+# Structured results — real quadratic order
+# ---------------------------------------------------------------------------
+
+
+class RealQuadraticSignCertificate(ContractModel):
+    rational_part_squared: CanonicalRational
+    radical_part_squared: CanonicalRational
+    magnitude_order: Literal["LT", "EQ", "GT"]
+
+
+class RealQuadraticOrderResult(ContractModel):
+    """Exact order and inspectable sign data for two real quadratic values."""
+
+    result_schema_version: Literal["1"] = "1"
+    left: RealQuadraticValue
+    right: RealQuadraticValue
+    difference: RealQuadraticValue
+    order: Literal["LT", "EQ", "GT"]
+    sign_basis: Literal[
+        "RATIONAL_ONLY",
+        "RADICAL_ONLY",
+        "SAME_SIGN",
+        "OPPOSING_SIGNS_SQUARED_MAGNITUDES",
+    ]
+    sign_certificate: RealQuadraticSignCertificate
+    arithmetic: Literal["EXACT_REAL_QUADRATIC"] = "EXACT_REAL_QUADRATIC"
+
+    @model_validator(mode="after")
+    def bind_exact_order(self) -> Self:
+        if not (self.left.radicand == self.right.radicand == self.difference.radicand):
+            raise ValueError("result values must share one radicand")
+        left_a = self.left.rational_part.as_fraction()
+        left_b = self.left.radical_coefficient.as_fraction()
+        right_a = self.right.rational_part.as_fraction()
+        right_b = self.right.radical_coefficient.as_fraction()
+        difference_a = left_a - right_a
+        difference_b = left_b - right_b
+        if (
+            self.difference.rational_part.as_fraction() != difference_a
+            or self.difference.radical_coefficient.as_fraction() != difference_b
+        ):
+            raise ValueError("result difference must equal left minus right")
+        sign = _quadratic_sign(difference_a, difference_b, self.difference.radicand)
+        expected_order: Literal["LT", "EQ", "GT"] = (
+            "LT" if sign < 0 else "GT" if sign > 0 else "EQ"
+        )
+        if self.order != expected_order:
+            raise ValueError("result order must match the exact quadratic difference")
+        expected_basis = (
+            "RATIONAL_ONLY"
+            if difference_b == 0
+            else "RADICAL_ONLY"
+            if difference_a == 0
+            else "SAME_SIGN"
+            if (difference_a > 0) == (difference_b > 0)
+            else "OPPOSING_SIGNS_SQUARED_MAGNITUDES"
+        )
+        if self.sign_basis != expected_basis:
+            raise ValueError("sign basis must match the exact difference structure")
+        rational_square = difference_a * difference_a
+        radical_square = difference_b * difference_b * self.difference.radicand
+        if (
+            self.sign_certificate.rational_part_squared.as_fraction() != rational_square
+            or self.sign_certificate.radical_part_squared.as_fraction()
+            != radical_square
+            or self.sign_certificate.magnitude_order
+            != _fraction_order(rational_square, radical_square)
+        ):
+            raise ValueError("sign certificate must contain exact squared magnitudes")
+        return self

src/jacobian/domains/arithmetic/bundle.py

@@ -11,8 +11,14 @@
 
 import platform
 
+from jacobian.contracts.arithmetic import (
+    MAX_REAL_QUADRATIC_DIGITS,
+    MAX_REAL_QUADRATIC_RADICAND,
+)
 from jacobian.contracts.capabilities import CapabilityDiagnostic
+from jacobian.domains.arithmetic.checkers import ARITHMETIC_EXACT_REPLAY_CHECKERS
 from jacobian.domains.arithmetic.integers import INTEGER_CAPABILITIES
+from jacobian.domains.arithmetic.quadratic import REAL_QUADRATIC_CAPABILITIES
 from jacobian.domains.arithmetic.rationals import RATIONAL_CAPABILITIES
 from jacobian.operations import (
     DomainBundle,
@@ -29,28 +35,43 @@ def build_arithmetic_bundle() -> DomainBundle:
         schema_namespace="jacobian.arithmetic",
         semantics=DomainSemantics(
             name="jacobian.exact-arithmetic",
-            version="1",
+            version="2",
             definition={
                 "description": (
                     "exact integer absolute value, sign, decimal digit sum/count, "
-                    "base expansion, integer nth root, and rational arithmetic/order "
-                    "over canonical integer and rational strings"
+                    "base expansion, integer nth root, rational arithmetic/order, "
+                    "and bounded same-radicand real-quadratic order"
                 ),
                 "integer_encoding": "canonical decimal string",
                 "rational_encoding": "canonical reduced num/den with positive denominator",
+                "real_quadratic_encoding": (
+                    "a+b*sqrt(d), with shared positive square-free d"
+                ),
                 "arithmetic": "exact via stdlib and maintained SymPy APIs",
-                "assurance": "computed; no independent checker",
+                "assurance": (
+                    "computed; real-quadratic order supports operator-authorized "
+                    "independent standard-library replay"
+                ),
             },
         ),
         provider_runtime=known_provider_runtime(
             "jacobian.sympy",
-            features=("exact-integer-arithmetic", "exact-rational-arithmetic"),
-            configuration={"sympy_version": SYMPY_VERSION},
+            features=(
+                "exact-integer-arithmetic",
+                "exact-rational-arithmetic",
+                "exact-real-quadratic-order",
+            ),
+            configuration={
+                "sympy_version": SYMPY_VERSION,
+                "real_quadratic_max_digits": MAX_REAL_QUADRATIC_DIGITS,
+                "real_quadratic_max_radicand": MAX_REAL_QUADRATIC_RADICAND,
+            },
         ),
         backend_version=f"python-{platform.python_version()};sympy-{SYMPY_VERSION}",
         capabilities=(
             *INTEGER_CAPABILITIES,
             *RATIONAL_CAPABILITIES,
+            *REAL_QUADRATIC_CAPABILITIES,
         ),
         diagnostics=DomainDiagnostics(
             invalid_request=CapabilityDiagnostic(
@@ -70,6 +91,8 @@ def build_arithmetic_bundle() -> DomainBundle:
         ),
         assurance_basis=(
             "deterministic exact arithmetic from the pinned stdlib/SymPy runtime; "
-            "no independent checker invoked"
+            "independent verification requires an explicit domain-owned verifier "
+            "invocation where declared"
         ),
+        checker_declarations=ARITHMETIC_EXACT_REPLAY_CHECKERS,
     )

src/jacobian/domains/arithmetic/checkers.py

@@ -0,0 +1,22 @@
+"""Independent checker declarations owned by exact arithmetic."""
+
+from jacobian.checker_operations import ExactReplayCheckerDeclaration
+from jacobian.contracts.arithmetic import RealQuadraticOrderRequest
+
+ARITHMETIC_EXACT_REPLAY_CHECKERS = (
+    ExactReplayCheckerDeclaration(
+        "arithmetic.real_quadratic.order.compute",
+        RealQuadraticOrderRequest,
+        "check_real_quadratic_order",
+        "arithmetic.real-quadratic-order.fraction-square-replay",
+        entrypoint_module="jacobian_checkers.real_quadratic",
+        replay_method="standard-library Fraction and integer-square replay",
+        reason=(
+            "operator-authorized standard-library checker independently compares "
+            "opposing real-quadratic terms without importing SymPy or producer code"
+        ),
+    ),
+)
+
+
+__all__ = ["ARITHMETIC_EXACT_REPLAY_CHECKERS"]