Bound BIT sender fusion at owned recipients (0% κ change)

docs/ci-verification.md

@@ -1,8 +1,25 @@
 # CI verification
 
-## Current selected-family replay: #6030
+## Current selected-family replay: #7000 with #7001
 
 The [selected record](../certificates/selected-result.json) binds conditional
+κ = 0.00363005817 to the [application review](research/pr-intake-evidence/pr7000-application/PROOF-REVIEW.md),
+[validation receipts](research/pr-intake-evidence/pr7000-application/VALIDATION.json),
+and [explicit source closure](../certificates/frontier7000-source.json).
+`make frontier7000-verify` follows that exact-source selected replay. The review
+reuses eleven authenticated preceding executions and records seven fresh serial
+application, scalar and complete native-catalogue executions. The earlier
+monolithic timeout is retained separately and is not completed coverage.
+Consult the receipts for exact commands, source heads and limits.
+
+The five inherited framework assumptions remain. No complete uniform word,
+literal multiplier execution, independent human proof or formal-kernel proof
+is asserted. Routine research submissions do not need to rerun this
+selected-family replay. The sections below preserve historical checkpoints.
+
+## Historical selected-family replay: #6030
+
+The [historical checkpoint](../certificates/checkpoints/frontier6030.json) binds conditional
 κ = 0.003125804 to the [proof review](research/pr-intake-evidence/pr6030-audit/PROOF-REVIEW.md),
 [validation receipts](research/pr-intake-evidence/pr6030-audit/VALIDATION.json),
 and [explicit source closure](../certificates/frontier6030-source.json).

research/bit-send-cochart-gate/PROOF.md

@@ -0,0 +1,58 @@
+# Exact sender support and chronology exclusions
+
+Replay the literal selected #7001 word over 659 independent binary input
+rows. ADD applies XOR in its declared common chart. SWAP exchanges rows and
+charts, MOVE changes the chart, and INIT and CLEAR use the retained owned
+allocation and erasure semantics. The complete final chart vector and all
+arbitrary-input public rows match the selected interface. This proof uses
+the necessary chart and linear-row contracts of that replay.
+
+## Fixed recipient route
+
+There are 360 consecutive public-sender contact triples `MOVE F→H`,
+`ADD A→B`, `MOVE H→G`, with ranks `(6,7,8)` and nonzero cargo. A direct
+`F→G` can expose the sender only on its endpoint charts in the isolated
+window. The 120 original recipients B are owned. The verifier checks their
+entire literal lifetimes. Their chart ranks are seven and, for nine summary
+owners, zero. Neither sender endpoint can be cocharted with B, even if every
+recipient contact barrier is waived and the fused MOVE may occur anywhere
+in the sender's contact gap. Correcting XORs across a recipient observation
+do not change this missing chart.
+
+## Rebind the owned chart
+
+Each owner has three incoming sends on the same middle chart. If all three
+senders use their early endpoints, the new owner requires a common rational
+rank-six subspace. Exact annihilator tests reject all 120 groups. If the
+owner uses the common late chart, all three senders can supply full-rank
+rows in the relaxed timing model. For 111 owners, the one original consumer
+never occupies any rank-eight chart in its whole trajectory. Its unchanged
+route therefore cannot consume the full-rank owner by a direct ADD.
+
+The other nine owners descend to chart zero before their first read. Their
+old descent has rank seven. A full-rank rebind changes its rank to eight.
+Put p=1−κ. Three rank-one pairs replaced by three rank-two MOVEs save
+`3(2−2^p) < 6κ`. By integration, the added descent cost
+`8^p−7^p` is at least `p·8^(−κ) ≥ (1−κ)/8`. At the exact target κ the latter
+bound exceeds `6κ`. All nine late rebinds lose before any additional costs.
+This scope keeps the original one consumer or one descent per owner.
+
+## Keep the owned chart and replace sender rows
+
+For each owner, keep its rank-seven chart and its original first output
+barrier, which is the sole outgoing rank-seven ADD or the summary descent.
+Choose a nonempty subset of its three input senders to fuse. For each
+chosen sender, remove its original transient rank-seven availability from
+the first MOVE through the second. Leave other old rows intact. Grant free
+XOR access to the union of every other literal row in the owner's chart
+from INIT through the output barrier, including other valid appearances of
+a chosen sender outside its removed interval. The owner itself starts zero.
+Even with arbitrary copies, its additional row contribution must lie in
+this granted span. The old unselected inputs are kept, so the extra target
+is the XOR of exactly the chosen source rows.
+
+Exact elimination excludes all 840 nonempty subsets, with zero unresolved
+cases. All 840 controls pass when the removed source rows are restored to
+the pool. The full receiver-window union deliberately overgrants simultaneous
+availability and erasure. The conclusion does not cover altered producer
+rows or alternative routes for the original public consumers.

