`Compfiles/Usa2008P6.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 8 curated AI-written annotations and 3305 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 compfiles documentation, Pinned compfiles corpus index

20 declarations, 0 contain sorry, 0 declared as axioms

USA Mathematical Olympiad 2008, Problem 6

At a certain mathematical conference, every pair of mathematicians are either friends or strangers. At mealtime, every participant eats in one of two large dining rooms. Each mathematician insists upon eating in a room which contains an even number of his or her friends. Prove that the number of ways that the mathematicians may be split between the two rooms is a power of two (i.e., is of the form 2^k for some positive integer k).

Imports (5)

Imported by 1 file

Compfiles.lean

def Usa2008P6.lap The Laplacian of the friendship graph as a ZMod 2-linear map: (lap G x) v = deg(v) * x v + ∑_{u ∼ v} x u line 58 source
Source documentation
The Laplacian of the friendship graph as a ZMod 2-linear map: (lap G x) v = deg(v) * x v + ∑_{u ∼ v} x u.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, SimpleGraph, Fin, DecidableRel, SimpleGraph.Adj, LinearMap, ZMod, OfNat.ofNat, RingHom.id
Proof uses: LinearMap.mk, AddHom.mk, HAdd.hAdd, HMul.hMul, SimpleGraph.degree, Membership.mem, Set, SimpleGraph.neighborSet, Finset.sum, SimpleGraph.neighborFinset
42 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
def lap : (Fin n → ZMod 2) →ₗ[ZMod 2] (Fin n → ZMod 2) where
…
```
lemma Usa2008P6.lap_apply line 69 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, SimpleGraph, Fin, DecidableRel, SimpleGraph.Adj, ZMod, OfNat.ofNat, Eq, LinearMap, RingHom.id, Usa2008P6.lap, HAdd.hAdd, HMul.hMul, SimpleGraph.degree, Membership.mem, Set, SimpleGraph.neighborSet, Finset.sum, SimpleGraph.neighborFinset
Proof uses: rfl
41 instances, coercions and auxiliary constants left out.
def Usa2008P6.degVec The degree vector, modulo 2 line 73 source
Source documentation
The degree vector, modulo 2.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, SimpleGraph, Fin, DecidableRel, SimpleGraph.Adj, ZMod, OfNat.ofNat
Proof uses: SimpleGraph.degree, Membership.mem, Set, SimpleGraph.neighborSet
14 instances, coercions and auxiliary constants left out.
```
def degVec : Fin n → ZMod 2 := fun v => (G.degree v : ZMod 2)
```
lemma Usa2008P6.ite_eq_one_add In ZMod 2 the indicator of a = b equals 1 + a + b line 76 source
Source documentation
In ZMod 2 the indicator of a = b equals 1 + a + b.
```
private lemma ite_eq_one_add :
    ∀ a b : ZMod 2, (if a = b then (1 : ZMod 2) else 0) = 1 + a + b := by decide
```
lemma Usa2008P6.mul_self_eq line 79 source
lemma Usa2008P6.even_card_filter_iff The combinatorial condition "an even number of friends share the room of v" is the linear equation (lap G x) v = deg(v) in ZMod 2 line 83 source
Source documentation
The combinatorial condition "an even number of friends share the room of v" is the linear equation (lap G x) v = deg(v) in ZMod 2.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, SimpleGraph, Fin, DecidableRel, SimpleGraph.Adj, ZMod, OfNat.ofNat, Iff, Even, Finset.card, Finset.filter, Eq, SimpleGraph.neighborFinset, Membership.mem, Set, SimpleGraph.neighborSet, LinearMap, RingHom.id, Usa2008P6.lap, SimpleGraph.degree
Proof uses: Finset.sum, HAdd.hAdd, Eq.mpr, ite, id, congrArg, Finset.card_filter, congrFun', Eq.trans, Nat.cast_sum, Finset.sum_congr, Eq.refl, Finset, Nat.cast_ite, ite_congr, Nat.cast_one, Not, Nat.cast_zero, rfl, Eq.symm and 15 more
97 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
```
lemma even_card_filter_iff (x : Fin n → ZMod 2) (v : Fin n) :
    Even ((G.neighborFinset v).filter fun u => x u = x v).card ↔
      lap G x v = (G.degree v : ZMod 2) := by
…
```
Mentions: Usa2008P6.lap
lemma Usa2008P6.sum_neighbor_mul_comm Swapping the order of summation over ordered pairs of adjacent vertices line 105 source
Source documentation
Swapping the order of summation over ordered pairs of adjacent vertices.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, SimpleGraph, Fin, DecidableRel, SimpleGraph.Adj, ZMod, OfNat.ofNat, Eq, Finset.sum, Finset.univ, SimpleGraph.neighborFinset, Membership.mem, Set, SimpleGraph.neighborSet, HMul.hMul
Proof uses: ite, Eq.mpr, Finset.filter, id, congrArg, Finset, SimpleGraph.neighborFinset_eq_filter, Finset.sum_filter, Eq.refl, Trans.simple, Finset.sum_congr, rfl, Finset.sum_comm, dite, ite_eq_left, SimpleGraph.Adj.symm, Not, ite_eq_right, Eq.symm
38 instances, coercions and auxiliary constants left out.

