Kernel-prove the base van der Waerden values

[DomTheDeveloper]

Result

Proves the exact two-color base values:

• W 1 = 1;
• W 2 = 3.

The proof gives explicit guaranteeing color intervals and explicit counter-colorings below each threshold. The W 2 upper bound is the two-color pigeonhole argument on {1,2,3}.

Green verification

Focused audit run 30212019209 passed every gate:

• source scan rejecting proof holes and trust escapes;
• exact registered Lake-module build;
• exact theorem axiom audits.

Both theorems depend only on:

[propext, Classical.choice, Quot.sound]

No sorryAx or compiler-trust dependency appears.

Status

Both proof theorems are green. Clean canonical wrapper replacements are still required before promotion to _PRs/ready/.

[github-actions]

👋 This is an automated welcome message. 🤖
Thanks for the contributions!

A few friendly reminders while the review gets started:

• Please take a look at the style guidelines,
  especially the conventions for references, categories, AMS tags, and answer(sorry).
• You can manage some PR labels by leaving a comment with +label-name or -label-name; for example, +awaiting-author or -awaiting-author.
• This repository is mainly for formalised statements. Proofs longer than about 25-50 lines are usually out of scope; longer proofs are welcome to be included/linked via the formal_proof mechanism.

Thanks again for helping improve Formal Conjectures.