Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
229 changes: 229 additions & 0 deletions research/rank7-restore-carrier-skips/CLAIM.json
Original file line number Diff line number Diff line change
@@ -0,0 +1,229 @@
{
"admitted_package_manifest_sha256": "2c367a7afa966a7952303364fbccd6332730e2d3ad48d2ef04a524f35daddb03",
"baseline_head": "e2ca469b08385d3d5e29a918d66dbefaf889e9f3",
"baseline_kappa": "17240352247481048785499999999999999999999998999999999999999999999999/10000000000000000000000000000000000000000000000000000000000000000000000",
"baseline_pr": 2969,
"baseline_status": "FINITE_NATIVE_OWNER_AND_MOMENT_CANDIDATE_OUTER_PENDING",
"calls": 666,
"complex_lower": "432434041596978996703/250000000000000000000000",
"declared_edits": {
"count": 2,
"edits_sha256": "ebffcc1e57e59439b9678ff8d9be518c457af22ce77235c2fdb46540ab9b9b79",
"previous_kappa": "0.0017290339826465135177169999999999999999999998999999999999999999999999",
"previous_pr": 2979
},
"fill_sha256": "c2136be9434cda511a1a8a44d98f9f72ea5376830a8426674253b4ee351c4c39",
"fixed_inventory_cap": {
"cap_lower": "4324344875160696378107/2500000000000000000000000",
"cap_upper": "17297379500642785512429/10000000000000000000000000",
"realized": "below the fractional optimum by the recorded gap (check_cap.py); the cap basis is fractional at T74"
},
"gain": "2850470819905554131/500000000000000000000000",
"helpers": 408,
"independent_inputs": 632,
"kappa": "17297361663879159868119999999999999999999998999999999999999999999999/10000000000000000000000000000000000000000000000000000000000000000000000",
"kappa_decimal": "0.0017297361663879159868119999999999999999999998999999999999999999999999",
"live_families": 66304,
"local_profile": {
"1": 2433,
"2": 712,
"3": 232,
"4": 108,
"5": 18,
"8": 8
},
"native_receipt_sha256": "7e982591b1362efe5e8d03fd98f67ff4ef676dd8a5fa3ca765c8ef1370be7019",
"physical_families": 66813,
"previous_claims": {
"pr2942": {
"claim_file": "comparators/PR2942-CLAIM.json",
"gain": "108122601948463419/15625000000000000000000",
"head": "a027b0f6fdb0ab2b42ba10fc31b53960166bf2bf",
"kappa": "17228163198632143279959999999999999999999998999999999999999999999999/10000000000000000000000000000000000000000000000000000000000000000000000",
"pr": 2942
},
"pr2957": {
"claim_file": "comparators/PR2957-CLAIM.json",
"gain": "6018751317177815841/1000000000000000000000000",
"head": "b74b25f3ccc84c16e1a801d73b2f47e5ea764c78",
"kappa": "17237174150707381709709999999999999999999998999999999999999999999999/10000000000000000000000000000000000000000000000000000000000000000000000",
"pr": 2957
},
"pr2966": {
"claim_file": "comparators/PR2966-CLAIM.json",
"gain": "28509469322319047/5000000000000000000000",
"head": "e62d3eb9005117d82a9babcfa937ecc53237c490",
"kappa": "17240342725234521774119999999999999999999998999999999999999999999999/10000000000000000000000000000000000000000000000000000000000000000000000",
"pr": 2966
},
"pr2969": {
"claim_file": "allocation/baseline/CLAIM.json",
"gain": "2850470819905554131/500000000000000000000000",
"head": "e2ca469b08385d3d5e29a918d66dbefaf889e9f3",
"kappa": "17240352247481048785499999999999999999999998999999999999999999999999/10000000000000000000000000000000000000000000000000000000000000000000000",
"pr": 2969
},
"pr2979": {
"claim_file": "comparators/PR2979-CLAIM.json",
"gain": "140436748280493819/200000000000000000000000",
"head": "be191346391661f4d35fc0d1508d0a6029572576",
"kappa": "17290339826465135177169999999999999999999998999999999999999999999999/10000000000000000000000000000000000000000000000000000000000000000000000",
"pr": 2979
}
},
"profile": {
"1": 1637688,
"2": 474192,
"3": 159468,
"4": 71928,
"48": 28190,
"5": 13716,
"8": 5328
},
"release_receipt_sha256": "906d15db82f7b5b8938d1b760f54d9229dc7b6f2dbe84cc9286f2d1015e36743",
"replicas": 74,
"scope": "Conditional finite supplier/outer certificate for PR2979's words (mdumitrean: joint rank-7 end frames, five further paired extractions, fourteen PR2957 rewrites) with one declared literal restore edit (R1, Stack2979 / Jeremy Kothe) and PR2979's literal T74 allocation unchanged (paid profile re-derived). Inherited all-size/compiler/theorem hypotheses remain. No selected-frontier change or independent-human-review claim.",
"source_manifest_sha256": "130650ad8833f6df88528c560e4d1cfbae084f4b15a64788a332ddcaff472a17",
"stages": {
"stage1": {
"frame_edits": 139,
"groups": {
"A": {
"W": [
256,
128,
64,
38,
20,
10,
1
],
"helpers": [
331,
450,
451,
508,
509
]
},
"B": {
"W": [
256,
128,
64,
34,
17,
11,
4
],
"helpers": [
299,
448,
449,
484,
485
]
},
"C": {
"W": [
256,
128,
64,
32,
19,
11,
6
],
"helpers": [
452,
453,
532,
533
]
},
"D": {
"W": [
256,
128,
64,
37,
21,
8,
3
],
"helpers": [
454,
455,
556,
557
]
},
"V45": {
"W": [
256,
128,
64,
35,
16,
11,
5
],
"helpers": [
249,
251,
265,
267
]
}
},
"kind": "joint codimension-2 end-frame lowering (frame-only)",
"record_sha256": "5fbfce004330ebc1fbac8de264614fe295f1a074811b478db4892c3bc3852cd3"
},
"stage2": {
"extractions": [
{
"helper": 226,
"normal": 42,
"step": 1
},
{
"helper": 228,
"normal": 42,
"step": 2
},
{
"helper": 230,
"normal": 42,
"step": 3
},
{
"helper": 363,
"normal": 7,
"step": 4
},
{
"helper": 395,
"normal": 7,
"step": 5
}
],
"kind": "rank-8 paired input/output extractions"
},
"stage3": {
"applier_sha256": "2509f1335e47543f8814b42d6bf83032b30c5899b4f7cc62a6adc03f5138ae13",
"count": 14,
"kind": "declared exactness-preserving gate rewrites (Jeremy Kothe, PR2957), re-addressed",
"rewrites_sha256": "a37ade675876e4f5b00b33066c84f495fccd264863b7eb5d813837b1d01c3e7d"
}
},
"status": "CONDITIONAL_CANDIDATE_COMPLETE_FINITE_RELEASE",
"width_inventory": {
"4": 26,
"5": 2,
"6": 16,
"7": 52,
"8": 99,
"9": 213
},
"zero_buffers": 91
}
45 changes: 45 additions & 0 deletions research/rank7-v45-profile-audit/README.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,45 @@
# Independent V45 frame and invoice audit for PR #2979