research/bit-send-cochart-gate/README.md

@@ -0,0 +1,45 @@
+# BIT sender fusion at owned recipients
+
+**NO VERIFIED GAIN.** On the exact selected #7001 word, 360 consecutive
+public sender triples have a rank-six to rank-seven MOVE, one outgoing ADD,
+and a rank-seven to rank-eight MOVE. Their 120 owned recipients never occupy
+either outer rank in the literal trajectory. Retiming across a recipient read
+cannot supply the missing cochart.
+
+Rebinding all three sends to one owned chart also fails the tested gates.
+The early spaces differ. Of the late cases, 111 unchanged consumers never
+reach full rank and nine summaries lose paid price. At the original
+rank-seven chart, no nonempty subset of sender rows can be replaced by
+other retained rows, even with a free union of donor rows over the entire
+window. [Proof](PROOF.md) · [Exact receipt](RECEIPT.json)
+
+## Replay
+
+From a clean checkout, use CPython 3.12 with assertions enabled.
+
+```sh
+python3.12 -B scripts/research_package.py --package research/bit-send-cochart-gate
+```
+
+The verifier reconstructs all 659 arbitrary-input endpoint rows, exact
+charts, owned lifetimes and sender triples. It checks all 120 group gates
+and 840 alias subsets. Both the retained word and canonical task card are
+source-pinned.
+
+## Scope and credit
+
+[#7157](https://github.com/CrocSwap/integer-mult-bounds/pull/7157) fixes
+the source rows for two public carriers of summary 770. This package tests
+all literal one-ADD sends into owned rank-seven recipients and their
+recovery before the next use. Credit Ali Romman's #5421 for owned summary
+relations, and DreamingOfClouds, zxv, CubeJerry and the retained authors for
+the #6834/#7001 native and paired-controller sources. Substantial OpenAI
+Codex and subagent assistance. Apache-2.0.
+
+## Open next questions
+
+Can a coupled prefix rewrite supply a new live receiver row? Start with two
+paid source arrivals and check the exact displaced destination rows jointly.
+Any replacement needs the same arbitrary-input public endpoints, restored
+ownership and a complete paid bill. A changed producer prefix or receiver
+operator is outside the three tested scopes.

research/bit-send-cochart-gate/RECEIPT.json

@@ -0,0 +1,23 @@
+{
+  "alias_hits": 0,
+  "alias_positive_controls": 840,
+  "alias_subsets": {
+    "1": 360,
+    "2": 360,
+    "3": 120
+  },
+  "dependencies": {
+    "research/paired-query-only-bit/retained/inputs/BIT-NATIVE-WORD.json.gz": "51203e7fc75ba10bd3ac3f8e675759f47e13d262bea66b6600d1e515095cad78"
+  },
+  "fixed_route_hits": 0,
+  "owned_recipients": 120,
+  "public_endpoint_rows": 659,
+  "rebind": {
+    "early_spaces_incompatible": 120,
+    "late_consumer_never_full": 111,
+    "late_summary_descent": 9
+  },
+  "sender_triples": 360,
+  "status": "PASS_BIT_SEND_COCHART_GATE",
+  "target": "10018846261809/2500000000000000"
+}

research/bit-send-cochart-gate/SOURCES.json

@@ -0,0 +1,24 @@
+{
+  "schema_version": 1,
+  "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "75d77b328ea02ded535e7f23aee5b1e55d0bb1a8",
+      "sha256": "154c3d30455d778fd3343b6b4851f0fa4665f0f7625b0adb3675e2bafbbf6bf1"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    },
+    {
+      "path": "research/paired-query-only-bit/retained/inputs/BIT-NATIVE-WORD.json.gz",
+      "usage": "input",
+      "git_blob": "b718d6b2848215ad785022106dfa9f871a3d1c0c",
+      "sha256": "51203e7fc75ba10bd3ac3f8e675759f47e13d262bea66b6600d1e515095cad78"
+    }
+  ]
+}

