GraphConjecture2.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

34 declarations, 0 contain sorry, 0 declared as axioms

Written on the Wall II - Conjecture 2

Reference: E. DeLaVina, Written on the Wall II, Conjectures of Graffiti.pc

Imports (1)

FormalConjectures.Util.ProblemImports

lemma WrittenOnTheWallII.GraphConjecture2.exists_max_indep_set_in_nbhd line 33 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, Nontrivial, SimpleGraph, Exists, Finset, And, HasSubset.Subset, Set, SimpleGraph.neighborSet, IsAntichain, SimpleGraph.Adj, Eq, Nat, Finset.card, SimpleGraph.indepNeighborsCard
Proof uses: Eq.mpr, Membership.mem, Set.Pairwise, Compl.compl, SimpleGraph.indepNum, SimpleGraph.induce, id, congrArg, funext, forall_congr, implies_congr, SupSet.sSup, setOf, SimpleGraph.IsNIndepSet, Not, Subtype.mk, Eq.substr, congr, Eq.refl, Eq.trans and 51 more
52 instances, coercions and auxiliary constants left out.

Tactic trace: 20 steps
Open to load the checked before-and-after goal states.
def WrittenOnTheWallII.GraphConjecture2.maxIndepSet line 51 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, Nontrivial, SimpleGraph, Finset
Proof uses: Classical.choose, And, HasSubset.Subset, Set, SimpleGraph.neighborSet, IsAntichain, SimpleGraph.Adj, Eq, Nat, Finset.card, SimpleGraph.indepNeighborsCard, WrittenOnTheWallII.GraphConjecture2.exists_max_indep_set_in_nbhd
3 instances, coercions and auxiliary constants left out.
lemma WrittenOnTheWallII.GraphConjecture2.sum_indepNeighbors_eq line 54 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, Nontrivial, SimpleGraph, DecidableRel, SimpleGraph.Adj, Eq, Real, Finset.sum, Finset.univ, SimpleGraph.indepNeighbors, Finset.card, WrittenOnTheWallII.GraphConjecture2.maxIndepSet
Proof uses: id, SimpleGraph.indepNeighborsCard, Classical.choose, Finset, And, HasSubset.Subset, Set, SimpleGraph.neighborSet, IsAntichain, Nat, WrittenOnTheWallII.GraphConjecture2.exists_max_indep_set_in_nbhd, Fintype.sum_congr, SimpleGraph.indepNum, SimpleGraph.induce, Classical.indefiniteDescription, Subtype, Subtype.mk, of_eq_true, Eq.trans, True and 4 more
13 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma WrittenOnTheWallII.GraphConjecture2.sum_card_eq_sum_din line 60 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, Nontrivial, SimpleGraph, DecidableRel, SimpleGraph.Adj, Eq, Real, Finset.sum, Finset.univ, Finset.card, WrittenOnTheWallII.GraphConjecture2.maxIndepSet, Finset.filter, Membership.mem, Finset
Proof uses: of_eq_true, Eq.trans, True, Nat, congr, congrArg, ite, OfNat.ofNat, DecidablePred, Fintype.sum_congr, Finset.card_filter, Finset.sum_comm, Finset.sum_congr, Eq.refl, Inter.inter, Finset.sum_ite_mem, HSMul.hSMul, Finset.univ_inter, Finset.sum_const, mul_one and 3 more
26 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma WrittenOnTheWallII.GraphConjecture2.h_spanning_tree_lemma line 64 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, Nontrivial, SimpleGraph, SimpleGraph.Connected, Exists, SimpleGraph.Subgraph, And, SimpleGraph.Subgraph.IsSpanning, SimpleGraph.IsTree, SimpleGraph.Subgraph.verts, SimpleGraph.Subgraph.coe
Proof uses: LE.le, SimpleGraph.Connected.exists_isTree_le, SimpleGraph.toSubgraph, Exists.intro, And.intro, SimpleGraph.toSubgraph.isSpanning, Eq.mpr, Set.univ, SimpleGraph.IsAcyclic, id, Eq, SimpleGraph.Reachable, SimpleGraph.Adj, SimpleGraph.IsBridge, Sym2.mk, Prod.mk, congr, congrArg, Membership.mem, Set and 49 more
31 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
lemma WrittenOnTheWallII.GraphConjecture2.max_leaf_tree_exists line 77 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, Nontrivial, SimpleGraph, DecidableRel, SimpleGraph.Adj, SimpleGraph.Connected, Exists, SimpleGraph.Subgraph, And, SimpleGraph.Subgraph.IsSpanning, SimpleGraph.IsTree, SimpleGraph.Subgraph.verts, SimpleGraph.Subgraph.coe, Eq, Real, SimpleGraph.Ls, Finset.card, Finset.filter, Nat and 7 more
Proof uses: setOf, Set.Finite, Set.Nonempty, WrittenOnTheWallII.GraphConjecture2.h_spanning_tree_lemma, Exists.intro, And.intro, Set.image, Set.Finite.image, Set.Nonempty.image, SupSet.sSup, Set.Nonempty.csSup_mem, Eq.refl, Eq.mpr, id, congrArg, Eq.symm
25 instances, coercions and auxiliary constants left out.

