Add 27 WOWII named graph-invariant files (batches 3-9, part 2/2)

[henrykmichalewski]

This PR adds 27 WOWII formalizations organized by graph invariant topic from our internal batches 3-9.

Part 2 of 2 of splitting our internal batch wowii-batches-3-9 (49 files total after excluding one held back) into two reviewer-manageable PRs grouped semantically. The companion PR (#3820) covers the GraphConjecture<N>.lean files indexed by individual WOWII conjecture numbers; this PR covers the Graph<InvariantName>.lean files where several conjectures around a shared graph invariant are gathered into a single file.

Invariants / topics in this PR

Achromatic Number, Arboricity, Bandwidth, Boxicity, Circumference, Crossing Number, Degeneracy, Distance (Odd), Edge Connectivity, Even Mode Min, Frequency Max L, Geodetic Number, Girth Complement, Isoperimetric, Length, Median Degree, Metric Dimension, Min Edge Degree, Mode, Mode Max, Odd Girth, Power, Rainbow Connection, Roman Domination, Thickness, Toughness, Wiener Index.

Guarantees

• Each file references the relevant WOWII conjectures (and resolved statements where applicable) with canonical source URLs.
• Formalizations were cross-checked against DeLaViña's current WOWII website for status (T/F/R/O) and statement text.

Related

• Add 16 WOWII open conjectures (batch 1) #3795 (batch 1, merged)
• Add 10 WOWII open conjectures (batch 2) #3796 (batch 2, open)
• Companion PR: Add 22 WOWII numbered conjectures (batches 3-9, part 1/2) #3820 (this batch, part 1/2 — numbered GraphConjecture<N> files)

[henrykmichalewski]

Fixed the build failure. GraphCircumference.lean was importing and opening WrittenOnTheWallII.GraphConjecture199 (which is intentionally excluded from this PR to avoid conflict with #3796) to reuse vertexConnectivity. Dropped the import/open and inlined the vertexConnectivity definition locally. Local lake build FormalConjectures.WrittenOnTheWallII.GraphCircumference succeeds.

[mo271]

can you double check that the numbering is correct here (see #3824)

[henrykmichalewski]

Thanks for flagging — re-audited all 27 named files in this PR against the WOWII source. No off-by-one numbering shift of the type you fixed in #3823 / #3824 appears here; 23 of the 27 files don't claim a specific WOWII number at all (they're topical / Graffiti.pc-style observations citing Harary–Hedetniemi, Nash-Williams, Roberts, Bondy–Murty, etc.).

So no code changes pushed for this PR.

That said, the audit did surface two files that claim a specific WOWII number but don't state the corresponding conjecture, which I want to disclose here for transparency:

• GraphFrequencyMaxL.lean — declares Conjecture 209 (a Hamiltonian-path implication: "if (1/6)·(1 + 2·|E(Gᶜ)|) ≤ frequency of λ_max(G) then G has a Hamiltonian path"), but the formal theorem body is the unrelated bound frequencyMaxL G ≤ G.indepNum.
• GraphLength.lean — declares Conjecture 19 (a lower bound on the largest induced bipartite subgraph: b(G) ≥ ⌊avg ecc(v) + max λ(v)⌋), but the formal theorem body uses α(G) (independence number, not b(G)) on the LHS and is in the wrong direction (≤ instead of ≥).

One file explicitly documents itself as a mirror of WOWII #96 with dist_odd in place of dist_even rather than as a literal Conjecture-96 formalisation: GraphDistOdd.lean. That's intentional, but the docstring could state it more clearly.

Happy to push a follow-up commit either dropping the WOWII-209/WOWII-19 attribution from those two files (recasting them as Graffiti.pc-style observations) or replacing the bodies with the real conjecture statements — your preference. The other 23 files are topical and unaffected.

[henrykmichalewski]

Follow-up: pushed f72987f bundling the audit findings I disclosed earlier:

• GraphLength.lean — was claiming WOWII Conjecture 19 in the docstring while stating an unrelated bound (α(G) ≤ ⌊length/n + max λ⌋, wrong invariant + wrong direction). Rewrote to state Conjecture 19 verbatim: b(G) ≥ ⌊avg_v ecc(v) + max_v l(v)⌋ using the upstream b G invariant and averageEccentricity. The auxiliary graphLength G = ∑ ecc(v) is retained.
• GraphFrequencyMaxL.lean — was claiming WOWII Conjecture 209 while stating an invented bound (frequencyMaxL G ≤ G.indepNum). Rewrote to state Conjecture 209 verbatim: (1/6)·(1 + 2·|E(Gᶜ)|) ≤ frequencyMaxL G → G has a Hamiltonian path.
• GraphDistOdd.lean — docstring polish: explicitly note this is a new Graffiti.pc-style observation (the distOdd-analogue of Conj 96), not a verbatim formalisation of a numbered WOWII conjecture.

All three files build cleanly.