# All eight edge-subset candidates on a three-edge graph

[← Guide index](https://ocme.evemisslab.com/en/derivations/) · [Original MKO](https://ocme.evemisslab.com/en/mko/mko-maximum-matching/)

This is an owner-adopted natural-language teaching guide. Finite/arithmetic checks are not universal proofs; no Lean was run, and review scope is recorded per revision. Original source status labels are retained as historical data. Formulas retain exact TeX; no new semantic AST is invented.

derivation-mko-maximum-matching-01 · ocme-new142-reader-adoption-20261021



## Goal and scope

Enumerate all2³ subsets for the maximum matching and all witnesses.

Exact small-graph enumeration, not a general efficient algorithm.





## Givens and symbols


- work


- G1 — V={0,1,2,3}; E consists of e0={0,1}, e1={1,2}, e2={2,3}; bit masks use order(e0,e1,e2).


- V,E — complete vertex and edge sets
- ν(G) — maximum matching cardinality





## Rules and sources

Some rule statements have reader clarifications in this revision: they are paraphrases, not verbatim quotations. Referenced original source bytes and hashes are unchanged.


- mko_definition · cited — For small, fully specified finite simple graphs, exhaustively enumerate all edge subsets, retain only valid matchings and obtain the exact maximum size and witnesses. Validate every candidate as a matching first. Maximal does not mean maximum, and several maximum matchings may coexist. · mko-maximum-matching
- work · prerequisite — A finite simple undirected graph has loop-free duplicate-free unordered edges; graph properties are audited on all declared V and E. Matchings have disjoint selected-edge endpoint sets; maximum means greatest cardinality over all valid matchings, and argmax contains every attaining set.





## Main derivation

S01 · impliesBefore

|E|=3

After

|\mathcal P(E)|=2^3=8

Conditions: none

Rule: work · Uses: G1, work

Leaf basis: work

Each edge is selected or not, giving exactly eight candidates.



S02 · impliesBefore

000

After

\varnothing\text{ valid, size }0

Conditions: none

Rule: work · Uses: G1, S01, work

Leaf basis: work

The empty set is a valid matching of size zero.



S03 · impliesBefore

100,010,001

After

\{e_0\},\{e_1\},\{e_2\}\text{ valid, size }1

Conditions: none

Rule: work · Uses: G1, S02, work

Leaf basis: work

All three singletons are valid existing edges.



S04 · impliesBefore

110

After

e_0\cap e_1=\{1\}\implies\text{invalid}

Conditions: none

Rule: work · Uses: G1, S03, work

Leaf basis: work

The first two-edge candidate has a shared endpoint.



S05 · impliesBefore

101

After

e_0\cap e_2=\varnothing\implies\text{valid, size }2

Conditions: none

Rule: work · Uses: G1, S04, work

Leaf basis: work

The valid two-edge candidate gives lower bound two.



S06 · impliesBefore

011

After

e_1\cap e_2=\{2\}\implies\text{invalid}

Conditions: none

Rule: work · Uses: G1, S05, work

Leaf basis: work

The last two-edge candidate also conflicts.



S07 · impliesBefore

111

After

\{e_0,e_1,e_2\}\text{ invalid since }e_0\cap e_1\ne\varnothing

Conditions: none

Rule: work · Uses: G1, S06, work

Leaf basis: work

The three-edge candidate contains a known conflicting pair and is invalid.



S08 · impliesBefore

\text{valid sizes }0,1,1,1,2

After

\nu(G)=2,\quad\operatorname{Argmax}=\{\{e_0,e_2\}\}

Conditions: none

Rule: work · Uses: G1, S07, work

Leaf basis: work

Maximize over all valid candidates and list all maximizers of this graph.







## Substeps and lemmas

No substeps in this guide.





## Reverse audits


- S08 · premise_audit · G1, S07, work — Uniqueness follows from this enumeration only, not from the notion of maximum.
- S07 · premise_audit · G1, S06, work — The count 1+3+3+1=8 matches the candidate total.
- S06 · premise_audit · G1, S05, work — All three two-edge subsets are classified.
- S05 · premise_audit · G1, S04, work — Both selected edges belong to the graph.
- S04 · premise_audit · G1, S03, work — Invalid candidates cannot enter the maximum comparison.
- S03 · premise_audit · G1, S02, work — All three are listed, not one representative sample.
- S02 · premise_audit · G1, S01, work — The empty case must be retained.
- S01 · premise_audit · G1, work — Every mask is a distinct subset; none are samples.





## Error controls and negative controls

Mask coverageRetain all eight masks000 through111.

Validity firstMaximize over valid matchings, not all subsets.


- The middle-edge singleton is maximum. → reject — {e0,e2} is valid and larger.
- Mask111 is maximum because it has most edges. → reject — It fails matching validity.
- One two-edge test lists all maximizers. → reject — The full eight candidates supply complete classification.





## Result and limitations

All eight subsets are classified: maximum size 2 with unique witness{e0,e2}.







## Verification and source binding

3 declared checks for this guide; only the listed expressions are covered.


- source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f
- adopted source SHA-256: 94fd437d003f1addeeb74ab8d4d231b1284b7766692069ced54c9aceff607234
- original source SHA-256: d891a3efe19c2e43e545e39e1e80e982def72e3a3b37c914e50437febe7b0dae
- Lean: NOT_RUN · independent AI: SCOPED_LEAD_AND_BILINGUAL_CONTEXT_REVIEW

[Same-source full JSON (formulas, ASTs, controls and revision log)](https://ocme.evemisslab.com/data/derivations/coverage-20261021/guides/derivation-mko-maximum-matching-01.json)