Tactic trace: 22 steps
Open to load the checked before-and-after goal states.
lemma WrittenOnTheWallII.GraphConjecture2.c_edge_bound_strong line 98 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, Nontrivial, SimpleGraph, DecidableRel, SimpleGraph.Adj, LE.le, Real, HAdd.hAdd, Finset.card, Finset.filter, Membership.mem, Finset, WrittenOnTheWallII.GraphConjecture2.maxIndepSet, Finset.univ, Union.union, SimpleGraph.neighborFinset
Proof uses: Disjoint, Eq.mpr, Not, id, Eq, congrArg, propext, Finset.disjoint_filter, IsAntichain, And.left, Classical.choose, And, HasSubset.Subset, Set, SimpleGraph.neighborSet, Nat, SimpleGraph.indepNeighborsCard, WrittenOnTheWallII.GraphConjecture2.exists_max_indep_set_in_nbhd, And.right, Classical.choose_spec and 14 more
44 instances, coercions and auxiliary constants left out.

Tactic trace: 26 steps
Open to load the checked before-and-after goal states.
lemma WrittenOnTheWallII.GraphConjecture2.tree_leaves_ge_degrees line 125 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, Nontrivial, SimpleGraph, DecidableRel, SimpleGraph.Adj, SimpleGraph.Subgraph, SimpleGraph.IsTree, SimpleGraph.Subgraph.verts, SimpleGraph.Subgraph.coe, SimpleGraph.Subgraph.Adj, GE.ge, Real, Finset.card, Finset.filter, Eq, Nat, SimpleGraph.Subgraph.degree, Membership.mem, Set and 5 more
Proof uses: Finset, Ne, Union.union, Eq.mpr, id, congrArg, Not, Finset.filter_union_filter_neg_eq, Eq.refl, Disjoint, Finset.disjoint_filter_filter_neg, Finset.sum, HMul.hMul, Sym2, SimpleGraph.edgeFinset, Fintype.card, SimpleGraph.IsTree.card_edgeFinset, Finset.univ, SimpleGraph.degree, SimpleGraph.sum_degrees_eq_twice_card_edges and 168 more
157 instances, coercions and auxiliary constants left out.

Tactic trace: 62 steps
Open to load the checked before-and-after goal states.
def WrittenOnTheWallII.GraphConjecture2.DoubleStar line 159 source
no axioms what this means
Statement uses: SimpleGraph, SimpleGraph.Adj
Proof uses: SimpleGraph.mk, Or, And, Eq, Ne, Not
2 instances, coercions and auxiliary constants left out.

Tactic trace: 64 steps
Open to load the checked before-and-after goal states.
lemma WrittenOnTheWallII.GraphConjecture2.DoubleStar_le line 199 source
standard axioms: Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, Nontrivial, SimpleGraph, SimpleGraph.Adj, LE.le, WrittenOnTheWallII.GraphConjecture2.DoubleStar
Proof uses: And, Eq, Or, Ne, Not, Eq.mpr, id, congrArg, And.left, And.right, SimpleGraph.symm
2 instances, coercions and auxiliary constants left out.

