Compfiles/Usa1985P4.lean

GitHub source file

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

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 compfiles documentation, Pinned compfiles corpus index

12 declarations, 0 contain sorry, 0 declared as axioms

USA Mathematical Olympiad 1985, Problem 4

A graph has n > 2 points. Show that we can find two points A and B such that at least ⌊n/2⌋ - 1 of the remaining points are joined to either both or neither of A and B.

Imports (8)
Imported by 1 file
  1. def Usa1985P4.mixedRel mixedRel n G X p says that the vertex X is distinct from the two endpoints of the pair p and is adjacent to exactly one of them line 38 source

    Source documentation

    mixedRel n G X p says that the vertex X is distinct from the two endpoints of the pair p and is adjacent to exactly one of them.

    no axioms what this means

    Statement uses: Nat, SimpleGraph, Fin, DecidableRel, SimpleGraph.Adj, Prod

    Proof uses: And, Ne, Prod.fst, Prod.snd, Or, Not

    Tactic trace: 2 steps

    Open to load the checked before-and-after goal states.

    def mixedRel (n : ℕ) (G : SimpleGraph (Fin n)) [DecidableRel G.Adj] (X : Fin n)
    (p : Fin n × Fin n) : Prop :=
…
  2. instance Usa1985P4.(instance at line 42) line 42 source
  3. def Usa1985P4.badPair The "bad" vertices for a pair p: the remaining vertices that are joined to exactly one of the two endpoints of p line 49 source

    Source documentation

    The "bad" vertices for a pair p: the remaining vertices that are joined to exactly one of the two endpoints of p.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Nat, SimpleGraph, Fin, DecidableRel, SimpleGraph.Adj, Prod, Finset

    Proof uses: Finset.filter, Usa1985P4.mixedRel, Finset.univ

    2 instances, coercions and auxiliary constants left out.

    def badPair (n : ℕ) (G : SimpleGraph (Fin n)) [DecidableRel G.Adj] (p : Fin n × Fin n) :
    Finset (Fin n) :=
…
  4. lemma Usa1985P4.badPair_eq_bipartiteBelow line 53 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Nat, SimpleGraph, Fin, DecidableRel, SimpleGraph.Adj, Prod, Eq, Finset, Usa1985P4.badPair, Finset.bipartiteBelow, Usa1985P4.mixedRel, Finset.univ

    Proof uses: rfl

    2 instances, coercions and auxiliary constants left out.

  5. lemma Usa1985P4.neighborFinset_subset_erase The neighbourhood of X does not contain X line 58 source

    Source documentation

    The neighbourhood of X does not contain X.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Nat, SimpleGraph, Fin, DecidableRel, SimpleGraph.Adj, LE.le, Finset, SimpleGraph.neighborFinset, Membership.mem, Set, SimpleGraph.neighborSet, Finset.erase, Finset.univ

    Proof uses: Iff.mpr, And, Ne, Finset.mem_erase, And.intro, Ne.symm, SimpleGraph.Adj.ne, Eq.mp, congrArg, propext, SimpleGraph.mem_neighborFinset, Finset.mem_univ

    15 instances, coercions and auxiliary constants left out.

    Tactic trace: 3 steps

    Open to load the checked before-and-after goal states.

    lemma neighborFinset_subset_erase (n : ℕ) (G : SimpleGraph (Fin n)) [DecidableRel G.Adj]
    (X : Fin n) : G.neighborFinset X ⊆ Finset.univ.erase X := by
…
  6. lemma Usa1985P4.degree_le The degree of a vertex is at most n - 1 line 65 source

    Source documentation

    The degree of a vertex is at most n - 1.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Nat, SimpleGraph, Fin, DecidableRel, SimpleGraph.Adj, LE.le, SimpleGraph.degree, Membership.mem, Set, SimpleGraph.neighborSet, HSub.hSub, OfNat.ofNat

    Proof uses: Finset.card, SimpleGraph.neighborFinset, Finset.erase, Finset.univ, Finset.card_le_card, Usa1985P4.neighborFinset_subset_erase, Eq.mp, congrArg, SimpleGraph.card_neighborFinset_eq_degree, Fintype.card, Fintype.card_fin, Finset.card_univ, Finset.card_erase_of_mem, Finset.mem_univ

    17 instances, coercions and auxiliary constants left out.

    Tactic trace: 3 steps

    Open to load the checked before-and-after goal states.

    lemma degree_le (n : ℕ) (G : SimpleGraph (Fin n)) [DecidableRel G.Adj] (X : Fin n) :
    G.degree X ≤ n - 1 := by
