# Graph isomorphism: checking bijectivity and both directions of adjacency preservation from a complete mapping table [← Guide index](https://ocme.evemisslab.com/en/derivations/) · [Original MKO](https://ocme.evemisslab.com/en/mko/mko-graph-isomorphism/) 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-isomorphism-01 · production-20261019-adopted-96 ## Goal and scope G has vertices 1, 2, 3, 4 and edges {1,2}, {2,3}, {3,4}, {1,4}; H has vertices a, b, c, d and edges {a,c}, {b,c}, {b,d}, {a,d}. Prove that f: 1↦a, 2↦c, 3↦b, 4↦d is a graph isomorphism G→H; show that the bijection g: 1↦a, 2↦b, 3↦c, 4↦d is not an isomorphism; and prove that the path P (edges {1,2}, {2,3}, {3,4}) is not isomorphic to H, even though f sends every edge of P to an edge of H. Stays inside the MKO: complete edge sets of finite undirected simple graphs and a complete mapping table (assumption a1). The guide checks both requirements of an isomorphism item by item and proves in general the lemma that an isomorphism induces a bijection between edge sets, using it as an invariant for refutation; a matching degree multiset is treated only as a necessary clue (assumption a2). The general theory of walks, paths, connected components and colouring is not treated, and the canonical MKO and its English edition are not changed. ## Givens and symbols - graph_basics - function_def - injective_surjective_def - finite_counting_basics - finite_forall - G1 — G: V(G)={1,2,3,4}, E(G)={{1,2},{2,3},{3,4},{1,4}} (complete list). - G2 — H: V(H)={a,b,c,d}, E(H)={{a,c},{b,c},{b,d},{a,d}} (complete list). - G3 — Mapping table f: f(1)=a, f(2)=c, f(3)=b, f(4)=d. - G4 — For comparison: mapping table g: g(1)=a, g(2)=b, g(3)=c, g(4)=d; path graph P: V(P)={1,2,3,4}, E(P)={{1,2},{2,3},{3,4}}. - V(G),\ E(G) — vertex set and edge set of G - \{u,v\} — unordered vertex pair; a possible edge when u≠v - f,\ g — two mapping tables from V(G) to V(H) - P — path graph on 1 to 4 with edges {1,2}, {2,3}, {3,4} - f^{-1} — inverse of the bijection f - \deg(v) — degree of the vertex v ## Rules and sources - graph_basics · prerequisite — (Simple undirected) graph: G=(V,E), where each edge is an unordered pair of distinct vertices; the degree of a vertex is the number of edges at it; handshake lemma Σ_v deg(v)=2|E|. - function_def · prerequisite — Function: f:A→B assigns to each a∈A exactly one f(a)∈B. Two functions are equal ⇔ they have the same domain and codomain and agree at every a. - injective_surjective_def · prerequisite — Injective: f(a)=f(a′) ⇒ a=a′. Surjective: every b∈B has some a∈A with f(a)=b. Bijective: both; then there is a unique inverse f⁻¹ with f⁻¹∘f=id_A and f∘f⁻¹=id_B. - finite_counting_basics · prerequisite — Finite counting: for disjoint finite sets A, B, |A∪B|=|A|+|B|; |A×B|=|A|·|B|; there is a bijection between finite sets ⇔ they have the same number of elements. - def_unfold · prerequisite — Unfolding a definition: replacing a defined term by its definition (or folding it back) does not change whether a statement is true. - exists_intro · prerequisite — ∃-introduction: if some a∈D satisfies P(a), then ∃x∈D, P(x). - and_intro_elim · prerequisite — Conjunction: from P and Q infer P∧Q; from P∧Q infer P and infer Q. - forall_elim · prerequisite — ∀-elimination (instantiation): if ∀x∈D, P(x) holds and a∈D, then P(a) holds. - set_extensionality · prerequisite — Set equality: A=B if and only if A⊆B and B⊆A, i.e. they have the same elements. - eq_replace · prerequisite — Replacement of equals: an expression inside a statement may be replaced by an equal expression without changing whether the statement is true. - case_analysis · prerequisite — Proof by cases: if P∨Q holds and both P⇒R and Q⇒R are proved, then R holds. The cases must cover every possibility. - set_operations_def · prerequisite — Set operations: x∈A∪B ⇔ x∈A or x∈B; x∈A∩B ⇔ x∈A and x∈B; x∈A∖B ⇔ x∈A and x∉B; in a universe U, Aᶜ=U∖A. - iff_intro · prerequisite — Biconditional: P⇔Q holds exactly when both P⇒Q and Q⇒P hold. - contradiction · prerequisite — Proof by contradiction: if assuming ¬P leads to a contradiction (a statement and its negation both hold), then P holds. - quantifier_negation · prerequisite — Negating quantifiers: ¬(∀x, P(x)) is equivalent to ∃x, ¬P(x), and ¬(∃x, P(x)) is equivalent to ∀x, ¬P(x). - contrapositive · prerequisite — Contrapositive: P⇒Q is equivalent to ¬Q⇒¬P. The converse Q⇒P is in general not equivalent to P⇒Q. - numeric_evaluation · prerequisite — Exact evaluation of an explicit integer or rational expression; independently recomputable. - mko_iso_def · cited — A graph isomorphism f:V(G)→V(H) must be bijective and, for all distinct u,v, {u,v} is an edge of G iff {f(u),f(v)} is an edge of H. Preserving edges without preserving nonedges is insufficient. · mko-graph-isomorphism - finite_forall · prerequisite — Finite universal: for a finite set D, 'for all t∈D, Φ(t)' is equivalent to the conjunction of the instances obtained by substituting each element of D; the list must be complete. - L_edge_bij · lemma — If φ:V(G)→V(H) is an isomorphism of finite simple graphs, then {u,v}↦{φ(u),φ(v)} is a bijection E(G)→E(H), so |E(G)|=|E(H)|. ## Main derivation S01 · definitionBefore f:V(G)\to V(H)\ \text{is an isomorphism} After f\ \text{bijective}\ \land\ \forall u\neq v:\ (\{u,v\}\in E(G)\Leftrightarrow\{f(u),f(v)\}\in E(H)) Conditions: none Rule: mko_iso_def · Uses: G1, G2, G3 Leaf basis: mko_iso_def + def_unfold Unfold the definition of the MKO: both requirements must hold. First, f is a bijection; second, for every pair of distinct vertices, 'adjacent in G' and 'images adjacent in H' are true or false together. The second requirement is an iff: edges must go to edges and nonedges to nonedges. S02 · impliesBefore f(1)=a,\ f(2)=c,\ f(3)=b,\ f(4)=d After f:V(G)\to V(H)\ \text{is a function} Conditions: none Rule: function_def · Uses: G1, G2, G3 Leaf basis: function_def The table gives exactly one value to each of the four vertices of V(G), and every value lies in V(H), so f is a function from V(G) to V(H). The table is complete (assumption a1), with no undefined vertex. S03 · impliesBefore f(1),f(2),f(3),f(4)=a,c,b,d After f(u)=f(v)\Rightarrow u=v Conditions: none Rule: injective_surjective_def · Uses: S02 Leaf basis: injective_surjective_def + finite_forall The four images a, c, b, d are pairwise distinct (C(4,2)=6 comparisons), so distinct vertices have distinct images; equivalently f(u)=f(v) implies u=v, and f is injective. S04 · impliesBefore V(H)=\{a,b,c,d\} After a=f(1),\ b=f(3),\ c=f(2),\ d=f(4) Conditions: none Rule: injective_surjective_def · Uses: S02, G2 Leaf basis: injective_surjective_def + exists_intro + finite_forall Find a preimage for every element of V(H): a=f(1), b=f(3), c=f(2), d=f(4). So f is surjective. S05 · impliesBefore f\ \text{injective},\ f\ \text{surjective} After f\ \text{bijective};\ f^{-1}:\ a\mapsto 1,\ b\mapsto 3,\ c\mapsto 2,\ d\mapsto 4 Conditions: none Rule: and_intro_elim · Uses: S03, S04 Leaf basis: and_intro_elim + injective_surjective_def Injective and surjective means bijective, with a unique inverse f⁻¹ read off the table backwards. The first requirement holds. S06 · equivalentBefore \forall u\neq v\in V(G):\ (\{u,v\}\in E(G)\Leftrightarrow\{f(u),f(v)\}\in E(H)) After \text{the iff for each of the}\ \tbinom42=6\ \text{unordered pairs} Conditions: none Rule: finite_forall · Uses: S01, G1, finite_forall Leaf basis: finite_forall + forall_elim + finite_counting_basics The condition for (u,v) and for (v,u) is the same statement, since {u,v}={v,u} and {f(u),f(v)}={f(v),f(u)}. The ordered pairs of distinct vertices are exactly the 6 unordered pairs taken in both orders, so the universal condition is equivalent to its holding for each of the 6 unordered pairs {1,2}, {1,3}, {1,4}, {2,3}, {2,4}, {3,4}. S07 · equivalentBefore \{u,v\}\mapsto\{f(u),f(v)\} After \{1,2\}\mapsto\{a,c\},\ \{1,3\}\mapsto\{a,b\},\ \{1,4\}\mapsto\{a,d\},\ \{2,3\}\mapsto\{b,c\},\ \{2,4\}\mapsto\{c,d\},\ \{3,4\}\mapsto\{b,d\} Conditions: none Rule: function_def · Uses: S06, G3 Leaf basis: function_def + eq_replace Look up the image of each of the 6 unordered pairs. For example the image of {2,3} is {f(2),f(3)}={c,b}={b,c}. Since f is injective, each image is again a set of two distinct vertices. S08 · case_splitBefore \{u,v\}\in E(G)\ ? After \{1,2\},\{2,3\},\{3,4\},\{1,4\}\in E(G);\ \{1,3\},\{2,4\}\notin E(G) Conditions: none Rule: case_analysis · Uses: G1, S06 Leaf basis: case_analysis + graph_basics Split the 6 unordered pairs by whether they are edges of G: four edges and two nonedges. Since E(G) is listed completely, an unlisted pair is a nonedge. S09 · impliesBefore \{f(u),f(v)\}\in E(H)\ ? After \{a,c\},\{b,c\},\{b,d\},\{a,d\}\in E(H);\ \{a,b\},\{c,d\}\notin E(H) Conditions: none Rule: graph_basics · Uses: G2, S07 Leaf basis: graph_basics + set_operations_def Look up the 6 images of S07 in the complete edge list of H: {a,c}, {b,c}, {b,d}, {a,d} are listed; {a,b} and {c,d} are not, so they are nonedges of H. S10 · impliesBefore \text{edge status of}\ \{u,v\}\ \text{in}\ G\ \text{and of its image in}\ H After \{u,v\}\in E(G)\Leftrightarrow\{f(u),f(v)\}\in E(H)\ \text{for all 6 pairs} Conditions: none Rule: iff_intro · Uses: S07, S08, S09 Leaf basis: iff_intro + case_analysis + finite_forall Compare pair by pair: the images {a,c}, {b,c}, {b,d}, {a,d} of the four edges {1,2}, {2,3}, {3,4}, {1,4} of G are edges of H; the images {a,b}, {c,d} of the two nonedges {1,3}, {2,4} of G are nonedges of H. For every pair both sides are true together or false together, so each iff holds. S11 · impliesBefore f\ \text{bijective},\ \text{iff on all 6 pairs} After f:G\to H\ \text{is an isomorphism},\ G\cong H Conditions: none Rule: mko_iso_def · Uses: S01, S05, S06, S10 Leaf basis: mko_iso_def + and_intro_elim Bijectivity comes from S05; S06 reduces the universal adjacency condition to 6 pairs, and S10 establishes all 6. By the definition in S01, f is an isomorphism, so G≅H. The conclusion depends only on the complete mapping table and complete edge lists, not on degrees or how the figures look. S12 · impliesBefore g(1)=a,\ g(2)=b,\ \{1,2\}\in E(G) After \{g(1),g(2)\}=\{a,b\}\notin E(H)\Rightarrow g\ \text{not an isomorphism} Conditions: none Rule: contradiction · Uses: S01, G1, G2, G4 Leaf basis: contradiction + quantifier_negation + injective_surjective_def The four images a, b, c, d of g are distinct and cover V(H), so g is also a bijection. But {1,2} is an edge of G while its image {a,b} is not an edge of H, so the iff fails at this pair. One counterexample refutes the universal condition, so g is not an isomorphism. Bijectivity alone is not enough. S13 · impliesBefore f\ \text{on}\ P:\ \{1,2\},\{2,3\},\{3,4\}\mapsto\{a,c\},\{b,c\},\{b,d\} After \text{every edge of}\ P\ \text{goes to an edge of}\ H Conditions: none Rule: graph_basics · Uses: G4, G3, G2 Leaf basis: graph_basics + function_def Regard f as a bijection V(P)→V(H): the images {a,c}, {b,c}, {b,d} of the three edges of P all lie in E(H). So f 'preserves edges'. This is exactly the situation the MKO warns about: preserving edges is not enough. S14 · impliesBefore \{1,4\}\notin E(P) After \{f(1),f(4)\}=\{a,d\}\in E(H)\Rightarrow f\ \text{is not an isomorphism}\ P\to H Conditions: none Rule: contradiction · Uses: S13, G4, G2 Leaf basis: contradiction + quantifier_negation {1,4} is not an edge of P (the edge list of P is complete), but its image {a,d} is an edge of H. The '⇐' direction of the iff fails, so f is not an isomorphism P→H. Declaring an isomorphism after checking only that edges go to edges is wrong. S15 · impliesBefore |E(P)|=3,\ |E(H)|=4 After \text{no isomorphism}\ P\to H\ \text{exists} Conditions: 3\neq 4 Rule: L_edge_bij · Uses: G2, G4 Leaf basis: L_edge_bij + contrapositive + numeric_evaluation By Lemma L_edge_bij (proved in S15.1 to S15.3), any isomorphism φ:P→H gives a bijection E(P)→E(H), so |E(P)|=|E(H)|. But 3≠4, so by contraposition there is no isomorphism P→H at all, not merely that f fails. A mismatch of the edge-count invariant suffices to refute. S16 · impliesBefore \deg\ \text{in}\ G\ \text{and}\ H After \{2,2,2,2\}=\{2,2,2,2\} Conditions: none Rule: graph_basics · Uses: G1, G2, S11 Leaf basis: graph_basics + numeric_evaluation In G, N(1)={2,4}, N(2)={1,3}, N(3)={2,4}, N(4)={1,3}; in H, N(a)={c,d}, N(b)={c,d}, N(c)={a,b}, N(d)={a,b}; every degree is 2, and the handshake lemma checks 4·2=2·4. The matching degree multiset is consistent with S11. In general it is only necessary: C6 and two triangles refute general sufficiency. Here, however, a simple graph on four vertices with all degrees 2 is necessarily C4, so this special condition forces both graphs to be C4. This guide instead selects the complete map proof of S11 and does not use that classification route. ## Substeps and lemmas S15.1 · impliesBefore \{u,v\}\in E(G) After \{\varphi(u),\varphi(v)\}\in E(H) Conditions: \varphi\ \text{isomorphism} Rule: mko_iso_def · Uses: mko_iso_def, injective_surjective_def Leaf basis: mko_iso_def + injective_surjective_def Let φ be an isomorphism and {u,v} an edge of G. Then u≠v, injectivity gives φ(u)≠φ(v), and the '⇒' direction of the iff gives {φ(u),φ(v)}∈E(H). So the correspondence really maps E(G) into E(H). S15.2 · impliesBefore \{\varphi(u),\varphi(v)\}=\{\varphi(u'),\varphi(v')\} After \{u,v\}=\{u',v'\} Conditions: \varphi\ \text{bijective} Rule: injective_surjective_def · Uses: S15.1, injective_surjective_def Leaf basis: injective_surjective_def + function_def Apply the inverse φ⁻¹ elementwise to the two equal two-element sets: it sends {φ(u),φ(v)} to {u,v} and {φ(u′),φ(v′)} to {u′,v′}, so the two edges are the same. The edge correspondence is injective. S15.3 · impliesBefore \{p,q\}\in E(H) After \{\varphi^{-1}(p),\varphi^{-1}(q)\}\in E(G)\ \Rightarrow\ |E(G)|=|E(H)| Conditions: \varphi\ \text{isomorphism} Rule: mko_iso_def · Uses: S15.1, S15.2, mko_iso_def, finite_counting_basics Leaf basis: mko_iso_def + injective_surjective_def + finite_counting_basics Given an edge {p,q} of H, let u=φ⁻¹(p) and v=φ⁻¹(q); then u≠v and {φ(u),φ(v)}={p,q}∈E(H), so the '⇐' direction of the iff gives {u,v}∈E(G), which is sent to {p,q}. The edge correspondence is therefore surjective. With S15.1 and S15.2 it is a bijection between the finite sets E(G) and E(H), so |E(G)|=|E(H)| by finite counting. S15.1 to S15.3 together prove Lemma L_edge_bij. ## Reverse audits - S16 · premise_audit · G1, G2, graph_basics — This guide records the step as a consistency check of an invariant; the direct map proof of S11 does not depend on it. Adding the classification that a four-vertex simple 2-regular graph is C4 would provide another proof route. - S15.3 · premise_audit · mko_iso_def, finite_counting_basics — Surjectivity is exactly where the 'nonedges to nonedges' half of the iff is used; an edge-preserving map does not guarantee it. This sub-step does not use L_edge_bij. - S15.2 · premise_audit · injective_surjective_def — It needs φ⁻¹ to exist, that is, φ bijective; this sub-step does not use L_edge_bij. - S15.1 · premise_audit · mko_iso_def, injective_surjective_def — Only one direction of the iff and injectivity are used; this sub-step does not use L_edge_bij. - S15 · premise_audit · L_edge_bij, contrapositive — It uses the contrapositive of 'isomorphic ⇒ equal edge counts'; the converse 'equal edge counts ⇒ isomorphic' is false and not claimed. - S14 · premise_audit · G4, G2, contradiction — This refutes only the table f; whether P and H are non-isomorphic altogether needs the invariant argument of S15. - S13 · premise_audit · G4, G3, G2 — Only the '⇒' direction is checked; it does not claim that nonedges are preserved (S14 shows they are not). - S12 · premise_audit · G1, G2, G4, contradiction — Refutation needs one failing pair; the step does not claim G and H are non-isomorphic (S11 proves they are), only that the table g is not an isomorphism. - S11 · sufficient_goal_reduction · S01, S05, S06, S10 — Goal G: f is an isomorphism. Sufficient condition H: f is bijective and the iff holds on all 6 pairs; H⇒G by S01 and S06. H is proved forwards in S02 to S10; G is never used as a premise. - S10 · premise_audit · S08, S09, iff_intro, case_analysis — The edge case gives the '⇒' direction and the nonedge case gives '⇐' (in contrapositive form: nonedges of G match nonedges of H). Missing either class would not give the iff. - S09 · premise_audit · G2, S07, graph_basics — It needs only table lookups; deciding nonedges relies on the complete list of E(H) (assumption a1). - S08 · premise_audit · G1, case_analysis — The two classes cover all 6 pairs and are disjoint; the complete list of E(G) is needed, otherwise 'not listed' would not mean nonedge. - S07 · inverse_equivalence · function_def, S05 — Looking up values replaces equals; f⁻¹ maps each image back to its pair, so the step is two-way. - S06 · inverse_equivalence · finite_forall, set_extensionality — The universal gives each instance (∀-elimination); with the complete list of 6 instances, all of them together give the universal. Both directions hold. - S05 · premise_audit · S03, S04, injective_surjective_def — Bijectivity is only the first requirement; on its own it does not give an isomorphism (g in S12 is also a bijection). - S04 · premise_audit · S02, G2, injective_surjective_def — Each element of V(H) needs only one preimage, and all four are listed. - S03 · premise_audit · S02, injective_surjective_def — All six comparisons are made; only injectivity is claimed, nothing about adjacency. - S02 · premise_audit · G3, function_def — It needs exactly one row per vertex with a value in V(H); both are read directly from the table. - S01 · premise_audit · mko_iso_def — This step only unfolds the definition; bijectivity is checked first (S02 to S05), then the adjacency condition (S06 to S10). ## Error controls and negative controls Preserving edges is not enoughThe common mistake named by the MKO is to declare an isomorphism after checking only that edges go to edges. f sends all three edges of P to edges of H (S13), but the nonedge {1,4} goes to the edge {a,d} (S14). Both directions of the iff must be checked: edges to edges and nonedges to nonedges. Matching degree sequences is not a proofThe six-cycle C6 and two disjoint triangles both have six vertices, six edges and every degree equal to 2, but they are not isomorphic: two triangles contain three pairwise adjacent vertices, C6 does not, and an isomorphism sends three pairwise adjacent vertices to three pairwise adjacent vertices. So matching invariants are only necessary; the isomorphism here comes from the pair-by-pair check of S11. Check bijectivity and adjacency separatelyg is a bijection but not an isomorphism (S12); separately, if a table sent two vertices to the same point, some {u,v} would have a one-point image that is not even a candidate edge. The MKO's order is to check bijectivity first, then all unordered vertex pairs. - For any two finite undirected simple graphs, equality of their degree multisets is sufficient to imply that the graphs are isomorphic → reject — C6 and two disjoint triangles have the same degree multiset but are not isomorphic, refuting the general claim. Four vertices all of degree 2 form a special case that does force both graphs to be C4; this guide nevertheless proves G≅H directly using the map in S11. - f sends every edge of P to an edge of H, so f is an isomorphism P→H → reject — The nonedge {1,4} is sent to the edge {a,d} of H. - g is a bijection V(G)→V(H), so g is an isomorphism → reject — {1,2}∈E(G) but {g(1),g(2)}={a,b}∉E(H). - P and H both have four vertices, so a suitable mapping table makes them isomorphic → reject — By L_edge_bij an isomorphism needs equal edge counts, but |E(P)|=3≠4=|E(H)|. ## Result and limitations f: 1↦a, 2↦c, 3↦b, 4↦d is a bijection and the adjacency iff holds on all 6 unordered vertex pairs, so f is an isomorphism and G≅H. The bijection g fails at {1,2}↦{a,b} and is not an isomorphism. f sends every edge of the path P to an edge of H but sends the nonedge {1,4} to the edge {a,d}; and by Lemma L_edge_bij, |E(P)|=3≠4=|E(H)|, so P and H are not isomorphic. - The remark in the error controls that an isomorphism preserves three pairwise adjacent vertices is explanatory; it follows directly from the iff condition and is not a numbered step. - finite_forall is a premise of this guide and is not derived here from more basic logical rules. ## Verification and source binding 5 declared checks for this guide; only the listed expressions are covered. - source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f - adopted source SHA-256: a7cc7455e8b911e77e5121725e1be4abeed121e79d85845f5c53dcd1836af658 - original source SHA-256: 9d22ff5f2bd20224ad3785c20866dd5d700d99fedad9037b43fd496881eceb3e - Lean: NOT_RUN · independent AI: NOT_MEASURED [Same-source full JSON (formulas, ASTs, controls and revision log)](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-graph-isomorphism-01.json)