Prove complete moment optimality of fixed eight-helper complex blocks

research/complex-block-rank-optimum/INPUTS.json

@@ -0,0 +1,39 @@
+{
+  "base_commit": "bce54fb3f895cbe5cd4c0eb477c3afeed100190f",
+  "inputs": [
+    {
+      "file": "inputs/selected.json.gz",
+      "commit": "bce54fb3f895cbe5cd4c0eb477c3afeed100190f",
+      "source_path": "research/community-frontier1042-audit/selected-replay.tar.gz",
+      "git_blob": "6f4dc6fe7631d8aacf8081fcaecf32197181685b",
+      "sha256": "16bc0ebb04b4be6c0ade74badc6a0c0cdba4215eda86e4ff9f13abf8ecebd219",
+      "payload_sha256": "4ddb29fb9bc6f27e0c0fbfcf19a2a93a3496ad900d0f6d89059d0305c9576c0c",
+      "archive_member": "t16/global/base/providers/gauge44/CANONICAL-WORD.json.gz"
+    },
+    {
+      "file": "inputs/pr1319-base.json.gz",
+      "commit": "603defe58aac018c6a8457840481390a15846fe4",
+      "source_path": "research/global-mixed-t74-exact-fill/vendor/pr1297/gauge44-word.json.gz",
+      "git_blob": "eacf8c773cb50637f93a762342b3b5f0853fe29a",
+      "sha256": "e8e6e78ff7422275c38324499e1f33fb2ecd30de9503aef2b8f1ee80d8c4df8e",
+      "payload_sha256": "44290efbd61ee8d4d7a2698cf083892eff0c1f601605f3d4d28b284ff42c0b68"
+    },
+    {
+      "file": "inputs/pr1319-extra.json.gz",
+      "commit": "603defe58aac018c6a8457840481390a15846fe4",
+      "source_path": "research/global-mixed-t74-exact-fill/vendor/pr1297/extra-word.json.gz",
+      "git_blob": "4d464f55a2955e5c832b5ce789d5d0e0a39fb4e1",
+      "sha256": "7b0e9fbda32749aabc7e156d9fe09bceb0624a178628fe69e5dfea783462f905",
+      "payload_sha256": "60f07abaafd6ede2bb42033dacab5b785b36bfa4fd6b153480608c9ca07af4f0"
+    }
+  ],
+  "orientation_program": {
+    "file": "inputs/selected-programs.json.gz",
+    "commit": "bce54fb3f895cbe5cd4c0eb477c3afeed100190f",
+    "source_path": "research/community-frontier1042-audit/selected-replay.tar.gz",
+    "git_blob": "6f4dc6fe7631d8aacf8081fcaecf32197181685b",
+    "archive_member": "t16/global/base/providers/gauge44/LOCAL-PROGRAMS.json.gz",
+    "sha256": "241fde27d4e43f5a9cb6b128f9f76c5131a53d09f0371676163f914d0b0fef3a",
+    "payload_sha256": "9f41d53659e9be84e20c661560c5687abbf5cd0660cdecbe01ad5eb29e6b8ee3"
+  }
+}

research/complex-block-rank-optimum/README.md

