diff --git a/research/bw16-global-clique-126/PROOF.md b/research/bw16-global-clique-126/PROOF.md
new file mode 100644
index 0000000000..baf7c3c08c
--- /dev/null
+++ b/research/bw16-global-clique-126/PROOF.md
@@ -0,0 +1,130 @@
+# A global upper bound of 126
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+## The finite object
+
+Coordinates are indexed by x in F2^4, represented by the integers 0 through
+15 in little-endian binary. Use ordinary real inner products. The vertex set
+V consists of the following canonical norm-eight lines, with the first
+nonzero coordinate positive:
+
+1. The 240 lines 2(e_i + s e_j), i<j and s in {+1,-1}.
+2. On each affine hyperplane H={x:a dot x=b}, a!=0, the 64 lines with entries
+   +1 or -1 on H, zero elsewhere, and an even number of negative entries.
+
+The second family has 30 supports, each of size eight. Quotienting the 128
+even sign patterns by overall sign gives 64 lines per support, so |V|=2160.
+This is the norm-eight BW16 shell in DaysSky's PR895 normalization. The shell
+setting and its two-shape description are credited premises. They can also
+be seen directly in RM(1,4)+2 RM(3,4)+4 Z^16: a norm-eight low residue has
+weight zero or eight, and RM(3,4) is the even-weight code.
+
+A clique means a subset of V with every two distinct lines nonorthogonal.
+
+## Lemma 1: the D16 equality case
+
+Let D be the first 240-line family. A clique in D has size at most 15. Every
+15-line clique has the form
+
+    S(i,s) = { 2(e_i+s_j e_j) : j!=i },  s_j in {+1,-1},
+
+up to independent overall signs of the representatives.
+
+To prove this, replace each line by its two-element coordinate support.
+Disjoint supports give orthogonal lines. Two distinct lines on the same
+support are orthogonal too, so a clique has at most one line per support.
+A pairwise intersecting family of two-element subsets either has a common
+point, or is contained in a triangle. Indeed, take {a,b} and {a,c}. Any edge
+avoiding a must be {b,c}; if that edge is present, all edges lie in the same
+triangle. A common-point family on sixteen coordinates has at most fifteen
+edges, and equality uses every other coordinate. This proves the lemma.
+
+## Lemma 2: a full star permits at most thirty lines in all
+
+If a clique C in V contains S(i,s), then |C|<=30. The bound is attained.
+
+Lemma 1 gives |C intersect D|<=15. Now consider an odd line v in C on an
+affine hyperplane H. If i is outside H, choose j distinct from i outside H;
+there are seven such choices. Both coordinates of 2(e_i+s_j e_j) vanish
+in v, contradicting compatibility. Thus i is in H.
+
+Choose the sign of v so v_i=1. For each j in H other than i, the inner
+product with the star line is 2(1+s_j v_j). This is nonzero exactly when
+v_j=s_j. Hence a fixed H permits at most one odd line. There are precisely
+fifteen affine hyperplanes containing i, one for each nonzero a with
+b=a dot i. Therefore |C|<=15+15=30. Some prescribed sign patterns fail the
+even-parity requirement; this can only reduce the count.
+
+For attainment take i=0, all s_j=+1, and the fifteen all-positive indicator
+vectors of the hyperplanes through zero. Distinct hyperplanes intersect in
+four coordinates, so these odd lines are mutually nonorthogonal. Each also
+meets every star line nonorthogonally. The resulting clique has thirty lines.
+
+## The exact nine-chart certificate
+
+List the six quadratic monomials in this order:
+
+    x0*x1, x0*x2, x0*x3, x1*x2, x1*x3, x2*x3.
+
+An integer c from 0 through 63 encodes their binary coefficients. Put
+q_c(x)=sum_{i<j} c_ij*x_i*x_j in F2 and define the integer matrix
+
+    H_c[x,b] = (-1)^(q_c(x)+b dot x),  x,b in F2^4.
+    U_c = H_c/4.
+
+Use exactly these eight forms:
+
+    0, 57, 53, 46, 35, 28, 18, 15.
+
+Together with the identity chart they satisfy the following finite facts:
+
+- H_c H_c^T=16 I for each of the eight matrices, so U_c is orthogonal.
+- D and the eight sets U_c D are pairwise disjoint subsets of V of size 240.
+  Their union is V.
+- For every c and every v in V, U_c^T v is integral and represents a line
+  in V. This exhausts 8*2160=17280 image checks. Orthogonality and the finite
+  bijection establish U_c^T V=V.
+
+`verify.py` constructs the entire shell and checks these facts with exact
+integer arithmetic. It divides only after testing divisibility. Thus these
+facts are a complete finite certificate, rather than sampled evidence or
+floating eigenvalue estimates. No theorem about an unmaterialized orbit is
+needed. Quadratic-phase Walsh bases and Kerdock/mutually unbiased bases are
+classical; the table is an explicit certificate, not a claim to those ideas.
+
+## Theorem
+
+Every clique in V has at most 126 lines.
+
+Suppose |C|>=127. The nine disjoint D16 sets partition V, so at least one
+contains fifteen members of C. Lemma 1 excludes more than fifteen. If it is
+the identity set, Lemma 2 gives |C|<=30. Otherwise apply U_c^T to the whole
+clique. The exact certificate ensures that the image is still a clique in V,
+and its intersection with D contains a full fifteen-line star. Lemma 2 again
+gives |C|<=30, a contradiction. Equivalently, every clique larger than thirty
+has at most fourteen lines in each chart, giving |C|<=9*14=126.
+
+The basic nine-chart counting bound is 135. The new step removes its D16
+equality case in every chart, improving that bound by nine. The classical
+135-frame geometry itself is not claimed as new. This is a finite geometric
+obstruction with a scoped written proof over all subsets of this fixed V;
+it is neither a failed clique search nor an all-dimensional lattice theorem.
+
+## Exact evidence and limits
+
+Besides the complete chart checks, the verifier compares the star formula
+with direct integer inner products against all 1920 odd lines on 176 named
+center/sign fixtures. It enumerates all 32768 sign patterns at center zero
+by the independent hyperplane-parity formula. The proof covers arbitrary
+signs at every center; the 176 direct fixtures are not described as an
+exhaustive census of all center/sign pairs. The thirty-line attainer has
+all 435 pairs checked.
+
+The published 72-line lower witness in PR895 is a cited result, not replayed
+here. The resulting interval 72<=omega(V)<=126 does not determine omega(V).
+A clique upper bound is not an upper bound on the binary decoder's minimum
+fitting rank. Physical native realization, scalar/helper delivery, arbitrary
+dirty restoration, a complete paid invoice and the five selected framework
+assumptions remain separate. No kappa or selected-frontier change follows.
+Independent human and formal proof-kernel review are unclaimed.
diff --git a/research/bw16-global-clique-126/README.md b/research/bw16-global-clique-126/README.md
new file mode 100644
index 0000000000..4cbe13c8b4
--- /dev/null
+++ b/research/bw16-global-clique-126/README.md
@@ -0,0 +1,104 @@
+# Global BW16 nonorthogonality clique bound 126
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+Every pairwise nonorthogonal subset of the 2160 norm-eight BW16 lines has
+at most **126** lines. This is a finite certificate with a scoped written
+combinatorial proof. The [proof](PROOF.md) covers every subset of this fixed
+shell, rather than a bounded search around one clique.
+
+Nine 240-line D16 sets partition the shell. Each contains at most fifteen
+clique members. The new equality-case step shows that fifteen members in
+any one chart force the entire clique to have at most thirty lines. Thus
+any clique larger than thirty has at most fourteen members per chart:
+
+    |C| <= 9*14 = 126.
+
+The baseline nine-chart count gives 135. The new step lowers it by nine.
+The conditional thirty-line bound is attained. DaysSky's PR895 supplies the
+published 72-line lower witness as a credited premise. It is not replayed.
+The remaining global interval is therefore 72<=omega<=126.
+
+## Reproduce
+
+From the repository root, with standard-library CPython 3.12:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/bw16-global-clique-126/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/bw16-global-clique-126/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/bw16-global-clique-126
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/bw16-global-clique-126 --check-source-history
+```
+
+Another CPython 3.12 executable may replace that absolute path. The direct
+marker is `PASS_BW16_GLOBAL_CLIQUE_126`. Verification is read-only and needs
+no Git, network, source imports, numerical library or solver. `--emit` writes
+a newly computed receipt to stdout; it is absent from registered checks.
+[RESULT.json](RESULT.json) is generated by that code, bound to the package
+source hashes and compared byte for byte in ordinary verification.
+
+The certificate checks all 2160 shell members against an independent
+Construction-D membership predicate, all nine disjoint blocks and all 17280
+inverse chart images. It also checks 176 literal star fixtures against all
+1920 odd lines, all 32768 sign patterns at center zero by a parity formula,
+and all 435 pairs of a thirty-line attainer. Six controls reject wrong norm,
+nonaffine support, odd sign parity, a damaged orthogonal matrix, duplicate
+charts and the false compatibility of the two signs on one coordinate edge.
+
+## Scope and credit
+
+Source and main predecessor: DaysSky / [PR895](https://github.com/CrocSwap/integer-mult-bounds/pull/895),
+head `3bf6fccaf17521ffdb9b3bec2740ba4886478556`. Its BW16 shell and screen
+setting motivate the global question. No source executable or source witness
+is copied or audited. Nick Petalas / [PR5118](https://github.com/CrocSwap/integer-mult-bounds/pull/5118)
+gives the earlier local insertion obstruction, not this global bound.
+DreamingOfClouds / PR446, PR595 and PR2244, Joel Pulikkan / PR620 and the
+retained decoder/lattice lineage keep their credit.
+
+Barnes-Wall, Reed-Muller, Construction-D, Walsh characters and Kerdock bases
+are classical. The classical 135-frame decomposition is also discussed in
+[Noam Elkies's lattice notes](https://people.math.harvard.edu/~elkies/M272.19/nov13.pdf).
+The broader Barnes-Wall construction is in [Nebe, Rains and Sloane](https://arxiv.org/abs/math/0207186).
+The claimed addition is the explicit global 126 bound and its equality-case
+proof and executable certificate. No general literature-priority claim is made.
+
+This changes the complex-rank-shape-decoder card to a geometric side result;
+it does not price a changed supplier. The selected-baseline binding-only
+first example passed. Canonical base is
+`7c49fe32c55de02c2c873655c804b16e4c3fef0a`, priority revision 8, selected PR6030.
+Live open/account work, recent handoffs and active Discussions, all retrieved
+BW16 PR bodies, main general-form and merged searches and local reservations
+were checked. Broader cached overlap has coverage/freshness limits; arbitrary
+diffs and unpublished work are not exhaustively covered.
+
+The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19375419)
+planned a global spectral certificate. The delivered certificate uses nine
+explicit orthogonal coordinate charts and the sharp full-star restriction.
+Discovery stopped at the first new verified bound. The classical 135 bound
+was identified as prior geometry, not claimed as an original improvement.
+
+The maximum clique, minimum binary fitting rank, native/helper/restoration
+costs, complete recursive/outer bill and multiplication theorem remain open.
+No kappa or selected-frontier change is claimed. Independent human and formal
+proof-kernel review are unclaimed. No Lean, Docker, selected cold replay or
+predecessor scientific suite was run.
+
+Power-of-ten scope is this fixed verifier. It has no recursion or dynamic
+code loading; all enumerations are bounded by sixteen coordinates, 2160
+lines, eight charts or 32768 sign patterns. Functions are below sixty lines.
+Managed Python allocation is a rule-3 deviation: live data are bounded by the
+fixed shell, nine 240-line blocks and one chart's 2160 images. The standard
+library allocates tuples/integers during checking. No process, cache, lock or
+background writer is created. Explicit exceptions keep all checks active
+under optimized Python. Input extensions need new resource bounds.
+
+## Open next questions
+
+1. Can the remaining interval 72<=omega<=126 be narrowed using compatibility
+   between distinct nonsaturated D16 charts? Start with their fourteen-line
+   equality possibilities. The present theorem does not classify them, and
+   this follow-on is not reserved.
+2. Can a changed decoder exploit a smaller set with a favorable complete
+   invoice? Start with an explicit fitting identity and charge every source,
+   target, restoration and native cost. Clique information alone cannot
+   answer that physical question.
diff --git a/research/bw16-global-clique-126/RESULT.json b/research/bw16-global-clique-126/RESULT.json
new file mode 100644
index 0000000000..6962ecc648
--- /dev/null
+++ b/research/bw16-global-clique-126/RESULT.json
@@ -0,0 +1,65 @@
+{
+  "block_sha256": [
+    "eb83acde02828b331447740e29e70860b76fadd1e8195539af660a945872c520",
+    "764f5983da5bbaa4f72107ee33bf0437a5f2662763b4f60fcdf9c79bf4d68e27",
+    "65ba5a9092a25f868251ac6855d9052017df6d2079a527331019381837ddf80f",
+    "02a24faf95dd2617ee0cce8e61afab59ac27c042cb7741160d625db259cf0736",
+    "c4b0c2cbc3ce2f29f3a13c298228d3d072a52f128819946270be278d7a3e076d",
+    "5c7f3d562b9739783b14e1a0ae330021b18f18386ffa85afd1a055f634f5b01e",
+    "4e314f41ad1235a5e4a2fa98655b388ad6f0db8c4da07f2c4904f6a7c495d518",
+    "c6996d13070d08bba9b159d0ec02aa3d4fcd4af486eb34532dcfdc2c176b87d6",
+    "a0d13f6d00a9e175e4d6a471711de28c14ee3f6e2c00a184268d85f974be4c97"
+  ],
+  "block_sizes": [
+    240,
+    240,
+    240,
+    240,
+    240,
+    240,
+    240,
+    240,
+    240
+  ],
+  "claim_type": "finite certificate with a scoped combinatorial proof",
+  "compatible_odd_histogram_at_center_zero": {
+    "0": 1024,
+    "15": 1024,
+    "7": 15360,
+    "8": 15360
+  },
+  "conditional_star_clique_maximum": 30,
+  "controls": [
+    "odd_sign_parity",
+    "nonaffine_support",
+    "wrong_norm",
+    "damaged_hadamard",
+    "duplicate_chart",
+    "same_edge_signs_are_orthogonal"
+  ],
+  "full_star_sign_patterns": 32768,
+  "global_clique_upper_bound": 126,
+  "inverse_transport_checks": 17280,
+  "literal_star_fixtures": 176,
+  "quadratic_forms": [
+    0,
+    57,
+    53,
+    46,
+    35,
+    28,
+    18,
+    15
+  ],
+  "schema_version": 1,
+  "shell_lines": 2160,
+  "shell_sha256": "1ec1067400299e389af79713c6713fbb50c0271ddadee16f9da838c5843f9134",
+  "source_sha256": {
+    "PROOF.md": "cfdfb4b412a8461045ea31ad39572713ddd1d9ff1faa0f6b0982d5d8088dc8ae",
+    "README.md": "47adadbe6c6e67459fab82c1a5c40aab035585606481d5ad70dc7285a5c78ea6",
+    "SOURCES.json": "911ffe8b456c49ccd19ee42c8e21b226a56dacba515e857300aa28cc1db87be7",
+    "TASK.json": "19930226c3438c68779af4ba15d2a2ae4310b6fec1510c81099950ef123b2e6e",
+    "VERIFY.json": "70b4e98924712f9a57a96ad5c0c9492e7f51865446aab15f7ac4eded2c86a371",
+    "verify.py": "a22fe0360e3c8a57dd929151b9ce91fe650d2a4f105795d0dadad890af86c503"
+  }
+}
diff --git a/research/bw16-global-clique-126/SOURCES.json b/research/bw16-global-clique-126/SOURCES.json
new file mode 100644
index 0000000000..594089b9c7
--- /dev/null
+++ b/research/bw16-global-clique-126/SOURCES.json
@@ -0,0 +1,18 @@
+{
+  "schema_version": 1,
+  "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a",
+  "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"
+    }
+  ]
+}
diff --git a/research/bw16-global-clique-126/TASK.json b/research/bw16-global-clique-126/TASK.json
new file mode 100644
index 0000000000..4bd5ecfdc1
--- /dev/null
+++ b/research/bw16-global-clique-126/TASK.json
@@ -0,0 +1,94 @@
+{
+  "schema_version": 1,
+  "task_id": "complex-rank-shape-decoder",
+  "priority_revision": 8,
+  "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a",
+  "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": "A global upper bound of 126 on BW16 nonorthogonality cliques, through an exact nine-D16 atlas and exclusion of its saturated stars.",
+  "scope_change_reason": "Take the global finite-geometric gap left by DaysSky PR895; this is a side result rather than a current P104 supplier itinerary.",
+  "bottleneck_link": "Geometric side result: limits clique-based lower-witness searches in this alternative lattice unit; no current supplier gain is inferred.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop discovery at the first new verified global bound, then package without further tightening.",
+  "outcome": "completed",
+  "evidence": "PROOF.md, generated RESULT.json and standalone exact verify.py.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Can cross-chart compatibility lower the global bound below 126?",
+      "why_it_matters": "The exact maximum remains in the cited interval 72..126.",
+      "first_step": "Classify fourteen-line nonsaturated D16 intersections before coupling charts.",
+      "blocked_by": "No such classification or coupling certificate is supplied."
+    },
+    {
+      "question": "Can a changed physical decoder benefit from this lattice geometry?",
+      "why_it_matters": "A clique bound alone neither prices nor admits a supplier.",
+      "first_step": "Write one fitting identity with its complete native and restoration bill.",
+      "blocked_by": "No physical construction or complete invoice is supplied."
+    }
+  ],
+  "source_question": {
+    "pr": 895,
+    "author": "DaysSky",
+    "head": "3bf6fccaf17521ffdb9b3bec2740ba4886478556",
+    "usage": "credited shell setting; no executable dependency"
+  },
+  "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19375419",
+  "environment": {
+    "python": "CPython 3.12.15",
+    "platform": "macOS arm64",
+    "dependencies": "standard library only"
+  },
+  "discovery_stop": "First new bound 126 established; classical frame bound 135 is prior geometry."
+}
diff --git a/research/bw16-global-clique-126/VERIFY.json b/research/bw16-global-clique-126/VERIFY.json
new file mode 100644
index 0000000000..a388082079
--- /dev/null
+++ b/research/bw16-global-clique-126/VERIFY.json
@@ -0,0 +1,34 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Exact complete shell/chart partition and automorphisms; full-star fixtures, parity census, attainer and six semantic controls; generated source-bound receipt."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-O",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Exact complete shell/chart partition and automorphisms; full-star fixtures, parity census, attainer and six semantic controls; generated source-bound receipt."
+    }
+  ]
+}
diff --git a/research/bw16-global-clique-126/verify.py b/research/bw16-global-clique-126/verify.py
new file mode 100644
index 0000000000..7546b48d27
--- /dev/null
+++ b/research/bw16-global-clique-126/verify.py
@@ -0,0 +1,267 @@
+"""Exact BW16 chart certificate; produced by Nick Petalas, Apache-2.0."""
+
+import argparse
+import hashlib
+import itertools
+import json
+from pathlib import Path
+
+HERE = Path(__file__).resolve().parent
+PAIRS = tuple(itertools.combinations(range(4), 2))
+# Bit k is the coefficient of x_i*x_j for (i,j)=PAIRS[k].
+FORMS = (0, 57, 53, 46, 35, 28, 18, 15)
+
+
+def require(condition, message):
+    if not condition:
+        raise ValueError(message)
+
+
+def canonical(vector):
+    require(len(vector) == 16 and any(vector), "nonzero sixteen-vector required")
+    first = next(value for value in vector if value)
+    return vector if first > 0 else tuple(-value for value in vector)
+
+
+def dot(left, right):
+    return sum(a * b for a, b in zip(left, right, strict=True))
+
+
+def shell_member(vector):
+    """Independent Construction-D membership, with the norm fixed to eight."""
+    if len(vector) != 16 or sum(value * value for value in vector) != 8:
+        return False
+    low = tuple(value % 2 for value in vector)
+    constant = low[0]
+    linear = tuple(low[1 << i] ^ constant for i in range(4))
+    for x in range(16):
+        predicted = (constant + sum(linear[i] * ((x >> i) & 1)
+                                    for i in range(4))) % 2
+        if predicted != low[x]:
+            return False
+    return sum((value - bit) // 2
+               for value, bit in zip(vector, low, strict=True)) % 2 == 0
+
+
+def make_shell():
+    lines = set()
+    for i, j in itertools.combinations(range(16), 2):
+        for sign in (1, -1):
+            lines.add(tuple(2 * (k == i) + 2 * sign * (k == j)
+                            for k in range(16)))
+    for a in range(1, 16):
+        for b in range(2):
+            support = [x for x in range(16) if (a & x).bit_count() % 2 == b]
+            require(len(support) == 8, "hyperplane size")
+            for signs in range(128):
+                if signs.bit_count() % 2:
+                    continue
+                vector = [0] * 16
+                vector[support[0]] = 1
+                for j, x in enumerate(support[1:]):
+                    vector[x] = 1 - 2 * ((signs >> j) & 1)
+                lines.add(tuple(vector))
+    require(len(lines) == 2160, "complete shell size")
+    require(all(shell_member(v) for v in lines), "shell membership")
+    return tuple(sorted(lines))
+
+
+def quadratic(form, x):
+    return sum(((form >> k) & 1) * ((x >> i) & 1) * ((x >> j) & 1)
+               for k, (i, j) in enumerate(PAIRS)) % 2
+
+
+def hadamard(form):
+    """Numerator H of the orthogonal matrix U=H/4."""
+    return tuple(tuple(1 - 2 * (quadratic(form, x) ^ ((b & x).bit_count() % 2))
+                       for b in range(16)) for x in range(16))
+
+
+def check_orthogonal(matrix):
+    for i in range(16):
+        for j in range(i, 16):
+            require(dot(matrix[i], matrix[j]) == 16 * (i == j),
+                    "Hadamard orthogonality")
+
+
+def roots_in_chart(matrix):
+    roots = set()
+    for i, j in itertools.combinations(range(16), 2):
+        for sign in (1, -1):
+            numerator = tuple(matrix[x][i] + sign * matrix[x][j]
+                              for x in range(16))
+            require(all(value % 2 == 0 for value in numerator), "root division")
+            roots.add(canonical(tuple(value // 2 for value in numerator)))
+    require(len(roots) == 240, "D16 block size")
+    return roots
+
+
+def inverse_transport(matrix, vector):
+    numerator = tuple(sum(matrix[x][b] * vector[x] for x in range(16))
+                      for b in range(16))
+    require(all(value % 4 == 0 for value in numerator), "chart denominator")
+    return canonical(tuple(value // 4 for value in numerator))
+
+
+def check_atlas(shell, forms=FORMS):
+    domain = set(shell)
+    coordinate = {v for v in shell if max(map(abs, v)) == 2}
+    require(len(coordinate) == 240, "coordinate block size")
+    blocks = [coordinate]
+    transport_checks = 0
+    for form in forms:
+        matrix = hadamard(form)
+        check_orthogonal(matrix)
+        block = roots_in_chart(matrix)
+        require(block <= domain, "chart root outside shell")
+        for previous in blocks:
+            require(not block & previous, "D16 blocks overlap")
+        blocks.append(block)
+        images = set()
+        for vector in shell:
+            image = inverse_transport(matrix, vector)
+            require(image in domain, "chart does not preserve shell")
+            images.add(image)
+            transport_checks += 1
+        require(images == domain, "chart is not onto shell")
+    require(len(blocks) == 9 and set.union(*blocks) == domain,
+            "atlas does not partition shell")
+    return blocks, transport_checks
+
+
+def star(center, signs):
+    leaves = [j for j in range(16) if j != center]
+    roots = []
+    for k, leaf in enumerate(leaves):
+        sign = 1 - 2 * ((signs >> k) & 1)
+        roots.append(canonical(tuple(2 * (j == center) + 2 * sign * (j == leaf)
+                                     for j in range(16))))
+    return tuple(roots)
+
+
+def compatible_odd(star_roots, odd_lines):
+    # Each root is sparse; this path uses literal integer inner products.
+    sparse = [tuple((i, value) for i, value in enumerate(root) if value)
+              for root in star_roots]
+    return {v for v in odd_lines
+            if all(sum(value * v[i] for i, value in root) != 0 for root in sparse)}
+
+
+def predicted_odd(center, signs):
+    """One possible line per affine hyperplane containing the star center."""
+    leaves = [j for j in range(16) if j != center]
+    values = {center: 1}
+    values.update({leaf: 1 - 2 * ((signs >> k) & 1)
+                   for k, leaf in enumerate(leaves)})
+    answer = set()
+    for a in range(1, 16):
+        b = (a & center).bit_count() % 2
+        support = [x for x in range(16) if (a & x).bit_count() % 2 == b]
+        vector = canonical(tuple(values[x] if x in support else 0
+                                 for x in range(16)))
+        if shell_member(vector):
+            answer.add(vector)
+    return answer
+
+
+def check_star_lemma(shell):
+    odd = tuple(v for v in shell if max(map(abs, v)) == 1)
+    require(len(odd) == 1920, "odd-line domain")
+    checked = 0
+    # Exhaust all signs at center zero. The proof quantifies over every center.
+    histogram = {}
+    masks = [sum(1 << (x - 1) for x in range(1, 16)
+                 if (a & x).bit_count() % 2 == 0) for a in range(1, 16)]
+    for signs in range(1 << 15):
+        count = sum((signs & mask).bit_count() % 2 == 0 for mask in masks)
+        histogram[str(count)] = histogram.get(str(count), 0) + 1
+    for center in range(16):
+        for signs in (0, 1, 3, 7, 31, 127, 255, 1023, 8191, 16383, 32767):
+            actual = compatible_odd(star(center, signs), odd)
+            require(actual == predicted_odd(center, signs), "star restriction")
+            require(len(actual) <= 15, "star cap")
+            checked += 1
+    witness = star(0, 0) + tuple(sorted(predicted_odd(0, 0)))
+    require(len(witness) == 30 and len(set(witness)) == 30, "star attainer size")
+    for left, right in itertools.combinations(witness, 2):
+        require(dot(left, right) != 0, "star attainer orthogonal pair")
+    return histogram, checked
+
+
+def check_controls(shell):
+    controls = []
+    for name, vector in (
+        ("odd_sign_parity", tuple(-1 if x == 0 else int(x < 8) for x in range(16))),
+        ("nonaffine_support", (1,) * 7 + (0, 1) + (0,) * 7),
+        ("wrong_norm", (2,) + (0,) * 15),
+    ):
+        require(not shell_member(vector), "accepted invalid membership control")
+        controls.append(name)
+    matrix = list(hadamard(FORMS[0]))
+    matrix[0] = (-matrix[0][0],) + matrix[0][1:]
+    try:
+        check_orthogonal(matrix)
+    except ValueError as error:
+        require(str(error) == "Hadamard orthogonality", "wrong matrix rejection")
+    else:
+        raise ValueError("accepted damaged Hadamard")
+    controls.append("damaged_hadamard")
+    try:
+        check_atlas(shell, (FORMS[0],) * 8)
+    except ValueError as error:
+        require(str(error) == "D16 blocks overlap", "wrong duplicate rejection")
+    else:
+        raise ValueError("accepted duplicate chart")
+    controls.append("duplicate_chart")
+    plus, minus = star(0, 0)[0], star(0, 1)[0]
+    require(plus != minus and dot(plus, minus) == 0, "opposite-edge control")
+    controls.append("same_edge_signs_are_orthogonal")
+    return controls
+
+
+def digest(value):
+    return hashlib.sha256(json.dumps(value, separators=(",", ":")).encode()).hexdigest()
+
+
+def result():
+    shell = make_shell()
+    blocks, checks = check_atlas(shell)
+    histogram, star_checks = check_star_lemma(shell)
+    controls = check_controls(shell)
+    require(9 * 14 == 126 and 30 < 127, "global pigeonhole implication")
+    sources = {}
+    for name in ("verify.py", "PROOF.md", "README.md", "TASK.json", "SOURCES.json", "VERIFY.json"):
+        sources[name] = hashlib.sha256((HERE / name).read_bytes()).hexdigest()
+    return {
+        "schema_version": 1,
+        "claim_type": "finite certificate with a scoped combinatorial proof",
+        "shell_lines": len(shell),
+        "shell_sha256": digest(shell),
+        "quadratic_forms": list(FORMS),
+        "block_sizes": [len(block) for block in blocks],
+        "block_sha256": [digest(sorted(block)) for block in blocks],
+        "inverse_transport_checks": checks,
+        "full_star_sign_patterns": 1 << 15,
+        "compatible_odd_histogram_at_center_zero": histogram,
+        "literal_star_fixtures": star_checks,
+        "conditional_star_clique_maximum": 30,
+        "global_clique_upper_bound": 126,
+        "controls": controls,
+        "source_sha256": sources,
+    }
+
+
+def main():
+    parser = argparse.ArgumentParser(description=__doc__)
+    parser.add_argument("--emit", action="store_true", help="emit a newly computed receipt on stdout")
+    args = parser.parse_args()
+    receipt = json.dumps(result(), indent=2, sort_keys=True) + "\n"
+    if args.emit:
+        print(receipt, end="")
+    else:
+        require((HERE / "RESULT.json").read_text() == receipt, "receipt mismatch")
+        print("PASS_BW16_GLOBAL_CLIQUE_126 lines=2160 blocks=9 transports=17280 bound=126")
+
+
+if __name__ == "__main__":
+    main()