**Result: partial positive audit of one local group, the profile-bearing word stages, and the literal T74 owner allocation, plus an exact negative screen of the audited profile at κ=0.1. It does not independently validate the full supplier or select a new κ.**

The selected conditional result remains κ = 0.001672660197076918. [PR #2979](https://github.com/CrocSwap/integer-mult-bounds/pull/2979) claims κ ≈ 0.0017290339826465135, about `0.0000563737855695955` above the selected value. It merged into `main` on 2026-10-16, but the selected record still names #1094; this audit does not admit the candidate or change the frontier. It independently reconstructs the V45 rank-7 frame group from the pinned parent words using explicit XOR-span closure, then rebuilds the profile-bearing word sections through the five extraction transforms and fourteen literal rewrites for both providers. It also independently checks the T74 owner allocation, in addition to the published aggregate arithmetic. It does not replay the full admission chain.

For V45, all 61 edited gate frames are hyperplanes of their old frames, each lies in the shared rank-7 subspace, and every gate touching a lowered helper stays in that subspace. Both parent providers give the same result. The coordinated four-helper lowering changes the exact weighted local profile price by −8,388,172 units and leaves +22,972 after paying for four freed width units. The single-helper control loses: its price delta is −2,038,159 and its margin is −53,141. The five-group positive control independently reproduces all 139 stage-1 edits, the declared stage-1 local profile and the changed width inventory.

The source replay reproduces the stage-2 profile `{1:2449, 2:710, 3:236, 4:102, 5:18, 8:8}` and the final profile `{1:2445, 2:706, 3:232, 4:108, 5:18, 8:8}`, with the claimed width inventory, for both providers. Its exact weighted stage deltas are −46,150,994, −10,523,403, and −52,350 units, summing to −56,726,747. A missing stage-2 frame change, stale rewrite preimage, and unshifted phase warp are rejected by negative controls.

The independent T74 owner replay reconstructs all 1,332 replica/child windows from the pinned nine-stage template and the literal `ORDER.json`, then checks every one of the 271,728 `FILL.json.gz` roles against its source window, provider width, family capacity, and bin coordinates. It verifies that repeated rank-level windows sharing one `(replica, pair, side, port)` family are time-disjoint; all 408 helper identities occur exactly once per call; and both dispatched providers reproduce the same 408-width inventory and paid profile. The resulting idle profile is `{1:17310, 3:4956, 5:1728, 48:28190}` and the full profile closes the exact rank-mass identity at 4,816,512. The physical count reconciles as `896×74 + 408 helpers + 8 centres + 91 private cleanup buffers + 2 inherited coefficient guards = 66,813`. These are source-bound finite allocation and stock-count checks, not a recertification of the global native/outer admission.

A separate 90-digit Decimal evaluation places the full-profile root at approximately `0.00172903398264651351771759`, consistent with the conservative value in the claim and above the selected κ. This is a numerical cross-check, not a new exact root certificate.

The independently reconstructed #2979 local profile and the newer six-skip profile from [PR #3042](https://github.com/CrocSwap/integer-mult-bounds/pull/3042) both fail the requested `κ=0.1` target under the inherited `m=73`, `w=896/9` recursive moment. The PR #3042 claim is pinned at its exact head in [SOURCES.json](SOURCES.json); [PR #3054](https://github.com/CrocSwap/integer-mult-bounds/pull/3054) reports composing that same six-skip word with a larger T740 allocation, which changes its idle profile but leaves the local profile unchanged. At `κ=1/10`, the retained transfer requires `a=1/9`, and the local child term is `(r/73)^(8/9)`. Integer ninth-root brackets, checked by exact integer powers, give

```text
(PR #2979) (1/w) Σ n_r (r/73)^(8/9) ≥ 48304277901/44800000000 > 1.
(PR #3042) (1/w) Σ n_r (r/73)^(8/9) ≥ 48295445607/44800000000 > 1.
```

Both left sides count only paid local children. They omit idle children and the centre path, whose costs are nonnegative, so no packing, extra unpaid coverage, or centre deletion can bring either **fixed profile** to `κ≥0.1` under that transfer. A different local profile, coverage law, or outer transfer could escape this scoped result; none is supplied here. The verifier checks the #2979 profile from its pinned words, reads the PR #3042 profile from its exact pinned claim, and checks rank-by-rank rational floors and both aggregate inequalities.

## Reproduce

From the repository root:

```sh
python3.12 scripts/research_package.py --package research/rank7-v45-profile-audit --check-only
python3.12 scripts/research_package.py --package research/rank7-v45-profile-audit
```

The verifier uses only standard-library arithmetic and JSON/gzip inputs pinned in [SOURCES.json](SOURCES.json). Its target screen uses exact integer ninth-root brackets, not floating-point powers.

## Limits

The stage-2/3 replay reconstructs only sections that determine the paid profile; it does not independently prove the extraction or rewrite operator identities, or reconstruct compensation and cleanup semantics. The owner replay checks literal finite rank windows, offsets and the stated stock count, but not the underlying binary frame transitions, global stock/precision/hosting premises, fresh native admission or outer release. The `κ=0.1` screen applies only to the audited local profile and inherited moment/transfer. Consequently, the audit does not certify the complete κ claim or update the selected frontier.

## Open next questions

The exact target screens show that the #2979 profile and its newer six-skip successor both need a substantial local-profile change (or a changed coverage/outer transfer) before their other open obligations could matter to `κ≥0.1`. For #2979, the next validation step remains a code-disjoint symbolic replay of the extraction/rewrite identities, compensation updates and inverse cleanup on all 632 independent inputs; a separate complete-stock/native/outer review is needed for its reported κ. See the structured questions in [TASK.json](TASK.json). Do not start another lowering census until those obligations are closed or explicitly handed off.

## Credit

The audited construction and its predecessor chain remain credited in `research/rank7-joint-endframes/NOTICE` and its README: Dugongue / Marius-Paul Dumitrean for PR #2979, Jeremy Kothe for the PR #2957 rewrites, and all listed predecessor contributors. This small audit does not replace or absorb those contributions. Prepared with substantial AI assistance by OpenAI Codex; Apache-2.0.
Loading