@@ -0,0 +1,173 @@
+# Fixed eight-array block decoders have no recursive moment headroom
+
+**Definitive dead end for the declared block class. No new kappa is claimed.**
+
+The twelve late helper blocks in the selected complex word already attain the
+minimum recursive moment over every finite rational scalar program on their
+eight arrays with the retained input frames, late output frames, and dirty
+helper endpoint contract. The result permits arbitrary gate order and length,
+repeated source reads, information splitting, and changed helper coordinates.
+It includes fusion with all later work inside each block. The retained provider
+uses one canonical word for both orientations; the backward program is its
+same-order inverse-transpose dual with the same frame climbs.
+
+For a block with four low helpers and common frame dimension u, the exact
+minimum at every 0<s<1 is:
+
+| Common dimension | Minimum complete helper moment | Native profile |
+| --- | --- | --- |
+| 4 | 24 + 8*2^s + 4*3^s | H1=24, H2=8, H3=4 |
+| 5 | 32 + 4*4^s | H1=32, H4=4 |
+
+[PROOF.md](PROOF.md) proves the bound without a program-length bound. Its input
+barrier does not assume read-once access. Its retirement argument accounts for
+outputs already written before a helper jumps directly to rank nine. The bound
+covers the whole helper path, including completion to rank nine.
+
+The complete complex supplier moment cannot decrease for any exponent in its
+range. The copied centres, other local paths, array volumes, owner assembly,
+endpoint law, and bit supplier stay fixed. Thus the feasible region of the
+complete outer recipe cannot expand. This is stronger than a scalar gate count
+or a bound on one compulsory visit to the common frame.
+
+## Scope
+
+Each block uses its existing eight physical arrays. All sixteen boundary values
+(eight helpers and eight external inputs) are independent. The four output
+ports retain their late entry frames and distinct final hyperplanes. Inputs
+are read-only and outputs are write-only additive ports. Helpers use rational
+scalar additions and nonzero scalings at common frames. Frames grow by
+inclusion. Each rank-r transport is charged as a rank-r recursive child.
+
+No extra array, target scratch, frame descent, changed centre, cross-block
+coding, or output access before the retained late entry frame is included.
+An independently redesigned backward supplier with a different interface is
+also outside the class. This is a declared interface restriction, not a claim that those routes are
+impossible. Phase conditions can only reduce the permitted program class; the
+lower bound grants every monotone common frame.
+
+The investigation considered product-transform fusion, a new support-masked
+block decoder, and joint exact factorization across the existing correction
+seam. The third route was selected because it had a concrete eight-array
+interface and could change the full recursive bill. The declared class is
+recorded in [TASK.json](TASK.json). It was not narrowed to a finite gate search.
+
+## Source and finite evidence
+
+Base commit: `bce54fb3f895cbe5cd4c0eb477c3afeed100190f`.
+[INPUTS.json](INPUTS.json) pins the three native word files by source commit,
+path, Git blob, compressed SHA256, and decompressed SHA256.
+
+| Native word | Blocks with u=4 / u=5 | Total optimal helper profile |
+| --- | --- | --- |
+| Selected PR1094 local word | 7 / 5 | H1=328, H2=56, H3=28, H4=20 |
+| PR1319 base provider | 10 / 2 | H1=304, H2=80, H3=40, H4=8 |
+| PR1319 extra provider | 11 / 1 | H1=296, H2=88, H3=44, H4=4 |
+
+The selected local word is the retained member of the PR1042 replay archive;
+PR1094 changes its global assembly. The selected conditional outer kappa at the
+base is 0.001672660197076918. The pending PR1319 source at
+`603defe58aac018c6a8457840481390a15846fe4` reports 0.001676855229071321.
+These values identify the applicable baselines. This package does not adopt a
+pending frontier or rerun either full construction.
+
+The retained orientation emitter is pinned in SOURCES.json. The selected
+emitted program pair is pinned in INPUTS.json. The checker verifies all 3486
+climb events agree, every non-centre scalar has the inverse-transpose form,
+and the complete paid profiles agree. The controller corollary uses this
+coupled orientation contract.
+
+The verifier extracts every input frame, output entry frame, endpoint cap,
+and rational output matrix from the emitted words. For each block it checks
+all 255 nonempty input subsets. Rational elimination is checked by exact Gram
+minors; binary pivot calculations are checked by enumerated spans. Each of the
+36 interfaces has a nonzero 16-by-16 prefix minor, checked by backward pullback
+and a separate forward replay. Each minor uses eight original source columns
+and the same eight dirty helper columns; it does not require free targets.
+The twelve failure controls reject a changed
+helper correction, a duplicated external input, a missing full helper end, and
+a corrupted input file in each source.
+
+[CERTIFICATE.json](CERTIFICATE.json) contains the extracted premises, all
+independence minors, and complete helper profiles. The finite checks establish
+the source-specific hypotheses of the proof. They are not a formal proof of
+the arbitrary-length theorem or the integer multiplication theorem.
+
+## Reproduce
+
+From the repository root, with Python 3.12 or later and no third-party packages:
+
+```sh
+python3 -I -B research/complex-block-rank-optimum/verify.py
+```
+
+Expected result:
+
+```text
+PASS_FIXED_BLOCK_MOMENT_PREMISES blocks=36 subsets=9180 minors=36 controls=12
+```
+
+The verifier checks the stored certificate without writing files. Use
+`--write-certificate` only to regenerate this package's certificate.
+
+The registered metadata check is:
+
+```sh
+python3 scripts/research_package.py --package research/complex-block-rank-optimum --check-only
+```
+
+The generic replay hook uses Python 3.12. Local verification used Python 3.14.7,
+one process, and no native solver. No full selected-construction cold replay,
+new all-size realization, or Lean proof is claimed.
+
+## Failed attempt and stopping rule
+
+An initial stronger claim, that no kernel can retire below rank eight, is
+false. Some input supports span rank seven and have nonzero kernel. The final
+proof retains those supports. A backward perturbation shows that a retiring
+helper has no earlier or later output response. The exact frame condition
+then forces a rank-six stop before retirement. Its full cost equals the
+retained rank-eight route. The checker requires that this case is present.
+
+The experiment was deterministic. Its finite domain was all input subsets in
+all twelve blocks of each of three pinned words. No random seed or uncompleted
+search is involved. Work stopped when the all-order proof covered this whole
+class and the native profiles attained its complete moment bound.
+
+## Open next questions
+
+A block with earlier output access or communication between blocks is outside
+this theorem. Such a change could escape the fixed interface. The first useful
+step is to specify the changed physical arrays, exact port times, and complete
+native bill before searching for a factorization. The unresolved requirement
+is an admitted interface with better complete cost, not more scalar words in
+the class proved optimal here. See the structured question in TASK.json.
+
+## Credit
+
+Thomas DiFiore's helper-basis screen in Discussion 1167, source commit
+`3e476186e261a531dc12c64a21bb15ac2a0736f8` in `tomdif/integer-mult-bounds`,
+identified the twelve correction blocks, the full dependency, and the open
+question of fusion with later work. This proof closes that question for the
+fixed late eight-array interface. It does not repackage the 10,428 permanent
+and 6,544 temporary basis-change experiments as an exhaustive theorem.
+
+Douglas Colkitt's PR1240 supplies the fixed-word packing ceiling and the
+optimistic rank-eight mass screen. PR679's selector-volume obstruction and
+PR717's fixed-order frame obstruction define different restrictions. This
+result changes gate order and length inside one existing array block and uses
+no selector or doubled volume. A final overlap refresh read the 60 most
+recently updated open PR bodies, covering the full session delta. New PR1389
+and PR1399 concern masked E-graph rigidity; PR1368 concerns R439 bit blocks.
+They do not prove this complete complex block moment result. PR1407 keeps the
+selected local word and changes only owner hosting.
+
+The selected construction is due to Rohan Arun's PR1094, Jeremy Kothe's PR1087,
+and the cumulative k8/slot/T16 lineage. PR1319 and its PR1297/PR1286 provider
+words are due to Rohan Arun, with Jeremy Kothe's PR1274 helper-donor work,
+Jeremy Diviney's mixed-provider work, and the other credits retained in
+[notices](notices). The unchanged bit supplier is PR589 on PR555.
+
+Prepared by Ali Romman with substantial OpenAI Codex assistance in the proof,
+implementation, verification, and documentation. New work is Apache-2.0.
+Inherited source notices and mathematical assumptions are retained.

