Switch the Erdős dataset to the Bloom statement selection - #28

Both formal-conjectures repo layouts must be supported simultaneously:
the erdos pin is about to move past upstream's FormalConjecturesUtil
rename while oeis/fc100open stay at the old-layout pin.

- apn/dataset.py: FCProfile registry keyed by pin; fc_profile() fails
  loudly on unregistered pins.
- apn/lean/Dockerfile: builder guards the lean-toolchain invariant,
  detects the layout from the checkout (the ground truth) for the lake
  build, and stages the proving-library sources into /staged so the base
  stage's COPY needs no branch.
- extract_ranges: the util module is a required --util-module CLI flag
  (no default), threaded through run_extractor / lean_sandbox.extract
  and all generator/test callers via fc_profile().
- prompts/solver/task: user_prompt names the pin's util module in the
  import-integrity rule instead of a hardcoded one.

All pins unchanged; pure refactor (Gate A rides on the existing suites).

…urces

C1/C2/C6 of the migration plan: fc_commit moves to the last FC commit on
Lean v4.27.0 (21 commits before the review commit 56534c04, which is on
v4.33.1); the 236 Tsoukalas-era Sources/*.lean are replaced by the 48
files hosting Bloom's selected statements; the selection doc moves to its
permanent home under apn/data/erdos/metadata/.

scripts/erdos_statement_certificate.py is the auditable link between the
vendored pin and the review commit: it certifies every selected
declaration command byte-identical between the two (vendor-time run:
48/48; residual non-statement diffs in 8 files), and that the vendored
copies match FC at the pin. Result recorded in NOTICE.md.

samples.jsonl and Isolated/ still reflect the old dataset; they are
regenerated in the next commits (C4).

…lection

C3/C5/C7 + workstream D of the migration plan:

- scripts/erdos_isolation.py: SORRY_ALLOWLIST_FILES emptied (no Bloom file
  needs one); VERDICT_PROSE pruned to the one snippet the 48 files still
  contain (138.variants.difference's recorded-verdict prose), after
  auditing every research-solved member's doc against the new sources.
- apn_erdos defaults to subset="bloom_selection" (47 scoreable selected
  statements); subset=None remains the whole census. Docstrings rewritten.
- tests/test_erdos.py: census invariants for the new universe (one row per
  research statement of the 48 files; 508 + 975.variants.quadratic value-
  typed, 647.variants.twenty_four proved-in-file; per-form counts; the
  selection all research-open; sketch invariants unchanged in spirit).
- tests/test_singlefile_proof.py: end-to-end accept case in the erdos
  pin's scorer image (institutionalizes the pin-move smoke test: compile +
  kernel replay against the module-built FormalConjecturesUtil oleans).

samples.jsonl, Isolated/, and subsets/bloom_selection.json are regenerated
in the next commit (C4/C5); test_erdos.py census constants are asserted
against that output.

C4/C5 of the migration plan, produced by generate_erdos_isolated.py in
the generate container at 488aade2 (with the extractor's new required
--util-module flag; a Lean parse fix to its usage error rides along):

- samples.jsonl: 144 universe rows -- every research-category statement
  of the 48 vendored files. 3 excluded: Erdos508.HadwigerNelsonProblem
  and Erdos975.erdos_975.variants.quadratic (value-typed answer(sorry)),
  Erdos647.erdos_647.variants.twenty_four (complete in-file proof).
- Isolated/: 141 per-target specs; answer forms 87 plain / 52 lhs_sorry /
  2 lhs_true (the recorded verdicts un-filled), 141 category attribute
  lists and 1 verdict-prose snippet stripped.
- subsets/bloom_selection.json: the 47 scoreable selected statements
  (apn_erdos's default subset), in problem-number order.
- tests/test_erdos.py: answer-form census pinned to the generated output.

Fast suites + mypy green; the container gates (test_erdos_isolation.py,
test_singlefile_proof.py) run in CI.