Tactic trace: 20 steps
Open to load the checked before-and-after goal states.
lemma WrittenOnTheWallII.GraphConjecture2.DoubleStar_isAcyclic line 210 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, Nontrivial, SimpleGraph, SimpleGraph.Adj, SimpleGraph.IsAcyclic, WrittenOnTheWallII.GraphConjecture2.DoubleStar
Proof uses: id, SimpleGraph.Walk, SimpleGraph.mk, Or, And, Eq, Ne, Not, HEq, SimpleGraph.Walk.IsCycle, SimpleGraph.Walk.nil, False.elim, False, Eq.mp, Eq.symm, eq_of_heq, SimpleGraph.Walk.cons, SimpleGraph.Adj.ne, rfl, LE.le.not_gt and 49 more
28 instances, coercions and auxiliary constants left out.

Tactic trace: 28 steps
Open to load the checked before-and-after goal states.
lemma WrittenOnTheWallII.GraphConjecture2.exists_maximal_acyclic line 228 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, Nontrivial, SimpleGraph, LE.le, SimpleGraph.IsAcyclic, Exists, And, Eq
Proof uses: Membership.mem, Set, setOf, Nat, Set.ncard, Set.exists_max_image, Exists.intro, And.intro, le_refl, And.elim, WrittenOnTheWallII.GraphConjecture2.exists_maximal_acyclic.match_1, le_antisymm, And.right, Eq.ge, Set.eq_of_subset_of_ncard_le, Set.setOf_subset_setOf_of_imp, Mathlib.Tactic.GCongr.and_right_mono, le_imp_le_of_le_of_le, LE.le.trans, Set.toFinite and 1 more
20 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
def WrittenOnTheWallII.GraphConjecture2.AddEdge line 232 source
no axioms what this means
Statement uses: SimpleGraph, Ne
Proof uses: SimpleGraph.mk, Or, SimpleGraph.Adj, And, Eq
2 instances, coercions and auxiliary constants left out.

Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
lemma WrittenOnTheWallII.GraphConjecture2.AddEdge_le line 247 source
standard axioms: Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, Nontrivial, SimpleGraph, Ne, LE.le, SimpleGraph.Adj, WrittenOnTheWallII.GraphConjecture2.AddEdge
Proof uses: Or, And, Eq, SimpleGraph.symm
5 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma WrittenOnTheWallII.GraphConjecture2.T_le_AddEdge line 255 source
standard axioms: Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, Nontrivial, SimpleGraph, Ne, LE.le, WrittenOnTheWallII.GraphConjecture2.AddEdge
Proof uses: SimpleGraph.Adj, Or.inl, Or, And, Eq
1 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma WrittenOnTheWallII.GraphConjecture2.Reachable_AddEdge_walk line 260 source
standard axioms: Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, Nontrivial, SimpleGraph, Ne, SimpleGraph.Walk, WrittenOnTheWallII.GraphConjecture2.AddEdge, Or, SimpleGraph.Reachable, And
Proof uses: SimpleGraph.Walk.rec, Or.inl, SimpleGraph.Reachable.refl, SimpleGraph.Adj, Eq, SimpleGraph.Reachable.trans, SimpleGraph.Adj.reachable, Or.inr, HEq, Eq.refl, And.intro, HEq.refl
4 instances, coercions and auxiliary constants left out.

Tactic trace: 55 steps
Open to load the checked before-and-after goal states.
lemma WrittenOnTheWallII.GraphConjecture2.Reachable_AddEdge line 302 source
standard axioms: Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, Nontrivial, SimpleGraph, Ne, SimpleGraph.Reachable, WrittenOnTheWallII.GraphConjecture2.AddEdge, Or, And
Proof uses: SimpleGraph.Walk, WrittenOnTheWallII.GraphConjecture2.Reachable_AddEdge_walk
1 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma WrittenOnTheWallII.GraphConjecture2.AddEdge_isAcyclic line 307 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, Nontrivial, SimpleGraph, Ne, SimpleGraph.IsAcyclic, Not, SimpleGraph.Reachable, WrittenOnTheWallII.GraphConjecture2.AddEdge
Proof uses: Eq.mpr, Sym2, Membership.mem, Set, SimpleGraph.edgeSet, SimpleGraph.IsBridge, id, Eq, congrArg, propext, SimpleGraph.isAcyclic_iff_forall_edge_isBridge, Sym2.ind, Sym2.mk, Prod.mk, And, SimpleGraph.Adj, SDiff.sdiff, SimpleGraph.fromEdgeSet, Singleton.singleton, SimpleGraph.isBridge_iff and 33 more
13 instances, coercions and auxiliary constants left out.

