diff --git a/.github/workflows/sourcecode-commutant.yml b/.github/workflows/sourcecode-commutant.yml new file mode 100644 index 0000000000..8f50dc9f42 --- /dev/null +++ b/.github/workflows/sourcecode-commutant.yml @@ -0,0 +1,39 @@ +name: Source-query endpoint support and frames + +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..5262b1f8e7 --- /dev/null +++ b/research/sourcecode-commutant/EXPECTED.json @@ -0,0 +1,495 @@ +{ + "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, + "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, + "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": 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": { + "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_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": [ + [ + 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": [ + "-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..7c1a95e6fd --- /dev/null +++ b/research/sourcecode-commutant/PROOF.md @@ -0,0 +1,189 @@ +# 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 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 +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. + +### 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 + + 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. + +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 +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. + +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 +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. +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 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 +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..9d23665152 --- /dev/null +++ b/research/sourcecode-commutant/README.md @@ -0,0 +1,112 @@ +# 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. 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 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. + +## 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. + +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. + +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. +[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. 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. + +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_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 +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 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 new file mode 100644 index 0000000000..6bc5f5491d --- /dev/null +++ b/research/sourcecode-commutant/SOURCES.json @@ -0,0 +1,53 @@ +{ + "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": "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": [ + { + "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": "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", + "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 new file mode 100644 index 0000000000..dbc52b2701 --- /dev/null +++ b/research/sourcecode-commutant/verify.py @@ -0,0 +1,281 @@ +"""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. +""" +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 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() + except ValueError: + return True + 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) + 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') + # 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') + 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)] + 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))) + 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=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(): + parser = argparse.ArgumentParser(description=__doc__) + 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('wb') 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_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__': + main()