problem6augmentation

This project extends the Problem 6 result in Archon-FirstProof-Results, the formalization of OpenAI's informal proof for FirstProof. We used Archon to formalize two new informal proofs by Prof. Ingo Althöfer that improve the lower-bound constant, at a total cost of around $50. This yields two independent Lean 4 proof variants:

• FirstProof/FirstProof6_constant — lower bound improved from ε/256 to ε/20
• FirstProof/FirstProof6_constant3 — lower bound improved from ε/256 to (3/40)·ε

The following was generated and summarized by Archon.

Differences from the Original Proof

The main theorem (Problem6.exists_eps_light_subset) states: for every simple graph G and ε ∈ (0,1], there exists an ε-light vertex subset S with |S| ≥ c·ε·|V|, where c is a positive absolute constant.

The original proof (FirstProof6) established c = 1/256 ≈ 0.004. This informal proof pushes c closer to the optimal value by refining the numerical constants.

As for the proof itself, the framework — a BSS coloring argument with a 6-step skeleton — is identical across all three versions. The only differences lie in the choice of numerical parameters.

Repository layout

problem6augmentation/
├── FirstProof/
│   ├── FirstProof6_constant/       # Variant 1: lower bound ε/20
│   │   ├── Problem6.lean           # Main theorem
│   │   ├── Problem6Aux.lean
│   │   └── Auxiliary/              # 7 auxiliary modules (same structure as original)
│   └── FirstProof6_constant3/      # Variant 2: lower bound (3/40)ε
│       ├── Problem6.lean           # Main theorem
│       ├── Problem6Aux.lean
│       └── Auxiliary/              # 7 auxiliary modules (same structure as original)
├── FirstProof_constant.lean        # Library entry point (imports constant variant)
├── FirstProof_constant3.lean       # Library entry point (imports constant3 variant)
└── lakefile.toml

Dependencies

• Lean version: 4.28.0
• Mathlib version: v4.28.0

---

Differences from FirstProof6 (for reviewers)

This section is for readers who have already read Archon-FirstProof-Results and want to know exactly what changed. The proof strategy is identical; all differences are parameter choices.

File-level overview

File	_constant vs original	_constant3 vs original
Auxiliary/ColoringFramework.lean	identical	one lemma rewritten (see below)
Problem6.lean	pervasive constant changes	major restructuring (see below)

---

Variant 1: FirstProof6_constant (bound ε/20)

Parameter substitution — every occurrence of the old parameters is replaced by the new ones; the rest of the proof structure is word-for-word the same:

Old (FirstProof6)	New (FirstProof6_constant)
u₀ = ε/2	u₀ = 2ε/3
k = n/4 (nat division)	k = n/3 (nat division)
r = ⌈16/ε⌉	r = ⌈4/ε⌉
initial barrier bound 2n/ε	3n/(2ε)
total potential bound 3n/ε	5n/(2ε)
n ≥ 4 throughout	n ≥ 12
small-n threshold n < 4	n < 12
final constant ε/256	ε/20

The arithmetic inside each lemma is updated to match, but no lemma is added, removed, or structurally changed.

---

Variant 2: FirstProof6_constant3 (bound 3ε/40)

This variant requires a different algebraic argument and introduces new definitions and lemmas.

New top-level definitions in Problem6.lean

def milkedK (n : ℕ) : ℕ := Nat.ceil (3 * (n : ℝ) / 8)
def milkedMStar (n : ℕ) : ℕ := n - milkedK n + 1
noncomputable def milkedCn (n : ℕ) : ℝ :=
  (n : ℝ) / (milkedMStar n : ℝ) * ((13 * (n : ℝ) - 8) / (5 * (n : ℝ) - 8))
noncomputable def milkedU0 (n : ℕ) (ε : ℝ) : ℝ := (5 / 8 - 1 / (n : ℝ)) * ε
def milkedR (n : ℕ) (ε : ℝ) : ℕ := Nat.ceil (milkedCn n / ε)

These replace the plain numeric expressions n/4, ⌈16/ε⌉, ε/2 used throughout FirstProof6. Every lemma that previously took r, k, u₀ as explicit parameters with specific bounds now calls these definitions instead.

New lemmas in Problem6.lean

• milkedK_formula: milkedK n = (3 * n + 7) / 8
• lemma1_polynomial_ineq: milkedCn n ≤ (100/9) · (milkedK n / n) for n ≥ 3

lemma1_polynomial_ineq is the key inequality that drives the final constant computation in eps_light_large_n.

Changes to Auxiliary/ColoringFramework.lean

Only one lemma changes: barrier_parameter_bound.

Aspect	Old	New
hypothesis	4 ≤ n	3 ≤ n
k	n / 4 (nat division)	Nat.ceil (3 * n / 8)
u₀	ε / 2	(5/8 − 1/n) · ε
conclusion	u_k ≤ 3ε/4 ∧ 3ε/4 < ε	u_k ≤ ε ∧ 0 < u₀

The new proof establishes u_k ≤ ε via the identity (5/8 − 1/n) + (3/8 + 1/n) = 1 after bounding ⌈3n/8⌉ ≤ 3n/8 + 1, and proves u₀ > 0 from 1/n ≤ 1/3 < 5/8 (using n ≥ 3).

Structural changes to Problem6.lean

total_barrier_bound_base: The initial barrier is now n / u₀ (i.e., n / milkedU0 n ε) instead of the fixed 2n/ε, since u₀ is no longer a fixed fraction of ε.

good_pair_exists:

• Step B: 4m ≥ 3n (old) → milkedMStar n ≤ m (new).
• Step E: the trace bound is now a strict inequality tr(U) < n / u₀.
• Step Q: the contradiction argument changes from 3n/ε < m·r to n/u₀ + n/ε ≤ m·r, using the algebraic identity n/u₀ + n/ε = milkedMStar n · milkedCn n / ε and m ≥ milkedMStar n, r ≥ Cₙ/ε.

total_barrier_bound: The old proof split into cases k ≤ r and k > r; the new proof eliminates the case split and always runs the BSS induction directly.

eps_light_large_n: The proof splits on r ≤ 5 vs r ≥ 6:

• Case r ≤ 5: |S| ≥ k/5, k ≥ 3n/8, so 40|S| ≥ 3n ≥ 3εn.
• Case r ≥ 6: uses lemma1_polynomial_ineq to get 9n · Cₙ ≤ 100k, combined with 5ε < Cₙ and εr < Cₙ + ε to conclude 40|S| · r ≥ 40k > 3nεr.

eps_light_small_n: threshold changes from n < 4 to n ≤ 2.

Final theorem: exists_eps_light_subset now states |S| ≥ (3/40) · ε · |V|; the case split is on 3 ≤ n / n ≤ 2.