research/complex-block-rank-optimum/SOURCES.json

@@ -0,0 +1,24 @@
+{
+  "schema_version": 1,
+  "base_commit": "bce54fb3f895cbe5cd4c0eb477c3afeed100190f",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11",
+      "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "c05fafaa25ba95b2d5af86b1800427198e3d20eb",
+      "sha256": "89b5928bc92c81e2647b6d702a7ad85a6795b8f44e2eb267b2ff3145d8f2b2ce"
+    },
+    {
+      "path": "research/complex-sw4-frame8/vendor/pr635/research/complex-571-cold14-st2/code/hpe_emit_local.py",
+      "usage": "provenance",
+      "git_blob": "534fdc71f7641c704575efc038363d7eb206b2df",
+      "sha256": "7e4a6fbc38c8228157b6311457d1496bf460291393043932d2c365f004f77805"
+    }
+  ]
+}

research/complex-block-rank-optimum/TASK.json

@@ -0,0 +1,60 @@
+{
+  "schema_version": 1,
+  "task_id": "complex-new-helper-inventory",
+  "priority_revision": 2,
+  "base_commit": "bce54fb3f895cbe5cd4c0eb477c3afeed100190f",
+  "original_card": {
+    "id": "complex-new-helper-inventory",
+    "question": "Can a new local cost interface change the deficit-to-recursive-cost ratio beyond current packing?",
+    "starting_points": [
+      "research/heterogeneous-owner-assembly/README.md",
+      "certificates/selected-result.json"
+    ],
+    "methods": [
+      "Propose a changed helper inventory and derive an optimistic exact moment.",
+      "Design a small completed instance and independently verify its endpoint and rank bill."
+    ],
+    "acceptance_gate": "A new physically realizable contract, not another mixture already covered by the frozen catalogue.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Read the frozen catalogue bound exclusions and select one genuinely different helper endpoint inventory.",
+      "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay."
+    },
+    "first_experiment": "Write the complete optimistic child histogram and reject it immediately if even the relaxation has insufficient headroom.",
+    "bottleneck_link": "Helper inventory changes can improve the moment; repacking a covered cost interface cannot evade its scoped bound.",
+    "allowed_variations": [
+      "Narrow to one changed boundary or helper type with explicit counts."
+    ],
+    "scope_change_triggers": [
+      "Mixing only providers already inside the pinned catalogue."
+    ],
+    "overlap_terms": [
+      "helper inventory",
+      "heterogeneous-owner",
+      "mutable leaver"
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "Prove the complete recursive moment optimum for arbitrary finite rational factorizations in the twelve fixed eight-array late block interfaces, on the selected word and both PR1319 providers. Retain the single-word provider whose backward program is the same-order inverse-transpose dual.",
+  "scope_change_reason": "The donor assigned within-call non-centre rank shape. The joint factorization route uses the existing eight physical arrays and changes all internal gate orders and lengths; it is distinct from the default new-inventory card. The fixed late output interface was declared before the proof work. The controller statement uses the actual coupled provider orientation rule; it does not cover independent backward-interface synthesis.",
+  "bottleneck_link": "Pointwise optimality of every complete helper moment prevents any decrease in the complex supplier moment or expansion of the retained complete outer-recipe feasible region.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop only after a proof covers arbitrary finite programs in the declared class and the emitted native word attains its lower bound; otherwise report no publishable result.",
+  "outcome": "negative-result",
+  "evidence": "PROOF.md and CERTIFICATE.json: 36 exact source/block interfaces, 9180 nonempty input subsets, 36 nonsingular boundary minors checked in both directions, and 12 rejected mutations.",
+  "author": "Ali Romman",
+  "ai_assistance": "Substantial OpenAI Codex assistance in mathematical reasoning, source extraction, exact verification, and prose.",
+  "open_questions": [
+    {
+      "question": "Can changed output availability or cross-block communication admit a lower complete recursive moment?",
+      "why_it_matters": "Such an interface is outside the proved class and could change the complex supplier exponent.",
+      "first_step": "Specify the physical arrays and native input/output schedule, then price the full optimistic recursive bill.",
+      "blocked_by": "No admitted changed interface or complete native construction is supplied here."
+    }
+  ]
+}

research/complex-block-rank-optimum/VERIFY.json

@@ -0,0 +1,19 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Native block extraction, all subset premises with two exact methods, 36 boundary independence minors, complete attained moments, certificate comparison, and 12 failure controls. Verify the retained coupled orientation contract against the emitted program pair."
+    }
+  ]
+}

