[Tuza ν=4] PATH_4 v9: AWAITING RESULT (40362bf6)

[kavanaghpatrick]

Current Status: Cover Bound PROVEN ✅, Main Theorem BLOCKED

What We Solved (ca70c430)

Aristotle proved 3 key lemmas for PATH_4:

Lemma	Statement	Status
cover_hits_sharing_A	Triangles sharing ≥2 vertices with A are covered	✅ PROVEN
cover_hits_sharing_D	Triangles sharing ≥2 vertices with D are covered	✅ PROVEN
path4_cover_card_le_8_of_packing	With packing hypothesis, cover ≤ 8	✅ PROVEN

What's Blocking tau_le_8_path4

The main theorem tau_le_8_path4 depends on a false lemma:

• path4_cover_card_le_8 (without packing) - NEGATED by Aristotle
• Counterexample: A = {0,3,4,5} has 4 vertices, not a triangle

Fix Submitted: v9 (UUID: 40362bf6)

Changed main theorem to use the CORRECT lemma with packing hypothesis:

-- OLD (false):
have hcover_size : (path4_cover G cfg).card ≤ 8 := path4_cover_card_le_8 G cfg

-- NEW (correct):
have hcover_size : (path4_cover G cfg).card ≤ 8 := path4_cover_card_le_8_of_packing G M cfg hM

Next Steps

1. Wait for v9 result (40362bf6)
2. If sorry remains, need to prove cover actually hits all triangles
3. May need isTriangleCover lemma connecting cover definition to τ

Files

• partial/tuza/nu4/SLOT263_SUMMARY.md - Status summary
• submissions/nu4_final/slot263_path4_v9_fixed.lean - Latest submission

False Lemmas to Avoid

• shared_vertex_concentrated_savings: Open lemma in slot50 and slot43 #26: path4_cover_le_8_no_packing - Need packing hypothesis
• Slot 40: Bridge Counting Bound #11: self_loop_cover - s(v,v) not a valid edge

[kavanaghpatrick]

Status Update: v9 already submitted to Aristotle (UUID: 40362bf6). Awaiting result.

The fix wires path4_cover_card_le_8_of_packing (with packing hypothesis) to the main theorem instead of the false path4_cover_card_le_8.

Will update when result arrives.