WrittenOnTheWallII/GraphConjecture160 misformalizes χ_{C₄} as countInducedC4

[changjonathanc]

Describe the misformalization

The formalization of Written on the Wall II Conjecture 160 interprets
χ_{C₄}(G) as the number of induced four-cycles in G:

let cC4 := countInducedC4 G

This occurs in GraphConjecture160.lean.

However, the historical WOWII notation defines χ_{C₄} as the C₄-free
characteristic function: it is 1 when G is C₄-free and 0 otherwise.
Here “C₄-free” means that G has no C₄ as a subgraph; the cycle need not be
induced. See the original WOWII conjecture list
and definition 73 in the original definition script.

Thus the current formalization substitutes a different invariant for the one
in the historical conjecture. The two invariants are neither equal nor counts
of the same objects.

Trivial proof/disproof

The existing sanity check already shows the mismatch on K₃:
countInducedC4 K₃ = 0, whereas the historical χ_{C₄}(K₃) = 1 because K₃
is C₄-free.

Conversely, on the four-cycle graph C₄, countInducedC4 C₄ is nonzero while
the historical characteristic function is 0.

These examples show that countInducedC4 does not formalize χ_{C₄}. They do
not by themselves prove or disprove the correctly stated conjecture.

Suggested fix

Replace countInducedC4 G with a 0/1 characteristic function detecting
whether four distinct vertices form a cycle, without requiring the absence of
chords. For example, following the treatment already used in
WrittenOnTheWallII/GraphConjecture133.lean:

let hasC4 := ∃ a b c d : α,
  a ≠ b ∧ a ≠ c ∧ a ≠ d ∧ b ≠ c ∧ b ≠ d ∧ c ≠ d ∧
  G.Adj a b ∧ G.Adj b c ∧ G.Adj c d ∧ G.Adj d a
let cC4 : ℕ := if hasC4 then 0 else 1

The theorem documentation should likewise use χ_{C₄} and describe it as the
C₄-free characteristic function, rather than as a count of induced cycles.
The now-irrelevant countInducedC4 sanity check can then be removed.

Additional context

The distinction matters in two independent ways:

• the historical invariant is a Boolean-valued characteristic function, not a count;
• it detects all C₄ subgraphs, not only induced C₄s.

The analogous formalization in GraphConjecture133.lean supports this reading
of the original notation.

AI assistance disclosure

This report and the proposed correction were prepared with assistance from
OpenAI Codex, using the model identified by the Codex UI as GPT-5.6 Sol. The
historical-source interpretation and suggested Lean change should be
independently reviewed by a human maintainer.

Choose either option

• I plan on working on this issue
• This issue is up for grabs: I would like to see this misformalization fixed by somebody else