TEMP: sync main into determinant order-64 port

.github/workflows/ci.yml

@@ -49,17 +49,33 @@ jobs:
           path: dist/
 
   python:
-    name: python
+    name: python (${{ matrix.lane }})
     runs-on: ubuntu-latest
-    timeout-minutes: 40
+    timeout-minutes: ${{ matrix.timeout-minutes }}
+    strategy:
+      fail-fast: false
+      matrix:
+        include:
+          - lane: unit
+            timeout-minutes: 10
+          - lane: component
+            timeout-minutes: 15
+          - lane: domain
+            timeout-minutes: 15
+          - lane: composition
+            timeout-minutes: 25
+          - lane: e2e
+            timeout-minutes: 15
+          - lane: provider
+            timeout-minutes: 25
     steps:
       - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
         with:
           persist-credentials: false
       - uses: ./.github/actions/setup-python-tests
         with:
           python-version: "3.12"
-      - run: make test-ordinary
+      - run: make test-${{ matrix.lane }}
         env:
           PYTEST_ARGS: >-
             --junitxml=pytest.xml
@@ -69,17 +85,17 @@ jobs:
       - uses: actions/upload-artifact@043fb46d1a93c77aae656e7c1c64a875d1fc6a0a # v7.0.1
         if: ${{ !cancelled() }}
         with:
-          name: junit-python-3.12
+          name: junit-python-${{ matrix.lane }}-3.12
           path: pytest.xml
           if-no-files-found: ignore
           retention-days: 7
       - if: ${{ !cancelled() }}
-        run: mv .coverage .coverage.python
+        run: mv .coverage .coverage.python-${{ matrix.lane }}
       - uses: actions/upload-artifact@043fb46d1a93c77aae656e7c1c64a875d1fc6a0a # v7.0.1
         if: ${{ !cancelled() }}
         with:
-          name: coverage-data-python
-          path: .coverage.python
+          name: coverage-data-python-${{ matrix.lane }}
+          path: .coverage.python-${{ matrix.lane }}
           include-hidden-files: true
 
   boundaries:

CONTRIBUTING.md

@@ -25,7 +25,8 @@ make check
 
 Then open a pull request. `make setup` installs the locked development
 environment with the complete maintained Python backend stack. `make check`
-runs Ruff, mypy, and the same Lean-free ordinary pytest invocation CI uses.
+runs Ruff, mypy, and the same Lean-free ordinary test suite CI covers in fixed
+semantic groups.
 Open the PR once it is green, and add any explicitly relevant specialist
 validation called out below.
 

Makefile

@@ -9,8 +9,9 @@ ORDERING_DEFAULT_SEED := --randomly-seed=17
 PYTEST_DIAGNOSTIC_ARGS ?= --durations=10
 RUFF_PATHS := src tests benchmarks
 PYTEST_RUNNER := $(UV_RUN) python tools/pytest_lifecycle.py
-# Ordinary pytest used by `make check` and the CI python job.
-ORDINARY_PYTEST_FLAGS := -n 4 --dist worksteal --timeout=180
+# Fixed semantic lanes covering the Lean-free ordinary testpaths. CI runs these
+# independently; `make check` runs the same lanes locally in this order.
+ORDINARY_TEST_LANES := unit component domain composition e2e provider
 PUBLIC_COMMANDS := setup quick check check-external fix
 
 include make/development.mk
@@ -81,9 +82,10 @@ test-e2e: ## Complete caller-visible journeys (serial, 180s).
 		$(if $(TESTS),$(TESTS),tests/e2e) \
 		$(PYTEST_DIAGNOSTIC_ARGS) $(PYTEST_ARGS)
 
-test-ordinary: ## Lean-free ordinary pytest (same flags as CI python).
-	$(UV_RUN) pytest $(ORDINARY_PYTEST_FLAGS) \
-		$(PYTEST_DIAGNOSTIC_ARGS) $(PYTEST_ARGS)
+test-ordinary: ## Lean-free ordinary suite in the fixed CI group order.
+	@for lane in $(ORDINARY_TEST_LANES); do \
+		$(MAKE) test-$$lane || exit $$?; \
+	done
 
 test-compatibility: ## Supported-version import/API compatibility smoke.
 	$(UV_RUN) pytest -n 0 --timeout=30 --timeout-method=thread \

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.
 

docs/reference/testing-strategy.md

