This guide gives one reviewer path through the artifact. It complements the compact claim packet in CLAIMS.md, the paper correspondence table in ../docs/PAPER_CLAIM_CORRESPONDENCE.md, and the code-orientation map in ../docs/CODE_MAP.md.

• Lean toolchain managed by elan, pinned by lean-toolchain to leanprover/lean4:v4.22.0.
• lake, supplied by the Lean toolchain.
• bash for scripts/reproduce_artifact.sh.
• rg for reviewer and hygiene scans.
• git for whitespace checks.
• pwsh or Windows PowerShell for scripts/gate.ps1. The reproduction script requires this in CI; outside CI it reports a skipped PowerShell gate if pwsh is not available.

The artifact is intended to run without Mathlib. Network access should not be needed once the pinned Lean toolchain and Lake dependencies are available.

From the repository root:

bash scripts/reproduce_artifact.sh

Expected successful output includes these section headers:

== Tool versions ==
== lake build ==
== public root builds for axiom checks ==
== classic RMQ concrete validation ==
== classic RMQ executable cost harness ==
== headline axiom check ==
== WordRAM axiom check ==
== full axiom check ==
== full repository gate ==
== forbidden source tokens ==
== forbidden reduction shortcuts ==
== whitespace dirty-tree diff check ==
== whitespace committed-patch diff check ==
Artifact reproduction completed successfully

The forbidden-token sections should print:

No forbidden source tokens found
No forbidden reduction shortcuts found

Rough timing is environment-dependent and dominated by lake build plus the public root builds. Reviewers should record wall-clock time with the command their shell provides, for example:

time bash scripts/reproduce_artifact.sh

On a warm checkout, later root builds may reuse Lake artifacts from the first full build. On a cold checkout or a machine that must install the Lean toolchain first, the first run may be substantially slower.

If the full reproduction script is unavailable because bash or pwsh is missing, run the explicit component checks below from the repository root and record the blocker.

lake build
lake build RMQPaper
lake build RMQHub
lake build RMQRankSelect
lake build RMQBPNavigation
lake build RMQUnionFind
lake build VerifiedDS
lake build RMQArchive
lake build RMQExamples
lake build RMQ.Core.GenericSelectBPCompat
lake exe rmq_succinct_classic_validate
lake exe rmq_succinct_classic_cost_harness
lake env lean scripts\headline_axiom_check.lean
lake env lean scripts\wordram_axiom_check.lean
lake env lean scripts\axiom_check.lean
powershell -ExecutionPolicy Bypass -File scripts\gate.ps1
git diff --check

The two forbidden-token scans are:

rg -n "\b(sorry|admit|axiom|unsafe|opaque|implemented_by|partial|extern|noncomputable)\b|import Mathlib" RMQ lakefile.toml
rg -n "native_decide|Lean\.ofReduceBool" RMQ

Expected result for both scans: no matches.

The fastest theorem-surface inspection route is:

lake env lean scripts\headline_axiom_check.lean
lake env lean scripts\wordram_axiom_check.lean
lake env lean scripts\axiom_check.lean

These scripts print curated #print axioms results for the public headline theorems, the WordRAM/read-store boundary, and the broad repository gate. The expected result may include Lean's ordinary logical axioms such as classical choice or propositional extensionality. It should not include sorryAx, Lean.ofReduceBool, or project-specific axioms.

The narrow paper import root is:

lake build RMQPaper

The main paper-facing names to inspect are listed in ../docs/PAPER_CLAIM_CORRESPONDENCE.md. Short public aliases live in ../RMQ/Headlines/RMQ.lean; the aggregate full-repository alias barrel remains ../RMQ/Headlines.lean. Construction-heavy source theorem names and files are in the correspondence table.

The proof trust base is Lean kernel checking of committed theorem declarations under the pinned toolchain. The public theorem surface proves, among other things:

