bipartite_graph_reconstruction_conjecture_2.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 348 curated AI-written annotations and 373 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 12 manuscript-grounded curated result annotations were composed from pinned companion PDFs and named source records in a Codex session on 2026-10-14; no human review is claimed, and the exact runtime model identifier was not exposed to the artifact generator. Twelve supporting declarations for the Hilbert-functions result were upgraded on 2026-10-14 from mechanically condensed doc comments to declaration-specific explanations bound to exact page-one terminology in the pinned human-written companion. The other Hilbert challenge statements were deliberately not described as companion-backed results because that manuscript proves P5 specifically. Fifteen previously unannotated declarations along the Hilbert P5 proof spine were annotated on 2026-10-14 from the pinned companion's seven-page argument, covering the two-generator decomposition, finite-difference bounds, critical-case reduction, and final log-concavity step. Each quotation is bound to its exact manuscript page and Lean declaration; no human review is claimed. Twenty-four further declarations along the Hilbert P5 box-count and finite-difference spine were annotated on 2026-10-14, covering the two-dimensional slice count, three-dimensional box formula, first- and second-difference identities, the seven-threshold curvature expression, boundary handling, pointwise transport, sum linearity, and lower-or-upper region classification. Every annotation is bound to an exact quotation on pages 2 or 3 of the pinned human-written companion; Lean-specific boundary and threshold helpers are identified as implementation lemmas rather than separate manuscript claims. No human review is claimed. Twenty-eight further declarations along the Hilbert P5 argument were annotated on 2026-10-14 from pages 2 through 6 of the pinned human-written companion. They expose the shifted residual sequence, exact lower- and upper-region formulas, symmetry by complementary divisors, the curvature-one and curvature-two splits, and the final algebraic reductions. Lean-only transport and integer-arithmetic helpers are labeled as proof infrastructure rather than new manuscript claims; each quotation is page-bound in the source ledger, and no human review is claimed. Twenty high-level declarations completing the Hilbert P5 curvature-one and curvature-two case spine were annotated on 2026-10-14 from pages 3 through 7 of the pinned human-written companion. The explanations separate cases A and B, lower and upper monomial regions, shifted residual evaluation, impossible mixed regions, and the surviving upper-upper estimate; wrapper lemmas are explicitly described as proof structure. Every quotation is page-bound, and no human review is claimed. Twenty-two graph-reconstruction declarations were upgraded or added on 2026-10-14 from the pinned four-page human-written companion, covering the incidence-deletion deck, edge and degree recovery, unique isolated vertices, vertex-type reconstruction, neighboring-type descent, adjacency recovery, and final bipartite isomorphism. The result annotation also records that `G_not_regular` is present in the Lean statement but unused by its proof term and absent from the companion theorem. Exact historical quotations from Paul J. Kelly (1957) and Bondy with Hemminger (1977) are linked separately; no human review is claimed. Eighteen declarations along the Erdős 741(i) strict-natural-density counterexample were added on 2026-10-14, covering the carry-free base-four digit split, full cross-sum coverage, sparse pure self-sums, fixed-factor fat intervals, the lower-scale density deficit, upper-scale sum growth, and the final convergence contradiction. The result annotation was corrected to distinguish the negative strict-natural-density Lean theorem from the compatible affirmative upper-density companion theorem; Ulam AI's written counterexample is explicitly identified as using a different interval length with the same mechanism. The quotations are page- and hash-bound where the PDFs expose text; Paul Erdős's scanned 1994 question was visually checked and is linked separately without a machine-audit claim. No human review is claimed. Twenty-eight additional declaration-level annotations were added on 2026-10-14 for the Erdős 12(i) proof, and its IsGood definition was upgraded from a source-comment condensation. They cover the prime and Chinese-remainder moduli, the actual Lean congruence-block witness, exclusion of cross-block and same-block triples, lower and upper counting bounds, and the positive liminf. The prior result annotation was corrected because the pinned human-written companion proves the same theorem with a different base-2-to-base-3 construction; it is no longer presented as the Lean proof. The original property-P definition from Erdős and Sárközy (1970) is separately linked and page-bound; no human review is claimed. The remaining fifty declarations in the Erdős 12(i) file were annotated on 2026-10-14, completing declaration-level coverage of all eighty definitions, lemmas, and theorems in that file. These additions expose the prime-recursion invariants, divisibility transport, Chinese-remainder witness bounds, numerical density envelopes, injective block coding, and liminf support lemmas instead of leaving the proof spine as raw Lean; no human review is claimed. Eighteen supporting declarations for Erdős 125 were added on 2026-10-14, completing all nineteen declarations in the file. The annotations follow the pinned companion through digit-block decomposition, irrational logarithmic approximation, the explicit Lean contraction factor 11/12, geometric iteration, and the lower-density conclusion. The original 1996 question of Burr, Erdős, Graham, and Li and the 2026 discussion contributions of GTSoukalas, Terence Tao, and Giuseppe Melfi are linked separately; no human review is claimed. Twenty-eight supporting declarations for Erdős 138 were upgraded or added on 2026-10-14, completing all twenty-nine declarations in the file. The annotations separate the greedy difference proof from the Lean-specific representation bridges and ultrafilter compactness proof of existence, and bind quotations from the pinned companion, the AlphaProof Nexus paper, Erdős's 1981 source, van der Waerden's recollection, and the 2026 Erdős Problems discussion. No human review is claimed. The curated Erdős 12(ii), 138, and 152 annotations were further linked on 2026-10-14 to exact quotations from Felix Behrend, Bartel van der Waerden, and Paul Erdős with Pál Turán; the historical quotation sources are labeled separately from the pinned AlphaProof proof companions. The curated Hilbert-functions result, its OrderIdeal and pureOSequence definitions, and the Erdős 846 annotation were further linked on 2026-10-14 to exact quotations from Richard P. Stanley and from Moe Putterman, Mehtaab Sawhney, and Gregory Valiant. The Stanley PDF is hash- and page-bound in the source ledger; these historical sources are labeled separately from the pinned AlphaProof proof companions. Three additional target-specific annotations for Ben Green's Problem 57, exact last-iterate anchored-GDA convergence, and Graffiti.pc Conjecture 2 were composed on 2026-10-14 from the exact pinned Lean statements, quotations from the AlphaProof Nexus paper, and quotations from Green, Ryu with Yuan and Yin, Surina et al., and Wang with Dai and Tong; no human review is claimed. Two additional target-specific quantum-optics annotations for the explicit AME(11,5) construction and the even N >= 4, D = N monochromatic-quantum-graph theorem were composed on 2026-10-14 from the exact pinned Lean statements, page-bound quotations from the AlphaProof Nexus paper, Helwig et al., and Krenn, Gu, and Zeilinger, and Mario Krenn's public priority correction. The AME annotation makes no first-discovery claim; the monochromatic annotation states that the local AlphaProof wrapper contains sorry and links the separate pinned proof-bearing Formal Conjectures artifact without silently treating it as local verification. Twelve declarations that the pinned source repeats verbatim in several files were annotated in only one of the copies, so the build rejected them as differing copies. On 2026-10-16 each curated annotation was copied unchanged to every identical copy: the eleven Hilbert-functions definitions from hilbert_functions_5 to hilbert_functions_1, _2, _3, _4, _7 and _8, and Erdos12.IsGood from erdos_12.parts.i to erdos_12.parts.ii (the better-sourced annotation was kept in each case). Each copy's quotations are bound in the source ledger like the original's; no new text was written and no human review is claimed. The remaining source-derived annotations were generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the source prose.

Credit: Google DeepMind published the AlphaProof Nexus proof artifacts. The pinned repository identifies the mathematical sources and collaborators, including OEIS, Erdős Problems, Gergely Bérczi, and Mario Krenn; those source records remain the authority for individual credit.

Project sources: Pinned AlphaProof Nexus results documentation, AlphaProof Nexus paper, Pinned human-written natural-language proof companions

68 declarations, 0 contain sorry, 0 declared as axioms

Imports (1)

Mathlib

abbrev edgeCount line 49 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: SimpleGraph, Nat
Proof uses: Nat.card, Sym2, SimpleGraph.edgeSet
1 instances, coercions and auxiliary constants left out.
structure BipartiteIso A graph isomorphism that preserves both sides of the bipartition line 52 source
Source documentation
Strict bipartite isomorphism that explicitly preserves the left and right partitions.
L4DEL explanation
is a graph isomorphism whose underlying bijection preserves both parts L and R.
— Human-written graph-reconstruction proof companion
BipartiteIso G H leftU rightV strengthens an ordinary graph isomorphism by requiring its vertex equivalence to preserve membership in leftU and rightV separately. Swapping the two sides is not allowed.
1. The inherited relation isomorphism preserves and reflects adjacency.
2. map_left and map_right make preservation of the named parts explicit in both directions.
Sources and attribution: Pinned Lean source (0647711a7118), Human-written graph-reconstruction proof companion
standard axioms: Quot.sound, propext what this means
Statement uses: SimpleGraph, Finset
```
structure BipartiteIso (G H : SimpleGraph V) (leftU rightV : Finset V) extends G ≃g H where
…
```
lemma isBipartiteWith_deleteIncidenceSet Deleting the incidence set of a vertex keeps the graph bipartite with the same partitions line 59 source
Source comment
Deleting the incidence set of a vertex keeps the graph bipartite with the same partitions.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, SimpleGraph, Finset, SimpleGraph.IsBipartiteWith, SimpleGraph.deleteIncidenceSet
Proof uses: Disjoint, Set, SimpleGraph.Adj, Or, And, Membership.mem, SimpleGraph.IsBipartiteWith.mk, SimpleGraph.deleteIncidenceSet_le
15 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma isBipartiteWith_deleteIncidenceSet (v : V)
    (hBipartite : G.IsBipartiteWith leftU rightV) :
    (G.deleteIncidenceSet v).IsBipartiteWith leftU rightV := by
