diff --git a/.github/workflows/verify.yml b/.github/workflows/verify.yml index e85afe14dd..c6ba75a7bb 100644 --- a/.github/workflows/verify.yml +++ b/.github/workflows/verify.yml @@ -29,6 +29,28 @@ jobs: - name: Require reproducible certificates and patches run: git diff --exit-code + ranked-pair-finite: + runs-on: ubuntu-24.04 + timeout-minutes: 20 + steps: + - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7 + with: + persist-credentials: false + - uses: actions/setup-python@5fda3b95a4ea91299a34e894583c3862153e4b97 # v7 + with: + python-version: '3.13' + - name: Fetch immutable PR62 construction sources + uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7 + with: + repository: CrocSwap/integer-mult-bounds + ref: ad0f25ff7b23cff7f08ad237c2254e6ecf74257e + path: build/ranked-pair-upstream + persist-credentials: false + - name: Independently replay words and rebuild exact CRT profiles + run: make ranked-pair-verify UPSTREAM=build/ranked-pair-upstream + - name: Require unchanged tracked artifacts + run: git diff --exit-code + formal: runs-on: ubuntu-24.04 timeout-minutes: 30 diff --git a/Makefile b/Makefile index a733e4b348..a00aa15c74 100644 --- a/Makefile +++ b/Makefile @@ -71,6 +71,36 @@ verify-certificates: python3 scripts/reuse_network.py python3 scripts/make_reuse_patch.py +# Independent verification of the pending PR62/63 rank-first construction. +# The offline check is separate from the pinned-source, C++/CRT replay. +verify-certificates: ranked-pair-check + +.PHONY: ranked-pair-check ranked-pair-verify formal-ranked-pair-verify +ranked-pair-check: + python3 research/ranked-pair-verification/verify.py + +ranked-pair-verify: ranked-pair-check + test -n "$(UPSTREAM)" + python3 research/ranked-pair-verification/audit/ranked-word-audit.py --upstream "$(UPSTREAM)" --generated build/ranked-pair + +formal-ranked-pair-verify: + python3 research/ranked-pair-verification/lean/check.py + +formal-historical-verify: formal-ranked-pair-verify + +# Later source-bound proof and finite-certificate checkpoint from PR64. +verify-certificates: machine-transfer-check + +.PHONY: machine-transfer-check formal-machine-transfer-verify +machine-transfer-check: + python3 research/machine-transfer-verification/verify.py + +LAKE_PROJECT ?= formal/lean +formal-machine-transfer-verify: + python3 research/machine-transfer-verification/verify_lean.py --lake-project "$(LAKE_PROJECT)" --output build/machine-transfer/lean + +formal-historical-verify: formal-machine-transfer-verify + verify-ternary: python3 scripts/complex_compression.py python3 scripts/make_complex_compression_patch.py diff --git a/README.md b/README.md index 9e01040cbb..371115f610 100644 --- a/README.md +++ b/README.md @@ -158,6 +158,12 @@ scoped negative results and reproducible certificates. ## Citation and license +The [independent rank-first pair verification](research/ranked-pair-verification/README.md) +records a conditional parameter refinement for the pending PR62/63 construction, +exact word/profile checks, and 45 scoped Lean theorems. Its construction matches +concurrent PR63; it does not replace the released bound or verify the full +multiplication machine. + Use [CITATION.cff](CITATION.cff), cite the individual contributions used and include the repository version or commit. [CONTRIBUTORS.md](CONTRIBUTORS.md), [NOTICE](NOTICE) and source-specific manifests preserve the dependency credits. diff --git a/research/machine-transfer-verification/README.md b/research/machine-transfer-verification/README.md new file mode 100644 index 0000000000..a8773e2920 --- /dev/null +++ b/research/machine-transfer-verification/README.md @@ -0,0 +1,137 @@ +# Formal transfer and finite-certificate checkpoint + +This package makes the completed research after the first PR64 checkpoint +reviewable and reproducible. It contains exact finite certificates, reusable +Lean proofs, concrete tape primitives and the current proof boundary. +**The full uniform fixed-tape integer multiplication theorem remains unfinished.** + +The strongest public finite candidate reproduced in this checkpoint is +[PR76](https://github.com/CrocSwap/integer-mult-bounds/pull/76), pinned at +`4b716171d4b3122d6b9db93f802751a41a209955`, with conditional +`kappa = 51738676045141 / 1000000000000000000 = 5.1738676045141e-5`. +Its supplied words, dirty-basis semantics, exact CRT profiles and assembly +arithmetic passed independent checks. Heuristic compiler regeneration was not +run for PR76. The latest **literal real-characteristic Lean instantiation** is +the earlier PR73 profile, with conditional `kappa = 5.1414646104194e-5`. +PR73's later withdrawal does not change its immutable certificate or theorem. +The PR76 result is not silently substituted into that Lean theorem. + +The completed PR69/71 combination experiment has the finite conditional +witness `kappa = 51544825802029 / 1000000000000000000` +(`5.1544825802029e-5`), above PR73 and below PR76. Both changed axes were +compiled and checked, including fresh CRT profiles and complete dirty-basis +replay. Its exact arithmetic is independently recomputed by the offline check; +there is no literal Lean profile instantiation for this experiment. + +## Review map + +| Package | Completed result | Remaining boundary | +| --- | --- | --- | +| `next-proof/analytic` | Actual real log/exp enclosures and characteristic contraction for PR64 | Supplied finite profile and physical realization | +| `next-proof/framed`, `next-proof/rows` | Typed XOR/gauge semantics and exact row-index bijections | Complete generated trace and physical routing | +| `transfer-proof/recurrence` | Floor-child depth, recurrence and uniform state-cost transfer | Named physical implementation hypotheses | +| `transfer-proof/tapes` | Literal fixed-alphabet stack push/pop, clean scratch and restored heads | Recursive scheduler composition | +| `transfer-proof/framed` | Concrete modular address-gauge algebra | Instantiation with the complete selected tables | +| `full-transfer/outerrows` | All-positive-width row supply, padding below factor two and descriptor absorption | Physical gathering and descriptor routines | +| `full-transfer/localization` | Rational table localization, eligible odd primes, unit pivots and modular transport | Concrete complete tables and setup costs | +| `full-transfer/framed` | Tensor identities and complete ambient finite schedule/profile correspondence | External finite checker, inherited local pivots; no full generated Lean trace | +| `full-transfer/latest-analytic` | Actual PR73 real characteristic and conditional state-cost specialization | Full deterministic multiplier | +| `stream-transfer/counters` | Six-state head-local binary counter; exact first completion, head return and fixed-direction amortized cost | Payload/reset/dispatcher costs and integration into routing | +| `stream-transfer/audit` | PR76 supplied-word/CRT/bridge/arithmetic validation and source pins | Compiler discovery regeneration and literal Lean specialization | +| `stream-transfer/experiments` | Bounded balanced-coarse/split-graph experiment and exact comparisons | No claim to beat PR76 or establish a global optimum | + +The counter bound is `4N + 2w` for N primitive calls in a **fixed direction**. +It does not cover arbitrary alternating increments and decrements, or include +the separate costs of payload emission, controller dispatch and counter reset. +Those costs must be included when proving a whole routing routine. + +The integrated inventory has 27 unique modules and 298 theorem/lemma audits. +It includes the 13 earlier `DirtyWrapper` declarations and 12 `FramedXor` +helpers beyond the historical selected prints. Duplicate module copies are +checked byte-for-byte and compiled once. These counts describe audit coverage, +not independent new mathematical results. Only standard Lean foundational +axioms are permitted; sources contain no proof escapes or custom axioms. + +## Reproduce from the repository root + +Python 3.11 or newer, standard library only: + +```sh +make machine-transfer-check +``` + +This validates the publication manifest, binds the PR64/68/73 literal Lean +profiles to their certificates, recomputes exact rational characteristic and +assembly inequalities for those profiles, PR76 and the completed combination, +and repeats the exact +counterexample to universal PR73-over-PR68 power dominance. It does **not** +rerun the Lean kernel, finite words, CRT profiler or compiler discovery. +It is included in `make verify-certificates` and hence `make verify`. + +With the repository's existing Lean 4.21.0 and pinned Mathlib project ready: + +```sh +make formal-machine-transfer-verify +# An already prepared compatible project can be selected explicitly: +make formal-machine-transfer-verify LAKE_PROJECT=/path/to/pinned/mathlib-project +``` + +The checker validates toolchain, dependency revision, source hashes and full +declaration coverage, then compiles all unique modules into a fresh temporary +directory and generates a kernel axiom-audit shim for each. It installs nothing +and writes reports under ignored `build/`. It also runs in the existing +historical formal CI job. Mathlib revision: +`308445d7985027f538e281e18df29ca16ede2ba3`. + +Full finite replay commands require the exact public source checkouts named in +the individual packages. For example, using a local checkout containing PR76 +at its pinned commit and unchanged checked-out files: + +```sh +P=research/machine-transfer-verification +python3 -B "$P/stream-transfer/audit/independent_pr76.py" \ + --repo /path/to/pr76-checkout --output build/pr76-independent.json +``` + +That command replays both entire dirty-state bases, checks literal scatter, +rebuilds the complete paid profile from the supplied axis profiles, and checks +the exact arithmetic. Fresh C++ CRT profiling is a distinct upstream command +documented in `stream-transfer/audit/README.txt`; its saved receipt is included. +The full ambient checks and experimental producer/replay commands have their +own explicit source requirements. Checkers do not fetch or modify tracked +upstream sources; the CRT setup creates an ignored parent archive. + +## Provenance and checkpoint handling + +`publication-manifest.json` is the authoritative hash inventory for this +publication. Leaf theorem manifests, source pins and scientific receipts are +retained. Old aggregate archive manifests, bulky GitHub API dumps, compiler +binaries and build logs are omitted. Historical checkpoint JSON/READMEs record +their status at creation, including statements that a checkpoint was then +unpublished. Their old workspace examples are historical; use the portable +commands above or pass explicit `--lake-project`, `--upstream`/`--repo` and +`--output` arguments to the leaf checkers. The standalone legacy scatter helper +is used through its path-independent library function. + +The manuscript is the completed full-transfer snapshot; current counter and +PR76 findings are documented in their package READMEs. No unfinished +`ClockReset` or integrated routing draft is included. One local source-path +metadata string in `selected-certificate.json` is normalized to the package +relative `pair-ranked-profile.json`; its mathematical fields are unchanged. +Pinned public PR68 and PR73 candidate bytes are preserved exactly. + +Credit for the public constructions and refinements remains with their authors: +Avi Eisenberg's PR62 graph; eumemic's PR57 compiler and PR69 balanced coarse +sums; Chafik Boukhalfa's PR60 priority and PR71 anchored split construction; +Rohan Arun's PR65 scheduling and PR67 costs; Dominik Scholz's PR68 controls and +PR73 parameter refinement; Alejandro Zarzuelo Urdiales's PR70 exchanges; Thomas DiFiore's PR74 node +ordering; and Dominik Scholz's PR76 composition. +All earlier data, complex-layer, matching and assembly credits and notices +remain applicable. This independent verification, formalization and bounded +combination work used substantial OpenAI Codex assistance, including separate +agent reviews. New sources follow the repository's Apache-2.0 license. + +Remaining decisive work is actual digit/row routing, complete table and ordered +child-plan instantiation, one fixed-tape recursive scheduler satisfying the +cost hypotheses, and the analytic resampling/precision/exact-recovery/setup +integration needed for the final multiplication theorem. diff --git a/research/machine-transfer-verification/audit/ranked-candidate-adversarial.json b/research/machine-transfer-verification/audit/ranked-candidate-adversarial.json new file mode 100644 index 0000000000..2971eed89e --- /dev/null +++ b/research/machine-transfer-verification/audit/ranked-candidate-adversarial.json @@ -0,0 +1,302 @@ +{ + "status": "PASS", + "axes": [ + { + "h": 23, + "v": 1771, + "R": 27918, + "word_sha256": "640696dd7cd893add9d6e12d0d587956fecf113b2eff8c29547b82e5a6f3c0ad", + "packed_sha256": "4757871d48bf471053afe4ae432e64432fb35b9b4a364c5939c63df627ebeedc", + "literal_scatter": { + "scatter_xors": 10626, + "central_outputs": 23, + "output_records": 5336, + "literal_binding": true, + "sequence_sha256": "902cb7c280eca5427f02d5b537e35a79612485c1119cfcf2f857e99a401e8fde" + }, + "transition_types": 124481, + "complete_charged_transition_types": 138003, + "transition_artifact": "outputs/audit/ranked-transitions-23.json.gz", + "transition_json_sha256": "2d97456d3dbee82b05ae276c39a1709e2fabaad093b9558af0ae4a8a695ea8eb", + "binary_profiler_input_sha256": "916f8b6ec54eacadaf55db59db03779a841a06a8647f13e8d40e07e451fa51f7", + "side_growth_singletons": 15939, + "full_basis_directions": 31460, + "full_basis_orientations": 2, + "elementary_xors": 149172, + "wrapped_xors": 621482, + "profile": [ + 0, + 343922, + 16866, + 10526, + 5756, + 4155, + 3904, + 3650, + 2861, + 2284, + 1800, + 1716, + 1263, + 1077, + 710, + 590, + 352, + 193, + 114, + 0, + 45, + 23, + 0, + 0 + ], + "mass": 642620, + "profiler_output_sha256": "d536378528a1d45c2c7a92c6173ba05542832edd2bfb4a09d24f883bb04515e2", + "original_profile_sha256": "5b480c170b6c00e8837f7ceebb75e6b53199cbf3a1dfd003c33306648bebc056", + "profile_delta": [ + 0, + 79, + -95, + -22, + -140, + -91, + -3, + -11, + -19, + 23, + 22, + 22, + 21, + 14, + 24, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "capped_delta": { + "1": -176, + "2": -431, + "3": -591, + "4": -729, + "5": -727, + "6": -634, + "7": -538, + "8": -431, + "9": -305, + "10": -202, + "11": -121, + "12": -62, + "13": -24, + "14": 0, + "15": 0, + "16": 0, + "17": 0, + "18": 0, + "19": 0, + "20": 0, + "21": 0, + "22": 0, + "23": 0 + }, + "concave_dominance": "strictly smaller sum n_t*t^p for every 0 assembly-specific two-margin ceiling", + "prior_certificate_sha256": "793d0292546f6f81a28eeddcee89a4dc59bea28283398e8caac8b1287130343d", + "current_certificate_sha256": "432a05ae372a33dd896ea68d9b5ac47a73f9142d07bcab4105d7ba95b46d9186", + "proof_of_unchanged_fields": "Reversing only that wording change reproduces the exact prior serialized-certificate SHA256.", + "moment_and_47_assembly_constraints": "freshly recomputed; same numerical outputs", + "expensive_word_checks": "not repeated; exact construction bytes and all mathematical certificate fields unchanged" + } +} diff --git a/research/machine-transfer-verification/audit/scatter_binding_audit.py b/research/machine-transfer-verification/audit/scatter_binding_audit.py new file mode 100644 index 0000000000..6bf8404c44 --- /dev/null +++ b/research/machine-transfer-verification/audit/scatter_binding_audit.py @@ -0,0 +1,81 @@ +#!/usr/bin/env python3 +"""Independent literal binding of output records to the paid scatter word. + +This check is deliberately separate from the inherited replay. It does not +establish all-size tape transfer, profile completeness, or an asymptotic bound. +""" +import gzip,hashlib,importlib.util,json,pathlib,subprocess,sys,time +if sys.flags.optimize: + raise RuntimeError('Run without -O: assertions are part of this checker') +from collections import Counter +from itertools import combinations +ROOT=pathlib.Path(__file__).resolve().parents[2] +REPO=ROOT/'work/agents/repository-audit/repo' +OUT=ROOT/'outputs/audit' +WORK=ROOT/'work/agents/repository-audit/replay-bindings' +PINS={ + 'pr57':('47916b3bf2895c117f8b53ffff4732f67178a132','certificates/skip-frame-word-{h}.json.gz'), + 'pr58':('96c52fb81cab6e714768e00ca33ca7f004ebcac4','certificates/joint-dual-word-{h}.json.gz'), + 'pr60':('e7a492dd8bee4e6f574ced784a62af2ce735edc4','certificates/joint-dual-word-{h}.json.gz'), + 'pair_assembly':('ad0f25ff7b23cff7f08ad237c2254e6ecf74257e','research/pair-assembly/frame/frame-word-{h}.json.gz'), +} +def blob(pin,path):return subprocess.run(['git','-C',str(REPO),'show',f'{pin}:{path}'],check=True,capture_output=True).stdout + +def verify_scatter(d): + h,v,R=d['h'],d['v'],d['R'];triples=list(combinations(range(h),3));assert len(triples)==v + assert set(map(int,d['sources']))==set(range(v)) + assert all(isinstance(s,int) and 0<=s= 0 else hi) + upper += delta * (hi if delta >= 0 else lo) + bounds.append({'width': t, 'signed_count_cross_product': delta, 'sqrt_lower': str(lo), 'sqrt_upper': str(hi)}) + denom = new['W'] * old['W'] + lower, upper = lower / denom, upper / denom + assert lower > 0 and caps[-1] < 0 + report = { + 'status': 'PASS: exact counterexample to universal power dominance', + 'new_candidate_sha256': sha256(rawnew).hexdigest(), + 'old_candidate_sha256': sha256(rawold).hexdigest(), + 'normalization': 'd_t = n_new(t)*W_old - n_old(t)*W_new; denominators are positive.', + 'positive_capped_sums': sum(c > 0 for c in caps), 'total_caps': len(caps), + 'rank_mass_difference_numerator': caps[-1], + 'witness_power': '1/2', 'equivalent_saving': '1/2', + 'sqrt_weighted_difference_interval': [str(lower), str(upper)], + 'relation_to_characteristic': 'This positive interval bounds sqrt(575)*(Psi_new(1/2)-Psi_old(1/2)). Thus the normalized new characteristic is strictly larger at power1/2.', + 'rows': bounds, + 'scope': 'This refutes all-power dominance, not the newer certified saving near power1. Both original certificates and their small-saving inequalities remain valid.' + } + args.output.parent.mkdir(parents=True, exist_ok=True) + args.output.write_text(json.dumps(report, indent=2) + '\n') + print(report['status']) + print('positive difference lower bound:', lower) + +if __name__ == '__main__': + main() diff --git a/research/machine-transfer-verification/full-transfer/audit/head-changes.json b/research/machine-transfer-verification/full-transfer/audit/head-changes.json new file mode 100644 index 0000000000..090bc724dd --- /dev/null +++ b/research/machine-transfer-verification/full-transfer/audit/head-changes.json @@ -0,0 +1,66 @@ +[ + { + "number": 66, + "title": "Split-pair dual-suffix frames: conditional \u03ba = 4.83109396e-5", + "pin": "568d973df24b0febe8b498fb7cd2513a72742366", + "previous": "b07443b7fb73200eeca4e681a2bccc226ef938b1", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/66", + "repository": "chafreaky/integer-mult-bounds" + }, + { + "number": 67, + "title": "Cost-aware retired-slot selection: conditional \u03ba = 5.1033760584215e-5", + "pin": "46991a21d13f37faf2350591de7d794cfaa4455e", + "previous": "b3745601e947a94316bf25c2c6263d93c06e3364", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/67", + "repository": "rohanarun/integer-mult-bounds" + }, + { + "number": 68, + "title": "Cost-aware live controls: conditional \u03ba = 5.103512721785e-5", + "pin": "b1b2af3415ecb494a0552b16c18045bf3ee05e95", + "previous": "85781f662b57521743cce07cdd5ea194e6f3879d", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/68", + "repository": "DominikScholz/integer-mult-bounds" + }, + { + "number": 69, + "title": "Balanced coarse sums: conditional \u03ba = 5.136837484e-5", + "pin": "91aa1f17e6e3fc063241686a41a34ddd0dc24c50", + "previous": null, + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/69", + "repository": "eumemic/integer-mult-bounds" + }, + { + "number": 70, + "title": "Profile-aware frame compilation: conditional kappa = 5.10403292611078e-5 above frozen #62", + "pin": "11a4e3176511ece840d57b7db045772945d9703c", + "previous": null, + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/70", + "repository": "alejandrozu/integer-mult-bounds" + }, + { + "number": 71, + "title": "Anchored split frames with profile-cost live reclamation: \u03ba = 5.1414646104039e-5", + "pin": "1bef94fd40a746452548c84a4a8f8834670a3113", + "previous": null, + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/71", + "repository": "chafreaky/integer-mult-bounds" + }, + { + "number": 72, + "title": "Searched orders on PR #49's graphs: conditional kappa = 4.125007391e-5", + "pin": "b841eb9de6bb83ccb979296c4e22c44fe842fa67", + "previous": null, + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/72", + "repository": "maxime-fleury/integer-mult-bounds" + }, + { + "number": 73, + "title": "Refine PR71 assembly backoff: conditional \u03ba = 5.1414646104194e-5", + "pin": "253ecc88faeed55a950c76026d1fe67a7f690123", + "previous": null, + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/73", + "repository": "DominikScholz/integer-mult-bounds" + } +] diff --git a/research/machine-transfer-verification/full-transfer/audit/incremental-inventory.json b/research/machine-transfer-verification/full-transfer/audit/incremental-inventory.json new file mode 100644 index 0000000000..ef58b5610d --- /dev/null +++ b/research/machine-transfer-verification/full-transfer/audit/incremental-inventory.json @@ -0,0 +1,820 @@ +{ + "snapshot_file": "github-snapshot.json", + "snapshot_sha256": "bcbbebad1fc634ad0a7c7a402b9b79c44f08bae2bd6237c4e1e5e155747cb13f", + "snapshot_file_mtime_utc": "2026-10-08T19:24:05.616956+00:00", + "total_prs": 73, + "main": "56b66d58297deca1d7dd130247d720e960f77a37", + "changed_or_new": [ + { + "number": 66, + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/66", + "title": "Split-pair dual-suffix frames: conditional \u03ba = 4.83109396e-5", + "author": "chafreaky", + "state": "OPEN", + "draft": false, + "head": "568d973df24b0febe8b498fb7cd2513a72742366", + "base": "fc74109a6978cb1849547e0dcb9d9df995ddaac5", + "previous": "b07443b7fb73200eeca4e681a2bccc226ef938b1", + "reported_kappa": "120777349/2500000000000", + "mechanism": "validation receipt only since prior snapshot", + "audit_depth": "No repeated finite checks; original construction already audited.", + "complete_git_changed_paths": [ + "Makefile", + "NOTICE", + "README.md", + "certificates/joint-dual-kappa.json", + "certificates/joint-dual-validation.json", + "certificates/split-dual-compiler.json", + "certificates/split-dual-kappa.json", + "certificates/split-dual-profiles-23.json", + "certificates/split-dual-profiles-25.json", + "certificates/split-dual-repository-validation.json", + "certificates/split-dual-transitions-23.json", + "certificates/split-dual-transitions-25.json", + "certificates/split-dual-validation.json", + "certificates/split-dual-word-23.json.gz", + "certificates/split-dual-word-25.json.gz", + "docs/ci-verification.md", + "references/frame-compiler/pr59/FETCH.json", + "references/frame-compiler/pr59/LICENSE", + "references/frame-compiler/pr59/NOTICE", + "references/frame-compiler/pr59/SOURCE.json", + "references/frame-compiler/pr59/research/skip-strips/skip_graph.py", + "references/frame-compiler/pr59/research/split-skip/SOURCE.json", + "references/frame-compiler/pr59/research/split-skip/clone-jobs-23.json", + "references/frame-compiler/pr59/research/split-skip/clone-jobs-25.json", + "references/frame-compiler/pr59/research/split-skip/clone_io.py", + "references/frame-compiler/pr59/research/split-skip/cloned_graph.py", + "references/frame-compiler/pr59/research/split-skip/config-23.json", + "references/frame-compiler/pr59/research/split-skip/config-25.json", + "references/frame-compiler/pr59/research/split-skip/split_graph.py", + "references/frame-compiler/pr59/scripts/exclusion_circuit.py", + "references/frame-compiler/pr59/scripts/partial_swap/paired.py", + "references/frame-compiler/pr59/scripts/partial_swap/shared.py", + "references/frame-compiler/pr60/LICENSE", + "references/frame-compiler/pr60/NOTICE", + "references/frame-compiler/pr60/README.md", + "references/frame-compiler/pr60/SOURCE.json", + "references/frame-compiler/pr60/certificates/joint-dual-kappa.json", + "references/frame-compiler/pr60/certificates/joint-dual-repository-validation.json", + "references/frame-compiler/pr60/research/joint-dual/PROOF.md", + "references/frame-compiler/pr60/research/joint-dual/README.md", + "references/frame-compiler/pr60/research/joint-dual/SOURCE.json", + "research/joint-dual/SOURCE.json", + "research/split-dual/PROOF.md", + "research/split-dual/README.md", + "research/split-dual/SOURCE.json", + "research/split-dual/config-23.json", + "research/split-dual/config-25.json", + "scripts/experiments/pin_split_dual_sources.py", + "scripts/experiments/split_dual_compiler.py", + "scripts/experiments/split_dual_compose.py", + "scripts/experiments/split_dual_graph.py", + "scripts/experiments/verify_split_dual.py", + "tests/test_split_dual.py" + ], + "github_files_page_truncated": false, + "comments": 0, + "reviews": 0, + "review_threads": 0 + }, + { + "number": 67, + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/67", + "title": "Cost-aware retired-slot selection: conditional \u03ba = 5.1033760584215e-5", + "author": "rohanarun", + "state": "OPEN", + "draft": false, + "head": "46991a21d13f37faf2350591de7d794cfaa4455e", + "base": "230b5ea8eb9344fd36f13daa2933ab7b027ce046", + "previous": "b3745601e947a94316bf25c2c6263d93c06e3364", + "reported_kappa": "10206752116843/200000000000000000", + "mechanism": "merged contemporary upstream changes; cost-aware scientific package unchanged except validation.json", + "audit_depth": "No repeated finite checks; earlier full focused replay and exact independent audit remain applicable to identical scientific package.", + "complete_git_changed_paths": [ + ".github/workflows/verify.yml", + "Makefile", + "NOTICE", + "README.md", + "certificates/joint-dual-kappa.json", + "certificates/joint-dual-validation.json", + "research/joint-dual/SOURCE.json", + "research/rank-pair/.gitignore", + "research/rank-pair/PROOF.md", + "research/rank-pair/frame-compiler.json", + "research/rank-pair/frame-profiles-23.json", + "research/rank-pair/frame-profiles-25.json", + "research/rank-pair/frame-transitions-23.json", + "research/rank-pair/frame-transitions-25.json", + "research/rank-pair/frame-word-23.json.gz", + "research/rank-pair/frame-word-25.json.gz", + "research/rank-pair/frame_compile.py", + "research/rank-pair/screen-certificate.json", + "research/rank-pair/screen.py", + "research/reordered-rank-pair/README.md", + "research/reordered-rank-pair/arithmetic/README.md", + "research/reordered-rank-pair/arithmetic/audit-receipt.json", + "research/reordered-rank-pair/arithmetic/audit.py", + "research/reordered-rank-pair/arithmetic/certificate.json", + "research/reordered-rank-pair/arithmetic/refine.py", + "research/reordered-rank-pair/arithmetic/test_arithmetic.py", + "research/reordered-rank-pair/current-comparison.json", + "research/reordered-rank-pair/frame-compiler.json", + "research/reordered-rank-pair/frame-profiles-23.json", + "research/reordered-rank-pair/frame-profiles-25.json", + "research/reordered-rank-pair/frame-transitions-23.json", + "research/reordered-rank-pair/frame-transitions-25.json", + "research/reordered-rank-pair/frame-word-23.json.gz", + "research/reordered-rank-pair/frame-word-25.json.gz", + "research/reordered-rank-pair/paired-candidate.json", + "research/reordered-rank-pair/test_negative.py", + "research/reordered-rank-pair/verify.py", + "research/slot-cost-rank-pair/README.md", + "research/slot-cost-rank-pair/arithmetic/README.md", + "research/slot-cost-rank-pair/arithmetic/audit-receipt.json", + "research/slot-cost-rank-pair/arithmetic/audit.py", + "research/slot-cost-rank-pair/arithmetic/certificate.json", + "research/slot-cost-rank-pair/arithmetic/refine.py", + "research/slot-cost-rank-pair/arithmetic/test_arithmetic.py", + "research/slot-cost-rank-pair/compiler.py", + "research/slot-cost-rank-pair/frame-compiler.json", + "research/slot-cost-rank-pair/frame-profiles-23.json", + "research/slot-cost-rank-pair/frame-profiles-25.json", + "research/slot-cost-rank-pair/frame-transitions-23.json", + "research/slot-cost-rank-pair/frame-transitions-25.json", + "research/slot-cost-rank-pair/frame-word-23.json.gz", + "research/slot-cost-rank-pair/frame-word-25.json.gz", + "research/slot-cost-rank-pair/paired-candidate.json", + "research/slot-cost-rank-pair/profile_oracle.cpp", + "research/slot-cost-rank-pair/test_negative.py", + "research/slot-cost-rank-pair/validation.json", + "research/slot-cost-rank-pair/verify.py", + "scripts/experiments/rank_pair_compiler.py", + "tests/test_rank_pair.py" + ], + "github_files_page_truncated": false, + "comments": 0, + "reviews": 0, + "review_threads": 0 + }, + { + "number": 68, + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/68", + "title": "Cost-aware live controls: conditional \u03ba = 5.103512721785e-5", + "author": "DominikScholz", + "state": "OPEN", + "draft": false, + "head": "b1b2af3415ecb494a0552b16c18045bf3ee05e95", + "base": "230b5ea8eb9344fd36f13daa2933ab7b027ce046", + "previous": "85781f662b57521743cce07cdd5ea194e6f3879d", + "reported_kappa": "1020702544357/20000000000000000", + "mechanism": "positive assembly backoff refinement on unchanged cost/live physical words", + "audit_depth": "Changed code and proof inspected; exact physical inputs unchanged from independently replayed85781f6. New parameter witness reported, not separately rerun in this pass.", + "complete_git_changed_paths": [ + ".github/workflows/verify.yml", + "Makefile", + "NOTICE", + "README.md", + "certificates/joint-dual-kappa.json", + "certificates/joint-dual-validation.json", + "research/circuit-space-clearing/.gitignore", + "research/circuit-space-clearing/README.md", + "research/circuit-space-clearing/compiler.py", + "research/circuit-space-clearing/draft-manifest.json", + "research/circuit-space-clearing/pr67-profiles-23.json", + "research/circuit-space-clearing/pr67-profiles-25.json", + "research/circuit-space-clearing/profile_oracle.cpp", + "research/circuit-space-clearing/run.py", + "research/circuit-space-clearing/screen.py", + "research/circuit-space-clearing/selected/arithmetic.json", + "research/circuit-space-clearing/selected/profile-23.json", + "research/circuit-space-clearing/selected/result-23.json", + "research/circuit-space-clearing/selected/transitions-23.bin.json", + "research/circuit-space-clearing/selected/word-23.json.gz", + "research/cost-live-both/.gitignore", + "research/cost-live-both/PROOF.md", + "research/cost-live-both/README.md", + "research/cost-live-both/candidate.json", + "research/cost-live-both/compiler.py", + "research/cost-live-both/experiment.py", + "research/cost-live-both/focused-manifest.json", + "research/cost-live-both/frame-compiler.json", + "research/cost-live-both/frame-profiles-23.json", + "research/cost-live-both/frame-profiles-25.json", + "research/cost-live-both/frame-transitions-23.json", + "research/cost-live-both/frame-transitions-25.json", + "research/cost-live-both/frame-word-23.json.gz", + "research/cost-live-both/frame-word-25.json.gz", + "research/cost-live-both/preserved-manifest.json", + "research/cost-live-both/profile_oracle.cpp", + "research/cost-live-both/validate.py", + "research/cost-live-both/validation-receipt.json", + "research/cost-live-composition/.gitignore", + "research/cost-live-composition/PROOF.md", + "research/cost-live-composition/README.md", + "research/cost-live-composition/candidate.json", + "research/cost-live-composition/compiler.py", + "research/cost-live-composition/experiment.py", + "research/cost-live-composition/frame-compiler.json", + "research/cost-live-composition/frame-profiles-23.json", + "research/cost-live-composition/frame-profiles-25.json", + "research/cost-live-composition/frame-transitions-23.json", + "research/cost-live-composition/frame-transitions-25.json", + "research/cost-live-composition/frame-word-23.json.gz", + "research/cost-live-composition/frame-word-25.json.gz", + "research/cost-live-composition/preserved-manifest.json", + "research/cost-live-composition/profile_oracle.cpp", + "research/cost-live-composition/validate.py", + "research/cost-live-parameters/PROOF.md", + "research/cost-live-parameters/certificate.json", + "research/cost-live-parameters/refine.py", + "research/cost-live-parameters/source-manifest.json", + "research/global-anchor-screen/PROOF.md", + "research/global-anchor-screen/SOURCE.json", + "research/global-anchor-screen/check_dominance.py", + "research/global-anchor-screen/comparison-pr63.json", + "research/global-anchor-screen/compiler-frozen.py", + "research/global-anchor-screen/concavity-screen.json", + "research/global-anchor-screen/controls.py", + "research/global-anchor-screen/evaluate.py", + "research/global-anchor-screen/selected-arithmetic.json", + "research/global-anchor-screen/selected-manifest.json", + "research/global-anchor-screen/selected-profiles-23.json", + "research/global-anchor-screen/selected-profiles-25.json", + "research/global-anchor-screen/selected-replay-23.json", + "research/global-anchor-screen/selected-replay-25.json", + "research/global-anchor-screen/selected-reproduction.json", + "research/global-anchor-screen/selected-result-23.json", + "research/global-anchor-screen/selected-result-25.json", + "research/global-anchor-screen/selected-word-23.json.gz", + "research/global-anchor-screen/selected-word-25.json.gz", + "research/global-anchor-screen/selected_compile.py", + "research/global-anchor-screen/validation.json", + "research/global-anchor-screen/verify.py", + "research/joint-dual/SOURCE.json", + "research/rank-pair/.gitignore", + "research/rank-pair/PROOF.md", + "research/rank-pair/frame-compiler.json", + "research/rank-pair/frame-profiles-23.json", + "research/rank-pair/frame-profiles-25.json", + "research/rank-pair/frame-transitions-23.json", + "research/rank-pair/frame-transitions-25.json", + "research/rank-pair/frame-word-23.json.gz", + "research/rank-pair/frame-word-25.json.gz", + "research/rank-pair/frame_compile.py", + "research/rank-pair/screen-certificate.json", + "research/rank-pair/screen.py", + "research/slot-cost-rank-pair/README.md", + "research/slot-cost-rank-pair/arithmetic/README.md", + "research/slot-cost-rank-pair/arithmetic/audit-receipt.json", + "research/slot-cost-rank-pair/arithmetic/audit.py", + "research/slot-cost-rank-pair/arithmetic/certificate.json", + "research/slot-cost-rank-pair/arithmetic/refine.py", + "research/slot-cost-rank-pair/arithmetic/test_arithmetic.py", + "research/slot-cost-rank-pair/compiler.py", + "research/slot-cost-rank-pair/frame-compiler.json", + "research/slot-cost-rank-pair/frame-profiles-23.json", + "research/slot-cost-rank-pair/frame-profiles-25.json", + "research/slot-cost-rank-pair/frame-transitions-23.json", + "research/slot-cost-rank-pair/frame-transitions-25.json", + "research/slot-cost-rank-pair/frame-word-23.json.gz", + "research/slot-cost-rank-pair/frame-word-25.json.gz", + "research/slot-cost-rank-pair/paired-candidate.json", + "research/slot-cost-rank-pair/profile_oracle.cpp", + "research/slot-cost-rank-pair/test_negative.py", + "research/slot-cost-rank-pair/verify.py", + "scripts/experiments/rank_pair_compiler.py", + "tests/test_rank_pair.py" + ], + "github_files_page_truncated": true, + "comments": 0, + "reviews": 0, + "review_threads": 0 + }, + { + "number": 69, + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/69", + "title": "Balanced coarse sums: conditional \u03ba = 5.136837484e-5", + "author": "eumemic", + "state": "OPEN", + "draft": true, + "head": "91aa1f17e6e3fc063241686a41a34ddd0dc24c50", + "base": "230b5ea8eb9344fd36f13daa2933ab7b027ce046", + "previous": null, + "reported_kappa": "1284209371/25000000000000", + "mechanism": "balance four-edge coarse sums into shared column pairs before their total", + "audit_depth": "Read changed graph/compiler and certificate claims; no fresh producer/CRT run. Retains older rank-first compiler. Potentially composable with71 graph/67-68 compiler, but untested.", + "complete_git_changed_paths": [ + ".github/workflows/verify.yml", + "Makefile", + "NOTICE", + "certificates/balanced-coarse-compiler.json", + "certificates/balanced-coarse-independent-audit.json", + "certificates/balanced-coarse-kappa.json", + "certificates/balanced-coarse-profiles-23.json", + "certificates/balanced-coarse-profiles-25.json", + "certificates/balanced-coarse-transitions-23.json", + "certificates/balanced-coarse-transitions-25.json", + "certificates/balanced-coarse-validation.json", + "certificates/balanced-coarse-word-23.json.gz", + "certificates/balanced-coarse-word-25.json.gz", + "certificates/ranked-interval-compiler.json", + "certificates/ranked-interval-kappa.json", + "certificates/ranked-interval-profiles-23.json", + "certificates/ranked-interval-profiles-25.json", + "certificates/ranked-interval-transitions-23.json", + "certificates/ranked-interval-transitions-25.json", + "certificates/ranked-interval-validation.json", + "certificates/ranked-interval-word-23.json.gz", + "certificates/ranked-interval-word-25.json.gz", + "references/frame-compiler/balanced-coarse/SOURCE.json", + "references/frame-compiler/pr62/LICENSE", + "references/frame-compiler/pr62/NOTICE", + "references/frame-compiler/pr62/SOURCE.json", + "references/frame-compiler/pr62/comparison-pr62.json", + "references/frame-compiler/pr62/research/pair-assembly/pair_graph.py", + "scripts/experiments/balanced_coarse_README.txt", + "scripts/experiments/balanced_coarse_compiler.py", + "scripts/experiments/balanced_coarse_compose.py", + "scripts/experiments/pr62_exploration/audit_balanced_coarse.py", + "scripts/experiments/ranked_interval_README.txt", + "scripts/experiments/ranked_interval_compiler.py", + "scripts/experiments/ranked_interval_compose.py", + "scripts/experiments/verify_balanced_coarse.py", + "scripts/experiments/verify_ranked_interval.py" + ], + "github_files_page_truncated": false, + "comments": 0, + "reviews": 0, + "review_threads": 0 + }, + { + "number": 70, + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/70", + "title": "Profile-aware frame compilation: conditional kappa = 5.10403292611078e-5 above frozen #62", + "author": "alejandrozu", + "state": "OPEN", + "draft": false, + "head": "11a4e3176511ece840d57b7db045772945d9703c", + "base": "230b5ea8eb9344fd36f13daa2933ab7b027ce046", + "previous": null, + "reported_kappa": "255201646305539/5000000000000000000", + "mechanism": "actual profile-moment costs for retired dependency circuits and bounded carried-signal exchanges on frozen62", + "audit_depth": "Read discovery algorithm, exact acceptance boundaries, strict scatter verifier, and two main Boolean Lean modules; no fresh builds or word/CRT replay. Claimed53 endpoints not independently recounted here.", + "complete_git_changed_paths": [ + "README.md", + "research/profile-aware-frame-search/.gitattributes", + "research/profile-aware-frame-search/.gitignore", + "research/profile-aware-frame-search/README.md", + "research/profile-aware-frame-search/candidate-certificate.json", + "research/profile-aware-frame-search/discovery/SEARCH.md", + "research/profile-aware-frame-search/discovery/build_pair_oracle.py", + "research/profile-aware-frame-search/discovery/compiler_profile_cost4_exchange_3d3d6f5c9a0b.py", + "research/profile-aware-frame-search/discovery/complement_search.py", + "research/profile-aware-frame-search/discovery/make_ledger.py", + "research/profile-aware-frame-search/discovery/matching-h23.json.gz", + "research/profile-aware-frame-search/discovery/matching-h25.json.gz", + "research/profile-aware-frame-search/discovery/pair-profiles-h23-c7b82221d91c24bd91cbdcc3c6280598ba39895d53c29bb751f810e08958f858.jsonl.gz", + "research/profile-aware-frame-search/discovery/pair-profiles-h25-a03304eb61e7e1497a563b2484859c29f9246b7e6839878e28a0b14d3cae88d2.jsonl.gz", + "research/profile-aware-frame-search/discovery/profile_cost4_exchange-regeneration.json", + "research/profile-aware-frame-search/discovery/regenerate_portable.py", + "research/profile-aware-frame-search/discovery/relabel_word.py", + "research/profile-aware-frame-search/discovery/runner-2d545544e429a83aea08c1d6b344dff149b1bfc75fcd9685c148bb01934f61f5.py", + "research/profile-aware-frame-search/discovery/search-ledger.json", + "research/profile-aware-frame-search/discovery/selected4-regeneration-receipt.json", + "research/profile-aware-frame-search/discovery/session.json", + "research/profile-aware-frame-search/discovery/verify_regeneration.py", + "research/profile-aware-frame-search/manifest.json", + "research/profile-aware-frame-search/math/Audit-compile.log", + "research/profile-aware-frame-search/math/Audit.lean", + "research/profile-aware-frame-search/math/CoordinateConjugacy-compile.log", + "research/profile-aware-frame-search/math/CoordinateConjugacy.lean", + "research/profile-aware-frame-search/math/DirtyComplementSafety-compile.log", + "research/profile-aware-frame-search/math/DirtyComplementSafety.lean", + "research/profile-aware-frame-search/math/FiniteRationalChecks-compile.log", + "research/profile-aware-frame-search/math/FiniteRationalChecks.lean", + "research/profile-aware-frame-search/math/FreshKernelReclaim-compile.log", + "research/profile-aware-frame-search/math/FreshKernelReclaim.lean", + "research/profile-aware-frame-search/math/ProfileSearchCertificate-compile.log", + "research/profile-aware-frame-search/math/ProfileSearchCertificate.lean", + "research/profile-aware-frame-search/math/RankFlowPrice-compile.log", + "research/profile-aware-frame-search/math/RankFlowPrice.lean", + "research/profile-aware-frame-search/math/generate_profile_case.py", + "research/profile-aware-frame-search/math/lake-manifest.json", + "research/profile-aware-frame-search/math/lakefile.lean", + "research/profile-aware-frame-search/math/lean-receipt.json", + "research/profile-aware-frame-search/math/lean-toolchain", + "research/profile-aware-frame-search/math/old-profile-lower-data.json", + "research/profile-aware-frame-search/math/verify.ps1", + "research/profile-aware-frame-search/math/verify_math.py", + "research/profile-aware-frame-search/math/weighted-input.json", + "research/profile-aware-frame-search/matrix-exponent-synthesis.tex", + "research/profile-aware-frame-search/receipts/compiled-23.json", + "research/profile-aware-frame-search/receipts/compiled-25.json", + "research/profile-aware-frame-search/receipts/verified-axis-23.json", + "research/profile-aware-frame-search/receipts/verified-axis-25.json", + "research/profile-aware-frame-search/selection-provenance.json", + "research/profile-aware-frame-search/verification/README.md", + "research/profile-aware-frame-search/verification/batch_axes.py", + "research/profile-aware-frame-search/verification/check_guards.py", + "research/profile-aware-frame-search/verification/export_weighted_case.py", + "research/profile-aware-frame-search/verification/frozen-sources.json", + "research/profile-aware-frame-search/verification/screen_axes.py", + "research/profile-aware-frame-search/verification/verify_words.py", + "research/profile-aware-frame-search/words/word-23.json.gz", + "research/profile-aware-frame-search/words/word-25.json.gz" + ], + "github_files_page_truncated": false, + "comments": 0, + "reviews": 0, + "review_threads": 0 + }, + { + "number": 71, + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/71", + "title": "Anchored split frames with profile-cost live reclamation: \u03ba = 5.1414646104039e-5", + "author": "chafreaky", + "state": "OPEN", + "draft": true, + "head": "1bef94fd40a746452548c84a4a8f8834670a3113", + "base": "56b66d58297deca1d7dd130247d720e960f77a37", + "previous": null, + "reported_kappa": "51414646104039/1000000000000000000", + "mechanism": "anchored [1,1,2] split groups,65 region schedules,67 cost selection,68 pending live controls and known-next-use scoring", + "audit_depth": "Full focused producer regeneration, exact word equality, dirty basis/frame replay, fresh CRT both axes, exact arithmetic and23 tests PASSED; independent both-axis F2/scatter and paid-profile assembly also passed. See pr71-73-verification-receipt.json.", + "complete_git_changed_paths": [ + "Makefile", + "NOTICE", + "README.md", + "certificates/joint-dual-kappa.json", + "certificates/joint-dual-validation.json", + "certificates/split-pair-compiler.json", + "certificates/split-pair-kappa.json", + "certificates/split-pair-profiles-23.json", + "certificates/split-pair-profiles-25.json", + "certificates/split-pair-repository-validation.json", + "certificates/split-pair-transitions-23.json", + "certificates/split-pair-transitions-25.json", + "certificates/split-pair-validation.json", + "certificates/split-pair-word-23.json.gz", + "certificates/split-pair-word-25.json.gz", + "references/frame-compiler/pr59-split-operation/LICENSE", + "references/frame-compiler/pr59-split-operation/NOTICE", + "references/frame-compiler/pr59-split-operation/SOURCE.json", + "references/frame-compiler/pr59-split-operation/research/split-skip/SOURCE.json", + "references/frame-compiler/pr59-split-operation/research/split-skip/split_graph.py", + "references/frame-compiler/pr65/LICENSE", + "references/frame-compiler/pr65/NOTICE", + "references/frame-compiler/pr65/SOURCE.json", + "references/frame-compiler/pr65/references/frame-compiler/pr48/SOURCE.json", + "references/frame-compiler/pr65/references/frame-compiler/pr48/research/copied-fixed/balanced_assembly.py", + "references/frame-compiler/pr65/references/frame-compiler/pr48/research/copied-fixed/certificate.json", + "references/frame-compiler/pr65/references/frame-compiler/pr48/research/copied-fixed/changed_graph.py", + "references/frame-compiler/pr65/references/frame-compiler/pr48/research/copied-fixed/profiles.cpp", + "references/frame-compiler/pr65/references/frame-compiler/pr48/research/copied-fixed/verify.py", + "references/frame-compiler/pr65/references/frame-compiler/pr48/scripts/exclusion_circuit.py", + "references/frame-compiler/pr65/references/frame-compiler/pr48/scripts/partial_swap/binary_io.hpp", + "references/frame-compiler/pr65/references/frame-compiler/pr48/scripts/partial_swap/paired.py", + "references/frame-compiler/pr65/references/frame-compiler/pr48/scripts/partial_swap/shared.py", + "references/frame-compiler/pr65/research/pair-assembly/PROOF.md", + "references/frame-compiler/pr65/research/pair-assembly/SOURCE.json", + "references/frame-compiler/pr65/research/pair-assembly/frame/frame-compiler.json", + "references/frame-compiler/pr65/research/pair-assembly/frame/frame_verify.py", + "references/frame-compiler/pr65/research/pair-assembly/pair_graph.py", + "references/frame-compiler/pr65/research/reordered-rank-pair/README.md", + "references/frame-compiler/pr65/research/reordered-rank-pair/arithmetic/README.md", + "references/frame-compiler/pr65/research/reordered-rank-pair/arithmetic/audit-receipt.json", + "references/frame-compiler/pr65/research/reordered-rank-pair/arithmetic/audit.py", + "references/frame-compiler/pr65/research/reordered-rank-pair/arithmetic/certificate.json", + "references/frame-compiler/pr65/research/reordered-rank-pair/arithmetic/refine.py", + "references/frame-compiler/pr65/research/reordered-rank-pair/arithmetic/test_arithmetic.py", + "references/frame-compiler/pr65/research/reordered-rank-pair/current-comparison.json", + "references/frame-compiler/pr65/research/reordered-rank-pair/frame-compiler.json", + "references/frame-compiler/pr65/research/reordered-rank-pair/frame-profiles-23.json", + "references/frame-compiler/pr65/research/reordered-rank-pair/frame-profiles-25.json", + "references/frame-compiler/pr65/research/reordered-rank-pair/frame-transitions-23.json", + "references/frame-compiler/pr65/research/reordered-rank-pair/frame-transitions-25.json", + "references/frame-compiler/pr65/research/reordered-rank-pair/frame-word-23.json.gz", + "references/frame-compiler/pr65/research/reordered-rank-pair/frame-word-25.json.gz", + "references/frame-compiler/pr65/research/reordered-rank-pair/paired-candidate.json", + "references/frame-compiler/pr65/research/reordered-rank-pair/test_negative.py", + "references/frame-compiler/pr65/research/reordered-rank-pair/verify.py", + "references/frame-compiler/pr65/scripts/exclusion_circuit.py", + "references/frame-compiler/pr65/scripts/experiments/binary_frame_math.py", + "references/frame-compiler/pr65/scripts/experiments/binary_frame_profile_prepare.py", + "references/frame-compiler/pr65/scripts/experiments/binary_frame_profiles.cpp", + "references/frame-compiler/pr65/scripts/experiments/binary_frame_replay.py", + "references/frame-compiler/pr65/scripts/experiments/rank_pair_compiler.py", + "references/frame-compiler/pr65/scripts/partial_swap/paired.py", + "references/frame-compiler/pr65/scripts/partial_swap/shared.py", + "references/frame-compiler/pr67/LICENSE", + "references/frame-compiler/pr67/NOTICE", + "references/frame-compiler/pr67/SOURCE.json", + "references/frame-compiler/pr67/research/slot-cost-rank-pair/README.md", + "references/frame-compiler/pr67/research/slot-cost-rank-pair/arithmetic/certificate.json", + "references/frame-compiler/pr67/research/slot-cost-rank-pair/compiler.py", + "references/frame-compiler/pr67/research/slot-cost-rank-pair/frame-compiler.json", + "references/frame-compiler/pr67/research/slot-cost-rank-pair/paired-candidate.json", + "references/frame-compiler/pr67/research/slot-cost-rank-pair/profile_oracle.cpp", + "references/frame-compiler/pr67/research/slot-cost-rank-pair/verify.py", + "references/frame-compiler/pr68/LICENSE", + "references/frame-compiler/pr68/NOTICE", + "references/frame-compiler/pr68/SOURCE.json", + "references/frame-compiler/pr68/research/global-anchor-screen/PROOF.md", + "references/frame-compiler/pr68/research/global-anchor-screen/SOURCE.json", + "references/frame-compiler/pr68/research/global-anchor-screen/compiler-frozen.py", + "references/frame-compiler/pr68/research/global-anchor-screen/selected-manifest.json", + "references/frame-compiler/pr68/research/global-anchor-screen/selected_compile.py", + "research/joint-dual/SOURCE.json", + "research/split-pair/PROOF.md", + "research/split-pair/README.md", + "research/split-pair/SOURCE.json", + "research/split-pair/config-23.json", + "research/split-pair/config-25.json", + "research/split-pair/engine-changes.patch", + "research/split-pair/engine-provenance.json", + "research/split-pair/parameters.json", + "scripts/experiments/pin_split_pair_sources.py", + "scripts/experiments/split_pair_arithmetic.py", + "scripts/experiments/split_pair_compiler.py", + "scripts/experiments/split_pair_compose.py", + "scripts/experiments/split_pair_engine.py", + "scripts/experiments/split_pair_graph.py", + "scripts/experiments/verify_split_pair.py", + "tests/test_split_pair.py", + "tests/test_split_pair_pending.py" + ], + "github_files_page_truncated": false, + "comments": 0, + "reviews": 0, + "review_threads": 0 + }, + { + "number": 72, + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/72", + "title": "Searched orders on PR #49's graphs: conditional kappa = 4.125007391e-5", + "author": "maxime-fleury", + "state": "CLOSED", + "draft": false, + "head": "b841eb9de6bb83ccb979296c4e22c44fe842fa67", + "base": "56b66d58297deca1d7dd130247d720e960f77a37", + "previous": null, + "reported_kappa": "4125007391/100000000000000", + "mechanism": "role-count order descent on49 graph; closed as superseded", + "audit_depth": "Read graph/source and author status corrections. No fresh replay. README local-optimum statement conflicts with its stopped-while-improving statement; no optimum certified.", + "complete_git_changed_paths": [ + "Makefile", + "README.md", + "research/ordered-descent/README.md", + "research/ordered-descent/SOURCE.json", + "research/ordered-descent/bits-23.json", + "research/ordered-descent/bits-25.json", + "research/ordered-descent/certificate.json", + "research/ordered-descent/climbed_graph.py", + "research/ordered-descent/comparison-climbed48.json", + "research/ordered-descent/comparison-pr40.json", + "research/ordered-descent/comparison-pr41.json", + "research/ordered-descent/comparison-pr42.json", + "research/ordered-descent/comparison-pr43.json", + "research/ordered-descent/comparison-pr44.json", + "research/ordered-descent/comparison-pr46.json", + "research/ordered-descent/comparison-pr47.json", + "research/ordered-descent/comparison-pr48.json", + "research/ordered-descent/links-23.uses", + "research/ordered-descent/links-25.uses", + "research/ordered-descent/optimize_matching.py", + "research/ordered-descent/original-23.json", + "research/ordered-descent/original-25.json", + "research/ordered-descent/producer.py", + "research/ordered-descent/profiles-23.json", + "research/ordered-descent/profiles-25.json", + "research/ordered-descent/profiles.cpp", + "research/ordered-descent/scalar-23.json", + "research/ordered-descent/scalar-25.json", + "research/ordered-descent/timeline-23.json", + "research/ordered-descent/timeline-25.json", + "research/ordered-descent/witness.py", + "tests/test_ordered_descent.py" + ], + "github_files_page_truncated": false, + "comments": 2, + "reviews": 0, + "review_threads": 0 + }, + { + "number": 73, + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/73", + "title": "Refine PR71 assembly backoff: conditional \u03ba = 5.1414646104194e-5", + "author": "DominikScholz", + "state": "OPEN", + "draft": true, + "head": "253ecc88faeed55a950c76026d1fe67a7f690123", + "base": "56b66d58297deca1d7dd130247d720e960f77a37", + "previous": null, + "reported_kappa": "25707323052097/500000000000000000", + "mechanism": "10^-18 assembly backoff on immutable71 construction", + "audit_depth": "Fresh parent-archive source closure and parameter regeneration byte-identical; independent characteristic and47 inequalities/seven margins passed. New actual-real Lean profile certificate passed66 audits; global physical theorem remains conditional.", + "complete_git_changed_paths": [ + "Makefile", + "NOTICE", + "README.md", + "certificates/joint-dual-kappa.json", + "certificates/joint-dual-validation.json", + "certificates/split-pair-compiler.json", + "certificates/split-pair-kappa.json", + "certificates/split-pair-profiles-23.json", + "certificates/split-pair-profiles-25.json", + "certificates/split-pair-repository-validation.json", + "certificates/split-pair-transitions-23.json", + "certificates/split-pair-transitions-25.json", + "certificates/split-pair-validation.json", + "certificates/split-pair-word-23.json.gz", + "certificates/split-pair-word-25.json.gz", + "references/frame-compiler/pr59-split-operation/LICENSE", + "references/frame-compiler/pr59-split-operation/NOTICE", + "references/frame-compiler/pr59-split-operation/SOURCE.json", + "references/frame-compiler/pr59-split-operation/research/split-skip/SOURCE.json", + "references/frame-compiler/pr59-split-operation/research/split-skip/split_graph.py", + "references/frame-compiler/pr65/LICENSE", + "references/frame-compiler/pr65/NOTICE", + "references/frame-compiler/pr65/SOURCE.json", + "references/frame-compiler/pr65/references/frame-compiler/pr48/SOURCE.json", + "references/frame-compiler/pr65/references/frame-compiler/pr48/research/copied-fixed/balanced_assembly.py", + "references/frame-compiler/pr65/references/frame-compiler/pr48/research/copied-fixed/certificate.json", + "references/frame-compiler/pr65/references/frame-compiler/pr48/research/copied-fixed/changed_graph.py", + "references/frame-compiler/pr65/references/frame-compiler/pr48/research/copied-fixed/profiles.cpp", + "references/frame-compiler/pr65/references/frame-compiler/pr48/research/copied-fixed/verify.py", + "references/frame-compiler/pr65/references/frame-compiler/pr48/scripts/exclusion_circuit.py", + "references/frame-compiler/pr65/references/frame-compiler/pr48/scripts/partial_swap/binary_io.hpp", + "references/frame-compiler/pr65/references/frame-compiler/pr48/scripts/partial_swap/paired.py", + "references/frame-compiler/pr65/references/frame-compiler/pr48/scripts/partial_swap/shared.py", + "references/frame-compiler/pr65/research/pair-assembly/PROOF.md", + "references/frame-compiler/pr65/research/pair-assembly/SOURCE.json", + "references/frame-compiler/pr65/research/pair-assembly/frame/frame-compiler.json", + "references/frame-compiler/pr65/research/pair-assembly/frame/frame_verify.py", + "references/frame-compiler/pr65/research/pair-assembly/pair_graph.py", + "references/frame-compiler/pr65/research/reordered-rank-pair/README.md", + "references/frame-compiler/pr65/research/reordered-rank-pair/arithmetic/README.md", + "references/frame-compiler/pr65/research/reordered-rank-pair/arithmetic/audit-receipt.json", + "references/frame-compiler/pr65/research/reordered-rank-pair/arithmetic/audit.py", + "references/frame-compiler/pr65/research/reordered-rank-pair/arithmetic/certificate.json", + "references/frame-compiler/pr65/research/reordered-rank-pair/arithmetic/refine.py", + "references/frame-compiler/pr65/research/reordered-rank-pair/arithmetic/test_arithmetic.py", + "references/frame-compiler/pr65/research/reordered-rank-pair/current-comparison.json", + "references/frame-compiler/pr65/research/reordered-rank-pair/frame-compiler.json", + "references/frame-compiler/pr65/research/reordered-rank-pair/frame-profiles-23.json", + "references/frame-compiler/pr65/research/reordered-rank-pair/frame-profiles-25.json", + "references/frame-compiler/pr65/research/reordered-rank-pair/frame-transitions-23.json", + "references/frame-compiler/pr65/research/reordered-rank-pair/frame-transitions-25.json", + "references/frame-compiler/pr65/research/reordered-rank-pair/frame-word-23.json.gz", + "references/frame-compiler/pr65/research/reordered-rank-pair/frame-word-25.json.gz", + "references/frame-compiler/pr65/research/reordered-rank-pair/paired-candidate.json", + "references/frame-compiler/pr65/research/reordered-rank-pair/test_negative.py", + "references/frame-compiler/pr65/research/reordered-rank-pair/verify.py", + "references/frame-compiler/pr65/scripts/exclusion_circuit.py", + "references/frame-compiler/pr65/scripts/experiments/binary_frame_math.py", + "references/frame-compiler/pr65/scripts/experiments/binary_frame_profile_prepare.py", + "references/frame-compiler/pr65/scripts/experiments/binary_frame_profiles.cpp", + "references/frame-compiler/pr65/scripts/experiments/binary_frame_replay.py", + "references/frame-compiler/pr65/scripts/experiments/rank_pair_compiler.py", + "references/frame-compiler/pr65/scripts/partial_swap/paired.py", + "references/frame-compiler/pr65/scripts/partial_swap/shared.py", + "references/frame-compiler/pr67/LICENSE", + "references/frame-compiler/pr67/NOTICE", + "references/frame-compiler/pr67/SOURCE.json", + "references/frame-compiler/pr67/research/slot-cost-rank-pair/README.md", + "references/frame-compiler/pr67/research/slot-cost-rank-pair/arithmetic/certificate.json", + "references/frame-compiler/pr67/research/slot-cost-rank-pair/compiler.py", + "references/frame-compiler/pr67/research/slot-cost-rank-pair/frame-compiler.json", + "references/frame-compiler/pr67/research/slot-cost-rank-pair/paired-candidate.json", + "references/frame-compiler/pr67/research/slot-cost-rank-pair/profile_oracle.cpp", + "references/frame-compiler/pr67/research/slot-cost-rank-pair/verify.py", + "references/frame-compiler/pr68/LICENSE", + "references/frame-compiler/pr68/NOTICE", + "references/frame-compiler/pr68/SOURCE.json", + "references/frame-compiler/pr68/research/global-anchor-screen/PROOF.md", + "references/frame-compiler/pr68/research/global-anchor-screen/SOURCE.json", + "references/frame-compiler/pr68/research/global-anchor-screen/compiler-frozen.py", + "references/frame-compiler/pr68/research/global-anchor-screen/selected-manifest.json", + "references/frame-compiler/pr68/research/global-anchor-screen/selected_compile.py", + "research/joint-dual/SOURCE.json", + "research/round6-pr71/.gitignore", + "research/round6-pr71/PARAMETER-PROOF.md", + "research/round6-pr71/parameter-certificate.json", + "research/round6-pr71/parameter-source-lock.json", + "research/round6-pr71/refine_parameters.py", + "research/split-pair/PROOF.md", + "research/split-pair/README.md", + "research/split-pair/SOURCE.json", + "research/split-pair/config-23.json", + "research/split-pair/config-25.json", + "research/split-pair/engine-changes.patch", + "research/split-pair/engine-provenance.json", + "research/split-pair/parameters.json", + "scripts/experiments/pin_split_pair_sources.py", + "scripts/experiments/split_pair_arithmetic.py", + "scripts/experiments/split_pair_compiler.py", + "scripts/experiments/split_pair_compose.py", + "scripts/experiments/split_pair_engine.py", + "scripts/experiments/split_pair_graph.py", + "scripts/experiments/verify_split_pair.py", + "tests/test_split_pair.py", + "tests/test_split_pair_pending.py" + ], + "github_files_page_truncated": true, + "comments": 0, + "reviews": 0, + "review_threads": 0 + } + ], + "typed_edges": [ + { + "source": 71, + "target": 73, + "kind": "git_ancestry", + "detail": "PR71 exact head is an ancestor of PR73; confirmed git merge-base --is-ancestor." + }, + { + "source": 59, + "target": 71, + "kind": "mathematical_or_implementation_dependency", + "detail": "split operation; configuration and graph are newly selected" + }, + { + "source": 62, + "target": 71, + "kind": "mathematical_or_implementation_dependency", + "detail": "interval/pair producer" + }, + { + "source": 65, + "target": 71, + "kind": "mathematical_or_implementation_dependency", + "detail": "region orders" + }, + { + "source": 67, + "target": 71, + "kind": "mathematical_or_implementation_dependency", + "detail": "profile-cost retired selection" + }, + { + "source": 68, + "target": 71, + "kind": "mathematical_or_implementation_dependency", + "detail": "pending passive live controls;71 uses known next-use scoring" + }, + { + "source": 71, + "target": 73, + "kind": "mathematical_or_implementation_dependency", + "detail": "same finite physical construction and characteristic, parameter backoff only" + }, + { + "source": 62, + "target": 69, + "kind": "mathematical_or_implementation_dependency", + "detail": "coarse graph source" + }, + { + "source": 57, + "target": 69, + "kind": "mathematical_or_implementation_dependency", + "detail": "joint frame compiler" + }, + { + "source": 60, + "target": 69, + "kind": "mathematical_or_implementation_dependency", + "detail": "rank-first priority" + }, + { + "source": 62, + "target": 70, + "kind": "mathematical_or_implementation_dependency", + "detail": "explicit frozen dependency; no later sources consumed" + }, + { + "source": 49, + "target": 72, + "kind": "mathematical_or_implementation_dependency", + "detail": "old graph/orders and matching family" + }, + { + "source": 69, + "target": 71, + "kind": "potential_compatibility_unverified", + "detail": "Column-pair coarse sums operate inside grouping and appear syntactically compatible with split groups. Counts, frames, matching, dirty words and actual profiles would all require regeneration." + }, + { + "source": 70, + "target": 71, + "kind": "potential_compatibility_unverified", + "detail": "Bounded weighted carry exchanges could be tried in the newer graph/compiler; global interactions forbid adding claimed gains." + } + ], + "strongest_reported_pr": 73, + "strongest_reported_kappa": "25707323052097/500000000000000000", + "scope": "One bounded repository refresh. Changed contributions inspected to stated depth; no claim of fresh exhaustive review or builds for every older PR. Git path inventories complete even where GraphQL file page truncated; no second landscape refresh performed.", + "strongest_freshly_verified_finite_pr": 73 +} diff --git a/research/machine-transfer-verification/full-transfer/audit/independent_pr71_73.py b/research/machine-transfer-verification/full-transfer/audit/independent_pr71_73.py new file mode 100644 index 0000000000..c41110a56c --- /dev/null +++ b/research/machine-transfer-verification/full-transfer/audit/independent_pr71_73.py @@ -0,0 +1,90 @@ +"""Independent selected PR71/73 binary-word and rational-witness audit. + +Run from the session workspace: +python3 outputs/full-transfer/audit/independent_pr71_73.py --repo CHECKOUT --output RECEIPT +The checkout must be pinned to PR73 253ecc88faeed55a950c76026d1fe67a7f690123. +No contributor semantic or arithmetic routine is imported. The shared independent +auditors are retained outputs from this research session and their hashes bind them. +""" +import argparse +from fractions import Fraction as Q +import gzip +from hashlib import sha256 +import importlib.util +import json +from pathlib import Path +import subprocess +import sys + +HERE = Path(__file__).resolve().parent +OUTPUTS = HERE.parents[1] +sys.path.insert(0, str(OUTPUTS)) +import independent_moment as im +import independent_assembly as ia + +def main(): + ap = argparse.ArgumentParser() + ap.add_argument('--repo', type=Path, required=True) + ap.add_argument('--output', type=Path, required=True) + args = ap.parse_args() + repo = args.repo.resolve() + pin = subprocess.check_output(['git','rev-parse','HEAD'],cwd=repo,text=True).strip() + assert pin == '253ecc88faeed55a950c76026d1fe67a7f690123' + helper = OUTPUTS/'audit/scatter_binding_audit.py' + spec = importlib.util.spec_from_file_location('strict_scatter',helper) + strict = importlib.util.module_from_spec(spec); spec.loader.exec_module(strict) + record = json.loads((repo/'certificates/split-pair-compiler.json').read_text()) + result = dict(source_pin=pin, payload='F2', axes=[], arithmetic=[], + independent_sources={str(p.relative_to(OUTPUTS)):sha256(p.read_bytes()).hexdigest() + for p in (Path(__file__), helper, Path(im.__file__), Path(ia.__file__))}, + scope='Exact scalar words and supplied finite profiles; full physical transfer remains separate.') + for h in (23,25): + path = repo/f'certificates/split-pair-word-{h}.json.gz' + raw = gzip.decompress(path.read_bytes()); w = json.loads(raw) + assert sha256(raw).hexdigest() == record['axes'][str(h)]['word_sha256'] + scatter = strict.verify_scatter(w) + v,R = w['v'],w['R'] + initial = [1 << i for i in range(2*v+R)] + M = [(2*v+a,2*v+b) for a,b,_ in w['ops']] + J = [tuple(x) for x in w['scatter']] + V = [(2*v+s,int(i)) for i,s in w['sources'].items()] + word = M+J+M[::-1]+V+M+J+M[::-1]+V + for dual in (False,True): + state = initial.copy() + for t,s in reversed(word) if dual else word: + if dual: t,s = s,t + assert t != s and 0 <= t < len(state) and 0 <= s < len(state) + state[t] ^= state[s] + expected = initial.copy() + for i in range(v): expected[i if dual else v+i] ^= initial[v+i if dual else i] + assert state == expected + files = [path, repo/f'certificates/split-pair-profiles-{h}.json', + repo/f'certificates/split-pair-transitions-{h}.json'] + result['axes'].append(dict(h=h,R=R,basis_size=len(initial),complete_both_orientations=True, + raw_word_sha256=sha256(raw).hexdigest(),literal_scatter=scatter, + inputs={str(p.relative_to(repo)):sha256(p.read_bytes()).hexdigest() for p in files})) + print(f'PASS h={h}: independent literal F2 basis, arbitrary dirty columns and scatter binding',flush=True) + names = ['certificates/split-pair-kappa.json','research/round6-pr71/parameter-certificate.json'] + certs = [json.loads((repo/name).read_text()) for name in names] + # PR71 embeds two arithmetic enclosures inside `bit`; PR73 moves these + # to top-level fields. Compare every remaining physical/profile field. + physical71 = {k:v for k,v in certs[0]['bit'].items() if k not in ('moment','excluded_moment')} + assert physical71 == certs[1]['bit'] + assert certs[0]['finite_bridge'] == certs[1]['finite_bridge'] + for name,c in zip(names,certs): + mr = im.run(repo/name,search=False);mr['source']=name + h = Q(1,10**12) if name == names[0] else Q(1,10**18) + ar = ia.assemble(c,Q(c['bit_saving']),Q(c['kappa']),h) + original = c['assembly'] if name == names[0] else c['preferred']['assembly'] + assert ar['constraints'] == {n:Q(v) for n,v in original['constraints'].items()} + assert ar['margins'] == {n:Q(v) for n,v in original['margins'].items()} + nextlo,nexthi = im.moment(c['bit']['m'],c['bit']['W'], + {int(t):n for t,n in c['bit']['child_multiplicities'].items()},Q(c['bit_saving'])+Q(1,10**18)) + assert nextlo > 1 + result['arithmetic'].append(dict(moment=mr,assembly=ar,next_saving_moment=[nextlo,nexthi])) + print(f'PASS {name}: independent characteristic and 47 inequalities/seven margins',flush=True) + result['same_profile_and_finite_bridge']=True + result['parameter_only_kappa_gain']=Q(certs[1]['kappa'])-Q(certs[0]['kappa']) + args.output.write_text(json.dumps(im.encode(result),indent=2)+'\n') + +if __name__ == '__main__': main() diff --git a/research/machine-transfer-verification/full-transfer/audit/independent_profile_assembly.py b/research/machine-transfer-verification/full-transfer/audit/independent_profile_assembly.py new file mode 100644 index 0000000000..d4a2ada153 --- /dev/null +++ b/research/machine-transfer-verification/full-transfer/audit/independent_profile_assembly.py @@ -0,0 +1,37 @@ +"""Rebuild complete PR71/73 child multiplicities from the two paid axis profiles. + +No contributor module is imported. This does not repeat CRT computation: it +binds the exact freshly reprofiled inputs and independently assembles them. +""" +import argparse +from collections import Counter +from hashlib import sha256 +import json +from math import comb +from pathlib import Path + +ap=argparse.ArgumentParser();ap.add_argument('--repo',type=Path,required=True);ap.add_argument('--output',type=Path,required=True);args=ap.parse_args() +r=args.repo; m=575;N=comb(23,3)*comb(25,3) +c=json.loads((r/'research/round6-pr71/parameter-certificate.json').read_text());bit=c['bit'] +profiles=[json.loads((r/f'certificates/split-pair-profiles-{h}.json').read_text()) for h in (23,25)] +record=json.loads((r/'certificates/split-pair-compiler.json').read_text()) +W=2*N;L=0;parts={'data':Counter({1:18*N,21:2*N,17:2*N,481:2*N}),'paid_endpoint_copy':Counter({1:N})};hashes={} +for h,p in zip((23,25),profiles): + assert p['h']==h and p['v']==comb(h,3) and p['loss']==h*(h-1) + assert p['R']==record['axes'][str(h)]['compiled']['roles']==record['axes'][str(h)]['replay']['roles'] + assert p['crt_disagreements']==0 and p['field_prime']==2**61-1 + assert sum(t*n for t,n in enumerate(p['blocks']))==h*p['R']+p['loss']==p['rank_sum'] + assert p['blocks'][0]==p['blocks'][h]==0 + rep=N//p['v'];assert rep*p['v']==N + bank=rep*p['R'];W+=bank;L+=rep*p['loss'] + parts[f'internal_{h}']=Counter({t:rep*n for t,n in enumerate(p['blocks']) if n}) + parts[f'exterior_{h}']=Counter({h:bank,m-2*h:bank}) + parts[f'data_growth_{h}']=Counter({1:2*N,h-2:2*N}) + path=r/f'certificates/split-pair-profiles-{h}.json';hashes[str(path.relative_to(r))]=sha256(path.read_bytes()).hexdigest() +rows=sum(parts.values(),Counter());mass=sum(t*n for t,n in rows.items()) +assert rows=={int(t):n for t,n in bit['child_multiplicities'].items()} +assert {k:dict(v) for k,v in parts.items()}=={k:{int(t):n for t,n in v.items()} for k,v in bit['parts'].items()} +assert (m,N,W,L,mass,max(rows),m*W-mass)==(bit['m'],bit['N'],bit['W'],bit['L'],bit['total_rank'],bit['maxchild'],bit['deficit']) +assert mass==m*W-N+L and m*W-mass==1846900 and max(rows)==529 +args.output.write_text(json.dumps(dict(status='PASS independent complete paid-profile assembly',m=m,N=N,W=W,L=L,rank_mass=mass,deficit=m*W-mass,parts=parts,child_multiplicities=dict(sorted(rows.items())),profile_input_sha256=hashes,source_sha256=sha256(Path(__file__).read_bytes()).hexdigest(),scope='Exact reconstruction from freshly checked axis profiles plus inherited fixed data/exterior recipe; ambient physical realization remains separate'),indent=2)+'\n') +print('PASS independent complete paid-profile assembly:',len(rows),'rows, W',W,'rank mass',mass) diff --git a/research/machine-transfer-verification/full-transfer/audit/normalized-dominance-control.json b/research/machine-transfer-verification/full-transfer/audit/normalized-dominance-control.json new file mode 100644 index 0000000000..8a1c0caab1 --- /dev/null +++ b/research/machine-transfer-verification/full-transfer/audit/normalized-dominance-control.json @@ -0,0 +1,181 @@ +{ + "status": "PASS: exact counterexample to universal power dominance", + "new_candidate_sha256": "f391f7cee5377ab148f3cecc223fd8111c3075578b1ee327610e4dd3e3468fb0", + "old_candidate_sha256": "06a0f2927f419c1ea108cd9b6f1e64d3174de8ba440a71c2e433c0bfee5a4b98", + "normalization": "d_t = n_new(t)*W_old - n_old(t)*W_new; denominators are positive.", + "positive_capped_sums": 528, + "total_caps": 529, + "rank_mass_difference_numerator": -3834424812900, + "witness_power": "1/2", + "equivalent_saving": "1/2", + "sqrt_weighted_difference_interval": [ + "3788563292986218058467890480077/7004110170662000000000000000000", + "18942816464931090324859772217743/35020550853310000000000000000000" + ], + "relation_to_characteristic": "This positive interval bounds sqrt(575)*(Psi_new(1/2)-Psi_old(1/2)). Thus the normalized new characteristic is strictly larger at power1/2.", + "rows": [ + { + "width": 1, + "signed_count_cross_product": 12357504972645973, + "sqrt_lower": "1", + "sqrt_upper": "1000000000000000001/1000000000000000000" + }, + { + "width": 2, + "signed_count_cross_product": 2264783943893354, + "sqrt_lower": "176776695296636881/125000000000000000", + "sqrt_upper": "1414213562373095049/1000000000000000000" + }, + { + "width": 3, + "signed_count_cross_product": -991880469183938, + "sqrt_lower": "1732050807568877293/1000000000000000000", + "sqrt_upper": "866025403784438647/500000000000000000" + }, + { + "width": 4, + "signed_count_cross_product": 181674412218917, + "sqrt_lower": "2", + "sqrt_upper": "2000000000000000001/1000000000000000000" + }, + { + "width": 5, + "signed_count_cross_product": -18565658933291, + "sqrt_lower": "17469281074217107/7812500000000000", + "sqrt_upper": "2236067977499789697/1000000000000000000" + }, + { + "width": 6, + "signed_count_cross_product": -104560578342803, + "sqrt_lower": "1224744871391589049/500000000000000000", + "sqrt_upper": "2449489742783178099/1000000000000000000" + }, + { + "width": 7, + "signed_count_cross_product": -294386859594805, + "sqrt_lower": "264575131106459059/100000000000000000", + "sqrt_upper": "2645751311064590591/1000000000000000000" + }, + { + "width": 8, + "signed_count_cross_product": -50401665355271, + "sqrt_lower": "2828427124746190097/1000000000000000000", + "sqrt_upper": "1414213562373095049/500000000000000000" + }, + { + "width": 9, + "signed_count_cross_product": -69480011467423, + "sqrt_lower": "3", + "sqrt_upper": "3000000000000000001/1000000000000000000" + }, + { + "width": 10, + "signed_count_cross_product": -44212902835670, + "sqrt_lower": "3162277660168379331/1000000000000000000", + "sqrt_upper": "790569415042094833/250000000000000000" + }, + { + "width": 11, + "signed_count_cross_product": -190462623728188, + "sqrt_lower": "3316624790355399849/1000000000000000000", + "sqrt_upper": "66332495807107997/20000000000000000" + }, + { + "width": 12, + "signed_count_cross_product": -87715094205196, + "sqrt_lower": "3464101615137754587/1000000000000000000", + "sqrt_upper": "866025403784438647/250000000000000000" + }, + { + "width": 13, + "signed_count_cross_product": -107772050256707, + "sqrt_lower": "3605551275463989293/1000000000000000000", + "sqrt_upper": "1802775637731994647/500000000000000000" + }, + { + "width": 14, + "signed_count_cross_product": -88230610731564, + "sqrt_lower": "748331477354788277/200000000000000000", + "sqrt_upper": "1870828693386970693/500000000000000000" + }, + { + "width": 15, + "signed_count_cross_product": -91747151703607, + "sqrt_lower": "774596669241483377/200000000000000000", + "sqrt_upper": "1936491673103708443/500000000000000000" + }, + { + "width": 16, + "signed_count_cross_product": -67904921267623, + "sqrt_lower": "4", + "sqrt_upper": "4000000000000000001/1000000000000000000" + }, + { + "width": 17, + "signed_count_cross_product": -20152208315750, + "sqrt_lower": "4123105625617660549/1000000000000000000", + "sqrt_upper": "82462112512353211/20000000000000000" + }, + { + "width": 18, + "signed_count_cross_product": -46920443308394, + "sqrt_lower": "2121320343559642573/500000000000000000", + "sqrt_upper": "4242640687119285147/1000000000000000000" + }, + { + "width": 19, + "signed_count_cross_product": -2781325835497, + "sqrt_lower": "272431183971292097/62500000000000000", + "sqrt_upper": "4358898943540673553/1000000000000000000" + }, + { + "width": 20, + "signed_count_cross_product": -29595973758273, + "sqrt_lower": "17469281074217107/3906250000000000", + "sqrt_upper": "4472135954999579393/1000000000000000000" + }, + { + "width": 21, + "signed_count_cross_product": 37094454429638, + "sqrt_lower": "2291287847477920003/500000000000000000", + "sqrt_upper": "4582575694955840007/1000000000000000000" + }, + { + "width": 22, + "signed_count_cross_product": -13157045149325, + "sqrt_lower": "2345207879911714777/500000000000000000", + "sqrt_upper": "938083151964685911/200000000000000000" + }, + { + "width": 23, + "signed_count_cross_product": 4264373411375, + "sqrt_lower": "4795831523312719541/1000000000000000000", + "sqrt_upper": "2397915761656359771/500000000000000000" + }, + { + "width": 25, + "signed_count_cross_product": -4172452268600, + "sqrt_lower": "5", + "sqrt_upper": "5000000000000000001/1000000000000000000" + }, + { + "width": 481, + "signed_count_cross_product": 16913490270600, + "sqrt_lower": "1370732012466331801/62500000000000000", + "sqrt_upper": "21931712199461308817/1000000000000000000" + }, + { + "width": 525, + "signed_count_cross_product": -4172452268600, + "sqrt_lower": "716027452336850001/31250000000000000", + "sqrt_upper": "22912878474779200033/1000000000000000000" + }, + { + "width": 529, + "signed_count_cross_product": -12741038002000, + "sqrt_lower": "23", + "sqrt_upper": "23000000000000000001/1000000000000000000" + } + ], + "scope": "This refutes all-power dominance, not the newer certified saving near power1. Both original certificates and their small-saving inequalities remain valid." +} diff --git a/research/machine-transfer-verification/full-transfer/audit/physical-recurrence-review.txt b/research/machine-transfer-verification/full-transfer/audit/physical-recurrence-review.txt new file mode 100644 index 0000000000..9a4bc17620 --- /dev/null +++ b/research/machine-transfer-verification/full-transfer/audit/physical-recurrence-review.txt @@ -0,0 +1,131 @@ +Adversarial review of the floor recurrence and physical volume contract +===================================================================== + +Scope: source inspection of PR73 253ecc88faeed55a950c76026d1fe67a7f690123, +which contains the PR71 physical construction unchanged. This review does not +instantiate a complete finite-state tape machine. No counterexample to the +written floor/remainder/spectator construction was found. + +1. Exact child width and volume + +notes/batched-bit-rows.tex and notes/batched-algorithms.tex use the actual child +width t*floor(e/m), not floor(t*e/m). These differ in general; the FloorDepth / +FloorRecurrence / PhysicalCostTransfer sources use the former, correct quantity. +For e>=m and 1<=t