[Rule] MaximumCommonEdgeSubgraph to MaximumClique

Prior-project proximity:
#1019, comment 4540508277
already suggests a future clique-based MCES formulation. It does not specify
this direct reduction or its association graph, but the suggestion must be
considered when assigning credit. No claim of an entirely unanticipated idea
or of global mathematical novelty is made.

Source

MaximumCommonEdgeSubgraph, without variant parameters.

There are two finite directed edge-labelled graphs G_i=(V_i,E_i), with
n_i=|V_i| and m_i=|E_i|. An arc is a triple (u,lambda,v). Arc collections
have set semantics; loops, antiparallel arcs and different labels on the same
ordered endpoint pair are allowed. A feasible source solution is a partial
injective map f:V_1 -> V_2. Its score is the number of source arcs
(u,lambda,v) whose endpoints are matched and for which
(f(u),lambda,f(v)) belongs to E_2.

The actual solution vector has length n_1, with values 0,...,n_2-1 for
matched vertices and sentinel n_2 for unmatched vertices. The objective is
maximization with value Max<i64>. An empty partial map is always feasible,
including when n_1>n_2.

Representation guard. Because the public raw graph fields can bypass the
normalizing constructor, the reduction rejects duplicate arc triples and
out-of-range arc endpoints at entry using a typed error. The proof concerns
the canonical set-domain instances stated above; rejection of malformed raw
representations does not change their mathematical construction.

Target

MaximumClique<SimpleGraph, One>, registered as
MaximumClique/graph=SimpleGraph/weight=One.

A target witness selects a pairwise adjacent set of vertices in an undirected
simple graph. All weights are one, so the score is clique cardinality and the
value is also Max<i64>. Empty cliques are feasible. Completed optimum values
map identically; arbitrary nonmaximum witness scores need not do so.

Motivation

This provides an exact direct route from directed edge-labelled MCES to the
clique-solving part of the reduction graph. The baseline audit of 257 exact
variant nodes and 344 edges found no witness path from this source to unit
MaximumClique. The existing related rule is
MCES -> ILP #1019,
implemented in src/rules/maximumcommonedgesubgraph_ilp.rs, with source model
#1018.

The new target removes explicit vertex-map variables and keeps only compatible
arc correspondences. Its usefulness is a new solving route, not a claim to
fill MCES's missing incoming NP-hardness chain. The 4,700-record historical
search found no dedicated proposal of this exact edge, but the nearby #1019
suggestion above is relevant. Catalog #183's R252 is CLIQUE -> LARGEST COMMON
SUBGRAPH, with a different direction and model.

This rule and the separately prepared ContactMapOverlap -> Clique rule share
the association-graph method. Their different source semantics do not ensure
that maintainers will award two independent nontrivial-reduction credits.

Reference

R. R. Nerem, P. Crawford-Kahrl, B. Cummins and T. Gedeon, A poset metric from
the directed maximum common edge subgraph, arXiv:1910.14638v2 (2020),
primary PDF, Section 6 and Theorem 6.3.

The paper's definitions and theorem were read. Its extended-line-digraph
construction relates a restricted directed MCES problem to clique, assuming
weakly connected simple oriented node-labelled graphs. That theorem is not
silently applied to the repository's broader edge-labelled domain. The direct
proof below independently covers its loops, labels, disconnected graphs and
partial maps. The classical association technique is not claimed as a new
literature result.

Reduction Algorithm