…
```
def bipartiteDeck The multiset of incidence-deleted cards up to bipartite isomorphism line 69 source
Source documentation
Deck of a bipartite graph. Deck is the multiset of all vertex-deleted subgraphs viewed unlabeled up to bipartite isomorphism.
L4DEL explanation
The bipartite deck is the multiset
— Human-written graph-reconstruction proof companion
bipartiteDeck G leftU rightV records one card for every vertex v: all edges incident to v are deleted, v remains as an isolated vertex, and the result is stored as its entire bipartite-isomorphism class. Repeated isomorphism classes retain multiplicity.
1. deleteIncidenceSet v removes incident edges rather than deleting the vertex from the type.
2. Mapping over univ produces one set-valued card per vertex, and the outer Multiset forgets their labels while retaining how often each card occurs.
Sources and attribution: Pinned Lean source (0647711a7118), Human-written graph-reconstruction proof companion
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, SimpleGraph, Finset, Multiset, Set
Proof uses: Multiset.map, setOf, Nonempty, BipartiteIso, SimpleGraph.deleteIncidenceSet, Finset.val, Finset.univ
```
def bipartiteDeck : Multiset (Set (SimpleGraph V)) :=
…
```
def degreeProfile The multiset of degrees seen around a vertex line 79 source
Source comment
The neighbor-degree profile of x ∈ U ⊔ V is the multiset P(x) = {deg_G(y) : y ∈ Neighbors(x)}
L4DEL explanation
The degree profile and type of x are
— Human-written graph-reconstruction proof companion
degreeProfile G x lists G.degree y once for every neighbor y of x. It remembers the degrees surrounding x but deliberately forgets which neighboring vertex supplied each degree.
1. neighborFinset x supplies distinct adjacent vertices.
2. Mapping G.degree over its underlying multiset preserves multiplicity, which is essential when several neighbors have the same degree.
Sources and attribution: Pinned Lean source (0647711a7118), Human-written graph-reconstruction proof companion
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, SimpleGraph, Multiset, Nat
Proof uses: Multiset.map, SimpleGraph.degree, SimpleGraph.Adj, Finset.val, SimpleGraph.neighborFinset
2 instances, coercions and auxiliary constants left out.
```
def degreeProfile (x : V) : Multiset ℕ :=
…
```
def τ A vertex type combines its degree with its neighbors' degrees line 85 source
Source comment
The type of x is τ(x) = (deg_G(x), P(x))
L4DEL explanation
The degree profile and type of x are
— Human-written graph-reconstruction proof companion
τ G x is the ordered pair consisting of the degree of x and its degree profile. Two vertices have the same type exactly when they have the same degree and the same multiset of neighboring degrees.
1. The first coordinate is local degree.
2. The second coordinate is a multiset, so it detects repeated neighbor degrees without identifying the neighbors themselves.
Sources and attribution: Pinned Lean source (0647711a7118), Human-written graph-reconstruction proof companion
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, SimpleGraph, Prod, Nat, Multiset
Proof uses: Prod.mk, SimpleGraph.degree, SimpleGraph.Adj, degreeProfile
2 instances, coercions and auxiliary constants left out.
```
def τ (x : V) : ℕ × Multiset ℕ :=
…
```
def R The typecount R(u, t) is the number of neighbors of u in rightV whose type τ equals t line 92 source
Source comment
The typecount R(u, t) is the number of neighbors of u in rightV whose type τ equals t. Symmetrically, R'(v, s) is the number of neighbors of v in leftU whose type τ equals s.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, SimpleGraph, Finset, Prod, Nat, Multiset
Proof uses: Finset.card, Finset.filter, And, Membership.mem, Eq, τ, SimpleGraph.neighborFinset, SimpleGraph.Adj
8 instances, coercions and auxiliary constants left out.
```
def R (u : V) (t : ℕ × Multiset ℕ) : ℕ :=
…
```
Mentions: u
def R' line 95 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, SimpleGraph, Finset, Prod, Nat, Multiset
Proof uses: Finset.card, Finset.filter, And, Membership.mem, Eq, τ, SimpleGraph.neighborFinset, SimpleGraph.Adj
8 instances, coercions and auxiliary constants left out.
def doubleDeck The double deck is D_2(G) = {G - x - y := x ≠ y ∈ U ⊔ V} viewed unlabeled up t bipartite isomorphism line 101 source
Source comment
The double deck is D_2(G) = {G - x - y := x ≠ y ∈ U ⊔ V} viewed unlabeled up t bipartite isomorphism.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, SimpleGraph, Finset, Multiset, Set
Proof uses: Multiset.map, Prod, setOf, Nonempty, BipartiteIso, SimpleGraph.deleteIncidenceSet, Prod.fst, Prod.snd, Finset.val, Finset.filter, Ne, Eq, Finset.univ
2 instances, coercions and auxiliary constants left out.
```
def doubleDeck : Multiset (Set (SimpleGraph V)) :=
…
```
lemma multiset_map_eq_implies_bij Equal unlabeled decks can be matched card by card line 110 source
L4DEL explanation
Equality of the two decks also gives a bijection f : Ω → Ω
— Human-written graph-reconstruction proof companion
If two functions on the same finite type produce equal multisets of values, this lemma constructs a permutation pairing every input of the first function with an input of the second having the same value. Applied to decks, it recovers a bijection between the deleted vertices of matched cards.
1. Multiset equality supplies equal fiber cardinalities for every card value.
2. Those balanced fibers are assembled into an equivalence e satisfying f a = g (e a) for every input.
Sources and attribution: Pinned Lean source (0647711a7118), Human-written graph-reconstruction proof companion
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, Eq, Multiset, Multiset.map, Finset.val, Finset.univ, Exists, Equiv
Proof uses: Iff, Finset, LE.le, Nat, Finset.card, Finset.biUnion, Finset.filter, And, Function.Injective, Membership.mem, Finset.all_card_le_biUnion_card_iff_exists_injective, Iff.mp, Eq.rec, Finset.sum, Finset.image, Trans.simple, Finset.sum_le_sum, LE.le.trans_eq, Finset.card_mono, Finset.filter_subset_filter and 45 more
37 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
```
lemma multiset_map_eq_implies_bij {α β : Type*} [Fintype α] (f g : α → β)
    (h : Multiset.map f (Finset.univ : Finset α).val = Multiset.map g (Finset.univ : Finset α).val) :
    ∃ (e : α ≃ α), ∀ a, f a = g (e a) := by
…
```
def BipartiteIso_refl line 120 source
standard axioms: Quot.sound, propext what this means
Statement uses: SimpleGraph, Finset, BipartiteIso
Proof uses: RelIso, SimpleGraph.Adj, RelIso.refl, BipartiteIso.mk
1 instances, coercions and auxiliary constants left out.
def BipartiteIso_symm line 126 source
standard axioms: Quot.sound, propext what this means
Statement uses: SimpleGraph, Finset, BipartiteIso
Proof uses: RelIso, SimpleGraph.Adj, RelIso.symm, BipartiteIso.toRelIso, BipartiteIso.mk
2 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma BipartiteIso_edgeCount line 138 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, SimpleGraph, Finset, BipartiteIso, Eq, Nat, edgeCount
Proof uses: RelIso, SimpleGraph.Adj, Iff, Membership.mem, Equiv, RelIso.toEquiv, RelIso.mk, id, Nat.card_congr, Sym2, SimpleGraph.edgeSet, Equiv.subtypeEquiv, Set, Equiv.mk, Sym2.map, Equiv.symm, Sym2.ind, Sym2.mk, Prod.mk, of_eq_true and 14 more
10 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
lemma edgeCount_deleteIncidenceSet An incidence-deleted card loses exactly the degree of its isolated vertex line 144 source
L4DEL explanation
removes exactly the edges incident to v
— Human-written graph-reconstruction proof companion
Deleting every edge incident to v changes the edge count from e(G) to e(G) − degree(v). Each incident undirected edge is removed once, even though degree is defined through the neighbor set.
1. The incidence set is identified with the image of the neighbors of v under the unordered-edge constructor.
2. Finite-set subtraction then gives the exact cardinality formula used to reconstruct degrees from card edge counts.
Sources and attribution: Pinned Lean source (0647711a7118), Human-written graph-reconstruction proof companion
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, SimpleGraph, DecidableRel, SimpleGraph.Adj, Eq, Nat, edgeCount, SimpleGraph.deleteIncidenceSet, HSub.hSub, SimpleGraph.degree
Proof uses: Eq.mpr, Finset.card, Sym2, Finset.filter, Not, Membership.mem, Set, SimpleGraph.incidenceSet, Set.toFinset, SimpleGraph.edgeSet, Finset.univ, id, congr, Nat.card, SimpleGraph.deleteEdges, SimpleGraph.neighborFinset, congrArg, Eq.trans, Fintype.card, SDiff.sdiff and 64 more
43 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
```
lemma edgeCount_deleteIncidenceSet (v : V) [DecidableRel G.Adj] :
    edgeCount (G.deleteIncidenceSet v) = edgeCount G - G.degree v := by
