A248380 / Sylver Coinage after 16 — odd replies closed, even branches remain

Durable handoff

The known odd-reply reduction has been formalized in Lean and committed in DomTheDeveloper/formal-conjectures.

• Draft PR: https://github.com/DomTheDeveloper/formal-conjectures/pull/97
• Branch: agent/a248380-odd-reply-reduction
• Commit: daadd7e34ff9fa7bb4849440e10f7f4cce18ce9f
• File: FormalConjectures/Other/SylverCoinageOddReply.lean

Established reduction

1. Every odd q is coprime to 16.
2. For every nonterminal odd reply q > 1, Hutchings's two-generator theorem implies {16, q} is an N-position for the original first player.
3. The remaining odd reply q = 1 loses immediately by the defining rule of Sylver Coinage.
4. Therefore every odd reply to the opening move 16 is eliminated.

Exact remaining target

The full value A248380(16) is still unresolved. Continue only with legal even replies and construct a complete minimax/winning-strategy certificate for them. The Lean file does not formalize the full game or prove Hutchings's theorem; it packages the specialization as a reusable reduction.

Verification status

The source is committed and the Formal Conjectures PR build is queued. Do not call it kernel-green until the pinned Lean 4.27.0 build completes successfully.

Any parallel solver working on Sylver Coinage after 16 should begin from this reduction and avoid redoing the odd-reply analysis.