Bound coupled BIT chart relabeling (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-coupled-chart-bound/AUDIT.json

@@ -0,0 +1,13 @@
+{
+  "best_directed_whole_upper": "-150259748047868384659982093203238820648182213478633/2500000000000000000000000000000000000000000000000",
+  "certificate_sha256": "1b99adc18dc7bb1839cc98d17b3be022bae939dd16d0f7d6bcea8fc24cd1f678",
+  "changed_optimal_assignments": 0,
+  "edges": 62474,
+  "forged_flow_rejected": true,
+  "scopes": 897,
+  "signed_original_net": [
+    "-300519496095736769319964186406477641296364427008833/5000000000000000000000000000000000000000000000000",
+    "-150259748047868384659982093203238820648182213480307/2500000000000000000000000000000000000000000000000"
+  ],
+  "status": "PASS_INDEPENDENT_897_BIT_FLOW_CUT_CERTIFICATES"
+}

research/bit-coupled-chart-bound/README.md

@@ -0,0 +1,104 @@
+# Whole-word bound on coupled BIT chart relabeling
+
+On the retained BIT word, a single adjacent nested chart pair cannot
+support the fixed target κ = 10018846261809/2500000000000000. The
+proof checks all 897 eligible pairs, with no unresolved pair. The exact
+conditional κ change is 0% (**NO VERIFIED GAIN**).
+
+## Scope and bound
+
+Fix the scalar order, logical lifetimes, public starting and final
+charts, every chart outside the active pair, and the complete caller
+bill. For one active pair, relabel any shared ADD contact at either
+chart, with the same label for both operands. The same relaxation
+applies to owned INIT and CLEAR. A physical SWAP carries the contact
+history of its logical role. Consecutive contacts on a role either
+share a chart or use one direct transition between strictly nested
+charts, charged at the dimension difference in either direction. The
+upper bound grants zero incremental setup, scalar work, routing,
+phase, ownership, restoration, precision and tape costs.
+
+The replay reconstructs 32,581 vertices, 62,474 role contact edges
+and all 2,871 original paid MOVEs. The 897 distinct eligible pairs are
+exactly the adjacent nested pairs occurring among those MOVEs.
+For each pair, every variable contact has two possible labels. An
+edge with two variable endpoints has zero cost for equal labels and
+the rank-one tariff for unequal labels. An edge to a fixed endpoint
+contributes a unary cost or forbids an incompatible label. Subtracting
+the smaller of the two unary costs and adding it to a constant gives
+a nonnegative source/sink capacity model. Each flow certificate has
+the same value as its cut. This proves the minimum paid lower bound
+over all simultaneous choices within that pair. Each cut witness
+uses the original labels. The full invoice has 107,352 paid jobs,
+19,950 productive fields and rank surplus 1,506. It is priced as
+productive minus paid moments with rank tariff r^(1−κ). The verifier
+encloses log(r) by a finite atanh series with geometric tail and the
+exponential by alternating Taylor bounds. It rounds lower and upper
+tariffs outward on the 10⁻⁴⁹ grid. Comparing upper old tariffs with
+lower new tariffs leaves at most
+`837/1250000000000000000000000000000000000000000000000` raw
+savings across the complete 36-copy invoice from interval rounding.
+The best whole-invoice net upper is exactly
+`-150259748047868384659982093203238820648182213478633/2500000000000000000000000000000000000000000000000`
+(approximately −60.10389921914735).
+
+The initial independent-edge bound retained all 897 pairs. The
+first exact solver hit its 90-second cap. A 16-pair Dinic retry and
+an 881-pair continuation then exhausted the scope. The retained
+certificate verifies the exhaustive result without an optimizer.
+No physical instance or changed BIT supplier was built.
+
+## Replay
+
+From a clean repository checkout, with CPython 3.12 and assertions:
+
+```sh
+python3.12 -B scripts/research_package.py --package research/bit-coupled-chart-bound
+```
+
+The two live inputs are the word and invoice under
+`research/paired-query-only-bit` at canonical commit
+`e54523517d0f03e58352e647c403a5af3e525a57`. The
+[source manifest](SOURCES.json) pins both paths, Git blobs and SHA-256
+digests. For a verified Git-free export, run from the extracted root:
+
+```sh
+python3.12 -I -B research/bit-coupled-chart-bound/verify.py --root .
+```
+
+The independent checker rebuilds the literal logical lifetimes,
+uses rational Gaussian elimination for nesting, reconstructs the
+full 36-copy signed invoice, and checks every directed cut/flow
+certificate. It tests altered source bytes and a forged flow.
+Expected output and the SHA-256 digest of the decompressed certificate
+are in [AUDIT.json](AUDIT.json). The certificates use exact integer
+capacities at the directed tariff grid declared in the verifier.
+
+## Open next questions
+
+Can simultaneous choices among three or more chart labels change the
+paid profile? First bound a specified multichart component with each
+shared ADD contact and endpoint charged once. A target-clearing bound
+would need an exact arbitrary-input action and fully charged replay.
+Additional intermediate moves, new chart stock, changes to contact
+order or lifetimes, and caller changes are outside this proof. Pairwise
+bounds cannot be added for overlapping changes.
+
+## Credit
+
+[#6726](https://github.com/CrocSwap/integer-mult-bounds/pull/6726)
+supplies the native BIT word and
+[#7001](https://github.com/CrocSwap/integer-mult-bounds/pull/7001)
+supplies the paired caller and retained signed invoice. The original
+attribution and license remain with those files.
+[#7289](https://github.com/CrocSwap/integer-mult-bounds/pull/7289)
+bounds balanced changes to ingress destinations at fixed clocks.
+[#7293](https://github.com/CrocSwap/integer-mult-bounds/pull/7293)
+fixes the original charts and tests the available destination span.
+This proof couples chart changes across both ADD operands and charges
+each contact edge once. [#7277](https://github.com/CrocSwap/integer-mult-bounds/pull/7277)
+is the separately reproduced complete conditional comparator used in
+this campaign. The campaign's Round 30 complex flow audit supplied the
+certificate algorithm.
+OpenAI Codex and subagents materially assisted the proof, implementation,
+independent audit and packaging. Apache-2.0.

research/bit-coupled-chart-bound/SOURCES.json

@@ -0,0 +1,30 @@
+{
+  "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"
+    },
+    {
+      "path": "research/paired-query-only-bit/EFREE-RESULT.json",
+      "usage": "input",
+      "git_blob": "575f76487f9999ecc3e7b1b70f9f71bc582ef8a8",
+      "sha256": "a46b6c6040f75184cab5467656811ad988c216e3bc8e44d595a5015b6e49620b"
+    }
+  ]
+}

research/bit-coupled-chart-bound/TASK.json

@@ -0,0 +1,77 @@
+{
+  "schema_version": 1,
+  "task_id": "bit-helper-contract",
+  "priority_revision": 8,
+  "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57",
+  "original_card": {
+    "id": "bit-helper-contract",
+    "question": "Can a changed G20 helper path or independent-target split improve the complete BIT moment without losing its physical endpoint?",
+    "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"
+    ],
+    "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."
+    ],
+    "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.",
+    "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."
+    },
+    "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.",
+    "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.",
+    "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."
+    ],
+    "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."
+    ],
+    "overlap_terms": [
+      "G20",
+      "helper split",
+      "5679",
+      "5708",
+      "independent target"
+    ],
+    "existing_checks": [
+      {
+        "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.",
+        "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.",
+        "status": "reviewed",
+        "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137",
+        "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5"
+      }
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "One adjacent nested chart pair at a time on the retained #7001/#6726 BIT word, with both ADD operands sharing their new chart and the complete 36-copy invoice.",
+  "scope_change_reason": "This holds scalar order, logical lifetimes, chart stock, public endpoints and caller fixed while changing both sides of shared ADD contacts.",
+  "bottleneck_link": "The complete retained BIT invoice is short by approximately 60.10389921914735 raw directed units at the fixed campaign target.",
+  "budget_minutes": 9,
+  "stop_rule": "Screen all eligible pair scopes within 180 seconds. A 90-second leading-cut attempt and 90-second 16-cut retry precede a 180-second continuation over at most 881 cases. Stop on a target-clearing cut, cap, or exhaustion. Independently verify every retained certificate within 180 seconds. A capped scope remains unresolved.",
+  "outcome": "negative-result",
+  "evidence": "README.md, CUTS.json.gz, AUDIT.json and verify.py. All 897 exact cuts and the full signed invoice are checked, with mutation and forged-flow controls.",
+  "author": "Round 30 research campaign",
+  "ai_assistance": "OpenAI Codex and subagents materially assisted proof, implementation, independent audit and packaging.",
+  "open_questions": [
+    {
+      "question": "Can simultaneous choices among three or more chart labels produce a compatible whole-word saving?",
+      "why_it_matters": "One adjacent chart pair alone cannot pay the target shortfall. A shared ADD contact couples any interaction between different pairs.",
+      "first_step": "Fix a bounded multichart component and compute a rigorous global upper with each contact and endpoint paid once before choosing a site.",
+      "blocked_by": "The binary flow certificates do not bound multichart choices. A target-clearing upper still needs a fully charged exact arbitrary-input action and replay."
+    }
+  ]
+}

research/bit-coupled-chart-bound/VERIFY.json

@@ -0,0 +1,24 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/paired-query-only-bit/retained/inputs/BIT-NATIVE-WORD.json.gz",
+    "research/paired-query-only-bit/EFREE-RESULT.json"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-B",
+        "{package}/verify.py",
+        "--root",
+        "."
+      ],
+      "timeout_seconds": 180,
+      "checks": "Authenticate exact canonical BIT inputs and verify all 897 whole-word flow/cut certificates, full directed signed prices and corrupted-input and forged-flow controls."
+    }
+  ]
+}

