Exclude two-carrier BIT recovery at summary 770 (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-two-carrier-chronology/PROOF.md

@@ -0,0 +1,50 @@
+# Fixed-source two-carrier exclusion
+
+Use the exact selected #7001 native word. Public fields initially carry the
+659 independent binary unit rows. An ADD XORs two cocharted rows, a SWAP
+exchanges rows and frames, and a MOVE changes the chart label. Owned INIT
+starts a zero row. CLEAR follows the retained owned-erasure premise. The
+replayed public endpoint is `X_i → X_i`, `Y_i → Y_i + X_i` and every helper
+independent. This calculation concerns the necessary binary scalar rows.
+
+Summary 770 is initialized at event 26,857, descends at event 26,861, and is
+first read at event 32,938, with zero-based indices. Preserve the other
+summaries and scalar contacts. Grant replacing up to two existing public
+ascents by carriers that bring their actual source rows to chart zero. For
+an ascent on one owner, its source row is fixed between the previous and
+following contacts, ignoring the chart change of that ascent. An eligible
+source has a positive-dimensional chart and an open cut in this contact
+window after the summary INIT and by the first read. Even while granting
+independent clock choices, there are only 907 eligible positive-rank events.
+Both additional eligible rank-zero source rows reduce to zero in the retained
+quotient.
+
+Let B be the span of every original chart-zero row available in that window,
+except summary 770 itself. There is no original read from 770 before the end
+of the window, so no other retained row in the window includes its effect.
+Giving access to the entire span overgrants timing, retention and copies.
+Keeping the retained scalar prefix, any new chart-zero contribution from
+one or two such carriers lies in the span of B and their literal source
+rows. New scalar combinations of available rows stay in that span. Grant
+free repair that restores the exact original public continuations without
+supplying a new chart-zero row. This relaxes the transport and price tests.
+
+The replay computes dim B = 119 and a nonzero coset t of the target row.
+For each eligible source row, compute its coset s in the same quotient.
+Recovery requires s=t for one source, or s₁+s₂=t for two. Count the latter by
+looking up t+s₁ in the full multiset. The lookup includes same-owner and
+disjoint-clock pairs as a relaxation. Both counts are zero. Thus all 821,022
+ordered distinct-owner pairs are excluded by the necessary row test without
+requiring any paid price or endpoint restrictions. The retained Boolean
+calculation is not an all-width native lowering proof.
+
+The replay independently reconstructs the event pool and quotient with
+low-pivot binary elimination. A second exact screen uses high-pivot
+elimination, explicitly checks 4,096 ordered pairs before its case cap, and
+independently indexes the entire source pool. Positive controls admit a
+synthetic pair and a single-source match. Negative controls reject a changed
+synthetic target and the target outside the retained basis.
+
+This result fixes the literal source rows and summary 770. A modified prefix
+that produces a different row, a different summary, and more than two
+carriers remain open. No complete supplier or κ improvement is claimed.

research/bit-two-carrier-chronology/README.md

@@ -0,0 +1,41 @@
+# Two public carriers cannot recover selected BIT summary 770
+
+**NO VERIFIED GAIN.** On the exact paired #7001 native word, one or two
+existing public MOVE source rows cannot recover summary 770 before its first
+consumer under the fixed scalar prefix. The exact screen grants all retained
+chart-zero rows over the full read window and free public endpoint repair.
+It checks 907 source events on 547 owners. No single or paired source reaches
+the target row in the quotient, including every one of the 821,022 ordered
+pairs of distinct owners. [Proof](PROOF.md)
+
+## Replay
+
+Use CPython 3.12 from a clean checkout at this package's commit.
+
+```sh
+python3.12 -B scripts/research_package.py --package research/bit-two-carrier-chronology
+```
+
+The verifier authenticates the #7001 native word, replays all 659 public
+endpoint rows and the owned clocks, reconstructs the exact source pool and
+checks complementary cosets by binary elimination. The receipt records source
+counts, exclusions and the immutable input hash. [Receipt](RECEIPT.json)
+
+## Scope and credit
+
+[#7149](https://github.com/CrocSwap/integer-mult-bounds/pull/7149) proves
+support bounds for joint replacements under fixed monotone public flow. This
+follow-up changes the proposed chronology by allowing two existing source
+rows to descend to chart zero. It holds the source rows and retained
+continuations fixed. Ali Romman's [#5421](https://github.com/CrocSwap/integer-mult-bounds/pull/5421)
+supplied the owned relation mechanism. DreamingOfClouds, zxv, CubeJerry and
+retained authors supplied the native and paired-controller lineage. Material
+OpenAI Codex and subagent assistance. Apache-2.0.
+
+## Open next questions
+
+Can an earlier legal scalar edit produce a new live source row? First find a
+small, exact source edit with a live cocharted donor before one of these
+ascents. Preserve arbitrary public output rows and charge the full paid and
+ordinary changes. The proof does not cover new producer rows, other summaries
+or three or more carriers.

research/bit-two-carrier-chronology/RECEIPT.json

@@ -0,0 +1,17 @@
+{
+  "basis_rank": 119,
+  "dependencies": {
+    "research/paired-query-only-bit/retained/inputs/BIT-NATIVE-WORD.json.gz": "51203e7fc75ba10bd3ac3f8e675759f47e13d262bea66b6600d1e515095cad78"
+  },
+  "first_read": 32938,
+  "one_source_matches": 0,
+  "ordered_distinct_owner_pairs": 821022,
+  "public_endpoint_rows": 659,
+  "rank_zero_sources_in_retained_basis": 2,
+  "source_events": 907,
+  "source_owners": 547,
+  "status": "PASS_TWO_CARRIER_BIT_ROW_EXCLUSION",
+  "summary": 770,
+  "summary_init": 26857,
+  "two_source_matches_including_same_owner": 0
+}

research/bit-two-carrier-chronology/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-two-carrier-chronology/TASK.json

@@ -0,0 +1,77 @@
+{
+  "actual_scope": "One or two existing public MOVE sources for summary 770 on the exact #7001 word. Preserve the literal scalar prefix and other summaries, grant all retained chart-zero rows over its read window and free endpoint repair.",
+  "ai_assistance": "Substantial OpenAI Codex and subagent assistance, including two exact implementations of the projection test.",
+  "author": "ToikY",
+  "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57",
+  "bottleneck_link": "The source chronology must supply a new arbitrary-input row before an owned rank-seven descent can be retired. This test excludes all one- and two-source recovery in the scoped fixed prefix independently of tariff.",
+  "budget_minutes": 20,
+  "evidence": "659 arbitrary-input endpoint rows checked. 907 eligible source events on 547 owners, quotient basis rank 119, zero one- or two-source matches. Explicit pair screen capped at 4096, whole pool excluded by exact indexing.",
+  "open_questions": [
+    {
+      "blocked_by": "Producer/consumer timing, public endpoint restoration and a fully charged route remain open.",
+      "first_step": "Identify a live cocharted donor before one of the pinned ascents and test the exact changed row.",
+      "question": "Can an earlier legal scalar edit create a new live source row?",
+      "why_it_matters": "An altered prefix can supply a coset absent from the fixed carrier pool."
+    }
+  ],
+  "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": "Change the proposed public chronology after #7149 closed the fixed monotone support scope. Preserve actual source rows and test one summary.",
+  "scope_status": "refined",
+  "stop_rule": "Replay all literal source events. Check at most 4096 explicit ordered pairs. Use an exact quotient multiset to check the whole pool under weaker timing and owner constraints.",
+  "task_id": "bit-helper-contract"
+}

research/bit-two-carrier-chronology/VERIFY.json

@@ -0,0 +1,14 @@
+{
+  "commands": [
+    {
+      "argv": ["{python}", "-I", "-B", "{package}/verify.py"],
+      "checks": "Authenticate the selected word, replay its 659 arbitrary-input endpoint rows, reconstruct the 907 source events and exhaust the one- and two-carrier quotient tests by exact indexing.",
+      "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"
+}

research/bit-two-carrier-chronology/verify.py

@@ -0,0 +1,142 @@
+"""Exact source-row exclusion for BIT summary 770 and two public carriers."""
+from bisect import bisect_left
+from collections import Counter, defaultdict
+import gzip
+from hashlib import sha256
+import json
+from pathlib import Path
+
+HERE = Path(__file__).resolve().parent
+SOURCE = 'research/paired-query-only-bit/retained/inputs/BIT-NATIVE-WORD.json.gz'
+PIN = '51203e7fc75ba10bd3ac3f8e675759f47e13d262bea66b6600d1e515095cad78'
+SUMMARY = 770
+INIT = 26857
+READ = 32938
+
+
+def basis(values):
+    pivots = {}
+    for value in values:
+        while value:
+            lead = value & -value
+            if lead not in pivots:
+                pivots[lead] = value
+                break
+            value ^= pivots[lead]
+    ordered = sorted(pivots.items())
+
+    def reduce(value):
+        for lead, pivot in ordered:
+            if value & lead:
+                value ^= pivot
+        return value
+
+    return reduce, len(pivots)
+
+
+def matches(signatures, target):
+    return signatures[target], sum(n * signatures[s ^ target] for s, n in signatures.items())
+
+
+def verify(path):
+    raw = path.read_bytes()
+    assert sha256(raw).hexdigest() == PIN
+    word = json.loads(gzip.decompress(raw))
+    n = word['public']
+    assert n == 659
+    dims = {int(key): f['dim'] for key, f in word['frames'].items()}
+    frames = word['start'] + [None] * word['owned_fields']
+    rows = [1 << i for i in range(n)] + [0] * word['owned_fields']
+    touch = defaultdict(list)
+    ascents = []
+    zero_rows = set()
+    target = None
+    first_read = None
+    erasures = 0
+    for i, (op, a, *args) in enumerate(word['program']):
+        touch[a].append(i)
+        changed = [a]
+        if op == 'ADD':
+            b, f = args
+            assert a != b and frames[a] == frames[b] == f
+            touch[b].append(i)
+            if b == SUMMARY and first_read is None:
+                first_read = i
+            rows[a] ^= rows[b]
+        elif op == 'SWAP':
+            b = args[0]
+            assert a < n and b < n
+            touch[b].append(i)
+            changed.append(b)
+            frames[a], frames[b] = frames[b], frames[a]
+            rows[a], rows[b] = rows[b], rows[a]
+        elif op == 'MOVE':
+            f, g = args
+            assert frames[a] == f
+            frames[a] = g
+            if a < n:
+                assert dims[f] < dims[g]
+                ascents.append((i, a, f, rows[a]))
+            elif a == SUMMARY:
+                assert target is None and dims[f] == 7 and g == 0
+                target = rows[a]
+        elif op == 'INIT':
+            assert a >= n and frames[a] is None
+            frames[a], rows[a] = args[0], 0
+            if a == SUMMARY:
+                assert i == INIT
+        else:
+            assert op == 'CLEAR' and a >= n and frames[a] == args[0]
+            erasures += bool(rows[a])
+            frames[a], rows[a] = None, 0
+        if INIT <= i < READ:
+            owners = range(len(frames)) if i == INIT else changed
+            zero_rows.update(rows[j] for j in owners if j != SUMMARY and frames[j] == 0)
+
+    assert first_read == READ and target is not None
+    assert frames == word['final'] + [None] * word['owned_fields']
+    assert all(rows[i] == (1 << i) ^ ((1 << (i-111)) if 111 <= i < 222 else 0) for i in range(n))
+    assert len(ascents) == 2862 and erasures == 237
+
+    pool = []
+    zero_sources = []
+    for i, role, frame, row in ascents:
+        contacts = touch[role]
+        j = bisect_left(contacts, i)
+        assert contacts[j] == i
+        previous = contacts[j-1] if j else -1
+        following = contacts[j+1] if j+1 < len(contacts) else len(word['program'])
+        if previous < READ and following > INIT:
+            if dims[frame]:
+                pool.append((role, row))
+            else:
+                zero_sources.append(row)
+
+    reduce, rank = basis(sorted(zero_rows))
+    goal = reduce(target)
+    assert rank == 119 and goal
+    assert len(zero_sources) == 2 and all(reduce(row) == 0 for row in zero_sources)
+    assert basis([*sorted(zero_rows), target])[0](target) == 0
+    assert matches(Counter({1: 1, 2: 1}), 3) == (0, 2)
+    assert matches(Counter({1: 1, 2: 1}), 4) == (0, 0)
+    assert matches(Counter({1: 1, 2: 1}), 1) == (1, 0)
+    signatures = Counter(reduce(row) for _, row in pool)
+    one, two = matches(signatures, goal)
+    assert (one, two) == (0, 0)
+    owners = Counter(role for role, _ in pool)
+    ordered_pairs = len(pool)**2 - sum(v*v for v in owners.values())
+    assert (len(pool), len(owners), ordered_pairs) == (907, 547, 821022)
+    return dict(status='PASS_TWO_CARRIER_BIT_ROW_EXCLUSION', summary=SUMMARY,
+                summary_init=INIT, first_read=READ, basis_rank=rank, public_endpoint_rows=n,
+                source_events=len(pool), source_owners=len(owners), ordered_distinct_owner_pairs=ordered_pairs,
+                rank_zero_sources_in_retained_basis=len(zero_sources),
+                one_source_matches=one, two_source_matches_including_same_owner=two,
+                dependencies={SOURCE: PIN})
+
+
+if __name__ == '__main__':
+    if not __debug__:
+        raise RuntimeError('Use assertions')
+    report = verify(HERE.parents[1] / SOURCE)
+    assert json.dumps(report, indent=2, sort_keys=True) + '\n' == (HERE / 'RECEIPT.json').read_text()
+    print(report['status'])