Selected computational definition review
This edition advances the initial queue: three of ten configurations and 41 of 65 declared definition entries received source-level comparison. The preserved observations and source hashes record each name separately. No intended-model mismatch was detected in this selection. Kernel checking, the complete import closure and program correspondence remain unverified.
What was compared
| Configuration | Entries | Selected meaning reviewed | Material application distinction |
|---|---|---|---|
| Brenier | 12 | Euclidean source, probability couplings, quadratic cost, optimal/unique plans, continuous L2 map norm and three positive atoms | A source-uniform continuum result; optimal plans/maps differ from an arbitrary discrete or regularized solver |
| KServer | 9 | Labeled tuples, causal probability simplex policy, recursive service cost, finite path expectation, attained offline infimum and quantified main statement | One existence policy for all fixed finite sequences; its distinct-start B=0 clause differs from the separately constructed uniform algorithm |
| LogspaceEquality | 20 | Binary words/languages, local heads, absorbing halt, fresh coin prefixes, counted writable cells, exact acceptance fractions and L/RL/BPL classes | Decision preservation with resource promises and acceptance gap; not random-output preservation or a selected compiler-resource proof |
The LogspaceEquality challenge and selected solution's displayed definition/structure prefix also match lexically after whitespace/comments are removed. This is a source-text control. It does not establish elaborated equality, statement validity or trusted imports. The KServer/Brenier comparisons permit ordinary binder renamings and were inspected manually; they have no machine-checked semantic equivalence certificate.
Important semantic corner cases
The Brenier uniform measure and W2 definitions are written on a broad type, while the selected theorem restricts to compact convex bodies with interior and compact probability targets. Those hypotheses exclude degenerate normalization, unavailable couplings and infinite cost; they are necessary to the interpretation. Uniqueness is at the plan/almost-everywhere map level, not equality of every pointwise prediction.
The KServer simplex contains exact real probabilities. Policy existence and the finite sum over k^h label strings are mathematical definitions, not efficient decision/evaluation routines. The separate uniform bit implementation has an unrestricted finite additive movement term and an exponentially delayed activation schedule in its constructor transition count.
Logspace counts visited cells through every finite time and on every coin tape, not only nonblank symbols or a favorable run. Input heads remain between endmarkers. Its L definition asks for a total deterministic decider without a separate polynomial clock; the paper explains polynomial time by configuration counting. The probabilistic classes explicitly impose the all-coin polynomial clock and acceptance gap. Their equality does not certify an arbitrary source program's supplied resource promises.
Detailed operational evidence, thirteen documentary contracts.
Remaining 24 entries
| Configuration | Entries | Next review focus |
|---|---|---|
| DefocusingNLS | 3 | Sobolev multiplication, Schrödinger evolution and odd-power meaning |
| ElementaryPositivity | 1 | A witness-only definition interface and its relation to the polynomial basis claim |
| EuclideanFiveColor | 1 | Unit-distance coloring domain and color-count quantification |
| Naimark | 7 | Simplicity, state/trace, representation uniqueness and compact-operator conclusion |
| OccupiedOverlap | 5 | Actual Hilbert/representation construction and endpoint meaning |
| Rokhlin | 4 | Time action, mixing and finite-order layout separation |
| SpinAngle | 3 | Row/column types and the quantitative angle function |
Comparator's documentation distinguishes accepted structural/type/axiom checks from intended semantics when definitions are supplied. See the primary documentation. The review therefore records human source observations rather than a successful mathematical certificate. No Lean/Lake/Comparator tool is present on PATH, and no source code was compiled.
Continue through these seven interfaces, inspect the declared solution and challenge under their actual hypotheses, and attach explicit source extents. Do not infer a failure merely from the existence of definition holes. Preserve this edition when deeper import/proof/program evidence arrives.