[edemaine]

Implements #2203, stacked on #2185. One fixed 64-register native program constructs the real shared box table and computes one sparse query. The reusable query routine traverses only compatible prefixes with at most t indexed inner terms: lower-order leaves multiply the original signed words, while threshold leaves compute the canonical box key and load its retained value. Actual stack construction, expansion, dispatch, signed arithmetic and lookup are charged. No enumeration, layout, execution or timing oracle is supplied.

BoxQuery.runs_wide gives actual State.init execution, same-state prefix and charged halt, exact signed query value, and preservation outside the computed allocation. BoxQuery.runs_bilinear specializes canonical left/right encodings to the existing bilinear product when t≤m; its nonzero signed depth-one client discharges every encoding and admission premise. The generic query only requires that the ordinary output code has m inner coordinates. Width admission is the binary ceiling logarithm of original magnitude/address budgets plus three; BoxQuery.prefix_bounded bounds every wider prefix independently of physical width. The complete flat code has at most 4096 slots including halt and never reads width.

BoxQuery.queryTime_eq_alpha proves the reusable query bound 258·(L+1)·Σ(d≤t) alpha(m,d)+28. Preparation is separate: original-header adaptation 4L+21, shared geometry, and one retained tile at 328·B+8. BoxQuery.preparationTime_le retains the existing beta count; BoxQuery.allocation_le bounds geometry, retained values and the uncleared stack by 10·(L+1)·10^L+50 words beyond the input. The original magnitude envelope is A+B+10^(2L)·A·B; neither it nor the sufficient width is a runtime certificate.

Source mapping: existing finite order/partition/alpha facts come from the pinned primary formal source, Sec4/Lemma27_28, BoxesFromLeaves and Programs/Sec4/Theorem30/{QuerySum,Query,Contracts,NineNext}. This original prefix worklist replaces that source's bounded-nine successor and per-tile trie; it preserves the finite expression, not its trace or time contract. Native level zero stays least significant, with inner/P0 digit nine. All six primary files were checked against their pinned Git blobs. Supplier code is unchanged.

Validation: all new modules and the complete new test module pass targeted Lean diagnostics. Strict scoped compilation passes for the new umbrella/test and affected table test. Tests include signed initialized depth0/1, a fully admitted same-state prefix/halt/bilinear client, minimum-admission zero operands, and actual depth-two one/19-leaf query fixtures with dirty stack and frame sentinels. The depth-two fixtures consume canonical table readback; they do not rerun the whole constructor. Full hygiene/simp, canonical imports, all30-library/1-test scoped doc/test checks, environment lints, declaration names and whitespace checks pass. Hosted CI passes all six global gates and the standard changed-file checks at exact head 228eefb. Independent nonauthoring agent /root/review_sparse_box_query approved the whole own layer and the final import/proof-hygiene deltas at 228eefb, with no blocking correctness/API/source/resource findings. Its hosted-validation condition is now satisfied. The optional finite-module dependency nit was fixed and its affected clients rechecked. This is agent review, not human or platform approval.

Global all-tile reuse, native wanted-query construction, Corollary26/ET integration and the tuned 1.9992 endpoint remain #1394. This milestone changes no curated abstract, catalogue selection or rendering. AI assistance: OpenAI Codex, including implementation agents; independent review is recorded separately.

[SamuelSchlesinger]

Coordinator jetski-coord-02304a17 (Jetski): pre-refreshed onto the refreshed #2185 head (c35dc26ac, which includes current main) with merge commit a7af9000e, so CI runs early. Source and test files are byte-identical to the approved 228eefb85. This layer's Complexity.lean and UPSTREAM.md additions are line-identical to its approved diff over #2185. ROADMAP.md takes main's text: progress status is not kept there, and the open 3SUM direction remains. Manual impact: none at this layer, because the native sparse-query internals are documented at the #2342/#2357/#2358 endpoints. Agent Operator's Manual: no edit. I'll retarget to main and queue after #2185 lands, carrying the recorded approval forward.

[SamuelSchlesinger]

Coordinator jetski-coord-02304a17 (Jetski): #2185 landed, so I merged main as 21b722a92 and retargeted to main. UPSTREAM.md was union-resolved. The diff against main is line-identical to this layer's pre-refreshed delta over #2185 (c35dc26ac..a7af9000e), whose source files are byte-identical to the approved 228eefb85. I'm carrying the recorded approval forward (manual note above) and will queue on green CI.