…
```
Mentions: edgeCount
def classEdgeCount line 152 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, SimpleGraph, Nat
Proof uses: InfSet.sInf, setOf, Exists, And, Membership.mem, Eq, edgeCount
2 instances, coercions and auxiliary constants left out.
lemma classEdgeCount_eq line 155 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, SimpleGraph, Finset, Eq, Nat, classEdgeCount, setOf, Nonempty, BipartiteIso, SimpleGraph.deleteIncidenceSet, edgeCount
Proof uses: id, IsLeast.csInf_eq, Exists, And, Membership.mem, Set, SimpleGraph.deleteEdges, SimpleGraph.incidenceSet, Nat.card, Sym2, SimpleGraph.edgeSet, And.intro, lowerBounds, Exists.intro, Nonempty.intro, BipartiteIso.mk, OfNat.ofNat, RelIso, SimpleGraph.Adj, Iff.rfl and 44 more
35 instances, coercions and auxiliary constants left out.

Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
lemma bipartiteDeck_edgeCountDeck line 169 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, Finset, SimpleGraph, Eq, Multiset, Set, bipartiteDeck, Nat, Multiset.map, classEdgeCount
Proof uses: Eq.mpr, id, congrArg, Eq.refl

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma sum_edgeCount_deleteIncidenceSet line 175 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, SimpleGraph, DecidableRel, SimpleGraph.Adj, Eq, Nat, Finset.sum, Finset.univ, edgeCount, SimpleGraph.deleteIncidenceSet, HSub.hSub, HMul.hMul, Fintype.card, OfNat.ofNat
Proof uses: Eq.mpr, Finset.card, Sym2, Finset.filter, Not, Membership.mem, Set, SimpleGraph.incidenceSet, Set.toFinset, SimpleGraph.edgeSet, HAdd.hAdd, id, congr, Nat.card, congrArg, Finset.sum_congr, Eq.refl, Finset, Eq.trans, SimpleGraph.deleteEdges and 52 more
90 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma sum_classEdgeCount_deck line 182 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, SimpleGraph, Finset, Eq, Nat, Multiset.sum, Multiset.map, Set, classEdgeCount, bipartiteDeck, Finset.sum, Finset.univ, edgeCount, SimpleGraph.deleteIncidenceSet
Proof uses: Multiset, Finset.val, id, Eq.mpr, setOf, Nonempty, BipartiteIso, Function.comp, congrArg, Multiset.map_map, Eq.rec, Eq.refl, funext, classEdgeCount_eq, Eq.symm, Finset.sum_eq_multiset_sum
2 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
lemma multiset_sum_eq line 197 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, SimpleGraph, Finset, Eq, Multiset, Set, bipartiteDeck, Nat, Multiset.sum, Multiset.map, classEdgeCount
Proof uses: Eq.mpr, id, congrArg, Eq.refl
2 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma bipartiteDeck_determines_edgeCount Recover the original number of edges from the deck line 203 source
L4DEL explanation
equation (2) shows that the deck determines e(K)
— Human-written graph-reconstruction proof companion
Equal bipartite decks of graphs on at least three vertices force equal total edge counts. Summing the edge counts of all cards counts each original edge once for every deleted vertex not incident to it, hence exactly n−2 times.
1. Each card's edge count is invariant under the bipartite isomorphism class stored in the deck.
2. Positivity of n−2 permits cancellation, turning equality of the card sums into edgeCount G = edgeCount H.
Sources and attribution: Pinned Lean source (0647711a7118), Human-written graph-reconstruction proof companion
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, Finset, SimpleGraph, GE.ge, Nat, Fintype.card, OfNat.ofNat, Eq, Multiset, Set, bipartiteDeck, edgeCount
Proof uses: Multiset.sum, Multiset.map, classEdgeCount, multiset_sum_eq, Finset.sum, Finset.univ, SimpleGraph.deleteIncidenceSet, sum_classEdgeCount_deck, HSub.hSub, HMul.hMul, sum_edgeCount_deleteIncidenceSet, SimpleGraph.Adj, GT.gt, Nat.sub_pos_of_lt, Eq.mpr, id, congrArg, Eq.symm, Nat.sub_mul, Eq.refl and 2 more
11 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
```
lemma bipartiteDeck_determines_edgeCount {G H : SimpleGraph V} (hV : Fintype.card V ≥ 3)
    (h : bipartiteDeck G leftU rightV = bipartiteDeck H leftU rightV) :
    edgeCount G = edgeCount H := by
…
```
Mentions: bipartiteDeck, edgeCount
def degreeMultiset The unlabeled multiset of all vertex degrees line 219 source
L4DEL explanation
the degree multisets of G and H are equal
— Human-written graph-reconstruction proof companion
degreeMultiset G lists the degree of every vertex of G while forgetting which vertex has which degree. This is the intermediate invariant reconstructed from the edge counts of the deck's cards.
1. Every vertex appears once through Finset.univ.
2. Using a multiset retains the multiplicity of each degree value.
Sources and attribution: Pinned Lean source (0647711a7118), Human-written graph-reconstruction proof companion
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, SimpleGraph, Multiset, Nat
Proof uses: Multiset.map, SimpleGraph.degree, SimpleGraph.Adj, Finset.val, Finset.univ
2 instances, coercions and auxiliary constants left out.
```
def degreeMultiset (G : SimpleGraph V) : Multiset ℕ :=
…
```
lemma deck_edgeCounts_eq line 222 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, Finset, SimpleGraph, Eq, Multiset, Set, bipartiteDeck, Nat, Multiset.map, edgeCount, SimpleGraph.deleteIncidenceSet, Finset.val, Finset.univ
Proof uses: classEdgeCount, id, Eq.mpr, setOf, Nonempty, BipartiteIso, Function.comp, congrArg, Multiset.map_map, Eq.rec, Eq.refl, funext, classEdgeCount_eq, Eq.symm

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
lemma degreeMultiset_eq_map_edgeCount line 242 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, SimpleGraph, DecidableRel, SimpleGraph.Adj, Eq, Multiset, Nat, degreeMultiset, Multiset.map, HSub.hSub, edgeCount, SimpleGraph.deleteIncidenceSet, Finset.val, Finset.univ
Proof uses: id, Eq.mpr, Finset.card, SimpleGraph.neighborFinset, Nat.card, Sym2, SimpleGraph.edgeSet, SimpleGraph.deleteEdges, SimpleGraph.incidenceSet, Finset.filter, Membership.mem, Set, And, Not, congr, congrArg, Multiset.map_congr, Eq.refl, Finset, SimpleGraph.neighborFinset_eq_filter and 59 more
48 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
lemma bipartiteDeck_determines_degreeMultiset Equal decks determine the complete degree distribution line 250 source
L4DEL explanation
equation (1) shows that the degree multisets of G and H are equal
— Human-written graph-reconstruction proof companion
Every type of proper subgraph which occurs in A or B
— Paul J. Kelly, A congruence theorem for trees (1957)
Once the original edge count and the multiset of card edge counts are known, the identity degree(v)=e(G)−e(Δv(G)) recovers the multiset of vertex degrees. Equal decks therefore give equal degree multisets.
1. The deck first determines edgeCount G = edgeCount H.
2. Mapping subtraction by that common edge count over the matched card counts yields identical degree multisets.
Sources and attribution: Pinned Lean source (0647711a7118), Human-written graph-reconstruction proof companion, Paul J. Kelly, A congruence theorem for trees (1957)
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, Finset, SimpleGraph, GE.ge, Nat, Fintype.card, OfNat.ofNat, DecidableRel, SimpleGraph.Adj, Eq, Multiset, Set, bipartiteDeck, degreeMultiset
Proof uses: Multiset.map, HSub.hSub, edgeCount, SimpleGraph.deleteIncidenceSet, Finset.val, Finset.univ, degreeMultiset_eq_map_edgeCount, bipartiteDeck_determines_edgeCount, deck_edgeCounts_eq, Eq.mpr, Function.comp, id, congrArg, Multiset.map_map, Function.comp_def, Eq.refl, Eq.symm
6 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
```
lemma bipartiteDeck_determines_degreeMultiset {G H : SimpleGraph V} (hV : Fintype.card V ≥ 3)
    [DecidableRel G.Adj] [DecidableRel H.Adj]
    (h : bipartiteDeck G leftU rightV = bipartiteDeck H leftU rightV) :
    degreeMultiset G = degreeMultiset H := by
