From 051b7ae23ff85d21e14bd6ce1791f7c28ff48053 Mon Sep 17 00:00:00 2001
From: JoyboyBrian <122925040+JoyboyBrian@users.noreply.github.com>
Date: Fri, 23 Oct 2026 05:48:56 -0700
Subject: [PATCH 1/2] Prove the exact two-call cost of the tied width-two
 transform

---
 .../PROOF.md                                  | 161 +++++++++++++++
 .../README.md                                 |  11 +
 .../RESULT.json                               |  24 +++
 .../SOURCES.json                              |  40 ++++
 .../TASK.json                                 |  95 +++++++++
 .../VERIFY.json                               |  21 ++
 .../engine-predecessor.md                     | 191 ++++++++++++++++++
 .../verify.py                                 |  64 ++++++
 8 files changed, 607 insertions(+)
 create mode 100644 research/tied-width-two-transform-exact-call-cost/PROOF.md
 create mode 100644 research/tied-width-two-transform-exact-call-cost/README.md
 create mode 100644 research/tied-width-two-transform-exact-call-cost/RESULT.json
 create mode 100644 research/tied-width-two-transform-exact-call-cost/SOURCES.json
 create mode 100644 research/tied-width-two-transform-exact-call-cost/TASK.json
 create mode 100644 research/tied-width-two-transform-exact-call-cost/VERIFY.json
 create mode 100644 research/tied-width-two-transform-exact-call-cost/engine-predecessor.md
 create mode 100644 research/tied-width-two-transform-exact-call-cost/verify.py

