[Rule] MaximumContactMapOverlap to MaximumClique

Literature gate: UNVERIFIED. The primary Strickland/Barnes/Sokol (2005)
abstract confirms the CMO-to-clique relationship, but its full construction
was not obtained in this session. The self-contained proof and independent
mathematical audits below are complete; comparison to the full primary text
is still pending. This draft must not be described as having passed the
/propose rule reference-reading gate.

Source

MaximumContactMapOverlap, without variant parameters.

There are two finite ordered vertex sets V_i={0,...,n_i-1} and simple
undirected contact sets E_i, of sizes m_i. Contacts are represented in
canonical increasing endpoint order. Loops, out-of-range endpoints and
duplicate contacts are rejected by the model.

A feasible alignment is an increasing partial injection f:V_1 -> V_2:
when both u<v are matched, f(u)<f(v). Its score is the number of source
contacts whose endpoint images form a target contact. The solution vector
has length n_1; zero means unmatched and j+1 means image j. Nonzero
entries must be strictly increasing. Values are Max<i64>, and all-unmatched
is always feasible, even when n_1>n_2.

Target

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

The target is an undirected simple compatibility graph with unit vertex
weights. It maximizes clique cardinality, with value Max<i64>. Completed
optimum values are equal; a nonmaximum clique may decode to an alignment
whose score exceeds its cardinality.

Motivation

This adds an exact direct route from ordered contact-map alignment to clique
solvers. The baseline graph of 257 exact variant nodes and 344 edges has no
witness path from this source to unit MaximumClique. The existing related
route is CMO -> ILP #1044,
implemented in src/rules/maximumcontactmapoverlap_ilp.rs; the source model is
#1043.

The 4,700-record public-history search found no dedicated proposal or explicit
suggestion of this exact pair. Cooccurrences of both names in PR #1067 and
review #1119 were lists of different contributions, not an edge between them.
This is a conclusion about the captured project history, not global novelty.

The construction preserves all endpoint order comparisons, which is essential:
plain graph isomorphism can overestimate the overlap. It supplies a solving
route and does not by itself complete an incoming NP-hardness chain for CMO.
It shares the association method with the separately prepared MCES rule;
whether these deserve two nontrivial-reduction credits is a maintainer decision.

Reference

D. M. Strickland, E. Barnes and J. S. Sokol, Optimal Protein Structure
Alignment Using Maximum Cliques, Operations Research 53(3), 389–402 (2005),
primary publisher page and abstract,
DOI 10.1287/opre.1040.0189.

Only the primary abstract was available. It establishes that this problem has
been formulated through maximum clique; no claim about its exact gadget,
theorem assumptions or proof is made without the full text. The construction
and proof below were derived independently for the repository's definitions.
The missing full-text comparison is a visible publication-readiness limitation,
not something that passing finite tests resolve.

A bounded literature follow-up found corroboration
in Rahrig, Leontis and Zirbel's primary 2010 R3D Align article: its own
alignment graph preserves order and unique assignments, and attributes the
two-amino-acid protein CMO construction to Strickland et al. This agreement
is an inference from a subsequent primary article, not inspection of the
2005 construction or its assumptions. The full-text gate remains UNVERIFIED.

Reduction Algorithm

Let N=m_1*m_2. Each contact in E_1 is (u,v) with u<v, and each contact
in E_2 is (a,b) with a<b.

1. For every ordered pair of stored contacts, create one target vertex
   p=((u,v),(a,b)) representing assignments A_p={(u,a),(v,b)}. List
   candidates first by source contact index, then by target contact index.

2. Join distinct candidates p,q exactly when every (s,t) in A_p and
   (s',t') in A_q has the same comparison on both sides:

   s < s' iff t < t';  s = s' iff t = t';  s > s' iff t > t'.
   

   Assign each target vertex weight one. A candidate is locally an increasing
   injection because its two contacts are canonically ordered.

3. Validate a target clique witness. Initialize a length-n_1 source vector
   to zero. For every selected (s,t) assignment, write t+1 at source
   position s; leave all other positions unmatched.

Forward. A source increasing partial alignment pairs each preserved
source contact with its unique target contact. These candidates restrict the
same increasing injection, so every pair preserves all endpoint comparisons.
They form a clique with cardinality equal to the source score. Hence maximum
clique size is at least the CMO optimum.

Backward. In a clique, equality preservation makes the union of all
endpoint assignments a function. Preservation of strict inequalities makes
it injective and increasing. Distinct selected candidates cannot use one
source contact: its two endpoint images would agree, forcing the same unique
target contact and thus the same candidate. Each clique vertex therefore
certifies a distinct preserved source contact. The extracted alignment has
score at least the clique size. This gives the reverse optimum inequality,
so the optima are equal and every maximum clique decodes optimally. Repeated
target contacts are also impossible by injectivity, bounding every clique by
min(m_1,m_2).