…
  7. lemma Usa1985P4.fiber_card Documented declaration: fiber_card line 76 source

    Source documentation

    For a fixed vertex X, the number of ordered pairs (Y, Z) with Y ≠ Z such that X is joined to exactly one of Y and Z equals 2 * (d * (n - 1 - d)), where d = G.degree X: choose which endpoint is adjacent to X, then choose that endpoint (a neighbour of X) and the other one (a non-neighbour different from X).

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Nat, SimpleGraph, Fin, DecidableRel, SimpleGraph.Adj, Eq, Finset.card, Prod, Finset.bipartiteAbove, Usa1985P4.mixedRel, Finset.offDiag, Finset.univ, HMul.hMul, OfNat.ofNat, SimpleGraph.degree, Membership.mem, Set, SimpleGraph.neighborSet, HSub.hSub

    Proof uses: Iff, Or, And, Ne, Prod.snd, Prod.fst, Not, id, Prod.mk, Iff.intro, Or.inl, And.intro, Or.inr, SimpleGraph.Adj.ne, Finset, Union.union, Finset.filter, Eq.mpr, congrArg, rfl and 58 more

    60 instances, coercions and auxiliary constants left out.

    Tactic trace: 50 steps

    Open to load the checked before-and-after goal states.

    lemma fiber_card (n : ℕ) (G : SimpleGraph (Fin n)) [DecidableRel G.Adj] (X : Fin n) :
    ((Finset.offDiag Finset.univ).bipartiteAbove (mixedRel n G) X).card =
      2 * (G.degree X * (n - 1 - G.degree X)) := by
…

    Mentions: Usa1985P4.mixedRel

  8. lemma Usa1985P4.double_count Double counting: summing the number of bad vertices over all ordered pairs (Y, Z) with Y ≠ Z equals the sum over vertices X of 2 * (d_X * (n - 1 - d_X)) line 150 source

    Source documentation

    Double counting: summing the number of bad vertices over all ordered pairs (Y, Z) with Y ≠ Z equals the sum over vertices X of 2 * (d_X * (n - 1 - d_X)).

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Nat, SimpleGraph, Fin, DecidableRel, SimpleGraph.Adj, Eq, Finset.sum, Prod, Finset.offDiag, Finset.univ, Finset.card, Usa1985P4.badPair, HMul.hMul, OfNat.ofNat, SimpleGraph.degree, Membership.mem, Set, SimpleGraph.neighborSet, HSub.hSub

    Proof uses: Trans.trans, Finset.bipartiteAbove, Usa1985P4.mixedRel, id, Eq.symm, Finset.bipartiteBelow, Finset.sum_card_bipartiteAbove_eq_sum_card_bipartiteBelow, Finset.sum_congr, rfl, Finset, Usa1985P4.fiber_card

    24 instances, coercions and auxiliary constants left out.

    Tactic trace: 3 steps

    Open to load the checked before-and-after goal states.

    lemma double_count (n : ℕ) (G : SimpleGraph (Fin n)) [DecidableRel G.Adj] :
    (∑ p ∈ Finset.offDiag (Finset.univ : Finset (Fin n)), (badPair n G p).card) =
      ∑ X : Fin n, 2 * (G.degree X * (n - 1 - G.degree X)) := by
…

    Mentions: Usa1985P4.badPair

  9. lemma Usa1985P4.two_mul_sum_badPair_le Twice the total number of bad incidences is at most n * (n - 1)^2, since for each vertex X of degree d we have 4 * d * (n - 1 - d) ≤ (n - 1)^2 (AM-GM) line 164 source

    Source documentation

    Twice the total number of bad incidences is at most n * (n - 1)^2, since for each vertex X of degree d we have 4 * d * (n - 1 - d) ≤ (n - 1)^2 (AM-GM).

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Nat, SimpleGraph, Fin, DecidableRel, SimpleGraph.Adj, LE.le, HMul.hMul, OfNat.ofNat, Finset.sum, Prod, Finset.offDiag, Finset.univ, Finset.card, Usa1985P4.badPair, HPow.hPow, HSub.hSub

    Proof uses: Eq.mpr, SimpleGraph.degree, Membership.mem, Set, SimpleGraph.neighborSet, id, Eq, congrArg, Usa1985P4.double_count, Finset.mul_sum, Trans.trans, Finset.sum_le_sum, Finset, Usa1985P4.degree_le, HAdd.hAdd, four_mul_le_sq_add, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.cast_pos and 25 more

    78 instances, coercions and auxiliary constants left out.

    Tactic trace: 12 steps

    Open to load the checked before-and-after goal states.

    lemma two_mul_sum_badPair_le (n : ℕ) (G : SimpleGraph (Fin n)) [DecidableRel G.Adj] :
    2 * (∑ p ∈ Finset.offDiag (Finset.univ : Finset (Fin n)), (badPair n G p).card) ≤
      n * (n - 1)^2 := by
