diff --git a/docs/ci-verification.md b/docs/ci-verification.md index 63ba3e9aa8..52b62d0481 100644 --- a/docs/ci-verification.md +++ b/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). diff --git a/research/bit-coupled-chart-bound/AUDIT.json b/research/bit-coupled-chart-bound/AUDIT.json new file mode 100644 index 0000000000..e44f42dc0d --- /dev/null +++ b/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" +} diff --git a/research/bit-coupled-chart-bound/CUTS.json.gz b/research/bit-coupled-chart-bound/CUTS.json.gz new file mode 100644 index 0000000000..352274d35a Binary files /dev/null and b/research/bit-coupled-chart-bound/CUTS.json.gz differ diff --git a/research/bit-coupled-chart-bound/README.md b/research/bit-coupled-chart-bound/README.md new file mode 100644 index 0000000000..fcaa076ace --- /dev/null +++ b/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. diff --git a/research/bit-coupled-chart-bound/SOURCES.json b/research/bit-coupled-chart-bound/SOURCES.json new file mode 100644 index 0000000000..2f232fb673 --- /dev/null +++ b/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" + } + ] +} diff --git a/research/bit-coupled-chart-bound/TASK.json b/research/bit-coupled-chart-bound/TASK.json new file mode 100644 index 0000000000..3e6c2dfbe9 --- /dev/null +++ b/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." + } + ] +} diff --git a/research/bit-coupled-chart-bound/VERIFY.json b/research/bit-coupled-chart-bound/VERIFY.json new file mode 100644 index 0000000000..4f2e4485cb --- /dev/null +++ b/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." + } + ] +} diff --git a/research/bit-coupled-chart-bound/pricing.py b/research/bit-coupled-chart-bound/pricing.py new file mode 100644 index 0000000000..40ec194017 --- /dev/null +++ b/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 diff --git a/research/bit-coupled-chart-bound/verify.py b/research/bit-coupled-chart-bound/verify.py new file mode 100644 index 0000000000..048d6fc6b4 --- /dev/null +++ b/research/bit-coupled-chart-bound/verify.py @@ -0,0 +1,241 @@ +"""Independently check every BIT label flow/cut and its complete invoice.""" +from argparse import ArgumentParser +from collections import Counter, defaultdict +from fractions import Fraction as F +from functools import cache +import gzip +from hashlib import sha256 +from itertools import pairwise +import json +from pathlib import Path +import runpy +from time import monotonic + +PACKAGE = Path(__file__).resolve().parent +WORD = "research/paired-query-only-bit/retained/inputs/BIT-NATIVE-WORD.json.gz" +INVOICE = "research/paired-query-only-bit/EFREE-RESULT.json" + + +def authenticate(path, raw, digest): + if sha256(raw).hexdigest() != digest: + raise ValueError(f"changed input {path}") + return raw + + +def load_inputs(root): + manifest = json.loads((PACKAGE / "SOURCES.json").read_bytes()) + pins = {} + for entry in manifest["files"]: + if entry["usage"] != "input": + continue + path = entry["path"] + assert path in (WORD, INVOICE) and path not in pins + pins[path] = entry["sha256"] + assert set(pins) == {WORD, INVOICE} + contents = {} + for path, digest in pins.items(): + raw = (root / path).read_bytes() + contents[path] = authenticate(path, raw, digest) + try: + authenticate(path, raw + b"\n", digest) + except ValueError: + continue + raise AssertionError("mutated source accepted") + return json.loads(gzip.decompress(contents[WORD])), json.loads(contents[INVOICE]) + + + +def incidence(word): + n=word['public'] + slots=list(range(n))+[None]*word['owned_fields'] + attr=[(f,False,-1) for f in word['start']] + visits={i:[i] for i in range(n)} + paid=[] + for t,(op,i,*a) in enumerate(word['program']): + if op=='SWAP': + j=a[0] + slots[i],slots[j]=slots[j],slots[i] + elif op=='MOVE': + paid.append(tuple(a)) + else: + v=len(attr) + attr.append((a[-1],True,t)) + if op=='INIT': + assert slots[i] is None + slots[i]=n+t + visits[n+t]=[v] + else: + visits[slots[i]].append(v) + if op=='ADD' and a[0]!=i: + visits[slots[a[0]]].append(v) + if op=='CLEAR': + slots[i]=None + assert all(v is None for v in slots[n:]) + for i,f in enumerate(word['final']): + visits[slots[i]].append(len(attr)) + attr.append((f,False,len(word['program']))) + assert len(visits)==n+237 + edges=[edge for seq in visits.values() for edge in pairwise(seq)] + assert Counter((attr[u][0],attr[v][0]) for u,v in edges if attr[u][0]!=attr[v][0])==Counter(paid) + return attr,edges,paid + + +def linrank(rows): + pivot={} + for row in rows: + r=list(row) + for j in range(len(r)): + x=r[j] + if not x: + continue + if j in pivot: + r=[a-x*b for a,b in zip(r,pivot[j],strict=True)] + else: + pivot[j]=[a/x for a in r] + break + return len(pivot) + + +def add(cap,u,v,w): + if u!=v and w: + cap[u,v]+=w + + +def certify(caps, flow, side, source, sink, n): + balance=[0]*n + used=set() + for u,v,f in flow: + if (u,v) in used or not 0