research/complex-block-rank-optimum/notices/PR1148-NOTICE.md

@@ -0,0 +1,8 @@
+Apache-2.0. Prepared for Thomas DiFiore with substantial OpenAI Codex assistance.
+
+* The preceding `k8-coordinated-owners`, `k8-eight-ends`, `k8-eight-ends-t16`, and `k8-three-demotions` packages supply the frozen constructions, owner slots, drivers, searches, and all retained source notices.
+* PR1111 by seslly / shipstuff, commit `381831ea554ea983e16224dabed8921b7d0ffdbc`, introduced the group-635 entrance-demotion lead. Its public PR description was consulted; no code or payload from that PR is consumed. The group-635 idea is not original to this package. This package composes it with two other groups, the eight-endpoint word, a joint frame refit, and its preceding T16 assignment. Credit also PR664's promotion mechanism and descendants.
+* The frame model derives from PR864 (navinor / Claude), as adapted and pinned in `../k8-eight-ends`. The new joint searches treat entrance labels as variables in the same frame graph and retain the scalar/cone constraints. Floating solver output is nomination data only.
+* Retain PR1018 and Rohan Arun's PR987 scalar-word lineage, PR1030's endpoint lead, Hao Yan / FanPUYen's PR858 T16 controller and independent checker, PR870/1074 admission work, PR942 by jon314159 and chafreaky's PR795/890 signed prices, and PR589's bit supplier. Their full dependency notices and source hashes remain in the preceding packages.
+* All global admission engines are unchanged. The exact bound adapts the preceding signed-dual proof with the new pinned local profile, using the same two rational arithmetic engines.
+* No claim of unconditional theorem certification, full Lean proof, or exact optimality of the floating discovery searches is made.