diff --git a/research/tied-width-two-transform-exact-call-cost/PROOF.md b/research/tied-width-two-transform-exact-call-cost/PROOF.md
new file mode 100644
index 0000000000..f3790121b6
--- /dev/null
+++ b/research/tied-width-two-transform-exact-call-cost/PROOF.md
@@ -0,0 +1,161 @@
+# Exact two-call cost at tied tensor width two
+
+## Source contract and statement
+
+Use the widened monomial game in Jacob Alan Sussman's PR4628 (head
+`ee4fd87f064017c23e5a86fc1dcfe0a5237caed3`, PROOF §§1–4). Put d=2^m,
+V=C^d, a=(1+i)/2, b=(1-i)/2, C_v=aI+bX_v. At the fixed width f=2,
+a paid call is C_v⊗C_v on one register. Free letters are B⊗B for monomial
+B on V; arbitrary finite complex scalar register mixing, copies and resets
+are free. There is one arbitrary input and finitely many zero helpers, all
+returned to zero. No independent-column letter is allowed.
+
+**Theorem.** For every m≥2, the exact paid-call cost of
+(C^⊗m)⊗(C^⊗m) is two. For m=1 it is one.
+
+This is a fixed-width result in the widened game, not the narrower affine
+engine, an all-width two-call program, an addition tariff, a dirty-helper
+return theorem or a physical supplier. PR5178 (Nick Petalas,
+`5fcfa050f2fc5445d7f0997206c5044b17f7e88f`) leaves the tied-column case open;
+its attaining individual-column permutations are not used here.
+
+## 1. The exact free algebra
+
+Write D for the span of d_i=e_i⊗e_i, S for the span of
+s_ij=e_i⊗e_j+e_j⊗e_i (i<j), and A for the span of
+a_ij=e_i⊗e_j−e_j⊗e_i. Then V⊗V=D⊕S⊕A. Every tied monomial preserves
+these three spaces. Let F be the linear span of tied monomials. It is an
+algebra, since their products are tied monomials. In fact
+
+    F = End(D) ⊕ End(S) ⊕ End(A).                 (1)
+
+Here is a finite legal synthesis, not an appeal to an arbitrary dense free
+map. For each address k, let Z_k be diagonal with entry i at k and 1
+elsewhere. On e_p⊗e_q, Z_k⊗Z_k has eigenvalue i^(δ_kp+δ_kq).
+For a weight w in {2e_p, e_p+e_q:p<q}, the operator
+
+    P_w = product_k [ (1/4) sum_(t=0)^3 i^(-t w_k)(Z_k^t⊗Z_k^t) ]
+
+projects onto the corresponding one-dimensional diagonal coordinate or
+ordered-pair two-space. This follows from the four-term character sum;
+all its letters are tied monomials. On the pair {p,q}, let τ exchange p,q.
+The operators P_(e_p+e_q)(I±τ⊗τ)/2 separately project onto s_pq and a_pq.
+Tied permutations take any diagonal coordinate to any other, or any pair
+coordinate to any other, with only a possible sign on A. Thus projector,
+permutation and scalar give every matrix unit on each of D,S,A separately.
+Their finite sums prove (1). All coefficients can be Gaussian rationals.
+
+A finite linear combination of free words can be executed with zero helpers:
+copy the input to one branch per summand, execute that word and scalar on its
+branch, sum into a separate accumulator, and reset branches. Products of such
+expressions are also finite free programs. This realizes (1) without treating
+a matrix unit as an additional primitive. The number of additions/helpers
+may grow rapidly with d and is not priced in this declared game.
+
+## 2. Gauge and cross-sector ranks
+
+Let H=[[1,1],[1,-1]] and D0=diag(1,-i). Then C=a D0 H D0.
+Tied diagonal maps and scalar multiplication therefore convert a paid call
+along the first bit into Q=W⊗W, where W is the unnormalized one-bit Walsh
+map, with independent pairs (2p,2p+1). They also convert the dense target
+into T=H_m⊗H_m, where (H_m)_(i,x)=(-1)^(i·x). These are invertible free
+pre/post gauges, so call cost is unchanged.
+
+Both Q and T commute with the tensor swap. Consequently their only
+cross-sector blocks among D,S,A are D→S and S→D. Put r=d/2 and let E_p
+be the S coordinate for {2p,2p+1}. Direct expansion gives
+
+    Q_SD d_(2p)=E_p,       Q_SD d_(2p+1)=−E_p,
+    Q_DS E_p=2(d_(2p)−d_(2p+1)),
+
+with Q_SD zero on no other D coordinates and Q_DS zero on all other S
+coordinates. Thus both cross-sector ranks equal r.
+
+For each nonzero binary address w, let u_w in S have coefficient1 on
+pairs {i,j} with i XOR j=w and 0 elsewhere. Let v_w be the row on D
+with v_w(x)=(-1)^(w·x). Then
+
+    T_SD = sum_(w≠0) u_w v_w,
+    T_DS = 2 sum_(w≠0) v_w^T u_w^T.               (2)
+
+The u_w have nonempty disjoint supports, and the Walsh rows v_w are linearly
+independent (H_m H_m^T=dI). Hence both ranks are d−1.
+
+## 3. Lower bound with any finite clean scratch
+
+A zero-call program has input-output operator in F. Before a unique paid
+call, every register contains an F-operator applied to the original input.
+After that call every register is a sum of an F-operator on the input and
+an F-operator applied to the called register. Thus any one-call endpoint is
+
+    F0 + L Q R,       F0,L,R in F.                (3)
+
+This remains valid with arbitrary singular mixing, copies and resets, any
+finite number of helpers, and a call on any helper. It follows by induction
+on the chronological straight-line steps, not by replacing one call with an
+arbitrary sum of unrelated double-coset terms.
+
+By (1), the SD block of (3) is L_S Q_SD R_D and has rank at most d/2.
+The target rank is d−1, strictly larger for d≥4. At least two calls are
+therefore necessary. For d=2 the target is the single call, and its nonzero
+SD block excludes zero calls.
+
+## 4. A literal two-call factorization for every m≥2
+
+Partition the d−1 nonzero addresses into W1,W2, each of size at most r.
+For each t, assign its addresses w to distinct indices p=0,...,|Wt|−1.
+Define block-diagonal free-algebra maps L_t,R_t by the following entries,
+setting all unspecified entries and their A blocks to zero:
+
+    (L_t)_S E_p = u_w,
+    row_(2p) ((R_t)_D) = v_w,
+    column_(2p) ((L_t)_D) = v_w^T,
+    row_(E_p) ((R_t)_S) = u_w^T.
+
+In particular the odd D rows of R_t and odd D columns of L_t vanish.
+Using the two explicit blocks of Q gives
+
+    (L_t Q R_t)_SD = sum_(w in Wt) u_w v_w,
+    (L_t Q R_t)_DS = 2 sum_(w in Wt) v_w^T u_w^T.
+
+All other cross-sector blocks vanish. Therefore
+
+    F0 := T−L1 Q R1−L2 Q R2
+
+is block diagonal and belongs to F by (1). This proves the exact identity
+T=F0+L1QR1+L2QR2, with two actual occurrences of Q, rather than mere
+membership in span(FQF).
+
+Keep a saved original input. Prepare R1x and R2x in separate zero banks
+using the finite free synthesis of §1, apply one paid call (with its free
+gauges) to each, and apply L1,L2. Form F0x freely, add the three outputs,
+copy the result into the input register, and reset every helper, including
+the saved input. Since only zero helpers were promised, these resets are
+legal. The endpoint is exact on every input and consumes exactly two calls.
+Undo the target gauge to obtain the stated C target. No ability to reset
+arbitrary dirty data is inferred.
+
+## Evidence and limits
+
+The universal theorem rests on the finite character-projector synthesis,
+one-call normal form and explicit all-d block factorization above. Small
+exact replay checks the complete operator in the original ordered tensor
+basis, the free-sector synthesis and hypothesis-removal controls. It is not
+an exhaustive program search. This does not contradict the source all-width
+m-call lower bound: width is fixed at two, and the free program is allowed
+to depend on m. There is no claim about optimal binary-addition counts,
+efficient phase/projector generation, physical tape/precision tariffs,
+selected κ, or the complete multiplication theorem.
+
+## Open next questions
+
+Determine the fixed-width call cost with only the narrower affine/phase
+engine alphabet, where (1) must be re-established rather than assumed.
+Separately price the many free linear combinations before considering a
+physical application. No such efficiency is obtained here.
+
+Credit Jacob Alan Sussman's PR4628, Nick Petalas's PR5178, eumemic, Swapnil
+Jain and the retained register-model lineage. Prepared by JoyboyBrian with
+substantial OpenAI Codex assistance. Apache-2.0; no human or kernel approval.
+
+Every nonzero source address v partitions the addresses into a perfect matching {x,x+v}. An allowed tied address permutation conjugates this matching to the first-bit matching, so every allowed paid C_v has the same cross-sector rank and the same one-call normal form used above.
diff --git a/research/tied-width-two-transform-exact-call-cost/README.md b/research/tied-width-two-transform-exact-call-cost/README.md
new file mode 100644
index 0000000000..fb8b7cda7b
--- /dev/null
+++ b/research/tied-width-two-transform-exact-call-cost/README.md
@@ -0,0 +1,11 @@
+# Exact two-call cost at tied width two
+
+In the widened complex register-mixing game of JacobAlanSussman PR #4628 and NickPetalas PR #5178, the dense transform at tied width two costs exactly two paid calls for every m>=2 (one for m=1). The written proof supplies all-m sector-algebra generation, the arbitrary-clean-helper lower bound, and a two-call factorization with every helper reset. This is not an affine-engine or physical-cost theorem.
+
+Read PROOF.md for the complete hypotheses and proof. verify.py uses exact integer/rational operations, pins both actual source contracts, checks the first two dimensions and actual complex transform gauges, and requires the complete typed RESULT.json. Finite controls support but do not replace the quantified proof. Source PR #4628 is retained byte-identically as engine-predecessor.md, with its original commit and blob recorded in SOURCES.json.
+
+Reproduce with Python 3.12: `python3 -B research/tied-width-two-transform-exact-call-cost/verify.py`. No dependencies, solver or proof assistant are needed.
+
+## Open next questions
+
+Price the finite free-projector implementation in an actual physical caller, or determine the optimum when the widened free register maps are disallowed. The present result does not settle either question or alter the selected multiplication frontier.
diff --git a/research/tied-width-two-transform-exact-call-cost/RESULT.json b/research/tied-width-two-transform-exact-call-cost/RESULT.json
new file mode 100644
index 0000000000..608cf925d3
--- /dev/null
+++ b/research/tied-width-two-transform-exact-call-cost/RESULT.json
@@ -0,0 +1,24 @@
+{
+  "theorem": "exactly two paid calls for tied width two and every m>=2",
+  "fixtures": [
+    {
+      "m": 2,
+      "target_cross_rank": 3,
+      "slice_cross_rank": 2,
+      "gauge_entries": 256,
+      "second_call_necessary": true
+    },
+    {
+      "m": 3,
+      "target_cross_rank": 7,
+      "slice_cross_rank": 4,
+      "gauge_entries": 4096,
+      "second_call_necessary": true
+    }
+  ],
+  "source_sha256": {
+    "research/finite-width-call-mixing-tradeoff/README.md": "06578fd61c2a60e535a633ca628780b2195c73a2e36e83dab3a3f6c755cb9230",
+    "research/tied-width-two-transform-exact-call-cost/engine-predecessor.md": "4a67f8ccb6284bf17389086bd00ff38c3d256fab4e69a184aade1a6ca33eb7fe"
+  },
+  "physical_tariff_claimed": false
+}
diff --git a/research/tied-width-two-transform-exact-call-cost/SOURCES.json b/research/tied-width-two-transform-exact-call-cost/SOURCES.json
new file mode 100644
index 0000000000..63a823a93b
--- /dev/null
+++ b/research/tied-width-two-transform-exact-call-cost/SOURCES.json
@@ -0,0 +1,40 @@
+{
+  "schema_version": 1,
+  "base_commit": "ec2780e8aeb1c88acaf5e9e470ef8c68e7fbbb6c",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395",
+      "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602",
+      "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72"
+    },
+    {
+      "path": "research/finite-width-call-mixing-tradeoff/README.md",
+      "usage": "input",
+      "git_blob": "af2a5b402313fe120865cb6c24c86738ae916a8b",
+      "sha256": "06578fd61c2a60e535a633ca628780b2195c73a2e36e83dab3a3f6c755cb9230"
+    },
+    {
+      "path": "research/tied-width-two-transform-exact-call-cost/engine-predecessor.md",
+      "usage": "input",
+      "sha256": "4a67f8ccb6284bf17389086bd00ff38c3d256fab4e69a184aade1a6ca33eb7fe",
+      "git_blob": "46bccf74885682ca3e4bf97aea78d12770eec59c"
+    }
+  ],
+  "external_origins": [
+    {
+      "author": "JacobAlanSussman",
+      "pull_request": 4628,
+      "commit": "ee4fd87f064017c23e5a86fc1dcfe0a5237caed3",
+      "path": "research/complex-small-m-lower-bounds/PROOF.md",
+      "retained_as": "engine-predecessor.md",
+      "sha256": "4a67f8ccb6284bf17389086bd00ff38c3d256fab4e69a184aade1a6ca33eb7fe"
+    }
+  ]
+}
diff --git a/research/tied-width-two-transform-exact-call-cost/TASK.json b/research/tied-width-two-transform-exact-call-cost/TASK.json
new file mode 100644
index 0000000000..ef0bb76f11
--- /dev/null
+++ b/research/tied-width-two-transform-exact-call-cost/TASK.json
@@ -0,0 +1,95 @@
+{
+  "schema_version": 1,
+  "task_id": "formal-interface-lemma",
+  "priority_revision": 7,
+  "base_commit": "ec2780e8aeb1c88acaf5e9e470ef8c68e7fbbb6c",
+  "original_card": {
+    "id": "formal-interface-lemma",
+    "question": "Can one uncovered interface implication be formalized with exact caller and certificate bindings?",
+    "starting_points": [
+      "docs/research/research-family-status.md",
+      "certificates/selected-result.json",
+      "research/gate-operand-parity-lean/README.md",
+      "research/staged544-certified-endpoint/README.md",
+      "research/unconditional-batched-crt/README.md"
+    ],
+    "methods": [
+      "Formalize a missing boundary lemma identified by the selected review.",
+      "Audit a formal theorem-to-certificate binding independently."
+    ],
+    "acceptance_gate": "State the exact formalized proposition and remaining assumptions; avoid duplicate arithmetic formalizations already present.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Inventory the gate-operand parity lemma (#3807) and certified endpoint arithmetic (#3857). Neither is a full multiplication proof. For #4100, audit the compact-switch statement and its hypotheses before formalizing it.",
+      "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately."
+    },
+    "first_experiment": "Write one missing statement with quantified hypotheses, actual caller and existing coverage. A compact-switch lemma is a candidate only after its mathematical contract is reviewed. Establish a bounded proof plan before a separately budgeted proof-assistant build; do not rerun large Lean jobs as orientation.",
+    "bottleneck_link": "A missing interface proof can reduce the conditional gap even if it does not change kappa.",
+    "allowed_variations": [
+      "Narrow to one formal lemma or one theorem-to-certificate binding."
+    ],
+    "scope_change_triggers": [
+      "Formalizing already-covered arithmetic and claiming the full multiplication theorem."
+    ],
+    "overlap_terms": [
+      "hyperplane end",
+      "formal interface",
+      "Lean binding",
+      "3807",
+      "3857",
+      "4100",
+      "gate-operand-parity-lean",
+      "staged544-certified-endpoint",
+      "unconditional-batched-crt"
+    ],
+    "existing_checks": [
+      {
+        "scope": "PR #3807: scoped gate-operand parity formalization.",
+        "evidence": "research/gate-operand-parity-lean/README.md",
+        "remaining": "Exact theorem-to-caller binding and genuinely uncovered interface lemmas.",
+        "status": "author-checked",
+        "source_commit": "4c3530f42a6abcc48e7a6bcffd6c901911dc8269",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "scope": "PR #3857: certified real-power moment/endpoint arithmetic.",
+        "evidence": "research/staged544-certified-endpoint/README.md",
+        "remaining": "Uniform algorithmic implications, not another endpoint digit.",
+        "status": "author-checked",
+        "source_commit": "ef4315b8caa605e47a2515004845eb2d2ed71a86",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "scope": "PR #4100: compact-switch formalization proposed as future validation.",
+        "evidence": "research/unconditional-batched-crt/README.md",
+        "remaining": "Audit the statement and assumptions before a formal proof campaign.",
+        "status": "author-checked",
+        "source_commit": "337d04939571a637aeab54a0f58f54fde811663a",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      }
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "Prove exact paid-call cost two for every m>=2 at tied width f=2 in the widened register-mixing game.",
+  "scope_change_reason": "The source width bound leaves the fixed-width all-m optimum open; this is a scoped algebraic interface theorem, not a physical supplier.",
+  "bottleneck_link": "Separates tied-register mixing call cost from the narrow affine engine and physical tariffs.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop if all-m sector algebra generation or arbitrary-helper one-call lower bound fails.",
+  "outcome": "completed",
+  "evidence": "PROOF.md gives the quantified theorem; exact source-bound controls check the first two dimensions and actual complex gauges.",
+  "author": "JoyboyBrian",
+  "ai_assistance": "OpenAI Codex Astra authored and checked the package; independent AI-assisted root review is not a kernel proof.",
+  "open_questions": [
+    {
+      "question": "What is the cost in the narrower affine engine or with priced free mixing?",
+      "why_it_matters": "The theorem uses the widened game and does not supply a physical tariff.",
+      "first_step": "Bind actual permitted free operations and price the projector expansion.",
+      "blocked_by": "No such tariff is proved here."
+    }
+  ]
+}
diff --git a/research/tied-width-two-transform-exact-call-cost/VERIFY.json b/research/tied-width-two-transform-exact-call-cost/VERIFY.json
new file mode 100644
index 0000000000..5a05fb86e9
--- /dev/null
+++ b/research/tied-width-two-transform-exact-call-cost/VERIFY.json
@@ -0,0 +1,21 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/finite-width-call-mixing-tradeoff/README.md",
+    "research/tied-width-two-transform-exact-call-cost/engine-predecessor.md"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 10,
+      "checks": "Exact character cross factors, actual Gaussian-integer transform gauges, all nonzero directions, mandatory typed receipt"
+    }
+  ]
+}
diff --git a/research/tied-width-two-transform-exact-call-cost/engine-predecessor.md b/research/tied-width-two-transform-exact-call-cost/engine-predecessor.md
new file mode 100644
index 0000000000..46bccf7488
--- /dev/null
+++ b/research/tied-width-two-transform-exact-call-cost/engine-predecessor.md
@@ -0,0 +1,191 @@
+# The written arguments
+
+Each part is headed by its status, in the words of the README. "Argued by hand" means a written argument that no
+person and no proof checker has checked. The setting and the words are those of README section 3: W arrays of 2^m
+complex numbers, calls C_v = aI + bX_v (a = (1+i)/2, b = (1−i)/2), free steps by game, and correctness at every
+number f of digit columns, where every letter acts the same way on each of the f columns.
+
+## 1. The kept-subspace bound
+
+*Status: proved in Lean for the engine game with rational mixing (`engine_lower_bound`). The form below, over any
+field and with any linear mixing, is argued by hand.*
+
+**Setting.** Fix a width f and let V be the data space of one array at that width. A program has R ≥ W registers;
+registers 1..W start with the inputs y_1..y_W, the others start at 0. Three kinds of step:
+- *mixing* (free): replace one register by any linear combination of all registers (copies into scratch, overwriting
+  and erasing included; nothing is assumed invertible);
+- *a free letter* (free): apply a map b of a group B to one register;
+- *a call* (paid): apply an invertible map g to one register.
+
+At the end, for each l, some register (a different one for each l) holds T_l·y_l, the target of array l.
+
+Let N ⊆ V be a subspace with b(N) = N for every free letter b, and let raise(g) = dim(N + gN) − dim N.
+
+**Theorem.** In every correct run, the sum of raise(g) over the calls is at least raise(T_1) + ... + raise(T_W). If
+every call has raise at most `cap` and every target has raise at least `demand`, then cap · s ≥ W · demand.
+
+*Proof.* A state gives a linear map M from V^W (the inputs) to V^R (the registers). Let A = M(N^W), the image of the
+inputs taken from N, and Φ = dim(A + N^R) − R·dim N: what the state adds beyond N in each register.
+- At the start A = N^W ⊕ 0 lies in N^R, so Φ = 0.
+- Mixing multiplies M by an R × R matrix acting on registers, and a free letter multiplies one block by b. Both map
+  N^R into itself, so they map A + N^R into (new A) + N^R. The new quotient is an image of the old one, so Φ does not
+  grow (an erasure may lower it).
+- A call g on register r multiplies block r by g. Call this map D; it is invertible, so dim(DA + N^R) =
+  dim(A + D^(−1)N^R). The space D^(−1)N^R is N in every block except block r, where it is g^(−1)N, and it exceeds N^R
+  by dim(N + g^(−1)N) − dim N = raise(g) dimensions. So Φ grows by at most raise(g).
+- At the end, keep only the W delivering registers. There the image of A is the direct sum over l of
+  (N + T_l N)/N, because the y_l vary independently over N. Dropping blocks cannot raise a dimension, so
+  Φ ≥ Σ_l raise(T_l).
+
+Φ starts at 0, ends at least at Σ_l raise(T_l), and grows by at most raise(g) per call. ∎
+
+In the Lean form, the free letters are the engine's shifts, address maps and phases, mixing takes a rational matrix,
+and correctness is required at every width (`GLiveKernel`). The one step that uses the mixing, that it maps N^R into
+itself, needs only that N is a complex subspace; so the same proof works for complex mixing. That last sentence is
+argued, not in Lean.
+
+## 2. The hook: kept, its cap, and the demands
+
+*Status: kept and cap proved in Lean at every block size (`hook_kept`, `hook_cap`); demands 8 (block 2) and 224
+(block 3) proved in Lean; the block-4 demand 86,592 checked by computer, with the split into 16 equal character
+blocks argued by hand.*
+
+At block m and width f = j + 2 write the data space of one array as V ⊗ V^(⊗(j+1)), V = C^(2^m), and keep only its
+part V ⊗ Λ^(j+1) V (every letter acts the same on each column, so it keeps this part). The hook is
+
+  N = span{ e_x ⊗ e_T : T a (j+1)-subset of addresses, x in T }.
+
+- *Kept.* A free letter inside one array sends each address x to one address π(x) and multiplies by a number c(x),
+  the same in every column. It sends e_x ⊗ e_T to a multiple of e_π(x) ⊗ e_π(T), and π(x) lies in π(T). So N is kept
+  by every shift, every address map (not only the affine ones) and every diagonal phase.
+- *Cap.* A call dir(z) pairs each address a with a + z. For each pair and each j-subset w, the vector
+  e_a ⊗ (e_a ∧ e_w) − e_(a+z) ⊗ (e_(a+z) ∧ e_w) lies in N and its image stays in N. These vectors have disjoint
+  supports (the w that contain both a and a + z give nothing), so they span a subspace of N of dimension
+  dim N − (2^m/2)·C(2^m − 2, j) that the call keeps inside N; hence raise(dir z) ≤ (2^m/2)·C(2^m − 2, j). At block 3 (j = 3) that is 280 − 200 = 80; `verify.py` builds the 200 vectors
+  exactly over the Gaussian integers for all 7 directions, and checks that 80 is attained. (Lean proves the formula
+  at every block by its own route.)
+- *Demand.* raise(C^(⊗m)) is the rank of the block of C^(⊗m) acting on V ⊗ Λ^(j+1) V from N to its complement. At
+  block 2 it is at least 8 (Lean, `dem2`). At block 3 the block is 280 × 280 and its rank is at least 224: the
+  characters of F_2^3 (the shifts commute with the kernel) split it into 8 blocks, each of rank at least 28 (Lean, `dem3`).
+  At block 4 the same split gives 16 blocks; one has rank at least 5,412 by a certificate checked by computer (a
+  second block was checked too), and that all 16 have that rank is argued by hand. So the demand is at least
+  16 × 5,412 = 86,592.
+
+**Consequences.** With the theorem of section 1: block 2 gives 8W ≤ 4s, so s ≥ 2W; block 3 gives 224W ≤ 80s, so
+s ≥ 14W/5; block 4 gives 86,592W ≤ 27,456s, so s ≥ 41W/13. At block 3, a run of two calls on one array raises the
+hook by at most 144 < 160 (136 exact vectors, checked by computer), so a grouped call of rank 2 also fits the bound.
+
+**The widened game** (every address permutation and every phase pattern free). *Status: argued by hand; three AI
+reviewers upheld it (one re-derived the bound against the Lean engine, one checked keptness exactly for 199 free
+steps including Toffoli, CCZ and controlled-S, one redid the numbers).* The kept bullet above covers every
+permutation and every diagonal, and nothing else changes, so 14W/5 and 41W/13 hold there too.
+
+## 3. Complex mixing and Harvey's B-calls
+
+*Status: argued by hand, not checked by a person. The numbers it uses are the ones proved in Lean in section 2.*
+
+- *Complex mixing.* Section 1's proof uses only that mixing is linear and maps N^R into N^R, which holds for complex
+  coefficients. So 2W and 14W/5 hold with complex mixing.
+- *B-calls.* B = (1 − i)·S·C·S with S = diag(1, i). A B-call along an axis at width f is (1 − i)^f times a C-call
+  between two diagonal maps (S on that bit, in every column). For invertible diagonals D_1, D_2 (which keep N) and a
+  nonzero scalar λ, raise(λ D_1 C D_2) = dim(D_1^(−1)N + C D_2 N) − dim N = raise(C). The same holds for the target
+  B^(⊗3) = (1 − i)^3 S^(⊗3) C^(⊗3) S^(⊗3). The program at width 5 is a fixed linear program, so section 1 applies
+  at that one width, which is all the block-3 proof uses. So 4 arrays at block 3 need at least 12 B-calls too.
+
+## 4. One array needs m calls
+
+*Status: argued by hand, not checked by a person. AI reviewers re-derived the general form in two rounds; the
+single-array support count was re-derived by one AI reviewer.*
+
+**Without scratch** (David Harvey's single-array programs P_M0 A_i1 P_M1 ⋯ A_ig P_Mg, with any free steps that send
+one address to one address). Follow one input basis vector e_x. A free step sends a basis vector to a multiple of
+one basis vector; a call sends it to a combination of at most two (at width f, of at most 2^f). After g calls,
+e_x has spread to at most 2^g addresses (2^(gf) at width f). Every column of the target has all its entries nonzero:
+the entries of B^(⊗m) are ±1, and those of C^(⊗m) are a^(m−d) b^d with d the distance between the two addresses.
+So 2^g ≥ 2^m and g ≥ m, at every width, width 1 included.
+
+**With scratch and mixing**, in every game whose free letters have at most c nonzeros in each column, with c not
+depending on f. The output of array l is a sum over the paths through the program, with fixed coefficients, of
+words in the letters; the number of paths does not depend on f. A path with j calls and k free letters gives an
+operator with at most c^k 2^(jf) nonzeros per column. If every path from input l to output l had at most m − 1 calls,
+the coefficient of input l in output l would have at most (number of paths)·c^(k_max)·2^((m−1)f) nonzeros per column,
+fewer than the target's 2^(mf) once f is large. So some path has at least m calls, and one array needs m calls.
+
+This needs correctness at large f. At width 1, one zero scratch array makes C^(⊗3) free: copy the array into the
+scratch, shift the copy by e_i, replace the array by a·(array) + b·(copy), for i = 1, 2, 3. The result is
+C_(e_3) C_(e_2) C_(e_1) = C^(⊗3) at width 1, but at width 2 it is a·I + b·(X_v ⊗ X_v) per direction instead of
+C_v ⊗ C_v. *Checked by computer* (`verify.py`, part `width`: equal at width 1, all 4,096 entries differ at width 2).
+
+## 5. Block 3 without phase letters: s ≥ 3W for every group of address maps
+
+*Status: argued by hand, not checked by a person; one AI reviewer re-derived it and recomputed the certificate with
+its own exact code. The certificate's numbers are checked by computer here (`verify.py`, part `face3`).*
+
+**Statement.** In the game with calls, shifts, any complex mixing with scratch, and address maps from any subgroup H
+of GL(3, 2), but no phase letters, every unit for W arrays at block 3 uses at least 3W calls.
+
+*Proof.*
+- *The group.* The calls dir(z) and the shifts X_a generate an abelian group A (every element is a polynomial in the
+  shifts). An address map h is not in A unless h = 1, and h^(−1) dir(z) h = dir(h^(−1) z), h^(−1) X_a h =
+  X_(h^(−1) a). So the letters generate the semidirect product A ⋊ H. A program right at every width is an identity
+  in the group algebra C[A ⋊ H].
+- *Trading address maps for arrays.* C[A ⋊ H] is a free right C[A]-module with basis H. Left multiplication gives an
+  injective algebra map ρ into n × n matrices over C[A] (n = |H|), with ρ(a) = diag_h(h^(−1) a h) for a in A and
+  ρ(h′) a permutation matrix. Apply ρ to every step. Each register becomes n registers; a call dir(z) becomes n
+  calls dir(h^(−1) z), one on each copy; a shift becomes shifts; an address map becomes a permutation of registers,
+  which is mixing. The result is a program with no address maps for nW arrays with nM calls, in which array (l, h)
+  is owed h^(−1) K h = dir(h^(−1) e_1) dir(h^(−1) e_2) dir(h^(−1) e_3): the kernel in another basis.
+- *The certificate.* At width 3 take the antisymmetric part Λ³(C^8), which every letter keeps, and N = the span of
+  the 24 *face* triples (three addresses that agree in one bit). Shifts and every diagonal map keep N. For every
+  direction, raise(dir z) = 8; for every basis b of F_2^3, raise(K_b) = 24 (exact ranks over Q(i)).
+- *Count.* Section 1 on the new program gives 8·nM ≥ 24·nW, so M ≥ 3W. ∎
+
+**Scope.** Pauli Z phases and scalars do not break it. The engine's phase letters do: S·dir(e_1)·S is a scalar times
+a Hadamard on one bit, a product of S phases gives CZ, and conjugating CZ by a Hadamard gives a CNOT, an address map.
+Then ρ produces address maps inside the new program, and they leak out of N (`verify.py` checks that a CNOT raises N
+by 8). Without address maps, phase letters alone also give 3W at block 3 (argued by hand). So a block-3 saver must
+use address maps and phase letters together. Harvey's §7.4 model has neither, and his §6 relabellings with C-calls
+fall under this section; his §6 B-calls along relabelled axes bring phases, and there only section 2's 14W/5
+applies.
+
+## 6. W + m and 2W in every game with bounded free steps
+
+*Status: argued by hand, not checked by a person. One AI reviewer re-derived 2W line by line and checked its key
+orthogonality fact with its own code over a wider set of free steps; one AI reviewer upheld the trace-limit version
+of W + m and reproduced its numbers. Below is the outline of the written proofs.*
+
+**Setting.** Free letters have at most s_0 nonzeros per row and column, each of modulus at most c_0, independent of f
+(this includes address maps, phases, Toffoli, controlled-S and maps that mix neighbouring digit columns). A unit is
+a straight-line program u_k = D_k c_k, c_k = Σ_(i<k) B_ki u_i + γ_k, with outputs K e_l = A_0^(l) + Σ_k A_k^(l) u_k,
+where D_k are calls and all coefficients are fixed combinations of free words. It must be right at infinitely many f.
+
+1. *Support growth gives orthogonality.* Every entry of K has modulus N^(−1/2) (N = 2^(mf)), and a word with at most
+   m − 1 calls has at most C·2^((m−1)f) nonzeros per row. Hence, for free words c, c′ and such a word w,
+   |tr((cKc′)* w)|/N ≤ C′·2^(−f/2).
+2. *The trace limit.* τ(y) = lim tr(y_f)/N along an ultrafilter over the widths is a trace; its GNS completion gives a
+   finite von Neumann algebra. Let H_k be the closure of the words with at most k calls and H_top the closure of
+   span{cKc′}. By step 1, H_top ⊥ H_(m−1). The projections onto these spaces commute with multiplication by free
+   words on either side.
+3. *Top layer.* Project the output identities onto H_top. Only calls that end a chain of m calls survive, and only
+   contents that start one. If s = W + m − 1, this leaves K·I_W = 𝐀 Z Γ with W × W matrices; direct finiteness of the
+   algebra makes all three invertible. (With s = W + m − 2 there are only W − 1 surviving calls, which is impossible:
+   s ≥ W + m − 1 for every W.)
+4. *Next layer* (W ≥ 2). Project instead onto H_(m−1) ⊖ H_(m−2). K and the inputs vanish there; using that 𝐀 is
+   invertible, the last path part reaching the top is forced into H_(m−2), so its top part is 0, against step 3.
+   So s ≥ W + m.
+5. *2W.* The same projections, with H_1 ⊖ H_0 as the next layer: every single call is orthogonal to the free words
+   (its entries have modulus 2^(−f/2)), so the next-layer path matrix is triangular with unitary diagonal, hence
+   invertible. Then the next-layer equation reads 𝐁·𝐆 = 0 and the top equation K·I_W = 𝐁·(…)·𝐆, with 𝐁 of rank at
+   least W and 𝐆 of rank at least W. Sylvester's rank inequality in the finite algebra (Murray and von Neumann)
+   gives rank 𝐁 + rank 𝐆 ≤ s, so s ≥ 2W.
+
+At block 2 this gives s ≥ 2W, the plain cost, in every such game. At larger m it adds to W + m only when W > m.
+
+## 7. From block 4 on: 2.9447 calls per array in the engine game
+
+*Status: argued by hand from exact computations, not checked by a person; two AI reviewers reproduced every number
+with their own code.* The block-4 hook is carried upward through projections between the frame graphs of the
+engine, controlled by a coupling argument; the exact values are 834,241/278,850 = 2.99172 at block 5 and
+1,188,222/399,685 = 2.97290 at block 6, and the bound stays above 2.9447 at every block. The programs and the
+written argument are in my repository (README, Sources). The projections use the engine's frames, so nothing here
+carries it to the widened game; there the bounds at blocks 5 and 6 are 62/29 and 63/31 (checked by computer).
diff --git a/research/tied-width-two-transform-exact-call-cost/verify.py b/research/tied-width-two-transform-exact-call-cost/verify.py
new file mode 100644
index 0000000000..e2c1fdb94b
--- /dev/null
+++ b/research/tied-width-two-transform-exact-call-cost/verify.py
@@ -0,0 +1,64 @@
+"""Exact character formulas and actual complex transform gauge; no numerical rounding."""
+from pathlib import Path
+import hashlib,json
+P=Path(__file__).resolve().parent
+def need(v,s):
+    if not v:raise ValueError(s)
+def canonical(v):return json.dumps(v,sort_keys=True,separators=(',',':'))
+def gm(a,b):return (a[0]*b[0]-a[1]*b[1],a[0]*b[1]+a[1]*b[0])
+def gp(a,n):
+    z=(1,0)
+    for _ in range(n):z=gm(z,a)
+    return z
+def chi(w,x):return (-1)**((w&x).bit_count())
+def rank(a):
+    from fractions import Fraction
+    a=[list(map(Fraction,r)) for r in a];k=0
+    for j in range(len(a[0])):
+        q=next((i for i in range(k,len(a)) if a[i][j]),None)
+        if q is None:continue
+        a[k],a[q]=a[q],a[k];v=a[k][j];a[k]=[x/v for x in a[k]]
+        for i in range(k+1,len(a)):
+            v=a[i][j];a[i]=[x-v*y for x,y in zip(a[i],a[k])]
+        k+=1
+    return k
+
+def source_hashes():
+    source=json.loads((P/'SOURCES.json').read_text());rows=[r for r in source['files'] if r['usage']=='input'];need(len(rows)==2,'both source contracts required')
+    for r in rows:need(hashlib.sha256((P.parents[1]/r['path']).read_bytes()).hexdigest()==r['sha256'],'source bytes')
+    return {r['path']:r['sha256'] for r in rows}
+def result():
+    sources=source_hashes();records=[]
+    for m in (2,3):
+        d=2**m;pairs=[(i,j) for i in range(d) for j in range(i+1,d)];r=d//2
+        # Derive target cross blocks from the ordered tensor entries, independently
+        # of the author's sparse L/R implementation in the separate checker.
+        sd=[[chi(i,x)*chi(j,x) for x in range(d)] for i,j in pairs]
+        ds=[[2*chi(x,i)*chi(x,j) for i,j in pairs] for x in range(d)]
+        need(rank(sd)==rank(ds)==d-1,'target cross ranks')
+        groups=(range(1,r+1),range(r+1,d));parts=[]
+        for ws in groups:
+            parts.append([[sum(int(i^j==w)*chi(w,x) for w in ws) for x in range(d)] for i,j in pairs])
+        need(all(parts[0][i][x]+parts[1][i][x]==sd[i][x] for i in range(len(pairs)) for x in range(d)),'both cross factors')
+        need(any(parts[0][i][x]!=sd[i][x] for i in range(len(pairs)) for x in range(d)),'missing second call rejected')
+        # C_m numerator is product of (1+i) for equal bits and (1-i) otherwise.
+        count=0
+        for a in range(d):
+         for b in range(d):
+          for x in range(d):
+           for y in range(d):
+            direct=(1,0)
+            for i,j in ((a,x),(b,y)):
+             for bit in range(m):direct=gm(direct,(1,1 if ((i^j)>>bit)&1==0 else -1))
+            gauge=gm(gp((1,1),2*m),gp((0,-1),sum(z.bit_count() for z in (a,b,x,y))))
+            sign=chi(a,x)*chi(b,y);gauge=(sign*gauge[0],sign*gauge[1])
+            need(direct==gauge,'actual complex numerator gauge');count+=1
+        # Every source C_v is a perfect matching, hence the same cross rank.
+        for v in range(1,d):
+            matching=[(x,x^v) for x in range(d) if x<(x^v)]
+            need(len(matching)==r and len({x for pair in matching for x in pair})==d,'all source directions')
+        records.append(dict(m=m,target_cross_rank=d-1,slice_cross_rank=r,gauge_entries=count,second_call_necessary=True))
+    return dict(theorem='exactly two paid calls for tied width two and every m>=2',fixtures=records,source_sha256=sources,physical_tariff_claimed=False)
+if __name__=='__main__':
+    need(canonical(result())==canonical(json.loads((P/'RESULT.json').read_text())),'mandatory typed complete receipt')
+    print('PASS_TIED_WIDTH_TWO_EXACT_CALL_COST')

