diff --git a/research/p104-quadratic-union-reduction/PROOF.md b/research/p104-quadratic-union-reduction/PROOF.md
new file mode 100644
index 0000000000..c53a84e867
--- /dev/null
+++ b/research/p104-quadratic-union-reduction/PROOF.md
@@ -0,0 +1,173 @@
+# A sharp two-plane union theorem for the E8 quadratic shell
+
+This scoped proof and its reduction were produced by Nick Petalas. Apache-2.0.
+Quadratic Gauss sums and finite quadratic-space theory are classical.
+
+Let V be an eight-dimensional vector space over F2. Let Q be a nondegenerate
+quadratic form of plus type, with polar form B. Thus
+
+    sum_(u in V) (-1)^Q(u) = 16.
+
+Write S = {u : Q(u)=1}; it has 120 elements. For a two-dimensional subspace
+A of V and a linear functional b on A, define the live set
+
+    L(A,b) = {u in S : B(u,a)=b(a) for every a in A}.
+
+The constraint plane is A; it need not be isotropic. Two constraint systems
+are consistent together exactly when their functionals agree on A intersect A'.
+Nondegeneracy of B makes every consistent combined system soluble in V.
+
+## Theorem
+
+For any two live sets, their union has at most **68** points. Equality holds
+exactly in the following configuration, up to exchanging the sets:
+
+- A is a nondegenerate plane, and Q restricted to A plus b is anisotropic;
+  consequently |L(A,b)|=36.
+- A' is an isotropic plane, and Q restricted to A' plus b' is a nonzero
+  linear functional; consequently |L(A',b')|=32.
+- A intersect A' is a line, and b,b' disagree on its nonzero vector.
+
+The two live sets are then disjoint. Every other union has at most **66**
+points. In particular, the maximum union of two 36-point sets is exactly 66.
+Here anisotropic means that all three nonzero plane vectors have value one.
+
+## 1. Fourier count
+
+For a subspace D of dimension r and a linear functional h on D, put
+
+    G(D,h) = sum_(a in D) (-1)^(Q(a)+h(a)).
+
+Quadratic completion gives
+
+    sum_(u in V) (-1)^(Q(u)+B(u,a)) = 16 (-1)^Q(a).
+
+Expand the indicator of the r affine linear equations using characters.
+The indicator of Q(u)=1 is (1-(-1)^Q(u))/2. Character orthogonality gives
+
+    N(D,h) = 2^(7-r) - 2^(3-r) G(D,h).                 (1)
+
+For a plane, G is 4 or 0 if its polar form is zero: the restricted quadratic
+refinement is linear. For a nondegenerate plane it is 2 or -2. Hence every
+live-set cardinality lies in {24,28,32,36}; 36 occurs precisely for the
+anisotropic plane refinement.
+
+We also use the elementary Gauss-sum rule in dimensions at most four.
+Let R be the radical of the polar form on D. If Q+h is nonzero on R,
+translation by a radical vector of value one cancels the sum, so G=0.
+Otherwise it descends to the nondegenerate quotient D/R; G is |R| times
+that quotient's Gauss sum. A nondegenerate quadratic space of dimension
+2s has Gauss sum plus or minus 2^s. Sum in a symplectic basis: each binary
+pair contributes 2 or -2. No pair census is used in this argument.
+
+## 2. Two 36-point sets have union at most 66
+
+Both constraint-plane refinements are anisotropic. On each nonzero vector
+of either plane, its functional is Q(a)+1. Thus the functionals agree on
+the intersection. Put D=A+A', r=dim D, and let h be their common extension.
+The intersection of the live sets is counted by (1).
+
+If r=2, the planes and functionals coincide; the union has size 36.
+Otherwise r is 3 or 4, and the polar form of D has rank at least two because
+it contains the nondegenerate plane A.
+
+If the polar rank is two, either Q+h is nonzero on its radical, giving
+G=0, or it vanishes there. In the latter case projection identifies A with
+the two-dimensional nondegenerate quotient. The induced refinement is
+anisotropic, so the quotient Gauss sum is -2 and G is negative. Formula (1)
+gives an intersection of size at least 2^(7-r), which is at least eight.
+
+The remaining possibility is r=4 and polar rank four. Here G is 4 or -4,
+so (1) gives an intersection of size 6 or 10. In all cases it has at least
+six points. The union is at most 36+36-6=66.
+
+## 3. The 68-point equality case is the only larger union
+
+If at most one live set has size 36, the other has size at most 32. Thus
+the union is at most 68. Equality requires sizes 36 and 32 and an empty
+intersection. Their constraint planes must respectively be nondegenerate
+and isotropic, by Section 1. They cannot be the same plane.
+
+Suppose their combined affine equations are consistent. Their span D has
+dimension three or four and polar rank at least two. For r=3, the radical
+rule gives |G| at most four, so (1) gives at least twelve intersection
+points. For r=4, polar rank is two or four, giving |G| at most eight and
+at least four intersection points. Consistency therefore precludes equality.
+
+The equations must instead be inconsistent. Two distinct planes can have
+inconsistent functionals only when their intersection is a line. Conversely,
+inconsistency on that line makes the live sets disjoint and attains 68.
+On its nonzero vector v, the anisotropic refinement has value one;
+inconsistency is equivalently (Q+b')(v)=0, the kernel of the nonzero linear
+refinement on A'. This proves the stated equality classification.
+
+Finally every union has even size. For inconsistent equations this follows
+from the individual cardinalities. For consistent equations r is at most
+four. Formula (1) is even for r at most three. For r=4 the polar rank is
+even and at most four, so G is divisible by four by the radical rule;
+N=8-G/2 is even. A union below 68 is therefore at most 66.
+
+## 4. Attainment
+
+Use a hyperbolic basis e1,f1,...,e4,f4, so Q(u)=sum x_i y_i and
+B(u,e_i)=y_i, B(u,f_i)=x_i.
+
+For 68, the first live set imposes x1=y1=1. It has 36 points, since the
+remaining six-dimensional plus form must be zero. The second imposes
+y1=0,y2=1. It has 32 points: x2 is determined by the other five free bits.
+They are disjoint. Their planes are span(e1,f1) and span(e1,e2), and their
+affine values disagree on e1, exactly as in Section 3.
+
+The plus sign matters. For the minus-type form Q'(u)=Q(u)+x1+y1,
+the plane systems y3=y4=0 and y3=1,y4=0 give disjoint live sets of
+sizes 40 and 32, hence union 72. The checker evaluates this counterdomain
+directly. It is outside the theorem's hypotheses.
+
+For the sharp two-36 bound, impose x1=y1=1 for one set and x2=y2=1 for the
+other. Each has 36 points. In their intersection, the last two hyperbolic
+pairs have Q=1, which has six solutions. The union has 66 points.
+
+## 5. Exact reduction of the outstanding P104 counting step
+
+Matarener's [PR6218](https://github.com/CrocSwap/integer-mult-bounds/pull/6218),
+head 159352d273bd7b9f92c55cee3a9ac9b955de9b86, Section 4 uses a finite
+P104 union bound of 66 in a proposed hand-proof route to compatible-plane
+disjointness. Its counting result is cited; neither that pair census nor
+its compatibility result is replayed here.
+
+In that source's E8/2E8 model, V is the even-weight subspace of F2^9,
+Q(u)=wt(u)/2 modulo two, and a root label is q=u+1. For a label constraint
+z, write epsilon=wt(z) modulo two and a=z+epsilon*1 in V. Then
+
+    q dot z = B(u,a)+epsilon.
+
+A label plane containing 1 has empty live set. Every other label plane
+projects injectively to a plane A in V and gives exactly the affine system
+above. The 104 ports are S minus sixteen specified root lines T.
+
+The theorem shows that proving the P104 union bound 66 requires checking
+only the exceptional 68-point configuration: it is equivalent to
+
+    |(L(A,b) union L(A',b')) intersect T| >= 2
+
+for every configuration in the theorem's equality class. All other pairs
+already have full-E8 union at most 66, before puncturing. This is a precise
+reduction, not a proof of the displayed puncture inequality. The latter
+depends on the two removed frames. The unrelated hyperplane and at-most-four
+pairwise non-orthogonal exception conditions in compatibility also remain.
+The 68-point fixture proves that the full-E8 relaxation alone cannot yield
+the required 66 bound. No compatible-plane or decoder-floor theorem is
+claimed as a new consequence here.
+
+## Finite corroboration domain
+
+The written proof is universal. Its finite checker separately enumerates all
+alternating polar matrices and all quadratic refinements on spaces D of
+dimension 2..4, with all unordered spanning pairs of planes. For consistent
+affine equations a common offset is absorbed into the quadratic refinement.
+For inconsistent equations the quadratic diagonal is absorbed into the two
+separate offsets; all sixteen pairs of linear offsets are tested. Thus the
+normalization removes no relative configuration. These small representative
+cases are not a count of literal pairs of planes in the eight-space.
+The second check directly evaluates every affine plane system in the full
+eight-space, without the Fourier formula, and compares its cardinality.
diff --git a/research/p104-quadratic-union-reduction/README.md b/research/p104-quadratic-union-reduction/README.md
new file mode 100644
index 0000000000..56bf4d5d1a
--- /dev/null
+++ b/research/p104-quadratic-union-reduction/README.md
@@ -0,0 +1,107 @@
+# A sharp quadratic-union reduction for the P104 plane question
+
+**Scoped written proof with finite exact corroboration.** Two affine
+codimension-two live sets in the full 120-line E8 quadratic model have union
+at most **68**. Equality has one exact shape: disjoint sets of sizes 36 and
+32, with a shared constraint line carrying inconsistent affine values.
+Every other pair has union at most 66; two 36-point sets attain 66.
+[PROOF.md](PROOF.md) gives a Gauss-sum proof and explicit attaining sets.
+
+This is a partial step toward Matarener's first open question in
+[PR6218](https://github.com/CrocSwap/integer-mult-bounds/pull/6218), at head
+`159352d273bd7b9f92c55cee3a9ac9b955de9b86`. The source reports a finite
+P104 union bound 66. The new theorem reduces its geometric proof to one
+configuration: show that every exceptional full-E8 68-point union contains
+at least two of the sixteen removed lines. The full-E8 fixture proves that
+puncture information is necessary for this route. That last assertion and
+compatible-plane disjointness remain open here. No predecessor census,
+word, bound or verifier was audited or replayed.
+
+An older P112 two-flat census already reports 68 in
+[PR3253](https://github.com/CrocSwap/integer-mult-bounds/pull/3253).
+The new contribution is the full-E8 proof, equality classification and
+P104 reduction. The numerical value 68 on P112 is not claimed again.
+[PR3269](https://github.com/CrocSwap/integer-mult-bounds/pull/3269) already
+uses signed Gauss sums for individual smaller affine supports; it supplies
+methodological context rather than this union theorem.
+
+## Exact evidence
+
+The new standard-library checker enumerates 288,072 consistent and 1,368
+inconsistent relative quadratic configurations on spans of dimension at
+most four. This is a finite corroboration of the proof, not the source's
+P104 pair census. It checks the equality shape, parity, and the two-36
+branch maxima 36, 52 and 66 at span dimensions two, three and four.
+
+A direct bitset enumeration independently checks the Fourier slice formula
+on every one of the 43,180 affine plane systems in the full quadratic model.
+Their cardinalities 24, 28, 32 and 36 occur respectively 5,355, 16,320,
+16,065 and 5,440 times. Literal eight-bit attaining sets have sizes
+(36,32), disjoint union 68, and (36,36), intersection 6, union 66.
+Seven mathematical/domain rejection controls remain active with optimization.
+An opposite-sign quadratic form has an explicit 72-point union, so the
+plus-type hypothesis cannot be dropped.
+The emitted JSON receipt binds all package-file hashes and the interpreter.
+No receipt is handwritten or stored in the checkout.
+
+## Reproduce
+
+From the repository root, using CPython 3.12 and the standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -Werror -B research/p104-quadratic-union-reduction/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -Werror -B research/p104-quadratic-union-reduction/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/p104-quadratic-union-reduction
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/p104-quadratic-union-reduction --check-source-history
+```
+
+Replace the interpreter prefix on another host. The expected status is
+`PASS_P104_QUADRATIC_UNION_REDUCTION`. Each registered command is bounded
+at 60 seconds; the first local direct replay took less than one second.
+The exact published timings belong in the PR's evidence. Direct replay also
+works in a Git-free export with the two declared inputs at their relative
+paths. Source pins and historical card/selected-record provenance are in
+[SOURCES.json](SOURCES.json); [TASK.json](TASK.json) records the scope change.
+
+## Limits and code bounds
+
+The result does not prove the source's puncture inequality, compatibility
+lemma or decoder floor. It does not supply a word, restoration/ownership
+contract, native implementation, complete signed invoice, supplier admission,
+new kappa or complete multiplication theorem. The five selected assumptions
+remain. No predecessor scientific replay, Lean, Docker or full selected replay
+is needed or claimed. Independent human and formal proof-kernel review are
+unclaimed.
+
+The checker has no recursion, network or subprocess. Its loops are bounded
+by dimensions 2..4 for relative forms, at most 64 polar forms, 16 refinements,
+35 planes per four-space, and fixed 256/512-point ambient fixtures. The
+largest list has 10,795 planes. Each function is below 60 physical lines.
+Power-of-Ten rule 3 deviation: CPython allocates integers and collections
+during execution. Fixed, non-configurable domains bound live data and the
+process releases it on exit. A variable-dimension CLI would require explicit
+capacity limits. Warning-strict execution and source compilation are the
+available diagnostics; no shared configuration is changed.
+
+## Open next questions
+
+1. Prove the puncture inequality for the single 68-point equality class.
+   This would replace the source's finite 66-union bound by a hand argument.
+   Start from its symplectic/isotropic shared-line normal form and the two
+   removed orthogonal frames. Their relative position is the missing input.
+2. After that counting step, prove compatible-plane disjointness with the
+   source's hyperplane and at-most-four non-orthogonal exceptions. The
+   present theorem does not track which uncovered ports are orthogonal.
+   Start with the root-normal case singled out by PR6218.
+
+## Credit
+
+This contribution was produced by Nick Petalas. Credit Matarener for PR6218's
+open proof question, B-form reduction, P104 compatibility setting and the
+E8/2E8 description, and the retained carrier-code E8 model. DreamingOfClouds
+retains the decoder census and P104 word/geometry credit; Ali Romman and the
+retained P104/native/caller/compiler contributors retain their work. Credit
+Nick Petalas's older PR3253 P112 census and PR3269 signed-support argument
+at their stated scopes. Quadratic Fourier inversion, Gauss sums, radicals,
+hyperbolic bases and finite quadratic-space classification are classical.
+Global literature priority is unclaimed. Apache-2.0.
diff --git a/research/p104-quadratic-union-reduction/SOURCES.json b/research/p104-quadratic-union-reduction/SOURCES.json
new file mode 100644
index 0000000000..6bd2e31cb2
--- /dev/null
+++ b/research/p104-quadratic-union-reduction/SOURCES.json
@@ -0,0 +1,42 @@
+{
+  "schema_version": 1,
+  "base_commit": "a5bff3bf133e482541c09eba4e773884bdb2b1b7",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a",
+      "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    },
+    {
+      "path": "research/p104-carrier-code-uniqueness/e8/E8-PROOF.md",
+      "usage": "input",
+      "git_blob": "91ef08f375a93d48a852fb0d595cfe5b4cea5cd2",
+      "sha256": "a2ce265ea2eafc03ad1ffcfd68bc0059bbeba6370776b12a8a121c78c0840697"
+    },
+    {
+      "path": "research/p104-carrier-code-uniqueness/e8/ports.json",
+      "usage": "input",
+      "git_blob": "b964c3ae2ea54d3763d74639d691ea9f5b02920e",
+      "sha256": "ba6a0b9cf76b7cccc1ce8b3d1aa78a4aa329b34d45aded694648f0cf43fc9fce"
+    },
+    {
+      "path": "research/p112-common-five-deletion/PROOF.md",
+      "usage": "provenance",
+      "git_blob": "f1a7bc31c55cc37ec55f271275cba978eed9a7b1",
+      "sha256": "3a9219b8b30fd7ec37680852d0bb7c9630c53723dfb7576573c8c41826b9ad59"
+    },
+    {
+      "path": "research/e8-quadratic-support-capacity/PROOF.md",
+      "usage": "provenance",
+      "git_blob": "4da8e98edcfbbb9d5cd17b7ee921aa323d2fc724",
+      "sha256": "0a68df931e4da65a9568a5ad3731c2a6c6f6b6fca57839d7d4c12a6fba0b333e"
+    }
+  ]
+}
diff --git a/research/p104-quadratic-union-reduction/TASK.json b/research/p104-quadratic-union-reduction/TASK.json
new file mode 100644
index 0000000000..5526a32d3e
--- /dev/null
+++ b/research/p104-quadratic-union-reduction/TASK.json
@@ -0,0 +1,94 @@
+{
+  "schema_version": 1,
+  "task_id": "complex-rank-shape-decoder",
+  "priority_revision": 8,
+  "base_commit": "a5bff3bf133e482541c09eba4e773884bdb2b1b7",
+  "original_card": {
+    "id": "complex-rank-shape-decoder",
+    "question": "Can a legal decoder or coframe change improve the full signed moment, including changed helper targets?",
+    "starting_points": [
+      "docs/research/current-priorities.md",
+      "docs/research/research-family-status.md",
+      "certificates/selected-result.json",
+      "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md",
+      "docs/research/recursive-invoice-preflight.md"
+    ],
+    "methods": [
+      "Construct and independently check one source-bound instance of the stated first experiment.",
+      "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change."
+    ],
+    "acceptance_gate": "A source-bound arbitrary-input identity and legal producer/consumer boundary with the complete paid and productive target invoice, including restoration, ownership, native alignment and extra charges. Price under the actual current model; historical ceiling.py assumptions must be established before use. A favorable optimistic relaxation keeps a route open but is not a completed supplier. A scoped local result remains useful; expansion requires the family-level budget gate.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_selected_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.",
+      "scope": "Source-bound orientation only, not a supplier replay or theorem proof."
+    },
+    "first_experiment": "Price one complete changed itinerary with both paid and productive histograms. Check #5693/#5698 for overlap and their exact hypotheses before another coframe search. Use the signed invoice preflight where its boundary contract agrees; an inconclusive concave comparison is not a power crossing. Stop if an optimistic complete budget fails at the chosen target or native delivery remains unspecified.",
+    "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.",
+    "allowed_variations": [
+      "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes."
+    ],
+    "scope_change_triggers": [
+      "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.",
+      "Treating an archived proposal or local numerical pass as complete supplier admission."
+    ],
+    "overlap_terms": [
+      "coframe",
+      "signed moment",
+      "5693",
+      "5698"
+    ],
+    "existing_checks": [
+      {
+        "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.",
+        "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md",
+        "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.",
+        "status": "reviewed",
+        "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137",
+        "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5"
+      }
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "Prove the sharp full-E8 two-affine-plane union bound 68, classify equality, and reduce the P104 66-union proof to the removed-line intersection of that one class.",
+  "scope_change_reason": "The advance claim targets PR6218 open question 1. This first original partial step isolates the puncture-dependent obstruction rather than proving full compatibility/disjointness or supplying a decoder itinerary.",
+  "bottleneck_link": "A side proof reduction for the geometric counting step in the P104 nine-term B-form decoder obstruction. It does not change a paid/productive invoice or kappa.",
+  "budget_minutes": 60,
+  "stop_rule": "Ship this first verified original reduction; leave puncture-specific and compatibility arguments open.",
+  "outcome": "partial",
+  "evidence": "PROOF.md and warning-strict normal/optimized verify.py: all 289440 relative quadratic cases, 43180 direct affine slices, two attaining fixtures and seven rejection controls.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Show every exceptional 68-point union contains at least two of the sixteen removed lines.",
+      "why_it_matters": "Together with this theorem this replaces the finite P104 66-union bound by a geometric proof.",
+      "first_step": "Use the shared-line symplectic/isotropic equality normal form and the two removed orthogonal frames.",
+      "blocked_by": "A puncture-specific geometric argument is not supplied."
+    },
+    {
+      "question": "Prove compatible-plane disjointness under the source hyperplane and non-orthogonal exception contract.",
+      "why_it_matters": "Would close the source geometric alternative to its pair census.",
+      "first_step": "After the union step, analyze the root-normal case and the exact uncovered root relationships.",
+      "blocked_by": "The union theorem alone does not track non-orthogonality of uncovered ports."
+    }
+  ],
+  "source_question": {
+    "pr": 6218,
+    "author": "Matarener",
+    "head": "159352d273bd7b9f92c55cee3a9ac9b955de9b86",
+    "section": "Open next questions 1"
+  },
+  "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19279538",
+  "progress_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19279624",
+  "environment": {
+    "python": "CPython 3.12.15",
+    "platform": "macOS",
+    "priority_revision": 8
+  }
+}
diff --git a/research/p104-quadratic-union-reduction/VERIFY.json b/research/p104-quadratic-union-reduction/VERIFY.json
new file mode 100644
index 0000000000..edf9247a70
--- /dev/null
+++ b/research/p104-quadratic-union-reduction/VERIFY.json
@@ -0,0 +1,35 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/p104-carrier-code-uniqueness/e8/E8-PROOF.md",
+    "research/p104-carrier-code-uniqueness/e8/ports.json"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-Werror",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 60,
+      "checks": "Exact relative quadratic configurations, all direct slices, attaining fixtures, source binding and seven rejection controls."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-O",
+        "-Werror",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 60,
+      "checks": "Same complete checks with optimization; all contracts use explicit exceptions."
+    }
+  ]
+}
diff --git a/research/p104-quadratic-union-reduction/verify.py b/research/p104-quadratic-union-reduction/verify.py
new file mode 100644
index 0000000000..23e5227e6f
--- /dev/null
+++ b/research/p104-quadratic-union-reduction/verify.py
@@ -0,0 +1,239 @@
+"""Exact corroboration of the quadratic-union reduction; Apache-2.0."""
+from collections import Counter
+from hashlib import sha256
+from itertools import combinations
+from pathlib import Path
+import json
+import platform
+
+PACKAGE = Path(__file__).resolve().parent
+
+
+def require(condition, reason):
+    if not condition:
+        raise ValueError(reason)
+
+
+def parity(value):
+    return value.bit_count() & 1
+
+
+def binary_rank(rows):
+    basis = [0] * 4
+    for value in rows:
+        for pivot in range(3, -1, -1):
+            if value >> pivot & 1:
+                if basis[pivot]:
+                    value ^= basis[pivot]
+                else:
+                    basis[pivot] = value
+                    break
+    return sum(value != 0 for value in basis)
+
+
+def planes(dimension):
+    require(2 <= dimension <= 8, 'plane ambient dimension')
+    return [(a, b, a ^ b) for a in range(1, 1 << dimension)
+            for b in range(a + 1, 1 << dimension) if (a ^ b) > b]
+
+
+def quadratic_values(dimension, polar, linear):
+    edges = list(combinations(range(dimension), 2))
+    return [parity(x & linear) ^ (sum(
+        ((x >> a) & 1) * ((x >> b) & 1) * ((polar >> k) & 1)
+        for k, (a, b) in enumerate(edges)) & 1)
+        for x in range(1 << dimension)]
+
+
+def offsets(plane, code):
+    return dict(zip(plane, (code & 1, code >> 1, parity(code))))
+
+
+def slice_size(gauss):
+    return 32 - 2 * gauss
+
+
+def check_bound(size_a, size_b, union, dimension, consistent):
+    require(union <= 68, 'universal union bound')
+    shape = (dimension == 3 and not consistent
+             and sorted((size_a, size_b)) == [32, 36])
+    require((union == 68) == shape, 'complete equality shape')
+    require(union % 2 == 0, 'even union cardinality')
+    if size_a == size_b == 36:
+        require(union <= 66, 'two maximum slices bound')
+
+
+def consistent_cases(dimension, polar, pairs, counts, maxima):
+    for linear in range(1 << dimension):
+        values = quadratic_values(dimension, polar, linear)
+        gauss = {p: 1 + sum(1 - 2 * values[x] for x in p)
+                 for pair in pairs for p in pair}
+        whole = sum(1 - 2 * value for value in values)
+        numerator = (1 << 8) - 16 * whole
+        require(numerator % (1 << (dimension + 1)) == 0,
+                'integral intersection count')
+        intersection = numerator // (1 << (dimension + 1))
+        for a, b in pairs:
+            size_a, size_b = slice_size(gauss[a]), slice_size(gauss[b])
+            union = size_a + size_b - intersection
+            check_bound(size_a, size_b, union, dimension, True)
+            counts['consistent'] += 1
+            if size_a == size_b == 36:
+                maxima[dimension] = max(maxima.get(dimension, 0), union)
+
+
+def inconsistent_cases(dimension, polar, pairs, counts):
+    if dimension == 4:
+        return  # The constraint planes have trivial intersection.
+    values = quadratic_values(dimension, polar, 0)
+    for a, b in pairs:
+        common = set(a) & set(b)
+        for code_a in range(4):
+            first = offsets(a, code_a)
+            for code_b in range(4):
+                second = offsets(b, code_b)
+                if all(first[x] == second[x] for x in common):
+                    continue
+                ga = 1 + sum(1 - 2 * (values[x] ^ first[x]) for x in a)
+                gb = 1 + sum(1 - 2 * (values[x] ^ second[x]) for x in b)
+                size_a, size_b = slice_size(ga), slice_size(gb)
+                check_bound(size_a, size_b, size_a + size_b, dimension, False)
+                if size_a + size_b == 68:
+                    symplectic = a if ga == -2 else b
+                    isotropic = b if ga == -2 else a
+                    require(len(common) == 1, 'one shared nonzero vector')
+                    require(all(values[x] ^ values[y] ^ values[x ^ y] == 0
+                                for x in isotropic for y in isotropic),
+                            '32-point equality plane is isotropic')
+                    x, y = symplectic[:2]
+                    require(values[x] ^ values[y] ^ values[x ^ y] == 1,
+                            '36-point equality plane is symplectic')
+                    counts['maximum_shape'] += 1
+                counts['inconsistent'] += 1
+
+
+def check_relative_forms():
+    counts, maxima = Counter(), {}
+    for dimension in range(2, 5):
+        all_planes = planes(dimension)
+        pairs = [(a, b) for index, a in enumerate(all_planes)
+                 for b in all_planes[index:]
+                 if binary_rank(a + b) == dimension]
+        for polar in range(1 << (dimension * (dimension - 1) // 2)):
+            consistent_cases(dimension, polar, pairs, counts, maxima)
+            inconsistent_cases(dimension, polar, pairs, counts)
+    require(counts['consistent'] + counts['inconsistent'] == 289440,
+            'complete relative-form domain')
+    require(maxima == {2: 36, 3: 52, 4: 66}, 'two-36 branch maxima')
+    return {'counts': dict(counts), 'two_36_maxima_by_span': maxima}
+
+
+def canonical_q(value):
+    return sum(((value >> (2 * k)) & 1)
+               * ((value >> (2 * k + 1)) & 1) for k in range(4)) & 1
+
+
+def canonical_b(left, right):
+    return canonical_q(left ^ right) ^ canonical_q(left) ^ canonical_q(right)
+
+
+def check_all_slices():
+    roots = [x for x in range(256) if canonical_q(x)]
+    full = (1 << len(roots)) - 1
+    zero = [sum(1 << i for i, u in enumerate(roots)
+                if canonical_b(u, a) == 0) for a in range(256)]
+    histogram = Counter()
+    for plane in planes(8):
+        a, b, _ = plane
+        for code in range(4):
+            first = zero[a] if not (code & 1) else full ^ zero[a]
+            second = zero[b] if not (code >> 1) else full ^ zero[b]
+            actual = (first & second).bit_count()
+            off = offsets(plane, code)
+            gauss = 1 + sum(1 - 2 * (canonical_q(x) ^ off[x]) for x in plane)
+            require(actual == slice_size(gauss), 'direct slice/Fourier equality')
+            histogram[actual] += 1
+    require(sum(histogram.values()) == 43180, 'all affine plane constraints')
+    require(set(histogram) == {24, 28, 32, 36}, 'slice cardinality spectrum')
+    return {'root_lines': len(roots), 'slice_histogram': dict(histogram)}
+
+
+def check_attainment():
+    roots = {x for x in range(256) if canonical_q(x)}
+    first = {x for x in roots if x & 3 == 3}
+    second = {x for x in roots if not (x & 2) and x & 8}
+    third = {x for x in roots if x & 12 == 12}
+    require((len(first), len(second), len(first & second), len(first | second))
+            == (36, 32, 0, 68), '68-point attainment')
+    require((len(third), len(first & third), len(first | third)) == (36, 6, 66),
+            'two-36 sharpness')
+    return {'maximum_fixture': [len(first), len(second), len(first | second)],
+            'two_36_fixture': [len(first), len(third), len(first | third)]}
+
+
+def check_plus_hypothesis():
+    minus = {x for x in range(256)
+             if canonical_q(x) ^ (x & 1) ^ ((x >> 1) & 1)}
+    first = {x for x in minus if not (x & 32) and not (x & 128)}
+    second = {x for x in minus if x & 32 and not (x & 128)}
+    require((len(minus), len(first), len(second), len(first | second))
+            == (136, 40, 32, 72), 'opposite-sign counterdomain')
+    return {'minus_shell': len(minus), 'minus_union': len(first | second)}
+
+
+def check_e8_link():
+    rows = json.loads((PACKAGE / 'SOURCES.json').read_text())['files']
+    root = PACKAGE.parent.parent
+    for row in rows:
+        if row['usage'] == 'input':
+            require(sha256((root / row['path']).read_bytes()).hexdigest()
+                    == row['sha256'], 'declared source bytes')
+    even = [x for x in range(512) if parity(x) == 0]
+    nonsingular = {x for x in even if (x.bit_count() // 2) & 1}
+    labels = {511 ^ x for x in nonsingular}
+    ports_path = root / 'research/p104-carrier-code-uniqueness/e8/ports.json'
+    ports = json.loads(ports_path.read_text())
+    require(len(ports) == len(set(ports)) == 104 and set(ports) <= labels,
+            'P104 is the declared puncture of the quadratic root model')
+    require(len(labels) == 120, 'complete E8 label shell')
+    gauss = sum(1 - 2 * ((x.bit_count() // 2) & 1) for x in even)
+    require(gauss == 16, 'plus-type quadratic normalization')
+    return {'quadratic_gauss_sum': gauss, 'full_labels': len(labels),
+            'punctured_labels': len(ports), 'removed_lines': len(labels-set(ports))}
+
+
+def check_rejections():
+    rejected = 0
+    bad = [(36, 36, 68, 3, False), (36, 32, 70, 4, True),
+           (36, 32, 68, 4, True), (36, 32, 68, 3, True),
+           (32, 32, 68, 3, False), (36, 36, 65, 4, True)]
+    for args in bad:
+        try:
+            check_bound(*args)
+        except ValueError:
+            rejected += 1
+    require(rejected == len(bad), 'false-bound and equality controls')
+    try:
+        planes(9)
+    except ValueError:
+        rejected += 1
+    require(rejected == 7, 'dimension-domain rejection')
+    return rejected
+
+
+def main():
+    result = {'status': 'PASS_P104_QUADRATIC_UNION_REDUCTION',
+              'claim_type': 'scoped proof with finite exact corroboration',
+              'relative_forms': check_relative_forms(),
+              'all_slices': check_all_slices(), 'attainment': check_attainment(),
+              'plus_hypothesis_control': check_plus_hypothesis(),
+              'e8_link': check_e8_link(), 'rejected_controls': check_rejections(),
+              'python': platform.python_version()}
+    result['package_sha256'] = {
+        path.name: sha256(path.read_bytes()).hexdigest()
+        for path in sorted(PACKAGE.iterdir()) if path.is_file()}
+    print(json.dumps(result, sort_keys=True, indent=2))
+
+
+if __name__ == '__main__':
+    main()