…
```
Mentions: bipartiteDeck, degreeMultiset
lemma degreeMultiset_eq_of_bipartiteIso line 266 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, SimpleGraph, DecidableRel, SimpleGraph.Adj, Finset, BipartiteIso, Eq, Multiset, Nat, degreeMultiset
Proof uses: RelIso, Iff, Membership.mem, Equiv, RelIso.toEquiv, RelIso.mk, id, Eq.subst, Multiset.map, SimpleGraph.degree, Finset.val, Finset.univ, Function.comp, Eq.trans, Eq.symm, Multiset.map_map, congr_arg, Multiset.map_univ_val_equiv, Multiset.map_congr, rfl and 12 more
10 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma degree_deleteIncidenceSet line 275 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, SimpleGraph, DecidableRel, SimpleGraph.Adj, Eq, Nat, SimpleGraph.degree, SimpleGraph.deleteIncidenceSet, ite, OfNat.ofNat, HSub.hSub
Proof uses: Eq.mpr, Finset.card, Finset.filter, And, Not, Membership.mem, Sym2, Set, SimpleGraph.incidenceSet, Sym2.mk, Prod.mk, Finset.univ, id, congr, SimpleGraph.neighborFinset, congrArg, Finset, Eq.trans, SimpleGraph.neighborFinset_eq_filter, Finset.filter.congr_simp and 40 more
36 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma count_degreeMultiset line 282 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, SimpleGraph, DecidableRel, SimpleGraph.Adj, Nat, Eq, Multiset.count, degreeMultiset, Finset.card, Finset.filter, SimpleGraph.degree, Finset.univ
Proof uses: id, Eq.mpr, Multiset.countP, Multiset.map, SimpleGraph.neighborFinset, Finset.val, congrArg, Eq.trans, Multiset.card, Multiset.filter, Multiset.countP_congr, Multiset.map_congr, Eq.refl, Multiset, Membership.mem, Std.Symm, propext, comm, DecidablePred, Multiset.countP_map and 18 more
14 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma count_degreeMultiset_del line 289 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, SimpleGraph, DecidableRel, SimpleGraph.Adj, Nat, Eq, Multiset.count, degreeMultiset, SimpleGraph.deleteIncidenceSet, Finset.card, Finset.filter, SimpleGraph.degree, Finset.univ
Proof uses: id, Eq.mpr, Multiset.map, Finset.val, congrArg, Eq.trans, Multiset.card, Multiset.filter, Multiset, Multiset.count_map, Multiset.toFinset, DecidablePred, Eq.symm, Multiset.toFinset_card_of_nodup, Multiset.Nodup.filter, Finset.nodup, Finset, Multiset.toFinset_filter, Finset.filter.congr_simp, Eq.refl and 9 more
17 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma count_degreeProfile_eq line 296 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, SimpleGraph, DecidableRel, SimpleGraph.Adj, Nat, Eq, Multiset.count, degreeProfile, Finset.card, Finset.filter, SimpleGraph.degree, SimpleGraph.neighborFinset
Proof uses: id, Eq.mpr, Multiset.map, Finset.val, congrArg, Eq.trans, Multiset.card, Multiset.filter, Multiset, Multiset.count_map, Multiset.toFinset, DecidablePred, Finset, Eq.symm, Multiset.toFinset_card_of_nodup, Multiset.Nodup.filter, Finset.nodup, Multiset.toFinset_filter, Finset.filter.congr_simp, Eq.refl and 9 more
15 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma sum_indicator_eq line 303 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, SimpleGraph, DecidableRel, SimpleGraph.Adj, Nat, Eq, HAdd.hAdd, Finset.card, Finset.filter, SimpleGraph.degree, SimpleGraph.neighborFinset, SimpleGraph.deleteIncidenceSet, Finset.univ, ite, OfNat.ofNat
Proof uses: Eq.mpr, Finset.sum, Finset.erase, id, congr, congrArg, Eq.trans, Finset, Finset.filter.congr_simp, funext, SimpleGraph.neighborFinset_eq_filter, Finset.card_filter, AddCommMonoid, Eq.symm, Finset.sum_erase_add, Finset.mem_univ, Eq.refl, ite_congr, Not, Finset.sum_congr and 48 more
62 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
lemma count_degreeMultiset_deleteIncidenceSet_add The degree-count recurrence before and after deleting one incidence set line 317 source
L4DEL explanation
Counting vertices of degree k before and after deleting the incidence set of v gives
— Human-written graph-reconstruction proof companion
For each degree d, this identity balances four effects of isolating v: the new card counts, the isolated deleted vertex, neighbors dropping from degree d+1 to d, and the original global degree counts.
1. A non-neighbor keeps its degree, while a neighbor loses exactly one and v becomes degree zero.
2. Counting each case gives the recurrence used to reconstruct the neighbor-degree profile one degree at a time.
Sources and attribution: Pinned Lean source (0647711a7118), Human-written graph-reconstruction proof companion
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, SimpleGraph, DecidableRel, SimpleGraph.Adj, Nat, Eq, HAdd.hAdd, Multiset.count, degreeMultiset, SimpleGraph.deleteIncidenceSet, ite, SimpleGraph.degree, OfNat.ofNat, degreeProfile
Proof uses: Finset.card, Finset.filter, SimpleGraph.neighborFinset, count_degreeProfile_eq, Finset.univ, count_degreeMultiset_del, count_degreeMultiset, sum_indicator_eq, Decidable.byContradiction, Not
12 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
lemma count_degreeMultiset_deleteIncidenceSet_add {V : Type*} [Fintype V] [DecidableEq V]
  (G : SimpleGraph V) [DecidableRel G.Adj] (v : V) (d : ℕ) :
  Multiset.count d (degreeMultiset (G.deleteIncidenceSet v)) + (if G.degree v = d then 1 else 0) + Multiset.count d (degreeProfile G v) =
  (if d = 0 then 1 else 0) + Multiset.count (d + 1) (degreeProfile G v) + Multiset.count d (degreeMultiset G) := by
…
```
Mentions: degreeMultiset, degreeProfile
lemma eq_of_add_eq_add_succ line 328 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, HAdd.hAdd, OfNat.ofNat, Exists, GE.ge, And
Proof uses: Exists.elim, And.elim, by_contra, Not, absurd, False, Eq.rec, Nat.rec, Ne.symm, Nat.zero, mt, Nat.succ, Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt, Not.intro, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl, Int, Eq.mp, Neg.neg, HSub.hSub and 52 more
81 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma count_degreeProfile_eq_zero line 334 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, SimpleGraph, Nat, GE.ge, Fintype.card, Eq, Multiset.count, degreeProfile, OfNat.ofNat
Proof uses: Eq.mpr, Not, Membership.mem, Multiset, Multiset.map, SimpleGraph.degree, SimpleGraph.Adj, Finset.val, SimpleGraph.neighborFinset, id, Function.comp, LT.lt, False, LE.le.not_gt, LE.le, Eq.rec, Exists.choose, And, Iff.mp, Exists and 4 more
12 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma profile_eq_of_iso A matched card and global degrees determine the deleted vertex's degree profile line 340 source
L4DEL explanation
Induction on k in (8) gives
— Human-written graph-reconstruction proof companion
When matched deleted vertices have the same degree, their cards are bipartite-isomorphic, and the original graphs have equal degree multisets, the multisets of their neighbors' original degrees are equal.
1. The degree-count recurrence is written once for each graph; global counts, card counts, and the deleted-vertex indicator cancel across the two equations.
2. The remaining recurrence equates profile counts by induction in d, with eventual zero counts above the finite vertex bound.
Sources and attribution: Pinned Lean source (0647711a7118), Human-written graph-reconstruction proof companion
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, SimpleGraph, DecidableRel, SimpleGraph.Adj, Finset, Eq, Multiset, Nat, degreeMultiset, SimpleGraph.degree, BipartiteIso, SimpleGraph.deleteIncidenceSet, degreeProfile
Proof uses: degreeMultiset_eq_of_bipartiteIso, HAdd.hAdd, Multiset.count, OfNat.ofNat, ite, count_degreeMultiset_deleteIncidenceSet_add, Eq.mpr, id, congrArg, Eq.refl, Decidable.byContradiction, Not, Exists, GE.ge, And, Exists.intro, Fintype.card, And.intro, count_degreeProfile_eq_zero, eq_of_add_eq_add_succ and 2 more
9 instances, coercions and auxiliary constants left out.

Tactic trace: 27 steps
Open to load the checked before-and-after goal states.
```
lemma profile_eq_of_iso {G H : SimpleGraph V} [DecidableRel G.Adj] [DecidableRel H.Adj]
    (leftU rightV : Finset V)
    (h_degG_eq_degH : degreeMultiset G = degreeMultiset H)
    (v : V) (u : V)
    (h_deg_vu : G.degree v = H.degree u)
    (iso : BipartiteIso (G.deleteIncidenceSet v) (H.deleteIncidenceSet u) leftU rightV) :
    degreeProfile G v = degreeProfile H u := by
…
```
Mentions: degreeMultiset, u, BipartiteIso, degreeProfile
lemma unique_isolated_of_2_connected The deleted vertex is the unique isolated vertex of its card line 371 source
L4DEL explanation
has a unique isolated vertex, namely v
— Human-written graph-reconstruction proof companion
Under the development's 2-connectivity hypothesis and |V| ≥ 3, the incidence-deleted card at v has degree zero exactly at v. Every other vertex retains an edge to someone other than v.
1. Connectivity rules out degree zero in the original graph.
2. Connectivity after deleting any one vertex rules out a vertex whose only neighbor was v, so no other isolated point is created.
Sources and attribution: Pinned Lean source (0647711a7118), Human-written graph-reconstruction proof companion
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, SimpleGraph, And, SimpleGraph.Connected, setOf, Ne, SimpleGraph.induce, GE.ge, Nat, Fintype.card, OfNat.ofNat, Iff, Eq, SimpleGraph.degree, SimpleGraph.deleteIncidenceSet, SimpleGraph.Adj
Proof uses: Eq.mpr, Membership.mem, Sym2, Set, SimpleGraph.incidenceSet, Sym2.mk, Prod.mk, id, forall_congr, Finset.card, SimpleGraph.neighborFinset, SimpleGraph.deleteEdges, congrArg, Eq.trans, Finset, Finset.filter, Not, Finset.univ, EmptyCollection.emptyCollection, SimpleGraph.neighborFinset_eq_filter and 74 more
56 instances, coercions and auxiliary constants left out.