Witness-value caveat. Pairwise-compatible selections can imply additional
preserved contacts not explicitly selected. For instance, the correspondences
(0,1)->(0,1) and (1,2)->(1,2) force the third contact (0,2)->(0,2) when
both maps contain it. Thus arbitrary witness scores need not be identical;
the implemented identity value map is for completed optima.

Complexity and corners. Construction takes O(N+N^2) time and output
space. Extraction takes O(n_1+N) beyond target validation. Comparisons and
index handling are polynomial in their encoded lengths; the Rust construction
grows the actual candidate vector without speculative product allocation.
Writing t+1 is valid because a target vertex index satisfies t<n_2.
Empty contact sets produce an empty graph and the all-unmatched alignment.
More source than target vertices requires no special case because alignment
is partial. Contacts sharing source endpoints must agree on images; disjoint
contacts cannot reuse target endpoints; crossing assignments are excluded.
No assumption about connectedness, contact density or absence of isolated
positions is used.

Size Overhead

The registered source parameters are num_contacts_1=m_1 and
num_contacts_2=m_2; both target parameter names are registered. If either
contact set is empty, both counts are zero.

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 establishes the general result. Independent finite audits exercise
its implementation without substituting for the proof or for reference reading.

• Constructor: 3,286,719 checks / 14,705 instances, seed 2026101307,
  including all graph pairs through five vertices restricted to at most two
  contacts on each side, all contact sets through three vertices, sampled
  larger contact sets, and every alignment/clique in each tested instance.
• Independent adversary, written from the proof: 1,202,845 checks / 9,676
  instances, seed 2026101315, including separate Hypothesis strategies;
  zero failures.
• Cross-comparison: 720 identical targets, 1,604 cross-extractions, 18,460
  source-value comparisons and 720 optimum equivalences, zero disagreements.
• Rust: 7 focused rule tests passed, including all pairs of contact graphs
  through three vertices and every target clique, the canonical example,
  empty graphs, partial alignments, malformed/crossing witnesses, parameter
  predictions and the nonmaximum-witness score caveat. Formatting passed.

Counts are assertions and instance executions, not independent samples.
Full unrestricted graph-pair enumeration through five vertices is not claimed.
Evidence paths under research/coauthorship-2026-10-13/ are
proofs/graph_contactmap_clique.typ,
verification/graph_contactmap_clique_constructor.py,
adversary/adv_contactmap_clique_report.json, and
verification/cross_association_graphs_report.json, with historical evidence
in history-association-supplement.md. These are local, not public certificate
URLs. The mathematical gate is VERIFIED; the primary-full-text gate remains
UNVERIFIED as stated at the top.

Example

Source. Both ordered vertex sets have positions 0,1,2,3. Contact lists are

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

As unordered graphs both are paths on four vertices, so omitting the order
restriction would incorrectly allow all three contacts to match.

Construction. The nine candidate assignments are:

Target. The complete compatibility-edge list is [(0,8),(4,8)], so
there are nine vertices and two edges. Clique {0,8} has value two and
extracts [1,0,2,4], meaning 0->0, position 1 unmatched, 2->1, 3->3.
It preserves source contacts (0,2) and (0,3).

No alignment can preserve all three contacts. Doing so would match every
source position; an increasing injection between two four-position sets is
then the identity, but identity preserves only (0,3). Thus the optimum is
two and threshold three is NO, despite the unordered isomorphism.

Two suboptimal feasible solutions are clique {0}, extracting [1,0,2,0],
and clique {4}, extracting [0,3,0,4]; each preserves exactly one contact.
The empty clique gives score zero. Candidates 0 and 4 cannot coexist because
their assigned images reverse the source order of positions 1 and 2.

BibTeX

@article{StricklandBarnesSokol2005ProteinCliques,
  author = {Strickland, D. M. and Barnes, E. and Sokol, J. S.},
  title = {Optimal Protein Structure Alignment Using Maximum Cliques},
  journal = {Operations Research},
  volume = {53},
  number = {3},
  pages = {389--402},
  year = {2005},
  doi = {10.1287/opre.1040.0189},
  url = {https://pubsonline.informs.org/doi/10.1287/opre.1040.0189}
}
@article{RahrigLeontisZirbel2010R3DAlign,
  author = {Rahrig and Leontis and Zirbel},
  title = {{R3D Align}: global pairwise alignment of {RNA} 3D structures using local superpositions},
  journal = {Bioinformatics},
  volume = {26},
  number = {21},
  pages = {2689--2697},
  year = {2010},
  url = {https://academic.oup.com/bioinformatics/article/26/21/2689/213314}
}

Attribution and submission status

Responsible human contributor: Thiago Costa
(@ThiagoCAltoe). Discovery, proofs, drafting,
implementation and adversarial checking were assisted by Codex AI agents.
Human scientific review and full-primary-text comparison are pending.
Maintainers decide acceptance, nontriviality and any separate credit from MCES;
none is claimed here.