[Feature]: Support independently verified maximum matching beyond 32 vertices

[yuelgrace1810-ops]

Area

Exact finite-graph invariants; maximum-matching producer/checker contracts and graph-size bounds.

Held-out reliability evidence

A weak-model held-out evaluation used Brenner, Kleist, Mütze, Rieck, and Verciani's official v6_nonham_adj.txt artifact from their resolution of Winkler's Venn-diagram conjecture (arXiv:2503.18554).

The frozen first published graph decodes to:

• 64 vertices;
• 124 undirected edges;
• maximum matching cardinality 31;
• an explicit Hall-deficient set of size 14 with neighborhood size 13.

The no-Jacobian control reconstructed the complete 124-edge graph, a valid 31-edge matching, and the Hall witness correctly.

The selectively routed Jacobian arm:

1. immediately discovered graph.invariant.maximum_matching.compute;
2. navigated reciprocally to graph.invariant.maximum_matching.verify;
3. inspected both exact contracts;
4. found that both contracts accept at most 32 vertices;
5. attempted the producer twice on a manually decoded 64-vertex payload;
6. fell back locally after execution cancellation.

Its final answer stated 123 edges instead of 124. The final matching and Hall conclusion were correct, but the claimed exact intermediate graph was not. It correctly withheld VERIFIED.

This is a source-bound example where the installed producer/checker pair is mathematically appropriate but cannot accept the proof artifact.

Deterministic reproduction on current main

Current main uses GraphInvariantRequest.graph: ChromaticGraph, where:

class ChromaticGraph(ContractModel):
    vertices: tuple[GraphVertex, ...] = Field(max_length=32)
    edges: tuple[tuple[GraphVertex, GraphVertex], ...] = Field(max_length=496)

and maximum-matching certificates additionally cap:

• maximum_matching_cardinality <= 16;
• upper_bound <= 16;
• odd_component_count <= 32;
• barrier size at 32 through the shared types.

Validating a 64-vertex request deterministically fails before producer dispatch:

graph.vertices
  Tuple should have at most 32 items after validation, not 64

The underlying producer is NetworkX maximum matching and the independent checker is a standard-library Tutte-Berge barrier replay, so this is a public contract/certificate-boundary issue, not absence of matching algorithms.

Why this needs design review

Blindly changing 32 to 64 is unsafe:

• ChromaticGraph is shared by coloring and several graph-invariant operations with different complexity profiles;
• maximum-matching result and Tutte-Berge certificate bounds must move coherently;
• input-size, edge-count, runtime, output-size, and checker-resource limits need explicit review;
• raising a shared schema could unintentionally broaden expensive unrelated operations.

The smallest plausible direction is a separately bounded polynomial-time matching request/result contract, or another capability-specific graph bound, while preserving the existing shared bound for operations whose costs justify it. That choice is architectural and should not be inferred from one evaluation.

Independent reuse evidence

This is not the first held-out case containing an exact graph above the shared 32-vertex surface:

• a prior 123-vertex conjecture-derived graph evaluation explicitly required structural reductions because exact graph tools could not accept the full artifact;
• this 64-vertex official Venn artifact now shows the same boundary for an already installed producer plus independent checker.

These are different source lineages and graph workflows. More evaluation is still needed before a Tool PR.

Requested acceptance boundary

A future design should preserve:

1. an explicit, documented vertex/edge/resource bound;
2. exact graph identity and full edge-list binding;
3. canonical vertex-disjoint matching witnesses;
4. coherent Tutte-Berge certificate ranges;
5. producer COMPUTED versus independently replayed VERIFIED;
6. fail-closed behavior on oversized inputs, timeouts, malformed witnesses, and wrong-graph candidates;
7. no accidental bound increase for unrelated exponential graph operations.

Regression coverage should include orders 32, 33, and the accepted maximum; a 64-vertex near-perfect bipartite graph; malformed duplicate-edge and duplicate-matched-vertex witnesses; wrong-input rebinding; and an oversized fail-closed case.

Overlap check

• Issue [Evaluation]: Jacobian is available but unused across a four-case conjecture canary #845 owns discovery/execution and context behavior, including cancelled math.run calls.
• Closed issue [Feature]: Add budgeted graph optimization outcomes with optimality witnesses #84 concerns general budgeted graph optimization outcomes and predates the installed exact maximum-matching pair.
• Issue Add canonical graph6 decoding and bound graph-invariant certificates #947 concerns graph6 decoding plus independent-set/zero-forcing capabilities.
• PR Derive verifier navigation from installed checker metadata #899 fixed producer/checker navigation and is working correctly here.

Searches of open/closed issues and PRs found no owner for the 32-vertex maximum-matching producer/checker boundary. This issue requests design review; it does not propose a benchmark-specific helper or an unreviewed limit increase.