Tactic trace: 22 steps
Open to load the checked before-and-after goal states.
```
lemma unique_isolated_of_2_connected {V : Type*} [Fintype V] [DecidableEq V]
  (G : SimpleGraph V) (h2 : G.Connected ∧ ∀ v, (G.induce {x | x ≠ v}).Connected) (hV : Fintype.card V ≥ 3)
  (v : V) : ∀ x : V, (G.deleteIncidenceSet v).degree x = 0 ↔ x = v := by
…
```
lemma iso_maps_isolated line 387 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, SimpleGraph, Finset, BipartiteIso, Iff, Eq, Nat, SimpleGraph.degree, SimpleGraph.Adj, OfNat.ofNat, Equiv, RelIso.toEquiv, BipartiteIso.toRelIso
Proof uses: RelIso, Membership.mem, BipartiteIso.mk, RelIso.mk, Iff.mp, Function.comp, Finset.card, SimpleGraph.neighborFinset, Eq.trans, Eq.symm, Finset.card_equiv, of_eq_true, True, forall_congr, congr, congrArg, propext, iff_self, eq_true, True.intro and 3 more
16 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma f_preserves_partitions Card matching preserves the named left and right parts line 397 source
L4DEL explanation
Since φv preserves L and R, (6) implies that f preserves the two parts
— Human-written graph-reconstruction proof companion
The permutation matching deleted cards sends each vertex to a vertex in the same bipartition part. The key is that the deleted vertex is recognizable inside its card as the unique isolated vertex.
1. A bipartite card isomorphism preserves leftU and rightV by definition.
2. Uniqueness identifies its image of v with the matching permutation's f v, transferring both membership equivalences to f.
Sources and attribution: Pinned Lean source (0647711a7118), Human-written graph-reconstruction proof companion
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, SimpleGraph, Finset, And, SimpleGraph.Connected, setOf, Ne, SimpleGraph.induce, GE.ge, Nat, Fintype.card, OfNat.ofNat, Equiv, Nonempty, BipartiteIso, SimpleGraph.deleteIncidenceSet, Iff, Membership.mem
Proof uses: Classical.choice, Eq, RelIso.toEquiv, SimpleGraph.Adj, BipartiteIso.toRelIso, iso_maps_isolated, Eq.mpr, SimpleGraph.degree, eq_of_heq, HEq, Eq.refl, HEq.refl, Eq.symm, SimpleGraph.neighborSet, Lean.Meta.FastSubsingleton.elim, unique_isolated_of_2_connected, BipartiteIso.map_left, Eq.mp, congrArg, BipartiteIso.map_right and 1 more
20 instances, coercions and auxiliary constants left out.

Tactic trace: 29 steps
Open to load the checked before-and-after goal states.
```
lemma f_preserves_partitions {V : Type*} [Fintype V] [DecidableEq V]
  (G H : SimpleGraph V) (leftU rightV : Finset V)
  (hG_2_conn : G.Connected ∧ ∀ v, (G.induce {x | x ≠ v}).Connected)
  (hH_2_conn : H.Connected ∧ ∀ v, (H.induce {x | x ≠ v}).Connected)
  (hV : Fintype.card V ≥ 3)
  (f : V ≃ V)
  (hf_iso : ∀ v, Nonempty (BipartiteIso (G.deleteIncidenceSet v) (H.deleteIncidenceSet (f v)) leftU rightV)) :
  (∀ v, v ∈ leftU ↔ f v ∈ leftU) ∧ (∀ v, v ∈ rightV ↔ f v ∈ rightV) := by
…
```
Mentions: BipartiteIso
lemma connected_of_induce_connected line 427 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, SimpleGraph, GE.ge, Nat, Fintype.card, OfNat.ofNat, SimpleGraph.Connected, setOf, Ne, SimpleGraph.induce
Proof uses: Eq.mpr, Eq.refl, Iff.mpr, Exists, SimpleGraph.Reachable, SimpleGraph.connected_iff_exists_forall_reachable, Or.elim, IsEmpty, Nonempty, isEmpty_or_nonempty, False.elim, Eq.mp, False, Eq.trans, LE.le, congrArg, Fintype.card_eq_zero, Eq, connected_of_induce_connected.match_1, Exists.intro and 45 more
38 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
lemma unique_isolated_mapped line 436 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, SimpleGraph, DecidableRel, SimpleGraph.Adj, SimpleGraph.Iso, Iff, Eq, Nat, SimpleGraph.degree, OfNat.ofNat
Proof uses: Equiv, of_eq_true, RelIso.mk, Eq.trans, True, congrArg, Equiv.symm, Eq.symm, Iff.mp, Eq.rec, Finset.card_equiv, SimpleGraph.neighborFinset, Membership.mem, Finset, forall_congr, congr, propext, Equiv.apply_symm_apply, iff_self, eq_true and 3 more
13 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma deleteIncidenceSet_induce_connected line 444 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, SimpleGraph, SimpleGraph.Connected, setOf, Ne, SimpleGraph.induce, GE.ge, Nat, Fintype.card, OfNat.ofNat, SimpleGraph.Iso, SimpleGraph.deleteIncidenceSet, Eq, SimpleGraph.Adj
Proof uses: id, Eq.mpr, Not, Exists, Membership.mem, Set, SimpleGraph.Reachable, Subtype.mk, Eq.trans, Subtype, congrArg, funext, Eq.rec, SimpleGraph.deleteEdges, SimpleGraph.incidenceSet, Exists.elim, Eq.mp, deleteIncidenceSet_induce_connected.match_1, Exists.intro, RelIso and 59 more
32 instances, coercions and auxiliary constants left out.

Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
lemma H_is_2_connected Matched incidence-deleted cards transfer 2-connectivity to H line 462 source
L4DEL explanation
Since the degree multisets of G and H are equal, H also has minimum degree at least 2.
— Human-written graph-reconstruction proof companion
If every incidence-deleted card of G is graph-isomorphic to a matched card of H and G is 2-connected, then every vertex-deleted induced subgraph of H is connected and hence H itself is connected.
1. The unique isolated vertex forces each card isomorphism to send the deleted vertex of G to its matched vertex of H.
2. Restricting the card isomorphism away from those isolated vertices transfers connectivity of every induced deletion; with at least three vertices, those connected deletions imply connectivity of H.
Sources and attribution: Pinned Lean source (0647711a7118), Human-written graph-reconstruction proof companion
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, SimpleGraph, And, SimpleGraph.Connected, setOf, Ne, SimpleGraph.induce, GE.ge, Nat, Fintype.card, OfNat.ofNat, Equiv, Nonempty, SimpleGraph.Iso, SimpleGraph.deleteIncidenceSet
Proof uses: Equiv.symm, Classical.choice, Eq, Equiv.apply_symm_apply, Eq.mpr, id, congrArg, Eq.symm, Nonempty.intro, SimpleGraph.Adj, Iff, SimpleGraph.degree, Eq.refl, unique_isolated_of_2_connected, DecidableRel, Classical.decRel, ite, HSub.hSub, degree_deleteIncidenceSet, Eq.mp and 11 more
19 instances, coercions and auxiliary constants left out.