Tactic trace: 19 steps
Open to load the checked before-and-after goal states.
```
lemma sum_neighbor_mul_comm (x y : Fin n → ZMod 2) :
    ∑ v, ∑ u ∈ G.neighborFinset v, x u * y v
      = ∑ v, ∑ u ∈ G.neighborFinset v, x v * y u := by
…
```
lemma Usa2008P6.lap_inner The Laplacian is symmetric with respect to the dot product line 126 source
Source documentation
The Laplacian is symmetric with respect to the dot product.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, SimpleGraph, Fin, DecidableRel, SimpleGraph.Adj, ZMod, OfNat.ofNat, Eq, Finset.sum, Finset.univ, HMul.hMul, LinearMap, RingHom.id, Usa2008P6.lap
Proof uses: HAdd.hAdd, SimpleGraph.degree, Membership.mem, Set, SimpleGraph.neighborSet, SimpleGraph.neighborFinset, Eq.mpr, id, congrArg, Usa2008P6.lap_apply, add_mul, Finset.sum_mul, Eq.refl, mul_add, Finset.mul_sum, Finset.sum_congr, rfl, Finset, Finset.sum_add_distrib, Usa2008P6.sum_neighbor_mul_comm and 18 more
70 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
```
lemma lap_inner (x y : Fin n → ZMod 2) :
    ∑ v, lap G x v * y v = ∑ v, x v * lap G y v := by
…
```
Mentions: Usa2008P6.lap
lemma Usa2008P6.inner_self_lap The key identity: xᵀ (L x) = ∑ v, deg(v) * x v over ZMod 2 line 143 source
Source documentation
The key identity: xᵀ (L x) = ∑ v, deg(v) * x v over ZMod 2. The cross terms cancel because each edge is counted twice.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, SimpleGraph, Fin, DecidableRel, SimpleGraph.Adj, ZMod, OfNat.ofNat, Eq, Finset.sum, Finset.univ, HMul.hMul, LinearMap, RingHom.id, Usa2008P6.lap, SimpleGraph.degree, Membership.mem, Set, SimpleGraph.neighborSet
Proof uses: HAdd.hAdd, SimpleGraph.neighborFinset, Eq.mpr, id, congrArg, Usa2008P6.lap_apply, mul_add, Finset.mul_sum, HAdd, Eq.rec, Eq.refl, mul_comm, mul_assoc, Finset.sum_congr, rfl, Finset, Finset.sum_add_distrib, Prod, Finset.filter, Prod.fst and 22 more
86 instances, coercions and auxiliary constants left out.