research/bit-coupled-chart-bound/pricing.py

@@ -0,0 +1,82 @@
+"""Directed interval arithmetic and the retained signed BIT invoice."""
+from collections import Counter
+from fractions import Fraction
+from functools import cache
+
+TARGET = "10018846261809/2500000000000000"
+SCALE = 10**49
+
+
+def rounded(x, upper):
+    scaled = SCALE*x
+    if upper:
+        return Fraction(-((-scaled.numerator) // scaled.denominator), SCALE)
+    return Fraction(scaled.numerator // scaled.denominator, SCALE)
+
+
+@cache
+def log_bounds(x):
+    z = (x-1)/(x+1)
+    terms = 60
+    exact_partial = 2*sum(z**(2*i+1)/(2*i+1) for i in range(terms))
+    tail = 2*z**(2*terms+1)/((2*terms+1)*(1-z*z))
+    return rounded(exact_partial, False), rounded(exact_partial+tail, True)
+
+
+@cache
+def power_bounds(rank, k):
+    binary = 2**(rank.bit_length()-1)
+    shift = binary.bit_length()-1
+    l2, u2 = log_bounds(Fraction(2))
+    lo, hi = log_bounds(Fraction(rank, binary))
+    lo, hi = k*(lo+shift*l2), k*(hi+shift*u2)
+    assert 0 <= lo <= hi < 1
+
+    def exponential(z, terms):
+        total = term = Fraction(1)
+        for i in range(1, terms+1):
+            term *= -z/i
+            total += term
+        return total
+
+    return rounded(rank*exponential(hi, 35), False), rounded(rank*exponential(lo, 34), True)
+
+
+def cost(hist, k):
+    lower = upper = Fraction(0)
+    for r, n in hist.items():
+        a, b = (n*x for x in power_bounds(r, k))
+        lower += min(a, b)
+        upper += max(a, b)
+    return lower, upper
+
+
+def profile(invoice, native, word, ranks):
+    copies = invoice["native_calls"]
+    assert copies == len(invoice["native_instances"]) == 36
+    assert {tuple((r["stage"], r["copy"])) for r in invoice["native_instances"]} == {
+        (stage, which) for stage in range(1, 19) for which in (0, 1)
+    }
+    assert all(r["ports"] == 111 for r in invoice["native_instances"])
+    assert native == Counter({int(r): n for r, n in invoice["native_paid"].items()})
+    assert sum(native.values()) == 2871
+    caller_paid = {1: 444, **{r: 444 for r in range(7, 57, 7)}}
+    assert invoice["event_counts"]["QUERY"]*111 == caller_paid[1]
+    assert invoice["event_counts"]["IDLE_ONE"]*111 == 8*444
+    full_paid = Counter({r: copies*n for r, n in native.items()})
+    full_paid.update(caller_paid)
+
+    helpers = Counter(ranks[word["final"][j]]-ranks[word["start"][j]]
+                      for j in range(222, word["public"]))
+    assert helpers == Counter({int(r): n for r, n in invoice["native_helpers"].items()})
+    caller_targets = {**{r: 444 for r in range(8, 65, 7)}, 127: 222}
+    full_targets = Counter({r: copies*n for r, n in helpers.items()})
+    full_targets.update(caller_targets)
+    assert full_paid == Counter({int(r): n for r, n in invoice["paid"].items()})
+    assert full_targets == Counter({int(r): n for r, n in invoice["targets"].items()})
+    assert sum(full_paid.values()) == invoice["paid_jobs"]
+    assert sum(full_targets.values()) == invoice["productive_fields"]
+    signed = full_targets.copy()
+    signed.subtract(full_paid)
+    assert sum(r*n for r, n in signed.items()) == invoice["rank_surplus"]
+    return signed, copies