Tactic trace: 24 steps
Open to load the checked before-and-after goal states.
```
lemma H_is_2_connected {V : Type*} [Fintype V] [DecidableEq V]
  (G H : SimpleGraph V)
  (hG_2_conn : G.Connected ∧ ∀ v, (G.induce {x | x ≠ v}).Connected)
  (hV : Fintype.card V ≥ 3)
  (f : V ≃ V)
  (hf_iso : ∀ v, Nonempty (G.deleteIncidenceSet v ≃g H.deleteIncidenceSet (f v))) :
  H.Connected ∧ ∀ v, (H.induce {x | x ≠ v}).Connected := by
…
```
def typeDrop How a neighbor's type changes when one incident edge is removed line 494 source
L4DEL explanation
d −̇ 1 = max(d−1, 0) is truncated subtraction and M \ {a} means deletion of one occurrence
— Human-written graph-reconstruction proof companion
typeDrop t d lowers the type's degree coordinate by one using natural-number subtraction and erases one occurrence of d from its degree-profile multiset. It models deleting the edge to a vertex of degree d.
1. Only one degree occurrence is erased, matching one lost neighbor rather than all neighbors of that degree.
2. The proof applies this operation only to genuine neighbors, whose original degree is positive.
Sources and attribution: Pinned Lean source (0647711a7118), Human-written graph-reconstruction proof companion
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Prod, Nat, Multiset
Proof uses: Prod.mk, HSub.hSub, Prod.fst, OfNat.ofNat, Multiset.erase, Prod.snd
4 instances, coercions and auxiliary constants left out.
```
def typeDrop (t : ℕ × Multiset ℕ) (d : ℕ) : ℕ × Multiset ℕ :=
…
```
def rightV_types line 497 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, SimpleGraph, Finset, Multiset, Prod, Nat
Proof uses: Multiset.map, τ, Finset.val
lemma count_map_eq_card_filter line 501 source
standard axioms: Quot.sound, propext what this means
Statement uses: DecidableEq, Multiset, Eq, Nat, Multiset.count, Multiset.map, Multiset.card, Multiset.filter
Proof uses: Eq.mpr, id, congrArg, Multiset.count_map, of_eq_true, Eq.trans, True, Multiset.filter_congr, Membership.mem, Iff.of_eq, eq_self
4 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma multiset_eq_of_add_map_drop line 506 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, Multiset, Nat, GT.gt, OfNat.ofNat, LT.lt, Membership.mem, Eq, HAdd.hAdd, Multiset.map
Proof uses: Finset.sup, Union.union, Finset, Multiset.toFinset, LE.le, Finset.le_sup, Finset.mem_union_left, Iff.mpr, Multiset.mem_toFinset, Finset.mem_union_right, GE.ge, HSub.hSub, Multiset.count, Nat.recAux, Not, Eq.mpr, id, congrArg, Multiset.count_eq_zero, Eq.refl and 13 more
33 instances, coercions and auxiliary constants left out.

Tactic trace: 75 steps
Open to load the checked before-and-after goal states.
lemma tau_deleteIncidenceSet_rightV_proof line 568 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, SimpleGraph, Finset, SimpleGraph.IsBipartiteWith, Membership.mem, Eq, Prod, Nat, Multiset, τ, SimpleGraph.deleteIncidenceSet, ite, SimpleGraph.Adj, typeDrop, SimpleGraph.degree
Proof uses: Ne, Disjoint, Set, Or, And, Iff.mp, Not, Set.disjoint_left, Eq.mp, congrArg, id, dite, Prod.mk, degreeProfile, Eq.mpr, if_pos, Prod.ext, HSub.hSub, Prod.fst, OfNat.ofNat and 139 more
94 instances, coercions and auxiliary constants left out.

Tactic trace: 74 steps
Open to load the checked before-and-after goal states.
lemma rightV_types_deleteIncidenceSet_map line 621 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, SimpleGraph, Finset, SimpleGraph.IsBipartiteWith, Membership.mem, Eq, Multiset, Prod, Nat, rightV_types, SimpleGraph.deleteIncidenceSet, Multiset.map, ite, SimpleGraph.Adj, typeDrop, τ, SimpleGraph.degree, Finset.val
Proof uses: id, Multiset.map_congr, rfl, tau_deleteIncidenceSet_rightV_proof
11 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma rightV_val_eq_filter_add_sdiff line 632 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, SimpleGraph, Finset, Eq, Multiset, Finset.val, HAdd.hAdd, Finset.filter, SimpleGraph.Adj, SDiff.sdiff, SimpleGraph.neighborFinset
Proof uses: Not, Finset.ext, of_eq_true, Iff, Membership.mem, Eq.trans, And, True, congr, congrArg, iff_self, Eq.mpr, id, Eq.symm, Multiset.filter, Multiset.filter_add_not
15 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
def S_multiset line 641 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, SimpleGraph, Finset, Multiset, Prod, Nat
Proof uses: Multiset.map, τ, Finset.val, Finset.filter, Membership.mem, SimpleGraph.neighborFinset, SimpleGraph.Adj
4 instances, coercions and auxiliary constants left out.
def T_multiset line 644 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, SimpleGraph, Finset, Multiset, Prod, Nat
Proof uses: Multiset.map, τ, Finset.val, SDiff.sdiff, SimpleGraph.neighborFinset, SimpleGraph.Adj
3 instances, coercions and auxiliary constants left out.
lemma rightV_types_eq_S_add_T line 647 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, SimpleGraph, Finset, Eq, Multiset, Prod, Nat, rightV_types, HAdd.hAdd, S_multiset, T_multiset
Proof uses: id, Multiset.map, τ, Finset.val, Finset.filter, Membership.mem, SimpleGraph.neighborFinset, SimpleGraph.Adj, SDiff.sdiff, rightV_val_eq_filter_add_sdiff, Eq.mpr, congrArg, Multiset.map_add, HAdd, Eq.rec, Eq.refl, Finset.ext, of_eq_true, Iff, Eq.trans and 4 more
12 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
lemma rightV_types_del_eq Split the opposite side into changed neighbor types and unchanged non-neighbor types line 660 source
L4DEL explanation
if x is adjacent to u, then deleting the incidence set of u removes the edge ux
— Human-written graph-reconstruction proof companion
After deleting all edges incident to a left-side vertex u, every right-side neighbor has its type transformed by typeDrop, while every right-side non-neighbor keeps its original type. The equality records those two multisets separately.
1. Bipartiteness ensures deleting u's incidence set cannot otherwise alter a right-side vertex's degree profile.
2. Filtering the right part into neighbors and non-neighbors converts the pointwise type formula into a multiset sum.
Sources and attribution: Pinned Lean source (0647711a7118), Human-written graph-reconstruction proof companion
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, SimpleGraph, Finset, SimpleGraph.IsBipartiteWith, Membership.mem, Eq, Multiset, Prod, Nat, rightV_types, SimpleGraph.deleteIncidenceSet, HAdd.hAdd, Multiset.map, typeDrop, SimpleGraph.degree, SimpleGraph.Adj, S_multiset, T_multiset
Proof uses: ite, τ, Finset.val, rightV_types_deleteIncidenceSet_map, Eq.mpr, id, congrArg, Finset.filter, SimpleGraph.neighborFinset, Finset.ext, of_eq_true, Iff, Eq.trans, And, True, congr, iff_self, SDiff.sdiff, Not, Multiset.filter and 18 more
22 instances, coercions and auxiliary constants left out.

Tactic trace: 27 steps
Open to load the checked before-and-after goal states.
```
lemma rightV_types_del_eq {V : Type*} [Fintype V] [DecidableEq V]
  (G : SimpleGraph V) (leftU rightV : Finset V)
  (hBipartite : G.IsBipartiteWith leftU rightV)
  (u : V) (hu : u ∈ leftU) :
  rightV_types (G.deleteIncidenceSet u) rightV =
  Multiset.map (fun t => typeDrop t (G.degree u)) (S_multiset G rightV u) + T_multiset G rightV u := by
…
```
Mentions: u, rightV_types, typeDrop, S_multiset, T_multiset
lemma BipartiteIso_degree_eq line 700 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, SimpleGraph, Finset, BipartiteIso, Eq, Nat, SimpleGraph.degree, SimpleGraph.Adj, Equiv, RelIso.toEquiv, BipartiteIso.toRelIso
Proof uses: SimpleGraph.neighborFinset, Finset.map, Equiv.toEmbedding, Equiv.symm, Finset.ext, Eq.mpr, Iff, Membership.mem, Exists, And, id, congr, congrArg, Eq.trans, Function.Embedding, funext, Iff.intro, Exists.intro, And.intro, Iff.mpr and 8 more
17 instances, coercions and auxiliary constants left out.

Tactic trace: 25 steps
Open to load the checked before-and-after goal states.
lemma BipartiteIso_degreeProfile_eq line 724 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, SimpleGraph, Finset, BipartiteIso, Eq, Multiset, Nat, degreeProfile, Equiv, RelIso.toEquiv, SimpleGraph.Adj, BipartiteIso.toRelIso
Proof uses: id, Multiset.map, SimpleGraph.degree, Finset.val, SimpleGraph.neighborFinset, Multiset.map_congr, rfl, Membership.mem, BipartiteIso_degree_eq, Eq.mpr, congrArg, Eq.symm, Function.comp, Multiset.map_map, Finset.map, Equiv.toEmbedding, Equiv.symm, Finset.ext, Iff, Exists and 19 more
16 instances, coercions and auxiliary constants left out.

Tactic trace: 39 steps
Open to load the checked before-and-after goal states.
lemma tau_eq_of_iso line 764 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, SimpleGraph, Finset, BipartiteIso, Eq, Prod, Nat, Multiset, τ, Equiv, RelIso.toEquiv, SimpleGraph.Adj, BipartiteIso.toRelIso
Proof uses: id, SimpleGraph.degree, BipartiteIso_degree_eq, degreeProfile, BipartiteIso_degreeProfile_eq, Eq.mpr, Prod.mk, congrArg, Eq.refl
8 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma rightV_types_eq_of_bij line 773 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, SimpleGraph, Finset, Equiv, Eq, Prod, Nat, Multiset, τ, Iff, Membership.mem, rightV_types
Proof uses: id, Multiset.map, Finset.val, Multiset.map_congr, rfl, Eq.mpr, congrArg, Eq.symm, Function.comp, Multiset.map_map, Iff.mpr, Multiset.count, Multiset.ext, Multiset.card, Multiset.filter, count_map_eq_card_filter, dite, Equiv.symm, Eq.mp, Equiv.apply_symm_apply and 23 more
14 instances, coercions and auxiliary constants left out.

