diff --git a/research/two-image-volume-independent-audit/NOTICE.md b/research/two-image-volume-independent-audit/NOTICE.md
new file mode 100644
index 0000000000..92311e3005
--- /dev/null
+++ b/research/two-image-volume-independent-audit/NOTICE.md
@@ -0,0 +1,7 @@
+# Attribution and retained source scope
+
+Prepared by JoyboyBrian with substantial OpenAI Codex assistance. New proof and checker: Apache-2.0.
+
+The exact retained files and original Git blob/SHA256 identities are listed in RETAINED-SOURCES.json. Cinna Davis authored PR4991's dirty-volume theorem and PR4998's compensated-pair construction, with their disclosed OpenAI Codex assistance. lee-phys authored PR4688's original two-image prefix; Yiyang (@Lyy-iiis) authored PR4710's phase repair. Their retained source notices remain unchanged. Credit Dugongue's PR4743 for the distinct triangular full-input port; Jacob Alan Sussman's PR4628 for the model and lower-bound context, with eumemic and Swapnil Jain as credited in the retained PR4688 README. The new work independently audits the quantified completed boundary and explicitly supplies the singular rank-drop step; it does not claim authorship of the predecessor construction or determinant invariant.
+
+The original and repaired source implementations are retained to bind their literal address/phase definitions. They are never imported or executed. PR4991 and PR4998 verifiers are deliberately absent. Their proof documents and PR4998's literal program are retained as independently auditable source evidence, not treated as accepted theorem certificates. All retained files are Apache-2.0 as declared by their source notices and repository license.
diff --git a/research/two-image-volume-independent-audit/PROOF.md b/research/two-image-volume-independent-audit/PROOF.md
new file mode 100644
index 0000000000..d8c00760d3
--- /dev/null
+++ b/research/two-image-volume-independent-audit/PROOF.md
@@ -0,0 +1,63 @@
+# Independent audit of the completed two-image boundary
+
+Prepared by JoyboyBrian with substantial OpenAI Codex assistance. Apache-2.0. This is an independent written scoped proof and exact finite source audit, not proof-assistant verification or acceptance of a complete multiplication construction.
+
+## Audit finding
+
+PR4991's nonsingular coefficient classification and its enlarged-alphabet affine determinant invariant are correct under their stated uniform full-state hypotheses. Its singular coefficient paragraph needs a separate rank argument: singularity alone does not contradict a language that syntactically permits singular register mixing. Section 4 below supplies that argument. Thus the claimed exclusion survives, with this explicit additional proof step. PR4998's compensated partner is a valid boundary escape; it is not a restored dirty bank.
+
+## 1. Literal source and quantifiers
+
+Use the retained PR4688 definitions on addresses `x=x0+2*x1+4*x2`: `U(x0,x1,x2)=(x0,x1,x2+x0)`, `V(x0,x1,x2)=(x1,x0,x2)`, with additions modulo two. The actual paid operator is `C=((1+i)/2)I+((1-i)/2)X0`. Because `X0` is a Hermitian involution, `C` has eigenvalues 1 and i and is unitary; replacing it by an unnormalized rank-equivalent operator would be invalid for this audit.
+
+The retained PR4710 code defines `S e_x=i^popcount(x)e_x`, `P=SUS`, and `Q=SVS`. These are actual linear maps, including global phases. The checker evaluates only the literal source defining expressions using a separately written composition routine, then checks them against independent bit-coordinate formulas. It never imports or executes a predecessor module. PR4991 and PR4998 verifiers were not read or retained. Retained bytes, Git blob IDs, source commits and paths are in RETAINED-SOURCES.json; their notices are preserved.
+
+For positive integer f, tensorize each letter individually. For fixed complex alpha,beta let `F_f=C_f(alpha U_f+beta V_f)C_f`; the repaired family replaces U,V with P,Q. In particular, the mixture is not `(alpha U+beta V)^(tensor f)`. A completed isolated target on q>=1 banks is `diag(F_f,H_2,f,...,H_q,f)`, where each H is unitary, including identity. All q inputs are arbitrary and independent; all q outputs are specified. There is no clean initialization, omitted output or discarded garbage.
+
+The language is one finite uniform word: fixed finite q, fixed register mixing matrices M acting as `M tensor I_(8^f)`, and fixed invertible 8-by-8 address letters B acting as `B^(tensor f)` on selected banks. Arbitrary full-state unitary letters, even depending on f, are also granted. Word length, nonunitary coefficients and base address matrices are fixed across f. Singular register mixing is syntactically permitted. The exclusion concerns all positive f, and also eventual equality at every f>=f0. It does not concern separate words chosen for separate widths.
+
+## 2. Character multiplicities from the actual phases
+
+Direct coordinate composition gives `R=U^-1 V` with cycles `(0)(4)(1 2 5 6)(3 7)`. Thus `R^4=I` and the traces at powers 0,1,2,3 are `(8,2,4,2)`. For the repaired pair, literal multiplication gives `P^-1 Q=S^-1 R S`, with no residual scalar phase. Consequently their tensor powers have identical traces and spectra. Merely matching projective monomials is insufficient: replacing Q by iQ changes the relative trace from 2 to 2i while retaining its underlying permutation.
+
+Trace multiplicativity gives `tr((R^(tensor f))^k)=(tr R^k)^f`. Apply the four order-four character projectors, in eigenvalue order `(1,i,-1,-i)`, to obtain
+
+`m_f=((8^f+4^f+2*2^f)/4, (8^f-4^f)/4, (8^f+4^f-2*2^f)/4, (8^f-4^f)/4)`.
+
+These are integer multiplicities independently because `m_0=(1,0,0,0)` and `m_(f+1)` is cyclic convolution of `m_f` with `(4,1,2,1)`. In particular all four entries are strictly positive at f=1 and remain so by convolution. Each is strictly less than `d=8^f`, since the other three entries are positive. This proves both bounds for every positive width, rather than extrapolating a finite receipt.
+
+For alpha=1,beta=2, factor the middle sum as `U_f(I+2R_f)`. The unitary outer factors have absolute determinant one, so `D_f=|det F_f|=3^(m_f,1) 5^(m_f,i)`. The repaired family has exactly the same D_f. Widths one and two give `(m_1,m_i)=(4,1),(22,12)`. The formula at width three gives `(148,112)` and hence `D_3 D_1^64/D_2^16=3^52/5^16 !=1`. Width three is used through the proved symbolic formula, not a direct matrix replay.
+
+## 3. All fixed nonsingular complex coefficient pairs
+
+For invertible final output every full-state factor is invertible. In particular every register mixing actually used must be invertible. The normalized logarithmic absolute determinant of any allowed word is `a+b f`: a mixing contributes `log|det M|`; a selected-bank address letter contributes `(f/8)log|det B|`, by the Kronecker determinant formula `det(B^(tensor f))=(det B)^(f*8^(f-1))`; every full-state unitary contributes zero. Summing these finitely many terms proves the invariant for arbitrary fixed invertible address matrices, not just the original permutation/phase alphabet. Fixed bank count ensures the mixing determinant is a fixed number. Arbitrary unitary helper targets do not alter the target profile.
+
+Suppose alpha*beta!=0, put t=beta/alpha, and first exclude t in `{1,-1,i,-i}`. All four eigenvalue factors are then nonzero. Define real finite numbers `A=log|1+t|`, `B=log|1-t|`, `E=log|1+t^2|`. The multiplicities in section 2 give exactly
+
+`log|det F_f|/8^f = log|alpha|+(A+B+E)/4+(A+B-E)/(4*2^f)+(A-B)/(2*4^f)`.
+
+The repaired family has the same formula. If this profile equals an affine function for every sufficiently large integer f, its convergent limit forces the affine slope to be zero. Subtract that limit and multiply by 2^f: taking f to infinity first gives `A+B-E=0`, and the remaining equality then gives `A-B=0`. This proves independence of the two decay modes on any infinite tail; it does not infer eventual behavior from the first three widths.
+
+Now `A=B` implies `|1+t|^2=|1-t|^2`, so Re(t)=0. Write t=iy for real y. The second condition requires `1+y^2=|1-y^2|`. For `y^2>0` the left side is strictly larger, whether `y^2<=1` or `y^2>=1`. Thus y=0 and t=0, contradicting beta!=0. This closes the critical pure-imaginary case as well as general fixed complex ratios. Therefore no nonsingular nonzero coefficient pair can be isolated by the uniform language, even eventually.
+
+## 4. The singular coefficient cases require rank, not volume
+
+For t in `{1,-1,i,-i}`, exactly one fourth-root eigenspace is killed by `I+tR_f`. Since every multiplicity is positive and strictly smaller than d, both literal prefix families satisfy `0<rank F_f<d` for every positive f. This uses the actual source spectrum; singularity alone would not suffice.
+
+Fix one such width and the same q banks as in section 1. The desired full-state target has rank `(q-1)d+rank F_f`, strictly between `(q-1)d` and qd. All address letters and unitary letters are invertible. If all register mixings were invertible too, their product could not equal a singular target. Hence some q-by-q register mixing M must be singular. But `rank(M tensor I_d)=d*rank M <=(q-1)d`. Multiplication by any other square factors cannot increase rank, so the whole word has rank at most `(q-1)d`, a contradiction. A mixing on a subset of banks has the same bound after adjoining its identity block.
+
+This argument includes q=1, arbitrary many but fixed helper banks, and unitary helper outputs. It is pointwise in width, so also excludes any eventual family. It does not take the logarithm of a zero determinant. This is the explicit completion of the singular branch of PR4991's all-coefficient statement.
+
+If exactly one of alpha,beta is zero and the other is nonzero, the target is a scalar times a composition of individually tensorized unitary letters. It is implementable by that literal single-image word and a fixed scalar mixing; its normalized volume is constant. These allowed boundary cases are not accidentally excluded.
+
+## 5. Compensated and clean-input boundary controls
+
+PR4998 has two arbitrary independent inputs and outputs `diag(F_f,F_f^-1)`. Its absolute determinant is one at every width, so its second bank cancels the first bank's volume profile. Its all-width block identity is `W(D)W(-I)=diag(D,D^-1)`, where `W(D)=E12(D)E21(-D^-1)E12(D)=[[0,D],[-D^-1,0]]`. Ordinary block multiplication proves this without commuting D with any outside C. Taking D to be the source middle sum and sandwiching with `diag(C_f,C_f^-1)` gives the claimed pair. The finite checker independently interprets retained PROGRAM.json at widths one/two and compares every independent input column with a target built from the literal source matrices and direct modular inversion. It confirms that the second output is not identity. It does not audit native rounding, the instruction invoice or Gaussian-consumer admission.
+
+Likewise the PR4688 clean-scratch implementation remains compatible. A full-space singular map may be injective on a proper clean-input subspace: `[[2,0],[0,0]]` maps `(x,0)` to `(2x,0)` injectively while its full determinant is zero. Thus the invertible full-space premise used in section 3 and the retained-dirty rank requirement in section 4 do not follow from correctness on clean inputs. Clean-workspace projector mechanisms and width-dependent nonunitary words are outside this theorem, and no statement about arbitrary global continuations of the prefix follows.
+
+## 6. Evidence and remaining scope
+
+The independent checker uses no external dependencies or predecessor imports. Exact monomial phases, source bytes, character traces and integer Bareiss determinants are checked at widths one/two. The all-width convolution and all-complex classification are written proofs above. The curvature witness is symbolic. The literal compensated program comparison is exact over F17 with i=4, a finite positive boundary control rather than a rational all-width program certificate. Semantic controls reject tensorizing a sum, dropping the absolute phase, calling the transformed inverse partner returned dirt, and extending a full-space invariant to clean input. Normal and optimized replays use explicit exceptions, so correctness does not rely on Python assertions.
+
+No five-in-fourteen conclusion, paid-call lower bound, native supplier, precision/tape acceptance, selected-frontier change, new kappa or full multiplication theorem is established. Original construction, spectrum and invariant credit remain with their authors; this audit adds independent source/quantifier coverage and the singular rank argument.
diff --git a/research/two-image-volume-independent-audit/README.md b/research/two-image-volume-independent-audit/README.md
new file mode 100644
index 0000000000..5c2e870b7f
--- /dev/null
+++ b/research/two-image-volume-independent-audit/README.md
@@ -0,0 +1,23 @@
+# Independent all-coefficient two-image boundary audit
+
+**Result:** PR4991's nonsingular dirty-helper volume obstruction is corroborated with literal original/repaired source phases and all-width quantifiers. Its singular coefficient cases need a rank argument in addition to noting singularity; [PROOF.md](PROOF.md#4-the-singular-coefficient-cases-require-rank-not-volume) supplies that missing step. The exclusion holds for every fixed alpha*beta!=0 in the stated fixed finite bank/word model, including eventual width tails. This is an independent written scoped proof, not a formalization or new multiplication exponent.
+
+For q arbitrary-input banks of dimension d, the singular cases have target rank `(q-1)d+rank(F)>(q-1)d`; any singular register-mixing factor has rank at most `(q-1)d`. For nonsingular coefficients, the source-specific normalized determinant contains independent `2^-f` and `4^-f` terms, incompatible with the allowed affine profile. Fixed arbitrary invertible address letters are included. Exactly one zero coefficient remains an allowed single-image case.
+
+PR4998's `diag(F,F^-1)` is a required positive boundary control: the inverse partner transforms an independent input and compensates the volume. It is not returned dirty state. No clean-input or width-dependent nonunitary-word exclusion is inferred.
+
+## Reproduction
+
+```sh
+python3.12 -B research/two-image-volume-independent-audit/verify.py --check research/two-image-volume-independent-audit/RESULT.json
+python3.12 -O -B research/two-image-volume-independent-audit/verify.py --check research/two-image-volume-independent-audit/RESULT.json
+python3.12 -B scripts/research_package.py --package research/two-image-volume-independent-audit
+```
+
+Executed on Python 3.12.14, Darwin 27.0.0 arm64: the direct normal replay took 0.17 seconds and the optimized replay 0.23 seconds; registered normal/optimized replay and metadata/pins checks passed. Standard library only. Exact character/determinant checks are bounded to widths one/two; the full-width and all-complex claims follow from the written proof. The retained compensated program is checked on all 16 and 128 independent columns over F17, solely as a finite boundary control. No predecessor verifier is imported/executed, and PR4991/4998 verifiers are absent. [RETAINED-SOURCES.json](RETAINED-SOURCES.json) binds original paths/commits/SHA256/Git blobs; all necessary pending-source bytes are committed here. [NOTICE.md](NOTICE.md) preserves predecessor credit and AI disclosure.
+
+This audit changes no predecessor package or selected record. It does not establish a continuation, Gaussian consumer, full native/tape/precision implementation, new paid-call bound or kappa.
+
+## Open next questions
+
+Can the compensated inverse partner be consumed as an independently priced Gaussian target? Name one actual consumer and retain both arbitrary independent outputs, precision, denominator-15 scalar arithmetic and tape charges. PR4998's exact local construction and this completed-boundary audit supply no such consumer. The structured dependency is in TASK.json; a new construction round is not justified by the isolation obstruction alone.
diff --git a/research/two-image-volume-independent-audit/RESULT.json b/research/two-image-volume-independent-audit/RESULT.json
new file mode 100644
index 0000000000..e5d870fd42
--- /dev/null
+++ b/research/two-image-volume-independent-audit/RESULT.json
@@ -0,0 +1,94 @@
+{
+  "all_width_character_formula": [
+    "(8^f+4^f+2*2^f)/4",
+    "(8^f-4^f)/4",
+    "(8^f+4^f-2*2^f)/4",
+    "(8^f-4^f)/4"
+  ],
+  "controls": [
+    "absolute phase of Q",
+    "tensorizing a sum",
+    "pure-imaginary nonzero ratio",
+    "singular rank-drop hypotheses",
+    "allowed single-image cases",
+    "compensating output is transformed",
+    "clean subspace is outside full-space volume lemma"
+  ],
+  "curvature_witness": "3^52/5^16 != 1",
+  "finite_checks": [
+    {
+      "absolute_determinant": "405",
+      "character_counts_1_i_minus1_minusi": [
+        4,
+        1,
+        2,
+        1
+      ],
+      "compensated_boundary": {
+        "original": {
+          "arithmetic": "F17 with i=4; finite boundary control only",
+          "independent_columns": 16,
+          "literal_instructions": 57,
+          "partner_is_identity": false,
+          "single_image_cases_invertible": true
+        },
+        "phase_repaired": {
+          "arithmetic": "F17 with i=4; finite boundary control only",
+          "independent_columns": 16,
+          "literal_instructions": 153,
+          "partner_is_identity": false,
+          "single_image_cases_invertible": true
+        }
+      },
+      "singular_target_ranks": [
+        6,
+        4,
+        7,
+        7
+      ],
+      "width": 1
+    },
+    {
+      "absolute_determinant": "7661391506103515625",
+      "character_counts_1_i_minus1_minusi": [
+        22,
+        12,
+        18,
+        12
+      ],
+      "compensated_boundary": {
+        "original": {
+          "arithmetic": "F17 with i=4; finite boundary control only",
+          "independent_columns": 128,
+          "literal_instructions": 57,
+          "partner_is_identity": false,
+          "single_image_cases_invertible": true
+        },
+        "phase_repaired": {
+          "arithmetic": "F17 with i=4; finite boundary control only",
+          "independent_columns": 128,
+          "literal_instructions": 153,
+          "partner_is_identity": false,
+          "single_image_cases_invertible": true
+        }
+      },
+      "singular_target_ranks": [
+        46,
+        42,
+        52,
+        52
+      ],
+      "width": 2
+    }
+  ],
+  "normalized_profile": "log|alpha|+(A+B+E)/4+(A+B-E)/(4*2^f)+(A-B)/(2*4^f)",
+  "result": "PASS",
+  "scope": "Independent scoped written theorem audit; exact finite source checks, not full theorem formalization",
+  "singular_gap_completion": "rank-drop argument for every fixed finite bank count",
+  "source_relative_traces": [
+    8,
+    2,
+    4,
+    2
+  ]
+}
diff --git a/research/two-image-volume-independent-audit/RETAINED-SOURCES.json b/research/two-image-volume-independent-audit/RETAINED-SOURCES.json
new file mode 100644
index 0000000000..0f16118736
--- /dev/null
+++ b/research/two-image-volume-independent-audit/RETAINED-SOURCES.json
@@ -0,0 +1,70 @@
+{
+  "schema_version": 1,
+  "files": [
+    {
+      "retained_path": "vendor/pr4688/README.md",
+      "source_commit": "f259dabc7d70e0db8d6d36bfda888f008bbfecc1",
+      "source_path": "research/complex-two-image-hook-prefix/README.md",
+      "git_blob": "ac33ab36287fe1f1d9ba51b5360f44536c2ff3fc",
+      "sha256": "91d45b5af6063e30c6860a4cb46cfc44960ecd67f37c3bce9675924e30b89b4e",
+      "license": "Apache-2.0"
+    },
+    {
+      "retained_path": "vendor/pr4688/verify.py",
+      "source_commit": "f259dabc7d70e0db8d6d36bfda888f008bbfecc1",
+      "source_path": "research/complex-two-image-hook-prefix/verify.py",
+      "git_blob": "8d2815a2806894bcc50fb34e854f4ef7632ea588",
+      "sha256": "99ff0beccd9a4e94cc607e02114d62b8ce0ea57ee00748b07ce0a0af91aec85e",
+      "license": "Apache-2.0"
+    },
+    {
+      "retained_path": "vendor/pr4710/README.md",
+      "source_commit": "f259dabc7d70e0db8d6d36bfda888f008bbfecc1",
+      "source_path": "research/phase-aligned-two-call-prefix/README.md",
+      "git_blob": "ef39626e0b25216d826d45371af1d181ab2754f1",
+      "sha256": "e866032429cb032f55edc9b2f3c6535ecf37680aae7cd9e8bb9b8cc21617aa64",
+      "license": "Apache-2.0"
+    },
+    {
+      "retained_path": "vendor/pr4710/verify.py",
+      "source_commit": "f259dabc7d70e0db8d6d36bfda888f008bbfecc1",
+      "source_path": "research/phase-aligned-two-call-prefix/verify.py",
+      "git_blob": "1d81448d5f21fc98ffced8001138c5f8e0e17bcf",
+      "sha256": "465839a468a8279d07d3c8167c4d089b395e8152665e2f71a656bca23c297a15",
+      "license": "Apache-2.0"
+    },
+    {
+      "retained_path": "vendor/pr4991/PROOF.md",
+      "source_commit": "99df28b2d9baafb1a0d82e45ce241bb33fa6f015",
+      "source_path": "research/two-image-dirty-volume/PROOF.md",
+      "git_blob": "013a1d10003481764d3d8af04c1d217d051ce349",
+      "sha256": "812aa297e22c444afde4920f119b519eab5b20685e6388ed725cc1748298d79e",
+      "license": "Apache-2.0"
+    },
+    {
+      "retained_path": "vendor/pr4991/SOURCES.json",
+      "source_commit": "99df28b2d9baafb1a0d82e45ce241bb33fa6f015",
+      "source_path": "research/two-image-dirty-volume/SOURCES.json",
+      "git_blob": "7cff1a85eae54adf714d1a5233d7db0244a6f5c7",
+      "sha256": "c7d1b4445ad9f11c4fb8b4e4db98debea06ba7a1bc42551760e1c917d473d6b9",
+      "license": "Apache-2.0"
+    },
+    {
+      "retained_path": "vendor/pr4998/PROOF.md",
+      "source_commit": "dd1bfbba907a62a8eaad696bcbfefafa421c752f",
+      "source_path": "research/two-image-compensated-pair/PROOF.md",
+      "git_blob": "c2d4d743f368d5e1cdf1955303f7d2d8a077b735",
+      "sha256": "bc07ad665eab28e8fbac7577b8ecb3cf35c24332688fc9354f5680199bfc727f",
+      "license": "Apache-2.0"
+    },
+    {
+      "retained_path": "vendor/pr4998/PROGRAM.json",
+      "source_commit": "dd1bfbba907a62a8eaad696bcbfefafa421c752f",
+      "source_path": "research/two-image-compensated-pair/PROGRAM.json",
+      "git_blob": "edcb335bc24f80738747d614f42f2815b84c25c7",
+      "sha256": "140eb578e7c1fc5ed3dfc47796b99ef953bae83153d430b412865f11b9bad983",
+      "license": "Apache-2.0"
+    }
+  ],
+  "independence": "No predecessor verifier is imported or executed. Original and phase-repair implementations are read as source definitions only; the PR4991 and PR4998 verifiers are not retained."
+}
diff --git a/research/two-image-volume-independent-audit/SOURCES.json b/research/two-image-volume-independent-audit/SOURCES.json
new file mode 100644
index 0000000000..28a71fd693
--- /dev/null
+++ b/research/two-image-volume-independent-audit/SOURCES.json
@@ -0,0 +1,81 @@
+{
+  "schema_version": 1,
+  "base_commit": "f259dabc7d70e0db8d6d36bfda888f008bbfecc1",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395",
+      "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602",
+      "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72"
+    },
+    {
+      "path": "research/two-image-volume-independent-audit/RETAINED-SOURCES.json",
+      "usage": "input",
+      "pin": "head:61b66445d137ccd84b7af350fb190a02adcf3ee2:research/two-image-volume-independent-audit/RETAINED-SOURCES.json",
+      "git_blob": "0f161187362c9373b225081aad5a8c1cd2748859",
+      "sha256": "aa9d3c29a330d44bb9e4b674effa5529a8d36a3dfec4e3a893f1357abc523e08"
+    },
+    {
+      "path": "research/two-image-volume-independent-audit/vendor/pr4688/README.md",
+      "usage": "input",
+      "pin": "head:61b66445d137ccd84b7af350fb190a02adcf3ee2:research/two-image-volume-independent-audit/vendor/pr4688/README.md",
+      "git_blob": "ac33ab36287fe1f1d9ba51b5360f44536c2ff3fc",
+      "sha256": "91d45b5af6063e30c6860a4cb46cfc44960ecd67f37c3bce9675924e30b89b4e"
+    },
+    {
+      "path": "research/two-image-volume-independent-audit/vendor/pr4688/verify.py",
+      "usage": "input",
+      "pin": "head:61b66445d137ccd84b7af350fb190a02adcf3ee2:research/two-image-volume-independent-audit/vendor/pr4688/verify.py",
+      "git_blob": "8d2815a2806894bcc50fb34e854f4ef7632ea588",
+      "sha256": "99ff0beccd9a4e94cc607e02114d62b8ce0ea57ee00748b07ce0a0af91aec85e"
+    },
+    {
+      "path": "research/two-image-volume-independent-audit/vendor/pr4710/README.md",
+      "usage": "input",
+      "pin": "head:61b66445d137ccd84b7af350fb190a02adcf3ee2:research/two-image-volume-independent-audit/vendor/pr4710/README.md",
+      "git_blob": "ef39626e0b25216d826d45371af1d181ab2754f1",
+      "sha256": "e866032429cb032f55edc9b2f3c6535ecf37680aae7cd9e8bb9b8cc21617aa64"
+    },
+    {
+      "path": "research/two-image-volume-independent-audit/vendor/pr4710/verify.py",
+      "usage": "input",
+      "pin": "head:61b66445d137ccd84b7af350fb190a02adcf3ee2:research/two-image-volume-independent-audit/vendor/pr4710/verify.py",
+      "git_blob": "1d81448d5f21fc98ffced8001138c5f8e0e17bcf",
+      "sha256": "465839a468a8279d07d3c8167c4d089b395e8152665e2f71a656bca23c297a15"
+    },
+    {
+      "path": "research/two-image-volume-independent-audit/vendor/pr4991/PROOF.md",
+      "usage": "input",
+      "pin": "head:61b66445d137ccd84b7af350fb190a02adcf3ee2:research/two-image-volume-independent-audit/vendor/pr4991/PROOF.md",
+      "git_blob": "013a1d10003481764d3d8af04c1d217d051ce349",
+      "sha256": "812aa297e22c444afde4920f119b519eab5b20685e6388ed725cc1748298d79e"
+    },
+    {
+      "path": "research/two-image-volume-independent-audit/vendor/pr4991/SOURCES.json",
+      "usage": "input",
+      "pin": "head:61b66445d137ccd84b7af350fb190a02adcf3ee2:research/two-image-volume-independent-audit/vendor/pr4991/SOURCES.json",
+      "git_blob": "7cff1a85eae54adf714d1a5233d7db0244a6f5c7",
+      "sha256": "c7d1b4445ad9f11c4fb8b4e4db98debea06ba7a1bc42551760e1c917d473d6b9"
+    },
+    {
+      "path": "research/two-image-volume-independent-audit/vendor/pr4998/PROGRAM.json",
+      "usage": "input",
+      "pin": "head:61b66445d137ccd84b7af350fb190a02adcf3ee2:research/two-image-volume-independent-audit/vendor/pr4998/PROGRAM.json",
+      "git_blob": "edcb335bc24f80738747d614f42f2815b84c25c7",
+      "sha256": "140eb578e7c1fc5ed3dfc47796b99ef953bae83153d430b412865f11b9bad983"
+    },
+    {
+      "path": "research/two-image-volume-independent-audit/vendor/pr4998/PROOF.md",
+      "usage": "input",
+      "pin": "head:61b66445d137ccd84b7af350fb190a02adcf3ee2:research/two-image-volume-independent-audit/vendor/pr4998/PROOF.md",
+      "git_blob": "c2d4d743f368d5e1cdf1955303f7d2d8a077b735",
+      "sha256": "bc07ad665eab28e8fbac7577b8ecb3cf35c24332688fc9354f5680199bfc727f"
+    }
+  ]
+}
diff --git a/research/two-image-volume-independent-audit/TASK.json b/research/two-image-volume-independent-audit/TASK.json
new file mode 100644
index 0000000000..861de7ae76
--- /dev/null
+++ b/research/two-image-volume-independent-audit/TASK.json
@@ -0,0 +1,129 @@
+{
+  "schema_version": 1,
+  "task_id": "formal-interface-lemma",
+  "priority_revision": 7,
+  "base_commit": "f259dabc7d70e0db8d6d36bfda888f008bbfecc1",
+  "original_card": {
+    "id": "formal-interface-lemma",
+    "question": "Can one uncovered interface implication be formalized with exact caller and certificate bindings?",
+    "starting_points": [
+      "docs/research/research-family-status.md",
+      "certificates/selected-result.json",
+      "research/gate-operand-parity-lean/README.md",
+      "research/staged544-certified-endpoint/README.md",
+      "research/unconditional-batched-crt/README.md"
+    ],
+    "methods": [
+      "Formalize a missing boundary lemma identified by the selected review.",
+      "Audit a formal theorem-to-certificate binding independently."
+    ],
+    "acceptance_gate": "State the exact formalized proposition and remaining assumptions; avoid duplicate arithmetic formalizations already present.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Inventory the gate-operand parity lemma (#3807) and certified endpoint arithmetic (#3857). Neither is a full multiplication proof. For #4100, audit the compact-switch statement and its hypotheses before formalizing it.",
+      "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately."
+    },
+    "first_experiment": "Write one missing statement with quantified hypotheses, actual caller and existing coverage. A compact-switch lemma is a candidate only after its mathematical contract is reviewed. Establish a bounded proof plan before a separately budgeted proof-assistant build; do not rerun large Lean jobs as orientation.",
+    "bottleneck_link": "A missing interface proof can reduce the conditional gap even if it does not change kappa.",
+    "allowed_variations": [
+      "Narrow to one formal lemma or one theorem-to-certificate binding."
+    ],
+    "scope_change_triggers": [
+      "Formalizing already-covered arithmetic and claiming the full multiplication theorem."
+    ],
+    "overlap_terms": [
+      "hyperplane end",
+      "formal interface",
+      "Lean binding",
+      "3807",
+      "3857",
+      "4100",
+      "gate-operand-parity-lean",
+      "staged544-certified-endpoint",
+      "unconditional-batched-crt"
+    ],
+    "existing_checks": [
+      {
+        "scope": "PR #3807: scoped gate-operand parity formalization.",
+        "evidence": "research/gate-operand-parity-lean/README.md",
+        "remaining": "Exact theorem-to-caller binding and genuinely uncovered interface lemmas.",
+        "status": "author-checked",
+        "source_commit": "4c3530f42a6abcc48e7a6bcffd6c901911dc8269",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "scope": "PR #3857: certified real-power moment/endpoint arithmetic.",
+        "evidence": "research/staged544-certified-endpoint/README.md",
+        "remaining": "Uniform algorithmic implications, not another endpoint digit.",
+        "status": "author-checked",
+        "source_commit": "ef4315b8caa605e47a2515004845eb2d2ed71a86",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "scope": "PR #4100: compact-switch formalization proposed as future validation.",
+        "evidence": "research/unconditional-batched-crt/README.md",
+        "remaining": "Audit the statement and assumptions before a formal proof campaign.",
+        "status": "author-checked",
+        "source_commit": "337d04939571a637aeab54a0f58f54fde811663a",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      }
+    ]
+  },
+  "scope_status": "refined",
+  "actual_scope": "Independently audit the full-width, all-fixed-complex-coefficient dirty-helper isolation theorem of PR4991 at the literal PR4688 and PR4710 prefixes, with PR4998 compensated output as a boundary control.",
+  "scope_change_reason": "The assigned task targets an author-checked theorem and its source binding, rather than existing arithmetic formalizations or the selected supplier. No clean workspace, width-dependent nonunitary word, or arbitrary permutation-pair extension is admitted.",
+  "bottleneck_link": "An independently checked completed-boundary obstruction prevents misusing a saturated prefix as a restored-dirty module; it does not change the selected conditional frontier.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop after an all-width proof audit and exact widths 1/2 source sanity checks, or one exact counterexample/missing implication. No native ranks, Lean, heavy matrix scan, or new supplier search.",
+  "outcome": "completed",
+  "evidence": "PROOF.md proves the all-width/all-fixed-complex-coefficient classification, including eventual-width tails; verify.py independently binds source phases and exact character/determinant checks at widths 1/2 plus the literal compensated boundary.",
+  "author": "JoyboyBrian",
+  "ai_assistance": "Substantial OpenAI Codex assistance in source audit, proof, code, and writing.",
+  "open_questions": [
+    {
+      "question": "Can the compensated inverse partner be consumed as an independently priced Gaussian target?",
+      "why_it_matters": "PR4998 escapes the isolation obstruction, but its transformed partner is not returned dirt or an admitted Gaussian job.",
+      "first_step": "Name one actual consumer and retain both independent outputs, precision, rational ADD, and tape charges.",
+      "blocked_by": "No such consumer or price contract is supplied by this audit."
+    }
+  ],
+  "first_fixture": {
+    "relative_operator": "R=U^-1 V from actual source address definitions and repaired P^-1Q with absolute phases",
+    "width_one_determinant": "3^4*5",
+    "curvature_witness": "D3*D1^64/D2^16=3^52/5^16",
+    "coefficient_cases": [
+      "alpha=0",
+      "beta=0",
+      "beta/alpha in {1,-1,i,-i}",
+      "pure-imaginary nonzero nonsingular ratio",
+      "general fixed complex nonzero ratio"
+    ],
+    "positive_boundary": "PR4998 diag(F,F^-1)"
+  },
+  "bounds": {
+    "direct_matrix_widths": [
+      1,
+      2
+    ],
+    "all_widths": "written character and affine-profile proof",
+    "all_complex_coefficients": "written classification plus singular rank-drop completion",
+    "local_check_budget_seconds": 10
+  },
+  "inherited_obligations": [
+    "Fixed finite bank count and fixed nonunitary word/coefficient/address data across widths.",
+    "Every input arbitrary and independent, every output prescribed; helper outputs identity or independently unitary.",
+    "No statement about clean-input subspaces, discarded outputs, width-dependent nonunitary words, or full multiplication theorem."
+  ],
+  "test_authoring_gate": {
+    "contract": "Literal source phases, full-state boundary, exact character multiplicities, and determinant-vs-rank branches.",
+    "credible_regression": "Tensorizing the sum, changing the absolute phase of Q, erasing arbitrary helper state, or calling the inverse partner returned dirt.",
+    "existing_coverage": "PR4991 is author-checked; this code-disjoint checker and written proof are the independent audit, including an explicit singular rank argument absent from its paragraph.",
+    "test_only_seams": "None. A standalone scoped verifier with direct semantic controls; no production exports or unrelated tests."
+  },
+  "new_contribution": "Independent quantifier/source audit; explicitly closes the singular-coefficient rank implication without changing the predecessor conclusion."
+}
diff --git a/research/two-image-volume-independent-audit/VERIFY.json b/research/two-image-volume-independent-audit/VERIFY.json
new file mode 100644
index 0000000000..4d2db2e64e
--- /dev/null
+++ b/research/two-image-volume-independent-audit/VERIFY.json
@@ -0,0 +1,43 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/two-image-volume-independent-audit/RETAINED-SOURCES.json",
+    "research/two-image-volume-independent-audit/vendor/pr4688/README.md",
+    "research/two-image-volume-independent-audit/vendor/pr4688/verify.py",
+    "research/two-image-volume-independent-audit/vendor/pr4710/README.md",
+    "research/two-image-volume-independent-audit/vendor/pr4710/verify.py",
+    "research/two-image-volume-independent-audit/vendor/pr4991/PROOF.md",
+    "research/two-image-volume-independent-audit/vendor/pr4991/SOURCES.json",
+    "research/two-image-volume-independent-audit/vendor/pr4998/PROGRAM.json",
+    "research/two-image-volume-independent-audit/vendor/pr4998/PROOF.md"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-Werror",
+        "-B",
+        "{package}/verify.py",
+        "--check",
+        "{package}/RESULT.json"
+      ],
+      "timeout_seconds": 10,
+      "checks": "Independent source characters/determinants at widths 1/2; exact phase conjugacy; compensated literal-program boundary and semantic controls."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-O",
+        "-B",
+        "{package}/verify.py",
+        "--check",
+        "{package}/RESULT.json"
+      ],
+      "timeout_seconds": 10,
+      "checks": "Independent source characters/determinants at widths 1/2; exact phase conjugacy; compensated literal-program boundary and semantic controls."
+    }
+  ]
+}
diff --git a/research/two-image-volume-independent-audit/vendor/pr4688/README.md b/research/two-image-volume-independent-audit/vendor/pr4688/README.md
new file mode 100644
index 0000000000..ac33ab3628
--- /dev/null
+++ b/research/two-image-volume-independent-audit/vendor/pr4688/README.md
@@ -0,0 +1,257 @@
+# An invertible two-call prefix attaining eight block-3 hook bounds
+
+**Result.** Two calls on one input can each gain the full 80 in eight
+width-five coordinate certificates, using one zero scratch register and a
+sum of two free address permutations between the calls. The scratch can be
+cleared, and the resulting operator is invertible at **every** positive digit
+width. Each of the two summands used alone gives a second gain of only 72.
+
+This is a scoped mathematical construction and an exact computational proof
+of its ranks. It makes the single-free-image obstruction in Jacob Sussman's
+[#4628](https://github.com/CrocSwap/integer-mult-bounds/pull/4628) sharp with
+respect to allowing two images, in this explicit example. It does **not**
+construct five transforms in fourteen calls, improve the call lower bound,
+or supply a new multiplication exponent. No Lean or human review is claimed.
+
+## 1. Was the proposed small-unit problem already solved?
+
+At the research checkpoint of 22 October 2026, canonical main was
+`b58ad9ef4d4e861b0eaa5dba41742bdc072dca51`. PR #4628 remained open at
+`ee4fd87f064017c23e5a86fc1dcfe0a5237caed3`; its source repository still had
+head `86e575e28ed94890872dcff1bb2621d7ff559cbd`. Both list block 3,
+five arrays in fourteen calls, as open in the engine game. The subsequent
+[#4643](https://github.com/CrocSwap/integer-mult-bounds/pull/4643) audits the
+projection bound at blocks at least 4; it does not settle this case.
+
+The overlap helper refreshed all pages of 445 open PR bodies and 3,589
+discussion records (snapshot times 15:29 and 15:31 UTC). Targeted PR search
+also included closed results. No resolution or competing claim for this
+prefix question was found. The sparse checkout searched only 36 of 5,860
+tracked package-note paths; neither this search nor the predecessor's open
+label proves global novelty. Exact source links are in section 6.
+
+## 2. Model and explicit program
+
+Addresses are triples $x=(x_0,x_1,x_2)\in\mathbb F_2^3$, encoded as
+$x_0+2x_1+4x_2$. Let $\mathcal V=\mathbb C^8$. A paid call is
+
+$$
+C=C_{e_0}=aI+bX_{e_0},\qquad
+a=(1+i)/2,\quad b=(1-i)/2,
+$$
+
+where $X_v e_x=e_{x+v}$. At digit width $f$, write
+$C_f=C^{\otimes f}$. The engine permits free invertible binary address
+maps on an array, applied identically in each column, and rational linear
+mixing of registers, including copies and erasures.
+
+Use just these two address permutations:
+
+$$
+Ue_{(x_0,x_1,x_2)}=e_{(x_0,x_1,x_2+x_0)},\qquad
+Ve_{(x_0,x_1,x_2)}=e_{(x_1,x_0,x_2)}.
+$$
+
+In address order $0,\ldots,7$, their images are respectively
+`[0,5,2,7,4,1,6,3]` and `[0,2,1,3,4,6,5,7]`.
+Write $U_f=U^{\otimes f}$, $V_f=V^{\otimes f}$.
+The prefix returns
+
+$$
+F_{2,f}y=C_f(U_f+2V_f)C_fy. \tag{1}
+$$
+
+An actual two-register implementation, starting from $(r_0,r_1)=(y,0)$, is:
+
+1. $r_0\leftarrow C_f r_0$. **One paid call.**
+2. $r_1\leftarrow r_0$; $r_1\leftarrow U_f r_1$.
+3. $r_0\leftarrow V_f r_0$; $r_1\leftarrow r_1+2r_0$.
+4. $r_0\leftarrow V_f r_0$, restoring $u=C_fy$, since $V^2=I$.
+5. $r_1\leftarrow C_f r_1$. **One paid call.** The state is $(u,F_{2,f}y)$.
+6. Apply the free mixing matrix $\left(\begin{smallmatrix}0&1\\0&0\end{smallmatrix}\right)$,
+   returning $(F_{2,f}y,0)$.
+
+This uses two rank-one calls, one initially zero scratch register, integer
+mixing coefficients, and no phase letters. No input copy outside these two
+registers is assumed. In particular, the sum in (1) is implemented by mixing;
+it is **not** $(U+2V)^{\otimes f}$.
+
+## 3. Invertibility at every width
+
+Both $U$ and $V$ are involutions. Put $R=U^{-1}V=UV$.
+As an address permutation,
+
+$$
+R=(0)(4)(1\ 2\ 5\ 6)(3\ 7),\qquad R^4=I.
+$$
+
+Consequently $R_f=R^{\otimes f}$ also satisfies $R_f^4=I$, and
+
+$$
+(I+2R_f)(I-2R_f+4R_f^2-8R_f^3)=-15I.
+$$
+
+Since $U_f+2V_f=U_f(I+2R_f)$, this supplies an explicit inverse using
+fixed rational coefficients, for every $f$. The two factors $C_f$ are
+invertible as well. Thus (1) is invertible at every width, and clearing
+$u$ in step 6 loses no input information. This is an analytic all-width
+proof; it does not infer uniform correctness from the width-five experiment.
+
+## 4. Exact simultaneous equality in eight cuts
+
+At width five restrict to the invariant subspace
+$H=\mathcal V\otimes\Lambda^4\mathcal V$, of dimension $8\binom84=560$.
+For a single-column matrix $g$, its action is
+$\rho(g)=g\otimes\Lambda^4g$, with entries
+
+$$
+\rho(g)_{(y,S),(x,T)}=g_{yx}\det(g_{S,T}). \tag{2}
+$$
+
+Split the coordinate basis $e_x\otimes e_T$ into four classes:
+
+| Class | Condition | Size |
+|---|---|---:|
+| $O_0$ | $x\in T$, $\bigoplus_{t\in T}t=0$ | 56 |
+| $O_1$ | $x\in T$, $\bigoplus_{t\in T}t\ne0$ | 224 |
+| $O_2$ | $x\notin T$, $\bigoplus_{t\in T}t=0$ | 56 |
+| $O_3$ | $x\notin T$, $\bigoplus_{t\in T}t\ne0$ | 224 |
+
+The zero-XOR four-subsets are affine planes. For a mask $b$, let $N_b$
+span the classes selected by its four binary digits. Every affine address
+map preserves membership and zero XOR (four copies of a translation cancel).
+Every diagonal phase preserves each coordinate line. Hence every $N_b$
+below is kept by the engine's free letters. In particular $N_3$ is the
+usual hook, and $N_8$ is the published single-term certificate $O_c$.
+
+Let $q_b:H\to H/N_b$. For a state with one input and output maps
+$A_1,\ldots,A_r$, its potential is
+
+$$
+\Phi_b(A_1,\ldots,A_r)
+=\operatorname{rank}\begin{bmatrix}
+q_bA_1|_{N_b}\\ \vdots\\ q_bA_r|_{N_b}
+\end{bmatrix}.
+$$
+
+Put $D=\rho(C)$, $A=D\rho(U)D$, $B=D\rho(V)D$, and
+$K=\rho(C_{e_2}C_{e_1}C_{e_0})$. Here $A+2B$ is the restriction
+of the actual output family (1) to $H$; no tensor lift of a sum is taken.
+The complete exact calculation is:
+
+| Mask $b$ | $\dim N_b$ | $\Phi_b(D)$ | $\Phi_b(D,A)$ | $\Phi_b(D,B)$ | $\Phi_b(D,A+2B)$ | $\Phi_b(A+2B)$ | $\Phi_b(K)$ |
+|---:|---:|---:|---:|---:|---:|---:|---:|
+| 2 | 224 | 80 | 152 | 152 | 160 | 160 | 224 |
+| 3 | 280 | 80 | 152 | 152 | 160 | 160 | 224 |
+| 6 | 280 | 80 | 152 | 152 | 160 | 160 | 224 |
+| 7 | 336 | 80 | 152 | 152 | 160 | 160 | 224 |
+| 8 | 224 | 80 | 152 | 152 | 160 | 160 | 224 |
+| 9 | 280 | 80 | 152 | 152 | 160 | 160 | 224 |
+| 12 | 280 | 80 | 152 | 152 | 160 | 160 | 224 |
+| 13 | 336 | 80 | 152 | 152 | 160 | 160 | 224 |
+
+The rank 80 is the cap for **every** direction: a binary invertible address
+map sends $e_0$ to any nonzero direction and preserves $N_b$.
+The kept-subspace argument of #4628 therefore bounds the increase from one
+call by 80, even with scratch and singular mixing. These caps and demands
+reproduce the known bound $80s\ge224W$, or $s\ge14W/5$.
+They are calibration results, not new lower bounds.
+
+For our prefix the first increase is 80 and the second is
+$160-80=80$, simultaneously for every listed cut. The free steps in
+between retain $u$ up to an invertible free image and hence preserve its
+potential. The joint-state and final-state columns show that the erasure also
+preserves all eight potentials. With either branch alone the second
+increase is only $152-80=72$.
+
+**What is new.** A second call can be fully productive on all these cuts
+without receiving a fresh independent input: two free images of the same
+earlier output suffice, and the combined map can remain uniformly invertible.
+Thus the published obstruction for a *single* free image cannot be used as
+a pruning rule for arbitrary free linear combinations of that output.
+This does not dispute the predecessor's deliberately narrower statement.
+
+## 5. A singular control that the eight cuts do not distinguish
+
+Replacing coefficient 2 by 1 gives $F_{1,f}=C_f(U_f+V_f)C_f$.
+The checker also obtains $\Phi_b(F_{1,5}|_H)=160$ for every listed cut.
+Nevertheless this family is singular. Indeed its nullity is the multiplicity
+of eigenvalue $-1$ in $R_f$. The projection onto that eigenspace is
+$(I-R_f+R_f^2-R_f^3)/4$. Since the numbers of fixed addresses of
+$R^0,R^1,R^2,R^3$ are $8,2,4,2$, tensor traces give exactly
+
+$$
+\dim\ker F_{1,f}=\frac{8^f+4^f-2\cdot2^f}{4}>0\quad(f\ge1).
+$$
+
+It is 2 at width one and 8,432 at width five. Erasing the retained first
+output in this variant therefore destroys information while preserving all
+eight potentials. This is a concrete check that equality in these
+certificates does not itself certify injectivity or completion. Coefficient
+2 avoids this defect by the explicit inverse in section 3.
+
+## 6. Reproduction, status, and credit
+
+```sh
+python3.12 -B research/complex-two-image-hook-prefix/verify.py
+python3.12 -O -B research/complex-two-image-hook-prefix/verify.py
+python3.12 -B scripts/research_package.py --package research/complex-two-image-hook-prefix
+```
+
+The verifier uses the standard library and computes ranks exactly over
+$\mathbb Q(i)$, with Gaussian-integer elimination and exact common-divisor
+removal. The ranks over $\mathbb C$ are the same. It replaces $C$ by
+$I-iX_{e_0}$, removing a nonzero scalar: each affected block of a rank
+matrix is rescaled uniformly, so no rank changes. It expands exterior
+products directly, checks all 313,600 entries of the first call against the
+independent minor formula (2), and checks its square against
+$\rho(I-iX)^2=-32i\rho(X)$.
+
+Seven controls cover deletion of either summand, duplication of a summand,
+replacement of the second permutation by the identity, an incorrect cap of
+79, the wrong tensor lift of a sum, and the singular coefficient-1 variant.
+Independent cycle enumeration at widths 1, 2, 3 checks the nullity formula.
+Exploration used NumPy/modular ranks; **none of those exploratory calculations
+or external libraries is an input to the registered proof computation**.
+No Lean build, all-history replay, or full integer-multiplication verification
+is claimed or needed for this scope.
+
+`SOURCES.json` pins the originating catalogue and selected record in this
+branch's base history. The pending predecessor's exact URLs and document
+hashes are bibliographic references in this note and `TASK.json`; replay
+does not require fetching an unrelated PR's Git objects.
+
+Predecessor credit:
+
+- Jacob Sussman, [#4628 README](https://github.com/jacobalansussman/integer-mult-bounds/blob/ee4fd87f064017c23e5a86fc1dcfe0a5237caed3/research/complex-small-m-lower-bounds/README.md)
+  and [PROOF.md](https://github.com/jacobalansussman/integer-mult-bounds/blob/ee4fd87f064017c23e5a86fc1dcfe0a5237caed3/research/complex-small-m-lower-bounds/PROOF.md):
+  model, kept-subspace argument, 14/5 bound, and open shapes.
+- Sussman's [single-term gain package](https://github.com/jacobalansussman/wht-power-saving-lean/tree/86e575e28ed94890872dcff1bb2621d7ff559cbd/research/block-bounds-and-new-rules/programs/five-in-fourteen-block3)
+  and [block-bounds README, section 3.5](https://github.com/jacobalansussman/wht-power-saving-lean/blob/86e575e28ed94890872dcff1bb2621d7ff559cbd/research/block-bounds-and-new-rules/README.md):
+  the single-image cap 72, eight tight-certificate context, and the warning
+  that a width-five candidate can fail at width six. This package independently
+  derives and checks its explicit example; it does not import those programs
+  or recheck the predecessor's classification of every single-image class.
+- eumemic's [#288](https://github.com/CrocSwap/integer-mult-bounds/pull/288)
+  for the underlying certificate method; Swapnil Jain's P1/P2 as credited by
+  #4628; OpenAI for the engine's call and free-operation model.
+
+Prepared for lee-phys with substantial OpenAI Codex assistance in the
+derivation, search, code, and writing. No independent human review.
+Apache-2.0. No predecessor package or selected-result record is modified.
+
+## Open next questions
+
+1. **Can a full 5-in-14 program use this prefix?** It may start with two
+   saturated calls on one input, but the remaining schedule must deliver all
+   five independent targets at every width. First test the prefix's allowed
+   continuations against the per-array end conditions at width six; do not
+   accept a candidate from this rank table alone. No continuation is supplied.
+2. **Which additional invariant distinguishes the singular and invertible
+   variants while retaining useful call bounds?** Their eight potentials
+   agree despite different kernels. Start from the explicit order-four
+   eigenspace in section 5 and track where that information resides under
+   shared-register mixing. A global lower bound requires a new argument.
+
+The structured questions and the explicit change from the task card's
+selected-supplier scope are recorded in `TASK.json`.
diff --git a/research/two-image-volume-independent-audit/vendor/pr4688/verify.py b/research/two-image-volume-independent-audit/vendor/pr4688/verify.py
new file mode 100644
index 0000000000..8d2815a280
--- /dev/null
+++ b/research/two-image-volume-independent-audit/vendor/pr4688/verify.py
@@ -0,0 +1,313 @@
+#!/usr/bin/env python3
+"""Exact Gaussian-integer ranks for a two-image block-3 prefix.
+
+Standard library only; no input files, floating point, assertions, or outputs
+other than the report. See README.md for the mathematical scope.
+"""
+
+from itertools import combinations, permutations, product
+
+
+ZERO, ONE, MINUS_I = (0, 0), (1, 0), (0, -1)
+I_POWERS = (ONE, (0, 1), (-1, 0), MINUS_I)
+SUBSETS = tuple(combinations(range(8), 4))
+BASIS = tuple((x, subset) for x in range(8) for subset in SUBSETS)
+INDEX = {label: index for index, label in enumerate(BASIS)}
+CUTS = (2, 3, 6, 7, 8, 9, 12, 13)
+U_PERM = tuple(x ^ ((x & 1) << 2) for x in range(8))
+V_PERM = tuple(x ^ (((x ^ (x >> 1)) & 1) * 3) for x in range(8))
+
+
+def require(condition, message):
+    if not condition:
+        raise ValueError(message)
+
+
+def add(a, b):
+    return a[0] + b[0], a[1] + b[1]
+
+
+def sub(a, b):
+    return a[0] - b[0], a[1] - b[1]
+
+
+def mul(a, b):
+    return a[0] * b[0] - a[1] * b[1], a[0] * b[1] + a[1] * b[0]
+
+
+def gaussian_divide(a, b):
+    denominator = b[0] ** 2 + b[1] ** 2
+    require(denominator != 0, "division by zero")
+    real = a[0] * b[0] + a[1] * b[1]
+    imag = a[1] * b[0] - a[0] * b[1]
+    require(real % denominator == imag % denominator == 0,
+            "Gaussian division is not exact")
+    return real // denominator, imag // denominator
+
+
+def gaussian_gcd(a, b):
+    """Euclidean gcd, up to a unit, using nearest integer quotients."""
+    while b != ZERO:
+        denominator = b[0] ** 2 + b[1] ** 2
+        quotient = (
+            (a[0] * b[0] + a[1] * b[1] + denominator // 2) // denominator,
+            (a[1] * b[0] - a[0] * b[1] + denominator // 2) // denominator,
+        )
+        a, b = b, sub(a, mul(quotient, b))
+    return a
+
+
+def accumulate(vector, index, coefficient):
+    value = add(vector.get(index, ZERO), coefficient)
+    if value == ZERO:
+        vector.pop(index, None)
+    else:
+        vector[index] = value
+
+
+def wedge_sign(addresses):
+    if len(set(addresses)) != len(addresses):
+        return 0
+    inversions = sum(addresses[i] > addresses[j]
+                     for i in range(len(addresses))
+                     for j in range(i + 1, len(addresses)))
+    return -1 if inversions % 2 else 1
+
+
+def lift_direction(direction):
+    """Columns of rho(I - i X_direction) on V tensor exterior^4 V."""
+    require(1 <= direction < 8, "direction must be nonzero")
+    columns = []
+    for x, subset in BASIS:
+        column = {}
+        for choices in product((0, 1), repeat=5):
+            images = tuple(t ^ (direction if choice else 0)
+                           for t, choice in zip(subset, choices[1:]))
+            sign = wedge_sign(images)
+            if not sign:
+                continue
+            phase = I_POWERS[-sum(choices) % 4]
+            row = INDEX[x ^ (direction if choices[0] else 0), tuple(sorted(images))]
+            accumulate(column, row, (sign * phase[0], sign * phase[1]))
+        columns.append(column)
+    return columns
+
+
+def apply_permutation(permutation, columns):
+    """Apply rho(P), retaining the sign from sorting each exterior basis."""
+    require(sorted(permutation) == list(range(8)), "not a permutation")
+    action = []
+    for x, subset in BASIS:
+        images = tuple(permutation[t] for t in subset)
+        action.append((INDEX[permutation[x], tuple(sorted(images))], wedge_sign(images)))
+    return [{action[j][0]: (action[j][1] * value[0], action[j][1] * value[1])
+             for j, value in column.items()} for column in columns]
+
+
+def compose(left, right):
+    columns = []
+    for column in right:
+        result = {}
+        for j, coefficient in column.items():
+            for i, value in left[j].items():
+                accumulate(result, i, mul(value, coefficient))
+        columns.append(result)
+    return columns
+
+
+def add_columns(left, right):
+    columns = []
+    for a, b in zip(left, right):
+        result = a.copy()
+        for i, value in b.items():
+            accumulate(result, i, value)
+        columns.append(result)
+    return columns
+
+
+def scale_columns(columns, scalar):
+    return [{j: mul((scalar, 0), value) for j, value in column.items()}
+            for column in columns]
+
+
+def orbit_number(x, subset):
+    nonplane = int(bool(subset[0] ^ subset[1] ^ subset[2] ^ subset[3]))
+    return 2 * int(x not in subset) + nonplane
+
+
+def cut_indices(mask):
+    return tuple(i for i, label in enumerate(BASIS)
+                 if mask & (1 << orbit_number(*label)))
+
+
+def project(columns, indices):
+    """Rows of the map N -> H/N, in coordinate bases."""
+    inside = set(indices)
+    rows = {i: {} for i in range(len(BASIS)) if i not in inside}
+    for column_index, j in enumerate(indices):
+        for i, value in columns[j].items():
+            if i in rows:
+                rows[i][column_index] = value
+    return list(rows.values())
+
+
+def rank_exact(rows):
+    """Rank over Q(i), using span-preserving operations in Z[i].
+
+    Multiply a row by a nonzero pivot, subtract a pivot-row multiple, and
+    divide by a nonzero common Gaussian divisor. Content removal keeps the
+    coefficients small. This computes exact rank, not a modular lower bound.
+    """
+    pivots = {}
+    for source in rows:
+        row = source.copy()
+        while row:
+            column = min(row)
+            if column not in pivots:
+                pivots[column] = row
+                break
+            pivot = pivots[column]
+            a, b = row[column], pivot[column]
+            row = {j: mul(b, value) for j, value in row.items()}
+            for j, value in pivot.items():
+                coefficient = mul(a, value)
+                accumulate(row, j, (-coefficient[0], -coefficient[1]))
+            if row:
+                common = ZERO
+                for value in row.values():
+                    common = gaussian_gcd(common, value)
+                    if common[0] ** 2 + common[1] ** 2 == 1:
+                        break
+                if common[0] ** 2 + common[1] ** 2 > 1:
+                    row = {j: gaussian_divide(value, common) for j, value in row.items()}
+    return len(pivots)
+
+
+def check_lift(direction):
+    """Check every entry against a separate determinant definition."""
+    matrix = [[ZERO for _ in range(8)] for _ in range(8)]
+    for x in range(8):
+        matrix[x][x] = ONE
+        matrix[x ^ 1][x] = MINUS_I
+    orders = tuple((order, wedge_sign(order)) for order in permutations(range(4)))
+    minors = {}
+    for rows in SUBSETS:
+        for cols in SUBSETS:
+            total = ZERO
+            for order, sign in orders:
+                term = (sign, 0)
+                for i in range(4):
+                    term = mul(term, matrix[rows[i]][cols[order[i]]])
+                total = add(total, term)
+            minors[rows, cols] = total
+    for j, (x, cols) in enumerate(BASIS):
+        for i, (y, rows) in enumerate(BASIS):
+            expected = mul(matrix[y][x], minors[rows, cols])
+            require(direction[j].get(i, ZERO) == expected, "exterior lift disagrees with minor")
+
+
+def reject_rank(rows, incorrect, label):
+    observed = rank_exact(rows)
+    require(observed != incorrect, "negative control was accepted: " + label)
+
+
+def main():
+    require(tuple(sum(orbit_number(*label) == j for label in BASIS) for j in range(4))
+            == (56, 224, 56, 224), "coordinate class sizes changed")
+    direction = lift_direction(1)
+    check_lift(direction)
+    identity = [{j: ONE} for j in range(len(BASIS))]
+    shift = apply_permutation(tuple(x ^ 1 for x in range(8)), identity)
+    expected_square = [{i: mul((0, -32), value) for i, value in column.items()}
+                       for column in shift]
+    require(compose(direction, direction) == expected_square,
+            "rho(I-iX)^2 must equal -32i rho(X)")
+    first_branch = compose(direction, apply_permutation(U_PERM, direction))
+    second_branch = compose(direction, apply_permutation(V_PERM, direction))
+    combined = add_columns(first_branch, scale_columns(second_branch, 2))
+    singular_variant = add_columns(first_branch, second_branch)
+    target = compose(lift_direction(4), compose(lift_direction(2), direction))
+
+    print("mask dim first U-only V-only joint final lambda=1-final target", flush=True)
+    for mask in CUTS:
+        indices = cut_indices(mask)
+        first = project(direction, indices)
+        values = (rank_exact(first),
+                  rank_exact(first + project(first_branch, indices)),
+                  rank_exact(first + project(second_branch, indices)),
+                  rank_exact(first + project(combined, indices)),
+                  rank_exact(project(combined, indices)),
+                  rank_exact(project(singular_variant, indices)),
+                  rank_exact(project(target, indices)))
+        require(values == (80, 152, 152, 160, 160, 160, 224),
+                "rank profile failed for cut " + str(mask))
+        print(mask, len(indices), *values, flush=True)
+
+    indices = cut_indices(2)
+    first = project(direction, indices)
+    reject_rank(first + project(first_branch, indices), 160, "delete V branch")
+    reject_rank(first + project(second_branch, indices), 160, "delete U branch")
+    reject_rank(first + project(add_columns(first_branch, first_branch), indices),
+                160, "duplicate U branch")
+    square = compose(direction, direction)
+    reject_rank(first + project(add_columns(first_branch, square), indices),
+                160, "replace V by identity")
+    reject_rank(first, 79, "undercount first call")
+
+    # R = U^{-1} V has cycles of lengths 1, 1, 2, 4. Its fourth power is I.
+    require(all(U_PERM[U_PERM[x]] == V_PERM[V_PERM[x]] == x for x in range(8)),
+            "U and V must be involutions")
+    ratio = tuple(U_PERM[V_PERM[x]] for x in range(8))
+    remaining, lengths = set(range(8)), []
+    while remaining:
+        start = min(remaining)
+        cycle, x = [], start
+        while x not in cycle:
+            cycle.append(x)
+            remaining.remove(x)
+            x = ratio[x]
+        require(x == start, "invalid permutation cycle")
+        lengths.append(len(cycle))
+    require(sorted(lengths) == [1, 1, 2, 4], "ratio cycle type changed")
+
+    # Polynomial identity (I+2R)(I-2R+4R^2-8R^3) = -15I for R^4=I.
+    polynomial = [0] * 4
+    for i, a in enumerate((1, 2)):
+        for j, b in enumerate((1, -2, 4, -8)):
+            polynomial[(i + j) % 4] += a * b
+    require(polynomial == [-15, 0, 0, 0], "uniform inverse identity failed")
+
+    # Independent cycle enumeration at widths 1, 2, 3 checks the all-width
+    # nullity formula of the lambda=1 negative control.
+    for width in (1, 2, 3):
+        remaining = set(product(range(8), repeat=width))
+        even_cycles = 0
+        while remaining:
+            start = min(remaining)
+            x, length = start, 0
+            while True:
+                remaining.remove(x)
+                length += 1
+                x = tuple(ratio[t] for t in x)
+                if x == start:
+                    break
+            even_cycles += int(length % 2 == 0)
+        require(even_cycles == (8 ** width + 4 ** width - 2 * 2 ** width) // 4,
+                "singular-variant nullity formula failed")
+        require(even_cycles > 0, "lambda=1 incorrectly accepted as invertible")
+
+    # Mixing acts outside the tensor lift: on e_1 tensor e_1, the incorrect
+    # (U+V) tensor (U+V) has the cross term e_5 tensor e_2; the true sum does not.
+    tensor_sum, sum_tensor = {}, {}
+    for permutation in (U_PERM, V_PERM):
+        accumulate(tensor_sum, (permutation[1], permutation[1]), ONE)
+    for p, q in product((U_PERM, V_PERM), repeat=2):
+        accumulate(sum_tensor, (p[1], q[1]), ONE)
+    require(tensor_sum.get((5, 2), ZERO) == ZERO
+            and sum_tensor[(5, 2)] == ONE, "width-two lift control failed")
+    print("PASS_CONTROLS 7", flush=True)
+    print("PASS_COMPLEX_TWO_IMAGE_HOOK_PREFIX", flush=True)
+
+
+if __name__ == "__main__":
+    main()
diff --git a/research/two-image-volume-independent-audit/vendor/pr4710/README.md b/research/two-image-volume-independent-audit/vendor/pr4710/README.md
new file mode 100644
index 0000000000..ef39626e0b
--- /dev/null
+++ b/research/two-image-volume-independent-audit/vendor/pr4710/README.md
@@ -0,0 +1,152 @@
+# A target-compatible phase repair of the two-image block-3 prefix
+
+This package gives a necessary-condition obstruction for one proposed beginning of a five-array, fourteen-call unit, and an explicit phase repair that removes that obstruction. It does **not** give a completed unit or a new multiplication exponent.
+
+The starting construction is [lee-phys's PR #4688](https://github.com/CrocSwap/integer-mult-bounds/pull/4688), frozen at `264c4b3cb13c82d171de352ecf60486dfb8d2bd4`. That work proves that its two-call prefix is invertible at every digit width and gains the full 80 per call in eight block-3 hook cuts. We retain its exact rank engine unchanged, with its complete calibration and controls. Jacob Sussman's [PR #4628](https://github.com/CrocSwap/integer-mult-bounds/pull/4628), head `ee4fd87f064017c23e5a86fc1dcfe0a5237caed3`, supplies the engine model and hook lower bound. Neither predecessor claimed that hook equality itself guaranteed a completion.
+
+## The missing target-alignment condition
+
+Let `𝓥=C^8`, with addresses `x=x0+2*x1+4*x2`. Write
+
+- `C_j = ((1+i)/2) I + ((1-i)/2) X_j`, where `X_j` flips bit `j`;
+- `C=C_0` and `K=C_2 C_1 C_0`;
+- `U`: CNOT from bit 0 to bit 2;
+- `V`: swap bits 0 and 1.
+
+Every letter acts by its tensor power at digit width `f`; a sum is implemented by mixing registers **after** the individual tensor powers.
+
+At width five, use `H=𝓥 tensor exterior^4(𝓥)`, of dimension 560, and the eight coordinate subspaces `N_b` of #4688. If `q_b:H->H/N_b`, the target has rank 224 and any one paid rank-one call adds at most 80 quotient rows. The two prefixes are
+
+```
+F_old,f = C_f (U_f + 2 V_f) C_f,
+F_new,f = C_f (P_f + 2 Q_f) C_f,
+S e_x   = i^popcount(x) e_x,
+P       = S U S,
+Q       = S V S.
+```
+
+All factors in `P,Q` are admitted free letters. `S` is the product of the three one-coordinate S phases. Both prefixes use exactly two paid rank-one calls and one zero scratch register, with the same copy/mix/erase schedule as #4688 (replace its `U,V` branches by `P,Q`, and restore the retained first output using `Q^{-1}`). The second prefix contains genuine phase letters, not just Pauli signs.
+
+The exact ranks are:
+
+| Cuts `b` | `rank(q F_old)` | `rank([q K; q F_old])` | `rank(q F_new)` | `rank([q K; q F_new])` |
+|---|---:|---:|---:|---:|
+| 3, 6, 7 | 160 | **280** | 160 | **224** |
+| 2, 8, 9, 12, 13 | 160 | 224 | 160 | 224 |
+
+All restrictions have domain `N_b`. These are ranks over `Q(i)`, calculated by exact Gaussian integer elimination. As in the predecessor, the implementation replaces each `C` by `I-iX` to remove a nonzero scalar. The two branches have equal paid-word length, so their common scalar cancels consistently in every pencil; independent nonzero scaling of target rows also preserves every joint rank. The second column of joint ranks is the extra test; measuring only the rank of the prefix does not detect the first prefix's misalignment.
+
+### Why the original literal beginning needs at least fifteen calls
+
+Fix the target rowspace `T` on all five independent inputs, and let `E` be the rowspace of the current stacked quotient observations. Define the remaining target deficit
+
+```
+d_T(E) = dim(T+E) - dim(E).
+```
+
+A free operation sends `E` into a subspace of itself, so it cannot decrease this deficit. For a paid call, retain the previous quotient rows conceptually: modulo those rows, at most `rank(q C|N)=80` new independent rows can appear. Consequently a paid call decreases `d_T` by at most 80. This argument permits arbitrary scratch, singular mixing and erasure.
+
+Suppose the **first two paid calls** are exactly the original #4688 prefix on one fresh independent input, and the other four inputs have not received paid work. For cut 3, the current rowspace has rank 160 and its union with the five target rowspaces has rank `280+4*224=1176`. Thus the deficit is **1016**, exceeding the capacity `12*80=960` of the twelve remaining calls. At least thirteen further calls are needed, for at least fifteen total. Keeping the first output `C_f y` does not help: #4688 already certifies `rank([q C; q F_old])=rank(q F_old)=160`.
+
+The same calculation for `W` fresh inputs gives the total lower bound `ceil((224*W+56)/80)` for this literal beginning. For example, six inputs would need at least eighteen calls, so it cannot begin a six-in-seventeen unit either.
+
+This is not an obstruction to an arbitrarily pre-encoded or later occurrence of the same word, nor a lower bound excluding five in fourteen generally. It is a statement about this literal two-call beginning on one fresh input. The original prefix's invertibility and full local gains remain valid.
+
+For the repaired prefix, the corresponding deficit is `64+4*224=960`. It passes this necessary test exactly. This equality does not supply a continuation.
+
+## An exact all-width inverse
+
+Both `U,V` are involutions. The relative monomial is
+
+```
+R=P^{-1}Q = S^{-1} U^{-1} V S,
+R^4=I,
+(I+2R)(I-2R+4R^2-8R^3)=-15I.
+```
+
+The same identity holds for `R_f=R^{tensor f}` at every positive `f`. Since `P_f+2Q_f=P_f(I+2R_f)`, the free middle operator is invertible with a fixed rational inverse. The two outside calls are invertible too. Thus clearing the retained first output loses no input information. No inverse has to be executed by the forward prefix.
+
+There is also no width-dependent conditioning loss: all outside factors are unitary and the eigenvalues of `R_f` are fourth roots of unity. The singular values of the prefix therefore belong to `{1,sqrt(5),3}`, with both extremes present for every positive width. Its Euclidean condition number is exactly 3. The original prefix has this same property; it is not a unique benefit of the repair and is not a full outer precision theorem.
+
+## The natural higher-width hook tests also pass
+
+The result is stronger than a width-five numerical coincidence. Put
+
+```
+A=C P C,  B=C Q C,
+A5=rho(A), B5=rho(B), K5=rho(K),
+rho(g)=g tensor exterior^4(g).
+```
+
+The checker proves, separately for each of the eight cuts:
+
+1. `rank([q K5; q A5])=rank([q K5; q B5])=224`. Equivalently, each branch separately annihilates `ker(q K5)` after applying `q`.
+2. All four pencil matrices `q(A5+2 lambda B5)|N`, for `lambda=1,-1,i,-i`, have rank **160**.
+
+For `r` additional digit columns, use the invariant space `H tensor 𝓥^{tensor r}` and the kept subspace `N_b tensor 𝓥^{tensor r}`. The relative single-column matrix `A^{-1}B=C^{-1}RC` has fourth power one and eigenvalue multiplicities `4,2,1,1`. Multiplying by an invertible matrix in the additional columns reduces the quotient prefix to the direct sum of the four pencil evaluations, with the multiplicities of `(A^{-1}B)^{tensor r}`. Its rank is therefore exactly
+
+```
+160 * 8^r.
+```
+
+The branchwise kernel inclusions tensor with the additional columns, so the joint target-prefix rank is exactly `224*8^r`. This proves zero alignment defect and two maximal call gains for **all these lifted cuts**, at every `r>=0`. In particular the width-six ranks are 1280 for the prefix and 1792 for the target and joint state.
+
+This does not claim that every possible higher-width certificate passes, that all output end conditions hold, or that a multi-input completion exists.
+
+## A concrete residual interface for further work
+
+The repaired prefix also has an explicit all-width relation to the target. With Hermitian Paulis `Y_j=i X_j Z_j`, put
+
+```
+a=Y0 Z1,  W=Z0 Z2,  J=Z1 V C2,
+M=X1 V CNOT(2->0) Z1 S2 CZ02.
+```
+
+`J` uses one paid call and `M` is entirely free. The independent standard-library checker `verify_residual.py` multiplies actual 8-by-8 matrices over Gaussian rationals and verifies the two **word** identities
+
+```
+J W C0 P C0 = M C2,
+J W C0 Q C0 = K a.
+```
+
+Tensorize these identities separately and then add the second with coefficient 2. For every positive digit width,
+
+```
+J_f W_f F_new,f = M_f C2_f + 2 K_f a_f.
+```
+
+Thus the remaining contamination is exactly a free image of one paid call, rather than an unspecified operator. This gives a precise cross-input cancellation problem. The formula itself is not a saving: directly computing both terms is insufficient to deliver five independent targets in fourteen calls.
+
+The same checker verifies four actual free projector sectors, generated on input by the commuting Hermitian Paulis `a=Y0 Z1` and `b=Y2`. At width `f`, set `e(alpha,beta)=(I+alpha*a_f)(I+beta*b_f)/4`. The prefix transports this projector to `e(epsilon*alpha,epsilon*beta)`, where `epsilon=(-1)^f`. These projectors can pack pieces of distinct independent inputs and separate them after the two-call prefix, but the other pieces must also be preserved and eventually processed. This is a feasible interface, not a complete unit.
+
+## Reproduction
+
+Only the Python standard library is required. No network, solver, floating point rank, or source checkout is used.
+
+```sh
+python3 -B verify.py --check RESULT.json
+python3 -O -B verify.py --check RESULT.json
+```
+
+The checker authenticates the unchanged #4688 engine and README, runs that predecessor's complete calibration and seven controls, computes the new Gaussian ranks, verifies the four-point pencils and the actual monomial inverse, and checks the exact deficit arithmetic. It also invokes the independent Gaussian-rational residual checker, including its wrong-phase and wrong-coefficient controls. Regenerate the deterministic report with `python3 -B verify.py --out RESULT.json`.
+
+The frozen predecessor engine is retained under `vendor/pr4688`; its provenance and hashes are in `PINNED-SOURCES.json` and `NOTICE.md`. No Lean proof or human review is claimed.
+
+The registered repository replay is:
+
+```sh
+python3 scripts/research_package.py --package research/phase-aligned-two-call-prefix
+```
+
+## Open next questions
+
+1. Complete the repaired prefix to five independent transforms in fourteen calls. Start with the explicit residual identity and the four Pauli sectors, preserving every complementary input piece and restored scratch. A literal all-width continuation and its complete paid bill remain missing.
+2. Test other width-six invariant subspaces and output end conditions. The proof above covers every natural `H tensor V^r` hook lift; it does not cover every invariant of the engine game.
+
+The structured questions, scope change and current-priority provenance are recorded in `TASK.json`. The selected frontier is unchanged.
+
+## Attribution and review scope
+
+Prepared by Yiyang (@Lyy-iiis), with substantial OpenAI Codex assistance in parallel research, implementation and independent agent review. New work is Apache-2.0. Credit lee-phys's #4688 for the original two-image construction, rank engine and controls; Jacob Sussman's #4628 and its retained sources for the model and lower bound; and the predecessors credited in the unchanged source README. The new result is the target-deficit analysis, explicit phase repair, lifted-hook proof and residual interface. No independent human review or full multiplication-theorem verification is claimed.
+
+`SOURCES.json` authenticates the vendored files through their first preservation commit on this branch; their Git blob IDs are also checked equal to the files at the original #4688 head. The original commit, paths and SHA256 hashes are recorded separately in `PINNED-SOURCES.json`. No predecessor branch is merged or modified.
diff --git a/research/two-image-volume-independent-audit/vendor/pr4710/verify.py b/research/two-image-volume-independent-audit/vendor/pr4710/verify.py
new file mode 100644
index 0000000000..1d81448d5f
--- /dev/null
+++ b/research/two-image-volume-independent-audit/vendor/pr4710/verify.py
@@ -0,0 +1,178 @@
+#!/usr/bin/env python3
+"""Exact target alignment and a phase-corrected two-call prefix. Standard library only."""
+from __future__ import annotations
+import argparse
+import hashlib
+import types
+import json
+from pathlib import Path
+import sys
+sys.dont_write_bytecode = True
+ROOT = Path(__file__).resolve().parent
+PINS = {
+    'vendor/pr4688/verify.py': '99ff0beccd9a4e94cc607e02114d62b8ce0ea57ee00748b07ce0a0af91aec85e',
+    'vendor/pr4688/README.md': '91d45b5af6063e30c6860a4cb46cfc44960ecd67f37c3bce9675924e30b89b4e',
+}
+
+def require(ok, message):
+    if not ok:
+        raise ValueError(message)
+
+def load_engine():
+    authenticated = {}
+    for path, digest in PINS.items():
+        payload = (ROOT / path).read_bytes()
+        require(hashlib.sha256(payload).hexdigest() == digest,
+                'changed immutable predecessor: ' + path)
+        authenticated[path] = payload
+    path = ROOT / 'vendor/pr4688/verify.py'
+    module = types.ModuleType('pinned_pr4688')
+    module.__file__ = str(path)
+    # Compile the exact authenticated bytes; never consult an existing .pyc.
+    exec(compile(authenticated['vendor/pr4688/verify.py'], str(path), 'exec'), module.__dict__)
+    return module
+
+def monomial_compose(a, b):
+    return (tuple(a[0][b[0][x]] for x in range(8)),
+            tuple((b[1][x] + a[1][b[0][x]]) % 4 for x in range(8)))
+
+def monomial_inverse(a):
+    p = tuple(a[0].index(x) for x in range(8))
+    return p, tuple(-a[1][p[x]] % 4 for x in range(8))
+
+def monomial_checks(m):
+    identity = (tuple(range(8)), (0,) * 8)
+    phase = (identity[0], tuple(x.bit_count() % 4 for x in range(8)))
+    u, v = (tuple(m.U_PERM), identity[1]), (tuple(m.V_PERM), identity[1])
+    P = monomial_compose(phase, monomial_compose(u, phase))
+    Q = monomial_compose(phase, monomial_compose(v, phase))
+    ratio = monomial_compose(monomial_inverse(P), Q)
+    power = identity
+    powers = []
+    for k in range(4):
+        powers.append(power)
+        power = monomial_compose(ratio, power)
+    require(power == identity and all(x != identity for x in powers[1:]), 'ratio order is not four')
+    # The ratio equals S^{-1} U^{-1} V S as an actual monomial, not merely projectively.
+    conjugate = monomial_compose(monomial_inverse(phase),
+                    monomial_compose(monomial_inverse(u), monomial_compose(v, phase)))
+    require(ratio == conjugate, 'ratio conjugacy')
+    traces = []
+    for p, e in powers:
+        trace = (0, 0)
+        for x in range(8):
+            if p[x] == x:
+                trace = m.add(trace, m.I_POWERS[e[x]])
+        traces.append(trace)
+    require(traces == [(8, 0), (2, 0), (4, 0), (2, 0)], 'ratio traces')
+    # Exact polynomial multiplication, reduced using R^4 = I.
+    product = [0] * 4
+    for degree, coefficient in enumerate((1, -2, 4, -8)):
+        product[degree] += coefficient
+        product[(degree + 1) % 4] += 2 * coefficient
+    require(product == [-15, 0, 0, 0], 'all-width inverse polynomial')
+    bad_phases = list(ratio[1])
+    bad_phases[1] = (bad_phases[1] + 1) % 4
+    bad_ratio = (ratio[0], tuple(bad_phases))
+    bad_power = identity
+    for _ in range(4):
+        bad_power = monomial_compose(bad_ratio, bad_power)
+    require(bad_power != identity, 'wrong monomial phase must fail fourth-power check')
+    return {'P': {'permutation': P[0], 'phase_exponents_mod4': P[1]},
+            'Q': {'permutation': Q[0], 'phase_exponents_mod4': Q[1]},
+            'R': {'permutation': ratio[0], 'phase_exponents_mod4': ratio[1]},
+            'R_order': 4, 'traces_R_powers': traces,
+            'eigenvalue_multiplicities_1_minus1_i_minusi': [4, 2, 1, 1],
+            'inverse_polynomial_product': product,
+            'negative_control': 'one changed R phase fails R^4=I'}
+
+def main():
+    parser = argparse.ArgumentParser(description=__doc__)
+    parser.add_argument('--out', type=Path, help='write the deterministic exact report')
+    parser.add_argument('--check', type=Path, help='require exact equality with a stored JSON report')
+    args = parser.parse_args()
+    m = load_engine()
+    # Unchanged predecessor replay includes independent exterior-minor calibration,
+    # the paid-call cap and target ranks, and its seven negative controls.
+    m.main()
+    D = m.lift_direction(1)
+    K = m.compose(m.lift_direction(4), m.compose(m.lift_direction(2), D))
+    phases = [m.I_POWERS[(x.bit_count() + sum(t.bit_count() for t in subset)) % 4]
+              for x, subset in m.BASIS]
+    def phase_columns(columns):
+        return [{i: m.mul(phases[i], value) for i, value in column.items()} for column in columns]
+    def repaired_branch(permutation):
+        return m.compose(D, phase_columns(m.apply_permutation(permutation, phase_columns(D))))
+    def complex_scale(columns, coefficient):
+        return [{i: m.mul(coefficient, value) for i, value in column.items()} for column in columns]
+    old_A = m.compose(D, m.apply_permutation(m.U_PERM, D))
+    old_B = m.compose(D, m.apply_permutation(m.V_PERM, D))
+    old = m.add_columns(old_A, m.scale_columns(old_B, 2))
+    A, B = repaired_branch(m.U_PERM), repaired_branch(m.V_PERM)
+    new = m.add_columns(A, m.scale_columns(B, 2))
+    pencil = [m.add_columns(A, complex_scale(B, coefficient))
+              for coefficient in ((2, 0), (-2, 0), (0, 2), (0, -2))]
+    records = []
+    print('mask oldPhi oldJoint newPhi newJoint branchJoints pencilRanks', flush=True)
+    for mask in m.CUTS:
+        inside = m.cut_indices(mask)
+        target = m.project(K, inside)
+        old_rows, new_rows = m.project(old, inside), m.project(new, inside)
+        old_phi, new_phi = m.rank_exact(old_rows), m.rank_exact(new_rows)
+        # Put the structured target rows first to keep Gaussian intermediates small.
+        old_joint = m.rank_exact(target + old_rows)
+        new_joint = m.rank_exact(target + new_rows)
+        branch_joints = [m.rank_exact(target + m.project(branch, inside)) for branch in (A, B)]
+        pencil_ranks = [m.rank_exact(m.project(value, inside)) for value in pencil]
+        expected_old_joint = 280 if mask in (3, 6, 7) else 224
+        require((old_phi, old_joint, new_phi, new_joint) == (160, expected_old_joint, 160, 224),
+                'prefix/target alignment at mask ' + str(mask))
+        require(branch_joints == [224, 224], 'termwise all-width alignment at mask ' + str(mask))
+        require(pencil_ranks == [160] * 4, 'four-point pencil at mask ' + str(mask))
+        record = {'mask': mask, 'N_dimension': len(inside), 'target_rank': 224,
+                  'old_prefix_rank': old_phi, 'old_target_joint_rank': old_joint,
+                  'old_missing_target_dimensions': old_joint - old_phi,
+                  'new_prefix_rank': new_phi, 'new_target_joint_rank': new_joint,
+                  'new_missing_target_dimensions': new_joint - new_phi,
+                  'new_single_branch_target_joint_ranks': branch_joints,
+                  'new_pencil_ranks_coefficients_2_minus2_2i_minus2i': pencil_ranks,
+                  'width6_lifted_prefix_rank': sum(w*r for w,r in zip((4,2,1,1), pencil_ranks)),
+                  'width6_lifted_target_and_joint_rank': 8 * 224}
+        records.append(record)
+        print(mask, old_phi, old_joint, new_phi, new_joint, branch_joints, pencil_ranks, flush=True)
+    require(records[1]['old_missing_target_dimensions'] + 4 * 224 == 1016,
+            'five-array remaining deficit')
+    require(1016 > 12 * 80, 'original prefix obstruction')
+    require(records[1]['new_missing_target_dimensions'] + 4 * 224 == 12 * 80,
+            'repaired remaining deficit')
+    monomials = monomial_checks(m)
+    residual_path = ROOT / 'verify_residual.py'
+    residual = types.ModuleType('independent_residual')
+    residual.__file__ = str(residual_path)
+    exec(compile(residual_path.read_bytes(), str(residual_path), 'exec'), residual.__dict__)
+    residual_report = residual.verify()
+    report = {'schema_version': 1,
+              'source_pr': 4688, 'source_head': '264c4b3cb13c82d171de352ecf60486dfb8d2bd4',
+              'source_sha256': PINS,
+              'scope': 'two-call prefix and necessary continuation conditions; no completed unit or new exponent',
+              'arithmetic': 'Gaussian integer elimination over Q(i), no numerical rank tolerance',
+              'cuts': records, 'monomial_inverse': monomials,
+              'exact_residual_interface': residual_report,
+              'all_extra_widths': {'extra_width_variable': 'r >= 0',
+                 'prefix_rank_each_lifted_cut': '160*8^r',
+                 'target_and_joint_rank_each_lifted_cut': '224*8^r',
+                 'proof': 'four eigenvalues of relative branch matrix; four-point pencil ranks and termwise kernel inclusion'},
+              'original_five_array_remaining_deficit': 1016,
+              'remaining_twelve_call_capacity': 960,
+              'repaired_five_array_remaining_deficit': 960,
+              'result': 'PASS'}
+    # Normalize tuples before comparing the JSON encoding.
+    report = json.loads(json.dumps(report))
+    if args.check:
+        require(json.loads(args.check.read_text()) == report, 'stored report mismatch')
+    if args.out:
+        args.out.write_text(json.dumps(report, indent=2, sort_keys=True) + '\n')
+    print('PASS_PHASE_PREFIX_TARGET_ALIGNMENT', flush=True)
+
+if __name__ == '__main__':
+    main()
diff --git a/research/two-image-volume-independent-audit/vendor/pr4991/PROOF.md b/research/two-image-volume-independent-audit/vendor/pr4991/PROOF.md
new file mode 100644
index 0000000000..013a1d1000
--- /dev/null
+++ b/research/two-image-volume-independent-audit/vendor/pr4991/PROOF.md
@@ -0,0 +1,201 @@
+# A tensor-width volume obstruction to isolating the two-image prefix
+
+Prepared by Cinna Davis with substantial OpenAI Codex assistance. Apache-2.0.
+Written theorem with exact corroboration; no Lean, independent human review,
+new κ, or complete small-unit exclusion is claimed.
+
+## 1. Completed interface, rather than an intermediate prefix
+
+Let V=C^8. Fix the actual permutations U and V_0 of lee-phys's PR4688:
+U is CNOT from bit 0 to bit 2, and V_0 swaps bits 0 and 1. Define
+
+`C = ((1+i)/2) I + ((1-i)/2) X_0`,
+`S e_x = i^popcount(x) e_x`, `P=S U S`, `Q=S V_0 S`.
+
+For any base letter g, write `g_f=g^(tensor f)`. Scalar coefficients act
+**after** individual letters have been tensorized. The two source prefixes are
+
+`F_f = C_f (U_f + 2 V_0,f) C_f`,
+`F'_f = C_f (P_f + 2 Q_f) C_f`.
+
+PR4688 proves the first family's invertibility and two-call implementation
+with one initially zero scratch array and a copy/mix/erase schedule. Yiyang's
+PR4710 supplies the phase repair. Dugongue's PR4743 supplies a different,
+reversible two-input triangular interface with this prefix off diagonal.
+None of those statements promises the following completed interface:
+
+`(x,z_1,...,z_s) -> (F_f x, z_1,...,z_s)`                 (1)
+
+for arbitrary independent x and arbitrary dirty z_j. The same distinction
+applies to F'_f. We test exactly (1). We may also allow independent unitary
+outputs on the helper banks, since they have unit absolute determinant.
+
+## 2. An enlarged uniform-word model
+
+Fix any finite number of array banks, each of dimension d_f=8^f, and one
+finite word whose register coefficients, base letters, bank count and word
+length do not change with f. Permit these full-state linear operations:
+
+1. Any fixed complex register mixing M, acting as `M tensor I_(d_f)`.
+2. Any fixed invertible 8-by-8 base address matrix B, acting as B_f on a
+   selected bank. Several banks or products are permitted.
+3. Arbitrary unitary full-state operations, even width-dependent ones.
+
+This grants much more than the source engine's free address permutations
+and phases, and includes every unitary paid C direction and its inverse.
+It does not price those extra grants or call them physically free. They
+make the impossibility statement stronger. No nonlinear operation or
+width-dependent nonunitary mixing coefficient is included.
+
+All banks are arbitrary independent inputs; all final banks are prescribed.
+There is no owned zero input, omitted output, or discarded input-dependent
+garbage. If the final map is invertible, every full-state factor is invertible:
+a singular square factor cannot occur in an invertible product. Thus allowing
+singular mixing syntactically cannot evade the determinant argument for this
+completed contract. This reasoning does not apply on a proper clean-input
+subspace, which is why the original clean-prefix construction is compatible
+with the result.
+
+**Uniform volume lemma.** For every word in this model with an invertible
+output, its normalized absolute log determinant is affine in f:
+
+`log |det T_f| / 8^f = a + b f`.                           (2)
+
+Indeed a register mixing contributes `log |det M|`, independent of f. A
+single-bank address letter has
+`det(B^(tensor f)) = (det B)^(f 8^(f-1))`, by induction from the Kronecker
+determinant formula, so contributes `(f/8) log |det B|`. A unitary full-state
+letter contributes zero. Determinants multiply, proving (2). For the narrower
+source game with only unitary address letters, b=0. Bank permutations and
+permitted free input/output frame changes have the same affine profile.
+
+This is an elementary determinant invariant. The new source-specific content
+is the profile below and what it excludes for these completed interfaces.
+
+## 3. Exact determinant profile of both retained prefixes
+
+The permutation `R=U^-1 V_0` has cycles
+
+`(0)(4)(1 2 5 6)(3 7)`.
+
+Its four power traces are `(8,2,4,2)`. Consequently R_f has eigenvalue
+multiplicities
+
+`m_1 = (8^f + 4^f + 2*2^f)/4`,
+`m_-1 = (8^f + 4^f - 2*2^f)/4`,
+`m_i = m_-i = (8^f - 4^f)/4`.                             (3)
+
+These follow from the four order-four character projectors: traces tensorize,
+so their numerators use 8^f, 2^f, 4^f and 2^f. They can also be obtained
+directly from the lengths of R_f's permutation cycles. All four
+multiplicities are positive for every f>=1.
+
+The paid C_f and U_f are unitary. Factor the middle sum as
+`U_f (I+2R_f)`. The +1 eigenspace contributes 3, the -1 eigenspace
+contributes -1, and an i/-i pair contributes `(1+2i)(1-2i)=5`. Hence
+
+`D_f := |det F_f| = 3^(m_1) 5^(m_i)`.                    (4)
+
+For the repaired word, `P^-1 Q = S^-1 R S` as actual matrices with absolute
+phases. It has exactly the same spectrum at every f. P_f and both paid
+factors are unitary, so `|det F'_f|=D_f` too. Projective equality would
+not suffice for this assertion; the source phase convention is retained.
+
+In particular:
+
+| Width f | Dimension | exponent of 3 in D_f | exponent of 5 in D_f |
+|---|---:|---:|---:|
+| 1 | 8 | 4 | 1 |
+| 2 | 64 | 22 | 12 |
+| 3 | 512 | 148 | 112 |
+
+If (2) held, its second difference at these three widths would vanish.
+Clearing the denominators 8,64,512 gives
+
+`D_3 D_1^64 / D_2^16 = 1`.
+
+But (4) gives the exact ratio `3^52/5^16`, which is not one. Thus **neither
+prefix can be isolated as (1)** by any finite uniform word in the enlarged
+model. The number of unitary paid calls is unrestricted. The contradiction
+still holds with any number of independent unitary helper targets, since
+their absolute determinants are one. It is unaffected by allowed free
+frame changes, which add only an affine profile.
+
+In the source's narrower unitary-address game, already widths one and two
+contradict a constant normalized determinant:
+
+`D_2 / D_1^8 = 5^4/3^10 != 1`.
+
+This is a completed-module obstruction. It is not a lower bound on every
+continuation of the original prefix and does not exclude five-in-fourteen.
+
+## 4. Tuning the two mixing coefficients cannot repair this contract
+
+The same conclusion holds for
+`C_f(alpha U_f + beta V_0,f) C_f`, and for the repaired P,Q pair,
+for **every fixed complex alpha,beta with alpha beta != 0**.
+
+Put t=beta/alpha. If t is one of ±1,±i, (3) makes the mixture singular
+already at width one and indeed at every width. Otherwise all logs below
+are finite. Set
+
+`A=log|1+t|`, `B=log|1-t|`, `E=log|1+t²|`.
+
+Using (3), the normalized log determinant of the middle mixture is
+
+`log|alpha| + (A+B+E)/4 + (A+B-E)/(4*2^f) + (A-B)/(2*4^f)`. (5)
+
+It is bounded and converges. If it were affine in f for every positive
+width, or even every sufficiently large width, its affine slope would
+be zero. The two distinct decaying sequences in (5) then force
+`A=B` and `A+B=E`. The first equation gives Re(t)=0; write t=i y with
+real y. The second becomes `1+y²=|1-y²|`, forcing y=0. This contradicts
+alpha beta != 0.
+
+The classification deliberately leaves the single-image cases alpha=0 or
+beta=0 available. Their normalized determinant is constant and the original
+single-branch word is implementable with its ordinary calls and scalar mix.
+The theorem does not infer impossibility of arbitrary pairs of permutations;
+it uses this exact order-four spectral distribution.
+
+## 5. Why the existing dirty-target port is a positive control
+
+PR4743's two-input port has the actual block form
+
+`T_f = [[C_f, 0], [F'_f, C_f]]`.
+
+Its determinant is `det(C_f)^2`, with absolute value one. F'_f is
+off diagonal and is dependent information about the first input; both
+diagonal channels remain present. This port is therefore compatible with
+(2) and is not (1). Extracting F'_f as an independent diagonal output while
+returning the other arbitrary input unchanged would be a new contract.
+
+Similarly a nonunitary compensating helper output such as an inverse-volume
+partner can remove the volume obstruction. The determinant lemma supplies
+no construction of that partner, its Gaussian compatibility, its precision,
+or its invoice. Clean initialized scratch, nonuniform width-dependent
+coefficients, changing the number of banks with f, nonlinear operations,
+or a different global continuation also lie outside the proved exclusion.
+
+## 6. Executed evidence and limits
+
+The independent standard-library verifier authenticates five main inputs
+with SHA256 and Git blob ids. It checks the source permutation definitions
+without importing its rank engine, constructs the coordinate maps separately,
+and checks the repaired ratio's exact phase conjugacy. Direct tensor-cycle
+enumeration at widths one through four agrees with (3). Separate exact
+Gaussian-rational matrix elimination at widths one and two agrees with (4)
+for both prefix variants. These checks operate on the individually tensorized
+monomial branches; they do not tensorize a sum.
+
+It also checks a unit-volume triangular positive case, allowed affine-profile
+examples, the complex-coefficient identities used in section 4, the singular
+coefficient-one control, and the available single-image case. The finite
+checks corroborate the proof; the all-width and all-coefficient statements
+come from sections 2–4. No large hook-rank replay, native supplier suite,
+five-in-fourteen schedule audit, selected cold replay or Lean build is run.
+
+The source scalar program, the phase repair, the triangular native ports,
+their rank and conditioning evidence, and all their original attribution
+remain unchanged. This result adds a volume invariant for one new completed
+dirty-helper boundary, without changing the selected conditional frontier.
diff --git a/research/two-image-volume-independent-audit/vendor/pr4991/SOURCES.json b/research/two-image-volume-independent-audit/vendor/pr4991/SOURCES.json
new file mode 100644
index 0000000000..7cff1a85ea
--- /dev/null
+++ b/research/two-image-volume-independent-audit/vendor/pr4991/SOURCES.json
@@ -0,0 +1,48 @@
+{
+  "schema_version": 1,
+  "base_commit": "b91956876e5b4122fd89179f1b57557ff8378f15",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395",
+      "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602",
+      "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72"
+    },
+    {
+      "path": "research/complex-prefix-native-ports/FULL-INPUT-PORT.md",
+      "usage": "input",
+      "git_blob": "39a461f2fbf2e009423cd784f56de121d190d842",
+      "sha256": "52b8462e28f9e87925ccfea27872630e2b2da23f19fd3d2265c2654bc016088c"
+    },
+    {
+      "path": "research/complex-two-image-hook-prefix/README.md",
+      "usage": "input",
+      "git_blob": "ac33ab36287fe1f1d9ba51b5360f44536c2ff3fc",
+      "sha256": "91d45b5af6063e30c6860a4cb46cfc44960ecd67f37c3bce9675924e30b89b4e"
+    },
+    {
+      "path": "research/complex-two-image-hook-prefix/verify.py",
+      "usage": "input",
+      "git_blob": "8d2815a2806894bcc50fb34e854f4ef7632ea588",
+      "sha256": "99ff0beccd9a4e94cc607e02114d62b8ce0ea57ee00748b07ce0a0af91aec85e"
+    },
+    {
+      "path": "research/phase-aligned-two-call-prefix/README.md",
+      "usage": "input",
+      "git_blob": "ef39626e0b25216d826d45371af1d181ab2754f1",
+      "sha256": "e866032429cb032f55edc9b2f3c6535ecf37680aae7cd9e8bb9b8cc21617aa64"
+    },
+    {
+      "path": "research/phase-aligned-two-call-prefix/verify.py",
+      "usage": "input",
+      "git_blob": "1d81448d5f21fc98ffced8001138c5f8e0e17bcf",
+      "sha256": "465839a468a8279d07d3c8167c4d089b395e8152665e2f71a656bca23c297a15"
+    }
+  ]
+}
diff --git a/research/two-image-volume-independent-audit/vendor/pr4998/PROGRAM.json b/research/two-image-volume-independent-audit/vendor/pr4998/PROGRAM.json
new file mode 100644
index 0000000000..edcb335bc2
--- /dev/null
+++ b/research/two-image-volume-independent-audit/vendor/pr4998/PROGRAM.json
@@ -0,0 +1,1316 @@
+{
+  "original": [
+    {
+      "bank": 0,
+      "op": "paid_C"
+    },
+    {
+      "bank": 1,
+      "op": "paid_C"
+    },
+    {
+      "bank": 1,
+      "letter": "X",
+      "op": "address",
+      "restores_shear_source": false
+    },
+    {
+      "coefficient": [
+        -1,
+        1
+      ],
+      "destination": 0,
+      "op": "add",
+      "source": 1
+    },
+    {
+      "coefficient": [
+        1,
+        1
+      ],
+      "destination": 1,
+      "op": "add",
+      "source": 0
+    },
+    {
+      "coefficient": [
+        -1,
+        1
+      ],
+      "destination": 0,
+      "op": "add",
+      "source": 1
+    },
+    {
+      "bank": 1,
+      "letter": "U",
+      "op": "address",
+      "restores_shear_source": false
+    },
+    {
+      "coefficient": [
+        1,
+        1
+      ],
+      "destination": 0,
+      "op": "add",
+      "source": 1
+    },
+    {
+      "bank": 1,
+      "letter": "U",
+      "op": "address",
+      "restores_shear_source": true
+    },
+    {
+      "bank": 1,
+      "letter": "V",
+      "op": "address",
+      "restores_shear_source": false
+    },
+    {
+      "coefficient": [
+        2,
+        1
+      ],
+      "destination": 0,
+      "op": "add",
+      "source": 1
+    },
+    {
+      "bank": 1,
+      "letter": "V",
+      "op": "address",
+      "restores_shear_source": true
+    },
+    {
+      "bank": 0,
+      "letter": "U",
+      "op": "address",
+      "restores_shear_source": false
+    },
+    {
+      "coefficient": [
+        1,
+        15
+      ],
+      "destination": 1,
+      "op": "add",
+      "source": 0
+    },
+    {
+      "bank": 0,
+      "letter": "U",
+      "op": "address",
+      "restores_shear_source": true
+    },
+    {
+      "bank": 0,
+      "letter": "U",
+      "op": "address",
+      "restores_shear_source": false
+    },
+    {
+      "bank": 0,
+      "letter": "V",
+      "op": "address",
+      "restores_shear_source": false
+    },
+    {
+      "bank": 0,
+      "letter": "U",
+      "op": "address",
+      "restores_shear_source": false
+    },
+    {
+      "coefficient": [
+        -2,
+        15
+      ],
+      "destination": 1,
+      "op": "add",
+      "source": 0
+    },
+    {
+      "bank": 0,
+      "letter": "U",
+      "op": "address",
+      "restores_shear_source": true
+    },
+    {
+      "bank": 0,
+      "letter": "V",
+      "op": "address",
+      "restores_shear_source": true
+    },
+    {
+      "bank": 0,
+      "letter": "U",
+      "op": "address",
+      "restores_shear_source": true
+    },
+    {
+      "bank": 0,
+      "letter": "U",
+      "op": "address",
+      "restores_shear_source": false
+    },
+    {
+      "bank": 0,
+      "letter": "V",
+      "op": "address",
+      "restores_shear_source": false
+    },
+    {
+      "bank": 0,
+      "letter": "U",
+      "op": "address",
+      "restores_shear_source": false
+    },
+    {
+      "bank": 0,
+      "letter": "V",
+      "op": "address",
+      "restores_shear_source": false
+    },
+    {
+      "bank": 0,
+      "letter": "U",
+      "op": "address",
+      "restores_shear_source": false
+    },
+    {
+      "coefficient": [
+        4,
+        15
+      ],
+      "destination": 1,
+      "op": "add",
+      "source": 0
+    },
+    {
+      "bank": 0,
+      "letter": "U",
+      "op": "address",
+      "restores_shear_source": true
+    },
+    {
+      "bank": 0,
+      "letter": "V",
+      "op": "address",
+      "restores_shear_source": true
+    },
+    {
+      "bank": 0,
+      "letter": "U",
+      "op": "address",
+      "restores_shear_source": true
+    },
+    {
+      "bank": 0,
+      "letter": "V",
+      "op": "address",
+      "restores_shear_source": true
+    },
+    {
+      "bank": 0,
+      "letter": "U",
+      "op": "address",
+      "restores_shear_source": true
+    },
+    {
+      "bank": 0,
+      "letter": "U",
+      "op": "address",
+      "restores_shear_source": false
+    },
+    {
+      "bank": 0,
+      "letter": "V",
+      "op": "address",
+      "restores_shear_source": false
+    },
+    {
+      "bank": 0,
+      "letter": "U",
+      "op": "address",
+      "restores_shear_source": false
+    },
+    {
+      "bank": 0,
+      "letter": "V",
+      "op": "address",
+      "restores_shear_source": false
+    },
+    {
+      "bank": 0,
+      "letter": "U",
+      "op": "address",
+      "restores_shear_source": false
+    },
+    {
+      "bank": 0,
+      "letter": "V",
+      "op": "address",
+      "restores_shear_source": false
+    },
+    {
+      "bank": 0,
+      "letter": "U",
+      "op": "address",
+      "restores_shear_source": false
+    },
+    {
+      "coefficient": [
+        -8,
+        15
+      ],
+      "destination": 1,
+      "op": "add",
+      "source": 0
+    },
+    {
+      "bank": 0,
+      "letter": "U",
+      "op": "address",
+      "restores_shear_source": true
+    },
+    {
+      "bank": 0,
+      "letter": "V",
+      "op": "address",
+      "restores_shear_source": true
+    },
+    {
+      "bank": 0,
+      "letter": "U",
+      "op": "address",
+      "restores_shear_source": true
+    },
+    {
+      "bank": 0,
+      "letter": "V",
+      "op": "address",
+      "restores_shear_source": true
+    },
+    {
+      "bank": 0,
+      "letter": "U",
+      "op": "address",
+      "restores_shear_source": true
+    },
+    {
+      "bank": 0,
+      "letter": "V",
+      "op": "address",
+      "restores_shear_source": true
+    },
+    {
+      "bank": 0,
+      "letter": "U",
+      "op": "address",
+      "restores_shear_source": true
+    },
+    {
+      "bank": 1,
+      "letter": "U",
+      "op": "address",
+      "restores_shear_source": false
+    },
+    {
+      "coefficient": [
+        1,
+        1
+      ],
+      "destination": 0,
+      "op": "add",
+      "source": 1
+    },
+    {
+      "bank": 1,
+      "letter": "U",
+      "op": "address",
+      "restores_shear_source": true
+    },
+    {
+      "bank": 1,
+      "letter": "V",
+      "op": "address",
+      "restores_shear_source": false
+    },
+    {
+      "coefficient": [
+        2,
+        1
+      ],
+      "destination": 0,
+      "op": "add",
+      "source": 1
+    },
+    {
+      "bank": 1,
+      "letter": "V",
+      "op": "address",
+      "restores_shear_source": true
+    },
+    {
+      "bank": 0,
+      "op": "paid_C"
+    },
+    {
+      "bank": 1,
+      "op": "paid_C"
+    },
+    {
+      "bank": 1,
+      "letter": "X",
+      "op": "address",
+      "restores_shear_source": false
+    }
+  ],
+  "phase_repaired": [
+    {
+      "bank": 0,
+      "op": "paid_C"
+    },
+    {
+      "bank": 1,
+      "op": "paid_C"
+    },
+    {
+      "bank": 1,
+      "letter": "X",
+      "op": "address",
+      "restores_shear_source": false
+    },
+    {
+      "coefficient": [
+        -1,
+        1
+      ],
+      "destination": 0,
+      "op": "add",
+      "source": 1
+    },
+    {
+      "coefficient": [
+        1,
+        1
+      ],
+      "destination": 1,
+      "op": "add",
+      "source": 0
+    },
+    {
+      "coefficient": [
+        -1,
+        1
+      ],
+      "destination": 0,
+      "op": "add",
+      "source": 1
+    },
+    {
+      "bank": 1,
+      "letter": "S0",
+      "op": "address",
+      "restores_shear_source": false
+    },
+    {
+      "bank": 1,
+      "letter": "S1",
+      "op": "address",
+      "restores_shear_source": false
+    },
+    {
+      "bank": 1,
+      "letter": "S2",
+      "op": "address",
+      "restores_shear_source": false
+    },
+    {
+      "bank": 1,
+      "letter": "U",
+      "op": "address",
+      "restores_shear_source": false
+    },
+    {
+      "bank": 1,
+      "letter": "S0",
+      "op": "address",
+      "restores_shear_source": false
+    },
+    {
+      "bank": 1,
+      "letter": "S1",
+      "op": "address",
+      "restores_shear_source": false
+    },
+    {
+      "bank": 1,
+      "letter": "S2",
+      "op": "address",
+      "restores_shear_source": false
+    },
+    {
+      "coefficient": [
+        1,
+        1
+      ],
+      "destination": 0,
+      "op": "add",
+      "source": 1
+    },
+    {
+      "bank": 1,
+      "letter": "-S2",
+      "op": "address",
+      "restores_shear_source": true
+    },
+    {
+      "bank": 1,
+      "letter": "-S1",
+      "op": "address",
+      "restores_shear_source": true
+    },
+    {
+      "bank": 1,
+      "letter": "-S0",
+      "op": "address",
+      "restores_shear_source": true
+    },
+    {
+      "bank": 1,
+      "letter": "U",
+      "op": "address",
+      "restores_shear_source": true
+    },
+    {
+      "bank": 1,
+      "letter": "-S2",
+      "op": "address",
+      "restores_shear_source": true
+    },
+    {
+      "bank": 1,
+      "letter": "-S1",
+      "op": "address",
+      "restores_shear_source": true
+    },
+    {
+      "bank": 1,
+      "letter": "-S0",
+      "op": "address",
+      "restores_shear_source": true
+    },
+    {
+      "bank": 1,
+      "letter": "S0",
+      "op": "address",
+      "restores_shear_source": false
+    },
+    {
+      "bank": 1,
+      "letter": "S1",
+      "op": "address",
+      "restores_shear_source": false
+    },
+    {
+      "bank": 1,
+      "letter": "S2",
+      "op": "address",
+      "restores_shear_source": false
+    },
+    {
+      "bank": 1,
+      "letter": "V",
+      "op": "address",
+      "restores_shear_source": false
+    },
+    {
+      "bank": 1,
+      "letter": "S0",
+      "op": "address",
+      "restores_shear_source": false
+    },
+    {
+      "bank": 1,
+      "letter": "S1",
+      "op": "address",
+      "restores_shear_source": false
+    },
+    {
+      "bank": 1,
+      "letter": "S2",
+      "op": "address",
+      "restores_shear_source": false
+    },
+    {
+      "coefficient": [
+        2,
+        1
+      ],
+      "destination": 0,
+      "op": "add",
+      "source": 1
+    },
+    {
+      "bank": 1,
+      "letter": "-S2",
+      "op": "address",
+      "restores_shear_source": true
+    },
+    {
+      "bank": 1,
+      "letter": "-S1",
+      "op": "address",
+      "restores_shear_source": true
+    },
+    {
+      "bank": 1,
+      "letter": "-S0",
+      "op": "address",
+      "restores_shear_source": true
+    },
+    {
+      "bank": 1,
+      "letter": "V",
+      "op": "address",
+      "restores_shear_source": true
+    },
+    {
+      "bank": 1,
+      "letter": "-S2",
+      "op": "address",
+      "restores_shear_source": true
+    },
+    {
+      "bank": 1,
+      "letter": "-S1",
+      "op": "address",
+      "restores_shear_source": true
+    },
+    {
+      "bank": 1,
+      "letter": "-S0",
+      "op": "address",
+      "restores_shear_source": true
+    },
+    {
+      "bank": 0,
+      "letter": "-S0",
+      "op": "address",
+      "restores_shear_source": false
+    },
+    {
+      "bank": 0,
+      "letter": "-S1",
+      "op": "address",
+      "restores_shear_source": false
+    },
+    {
+      "bank": 0,
+      "letter": "-S2",
+      "op": "address",
+      "restores_shear_source": false
+    },
+    {
+      "bank": 0,
+      "letter": "U",
+      "op": "address",
+      "restores_shear_source": false
+    },
+    {
+      "bank": 0,
+      "letter": "-S0",
+      "op": "address",
+      "restores_shear_source": false
+    },
+    {
+      "bank": 0,
+      "letter": "-S1",
+      "op": "address",
+      "restores_shear_source": false
+    },
+    {
+      "bank": 0,
+      "letter": "-S2",
+      "op": "address",
+      "restores_shear_source": false
+    },
+    {
+      "coefficient": [
+        1,
+        15
+      ],
+      "destination": 1,
+      "op": "add",
+      "source": 0
+    },
+    {
+      "bank": 0,
+      "letter": "S2",
+      "op": "address",
+      "restores_shear_source": true
+    },
+    {
+      "bank": 0,
+      "letter": "S1",
+      "op": "address",
+      "restores_shear_source": true
+    },
+    {
+      "bank": 0,
+      "letter": "S0",
+      "op": "address",
+      "restores_shear_source": true
+    },
+    {
+      "bank": 0,
+      "letter": "U",
+      "op": "address",
+      "restores_shear_source": true
+    },
+    {
+      "bank": 0,
+      "letter": "S2",
+      "op": "address",
+      "restores_shear_source": true
+    },
+    {
+      "bank": 0,
+      "letter": "S1",
+      "op": "address",
+      "restores_shear_source": true
+    },
+    {
+      "bank": 0,
+      "letter": "S0",
+      "op": "address",
+      "restores_shear_source": true
+    },
+    {
+      "bank": 0,
+      "letter": "-S0",
+      "op": "address",
+      "restores_shear_source": false
+    },
+    {
+      "bank": 0,
+      "letter": "-S1",
+      "op": "address",
+      "restores_shear_source": false
+    },
+    {
+      "bank": 0,
+      "letter": "-S2",
+      "op": "address",
+      "restores_shear_source": false
+    },
+    {
+      "bank": 0,
+      "letter": "U",
+      "op": "address",
+      "restores_shear_source": false
+    },
+    {
+      "bank": 0,
+      "letter": "V",
+      "op": "address",
+      "restores_shear_source": false
+    },
+    {
+      "bank": 0,
+      "letter": "U",
+      "op": "address",
+      "restores_shear_source": false
+    },
+    {
+      "bank": 0,
+      "letter": "-S0",
+      "op": "address",
+      "restores_shear_source": false
+    },
+    {
+      "bank": 0,
+      "letter": "-S1",
+      "op": "address",
+      "restores_shear_source": false
+    },
+    {
+      "bank": 0,
+      "letter": "-S2",
+      "op": "address",
+      "restores_shear_source": false
+    },
+    {
+      "coefficient": [
+        -2,
+        15
+      ],
+      "destination": 1,
+      "op": "add",
+      "source": 0
+    },
+    {
+      "bank": 0,
+      "letter": "S2",
+      "op": "address",
+      "restores_shear_source": true
+    },
+    {
+      "bank": 0,
+      "letter": "S1",
+      "op": "address",
+      "restores_shear_source": true
+    },
+    {
+      "bank": 0,
+      "letter": "S0",
+      "op": "address",
+      "restores_shear_source": true
+    },
+    {
+      "bank": 0,
+      "letter": "U",
+      "op": "address",
+      "restores_shear_source": true
+    },
+    {
+      "bank": 0,
+      "letter": "V",
+      "op": "address",
+      "restores_shear_source": true
+    },
+    {
+      "bank": 0,
+      "letter": "U",
+      "op": "address",
+      "restores_shear_source": true
+    },
+    {
+      "bank": 0,
+      "letter": "S2",
+      "op": "address",
+      "restores_shear_source": true
+    },
+    {
+      "bank": 0,
+      "letter": "S1",
+      "op": "address",
+      "restores_shear_source": true
+    },
+    {
+      "bank": 0,
+      "letter": "S0",
+      "op": "address",
+      "restores_shear_source": true
+    },
+    {
+      "bank": 0,
+      "letter": "-S0",
+      "op": "address",
+      "restores_shear_source": false
+    },
+    {
+      "bank": 0,
+      "letter": "-S1",
+      "op": "address",
+      "restores_shear_source": false
+    },
+    {
+      "bank": 0,
+      "letter": "-S2",
+      "op": "address",
+      "restores_shear_source": false
+    },
+    {
+      "bank": 0,
+      "letter": "U",
+      "op": "address",
+      "restores_shear_source": false
+    },
+    {
+      "bank": 0,
+      "letter": "V",
+      "op": "address",
+      "restores_shear_source": false
+    },
+    {
+      "bank": 0,
+      "letter": "U",
+      "op": "address",
+      "restores_shear_source": false
+    },
+    {
+      "bank": 0,
+      "letter": "V",
+      "op": "address",
+      "restores_shear_source": false
+    },
+    {
+      "bank": 0,
+      "letter": "U",
+      "op": "address",
+      "restores_shear_source": false
+    },
+    {
+      "bank": 0,
+      "letter": "-S0",
+      "op": "address",
+      "restores_shear_source": false
+    },
+    {
+      "bank": 0,
+      "letter": "-S1",
+      "op": "address",
+      "restores_shear_source": false
+    },
+    {
+      "bank": 0,
+      "letter": "-S2",
+      "op": "address",
+      "restores_shear_source": false
+    },
+    {
+      "coefficient": [
+        4,
+        15
+      ],
+      "destination": 1,
+      "op": "add",
+      "source": 0
+    },
+    {
+      "bank": 0,
+      "letter": "S2",
+      "op": "address",
+      "restores_shear_source": true
+    },
+    {
+      "bank": 0,
+      "letter": "S1",
+      "op": "address",
+      "restores_shear_source": true
+    },
+    {
+      "bank": 0,
+      "letter": "S0",
+      "op": "address",
+      "restores_shear_source": true
+    },
+    {
+      "bank": 0,
+      "letter": "U",
+      "op": "address",
+      "restores_shear_source": true
+    },
+    {
+      "bank": 0,
+      "letter": "V",
+      "op": "address",
+      "restores_shear_source": true
+    },
+    {
+      "bank": 0,
+      "letter": "U",
+      "op": "address",
+      "restores_shear_source": true
+    },
+    {
+      "bank": 0,
+      "letter": "V",
+      "op": "address",
+      "restores_shear_source": true
+    },
+    {
+      "bank": 0,
+      "letter": "U",
+      "op": "address",
+      "restores_shear_source": true
+    },
+    {
+      "bank": 0,
+      "letter": "S2",
+      "op": "address",
+      "restores_shear_source": true
+    },
+    {
+      "bank": 0,
+      "letter": "S1",
+      "op": "address",
+      "restores_shear_source": true
+    },
+    {
+      "bank": 0,
+      "letter": "S0",
+      "op": "address",
+      "restores_shear_source": true
+    },
+    {
+      "bank": 0,
+      "letter": "-S0",
+      "op": "address",
+      "restores_shear_source": false
+    },
+    {
+      "bank": 0,
+      "letter": "-S1",
+      "op": "address",
+      "restores_shear_source": false
+    },
+    {
+      "bank": 0,
+      "letter": "-S2",
+      "op": "address",
+      "restores_shear_source": false
+    },
+    {
+      "bank": 0,
+      "letter": "U",
+      "op": "address",
+      "restores_shear_source": false
+    },
+    {
+      "bank": 0,
+      "letter": "V",
+      "op": "address",
+      "restores_shear_source": false
+    },
+    {
+      "bank": 0,
+      "letter": "U",
+      "op": "address",
+      "restores_shear_source": false
+    },
+    {
+      "bank": 0,
+      "letter": "V",
+      "op": "address",
+      "restores_shear_source": false
+    },
+    {
+      "bank": 0,
+      "letter": "U",
+      "op": "address",
+      "restores_shear_source": false
+    },
+    {
+      "bank": 0,
+      "letter": "V",
+      "op": "address",
+      "restores_shear_source": false
+    },
+    {
+      "bank": 0,
+      "letter": "U",
+      "op": "address",
+      "restores_shear_source": false
+    },
+    {
+      "bank": 0,
+      "letter": "-S0",
+      "op": "address",
+      "restores_shear_source": false
+    },
+    {
+      "bank": 0,
+      "letter": "-S1",
+      "op": "address",
+      "restores_shear_source": false
+    },
+    {
+      "bank": 0,
+      "letter": "-S2",
+      "op": "address",
+      "restores_shear_source": false
+    },
+    {
+      "coefficient": [
+        -8,
+        15
+      ],
+      "destination": 1,
+      "op": "add",
+      "source": 0
+    },
+    {
+      "bank": 0,
+      "letter": "S2",
+      "op": "address",
+      "restores_shear_source": true
+    },
+    {
+      "bank": 0,
+      "letter": "S1",
+      "op": "address",
+      "restores_shear_source": true
+    },
+    {
+      "bank": 0,
+      "letter": "S0",
+      "op": "address",
+      "restores_shear_source": true
+    },
+    {
+      "bank": 0,
+      "letter": "U",
+      "op": "address",
+      "restores_shear_source": true
+    },
+    {
+      "bank": 0,
+      "letter": "V",
+      "op": "address",
+      "restores_shear_source": true
+    },
+    {
+      "bank": 0,
+      "letter": "U",
+      "op": "address",
+      "restores_shear_source": true
+    },
+    {
+      "bank": 0,
+      "letter": "V",
+      "op": "address",
+      "restores_shear_source": true
+    },
+    {
+      "bank": 0,
+      "letter": "U",
+      "op": "address",
+      "restores_shear_source": true
+    },
+    {
+      "bank": 0,
+      "letter": "V",
+      "op": "address",
+      "restores_shear_source": true
+    },
+    {
+      "bank": 0,
+      "letter": "U",
+      "op": "address",
+      "restores_shear_source": true
+    },
+    {
+      "bank": 0,
+      "letter": "S2",
+      "op": "address",
+      "restores_shear_source": true
+    },
+    {
+      "bank": 0,
+      "letter": "S1",
+      "op": "address",
+      "restores_shear_source": true
+    },
+    {
+      "bank": 0,
+      "letter": "S0",
+      "op": "address",
+      "restores_shear_source": true
+    },
+    {
+      "bank": 1,
+      "letter": "S0",
+      "op": "address",
+      "restores_shear_source": false
+    },
+    {
+      "bank": 1,
+      "letter": "S1",
+      "op": "address",
+      "restores_shear_source": false
+    },
+    {
+      "bank": 1,
+      "letter": "S2",
+      "op": "address",
+      "restores_shear_source": false
+    },
+    {
+      "bank": 1,
+      "letter": "U",
+      "op": "address",
+      "restores_shear_source": false
+    },
+    {
+      "bank": 1,
+      "letter": "S0",
+      "op": "address",
+      "restores_shear_source": false
+    },
+    {
+      "bank": 1,
+      "letter": "S1",
+      "op": "address",
+      "restores_shear_source": false
+    },
+    {
+      "bank": 1,
+      "letter": "S2",
+      "op": "address",
+      "restores_shear_source": false
+    },
+    {
+      "coefficient": [
+        1,
+        1
+      ],
+      "destination": 0,
+      "op": "add",
+      "source": 1
+    },
+    {
+      "bank": 1,
+      "letter": "-S2",
+      "op": "address",
+      "restores_shear_source": true
+    },
+    {
+      "bank": 1,
+      "letter": "-S1",
+      "op": "address",
+      "restores_shear_source": true
+    },
+    {
+      "bank": 1,
+      "letter": "-S0",
+      "op": "address",
+      "restores_shear_source": true
+    },
+    {
+      "bank": 1,
+      "letter": "U",
+      "op": "address",
+      "restores_shear_source": true
+    },
+    {
+      "bank": 1,
+      "letter": "-S2",
+      "op": "address",
+      "restores_shear_source": true
+    },
+    {
+      "bank": 1,
+      "letter": "-S1",
+      "op": "address",
+      "restores_shear_source": true
+    },
+    {
+      "bank": 1,
+      "letter": "-S0",
+      "op": "address",
+      "restores_shear_source": true
+    },
+    {
+      "bank": 1,
+      "letter": "S0",
+      "op": "address",
+      "restores_shear_source": false
+    },
+    {
+      "bank": 1,
+      "letter": "S1",
+      "op": "address",
+      "restores_shear_source": false
+    },
+    {
+      "bank": 1,
+      "letter": "S2",
+      "op": "address",
+      "restores_shear_source": false
+    },
+    {
+      "bank": 1,
+      "letter": "V",
+      "op": "address",
+      "restores_shear_source": false
+    },
+    {
+      "bank": 1,
+      "letter": "S0",
+      "op": "address",
+      "restores_shear_source": false
+    },
+    {
+      "bank": 1,
+      "letter": "S1",
+      "op": "address",
+      "restores_shear_source": false
+    },
+    {
+      "bank": 1,
+      "letter": "S2",
+      "op": "address",
+      "restores_shear_source": false
+    },
+    {
+      "coefficient": [
+        2,
+        1
+      ],
+      "destination": 0,
+      "op": "add",
+      "source": 1
+    },
+    {
+      "bank": 1,
+      "letter": "-S2",
+      "op": "address",
+      "restores_shear_source": true
+    },
+    {
+      "bank": 1,
+      "letter": "-S1",
+      "op": "address",
+      "restores_shear_source": true
+    },
+    {
+      "bank": 1,
+      "letter": "-S0",
+      "op": "address",
+      "restores_shear_source": true
+    },
+    {
+      "bank": 1,
+      "letter": "V",
+      "op": "address",
+      "restores_shear_source": true
+    },
+    {
+      "bank": 1,
+      "letter": "-S2",
+      "op": "address",
+      "restores_shear_source": true
+    },
+    {
+      "bank": 1,
+      "letter": "-S1",
+      "op": "address",
+      "restores_shear_source": true
+    },
+    {
+      "bank": 1,
+      "letter": "-S0",
+      "op": "address",
+      "restores_shear_source": true
+    },
+    {
+      "bank": 0,
+      "op": "paid_C"
+    },
+    {
+      "bank": 1,
+      "op": "paid_C"
+    },
+    {
+      "bank": 1,
+      "letter": "X",
+      "op": "address",
+      "restores_shear_source": false
+    }
+  ]
+}
diff --git a/research/two-image-volume-independent-audit/vendor/pr4998/PROOF.md b/research/two-image-volume-independent-audit/vendor/pr4998/PROOF.md
new file mode 100644
index 0000000000..c2d4d743f3
--- /dev/null
+++ b/research/two-image-volume-independent-audit/vendor/pr4998/PROOF.md
@@ -0,0 +1,177 @@
+# A four-call compensated two-image interface
+
+Prepared by Cinna Davis with substantial OpenAI Codex assistance. Apache-2.0.
+Written all-width algebra with exact finite corroboration, not a proof-assistant
+certificate, new κ or complete Gaussian supplier.
+
+## 1. Inputs and intended output
+
+Retain the actual base letters of lee-phys's PR4688 and Yiyang's PR4710:
+U is CNOT(0→2), V swaps bits 0 and 1, `S e_x=i^popcount(x)e_x`,
+`P=SUS`, `Q=SVS`, and
+
+`C=((1+i)/2)I+((1-i)/2)X_0`.
+
+Each base letter g is tensorized individually: `g_f=g^(tensor f)`. For
+either `(A,B)=(U,V)` or `(P,Q)`, let
+
+`L_f=A_f+2B_f`, `F_f=C_f L_f C_f`.
+
+On two arbitrary independent inputs x,y we construct exactly
+
+`(x,y) -> (F_f x,F_f^-1 y)`                               (1)
+
+for every positive f. There is no assumed relation between x and y and
+no initially zero logical array. The second output is a specified transformed
+partner. It is not y restored. The goal is a local completed linear interface,
+not two independent canonical Gaussian jobs.
+
+## 2. A finite free inverse, uniform in tensor width
+
+For either pair R=A^-1 B has order four. For the original letters,
+`R=U^-1V=UV`; for the repaired letters it is `S^-1(UV)S` with absolute
+phases. Hence R_f also has order four. The exact polynomial identity
+
+`(I+2R_f)(I-2R_f+4R_f²-8R_f³)=-15I`
+
+holds at every width. Therefore
+
+`L_f^-1 = sum_(k=0)^3 c_k R_f^k A_f^-1`,
+`(c_0,c_1,c_2,c_3)=(-1,2,-4,8)/15`.                     (2)
+
+This formula and the source-prefix invertibility are predecessor results;
+they are not claimed as new. All its terms are individually tensorized free
+monomial words with fixed rational coefficients. The sum is formed by register
+mixing after tensorization. This is not the tensor power of the width-one sum.
+
+For a fixed sum of free words `D=sum_j d_j M_j`, implement the dirty-source
+shear `E12(D):(x,y)->(x+D y,y)` one term at a time:
+
+1. Apply M_j to the source y.
+2. Add d_j times that source into x.
+3. Apply M_j^-1 to restore the source y.
+
+No clean copy is used. Every term sees the same original source y, since it
+is restored before the next term. Arbitrary x and y are permitted. Negative
+coefficients invert the shear. The same procedure implements E21(D).
+
+## 3. Completed compensated product
+
+For an invertible operator D, define
+
+`W(D)=E12(D) E21(-D^-1) E12(D)
+     = [[0,D],[-D^-1,0]]`.
+
+Products act on column vectors from right to left. Since
+
+`W(-I)=[[0,-I],[I,0]]`,
+
+we obtain the exact noncommutative block identity
+
+`W(D)W(-I)=diag(D,D^-1)`.                                (3)
+
+The three shears within each W have palindromic order, so the literal
+execution of (3) is: E12(-I), E21(I), E12(-I), E12(D), E21(-D^-1), E12(D).
+Use D=L_f and the source-restoring implementations above. Sandwich this
+product between two copies of `diag(C_f,C_f^-1)`. The result is
+
+`diag(C_f,C_f^-1) diag(L_f,L_f^-1) diag(C_f,C_f^-1)
+ = diag(F_f,F_f^-1)`,
+
+proving (1) at every width. No commuting of C with L or its inverse is used.
+Both inputs and both outputs remain explicit throughout the construction.
+
+The elementary kernel satisfies `C²=X_0`, `C⁴=I` and `C^-1=X_0 C`. Thus
+each boundary C_f^-1 requires one forward paid C_f and one free X_0,f.
+There are two paid forward kernels per boundary, four in total.
+
+The inverse of the completed map uses the same program with the two banks
+swapped before and after: `J diag(F,F^-1) J=diag(F^-1,F)`. This implements
+the actual algebraic inverse with the same four ideal paid calls and two
+additional free bank swaps. It does not make a claim about the inverse of
+an approximate child realization.
+
+## 4. Complete ideal-game instruction bill
+
+PROGRAM.json is an explicit straight-line program using only `paid_C`,
+individual address letters and ordinary scalar ADDs. The allowed address
+letters are U,V,X_0 and the three one-coordinate phases S_j and their
+inverses; combined S is not counted as one primitive. Terms of L and L^-1
+are expanded fully into those letters. Each phase/permutation applied to a
+shear source has a recorded inverse restore. No initialization, COPY or
+CLEAR instruction occurs.
+
+| Variant | Paid rank-one C calls | Scalar ADDs | Primitive address applications | Extra bank swaps for inverse |
+|---|---:|---:|---:|---:|
+| Original U,V | 4 | 11 | 42 | 2 |
+| Phase-repaired P,Q | 4 | 11 | 138 | 2 |
+
+The ADD count is three for W(-I), two for each of the two L shears, and
+four for the inverse-L shear. Coefficients include the rational denominator
+15 of (2); they are not all dyadic. The instruction count and coefficients
+are independent of f. In the abstract source engine, fixed rational register
+mixing is permitted, but actual exact-grid or rounded native execution needs
+its own precision and storage bill.
+
+For the original variant the inverse-L monomial `R^k U^-1` is executed as
+U followed by k copies of (V,U). Its length is 1+2k. The four terms and
+their restores cost `2*(1+3+5+7)=32` address applications. The two L
+shears cost eight more. The two boundary inverse kernels add two X_0,
+giving 42. For the repaired variant the same monomial simplifies to
+`S^-1 (UV)^k U S^-1`, of length 7+2k, so those terms/restores cost 80.
+The two L shears cost 56, and the boundary shifts add two, giving 138.
+
+This is the complete bill in the stated ideal linear game. It is not an
+admitted recursion, binary caller, tape implementation or outer moment.
+No paid-call saving over separately providing these two nonunitary maps is
+claimed. Counting either as a Gaussian helper job would require a new
+consumer argument.
+
+## 5. Conditioning and the determinant boundary
+
+The order-four R_f is unitary. Its four eigenvalues all occur for every
+positive width, so I+2R_f has singular values 3,1,sqrt(5). Multiplication
+by the unitary A_f and C_f does not change singular values. Consequently
+both L_f and F_f have largest singular value 3 and smallest 1.
+For the complete pair (1), the operator norm and inverse norm are both 3;
+its Euclidean condition number is exactly 9, independently of f.
+
+There is also a conservative uniform intermediate norm bound 32 relative
+to the full two-bank input norm. W(-I)'s scalar steps have prefix norm at
+most four and its completed map is a unitary signed swap. Each partially
+completed L shear has norm at most `1+sum|coefficients|<=4`. Each partial
+inverse-L shear has norm at most two because its coefficient magnitudes
+sum to one. The three large shears therefore have prefix norms bounded by
+4,8,32. Address letters and the boundary kernels are unitary. This bound
+counts all intermediate term additions, not just completed large shears.
+It is an exact ideal norm statement, not a recursive rounding theorem.
+
+PR4991's completed dirty-return obstruction concerns `diag(F,I,...)`.
+Here `det F * det F^-1=1`. The transformed partner explicitly supplies the
+opposite volume profile, so that obstruction is respected. A local inverse
+partner is therefore constructible; whether it is a useful independently
+priced target in an actual Gaussian consumer remains unanswered. Since F
+has unequal singular values, it is not a scalar multiple of a unitary
+Gaussian, even after unitary input/output frame changes.
+
+## 6. Independent intended-map checks
+
+The verifier emits PROGRAM.json and runs a separate primitive interpreter.
+Its target oracle builds dense C_f and monomial branch matrices directly
+from coordinate entries, multiplies `C_f L_f C_f`, then obtains F_f^-1
+by Gaussian elimination. That oracle does not use the polynomial inverse,
+the shear decomposition, or the generated source-restoration schedule.
+
+For both variants, all sixteen independent input columns at width one are
+checked over Q(i). All 128 independent input columns at width two are
+checked over F17 with i=4. Each column is checked against the actual target
+and both inverse multiplication orders, giving 288 distinct input columns.
+The modular computation is finite corroboration, not a claim that modular
+equality proves rational equality at width two. A width-three dirty fixture
+also round-trips. The written operator identities prove all widths.
+
+Controls reject an inverse-polynomial sign change, omission of a literal
+source-restoring U, relabelling the transformed partner as restored input,
+and omission of the fourth paid call from the invoice. Checks remain active
+under Python optimization. No finite checks are interpreted as a new κ,
+Gaussian supplier admission or a completed five-in-fourteen construction.
diff --git a/research/two-image-volume-independent-audit/verify.py b/research/two-image-volume-independent-audit/verify.py
new file mode 100644
index 0000000000..fa26341559
--- /dev/null
+++ b/research/two-image-volume-independent-audit/verify.py
@@ -0,0 +1,290 @@
+#!/usr/bin/env python3
+"""Code-disjoint, bounded source/character/boundary checks; standard library only."""
+from __future__ import annotations
+
+import argparse
+import ast
+import hashlib
+import json
+from fractions import Fraction
+from pathlib import Path
+
+ROOT = Path(__file__).resolve().parent
+
+
+def require(value, message):
+    if not value:
+        raise ValueError(message)
+
+
+def compose(left, right):
+    return (tuple(left[0][right[0][x]] for x in range(len(right[0]))),
+            tuple((right[1][x] + left[1][right[0][x]]) % 4
+                  for x in range(len(right[0]))))
+
+
+def inverse(word):
+    p = tuple(word[0].index(x) for x in range(len(word[0])))
+    return p, tuple(-word[1][p[x]] % 4 for x in range(len(p)))
+
+
+def power(word, exponent):
+    result = tuple(range(len(word[0]))), (0,) * len(word[0])
+    for _ in range(exponent):
+        result = compose(word, result)
+    return result
+
+
+def tensor(left, right):
+    n = len(right[0])
+    return (tuple(a * n + b for a in left[0] for b in right[0]),
+            tuple((a + b) % 4 for a in left[1] for b in right[1]))
+
+
+def trace(word):
+    counts = [0] * 4
+    for x, y in enumerate(word[0]):
+        if x == y:
+            counts[word[1][x]] += 1
+    return counts[0] - counts[2], counts[1] - counts[3]
+
+
+def source_definitions():
+    pins = json.loads((ROOT / 'RETAINED-SOURCES.json').read_text())
+    for row in pins['files']:
+        data = (ROOT / row['retained_path']).read_bytes()
+        require(hashlib.sha256(data).hexdigest() == row['sha256'], 'retained source changed')
+        require(hashlib.sha1(b'blob ' + str(len(data)).encode() + b'\0' + data).hexdigest()
+                == row['git_blob'], 'retained Git blob mismatch')
+    # Evaluate only literal defining expressions, never import a predecessor module.
+    old = ast.parse((ROOT / 'vendor/pr4688/verify.py').read_text())
+    env = {'__builtins__': {}, 'tuple': tuple, 'range': range}
+    definitions = {}
+    for node in old.body:
+        if isinstance(node, ast.Assign) and isinstance(node.targets[0], ast.Name):
+            name = node.targets[0].id
+            if name in ('U_PERM', 'V_PERM'):
+                definitions[name] = eval(compile(ast.Expression(node.value), '<source-definition>', 'eval'), env)
+    expected_u, expected_v = [], []
+    for x in range(8):
+        a, b, c = (x >> j & 1 for j in range(3))
+        expected_u.append(a + 2 * b + 4 * (c ^ a))
+        expected_v.append(b + 2 * a + 4 * c)
+    require(definitions == {'U_PERM': tuple(expected_u), 'V_PERM': tuple(expected_v)},
+            'source address definition differs from independent coordinate action')
+    u, v = (tuple(expected_u), (0,) * 8), (tuple(expected_v), (0,) * 8)
+    identity = tuple(range(8)), (0,) * 8
+    env.update(identity=identity, u=u, v=v, monomial_compose=compose)
+    repaired = ast.parse((ROOT / 'vendor/pr4710/verify.py').read_text())
+    fn = next(n for n in repaired.body if isinstance(n, ast.FunctionDef) and n.name == 'monomial_checks')
+    for node in fn.body:
+        if isinstance(node, ast.Assign) and isinstance(node.targets[0], ast.Name):
+            name = node.targets[0].id
+            if name in ('phase', 'P', 'Q'):
+                env[name] = eval(compile(ast.Expression(node.value), '<source-definition>', 'eval'), env)
+    s = identity[0], tuple(sum(x >> j & 1 for j in range(3)) % 4 for x in range(8))
+    require(env['phase'] == s, 'source phase is not exact i^popcount')
+    require(env['P'] == compose(s, compose(u, s)) and env['Q'] == compose(s, compose(v, s)),
+            'source branch phase binding')
+    return u, v, s, env['P'], env['Q']
+
+
+def det_integer(matrix):
+    a = [row[:] for row in matrix]
+    previous, sign = 1, 1
+    for k in range(len(a) - 1):
+        pivot_row = next((r for r in range(k, len(a)) if a[r][k]), None)
+        if pivot_row is None:
+            return 0
+        if pivot_row != k:
+            a[k], a[pivot_row] = a[pivot_row], a[k]
+            sign = -sign
+        pivot = a[k][k]
+        for i in range(k + 1, len(a)):
+            for j in range(k + 1, len(a)):
+                numerator = a[i][j] * pivot - a[i][k] * a[k][j]
+                require(numerator % previous == 0, 'Bareiss nonexact division')
+                a[i][j] = numerator // previous
+            a[i][k] = 0
+        previous = pivot
+    return sign * a[-1][-1]
+
+
+def counts(width):
+    d, a, b = 8 ** width, 4 ** width, 2 ** width
+    return [(d + a + 2 * b) // 4, (d - a) // 4,
+            (d + a - 2 * b) // 4, (d - a) // 4]
+
+
+def multiply(a, b, p=17):
+    out = [[0] * len(b[0]) for _ in a]
+    for i, row in enumerate(a):
+        for k, value in enumerate(row):
+            if value:
+                for j, other in enumerate(b[k]):
+                    out[i][j] = (out[i][j] + value * other) % p
+    return out
+
+
+def eye(n):
+    return [[int(i == j) for j in range(n)] for i in range(n)]
+
+
+def invert(a, p=17):
+    n = len(a)
+    rows = [a[i][:] + eye(n)[i] for i in range(n)]
+    for j in range(n):
+        k = next((k for k in range(j, n) if rows[k][j] % p), None)
+        require(k is not None, 'unexpected singular modular operator')
+        rows[j], rows[k] = rows[k], rows[j]
+        scale = pow(rows[j][j], -1, p)
+        rows[j] = [x * scale % p for x in rows[j]]
+        for k in range(n):
+            if k != j and rows[k][j]:
+                c = rows[k][j]
+                rows[k] = [(x - c * y) % p for x, y in zip(rows[k], rows[j])]
+    return [row[n:] for row in rows]
+
+
+def matrix(word):
+    out = [[0] * len(word[0]) for _ in word[0]]
+    for x, y in enumerate(word[0]):
+        out[y][x] = pow(4, word[1][x], 17)
+    return out
+
+
+def lift(word, width):
+    result = word
+    for _ in range(width - 1):
+        result = tensor(result, word)
+    return result
+
+
+def kernel(width):
+    n = 8 ** width
+    out = eye(n)
+    for digit in range(width):
+        updated = [[0] * n for _ in range(n)]
+        mask = 8 ** digit
+        for x in range(n):
+            updated[x] = [(11 * a + 7 * b) % 17 for a, b in zip(out[x], out[x ^ mask])]
+        out = updated
+    return out
+
+
+def boundary_check(u, v, s, P, Q, width):
+    program = json.loads((ROOT / 'vendor/pr4998/PROGRAM.json').read_text())
+    n = 8 ** width
+    c = kernel(width)
+    require(multiply(c, invert(c)) == eye(n), 'paid C invertibility')
+    x = tuple(z ^ 1 for z in range(8)), (0,) * 8
+    require(multiply(c, c) == matrix(lift(x, width)), 'actual normalized C squared is X')
+    result = {}
+    for variant, a, b in [('original', u, v), ('phase_repaired', P, Q)]:
+        am, bm = matrix(lift(a, width)), matrix(lift(b, width))
+        for image in (am, bm):
+            single = multiply(c, multiply(image, c))
+            require(multiply(single, invert(single)) == eye(n), 'allowed single-image boundary')
+        middle = [[(x + 2 * y) % 17 for x, y in zip(rx, ry)] for rx, ry in zip(am, bm)]
+        f = multiply(c, multiply(middle, c))
+        fi = invert(f)
+        state = [eye(2 * n)[:n], eye(2 * n)[n:]]
+        for op in program[variant]:
+            if op['op'] == 'paid_C':
+                bank = op['bank']
+                state[bank] = multiply(c, state[bank])
+            elif op['op'] == 'add':
+                numerator, denominator = op['coefficient']
+                coefficient = numerator * pow(denominator, -1, 17) % 17
+                dst, src = op['destination'], op['source']
+                state[dst] = [[(x + coefficient * y) % 17 for x, y in zip(rx, ry)]
+                              for rx, ry in zip(state[dst], state[src])]
+            else:
+                require(op['op'] == 'address', 'unknown program instruction')
+                name = op['letter']
+                if name in ('U', 'V', 'X'):
+                    word = {'U': u, 'V': v, 'X': (tuple(x ^ 1 for x in range(8)), (0,) * 8)}[name]
+                else:
+                    sign = -1 if name.startswith('-') else 1
+                    bit = int(name[-1])
+                    word = tuple(range(8)), tuple(sign * (x >> bit & 1) % 4 for x in range(8))
+                bank = op['bank']
+                state[bank] = multiply(matrix(lift(word, width)), state[bank])
+        expected = [row + [0] * n for row in f] + [[0] * n + row for row in fi]
+        require(state[0] + state[1] == expected, 'compensated program differs from independent map')
+        require(fi != eye(n), 'compensated partner must not be called returned dirt')
+        result[variant] = {'independent_columns': 2 * n, 'literal_instructions': len(program[variant]),
+                           'partner_is_identity': False, 'single_image_cases_invertible': True, 'arithmetic': 'F17 with i=4; finite boundary control only'}
+    return result
+
+
+def verify():
+    u, v, s, P, Q = source_definitions()
+    r = compose(inverse(u), v)
+    repaired = compose(inverse(P), Q)
+    require(repaired == compose(inverse(s), compose(r, s)), 'absolute-phase conjugacy')
+    require(power(r, 4) == power(r, 0) and power(r, 2) != power(r, 0), 'source relative order')
+    require([trace(power(r, k)) for k in range(4)] == [(8, 0), (2, 0), (4, 0), (2, 0)], 'base characters')
+    # A projectively equal Q with changed absolute phase changes the relative spectrum.
+    wrong_q = Q[0], tuple((x + 1) % 4 for x in Q[1])
+    require(trace(compose(inverse(P), wrong_q)) != trace(repaired), 'absolute-phase omission control')
+    records = []
+    base_counts = [4, 1, 2, 1]  # Eigenvalue order 1,i,-1,-i.
+    previous = [1, 0, 0, 0]
+    for width in (1, 2):
+        rt, rpt = lift(r, width), lift(repaired, width)
+        require(rpt == compose(inverse(lift(s, width)), compose(rt, lift(s, width))), 'tensor phase conjugacy')
+        traces = [trace(power(rt, k))[0] for k in range(4)]
+        require(traces == [8 ** width, 2 ** width, 4 ** width, 2 ** width], 'tensor character trace')
+        character_counts = [(traces[0] + traces[2] + 2 * traces[1]) // 4,
+                            (traces[0] - traces[2]) // 4,
+                            (traces[0] + traces[2] - 2 * traces[1]) // 4,
+                            (traces[0] - traces[2]) // 4]
+        convolution = [sum(previous[j] * base_counts[(k - j) % 4] for j in range(4)) for k in range(4)]
+        require(character_counts == counts(width) == convolution, 'character/convolution independence')
+        previous = convolution
+        d = 8 ** width
+        a = eye(d)
+        for x, y in enumerate(rt[0]):
+            a[y][x] += 2
+        absolute_det = abs(det_integer(a))
+        m = counts(width)
+        require(absolute_det == 3 ** m[0] * 5 ** m[1], 'direct exact determinant')
+        singular_ranks = [d - m[2], d - m[0], d - m[1], d - m[3]]
+        require(all(0 < rank < d for rank in singular_ranks), 'singular rank-drop hypotheses')
+        # A q-bank singular register mixing loses >=d rank; these targets lose <d.
+        for q in (1, 2, 4):
+            require(all((q - 1) * d + rank > (q - 1) * d for rank in singular_ranks), 'rank threshold')
+        records.append({'width': width, 'character_counts_1_i_minus1_minusi': m,
+                        'absolute_determinant': str(absolute_det), 'singular_target_ranks': singular_ranks,
+                        'compensated_boundary': boundary_check(u, v, s, P, Q, width)})
+    m3 = counts(3)
+    require((m3[0] + 64 * 4 - 16 * 22, m3[1] + 64 - 16 * 12) == (52, -16), 'symbolic curvature')
+    require(3 ** 52 != 5 ** 16, 'nonaffine curvature witness')
+    require(3 ** 64 * 5 ** 16 != 3 ** 22 * 5 ** 12, 'tensorizing a sum control')
+    # For t=iy, A=B automatically, but the second condition cannot hold when y!=0.
+    for y in (Fraction(1, 2), Fraction(-1, 2), Fraction(2), Fraction(-2)):
+        require(1 + y * y > abs(1 - y * y), 'pure-imaginary coefficient classification control')
+    require(det_integer([[2, 0], [0, 0]]) == 0, 'clean full-space map is singular')
+    require(multiply([[2, 0], [0, 0]], [[1], [0]]) == [[2], [0]], 'clean restriction remains injective')
+    return {'result': 'PASS', 'scope': 'Independent scoped written theorem audit; exact finite source checks, not full theorem formalization',
+            'singular_gap_completion': 'rank-drop argument for every fixed finite bank count',
+            'source_relative_traces': [8, 2, 4, 2], 'finite_checks': records,
+            'all_width_character_formula': ['(8^f+4^f+2*2^f)/4', '(8^f-4^f)/4', '(8^f+4^f-2*2^f)/4', '(8^f-4^f)/4'],
+            'normalized_profile': 'log|alpha|+(A+B+E)/4+(A+B-E)/(4*2^f)+(A-B)/(2*4^f)',
+            'curvature_witness': '3^52/5^16 != 1',
+            'controls': ['absolute phase of Q', 'tensorizing a sum', 'pure-imaginary nonzero ratio',
+                         'singular rank-drop hypotheses', 'allowed single-image cases', 'compensating output is transformed', 'clean subspace is outside full-space volume lemma']}
+
+
+if __name__ == '__main__':
+    parser = argparse.ArgumentParser(description=__doc__)
+    parser.add_argument('--out', type=Path)
+    parser.add_argument('--check', type=Path)
+    args = parser.parse_args()
+    result = verify()
+    if args.check:
+        require(json.loads(args.check.read_text()) == result, 'stored report differs')
+    if args.out:
+        args.out.write_text(json.dumps(result, indent=2, sort_keys=True) + '\n')
+    print('PASS_TWO_IMAGE_VOLUME_INDEPENDENT_AUDIT')