research/bit-send-cochart-gate/TASK.json

@@ -0,0 +1,77 @@
+{
+  "actual_scope": "The exact #7001 360 outgoing-ADD sender triples, 120 owned receiver rebinds and all 840 nonempty sender subsets under fixed first output and granted rank-seven aliases.",
+  "ai_assistance": "Substantial OpenAI Codex and subagent assistance, including independent chart and row checks.",
+  "author": "ToikY",
+  "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57",
+  "bottleneck_link": "The optimistic one-ADD price requires real cocharted recipient support. These three exact necessary gates exclude the tested sender fusions.",
+  "budget_minutes": 20,
+  "evidence": "360 fixed-route sends, 120 full-group rebinds and 840 existing-row alias subsets exhausted. Exact 659 input-row endpoints and 840 restored-source controls pass.",
+  "open_questions": [
+    {
+      "blocked_by": "Exact live rows, compatible arrival clocks, endpoint restoration, and fully charged price remain open.",
+      "first_step": "Pin two paid arrivals and solve the two displaced destination rows against the retained same-chart basis.",
+      "question": "Can a coupled prefix rewrite supply a new live receiver row?",
+      "why_it_matters": "A changed producer can provide a direction unavailable in the original cochart span."
+    }
+  ],
+  "original_card": {
+    "acceptance_gate": "A full boundary contract and paid profile; unchanged scalar counts alone are insufficient. 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.",
+    "allowed_variations": [
+      "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes."
+    ],
+    "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.",
+    "existing_checks": [
+      {
+        "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md",
+        "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.",
+        "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.",
+        "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5",
+        "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137",
+        "status": "reviewed"
+      }
+    ],
+    "first_experiment": "First read #5679/#5708 and their audits as pending component proposals. Choose one uncovered helper group/cut on an exact word; compare arbitrary-input native action, targets, owned storage, both orientations and full signed bill. Stop if the gain is only a scalar count or repaid by lost targets. Do not rerun the frozen #5609 common-frame domain without changing its hypothesis.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_selected_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.",
+      "scope": "Source-bound orientation only, not a supplier replay or theorem proof."
+    },
+    "id": "bit-helper-contract",
+    "methods": [
+      "Construct and independently check one source-bound instance of the stated first experiment.",
+      "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change."
+    ],
+    "overlap_terms": [
+      "G20",
+      "helper split",
+      "5679",
+      "5708",
+      "independent target"
+    ],
+    "question": "Can a changed G20 helper path or independent-target split improve the complete BIT moment without losing its physical endpoint?",
+    "scope_change_triggers": [
+      "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.",
+      "Treating an archived proposal or local numerical pass as complete supplier admission."
+    ],
+    "starting_points": [
+      "docs/research/current-priorities.md",
+      "docs/research/research-family-status.md",
+      "certificates/selected-result.json",
+      "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md",
+      "research/g20-helper-split/README.md",
+      "research/g20-conjugation-admission/README.md"
+    ]
+  },
+  "outcome": "negative-result",
+  "priority_revision": 8,
+  "schema_version": 1,
+  "scope_change_reason": "Investigate actual sender-to-owned receiver routes after the fixed two-carrier source-pool exclusion.",
+  "scope_status": "refined",
+  "stop_rule": "Exhaust 360 fixed-route sends, 120 complete rebinds and 840 nonempty subsets. Use exact necessary support and directed or rigorous analytic price. Stop before a literal build if none survives.",
+  "task_id": "bit-helper-contract"
+}

research/bit-send-cochart-gate/VERIFY.json

@@ -0,0 +1,14 @@
+{
+  "commands": [
+    {
+      "argv": ["{python}", "-I", "-B", "{package}/verify.py"],
+      "checks": "Authenticate the selected word, check all arbitrary public rows and owned charts, exhaust the fixed recipient and rebind gates, and test all 840 exact sender subsets against the granted cochart span.",
+      "timeout_seconds": 30
+    }
+  ],
+  "inputs": ["research/paired-query-only-bit/retained/inputs/BIT-NATIVE-WORD.json.gz"],
+  "python": "3.12",
+  "requirements": [],
+  "schema_version": 1,
+  "status": "ready"
+}