Tactic trace: 195 steps
Open to load the checked before-and-after goal states.
lemma WrittenOnTheWallII.GraphConjecture2.walk_leaves_C line 440 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, Nontrivial, SimpleGraph, SimpleGraph.Reachable, Not, Exists, And, SimpleGraph.Adj
Proof uses: Eq.mpr, Eq.refl, by_contra, Function.comp, False, SimpleGraph.Walk, SimpleGraph.Reachable.elim, SimpleGraph.Walk.rec, id
1 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma WrittenOnTheWallII.GraphConjecture2.reachable_edge line 445 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, Nontrivial, SimpleGraph, SimpleGraph.Connected, Not, Exists, And, SimpleGraph.Adj, SimpleGraph.Reachable
Proof uses: Decidable.byContradiction, Classical.propDecidable, SimpleGraph.Connected.mk, Eq.mp, Eq.trans, binderNameHint, forall_congr, SimpleGraph.Connected.preconnected, SimpleGraph.Reachable.refl, WrittenOnTheWallII.GraphConjecture2.reachable_edge.match_1, WrittenOnTheWallII.GraphConjecture2.walk_leaves_C, Exists.intro, And.intro, SimpleGraph.Reachable.trans
7 instances, coercions and auxiliary constants left out.

Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
lemma WrittenOnTheWallII.GraphConjecture2.maximal_acyclic_is_connected line 462 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, Nontrivial, SimpleGraph, SimpleGraph.Connected, LE.le, SimpleGraph.IsAcyclic, Eq
Proof uses: Decidable.byContradiction, Classical.propDecidable, SimpleGraph.Adj, Not, WrittenOnTheWallII.GraphConjecture2.maximal_acyclic_is_connected.match_1, Exists, And, SimpleGraph.Reachable, False, WrittenOnTheWallII.GraphConjecture2.reachable_edge, Ne, SimpleGraph.Adj.ne, WrittenOnTheWallII.GraphConjecture2.AddEdge, WrittenOnTheWallII.GraphConjecture2.AddEdge_le, WrittenOnTheWallII.GraphConjecture2.AddEdge_isAcyclic, WrittenOnTheWallII.GraphConjecture2.T_le_AddEdge, Or.inr, Or, Or.inl, And.intro and 4 more
3 instances, coercions and auxiliary constants left out.

Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
lemma WrittenOnTheWallII.GraphConjecture2.exists_optimal_tree line 479 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, Nontrivial, SimpleGraph, DecidableRel, SimpleGraph.Adj, SimpleGraph.Connected, Exists, SimpleGraph.Subgraph, And, SimpleGraph.Subgraph.IsSpanning, SimpleGraph.IsTree, SimpleGraph.Subgraph.verts, SimpleGraph.Subgraph.coe, SimpleGraph.Subgraph.Adj, Membership.mem, Finset, SimpleGraph.neighborFinset, SDiff.sdiff
Proof uses: WrittenOnTheWallII.GraphConjecture2.DoubleStar, LE.le, WrittenOnTheWallII.GraphConjecture2.DoubleStar_le, SimpleGraph.IsAcyclic, WrittenOnTheWallII.GraphConjecture2.DoubleStar_isAcyclic, WrittenOnTheWallII.GraphConjecture2.exists_optimal_tree.match_1, Eq, WrittenOnTheWallII.GraphConjecture2.exists_maximal_acyclic, WrittenOnTheWallII.GraphConjecture2.maximal_acyclic_is_connected, SimpleGraph.toSubgraph, Exists.intro, Eq.mpr, id, SimpleGraph.Reachable, Subtype.mk, Set, Iff.mpr, True, Iff.of_eq, Set.univ and 42 more
29 instances, coercions and auxiliary constants left out.