@@ -31,6 +31,11 @@ Make targets that own storage, process, MCP, and Lean isolation. `make
 check-external` covers Lean and maintained-provider probes when those trees
 change.
 
+Hosted CI runs that same ordinary suite as six fixed semantic lanes: `unit`,
+`component`, `domain`, `composition`, `e2e`, and `provider`. These are static
+Make targets, not path-selected or timing-planned shards; `make check` runs all
+six in the same order.
+
 ## Test ownership
 
 The filesystem is the metadata. A test under `tests/domain/` is a domain test;

pyproject.toml

@@ -23,6 +23,7 @@ dependencies = [
     "mcp-types==2.0.0",
     "networkx==3.6.1",
     "pydantic>=2.12,<3",
+    "pydantic-core>=2.41,<3",
     "python-flint==0.9.0",
     "rfc8785==0.1.4",
     "sympy==1.14.0",

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/composition.py

@@ -5,7 +5,7 @@
 from pathlib import Path
 
 from jacobian.installation.context import create_installation_context
-from jacobian.portfolio import install_portfolio
+from jacobian.portfolio.assembler import install_portfolio
 from jacobian.runtime.bootstrap import bootstrap_services
 from jacobian.runtime.config import RuntimeOptions
 from jacobian.runtime.model import JacobianRuntime

src/jacobian/contracts/graph_coloring.py

@@ -6,9 +6,7 @@
 
 from pydantic import Field, StrictInt, StringConstraints, model_validator
 
-from jacobian.contracts.common import ArtifactUri, Sha256Digest
 from jacobian.contracts.results import ContractModel
-from jacobian.contracts.sat import CanonicalCnf
 
 GraphVertex = Annotated[
     str,
@@ -41,71 +39,6 @@ def require_simple_graph(self) -> Self:
         return self
 
 
-class GraphColoringEncodingRequest(ContractModel):
-    """Materialize the exact CNF semantics of k-colorability."""
-
-    graph: ChromaticGraph
-    colors: StrictInt = Field(ge=1, le=32)
-
-
-class GraphColoringEncodingClaim(ContractModel):
-    """Claim that one graph/color-count pair has a canonical encoding."""
-
-    claim_schema_version: Literal["1"] = "1"
-    predicate: Literal["GRAPH_K_COLORABILITY_ENCODING"] = (
-        "GRAPH_K_COLORABILITY_ENCODING"
-    )
-    graph: ChromaticGraph
-    colors: StrictInt = Field(ge=1, le=32)
-
-
-class GraphColoringEncodingScope(ContractModel):
-    """Graph-owned scope binding the encoding to the SAT CNF artifact."""
-
-    scope_schema_version: Literal["1"] = "1"
-    graph: ChromaticGraph
-    colors: StrictInt = Field(ge=1, le=32)
-    cnf_uri: ArtifactUri
-    cnf_object_digest: Sha256Digest
-    cnf: CanonicalCnf
-
-
-class GraphColoringEncodingCandidate(ContractModel):
-    """Pointer candidate checked against the graph-owned encoding scope."""
-
-    candidate_schema_version: Literal["1"] = "1"
-    cnf_uri: ArtifactUri
-    scope_uri: ArtifactUri
-
-
-class GraphColoringEncodingReplay(ContractModel):
-    """Certificate payload for independent graph-to-CNF replay."""
-
-    method: Literal["INDEPENDENT_GRAPH_COLORING_CNF_REPLAY"] = (
-        "INDEPENDENT_GRAPH_COLORING_CNF_REPLAY"
-    )
-    claim_uri: ArtifactUri
-    candidate_uri: ArtifactUri
-    scope_uri: ArtifactUri
-
-
-class GraphColoringEncodingOutput(ContractModel):
-    """Materialized encoding and its replay certificate."""
-
-    graph: ChromaticGraph
-    colors: StrictInt = Field(ge=1, le=32)
-    cnf_uri: ArtifactUri
-    scope_uri: ArtifactUri
-    claim_uri: ArtifactUri
-    candidate_uri: ArtifactUri
-    certificate_uri: ArtifactUri
-    variable_count: StrictInt = Field(ge=0, le=1_000_000)
-    clause_count: StrictInt = Field(ge=0, le=1_000_000)
-    encoding_version: Literal["exactly-one-and-edge-separation/v1"] = (
-        "exactly-one-and-edge-separation/v1"
-    )
-
-
 class ChromaticNumberBudget(ContractModel):
     """Total wall-clock budget for the bounded coloring search."""