Tactic trace: 76 steps
Open to load the checked before-and-after goal states.
lemma rightV_types_eq_of_bipartiteIso line 849 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, SimpleGraph, Finset, BipartiteIso, Eq, Multiset, Prod, Nat, rightV_types
Proof uses: rightV_types_eq_of_bij, RelIso.toEquiv, SimpleGraph.Adj, BipartiteIso.toRelIso, tau_eq_of_iso, BipartiteIso.map_right

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma rightV_types_del_eq_of_iso line 858 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, SimpleGraph, Finset, BipartiteIso, SimpleGraph.deleteIncidenceSet, Eq, Multiset, Prod, Nat, rightV_types
Proof uses: rightV_types_eq_of_bipartiteIso

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma S_add_map_T_eq Matched cards give a cancellable equation for neighboring-type multisets line 867 source
L4DEL explanation
Taking the number of occurrences of an arbitrary type t in (13) gives
— Human-written graph-reconstruction proof companion
The global types on the opposite side and the local types in the matched deleted cards are equal. Decomposing both by adjacency yields the manuscript's balance equation between the two neighboring-type multisets and their type-dropped images.
1. S_multiset contains types of neighbors on the opposite side; T_multiset contains types of non-neighbors.
2. Equal global and deleted-card type multisets let the unchanged T terms cancel, leaving S_G + drop(S_H) = S_H + drop(S_G).
Sources and attribution: Pinned Lean source (0647711a7118), Human-written graph-reconstruction proof companion
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, SimpleGraph, Finset, SimpleGraph.IsBipartiteWith, Equiv, Nonempty, BipartiteIso, SimpleGraph.deleteIncidenceSet, Eq, Prod, Nat, Multiset, τ, Iff, Membership.mem, HAdd.hAdd, S_multiset, Multiset.map, typeDrop and 2 more
Proof uses: Classical.choice, rightV_types, rightV_types_del_eq_of_iso, T_multiset, rightV_types_del_eq, Iff.mp, congrArg, Prod.fst, rightV_types_eq_S_add_T, rightV_types_eq_of_bij, Trans.trans, Eq.trans, Mathlib.Tactic.Abel.term, OfNat.ofNat, Mathlib.Tactic.Abel.subst_into_add, Mathlib.Tactic.Abel.term_atom, Mathlib.Tactic.Abel.term_add_const, zero_add, Eq.symm, Mathlib.Tactic.Abel.const_add_term and 6 more
35 instances, coercions and auxiliary constants left out.

Tactic trace: 26 steps
Open to load the checked before-and-after goal states.
```
lemma S_add_map_T_eq {V : Type*} [Fintype V] [DecidableEq V]
  (G H : SimpleGraph V) (leftU rightV : Finset V)
  (hBipartiteG : G.IsBipartiteWith leftU rightV)
  (hBipartiteH : H.IsBipartiteWith leftU rightV)
  (f : V ≃ V)
  (hf_iso : ∀ v, Nonempty (BipartiteIso (G.deleteIncidenceSet v) (H.deleteIncidenceSet (f v)) leftU rightV))
  (hf_type : ∀ v, τ G v = τ H (f v))
  (hf_left : ∀ v, v ∈ leftU ↔ f v ∈ leftU)
  (hf_right : ∀ v, v ∈ rightV ↔ f v ∈ rightV)
  (u : V) (hu : u ∈ leftU) :
  S_multiset G rightV u + Multiset.map (fun t => typeDrop t (G.degree u)) (S_multiset H rightV (f u)) =
  S_multiset H rightV (f u) + Multiset.map (fun t => typeDrop t (G.degree u)) (S_multiset G rightV u) := by
…
```
Mentions: BipartiteIso, τ, u, S_multiset, typeDrop
lemma S_multiset_eq Descending degree induction recovers each neighboring-type multiset line 910 source
L4DEL explanation
equality of the type-profile counts can be proved by descending induction on the first coordinate of t
— Human-written graph-reconstruction proof companion
The balance equation involving S_G, S_H, and typeDrop forces S_G = S_H. Type dropping strictly lowers the first coordinate, so the equality can be solved from the highest degrees downward.
1. Degree-zero vertices have empty neighbor-type multisets and form the immediate base case.
2. Otherwise every type in either multiset has positive first coordinate; the generic multiset lemma cancels their strictly lower dropped images by descending induction.
Sources and attribution: Pinned Lean source (0647711a7118), Human-written graph-reconstruction proof companion
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, SimpleGraph, Finset, SimpleGraph.IsBipartiteWith, Equiv, Nonempty, BipartiteIso, SimpleGraph.deleteIncidenceSet, Eq, Prod, Nat, Multiset, τ, Iff, Membership.mem, S_multiset
Proof uses: HAdd.hAdd, Multiset.map, typeDrop, SimpleGraph.degree, SimpleGraph.Adj, S_add_map_T_eq, dite, OfNat.ofNat, EmptyCollection.emptyCollection, Eq.mpr, Not, id, Eq.trans, Multiset.filter, Finset.val, SimpleGraph.neighborFinset, forall_congr, implies_congr, Eq.refl, Iff.mpr and 32 more
36 instances, coercions and auxiliary constants left out.

Tactic trace: 40 steps
Open to load the checked before-and-after goal states.
```
lemma S_multiset_eq {V : Type*} [Fintype V] [DecidableEq V]
  (G H : SimpleGraph V) (leftU rightV : Finset V)
  (hBipartiteG : G.IsBipartiteWith leftU rightV)
  (hBipartiteH : H.IsBipartiteWith leftU rightV)
  (f : V ≃ V)
  (hf_iso : ∀ v, Nonempty (BipartiteIso (G.deleteIncidenceSet v) (H.deleteIncidenceSet (f v)) leftU rightV))
  (hf_type : ∀ v, τ G v = τ H (f v))
  (hf_left : ∀ v, v ∈ leftU ↔ f v ∈ leftU)
  (hf_right : ∀ v, v ∈ rightV ↔ f v ∈ rightV)
  (u : V) (hu : u ∈ leftU) :
  S_multiset G rightV u = S_multiset H rightV (f u) := by
…
```
Mentions: BipartiteIso, τ, u, S_multiset
def typeProfile The multiset of full vertex types around one vertex line 947 source
L4DEL explanation
The type profile of u is the multiset of the types of its neighbors
— Human-written graph-reconstruction proof companion
typeProfile G x maps the vertex-type invariant τ G over every neighbor of x. Compared with degreeProfile, it remembers both each neighbor's degree and that neighbor's own surrounding degree multiset.
1. The profile remains unlabeled: it records which types occur and with what multiplicity, not the identities of their carriers.
2. Equality of these profiles under the matching bijection is the last invariant needed before reconstructing adjacency.
Sources and attribution: Pinned Lean source (0647711a7118), Human-written graph-reconstruction proof companion
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, SimpleGraph, Multiset, Prod, Nat
Proof uses: Multiset.map, τ, Finset.val, SimpleGraph.neighborFinset, SimpleGraph.Adj
2 instances, coercions and auxiliary constants left out.
```
def typeProfile (G : SimpleGraph V) (x : V) : Multiset (ℕ × Multiset ℕ) :=
…
```
lemma typeProfile_eq_S line 950 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, SimpleGraph, Finset, SimpleGraph.IsBipartiteWith, Membership.mem, Eq, Multiset, Prod, Nat, typeProfile, S_multiset
Proof uses: Disjoint, Set, SimpleGraph.Adj, Or, And, SimpleGraph.IsBipartiteWith.mk, id, Eq.mpr, Multiset.map, τ, Finset.val, SimpleGraph.neighborFinset, Finset.filter, congrArg, Finset.filter_true_of_mem, Eq.mp, propext, SimpleGraph.mem_neighborFinset, Or.inl, Eq.trans and 13 more
32 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma typeProfile_eq_S_right line 959 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, SimpleGraph, Finset, SimpleGraph.IsBipartiteWith, Membership.mem, Eq, Multiset, Prod, Nat, typeProfile, S_multiset
Proof uses: id, Multiset.map, τ, Finset.val, SimpleGraph.neighborFinset, SimpleGraph.Adj, Finset.filter, Disjoint, Set, Or, And, SimpleGraph.IsBipartiteWith.mk, Eq.mpr, congrArg, Finset.filter_true_of_mem, by_contra, Not, False.elim, False, Eq.mp and 13 more
33 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma count_typeProfile_eq_one_iff_adj Distinct vertex types turn profile membership into adjacency line 968 source
L4DEL explanation
Since types are pairwise distinct, adjacency is determined by type profiles
— Human-written graph-reconstruction proof companion
If every vertex type in G is distinct, the type of y appears exactly once in the type profile of x precisely when x is adjacent to y. No other neighbor can impersonate y by carrying the same type.
1. Adjacency inserts y into x's neighbor set and therefore inserts τ G y into the mapped multiset.
2. Conversely, an occurrence comes from some neighbor with that type; pairwise distinctness identifies that neighbor with y.
Sources and attribution: Pinned Lean source (0647711a7118), Human-written graph-reconstruction proof companion
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, SimpleGraph, Ne, Prod, Nat, Multiset, τ, Iff, Eq, Multiset.count, typeProfile, OfNat.ofNat, SimpleGraph.Adj
Proof uses: id, Eq.mpr, Prod.mk, SimpleGraph.degree, degreeProfile, Multiset.map, Finset.val, SimpleGraph.neighborFinset, Multiset.card, Multiset.filter, congrArg, Eq.trans, Multiset.count_map, Multiset.filter_congr, Membership.mem, Iff.of_eq, propext, Function.Injective.eq_iff, Iff.mp, Not and 21 more
19 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
lemma count_typeProfile_eq_one_iff_adj {V : Type*} [Fintype V] [DecidableEq V]
  (G : SimpleGraph V)
  (h_distinct : ∀ x y : V, x ≠ y → τ G x ≠ τ G y)
  (x y : V) :
  Multiset.count (τ G y) (typeProfile G x) = 1 ↔ G.Adj x y := by