Tactic trace: 26 steps
Open to load the checked before-and-after goal states.
lemma WrittenOnTheWallII.GraphConjecture2.union_neighbor_bound line 500 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, Nontrivial, SimpleGraph, DecidableRel, SimpleGraph.Adj, SimpleGraph.Connected, LE.le, Real, Finset.card, Union.union, Finset, SimpleGraph.neighborFinset, HAdd.hAdd, SimpleGraph.Ls, OfNat.ofNat, Nat
Proof uses: Exists, SimpleGraph.Subgraph, And, SimpleGraph.Subgraph.IsSpanning, SimpleGraph.IsTree, SimpleGraph.Subgraph.verts, SimpleGraph.Subgraph.coe, SimpleGraph.Subgraph.Adj, Membership.mem, SDiff.sdiff, WrittenOnTheWallII.GraphConjecture2.exists_optimal_tree, GE.ge, Finset.filter, Eq, SimpleGraph.Subgraph.degree, Set, Classical.propDecidable, Set.toFinset, HSub.hSub, WrittenOnTheWallII.GraphConjecture2.tree_leaves_ge_degrees and 97 more
104 instances, coercions and auxiliary constants left out.

Tactic trace: 19 steps
Open to load the checked before-and-after goal states.
lemma WrittenOnTheWallII.GraphConjecture2.c_edge_Ls_bound line 514 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, Nontrivial, SimpleGraph, DecidableRel, SimpleGraph.Adj, SimpleGraph.Connected, LE.le, Real, HAdd.hAdd, Finset.card, Finset.filter, Membership.mem, Finset, WrittenOnTheWallII.GraphConjecture2.maxIndepSet, Finset.univ, SimpleGraph.Ls, OfNat.ofNat, Nat
Proof uses: Union.union, SimpleGraph.neighborFinset, WrittenOnTheWallII.GraphConjecture2.c_edge_bound_strong, WrittenOnTheWallII.GraphConjecture2.union_neighbor_bound, le_of_not_gt, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HSub.hSub, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.add_congr, Int.rawCast, Int.negOfNat, HMul.hMul, HPow.hPow, Nat.rawCast, Mathlib.Tactic.Ring.instCommSemiringNat, Mathlib.Tactic.Ring.sub_congr, Mathlib.Tactic.Ring.atom_pf and 30 more
67 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma WrittenOnTheWallII.GraphConjecture2.c_edge_bound line 520 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, Nontrivial, SimpleGraph, DecidableRel, SimpleGraph.Adj, LE.le, Real, HAdd.hAdd, Finset.card, Finset.filter, Membership.mem, Finset, WrittenOnTheWallII.GraphConjecture2.maxIndepSet, Finset.univ, Fintype.card
Proof uses: Disjoint, Eq.mpr, Not, id, Eq, congrArg, propext, Finset.disjoint_filter, IsAntichain, And.left, Classical.choose, And, HasSubset.Subset, Set, SimpleGraph.neighborSet, Nat, SimpleGraph.indepNeighborsCard, WrittenOnTheWallII.GraphConjecture2.exists_max_indep_set_in_nbhd, And.right, Classical.choose_spec and 9 more
37 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
lemma WrittenOnTheWallII.GraphConjecture2.c_deg_bound line 533 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, Nontrivial, SimpleGraph, DecidableRel, SimpleGraph.Adj, LE.le, Real, Finset.card, Finset.filter, Membership.mem, Finset, WrittenOnTheWallII.GraphConjecture2.maxIndepSet, Finset.univ, SimpleGraph.degree
Proof uses: HasSubset.Subset, SimpleGraph.neighborFinset, Set, Classical.choose, And, SimpleGraph.neighborSet, IsAntichain, Eq, Nat, SimpleGraph.indepNeighborsCard, WrittenOnTheWallII.GraphConjecture2.exists_max_indep_set_in_nbhd, And.left, Classical.choose_spec, And.right, Eq.mp, congrArg, propext, Finset.mem_filter, Eq.mpr, id and 5 more
29 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
def WrittenOnTheWallII.GraphConjecture2.S_heavy line 544 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, Nontrivial, SimpleGraph, DecidableRel, SimpleGraph.Adj, Finset
Proof uses: Finset.filter, LT.lt, Real, HAdd.hAdd, HDiv.hDiv, SimpleGraph.Ls, OfNat.ofNat, Finset.card, Membership.mem, WrittenOnTheWallII.GraphConjecture2.maxIndepSet, Finset.univ
15 instances, coercions and auxiliary constants left out.
lemma WrittenOnTheWallII.GraphConjecture2.S_heavy_is_indep line 547 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, Nontrivial, SimpleGraph, DecidableRel, SimpleGraph.Adj, SimpleGraph.Connected, SimpleGraph.IsIndepSet, Finset, WrittenOnTheWallII.GraphConjecture2.S_heavy
Proof uses: Membership.mem, Set, Ne, Eq.mp, congrArg, propext, Finset.mem_coe, LT.lt, Real, HAdd.hAdd, HDiv.hDiv, SimpleGraph.Ls, OfNat.ofNat, Finset.card, Finset.filter, WrittenOnTheWallII.GraphConjecture2.maxIndepSet, Finset.univ, And.right, And, Finset.mem_filter and 83 more
86 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
lemma WrittenOnTheWallII.GraphConjecture2.S_heavy_inter_bound line 559 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, Nontrivial, SimpleGraph, DecidableRel, SimpleGraph.Adj, SimpleGraph.Connected, LE.le, Real, Finset.card, Inter.inter, Finset, SimpleGraph.neighborFinset, WrittenOnTheWallII.GraphConjecture2.S_heavy, HAdd.hAdd, HDiv.hDiv, SimpleGraph.Ls, OfNat.ofNat, Nat
Proof uses: dite, Eq, EmptyCollection.emptyCollection, Iff.mpr, Finset.card_eq_zero, cast, Eq.symm, Eq.trans, congrArg, Nat.cast_zero, Eq.mpr, SupSet.sSup, Set.image, SimpleGraph.Subgraph, Finset.filter, SimpleGraph.Subgraph.degree, Membership.mem, Set, SimpleGraph.Subgraph.verts, Classical.propDecidable and 141 more
152 instances, coercions and auxiliary constants left out.

