EGRS75 two-prime closure — NO-VACUITY SMOKE PROBE (2026-06-12).

Instantiates the closed theorem MuFinish.egrs_two_prime_mu at the three smallest odd-prime pairs. Purpose: machine-check that the hypotheses are satisfiable (no hidden vacuity) and that the closure is usable downstream. All three MUST be kernel-clean.

theorem Egrs75.SmokeProbe.egrs_3_5 : {n : ℕ | ¬3 ∣ n.centralBinom ∧ ¬5 ∣ n.centralBinom}.Infinite

Infinitely many n with 3 ∤ C(2n,n) and 5 ∤ C(2n,n).

theorem Egrs75.SmokeProbe.egrs_3_7 : {n : ℕ | ¬3 ∣ n.centralBinom ∧ ¬7 ∣ n.centralBinom}.Infinite

Infinitely many n with 3 ∤ C(2n,n) and 7 ∤ C(2n,n).

theorem Egrs75.SmokeProbe.egrs_5_7 : {n : ℕ | ¬5 ∣ n.centralBinom ∧ ¬7 ∣ n.centralBinom}.Infinite

Infinitely many n with 5 ∤ C(2n,n) and 7 ∤ C(2n,n).

theorem Egrs75.SmokeProbe.egrs_two_prime_challenge_form {p q : ℕ} (hp : Nat.Prime p) (hq : Nat.Prime q) (hpo : Odd p) (hqo : Odd q) (hpq : p ≠ q) : {n : ℕ | ¬p ∣ n.centralBinom ∧ ¬q ∣ n.centralBinom}.Infinite

Comparator challenge form (2026-06-12). Byte-identical to the statement in comparator/egrs75/Challenge.lean (the leanprover/comparator workspace shipped with this development): Mathlib-vocabulary only, no project definitions. If this compiles clean, the comparator Solution bridge does too.