Integrate accepted RMQ extensions and repair Linux verification

.gitattributes

@@ -12,3 +12,20 @@ docs/internal/E1_ARCHITECTURE_COORDINATOR_HANDOFF.md -text
 # or re-touches those lines. Reformatting the dossier is not the fix; it is
 # evidence, not maintained prose.
 docs/internal/E1_ARCHITECTURE_COORDINATOR_HANDOFF.md -whitespace
+
+# BV-1 source and replay evidence retain their exact recorded bytes on checkout.
+# The patterns are confined to this extension; no other family is affected.
+RMQ/Core/WordRAM/Bitvector/** -text whitespace=blank-at-eol,blank-at-eof,space-before-tab,cr-at-eol
+RMQ/Validation/PackedBitvector.lean -text whitespace=blank-at-eol,blank-at-eof,space-before-tab,cr-at-eol
+scripts/packed_bitvector_* -text whitespace=blank-at-eol,blank-at-eof,space-before-tab,cr-at-eol
+docs/internal/extensions/bv1/** -text whitespace=blank-at-eol,blank-at-eof,space-before-tab,cr-at-eol
+
+# These exact replay-pinned artifacts retain their recorded final blank line.
+# Other trailing whitespace and indentation checks remain enabled.
+RMQ/Core/WordRAM/Bitvector/Capstone.lean whitespace=blank-at-eol,-blank-at-eof,space-before-tab,cr-at-eol
+docs/internal/extensions/bv1/CHECKOUT_BYTES_DISPOSITION.md whitespace=blank-at-eol,-blank-at-eof,space-before-tab,cr-at-eol
+docs/internal/extensions/bv1/CHECKOUT_BYTES_LAKEFILE_DISPOSITION.md whitespace=blank-at-eol,-blank-at-eof,space-before-tab,cr-at-eol
+docs/internal/extensions/bv1/COORDINATOR_ROUTE_DISPOSITION.md whitespace=blank-at-eol,-blank-at-eof,space-before-tab,cr-at-eol
+docs/internal/extensions/bv1/controls/public_mutations/fixtures/B39CFA73CEAA05B8D0E8E803CACF0696529FDBF7F2BD3BEFB5A8805045127618/*.constructor.lean whitespace=blank-at-eol,-blank-at-eof,space-before-tab,cr-at-eol
+docs/internal/extensions/bv1/controls/public_mutations/snapshots/97405C70ED3B60CED72874D6DF622D2E9BBA0BD8F04808A3F98ED34EE1CEB770/Capstone.lean whitespace=blank-at-eol,-blank-at-eof,space-before-tab,cr-at-eol
+scripts/packed_bitvector_validation_controls.ps1 whitespace=blank-at-eol,-blank-at-eof,space-before-tab,cr-at-eol

.github/workflows/artifact-repro.yml

@@ -15,7 +15,20 @@ jobs:
       - name: Checkout
         uses: actions/checkout@11d5960a326750d5838078e36cf38b85af677262 # v4
         with:
-          fetch-depth: 2
+          # 0, not 2: the gate's [retrospective-record] leg re-derives each
+          # pre-policy commit's missing-path set by running the production
+          # checker over `<sha>~1..<sha>`, and those commits sit far behind the
+          # tip. At depth 2 they are simply absent from the clone, and every one
+          # of them failed to resolve. ci.yml already fetches full history.
+          # WDD-20260817-080.
+          fetch-depth: 0
+          # Annotated tags, explicitly. actions/checkout fetches with
+          # --no-tags when fetch-depth > 0 and fetch-tags is unset, so
+          # tag_annotation_check.ps1 found no annotated tags and failed
+          # -- correctly, since 'nothing was checked' is not a pass. The
+          # repair belongs here, not in the checker: its header says CI
+          # must not pass -AllowNoTags.
+          fetch-tags: true
 
       - name: Install tools
         run: |

.github/workflows/ci.yml

@@ -14,7 +14,16 @@ jobs:
         with:
           # The strict design-decision scan diffs against HEAD~1 on push
           # events; the default depth-1 checkout cannot resolve that base.
-          fetch-depth: 2
+          # 0, not 2: per-commit certification below walks the pushed range,
+          # and depth 2 makes anything past HEAD~1 unresolvable.
+          fetch-depth: 0
+          # Annotated tags, explicitly. actions/checkout fetches with
+          # --no-tags when fetch-depth > 0 and fetch-tags is unset, so
+          # tag_annotation_check.ps1 found no annotated tags and failed
+          # -- correctly, since 'nothing was checked' is not a pass. The
+          # repair belongs here, not in the checker: its header says CI
+          # must not pass -AllowNoTags.
+          fetch-tags: true
 
       - name: Install tools
         run: |
@@ -30,8 +39,17 @@ jobs:
           lake --version
 
       - name: Run repository gate
-        shell: pwsh
-        run: ./scripts/gate.ps1
+        # bash, not pwsh, so the stack limit can be raised first. The packed-query
+        # replay runs its runtime fixtures with `lean --run`, whose interpreter
+        # recursion needs far more than Linux's default 8 MiB main-thread stack
+        # (it fails with "deep recursion was detected at 'interpreter'"); Windows
+        # reserves a large stack for lean.exe, so the local gate never saw this.
+        # Children inherit the limit. 1 GiB is the value measured to work.
+        shell: bash
+        run: |
+          ulimit -s 1048576
+          echo "stack limit: $(ulimit -s) KB"
+          pwsh -NoLogo -NoProfile -File ./scripts/gate.ps1
 
       - name: Run strict claim-drift scan
         if: always()
@@ -42,9 +60,93 @@ jobs:
         if: always()
         shell: pwsh
         run: |
+          # PER-COMMIT, not aggregate. The repository states that every commit
+          # carries its own design-log update; running the check once over a
+          # whole range does not enforce that, because one commit's
+          # DESIGN_DECISIONS.md satisfies the membership test for every
+          # code-sensitive file in the range. WDD-20260816-043 records a commit
+          # that breached the invariant and passed CI for exactly this reason.
+          # `--depth=0` is not valid git ("depth 0 is not a positive number"), so
+          # the pull-request branch never ran. And `HEAD~1..HEAD` is a fixed
+          # ONE-COMMIT window: a push of three commits certified only the tip, which
+          # is the same blind spot this step was added to close. `fetch-depth: 0`
+          # above makes the full history available; the push range comes from the
+          # event, guarding the all-zeros SHA git uses for a new branch.
           if ("${{ github.event_name }}" -eq "pull_request") {
-            git fetch origin "${{ github.base_ref }}" --depth=1
-            ./scripts/design_decision_check.ps1 -Base "origin/${{ github.base_ref }}" -Strict
+            git fetch origin "${{ github.base_ref }}"
+            $range = "origin/${{ github.base_ref }}..HEAD"
+          } elseif ("${{ github.event.before }}" -and
+                    "${{ github.event.before }}" -notmatch '^0{40}$') {
+            $range = "${{ github.event.before }}..HEAD"
           } else {
-            ./scripts/design_decision_check.ps1 -Base "HEAD~1" -Strict
+            $range = "HEAD~1..HEAD"
+          }
+          # --no-merges. `design_decision_check.ps1` REFUSES a merge commit, because
+          # a merge's first-parent diff carries the merged branch's design log and
+          # would certify anything the merge itself introduced. That refusal is
+          # right, but `git rev-list` enumerates merges -- so without this flag the
+          # step could never pass on a pull request, where actions/checkout builds
+          # `refs/pull/N/merge` and HEAD IS a merge commit, nor on any push
+          # containing one.
+          #
+          # Residual, stated because it is real: content introduced by a merge
+          # alone -- a conflict resolution present in neither parent -- is then
+          # never certified by anything. That is the same trade DD-20260816-122
+          # already accepted when it chose refusal over judging a merge by the
+          # union of its parents.
+          $commits = @(git rev-list --reverse --no-merges $range)
+          if ($commits.Count -eq 0) {
+            Write-Host "DESIGN-CHECK: no commits in $range; nothing to certify"
+            exit 1
+          }
+          $bad = 0
+          foreach ($c in $commits) {
+            Write-Host "--- $c $(git log -1 --format=%s $c)"
+            ./scripts/design_decision_check.ps1 -Base "$c~1" -Head $c -Strict
+            if ($LASTEXITCODE -ne 0) { $bad++ }
+          }
+          if ($bad -gt 0) {
+            Write-Host "DESIGN-CHECK: $bad of $($commits.Count) commit(s) failed per-commit certification"
+            exit 1
           }
+          Write-Host "DESIGN-CHECK: all $($commits.Count) commit(s) certified individually"
+
+  owned-process-windows:
+    # The repository gate's process-ownership layer has two implementations --
+    # a POSIX setsid process group and a Windows kill-on-close job -- and only
+    # the POSIX one was ever exercised by CI, because every job here runs
+    # ubuntu.  The Windows path shipped to `audit-v1-rc-2` without a
+    # descendant-death barrier: it closed the job and waited on the root alone,
+    # so a grandchild could still be alive when a caller asserted the tree was
+    # dead.  The 2026-08-12 fresh-blind audit hit exactly that on the required
+    # Windows gate path.
+    #
+    # This job is deliberately small: it runs only the ownership self-tests, so
+    # it needs no Lean build and costs a minute, while covering the code path
+    # that a green ubuntu run says nothing about.  `-AllowInconclusive` must
+    # never be passed here; an inconclusive barrier run exits nonzero on
+    # purpose.
+    name: Owned-process ownership (Windows)
+    runs-on: windows-2022
+    steps:
+      - name: Checkout
+        uses: actions/checkout@11d5960a326750d5838078e36cf38b85af677262 # v4
+
+      - name: Owned-process self-test (Windows job ownership + descendant barrier)
+        shell: pwsh
+        run: ./scripts/owned_process_tree.ps1 -SelfTest
+
+  owned-process-posix:
+    # The POSIX twin of the job above, run standalone for the same reason: the
+    # aggregate gate reaches these assertions only after a full Lean build, so a
+    # regression in either ownership implementation should be visible in a
+    # minute rather than behind twenty.
+    name: Owned-process ownership (POSIX)
+    runs-on: ubuntu-24.04
+    steps:
+      - name: Checkout
+        uses: actions/checkout@11d5960a326750d5838078e36cf38b85af677262 # v4
+
+      - name: Owned-process self-test (setsid group + descendant barrier)
+        shell: pwsh
+        run: ./scripts/owned_process_tree.ps1 -SelfTest

.github/workflows/release-artifact.yml

@@ -17,6 +17,10 @@ jobs:
         uses: actions/checkout@11d5960a326750d5838078e36cf38b85af677262 # v4
         with:
           fetch-depth: 2
+          # This workflow also runs scripts/gate.ps1, through
+          # scripts/reproduce_artifact.sh, so it needs tags for the same reason
+          # ci.yml does. WDD-20260816-057 said "every workflow" and fixed two.
+          fetch-tags: true
 
       - name: Install tools
         run: |

README.md

@@ -7,13 +7,42 @@ story: exact range-minimum queries can be answered at constant modeled query
 cost from a Cartesian-shape payload of at most
 `2*n + o(n)` bits,
 and any fixed-length payload-only exact RMQ encoding needs
-`2n - 1.5 log n - O(1)` bits. "Modeled cost" counts charged probes into that
-payload, not machine instructions or wall-clock time, and the cost of building
-the payload is accounted separately and is not part of this bound.
+`2n - 1.5 log n - O(1)` bits. "Modeled cost" there counts charged probes into
+that payload, not machine instructions or wall-clock time. A separate
+accepted theorem, `RMQ.Headlines.succinctRMQFullyChargedPackedQuery`,
+charges every primitive instruction of its own machine query; it is
+summarized in the next paragraph. The earlier **210** trace and **427** probe
+bounds keep their separate charge policies, and none of these bounds is a Lean
+wall-clock bound. The cost of building the payload -- preprocessing time and
+workspace, in any model -- is **unproved and excluded from every query
+bound**: no theorem here bounds it, and none is claimed.
 The same code base is now growing into a
 verified advanced-data-structures testbed, with standalone rank/select,
 balanced-parentheses navigation, and union-find spokes.
 
+**Fully charged packed query (accepted).** Import `RMQPaper` and use
+`RMQ.Headlines.succinctRMQFullyChargedPackedQuery`. For every `xs : List Int`
+it fixes one numeric memory -- 174 counted metadata words followed by the
+existing packed allocation of the payload, densely repacked into `w(n)`-bit
+words with `log2(n+2)+1 <= w(n) <= 192*(log2(n+2)+1)` -- and one closed
+loop-free program of **837,572** primitive instructions that does not
+depend on `xs` or `n`. Each executed instruction is one step. Every valid
+half-open range returns its leftmost minimum, and for every representable
+endpoint pair the run halts within at most 837,572 steps, which is simply the
+program length; the committed valid-query fixtures observe 6,003 to 16,358
+steps. The memory, the literal program encoding and 8,271 registers plus three
+control words fit in `2n + o(n)` bits, but the code and scratch term exceeds
+`n` for every `n` below about `2^28`, so it is lower order only asymptotically.
+The word model assumes unit-cost multiplication, division, remainder, variable
+shifts and bitwise operations, and every executed operation is proved free of
+overflow, underflow, zero division and oversized shifts. Endpoints outside the
+word domain are rejected by an uncharged value-level check. Preprocessing is
+unbounded and unclaimed, and Lean runtime is a separate, unmeasured quantity.
+Status: **ACCEPTED**, following the replay campaign, both-host aggregate gates
+and independent audit; see the [coordinator acceptance record](docs/internal/packed_query/PQ1_COORDINATOR_ACCEPTANCE.md). The
+[machine review packet](docs/WORD_RAM_REVIEW_PACKET.md) states the full model,
+allocation/run identity and validation contract.
+
 Range-minimum query (RMQ) asks for the leftmost position of the smallest value
 in a subarray. The surprising theorem is not that RMQ can be solved, but that
 the array values can be discarded: the Cartesian shape alone determines every
@@ -64,6 +93,7 @@ for checked historical profiles under `Legacy`/`Compatibility` names.
 
 | Alias | Meaning |
 | --- | --- |
+| `RMQ.Headlines.succinctRMQFullyChargedPackedQuery` | Accepted primitive-machine theorem over ordinary `xs : List Int`, following the replay campaign, both-host aggregate gates and independent audit: one numeric memory and one closed loop-free program; exact leftmost answers for valid half-open ranges; the rejection packet `0` with no memory reads for representable invalid ranges; halting within at most 837,572 primitive instructions; every stored word, operand and prefix state within one logarithmic word width; and memory, literal program encoding and registers within `2n + o(n)` bits. Unit-cost multiplication, division, remainder, shifts and bitwise operations are model assumptions; preprocessing is unclaimed. |
 | `RMQ.Headlines.succinctRMQListIntTwoNPlusOConstantQuery` | Reader-facing theorem over ordinary `xs : List Int`: `buildPayload.length <= 2*n + overhead n` with `overhead = o(n)`; valid half-open queries return the exact leftmost RMQ answer, invalid or empty ranges return `none`, and modeled query cost is constant. |
 | `RMQ.Headlines.listIntSuccinctRMQFlatPayloadStoreNoSyntheticExecutionStory` | Reader-facing no-synthetic execution story over ordinary `xs : List Int`, including the same public space inequality and range contract. Exact physical-word erasure is also conjoined directly in the paper main theorem; the construction is not padded to manufacture a size equality. |
 | `RMQ.Headlines.listIntSuccinctRMQPaperMainTheorem` | Paper-facing theorem consuming the manifest packet, guarded reviewer-native certificate and independent 24-field required-facts projection, guarded list packet, literal same-execution `nonSyntheticWeight <= 210`, and complete supplied-store `TraceResult` equality under exact ordered dynamic-read agreement, together with the existing payload, answer, invalid-range, provenance, and no-synthetic clauses. |
@@ -209,6 +239,11 @@ At a high level, the repository currently includes:
   Catalan slack equivalent to `2n - 1.5 log n - O(1)`;
 - a payload-accounted BP-native succinct RMQ upper bound with payload length at
   most `2*n + o(n)` and constant modeled query cost;
+- an accepted primitive-machine query,
+  `RMQ.Headlines.succinctRMQFullyChargedPackedQuery`, whose numeric memory,
+  literal program and finite register bank occupy `2n + o(n)` bits and whose
+  run charges every executed primitive instruction, within a fixed budget
+  equal to its loop-free program length (validated by replay, both-host aggregate gates and independent audit);
 - an interpreter-backed final succinct RMQ query surface whose all-size
   execution story emits one global `WordRAM.TraceEvent` stream; every event is
   a payload `readWord`, as checked by
@@ -226,7 +261,14 @@ At a high level, the repository currently includes:
 The cost statements are model-relative. They use a small `Costed` layer and a
 traced RAM substrate with unit-cost indexed reads, word operations, branches,
 comparisons, and table accesses where explicitly modeled. They are not claims
-about Lean's executable `List` runtime.
+about Lean's executable `List` runtime. The `210` charged-trace and `427`
+packed-probe theorems leave controller dispatch, decoding, arithmetic and
+branching uncharged. The separate accepted theorem
+`RMQ.Headlines.succinctRMQFullyChargedPackedQuery` uses a different execution:
+a register machine over numeric memory whose nine instruction forms (load,
+constant, move, arithmetic, comparison, jump, register jump, branch-if-zero,
+halt) each cost one step, with unit-cost multiplication, division, remainder,
+variable shifts and bitwise operations on `w(n)`-bit words.
 
 The space statements count payload bits separately from proof-only fields and
 certificates. The succinct RMQ theorem counts the balanced-parentheses shape
@@ -335,7 +377,8 @@ imports, this material):
 - [`docs/TRUST_AUDIT_PACKET.md`](docs/TRUST_AUDIT_PACKET.md): skeptical-review
   packet for the headline theorem.
 - [`docs/WORD_RAM_REVIEW_PACKET.md`](docs/WORD_RAM_REVIEW_PACKET.md): focused
-  review packet for the first-order Word-RAM anti-oracle boundary.
+  review packet for the accepted primitive-machine query and for the
+  first-order Word-RAM anti-oracle boundary of the charged-trace theorem.
 - [`docs/TRUST_BASE.md`](docs/TRUST_BASE.md): dependency policy, model
   glossary, and verification commands.
 - [`docs/FAMILY_SUMMARY.md`](docs/FAMILY_SUMMARY.md): full theorem inventory,
@@ -363,11 +406,10 @@ package, calibrate, and reuse the infrastructure:
    stories where that materially clarifies theorem surfaces;
 2. push the union-find spoke from the current sequence/event scorecard toward a
    true inverse-Ackermann amortized theorem over strict residual events; and
-3. have E1 define a richer instruction semantics and prove that it simulates
-   the same canonical execution while charging controller work; the current theorem deliberately
-   provides no parallel controller-operation vocabulary; the M1 reviewer-native
-   adequacy candidate remains word-addressed over the supplied store, while S1
-   serialized-payload querying and complete preprocessing remain separate; and
+3. package the accepted primitive-machine query
+   `RMQ.Headlines.succinctRMQFullyChargedPackedQuery` with its replay and audit
+   evidence; preprocessing cost, extraction and production serialization
+   remain separate targets; and
 4. promote shared cost, refinement, lower-bound, and amortized-analysis pieces
    into a more neutral library surface only when concrete reuse demands it.
 

RMQ.lean

@@ -67,6 +67,8 @@ import RMQ.Core.SuccinctFinal.RAM.PackedCellProbe.ExecutedUniverse
 import RMQ.Core.SuccinctFinal.RAM.PackedCellProbe.Boundaries
 import RMQ.Validation.EGCPFinalFalsification
 import RMQ.Validation.EGCPStageA
+import RMQ.Validation.PackedQueryContract
+import RMQ.Core.WordRAM.Packed.ArrayRun
 import RMQ.Core.SuccinctFinalModelAdequacy
 import RMQ.Core.SuccinctRankSelect
 import RMQ.Core.BPCloseNavigation