Index the two arc sets in their stored order. A candidate p=(e,e') pairs
e=(u,lambda,v) in E_1 with e'=(a,lambda,b) in E_2.

1. Retain exactly pairs having equal labels and equal loop status:
   (u=v) if and only if (a=b). Candidate p represents endpoint assignments
   A_p={(u,a),(v,b)}. It is a well-defined partial injection even for loops.

2. Create one target vertex per retained pair, ordered first by source arc
   index and then by target arc index.

3. Join distinct candidates p,q exactly when, for every (s,t) in A_p and
   (s',t') in A_q,

   (s = s') if and only if (t = t').
   

   Equality implies agreement of repeated source assignments, and the converse
   excludes two source vertices sharing an image. Each candidate has weight one.

4. Validate a target clique witness. Initialize all n_1 source entries to
   unmatched sentinel n_2; then write the endpoint assignments of each
   selected candidate. Pairwise compatibility guarantees agreement.

Forward. For any feasible partial injection f, every preserved source
arc has one unique target arc with the required labelled image triple. The
corresponding candidates restrict the same injection and are pairwise adjacent.
They form a clique whose cardinality equals the source score. Therefore the
maximum clique size is at least the MCES optimum.

Backward. The union of assignments from a clique is a partial injection:
each candidate is locally valid and every pair agrees on equal source
vertices and preserves inequality. Distinct clique vertices cannot use the
same source arc, since agreement fixes both target endpoints and set semantics
then fix its label-matching target arc. Thus a clique of size c certifies at
least c distinct preserved source arcs. Its extracted map has score at least
c, proving that the MCES optimum is at least the maximum clique size. Both
optima are equal, and every maximum clique extracts an optimal source map.
Injectivity similarly excludes repeated target arcs, so every clique has size
at most min(m_1,m_2).

Objective caveat. A nonmaximum clique may induce additional preserved arcs
which were not explicitly selected. For example, three consecutive correctly
matched arcs of a labelled directed four-cycle determine all four vertex
images and can preserve its fourth arc. Accordingly the witness theorem is
score domination for arbitrary cliques, and equality for optimal witnesses;
the aggregate identity is only a map of completed optimum values.

Complexity and corner cases. Write B=m_1*m_2. Candidate generation takes
O(B) endpoint/label comparisons; construction takes O(B+B^2) time and at
most O(B+B^2) output space. Endpoint and label comparisons are polynomial in
their encoded lengths. Extraction takes O(n_1+N) beyond target validation,
where N is the number of candidates. The code grows the actual candidate
list without a product-sized speculative allocation. Empty arc sets or
incompatible labels give an empty target graph and all-unmatched extraction.
A loop/nonloop pair is discarded, preventing an inconsistent or noninjective
single candidate. Partiality handles n_1>n_2 directly. Reversed arcs are not
identified, and different labels remain distinct scored arcs.

Size Overhead

The source size parameters are num_arcs_1=m_1 and num_arcs_2=m_2; both
target names are registered parameters. For zero candidate-product the edge
bound evaluates to zero, rather than allocating a negative-sized object.

Validation Method

Local engineering checkpoint. Production code 650a8023 passed fmt,
complete clippy, 6,980 ordinary tests and 149 doctests in a separate retry.
The original Cargo command was interrupted by RAM exhaustion in doctest
compilation, not recorded as exit zero. Test-only HEAD a4b8cba0 changes no
production code and passed fresh fmt (4.566 s), clippy (45.973 s), and all
eight focused rule-05 tests. CLI round trips/default solve, four exporters,
full manual and topology passed. 89 new rule tests were measured below
five seconds: 88 earlier tests (maximum 4.7597 s including startup) plus
the allocation regression (0.017 s). Final new-production coverage PASS:
1,223/1,233 instrumented added lines, 99.189%; every rule exceeds 95%.
The audit excludes 814 added lines with no DA record explicitly; ten
instrumented lines remain uncovered. The focused instrumented extension
passed 8/8 tests. Human scientific review and maintainer approval remain
pending.

All mathematical counts below are local evidence. Proof sources, constructor,
independent adversarial and cross-check scripts are prepared locally and can
accompany a later implementation PR; they are not public certificate URLs.

The proof above is the correctness argument; finite checks complement it.

• Constructor: 2,495,383 checks / 10,267 instances, seed 2026101306.
  This includes all unlabelled directed looped graph pairs through two
  vertices, sampled dimensions through five vertices with three labels and
  up to six arcs, every partial injection and every clique per tested instance.
• Independent adversary, written from the proof: 1,214,971 checks / 9,061
  instances, seed 2026101313, including separate Hypothesis strategies;
  zero failures.
• Cross-comparison: 720 identical targets, 1,175 cross-extractions, 67,900
  source-value comparisons and 720 optimum equivalences, zero disagreements.
• Rust: 7 focused rule tests passed, including small exhaustive looped
  graph-pair checks, every target clique, empty graphs, arbitrary labels,
  antiparallel arcs, wrong-length/nonclique rejection, parameter predictions,
  and the distinction between arbitrary and optimal witness scores. Formatting
  passed.

Counts refer to assertions and instance executions, not independent samples.
Arbitrary labels and all graph pairs through five vertices were not literally
exhausted. Local reproducible evidence is in
research/coauthorship-2026-10-13/proofs/graph_mces_clique.typ,
verification/graph_mces_clique_constructor.py,
adversary/adv_mces_clique_report.json, and
verification/cross_association_graphs_report.json. The history supplement
and its search script cover all 4,700 captured records. These evidence files
are not public certificate URLs yet.

Example

Source. Use four source vertices and the labelled directed four-cycle

E_1 = [(0,0,1), (1,1,2), (2,2,3), (3,3,0)].

Use five target-side vertices and arcs

E_2 = [(0,0,1), (1,1,3), (3,2,4), (4,3,0), (2,0,3)].

The middle coordinate is the label. The last arc provides a competing match
for the first source arc, and its endpoint choices conflict with every other
required arc correspondence.

Construction. The five retained candidates, in construction order, are:

Target. All weights are one; the complete edge list is
[(0,2),(0,3),(0,4),(2,3),(2,4),(3,4)]. Candidate 1 is isolated. The target
is a four-clique plus one isolated vertex, with five vertices and six edges.

The clique {0,2,3,4} extracts the map [0,1,3,4] and preserves all four
source arcs. Since the source has only four arcs, this is optimal on both
sides; a score threshold of five is NO.

Two suboptimal feasible solutions are explicit. Clique {0,2} extracts
[0,1,3,5] and preserves exactly two source arcs. Clique {1} extracts
[2,3,5,5] and preserves exactly one. Here sentinel 5 means unmatched. This
example tests shared-endpoint consistency, injectivity, labels and the
possibility of more source than matched vertices. The smaller three-arc
canonical fixture in the Rust tests/manual is also audited separately.

BibTeX

@misc{NeremEtAl2020DirectedMCES,
  author = {Nerem, R. R. and Crawford-Kahrl, P. and Cummins, B. and Gedeon, T.},
  title = {A poset metric from the directed maximum common edge subgraph},
  year = {2020},
  eprint = {1910.14638},
  archivePrefix = {arXiv},
  note = {Version 2, Section 6 and Theorem 6.3},
  url = {https://arxiv.org/abs/1910.14638}
}

Attribution and submission status

Responsible human contributor: Thiago Costa
(@ThiagoCAltoe). Discovery, proofs, drafting,
implementation and adversarial checks were assisted by Codex AI agents.
Human scientific review is pending. Maintainers decide whether the
existing #1019 suggestion and shared association technique affect novelty,
nontriviality or separate credit. No acceptance or coauthorship is claimed.