Proposal: normalized post-opening API for Catch-Up

### Background

The Catch-Up conjecture was added in #1324 and is currently formalized in `FormalConjectures/Paper/CatchUpConjecture.lean` using an evaluator whose state records both players' absolute scores.

Before opening a PR, I would appreciate guidance on a small proof-oriented extension of that formalization. This proposal does **not** claim a new case of the conjecture or a reduction theorem.

### Proposed first PR

The proposed PR would modify only the existing Catch-Up file and add approximately 230 net lines. It would:

- define a normalized post-opening `Position` using the remaining counters and the current player's score deficit;
- define the normalized one-pick transition and recursive evaluator;
- prove that the normalized evaluator agrees with the existing absolute-score evaluator when the current player is not ahead;
- expose the existing game value through normalized post-opening positions;
- add elementary API for adjoining the four counters immediately above `N`, together with small regression tests.

The main evaluator-correspondence proof is approximately 44 proof lines. All new results would be tagged `category API` or `category test`, and the existing open conjecture would remain unchanged.

### Explicitly out of scope

This first PR would not include:

- an absolute `GamePosition` carrying the player to move;
- `CanAvoidLoss`, strategy semantics, or reachability;
- exact-search or comparison scripts;
- certificates;
- a proposed `N ↦ N + 4` theorem;
- any claim that a new instance or family of the conjecture has been proved.

### Motivation

The normalized state removes irrelevant translation of both scores by the same constant. Proving agreement with the existing evaluator would ensure that later experiments use the same game semantics as the conjecture statement rather than a separate computational model.

### Questions for maintainers

1. Is this amount of problem-specific API appropriate in the existing `FormalConjectures/Paper` file?
2. Given the repository's guidance about longer proofs, is the evaluator-correspondence proof acceptable here, or should this development live externally or in another location?
3. Should the elementary four-counter API be included with the normalized evaluator, or deferred to a separate follow-up?
4. Is the proposed scope small enough for a first PR, or would you prefer a still smaller slice?

The current local version passes `lake --wfail build`. I will wait for guidance on scope and placement before preparing the PR.

AI assistance disclosure: I developed the Lean code interactively with Codex, reviewed the resulting definitions and proofs, and will include the same disclosure in any PR description.

Start by reading FormalConjectures/Paper/CatchUpConjecture.lean and the repository guidance on longer proofs; the issue reports that lake --wfail build currently passes. Done means adding the normalized Position, transition, evaluator correspondence, existing game-value API, and four-counter API with regression tests, without changing the conjecture or adding the listed out-of-scope work.

Written by the indexing model from the issue text.