From 43cd6833035e97aaa3191ce7954a3ad1568257fe Mon Sep 17 00:00:00 2001 From: JoyboyBrian <122925040+JoyboyBrian@users.noreply.github.com> Date: Sat, 24 Oct 2026 21:25:30 -0700 Subject: [PATCH 1/3] Prove native shared-port prefix observation rank bound --- .../.gitattributes | 1 + .../shared-port-prefix-observation/PINS.json | 23 + .../shared-port-prefix-observation/PROOF.md | 25 + .../shared-port-prefix-observation/README.md | 11 + .../RESULT.json | 13 + .../SOURCES.json | 36 + .../shared-port-prefix-observation/TASK.json | 72 + .../VERIFY.json | 30 + .../source/WORD.json | 1550 +++++++++++++++++ .../source/algebra.py | 499 ++++++ .../source/endpoint-proof.md | 242 +++ .../shared-port-prefix-observation/verify.py | 70 + 12 files changed, 2572 insertions(+) create mode 100644 research/shared-port-prefix-observation/.gitattributes create mode 100644 research/shared-port-prefix-observation/PINS.json create mode 100644 research/shared-port-prefix-observation/PROOF.md create mode 100644 research/shared-port-prefix-observation/README.md create mode 100644 research/shared-port-prefix-observation/RESULT.json create mode 100644 research/shared-port-prefix-observation/SOURCES.json create mode 100644 research/shared-port-prefix-observation/TASK.json create mode 100644 research/shared-port-prefix-observation/VERIFY.json create mode 100644 research/shared-port-prefix-observation/source/WORD.json create mode 100644 research/shared-port-prefix-observation/source/algebra.py create mode 100644 research/shared-port-prefix-observation/source/endpoint-proof.md create mode 100644 research/shared-port-prefix-observation/verify.py diff --git a/research/shared-port-prefix-observation/.gitattributes b/research/shared-port-prefix-observation/.gitattributes new file mode 100644 index 0000000000..32c4aa2f30 --- /dev/null +++ b/research/shared-port-prefix-observation/.gitattributes @@ -0,0 +1 @@ +source/* -text diff --git a/research/shared-port-prefix-observation/PINS.json b/research/shared-port-prefix-observation/PINS.json new file mode 100644 index 0000000000..ec3b99fc1d --- /dev/null +++ b/research/shared-port-prefix-observation/PINS.json @@ -0,0 +1,23 @@ +[ + { + "path": "source/WORD.json", + "upstream_path": "research/block3-shared-port-composition/WORD.json", + "commit": "32890bc5de034ab8fc93ac88ead7279a6a416d04", + "sha256": "05c81a7dfb37c240fdaef332474deb90f1b38e60dec392f3a23089f973a5f1ba", + "git_blob": "6126739ac5dce9122bc201c454e8213e8b1bac55" + }, + { + "path": "source/algebra.py", + "upstream_path": "research/block3-shared-port-composition/completion/sources/inputs/pr4813-verify_schedule.py", + "commit": "32890bc5de034ab8fc93ac88ead7279a6a416d04", + "sha256": "6216fd67f1a762303f0eed0e37b90ea0c72cf8e0cb7db70b1b27b2001ac20069", + "git_blob": "17a8439633effba74fff63a8fe4c332b8d709d80" + }, + { + "path": "source/endpoint-proof.md", + "upstream_path": "research/block3-shared-port-composition/completion/PROOF.md", + "commit": "32890bc5de034ab8fc93ac88ead7279a6a416d04", + "sha256": "6bc80c79a789003fc75f01ff41856b3872bc6dd5796fa46d6a85bc0254f0742c", + "git_blob": "dc03c9402a806a5caeecf8bae38ea460e8a5aa93" + } +] diff --git a/research/shared-port-prefix-observation/PROOF.md b/research/shared-port-prefix-observation/PROOF.md new file mode 100644 index 0000000000..7ed7ea3e12 --- /dev/null +++ b/research/shared-port-prefix-observation/PROOF.md @@ -0,0 +1,25 @@ +# Recording-only prefix theorem + +## Source and algebra + +Use exactly the source definitions and finite-phase Clifford group G, monomial subgroup H and central-character algebras A_f,B_f in `source/endpoint-proof.md`. That attributed proof is retained verbatim from block3-shared-port-composition/completion. Put d=dim_E B_f. Grade-three projection pi3 is a B_f-bimodule map: multiplying a pure Clifford by a monomial on either side preserves its support size eight. Absolute phases are retained; quotient scalar phases specialize at width f. Each pure matrix is tensor-powered, while every integer ADD coefficient remains outside that power. + +Our certificate is a finite symbolic identity in the group algebra, not extrapolation from numeric width-one ranks. `verify.py` groups identical absolute-phase rational 8x8 matrices and checks uniform support. Starting from I_5, it replays every actual fused source gate and saves all five owner rows after each gate, plus the entrance. Stack these rows to form O. The exact certificate proves (a) pi3(O)'s entire x0 column is zero; (b) the final rows 1..4 and columns 1..4 are lower triangular with pure grade-three unit AD on the diagonal. Thus rank_E pi3(O)=4d in every central-character quotient: the zero column bounds above; elimination using (AD)^-1 bounds below. No assumption that B_f is a domain is used. + +## All allowed observers + +Recording does not change a producer owner. Each recorded value may be copied, added, discarded or linearly monomial-transformed; recording may reuse arbitrary dirty buffers or retain original inputs. Every resulting target map has form L(O direct_sum I_s)R+E, for rectangular matrices L,R over B_f and a free B_f bypass E. The same precontroller R enters all prefixes because there is only one producer invocation. Interleaved observer-side transformations can be collected into L by linearity; no feedback from recordings to live producer owners is allowed. Any extra independent dirty inputs simply add identity bypass columns. Projecting gives L(pi3(O) direct_sum 0)R, of image dimension at most4d, including after restricting to the five independent target input columns. Five independent pure grade-three targets have dimension5d since each is invertible in A_f. Hence no such algebraic completion exists. + +For operator rather than formal-group identities, the retained homogeneous separating-polynomial argument proves tensor evaluation injective for every f>=|G/Z|-1. It follows that no all-positive-width implementation in this fixed finite columnwise alphabet exists. Small widths with accidental dependencies are not individually ruled out. Width-dependent scalars and arbitrarily many finite free buffers remain allowed. This is stronger than final-output-only observation, not stronger than unrestricted nonlinear or feedback controllers. + +## Exact changed-interface control + +Raw `five_ports` and fused `fused_five_ports` have identical group-algebra endpoints. At raw gate index11 (zero-based), owner1 has grade-three x0 coefficient 2g for one pure unit g, and zero grade-three coefficient on every other input. Adding that single recorded row to final rows1..4 gives a triangular5x5 unit minor, hence image dimension5d. This is a positive control for information only. It exposes a cut strictly internal to an atomic fused child and is outside the theorem's ABI. Lower-grade contamination, owner restoration and any complete decoder remain unresolved. + +## Complete invoice and family gate + +The unchanged producer pays two H1 plus four H3, 24 monomial gates and10 field ADDs (verify the source gate counts). Recording all cuts with five fresh field owners costs 5*(gates+1) fields and copies that many field values; retaining only changed rows reduces storage but cannot improve the upper bound. At N=512^f this literal reference recording costs O(gates*N) scalar traffic/storage; arbitrary free processing is generously uncharged in the obstruction. Dirty recording must pay its own restoration if a concrete caller demands it; our relaxed theorem does not require restoration and thus remains an upper bound. + +At most four independent rank-three jobs can be credited. Even generously crediting a fifth rank-two target gives reward <=4*3^t+2^t versus paid4*3^t+2, so reward minus paid <=2^t-2<=0 for 0<=t<=1. No positive scalar-recursion saving follows in the unchanged interface. This is a moment bound for that five-job target list, not a global circuit lower bound. + +Exposing the raw internal cut changes the paid interface. Replacing a fused H3 by its three H1 constituents changes cost by3-3^t; it is not automatically unaffordable. Full rank alone does not supply the missing decoder, bound lower-grade contamination, cost physical copying, meet rounding precision or return dirty scratch. A new construction round requires a complete cost/error/storage/cleanup invoice for those obligations. The present result therefore closes the unchanged recording route and identifies precisely the changed interface that escapes it. diff --git a/research/shared-port-prefix-observation/README.md b/research/shared-port-prefix-observation/README.md new file mode 100644 index 0000000000..eae0c1286a --- /dev/null +++ b/research/shared-port-prefix-observation/README.md @@ -0,0 +1,11 @@ +# Every declared shared-port prefix still has grade-three image dimension 4d + +The actual PR4856 fused five-bank producer cannot deliver five independent rank-three targets by recording its native boundaries and applying free linear monomial-algebra processing. This closes the prefix-recording question expressly excluded by the retained endpoint completion. The proof permits every prefix, every owner, arbitrarily many clean or dirty recording buffers, original-input bypasses, and width-dependent free linear pre/post processing. Observers cannot feed changes into the producer or inspect inside an atomic paid child. + +`PROOF.md` gives the quantified theorem. `PINS.json` authenticates verbatim source before executing its exact matrix primitives. `verify.py` independently replays every actual gate in the group algebra, retaining scalar coefficients outside tensor powers. `RESULT.json` is checked, not regenerated. Run `python3 -I -B research/shared-port-prefix-observation/verify.py`, also with `-O`. + +A decisive positive control exposes one internal raw C2 cut: its stacked grade-three channel has dimension 5d. Thus the theorem does not apply to arbitrary child-internal observations, and that changed interface remains a productive route. Full rank is only a necessary information condition, not a completion construction. + +## Open next questions + +Can the raw cut be exposed by an actual recursively priced child while retaining the remaining state, precision and cleanup contract? Can its lower-grade contamination be removed without losing the apparent saving? These need a new complete producer/observer invoice before construction expansion. No selected result or kappa change is claimed. diff --git a/research/shared-port-prefix-observation/RESULT.json b/research/shared-port-prefix-observation/RESULT.json new file mode 100644 index 0000000000..7045be8bc7 --- /dev/null +++ b/research/shared-port-prefix-observation/RESULT.json @@ -0,0 +1,13 @@ +{ + "fused_gates": 40, + "retained_cuts": 41, + "rows_observable": 205, + "grade3_image_dimension": "4 dim(B_f)", + "raw_first_pivot_cut": 11, + "raw_stack_dimension": "5 dim(B_f)", + "paid_profile": { + "1": 2, + "3": 4 + }, + "scope": "fixed producer; recording-only native gate boundaries; sufficiently-large-width obstruction to all-width completion" +} diff --git a/research/shared-port-prefix-observation/SOURCES.json b/research/shared-port-prefix-observation/SOURCES.json new file mode 100644 index 0000000000..472a799db1 --- /dev/null +++ b/research/shared-port-prefix-observation/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "32890bc5de034ab8fc93ac88ead7279a6a416d04", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "fc3d4ba105e1f097d0d7d051a308281e86ab1446", + "sha256": "66974efdced4083c00025f97d95d83909a226cdf801edb9301c195c6641f6903" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "research/block3-shared-port-composition/WORD.json", + "usage": "provenance", + "git_blob": "6126739ac5dce9122bc201c454e8213e8b1bac55", + "sha256": "05c81a7dfb37c240fdaef332474deb90f1b38e60dec392f3a23089f973a5f1ba" + }, + { + "path": "research/block3-shared-port-composition/completion/sources/inputs/pr4813-verify_schedule.py", + "usage": "provenance", + "git_blob": "17a8439633effba74fff63a8fe4c332b8d709d80", + "sha256": "6216fd67f1a762303f0eed0e37b90ea0c72cf8e0cb7db70b1b27b2001ac20069" + }, + { + "path": "research/block3-shared-port-composition/completion/PROOF.md", + "usage": "provenance", + "git_blob": "dc03c9402a806a5caeecf8bae38ea460e8a5aa93", + "sha256": "6bc80c79a789003fc75f01ff41856b3872bc6dd5796fa46d6a85bc0254f0742c" + } + ] +} diff --git a/research/shared-port-prefix-observation/TASK.json b/research/shared-port-prefix-observation/TASK.json new file mode 100644 index 0000000000..4ac6c9453d --- /dev/null +++ b/research/shared-port-prefix-observation/TASK.json @@ -0,0 +1,72 @@ +{ + "schema_version": 1, + "task_id": "complex-rank-shape-decoder", + "priority_revision": 7, + "base_commit": "32890bc5de034ab8fc93ac88ead7279a6a416d04", + "original_card": { + "id": "complex-rank-shape-decoder", + "question": "Can a decoder deliver the local paid mass in fewer, larger-rank children (block frame climbs instead of rank-1 to rank-3 steps)?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/complex-local-word-ceiling/README.md", + "research/complex-decoder-field-extension-seed44/README.md", + "research/complex-frame-pair-decoders/README.md", + "research/selected-k8-unrestricted-ends/README.md", + "research/eisenstein-reduction-copy-floor/README.md" + ], + "methods": [ + "Find one exact small decoding identity whose frame path climbs in blocks, and price its complete per-call profile.", + "Bound the best effective child rank achievable for one fixed support alphabet, including copies, frames and restoration." + ], + "acceptance_gate": "A per-call local profile, with all copied information, frames and restoration counted, whose ceiling exceeds the selected word's by at least 5%; masked or overcomplete supports must change an assumption of the eight-term all-pairs bound. 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", + "research/complex-local-word-ceiling/verify.py" + ], + "expected": "PASS_COMPLEX_LOCAL_WORD_CEILING", + "inspect": "Read the selected word's per-call local profile, its packing ceiling and the lever table; run levers.py for the ideal budget of the lever you target.", + "scope": "Positive control and planning budget only; this is not a new construction or full cold replay." + }, + "first_experiment": "Before any synthesis, write the candidate per-call local profile (and centre charge / unpaid coordinates if changed) and screen it with ceiling.ceiling(); reject it if even the ideal ceiling does not beat the selected word's by your stated margin. Ideal budget: rank-16 delivery is 2.31x (levers.py).", + "bottleneck_link": "Rank-1 children are about half of recursive cost; the selected word's effective child rank is about 3.9. Larger-rank delivery lowers recursive cost per unit of paid mass.", + "allowed_variations": [ + "One masked, overcomplete or block decoder family with exact labels and supports.", + "A scoped lower bound on effective rank for one alphabet.", + "If the coverage law, template or guard changes, derive an applicable fully charged replacement bound instead of applying the incumbent ceiling outside its scope." + ], + "scope_change_triggers": [ + "Repacking idle remainders of an unchanged word (covered by the packing ceiling).", + "Repeating the eight-term all-pairs search inside its proved scope.", + "Only changing helper terminal subspaces and monotone frames within the fixed scalar word, entrances and cleanup contract already covered by #1995/#2013.", + "Searching below C=40 in the #2017 Eisenstein binary scalar-rectangle or fixed-support block-linear additive pairing model; specify a changed premise instead. This bound does not cover every complex decoder.", + "Continuing a partial cost improvement while leaving the same unpriced consumer, restoration or central-readout obligation unresolved; refresh the family expansion decision first. Local product-retiming evidence has a narrow scope and is not a ban on changed graphs or contracts." + ], + "overlap_terms": [ + "rank shape", + "block climb", + "masked decoder", + "overcomplete", + "effective rank" + ] + }, + "scope_status": "changed", + "actual_scope": "All native-boundary recordings of the shared fused producer have grade3 image dimension exactly4d; raw internal cut changes it to5d.", + "scope_change_reason": "Resolve the explicit prefix-observer handoff excluded by endpoint-only completion.", + "bottleneck_link": "Closes a specific missing interface obligation before another construction round; no selected-frontier change.", + "budget_minutes": 60, + "stop_rule": "20-minute source-bound proof gate, then finish exact quantified result and controls; stop if only an old theorem or finite extrapolation survives.", + "outcome": "scoped-proof", + "evidence": "PROOF.md; source-pinned verify.py; RESULT.json; VERIFY.json", + "author": "JoyboyBrian", + "ai_assistance": "OpenAI Codex substantial proof and implementation assistance", + "open_questions": [ + { + "question": "Expose and price the raw child-internal cut, including lower-grade elimination and cleanup.", + "why_it_matters": "A changed interface is necessary before claiming additional recursive savings.", + "first_step": "Write the complete changed producer/caller invoice before synthesis.", + "blocked_by": "Unproved changed-interface implementation" + } + ] +} diff --git a/research/shared-port-prefix-observation/VERIFY.json b/research/shared-port-prefix-observation/VERIFY.json new file mode 100644 index 0000000000..28250161ce --- /dev/null +++ b/research/shared-port-prefix-observation/VERIFY.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 30, + "checks": "All-prefix algebra rank certificate, raw internal pivot, exact endpoint and three scientific controls" + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 30, + "checks": "All-prefix algebra rank certificate, raw internal pivot, exact endpoint and three scientific controls" + } + ] +} diff --git a/research/shared-port-prefix-observation/source/WORD.json b/research/shared-port-prefix-observation/source/WORD.json new file mode 100644 index 0000000000..6126739ac5 --- /dev/null +++ b/research/shared-port-prefix-observation/source/WORD.json @@ -0,0 +1,1550 @@ +{ + "two_ports": [ + [ + "paid", + 0, + "A" + ], + [ + "mono", + 0, + "P" + ], + [ + "add", + 1, + 0, + 1 + ], + [ + "mono", + 0, + "Pinv" + ], + [ + "mono", + 0, + "Q" + ], + [ + "add", + 1, + 0, + 2 + ], + [ + "mono", + 0, + "Qinv" + ], + [ + "paid", + 1, + "A" + ], + [ + "mono", + 1, + "W" + ], + [ + "paid", + 1, + "C2" + ], + [ + "mono", + 1, + "V" + ], + [ + "mono", + 1, + "Z1" + ], + [ + "paid", + 1, + "A" + ], + [ + "mono", + 1, + "P" + ], + [ + "add", + 2, + 1, + 1 + ], + [ + "mono", + 1, + "Pinv" + ], + [ + "mono", + 1, + "Q" + ], + [ + "add", + 2, + 1, + 2 + ], + [ + "mono", + 1, + "Qinv" + ], + [ + "paid", + 2, + "A" + ], + [ + "mono", + 2, + "W" + ], + [ + "paid", + 2, + "C2" + ], + [ + "mono", + 2, + "V" + ], + [ + "mono", + 2, + "Z1" + ] + ], + "five_ports": [ + [ + "paid", + 0, + "A" + ], + [ + "mono", + 0, + "P" + ], + [ + "add", + 1, + 0, + 1 + ], + [ + "mono", + 0, + "Pinv" + ], + [ + "mono", + 0, + "Q" + ], + [ + "add", + 1, + 0, + 2 + ], + [ + "mono", + 0, + "Qinv" + ], + [ + "paid", + 1, + "A" + ], + [ + "mono", + 1, + "W" + ], + [ + "paid", + 1, + "C2" + ], + [ + "mono", + 1, + "V" + ], + [ + "mono", + 1, + "Z1" + ], + [ + "paid", + 1, + "A" + ], + [ + "mono", + 1, + "P" + ], + [ + "add", + 2, + 1, + 1 + ], + [ + "mono", + 1, + "Pinv" + ], + [ + "mono", + 1, + "Q" + ], + [ + "add", + 2, + 1, + 2 + ], + [ + "mono", + 1, + "Qinv" + ], + [ + "paid", + 2, + "A" + ], + [ + "mono", + 2, + "W" + ], + [ + "paid", + 2, + "C2" + ], + [ + "mono", + 2, + "V" + ], + [ + "mono", + 2, + "Z1" + ], + [ + "paid", + 2, + "A" + ], + [ + "mono", + 2, + "P" + ], + [ + "add", + 3, + 2, + 1 + ], + [ + "mono", + 2, + "Pinv" + ], + [ + "mono", + 2, + "Q" + ], + [ + "add", + 3, + 2, + 2 + ], + [ + "mono", + 2, + "Qinv" + ], + [ + "paid", + 3, + "A" + ], + [ + "mono", + 3, + "W" + ], + [ + "paid", + 3, + "C2" + ], + [ + "mono", + 3, + "V" + ], + [ + "mono", + 3, + "Z1" + ], + [ + "paid", + 3, + "A" + ], + [ + "mono", + 3, + "P" + ], + [ + "add", + 4, + 3, + 1 + ], + [ + "mono", + 3, + "Pinv" + ], + [ + "mono", + 3, + "Q" + ], + [ + "add", + 4, + 3, + 2 + ], + [ + "mono", + 3, + "Qinv" + ], + [ + "paid", + 4, + "A" + ], + [ + "mono", + 4, + "W" + ], + [ + "paid", + 4, + "C2" + ], + [ + "mono", + 4, + "V" + ], + [ + "mono", + 4, + "Z1" + ], + [ + "paid", + 4, + "A" + ], + [ + "mono", + 4, + "P" + ], + [ + "add", + 0, + 4, + 1 + ], + [ + "mono", + 4, + "Pinv" + ], + [ + "mono", + 4, + "Q" + ], + [ + "add", + 0, + 4, + 2 + ], + [ + "mono", + 4, + "Qinv" + ], + [ + "paid", + 0, + "A" + ] + ], + "fused_two_ports": [ + [ + "paid", + 0, + "A" + ], + [ + "mono", + 0, + "P" + ], + [ + "add", + 1, + 0, + 1 + ], + [ + "mono", + 0, + "Pinv" + ], + [ + "mono", + 0, + "Q" + ], + [ + "add", + 1, + 0, + 2 + ], + [ + "mono", + 0, + "Qinv" + ], + [ + "paid", + 1, + "K" + ], + [ + "mono", + 1, + "N" + ], + [ + "mono", + 1, + "P" + ], + [ + "add", + 2, + 1, + 1 + ], + [ + "mono", + 1, + "Pinv" + ], + [ + "mono", + 1, + "Q" + ], + [ + "add", + 2, + 1, + 2 + ], + [ + "mono", + 1, + "Qinv" + ], + [ + "paid", + 2, + "A" + ], + [ + "mono", + 2, + "W" + ], + [ + "paid", + 2, + "C2" + ], + [ + "mono", + 2, + "V" + ], + [ + "mono", + 2, + "Z1" + ] + ], + "fused_five_ports": [ + [ + "paid", + 0, + "A" + ], + [ + "mono", + 0, + "P" + ], + [ + "add", + 1, + 0, + 1 + ], + [ + "mono", + 0, + "Pinv" + ], + [ + "mono", + 0, + "Q" + ], + [ + "add", + 1, + 0, + 2 + ], + [ + "mono", + 0, + "Qinv" + ], + [ + "paid", + 1, + "K" + ], + [ + "mono", + 1, + "N" + ], + [ + "mono", + 1, + "P" + ], + [ + "add", + 2, + 1, + 1 + ], + [ + "mono", + 1, + "Pinv" + ], + [ + "mono", + 1, + "Q" + ], + [ + "add", + 2, + 1, + 2 + ], + [ + "mono", + 1, + "Qinv" + ], + [ + "paid", + 2, + "K" + ], + [ + "mono", + 2, + "N" + ], + [ + "mono", + 2, + "P" + ], + [ + "add", + 3, + 2, + 1 + ], + [ + "mono", + 2, + "Pinv" + ], + [ + "mono", + 2, + "Q" + ], + [ + "add", + 3, + 2, + 2 + ], + [ + "mono", + 2, + "Qinv" + ], + [ + "paid", + 3, + "K" + ], + [ + "mono", + 3, + "N" + ], + [ + "mono", + 3, + "P" + ], + [ + "add", + 4, + 3, + 1 + ], + [ + "mono", + 3, + "Pinv" + ], + [ + "mono", + 3, + "Q" + ], + [ + "add", + 4, + 3, + 2 + ], + [ + "mono", + 3, + "Qinv" + ], + [ + "paid", + 4, + "K" + ], + [ + "mono", + 4, + "N" + ], + [ + "mono", + 4, + "P" + ], + [ + "add", + 0, + 4, + 1 + ], + [ + "mono", + 4, + "Pinv" + ], + [ + "mono", + 4, + "Q" + ], + [ + "add", + 0, + 4, + 2 + ], + [ + "mono", + 4, + "Qinv" + ], + [ + "paid", + 0, + "A" + ] + ], + "snapshot_restore": [ + [ + "paid", + 0, + "A" + ], + [ + "mono", + 0, + "P" + ], + [ + "add", + 1, + 0, + 1 + ], + [ + "mono", + 0, + "Pinv" + ], + [ + "mono", + 0, + "Q" + ], + [ + "add", + 1, + 0, + 2 + ], + [ + "mono", + 0, + "Qinv" + ], + [ + "paid", + 1, + "A" + ], + [ + "mono", + 1, + "W" + ], + [ + "paid", + 1, + "C2" + ], + [ + "mono", + 1, + "V" + ], + [ + "mono", + 1, + "Z1" + ], + [ + "add", + 5, + 1, + 1 + ], + [ + "mono", + 1, + "Z1" + ], + [ + "mono", + 1, + "V" + ], + [ + "paid", + 1, + "C2" + ], + [ + "mono", + 1, + "X2" + ], + [ + "mono", + 1, + "W" + ], + [ + "paid", + 1, + "A" + ], + [ + "mono", + 1, + "X0" + ], + [ + "mono", + 0, + "P" + ], + [ + "add", + 1, + 0, + -1 + ], + [ + "mono", + 0, + "Pinv" + ], + [ + "mono", + 0, + "Q" + ], + [ + "add", + 1, + 0, + -2 + ], + [ + "mono", + 0, + "Qinv" + ], + [ + "paid", + 1, + "A" + ], + [ + "mono", + 1, + "P" + ], + [ + "add", + 2, + 1, + 1 + ], + [ + "mono", + 1, + "Pinv" + ], + [ + "mono", + 1, + "Q" + ], + [ + "add", + 2, + 1, + 2 + ], + [ + "mono", + 1, + "Qinv" + ], + [ + "paid", + 2, + "A" + ], + [ + "mono", + 2, + "W" + ], + [ + "paid", + 2, + "C2" + ], + [ + "mono", + 2, + "V" + ], + [ + "mono", + 2, + "Z1" + ], + [ + "add", + 6, + 2, + 1 + ], + [ + "mono", + 2, + "Z1" + ], + [ + "mono", + 2, + "V" + ], + [ + "paid", + 2, + "C2" + ], + [ + "mono", + 2, + "X2" + ], + [ + "mono", + 2, + "W" + ], + [ + "paid", + 2, + "A" + ], + [ + "mono", + 2, + "X0" + ], + [ + "mono", + 1, + "P" + ], + [ + "add", + 2, + 1, + -1 + ], + [ + "mono", + 1, + "Pinv" + ], + [ + "mono", + 1, + "Q" + ], + [ + "add", + 2, + 1, + -2 + ], + [ + "mono", + 1, + "Qinv" + ], + [ + "paid", + 2, + "A" + ], + [ + "mono", + 2, + "P" + ], + [ + "add", + 3, + 2, + 1 + ], + [ + "mono", + 2, + "Pinv" + ], + [ + "mono", + 2, + "Q" + ], + [ + "add", + 3, + 2, + 2 + ], + [ + "mono", + 2, + "Qinv" + ], + [ + "paid", + 3, + "A" + ], + [ + "mono", + 3, + "W" + ], + [ + "paid", + 3, + "C2" + ], + [ + "mono", + 3, + "V" + ], + [ + "mono", + 3, + "Z1" + ], + [ + "add", + 7, + 3, + 1 + ], + [ + "mono", + 3, + "Z1" + ], + [ + "mono", + 3, + "V" + ], + [ + "paid", + 3, + "C2" + ], + [ + "mono", + 3, + "X2" + ], + [ + "mono", + 3, + "W" + ], + [ + "paid", + 3, + "A" + ], + [ + "mono", + 3, + "X0" + ], + [ + "mono", + 2, + "P" + ], + [ + "add", + 3, + 2, + -1 + ], + [ + "mono", + 2, + "Pinv" + ], + [ + "mono", + 2, + "Q" + ], + [ + "add", + 3, + 2, + -2 + ], + [ + "mono", + 2, + "Qinv" + ], + [ + "paid", + 3, + "A" + ], + [ + "mono", + 3, + "P" + ], + [ + "add", + 4, + 3, + 1 + ], + [ + "mono", + 3, + "Pinv" + ], + [ + "mono", + 3, + "Q" + ], + [ + "add", + 4, + 3, + 2 + ], + [ + "mono", + 3, + "Qinv" + ], + [ + "paid", + 4, + "A" + ], + [ + "mono", + 4, + "W" + ], + [ + "paid", + 4, + "C2" + ], + [ + "mono", + 4, + "V" + ], + [ + "mono", + 4, + "Z1" + ], + [ + "add", + 8, + 4, + 1 + ], + [ + "mono", + 4, + "Z1" + ], + [ + "mono", + 4, + "V" + ], + [ + "paid", + 4, + "C2" + ], + [ + "mono", + 4, + "X2" + ], + [ + "mono", + 4, + "W" + ], + [ + "paid", + 4, + "A" + ], + [ + "mono", + 4, + "X0" + ], + [ + "mono", + 3, + "P" + ], + [ + "add", + 4, + 3, + -1 + ], + [ + "mono", + 3, + "Pinv" + ], + [ + "mono", + 3, + "Q" + ], + [ + "add", + 4, + 3, + -2 + ], + [ + "mono", + 3, + "Qinv" + ], + [ + "add", + 9, + 0, + 1 + ], + [ + "paid", + 0, + "A" + ], + [ + "mono", + 0, + "X0" + ], + [ + "paid", + 4, + "A" + ], + [ + "mono", + 4, + "P" + ], + [ + "add", + 0, + 4, + 1 + ], + [ + "mono", + 4, + "Pinv" + ], + [ + "mono", + 4, + "Q" + ], + [ + "add", + 0, + 4, + 2 + ], + [ + "mono", + 4, + "Qinv" + ], + [ + "paid", + 0, + "A" + ] + ], + "fused_five_raw_inverse_transpose": [ + [ + "paid", + 0, + "bar_A" + ], + [ + "mono", + 0, + "bar_P" + ], + [ + "add", + 0, + 1, + -1 + ], + [ + "mono", + 0, + "bar_Pinv" + ], + [ + "mono", + 0, + "bar_Q" + ], + [ + "add", + 0, + 1, + -2 + ], + [ + "mono", + 0, + "bar_Qinv" + ], + [ + "paid", + 1, + "bar_K" + ], + [ + "mono", + 1, + "bar_N" + ], + [ + "mono", + 1, + "bar_P" + ], + [ + "add", + 1, + 2, + -1 + ], + [ + "mono", + 1, + "bar_Pinv" + ], + [ + "mono", + 1, + "bar_Q" + ], + [ + "add", + 1, + 2, + -2 + ], + [ + "mono", + 1, + "bar_Qinv" + ], + [ + "paid", + 2, + "bar_K" + ], + [ + "mono", + 2, + "bar_N" + ], + [ + "mono", + 2, + "bar_P" + ], + [ + "add", + 2, + 3, + -1 + ], + [ + "mono", + 2, + "bar_Pinv" + ], + [ + "mono", + 2, + "bar_Q" + ], + [ + "add", + 2, + 3, + -2 + ], + [ + "mono", + 2, + "bar_Qinv" + ], + [ + "paid", + 3, + "bar_K" + ], + [ + "mono", + 3, + "bar_N" + ], + [ + "mono", + 3, + "bar_P" + ], + [ + "add", + 3, + 4, + -1 + ], + [ + "mono", + 3, + "bar_Pinv" + ], + [ + "mono", + 3, + "bar_Q" + ], + [ + "add", + 3, + 4, + -2 + ], + [ + "mono", + 3, + "bar_Qinv" + ], + [ + "paid", + 4, + "bar_K" + ], + [ + "mono", + 4, + "bar_N" + ], + [ + "mono", + 4, + "bar_P" + ], + [ + "add", + 4, + 0, + -1 + ], + [ + "mono", + 4, + "bar_Pinv" + ], + [ + "mono", + 4, + "bar_Q" + ], + [ + "add", + 4, + 0, + -2 + ], + [ + "mono", + 4, + "bar_Qinv" + ], + [ + "paid", + 0, + "bar_A" + ] + ] +} diff --git a/research/shared-port-prefix-observation/source/algebra.py b/research/shared-port-prefix-observation/source/algebra.py new file mode 100644 index 0000000000..17a8439633 --- /dev/null +++ b/research/shared-port-prefix-observation/source/algebra.py @@ -0,0 +1,499 @@ +#!/usr/bin/env python3 +"""Algebraic Verification of the 5-in-14 Block-3 Unit Schedule. + +Synthesizes: + 1. Finite Geometry of Sp_6(F_2): 14 rank-one Lagrangian neighbors partition + under the 768-element stabilizer into orbits of sizes [1, 1, 12] (PR #4743). + 2. Full-Input Native Ports (PR #4743): + - Two-call port U_2 = [[A, 0], [F, A]] (2 paid calls, condition number <= 16). + - Three-call port U_3 = [[A, 0], [B, D]] (3 paid calls, condition number <= 16). + - Residual identity B = D L A = M C_2 + 2 K a. + 3. Swap-Sector Completion: + - On T x_i = sigma_i x_i: u_i - sigma_i M T t_i = D x_{i+1} + 2 K a x_i. + - Scaling by H = (1/2) out_pauli^dagger yields v_i = K x_i + E x_{i+1}. + - Coupler G = K^-1 E satisfies G^dagger G = (1/4) I, ||G|| = 1/2. + 4. 5-Array Chaining Schedule in 14 Calls: + - 4 Three-Call Ports on (x1,x2), (x2,x3), (x3,x4), (x4,x5) -> 12 calls (orbit 12). + - 1 Two-Call Port on (x5,x1) -> 2 calls (the two size-1 orbits). + - Total paid calls = 4 * 3 + 2 = 14 calls (ZERO SLACK). + 5. Recovery of All 5 Canonical Targets K x_1, ..., K x_5: + - Proves exact solvability of the 5-array linear system over Q(i). + - Verifies reconstruction on both swap sectors and arbitrary combinations. + +Standard library only (fractions, itertools, json). Exact Q(i) arithmetic. +""" + +from __future__ import annotations +import json +import time +from fractions import Fraction +from itertools import product + + +# ============================================================================== +# SECTION 1: Exact Gaussian Rational Arithmetic +# ============================================================================== + +def q(real=0, imag=0): + return (Fraction(real), Fraction(imag)) + +ZERO, ONE, I = q(), q(1), q(0, 1) +I_POWERS = (ONE, I, q(-1), q(0, -1)) + +def add(x, y): return (x[0] + y[0], x[1] + y[1]) +def sub(x, y): return (x[0] - y[0], x[1] - y[1]) +def mul(x, y): return (x[0] * y[0] - x[1] * y[1], x[0] * y[1] + x[1] * y[0]) + +def div(x, y): + denom = y[0] ** 2 + y[1] ** 2 + if denom == 0: + raise ZeroDivisionError("division by zero in Q(i)") + return ((x[0] * y[0] + x[1] * y[1]) / denom, (x[1] * y[0] - x[0] * y[1]) / denom) + +def scale(c, a): + return tuple(tuple(mul(c, v) for v in row) for row in a) + +def plus(a, b): + return tuple(tuple(add(x, y) for x, y in zip(ar, br)) for ar, br in zip(a, b)) + +def mm(a, b): + n = len(a) + p = len(b[0]) + k_dim = len(b) + out = [[ZERO for _ in range(p)] for _ in range(n)] + for r in range(n): + for k in range(k_dim): + if a[r][k] == ZERO: + continue + for c in range(p): + if b[k][c] != ZERO: + out[r][c] = add(out[r][c], mul(a[r][k], b[k][c])) + return tuple(tuple(row) for row in out) + +def mv(mat, vec): + n = len(mat) + k_dim = len(vec) + out = [ZERO for _ in range(n)] + for r in range(n): + for k in range(k_dim): + if mat[r][k] != ZERO and vec[k] != ZERO: + out[r] = add(out[r], mul(mat[r][k], vec[k])) + return tuple(out) + +def ident(n=8): + return tuple(tuple(ONE if r == c else ZERO for c in range(n)) for r in range(n)) + +def adjoint(a): + return tuple(tuple((a[c][r][0], -a[c][r][1]) for c in range(len(a))) for r in range(len(a[0]))) + +def monomial(permutation, phases=None): + if phases is None: + phases = [0] * len(permutation) + n = len(permutation) + return tuple( + tuple(I_POWERS[phases[c] % 4] if r == permutation[c] else ZERO for c in range(n)) + for r in range(n) + ) + +def pauli(x, z): + return monomial( + [j ^ x for j in range(8)], + [(x & z).bit_count() + 2 * (j & z).bit_count() for j in range(8)] + ) + +def c_letter(bit): + return plus( + scale(q(Fraction(1, 2), Fraction(1, 2)), ident()), + scale(q(Fraction(1, 2), Fraction(-1, 2)), pauli(1 << bit, 0)) + ) + +def s_letter(mask): + return monomial(list(range(8)), [(j & mask).bit_count() for j in range(8)]) + +def word(*letters): + out = ident(len(letters[0])) + for letter in letters: + out = mm(out, letter) + return out + + +# ============================================================================== +# SECTION 2: Finite Geometry in Sp_6(F_2) (PR #4743) +# ============================================================================== + +def lin(cols, v): + s = 0 + for i, c in enumerate(cols): + if (v >> i) & 1: + s ^= c + return s + +def rank_f2(vs): + piv = {} + for v in vs: + while v: + k = v.bit_length() - 1 + if k in piv: + v ^= piv[k] + else: + piv[k] = v + break + return len(piv) + +def space_f2(vs): + return tuple(sorted({lin(vs, k) for k in range(1 << len(vs))})) + +def verify_finite_geometry(): + gl = [a for a in product(range(1, 8), repeat=3) if rank_f2(a) == 3] + base = space_f2((9, 16, 32)) + hs = [] + stab = [] + neighbors = set() + + for a in gl: + inv = [next(x for x in range(8) if lin(a, x) == 1 << i) for i in range(3)] + it = [sum(((inv[j] >> i) & 1) << j for j in range(3)) for i in range(3)] + for mask in range(64): + q_vec = [((mask >> i) & 1) << i for i in range(3)] + for z, (i, j) in enumerate([(0, 1), (0, 2), (1, 2)], 3): + if (mask >> z) & 1: + q_vec[i] ^= 1 << j + q_vec[j] ^= 1 << i + def h(v): + x = v & 7 + z = v >> 3 + return lin(a, x) | (lin(it, z ^ lin(q_vec, x)) << 3) + cols = tuple(h(1 << j) for j in range(6)) + hs.append(cols) + sub = space_f2(tuple(lin(cols, z) for z in (9, 16, 32))) + neighbors.add(sub) + if sub == base: + stab.append(cols) + + unseen = set(neighbors) + orbits = [] + while unseen: + s = next(iter(unseen)) + orb = {tuple(sorted(lin(h_col, v) for v in s)) for h_col in stab} + unseen -= orb + orbits.append(len(orb)) + + orbit_profile = sorted(orbits) + assert len(neighbors) == 14, "Lagrangian neighbors count must be 14" + assert len(stab) == 768, "Common stabilizer order must be 768" + assert orbit_profile == [1, 1, 12], "Stabilizer orbits must partition into [1, 1, 12]" + return { + "GL3_order": len(gl), + "symplectic_group_order": len(hs), + "rank_one_neighbors": len(neighbors), + "stabilizer_order": len(stab), + "stabilizer_orbits": orbit_profile, + } + + +# ============================================================================== +# SECTION 3: Operators & Full-Input Triangular Ports (PR #4743) +# ============================================================================== + +def load_operators(): + I_8 = ident(8) + C0, C1, C2 = (c_letter(j) for j in range(3)) + U = monomial([0, 5, 2, 7, 4, 1, 6, 3]) + V = monomial([0, 2, 1, 3, 4, 6, 5, 7]) + S = s_letter(7) + + P = word(S, U, S) + Q = word(S, V, S) + L = plus(P, scale(q(2), Q)) + + K = word(C0, C1, C2) + a = pauli(1, 3) # Y0 Z1 + W = pauli(0, 5) # Z0 Z2 + J = word(pauli(0, 2), V, C2) # Z1 V01 C2 (1 paid call) + M = monomial([2, 0, 3, 1, 4, 6, 5, 7], [0, 0, 2, 2, 1, 3, 3, 1]) + + A = C0 + D = word(J, W, C0) + B = word(D, L, A) + F = word(A, L, A) + T = monomial([((x & 1) << 2) | (x & 2) | ((x & 4) >> 2) for x in range(8)]) + + out_pauli = word(K, a, adjoint(K)) + H = scale(q(Fraction(1, 2)), adjoint(out_pauli)) + E = word(H, D) + G = word(adjoint(K), E) + + # Core identities + assert word(D, L, A) == B, "B = D L A" + assert B == plus(word(M, C2), scale(q(2), word(K, a))), "B = M C2 + 2 K a" + assert word(H, K, a) == scale(q(Fraction(1, 2)), K), "H K a = (1/2) K" + assert word(adjoint(G), G) == scale(q(Fraction(1, 4)), I_8), "G^dagger G = (1/4) I" + + return { + "I": I_8, "C0": C0, "C1": C1, "C2": C2, "K": K, + "A": A, "D": D, "B": B, "F": F, "T": T, "M": M, "W": W, "J": J, + "H": H, "E": E, "G": G, "out_pauli": out_pauli + } + + +# ============================================================================== +# SECTION 4: 5-Array 14-Call Schedule & Full Target Recovery +# ============================================================================== + +def gaussian_elimination_q(matrix, rhs_vectors): + """Gaussian elimination over Q(i) to solve M x = rhs for multiple rhs vectors.""" + n_rows = len(matrix) + n_cols = len(matrix[0]) + n_rhs = len(rhs_vectors) + + # Augmented matrix: [M | RHS] + aug = [list(matrix[r]) + [rhs_vectors[k][r] for k in range(n_rhs)] for r in range(n_rows)] + + pivots = [] + curr_row = 0 + for col in range(n_cols): + # Find pivot + sel = None + for r in range(curr_row, n_rows): + if aug[r][col] != ZERO: + sel = r + break + if sel is None: + continue + + aug[curr_row], aug[sel] = aug[sel], aug[curr_row] + p_val = aug[curr_row][col] + # Scale pivot row to 1 + aug[curr_row] = [div(val, p_val) for val in aug[curr_row]] + + # Eliminate in all other rows + for r in range(n_rows): + if r != curr_row and aug[r][col] != ZERO: + coeff = aug[r][col] + aug[r] = [sub(aug[r][c], mul(coeff, aug[curr_row][c])) for c in range(len(aug[r]))] + + pivots.append((curr_row, col)) + curr_row += 1 + + rank = len(pivots) + return rank, aug, pivots + + +def run_5in14_verification(): + print("=" * 80) + print("5-IN-14 BLOCK-3 UNIT SCHEDULE VERIFICATION OVER Q(i)") + print("=" * 80) + + # Part 1: Finite Geometry + print("\n[Part 1: Sp_6(F_2) 14-Neighbor Geometry]") + geo = verify_finite_geometry() + print(f" Rank-1 Lagrangian Neighbors: {geo['rank_one_neighbors']}") + print(f" Common Stabilizer Group Order: {geo['stabilizer_order']}") + print(f" Stabilizer Orbit Sizes: {geo['stabilizer_orbits']} (Orbits: 1, 1, 12)") + print(" -> Corresponds EXACTLY to 12 calls (4 x 3-call ports) + 2 calls (1 x 2-call port) = 14!") + + # Part 2: Native Port Properties + print("\n[Part 2: Full-Input Native Triangular Ports (PR #4743)]") + ops = load_operators() + I = ops["I"] + K, A, D, B, F, T = ops["K"], ops["A"], ops["D"], ops["B"], ops["F"], ops["T"] + E, G, H, M = ops["E"], ops["G"], ops["H"], ops["M"] + + print(" Two-Call Port U_2 = [[A, 0], [F, A]]: 2 paid calls, condition number <= 16 [VERIFIED]") + print(" Three-Call Port U_3 = [[A, 0], [B, D]]: 3 paid calls, condition number <= 16 [VERIFIED]") + print(" Residual Identity: B = D L A = M C_2 + 2 K a [VERIFIED]") + print(" Swap Sector Closure: C2 x = sigma T C0 x -> Residual subtraction is FREE [VERIFIED]") + print(f" Coupler Operator G = K^-1 E: G^dagger G = (1/4) I, ||G|| = 1/2 [VERIFIED]") + + # Part 3: Chaining Schedule over 5 Arrays (Calls 1..14) + print("\n[Part 3: 14-Call Schedule on 5 Arrays (x1, x2, x3, x4, x5)]") + print(" Schedule Architecture:") + print(" - Port 1 (Calls 1, 2, 3): U_3 on (x1, x2) -> v_1 = K x1 + E x2, t_1 = A x1") + print(" - Port 2 (Calls 4, 5, 6): U_3 on (x2, x3) -> v_2 = K x2 + E x3, t_2 = A x2") + print(" - Port 3 (Calls 7, 8, 9): U_3 on (x3, x4) -> v_3 = K x3 + E x4, t_3 = A x3") + print(" - Port 4 (Calls 10, 11, 12): U_3 on (x4, x5) -> v_4 = K x4 + E x5, t_4 = A x4") + print(" - Port 5 (Calls 13, 14): U_2 on (x5, x1) -> s_1 = A x1 + F x5, t_5 = A x5") + print(" - Free Subtraction: w_5 = s_1 - t_1 = F x5") + print(" Total Paid Calls: 3 + 3 + 3 + 3 + 2 = 14 Calls (ZERO SLACK: 14 * 80 = 5 * 224 = 1120).") + + # Part 4: Constructing the Exact 5-Array Multi-Port Operator + print("\n[Part 4: Exact Multi-Port Matrix Construction & Rank Analysis]") + # Input dimension: 5 arrays * 8 coordinates = 40 dimensions + # Build linear observation rows: + # v1 (8 rows): K x1 + E x2 + # v2 (8 rows): K x2 + E x3 + # v3 (8 rows): K x3 + E x4 + # v4 (8 rows): K x4 + E x5 + # w5 (8 rows): F x5 + # t1..t5 (40 rows): A x1, A x2, A x3, A x4, A x5 + # Total observations: 80 rows in 40 unknown variables. + + matrix_rows = [] + # 1. v1 = K x1 + E x2 + for r in range(8): + row = [ZERO] * 40 + for c in range(8): + row[0 + c] = K[r][c] + row[8 + c] = E[r][c] + matrix_rows.append(row) + + # 2. v2 = K x2 + E x3 + for r in range(8): + row = [ZERO] * 40 + for c in range(8): + row[8 + c] = K[r][c] + row[16 + c] = E[r][c] + matrix_rows.append(row) + + # 3. v3 = K x3 + E x4 + for r in range(8): + row = [ZERO] * 40 + for c in range(8): + row[16 + c] = K[r][c] + row[24 + c] = E[r][c] + matrix_rows.append(row) + + # 4. v4 = K x4 + E x5 + for r in range(8): + row = [ZERO] * 40 + for c in range(8): + row[24 + c] = K[r][c] + row[32 + c] = E[r][c] + matrix_rows.append(row) + + # 5. w5 = F x5 + for r in range(8): + row = [ZERO] * 40 + for c in range(8): + row[32 + c] = F[r][c] + matrix_rows.append(row) + + # 6..10. t_k = A x_k + for k in range(5): + for r in range(8): + row = [ZERO] * 40 + for c in range(8): + row[k * 8 + c] = A[r][c] + matrix_rows.append(row) + + # Verify Rank of the Observation System + rank, _, pivots = gaussian_elimination_q(matrix_rows, []) + print(f" Observation Rows: {len(matrix_rows)}") + print(f" Input Dimensionality: 40 (5 arrays x 8 coordinates)") + print(f" Observation Matrix Rank: {rank} / 40 (FULL INJECTIVE RANK!)") + assert rank == 40, "Observation matrix must have full rank 40" + + # Part 5: Exact Target Reconstruction & Sector Inversion + print("\n[Part 5: Exact Recovery of All 5 Canonical Targets K x_1..K x_5]") + # Test on arbitrary input vectors across both swap sectors + # Create test vectors for 5 arrays: + test_cases = [ + ("All Positive Swap Sectors (sigma = +1 for all 5 arrays)", [1, 1, 1, 1, 1]), + ("Mixed Swap Sectors (+1, -1, +1, -1, +1)", [1, -1, 1, -1, 1]), + ("All Negative Swap Sectors (sigma = -1 for all 5 arrays)", [-1, -1, -1, -1, -1]), + ] + + for label, sigmas in test_cases: + # Form sector projectors + projectors = [scale(q(Fraction(1, 2)), plus(I, scale(q(s), T))) for s in sigmas] + # Choose concrete test inputs x_k = E_sigma_k * base_vector + x_inputs = [] + for k in range(5): + base_vec = tuple(q(1 if i == k else 0) for i in range(8)) + vec = mv(projectors[k], base_vec) + # Ensure non-trivial vector + if all(v == ZERO for v in vec): + base_vec = tuple(q(1 if i == ((k + 1) % 8) else 0) for i in range(8)) + vec = mv(projectors[k], base_vec) + x_inputs.append(vec) + + # Expected canonical targets: K x_k + expected_targets = [mv(K, x_inputs[k]) for k in range(5)] + + # Simulate the physical outputs from the 14-call schedule: + # Ports 1..4: + v_obs = [] + for k in range(4): + # Port on (x_k, x_{k+1}): + # Raw second output: u = D x_{k+1} + B x_k + # Since B x_k = sigma_k M T A x_k + 2 K a x_k: + # Subtraction: u - sigma_k M T (A x_k) = D x_{k+1} + 2 K a x_k + # Scaling by H: v_k = K x_k + E x_{k+1} + term1 = mv(K, x_inputs[k]) + term2 = mv(E, x_inputs[k + 1]) + vk = tuple(add(term1[i], term2[i]) for i in range(8)) + v_obs.append(vk) + + # Port 5 (2-call port on (x5, x1)): + # Raw second output: s_1 = A x1 + F x5 + # Subtraction: w5 = s_1 - A x1 = F x5 + w5_obs = mv(F, x_inputs[4]) + + # Retained t_k = A x_k + t_obs = [mv(A, x_inputs[k]) for k in range(5)] + + # Combine all physical observations into single 80-dim vector: + all_obs = [] + for vk in v_obs: all_obs.extend(vk) + all_obs.extend(w5_obs) + for tk in t_obs: all_obs.extend(tk) + + # Solve for x = (x1, x2, x3, x4, x5) using the observation matrix: + # Solves M x_rec = all_obs + _, aug, _ = gaussian_elimination_q(matrix_rows, [all_obs]) + recovered_x_flat = [aug[r][-1] for r in range(40)] + + # Group into 5 arrays: + recovered_x = [tuple(recovered_x_flat[k * 8 : (k + 1) * 8]) for k in range(5)] + + # Compute recovered targets: K x_rec + recovered_targets = [mv(K, recovered_x[k]) for k in range(5)] + + # Verify exact equality with expected targets: + max_error = 0 + for k in range(5): + for i in range(8): + diff = sub(recovered_targets[k][i], expected_targets[k][i]) + err = abs(diff[0]) + abs(diff[1]) + if err > max_error: + max_error = err + + print(f" Test: {label}") + print(f" Max Reconstruction Error across all 5 arrays: {max_error} [EXACT RECOVERY!]") + assert max_error == 0, f"Target reconstruction failed for {label}" + + print("-" * 80) + print("Key Mathematical Findings:") + print(" 1. The 14 Lagrangian rank-one neighbors in Sp_6(F_2) partition under the 768-element") + print(" stabilizer into orbits of sizes 1, 1, and 12.") + print(" 2. The size-12 orbit exactly powers four 3-call full-input triangular ports (12 calls).") + print(" 3. The two size-1 orbits power one 2-call triangular port (2 calls).") + print(" 4. Total paid calls = 12 + 2 = 14 calls, matching the PR #4628 lower bound 14W/5") + print(" and clearing the PR #4710 deficit 960 with ZERO SLACK (14 * 80 = 5 * 224 = 1120).") + print(" 5. The resulting cyclic/cascade observation matrix has full injective rank 40,") + print(" recovering all 5 canonical targets K x_1, ..., K x_5 with condition number <= 16.") + print("=" * 80) + + +def main(): + import io, contextlib + f = io.StringIO() + with contextlib.redirect_stdout(f): + run_5in14_verification() + result = { + "arrays": 5, + "condition_number_bound": 16, + "max_reconstruction_error": 0, + "new_kappa": False, + "observation_matrix_rank": 40, + "paid_calls": 14, + "stabilizer_orbits": [1, 1, 12], + "status": "PASS_FIVE_IN_FOURTEEN_SCHEDULE", + "total_state_dimension": 40, + "zero_slack_identity": "14 * 80 == 5 * 224 == 1120" + } + print(json.dumps(result, sort_keys=True)) + + +if __name__ == "__main__": + main() diff --git a/research/shared-port-prefix-observation/source/endpoint-proof.md b/research/shared-port-prefix-observation/source/endpoint-proof.md new file mode 100644 index 0000000000..dc03c9402a --- /dev/null +++ b/research/shared-port-prefix-observation/source/endpoint-proof.md @@ -0,0 +1,242 @@ +# The retained five-bank word has no free monomial-algebra completion + +This is an outputs-only exact embedding gate for PR4856 at +`0970de4ec97fc942e6202403ffd7586d19559391`. It applies the group-algebra +projection and all-width faithfulness argument retained in PR4920 at +`7eb4ef5251f7ba96c7e5d78c42fc98e66b7be4ba` to the actual five-bank endpoint. +It is not a circuit search, a new construction, or a new kappa value. +The earlier direct PR4908 binding gate did not allow cross-output ADD; +this argument does, within the fixed finite columnwise Clifford alphabet. + +## Exact source word and expansion + +Use the source's absolute-phase three-axis Clifford letters. Products act +on a column from right to left. Put + + A=C0, K=C0 C1 C2, + P=S U S, Q=S V S, S=s_letter(7), + U=monomial([0,5,2,7,4,1,6,3]), + V=monomial([0,2,1,3,4,6,5,7]), + D=Z1 V C2 W C0, W=Z0 Z2, + B=D(P+2Q)A, F=A(P+2Q)A. + +Crucially, at width f these expressions mean +`B_f=D_f(P_f+2Q_f)A_f`, with each pure letter tensor-powered separately. +The scalar 2 stays outside the tensor power. The source's pure identities +include `A^2=X0` and `AD=N K` with a unit-phase monomial N. + +The actual retained owner map is + + u0=x0; uj=D xj+B u(j-1), j=1,...,4; + y0=A^2 x0+F u4; yj=A uj, j=1,...,4. + +Consequently its block matrix M has + + M00=A^2+F B^4, + M0k=F B^(4-k)D, 1<=k<=4, + Mj0=A B^j, 1<=j<=4, + Mjk=A B^(j-k)D, 1<=k<=j<=4, + Mjk=0, j>=1 and k>j. + +The executable expands `B=bP+2bQ` and `F=hP+2hQ`, where each b/h is a +single Clifford word. It groups by exact rational-complex 8-by-8 matrices, +retaining absolute phases and integer coefficients. It independently +replays both `five_ports` and `fused_five_ports` in the frozen WORD.json IN +THE EXACT GROUP ALGEBRA and matches all 25 blocks to this recurrence. Group +keys retain absolute one-column matrices, and scalar coefficients remain +outside tensor powers. Ordinary one-column operator equality is only an +additional check. Changing an actual ADD sign or omitting the actual +closing bank0 A gate fails this group-algebra comparison. Thus this is the source endpoint, +not a replacement diagonal-only model. All full matrices, branch labels, +coefficients and grades are retained in RESULT.json. + +The entries below list counts of distinct exact group elements by grade +`(rank0,rank1,rank2,rank3)`, after grouping identical pure words: + +| row / column | 0 | 1 | 2 | 3 | 4 | +|---|---|---|---|---|---| +| 0 | (6,0,26,0) | (0,16,0,0) | (0,0,8,0) | (0,4,0,0) | (0,0,2,0) | +| 1 | (0,0,2,0) | (0,0,0,1) | 0 | 0 | 0 | +| 2 | (0,4,0,0) | (2,0,0,0) | (0,0,0,1) | 0 | 0 | +| 3 | (0,0,8,0) | (0,0,0,4) | (2,0,0,0) | (0,0,0,1) | 0 | +| 4 | (0,16,0,0) | (8,0,0,0) | (0,0,0,4) | (2,0,0,0) | (0,0,0,1) | + +In particular M00 has 33 ungrouped terms, 32 exact group elements, and 32 +distinct projective classes. Its rank0 and rank2 coefficient masses are 43 +and 201. The `A^2=X0` term has coefficient 1 and is the only term in its +projective class, even among all 32 FB^4 branch terms. Therefore its +coefficient remains1 in every central-character quotient: no scalar phase +from another term in that class can cancel it. This alone does not assert +linear independence of different Clifford matrices at small widths. + +## All-width algebra, including absolute phases + +Let G be a chosen finite-phase group of exact one-column three-axis Clifford +matrices, containing all source letters and the full monomial Clifford +subgroup H in that finite alphabet. Put `Z={z in G : z is scalar}`; H +contains Z. This uses a finite-phase Clifford group, not the normalizer +enlarged by arbitrary U(1) phases. Work over a characteristic-zero splitting +field E. At width f set + + A_f=E[G]/(z-scalar(z)^f : z in Z), + B_f=E[H]/(z-scalar(z)^f : z in Z). + +These are the central-character twisted group algebras on G/Z and H/Z. +Projection pi0 from A_f to B_f discards all nonmonomial projective classes. +Multiplication by H on either side preserves monomial membership and its +complement; hence pi0 is a B_f-bimodule map, entrywise on owner matrices. +The other Fourier-grade projections have the same bimodule property. +Monomial row/column permutations and phases preserve the uniform support +size 2^rank of a pure Clifford matrix, which is the grade used here. + +The retained PR4920 independent review proves that the tensor evaluation +of A_f is injective for every f>=|G/Z|-1. Briefly, for each projective +representative v_t choose for every other v_u a linear functional zero at +v_u and nonzero at v_t. Their product isolates v_t in degree |G/Z|-1; +multiplication by a nonvanishing linear functional extends to any larger +degree. Applying this homogeneous polynomial to tensor powers establishes +linear independence. Scalar phases specialize as scalar(z)^f. This +argument permits width-dependent scalar coefficients and free controls +within the same fixed finite alphabet. + +The unique X0 class above therefore proves `pi0(M_f) != 0` as an algebra +matrix for every f, and as an evaluated operator matrix for every +sufficiently large f. The all-width endpoint obstruction uses these +sufficiently large widths. It makes no grade-projection claim based only +on accidental relations between one-column matrix sums. + +## Stronger rank3 resource bound: linear copy, drop, reset and clean buffers + +The parent identified a stronger invariant from the complete grade table. +Let `A_(3),f` be the E-vector space spanned by rank3 projective classes in +A_f. It is a B_f-bimodule. Projection pi3 onto this space is therefore a +B_f-bimodule map. Consider the right-B_f-linear input map + + pi3(M_f): B_f^5 -> A_(3),f^5. + +The exact group-algebra checks establish that its entire first row AND +first column vanish. Its lower4-by-4 block is lower triangular with the +single group unit AD, of grade3, on every diagonal position. Thus its +image has E-dimension exactly4*d, where d=dim_E B_f. The zero first input +column gives the upper bound4*d. For the lower bound, a vector in the +kernel of the lower triangular block has `AD*x1=0` in its first row; +multiplication by the group inverse gives x1=0. Successive rows then give +x2=x3=x4=0. This is an injective map from B_f^4 into A_(3),f^4; no domain +or division property for B_f is assumed. + +Allow arbitrary rectangular pre/post matrices over B_f, and arbitrary +owned free buffers, saved original inputs, linear copies, dropping and +resets. For this linear alphabet any such pre/post policy, restricted to +the five original independent inputs and the five desired output rows, +has form + + T = L (M_f direct_sum I_s) R + E0, + +for some s, where L,R are arbitrary compatible matrices over B_f and +`E0` is a free B_f-valued bypass (which can also be absorbed into a larger +identity summand). No invertibility or scratch restoration is required. +Identity and zero/clean bypass resources have zero pi3. Therefore + + pi3(T) = L (pi3(M_f) direct_sum 0_s) R, + rank_E pi3(T) <= 4*d. + +Here R maps B_f-input modules into B_f intermediate modules, while L acts +E-linearly on the A_(3),f output space. This is not incorrectly treating +pi3(M_f) as a B_f-valued endomorphism. Neither map can increase the image +dimension4*d. Scalar coefficients and the number of buffers may depend on +width; the inequality holds separately at each sufficiently large width. + +Five independent pure grade3 target words `diag(g1,...,g5)` instead define +an injective map `B_f^5 -> A_(3),f^5`: each gj is a group unit, including +any allowed monomial boundaries. Their grade3 image dimension is5*d. +This contradicts the bound. Extra discarded or main-dependent garbage +outputs cannot repair the five required output rows. Thus the unchanged +producer has no exact five-target completion by any such free linear +pre/post decoder, even with clean/copy/drop/reset buffers and saved-input +bypass. The all-width applicability is the preceding sufficiently-large-f +faithfulness argument. No accidental small-width equality is ruled out by +this algebraic proof. + +## Supporting rank0 proof for invertible controls and restored dirty scratch + +Allow any number s of dirty scratch owners returned unchanged. Grant +arbitrary invertible pre- and postcontrollers L,R over B_f on all 5+s +owners, with unrestricted scalar coefficients, cross-owner ADD and full +monomial Clifford boundaries. This is a relaxation of a finite native +free controller; all its Gaussian calls remain those in M. Suppose + + L (M_f direct_sum I_s) R = diag(g1,...,g5,I_s), + +where each gj is a single pure rank3 Gaussian Clifford, with arbitrary +monomial input/output boundaries. Each target gj has zero pi0 projection. +Applying the bimodule projection gives + + L (pi0(M_f) direct_sum I_s) R = diag(0,0,0,0,0,I_s). + +Let d=dim_E B_f. Regard these matrices as E-linear maps on the regular +right module B_f^(5+s), using left multiplication for their entries. +A nonzero B_f entry gives a nonzero linear map (apply it to1), even though +B_f can have zero divisors. Thus `rank_E pi0(M_f)>=1`. The left side has +rank at least `s*d+1`, since the two blocks act on separate summands and +L,R are invertible. The right side has rank exactly `s*d`, a contradiction. +Equivalently the respective nullities are at most5*d-1 and exactly5*d. +No domain assumption, determinant argument or positivity assumption is +used. The argument holds for each sufficiently large f, so an all-width +completion of this form is impossible. + +Without scratch, the nonzero grade component and invertibility suffice +immediately. With scratch, the rank argument prevents moving that component +into an identity scratch block. Arbitrary scratch count and width-dependent +free coefficients do not change the contradiction. + +## Complete invoice and stop gate + +The actual fused source bill remains `2H1+4H3`,24 monomial passes and10 +ADD passes. Five independent rank3 rewards would give optimistic recursive +moment `3^(1-C)-2`, but the required free completion is now excluded in the +declared alphabet. One additional ordinary rank1 Gaussian already changes +this upper bound to `3^(1-C)-3<=0` for 0<=C<1. Thus that completion cannot +fund a positive moment before any finite/compiler reserve. + +There is also no profitable downgrade to five independent pure Gaussian +targets of ranks at most3. If k of them have rank3, the target pi3 map +has image dimension k*d, so the resource bound forces k<=4. Put t=1-C, +with0<=t<=1. The other targets have rank at most2; granting all five jobs +and zero finite bill gives + + reward <= 4*3^t + 2^t, + paid recursive cost = 4*3^t + 2, + moment <= 2^t - 2 <= 0. + +This bound is strict for0<=t<1, equivalently positive C, and only reaches +zero at C=0. If k<4, monotonicity `3^t>=2^t` gives the same upper bound. +An empty/rank0 job can only reduce reward under the convention h(0)=0. +Thus no five-target census with ranks at most3 can make this unchanged +paid profile profitable through a free linear pre/post decoder in scope. + +This closes the zero-extra-Gaussian pre/post completion question for the +unchanged five-bank word under arbitrary free linear full-monomial Clifford +ADD controllers, including owned clean/copy/drop/reset buffers and saved +original-input bypass. The rank0 proof separately covers arbitrary restored +dirty identity scratch with invertible controls. It also includes +any PR4908 inverse representable by such controllers if it were bound to +this actual endpoint. No new decoder, precision schedule or kappa is +supplied or needed for this negative gate. + +Open next questions require a changed premise: another paid word/profile, +transformed nonmonomial helper resources with a complete invoice, another +target census, or a non-columnwise address grammar. Arbitrary width-specific +address permutations outside the fixed finite tensor alphabet and changed +main sizes are outside this claim. The same applies to prefix taps, saving +intermediate producer states, and inserting free gates inside the retained +producer word. The model grants one invocation of that complete fixed +producer plus pre/post controls and saved original-input bypass. These are +scope limits, not proposed successes. + +Sources retain their original authorship and Apache-2.0 notices. The +five-bank construction and invoice are PR4856's; the projection and +phase-aware faithfulness argument are reused with credit from PR4920 and +its independent review. The parent research agent proposed the stronger +maximal-grade resource bound removing controller invertibility and scratch +restoration assumptions. New expansion and application: OpenAI Codex +gpt-6.1-sol/high, outputs-only work for the parent research session. diff --git a/research/shared-port-prefix-observation/verify.py b/research/shared-port-prefix-observation/verify.py new file mode 100644 index 0000000000..9aee7530a7 --- /dev/null +++ b/research/shared-port-prefix-observation/verify.py @@ -0,0 +1,70 @@ +"""Source-bound group-algebra prefix certificate. JoyboyBrian/OpenAI, Apache-2.0.""" +import json,hashlib +from pathlib import Path +from collections import defaultdict +p=Path(__file__).resolve().parent + +def need(ok,why): + if not ok:raise ValueError(why) +for pin in json.loads((p/'PINS.json').read_text()): + need(hashlib.sha256((p/pin['path']).read_bytes()).hexdigest()==pin['sha256'],'source authentication '+pin['path']) +d={'__name__':'source'} +exec(compile((p/'source/algebra.py').read_bytes(),'authenticated algebra','exec'),d) +op=d['load_operators']();word,adj=d['word'],d['adjoint'];I=d['ident']();S=d['s_letter'](7);V=d['monomial']([0,2,1,3,4,6,5,7]);P=word(S,d['monomial']([0,5,2,7,4,1,6,3]),S);Q=word(S,V,S) +letters=dict(op,P=P,Pinv=adj(P),Q=Q,Qinv=adj(Q),V=V,Z1=d['pauli'](0,2),N=word(op['A'],op['D'],adj(op['K']))) +def grade(m): + counts={sum(z!=d['ZERO'] for z in row) for row in m} + need(len(counts)==1 and next(iter(counts)) in (1,2,4,8),'pure uniform grade') + return next(iter(counts)).bit_length()-1 + +def replay(gates): + mat=[[{I:1}if j==k else{} for k in range(5)]for j in range(5)] + cuts=[[[dict(c) for c in row] for row in mat]] + for gate in gates: + kind,dst=gate[:2] + if kind=='add': + src,c=gate[2:] + for k in range(5): + ans=defaultdict(int,mat[dst][k]) + for m,a in mat[src][k].items():ans[m]+=c*a + mat[dst][k]={m:a for m,a in ans.items()if a} + else: + need(kind in ('paid','mono'),'native gate kind') + mat[dst]=[{word(letters[gate[2]],m):a for m,a in cell.items()}for cell in mat[dst]] + cuts.append([[dict(c) for c in row]for row in mat]) + return cuts + +def projected(cell):return {m:a for m,a in cell.items()if grade(m)==3} + +def certify(gates): + cuts=replay(gates) + need(all(not projected(row[0])for cut in cuts for row in cut),'prefix first-column grade3 vanishes') + last=cuts[-1];AD=word(op['A'],op['D']) + need(grade(AD)==3,'diagonal is grade3 unit') + for j in range(1,5): + need(projected(last[j][j])=={AD:1},'unit diagonal') + for k in range(j+1,5):need(not projected(last[j][k]),'triangular minor') + return cuts + +def main(): + source=json.loads((p/'source/WORD.json').read_text());g=source['fused_five_ports'];cuts=certify(g) + raw=replay(source['five_ports']);tap=projected(raw[12][1][0]) + need(len(tap)==1 and list(tap.values())==[2],'raw cut11 unit pivot coefficient2') + need(all(not projected(raw[12][1][k])for k in range(1,5)),'raw cut only x0 grade3') + need(raw[-1]==cuts[-1],'raw/fused endpoint equality with absolute phases') + # Boundary-expansion fault: replacing the source by its raw lowering must fail. + try:certify(source['five_ports']) + except ValueError:pass + else:raise ValueError('raw internal observation control accepted') + # A hypothetical extra paid rank3 observer really changes the rank witness. + extra=[['paid',0,'K']]+g + try:certify(extra) + except ValueError:pass + else:raise ValueError('added rank3 observer control accepted') + # Actual producer sign fault breaks endpoint binding, not merely rank. + bad=[list(x)for x in g];j=next(i for i,x in enumerate(bad)if x[0]=='add');bad[j][3]*=-1 + need(replay(bad)[-1]!=raw[-1],'actual ADD sign fault detection') + result=dict(fused_gates=len(g),retained_cuts=len(cuts),rows_observable=5*len(cuts),grade3_image_dimension='4 dim(B_f)',raw_first_pivot_cut=11,raw_stack_dimension='5 dim(B_f)',paid_profile={'1':2,'3':4},scope='fixed producer; recording-only native gate boundaries; sufficiently-large-width obstruction to all-width completion') + need(result==json.loads((p/'RESULT.json').read_text()),'receipt equality') + print(json.dumps(result,sort_keys=True)) +if __name__=='__main__':main() From 52115124ec9902b5e8ea3d12e171829cafea6c02 Mon Sep 17 00:00:00 2001 From: JoyboyBrian <122925040+JoyboyBrian@users.noreply.github.com> Date: Sat, 24 Oct 2026 21:26:16 -0700 Subject: [PATCH 2/3] Reject unauthenticated prefix sources and altered receipts in isolated replay --- .../shared-port-prefix-observation/README.md | 2 ++ .../shared-port-prefix-observation/TASK.json | 2 +- .../VERIFY.json | 10 +++++++++ .../test_package.py | 21 +++++++++++++++++++ 4 files changed, 34 insertions(+), 1 deletion(-) create mode 100644 research/shared-port-prefix-observation/test_package.py diff --git a/research/shared-port-prefix-observation/README.md b/research/shared-port-prefix-observation/README.md index eae0c1286a..7100174253 100644 --- a/research/shared-port-prefix-observation/README.md +++ b/research/shared-port-prefix-observation/README.md @@ -9,3 +9,5 @@ A decisive positive control exposes one internal raw C2 cut: its stacked grade-t ## Open next questions Can the raw cut be exposed by an actual recursively priced child while retaining the remaining state, precision and cleanup contract? Can its lower-grade contamination be removed without losing the apparent saving? These need a new complete producer/observer invoice before construction expansion. No selected result or kappa change is claimed. + +Package-boundary controls run with `python3 -I -B research/shared-port-prefix-observation/test_package.py`: copied-source mutation must fail before import; receipt mutation must fail in normal and optimized Python. All executable inputs are local to this package. Frozen predecessor bytes retain their attribution. diff --git a/research/shared-port-prefix-observation/TASK.json b/research/shared-port-prefix-observation/TASK.json index 4ac6c9453d..ee4afda7c4 100644 --- a/research/shared-port-prefix-observation/TASK.json +++ b/research/shared-port-prefix-observation/TASK.json @@ -57,7 +57,7 @@ "bottleneck_link": "Closes a specific missing interface obligation before another construction round; no selected-frontier change.", "budget_minutes": 60, "stop_rule": "20-minute source-bound proof gate, then finish exact quantified result and controls; stop if only an old theorem or finite extrapolation survives.", - "outcome": "scoped-proof", + "outcome": "negative-result", "evidence": "PROOF.md; source-pinned verify.py; RESULT.json; VERIFY.json", "author": "JoyboyBrian", "ai_assistance": "OpenAI Codex substantial proof and implementation assistance", diff --git a/research/shared-port-prefix-observation/VERIFY.json b/research/shared-port-prefix-observation/VERIFY.json index 28250161ce..c4bfa32561 100644 --- a/research/shared-port-prefix-observation/VERIFY.json +++ b/research/shared-port-prefix-observation/VERIFY.json @@ -25,6 +25,16 @@ ], "timeout_seconds": 30, "checks": "All-prefix algebra rank certificate, raw internal pivot, exact endpoint and three scientific controls" + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/test_package.py" + ], + "timeout_seconds": 30, + "checks": "Isolated normal and optimized source-before-import authentication, typed receipt and native recipe mutations" } ] } diff --git a/research/shared-port-prefix-observation/test_package.py b/research/shared-port-prefix-observation/test_package.py new file mode 100644 index 0000000000..59fdd02523 --- /dev/null +++ b/research/shared-port-prefix-observation/test_package.py @@ -0,0 +1,21 @@ +"""Isolated package-boundary faults; no shared source mutation.""" +import json,shutil,subprocess,sys,tempfile +from pathlib import Path +HERE=Path(__file__).resolve().parent + +def need(ok,why): + if not ok:raise ValueError(why) +def run(p,opt):return subprocess.run([sys.executable,'-I']+opt+['-B',str(p/'verify.py')],capture_output=True,text=True,timeout=15) +for opt in ([],['-O']): + with tempfile.TemporaryDirectory() as tmp: + p=Path(tmp)/'package';shutil.copytree(HERE,p) + result=run(p,opt);need(result.returncode==0,'isolated baseline '+result.stderr) + source=p/'source/algebra.py';old=source.read_bytes();source.write_bytes(old+b'\nraise RuntimeError("UNAUTHENTICATED_CODE_EXECUTED")\n') + result=run(p,opt);need(result.returncode!=0 and 'source authentication' in result.stderr and 'UNAUTHENTICATED_CODE_EXECUTED' not in result.stderr,'authenticate before executing source') + source.write_bytes(old) + receipt=p/'RESULT.json';old=receipt.read_bytes();data=json.loads(old);data['unexpected_field']='tampered';receipt.write_text(json.dumps(data)) + result=run(p,opt);need(result.returncode!=0 and 'receipt equality' in result.stderr,'typed whole receipt rejection');receipt.write_bytes(old) + if (p/'RECIPES.json').exists(): + q=p/'RECIPES.json';data=json.loads(q.read_text());data[0]['left']['phase']=(data[0]['left']['phase']+1)%4;q.write_text(json.dumps(data));result=run(p,opt) + need(result.returncode!=0 and 'native recipe receipt' in result.stderr,'native recipe mutation rejection') +print('PASS_PACKAGE_BOUNDARY_CONTROLS normal and optimized') From b1a0751717552a99906fc44487a8f8af175cd39c Mon Sep 17 00:00:00 2001 From: JoyboyBrian <122925040+JoyboyBrian@users.noreply.github.com> Date: Sat, 24 Oct 2026 21:27:00 -0700 Subject: [PATCH 3/3] Preserve JSON types and test read-only exported prefix package --- research/shared-port-prefix-observation/test_package.py | 6 ++++++ research/shared-port-prefix-observation/verify.py | 2 +- 2 files changed, 7 insertions(+), 1 deletion(-) diff --git a/research/shared-port-prefix-observation/test_package.py b/research/shared-port-prefix-observation/test_package.py index 59fdd02523..597d8dff38 100644 --- a/research/shared-port-prefix-observation/test_package.py +++ b/research/shared-port-prefix-observation/test_package.py @@ -9,12 +9,18 @@ def run(p,opt):return subprocess.run([sys.executable,'-I']+opt+['-B',str(p/'veri for opt in ([],['-O']): with tempfile.TemporaryDirectory() as tmp: p=Path(tmp)/'package';shutil.copytree(HERE,p) + for item in [p]+list(p.rglob('*')):item.chmod(0o700 if item.is_dir()else 0o600) result=run(p,opt);need(result.returncode==0,'isolated baseline '+result.stderr) source=p/'source/algebra.py';old=source.read_bytes();source.write_bytes(old+b'\nraise RuntimeError("UNAUTHENTICATED_CODE_EXECUTED")\n') result=run(p,opt);need(result.returncode!=0 and 'source authentication' in result.stderr and 'UNAUTHENTICATED_CODE_EXECUTED' not in result.stderr,'authenticate before executing source') source.write_bytes(old) receipt=p/'RESULT.json';old=receipt.read_bytes();data=json.loads(old);data['unexpected_field']='tampered';receipt.write_text(json.dumps(data)) result=run(p,opt);need(result.returncode!=0 and 'receipt equality' in result.stderr,'typed whole receipt rejection');receipt.write_bytes(old) + data=json.loads(old) + if 'witness_input' in data:data['witness_input'][0][0]=True + else:data['fused_gates']=float(data['fused_gates']) + receipt.write_text(json.dumps(data));result=run(p,opt) + need(result.returncode!=0 and 'receipt equality' in result.stderr,'bool/int or float/int receipt type rejection');receipt.write_bytes(old) if (p/'RECIPES.json').exists(): q=p/'RECIPES.json';data=json.loads(q.read_text());data[0]['left']['phase']=(data[0]['left']['phase']+1)%4;q.write_text(json.dumps(data));result=run(p,opt) need(result.returncode!=0 and 'native recipe receipt' in result.stderr,'native recipe mutation rejection') diff --git a/research/shared-port-prefix-observation/verify.py b/research/shared-port-prefix-observation/verify.py index 9aee7530a7..1d4d8b4249 100644 --- a/research/shared-port-prefix-observation/verify.py +++ b/research/shared-port-prefix-observation/verify.py @@ -65,6 +65,6 @@ def main(): bad=[list(x)for x in g];j=next(i for i,x in enumerate(bad)if x[0]=='add');bad[j][3]*=-1 need(replay(bad)[-1]!=raw[-1],'actual ADD sign fault detection') result=dict(fused_gates=len(g),retained_cuts=len(cuts),rows_observable=5*len(cuts),grade3_image_dimension='4 dim(B_f)',raw_first_pivot_cut=11,raw_stack_dimension='5 dim(B_f)',paid_profile={'1':2,'3':4},scope='fixed producer; recording-only native gate boundaries; sufficiently-large-width obstruction to all-width completion') - need(result==json.loads((p/'RESULT.json').read_text()),'receipt equality') + need(json.dumps(result,sort_keys=True)==json.dumps(json.loads((p/'RESULT.json').read_text()),sort_keys=True),'receipt equality') print(json.dumps(result,sort_keys=True)) if __name__=='__main__':main()