From fb607e2385980dd36cd4bfc53885cb2ffab5d5dc Mon Sep 17 00:00:00 2001 From: Nicholas Stone Date: Sun, 25 Oct 2026 22:33:52 +0800 Subject: [PATCH] Prove coordinate isolation excludes the 24 remaining span-six pools --- .../PROOF.md | 133 +++++++++++++++ .../README.md | 40 +++++ .../SOURCES.json | 36 ++++ .../TASK.json | 64 +++++++ .../VALIDATION.json | 46 ++++++ .../VERIFY.json | 34 ++++ .../verify.py | 156 ++++++++++++++++++ 7 files changed, 509 insertions(+) create mode 100644 research/coordinate-kernel-span-six-closure/PROOF.md create mode 100644 research/coordinate-kernel-span-six-closure/README.md create mode 100644 research/coordinate-kernel-span-six-closure/SOURCES.json create mode 100644 research/coordinate-kernel-span-six-closure/TASK.json create mode 100644 research/coordinate-kernel-span-six-closure/VALIDATION.json create mode 100644 research/coordinate-kernel-span-six-closure/VERIFY.json create mode 100644 research/coordinate-kernel-span-six-closure/verify.py diff --git a/research/coordinate-kernel-span-six-closure/PROOF.md b/research/coordinate-kernel-span-six-closure/PROOF.md new file mode 100644 index 0000000000..bf20f5d4f9 --- /dev/null +++ b/research/coordinate-kernel-span-six-closure/PROOF.md @@ -0,0 +1,133 @@ +# Closing the 24 coordinate-kernel pools at span six + +Prepared for Nicholas Stone with substantial OpenAI Codex assistance, 2026-10-25. +New material: Apache-2.0. This is a written reduction using the explicitly cited +predecessor lemma, with finite exact corroboration, not a proof-kernel theorem. + +## Statement + +In the four-scalar-register formal abelian BIT model, no eight-call word of +rational address span six with noncoordinate projectors in a coordinate +permutation of (0x0003,0x0022,0x0550) can have a diagonal monomial endpoint +with three invertible rational 3-by-3 target addresses. The fourth endpoint +address is arbitrary and all four input registers are arbitrary. + +A paid factor is D_N([A])=I+([A]-1)N over F2[G], where G is the additive +group of rational 3-by-3 matrices, rank_Q(A)=1, and N=xy^t is a binary +rank-one idempotent. Coordinate-projector calls may be interleaved arbitrarily. +No arbitrary scalar basis change of a diagonal endpoint is made in this proof. + +## Inherited lemma + +David Govea's PR720, research/three-register-no-target-flag/README.md sections +1--4, states: for a three-register word with torsion-free abelian exponents, +relation lattice of rank at most two, and diagonal monomial endpoint, the +three endpoint exponents are sums of pairwise disjoint subsets of the paid +exponents. In particular their matrix ranks sum to at most the sum of the +paid matrix ranks. No invertibility or target flag is required for this lemma. +This is the low-corank lemma, not PR720's span-five exhaustive census. +Its source and inherited PR468/PR288/PR203 attribution are recorded in SOURCES.json. +The present package does not independently reprove that predecessor lemma. + +## 1. A literal coordinate block + +For packed bit 4i+j denoting entry (i,j), the representative is + + X = [[1,1,0,0], [0,0,0,0], [0,0,0,0], [0,0,0,0]], + Y = [[0,1,0,0], [0,1,0,0], [0,0,0,0], [0,0,0,0]], + Z = [[0,0,0,0], [1,0,1,0], [1,0,1,0], [0,0,0,0]]. + +Each has zero fourth row AND zero fourth column. Every coordinate projector +also preserves the coordinate decomposition F2^4=F2^3 direct-sum F2. +Thus EVERY allowed factor, including every interleaved coordinate factor, +is block diagonal in this decomposition. E_33 acts only on the singleton; +X,Y,Z,E_00,E_11,E_22 act only on the triple. Restricting a triple factor +leaves a nonzero rank-one idempotent. No dirty input is discarded: the +decomposition is an identity of full operators on arbitrary inputs. + +The 24 pools are coordinate permutations of this representative (PR5231). +A coordinate permutation preserves diagonality and merely relocates the +singleton. It need not preserve which coordinate is auxiliary, and the +argument below makes no such assumption. + +## 2. Relation rank cannot grow on restriction + +Let J be the set of triple-block calls and K the singleton calls, with +|J|+|K|=8. The full rational relation space is + + L_Q = {c in Q^8 : sum_j c_j A_j=0}, dim L_Q=8-6=2. + +Every relation among (A_j)_{j in J}, extended by zeros on K, lies in L_Q. +This is an injection, so the triple subword's relation rank is at most two. +The generated address group is finitely generated and torsion free, so its +integral relation lattice has this same rank. Relations involving both +blocks do not invalidate this injection. No direct-sum assumption about +their ADDRESS spans is needed. + +## 3. Rank budget + +The full diagonal endpoint restricts to a diagonal monomial endpoint on +the triple. Apply the inherited disjoint-subset lemma to that subword: + + sum_(i in triple) rank_Q(C_i) <= |J|. + +On the singleton each factor is multiplication by its monomial, so + + C_singleton = sum_(j in K) A_j, + rank_Q(C_singleton) <= |K|. + +Adding gives sum_(i=0)^3 rank_Q(C_i) <= 8. Three invertible 3-by-3 targets +already contribute nine, and the remaining rank is nonnegative. Contradiction. +This covers a singleton data register as well as a singleton auxiliary. +It allows arbitrary auxiliary diagonal address and arbitrary call order. + +Equivalently, the lemma supplies disjoint frame assignments on the triple; +the singleton uses only the complementary indices K. Hence all four target +addresses admit disjoint-subset assignments in this class at relation rank <=2. +This stronger statement holds for any call count and any rational matrix size, +provided the coordinate 3+1 decomposition and relation-rank condition hold. + +## 4. Scope and consequence + +This resolves the 24-pool handoff of PR5231 using coordinate isolation, not +the kernel-support-union >=2 obstruction from that PR. The union is indeed +one here; that old argument failing does not make the coordinate block coupled. + +Combining this result with the retained PR4119 classification, PR5075 cyclic-line +closure, and PR5231 exclusion of the other 48 pools would exclude the entire +eight-call span-six case for FOUR scalar registers. That combined statement +additionally depends on those predecessor reductions; the new checker does +not independently validate their universal proofs or re-enumerate the full +four-register flag census. The local result proved here is the 24-pool closure. + +This does not settle span five or arbitrarily many auxiliary registers, and +does not change a physical supplier or the selected multiplication exponent. +For an upper-bound control, nine coordinate calls can produce three invertible +targets with total address span six. They belong to the allowed alphabet but +do not use all three exceptional projectors; no nine-call attainer with an +exactly prescribed occurring exceptional triple is asserted. + +## Verification and credit + +verify.py checks all 24 coordinate permutations, the literal 3+1 block and +restricted idempotents, and all positions of the three data targets. A separate +dense-matrix formal Laurent engine checks block factorization for every word +through length four in the seven-letter representative alphabet, and for +nontrivial cancelling words. It checks a nine-call span-six positive control, +rejects the two previously excluded 48-orbit representatives as coordinate- +isolation inputs, and rejects an off-block bridge and a rank-two projector. +These finite checks support the algebraic proof; they do not enumerate all +eight-call rational-address words or replace the inherited lemma. + +Credit: woklerx/PR1846 (scalar orbit split), unpaidmoon/PR4119 (span-six +classification), Nick Petalas/PR5231 (48-pool exclusion and the explicit +24-pool question), David Govea/PR720 (arbitrary-target disjoint-subset lemma), +Ali Romman/PR468, eumemic/PR288 and huxint/PR203 (underlying model and methods). +JoyboyBrian/PR5075 supplies the separate cyclic-line closure. Only the +coordinate-isolation application and its checks are new work here. + +Open next question: at four scalar registers, can frame span five permit eight +calls? Its relation rank is three, so the lemma used here cannot decide the +general coupled case. Start by retaining exact chronological endpoints while +classifying three-dimensional off-diagonal pattern spaces. No search of that +new problem was performed in this package. diff --git a/research/coordinate-kernel-span-six-closure/README.md b/research/coordinate-kernel-span-six-closure/README.md new file mode 100644 index 0000000000..3e6a3c5728 --- /dev/null +++ b/research/coordinate-kernel-span-six-closure/README.md @@ -0,0 +1,40 @@ +# 剩余 24 类坐标核结构的八调用不可能性 + +结论：在 PR5231 指定的四寄存器形式阿贝尔 BIT 模型中，剩余 24 类 +坐标核结构均不能在地址张成维数为 6 时，以 8 次秩一调用实现三个 +可逆的 3×3 有理地址矩阵目标。辅助输入任意，辅助输出允许任意对角单项式。 + +核心是一个保留原坐标的 3+1 分块，而不是继续扩大搜索。 +代表结构的三个非坐标投影都在第四行和第四列为零，所有允许的坐标 +投影也保持这一分块。三寄存器子词的关系空间通过补零嵌入原关系空间， +故关系秩至多为 2。由 PR720 第 1—4 节的互不相交子集引理，三块输出的 +地址秩之和不超过该子词调用数；孤立坐标的地址秩不超过其调用数。 +因此总秩 ≤8，与三个满秩目标所需的总秩 ≥9 矛盾。 + +完整英文证明见 PROOF.md，依赖来源及当前主分支快照见 SOURCES.json +。沿用的引理归 David Govea / PR720 及其 PR468、PR288、 +PR203 前驱工作；24/48 分类和题目来源归 woklerx、unpaidmoon 和 +Nick Petalas。新贡献仅为坐标隔离归约及相应检查。 + +运行（仅 Python 标准库，无网络、无第三方依赖）： + +```sh +python3 -I -B verify.py +python3 -I -O -B verify.py +``` + +检查覆盖全部 24 个坐标置换池、96 种数据寄存器位置组合、七字母表中 +长度 1—4 的全部 2800 个形式词、逆元抵消、模型边界反例，以及一个 +地址维数为 6 的九调用正例。有限检查不是八调用全枚举；普遍结论由 +PROOF.md 的推导及明确引用的前驱引理支持。没有重新证明该引理、执行 +原有完整分类程序或进行证明助手核验。 + +结果待维护者审阅；没有修改乘法指数 κ。 +跨度 5 的一般耦合结构与更多辅助寄存器的情况仍不在此结果内。 + +Nicholas Stone，OpenAI Codex 提供实质性证明、代码及整理协助。 +新材料采用 Apache-2.0；前驱来源及其署名已在 PROOF.md 和 SOURCES.json 中注明。 + +## Open next questions + +See TASK.json: frame-span five with one dirty auxiliary remains outside this proof. Its relation rank is three; begin with three-dimensional off-diagonal pattern spaces and exact chronological endpoints. diff --git a/research/coordinate-kernel-span-six-closure/SOURCES.json b/research/coordinate-kernel-span-six-closure/SOURCES.json new file mode 100644 index 0000000000..57482bc9b5 --- /dev/null +++ b/research/coordinate-kernel-span-six-closure/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "13be6ac685845c1ff671f5d26e7166165abd998e", + "files": [ + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "fc3d4ba105e1f097d0d7d051a308281e86ab1446", + "sha256": "66974efdced4083c00025f97d95d83909a226cdf801edb9301c195c6641f6903" + }, + { + "path": "research/flagless-kernel-obstruction/PROOF.md", + "usage": "input", + "git_blob": "78a9e1de94982b8158c50ec403e0d27d91fba59d", + "sha256": "9d45d578ef68bef05da4352d3c46449cffefe6917b42d760bd59fb4595930207" + }, + { + "path": "research/auxiliary-span-six-flag/README.md", + "usage": "input", + "git_blob": "fcb3305be469805d6f6a15eb2c8ca6676af16730", + "sha256": "babb6e44c8ac7640a0cde329b7f6582e72adc2c9307de0d4b5bd2b2510489e1d" + }, + { + "path": "research/three-register-no-target-flag/README.md", + "usage": "input", + "git_blob": "290bfb79db5f4177b8b03bc2027c3848671fac9e", + "sha256": "95d4483da9b19df051c7d13fe290eefb82da019ab4be8e66ad9216199ddda4eb" + } + ] +} diff --git a/research/coordinate-kernel-span-six-closure/TASK.json b/research/coordinate-kernel-span-six-closure/TASK.json new file mode 100644 index 0000000000..81333e4283 --- /dev/null +++ b/research/coordinate-kernel-span-six-closure/TASK.json @@ -0,0 +1,64 @@ +{ + "schema_version": 1, + "task_id": "bit-new-register-model", + "priority_revision": 7, + "base_commit": "13be6ac685845c1ff671f5d26e7166165abd998e", + "original_card": { + "id": "bit-new-register-model", + "question": "Can an explicitly larger or nonabelian register model escape the scoped three-register obstruction?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/bit-three-register-lower-bound/README.md", + "certificates/selected-result.json", + "research/bit-gl3-mixed-targets-length10/README.md", + "docs/research/community-efficient1000-review.md" + ], + "methods": [ + "Construct the smallest exact identity in a newly specified legal operation alphabet.", + "Derive a target-specific relaxation bound for that same explicit alphabet." + ], + "acceptance_gate": "Name the changed hypothesis, all counted roles and a uniform identity; finite column tests alone do not certify it. 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_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read Model section 1 of the three-register bound and identify the exact excluded free operations.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "First compare the alphabet, role count and length with the fully replayed #1974 census and #2027 mixed-root tariff. Identify a changed premise and a legal native implementation; then price one smallest completed instance before searching larger words.", + "bottleneck_link": "A small-width completed saving changes the bit primitive; a finite-address identity alone is insufficient.", + "allowed_variations": [ + "Choose a fixed larger register count or a specified nonabelian operation family." + ], + "scope_change_triggers": [ + "Remaining inside the already-excluded three-register abelian model.", + "Repeating the two-register GL3 census or a covered three-register length without changing a hypothesis; a formal group-algebra word without native conversion is a partial result." + ], + "overlap_terms": [ + "three-register", + "nonabelian", + "group algebra" + ] + }, + "scope_status": "refined", + "actual_scope": "Exclude the remaining 24 coordinate-kernel pools for eight rank-one calls at frame span six in the four-register dirty diagonal-output contract.", + "scope_change_reason": "Explicit user-selected PR5231 handoff, resolved by coordinate 3+1 restriction and the inherited two-relation disjoint-subset lemma.", + "bottleneck_link": "Closes the remaining coordinate-kernel branch without a native supplier or kappa inference.", + "budget_minutes": 60, + "stop_rule": "Stop after the scoped proof, exact finite checks and publication; do not expand to span five.", + "outcome": "negative-result", + "evidence": "PROOF.md and verify.py", + "author": "Nicholas Stone / NicholasStone", + "ai_assistance": "Substantial OpenAI Codex assistance; no independent human or proof-kernel review.", + "open_questions": [ + { + "question": "Can span five admit an eight-call word with one dirty auxiliary?", + "why_it_matters": "Its relation rank three remains outside this reduction.", + "first_step": "Classify three-dimensional pattern spaces while retaining exact chronological endpoints.", + "blocked_by": "The inherited disjoint-subset lemma only covers relation rank at most two." + } + ] +} diff --git a/research/coordinate-kernel-span-six-closure/VALIDATION.json b/research/coordinate-kernel-span-six-closure/VALIDATION.json new file mode 100644 index 0000000000..5bc14ee49d --- /dev/null +++ b/research/coordinate-kernel-span-six-closure/VALIDATION.json @@ -0,0 +1,46 @@ +{ + "python": "3.14.4 (main, Apr 7 2026, 13:13:20) [Clang 21.0.0 (clang-2100.0.123.102)]", + "platform": "macOS-26.5.2-arm64-arm-64bit-Mach-O", + "commands": [ + { + "command": "python3 -I -B verify.py", + "exit_code": 0, + "result": { + "status": "PASS_COORDINATE_KERNEL_CLOSURE", + "pools": 24, + "data_placements": 96, + "formal_words": 2800, + "inverse_controls": 7, + "negative_controls": 4, + "positive_calls": 9, + "positive_address_span": 6, + "inherited_lemma_reproved": false + } + }, + { + "command": "python3 -I -O -B verify.py", + "exit_code": 0, + "result": { + "status": "PASS_COORDINATE_KERNEL_CLOSURE", + "pools": 24, + "data_placements": 96, + "formal_words": 2800, + "inverse_controls": 7, + "negative_controls": 4, + "positive_calls": 9, + "positive_address_span": 6, + "inherited_lemma_reproved": false + } + } + ], + "review": "Single-agent written proof and exact finite checks. No independent human, agent, or proof-kernel review.", + "source_checks": "Three predecessor texts fetched at the pinned canonical commit. Full predecessor suites were not rerun.", + "publication_validation": { + "python": "3.14.4 (main, Apr 7 2026, 13:13:20) [Clang 21.0.0 (clang-2100.0.123.102)]", + "platform": "macOS-26.5.2-arm64-arm-64bit-Mach-O", + "source_pins": "API-fetched canonical commit; all five Git blob IDs recomputed and all declared live input SHA256 values checked.", + "metadata": "Upstream validate(check_pins=False) passed in a local Git fixture. Full canonical-history metadata replay and source-history preflight were not run locally; shell network DNS is unavailable.", + "replay": "Updated source-authenticating verify.py passed normal and optimized direct commands. Hosted Python 3.12 replay is pending.", + "overlap": "Bounded live PR title/body searches; no complete Discussion or arbitrary diff coverage; no exclusivity claim." + } +} diff --git a/research/coordinate-kernel-span-six-closure/VERIFY.json b/research/coordinate-kernel-span-six-closure/VERIFY.json new file mode 100644 index 0000000000..cc40c991a9 --- /dev/null +++ b/research/coordinate-kernel-span-six-closure/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/flagless-kernel-obstruction/PROOF.md", + "research/auxiliary-span-six-flag/README.md", + "research/three-register-no-target-flag/README.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 30, + "checks": "All 24 pools, exact formal block restrictions, inverse and model-boundary controls, and nine-call span-six positive control; authenticate the declared predecessor inputs." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 30, + "checks": "All 24 pools, exact formal block restrictions, inverse and model-boundary controls, and nine-call span-six positive control; authenticate the declared predecessor inputs." + } + ] +} diff --git a/research/coordinate-kernel-span-six-closure/verify.py b/research/coordinate-kernel-span-six-closure/verify.py new file mode 100644 index 0000000000..affd795069 --- /dev/null +++ b/research/coordinate-kernel-span-six-closure/verify.py @@ -0,0 +1,156 @@ +#!/usr/bin/env python3 +"""Exact finite corroboration; the universal claim uses the cited written lemma.""" +import itertools as it +import json +import hashlib +from pathlib import Path +from fractions import Fraction + +def require(ok, message): + if not ok: + raise RuntimeError(message) + +def unpack(n): + return tuple(tuple((n >> (4*i+j)) & 1 for j in range(4)) for i in range(4)) + +def pack(a): + return sum(a[i][j] << (4*i+j) for i in range(4) for j in range(4)) + +def mm(a,b): + n=len(a) + return tuple(tuple(sum(a[i][k]*b[k][j] for k in range(n))%2 + for j in range(n)) for i in range(n)) + +def rank(a, binary=False): + a=[[Fraction(x) for x in row] for row in a] + r=0 + for c in range(len(a[0])): + p=next((i for i in range(r,len(a)) if a[i][c]),None) + if p is None: continue + a[r],a[p]=a[p],a[r] + v=a[r][c] + a[r]=[x/v for x in a[r]] + for i in range(len(a)): + if i!=r: + v=a[i][c] + a[i]=[x-v*y for x,y in zip(a[i],a[r])] + if binary: a[i]=[x%2 for x in a[i]] + r+=1 + if r==len(a): break + return r + +POOL=(0x0003,0x0022,0x0550) +COORD=tuple(1 << (5*i) for i in range(4)) + +def isolated(pool): + return [q for q in range(4) if all( + not a[q][j] and not a[j][q] + for n in pool for a in [unpack(n)] for j in range(4))] + +def permute(n,p): + a=unpack(n); b=[[0]*4 for _ in range(4)] + for i in range(4): + for j in range(4): b[p[i]][p[j]]=a[i][j] + return pack(b) + +# Formal Laurent polynomials: sets of integer exponent tuples over F2. +def add(a,b): return a ^ b +def mul(a,b): + out=set() + for x in a: + for y in b: + z=tuple(u+v for u,v in zip(x,y)) + if z in out: out.remove(z) + else: out.add(z) + return out + +def identity(n,d): + return [[{(0,)*d} if i==j else set() for j in range(n)] for i in range(n)] + +def formal_mm(a,b): + n=len(a); out=[[set() for _ in range(n)] for _ in range(n)] + for i in range(n): + for j in range(n): + for k in range(n): out[i][j]^=mul(a[i][k],b[k][j]) + return out + +def factor(n,a): + d=len(a); m=len(n); f=identity(m,d); coeff={(0,)*d}^{tuple(a)} + for i in range(m): + for j in range(m): + if n[i][j]: f[i][j]^=coeff + return f + +def execute(word,frames,n=4): + out=identity(n,len(frames[0])) + for p,a in zip(word,frames): out=formal_mm(factor(p,a),out) + return out + +def check_split(word,frames): + full=execute(word,frames) + small=execute([tuple(tuple(n[i][j] for j in range(3)) for i in range(3)) + for n in word],frames,3) + total=tuple(sum(a[c] for n,a in zip(word,frames) if n[3][3]) + for c in range(len(frames[0]))) + for i in range(4): + for j in range(4): + expected=small[i][j] if i<3 and j<3 else ({total} if i==j==3 else set()) + require(full[i][j]==expected,'formal block factorization') + +def main(): + package=Path(__file__).resolve().parent + root=package.parent.parent + for row in json.loads((package/"SOURCES.json").read_text())["files"]: + if row["usage"]=="input": + require(hashlib.sha256((root/row["path"]).read_bytes()).hexdigest()==row["sha256"], "source drift: "+row["path"]) + pools={tuple(sorted(permute(n,p) for n in POOL)) for p in it.permutations(range(4))} + require(len(pools)==24,'orbit size') + placements=0 + for pool in pools: + iso=isolated(pool); require(len(iso)==1,'unique isolated coordinate') + q=iso[0]; active=[i for i in range(4) if i!=q] + for n in pool+COORD: + a=unpack(n) + require(mm(a,a)==a and rank(a,True)==1,'idempotent rank') + require(all(not a[q][j] and not a[j][q] for j in active),'off-block entry') + b=tuple(tuple(a[i][j] for j in active) for i in active) + require(rank(b,True)==(0 if n==COORD[q] else 1),'restricted rank') + for data in it.combinations(range(4),3): + # Every possible call split has budget 8, independently of isolated role. + require(sum(3 for _ in data)>8,'target rank contradiction') + placements+=1 + alphabet=[unpack(n) for n in POOL+COORD] + words=0 + for k in range(1,5): + frames=[tuple(int(i==j) for j in range(k)) for i in range(k)] + for word in it.product(alphabet,repeat=k): + check_split(word,frames); words+=1 + # Genuine collisions including inverses; exact full endpoint is identity. + for n in alphabet: + frames=[(1,),(-1,)] + check_split([n,n],frames) + require(execute([n,n],frames)==identity(4,1),'inverse cancellation') + # Negative controls: two old orbits, an off-block rank-one bridge, rank-two update. + transpose=lambda n: pack(tuple(zip(*unpack(n)))) + old=(0x0003,0x0022,0x0dd0) + require(not isolated(old),'48-orbit separation') + require(not isolated(tuple(transpose(n) for n in old)),'transpose separation') + require(not isolated(POOL+(1+(1<<3),)),'off-block bridge rejected') + require(rank(unpack(COORD[0]+COORD[1]),True)==2,'rank-two rejected') + # Nine calls, three full-rank targets, address span exactly six. + units=[tuple(int(k==i*3+j) for k in range(9)) for i,j in + [(0,0),(1,1),(2,2),(0,1),(1,2),(2,0)]] + frames=units[:3]+units[3:]+units[:3] + word=[unpack(COORD[i]) for i in range(3) for _ in range(3)] + out=execute(word,frames) + require(rank(frames)==6,'span-six positive control') + for i in range(4): + target=tuple(sum(frames[k][c] for k in range(9) if k//3==i) for c in range(9)) + for j in range(4): require(out[i][j]==({target} if i==j else set()),'endpoint') + if i<3: require(rank([target[j:j+3] for j in (0,3,6)])==3,'invertible target') + print(json.dumps({'status':'PASS_COORDINATE_KERNEL_CLOSURE', + 'pools':len(pools),'data_placements':placements,'formal_words':words, + 'inverse_controls':7,'negative_controls':4,'positive_calls':9, + 'positive_address_span':6,'inherited_lemma_reproved':False},sort_keys=True)) + +if __name__=='__main__': main()