…

    Mentions: Usa1985P4.badPair

  10. lemma Usa1985P4.exists_pair_le Averaging: some ordered pair (A, B) with A ≠ B has at most ⌊(n - 1)/2⌋ bad remaining vertices line 184 source

    Source documentation

    Averaging: some ordered pair (A, B) with A ≠ B has at most ⌊(n - 1)/2⌋ bad remaining vertices.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Nat, LT.lt, OfNat.ofNat, SimpleGraph, Fin, DecidableRel, SimpleGraph.Adj, Exists, Prod, And, Membership.mem, Finset, Finset.offDiag, Finset.univ, LE.le, Finset.card, Usa1985P4.badPair, HDiv.hDiv, HSub.hSub

    Proof uses: Decidable.byContradiction, Not, Finset.sum, HAdd.hAdd, Finset.sum_le_sum, Iff.mpr, Nat.succ, Nat.succ_le_iff, Eq.mp, Eq.trans, binderNameHint, forall_congr, Mathlib.Tactic.Push.not_and_eq, implies_congr, Eq.refl, HMul.hMul, HPow.hPow, Nat.mul_pos, Eq, Eq.mpr and 43 more

    90 instances, coercions and auxiliary constants left out.

    Tactic trace: 27 steps

    Open to load the checked before-and-after goal states.

    lemma exists_pair_le (n : ℕ) (hn : 2 < n) (G : SimpleGraph (Fin n)) [DecidableRel G.Adj] :
    ∃ p ∈ Finset.offDiag (Finset.univ : Finset (Fin n)),
      (badPair n G p).card ≤ (n - 1) / 2 := by
…

    Mentions: Usa1985P4.badPair

  11. lemma Usa1985P4.answer_card The vertices joined to both or neither endpoint of p are the remaining vertices that are not bad; there are (n - 2) - (#bad) of them line 216 source

    Source documentation

    The vertices joined to both or neither endpoint of p are the remaining vertices that are not bad; there are (n - 2) - (#bad) of them.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Nat, SimpleGraph, Fin, DecidableRel, SimpleGraph.Adj, Prod, Membership.mem, Finset, Finset.offDiag, Finset.univ, Eq, Finset.card, Finset.filter, And, Ne, Prod.fst, Prod.snd, Iff, HSub.hSub, OfNat.ofNat and 1 more

    Proof uses: SDiff.sdiff, Finset.ext, Eq.mpr, Not, Usa1985P4.mixedRel, id, congr, congrArg, Eq.trans, True, congrFun', true_and, Or, Usa1985P4.mixedRel.eq_1, Iff.intro, And.intro, False, Iff.mp, Decidable.iff_iff_and_or_not_and_not, False.elim and 20 more

    33 instances, coercions and auxiliary constants left out.

    Tactic trace: 20 steps

    Open to load the checked before-and-after goal states.

    lemma answer_card (n : ℕ) (G : SimpleGraph (Fin n)) [DecidableRel G.Adj] (p : Fin n × Fin n)
    (hp : p ∈ Finset.offDiag (Finset.univ : Finset (Fin n))) :
    (Finset.univ.filter fun X => X ≠ p.1 ∧ X ≠ p.2 ∧ (G.Adj X p.1 ↔ G.Adj X p.2)).card =
      (n - 2) - (badPair n G p).card := by
…

    Mentions: Usa1985P4.badPair

  12. problem Usa1985P4.usa1985_p4 line 248 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Nat, LT.lt, OfNat.ofNat, SimpleGraph, Fin, DecidableRel, SimpleGraph.Adj, Exists, And, Ne, LE.le, HSub.hSub, HDiv.hDiv, Finset.card, Finset.filter, Iff, Eq, Finset.univ

    Proof uses: Prod, Membership.mem, Finset, Finset.offDiag, Usa1985P4.badPair, Usa1985P4.exists_pair_le, Exists.intro, Prod.fst, Prod.snd, And.intro, And.right, Iff.mp, Finset.mem_offDiag, Eq.mpr, id, congrArg, Usa1985P4.answer_card

    29 instances, coercions and auxiliary constants left out.

    Tactic trace: 4 steps

    Open to load the checked before-and-after goal states.