Prove the all-prefix information deficit of the native shared-port producer

research/shared-port-prefix-observation/.gitattributes

@@ -0,0 +1 @@
+source/* -text

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"
+  }
+]

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.

research/shared-port-prefix-observation/README.md

@@ -0,0 +1,13 @@
+# 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.
+
+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.

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"
+}

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"
+    }
+  ]
+}

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": "negative-result",
+  "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"
+    }
+  ]
+}

research/shared-port-prefix-observation/VERIFY.json

@@ -0,0 +1,40 @@
+{
+  "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"
+    },
+    {
+      "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"
+    }
+  ]
+}