From 98dbccf3e42da2622b591a86d26f1e459caf29ce Mon Sep 17 00:00:00 2001 From: Chafik Boukhalfa Date: Wed, 14 Oct 2026 16:36:18 +0400 Subject: [PATCH 1/3] Prove fixed-frame obstruction for source-query codes --- .github/workflows/sourcecode-commutant.yml | 39 ++++ research/sourcecode-commutant/EXPECTED.json | 107 ++++++++++ research/sourcecode-commutant/PROOF.md | 101 +++++++++ research/sourcecode-commutant/README.md | 86 ++++++++ research/sourcecode-commutant/SOURCES.json | 39 ++++ research/sourcecode-commutant/verify.py | 215 ++++++++++++++++++++ 6 files changed, 587 insertions(+) create mode 100644 .github/workflows/sourcecode-commutant.yml create mode 100644 research/sourcecode-commutant/EXPECTED.json create mode 100644 research/sourcecode-commutant/PROOF.md create mode 100644 research/sourcecode-commutant/README.md create mode 100644 research/sourcecode-commutant/SOURCES.json create mode 100644 research/sourcecode-commutant/verify.py diff --git a/.github/workflows/sourcecode-commutant.yml b/.github/workflows/sourcecode-commutant.yml new file mode 100644 index 0000000000..ac58cc7d6a --- /dev/null +++ b/.github/workflows/sourcecode-commutant.yml @@ -0,0 +1,39 @@ +name: Source-code fixed-frame commutant + +on: + pull_request: + paths: + - research/sourcecode-commutant/** + - research/community-frontier1042-audit/selected-replay.tar.gz + - .github/workflows/sourcecode-commutant.yml + push: + branches: + - codex/sourcecode-commutant-20261014 + paths: + - research/sourcecode-commutant/** + - .github/workflows/sourcecode-commutant.yml + workflow_dispatch: + +permissions: + contents: read + +jobs: + verify: + runs-on: ubuntu-latest + timeout-minutes: 5 + strategy: + fail-fast: false + matrix: + python: ['3.11', '3.14'] + steps: + - uses: actions/checkout@v4 + - uses: actions/setup-python@v5 + with: + python-version: ${{ matrix.python }} + - name: Replay exact source-derived certificate + run: python -I -O -B research/sourcecode-commutant/verify.py --out "$RUNNER_TEMP/commutant-replay.json" + - uses: actions/upload-artifact@v4 + with: + name: commutant-certificate-${{ matrix.python }} + path: ${{ runner.temp }}/commutant-replay.json + if-no-files-found: error diff --git a/research/sourcecode-commutant/EXPECTED.json b/research/sourcecode-commutant/EXPECTED.json new file mode 100644 index 0000000000..e4548832d7 --- /dev/null +++ b/research/sourcecode-commutant/EXPECTED.json @@ -0,0 +1,107 @@ +{ + "R_L_mismatch": [ + 0, + 0, + "1", + "0" + ], + "compensation_ports": [ + 0, + 7, + 20, + 27, + 36, + 46, + 57, + 111 + ], + "controls": { + "changed_source_archive": true, + "constant_character": true, + "false_determinant": true, + "zeroed_matrix_row": true + }, + "full_rank_characters": 494, + "predecessor_head": "7649d9ceecec949541bec4bbde5929344166ba59", + "predecessor_pr": 1862, + "query_ports": [ + 21, + 37, + 47, + 76, + 81, + 87, + 92, + 110 + ], + "rank_census": [ + { + "characters": 1, + "ranks": [ + 0, + 8 + ] + }, + { + "characters": 8, + "ranks": [ + 7, + 8 + ] + }, + { + "characters": 1, + "ranks": [ + 8, + 0 + ] + }, + { + "characters": 8, + "ranks": [ + 8, + 7 + ] + }, + { + "characters": 494, + "ranks": [ + 8, + 8 + ] + } + ], + "schema": 1, + "scope": "No G=I+ZB with arbitrary address-linear B can satisfy LG=R and commute with diag(C_q), or with the specified output frame diag(F C_q^-1). The written witness extends to every positive tensor power. Does not exclude changed operators, monomial conjugacies, paid transitions, different response spaces, or all zero-native circuits; no supplier or kappa claim.", + "source_archive_sha256": "22c3f4dce4b897a1d423d1388801933e288b6a6b1906cb15e1b16a5eb68db754", + "status": "PASS_SOURCECODE_FIXED_FRAME_COMMUTANT", + "witness": { + "character": 1, + "determinants": [ + "-3/512", + "-3/1024" + ], + "port_minors": [ + [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 12 + ], + [ + 25, + 26, + 27, + 28, + 29, + 30, + 31, + 44 + ] + ] + } +} diff --git a/research/sourcecode-commutant/PROOF.md b/research/sourcecode-commutant/PROOF.md new file mode 100644 index 0000000000..664c671c9e --- /dev/null +++ b/research/sourcecode-commutant/PROOF.md @@ -0,0 +1,101 @@ +# A commuting source code cannot log the complete query at this interface + +The local source encoder in PR1862 is valid and its unchanged replay passes. +This note rules out one shortcut for carrying that code: keeping the same +operator across the individual source output frames. It does not rule out +changed charts, different encoders, paid transports or a complete supplier. +In particular, it is not a lower bound for every zero-native-cost circuit. + +Let V=C^512 be the local nine-bit address space. At port i, write + + C_qi=((1+i)I+(1-i)X_qi)/2, + S_i=F C_qi^-1, F=product_{a=0}^8 C_(2^a). + +The retained source output frame is S=diag(S_i). These are the frames in +PR1862's proof; they must not be replaced by a common full frame. Put +D=diag(C_qi). Its eight-by-112 R, 112-by-eight Z, and eight-port selector L +are those of the pinned PR1862 replay. Every row of Z is a nonzero scalar +multiple of the corresponding row of K=R^T/4: the multiplier is -12 on the +eight compensation ports and one elsewhere. + +Allow B to be an arbitrary eight-by-112 matrix of complex linear operators +on V. Thus this includes address-valued coefficients, not just dyadic scalar +matrices. Consider G=I+ZB. The proposed complete logger condition is + + L G=R tensor I_V. + +There is no such G commuting with D. There is also no such G commuting +with S. Invertibility of G is not needed for this obstruction. + +## One Fourier output character suffices + +In the binary Fourier basis indexed by x in F2^9, C_qi has eigenvalue +i^(qi dot x). Fix output character x=1. For either bit b=0 or b=1, the +rows of Z with qi dot x different from b have rank eight. The checker +gives explicit nonzero minors: + +| Excluded eigenbit b | Eight port rows | Determinant of Z minor | +| --- | --- | --- | +| 0 | 0,1,2,3,4,5,6,12 | -3/512 | +| 1 | 25,26,27,28,29,30,31,44 | -3/1024 | + +For fixed input port j and input character y, let b_j(x,y) in C^8 be the +corresponding coefficients of B. Commutation with D requires + + (i^(qi dot x)-i^(qj dot y)) Z_i b_j(x,y)=0 + +for every row i. The eigenbit qj dot y is either zero or one. Its excluded +rows have rank eight, forcing b_j(x,y)=0. This holds for every j and y. +Consequently G-I has no output at character x. + +For S, its eigenvalue at output character x is i^(|x|-qi dot x), hence +either i or 1. The input eigenvalue of S_j is one of 1,i,-1,-i. If it is +1 or i, one of the same two full-rank row sets forces b_j(x,y)=0. For +either other phase, all rows are excluded; they have rank eight as well. +Again G-I has no output at character x. + +Therefore L G equals L, rather than R, on that output character. This +contradicts the required logger identity: query row zero has coefficient +one at source port zero, while L is supported on the eight selected query +ports and has coefficient zero there. The checker records this coefficient +witness directly from the pinned replay. + +## Tensor powers and scope + +For any positive tensor power t, use output character (1,0,...,0). The +output eigenvalues of each tensor-powered C_qi or S_i still have just the +two phases used above. An arbitrary input character gives one of four +phases. The same two minors, or the entire rank-eight row set, again force +every coefficient b_j at that output character to vanish. The obstruction +therefore persists for arbitrary address-linear B on V^tensor t. + +This concerns commutation with the unchanged output operator. A compiler +could instead change the code under a monomial conjugacy, carry it through +later compulsory native work, use a different response space, or pay for +transport. None of those possibilities is priced or excluded here. The +actual PR1862 local construction and its arbitrary-helper restoration are +not contradicted. + +## Reproduce and credit + +`python3 -I -O -B research/sourcecode-commutant/verify.py` reads the frozen +PR1042 archive directly and checks its compressed and decoded member hashes. +It reconstructs R by a separate exact scalar-prefix replay, checks the disjoint +coordinate minors and RZ=LZ=I, and matches canonical to physical line labels. +No PR1862 implementation, local Git database or network is required at runtime. +The rank and determinant computations use separate integer and rational +elimination methods. All 512 characters are inspected as supplementary evidence: +494 have rank eight in both groups, eight have ranks (7,8), eight have (8,7), and +the two constant characters have (0,8) and (8,0). The single explicit witness +already proves the statement. Four actual mutations reject a constant character, +a zeroed matrix row, a false determinant and a changed source archive. + +PR1862 head 7649d9ceecec949541bec4bbde5929344166ba59 supplies the encoder, +fixed-support response space and pinned historical complex supplier. +Its sources and notices retain the PR1042/PR1094, gauge44, E8, frame and +native-checker lineage. This note adds the fixed-frame commutant obstruction; +it claims no independent human review, complete native supplier or kappa. + +The next useful question is a paid or conjugated chart transition with an +explicit invoice. Requiring the original encoder to commute with the line +frames cannot supply that transition. diff --git a/research/sourcecode-commutant/README.md b/research/sourcecode-commutant/README.md new file mode 100644 index 0000000000..157e35dadf --- /dev/null +++ b/research/sourcecode-commutant/README.md @@ -0,0 +1,86 @@ +# Fixed-frame commutation cannot carry the complete source query + +PR1862 gives a valid local source encoder that stores the eight-coordinate +centre query in existing source fields. Its output fields have different +native frames. This package rules out one way to avoid transporting the +code: an encoder in that fixed response space cannot both retain the full +query and commute with the unchanged line or specified output-frame operator. + +The statement allows arbitrary address-linear operator coefficients, not +only scalar coefficients. It holds for every positive tensor power in the +stated frame model. It does **not** exclude changed operators, monomial +conjugacies, different response spaces, carrying the code through later +native work, or paid chart transitions. It is not a lower bound for every +zero-native-cost circuit. No new supplier or kappa is claimed. + +## Result and evidence + +For G=I+ZB and the eight-port query read L in PR1862, there is no solution to +LG=R that commutes with diag(C_q), or with diag(F C_q^-1). Here B may contain +arbitrary complex linear maps on the address payload. + +One Fourier output character is enough. At x=1, both excluded-eigenvalue +row sets of Z contain an invertible eight-by-eight minor. Their exact +determinants are -3/512 and -3/1024. Commutation forces the whole output +row of B at that character to vanish, contradicting a nonzero R-L coefficient. +[PROOF.md](PROOF.md) supplies the argument and tensor-power extension. + +[EXPECTED.json](EXPECTED.json) is the exact finite certificate. The verifier +derives R directly from the pinned historical scalar program, checks the +source response identities and physical labels, and checks all 512 characters. +There are 494 full-rank cases in both eigenvalue groups. Four actual mutations +fail: a constant character, a zeroed matrix row, a false determinant and a +changed source archive. Checks remain active under Python optimization. + +The finite certificate and written argument are separate from a complete +native replay, global routing, precision, hosting or multiplication theorem. +The specified output-frame model is the contract stated in PR1862; this +package does not re-audit all of that predecessor's native events or phases. + +## Reproduce + +Python 3.11 or newer, standard library only, from the repository root: + +```sh +python3 -I -O -B research/sourcecode-commutant/verify.py +``` + +Expected output: + +```text +PASS_SOURCECODE_FIXED_FRAME_COMMUTANT characters=512 full_rank=494 minors=2 controls=4 no_new_kappa +``` + +The runtime reads only its committed certificate and the frozen input archive +declared in [SOURCES.json](SOURCES.json). It needs no network, Git history, +pending PR implementation or generated predecessor receipt. The dedicated +workflow runs the same check under Python 3.11 and 3.14 and retains receipts. +A local replay is separate from hosted CI completion. + +## Open next questions + +1. **A changed or paid chart transition.** This matters because the local + encoder is useful only if its source data can be restored or its code can + be carried onward. First derive the actual conjugated source map between + two routed charts and price its native transfers. The missing component + is a complete physical access, restoration and precision invoice. +2. **A different response space.** This matters because the obstruction fixes + Z and the eight-port read L. First identify a changed target-support or + query contract and check its excluded-row ranks before searching for a + circuit. No useful alternative response space is constructed here. + +## Credit and review scope + +@aliromman's [PR1862](https://github.com/CrocSwap/integer-mult-bounds/pull/1862), +pinned at 7649d9ceecec949541bec4bbde5929344166ba59, +supplies the encoder, fixed-support response space and exact local construction. +Its valid local result is not contradicted. The E8 unit, PR1042 archive, +PR1094 assembly and retained gauge44/native lineage remain credited to their +authors. The source notices credit icekylinx, Hao Yan / FanPUYen, Jeremy Kothe, +Chafik Boukhalfa, rohanarun and NewBArch for the retained frame and supplier work. +No predecessor code is copied into this package. + +The new contribution is the operator-valued fixed-frame commutant obstruction, +the two-minor witness and a separate source-derived exact verifier. Prepared +for Chafik Boukhalfa with substantial OpenAI Codex assistance. No independent +human review or formal proof assistant is claimed. New material is Apache-2.0. diff --git a/research/sourcecode-commutant/SOURCES.json b/research/sourcecode-commutant/SOURCES.json new file mode 100644 index 0000000000..d6c6378ccd --- /dev/null +++ b/research/sourcecode-commutant/SOURCES.json @@ -0,0 +1,39 @@ +{ + "schema": 1, + "base_commit": "0b1cccf86e2f5132ed286a26ef0a681a495740ea", + "frozen_source_base": "bce54fb3f895cbe5cd4c0eb477c3afeed100190f", + "inputs": [ + { + "path": "research/community-frontier1042-audit/selected-replay.tar.gz", + "git_blob": "6f4dc6fe7631d8aacf8081fcaecf32197181685b", + "sha256": "22c3f4dce4b897a1d423d1388801933e288b6a6b1906cb15e1b16a5eb68db754", + "role": "Original local word, forward program and physical data phases; exact archive/member/payload pins in verify.py." + } + ], + "pending_predecessor": { + "pr": 1862, + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1862", + "head": "7649d9ceecec949541bec4bbde5929344166ba59", + "role": "Source-code response space Z, disjoint minors A/T, query condition LG=R and specified output-frame model. No code imported." + }, + "predecessor_roles": [ + { + "pr": 1042, + "role": "Frozen historical source archive." + }, + { + "pr": 1094, + "role": "Historical assembly also consumes that archive." + }, + { + "pr": 799, + "role": "Retained local supplier lineage credited in archive notices." + }, + { + "pr": 741, + "role": "Retained frame work credited in archive notices." + } + ], + "scope": "Finite exact input/census/minor certificate and written commutant argument only; not a full local native replay, global compiler or supplier audit.", + "disclosure": "New proof, independent scalar-prefix/rank checker and packaging prepared for Chafik Boukhalfa with substantial OpenAI Codex assistance. No independent human review or formal proof assistant." +} diff --git a/research/sourcecode-commutant/verify.py b/research/sourcecode-commutant/verify.py new file mode 100644 index 0000000000..a0308a5845 --- /dev/null +++ b/research/sourcecode-commutant/verify.py @@ -0,0 +1,215 @@ +"""Exact fixed-frame commutant obstruction for PR1862's response space. + +Read frozen original inputs directly; import no pending PR implementation. +This is finite evidence for PROOF.md, not a complete supplier verification. +""" +from collections import Counter +from fractions import Fraction as Q +from hashlib import sha256 +from io import BytesIO +from pathlib import Path +import argparse +import copy +import gzip +import json +import math +import tarfile + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +ARCHIVE = ROOT / 'research/community-frontier1042-audit/selected-replay.tar.gz' +ARCHIVE_SHA = '22c3f4dce4b897a1d423d1388801933e288b6a6b1906cb15e1b16a5eb68db754' +MEMBERS = { + 'slots/local/CANONICAL-WORD.json.gz': ('16bc0ebb04b4be6c0ade74badc6a0c0cdba4215eda86e4ff9f13abf8ecebd219', '4ddb29fb9bc6f27e0c0fbfcf19a2a93a3496ad900d0f6d89059d0305c9576c0c'), + 'slots/local/LOCAL-PROGRAMS.json.gz': ('241fde27d4e43f5a9cb6b128f9f76c5131a53d09f0371676163f914d0b0fef3a', '9f41d53659e9be84e20c661560c5687abbf5cd0660cdecbe01ad5eb29e6b8ee3'), + 't16/global/base/work/complex-nine-native/DATA-PHASES.json': ('c5916ff312678f12aba403847643fbbc29f643acec60bdf836fa56cd3e8251fa', 'c5916ff312678f12aba403847643fbbc29f643acec60bdf836fa56cd3e8251fa'), +} +A = [0, 7, 20, 27, 36, 46, 57, 111] +T = [21, 37, 47, 76, 81, 87, 92, 110] + + +def need(ok, reason): + if not ok: + raise ValueError(reason) + + +def load(raw): + need(sha256(raw).hexdigest() == ARCHIVE_SHA, 'frozen archive hash') + data = {} + with tarfile.open(fileobj=BytesIO(raw), mode='r:gz') as tf: + for name, (packed_hash, payload_hash) in MEMBERS.items(): + matches = [m for m in tf.getmembers() if m.name == name] + need(len(matches) == 1 and matches[0].isfile(), 'unique regular archive member') + packed = tf.extractfile(matches[0]).read() + need(sha256(packed).hexdigest() == packed_hash, 'archive member hash') + payload = gzip.decompress(packed) if name.endswith('.gz') else packed + need(sha256(payload).hexdigest() == payload_hash, 'decoded member hash') + data[name.rsplit('/', 1)[1]] = json.loads(payload) + return data + + +def query_rows(word, program): + n = 2 * word['v'] + word['R'] + need((word['v'], word['R'], word['h']) == (112, 480, 9), 'source geometry') + rows = [{i: Q(1)} for i in range(n + 8)] + found = False + def index(field): + tag, i = field + need(tag in ('L', 'C'), 'field namespace') + return i + (n if tag == 'C' else 0) + for event in program: + if event == ['phase', 'centers']: + found = True + break + if event[0] != 'scalar': + continue + op = event[1] + dst = index(op[1]) + if op[0] == 'clear': + rows[dst] = {} + elif op[0] == 'copy': + rows[dst] = rows[index(op[2])].copy() + elif op[0] == 'scale': + value = Q(op[2], op[3]) + rows[dst] = {j: value * x for j, x in rows[dst].items() if value * x} + else: + need(op[0] == 'add', 'scalar operation') + value = Q(op[3], op[4]) + for j, x in list(rows[index(op[2])].items()): + y = rows[dst].get(j, Q(0)) + value * x + if y: + rows[dst][j] = y + else: + rows[dst].pop(j, None) + need(found and len(word['centers']) == 8, 'centre boundary') + need(all(not any(112 <= j < 224 or j >= n for j in rows[c]) for c in word['centers']), 'source/helper-only query') + return [[rows[c].get(j, Q(0)) for j in range(112)] for c in word['centers']] + + +def product(a, b): + return [[sum(x * y for x, y in zip(row, col)) for col in zip(*b)] for row in a] + + +def determinant(a): + a = [[Q(x) for x in row] for row in a] + result = Q(1) + for j in range(len(a)): + p = next((i for i in range(j, len(a)) if a[i][j]), None) + if p is None: + return Q(0) + if p != j: + a[j], a[p] = a[p], a[j] + result = -result + pivot = a[j][j] + result *= pivot + for i in range(j + 1, len(a)): + coefficient = a[i][j] / pivot + a[i] = [x - coefficient * y for x, y in zip(a[i], a[j])] + return result + + +def integer_row(row): + denominator = math.lcm(*(x.denominator for x in row)) + values = [int(x * denominator) for x in row] + divisor = math.gcd(*values) + return [x // divisor for x in values] if divisor else values + + +def independent_ports(rows, ports): + pivots, chosen = {}, [] + for port in ports: + v = integer_row(rows[port]) + for j, b in sorted(pivots.items()): + if v[j]: + x, y = b[j], v[j] + v = [x * a - y * c for a, c in zip(v, b)] + divisor = math.gcd(*v) + if divisor: + v = [a // divisor for a in v] + if any(v): + pivots[next(j for j, x in enumerate(v) if x)] = v + chosen.append(port) + if len(chosen) == 8: + break + return chosen + + +def validate_witness(witness, q, z): + x = witness['character'] + for bit, ports in enumerate(witness['port_minors']): + need(len(ports) == len(set(ports)) == 8, 'eight distinct minor rows') + need(all(((q[i] & x).bit_count() & 1) != bit for i in ports), 'excluded eigenvalue rows') + d = determinant([z[i] for i in ports]) + need(d != 0 and str(d) == witness['determinants'][bit], 'exact nonzero determinant') + + +def rejected(fn): + try: + fn() + except ValueError: + return True + return False + + +def build(): + raw = ARCHIVE.read_bytes() + data = load(raw) + word = data['CANONICAL-WORD.json.gz'] + q = word['ports'] + physical_q = [row['q'] for row in sorted(data['DATA-PHASES.json']['recipes'], key=lambda r: r['port'])] + need(q == physical_q and len(set(q)) == 112, 'physical input line labels') + r = query_rows(word, data['LOCAL-PROGRAMS.json.gz']['forward']) + rt = list(map(list, zip(*r))) + ident = [[Q(i == j) for j in range(8)] for i in range(8)] + need(product(r, rt) == [[56 * x for x in row] for row in ident], 'R R transpose') + need(len(A) == len(T) == 8 and not set(A) & set(T), 'disjoint selected minors') + for ports in (A, T): + small = [[row[j] for j in ports] for row in r] + need(product(small, list(map(list, zip(*small)))) == [[4 * x for x in row] for row in ident], 'dyadic coordinate minor') + k = [[x / 4 for x in row] for row in rt] + z = [[(-12 if i in A else 1) * x for x in row] for i, row in enumerate(k)] + ell = [[x if j in T else Q(0) for j, x in enumerate(row)] for row in r] + need(product(r, z) == product(ell, z) == ident, 'fixed-support response identities') + census, witness = [], None + for x in range(512): + minors = [independent_ports(z, [i for i, qi in enumerate(q) if ((qi & x).bit_count() & 1) != bit]) for bit in (0, 1)] + ranks = list(map(len, minors)) + census.append(ranks) + if witness is None and ranks == [8, 8]: + witness = dict(character=x, port_minors=minors, determinants=[str(determinant([z[i] for i in ps])) for ps in minors]) + need(witness is not None, 'full-rank character') + validate_witness(witness, q, z) + mismatch = next((i, j, str(r[i][j]), str(ell[i][j])) for i in range(8) for j in range(112) if r[i][j] != ell[i][j]) + bad_character = dict(witness, character=0) + bad_z = copy.deepcopy(z) + bad_z[witness['port_minors'][0][0]] = [Q(0)] * 8 + bad_det = dict(witness, determinants=['0', witness['determinants'][1]]) + mutated_raw = bytes([raw[0] ^ 1]) + raw[1:] + controls = dict(constant_character=rejected(lambda: validate_witness(bad_character, q, z)), zeroed_matrix_row=rejected(lambda: validate_witness(witness, q, bad_z)), false_determinant=rejected(lambda: validate_witness(bad_det, q, z)), changed_source_archive=rejected(lambda: load(mutated_raw))) + need(all(controls.values()), 'mutation controls') + counts = Counter(map(tuple, census)) + return dict(schema=1, status='PASS_SOURCECODE_FIXED_FRAME_COMMUTANT', source_archive_sha256=ARCHIVE_SHA, predecessor_pr=1862, predecessor_head='7649d9ceecec949541bec4bbde5929344166ba59', compensation_ports=A, query_ports=T, rank_census=[dict(ranks=list(rs), characters=n) for rs, n in sorted(counts.items())], full_rank_characters=counts[8, 8], witness=witness, R_L_mismatch=list(mismatch), controls=controls, scope='No G=I+ZB with arbitrary address-linear B can satisfy LG=R and commute with diag(C_q), or with the specified output frame diag(F C_q^-1). The written witness extends to every positive tensor power. Does not exclude changed operators, monomial conjugacies, paid transitions, different response spaces, or all zero-native circuits; no supplier or kappa claim.') + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--record', action='store_true', help='write EXPECTED.json only if absent') + parser.add_argument('--out', type=Path, help='write a new replay receipt') + args = parser.parse_args() + result = build() + raw = (json.dumps(result, indent=2, sort_keys=True) + '\n').encode() + expected = HERE / 'EXPECTED.json' + if args.record: + with expected.open('xb') as f: + f.write(raw) + else: + need(json.loads(expected.read_text(encoding='utf-8')) == result, 'expected exact certificate') + if args.out: + args.out.parent.mkdir(parents=True, exist_ok=True) + with args.out.open('xb') as f: + f.write(raw) + print('PASS_SOURCECODE_FIXED_FRAME_COMMUTANT characters=512 full_rank=494 minors=2 controls=4 no_new_kappa') + + +if __name__ == '__main__': + main() From 4d9fa6016682c910be06e55b1c974d53052aee76 Mon Sep 17 00:00:00 2001 From: Chafik Boukhalfa Date: Wed, 14 Oct 2026 16:50:23 +0400 Subject: [PATCH 2/3] Prove complete endpoint support for invertible full-query encoders --- .github/workflows/sourcecode-commutant.yml | 2 +- research/sourcecode-commutant/EXPECTED.json | 260 +++++++++++++++++++- research/sourcecode-commutant/PROOF.md | 55 ++++- research/sourcecode-commutant/README.md | 51 ++-- research/sourcecode-commutant/SOURCES.json | 20 +- research/sourcecode-commutant/verify.py | 39 ++- 6 files changed, 396 insertions(+), 31 deletions(-) diff --git a/.github/workflows/sourcecode-commutant.yml b/.github/workflows/sourcecode-commutant.yml index ac58cc7d6a..8f50dc9f42 100644 --- a/.github/workflows/sourcecode-commutant.yml +++ b/.github/workflows/sourcecode-commutant.yml @@ -1,4 +1,4 @@ -name: Source-code fixed-frame commutant +name: Source-query endpoint support and frames on: pull_request: diff --git a/research/sourcecode-commutant/EXPECTED.json b/research/sourcecode-commutant/EXPECTED.json index e4548832d7..e863b78eb4 100644 --- a/research/sourcecode-commutant/EXPECTED.json +++ b/research/sourcecode-commutant/EXPECTED.json @@ -71,10 +71,264 @@ ] } ], - "schema": 1, - "scope": "No G=I+ZB with arbitrary address-linear B can satisfy LG=R and commute with diag(C_q), or with the specified output frame diag(F C_q^-1). The written witness extends to every positive tensor power. Does not exclude changed operators, monomial conjugacies, paid transitions, different response spaces, or all zero-native circuits; no supplier or kappa claim.", + "schema": 2, + "scope": "Every invertible full-query encoder has source-change and target-correction supports covering all 112 ports. Endpoint support is not a universal native-child charge. The fixed-Z logger is unique and cannot commute with diag(C_q), or with the specified output frame diag(F C_q^-1), even allowing address-linear coefficients and positive tensor powers. Does not exclude changed/conjugated operators, paid transitions or all zero-native circuits; no supplier or kappa claim.", "source_archive_sha256": "22c3f4dce4b897a1d423d1388801933e288b6a6b1906cb15e1b16a5eb68db754", - "status": "PASS_SOURCECODE_FIXED_FRAME_COMMUTANT", + "status": "PASS_SOURCECODE_SUPPORT_AND_FIXED_FRAME", + "support_cover": { + "Q_minor_determinant": "-256", + "Q_minor_ports": [ + 0, + 7, + 20, + 27, + 36, + 46, + 57, + 111 + ], + "conditional_rowwise_out_and_back_budget": 120, + "minimum_endpoint_support_sum": 112, + "minimum_source_support": 8, + "minimum_target_support": 8, + "missing_premise_counterexamples": { + "no_invertibility": { + "G": [ + [ + 1, + 1, + 1 + ], + [ + 0, + 1, + 0 + ], + [ + 0, + -1, + 0 + ] + ], + "K": [ + [ + 1 + ], + [ + 1 + ], + [ + 1 + ] + ], + "L": [ + [ + 1, + 0, + 0 + ] + ], + "R": [ + [ + 1, + 1, + 1 + ] + ], + "full_query_difference": true, + "invertible": false, + "invertible_J": true, + "logger": true, + "nonzero_K_rows": true, + "source_support": [ + 0, + 2 + ], + "target_support": [ + 0, + 2 + ], + "union": [ + 0, + 2 + ] + }, + "no_query_difference_rank": { + "G": [ + [ + 1, + 0, + 0 + ], + [ + 0, + 1, + 0 + ], + [ + 0, + 0, + 1 + ] + ], + "K": [ + [ + 1 + ], + [ + 1 + ], + [ + 1 + ] + ], + "L": [ + [ + 1, + 1, + 1 + ] + ], + "R": [ + [ + 1, + 1, + 1 + ] + ], + "full_query_difference": false, + "invertible": true, + "invertible_J": true, + "logger": true, + "nonzero_K_rows": true, + "source_support": [], + "target_support": [], + "union": [] + }, + "zero_K_row": { + "G": [ + [ + 1, + 1, + 1 + ], + [ + 0, + 1, + 0 + ], + [ + 0, + 0, + 1 + ] + ], + "K": [ + [ + 1 + ], + [ + 0 + ], + [ + 1 + ] + ], + "L": [ + [ + 1, + 0, + 0 + ] + ], + "R": [ + [ + 1, + 1, + 1 + ] + ], + "full_query_difference": true, + "invertible": true, + "invertible_J": true, + "logger": true, + "nonzero_K_rows": false, + "source_support": [ + 0 + ], + "target_support": [ + 2 + ], + "union": [ + 0, + 2 + ] + } + }, + "nonzero_K_rows": 112, + "query_rank": 8, + "sharp_three_port_example": { + "G": [ + [ + 1, + 1, + 1 + ], + [ + 0, + 1, + 0 + ], + [ + 0, + 0, + 1 + ] + ], + "K": [ + [ + 1 + ], + [ + 1 + ], + [ + 1 + ] + ], + "L": [ + [ + 1, + 0, + 0 + ] + ], + "R": [ + [ + 1, + 1, + 1 + ] + ], + "full_query_difference": true, + "invertible": true, + "invertible_J": true, + "logger": true, + "nonzero_K_rows": true, + "source_support": [ + 0 + ], + "target_support": [ + 1, + 2 + ], + "union": [ + 0, + 1, + 2 + ] + } + }, "witness": { "character": 1, "determinants": [ diff --git a/research/sourcecode-commutant/PROOF.md b/research/sourcecode-commutant/PROOF.md index 664c671c9e..cd1362b7da 100644 --- a/research/sourcecode-commutant/PROOF.md +++ b/research/sourcecode-commutant/PROOF.md @@ -1,7 +1,53 @@ -# A commuting source code cannot log the complete query at this interface +# Endpoint support and fixed-frame obstructions for complete source queries + +## Every invertible full-query encoder has complete endpoint support + +Let R,L be r-by-n matrices, K be n-by-r, and J=I-KR. Assume R-L has full +row rank and every row K_i is nonzero. For any invertible G satisfying +LG=R, put Delta=G-I and H=J Delta. H is precisely the target correction +needed by the input prelude X+=HY, Y=GY before the retained clean-J word. + +The full-query identity gives + + R Delta=RG-R=(R-L)G. + +Its row rank is r. If Delta_i=0 and H_i=0 at a port i, then +K_i R Delta=0. A full-row-rank matrix has no nonzero left annihilator, +so K_i=0, a contradiction. The changed-source and corrected-target row +supports therefore cover all n ports. Also L Delta=R-L gives +rank(Delta)>=r, so at least r source rows change. If J is invertible, +rank(H)=rank(Delta)>=r, so at least r target rows are corrected. + +For an arbitrary finite address payload, tensor R,L,K with its identity +and allow G to be any invertible complex linear map on all port payloads. +The same proof uses full row rank r times the payload dimension. A nonzero +K_i tensor identity cannot annihilate that surjective map. The covering +statement therefore counts whole port blocks and is not restricted to +scalar source codes. + +In the pinned instance n=112 and r=8. The R-L minor on A has nonzero +determinant, all 112 K_i are nonzero, and RK=14I. The latter implies +J^-1=I-KR/13 over C; no circuit division by 13 is proposed. Thus both +supports contain at least eight ports and their union contains all 112. +Since G^-1-I=-Delta G^-1, the source support is also exactly the support +of the inverse's changed rows. + +If a particular rowwise implementation charges at least one rank-one child +for every active target and source endpoint, it pays at least 112. If its +source normalization and return each cost one such child, it pays at least +112+8=120. These are conditional cost comparators. The support theorem +alone is not a universal native-cost lower bound and does not rule out a +compiler carrying updates through compulsory later work. + +Three literal n=3,r=1 examples show that dropping invertibility, full rank +of R-L, or nonzero K rows can invalidate the cover. Each retains the other +premises, including invertibility of J. A fourth valid example attains +|source support|+|target support|=n. The verifier checks all four examples. + +## The fixed-frame commuting shortcut also fails The local source encoder in PR1862 is valid and its unchanged replay passes. -This note rules out one shortcut for carrying that code: keeping the same +The following argument rules out one shortcut for carrying that code: keeping the same operator across the individual source output frames. It does not rule out changed charts, different encoders, paid transports or a complete supplier. In particular, it is not a lower bound for every zero-native-cost circuit. @@ -27,6 +73,11 @@ matrices. Consider G=I+ZB. The proposed complete logger condition is There is no such G commuting with D. There is also no such G commuting with S. Invertibility of G is not needed for this obstruction. +For this particular Z and L, LZ=I. The logger condition already forces +B=R-L, even when B initially allows address-linear operators. Thus there +is only one full-query logger in this fixed response family. The Fourier +argument below verifies its incompatibility with the fixed frames directly. + ## One Fourier output character suffices In the binary Fourier basis indexed by x in F2^9, C_qi has eigenvalue diff --git a/research/sourcecode-commutant/README.md b/research/sourcecode-commutant/README.md index 157e35dadf..ceb230b049 100644 --- a/research/sourcecode-commutant/README.md +++ b/research/sourcecode-commutant/README.md @@ -1,23 +1,37 @@ -# Fixed-frame commutation cannot carry the complete source query +# Full-query source codes require complete endpoint support PR1862 gives a valid local source encoder that stores the eight-coordinate -centre query in existing source fields. Its output fields have different -native frames. This package rules out one way to avoid transporting the -code: an encoder in that fixed response space cannot both retain the full -query and commute with the unchanged line or specified output-frame operator. - -The statement allows arbitrary address-linear operator coefficients, not -only scalar coefficients. It holds for every positive tensor power in the -stated frame model. It does **not** exclude changed operators, monomial -conjugacies, different response spaces, carrying the code through later -native work, or paid chart transitions. It is not a lower bound for every -zero-native-cost circuit. No new supplier or kappa is claimed. +centre query in existing source fields. For any invertible full-query encoder +at this interface, the source fields it changes and the target fields it must +correct together cover all 112 ports. Both endpoints cannot be sparse. + +The support theorem allows arbitrary finite address-linear encoders. A second, +narrower result rules out a fixed-response logger commuting with the unchanged +line or specified output-frame operator, for every positive tensor power. +Neither result excludes changed operators, monomial conjugacies, carrying the +code through later native work, or paid chart transitions. Endpoint support is +not a universal native-child charge. No new supplier or kappa is claimed. ## Result and evidence +Write J=I-KR, Delta=G-I and H=J Delta. The full-query condition LG=R gives +R Delta=(R-L)G. Since R-L has rank eight and G is invertible, this matrix +has full row rank. If both Delta_i and H_i vanish at a port, then +K_i R Delta=0, contradicting the nonzero K_i. Thus the endpoint supports +cover all 112 ports. Each support also contains at least eight ports. + +This supplies a scoped cost control: a model charging one rank-one child per +active endpoint already pays at least 112. Charging a changed source for both +outward and return transfers gives at least 120. Those prices are conditional +rowwise comparators, not a lower bound for all implementations; the old eight +rank-eight centre queries cost 64 in rank mass. A useful implementation must +beat that per-endpoint charging model. + For G=I+ZB and the eight-port query read L in PR1862, there is no solution to LG=R that commutes with diag(C_q), or with diag(F C_q^-1). Here B may contain -arbitrary complex linear maps on the address payload. +arbitrary complex linear maps, although LZ=I already makes the full-query +logger unique: B=R-L. This is a fixed-frame obstruction, not a lower bound +for every zero-native-cost circuit. One Fourier output character is enough. At x=1, both excluded-eigenvalue row sets of Z contain an invertible eight-by-eight minor. Their exact @@ -30,7 +44,9 @@ derives R directly from the pinned historical scalar program, checks the source response identities and physical labels, and checks all 512 characters. There are 494 full-rank cases in both eigenvalue groups. Four actual mutations fail: a constant character, a zeroed matrix row, a false determinant and a -changed source archive. Checks remain active under Python optimization. +changed source archive. Three explicit three-port counterexamples show why +invertibility, rank(R-L) and nonzero K rows are needed. A valid toy attains +the support-cover inequality. Checks remain active under Python optimization. The finite certificate and written argument are separate from a complete native replay, global routing, precision, hosting or multiplication theorem. @@ -48,7 +64,7 @@ python3 -I -O -B research/sourcecode-commutant/verify.py Expected output: ```text -PASS_SOURCECODE_FIXED_FRAME_COMMUTANT characters=512 full_rank=494 minors=2 controls=4 no_new_kappa +PASS_SOURCECODE_SUPPORT_AND_FRAME endpoint_support>=112 characters=512 full_rank=494 mutations=4 premise_controls=3 no_new_kappa ``` The runtime reads only its committed certificate and the frozen input archive @@ -80,7 +96,8 @@ authors. The source notices credit icekylinx, Hao Yan / FanPUYen, Jeremy Kothe, Chafik Boukhalfa, rohanarun and NewBArch for the retained frame and supplier work. No predecessor code is copied into this package. -The new contribution is the operator-valued fixed-frame commutant obstruction, -the two-minor witness and a separate source-derived exact verifier. Prepared +The new contribution is the endpoint-support tradeoff for arbitrary invertible +full-query encoders, the fixed-frame obstruction and its two-minor witness, +and a separate source-derived exact verifier. Prepared for Chafik Boukhalfa with substantial OpenAI Codex assistance. No independent human review or formal proof assistant is claimed. New material is Apache-2.0. diff --git a/research/sourcecode-commutant/SOURCES.json b/research/sourcecode-commutant/SOURCES.json index d6c6378ccd..c49281eafd 100644 --- a/research/sourcecode-commutant/SOURCES.json +++ b/research/sourcecode-commutant/SOURCES.json @@ -14,7 +14,7 @@ "pr": 1862, "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1862", "head": "7649d9ceecec949541bec4bbde5929344166ba59", - "role": "Source-code response space Z, disjoint minors A/T, query condition LG=R and specified output-frame model. No code imported." + "role": "Clean-J source interface, full-query read LG=R, response Z, disjoint minors A/T and specified output-frame model. No pending code imported." }, "predecessor_roles": [ { @@ -34,6 +34,20 @@ "role": "Retained frame work credited in archive notices." } ], - "scope": "Finite exact input/census/minor certificate and written commutant argument only; not a full local native replay, global compiler or supplier audit.", - "disclosure": "New proof, independent scalar-prefix/rank checker and packaging prepared for Chafik Boukhalfa with substantial OpenAI Codex assistance. No independent human review or formal proof assistant." + "scope": "Endpoint-support tradeoff for arbitrary invertible full-query encoders, with exact premise witnesses and three-port controls; fixed-response logger uniqueness and fixed-frame commutant obstruction. No full local native replay, global compiler, universal native-cost lower bound or supplier audit.", + "disclosure": "New proof, independent scalar-prefix/rank checker and packaging prepared for Chafik Boukhalfa with substantial OpenAI Codex assistance. No independent human review or formal proof assistant.", + "overlap": { + "checked_utc": "2026-10-14 12:45 UTC", + "queries": [ + "GitHub PR source code, source-code, commutant", + "GitHub Discussion commutant" + ], + "predecessor_current_head_verified": "7649d9ceecec949541bec4bbde5929344166ba59", + "neighbor": { + "pr": 1756, + "head": "b78859dd6f0d07bf1dda81718a18102bfec9cccb", + "scope_difference": "One read-only source and two clean-cache output ports; excludes multi-source coding. This package treats a full eight-query invertible source code and its endpoint support." + }, + "limits": "Targeted live search, not a novelty proof; no Discussion claim posted." + } } diff --git a/research/sourcecode-commutant/verify.py b/research/sourcecode-commutant/verify.py index a0308a5845..7a79a669e0 100644 --- a/research/sourcecode-commutant/verify.py +++ b/research/sourcecode-commutant/verify.py @@ -1,4 +1,4 @@ -"""Exact fixed-frame commutant obstruction for PR1862's response space. +"""Endpoint-support tradeoff and fixed-frame obstruction for complete queries. Read frozen original inputs directly; import no pending PR implementation. This is finite evidence for PROOF.md, not a complete supplier verification. @@ -151,6 +151,19 @@ def rejected(fn): return False +def endpoint_toy(k, ell, g): + """Literal three-port examples exercise every support-cover premise.""" + r = [[1, 1, 1]] + eye = [[int(i == j) for j in range(3)] for i in range(3)] + delta = [[g[i][j] - eye[i][j] for j in range(3)] for i in range(3)] + kr = product(k, r) + jay = [[eye[i][j] - kr[i][j] for j in range(3)] for i in range(3)] + h = product(jay, delta) + source = [i for i, row in enumerate(delta) if any(row)] + target = [i for i, row in enumerate(h) if any(row)] + return dict(R=r, K=k, L=ell, G=g, logger=product(ell, g) == r, invertible=determinant(g) != 0, full_query_difference=any(a != b for a, b in zip(r[0], ell[0])), nonzero_K_rows=all(any(row) for row in k), invertible_J=determinant(jay) != 0, source_support=source, target_support=target, union=sorted(set(source) | set(target))) + + def build(): raw = ARCHIVE.read_bytes() data = load(raw) @@ -170,6 +183,22 @@ def build(): z = [[(-12 if i in A else 1) * x for x in row] for i, row in enumerate(k)] ell = [[x if j in T else Q(0) for j, x in enumerate(row)] for row in r] need(product(r, z) == product(ell, z) == ident, 'fixed-support response identities') + difference = [[x-y for x, y in zip(a, b)] for a, b in zip(r, ell)] + q_minor = determinant([[row[j] for j in A] for row in difference]) + need(q_minor != 0 and all(any(row) for row in k), 'support-cover hypotheses') + need(product(r, k) == [[14*x for x in row] for row in ident], 'invertible J via RK=14I') + good_g = [[1, 1, 1], [0, 1, 0], [0, 0, 1]] + singular_g = [[1, 1, 1], [0, 1, 0], [0, -1, 0]] + identity_g = [[int(i == j) for j in range(3)] for i in range(3)] + positive = endpoint_toy([[1], [1], [1]], [[1, 0, 0]], good_g) + need(positive['logger'] and positive['invertible'] and positive['union'] == [0, 1, 2], 'sharp support-cover toy') + need(len(positive['source_support']) + len(positive['target_support']) == 3, 'sharp union budget') + premise_examples = dict(no_invertibility=endpoint_toy([[1], [1], [1]], [[1, 0, 0]], singular_g), no_query_difference_rank=endpoint_toy([[1], [1], [1]], [[1, 1, 1]], identity_g), zero_K_row=endpoint_toy([[1], [0], [1]], [[1, 0, 0]], good_g)) + for name, example in premise_examples.items(): + need(example['logger'] and len(example['union']) < 3 and example['invertible_J'], 'genuine missing-premise counterexample '+name) + need(not premise_examples['no_invertibility']['invertible'] and premise_examples['no_invertibility']['full_query_difference'] and premise_examples['no_invertibility']['nonzero_K_rows'], 'invertibility control isolates premise') + need(premise_examples['no_query_difference_rank']['invertible'] and not premise_examples['no_query_difference_rank']['full_query_difference'] and premise_examples['no_query_difference_rank']['nonzero_K_rows'], 'query-difference control isolates premise') + need(premise_examples['zero_K_row']['invertible'] and premise_examples['zero_K_row']['full_query_difference'] and not premise_examples['zero_K_row']['nonzero_K_rows'], 'K-row control isolates premise') census, witness = [], None for x in range(512): minors = [independent_ports(z, [i for i, qi in enumerate(q) if ((qi & x).bit_count() & 1) != bit]) for bit in (0, 1)] @@ -188,19 +217,19 @@ def build(): controls = dict(constant_character=rejected(lambda: validate_witness(bad_character, q, z)), zeroed_matrix_row=rejected(lambda: validate_witness(witness, q, bad_z)), false_determinant=rejected(lambda: validate_witness(bad_det, q, z)), changed_source_archive=rejected(lambda: load(mutated_raw))) need(all(controls.values()), 'mutation controls') counts = Counter(map(tuple, census)) - return dict(schema=1, status='PASS_SOURCECODE_FIXED_FRAME_COMMUTANT', source_archive_sha256=ARCHIVE_SHA, predecessor_pr=1862, predecessor_head='7649d9ceecec949541bec4bbde5929344166ba59', compensation_ports=A, query_ports=T, rank_census=[dict(ranks=list(rs), characters=n) for rs, n in sorted(counts.items())], full_rank_characters=counts[8, 8], witness=witness, R_L_mismatch=list(mismatch), controls=controls, scope='No G=I+ZB with arbitrary address-linear B can satisfy LG=R and commute with diag(C_q), or with the specified output frame diag(F C_q^-1). The written witness extends to every positive tensor power. Does not exclude changed operators, monomial conjugacies, paid transitions, different response spaces, or all zero-native circuits; no supplier or kappa claim.') + return dict(schema=2, status='PASS_SOURCECODE_SUPPORT_AND_FIXED_FRAME', source_archive_sha256=ARCHIVE_SHA, predecessor_pr=1862, predecessor_head='7649d9ceecec949541bec4bbde5929344166ba59', compensation_ports=A, query_ports=T, support_cover=dict(Q_minor_ports=A, Q_minor_determinant=str(q_minor), nonzero_K_rows=112, query_rank=8, minimum_source_support=8, minimum_target_support=8, minimum_endpoint_support_sum=112, conditional_rowwise_out_and_back_budget=120, sharp_three_port_example=positive, missing_premise_counterexamples=premise_examples), rank_census=[dict(ranks=list(rs), characters=n) for rs, n in sorted(counts.items())], full_rank_characters=counts[8, 8], witness=witness, R_L_mismatch=list(mismatch), controls=controls, scope='Every invertible full-query encoder has source-change and target-correction supports covering all 112 ports. Endpoint support is not a universal native-child charge. The fixed-Z logger is unique and cannot commute with diag(C_q), or with the specified output frame diag(F C_q^-1), even allowing address-linear coefficients and positive tensor powers. Does not exclude changed/conjugated operators, paid transitions or all zero-native circuits; no supplier or kappa claim.') def main(): parser = argparse.ArgumentParser(description=__doc__) - parser.add_argument('--record', action='store_true', help='write EXPECTED.json only if absent') + parser.add_argument('--record', action='store_true', help='regenerate the package EXPECTED.json during authoring') parser.add_argument('--out', type=Path, help='write a new replay receipt') args = parser.parse_args() result = build() raw = (json.dumps(result, indent=2, sort_keys=True) + '\n').encode() expected = HERE / 'EXPECTED.json' if args.record: - with expected.open('xb') as f: + with expected.open('wb') as f: f.write(raw) else: need(json.loads(expected.read_text(encoding='utf-8')) == result, 'expected exact certificate') @@ -208,7 +237,7 @@ def main(): args.out.parent.mkdir(parents=True, exist_ok=True) with args.out.open('xb') as f: f.write(raw) - print('PASS_SOURCECODE_FIXED_FRAME_COMMUTANT characters=512 full_rank=494 minors=2 controls=4 no_new_kappa') + print('PASS_SOURCECODE_SUPPORT_AND_FRAME endpoint_support>=112 characters=512 full_rank=494 mutations=4 premise_controls=3 no_new_kappa') if __name__ == '__main__': From 6d455d2d71eb35ecf8e562711e5f719b994fe3f3 Mon Sep 17 00:00:00 2001 From: Chafik Boukhalfa Date: Wed, 14 Oct 2026 17:07:59 +0400 Subject: [PATCH 3/3] Extend frame obstruction to every logger and attain the support bound --- research/sourcecode-commutant/EXPECTED.json | 138 +++++++++++++++++++- research/sourcecode-commutant/PROOF.md | 43 +++++- research/sourcecode-commutant/README.md | 33 +++-- research/sourcecode-commutant/SOURCES.json | 2 +- research/sourcecode-commutant/verify.py | 41 +++++- 5 files changed, 237 insertions(+), 20 deletions(-) diff --git a/research/sourcecode-commutant/EXPECTED.json b/research/sourcecode-commutant/EXPECTED.json index e863b78eb4..5262b1f8e7 100644 --- a/research/sourcecode-commutant/EXPECTED.json +++ b/research/sourcecode-commutant/EXPECTED.json @@ -18,9 +18,26 @@ "controls": { "changed_source_archive": true, "constant_character": true, + "constant_forced_character": true, + "equal_line_labels": true, "false_determinant": true, + "zero_forced_coefficient": true, "zeroed_matrix_row": true }, + "forced_selected_row": { + "character": 2, + "coefficient": "1/2", + "input_port": 2, + "line_eigenbits": [ + 0, + 1 + ], + "output_frame_phases_mod4": [ + 1, + 0 + ], + "output_port": 21 + }, "full_rank_characters": 494, "predecessor_head": "7649d9ceecec949541bec4bbde5929344166ba59", "predecessor_pr": 1862, @@ -71,8 +88,8 @@ ] } ], - "schema": 2, - "scope": "Every invertible full-query encoder has source-change and target-correction supports covering all 112 ports. Endpoint support is not a universal native-child charge. The fixed-Z logger is unique and cannot commute with diag(C_q), or with the specified output frame diag(F C_q^-1), even allowing address-linear coefficients and positive tensor powers. Does not exclude changed/conjugated operators, paid transitions or all zero-native circuits; no supplier or kappa claim.", + "schema": 3, + "scope": "Every invertible full-query encoder has source-change and target-correction supports covering all 112 ports; an explicit algebraic encoder attains the cover with 8 changed source and 104 corrected target ports. Endpoint support is not a universal native-child charge. No logger with this fixed eight-port read L can commute with diag(C_q), or with the specified output frame diag(F C_q^-1), even allowing arbitrary address-linear G and positive tensor powers. The fixed-Z logger is unique; its separate two-minor test agrees. Does not exclude changed/conjugated operators, changed query reads, paid transitions or all zero-native circuits; no supplier or kappa claim.", "source_archive_sha256": "22c3f4dce4b897a1d423d1388801933e288b6a6b1906cb15e1b16a5eb68db754", "status": "PASS_SOURCECODE_SUPPORT_AND_FIXED_FRAME", "support_cover": { @@ -267,6 +284,123 @@ }, "nonzero_K_rows": 112, "query_rank": 8, + "sharp_actual_source_support": [ + 21, + 37, + 47, + 76, + 81, + 87, + 92, + 110 + ], + "sharp_actual_target_support": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 7, + 8, + 9, + 10, + 11, + 12, + 13, + 14, + 15, + 16, + 17, + 18, + 19, + 20, + 22, + 23, + 24, + 25, + 26, + 27, + 28, + 29, + 30, + 31, + 32, + 33, + 34, + 35, + 36, + 38, + 39, + 40, + 41, + 42, + 43, + 44, + 45, + 46, + 48, + 49, + 50, + 51, + 52, + 53, + 54, + 55, + 56, + 57, + 58, + 59, + 60, + 61, + 62, + 63, + 64, + 65, + 66, + 67, + 68, + 69, + 70, + 71, + 72, + 73, + 74, + 75, + 77, + 78, + 79, + 80, + 82, + 83, + 84, + 85, + 86, + 88, + 89, + 90, + 91, + 93, + 94, + 95, + 96, + 97, + 98, + 99, + 100, + 101, + 102, + 103, + 104, + 105, + 106, + 107, + 108, + 109, + 111 + ], + "sharp_example": "G=I+U(R-L), U=K restricted to rows T. RU=LU=I and (R-L)U=0, so G^-1=I-U(R-L). Target correction=(U-K)(R-L). Algebraic example, no complete native invoice.", "sharp_three_port_example": { "G": [ [ diff --git a/research/sourcecode-commutant/PROOF.md b/research/sourcecode-commutant/PROOF.md index cd1362b7da..7c1a95e6fd 100644 --- a/research/sourcecode-commutant/PROOF.md +++ b/research/sourcecode-commutant/PROOF.md @@ -44,7 +44,18 @@ of R-L, or nonzero K rows can invalidate the cover. Each retains the other premises, including invertibility of J. A fourth valid example attains |source support|+|target support|=n. The verifier checks all four examples. -## The fixed-frame commuting shortcut also fails +The cover is also sharp in the actual 112-port instance. Let U equal K on +the eight selected rows T and zero elsewhere, and put Q=R-L. Then + + RU=LU=I, QU=0, G=I+UQ, G^-1=I-UQ, LG=R. + +Exactly eight source rows change. The required target correction is +J UQ=(U-K)Q, zero on T and nonzero on every other row because Q has full +row rank and K_i is nonzero. It has exactly 104 target rows. This is an +algebraic endpoint example, not a complete native implementation or cost +invoice; its sparse source comes with a much wider target correction. + +## The fixed-read commuting shortcut also fails The local source encoder in PR1862 is valid and its unchanged replay passes. The following argument rules out one shortcut for carrying that code: keeping the same @@ -64,6 +75,27 @@ are those of the pinned PR1862 replay. Every row of Z is a nonzero scalar multiple of the corresponding row of K=R^T/4: the multiplier is -12 on the eight compensation ports and one elsewhere. +### A forced row rules out every response space + +Write L=L_T selector_T, where L_T is an invertible eight-by-eight matrix. +For any address-linear G, the logger identity LG=R tensor identity forces + + G_T=L_T^-1 R tensor identity. + +This contains a nonzero off-diagonal coefficient p_ij with i in T, j outside +T, and qi different from qj. Commutation with D would require +p_ij(C_qi-C_qj)=0, which is false. Commutation with S would require +p_ij F(C_qi^-1-C_qj^-1)=0, also false since F is invertible. The verifier +computes the forced coefficient and a Fourier character distinguishing the +two lines. A character (x,0,...,0) distinguishes their positive tensor powers. + +Thus no logger with this fixed eight-port read commutes with D or S. This +statement does not restrict the encoder to the response space Z, and it +does not require invertibility of G. A different, address-valued read or +query contract is outside its scope. + +### Fixed-response uniqueness and a separate two-minor witness + Allow B to be an arbitrary eight-by-112 matrix of complex linear operators on V. Thus this includes address-valued coefficients, not just dyadic scalar matrices. Consider G=I+ZB. The proposed complete logger condition is @@ -120,7 +152,8 @@ phases. The same two minors, or the entire rank-eight row set, again force every coefficient b_j at that output character to vanish. The obstruction therefore persists for arbitrary address-linear B on V^tensor t. -This concerns commutation with the unchanged output operator. A compiler +The general forced-row result and the narrower two-minor result concern +commutation with the unchanged output operator. A compiler could instead change the code under a monomial conjugacy, carry it through later compulsory native work, use a different response space, or pay for transport. None of those possibilities is priced or excluded here. The @@ -140,11 +173,15 @@ elimination methods. All 512 characters are inspected as supplementary evidence: the two constant characters have (0,8) and (8,0). The single explicit witness already proves the statement. Four actual mutations reject a constant character, a zeroed matrix row, a false determinant and a changed source archive. +Three more reject a zero forced coefficient, equal line labels and a +constant distinguishing character. The actual-instance sparse-source +example is checked by RU=LU=I, QU=0 and its complete endpoint supports. PR1862 head 7649d9ceecec949541bec4bbde5929344166ba59 supplies the encoder, fixed-support response space and pinned historical complex supplier. Its sources and notices retain the PR1042/PR1094, gauge44, E8, frame and -native-checker lineage. This note adds the fixed-frame commutant obstruction; +native-checker lineage. This note adds the support tradeoff, its sharp +actual-instance example and the general fixed-read commutant obstruction; it claims no independent human review, complete native supplier or kappa. The next useful question is a paid or conjugated chart transition with an diff --git a/research/sourcecode-commutant/README.md b/research/sourcecode-commutant/README.md index ceb230b049..9d23665152 100644 --- a/research/sourcecode-commutant/README.md +++ b/research/sourcecode-commutant/README.md @@ -6,8 +6,9 @@ at this interface, the source fields it changes and the target fields it must correct together cover all 112 ports. Both endpoints cannot be sparse. The support theorem allows arbitrary finite address-linear encoders. A second, -narrower result rules out a fixed-response logger commuting with the unchanged -line or specified output-frame operator, for every positive tensor power. +narrower result rules out any logger with the fixed eight-port read commuting +with the unchanged line or specified output-frame operator, for every positive +tensor power; it does not require the response space to be Z. Neither result excludes changed operators, monomial conjugacies, carrying the code through later native work, or paid chart transitions. Endpoint support is not a universal native-child charge. No new supplier or kappa is claimed. @@ -27,13 +28,18 @@ rowwise comparators, not a lower bound for all implementations; the old eight rank-eight centre queries cost 64 in rank mass. A useful implementation must beat that per-endpoint charging model. -For G=I+ZB and the eight-port query read L in PR1862, there is no solution to -LG=R that commutes with diag(C_q), or with diag(F C_q^-1). Here B may contain -arbitrary complex linear maps, although LZ=I already makes the full-query -logger unique: B=R-L. This is a fixed-frame obstruction, not a lower bound -for every zero-native-cost circuit. +An explicit algebraic encoder attains the cover with eight changed source +ports and 104 corrected target ports: G=I+U(R-L), where U equals K on the +selected source rows and is zero elsewhere. This sharpness example does not +supply a complete native invoice or a saving. -One Fourier output character is enough. At x=1, both excluded-eigenvalue +The selected read forces G_T=L_T^-1 R for every logger. One nonzero coefficient +between different line labels prevents commutation with diag(C_q) or with +diag(F C_q^-1), even allowing arbitrary address-linear G. In the narrower +G=I+ZB family, LZ=I also makes the logger unique: B=R-L. These are fixed-frame +obstructions, not a lower bound for every zero-native-cost circuit. + +A separate Fourier-rank check corroborates the fixed-Z case. At x=1, both excluded-eigenvalue row sets of Z contain an invertible eight-by-eight minor. Their exact determinants are -3/512 and -3/1024. Commutation forces the whole output row of B at that character to vanish, contradicting a nonzero R-L coefficient. @@ -44,7 +50,9 @@ derives R directly from the pinned historical scalar program, checks the source response identities and physical labels, and checks all 512 characters. There are 494 full-rank cases in both eigenvalue groups. Four actual mutations fail: a constant character, a zeroed matrix row, a false determinant and a -changed source archive. Three explicit three-port counterexamples show why +changed source archive. Three additional forced-row mutations reject a zero +coefficient, equal line labels and a constant distinguishing character. +Three explicit three-port counterexamples show why invertibility, rank(R-L) and nonzero K rows are needed. A valid toy attains the support-cover inequality. Checks remain active under Python optimization. @@ -64,7 +72,7 @@ python3 -I -O -B research/sourcecode-commutant/verify.py Expected output: ```text -PASS_SOURCECODE_SUPPORT_AND_FRAME endpoint_support>=112 characters=512 full_rank=494 mutations=4 premise_controls=3 no_new_kappa +PASS_SOURCECODE_SUPPORT_AND_FRAME endpoint_support>=112 sharp=8+104 characters=512 full_rank=494 mutations=7 premise_controls=3 no_new_kappa ``` The runtime reads only its committed certificate and the frozen input archive @@ -96,8 +104,9 @@ authors. The source notices credit icekylinx, Hao Yan / FanPUYen, Jeremy Kothe, Chafik Boukhalfa, rohanarun and NewBArch for the retained frame and supplier work. No predecessor code is copied into this package. -The new contribution is the endpoint-support tradeoff for arbitrary invertible -full-query encoders, the fixed-frame obstruction and its two-minor witness, +The new contribution is the sharp endpoint-support tradeoff for arbitrary +invertible full-query encoders, the general fixed-read frame obstruction, +the supplementary two-minor witness, and a separate source-derived exact verifier. Prepared for Chafik Boukhalfa with substantial OpenAI Codex assistance. No independent human review or formal proof assistant is claimed. New material is Apache-2.0. diff --git a/research/sourcecode-commutant/SOURCES.json b/research/sourcecode-commutant/SOURCES.json index c49281eafd..6bc5f5491d 100644 --- a/research/sourcecode-commutant/SOURCES.json +++ b/research/sourcecode-commutant/SOURCES.json @@ -34,7 +34,7 @@ "role": "Retained frame work credited in archive notices." } ], - "scope": "Endpoint-support tradeoff for arbitrary invertible full-query encoders, with exact premise witnesses and three-port controls; fixed-response logger uniqueness and fixed-frame commutant obstruction. No full local native replay, global compiler, universal native-cost lower bound or supplier audit.", + "scope": "Sharp endpoint-support tradeoff for arbitrary invertible full-query encoders, with an 8-source/104-target algebraic example and necessary-premise controls; general fixed-selected-read frame obstruction and fixed-Z uniqueness/two-minor corroboration. No full native implementation, global compiler, universal native-cost lower bound or supplier audit.", "disclosure": "New proof, independent scalar-prefix/rank checker and packaging prepared for Chafik Boukhalfa with substantial OpenAI Codex assistance. No independent human review or formal proof assistant.", "overlap": { "checked_utc": "2026-10-14 12:45 UTC", diff --git a/research/sourcecode-commutant/verify.py b/research/sourcecode-commutant/verify.py index 7a79a669e0..dbc52b2701 100644 --- a/research/sourcecode-commutant/verify.py +++ b/research/sourcecode-commutant/verify.py @@ -143,6 +143,17 @@ def validate_witness(witness, q, z): need(d != 0 and str(d) == witness['determinants'][bit], 'exact nonzero determinant') +def validate_selected_row(witness, q): + i, j, x = (witness[key] for key in ('output_port', 'input_port', 'character')) + coefficient = Q(witness['coefficient']) + need(coefficient != 0, 'nonzero forced coefficient') + bits = [(q[p] & x).bit_count() & 1 for p in (i, j)] + need(bits[0] != bits[1], 'different line eigenvalues') + need(witness['line_eigenbits'] == bits, 'line eigenbit receipt') + phases = [(x.bit_count()-b) % 4 for b in bits] + need(witness['output_frame_phases_mod4'] == phases and phases[0] != phases[1], 'different output-frame eigenvalues') + + def rejected(fn): try: fn() @@ -183,7 +194,30 @@ def build(): z = [[(-12 if i in A else 1) * x for x in row] for i, row in enumerate(k)] ell = [[x if j in T else Q(0) for j, x in enumerate(row)] for row in r] need(product(r, z) == product(ell, z) == ident, 'fixed-support response identities') + # Every LG=R forces G_T=L_T^-1 R=K_T R, even for operator-valued G. + kt = [k[i] for i in T] + selected_rows = product(kt, r) + need(product([[row[j] for j in T] for row in ell], kt) == ident, 'inverse selected read') + selected_index, j, value = next((t, j, x) for t, row in enumerate(selected_rows) for j, x in enumerate(row) if j not in T and x) + i = T[selected_index] + character = (q[i] ^ q[j]) & -(q[i] ^ q[j]) + bits = [(q[p] & character).bit_count() & 1 for p in (i, j)] + forced = dict(output_port=i, input_port=j, coefficient=str(value), character=character, line_eigenbits=bits, output_frame_phases_mod4=[(character.bit_count()-b) % 4 for b in bits]) + validate_selected_row(forced, q) + # A sparse-source algebraic logger attains the cover in the actual 112-port instance. + u = [[Q(0)]*8 for _ in range(112)] + for p in T: + u[p] = k[p][:] difference = [[x-y for x, y in zip(a, b)] for a, b in zip(r, ell)] + need(product(r, u) == product(ell, u) == ident, 'sparse-source response') + need(product(difference, u) == [[Q(0)]*8 for _ in range(8)], 'nilpotent sparse-source encoder') + delta = product(u, difference) + response = [[a-b for a, b in zip(ui, ki)] for ui, ki in zip(u, k)] + correction = product(response, difference) + source_support = [i for i, row in enumerate(delta) if any(row)] + target_support = [i for i, row in enumerate(correction) if any(row)] + need(source_support == T and len(target_support) == 104 and not set(source_support)&set(target_support), 'actual-instance sharp endpoint support') + need(sorted(source_support+target_support) == list(range(112)), 'actual-instance cover') q_minor = determinant([[row[j] for j in A] for row in difference]) need(q_minor != 0 and all(any(row) for row in k), 'support-cover hypotheses') need(product(r, k) == [[14*x for x in row] for row in ident], 'invertible J via RK=14I') @@ -215,9 +249,12 @@ def build(): bad_det = dict(witness, determinants=['0', witness['determinants'][1]]) mutated_raw = bytes([raw[0] ^ 1]) + raw[1:] controls = dict(constant_character=rejected(lambda: validate_witness(bad_character, q, z)), zeroed_matrix_row=rejected(lambda: validate_witness(witness, q, bad_z)), false_determinant=rejected(lambda: validate_witness(bad_det, q, z)), changed_source_archive=rejected(lambda: load(mutated_raw))) + same_q = list(q) + same_q[forced['input_port']] = same_q[forced['output_port']] + controls.update(zero_forced_coefficient=rejected(lambda: validate_selected_row(dict(forced, coefficient='0'), q)), equal_line_labels=rejected(lambda: validate_selected_row(forced, same_q)), constant_forced_character=rejected(lambda: validate_selected_row(dict(forced, character=0), q))) need(all(controls.values()), 'mutation controls') counts = Counter(map(tuple, census)) - return dict(schema=2, status='PASS_SOURCECODE_SUPPORT_AND_FIXED_FRAME', source_archive_sha256=ARCHIVE_SHA, predecessor_pr=1862, predecessor_head='7649d9ceecec949541bec4bbde5929344166ba59', compensation_ports=A, query_ports=T, support_cover=dict(Q_minor_ports=A, Q_minor_determinant=str(q_minor), nonzero_K_rows=112, query_rank=8, minimum_source_support=8, minimum_target_support=8, minimum_endpoint_support_sum=112, conditional_rowwise_out_and_back_budget=120, sharp_three_port_example=positive, missing_premise_counterexamples=premise_examples), rank_census=[dict(ranks=list(rs), characters=n) for rs, n in sorted(counts.items())], full_rank_characters=counts[8, 8], witness=witness, R_L_mismatch=list(mismatch), controls=controls, scope='Every invertible full-query encoder has source-change and target-correction supports covering all 112 ports. Endpoint support is not a universal native-child charge. The fixed-Z logger is unique and cannot commute with diag(C_q), or with the specified output frame diag(F C_q^-1), even allowing address-linear coefficients and positive tensor powers. Does not exclude changed/conjugated operators, paid transitions or all zero-native circuits; no supplier or kappa claim.') + return dict(schema=3, status='PASS_SOURCECODE_SUPPORT_AND_FIXED_FRAME', source_archive_sha256=ARCHIVE_SHA, predecessor_pr=1862, predecessor_head='7649d9ceecec949541bec4bbde5929344166ba59', compensation_ports=A, query_ports=T, support_cover=dict(Q_minor_ports=A, Q_minor_determinant=str(q_minor), nonzero_K_rows=112, query_rank=8, minimum_source_support=8, minimum_target_support=8, minimum_endpoint_support_sum=112, conditional_rowwise_out_and_back_budget=120, sharp_actual_source_support=source_support, sharp_actual_target_support=target_support, sharp_example='G=I+U(R-L), U=K restricted to rows T. RU=LU=I and (R-L)U=0, so G^-1=I-U(R-L). Target correction=(U-K)(R-L). Algebraic example, no complete native invoice.', sharp_three_port_example=positive, missing_premise_counterexamples=premise_examples), forced_selected_row=forced, rank_census=[dict(ranks=list(rs), characters=n) for rs, n in sorted(counts.items())], full_rank_characters=counts[8, 8], witness=witness, R_L_mismatch=list(mismatch), controls=controls, scope='Every invertible full-query encoder has source-change and target-correction supports covering all 112 ports; an explicit algebraic encoder attains the cover with 8 changed source and 104 corrected target ports. Endpoint support is not a universal native-child charge. No logger with this fixed eight-port read L can commute with diag(C_q), or with the specified output frame diag(F C_q^-1), even allowing arbitrary address-linear G and positive tensor powers. The fixed-Z logger is unique; its separate two-minor test agrees. Does not exclude changed/conjugated operators, changed query reads, paid transitions or all zero-native circuits; no supplier or kappa claim.') def main(): @@ -237,7 +274,7 @@ def main(): args.out.parent.mkdir(parents=True, exist_ok=True) with args.out.open('xb') as f: f.write(raw) - print('PASS_SOURCECODE_SUPPORT_AND_FRAME endpoint_support>=112 characters=512 full_rank=494 mutations=4 premise_controls=3 no_new_kappa') + print('PASS_SOURCECODE_SUPPORT_AND_FRAME endpoint_support>=112 sharp=8+104 characters=512 full_rank=494 mutations=7 premise_controls=3 no_new_kappa') if __name__ == '__main__':