From a5c0e17c561e76dd8fe82cd64d089066fd41aeea Mon Sep 17 00:00:00 2001
From: JoyboyBrian <122925040+JoyboyBrian@users.noreply.github.com>
Date: Fri, 23 Oct 2026 05:49:33 -0700
Subject: [PATCH 2/2] Independently certify sparse two-call factors and finite
 free projectors

---
 .../README.md                                 |  2 +
 .../SOURCES.json                              |  3 +-
 .../VERIFY.json                               |  9 +++
 .../independent.py                            | 76 +++++++++++++++++++
 4 files changed, 89 insertions(+), 1 deletion(-)
 create mode 100644 research/tied-width-two-transform-exact-call-cost/independent.py

diff --git a/research/tied-width-two-transform-exact-call-cost/README.md b/research/tied-width-two-transform-exact-call-cost/README.md
index fb8b7cda7b..2aa542fa4b 100644
--- a/research/tied-width-two-transform-exact-call-cost/README.md
+++ b/research/tied-width-two-transform-exact-call-cost/README.md
@@ -9,3 +9,5 @@ Reproduce with Python 3.12: `python3 -B research/tied-width-two-transform-exact-
 ## Open next questions
 
 Price the finite free-projector implementation in an actual physical caller, or determine the optimum when the widened free register maps are disallowed. The present result does not settle either question or alter the selected multiplication frontier.
+
+The separate `independent.py` checker adapts the independent root reviewer’s exact sparse-factor construction, with ordered tensor-to-sector conversion and all four-root projectors. It imports no primary verifier. Run it with the same Python command. The engine source pin points to its first retained commit so the export has verifiable publication ancestry.
diff --git a/research/tied-width-two-transform-exact-call-cost/SOURCES.json b/research/tied-width-two-transform-exact-call-cost/SOURCES.json
index 63a823a93b..ecd0e6ef0b 100644
--- a/research/tied-width-two-transform-exact-call-cost/SOURCES.json
+++ b/research/tied-width-two-transform-exact-call-cost/SOURCES.json
@@ -24,7 +24,8 @@
       "path": "research/tied-width-two-transform-exact-call-cost/engine-predecessor.md",
       "usage": "input",
       "sha256": "4a67f8ccb6284bf17389086bd00ff38c3d256fab4e69a184aade1a6ca33eb7fe",
-      "git_blob": "46bccf74885682ca3e4bf97aea78d12770eec59c"
+      "git_blob": "46bccf74885682ca3e4bf97aea78d12770eec59c",
+      "pin": "head:051b7ae23ff85d21e14bd6ce1791f7c28ff48053:research/tied-width-two-transform-exact-call-cost/engine-predecessor.md"
     }
   ],
   "external_origins": [
diff --git a/research/tied-width-two-transform-exact-call-cost/VERIFY.json b/research/tied-width-two-transform-exact-call-cost/VERIFY.json
index 5a05fb86e9..dea72ffb6c 100644
--- a/research/tied-width-two-transform-exact-call-cost/VERIFY.json
+++ b/research/tied-width-two-transform-exact-call-cost/VERIFY.json
@@ -16,6 +16,15 @@
       ],
       "timeout_seconds": 10,
       "checks": "Exact character cross factors, actual Gaussian-integer transform gauges, all nonzero directions, mandatory typed receipt"
+    },
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "{package}/independent.py"
+      ],
+      "timeout_seconds": 10,
+      "checks": "Independent ordered tensor conversion, explicit sparse LQR factors and exact free projectors"
     }
   ]
 }
diff --git a/research/tied-width-two-transform-exact-call-cost/independent.py b/research/tied-width-two-transform-exact-call-cost/independent.py
new file mode 100644
index 0000000000..0b9e762af1
--- /dev/null
+++ b/research/tied-width-two-transform-exact-call-cost/independent.py
@@ -0,0 +1,76 @@
+"""Independent sparse factor checker, adapted from the root reviewer with attribution.
+Uses ordered tensor construction and Fraction sector conversion, not primary formulas.
+"""
+from fractions import Fraction as F
+import json,hashlib,time
+from pathlib import Path
+
+def matmul(a,b):
+    bt=list(zip(*b))
+    return [[sum(x*y for x,y in zip(row,col) if x and y) for col in bt] for row in a]
+def rank(a):
+    a=[list(map(F,r)) for r in a];k=0
+    for j in range(len(a[0])):
+        p=next((i for i in range(k,len(a)) if a[i][j]),None)
+        if p is None:continue
+        a[k],a[p]=a[p],a[k];v=a[k][j];a[k]=[x/v for x in a[k]]
+        for i in range(k+1,len(a)):
+            if a[i][j]:
+                v=a[i][j];a[i]=[x-v*y for x,y in zip(a[i],a[k])]
+        k+=1
+    return k
+def ordered_to_sector(a,d):
+    pairs=[(i,j) for i in range(d) for j in range(i+1,d)]
+    basis=[[(i*d+i,1)] for i in range(d)]+[[(i*d+j,1),(j*d+i,1)] for i,j in pairs]+[[(i*d+j,1),(j*d+i,-1)] for i,j in pairs]
+    out=[]
+    for v in basis:
+        y=[sum(a[k][i]*c for i,c in v) for k in range(d*d)]
+        out.append([y[i*d+i] for i in range(d)]+[F(y[i*d+j]+y[j*d+i],2) for i,j in pairs]+[F(y[i*d+j]-y[j*d+i],2) for i,j in pairs])
+    return [list(r) for r in zip(*out)],pairs
+def kron(a):return [[a[i][k]*a[j][l] for k in range(len(a)) for l in range(len(a))] for i in range(len(a)) for j in range(len(a))]
+def need(value, message):
+    if not value:raise ValueError(message)
+rows=[]
+for m in (2,3):
+    d=2**m;n=d*d;s=d*(d-1)//2
+    h=[[(-1)**((i&j).bit_count()) for j in range(d)] for i in range(d)]
+    w=[[((-1)**(i*j)) if i//2==j//2 else 0 for j in range(d)] for i in range(d)]
+    T,pairs=ordered_to_sector(kron(h),d);Q,_=ordered_to_sector(kron(w),d)
+    targetrank=rank([r[:d] for r in T[d:d+s]]);slicerank=rank([r[:d] for r in Q[d:d+s]])
+    need((targetrank,slicerank)==(d-1,d//2),'independent cross rank')
+    pieces=[]
+    for ws in (list(range(1,1+d//2)),list(range(1+d//2,d))):
+        L=[[0]*n for _ in range(n)];R=[[0]*n for _ in range(n)]
+        for p,address in enumerate(ws):
+            e=pairs.index((2*p,2*p+1));v=[(-1)**((address&x).bit_count()) for x in range(d)]
+            for z,x in enumerate(v):R[2*p][z]=x;L[z][2*p]=x
+            for z,(i,j) in enumerate(pairs):
+                if i^j==address:L[d+z][d+e]=1;R[d+e][d+z]=1
+        pieces.append(matmul(matmul(L,Q),R))
+    residual=[[T[i][j]-pieces[0][i][j]-pieces[1][i][j] for j in range(n)] for i in range(n)]
+    sector=lambda i:0 if i<d else 1 if i<d+s else 2
+    need(all(residual[i][j]==0 for i in range(n) for j in range(n) if sector(i)!=sector(j)),'two-call residual sectors')
+    need(any(T[i][j]!=pieces[0][i][j] for i in range(d,d+s) for j in range(d)),'one-call negative')
+    phasechecks=0
+    # Each coordinate character factor is evaluated independently; no author helper imported.
+    for p in range(d):
+      for q in range(d):
+       for i in range(d):
+        for j in range(d):
+         acc=1
+         for k in range(d):
+          e=(int(k==i)+int(k==j)-int(k==p)-int(k==q))%4
+          z=[(1,0),(0,1),(-1,0),(0,-1)]
+          real=sum(z[(t*e)%4][0] for t in range(4));imag=sum(z[(t*e)%4][1] for t in range(4))
+          need(imag==0 and real in (0,4),'exact roots of unity');acc*=real//4
+         need(acc==int(sorted((i,j))==sorted((p,q))),'free character projector')
+         phasechecks+=1
+    rows.append(dict(m=m,dimension=n,target_cross_rank=targetrank,slice_cross_rank=slicerank,all_endpoint_entries=n*n,phase_entries=phasechecks,one_call_negative_control=True))
+
+P=Path(__file__).resolve().parent
+sources=json.loads((P/'SOURCES.json').read_text());inputs=[r for r in sources['files'] if r['usage']=='input'];need(len(inputs)==2,'both source contracts')
+for r in inputs:need(hashlib.sha256((P.parents[1]/r['path']).read_bytes()).hexdigest()==r['sha256'],'source bytes')
+receipt=json.loads((P/'RESULT.json').read_text())
+need(type(receipt['physical_tariff_claimed'])is bool and not receipt['physical_tariff_claimed'],'typed scope')
+need([x['target_cross_rank'] for x in receipt['fixtures']]==[x['target_cross_rank'] for x in rows],'independent receipt ranks')
+print('PASS_INDEPENDENT_SECTOR_FACTORS_AND_FREE_PROJECTORS')