# Maximal versus maximum in P4 [← Guide index](https://ocme.evemisslab.com/en/derivations/) · [Original MKO](https://ocme.evemisslab.com/en/mko/mko-graph-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-graph-matching-01 · ocme-new142-reader-adoption-20261021 ## Goal and scope Audit selected edges and endpoints, then distinguish matching properties. Selected edges are identified by original edge indices. ## Givens and symbols - work - G1 — V={0,1,2,3}; all edges are e0={0,1}, e1={1,2}, e2={2,3}. M={e1}, N={e0,e2}. - V,E — complete vertex and edge sets - M,N — candidate edge sets ## 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 — On a fully specified finite simple undirected graph, check that every selected edge exists and that their endpoint sets are disjoint. Distinguish matching, maximal, maximum and perfect. A larger valid matching can disprove maximum cardinality, but one matching alone does not establish optimality. · mko-graph-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. A matching selects original edges with disjoint endpoint sets; maximal means no edge can be added; maximum means greatest cardinality among all matchings; perfect covers every vertex exactly once. ## Main derivation S01 · impliesBefore M=\{e_1\} After M\subseteq E,\quad\operatorname{ends}(e_1)=\{1,2\} Conditions: none Rule: work · Uses: G1, work Leaf basis: work The sole selected edge of M exists in the original graph. S02 · impliesBefore |M|=1 After M\text{ is a matching} Conditions: none Rule: work · Uses: G1, S01, work Leaf basis: work With one edge, the no-common-endpoint condition for distinct selected edges is vacuous. S03 · impliesBefore e_0\cap e_1=\{1\},\quad e_2\cap e_1=\{2\} After M\cup\{e_0\},M\cup\{e_2\}\text{ are invalid} Conditions: none Rule: work · Uses: G1, S02, work Leaf basis: work Both unselected edges conflict with M. S04 · impliesBefore \forall e\in E\setminus M:\ M\cup\{e\}\text{ invalid} After M\text{ is inclusion-maximal} Conditions: none Rule: work · Uses: G1, S03, work Leaf basis: work No single edge can be added, giving maximality, not maximum cardinality. S05 · impliesBefore N=\{e_0,e_2\}\subseteq E After \{0,1\}\cap\{2,3\}=\varnothing Conditions: none Rule: work · Uses: G1, S04, work Leaf basis: work Both edges of N exist and have disjoint endpoints. S06 · impliesBefore N\text{ matching},\quad|N|=2>|M|=1 After M\text{ is not maximum} Conditions: none Rule: work · Uses: G1, S05, work Leaf basis: work A larger valid matching completely witnesses that M is not maximum. S07 · impliesBefore \bigcup_{e\in N}\operatorname{ends}(e)=V After N\text{ is perfect} Conditions: none Rule: work · Uses: G1, S06, work Leaf basis: work N covers all four vertices exactly once. S08 · impliesBefore 2|Q|\le|V|=4\quad\text{for every matching }Q After |Q|\le2=|N| Conditions: none Rule: work · Uses: G1, S07, work Leaf basis: work Disjoint endpoints give a global bound, proving N maximum as well. ## Substeps and lemmas No substeps in this guide. ## Reverse audits - S08 · premise_audit · G1, S07, work — The bound is explicit rather than hidden behind the word perfect. - S07 · premise_audit · G1, S06, work — M covers only 1,2 and is not perfect. - S06 · premise_audit · G1, S05, work — Disproving M's optimality does not require first finding all matchings. - S05 · premise_audit · G1, S04, work — M and N need not be nested to compare cardinalities. - S04 · premise_audit · G1, S03, work — Do not replace local nonextendability with global comparison. - S03 · premise_audit · G1, S02, work — E minus M is exhausted; no other addable edge exists. - S02 · premise_audit · G1, S01, work — Vacuity does not replace edge membership. - S01 · premise_audit · G1, work — A nonexistent edge index cannot belong to a matching. ## Error controls and negative controls Edge indexUse only e0,e1,e2; audit membership before endpoints. Three obligationsMatching checks validity, maximality checks additions, maximum checks global bounds. - M is maximal, hence maximum. → reject — N has two edges versus M's one. - {e0,e1} is a matching. → reject — They share vertex 1. - A maximum matching must be unique. → reject — On a four-cycle either pair of opposite edges is maximum, so uniqueness is not implied. ## Result and limitations M is maximal but not maximum; N is perfect and maximum. ## Verification and source binding 2 declared checks for this guide; only the listed expressions are covered. - source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f - adopted source SHA-256: 22060fb56bf6f78f3fa82bf3167fab58e9952536d67a4ce7133e8e015f9d26c7 - original source SHA-256: 4cbd728a4a404d039a883891cd08ccedaba32b8a02eb68156ade1d3055bfc564 - 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-graph-matching-01.json)