diff --git a/research/unequal-gain-cycle-optimum/README.md b/research/unequal-gain-cycle-optimum/README.md
new file mode 100644
index 0000000000..fefe3c2aa6
--- /dev/null
+++ b/research/unequal-gain-cycle-optimum/README.md
@@ -0,0 +1,221 @@
+# Equal gains uniquely minimize cycle conditioning at fixed product
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+Let `W>=2`, `d>=1`, and let `U_0,...,U_(W-1)` be arbitrary complex unitary
+`d x d` matrices. For positive real gains `g_j` with geometric mean
+`r=(product_j g_j)^(1/W)` in `(0,1)`, define
+
+\[
+ (T_gx)_j=g_jU_jx_{j+1\bmod W},\qquad A_g=I+T_g.
+\]
+
+In the ordinary, unweighted Euclidean norm,
+
+\[
+ \boxed{\kappa_2(A_g)\ \geq\ \kappa_2(A_r),
+ \qquad\text{equality if and only if every }g_j=r.}
+\]
+
+Here `A_r` uses the **same unitary edges**, with every gain replaced by `r`.
+Thus unequal positive gains cannot improve conditioning, even before the
+unitary edges are optimized. Individual gains may exceed one.
+
+This is a **scoped algebraic proof**, with exact finite corroboration. It
+settles the fixed-product algebraic part of the nonuniform-gain question
+left by [PR #4880](https://github.com/CrocSwap/integer-mult-bounds/pull/4880).
+That predecessor proves the equal-gain optimum and is cited as a premise,
+not audited or replayed here. No new supplier, kappa or multiplication
+theorem is claimed.
+
+## Sharp fixed-product optimum
+
+Put `a=1+r^2`, `b=2r`, `c=cos(pi/W)`, and `H=U_0...U_(W-1)`.
+Combining the new comparison with #4880 gives
+
+\[
+ \min_{\substack{g_j>0,\ \prod g_j=r^W\\ U_j\text{ unitary}}}
+ \kappa_2(A_g)=
+ \begin{cases}
+ \sqrt{(a+bc)/(a-bc)},&W\text{ even},\\
+ (1+r)/\sqrt{a-bc},&W\text{ odd}.
+ \end{cases}
+\]
+
+Equality holds exactly when every gain equals `r` and
+`H=(-1)^(W+1) I_d`. The numerical formula and the ordered-product criterion
+on this equal-gain locus belong to #4880. The new step is that no nonuniform
+positive gain vector can attain or beat them. At three banks and product
+`1/8`, the exact optimum remains `sqrt(3)`; every unequal gain vector has a
+strictly larger condition number, whatever its unitary couplings.
+
+This fixes the product, rather than the arithmetic mean or a physical gain
+tariff. It does not compute the exact optimum for a prescribed unequal vector.
+
+## Proof of the strict comparison
+
+### Positive diagonal similarity preserves the spectrum
+
+Set `D_0=1` and `D_(j+1)=r D_j/g_j` for `0<=j<W-1`. Regard `D` as the block
+diagonal matrix with blocks `D_j I_d`. All blocks are positive. The product
+constraint gives `g_(W-1)=r D_(W-1)/D_0`, so the closing edge satisfies the
+same identity as every other edge. Direct substitution yields
+
+\[
+ T_g=D(rS)D^{-1},\qquad A_g=D(I+rS)D^{-1}=DA_rD^{-1},
+ \qquad (Sx)_j=U_jx_{j+1}.
+\]
+
+The operator `S` is unitary. Hence `A_r` is normal, every eigenvalue `z` of
+`T_g` has modulus `r`, and every eigenvalue `1+z` of `A_g` is nonzero.
+In particular all matrices in the statement are invertible, even when an
+individual gain exceeds one.
+
+Let `M` and `m` be the largest and smallest eigenvalue moduli of `A_g`.
+The normal matrix `A_r` has the same spectrum, so
+`kappa_2(A_r)=M/m`. The spectral-radius inequalities give
+
+\[
+ \|A_g\|_2\geq M,\qquad \|A_g^{-1}\|_2\geq 1/m.
+\]
+
+Their product proves the non-strict comparison. This uses similarity only
+to identify eigenvalues; it does not assume similarity preserves Euclidean
+singular values.
+
+### Equality forces all gains to agree
+
+Suppose the condition numbers agree. Each of the preceding inequalities has
+a positive right side, so equality of their product forces `||A_g||_2=M`.
+Choose a nonzero eigenvector `x` of `T_g` with eigenvalue `z` for which
+`lambda=1+z` has modulus `M`. Then `A_g x=lambda x` attains the operator
+norm, so
+
+\[
+ A_g^*A_gx=M^2x,
+ \qquad A_g^*x=\overline\lambda x,
+ \qquad T_g^*x=\overline z x.
+\]
+
+The middle identity follows by dividing the first by the nonzero `lambda`.
+Consequently `T_g^*T_gx=r^2x`. But direct block multiplication gives
+
+\[
+ T_g^*T_g=\operatorname{diag}
+ (g_{W-1}^2I_d,g_0^2I_d,\ldots,g_{W-2}^2I_d).
+\]
+
+Every block `x_j` is nonzero. Indeed `g_jU_jx_(j+1)=z x_j`, and `g_j>0`,
+`z!=0` and invertibility of every `U_j` propagate a zero block around the
+whole cycle, contradicting `x!=0`. The diagonal identity therefore forces
+`g_j^2=r^2` for every `j`. Positivity gives `g_j=r`. Conversely those gains
+make `A_g=A_r`, proving the equality statement.
+
+The corollary now follows from #4880's equal-gain theorem. Its attaining
+closing edge remains available, so the minimum is achieved in every `d`.
+The spectral-radius and norm-attainment tools are classical; no literature
+priority for those methods is asserted.
+
+## Exact finite evidence
+
+The standalone verifier constructs literal rational matrices, with no
+predecessor imports or scientific replays. Its fixed domain has
+`W in {2,3,4,5,7}`, `d in {1,2}`, `r in {1/3,1/2}`, two signed scalar edge
+products, and two rational orthogonal bank-gauge families. One matrix family
+has a noncentral ordered product. The dimension-two cases include
+noncommuting edges and nonmonomial rational orthogonal matrices.
+
+For each edge tuple it checks three gain profiles `g_j=r 2^(e_j)`:
+all exponents zero, `(1,-1,0,...)`, and `(2,0,...,-2)`. It checks exact
+diagonal similarity, both weighted-shift Gram diagonals, and normality of
+the uniform comparator. Independent rational positive-definiteness tests
+enclose both extreme eigenvalues of each literal Gram matrix. The resulting
+condition-ratio brackets are strictly separated for every nonuniform fixture.
+The global sharp formula is not numerically retested as the deliverable.
+
+The generated receipt enumerates 120 literal cycles, 80 strict gaps and 40
+uniform controls, including 54 cycles with noncommuting edges and 40 with
+a gain above one. Thirteen named boundary controls cover invalid gains,
+product, mean, bank count, shape and unitarity, a reversed similarity gauge,
+singular and indefinite pivots, and two changes of contract.
+
+In the same-spectrum exhibit, `A=[[1,1],[-1/4,1]]` has the uniform comparator's
+eigenvalues but a nonscalar Euclidean Gram matrix satisfying
+`det(tI-A^T A)=(16t^2-49t+25)/16`. In the changed-metric exhibit, its diagonal weighted
+bank norm makes it a scaled isometry. This shows why the unweighted Euclidean
+norm and the distinction between eigenvalues and singular values matter.
+
+The arbitrary-width, arbitrary-complex theorem rests on the written proof.
+Finite rational comparisons corroborate it within the enumerated domain.
+Receipts come from the verifier and bind all five package files by SHA256;
+none is hand-written or retained as a generated checkout output.
+
+## Reproduce
+
+From the repository root, using only the Python standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/unequal-gain-cycle-optimum/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/unequal-gain-cycle-optimum/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/unequal-gain-cycle-optimum
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/unequal-gain-cycle-optimum --check-source-history
+```
+
+Other hosts may substitute any CPython 3.12 interpreter. The direct marker is
+`PASS_UNEQUAL_GAIN_CYCLE_OPTIMUM`. Redirect stdout outside the checkout to retain
+the generated receipt. The registered normal and optimized commands run every
+fixture and control; scientific checks use explicit exceptions.
+
+The selected source-binding orientation passed on canonical main
+`de5ec2e7a6074068452f45b1a191b5c72832df4a`, priority revision 8, after its
+omitted inputs were materialized with the sparse helper. That command is
+metadata orientation, not a supplier replay. The original formal-interface
+card is explicitly changed to a written algebraic theorem rather than a
+proof-assistant formalization or predecessor audit. TASK.json records this
+scope and the [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19213514).
+
+## Attribution and limitations
+
+Credit Nick Petalas #4880 for the equal-gain theorem and open nonuniform
+question. Chris R / Clear1nsight #4842 supplies the complete-cascade context;
+hexapode #4818/#4819/#4826 supplies the proposed schedules. The retained
+construction lineage includes Dugongue #4743, Yiyang / Lyy-iiis #4710,
+lee-phys #4688 and Jacob Alan Sussman #4628. William Lawyer #852 studies
+balanced weighted-cycle inverses in the infinity norm under local weight caps;
+it is a different contract and is not replayed or contradicted here.
+All predecessor credit and source notices remain unchanged by citation.
+
+The theorem assumes scalar positive gains, unitary edge factors, one directed
+cycle and unweighted Euclidean bank norms, with geometric mean strictly below
+one. Nonunitary factors, zero gains, singular mean-one cases, changed graphs
+and other norms are excluded. No quantitative uniform gap away from equal
+gains or exact optimum for a prescribed unequal vector is supplied.
+
+Native emission of changed gains/couplings, arbitrary dirty-bank ownership and
+restoration, independent targets, normalization, intermediate amplification,
+complete caller costs, stock, compiler, physical tape, rounding and analytic
+recovery remain unpriced. A diagonal similarity is not a free physical
+normalization. No family construction expansion or selected-frontier change
+follows. Lean, Docker, predecessor scientific suites and the selected complete
+cold replay are unrun. Independent human and formal proof-kernel review are
+unclaimed.
+
+Power-of-ten inspection: no recursion; all scientific loops have fixed finite
+domains, matrices have at most 14 rows and each root bracket uses exactly 24
+iterations. Functions stay below 60 physical lines. Python fractions and
+collections allocate dynamically, a managed-runtime deviation; fixed rational
+inputs and bounded matrix sizes bound live data. The rejection helper's only
+indirect targets are the two named local functions `cycle` and
+`check_similarity`. Warning-strict ordinary and optimized replay are registered.
+No package verifier writes files or launches processes.
+
+## Open next questions
+
+- Can one physical three-bank native word realize the attaining closing
+  product while retaining arbitrary input banks and every independent target?
+  Start with one literal caller and its full paid invoice. Native compatibility,
+  ownership and restoration costs are the blockers.
+- For one prescribed nonuniform gain vector, what is the exact optimum over
+  unitary couplings? Start with a priced two- or three-bank vector and a full
+  singular-value calculation. The present fixed-product theorem gives strict
+  exclusion of the uniform benchmark, not that different optimum or its tariff.
diff --git a/research/unequal-gain-cycle-optimum/SOURCES.json b/research/unequal-gain-cycle-optimum/SOURCES.json
new file mode 100644
index 0000000000..7422b45fbd
--- /dev/null
+++ b/research/unequal-gain-cycle-optimum/SOURCES.json
@@ -0,0 +1,24 @@
+{
+  "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"
+    },
+    {
+      "path": "research/unitary-cycle-optimal-conditioning/README.md",
+      "usage": "provenance",
+      "git_blob": "a2f36e8bf5a313ea919ad4d3f9ef054d574be58c",
+      "sha256": "de0d5bf48f56e7666d9da8cbfa3c37ee823bc62e1b3b450b713e409b9370a574"
+    }
+  ]
+}
diff --git a/research/unequal-gain-cycle-optimum/TASK.json b/research/unequal-gain-cycle-optimum/TASK.json
new file mode 100644
index 0000000000..71ad865b81
--- /dev/null
+++ b/research/unequal-gain-cycle-optimum/TASK.json
@@ -0,0 +1,163 @@
+{
+  "schema_version": 1,
+  "task_id": "formal-interface-lemma",
+  "priority_revision": 8,
+  "base_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a",
+  "original_card": {
+    "id": "formal-interface-lemma",
+    "question": "Can one uncovered interface implication be formalized with exact caller and certificate bindings?",
+    "starting_points": [
+      "docs/research/research-family-status.md",
+      "certificates/selected-result.json",
+      "research/gate-operand-parity-lean/README.md",
+      "research/staged544-certified-endpoint/README.md",
+      "research/unconditional-batched-crt/README.md"
+    ],
+    "methods": [
+      "Formalize a missing boundary lemma identified by the selected review.",
+      "Audit a formal theorem-to-certificate binding independently."
+    ],
+    "acceptance_gate": "State the exact formalized proposition and remaining assumptions; avoid duplicate arithmetic formalizations already present.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_selected_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Resolve the current selected review, separate complex/ordinary BIT/admitted BIT/outer budgets, and compare the card against live handoffs before starting. Historical ceilings require exact source/model equivalence.",
+      "scope": "Source-binding orientation only; not a scientific replay or all-size proof. Materialize selected inputs if this checkout is sparse."
+    },
+    "first_experiment": "Write one missing statement with quantified hypotheses, actual caller and existing coverage. A compact-switch lemma is a candidate only after its mathematical contract is reviewed. Establish a bounded proof plan before a separately budgeted proof-assistant build; do not rerun large Lean jobs as orientation.",
+    "bottleneck_link": "A missing interface proof can reduce the conditional gap even if it does not change kappa.",
+    "allowed_variations": [
+      "Narrow to one formal lemma or one theorem-to-certificate binding."
+    ],
+    "scope_change_triggers": [
+      "Formalizing already-covered arithmetic and claiming the full multiplication theorem."
+    ],
+    "overlap_terms": [
+      "hyperplane end",
+      "formal interface",
+      "Lean binding",
+      "3807",
+      "3857",
+      "4100",
+      "gate-operand-parity-lean",
+      "staged544-certified-endpoint",
+      "unconditional-batched-crt"
+    ],
+    "existing_checks": [
+      {
+        "scope": "PR #3807: scoped gate-operand parity formalization.",
+        "evidence": "research/gate-operand-parity-lean/README.md",
+        "remaining": "Exact theorem-to-caller binding and genuinely uncovered interface lemmas.",
+        "status": "author-checked",
+        "source_commit": "4c3530f42a6abcc48e7a6bcffd6c901911dc8269",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "scope": "PR #3857: certified real-power moment/endpoint arithmetic.",
+        "evidence": "research/staged544-certified-endpoint/README.md",
+        "remaining": "Uniform algorithmic implications, not another endpoint digit.",
+        "status": "author-checked",
+        "source_commit": "ef4315b8caa605e47a2515004845eb2d2ed71a86",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "scope": "PR #4100: compact-switch formalization proposed as future validation.",
+        "evidence": "research/unconditional-batched-crt/README.md",
+        "remaining": "Audit the statement and assumptions before a formal proof campaign.",
+        "status": "author-checked",
+        "source_commit": "337d04939571a637aeab54a0f58f54fde811663a",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      }
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "For fixed unitary W-cycle edges and positive gains with geometric mean 0<r<1, prove Euclidean conditioning is strictly worse than uniform gain r unless all gains equal r; deduce the sharp fixed-product optimum and all equality cases.",
+  "scope_change_reason": "The selected formal-interface card is changed to a written algebraic boundary theorem rather than proof-assistant formalization or an audit. It answers the nonuniform-gain question left by PR4880 without replaying predecessor evidence.",
+  "bottleneck_link": "An observation-interface precision budget depends on complete Euclidean conditioning. Unequal scalar gains cannot beat the equal-gain optimum at fixed product; this removes a proposed algebraic escape, without pricing a physical caller.",
+  "budget_minutes": 60,
+  "stop_rule": "Package the first proved strict comparison; do not extend to new native words, prescribed-unequal-profile optima or quantitative gap optimization.",
+  "outcome": "completed",
+  "evidence": "README written proof for every W>=2 and d>=1 over complex unitary edges; independent literal rational Gram inequalities in verify.py.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Can one physical three-bank native word realize the attaining closing product while retaining every arbitrary input and independent target?",
+      "why_it_matters": "The fixed-product optimum is an algebraic design target; a physical supplier needs funded native emission and restoration.",
+      "first_step": "Fix one literal three-bank caller and emit its closing coupling with a complete paid invoice.",
+      "blocked_by": "Source-compatible native implementation, ownership and restoration costs are not supplied."
+    },
+    {
+      "question": "For one prescribed nonuniform gain vector, what is the exact optimum over unitary couplings?",
+      "why_it_matters": "The strict comparison excludes equality with the uniform benchmark but gives no exact nonuniform optimum.",
+      "first_step": "Fix a priced two- or three-bank gain vector and derive its complete singular-value optimization.",
+      "blocked_by": "The present theorem holds product fixed while allowing gains to vary, and does not solve this different optimization or its physical tariff."
+    }
+  ],
+  "verification_domain": {
+    "banks": [
+      2,
+      3,
+      4,
+      5,
+      7
+    ],
+    "internal_dimensions": [
+      1,
+      2
+    ],
+    "geometric_means": [
+      "1/3",
+      "1/2"
+    ],
+    "gain_exponents": [
+      [
+        0,
+        "..."
+      ],
+      [
+        1,
+        -1,
+        0,
+        "..."
+      ],
+      [
+        2,
+        0,
+        "...",
+        -2
+      ]
+    ],
+    "edge_families": "Two signed scalar products; rational orthogonal bank gauges with parity-optimal scalar and noncentral reflection products.",
+    "comparison": "24-step exact rational positive-definiteness enclosures of both Gram extremes, with disjoint condition-ratio brackets for every nonuniform fixture.",
+    "limits": "120 literal cycles, 80 strict comparisons, 40 uniform controls; no sampling claim for arbitrary complex widths."
+  },
+  "predecessors": [
+    {
+      "pr": 4880,
+      "author": "Nick Petalas",
+      "head": "dea483c4aa02a823dbdf351641382fbc1b2d62f6",
+      "use": "Cited equal-gain optimum and open nonuniform question. No predecessor verifier is imported or rerun."
+    },
+    {
+      "pr": 4842,
+      "author": "Chris R / Clear1nsight",
+      "head": "acd3384454083d4eb673343eb7762877d43e5394",
+      "use": "Cited complete-cascade context only."
+    },
+    {
+      "pr": 852,
+      "author": "William Lawyer",
+      "use": "Different infinity-norm balanced weighted-cycle inverse contract; not rechecked or imported."
+    }
+  ],
+  "overlap": {
+    "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19213514",
+    "priority_revision": 8,
+    "coverage": "405 open PRs and 5286 Discussion records in complete-paginated cached remote searches at 2026-10-27 09:03/09:04 UTC; live latest handoffs and active Discussions, 60 account PRs, local reservations, main-tree distinctive-term searches and merged PR searches. Sparse local-note coverage and arbitrary diffs are incomplete; unpublished work is outside coverage."
+  }
+}
diff --git a/research/unequal-gain-cycle-optimum/VERIFY.json b/research/unequal-gain-cycle-optimum/VERIFY.json
new file mode 100644
index 0000000000..1e1858bf84
--- /dev/null
+++ b/research/unequal-gain-cycle-optimum/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": "All literal rational similarity/Gram comparisons and 13 boundary controls."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-O",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "All literal rational similarity/Gram comparisons and 13 boundary controls with assertions disabled."
+    }
+  ]
+}
diff --git a/research/unequal-gain-cycle-optimum/verify.py b/research/unequal-gain-cycle-optimum/verify.py
new file mode 100644
index 0000000000..ff9c4a30df
--- /dev/null
+++ b/research/unequal-gain-cycle-optimum/verify.py
@@ -0,0 +1,284 @@
+"""Exact finite corroboration of the unequal-gain cycle theorem.
+
+Produced by Nick Petalas. Apache-2.0.
+The arbitrary-width theorem is the written proof, not these finite fixtures.
+"""
+
+import json
+from collections.abc import Callable
+from fractions import Fraction as Q
+from hashlib import sha256
+from itertools import product
+from pathlib import Path
+
+Matrix = tuple[tuple[Q, ...], ...]
+MAX_SIZE = 14
+BISECTION_STEPS = 24
+
+
+def require(condition: bool, message: str) -> None:
+    if not condition:
+        raise ValueError(message)
+
+
+def identity(n: int) -> Matrix:
+    require(1 <= n <= MAX_SIZE, "matrix size")
+    return tuple(tuple(Q(i == j) for j in range(n)) for i in range(n))
+
+
+def transpose(a: Matrix) -> Matrix:
+    return tuple(zip(*a, strict=True))
+
+
+def multiply(a: Matrix, b: Matrix) -> Matrix:
+    n = len(a)
+    require(1 <= n <= MAX_SIZE and len(b) == n, "matrix sizes")
+    columns = transpose(b)
+    return tuple(
+        tuple(
+            sum((x * y for x, y in zip(row, col, strict=True)), Q(0)) for col in columns
+        )
+        for row in a
+    )
+
+
+def validate(gains: tuple[Q, ...], edges: tuple[Matrix, ...], r: Q) -> None:
+    w = len(gains)
+    require(2 <= w <= 7 and len(edges) == w, "cycle size")
+    d = len(edges[0])
+    require(d in (1, 2) and w * d <= MAX_SIZE, "internal dimension")
+    require(0 < r < 1 and all(g > 0 for g in gains), "positive gains and mean")
+    gain_product = Q(1)
+    for gain in gains:
+        gain_product *= gain
+    require(gain_product == r**w, "fixed product")
+    for edge in edges:
+        require(len(edge) == d and all(len(row) == d for row in edge), "edge shape")
+        require(multiply(transpose(edge), edge) == identity(d), "unitary edge")
+
+
+def cycle(gains: tuple[Q, ...], edges: tuple[Matrix, ...], r: Q) -> Matrix:
+    validate(gains, edges, r)
+    w, d = len(gains), len(edges[0])
+    a = [list(row) for row in identity(w * d)]
+    for j, gain in enumerate(gains):
+        for row, col in product(range(d), repeat=2):
+            a[j * d + row][((j + 1) % w) * d + col] += gain * edges[j][row][col]
+    return tuple(tuple(row) for row in a)
+
+
+def gauge(gains: tuple[Q, ...], r: Q, d: int) -> tuple[Q, ...]:
+    weights = [Q(1)]
+    for gain in gains[:-1]:
+        weights.append(r * weights[-1] / gain)
+    require(r * weights[-1] == gains[-1], "closing gauge")
+    return tuple(weight for weight in weights for _ in range(d))
+
+
+def check_similarity(a: Matrix, b: Matrix, weights: tuple[Q, ...]) -> None:
+    n = len(a)
+    require(len(b) == n and len(weights) == n, "similarity sizes")
+    require(all(weights), "invertible gauge")
+    conjugated = tuple(
+        tuple(a[i][j] * weights[j] / weights[i] for j in range(n)) for i in range(n)
+    )
+    require(conjugated == b, "weighted-to-uniform similarity")
+
+
+def positive_definite(a: Matrix) -> bool:
+    """Exact Schur elimination; nonpositive pivots reject strict positivity."""
+    n = len(a)
+    require(1 <= n <= MAX_SIZE and a == transpose(a), "symmetric bounded matrix")
+    work = [list(row) for row in a]
+    for k in range(n):
+        pivot = work[k][k]
+        if pivot <= 0:
+            return False
+        for i in range(k + 1, n):
+            for j in range(i, n):
+                value = work[i][j] - work[i][k] * work[j][k] / pivot
+                work[i][j] = work[j][i] = value
+    return True
+
+
+def shift(a: Matrix, t: Q, sign: int) -> Matrix:
+    n = len(a)
+    return tuple(
+        tuple(sign * a[i][j] - (t if i == j else 0) for j in range(n)) for i in range(n)
+    )
+
+
+def extreme_bounds(a: Matrix) -> tuple[Q, Q, Q, Q]:
+    """Enclose both extremes of a positive Gram matrix by rational PD tests."""
+    gram = multiply(transpose(a), a)
+    require(positive_definite(gram), "invertible observation")
+    cap = 1 + max(sum(abs(value) for value in row) for row in gram)
+    min_lo, min_hi, max_lo, max_hi = Q(0), cap, Q(0), cap
+    for _ in range(BISECTION_STEPS):
+        mid = (min_lo + min_hi) / 2
+        if positive_definite(shift(gram, mid, 1)):
+            min_lo = mid
+        else:
+            min_hi = mid
+        mid = (max_lo + max_hi) / 2
+        if positive_definite(shift(gram, -mid, -1)):
+            max_hi = mid
+        else:
+            max_lo = mid
+    require(0 < min_lo <= min_hi < cap and 0 < max_lo <= max_hi, "root brackets")
+    return min_lo, min_hi, max_lo, max_hi
+
+
+def check_weight_diagonals(a: Matrix, gains: tuple[Q, ...], d: int) -> None:
+    n = len(a)
+    t = tuple(tuple(a[i][j] - Q(i == j) for j in range(n)) for i in range(n))
+    left, right = multiply(transpose(t), t), multiply(t, transpose(t))
+    expected_left = tuple(
+        tuple(
+            gains[(i // d - 1) % len(gains)] ** 2 if i == j else Q(0) for j in range(n)
+        )
+        for i in range(n)
+    )
+    expected_right = tuple(
+        tuple(gains[i // d] ** 2 if i == j else Q(0) for j in range(n))
+        for i in range(n)
+    )
+    require(left == expected_left and right == expected_right, "gain diagonals")
+    require((left == right) == (len(set(gains)) == 1), "normality equality")
+
+
+def edge_families(w: int) -> tuple[tuple[Matrix, ...], ...]:
+    sigma = Q((-1) ** (w + 1))
+    scalar = tuple(((Q(1),),) for _ in range(w - 1))
+    rotation = ((Q(3, 5), Q(-4, 5)), (Q(4, 5), Q(3, 5)))
+    reflection = ((Q(1), Q(0)), (Q(0), Q(-1)))
+    bases = tuple((identity(2), rotation, reflection)[j % 3] for j in range(w))
+    prefix = tuple(multiply(bases[j], transpose(bases[j + 1])) for j in range(w - 1))
+    closing = tuple(tuple(sigma * x for x in row) for row in bases[-1])
+    noncentral = multiply(bases[-1], reflection)
+    return (
+        scalar + (((sigma,),),),
+        scalar + (((-sigma,),),),
+        prefix + (closing,),
+        prefix + (noncentral,),
+    )
+
+
+def fixtures() -> dict[str, int]:
+    counts = {
+        "literal_cycles": 0,
+        "uniform_controls": 0,
+        "strict_gaps": 0,
+        "noncommuting_cycles": 0,
+        "gains_above_one": 0,
+    }
+    for w, r in product((2, 3, 4, 5, 7), (Q(1, 3), Q(1, 2))):
+        exponents = ((0,) * w, (1, -1) + (0,) * (w - 2), (2,) + (0,) * (w - 2) + (-2,))
+        for edges in edge_families(w):
+            d = len(edges[0])
+            b = cycle((r,) * w, edges, r)
+            require(
+                multiply(transpose(b), b) == multiply(b, transpose(b)),
+                "normal comparator",
+            )
+            b_min_lo, _, _, b_max_hi = extreme_bounds(b)
+            noncommuting = any(
+                multiply(x, y) != multiply(y, x) for x, y in product(edges, repeat=2)
+            )
+            for powers in exponents:
+                gains = tuple(r * Q(2) ** power for power in powers)
+                a = cycle(gains, edges, r)
+                check_similarity(a, b, gauge(gains, r, d))
+                check_weight_diagonals(a, gains, d)
+                counts["literal_cycles"] += 1
+                counts["noncommuting_cycles"] += int(noncommuting)
+                counts["gains_above_one"] += int(max(gains) > 1)
+                if len(set(gains)) == 1:
+                    require(a == b, "uniform attainment")
+                    counts["uniform_controls"] += 1
+                    continue
+                _, a_min_hi, a_max_lo, _ = extreme_bounds(a)
+                require(
+                    a_max_lo * b_min_lo > b_max_hi * a_min_hi,
+                    "strict condition gap from disjoint rational bounds",
+                )
+                counts["strict_gaps"] += 1
+    return counts
+
+
+def expect_rejection(action: Callable[..., object], args: tuple, label: str) -> None:
+    try:
+        action(*args)
+    except ValueError:
+        return
+    raise ValueError("control accepted: " + label)
+
+
+def controls() -> tuple[str, ...]:
+    r, edges = Q(1, 2), (((Q(1),),), ((Q(-1),),))
+    invalid = (
+        ("zero gain", cycle, ((Q(0), Q(1)), edges, r)),
+        ("negative gains", cycle, ((Q(-1), Q(-1, 4)), edges, r)),
+        ("wrong product", cycle, ((Q(1), Q(1, 2)), edges, r)),
+        ("zero mean", cycle, ((r, r), edges, Q(0))),
+        ("unit mean", cycle, ((r, r), edges, Q(1))),
+        ("one bank", cycle, ((r,), edges[:1], r)),
+        ("nonunitary", cycle, ((r, r), (((Q(2),),), edges[1]), r)),
+        ("wrong shape", cycle, ((r, r), (identity(2), edges[1]), r)),
+    )
+    for label, action, args in invalid:
+        expect_rejection(action, args, label)
+    gains = (Q(1), Q(1, 4))
+    a, b = cycle(gains, edges, r), cycle((r, r), edges, r)
+    expect_rejection(check_similarity, (a, b, (Q(1), Q(2))), "reversed gauge")
+    gram = multiply(transpose(a), a)
+    require(gram == ((Q(17, 16), Q(3, 4)), (Q(3, 4), Q(2))), "literal two-bank Gram")
+    require(gram[0][0] + gram[1][1] == Q(49, 16), "two-bank trace")
+    require(
+        gram[0][0] * gram[1][1] - gram[0][1] ** 2 == Q(25, 16), "two-bank determinant"
+    )
+    require(
+        gram != tuple(tuple(Q(5, 4) * x for x in row) for row in identity(2)),
+        "same spectrum does not preserve Euclidean conditioning",
+    )
+    weights = gauge(gains, r, 1)
+    metric = tuple(
+        tuple(1 / weights[i] ** 2 if i == j else Q(0) for j in range(2))
+        for i in range(2)
+    )
+    require(
+        multiply(transpose(a), multiply(metric, a))
+        == tuple(tuple(Q(5, 4) * x for x in row) for row in metric),
+        "bank-weighted norm is a different contract",
+    )
+    require(not positive_definite(((Q(1), Q(1)), (Q(1), Q(1)))), "singular pivot")
+    require(not positive_definite(((Q(1), Q(2)), (Q(2), Q(1)))), "indefinite pivot")
+    return tuple(row[0] for row in invalid) + (
+        "reversed gauge",
+        "same-spectrum exhibit",
+        "changed-metric exhibit",
+        "singular",
+        "indefinite",
+    )
+
+
+def main() -> None:
+    counts = fixtures()
+    labels = controls()
+    counts["boundary_controls"] = len(labels)
+    package = Path(__file__).resolve().parent
+    names = ("README.md", "SOURCES.json", "TASK.json", "VERIFY.json", "verify.py")
+    hashes = {name: sha256((package / name).read_bytes()).hexdigest() for name in names}
+    receipt = {
+        "status": "PASS_UNEQUAL_GAIN_CYCLE_OPTIMUM",
+        "claim_type": "scoped proof",
+        "finite_evidence": counts,
+        "control_labels": labels,
+        "bisection_steps": BISECTION_STEPS,
+        "source_sha256": hashes,
+    }
+    print(json.dumps(receipt, sort_keys=True, indent=2))
+
+
+if __name__ == "__main__":
+    main()