# Definition semantics before proof-run labels

The [static queue](../snapshots/2026-10-08-baseline/definition-hole-review-queue-2026-10-09-v1.json) scans all 416 Comparator configurations at the pinned revision and finds ten with nonempty `definition_names`, totaling 65 entries. Those are declared holes requiring review, not evidence of wrong definitions or failed proofs.

Comparator checks the configured definition holes' names, types, universes, safety, permitted axioms and kernel acceptance. Its documentation says intended meaning needs additional oversight because a structurally accepted definition can defeat a challenge's intent. Theorem comparison and semantic correspondence must therefore remain separate evidence records. [Comparator documentation](https://github.com/leanprover/comparator).

The queue includes KServer policy/cost/main-statement definitions, Brenier transport/cost definitions, computational-machine definitions for LogspaceEquality, and seven other configurations. Review each solution definition against its intended paper model and the trustworthy challenge/import closure. Record exact versioned files, reviewer/date, semantics, known exclusions and unresolved bridges. A nonempty hole list alone must never generate a fraud or invalidity verdict.

The current host lacks Lean, Lake, Comparator, landrun, lean4export and elan on PATH. The source pins Lean 4.34.1. No proof run occurred. Comparator's documented trust/sandbox requirements must be evaluated before running source compilation; preserve source and manifests in any fresh verification environment. The SwitchChain challenge deliberately has theorem placeholders, while its configured solution supplies theorem proofs. Those placeholders are not proof-failure evidence.

Prioritize semantic review of the computational definitions before attaching a broad algorithm-correctness label. This can strengthen the shared evidence platform's reviewer workflow, but no expert/customer benchmark or demand test has been completed.