Erdős problem #375

Resolve the closest-prior computational artifact trail before allocating further computation.

First action: Inspect https://mathoverflow.net/questions/248146/on-comparing-two-almost-injective-divisor-maps and its EACA-slide link, including archived targets, and record every source-code, data, range, and exception artifact.

Stop or redirect when: Stop when a runnable artifact permits independent replay of the smallest claimed failure and repair, or when the public trail ends without code or certificates and park the bound-extension lane.

• Recover and audit the Brox-Paseman provisional computation artifacts.
  Follow the EACA slides and MathOverflow links; inventory code, logs, exact failures, cover semantics, and replay the smallest failure if runnable artifacts exist.
• Formalize the Hall-certificate contract or a finite interval checker in Lean.
  After disk repair, bootstrap Formal Conjectures and compile a minimal Hall-equivalence lemma with no sorry.

• isolated adversarial reconstruction
  Start from only a recovered provisional artifact and its stated range, reconstruct the smallest claimed exceptional interval using an independently written factor-divisor representation, and record the first discrepancy.
• counterexample and witness search
  Factor each composite interval, construct its position-to-prime-divisor bipartite graph, test for a perfect matching, and emit a Hall-deficient subset on failure; compare against trial division plus exhaustive Hall-subset enumeration on a smaller domain.
  Reopen only if: Resume larger counterexample scanning only with a validated novelty target, requested range, structural observable, or actual Hall candidate; resume Lean only after several GB of verified free space.

• Compile or extend the Lean formalization in the current host state.
  Cache unpacking failed with only 64 KB free disk; cleanup restored only 369 MB.
  Reopen only if: Verify several GB of free disk, rerun the prescribed bootstrap, and compile without sorry.
• Use only the number of distinct prime factors in the whole interval product.
  This checks Hall's inequality only for the full left set; a proper subset can still be deficient.
  Reopen only if: A proof that the special consecutive-integer divisor graphs make the whole-set condition sufficient for every subset.
• Treat a larger arbitrary local cutoff as a contribution.
  The accepted 2006 range and later provisional claims are vastly larger.
  Reopen only if: A counterexample, expert-requested range, validated best-bound improvement, or new structural theorem.