Tactic trace: 38 steps
Open to load the checked before-and-after goal states.
lemma WrittenOnTheWallII.GraphConjecture2.fms_algebraic_sum line 587 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, Nontrivial, SimpleGraph, DecidableRel, SimpleGraph.Adj, Real, LE.le, OfNat.ofNat, SimpleGraph.degree, HAdd.hAdd, HMul.hMul, Nat, Finset, SimpleGraph.IsIndepSet, Iff, Membership.mem, LT.lt, Not, Finset.card and 5 more
Proof uses: SDiff.sdiff, Eq, Union.union, of_eq_true, Eq.trans, HasSubset.Subset, True, congrArg, Finset.union_sdiff_self_eq_union, eq_true, True.intro, Disjoint, Eq.mpr, Eq.refl, Finset.disjoint_sdiff, forall_congr, implies_congr, And, congr, propext and 156 more
172 instances, coercions and auxiliary constants left out.

Tactic trace: 55 steps
Open to load the checked before-and-after goal states.
lemma WrittenOnTheWallII.GraphConjecture2.fms_combinatorial_core line 638 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, Nontrivial, SimpleGraph, DecidableRel, SimpleGraph.Adj, SimpleGraph.Connected, LE.le, Real, Finset.sum, Finset.univ, Finset.card, Finset.filter, Membership.mem, Finset, WrittenOnTheWallII.GraphConjecture2.maxIndepSet, HMul.hMul, Fintype.card, HAdd.hAdd, HDiv.hDiv and 3 more
Proof uses: WrittenOnTheWallII.GraphConjecture2.S_heavy, SimpleGraph.degree, WrittenOnTheWallII.GraphConjecture2.c_deg_bound, WrittenOnTheWallII.GraphConjecture2.c_edge_Ls_bound, Eq, Trans.trans, mul_add, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, HPow.hPow, Mathlib.Tactic.Ring.instCommSemiringNat, Mathlib.Meta.NormNum.instAddMonoidWithOne', Mathlib.Tactic.Ring.add_congr, Mathlib.Tactic.Ring.mul_congr, NNRat.rawCast, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Meta.NormNum.instAtLeastTwo, Mathlib.Tactic.Ring.div_congr and 109 more
130 instances, coercions and auxiliary constants left out.

