## Pre-submission checklist ### Lean artifact - [x] `Score/DeterministicScore.lean` compiles with `lake build` (Lean 4.25.2 + Mathlib v4.25.2) - [x] Zero `sorry`, zero `admit` - [x] 51 theorems verified - [ ] Pin final commit hash in `artifact.md` - [ ] Attach build log to supplementary material ### Rust artifact - [x] `cargo test -p ruvector-core` — 238 passed, 0 failed - [x] 19 deterministic-score-specific tests pass - [ ] Pin final commit hash in `artifact.md` - [ ] Attach test log to supplementary material ### Paper - [ ] Download official `lipics-v2021` v2021.1.3 and build PDF with `make paper` - [ ] Verify page count ≤ 16 (excluding references), no appendix - [ ] Run `make validate` — claims and scope checks pass - [ ] Anonymize for lightweight double-blind: no author names, own-work cited in third person - [ ] Anonymize supplementary material ### Venue - [ ] Re-verify ITP 2026 CFP is still open and format hasn't changed - [ ] Decide GenAI disclosure per final venue policy (`ai-use.md`) ### Final - [ ] Update theorem count if any theorems added/removed since last check - [ ] Sync `artifacts/lean/` and `artifacts/rust/` copies with latest source
Pre-submission checklist
Lean artifact
Score/DeterministicScore.leancompiles withlake build(Lean 4.25.2 + Mathlib v4.25.2)sorry, zeroadmitartifact.mdRust artifact
cargo test -p ruvector-core— 238 passed, 0 failedartifact.mdPaper
lipics-v2021v2021.1.3 and build PDF withmake papermake validate— claims and scope checks passVenue
ai-use.md)Final
artifacts/lean/andartifacts/rust/copies with latest source