feat: tighten domain diagnostics and Gaussian inputs

Author: morluto

benchmarks/tooling/codex_visibility.py

@@ -463,8 +463,7 @@ def _codex_arguments(
     tool_mode: ToolMode,
 ) -> tuple[str, ...]:
     arguments = [
-        "-a",
-        "never",
+        "--approve-for-me",
         "exec",
         "--ephemeral",
         "--skip-git-repo-check",

docs/reference/capabilities/graphs/graph-distance-matrix.md

@@ -43,8 +43,8 @@ verification of the distance claim.
 
 ## Independent verification
 
-`graph.distance_matrix.verify` consumes one stored producer result and can
-promote that exact matrix to `VERIFIED`. The operator-authorized checker uses
+`graph.distance_matrix.verify` consumes the exact producer input plus one complete
+typed candidate inline and can promote that matrix to `VERIFIED`. The operator-authorized checker uses
 only Python standard-library adjacency sets, queues, and integer distances. It
 does not import NetworkX or the producer package.
 
@@ -55,9 +55,9 @@ checks. Acceptance still requires an exhaustive breadth-first traversal from
 every source and exact comparison of every finite distance and unreachable
 `null`.
 
-The verification record is bound to the exact graph input artifact, matrix
-result artifact, schemas, semantics, checker source digest, witness format, and
-provider runtime. Rejection, timeout, cancellation, unavailable runtime, or
+The verification record is bound to the canonical graph input and matrix
+candidate digests, semantics, checker source digest, and provider runtime.
+Rejection, timeout, cancellation, unavailable runtime, or
 checker error remains `UNKNOWN` and cannot produce `VERIFIED`.
 
 ## Public composition evidence

docs/reference/capabilities/graphs/graph-maximum-matching.md

@@ -6,20 +6,20 @@
 matching together with a Tutte–Berge barrier certificate. The producer remains
 `COMPUTED`. An operator-authorized
 `graph.invariant.maximum_matching.verify` capability may promote the exact
-stored result to `VERIFIED` only after independent clean-process replay.
+submitted `{input, candidate}` claim to `VERIFIED` only after independent
+clean-process replay.
 
 ## Exact claim and scope
 
 The verifier checks one claim:
 
-> The stored witness edges form a maximum-cardinality matching of the exact
-> stored finite simple undirected graph.
+> The submitted witness edges form a maximum-cardinality matching of the exact
+> submitted finite simple undirected graph.
 
-The claim is bound to the producer input artifact, result artifact, graph
-semantics, result schema version, checker identity, and checker provider
-runtime. It does not certify a graph supplied directly by the caller, a
-different matching, or any theorem that uses the matching as an intermediate
-fact.
+The claim is bound to canonical producer-input and candidate digests, graph
+semantics, checker identity, and checker provider runtime. It does not certify
+a different graph or matching, or any theorem that uses the matching as an
+intermediate fact.
 
 The producer accepts at most 64 vertices and 2,016 edges through a
 matching-specific graph contract. Other graph invariants retain their own

docs/reference/capabilities/graphs/graph-metric-verification.md

@@ -6,12 +6,12 @@
 `graph.invariant.radius.compute` version `2` retain their existing producer
 contracts and `COMPUTED` assurance. Operator-authorized
 `graph.invariant.diameter.verify` and `graph.invariant.radius.verify`
-capabilities can promote one exact stored result to `VERIFIED` after
+capabilities can promote one exact submitted `{input, candidate}` claim to `VERIFIED` after
 independent all-sources breadth-first replay.
 
 ## Exact claims and conventions
 
-Each verifier checks one stored producer result against the exact stored finite
+Each verifier checks one complete typed candidate against the exact submitted finite
 simple undirected graph:
 
 - for a nonempty connected graph, diameter is the maximum vertex eccentricity
@@ -21,8 +21,8 @@ simple undirected graph:
   and returns `status = NOT_APPLICABLE`, `connected = false`, and
   `exactness = NOT_APPLICABLE`.
 
-The claim is bound to the input artifact, result artifact, graph semantics,
-result schema, checker identity, checker source digest, and provider runtime.
+The claim is bound to canonical input and candidate digests, graph semantics,
+checker identity, checker source digest, and provider runtime.
 The verifier does not certify a directly supplied graph, an unbounded graph
 family, or a theorem that later uses the metric.
 

src/jacobian/adapters/mcp/guidance.py

@@ -3,43 +3,41 @@
 from __future__ import annotations
 
 SERVER_DESCRIPTION = (
-    "Use atomic exact and symbolic mathematics, with separate checker operations "
-    "when independent verification is needed."
+    "Search and run installed Jacobian exact-math operations, with separate checker "
+    "operations for independent verification."
 )
 
 SERVER_INSTRUCTIONS = (
-    "Use Jacobian whenever a task may benefit from a specialized exact mathematical "
-    "operation, including matrix or polynomial computation. This applies even when the "
-    "user does not name Jacobian and shell code could also calculate the result. Unless "
+    "Search and run the locally installed Jacobian toolbox whenever a task may benefit "
+    "from exact computation, symbolic transformation, finite search, formal inspection, "
+    "or independent checking, even when the user does not name Jacobian or shell code "
+    "could also calculate the result. math.find is the authoritative local inventory; "
+    "internet search cannot show which operations are available in this runtime. Unless "
     "an exact installed capability ID and its typed contract are already available, call "
-    "math.find with a plain-language desired local mathematical outcome; no capability "
-    "ID is required. math.run may execute a known contract directly. "
+    "math.find with a plain-language desired local mathematical outcome. math.run may "
+    "execute a known contract directly. "
     "For declaration queries explicitly targeting Jacobian's pinned CORE or MATHLIB "
     "environment, use the pinned mathematical operation; do not substitute repository "
     "search, cached Mathlib files, or a local Lean process because they may not match "
-    "that server environment. Project-local Lean "
-    "declarations are outside the server catalog and may require project-local tools. "
-    "Other uses include symbolic transformation, structural analysis, examples or "
-    "counterexamples, bounded search, Lean/Mathlib declaration search or formal-"
-    "environment inspection, and requested independent verification. "
-    "Do not report that no specialized mathematical operation is available without "
-    "checking math.find. When independent checking is requested, multiple calculations "
-    "or programs authored by the same model are not independent checker evidence. "
-    "Search again whenever the objective or available evidence changes. "
+    "that server environment. Project-local Lean declarations are outside the server "
+    "catalog and may require project-local tools. Repeating the same lookup against an "
+    "unchanged catalog returns the same operation facts; math.find is operation lookup, "
+    "not confirmation. Merely restating an accepted value without new evidence is not a "
+    "mathematical-tool use case. "
     "The model owns representation, decomposition, composition, iteration, verification "
-    "timing, and stopping. Results keep execution status, mathematical conclusion, "
-    "and verification record separate. No descriptor match, timeout, "
-    "bounded or exhausted search, or failure to find a witness is a mathematical "
-    "conclusion. Only a result with a local verification record URI is "
-    "verified. A verification record for an input, premise, factorization, or related "
-    "artifact does not verify a model-derived conclusion; the record must be bound to "
-    "the exact final claim."
+    "timing, and stopping. An operation match, timeout, incomplete search, or failure to "
+    "find a witness is not a mathematical conclusion. Independent checking uses a "
+    "separate checker operation; model-authored duplicate calculations are not independent "
+    "evidence. Only a result with a local verification record URI is verified. A record "
+    "for an input, premise, factorization, or related artifact does not verify a model-"
+    "derived conclusion; the record must be bound to the exact final claim."
 )
 
 MATH_FIND_DESCRIPTION = """\
-Search or inspect installed math tools by desired outcome or exact ID. Use when a
-task may benefit from exact computation, search, structural analysis, or a separate
-checker tool—even if shell code could also calculate the answer.
+Search or inspect locally installed Jacobian math tools by desired outcome or exact ID.
+This is the authoritative runtime inventory; internet search is not. Use when a task
+may benefit from exact computation, search, structural analysis, or a separate checker
+tool—even if shell code could also calculate the answer.
 
 Forms:
 - `request.op="search"`: plain-language mathematical outcome (compact cards).
@@ -58,15 +56,17 @@
 """
 
 MATH_RUN_DESCRIPTION = """\
-Run one installed math tool by ID with its typed `payload`. Read the mathematical
-value in `output` first, then execution status. If the payload shape is unknown,
-inspect the exact operation with math.find, then copy and adapt one of its
-`invocation_examples`. Do not call math.run with an empty `payload` merely to
-discover required fields; the inspect result is the authoritative contract.
+Run one installed math tool by ID with its typed `payload`. Check execution status
+before treating `output` as mathematical evidence. For a completed run, interpret the
+operation-owned result fields and any `verification_record_uri` to determine exactly
+what the run established. If the payload shape is unknown, inspect the exact operation
+with math.find and copy its `invocation_examples`. Do not call math.run with an empty
+`payload` merely to discover required fields; the inspect result is the authoritative
+contract.
 
 Ordinary tools return calculations. Independent checking uses a separate checker
 tool ID (for example `polynomial.identity.verify`), not a switch on the producer.
-Failed or incomplete runs are not mathematical conclusions.
+Failed, cancelled, timed-out, or incomplete runs are not mathematical conclusions.
 
 Examples:
 - `{"capability_id":"integer.compute.gcd","payload":{"left":"84","right":"30"}}`

src/jacobian/domains/certified_snf/checkers.py

@@ -19,7 +19,7 @@
         verification_title="Verify a transformation-certified Smith normal form",
         verification_description=(
             "Independently verify the full Smith diagonal and both unimodular "
-            "basis transformations against the exact stored integer matrix."
+            "basis transformations against the exact submitted integer matrix input."
         ),
         verification_tags=(
             "verification",

src/jacobian/domains/graph_optimization/checkers.py

@@ -29,7 +29,7 @@
         verification_title="Verify a Hamiltonian-path decision",
         verification_description=(
             "Independently verify a spanning path witness or exhaust the bounded "
-            "finite path state space for one stored negative decision."
+            "finite path state space for one submitted negative decision."
         ),
         verification_tags=(
             "verification",
@@ -52,8 +52,8 @@
         verification_capability_id="graph.induced_tree.maximum.verify",
         verification_title="Verify a maximum induced tree result",
         verification_description=(
-            "Independently exhaust bounded vertex subsets to verify one stored "
-            "exact maximum induced-tree result and its graph binding."
+            "Independently exhaust bounded vertex subsets to verify one submitted "
+            "exact maximum induced-tree result against its exact graph input."
         ),
         verification_tags=("verification", "exact", "graph", "induced-tree"),
     ),
@@ -73,7 +73,7 @@
         verification_description=(
             "Independently verify source connectivity, spanning-tree feasibility, "
             "exact total weight, and every fundamental-cycle non-improvement check "
-            "for one stored exact rational weighted-graph result."
+            "for one submitted exact rational weighted-graph result."
         ),
         verification_tags=(
             "verification",
@@ -98,7 +98,7 @@
         verification_capability_id="graph.invariant.diameter.verify",
         verification_title="Verify an exact graph diameter",
         verification_description=(
-            "Independently replay all-source shortest paths to verify one stored "
+            "Independently replay all-source shortest paths to verify one submitted "
             "diameter result, including its disconnected-graph convention."
         ),
         verification_tags=(
@@ -123,7 +123,7 @@
         verification_capability_id="graph.invariant.radius.verify",
         verification_title="Verify an exact graph radius",
         verification_description=(
-            "Independently replay all-source shortest paths to verify one stored "
+            "Independently replay all-source shortest paths to verify one submitted "
             "radius result, including its disconnected-graph convention."
         ),
         verification_tags=(
@@ -149,7 +149,7 @@
         verification_title="Verify an exact graph distance matrix",
         verification_description=(
             "Independently replay every source shortest-path traversal to verify "
-            "one stored all-pairs distance matrix, including unreachable pairs."
+            "one submitted all-pairs distance matrix, including unreachable pairs."
         ),
         verification_tags=(
             "verification",
@@ -175,7 +175,7 @@
         verification_title="Verify a maximum matching result",
         verification_description=(
             "Independently verify matching feasibility and a Tutte-Berge upper-bound "
-            "certificate for one exact stored finite graph."
+            "certificate submitted with its exact finite graph input."
         ),
         verification_tags=(
             "verification",

src/jacobian/domains/number_theory/checkers.py

@@ -25,7 +25,7 @@
         verification_title="Verify an integer prime factorization",
         verification_description=(
             "Independently verify the complete canonical prime-power "
-            "factorization of one stored nonzero integer result."
+            "factorization submitted with its exact nonzero integer input."
         ),
         verification_tags=(
             "verification",
@@ -49,8 +49,9 @@
         verification_capability_id="integer.powerful.verify",
         verification_title="Verify a powerful-number decision",
         verification_description=(
-            "Independently verify one stored powerful-number decision, its "
-            "complete canonical factor witness, and every violating prime."
+            "Independently verify one submitted powerful-number decision against "
+            "its exact integer input, complete canonical factor witness, and every "
+            "violating prime."
         ),
         verification_tags=(
             "verification",

src/jacobian/domains/probability/bundle.py

@@ -1,14 +1,32 @@
 """Finite-probability domain bundle."""
 
+from dataclasses import replace
+from typing import Any
+
 from jacobian.contracts.capabilities import CapabilityDiagnostic
 from jacobian.domain_bundles import DomainBundle
 from jacobian.domains.probability.checkers import PROBABILITY_EXACT_REPLAY_CHECKERS
+from jacobian.domains.probability.gaussian_inputs import (
+    CanonicalGaussianPolynomialMomentRequest,
+)
 from jacobian.domains.probability.operations import FINITE_PROBABILITY_CAPABILITIES
 from jacobian.operations import DomainDiagnostics, DomainSemantics
 from jacobian.provider_runtime import PYTHON_FLINT_VERSION
 from jacobian.providers.flint_runtime import python_flint_probability_provider_runtime
 
 
+def _operation_with_canonical_gaussian_input(operation: Any) -> Any:
+    if operation.spec.operation_id != "probability.gaussian_polynomial.moment.compute":
+        return operation
+    return replace(
+        operation,
+        spec=replace(
+            operation.spec,
+            request_type=CanonicalGaussianPolynomialMomentRequest,
+        ),
+    )
+
+
 def build_finite_probability_bundle() -> DomainBundle:
     """Build this domain-owned installation unit explicitly."""
     return DomainBundle(
@@ -31,7 +49,10 @@ def build_finite_probability_bundle() -> DomainBundle:
         ),
         provider_runtime=python_flint_probability_provider_runtime(),
         backend_version=f"python-flint-{PYTHON_FLINT_VERSION}",
-        capabilities=FINITE_PROBABILITY_CAPABILITIES,
+        capabilities=tuple(
+            _operation_with_canonical_gaussian_input(operation)
+            for operation in FINITE_PROBABILITY_CAPABILITIES
+        ),
         diagnostics=DomainDiagnostics(
             invalid_request=CapabilityDiagnostic(
                 code="INVALID_FINITE_PROBABILITY_REQUEST",

src/jacobian/polynomials/installation.py

@@ -9,6 +9,7 @@
 from jacobian.contracts.checkers import EvidenceKind
 from jacobian.contracts.evidence import CertificateEnvelope, WitnessEnvelope
 from jacobian.contracts.polynomials import (
+    MAX_POLYNOMIAL_VARIABLES,
     PolynomialIdentityClaim,
     PolynomialInjectivityClaim,
     PolynomialJacobian,
@@ -71,7 +72,7 @@ def install_polynomial_capabilities(
             ),
             "domain": "QQ",
             "map_shape": "square",
-            "maximum_dimension": 4,
+            "maximum_dimension": MAX_POLYNOMIAL_VARIABLES,
             "maximum_terms_per_coordinate": 1024,
             "maximum_exponent": 32,
             "maximum_derived_exponent": 127,