Tactic trace: 28 steps
Open to load the checked before-and-after goal states.
lemma WrittenOnTheWallII.GraphConjecture2.fms_lemma line 670 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, Nontrivial, SimpleGraph, DecidableRel, SimpleGraph.Adj, SimpleGraph.Connected, LE.le, Real, Finset.sum, Finset.univ, SimpleGraph.indepNeighbors, HMul.hMul, Fintype.card, HAdd.hAdd, HDiv.hDiv, SimpleGraph.Ls, OfNat.ofNat, Nat
Proof uses: Eq, Finset.card, WrittenOnTheWallII.GraphConjecture2.maxIndepSet, WrittenOnTheWallII.GraphConjecture2.sum_indepNeighbors_eq, Finset.filter, Membership.mem, Finset, WrittenOnTheWallII.GraphConjecture2.sum_card_eq_sum_din, Eq.mpr, id, congrArg, WrittenOnTheWallII.GraphConjecture2.fms_combinatorial_core
36 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma WrittenOnTheWallII.GraphConjecture2.l_le_Ls_div_2_plus_1 line 677 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, Nontrivial, SimpleGraph, DecidableRel, SimpleGraph.Adj, SimpleGraph.Connected, LE.le, Real, SimpleGraph.l, HAdd.hAdd, HDiv.hDiv, SimpleGraph.Ls, OfNat.ofNat, Nat
Proof uses: Eq, Finset.sum, Finset.univ, SimpleGraph.indepNeighbors, Fintype.card, rfl, HMul.hMul, WrittenOnTheWallII.GraphConjecture2.fms_lemma, LT.lt, Ne, Fintype.card_ne_zero, Iff.mpr, Nat.cast_pos, Nat.pos_of_ne_zero, Eq.mpr, id, congrArg, div_mul_cancel₀, ne_of_gt, Trans.trans and 5 more
69 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
theorem WrittenOnTheWallII.GraphConjecture2.conjecture2 Graffiti.pc Conjecture 2: average local independence forces many spanning-tree leaves line 704 source
Source documentation
WOWII Conjecture 2
For a simple connected graph G, Ls(G) ≥ 2 · (l(G) - 1) where l(G) is the average independence number of the neighbourhoods of the vertices of G.
L4DEL explanation
The key idea is to look at the degrees of the vertices on the right side
— George Tsoukalas et al., AlphaProof Nexus paper (Appendix I)
We prove Graffiti.pc Conjecture 2, a 1996 conjecture listed as open
— Independent proof by Yanmohan Wang, Tianyue Dai, and Rui Tong (2026)
In every finite connected simple graph, the maximum number Ls(G) of leaves in a spanning tree is at least 2(l(G)-1), where l(G) is the average, over vertices, of the largest independent set inside each open neighbourhood.
1. Choose a maximum independent set in every vertex neighbourhood and let c(x) count how many of those chosen sets contain x; double counting identifies the average of c with l(G).
2. For every edge xy, independence and a spanning-tree construction bound c(x)+c(y) by Ls(G)+2.
3. Vertices with c(x) > Ls(G)/2+1 form an independent heavy set, and each light vertex has only boundedly many heavy neighbours.
4. A discharging inequality moves each heavy vertex's excess to light neighbours without exceeding their slack, proving l(G) ≤ Ls(G)/2+1 and hence the claimed result.
Sources and attribution: Pinned Lean source (0647711a7118), George Tsoukalas et al., AlphaProof Nexus paper (Appendix I), Independent proof by Yanmohan Wang, Tianyue Dai, and Rui Tong (2026)
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, Nontrivial, SimpleGraph, SimpleGraph.Connected, LE.le, Real, HMul.hMul, OfNat.ofNat, Nat, HSub.hSub, SimpleGraph.l, SimpleGraph.Ls, Classical.propDecidable, SimpleGraph.Adj
Proof uses: Eq, rfl, HAdd.hAdd, HDiv.hDiv, WrittenOnTheWallII.GraphConjecture2.l_le_Ls_div_2_plus_1, le_of_not_gt, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, inferInstance, AddMonoidWithOne, Mathlib.Meta.NormNum.instAtLeastTwo, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.add_congr, Int.rawCast, Int.negOfNat, HPow.hPow, Nat.rawCast, Mathlib.Tactic.Ring.instCommSemiringNat and 59 more
90 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
theorem conjecture2 (G : SimpleGraph α) (h : G.Connected) :
  2 * (l G - 1) ≤ Ls G := by
…
```