Next batch of theorems

[cgbarlow]

Testing whether #387 is working properly to create non trivial batch

[cgbarlow]

On it — sourcing the next batch and running each candidate through the ADR-035 triviality gate (check_triviality) on top of the usual type-check + absence check. The point of this batch is to exercise #387 end-to-end: only non-trivial candidates are admitted, and I'll report any the probe rightly rejects (a one-shot-closable or already-in-mathlib-under-another-name statement).

[cgbarlow]

Result — the #387 gate works (PR #404)

Ran 10 agent-sourced candidates through the full pipeline (type-check + absence + ADR-035 triviality gate). 3 admitted, 7 dropped — and the drops are the interesting part:

Admitted (type-check ✓, absent ✓, non-trivial ✓):

• nat-sq-lt-two-pow — n² < 2ⁿ for n ≥ 5 (two-layer induction)
• prod-one-sub-inv-sq-telescope — ∏(1−1/k²) = (n+1)/(2n) over ℚ (rational telescope)
• no-nat-sq-eq-two-mul-sq — ¬∃ a b, 0<b ∧ a²=2b² (√2 irrationality, descent — Freek docs(v0.1.0): adopt development protocols + governance ADRs (ADR-001..005) #1)

Dropped — each by a different guard:

• 5 pool duplicates (Fibonacci ×2, ∑k·2^k, ∑(2k+1)³, ∑k·k!) — dedup; the ∑k·k! one was also off-by-one false (numeric truth-check).
• catalan — already in mathlib (catalan_eq_centralBinom_div); caught by a type-check name collision.
• modEq_nine_digits_sum — the exact mathlib lemma (Data/Nat/Digits/Div.lean:28); caught by the absence grep. The triviality probe passed it (it isn't simp/aesop-closable, and exact?-membership is deferred) — so this shows absence and triviality are complementary, not redundant.

Verdict on #387: the triviality gate correctly passed all genuinely-non-trivial statements and rejected none of them spuriously; it's not a standalone duplicate-detector (the exact?/membership case is the absence check's job), which is by design. The gate itself is healthy.

Two real probe bugs the run surfaced (tracked as #387 follow-ups, separate PRs):

1. a failed to synthesize instance type error is mis-classified non-trivial instead of probe-error (regex gap);
2. check_triviality --all uses --per-tactic (≤11 builds/goal) → the retro-audit timed out at 90 min. Switching bulk to the combined probe.

[cgbarlow]

Done. The #387 triviality gate was exercised on a real sourcing run: 10 candidates → 3 admitted (in PR #404: nat-sq-lt-two-pow, prod-one-sub-inv-sq-telescope, no-nat-sq-eq-two-mul-sq), 7 correctly rejected (5 pool duplicates incl. one off-by-one false; catalan already in mathlib by name-collision; modEq_nine_digits_sum the exact mathlib lemma caught by the absence grep). Conclusion: the gate works and is complementary to the absence check. Two probe bugs the run surfaced are tracked separately as #410 and #411.

[cgbarlow]

we need the next 50 goals... create these in batches. Each goal needs to get us closer to #365

[cgbarlow]

Do these latest targets get us any closer to #365 goal? #81 (comment)

next batch must get us closer to #365. Also, per previous comment, I asked for 50 new goals, not 6... how are we going with our 50 next goals? what's the plan to get that done?