• exact half-open leftmost RMQ answers for the list-facing succinct RMQ theorem;
• buildPayload.length <= 2*n + overhead n, with overhead = o(n), for the advertised succinct construction, without padding to force equality;
• model-level constant query cost, not Lean runtime or compiled-code performance;
• a final global trace with no synthetic cost-only marker events;
• one pre-execution physical word list erasing exactly to the public SuccinctClassic.buildPayload, organized by one exhaustive typed 22-source universe over logical segments 0..22, with BP roles 0 and 19 sharing one physical source and canonical close included;
• genuine supplied flat-physical execution through the existing evaluator and a checked address-translation adapter, preserving results, cost, ordered successful and failed reads, repetitions, and footprint;
• complete physical-execution equality under agreement on the first execution's consumed ordered footprint, plus a checked consumed-address disagreement witness showing that the supplied store is not ignored;
• indexed occurrence provenance for the exact current query through the program instruction, folded pre-state, component-local occurrence, invocation parameters, and multiplicity-preserving offset; separately, one query-independent manifest packet proves every counted source and shared-BP consumer has some successful closed-valid whole-query witness, and rejects rejected fresh segment 23 with the common predicate plus a checked positive-to-mutation bridge;
• coherent rejection of empty, reversed, and out-of-bounds ranges across the canonical, supplied-store, trace, and costed list surfaces;
• a linear reviewer capacity and query-independent logarithmic word width bounding physical words, physical addresses, and primitive operands/results;
• the checked principled all-size charged-trace query cap 210: the strong theorem RMQ.Headlines.succinctRMQWholeQueryGlobalWordTraceResultReadWordOnly proves every actual event is readWord, and direct event weights equal both emitted trace length and the same execution's modeled cost;
• as an accepted result following the replay campaign, both-host aggregate gates and independent audit, RMQ.Headlines.succinctRMQFullyChargedPackedQuery: one numeric memory and one closed loop-free primitive program whose run halts within at most 837,572 primitive instructions for every representable endpoint pair, returns the leftmost minimum on valid ranges, and fits memory, literal program encoding and registers in 2n + o(n) bits, under a word model with unit-cost multiplication, division, remainder, shifts and bitwise operations; and
• an information-theoretic Catalan/Cartesian-shape RMQ lower bound.

Earlier cost and dispatch theorems remain available only through the explicit compatibility history. They are not the canonical reviewer route described by this guide.

lake exe rmq_succinct_classic_validate runs executable validation for the classic public succinct RMQ API. lake build RMQExamples checks small external import examples.

lake exe rmq_succinct_classic_cost_harness prints a compact reviewer-facing report for deterministic fixtures: input size, half-open query windows, returned answer, reference answer, canonical same-block/cross-block route, the exact 21-case registry, uniform 210 charged-trace bound, and the modeled queryCosted.cost trace/event count. The registry records historical pre-cost, current post-cost, answer, route, and disposition under unique stable IDs. Controller work is uncharged in the charged-trace model this harness reports, and the harness is not a conventional word-RAM runtime benchmark. The accepted primitive-machine query has its own runtime fixtures inside scripts/packed_query_replay.ps1, which the aggregate gate runs on a clean committed tree; they report primitive steps and reads, not wall-clock time.

The cost harness has an opt-in construction profile for larger experiments:

lake exe rmq_succinct_classic_cost_harness -- --profile-size N

This profile mode is not part of the default artifact gate. It emits phase markers around the current public List Int construction/query path so a reviewer can separately time construction experiments without confusing Lean runtime with the checked model-cost theorem.

Validation and examples are useful reviewer smoke tests. They are not part of the proof trust base, and they do not replace Lean kernel checking of theorem declarations.

The artifact does not claim:

• any model claim about compiled Lean runtime performance;
• compiler correctness;
• CPU, cache, or memory-hierarchy semantics;
• extraction or benchmarking;
• production serialization;
• optimized constants;
• preprocessing time or space from the query-only theorems; the separate lifecycle model supplies its own construction and retained-capacity bounds;
• attainment or tightness of any budget, including the 837,572-instruction budget of the accepted theorem RMQ.Headlines.succinctRMQFullyChargedPackedQuery;
• an exact or minimal dynamic read set; or
• unqualified priority status for the mechanization.

AI assistance and ADD records are workflow/provenance evidence, not proof objects. See ../docs/AI_ASSISTED_DEVELOPMENT_NOTE.md and ../docs/ADD_PROVENANCE.md.