Tactic trace: 33 steps
Open to load the checked before-and-after goal states.
```
lemma inner_self_lap (x : Fin n → ZMod 2) :
    ∑ v, x v * lap G x v = ∑ v, (G.degree v : ZMod 2) * x v := by
…
```
Mentions: Usa2008P6.lap
def Usa2008P6.Tmap Pairing with d, restricted to the kernel of lap G, as a linear map into the dual of the kernel line 179 source
Source documentation
Pairing with d, restricted to the kernel of lap G, as a linear map into the dual of the kernel.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, SimpleGraph, Fin, DecidableRel, SimpleGraph.Adj, LinearMap, ZMod, OfNat.ofNat, RingHom.id, Module.Dual, Subtype, Membership.mem, Submodule, LinearMap.ker, Usa2008P6.lap
Proof uses: LinearMap.mk₂, Finset.sum, Finset.univ, HMul.hMul
59 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
```
def Tmap : (Fin n → ZMod 2) →ₗ[ZMod 2] Module.Dual (ZMod 2) ↥(LinearMap.ker (lap G)) :=
…
```
Mentions: Usa2008P6.lap
lemma Usa2008P6.Tmap_apply line 192 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, SimpleGraph, Fin, DecidableRel, SimpleGraph.Adj, ZMod, OfNat.ofNat, Subtype, Membership.mem, Submodule, LinearMap.ker, RingHom.id, Usa2008P6.lap, Eq, Module.Dual, LinearMap, Usa2008P6.Tmap, Finset.sum, Finset.univ, HMul.hMul
Proof uses: rfl
63 instances, coercions and auxiliary constants left out.
lemma Usa2008P6.mem_ker_Tmap line 195 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, SimpleGraph, Fin, DecidableRel, SimpleGraph.Adj, ZMod, OfNat.ofNat, Iff, Membership.mem, Submodule, LinearMap.ker, Module.Dual, Subtype, RingHom.id, Usa2008P6.lap, Usa2008P6.Tmap, Eq, LinearMap
Proof uses: Eq.mpr, id, congrArg, propext, LinearMap.mem_ker, LinearMap.ext_iff, forall_congr', LinearMap.zero_apply, Iff.rfl
69 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Usa2008P6.range_lap_le_ker_Tmap The range of lap G is contained in the "orthogonal complement" of its kernel line 201 source
Source documentation
The range of lap G is contained in the "orthogonal complement" of its kernel.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, SimpleGraph, Fin, DecidableRel, SimpleGraph.Adj, LE.le, Submodule, ZMod, OfNat.ofNat, LinearMap.range, RingHom.id, Usa2008P6.lap, LinearMap.ker, Module.Dual, Subtype, Membership.mem, Usa2008P6.Tmap
Proof uses: Eq, LinearMap, HEq, Eq.refl, Eq.mpr, id, congrArg, propext, Usa2008P6.mem_ker_Tmap, Subtype.mk, Finset.sum, Finset.univ, HMul.hMul, Usa2008P6.Tmap_apply, Usa2008P6.lap_inner, Iff.mp, LinearMap.mem_ker, of_eq_true, Eq.trans, True and 8 more
78 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
```
lemma range_lap_le_ker_Tmap : LinearMap.range (lap G) ≤ LinearMap.ker (Tmap G) := by
…
```
Mentions: Usa2008P6.lap, Usa2008P6.Tmap
lemma Usa2008P6.degVec_mem_ker_Tmap The degree vector is orthogonal to the kernel of lap G line 211 source
Source documentation
The degree vector is orthogonal to the kernel of lap G.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, SimpleGraph, Fin, DecidableRel, SimpleGraph.Adj, Membership.mem, ZMod, OfNat.ofNat, Submodule, LinearMap.ker, Module.Dual, Subtype, RingHom.id, Usa2008P6.lap, Usa2008P6.Tmap, Usa2008P6.degVec
Proof uses: Eq.mpr, Eq, LinearMap, id, congrArg, propext, Usa2008P6.mem_ker_Tmap, Subtype.mk, Finset.sum, Finset.univ, HMul.hMul, Usa2008P6.Tmap_apply, SimpleGraph.degree, Set, SimpleGraph.neighborSet, Eq.symm, Usa2008P6.inner_self_lap, Iff.mp, LinearMap.mem_ker, of_eq_true and 9 more
77 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
lemma degVec_mem_ker_Tmap : degVec G ∈ LinearMap.ker (Tmap G) := by
…
```
Mentions: Usa2008P6.degVec, Usa2008P6.Tmap
lemma Usa2008P6.Tmap_surjective Every functional on the kernel of lap G is realized by a dot product: extend it by zero on a complement and read off the coordinates line 221 source
Source documentation
Every functional on the kernel of lap G is realized by a dot product: extend it by zero on a complement and read off the coordinates.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, SimpleGraph, Fin, DecidableRel, SimpleGraph.Adj, Function.Surjective, ZMod, OfNat.ofNat, Module.Dual, Subtype, Membership.mem, Submodule, LinearMap.ker, RingHom.id, Usa2008P6.lap, LinearMap, Usa2008P6.Tmap
Proof uses: IsCompl, Exists, Eq, Submodule.exists_isCompl, LinearMap.comp, Submodule.projectionOnto, Exists.intro, Pi.single, LinearMap.ext, Eq.mpr, Subtype.mk, Finset.sum, Finset.univ, HMul.hMul, id, congrArg, Usa2008P6.Tmap_apply, HSMul.hSMul, pi_eq_sum_univ', Eq.rec and 12 more
94 instances, coercions and auxiliary constants left out.

Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
```
lemma Tmap_surjective : Function.Surjective (Tmap G) := by
…
```
Mentions: Usa2008P6.Tmap
lemma Usa2008P6.range_lap_eq_ker_Tmap A symmetric matrix over ZMod 2 has range equal to the orthogonal complement of its kernel; here this is phrased via Tmap line 243 source
Source documentation
A symmetric matrix over ZMod 2 has range equal to the orthogonal complement of its kernel; here this is phrased via Tmap.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, SimpleGraph, Fin, DecidableRel, SimpleGraph.Adj, Eq, Submodule, ZMod, OfNat.ofNat, LinearMap.range, RingHom.id, Usa2008P6.lap, LinearMap.ker, Module.Dual, Subtype, Membership.mem, Usa2008P6.Tmap
Proof uses: Submodule.eq_of_le_of_finrank_eq, Usa2008P6.range_lap_le_ker_Tmap, HAdd.hAdd, Module.finrank, LinearMap.finrank_range_add_finrank_ker, Top.top, Iff.mpr, Function.Surjective, LinearMap, LinearMap.range_eq_top, Usa2008P6.Tmap_surjective, Eq.mpr, id, congrArg, finrank_top, Subspace.dual_finrank_eq
72 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
```
lemma range_lap_eq_ker_Tmap : LinearMap.range (lap G) = LinearMap.ker (Tmap G) := by
…
```
Mentions: Usa2008P6.lap, Usa2008P6.Tmap
lemma Usa2008P6.exists_solution There is at least one valid room assignment line 255 source
Source documentation
There is at least one valid room assignment.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, SimpleGraph, Fin, DecidableRel, SimpleGraph.Adj, Exists, ZMod, OfNat.ofNat, Eq, LinearMap, RingHom.id, Usa2008P6.lap, Usa2008P6.degVec
Proof uses: Membership.mem, Submodule, LinearMap.range, Eq.mpr, LinearMap.ker, Module.Dual, Subtype, Usa2008P6.Tmap, id, congrArg, Usa2008P6.range_lap_eq_ker_Tmap, Usa2008P6.degVec_mem_ker_Tmap, Iff.mp, LinearMap.mem_range
43 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
lemma exists_solution : ∃ x0, lap G x0 = degVec G := by
…
```
Mentions: Usa2008P6.lap, Usa2008P6.degVec
def Usa2008P6.solutionEquiv The valid assignments form a coset of the kernel of lap G line 262 source
Source documentation
The valid assignments form a coset of the kernel of lap G.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, SimpleGraph, Fin, DecidableRel, SimpleGraph.Adj, ZMod, OfNat.ofNat, Eq, LinearMap, RingHom.id, Usa2008P6.lap, Usa2008P6.degVec, Equiv, Subtype, Membership.mem, Submodule, LinearMap.ker
Proof uses: Equiv.mk, Subtype.mk, HAdd.hAdd, HSub.hSub
47 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
```
def solutionEquiv (x0 : Fin n → ZMod 2) (hx0 : lap G x0 = degVec G) :
    ↥(LinearMap.ker (lap G)) ≃ {x // lap G x = degVec G} where
…
```
Mentions: Usa2008P6.lap, Usa2008P6.degVec
lemma Usa2008P6.card_solutions line 272 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, SimpleGraph, Fin, DecidableRel, SimpleGraph.Adj, ZMod, OfNat.ofNat, Eq, LinearMap, RingHom.id, Usa2008P6.lap, Usa2008P6.degVec, Fintype.card, Subtype, HPow.hPow, Module.finrank, Membership.mem, Submodule, LinearMap.ker
Proof uses: Eq.mpr, Nat.card, id, congrArg, Eq.symm, Nat.card_eq_fintype_card, Nat.card_congr, Equiv.symm, Usa2008P6.solutionEquiv, Module.natCard_eq_pow_finrank, ZMod.card, Eq.refl
81 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
problem Usa2008P6.usa2008_p6 line 280 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, SimpleGraph, Fin, DecidableRel, SimpleGraph.Adj, Exists, Eq, Fintype.card, Subtype, ZMod, OfNat.ofNat, Even, Finset.card, Finset.filter, SimpleGraph.neighborFinset, Membership.mem, Set, SimpleGraph.neighborSet, HPow.hPow
Proof uses: LinearMap, RingHom.id, Usa2008P6.lap, Usa2008P6.degVec, Usa2008P6.exists_solution, Exists.intro, Module.finrank, Submodule, LinearMap.ker, Iff, Eq.mpr, id, congrArg, propext, funext_iff, forall_congr', Usa2008P6.even_card_filter_iff, Fintype.card_congr, Equiv.subtypeEquivRight, Usa2008P6.card_solutions and 1 more
60 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.