Matching.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 10 curated AI-written annotations and 7190 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was 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 quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

6 declarations, 0 contain sorry, 0 declared as axioms

Imports (2)

Imported by 2 files

def SimpleGraph.matchingNumber matchingNumber G is the size of a maximum matching of G line 30 source
Source documentation
matchingNumber G is the size of a maximum matching of G.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, SimpleGraph, DecidableRel, SimpleGraph.Adj, Real
Proof uses: Set, SimpleGraph.Subgraph, Set.ofPred, SimpleGraph.Subgraph.IsMatching, SupSet.sSup, Set.image, Finset.card, Sym2, Set.toFinset, SimpleGraph.Subgraph.edgeSet, Membership.mem, Classical.propDecidable
6 instances, coercions and auxiliary constants left out.
```
noncomputable def matchingNumber (G : SimpleGraph α) [DecidableRel G.Adj] : ℝ :=
…
```
def SimpleGraph.IsEdgeMatching A finite set of edges M is a matching of G if every element of M is an edge of G and any two edges of M are equal or share no vertex (no vertex is covered twice) line 37 source
Source documentation
A finite set of edges M is a matching of G if every element of M is an edge of G and any two edges of M are equal or share no vertex (no vertex is covered twice).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: SimpleGraph, Finset, Sym2
Proof uses: And, Membership.mem, Set, SimpleGraph.edgeSet, Or, Eq, Not
4 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
def IsEdgeMatching (G : SimpleGraph α) (M : Finset (Sym2 α)) : Prop :=
…
```
instance SimpleGraph.(instance at line 41) line 41 source
def SimpleGraph.IsMaximalEdgeMatching A matching M of G is maximal if no further edge of G can be added to M while keeping the matching property line 47 source
Source documentation
A matching M of G is maximal if no further edge of G can be added to M while keeping the matching property.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, SimpleGraph, Finset, Sym2
Proof uses: And, SimpleGraph.IsEdgeMatching, Membership.mem, Set, SimpleGraph.edgeSet, Not, Insert.insert
5 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
def IsMaximalEdgeMatching (G : SimpleGraph α) (M : Finset (Sym2 α)) : Prop :=
…
```
instance SimpleGraph.(instance at line 51) line 51 source
theorem SimpleGraph.matching_card_bound Documented declaration: matching_card_bound line 57 source
Source documentation
In a finite graph, twice the number of edges of any matching is at most the number of vertices: each edge contributes two distinct vertices, and a matching's edges are vertex-disjoint.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, SimpleGraph, SimpleGraph.Subgraph, Sym2, SimpleGraph.Subgraph.edgeSet, SimpleGraph.Subgraph.IsMatching, LE.le, Nat, HMul.hMul, OfNat.ofNat, Finset.card, Set.toFinset, Fintype.card
Proof uses: Membership.mem, Finset, Ne, Disjoint, Sym2.toFinset, Eq.mpr, Not, id, Eq, congrArg, propext, Finset.disjoint_left, Sym2.mk, Exists, False, Iff.mp, Sym2.mem_iff_exists, Eq.mp, Sym2.mem_toFinset, Set and 23 more
27 instances, coercions and auxiliary constants left out.

Tactic trace: 20 steps
Open to load the checked before-and-after goal states.
```
theorem matching_card_bound (G : SimpleGraph α) (M : Subgraph G) [Fintype ↥M.edgeSet]
    (h : M.IsMatching) : 2 * M.edgeSet.toFinset.card ≤ Fintype.card α := by
…
```