feat(arithmetic): add verified real-quadratic order

src/jacobian/domains/arithmetic/bundle.py

@@ -15,6 +15,10 @@
 from jacobian.domain_bundles import DomainBundle
 from jacobian.domains.arithmetic.integers import INTEGER_CAPABILITIES
 from jacobian.domains.arithmetic.rationals import RATIONAL_CAPABILITIES
+from jacobian.domains.arithmetic.real_quadratic import (
+    REAL_QUADRATIC_CAPABILITIES,
+    REAL_QUADRATIC_CHECKERS,
+)
 from jacobian.operations import (
     DomainDiagnostics,
     DomainSemantics,
@@ -50,7 +54,9 @@ def build_arithmetic_bundle() -> DomainBundle:
         capabilities=(
             *INTEGER_CAPABILITIES,
             *RATIONAL_CAPABILITIES,
+            *REAL_QUADRATIC_CAPABILITIES,
         ),
+        checker_declarations=REAL_QUADRATIC_CHECKERS,
         diagnostics=DomainDiagnostics(
             invalid_request=CapabilityDiagnostic(
                 code="INVALID_ARITHMETIC_REQUEST",

src/jacobian/domains/arithmetic/real_quadratic.py

@@ -0,0 +1,97 @@
+"""Typed real-quadratic order operation and checker declaration."""
+
+from jacobian.checker_operations import ExactReplayCheckerDeclaration
+from jacobian.contracts.capabilities import (
+    CapabilityInstallTier,
+    CapabilityProviderRuntime,
+)
+from jacobian.domains._examples import example
+from jacobian.domains.arithmetic._support import arithmetic_operation
+from jacobian.math.real_quadratic import (
+    RealQuadraticOrderRequest,
+    RealQuadraticOrderValue,
+    real_quadratic_order,
+)
+from jacobian.provider_runtime import source_provider_runtime
+
+
+def _real_quadratic_runtime(
+    *, checker_ids: tuple[str, ...] = ()
+) -> CapabilityProviderRuntime:
+    return source_provider_runtime(
+        "jacobian.real-quadratic-checker",
+        version="1",
+        entrypoint="jacobian_checkers.real_quadratic:check_real_quadratic_order",
+        install_tier=CapabilityInstallTier.T1,
+        license_id="MIT",
+        features=("standard-library-rational-replay", "clean-process-checker"),
+        checker_ids=checker_ids,
+    )
+
+
+REAL_QUADRATIC_CAPABILITIES = (
+    arithmetic_operation(
+        "arithmetic.real_quadratic.order.compute",
+        "Compare exact real quadratic values",
+        (
+            "Compare two bounded values a+b*sqrt(d) in one shared real quadratic "
+            "field, returning their exact difference and squared-magnitude sign data."
+        ),
+        RealQuadraticOrderRequest,
+        RealQuadraticOrderValue,
+        real_quadratic_order,
+        "arithmetic",
+        "real-quadratic",
+        "quadratic-surd",
+        "exact-order",
+        invocation_examples=(
+            example(
+                "pang_m4_scalar_gap",
+                "Compare 3*sqrt(3)/8 with 1/2+sqrt(3)/20 exactly.",
+                {
+                    "left": {
+                        "rational_part": {"num": "0", "den": "1"},
+                        "radical_coefficient": {"num": "3", "den": "8"},
+                        "radicand": 3,
+                    },
+                    "right": {
+                        "rational_part": {"num": "1", "den": "2"},
+                        "radical_coefficient": {"num": "1", "den": "20"},
+                        "radicand": 3,
+                    },
+                },
+            ),
+        ),
+    ),
+)
+
+REAL_QUADRATIC_CHECKERS = (
+    ExactReplayCheckerDeclaration(
+        "arithmetic.real_quadratic.order.compute",
+        RealQuadraticOrderRequest,
+        "check_real_quadratic_order",
+        "arithmetic.real-quadratic.fraction-square-replay",
+        entrypoint_module="jacobian_checkers.real_quadratic",
+        provider_runtime_factory=_real_quadratic_runtime,
+        replay_method="standard-library Fraction squared-magnitude replay",
+        reason=(
+            "operator-authorized standard-library checker independently compares "
+            "the exact rational and radical squared magnitudes"
+        ),
+        verification_capability_id="arithmetic.real_quadratic.order.verify",
+        verification_title="Verify an exact real-quadratic order",
+        verification_description=(
+            "Independently replay the shared-field difference, sign case, squared "
+            "magnitudes, and resulting order using exact rational arithmetic."
+        ),
+        verification_tags=(
+            "verification",
+            "exact",
+            "arithmetic",
+            "real-quadratic",
+            "order",
+        ),
+    ),
+)
+
+__all__ = ["REAL_QUADRATIC_CAPABILITIES", "REAL_QUADRATIC_CHECKERS"]

src/jacobian/math/real_quadratic.py

@@ -0,0 +1,189 @@
+"""Exact order in one real quadratic field."""
+
+from __future__ import annotations
+
+from fractions import Fraction
+from math import isqrt
+from typing import Literal, Self
+
+from pydantic import Field, StrictInt, model_validator
+
+from jacobian.contracts.exact import CanonicalRational, require_bounded_rational
+from jacobian.contracts.results import ContractModel
+
+_MAX_RADICAND = 1_000_000
+_MAX_DIGITS = 256
+RealQuadraticSignBasis = Literal[
+    "RATIONAL_ONLY",
+    "RADICAL_ONLY",
+    "SAME_SIGN",
+    "OPPOSING_SIGNS_SQUARED_MAGNITUDES",
+]
+
+
+def _is_square_free(value: int) -> bool:
+    return all(value % (divisor * divisor) for divisor in range(2, isqrt(value) + 1))
+
+
+def _order(left: Fraction, right: Fraction) -> Literal["LT", "EQ", "GT"]:
+    return "LT" if left < right else "GT" if left > right else "EQ"
+
+
+def _sign(a: Fraction, b: Fraction, d: int) -> int:
+    if b == 0:
+        return (a > 0) - (a < 0)
+    if a == 0:
+        return (b > 0) - (b < 0)
+    if (a > 0) == (b > 0):
+        return (a > 0) - (a < 0)
+    rational_square = a * a
+    radical_square = b * b * d
+    if rational_square == radical_square:
+        raise ValueError("square-free quadratic magnitudes cannot tie")
+    dominant = b if radical_square > rational_square else a
+    return (dominant > 0) - (dominant < 0)
+
+
+class RealQuadraticValue(ContractModel):
+    rational_part: CanonicalRational
+    radical_coefficient: CanonicalRational
+    radicand: StrictInt = Field(ge=2, le=_MAX_RADICAND)
+
+    @model_validator(mode="after")
+    def require_canonical_field_value(self) -> Self:
+        require_bounded_rational(
+            self.rational_part, max_digits=_MAX_DIGITS, label="rational part"
+        )
+        require_bounded_rational(
+            self.radical_coefficient,
+            max_digits=_MAX_DIGITS,
+            label="radical coefficient",
+        )
+        if not _is_square_free(self.radicand):
+            raise ValueError("real-quadratic radicand must be square-free")
+        return self
+
+
+class RealQuadraticOrderRequest(ContractModel):
+    left: RealQuadraticValue
+    right: RealQuadraticValue
+
+    @model_validator(mode="after")
+    def require_shared_field(self) -> Self:
+        if self.left.radicand != self.right.radicand:
+            raise ValueError("comparison requires one shared radicand")
+        return self
+
+
+class RealQuadraticSignCertificate(ContractModel):
+    rational_part_squared: CanonicalRational
+    radical_part_squared: CanonicalRational
+    magnitude_order: Literal["LT", "EQ", "GT"]
+
+
+class RealQuadraticOrderValue(ContractModel):
+    left: RealQuadraticValue
+    right: RealQuadraticValue
+    difference: RealQuadraticValue
+    order: Literal["LT", "EQ", "GT"]
+    sign_basis: RealQuadraticSignBasis
+    sign_certificate: RealQuadraticSignCertificate
+
+    @model_validator(mode="after")
+    def bind_exact_order(self) -> Self:
+        a = (
+            self.left.rational_part.as_fraction()
+            - self.right.rational_part.as_fraction()
+        )
+        b = (
+            self.left.radical_coefficient.as_fraction()
+            - self.right.radical_coefficient.as_fraction()
+        )
+        if (
+            self.difference.radicand != self.left.radicand
+            or self.difference.rational_part.as_fraction() != a
+            or self.difference.radical_coefficient.as_fraction() != b
+        ):
+            raise ValueError("difference must equal left minus right")
+        expected_order = (
+            "LT"
+            if _sign(a, b, self.left.radicand) < 0
+            else "GT"
+            if _sign(a, b, self.left.radicand) > 0
+            else "EQ"
+        )
+        if self.order != expected_order:
+            raise ValueError("order must match exact quadratic sign")
+        expected_basis: RealQuadraticSignBasis = (
+            "RATIONAL_ONLY"
+            if b == 0
+            else "RADICAL_ONLY"
+            if a == 0
+            else "SAME_SIGN"
+            if (a > 0) == (b > 0)
+            else "OPPOSING_SIGNS_SQUARED_MAGNITUDES"
+        )
+        if self.sign_basis != expected_basis:
+            raise ValueError("sign basis does not match difference structure")
+        rational_square = a * a
+        radical_square = b * b * self.left.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
+            != _order(rational_square, radical_square)
+        ):
+            raise ValueError("sign certificate does not match squared magnitudes")
+        return self
+
+
+def real_quadratic_order(
+    request: RealQuadraticOrderRequest,
+) -> RealQuadraticOrderValue:
+    a = (
+        request.left.rational_part.as_fraction()
+        - request.right.rational_part.as_fraction()
+    )
+    b = (
+        request.left.radical_coefficient.as_fraction()
+        - request.right.radical_coefficient.as_fraction()
+    )
+    d = request.left.radicand
+    sign = _sign(a, b, d)
+    basis: RealQuadraticSignBasis = (
+        "RATIONAL_ONLY"
+        if b == 0
+        else "RADICAL_ONLY"
+        if a == 0
+        else "SAME_SIGN"
+        if (a > 0) == (b > 0)
+        else "OPPOSING_SIGNS_SQUARED_MAGNITUDES"
+    )
+    rational_square = a * a
+    radical_square = b * b * d
+    return RealQuadraticOrderValue(
+        left=request.left,
+        right=request.right,
+        difference=RealQuadraticValue(
+            rational_part=CanonicalRational.from_fraction(a),
+            radical_coefficient=CanonicalRational.from_fraction(b),
+            radicand=d,
+        ),
+        order="LT" if sign < 0 else "GT" if sign > 0 else "EQ",
+        sign_basis=basis,
+        sign_certificate=RealQuadraticSignCertificate(
+            rational_part_squared=CanonicalRational.from_fraction(rational_square),
+            radical_part_squared=CanonicalRational.from_fraction(radical_square),
+            magnitude_order=_order(rational_square, radical_square),
+        ),
+    )
+
+
+__all__ = [
+    "RealQuadraticOrderRequest",
+    "RealQuadraticOrderValue",
+    "RealQuadraticSignCertificate",
+    "RealQuadraticValue",
+    "real_quadratic_order",
+]