Evidence work still open#
These are unresolved provenance or checking tasks, not undocumented solver algorithms. The original records remain available and retain their limitations.
Task |
What is needed to close it |
|---|---|
Published QF_LRA tables |
Identify exact Primo commits, manifests, commands, and raw artifacts for Tables 1–2 in the September 2026 paper; verify every aggregate against the ledger. The report currently supplies publication-level results only. |
Quantifier reference-less UNSAT answers |
Resolve the nine unconfirmed answers in the historical pool-check record, or retain them as explicitly unconfirmed. Do not infer confirmation from a later unrelated gate. |
Quantifier export trust |
Independently check the conservative-extension conditions of witness exports if proof-like validation is required. The current checker trusts that export contract; see the checking argument. |
Historical records with missing metadata |
Preserve the original evidence status and name the missing command, revision or artifact. Do not backfill guesses or count them as qualification. |
Results-storage migration is separate work. Changing the storage format would not supply missing experiment identities or strengthen an incomplete correctness check.
Publication preparation inspection, 2026-10-02#
The ledger at f95ba8a contained 709 historical/qualification entries. Searches
for the published QF_LRA aggregate values and likely local paper/tuning artifact
directories did not establish a matching experiment identity. A numerical
substring hit in an unrelated incremental-UF record was rejected as evidence.
The paper report therefore retains its publication-level attribution and makes
no raw-artifact reproducibility claim. The owner may have the tuning manifests
and measurements elsewhere; no values or commit identities have been guessed.