…
```
Mentions: τ, typeProfile
lemma adjacency_preserved_left Type and type-profile preservation force adjacency preservation from the left side line 978 source
L4DEL explanation
τK (b) ∈ TK (a)
— Human-written graph-reconstruction proof companion
For a left-part vertex x, equality of type profiles and pointwise preservation of τ show that y occurs as a neighbor of x exactly when f y occurs as a neighbor of f x.
1. Distinct types make τ G y a unique marker for y inside typeProfile G x.
2. Transporting that marker through the profile equality and the bijection gives the corresponding adjacency statement in H.
Sources and attribution: Pinned Lean source (0647711a7118), Human-written graph-reconstruction proof companion
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, SimpleGraph, Finset, Equiv, Ne, Prod, Nat, Multiset, τ, Eq, Membership.mem, typeProfile, Iff, SimpleGraph.Adj
Proof uses: by_contra, Not, absurd, False, id, Multiset.map, Finset.val, SimpleGraph.neighborFinset, Eq.mpr, Prod.mk, SimpleGraph.degree, degreeProfile, congr, congrArg, Multiset.map_congr, Eq.refl, Function.comp, Iff.intro, Exists.elim, And and 34 more
18 instances, coercions and auxiliary constants left out.

Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
```
lemma adjacency_preserved_left {V : Type*} [Fintype V] [DecidableEq V]
  (G H : SimpleGraph V) (leftU rightV : Finset V)
  (f : V ≃ V)
  (h_distinct : ∀ x y : V, x ≠ y → τ G x ≠ τ G y)
  (h_tau : ∀ v, τ G v = τ H (f v))
  (h_typeProfile : ∀ u, u ∈ leftU → typeProfile G u = typeProfile H (f u))
  (x y : V) (hx : x ∈ leftU) :
  G.Adj x y ↔ H.Adj (f x) (f y) := by
…
```
Mentions: τ, u, typeProfile
lemma type_preserving_bijection_is_iso Upgrade the card-matching bijection to a bipartite graph isomorphism line 994 source
L4DEL explanation
Thus f is a graph isomorphism
— Human-written graph-reconstruction proof companion
A vertex bijection that preserves both partition sides, all vertex types, and the matched incidence-deleted cards must preserve every edge. The proof packages that adjacency equivalence with the side-preservation witnesses as a BipartiteIso.
1. Neighboring-type multisets agree for left-side vertices, so adjacency from the left side is preserved.
2. Symmetry handles edges presented from the right, while bipartiteness rules out right-to-right pairs; the resulting relation isomorphism uses the original bijection f.
Sources and attribution: Pinned Lean source (0647711a7118), Human-written graph-reconstruction proof companion
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, SimpleGraph, Finset, SimpleGraph.IsBipartiteWith, Ne, Prod, Nat, Multiset, τ, And, SimpleGraph.Connected, setOf, SimpleGraph.induce, GE.ge, Fintype.card, OfNat.ofNat, Eq, Finset.univ, Union.union and 6 more
Proof uses: S_multiset, S_multiset_eq, typeProfile, Iff.mp, typeProfile_eq_S, Eq.mpr, id, congrArg, Eq.refl, SimpleGraph.Adj, adjacency_preserved_left, dite, Not, Finset.mem_univ, Or.resolve_left, Eq.mp, Or, propext, Finset.mem_union, SimpleGraph.adj_comm and 13 more
41 instances, coercions and auxiliary constants left out.

Tactic trace: 49 steps
Open to load the checked before-and-after goal states.
```
lemma type_preserving_bijection_is_iso {V : Type*} [Fintype V] [DecidableEq V]
  (G H : SimpleGraph V) (leftU rightV : Finset V)
  (hG_bipartite : G.IsBipartiteWith leftU rightV)
  (hH_bipartite : H.IsBipartiteWith leftU rightV)
  (hG_distinct : ∀ x y : V, x ≠ y → τ G x ≠ τ G y)
  (hG_2_conn : G.Connected ∧ ∀ v, (G.induce {x | x ≠ v}).Connected)
  (hV : Fintype.card V ≥ 3)
  (hV_parts : (univ : Finset V) = leftU ∪ rightV)
  (f : V ≃ V)
  (hf_iso : ∀ v, Nonempty (BipartiteIso (G.deleteIncidenceSet v) (H.deleteIncidenceSet (f v)) leftU rightV))
  (hf_type : ∀ v, τ G v = τ H (f v))
  (hf_left : ∀ v, v ∈ leftU ↔ f v ∈ leftU)
…
```
Mentions: τ, BipartiteIso
theorem Conjecture2 Reconstructing a typed bipartite graph from its incidence-deletion deck line 1069 source
Source comment
Let G = (U ⊔ V, E) be a finite simple bipartite graph with |U| = u, |V| = v, n = u + v ≥ 3. Assume: 1. G is 2-connected. 2. G is not a regular graph (the degree sequence is non-constant on U ⊔ V) 3. All vertex types are pairwise distinct Then deck(G) determines G uniquely up to bipartite isomorphism.
L4DEL explanation
If DB(G) = DB(H), then G and H are bipartite-isomorphic.
— Human-written graph-reconstruction proof companion
Every type of proper subgraph which occurs in A or B
— Paul J. Kelly, A congruence theorem for trees (1957)
every finite simple undirected graph on three or more vertices is determined, up to isomorphism, by its collection of vertex-deleted subgraphs
— J. A. Bondy and R. L. Hemminger, Graph reconstruction—a survey (1977)
Let G and H use the same finite bipartition. If G remains connected after deleting any vertex, its vertex types are pairwise distinct, and the two incidence-deletion decks agree, then a bijection preserving the two parts also preserves every edge. Thus the deck determines G up to bipartite isomorphism under these strong distinguishability hypotheses.
1. Equality of decks pairs every incidence-deleted card of G with a bipartite-isomorphic card of H.
2. From those paired cards the proof recovers degrees, degree profiles, vertex types, and then each vertex's multiset of neighbouring types.
3. Pairwise distinct vertex types make adjacency readable from the neighbouring-type multiset, so the card pairing extends to a bipartition-preserving graph isomorphism.
4. The Lean statement also accepts G_not_regular, but the proof term never uses it and the companion theorem does not assume non-regularity. It is therefore a redundant formal hypothesis, not part of the mathematical mechanism described here.
Sources and attribution: Pinned Lean source (0647711a7118), Human-written graph-reconstruction proof companion, Paul J. Kelly, A congruence theorem for trees (1957), J. A. Bondy and R. L. Hemminger, Graph reconstruction—a survey (1977)
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, SimpleGraph, Finset, SimpleGraph.IsBipartiteWith, GE.ge, Nat, Fintype.card, OfNat.ofNat, Eq, Finset.univ, Union.union, And, SimpleGraph.Connected, setOf, Ne, SimpleGraph.induce, Not, SimpleGraph.IsRegularOfDegree, SimpleGraph.Adj and 7 more
Proof uses: Exists, Equiv, SimpleGraph.deleteIncidenceSet, multiset_map_eq_implies_bij, Exists.intro, Membership.mem, Nonempty.intro, BipartiteIso.mk, RelIso, RelIso.refl, Iff, RelIso.toEquiv, Iff.intro, And.intro, Eq.rec, edgeCount, bipartiteDeck_determines_edgeCount, degreeMultiset, bipartiteDeck_determines_degreeMultiset, SimpleGraph.degree and 63 more
37 instances, coercions and auxiliary constants left out.

Tactic trace: 68 steps
Open to load the checked before-and-after goal states.
```
theorem Conjecture2
    -- G, H are finite simple bipartite graphs on at least 3 vertices.
  (V : Type*) [Fintype V] [DecidableEq V]
  (G H : SimpleGraph V) (leftU rightV : Finset V)
  (hGBipartite : G.IsBipartiteWith leftU rightV)
  (hHBipartite : H.IsBipartiteWith leftU rightV)
  (hV : Fintype.card V ≥ 3)
  (hV_parts : (univ : Finset V) = leftU ∪ rightV)
    -- G is 2-connected means G is connected, and the subgraph after removal of any vertex is still connected.
  (G_2_connected : G.Connected ∧ ∀ (v : V), (G.induce {x | x ≠ v}).Connected)
    -- G is not a regular graph
  (G_not_regular : ∀ d : ℕ, ¬ G.IsRegularOfDegree d)
…
```