diff --git a/research/paired-log-phase-query-bound/README.md b/research/paired-log-phase-query-bound/README.md
new file mode 100644
index 0000000000..0c7957111a
--- /dev/null
+++ b/research/paired-log-phase-query-bound/README.md
@@ -0,0 +1,316 @@
+# A phase-query bound for matched paired-log decoders
+
+We prove that four independent matched P112 query swaps require at least
+**555 single-array phase events** in the model below, even with shared
+linear processing, COPY, CLEAR and private scratch. For one bank we obtain
+139. We allow physical scalar mixing between different canonical frames.
+
+Under the declared completed-log budget, we can afford at most 497 additional
+rank-one calls at the comparison saving. The proposed matched primitive
+therefore cannot close that budget in this alphabet. We leave the selected
+multiplication exponent unchanged.
+
+The new contribution combines an averaged nonzero-defect rank inequality,
+a common Pauli-trivial tensor sector, and the exact P112 target calculation.
+We build on eumemic's [PR288, Section 1.2](https://github.com/CrocSwap/integer-mult-bounds/pull/288)
+and Ali Romman's [PR468](https://github.com/CrocSwap/integer-mult-bounds/pull/468)
+for compact-WY/causal factorization, image and row spans, character
+specialization and Sylvester rank inequalities. We do not claim those
+ingredients as new.
+
+## Model and claim boundary
+
+Fix a payload dimension m and tensor length lambda. Each physical role
+contains one array in `(C^(2^m))^tensor(lambda)`. An exact fixed straight-line
+program may use:
+
+- Constant complex linear maps on the **role coordinates**, tensored with
+  the payload identity. We include COPY, CLEAR, zero-initialized scratch,
+  discarded temporaries, and any number of restored dirty roles.
+- Uniform tensor Paulis `P^tensor(lambda)` on individual roles.
+- Paid application to one role of `G^tensor(lambda)`, where G is a product
+  of the commuting directional phases
+
+      C_q = (1+i)I/2 + (1-i)X_q/2.
+
+Here X_q translates the m-bit address by q. The Fourier multiplier of C_q
+is `i^(q dot u)`, with the binary dot product read as 0 or 1. We absorb
+fixed scalar factors into the constant linear maps. A nontrivial phase
+event has nonzero binary symmetric polar; Pauli-only events do not count.
+
+The lower bound applies to programs that implement the target for all
+sufficiently large tensor lengths. We use witnesses at arbitrarily large
+multiples of four. A program and its constant coefficients may depend on
+lambda; the argument applies at each such witness length.
+
+We exclude data-dependent branching, nonlinear arithmetic, arbitrary
+payload-coordinate linear maps, independently chosen per-layer Paulis,
+and noncommuting payload adapters. We also exclude a new child interface
+that acts on several roles as one oracle. A researcher proposing one must
+specify its action and price before comparing costs.
+
+Our endpoint is four coherent copies of the matched query swap defined
+below. We do **not** identify the complete mixed-chart inverse in
+[PR1998](https://github.com/CrocSwap/integer-mult-bounds/pull/1998) with
+this endpoint. The result rules out this proposed implementation strategy;
+it does not settle every terminal decoder or integer multiplication algorithm.
+
+## 1. A causal rank inequality with singular free maps
+
+Consider a family of scalar-specialized programs indexed by chi. Replace
+each phase query by identity and call the resulting baseline map M0. There
+are k nontrivial events. At event j, let alpha_j be the query multiplier
+minus one, so alpha_j is 0 or -2 in the real character sectors used below.
+
+Unroll the constant linear computation. Let V_j map the genuine inputs
+to event j's baseline read, and let U_j propagate an injection just after
+event j to the declared outputs. Let H_ji propagate event i's injection to
+event j's read, for i<j. Chronology makes H strictly lower triangular.
+If q collects the actual prequery reads, then
+
+    q = V x + H D_alpha q,
+    M_chi - M0 = U D_alpha (I-H D_alpha)^-1 V.          (1)
+
+The inverse is a finite triangular series. We need no inverse for a free
+map. Clean ancillas add zero rows to the input embedding; discarded
+temporaries disappear under output projection. COPY and CLEAR remain
+constant linear operations, so (1) includes them.
+
+Let S be the active events and t=|S|. Restricting (1) gives
+
+    M_chi-M0 = U_S A_S V_S,
+
+where A_S is triangular with diagonal -2 and therefore invertible. Define
+d_image as the dimension of the span of the images of all target differences
+M_chi-M0, and d_row as the analogous row-space dimension. Equation (1) gives
+`rank U >= d_image` and `rank V >= d_row`. Deleting k-t columns or rows
+reduces rank by at most k-t. Sylvester's inequality now gives
+
+    rank(M_chi-M0) >= d_image+d_row-2k+t.              (2)
+
+If each nontrivial event is active on half the characters, average (2):
+
+    k >= (2/3)(d_image+d_row-R_average),              (3)
+
+where R_average is the average target-difference rank. An upper bound on
+R_average gives a valid lower bound in (3). We impose no restriction on
+intersections among the event supports and no bound on scratch space.
+
+PR288 already uses compact-WY factorization and both span directions for
+a target-zero character argument. Here we retain the nonzero target rank,
+average over characters, and extend the causal factorization to singular
+free programs before applying it to the matched decoder.
+
+## 2. Real characters in a common Pauli-trivial tensor sector
+
+An unrestricted character average would miscount a free Pauli. For example,
+a free X on one scalar role has nonzero differences in half the ordinary
+Fourier characters. We instead construct a subspace on which **all** allowed
+uniform tensor Paulis act as identity. Thus role-dependent free Paulis cause
+no character-dependent free mixing in (1).
+
+Modulo translations, the commuting phase group has binary symmetric polar
+
+    C_q -> q q^T,
+
+and the polars generate the full symmetric matrix space over F2. For a
+linear functional L on that space, write
+
+    L(q q^T) = sum_i a_i q_i + sum_(i<j) b_ij q_i q_j.
+
+Choose a tuple of Fourier frequencies as follows. Include `e_i+e_j` once
+for each b_ij=1. If degree_i counts those incidences, include
+`(2a_i-degree_i) mod 4` copies of e_i. Pad with zero frequencies to a common
+length lambda divisible by four. A length of at least
+
+    binomial(m,2)+3m
+
+suffices. Each coordinate count is even, so the total frequency XOR is zero.
+The exact parity expansion modulo four gives
+
+    C_q^tensor(lambda) -> (-1)^L(q q^T).
+
+Uniform tensor X operations act as identity because that total XOR is zero.
+Now sum the corresponding Fourier basis vector over all simultaneous
+frequency translations by v in F2^m. This is a nonzero orbit sum, fixed by
+every uniform tensor Z. If q dot v=1, the phase count changes from n to
+lambda-n; since lambda is a multiple of four and n is even, its value modulo
+four stays unchanged. Hence the orbit sum retains the desired phase character.
+
+We obtain all real polar characters at the **same** tensor length, inside
+one common Pauli-trivial subspace. Padding with four zero frequencies
+extends the construction to arbitrarily large permitted lengths. Each
+nonzero polar evaluates to -1 on exactly half these characters, as required
+by (3). This includes higher-rank commuting phase children on one array:
+after specialization they still change just one role coordinate.
+
+We never expand `C_q^tensor(lambda)` as a two-term sum of uniform tensor
+translations. That identity would be false for lambda>1.
+
+## 3. Exact matched query target
+
+Partition v data ports into r selected coordinates a and v-r ordinary
+coordinates b. Introduce r independent log coordinates z, with each z_i
+in the same hole gauge as a_i. For the pinned P112 minor,
+
+    R'=[I B],  P'=(I,0)^T,  Z'=(-12I,B^T)^T,
+    BB^T=13I,  v=112,  r=8.
+
+The source is Ali Romman's unchanged `native-source-codes` loader and its
+frozen archive. We use selected ports `[0,7,20,23,86,93,108,111]`.
+The matrix B has 416 nonzeros, all +/-1/2, and no zero row or column.
+
+The query swap sends
+
+    Y'=(I-Z'R')Y+P'z,  z'=R'Y.
+
+Writing beta=13, its constant role matrix is
+
+    T(B) = [ beta I    (beta-1)B      I ]
+           [ -B^T     I-B^T B        0 ]
+           [ I        B              0 ].
+
+In a real character sector the hole gauges are signs. Put
+`D=diag(D_A,D_B,D_A)` and `B'=D_A B D_B`. The physical target is
+`D T(B) D = T(B')`; its baseline is T(B). Put E=B'-B. Direct subtraction gives
+
+    Delta = [ 0       (beta-1)E                  0 ]
+            [ -E^T    -B^T E-E^T B'              0 ]
+            [ 0       E                         0 ].
+
+After removing dependent selected rows and zero log columns, the remaining
+block reduces by invertible row and column additions to
+`[[0,E],[-E^T,0]]`. Therefore
+
+    rank Delta = 2 rank E <= 2r.                    (4)
+
+We next prove `d_image=d_row=v`. Write P_q=q q^T. Distinct unordered pairs
+of the 112 hole labels have distinct nonzero differences P_q+P_p. One can
+check the 6,216 pairs directly. For a general justification, a dependence
+among at most four distinct nonzero rank-one symmetric polars would give
+`Q Q^T=0`; Sylvester's inequality forces rank Q<=2, which contains at most
+three distinct nonzero binary vectors. The smaller cases follow as well.
+
+For each nonzero B_ij, the Fourier coefficient of Delta at the unique
+selected-ordinary pair character is
+
+    B_ij [ ((beta-1)e_ai+e_zi)e_bj^T - e_bj e_ai^T ].
+
+Its image spans `((beta-1)e_ai+e_zi,e_bj)`, and its row space spans
+`(e_bj^T,e_ai^T)`. Fourier coefficients are linear combinations of the
+character evaluations. Since B has no zero rows or columns, these
+coefficients give v independent directions on each side. The block formula
+also confines every image and row space to those respective v-dimensional
+spaces. Thus the dimensions equal v.
+
+Equations (3) and (4) yield
+
+    k >= ceil(4(v-r)/3).
+
+For P112 this is 139. For four independent banks, the dimensions add to
+448 on each side and the rank upper bound becomes 64. Even if the program
+shares scratch and mixes the four banks, it needs
+
+    k >= ceil((2/3)(448+448-64)) = 555.              (5)
+
+We claim a lower bound, not an optimal 555-event construction.
+
+## 4. Coherent cover routes and price comparison
+
+For the actual coherent port route D_s, `rho_s(p)q_p=q_p`. On the chosen
+Pauli-trivial sector the payload translations disappear, while owner
+reindexing is a constant permutation of expanded role coordinates. It
+commutes with the diagonal hole signs, because the source owner
+`d rho_s(p)` has normal `d q_p`. Hence a coherently routed target is a
+constant conjugate of a direct sum of the preceding targets, with q replaced
+by d q in each cover block.
+
+The image and row dimensions scale by the cover size, as does the rank
+bound. A uniform full-cover program therefore still needs at least 555
+events per four-bank cover sweep. For a nonuniform program the average
+lower bound is 554+2/3 events per cover element. Cross-owner constant linear
+mixing does not change the argument. We require four such coherent target
+endpoints; arbitrary products of different intermediate charts need a
+separate analysis.
+
+For the conditional completed-log model, take m=73, W=968, fixed profile
+
+    {1:21204, 2:4500, 3:3744, 4:1170, 5:738, 8:16, 9:40,
+     16:32, 17:16, 24:8, 32:16, 33:8, 40:8, 48:48, 49:8}
+
+and idle mass 14,778. These are declared comparison inputs from the earlier
+uniform-log investigation, not a new hosting certificate. We put the idle
+mass at the allowed cap 51 to give a favorable lower moment. At
+
+    a = 67018507072324140917/40000000000000000000000,
+
+the unnormalized allowance lies strictly between 500.73765694042 and
+500.73765694043. We can fit 497 additional rank-one calls; 498 fail.
+The verifier encloses these inequalities with the pinned exact arithmetic
+from Douglas Colkitt's `complex-local-word-ceiling` package.
+
+Every ordinary single-array phase event has native rank at least one.
+Higher-rank commuting children cost more than rank-one children at this
+fixed width, so they cannot evade (5). A rank-additive batch of several
+events also cannot fit: even its rank mass is at least 554+2/3 per cover,
+above the allowance, and each rank unit has moment price at least one.
+We make no claim for a new joint child interface with a different charge.
+Sharing the decoder with already counted earlier work would also change
+the stated appended-terminal comparison and requires a new full invoice.
+
+## Reproduction and evidence
+
+From the repository root, using Python 3.12 and its standard library:
+
+```sh
+python3.12 scripts/research_package.py --package research/paired-log-phase-query-bound
+```
+
+Direct optimized replay:
+
+```sh
+python3 -I -O -B research/paired-log-phase-query-bound/verify.py
+```
+
+We check 96 exact character maps from 12 constant linear programs containing
+48 singular COPY/CLEAR steps, against an independent direct execution. We
+exhaust 64 Pauli-trivial characters at tensor length 12, with 3,584 exact
+phase checks. We reconstruct the actual source minor, check all 6,216 pair
+characters, certify the two 112-dimensional spans and compare 57 exact
+target differences with the block formula. Exact rational ranks of E and
+modular lower certificates corroborate (4); the written block elimination
+proves it for all characters. The generic average theorem and the general
+tensor-sector construction are proofs, not extrapolations from these samples.
+
+Controls cover omitted causal propagation, a nontrivial Pauli sector,
+duplicated hole labels, unmatched log gauges, neutral events and understated
+costs. Checks use exceptions and remain active under `-O`. We have not
+formalized the proof in a proof assistant or audited the full multiplication
+theorem.
+
+## Open next questions
+
+- Can noncommuting payload adapters yield a cheaper matched query swap?
+  They can move between the character sectors used here. A researcher can
+  start with one explicit address-linear adapter between two phase events,
+  then check the tensor-valid endpoint and complete price. We have no such
+  construction.
+- Can a different terminal endpoint or shared earlier work close the
+  paired-log controller? A researcher must derive its exact physical map
+  and full invoice before applying this bound. The mixed-chart observation
+  theorem alone does not specify an admitted native implementation.
+
+## Attribution
+
+Jose Manuel (@jmbarrancoml), with substantial OpenAI Codex assistance in
+mathematics, implementation and prose. Mathematical collaborators checked
+the causal expansion and target identities; the primary agent implemented
+the replay. We have not obtained independent human review.
+
+We credit eumemic (#288) and Ali Romman (#468) for the rank-factorization
+and span methods; Ali Romman (#1862/#1969) for source codes and exact
+phase/route conventions; Rohan Arun (#1931) for the local source-word
+continuation; and Douglas Colkitt for interval arithmetic. Jeremy Diviney's
+#836 addresses unitary or gauged mixing in a broader frame setting; our
+arbitrary constant role-linear maps and restricted commuting-phase alphabet
+give a different scope. We retain the original files and their notices.
diff --git a/research/paired-log-phase-query-bound/SOURCES.json b/research/paired-log-phase-query-bound/SOURCES.json
new file mode 100644
index 0000000000..a6733763dc
--- /dev/null
+++ b/research/paired-log-phase-query-bound/SOURCES.json
@@ -0,0 +1,26 @@
+{
+  "schema_version": 1,
+  "base_commit": "e112d71c8d7bb32435debcc54df932593dd8223a",
+  "files": [
+    {"path": "docs/research/agent-task-catalog.json", "usage": "provenance", "git_blob": "06c96f5579bb67ed1b86d334e78fbed7da6945f1", "sha256": "6686ad58f1fbdbc87134a78901b60fd53a20d3984355e91defbbebc9e9fa8075"},
+    {"path": "certificates/selected-result.json", "usage": "provenance", "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32"},
+    {"path": "research/native-source-codes/source_data.py", "usage": "input", "git_blob": "c9d465ed47500304bef65fcb588befe356c5cf09", "sha256": "d23924511e3aed41e5e64511ca70126a636d91c8aa02e656cb61d6ceca1fe0a0"},
+    {"path": "research/community-frontier1042-audit/selected-replay.tar.gz", "usage": "input", "git_blob": "6f4dc6fe7631d8aacf8081fcaecf32197181685b", "sha256": "22c3f4dce4b897a1d423d1388801933e288b6a6b1906cb15e1b16a5eb68db754"},
+    {"path": "research/complex-local-word-ceiling/ceiling.py", "usage": "input", "git_blob": "6c0f54527d879396f689523bfde19928a9b6157c", "sha256": "86a1432870b3b21d8454106ec9162fddc0471472d9214c590a1420f2426cedfc"},
+    {"path": "research/abelian-cayley-metric-scope/sources/pr288-README.md", "usage": "provenance", "git_blob": "dc04f533bd0f3b185969bb259e876a73714f7285", "sha256": "c091e98c415e2a80bb28402b789363eb97dd3492061ca8875e421ae437de7482"},
+    {"path": "research/bit-three-register-lower-bound/README.md", "usage": "provenance", "git_blob": "25e41c370c101a33a6deb978de08b03ed7539b79", "sha256": "c12b33ef388deece0cbf891505a2ce2c0779a0c3a6cf1f0f7f7039bab59cbebd"}
+  ],
+  "predecessors": [
+    {"author": "eumemic", "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/288", "head": "475a088b5862f75f0b10596cfd6842d19531a5ec", "scope": "Section1.2 compact-WY/Sylvester argument, character specialization and both image and row spans. We add the averaged nonzero-defect form and singular-program application."},
+    {"author": "Ali Romman (@aliromman)", "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/468", "head": "07a78bf335b0b5039a1fecd7cd74a0fe1d1605ea", "scope": "Explicit I+XTY^T factorization and projected span bounds for the distinct abelian bit model."},
+    {"author": "Ali Romman (@AliRomman)", "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1862", "head": "bb29ea73ad9be9a0c3d53cdcb1d22b2ee9ffe42f", "scope": "Native source codes and the pinned source loader, including retained supplier attribution."},
+    {"author": "Ali Romman (@AliRomman)", "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1969", "head": "a6e6ad3936f67b8f63b5b68c5e75d540610a65e7", "scope": "Exact affine owner and phase conventions; contextual route proof, no code imported."},
+    {"author": "Rohan Arun (@rohanarun)", "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1931", "head": "d043a01b222365a951853904c001761921bb843b", "scope": "Local source-word continuation that motivated the paired-log target; no code imported."},
+    {"author": "Jose Manuel (@jmbarrancoml)", "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1998", "head": "9a3a967693055eba38ee4a5f5d311295fc4c224c", "scope": "Ordered scalar decoder and observation-space requirement; this package does not identify its mixed-chart inverse with the matched target."},
+    {"author": "Douglas Colkitt", "path": "research/complex-local-word-ceiling/ceiling.py", "scope": "Imported exact interval arithmetic for the conditional budget comparison."},
+    {"author": "Jeremy Diviney (@jeremydiviney)", "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/836", "scope": "Nearby unitary/positive-diagonal-gauged mixing obstruction; different free-frame and mixing hypotheses, no code imported."}
+  ],
+  "source_archive_policy": "The pinned loader reads the same frozen archive at bce54fb3f895cbe5cd4c0eb477c3afeed100190f and authenticates each member. The registered input list also binds the current tracked archive bytes. Full Git history is required.",
+  "conditional_profile_source": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1167#discussioncomment-18930295",
+  "attribution": "The causal average bound, Pauli-trivial tensor-sector construction and matched-target specialization are this contribution. Earlier rank-factorization methods, source words, phase conventions and arithmetic retain their credit and unchanged notices."
+}
diff --git a/research/paired-log-phase-query-bound/TASK.json b/research/paired-log-phase-query-bound/TASK.json
new file mode 100644
index 0000000000..e59b520631
--- /dev/null
+++ b/research/paired-log-phase-query-bound/TASK.json
@@ -0,0 +1,35 @@
+{
+  "schema_version": 1,
+  "task_id": "complex-new-helper-inventory",
+  "priority_revision": 3,
+  "base_commit": "e112d71c8d7bb32435debcc54df932593dd8223a",
+  "original_card": {
+    "id": "complex-new-helper-inventory",
+    "question": "Can a new local cost interface change the deficit-to-recursive-cost ratio beyond current packing?",
+    "starting_points": ["research/complex-local-word-ceiling/README.md", "research/heterogeneous-owner-assembly/README.md", "certificates/selected-result.json"],
+    "methods": ["Propose a changed helper inventory and derive an optimistic exact moment.", "Design a small completed instance and independently verify its endpoint and rank bill."],
+    "acceptance_gate": "A new physically realizable contract outside the frozen catalogue whose per-call profile, screened with ceiling.ceiling(), beats the selected word's packing ceiling; a lower cap does not establish identical circuitry or order attainable optima, and is insufficient to pass the stronger-budget target under this model.",
+    "first_step": {"command": ["python3", "-B", "research/complex-local-word-ceiling/verify.py"], "expected": "PASS_COMPLEX_LOCAL_WORD_CEILING", "inspect": "Read the selected word's per-call local profile, its packing ceiling and the lever table; run levers.py for the ideal budget of the lever you target.", "scope": "Positive control and planning budget only; this is not a new construction or full cold replay."},
+    "first_experiment": "Before any synthesis, write the candidate per-call local profile (and centre charge / unpaid coordinates if changed) and screen it with ceiling.ceiling(); reject it if even the ideal ceiling does not beat the selected word's by your stated margin.",
+    "bottleneck_link": "Packing of the selected word is capped at +0.87% (ceiling model); only a lower local excess spend or a changed coverage law raises the cap.",
+    "allowed_variations": ["Narrow to one changed boundary or helper type with explicit counts.", "If the coverage law, template or guard changes, derive an applicable fully charged replacement bound instead of applying the incumbent ceiling outside its scope."],
+    "scope_change_triggers": ["Mixing only providers already inside the pinned catalogue."],
+    "overlap_terms": ["helper inventory", "heterogeneous-owner", "mutable leaver"]
+  },
+  "scope_status": "changed",
+  "actual_scope": "An averaged-rank phase-event bound for fixed role-linear programs, applied to the matched P112 terminal query swap with off-frame mixing, COPY, CLEAR and private scratch.",
+  "scope_change_reason": "We sought a shared native query/update implementation beyond the previous common-hub template. A causal rank inequality excludes the proposed matched endpoint under the commuting-phase alphabet. This is a scoped negative result and does not meet the positive supplier acceptance gate.",
+  "bottleneck_link": "The completed-log model leaves a conditional favorable terminal allowance below 501 moment units. The matched four-bank primitive needs at least 555 single-array phase events in the declared alphabet, so scalar observability alone cannot complete this route.",
+  "budget_minutes": 120,
+  "stop_rule": "Complete the causal proof, tensor-sector construction, exact source specialization and focused PR. Leave noncommuting adapters and the broader constructive goal open.",
+  "outcome": "negative-result",
+  "evidence": "Universal causal expansion and averaged Sylvester bound; explicit common Pauli-trivial character sector; exact P112 source minor; 555-event joint lower bound; conditional moment comparison; seven assumption controls.",
+  "author": "Jose Manuel (@jmbarrancoml)",
+  "ai_assistance": "Substantial OpenAI Codex assistance in proof, implementation and prose. Mathematical collaborators checked the causal and target formulas; the primary agent implemented the replay. No independent human review.",
+  "coordination": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1167#discussioncomment-18931242",
+  "overlap": "Live refresh covered 329 open PRs at 2026-10-14 18:12:39 UTC, 693 Discussion records at 18:14:26 UTC and 1383 local records, with complete pagination and no warnings. We inspected PR288 and PR468, credited their rank-factorization and span methods, and separated PR836's unitary/gauged setting. Text coverage does not establish novelty.",
+  "open_questions": [
+    {"question": "Can noncommuting payload adapters implement the matched query swap below this price?", "why_it_matters": "Such adapters can leave the common character sectors used in the proof.", "first_step": "Insert one explicit address-linear adapter between two phase events and verify a tensor-valid endpoint with its complete price.", "blocked_by": "No such construction follows from the current argument."},
+    {"question": "Can a different terminal endpoint or sharing with earlier paid work close the controller?", "why_it_matters": "The theorem concerns four coherent matched targets and an appended-terminal budget.", "first_step": "Derive the exact alternative physical map and invoice before applying any query bound.", "blocked_by": "The mixed-chart scalar inverse alone does not specify a complete native implementation."}
+  ]
+}
diff --git a/research/paired-log-phase-query-bound/VERIFY.json b/research/paired-log-phase-query-bound/VERIFY.json
new file mode 100644
index 0000000000..ed91c9dd03
--- /dev/null
+++ b/research/paired-log-phase-query-bound/VERIFY.json
@@ -0,0 +1,18 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/native-source-codes/source_data.py",
+    "research/community-frontier1042-audit/selected-replay.tar.gz",
+    "research/complex-local-word-ceiling/ceiling.py"
+  ],
+  "commands": [
+    {
+      "argv": ["{python}", "-I", "-O", "-B", "{package}/verify.py"],
+      "timeout_seconds": 120,
+      "checks": "Pinned P112 minor; 96 direct/causal program maps with COPY/CLEAR; 3584 Pauli-trivial phase checks; 6216 pair characters; 57 exact target blocks; rank certificates; 555-event lower bound; conditional moment comparison and seven assumption controls. Universal coverage follows from the written proof."
+    }
+  ]
+}
diff --git a/research/paired-log-phase-query-bound/verify.py b/research/paired-log-phase-query-bound/verify.py
new file mode 100644
index 0000000000..9257b11902
--- /dev/null
+++ b/research/paired-log-phase-query-bound/verify.py
@@ -0,0 +1,357 @@
+"""Exact premises for the averaged-rank phase-query bound.
+
+Jose Manuel (@jmbarrancoml), with substantial OpenAI Codex assistance.
+Apache-2.0. Source geometry: Ali Romman and the retained supplier lineage.
+The causal/character rank method follows eumemic PR288 and Ali Romman PR468.
+"""
+
+from collections import Counter
+from fractions import Fraction as F
+from hashlib import sha256
+import importlib.util
+import json
+from pathlib import Path
+from random import Random
+
+ROOT = Path(__file__).resolve().parents[2]
+A_PORTS = [0, 7, 20, 23, 86, 93, 108, 111]
+SOURCE_PATH = "research/native-source-codes/source_data.py"
+COST_PATH = "research/complex-local-word-ceiling/ceiling.py"
+IMPORT_PINS = {
+    SOURCE_PATH: "d23924511e3aed41e5e64511ca70126a636d91c8aa02e656cb61d6ceca1fe0a0",
+    COST_PATH: "86a1432870b3b21d8454106ec9162fddc0471472d9214c590a1420f2426cedfc",
+}
+
+
+def require(condition, message):
+    if not condition:
+        raise ValueError(message)
+
+
+def load(path, name):
+    require(sha256((ROOT / path).read_bytes()).hexdigest() == IMPORT_PINS[path], "import source pin")
+    spec = importlib.util.spec_from_file_location(name, ROOT / path)
+    module = importlib.util.module_from_spec(spec)
+    spec.loader.exec_module(module)
+    return module
+
+
+def zeros(n, m):
+    return [[0] * m for _ in range(n)]
+
+
+def eye(n):
+    return [[int(i == j) for j in range(n)] for i in range(n)]
+
+
+def transpose(a):
+    return [list(x) for x in zip(*a)]
+
+
+def multiply(a, b):
+    if not a:
+        return []
+    require(len(a[0]) == len(b), "matrix dimensions")
+    out = zeros(len(a), len(b[0]))
+    for i, row in enumerate(a):
+        for k, x in enumerate(row):
+            if x:
+                for j, y in enumerate(b[k]):
+                    if y:
+                        out[i][j] += x * y
+    return out
+
+
+def difference(a, b):
+    return [[x - y for x, y in zip(ra, rb)] for ra, rb in zip(a, b)]
+
+
+def rank(rows, prime=None):
+    if not rows or not rows[0]:
+        return 0
+    a = [[int(x) % prime if prime else F(x) for x in row] for row in rows]
+    pivot = 0
+    for col in range(len(a[0])):
+        found = next((i for i in range(pivot, len(a)) if a[i][col]), None)
+        if found is None:
+            continue
+        a[pivot], a[found] = a[found], a[pivot]
+        scale = pow(a[pivot][col], -1, prime) if prime else 1 / a[pivot][col]
+        a[pivot] = [(x * scale) % prime if prime else x * scale for x in a[pivot]]
+        for i in range(pivot + 1, len(a)):
+            c = a[i][col]
+            if c:
+                a[i] = [(x - c * y) % prime if prime else x - c * y
+                        for x, y in zip(a[i], a[pivot])]
+        pivot += 1
+        if pivot == len(a):
+            break
+    return pivot
+
+
+def expect_rejection(call, label):
+    try:
+        call()
+    except ValueError:
+        return label
+    raise ValueError("negative control accepted: " + label)
+
+
+def causal_checks():
+    """Compare a direct program with the causal expansion, including singular maps."""
+    rng = Random(20261014)
+    examples, characters, singular_steps, causal_control = 12, 8, 0, False
+    for fixture in range(examples):
+        n, inputs, outputs, k = 6, (4 if fixture % 2 else 6), (4 if fixture % 2 else 6), 6
+        entry = [row[:inputs] for row in eye(n)]
+        exit_map = eye(n)[:outputs]
+        coordinates = [rng.randrange(n) for _ in range(k)]
+        labels = [1 + rng.randrange(7) for _ in range(k)]
+        maps = []
+        for j in range(k):
+            a = eye(n)
+            for _ in range(5):
+                target, source = rng.sample(range(n), 2)
+                c = rng.choice([-2, -1, 1, 2])
+                a[target] = [x + c * y for x, y in zip(a[target], a[source])]
+            if j % 3 == 1:
+                target, source = rng.sample(range(n), 2)
+                a[target] = a[source][:]  # singular COPY
+                singular_steps += 1
+            if j % 3 == 2:
+                a[rng.randrange(n)] = [0] * n  # CLEAR
+                singular_steps += 1
+            maps.append(a)
+        prefix = entry
+        v = []
+        for j in range(k):
+            v.append(prefix[coordinates[j]][:])
+            prefix = multiply(maps[j], prefix)
+        baseline = multiply(exit_map, prefix)
+        suffix, u = exit_map, zeros(outputs, k)
+        for j in range(k - 1, -1, -1):
+            suffix = multiply(suffix, maps[j])
+            for i in range(outputs):
+                u[i][j] = suffix[i][coordinates[j]]
+        h = zeros(k, k)
+        for earlier in range(k):
+            propagation = eye(n)
+            for later in range(earlier + 1, k):
+                propagation = multiply(maps[later - 1], propagation)
+                h[later][earlier] = propagation[coordinates[later]][coordinates[earlier]]
+        differences, defects, active_counts = [], [], []
+        for character in range(characters):
+            alpha = [-2 if (character & label).bit_count() % 2 else 0 for label in labels]
+            direct = [row[:] for row in entry]
+            for j in range(k):
+                direct[coordinates[j]] = [(1 + alpha[j]) * x for x in direct[coordinates[j]]]
+                direct = multiply(maps[j], direct)
+            actual = difference(multiply(exit_map, direct), baseline)
+            injection = zeros(k, inputs)
+            for j in range(k):
+                for t in range(inputs):
+                    injection[j][t] = alpha[j] * (v[j][t] + sum(h[j][i] * injection[i][t] for i in range(j)))
+            require(multiply(u, injection) == actual, "causal expansion")
+            diagonal_only = [[alpha[j] * x for x in v[j]] for j in range(k)]
+            causal_control |= multiply(u, diagonal_only) != actual
+            active = [j for j in range(k) if alpha[j]]
+            us = [[row[j] for j in active] for row in u]
+            vs = [v[j] for j in active]
+            defect = rank(actual)
+            require(defect >= rank(us) + rank(vs) - len(active), "active-set Sylvester bound")
+            differences.append(actual)
+            defects.append(defect)
+            active_counts.append(len(active))
+        du = rank([row for delta in differences for row in transpose(delta)])
+        dv = rank([row for delta in differences for row in delta])
+        require(sum(active_counts) == characters * k // 2, "half-active nonzero queries")
+        for defect, active in zip(defects, active_counts):
+            require(defect >= du + dv - 2 * k + active, "global span deletion bound")
+        require(3 * k * characters >= 2 * ((du + dv) * characters - sum(defects)), "averaged-rank bound")
+    require(causal_control, "causal omission control was not exercised")
+    return {"programs": examples, "character_maps": examples * characters, "singular_free_steps": singular_steps,
+            "omitting_causal_propagation_changes_a_checked_map": causal_control}
+
+
+def quadratic_pairs(m):
+    return [(i, j) for i in range(m) for j in range(i, m)]
+
+
+def polar(q, m):
+    return sum(((q >> i) & 1) * ((q >> j) & 1) << k for k, (i, j) in enumerate(quadratic_pairs(m)))
+
+
+def frequency_tuple(form, m):
+    pairs, degrees, linear, frequencies = quadratic_pairs(m), [0] * m, [0] * m, []
+    for k, (i, j) in enumerate(pairs):
+        if not ((form >> k) & 1):
+            continue
+        if i == j:
+            linear[i] = 1
+        else:
+            frequencies.append((1 << i) | (1 << j))
+            degrees[i] += 1
+            degrees[j] += 1
+    for i in range(m):
+        frequencies += [1 << i] * ((2 * linear[i] - degrees[i]) % 4)
+    length = 4 * ((m * (m - 1) // 2 + 3 * m + 3) // 4)
+    require(len(frequencies) <= length, "common tensor length")
+    frequencies += [0] * (length - len(frequencies))
+    return frequencies
+
+
+def sector_checks():
+    checks = 0
+    for form in range(64):
+        frequencies = frequency_tuple(form, 3)
+        require(len(frequencies) == 12, "small common tensor length")
+        for shift in range(8):
+            shifted = [x ^ shift for x in frequencies]
+            xor = 0
+            for x in shifted:
+                xor ^= x
+            require(xor == 0, "uniform X stabilizer")
+            for q in range(1, 8):
+                phase = sum((q & x).bit_count() % 2 for x in shifted) % 4
+                wanted = 2 * ((form & polar(q, 3)).bit_count() % 2)
+                require(phase == wanted, "Pauli-trivial character witness")
+                checks += 1
+    # Uniform Z permutes the eight shifted tuples; the equal-weight orbit sum
+    # is nonzero and fixed. These checks distinguish free Pauli translations
+    # from unconstrained character sectors, where the theorem would not apply.
+    bad = frequency_tuple(0, 3)
+    bad[0] ^= 1
+    bad_x_phase = sum((1 & x).bit_count() % 2 for x in bad) % 2
+    require(bad_x_phase == 1, "nontrivial Pauli control")
+    control = expect_rejection(lambda: require(bad_x_phase == 0, "uniform X is not trivial"),
+                               "unqualified free-Pauli sector")
+    return {"characters": 64, "tensor_length": 12, "exact_phase_checks": checks, "control": control}
+
+
+def target_checks():
+    source = load(SOURCE_PATH, "pinned_native_source")
+    data = source.load_local(ROOT)
+    word, program = data["CANONICAL-WORD.json.gz"], data["LOCAL-PROGRAMS.json.gz"]["forward"]
+    boundary = source.replay(program, 704, program.index(["phase", "centers"]))
+    r = [[boundary[c].get(j, 0) for j in range(112)] for c in word["centers"]]
+    a = [[row[j] for j in A_PORTS] for row in r]
+    ordinary = [j for j in range(112) if j not in A_PORTS]
+    require(multiply(transpose(a), a) == [[4 * x for x in row] for row in eye(8)], "selected minor")
+    # B=R_A^-1 R_B; store 2B as small integers.
+    b2 = multiply(transpose(a), [[row[j] for j in ordinary] for row in r])
+    b2 = [[F(x) / 2 for x in row] for row in b2]
+    require(all(x.denominator == 1 and x in (-1, 0, 1) for row in b2 for x in row), "twice-B coefficients")
+    b2 = [[int(x) for x in row] for row in b2]
+    require(multiply(b2, transpose(b2)) == [[52 * x for x in row] for row in eye(8)], "B B^T=13I")
+    require(all(any(row) for row in b2) and all(any(col) for col in zip(*b2)), "nonzero rows and columns")
+    labels = word["ports"]
+    require(len(set(labels)) == 112 and all(q.bit_count() % 2 for q in labels), "distinct odd hole labels")
+    polars = [polar(q, 9) for q in labels]
+    pair_keys = [polars[i] ^ polars[j] for i in range(112) for j in range(i)]
+    require(len(set(pair_keys)) == 6216 and 0 not in pair_keys, "unique pair characters")
+    wrong_polars = polars[:]
+    wrong_polars[1] = wrong_polars[0]
+    pair_control = expect_rejection(lambda: require(
+        len({wrong_polars[i] ^ wrong_polars[j] for i in range(112) for j in range(i)}) == 6216,
+        "duplicate hole label"), "duplicate hole character")
+    n, v, selected, ordinary_count = 120, 112, 8, 104
+    t4 = zeros(n, n)
+    bb = multiply(transpose(b2), b2)
+    for i in range(8):
+        t4[i][i], t4[i][112+i], t4[112+i][i] = 52, 4, 4
+        for j in range(104):
+            t4[i][8+j], t4[112+i][8+j], t4[8+j][i] = 24*b2[i][j], 2*b2[i][j], -2*b2[i][j]
+    for i in range(104):
+        for j in range(104):
+            t4[8+i][8+j] = 4 * int(i == j) - bb[i][j]
+    images, rows = [], []
+    for j in range(104):
+        e = [0] * n
+        e[8+j] = 1
+        images.append(e)
+        rows.append(e[:])
+    for i in range(8):
+        image, row = [0] * n, [0] * n
+        image[i], image[112+i], row[i] = 12, 1, 1
+        images.append(image)
+        rows.append(row)
+    require(rank(images, 1009) == rank(rows, 1009) == v, "union-span certificate")
+    rng = Random(1128)
+    forms = [1 << i for i in range(45)] + [rng.getrandbits(45) for _ in range(12)]
+    ranks = Counter()
+    order = A_PORTS + ordinary + A_PORTS
+    log_control = False
+    for form in forms:
+        signs = [1 - 2 * ((form & polars[p]).bit_count() % 2) for p in order]
+        actual = [[(signs[i] * signs[j] - 1) * t4[i][j] for j in range(n)] for i in range(n)]
+        bp = [[signs[i] * signs[8+j] * b2[i][j] for j in range(104)] for i in range(8)]
+        e = difference(bp, b2)
+        formula = zeros(n, n)
+        bb_delta = difference(multiply(transpose(bp), bp), bb)
+        for i in range(8):
+            for j in range(104):
+                formula[i][8+j], formula[112+i][8+j], formula[8+j][i] = 24*e[i][j], 2*e[i][j], -2*e[i][j]
+        for i in range(104):
+            for j in range(104):
+                formula[8+i][8+j] = -bb_delta[i][j]
+        require(formula == actual, "exact target block identity")
+        wrong_signs = signs[:]
+        wrong_signs[112] *= -1
+        wrong_target = [[(wrong_signs[i] * wrong_signs[j] - 1) * t4[i][j]
+                         for j in range(n)] for i in range(n)]
+        require(wrong_target != formula, "unmatched-log control did not fail")
+        log_control = True
+        erank = rank(e)
+        require(rank(actual, 1009) == 2 * erank, "rank identity corroboration")
+        ranks[2 * erank] += 1
+    require((4 * (v - selected) + 2) // 3 == 139, "one-bank floor")
+    require((4 * 4 * (v - selected) + 2) // 3 == 555, "joint four-bank floor")
+    return {"ports": v, "selected_ports": A_PORTS, "B_nonzeros": sum(bool(x) for row in b2 for x in row),
+            "pair_characters": len(pair_keys), "union_image_dimension": v, "union_row_dimension": v,
+            "target_sign_cases": len(forms), "defect_rank_histogram": dict(sorted(ranks.items())),
+            "rank_bound_per_character": 16, "one_bank_floor": 139, "joint_four_bank_floor": 555,
+            "pair_control": pair_control, "unmatched_log_gauge_rejected": log_control}
+
+
+def budget_check():
+    cost = load(COST_PATH, "pinned_interval_cost")
+    profile = {1:21204, 2:4500, 3:3744, 4:1170, 5:738, 8:16, 9:40,
+               16:32, 17:16, 24:8, 32:16, 33:8, 40:8, 48:48, 49:8, 51:F(14778,51)}
+    q, m, roles = F(67018507072324140917,40000000000000000000000), 73, 968
+    require(sum(r*n for r,n in profile.items()) == 69840, "conditional rank mass")
+    lo = hi = F(0)
+    for r, count in profile.items():
+        a, b = cost.child_cost(r, m, q)
+        lo += count * m * a
+        hi += count * m * b
+    allowance = (m*roles-hi, m*roles-lo)
+    require(F(50073765694042,10**11) < allowance[0] <= allowance[1] < F(50073765694043,10**11),
+            "certified favorable allowance")
+    one = tuple(m*x for x in cost.child_cost(1,m,q))
+    require(497*one[1] < allowance[0] and 498*one[0] > allowance[1], "integer rank-one budget")
+    require(F(555) > allowance[1], "even rank-mass price misses budget")
+    return {"q": str(q), "conditional_fixed_width": m, "conditional_roles": roles,
+            "allowance_decimal_bracket": ["500.73765694042", "500.73765694043"],
+            "rank1_budget": 497, "phase_event_floor": 555}
+
+
+def main():
+    controls = []
+    causal = causal_checks()
+    sector = sector_checks()
+    target = target_checks()
+    budget = budget_check()
+    controls.append(expect_rejection(lambda: require(3*554 >= 2*(896-64), "understated query count"), "554-call claim"))
+    controls.append(expect_rejection(lambda: require(555 <= F(50073765694043,10**11), "underpriced phase events"), "decoder budget claim"))
+    controls += ["omitted causal propagation", sector["control"], target["pair_control"], "unmatched log gauge"]
+    controls.append(expect_rejection(lambda: require(
+        sum((x & 0).bit_count() % 2 for x in range(8)) == 4, "neutral query is not half-active"),
+        "counting a neutral query as nontrivial"))
+    print(json.dumps({"status": "PASS_PAIRED_LOG_PHASE_QUERY_BOUND", "causal_programs": causal,
+                      "pauli_trivial_sector": sector, "matched_target": target,
+                      "conditional_budget": budget, "negative_controls": controls,
+                      "scope": "Fixed role-linear schedules with single-array commuting phase queries; see README for tensor, cover and billing boundaries."}, indent=2, sort_keys=True))
+
+
+if __name__ == "__main__":
+    main()