diff --git a/research/p104-uniform-encoding-gap/PROOF.md b/research/p104-uniform-encoding-gap/PROOF.md new file mode 100644 index 0000000000..18ab29ece0 --- /dev/null +++ b/research/p104-uniform-encoding-gap/PROOF.md @@ -0,0 +1,131 @@ +# Uniform completion does not transfer from E0 to the physical encoding + +## Statement + +Let each port carry a copy of one address space. Write a two-bank state as +`(r, w)`. Let `U_C` apply one address operator `C` on every port of both banks. +Let `D` and `H` be scalar matrices on the ports, with `H` diagonal and +`H^2 = H`. Define the scalar-bank encoding and the physical encoding by + +``` +E0(r, w) = (D r + H w, w), +L(r, w) = (D r + H T w, w), +``` + +where `(T w)_p = T_p w_p` and each `T_p` is an address operator. Let `J0 = I - H` +and + +``` +Pi(r, w) = (J0 r + H w, H r + J0 w). +``` + +`Pi` is the literal N-slot swap. It fixes the J slots. Then: + +1. `U_C E0 = E0 U_C` for every address operator `C`. +2. `U_C L = L U_C` if and only if `C T_p = T_p C` whenever `H_pp = 1`. +3. `U_C Pi = Pi U_C` for every `C`, and therefore + `U_C (Pi L) - (Pi L) U_C = Pi (U_C L - L U_C)`. + The literal-slot encoding commutes with `U_C` exactly when `L` does. + +In the four-point model below, `H = diag(0, 1)`, `T_N = C_{e1}`, and +`C = Z_{e1}` satisfy the scalar identity and fail both physical identities. +The same `Z_{e1}` commutes with `C_{e2}`. Every translation chart commutes with +every other translation chart, so a uniform completion that stays in that +family still passes through `L`. + +This is not an adjacent completed-call pair, not a native bill, and not a +kappa. + +## Proof + +Scalars commute with every address operator, and `U_C` uses the same `C` on +every port. For a scalar matrix `M`, + +``` +U_C (M v)_p = C sum_q M_pq v_q = sum_q M_pq C v_q = (M U_C v)_p. +``` + +`E0` and `Pi` are built from scalar blocks, so both commute with every `U_C`. +That is the positive control for a scalar-bank encoding. + +For the physical encoding the second block is not scalar: + +``` +U_C L(r, w) = (C D r + C H T w, C w), +L U_C(r, w) = (D C r + H T C w, C w). +``` + +`D` and `H` are scalar, so `C D = D C` and `C H = H C`. The states agree if +and only if `H C T w = H T C w` for every `w`, which is +`C T_p = T_p C` on every port with `H_pp = 1`. + +Because `Pi` commutes with `U_C`, + +``` +U_C Pi L - Pi L U_C = Pi U_C L - Pi L U_C = Pi (U_C L - L U_C). +``` + +`Pi` is invertible (`Pi^2 = I`), so it preserves vanishing of the commutator +and does not restore a failing one. + +## Finite witness + +Order the addresses of `(F_2)^2` as `0, e1, e2, e1+e2`. Translation acts by +`(X_u f)(x) = f(x+u)`. The character `Z_{e1}` multiplies by `(-1)^{x·e1}`. +These are the same translation and character operations used to state the +chart formula and the normalization identity in PR #3954, §§3–4. They are +rederived here; that package is not imported. + +The Pauli relation `Z_{e1} X_{e1} = - X_{e1} Z_{e1}` holds, while +`Z_{e1}` commutes with `X_{e2}`, and `X_{e1}` commutes with `X_{e2}`. +The boundary chart of PR #3954 is + +``` +C_u = ((1+i) I + (1-i) X_u) / 2. +``` + +Commutation with `C_u` is equivalent to commutation with the Gaussian-integer +operator `S_u = (1+i) I + (1-i) X_u = 2 C_u`, because the commutator scales by +the central integer 2. Direct multiplication gives + +``` +[Z_{e1}, S_{e1}] = + [ 0 2-2i 0 0 ] + [-2+2i 0 0 0 ] + [ 0 0 0 2-2i ] + [ 0 0 -2+2i 0 ]. +``` + +The `(0,1)` entry `2-2i` is the recorded witness. Thus `Z_{e1}` does not +commute with `C_{e1}`. It does commute with `C_{e2}`. + +Take two ports, `H = diag(0, 1)`, and the non-scalar integer matrix + +``` +D = [[1, 1], [1, 2]]. +``` + +The general identity already covers every scalar-entry `D`, including the +104-port pivot matrix of PR #3954. This check uses the 2×2 matrix above so +that the certificate does not depend on reloading that pivot. Both verifiers +rebuild the operators and test: + +- `U_Z` commutes with `E0`; +- `U_Z` fails to commute with `L` and with `Pi L`, on 4 of the 16 basis + directions, and `Pi` carries one commutator to the other; +- `U_{S_{e1}}` commutes with `L` and with `Pi L`; +- replacing the N-port chart by `S_{e2}` restores commutation with `U_Z`. + +## What this does not decide + +A uniform completion whose operator lies in the algebra generated by the +translations still commutes with every `C_u`, hence with `L` and `Pi L`. +The obstruction bites only when the common operator fails to commute with an +active port chart. PR #3954's positive control says "any" common operator, +and the reason it gives is that the encoding coefficients are scalars. That +reason applies to `E0` and not to `L` or `Pi L`. + +The sentence does not by itself produce a matched physical caller. This note +does not construct the adjacent completed-call pair requested by discussion +#1166 comment 19034066, and it does not price owners, orientation, width, or +tape. diff --git a/research/p104-uniform-encoding-gap/README.md b/research/p104-uniform-encoding-gap/README.md new file mode 100644 index 0000000000..e46a73f13d --- /dev/null +++ b/research/p104-uniform-encoding-gap/README.md @@ -0,0 +1,68 @@ +# Uniform completion against the physical P104 encoding + +**Scoped commutation obstruction. No new κ and no selected-frontier change.** +Selected κ stays `0.001672660197076918`. + +PR #3954 shows that a common address operator commutes with the scalar-bank +encoding `E0`, because that encoding's blocks are scalar matrices. The handoff +in discussion #1166 comment 19034066 records the consequence that was left +open: uniform completed transforms commute with scalar bank encodings, and +that fact alone does not give a matched physical caller. The requested +construction is an adjacent completed-call pair. This package does not build +that pair. + +It separates the scalar encoding from the physical one. For + +``` +E0(r, w) = (D r + H w, w), L(r, w) = (D r + H T w, w), +``` + +`U_C` commutes with `E0` for every address operator `C`, and commutes with `L` +exactly when `C` commutes with every active port chart `T_p`. The literal slot +swap `Pi` commutes with every `U_C`, so `Pi L` fails for the same operators as +`L`. On the four-point translation model, `Z_{e1}` commutes with `E0` and with +`C_{e2}`, and it fails for `C_{e1}` on both `L` and `Pi L`. The address +commutator entry is `2-2i`. + +Charts generated by translations still commute with each other, so a uniform +completion that stays in that family is not blocked here. The written argument +is in [PROOF.md](PROOF.md). + +## Reproduce + +CPython 3.12, standard library, from the repository root: + +```sh +python3.12 -B research/p104-uniform-encoding-gap/verify.py +python3.12 -B research/p104-uniform-encoding-gap/independent.py +python3.12 -B research/p104-uniform-encoding-gap/test_verify.py +python3.12 -B scripts/research_package.py --package research/p104-uniform-encoding-gap +``` + +`verify.py` multiplies the 16×16 Gaussian-integer matrices. +`independent.py` does not import it; it applies the same maps to vectors. +`test_verify.py` rejects an even-direction chart offered as an obstruction. + +## Open next questions + +1. Which operators does one actual completed P104 call apply uniformly? If + they all lie in the translation algebra, this commutator does not block + that call, and the adjacent-pair search has to move elsewhere. The first + step is to read the retained caller at one completed role and name the + operator. That caller text is not pinned in this package. +2. The adjacent completed-call pair from comment 19034066 is untouched. Its + entrance and exit still have to match on every data and helper role, with + a physical intertwiner and a full bill. This commutation gap does not + supply that pair, and it does not prove that no such pair exists. + +## Credit + +The scalar-bank positive control, the chart formula `C_u`, the literal swap +`Pi`, and the normalization character are from Clear1nsight, PR #3954, head +`f1e2839819959cd0534d008be91ed5b79ec55a6a`, retaining the P104 and native +lineage named there (Rohan Arun, Chafik Boukhalfa, Adam Gall, and the authors +credited in that package). This package rederives the four-point translation +and character relations and does not import that code. + +Prepared by unpaidmoon with substantial Cursor Grok assistance. No independent +human review is claimed. Apache-2.0. diff --git a/research/p104-uniform-encoding-gap/SOURCES.json b/research/p104-uniform-encoding-gap/SOURCES.json new file mode 100644 index 0000000000..a604c6a640 --- /dev/null +++ b/research/p104-uniform-encoding-gap/SOURCES.json @@ -0,0 +1,18 @@ +{ + "schema_version": 1, + "base_commit": "bb4bccbf42844d2801487450727c2f63e10d1d0f", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81", + "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "67f085acd86acd7d4e03922d9cf4b26bca66fed5", + "sha256": "47b42433f5a85809a3aadd29c2c339da2c6ed728e4f7762df6b88bccb7874cf0" + } + ] +} diff --git a/research/p104-uniform-encoding-gap/TASK.json b/research/p104-uniform-encoding-gap/TASK.json new file mode 100644 index 0000000000..9985aa7367 --- /dev/null +++ b/research/p104-uniform-encoding-gap/TASK.json @@ -0,0 +1,94 @@ +{ + "schema_version": 1, + "task_id": "p104-side-correction", + "priority_revision": 6, + "base_commit": "bb4bccbf42844d2801487450727c2f63e10d1d0f", + "original_card": { + "id": "p104-side-correction", + "question": "Can the proposed P104 joint endpoint flags be realized by a chronological correction program with coefficients, dirty restoration and an affordable complete bill?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/p104-native-channel/README.md", + "research/p104-native-channel/PROOF.md", + "docs/research/community-efficient1000-review.md", + "research/p104-joint-unit-flags/README.md" + ], + "methods": [ + "Construct one side-correction word at an explicit chronological cut with the needed frames still available.", + "Derive a lower bound on the side correction and hosting costs that decides whether this channel can beat the selected budget." + ], + "acceptance_gate": "An exact arbitrary-input identity, source/target frame availability and restoration at the chosen cut, plus the complete channel+correction+idle/hosting bill or an explicit favorable bound. The native channel alone is not a supplier. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read the revision-6 family record and #2981 static joint flags, alongside the reviewed #1991 channel. #2981 is an author-checked source archive, not an independently validated executable correction or a refutation of program-level lifetime floors.", + "scope": "Source-bound orientation only. Read the named package and review before relying on its local evidence; this command is not its replay or supplier admission." + }, + "first_experiment": "After checking live handoffs, pin one named collection from #2981 and attach acquisition/delivery times, source dependencies and coefficient requirements. Test legal access and arbitrary dirty restoration; price any completion against the full channel/endpoint/hosting allowance. Stop with the exact missing implication or a scoped counterexample rather than expanding the static cover census.", + "bottleneck_link": "Completing an already realized changed channel tests a concrete construction opportunity, instead of refining the incumbent packing. A positive local result still needs global and all-size admission.", + "allowed_variations": [ + "One correction factorization, one chronological cut, or one explicit hosting obstruction.", + "A changed correction schedule with an updated full bill and native frame contract." + ], + "scope_change_triggers": [ + "Recompiling the already certified low-rank channel without closing a new obligation.", + "Treating a pending ancestor, local histogram or unpriced side correction as an admitted global supplier.", + "Repeating a correction or physical conversion already supplied by a pending follow-up without adding independent coverage or a different unresolved obligation.", + "Repeating the 208-flag static matching or calling a static nested cover a chronological correction program. Independent audit of that certificate is distinct and remains useful." + ], + "overlap_terms": [ + "P104", + "I-G/2", + "side correction", + "native channel", + "1972", + "1991", + "2586", + "endpoint transport", + "physical dual", + "relay composition", + "2981", + "joint unit flags", + "acquisition delivery", + "static nesting" + ], + "existing_checks": [ + { + "scope": "PR #2981 reports static joint endpoint flags and a matching of 208 departure and arrival flags; archival intake is not independent verification.", + "evidence": "research/p104-joint-unit-flags/README.md", + "remaining": "Independent flag check and a chronological coefficient program with dirty restoration and a complete cost.", + "status": "author-checked", + "source_commit": "3d24b92d8ba057b57cb2d480170ec407520e6882", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Prove that a uniform address operator commutes with the scalar-bank encoding E0 for every operator, and commutes with the physical encoding L and the literal encoding Pi L exactly when it commutes with every active port chart. Witness the failure at Z_e1 against C_e1. Do not construct the adjacent completed-call pair.", + "scope_change_reason": "The catalogue card asks for a chronological side-correction word. Discussion #1166 comment 19034066 instead asks for one adjacent completed-call pair. Fewer than 25 eligible handoffs remained, and the session index selected that handoff for a distinct piece. This piece audits the scalar-bank commutation shortcut named in the same handoff, which is not the pair construction.", + "bottleneck_link": "A joint physical encoding is one route toward a changed complex supplier. Quoting the scalar-bank commutation as if it were already that encoding would skip an unpaid intertwiner. The obstruction removes that shortcut and leaves the adjacent pair open.", + "budget_minutes": 60, + "stop_rule": "Stop once the commutation identity and the four-point witness are checked. Do not search for an adjacent pair or price a native caller in this package.", + "outcome": "completed", + "evidence": "PROOF.md gives the block identity. verify.py and independent.py agree on the witness [Z_e1, S_e1]_(0,1)=2-2i, with physical and literal defects of support 4, and on the commuting controls E0, S_e1 against itself, and S_e2 against Z_e1.", + "author": "unpaidmoon", + "ai_assistance": "Cursor Grok 4.7, including the matrix and vector checkers.", + "open_questions": [ + { + "question": "Which operators does one actual completed P104 call apply uniformly?", + "why_it_matters": "Translation charts commute with each other, so this gap blocks only a uniform operator outside that family. A legal completed call might never leave the family.", + "first_step": "Name the operator on one completed role of the retained caller and test its commutator with one active port chart.", + "blocked_by": "The caller source cited by PR #3954 is not pinned in this package." + }, + { + "question": "Does any adjacent completed-call pair match encoded exit to encoded entrance on every data and helper role?", + "why_it_matters": "That is the construction requested by comment 19034066. This commutation gap does not build it and does not prove it is impossible.", + "first_step": "Pin one ordered pair of completed calls and compare one data role and one helper role before writing an intertwiner.", + "blocked_by": "No matched physical caller was supplied by PR #3954, and this package does not search for one." + } + ] +} diff --git a/research/p104-uniform-encoding-gap/VERIFY.json b/research/p104-uniform-encoding-gap/VERIFY.json new file mode 100644 index 0000000000..0a4be90139 --- /dev/null +++ b/research/p104-uniform-encoding-gap/VERIFY.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "16x16 Gaussian commutators: E0 commutes, L and Pi L fail for Z_e1, translation and even-direction controls commute." + }, + { + "argv": [ + "{python}", + "-B", + "{package}/independent.py" + ], + "timeout_seconds": 60, + "checks": "Vector replay with no import of verify.py; same witness column and basis miss counts." + }, + { + "argv": [ + "{python}", + "-B", + "{package}/test_verify.py" + ], + "timeout_seconds": 60, + "checks": "Rejects the even-direction chart as an obstruction and accepts the odd-direction witness." + } + ] +} diff --git a/research/p104-uniform-encoding-gap/independent.py b/research/p104-uniform-encoding-gap/independent.py new file mode 100644 index 0000000000..8fa6bc89d0 --- /dev/null +++ b/research/p104-uniform-encoding-gap/independent.py @@ -0,0 +1,175 @@ +#!/usr/bin/env python3 +"""Vector-form replay of the uniform-encoding gap. Does not import verify.py.""" +from __future__ import annotations + +ZERO = (0, 0) +ONE = (1, 0) +I = (0, 1) + + +def gadd(a, b): + return (a[0] + b[0], a[1] + b[1]) + + +def gsub(a, b): + return (a[0] - b[0], a[1] - b[1]) + + +def gmul(a, b): + return (a[0] * b[0] - a[1] * b[1], a[0] * b[1] + a[1] * b[0]) + + +def zvec(): + return tuple(ONE if (addr & 1) == 0 else (-1, 0) for addr in range(4)) + + +def apply(matrix_cols, vector): + """matrix_cols[j] is the image of basis vector j.""" + out = [ZERO] * 4 + for j, coef in enumerate(vector): + if coef == ZERO: + continue + for i in range(4): + out[i] = gadd(out[i], gmul(coef, matrix_cols[j][i])) + return tuple(out) + + +def translation_cols(shift): + cols = [] + for addr in range(4): + image = [ZERO] * 4 + image[addr ^ shift] = ONE + cols.append(tuple(image)) + return cols + + +def chart_cols(shift): + """Columns of S_u = (1+i)I + (1-i) X_u.""" + translated = translation_cols(shift) + cols = [] + for addr in range(4): + image = [ZERO] * 4 + image[addr] = gadd(ONE, I) + for i in range(4): + image[i] = gadd(image[i], gmul(gsub(ONE, I), translated[addr][i])) + cols.append(tuple(image)) + return cols + + +def character_cols(): + signs = zvec() + return tuple(tuple(signs[i] if i == j else ZERO for i in range(4)) for j in range(4)) + + +def matvec(cols, vector): + return apply(cols, vector) + + +def commutator_on(cols_left, cols_right, vector): + return tuple( + gsub(a, b) + for a, b in zip( + matvec(cols_left, matvec(cols_right, vector)), + matvec(cols_right, matvec(cols_left, vector)), + ) + ) + + +# State is (r_J, r_N, w_J, w_N), each an address 4-tuple. +BASIS = tuple(tuple(ONE if i == addr else ZERO for i in range(4)) for addr in range(4)) +D = ((1, 1), (1, 2)) + + +def scale_addr(coef, vector): + return tuple(gmul((coef, 0), entry) for entry in vector) + + +def add_addr(left, right): + return tuple(gadd(a, b) for a, b in zip(left, right)) + + +def sub_addr(left, right): + return tuple(gsub(a, b) for a, b in zip(left, right)) + + +def zero_addr(): + return (ZERO, ZERO, ZERO, ZERO) + + +def uniform(cols, state): + return tuple(matvec(cols, slot) for slot in state) + + +def physical(chart, state): + r_j, r_n, w_j, w_n = state + # r' = D r + (0, T w_N), w' = w. + out_j = add_addr(scale_addr(D[0][0], r_j), scale_addr(D[0][1], r_n)) + out_n = add_addr(scale_addr(D[1][0], r_j), scale_addr(D[1][1], r_n)) + out_n = add_addr(out_n, matvec(chart, w_n)) + return (out_j, out_n, w_j, w_n) + + +def scalar(state): + r_j, r_n, w_j, w_n = state + out_j = add_addr(scale_addr(D[0][0], r_j), scale_addr(D[0][1], r_n)) + out_n = add_addr( + add_addr(scale_addr(D[1][0], r_j), scale_addr(D[1][1], r_n)), + w_n, + ) + return (out_j, out_n, w_j, w_n) + + +def permute(state): + r_j, r_n, w_j, w_n = state + return (r_j, w_n, w_j, r_n) + + +def states_equal(left, right): + return all(a == b for pair in zip(left, right) for a, b in zip(pair[0], pair[1])) + + +def basis_states(): + for slot in range(4): + for addr in range(4): + state = [zero_addr(), zero_addr(), zero_addr(), zero_addr()] + state[slot] = BASIS[addr] + yield tuple(state) + + +def difference(apply_encoding, cols): + misses = 0 + for state in basis_states(): + left = uniform(cols, apply_encoding(state)) + right = apply_encoding(uniform(cols, state)) + if not states_equal(left, right): + misses += 1 + return misses + + +def main(): + zeta = character_cols() + chart_e1 = chart_cols(1) + chart_e2 = chart_cols(2) + if difference(scalar, zeta) != 0: + raise ValueError("independent scalar encoding failed") + physical_misses = difference(lambda state: physical(chart_e1, state), zeta) + even_misses = difference(lambda state: physical(chart_e2, state), zeta) + literal_misses = difference(lambda state: permute(physical(chart_e1, state)), zeta) + self_misses = difference(lambda state: physical(chart_e1, state), chart_e1) + if physical_misses == 0 or literal_misses == 0: + raise ValueError("independent physical obstruction vanished") + if even_misses != 0 or self_misses != 0: + raise ValueError("independent commuting controls failed") + column = commutator_on(zeta, chart_e1, BASIS[0]) + if column != (ZERO, (-2, 2), ZERO, ZERO): + raise ValueError("independent address column changed: " + repr(column)) + print( + "PASS_P104_UNIFORM_ENCODING_GAP_INDEPENDENT" + f" scalar_misses=0 physical_basis_misses={physical_misses}" + f" literal_basis_misses={literal_misses} even_misses=0 self_misses=0" + " address_column0=0,-2+2i no_new_kappa" + ) + + +if __name__ == "__main__": + main() diff --git a/research/p104-uniform-encoding-gap/test_verify.py b/research/p104-uniform-encoding-gap/test_verify.py new file mode 100644 index 0000000000..0feafda098 --- /dev/null +++ b/research/p104-uniform-encoding-gap/test_verify.py @@ -0,0 +1,51 @@ +#!/usr/bin/env python3 +"""Failure controls for the uniform-encoding gap. Loads verify.py by path.""" +import importlib.util +from pathlib import Path + +_PATH = Path(__file__).resolve().parent / "verify.py" +_SPEC = importlib.util.spec_from_file_location("p104_uniform_encoding_gap_verify", _PATH) +gap = importlib.util.module_from_spec(_SPEC) +_SPEC.loader.exec_module(gap) + + +def require(condition, reason): + if not condition: + raise ValueError(reason) + + +def nnz_commutator(encoding, operator): + return gap.nnz(gap.commutator(gap.lift_uniform(operator), encoding)) + + +def main(): + facts = gap.report() + require(facts["physical_defect_nnz"] == 4, "witness support changed") + require(facts["address_commutator_01"] == (2, -2), "recorded address entry changed") + identity = gap.eye(gap.ADDR) + zeta = gap.character_e1() + scalar = gap.encoding([identity, identity], gap.SCALAR_D) + physical = gap.encoding([identity, gap.chart(1)], gap.SCALAR_D) + even = gap.encoding([identity, gap.chart(2)], gap.SCALAR_D) + require(nnz_commutator(scalar, zeta) == 0, "scalar control") + require(nnz_commutator(physical, zeta) != 0, "physical witness") + require(nnz_commutator(even, zeta) == 0, "even-direction control") + require(nnz_commutator(physical, identity) == 0, "identity completion must commute") + + def assert_obstruction(port_chart): + candidate = gap.encoding([identity, port_chart], gap.SCALAR_D) + if nnz_commutator(candidate, zeta) == 0: + raise ValueError("expected an obstruction") + + raised = False + try: + assert_obstruction(gap.chart(2)) + except ValueError as exc: + raised = "expected an obstruction" in str(exc) + require(raised, "the even-direction chart must fail an obstruction claim") + assert_obstruction(gap.chart(1)) + print("PASS_P104_UNIFORM_ENCODING_GAP_TESTS groups=3") + + +if __name__ == "__main__": + main() diff --git a/research/p104-uniform-encoding-gap/verify.py b/research/p104-uniform-encoding-gap/verify.py new file mode 100644 index 0000000000..ffd8166083 --- /dev/null +++ b/research/p104-uniform-encoding-gap/verify.py @@ -0,0 +1,210 @@ +#!/usr/bin/env python3 +"""Uniform completion commutes with E0 and not with the physical encodings. + +Separate from PR #3954's checker. No predecessor module is imported. +""" +from __future__ import annotations + +ZERO = (0, 0) +ONE = (1, 0) +I = (0, 1) + +# Two ports, J then N. Address space is the four-point square {0, e1, e2, e1+e2}. +PORTS = 2 +ADDR = 4 +DIM = 2 * PORTS * ADDR + + +def gadd(a, b): + return (a[0] + b[0], a[1] + b[1]) + + +def gsub(a, b): + return (a[0] - b[0], a[1] - b[1]) + + +def gmul(a, b): + return (a[0] * b[0] - a[1] * b[1], a[0] * b[1] + a[1] * b[0]) + + +def mm(left, right): + size = len(left) + out = [[ZERO] * size for _ in range(size)] + for i in range(size): + for k in range(size): + if left[i][k] == ZERO: + continue + for j in range(size): + if right[k][j] == ZERO: + continue + out[i][j] = gadd(out[i][j], gmul(left[i][k], right[k][j])) + return out + + +def msub(left, right): + return [[gsub(left[i][j], right[i][j]) for j in range(len(left))] for i in range(len(left))] + + +def eye(size): + return [[ONE if i == j else ZERO for j in range(size)] for i in range(size)] + + +def nnz(matrix): + return sum(entry != ZERO for row in matrix for entry in row) + + +def slot(bank, port, addr): + return (bank * PORTS + port) * ADDR + addr + + +def translation(shift): + matrix = [[ZERO] * ADDR for _ in range(ADDR)] + for addr in range(ADDR): + # (X_u f)(x) = f(x+u). + matrix[addr][addr ^ shift] = ONE + return matrix + + +def character_e1(): + """Multiplication by (-1)^{x·e1}.""" + matrix = [[ZERO] * ADDR for _ in range(ADDR)] + for addr in range(ADDR): + matrix[addr][addr] = ONE if (addr & 1) == 0 else (-1, 0) + return matrix + + +def chart(shift): + """S_u = (1+i)I + (1-i) X_u = 2 C_u, with C_u the PR #3954 boundary chart.""" + return [ + [ + gadd(gmul(gadd(ONE, I), eye(ADDR)[i][j]), gmul(gsub(ONE, I), translation(shift)[i][j])) + for j in range(ADDR) + ] + for i in range(ADDR) + ] + + +def lift_uniform(operator): + matrix = [[ZERO] * DIM for _ in range(DIM)] + for bank in range(2): + for port in range(PORTS): + for i in range(ADDR): + for j in range(ADDR): + matrix[slot(bank, port, i)][slot(bank, port, j)] = operator[i][j] + return matrix + + +def encoding(port_charts, scalar_d): + """L(r, w) = (D r + H T w, w), H = diag(0, 1). + + port_charts[p] is the address operator T_p. The J chart is stored and then + killed by H, matching the block H T. + """ + matrix = [[ZERO] * DIM for _ in range(DIM)] + for port in range(PORTS): + for addr in range(ADDR): + matrix[slot(1, port, addr)][slot(1, port, addr)] = ONE + for row in range(PORTS): + for col in range(PORTS): + coef = (scalar_d[row][col], 0) + if coef == ZERO: + continue + for addr in range(ADDR): + target = slot(0, row, addr) + source = slot(0, col, addr) + matrix[target][source] = gadd(matrix[target][source], coef) + chart_n = port_charts[1] + for i in range(ADDR): + for j in range(ADDR): + matrix[slot(0, 1, i)][slot(1, 1, j)] = gadd( + matrix[slot(0, 1, i)][slot(1, 1, j)], chart_n[i][j] + ) + return matrix + + +def literal_pi(): + """Pi swaps the N slot between the two banks and fixes J.""" + matrix = [[ZERO] * DIM for _ in range(DIM)] + for addr in range(ADDR): + matrix[slot(0, 0, addr)][slot(0, 0, addr)] = ONE + matrix[slot(0, 1, addr)][slot(1, 1, addr)] = ONE + matrix[slot(1, 0, addr)][slot(1, 0, addr)] = ONE + matrix[slot(1, 1, addr)][slot(0, 1, addr)] = ONE + return matrix + + +def commutator(left, right): + return msub(mm(left, right), mm(right, left)) + + +# A non-scalar integer D. Any scalar-entry D is covered by the written proof; +# this one keeps the check off the identity matrix. +SCALAR_D = [[1, 1], [1, 2]] + + +def report(): + zeta = character_e1() + chart_e1 = chart(1) + chart_e2 = chart(2) + identity = eye(ADDR) + uniform_z = lift_uniform(zeta) + uniform_e1 = lift_uniform(chart_e1) + scalar = encoding([identity, identity], SCALAR_D) + physical = encoding([identity, chart_e1], SCALAR_D) + even_physical = encoding([identity, chart_e2], SCALAR_D) + pi = literal_pi() + literal = mm(pi, physical) + defect = commutator(uniform_z, physical) + literal_defect = commutator(uniform_z, literal) + address_defect = commutator(zeta, chart_e1) + if nnz(commutator(uniform_z, scalar)) != 0: + raise ValueError("scalar-bank E0 failed to commute with Z_e1") + if nnz(defect) == 0: + raise ValueError("physical L_T commuted with Z_e1") + if nnz(literal_defect) == 0: + raise ValueError("literal Pi L_T commuted with Z_e1") + if literal_defect != mm(pi, defect): + raise ValueError("Pi did not intertwine the physical commutator") + if nnz(commutator(uniform_z, pi)) != 0: + raise ValueError("uniform Z_e1 failed to commute with Pi") + if nnz(commutator(uniform_e1, physical)) != 0 or nnz(commutator(uniform_e1, literal)) != 0: + raise ValueError("translation chart failed to commute with its own physical encoding") + if nnz(commutator(uniform_z, even_physical)) != 0: + raise ValueError("even character direction was not a commuting control") + if nnz(commutator(translation(1), translation(2))) != 0: + raise ValueError("the two translations failed to commute") + if address_defect != [ + [ZERO, (2, -2), ZERO, ZERO], + [(-2, 2), ZERO, ZERO, ZERO], + [ZERO, ZERO, ZERO, (2, -2)], + [ZERO, ZERO, (-2, 2), ZERO], + ]: + raise ValueError("address commutator [Z_e1, S_e1] changed") + if nnz(defect) != 4 or nnz(literal_defect) != 4 or nnz(address_defect) != 4: + raise ValueError("unexpected commutator support") + return { + "scalar_commutes": True, + "physical_defect_nnz": nnz(defect), + "literal_defect_nnz": nnz(literal_defect), + "address_commutator_01": address_defect[0][1], + "translation_subalgebra_commutes": True, + "even_direction_commutes": True, + "pi_intertwines": True, + } + + +def main(): + facts = report() + entry = facts["address_commutator_01"] + print( + "PASS_P104_UNIFORM_ENCODING_GAP" + f" scalar_commutes=1 physical_defect_nnz={facts['physical_defect_nnz']}" + f" literal_defect_nnz={facts['literal_defect_nnz']}" + f" address_entry_01={entry[0]}{entry[1]:+d}i" + " translation_subalgebra_commutes=1 even_direction_commutes=1 pi_intertwines=1" + " no_new_kappa" + ) + + +if __name__ == "__main__": + main()