From f0776668541d2828dd10e290c8e5adabe990f96d Mon Sep 17 00:00:00 2001
From: Nick Petalas <webmasternikos@gmail.com>
Date: Tue, 27 Oct 2026 12:43:54 +0000
Subject: [PATCH] feat(research): prove exact serialized carry state counts

---
 research/quarter-carry-cut-states/PROOF.md    | 143 +++++++++++
 research/quarter-carry-cut-states/README.md   | 116 +++++++++
 .../quarter-carry-cut-states/SOURCES.json     |  32 +++
 research/quarter-carry-cut-states/TASK.json   |  83 +++++++
 research/quarter-carry-cut-states/VERIFY.json |  32 +++
 research/quarter-carry-cut-states/verify.py   | 228 ++++++++++++++++++
 6 files changed, 634 insertions(+)
 create mode 100644 research/quarter-carry-cut-states/PROOF.md
 create mode 100644 research/quarter-carry-cut-states/README.md
 create mode 100644 research/quarter-carry-cut-states/SOURCES.json
 create mode 100644 research/quarter-carry-cut-states/TASK.json
 create mode 100644 research/quarter-carry-cut-states/VERIFY.json
 create mode 100644 research/quarter-carry-cut-states/verify.py

diff --git a/research/quarter-carry-cut-states/PROOF.md b/research/quarter-carry-cut-states/PROOF.md
new file mode 100644
index 0000000000..e691938cfc
--- /dev/null
+++ b/research/quarter-carry-cut-states/PROOF.md
@@ -0,0 +1,143 @@
+# Sharp state count at a serialized carry cut
+
+This is a scoped written proof, produced by Nick Petalas. Finite enumeration
+corroborates the proof; it does not replace its quantifiers.
+
+## Contract
+
+Fix integers q>=2, Q>=1, A in Z and D>=1 with gcd(D,qQ)=1. The parameters are public.
+The source low digit x and target low digit y independently range over
+{0,...,q-1}. Put
+
+    t = (y + A D^(-1) x) mod q,       0<=t<q,
+    K(x,y) = (A x + D y - D t)/q,
+    C(x,y) = D^(-1) K(x,y) mod Q.
+
+Each inverse is taken in the indicated modulus. When Q=1, C is zero. The
+integer K is well-defined. C is the high translation of the rational shear
+on the full modulus qQ, with source and target high digits initially zero.
+
+A deterministic producer reads all of x before any of y. After that cut it
+cannot reread x, inspect an x-dependent external object, or retrieve an early
+output. It must subsequently produce C exactly for every y. Every retained
+x-dependent datum, including control and head positions, is part of its cut
+state. Computation on the public parameters is unrestricted. The theorem
+counts distinguishable states at this cut, not total peak workspace or time.
+
+Two source digits may share a state exactly when their complete response
+functions y -> C(x,y) agree. A common state gives identical future behavior,
+and an equivalence-class label is a sufficient one-way message.
+
+## Theorem
+
+Write
+
+    g = gcd(A,q),     d = q/g,     e = Q/gcd(A/g,Q).
+
+The convention gcd(0,q)=q applies. The exact minimum number R of cut states is
+
+    R = 1                         if Q=1,
+    R = d min(g,e)                if Q>1.
+
+Consequently ceil(log2 R) binary bits are necessary and sufficient for an
+encoding at this cut. Sufficiency permits later unrestricted computation;
+it is not a constant-workspace physical producer.
+
+### 1. Every response is a single step
+
+Let
+
+    r_x = (A D^(-1) x) mod q,
+    b_x = (A x - D r_x)/q.
+
+Since 0<=r_x,y<q,
+
+    K(x,y) = b_x + D 1[y >= q-r_x],
+    C(x,y) = D^(-1)b_x + 1[y >= q-r_x] mod Q.
+
+For r_x=0, the threshold is q and the indicator is always zero.
+
+If Q>1, two different r values give different response functions. At y=0
+their constant terms either differ already, or agree. In the latter case,
+choose y=q-max(r_x,r_x'). Exactly one indicator is one, so the responses
+differ by one modulo Q. This y lies in {1,...,q-1} when the r values differ.
+
+For equal r, the response functions agree precisely when b_x=b_x' mod Q,
+because D is a unit modulo Q.
+
+### 2. Count each fiber exactly
+
+Multiplication by A D^(-1) modulo q has exactly d image residues and g
+preimages per image residue. Equal-r digits have the unique form
+
+    x = x0 + j d,      0<=x0<d,      0<=j<g.
+
+The r value depends only on x0, and different x0 have different r values.
+Within this fiber,
+
+    b_(x0+jd) = b_x0 + j A/g.
+
+The additive order of A/g modulo Q is e. The g consecutive j values
+therefore give exactly min(g,e) distinct b residues. Different fibers cannot
+merge by part 1. This proves R=d min(g,e). For Q=1 every response is zero,
+so R=1. The argument includes A=0: then d=e=1.
+
+### 3. Attain the bound
+
+For Q>1 put m=min(g,e), write x=x0+jd as above, and retain
+
+    label(x) = x0 m + (j mod e).
+
+The labels are exactly {0,...,dm-1}. Decode a label into
+
+    x_star = floor(label/m) + (label mod m) d.
+
+This is a valid source digit with the same r and the same b modulo Q as x.
+Computing C(x_star,y) therefore returns the correct answer. For Q=1 retain
+the single constant label. Thus the information lower bound is attained.
+
+## Quarter-shear consequence
+
+Take A=1, D=4, odd q>=3 and Q=q^(w-1). If w=1, the high output is trivial and
+R=1. For every w>=2, g=1 and R=q. The exact serialized-cut storage is therefore
+ceil(log2 q) binary bits, despite a width-independent final carry packet.
+
+The literal fixture q=257,w=2 has 257 pairwise distinct response functions,
+requiring nine binary bits at the cut. Its integer K takes only eight values,
+{-3,-2,-1,0,1,2,3,4}; the verifier enumerates every x,y in this fixture. A
+small final packet alone therefore cannot justify constant retained state in
+this access order. The theorem leaves interleaved reads and rereads open.
+
+## Exact packet variant
+
+If the output is the integer K rather than its high-modulus image, the same
+step argument applies over the integers. Equal r values have different b
+values whenever A is nonzero and x differs. Hence there are exactly q cut
+states for every A!=0, and one for A=0. This holds even at Q=1, where producing
+the high correction instead needs only one state. The two output contracts
+must not be conflated.
+
+## Relation to the predecessor
+
+Ali Romman's PR #5849 at `35ee8364ccfe54d6d5ec154fbf74993624b0a0d4`
+implements an original-owner runtime rotation from a supplied carry packet
+and explicitly leaves production from the low cache open. PR #5841 at
+`58a032ffafc2c5d08b8f53c2e98657b75c48379d` supplies its fused carry algebra.
+Those results and physical bounds are cited premises, not replayed or
+independently validated here. The scalar rational shear above isolates one
+packet-production boundary; it does not assert that every released G20 route
+uses this serialized access order or contains this precise scalar fixture.
+
+The state-equivalence argument is the standard deterministic one-way
+communication method. The contribution is its exact rational-carry quotient,
+including the nonunit-coefficient collapse and an attaining encoding.
+No claim is made to invent communication complexity or modular arithmetic.
+
+## Limits
+
+This is not a lower bound for arbitrary tape algorithms, interleaved access,
+multiple passes, early output, a previously computed low cache, or amortized
+production of several packets. The encoding is not a literal finite-tape
+program. Its computation, source access, erasure, routing and interaction with
+the complete caller remain unpaid. No selected saving, frontier or framework
+assumption changes, and no complete multiplication theorem is claimed.
diff --git a/research/quarter-carry-cut-states/README.md b/research/quarter-carry-cut-states/README.md
new file mode 100644
index 0000000000..b713823b00
--- /dev/null
+++ b/research/quarter-carry-cut-states/README.md
@@ -0,0 +1,116 @@
+# Exact retained state for serialized rational-shear carries
+
+Scoped written mathematical proof with finite corroboration, produced by Nick
+Petalas. No new kappa is claimed.
+
+A rational shear has source low digit x, later target low digit y, radix q,
+coefficient A/D and high modulus Q. If all of x must be read before any of y,
+with no reread or early output, the exact minimum number of distinguishable
+states after reading x is
+
+```text
+g = gcd(A,q),  d = q/g,  e = Q/gcd(A/g,Q)
+R = 1                    if Q=1
+R = d * min(g,e)         if Q>1
+```
+
+This counts all retained information, including controller and head state.
+It permits arbitrary lossless encodings. An explicit class label attains the
+bound. The domain is q>=2, Q>=1, arbitrary integer A, positive D and
+gcd(D,qQ)=1. [PROOF.md](PROOF.md) gives the exact output contract and proof.
+The result counts information at one cut, not total workspace or physical time.
+
+For a quarter shear, odd q>=3 and high width w>=2, R=q. At q=257 the verifier
+checks 257 distinct response functions and every pair of source/target digits.
+Nine binary bits are necessary at the cut although the integer carry takes
+only the eight values -3 through 4. A finite final packet does not by itself
+supply a constant-state producer in this access order. At w=1 the high
+correction is zero and needs one state. Producing the exact integer carry is
+a different contract: it needs q states whenever A is nonzero.
+
+## Connection and scope change
+
+Ali Romman's [PR #5849](https://github.com/CrocSwap/integer-mult-bounds/pull/5849)
+at `35ee8364ccfe54d6d5ec154fbf74993624b0a0d4` supplies a complete original-owner
+rotation from a caller-supplied packet and explicitly leaves its production
+from the low cache open. [PR #5841](https://github.com/CrocSwap/integer-mult-bounds/pull/5841)
+at `58a032ffafc2c5d08b8f53c2e98657b75c48379d` supplies the fused carry algebra.
+These predecessor results are cited, not audited or replayed here. Their
+runtime programs are not imported and their physical costs are not recertified.
+
+The `bit-helper-contract` card is changed from a new helper/target moment
+improvement to a sharp information obligation for one explicit carry-producer
+interface. This helps decide whether a proposed serialized cache layout can
+produce its packet with constant retained state. It does not assert that the
+released G20 word uses this layout, or instantiate this scalar quarter-shear
+fixture as one of its actual ports. The selected frontier is unchanged.
+
+## Reproduce
+
+From the repository root, using the local interpreter:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/quarter-carry-cut-states/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -O -B research/quarter-carry-cut-states/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/quarter-carry-cut-states
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/quarter-carry-cut-states --check-source-history
+```
+
+Any CPython 3.12 interpreter can replace that local path. Only the standard
+library is needed. Normal and optimized checks print
+`PASS_QUARTER_CARRY_CUT_STATES` inside a generated JSON receipt bound to all six
+package files. No receipt is handwritten or stored as an authoritative result.
+
+The verifier enumerates all admissible q=2..25, Q=1..16, A=-24..24, D=1..8
+systems, plus every odd q=3..65 and w=1..6 for the quarter corollary and the
+complete q=257,w=2 fixture. Its independent oracle applies the rational shear
+directly modulo qQ and extracts the high digit. It compares every response,
+checks every attaining label, counts the integer-packet response classes, and
+constructs a separating target digit for every pair in the q=257 fixture.
+Nonunit collapse, zero coefficient, negative coefficient, Q=1, invalid input
+and incorrect constant-packet interpretations have explicit controls.
+
+The default replay is read-only and Git-free. Git is required only by the
+repository's provenance and publication preflights. [SOURCES.json](SOURCES.json)
+pins the catalogue and selected record as historical provenance at the base
+commit. The predecessor links are scholarly context, not executable inputs or
+unmerged Git-history dependencies.
+
+## Limits and implementation checks
+
+No literal tape producer, complete cache layout, source admission, erasure,
+routing, native caller, precision/stock or all-size multiplication theorem is
+proved. All five selected framework assumptions remain. Interleaved access,
+source rereads, early output, precomputed cache summaries and amortized joint
+packet production are outside the lower bound. Human and formal proof-kernel
+review are unclaimed.
+
+The verifier has fixed finite census loops, no recursion and explicit
+parameter/radix limits. Python allocates dynamically, a managed-runtime
+Power-of-Ten deviation. At most O(257^2) response entries are live, and parameter
+integers have at most 4096 bits. The proof itself has no such finite bound.
+Warning-strict normal/optimized execution and in-memory compilation supply the
+available language diagnostics. No separate static type checker is installed on PATH.
+Checks use explicit exceptions and remain active under optimization.
+
+## Open next questions
+
+1. Can a concrete low-cache layout interleave the relevant source and target
+   digits and avoid this serialized-cut storage? This determines whether the
+   obstruction applies to an actual packet producer. Start with one explicitly
+   ordered pair of low-digit streams and charge every reread and erasure.
+   A literal caller/cache layout is the blocker.
+2. What is the joint cut-state count when one retained source digit serves
+   several rational-shear packets? Shared information could make separate
+   per-packet charges too large. Start by quotienting the tuple of two response
+   functions. A declared joint output and access contract is needed.
+
+## Credit
+
+New proof and verifier produced by Nick Petalas. Credit Ali Romman for the
+PR #5849 packet-production question and PR #5841 fused carry contract,
+JoyboyBrian for the retained descriptor/affine-shear work, Tekalign for the
+carry-stream predecessors, and the retained ROW/native/tape contributors.
+The state-equivalence proof uses the classical deterministic one-way
+communication method; modular arithmetic and that method are not claimed as
+new. New material is Apache-2.0. No predecessor files or credit lines change.
diff --git a/research/quarter-carry-cut-states/SOURCES.json b/research/quarter-carry-cut-states/SOURCES.json
new file mode 100644
index 0000000000..05516caf4b
--- /dev/null
+++ b/research/quarter-carry-cut-states/SOURCES.json
@@ -0,0 +1,32 @@
+{
+  "schema_version": 1,
+  "base_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8",
+      "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    }
+  ],
+  "cited_predecessors": [
+    {
+      "pr": 5849,
+      "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/5849",
+      "commit": "35ee8364ccfe54d6d5ec154fbf74993624b0a0d4",
+      "usage": "Scholarly context only; packet-production question, not a runtime input."
+    },
+    {
+      "pr": 5841,
+      "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/5841",
+      "commit": "58a032ffafc2c5d08b8f53c2e98657b75c48379d",
+      "usage": "Scholarly context only; fused carry algebra, not a runtime input."
+    }
+  ]
+}
diff --git a/research/quarter-carry-cut-states/TASK.json b/research/quarter-carry-cut-states/TASK.json
new file mode 100644
index 0000000000..6678e1293f
--- /dev/null
+++ b/research/quarter-carry-cut-states/TASK.json
@@ -0,0 +1,83 @@
+{
+  "schema_version": 1,
+  "task_id": "bit-helper-contract",
+  "priority_revision": 8,
+  "base_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a",
+  "original_card": {
+    "id": "bit-helper-contract",
+    "question": "Can a changed G20 helper path or independent-target split improve the complete BIT moment without losing its physical endpoint?",
+    "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",
+      "research/g20-helper-split/README.md",
+      "research/g20-conjugation-admission/README.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 full boundary contract and paid profile; unchanged scalar counts alone are insufficient. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.",
+    "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": "First read #5679/#5708 and their audits as pending component proposals. Choose one uncovered helper group/cut on an exact word; compare arbitrary-input native action, targets, owned storage, both orientations and full signed bill. Stop if the gain is only a scalar count or repaid by lost targets. Do not rerun the frozen #5609 common-frame domain without changing its hypothesis.",
+    "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": [
+      "G20",
+      "helper split",
+      "5679",
+      "5708",
+      "independent target"
+    ],
+    "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": "Exact retained-state count for a serialized rational-shear carry producer, including nonunit coefficients and an attaining cut encoding.",
+  "scope_change_reason": "The helper-moment card is changed to the unfilled low-cache packet-production boundary in PR5849, with an explicit source-before-target access order.",
+  "bottleneck_link": "A finite final packet alphabet does not price the information retained by its producer. This sharp boundary can reject constant-state serialized layouts without claiming a BIT moment improvement.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop at the first verified original cut-state formula; leave interleaved and joint-cache questions open.",
+  "outcome": "completed",
+  "evidence": "PROOF.md and read-only verify.py; runtime receipts enumerate every finite check and bind package hashes.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Can an actual low-cache layout interleave the two low-digit streams to avoid serialized-cut storage?",
+      "why_it_matters": "Determines applicability to a physical packet producer.",
+      "first_step": "Specify one ordered pair of low-digit streams and charge reads and erasure.",
+      "blocked_by": "No literal caller/cache layout is supplied."
+    },
+    {
+      "question": "What is the exact joint cut-state count for two carry packets sharing one retained source digit?",
+      "why_it_matters": "Separate per-packet storage charges can overcount shared information.",
+      "first_step": "Quotient the tuple of two response functions under an explicit access order.",
+      "blocked_by": "A joint output and cache-access contract must be fixed."
+    }
+  ]
+}
diff --git a/research/quarter-carry-cut-states/VERIFY.json b/research/quarter-carry-cut-states/VERIFY.json
new file mode 100644
index 0000000000..d866f71311
--- /dev/null
+++ b/research/quarter-carry-cut-states/VERIFY.json
@@ -0,0 +1,32 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 300,
+      "checks": "Complete declared modular-response census, exact class count and attaining encoding, quarter family, pair separators and rejection controls."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-W",
+        "error",
+        "-O",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 300,
+      "checks": "The same mathematical and boundary checks with Python assertions disabled."
+    }
+  ]
+}
diff --git a/research/quarter-carry-cut-states/verify.py b/research/quarter-carry-cut-states/verify.py
new file mode 100644
index 0000000000..f5fcadf068
--- /dev/null
+++ b/research/quarter-carry-cut-states/verify.py
@@ -0,0 +1,228 @@
+#!/usr/bin/env python3
+"""Exact rational-carry cut classes, produced by Nick Petalas. Apache-2.0."""
+
+from dataclasses import dataclass
+import hashlib
+import json
+from math import gcd
+from pathlib import Path
+
+
+def need(condition: bool, message: str) -> None:
+    if not condition:
+        raise ValueError(message)
+
+
+@dataclass(frozen=True)
+class Problem:
+    q: int
+    high: int
+    numerator: int
+    denominator: int
+
+    def __post_init__(self) -> None:
+        values = (self.q, self.high, self.numerator, self.denominator)
+        need(all(type(v) is int for v in values), "integer parameters required")
+        need(all(v.bit_length() <= 4096 for v in values), "parameter bit limit")
+        need(self.q >= 2 and self.high >= 1, "invalid modulus")
+        need(self.denominator >= 1, "positive denominator required")
+        need(gcd(self.denominator, self.q * self.high) == 1, "denominator not a unit")
+
+
+def parameters(p: Problem) -> tuple[int, int, int, int]:
+    g = gcd(p.numerator, p.q)
+    d = p.q // g
+    e = p.high // gcd(p.numerator // g, p.high)
+    return g, d, e, min(g, e)
+
+
+def count(p: Problem) -> int:
+    if p.high == 1:
+        return 1
+    _, d, _, m = parameters(p)
+    return d * m
+
+
+def encode(p: Problem, x: int) -> int:
+    need(type(x) is int and 0 <= x < p.q, "source digit out of range")
+    if p.high == 1:
+        return 0
+    _, d, e, m = parameters(p)
+    return (x % d) * m + (x // d) % e
+
+
+def representative(p: Problem, label: int) -> int:
+    need(type(label) is int and 0 <= label < count(p), "label out of range")
+    if p.high == 1:
+        return 0
+    _, d, _, m = parameters(p)
+    return label // m + (label % m) * d
+
+
+def integer_packet(p: Problem, x: int, y: int) -> int:
+    need(0 <= x < p.q and 0 <= y < p.q, "digit out of range")
+    t = (y + p.numerator * pow(p.denominator, -1, p.q) * x) % p.q
+    n = p.numerator * x + p.denominator * (y - t)
+    need(n % p.q == 0, "nonintegral carry")
+    return n // p.q
+
+
+def step_response(p: Problem, x: int, y: int) -> int:
+    packet = integer_packet(p, x, y)
+    return packet * pow(p.denominator, -1, p.high) % p.high
+
+
+def full_modulus_response(p: Problem, x: int, y: int) -> int:
+    modulus = p.q * p.high
+    output = (y + p.numerator * x * pow(p.denominator, -1, modulus)) % modulus
+    return output // p.q
+
+
+def distinguish(p: Problem, x: int, other: int) -> int:
+    need(p.high > 1 and encode(p, x) != encode(p, other), "equivalent sources")
+    if full_modulus_response(p, x, 0) != full_modulus_response(p, other, 0):
+        return 0
+    inverse = pow(p.denominator, -1, p.q)
+    r = p.numerator * x * inverse % p.q
+    other_r = p.numerator * other * inverse % p.q
+    need(r != other_r, "equal thresholds must have unequal constants")
+    y = p.q - max(r, other_r)
+    need(0 < y < p.q, "invalid threshold witness")
+    need(full_modulus_response(p, x, y) != full_modulus_response(p, other, y),
+         "threshold witness did not separate responses")
+    return y
+
+
+def check_problem(p: Problem, stats: dict[str, int], digest) -> None:
+    need(p.q <= 257, "enumeration radix limit")
+    signatures = []
+    packets = set()
+    labels = set()
+    for x in range(p.q):
+        label = encode(p, x)
+        labels.add(label)
+        rep = representative(p, label)
+        need(0 <= rep < p.q, "invalid representative")
+        row = []
+        packet_row = []
+        for y in range(p.q):
+            value = full_modulus_response(p, x, y)
+            need(value == step_response(p, x, y), "full-width oracle disagrees")
+            need(value == full_modulus_response(p, rep, y), "encoding loses information")
+            row.append(value)
+            packet_row.append(integer_packet(p, x, y))
+            stats["digit_pairs"] += 1
+        signatures.append(tuple(row))
+        packets.add(tuple(packet_row))
+    need(len(set(signatures)) == count(p), "incorrect class count")
+    need(labels == set(range(count(p))), "encoding is not onto")
+    need(len(packets) == (1 if p.numerator == 0 else p.q), "packet count")
+    digest.update(str((p, tuple(sorted(labels)), len(packets))).encode())
+    stats["systems"] += 1
+
+
+def complete_small_domain(stats: dict[str, int], digest) -> None:
+    for q in range(2, 26):
+        for high in range(1, 17):
+            for numerator in range(-24, 25):
+                for denominator in range(1, 9):
+                    if gcd(denominator, q * high) != 1:
+                        continue
+                    check_problem(Problem(q, high, numerator, denominator), stats, digest)
+
+
+def quarter_family(stats: dict[str, int], digest) -> None:
+    for q in range(3, 66, 2):
+        for width in range(1, 7):
+            p = Problem(q, q ** (width - 1), 1, 4)
+            need(count(p) == (1 if width == 1 else q), "quarter corollary")
+            check_problem(p, stats, digest)
+            stats["quarter_systems"] += 1
+    p = Problem(257, 257, 1, 4)
+    check_problem(p, stats, digest)
+    codes = {integer_packet(p, x, y) for x in range(p.q) for y in range(p.q)}
+    need(codes == set(range(-3, 5)), "quarter packet alphabet")
+    need((count(p) - 1).bit_length() == 9, "quarter bit count")
+    for x in range(p.q):
+        for other in range(x):
+            y = distinguish(p, x, other)
+            need(full_modulus_response(p, x, y) != full_modulus_response(p, other, y),
+                 "bad pair separator")
+            stats["quarter_separators"] += 1
+
+
+def nonunit_and_collapse_controls(stats: dict[str, int]) -> None:
+    fixtures = [(9, 3, 9, 1, 3), (9, 9, 27, 4, 3), (12, 4, 24, 5, 2),
+                (15, 3, 5, 2, 9), (8, 2, 8, 3, 2), (8, 1, 1, 3, 1),
+                (9, 9, 0, 4, 1), (6, 5, -12, 7, 5)]
+    for q, high, a, d, expected in fixtures:
+        p = Problem(q, high, a, d)
+        actual = len({tuple(full_modulus_response(p, x, y) for y in range(q))
+                      for x in range(q)})
+        need(actual == expected == count(p), "collapse fixture")
+        stats["collapse_controls"] += 1
+
+
+def rejection_controls(stats: dict[str, int]) -> None:
+    invalid = [(1, 3, 1, 4), (3, 0, 1, 4), (3, 3, 1, 0),
+               (3, 3, 1, 3), (3, 2, 1, 4), (True, 3, 1, 4),
+               (3, 3, 1.0, 4), (3, 3, 1 << 4096, 4)]
+    for args in invalid:
+        try:
+            Problem(*args)
+        except ValueError:
+            stats["invalid_inputs_rejected"] += 1
+        else:
+            raise ValueError("invalid input accepted")
+    p = Problem(17, 17, 1, 4)
+    for bad in (-1, p.q, True):
+        try:
+            encode(p, bad)
+        except ValueError:
+            stats["invalid_inputs_rejected"] += 1
+        else:
+            raise ValueError("invalid source accepted")
+    for bad in (-1, count(p), True):
+        try:
+            representative(p, bad)
+        except ValueError:
+            stats["invalid_inputs_rejected"] += 1
+        else:
+            raise ValueError("invalid label accepted")
+
+
+def semantic_controls(stats: dict[str, int]) -> None:
+    p = Problem(17, 17, 1, 4)
+    need(full_modulus_response(p, 0, 0) != full_modulus_response(p, 1, 0),
+         "constant-code mutant survived")
+    need(count(p) > 8, "final packet alphabet mistaken for cut states")
+    need(full_modulus_response(p, 1, 16) != full_modulus_response(p, 0, 16),
+         "stale-source mutant survived")
+    collapsed = Problem(9, 3, 9, 1)
+    need(count(collapsed) != collapsed.q, "nonunit no-collapse mutant survived")
+    trivial = Problem(17, 1, 1, 4)
+    need(count(trivial) != trivial.q, "Q=1 mutant survived")
+    need(integer_packet(trivial, 1, 0) != integer_packet(trivial, 0, 0),
+         "integer packet conflated with high correction")
+    stats["semantic_controls"] += 6
+
+
+def main() -> None:
+    stats = dict.fromkeys(("systems", "digit_pairs", "quarter_systems",
+                          "quarter_separators", "collapse_controls",
+                          "invalid_inputs_rejected", "semantic_controls"), 0)
+    digest = hashlib.sha256()
+    complete_small_domain(stats, digest)
+    quarter_family(stats, digest)
+    nonunit_and_collapse_controls(stats)
+    rejection_controls(stats)
+    semantic_controls(stats)
+    package = Path(__file__).resolve().parent
+    names = ("README.md", "PROOF.md", "TASK.json", "SOURCES.json", "VERIFY.json", "verify.py")
+    hashes = {name: hashlib.sha256((package / name).read_bytes()).hexdigest() for name in names}
+    print(json.dumps({"status": "PASS_QUARTER_CARRY_CUT_STATES", "coverage": stats,
+                      "census_sha256": digest.hexdigest(), "package_sha256": hashes}, sort_keys=True))
+
+
+if __name__ == "__main__":
+    main()