From 0d6bf0ba8a92e9f35a097c47242b1bbe8d66ea20 Mon Sep 17 00:00:00 2001 From: commdata2338 <199849969+commdata2338@users.noreply.github.com> Date: Wed, 14 Oct 2026 17:54:29 -0500 Subject: [PATCH] Research: prove a ten-contact obstruction to the fixed P104 room carrier Resolves the released capture-order handoff in discussion #2131. With the original G captures and query caps retained and frame paths monotone, the added carrier B0 cannot gather X2 + X4 inside R = span(32,196): five sources (X2, X4, X58, X76, X88) each need two contacts with a distinct pair among four helpers (G1, G7, G20, B0), and each source's label lies in exactly its two helpers' caps. A source's earlier contact must be its helper's first required contact, which is injective, and five sources cannot use four first contacts. So no order of the 418 captures exists, not only the two failed greedy prefixes. Two independent exact enumerations find zero legal orders, and deleting any one of the ten contacts admits an order. A scoped negative result; no supplier or kappa change. Adds research/p104-carrier-capture-order/ only. Submitted by @commdata2338 with substantial AI assistance (OpenAI Codex research and implementation; packaged with Claude Code). Co-Authored-By: Claude Opus 5.5 (1M context) Claude-Session: https://claude.ai/code/session_01X86sCSXdoDd61SDFfC1PKG --- .../CERTIFICATE.json | 529 ++++++++++++++++++ research/p104-carrier-capture-order/README.md | 197 +++++++ .../p104-carrier-capture-order/SOURCES.json | 30 + research/p104-carrier-capture-order/TASK.json | 130 +++++ .../p104-carrier-capture-order/VERIFY.json | 33 ++ research/p104-carrier-capture-order/verify.py | 328 +++++++++++ 6 files changed, 1247 insertions(+) create mode 100644 research/p104-carrier-capture-order/CERTIFICATE.json create mode 100644 research/p104-carrier-capture-order/README.md create mode 100644 research/p104-carrier-capture-order/SOURCES.json create mode 100644 research/p104-carrier-capture-order/TASK.json create mode 100644 research/p104-carrier-capture-order/VERIFY.json create mode 100644 research/p104-carrier-capture-order/verify.py diff --git a/research/p104-carrier-capture-order/CERTIFICATE.json b/research/p104-carrier-capture-order/CERTIFICATE.json new file mode 100644 index 0000000000..c340bfd27a --- /dev/null +++ b/research/p104-carrier-capture-order/CERTIFICATE.json @@ -0,0 +1,529 @@ +{ + "contacts": [ + { + "coefficient": "2", + "event_id": 631, + "helper": "G7", + "source": "X58" + }, + { + "coefficient": "-2", + "event_id": 745, + "helper": "G7", + "source": "X4" + }, + { + "coefficient": "-2", + "event_id": 799, + "helper": "G1", + "source": "X88" + }, + { + "coefficient": "2", + "event_id": 807, + "helper": "G20", + "source": "X76" + }, + { + "coefficient": "2", + "event_id": 945, + "helper": "G7", + "source": "X88" + }, + { + "coefficient": "2", + "event_id": 1154, + "helper": "G20", + "source": "X58" + }, + { + "coefficient": "2", + "event_id": 1160, + "helper": "G20", + "source": "X2" + }, + { + "coefficient": "2", + "event_id": 1267, + "helper": "G1", + "source": "X76" + }, + { + "coefficient": "1", + "event_id": "carrier-X2", + "helper": "B0", + "source": "X2" + }, + { + "coefficient": "1", + "event_id": "carrier-X4", + "helper": "B0", + "source": "X4" + } + ], + "first_contact_premises": { + "deficit": 1, + "helpers": 4, + "sources": 5 + }, + "helper_caps": { + "B0": [ + 32, + 196 + ], + "G1": [ + 1, + 2, + 8, + 16, + 32, + 64, + 128, + 256 + ], + "G20": [ + 1, + 2, + 8, + 16, + 36, + 64, + 128, + 260 + ], + "G7": [ + 1, + 2, + 4, + 8, + 16, + 64, + 128, + 256 + ] + }, + "membership": { + "X2": { + "B0": true, + "G1": false, + "G20": true, + "G7": false + }, + "X4": { + "B0": true, + "G1": false, + "G20": false, + "G7": true + }, + "X58": { + "B0": false, + "G1": false, + "G20": true, + "G7": true + }, + "X76": { + "B0": false, + "G1": true, + "G20": true, + "G7": false + }, + "X88": { + "B0": false, + "G1": true, + "G20": false, + "G7": true + } + }, + "original_capture_control": { + "captures": 416, + "final_G_dimensions": { + "G0": 7, + "G1": 7, + "G10": 7, + "G11": 5, + "G12": 8, + "G13": 6, + "G14": 7, + "G15": 6, + "G16": 8, + "G17": 7, + "G18": 6, + "G19": 2, + "G2": 3, + "G20": 8, + "G21": 6, + "G22": 4, + "G23": 8, + "G24": 5, + "G25": 2, + "G26": 7, + "G27": 8, + "G28": 7, + "G29": 5, + "G3": 3, + "G30": 5, + "G31": 3, + "G4": 7, + "G5": 8, + "G6": 7, + "G7": 6, + "G8": 8, + "G9": 5 + }, + "helpers": 32 + }, + "query_bindings": { + "G1": { + "event_id": 1563, + "frame": [ + 1, + 2, + 8, + 16, + 32, + 64, + 128, + 256 + ], + "query": "Q0" + }, + "G20": { + "event_id": 1544, + "frame": [ + 1, + 2, + 8, + 16, + 36, + 64, + 128, + 260 + ], + "query": "Q5" + }, + "G7": { + "event_id": 1557, + "frame": [ + 1, + 2, + 4, + 8, + 16, + 64, + 128, + 256 + ], + "query": "Q1" + } + }, + "rejected_controls": [ + "ten_single_contact_deletions_in_proof_checker", + "G1_cap_enlargement_in_proof_checker", + "B0_cap_enlargement_in_proof_checker", + "wrong_initial_source_label", + "omitted_contact_in_order", + "changed_coefficient_in_certificate", + "changed_count_in_certificate", + "boolean_for_integer_in_certificate", + "duplicate_JSON_key" + ], + "relaxed_cap_controls": [ + { + "example": [ + 631, + 799, + 945, + 1160, + 807, + 1154, + 1267, + "carrier-X4", + 745, + "carrier-X2" + ], + "helper": "G1", + "legal_orders": 135360 + }, + { + "example": [ + 631, + 745, + 799, + 807, + 945, + 1154, + 1160, + 1267, + "carrier-X2", + "carrier-X4" + ], + "helper": "B0", + "legal_orders": 135360 + } + ], + "room": [ + 32, + 196 + ], + "schema_version": 1, + "signature_census": { + "example": [], + "legal_orders": 0, + "rejected_moves": 3612, + "states": 2921 + }, + "single_contact_deletions": [ + { + "omitted": 631, + "signature": { + "example": [ + 745, + 799, + 807, + 945, + 1154, + 1267, + "carrier-X2", + 1160, + "carrier-X4" + ], + "legal_orders": 13760, + "rejected_moves": 1082, + "states": 1308 + }, + "subspace": { + "legal_orders": 13760, + "states": 1562 + } + }, + { + "omitted": 745, + "signature": { + "example": [ + 631, + 799, + 807, + 945, + 1154, + 1267, + "carrier-X2", + 1160, + "carrier-X4" + ], + "legal_orders": 13520, + "rejected_moves": 1116, + "states": 1279 + }, + "subspace": { + "legal_orders": 13520, + "states": 1506 + } + }, + { + "omitted": 799, + "signature": { + "example": [ + 631, + 945, + 1160, + 1154, + 1267, + 807, + "carrier-X4", + 745, + "carrier-X2" + ], + "legal_orders": 14860, + "rejected_moves": 1204, + "states": 1338 + }, + "subspace": { + "legal_orders": 14860, + "states": 1864 + } + }, + { + "omitted": 807, + "signature": { + "example": [ + 631, + 799, + 945, + 1160, + 1154, + 1267, + "carrier-X4", + 745, + "carrier-X2" + ], + "legal_orders": 13520, + "rejected_moves": 1116, + "states": 1279 + }, + "subspace": { + "legal_orders": 13520, + "states": 1506 + } + }, + { + "omitted": 945, + "signature": { + "example": [ + 631, + 1160, + 1154, + 1267, + 799, + 807, + "carrier-X4", + 745, + "carrier-X2" + ], + "legal_orders": 13520, + "rejected_moves": 1116, + "states": 1279 + }, + "subspace": { + "legal_orders": 13520, + "states": 1506 + } + }, + { + "omitted": 1154, + "signature": { + "example": [ + 745, + 631, + 799, + 807, + 945, + 1267, + "carrier-X2", + 1160, + "carrier-X4" + ], + "legal_orders": 13760, + "rejected_moves": 1082, + "states": 1308 + }, + "subspace": { + "legal_orders": 13760, + "states": 1562 + } + }, + { + "omitted": 1160, + "signature": { + "example": [ + 631, + 799, + 807, + 945, + 1154, + 1267, + "carrier-X4", + 745, + "carrier-X2" + ], + "legal_orders": 13520, + "rejected_moves": 1116, + "states": 1279 + }, + "subspace": { + "legal_orders": 13520, + "states": 1506 + } + }, + { + "omitted": 1267, + "signature": { + "example": [ + 631, + 799, + 945, + 1160, + 807, + 1154, + "carrier-X4", + 745, + "carrier-X2" + ], + "legal_orders": 14860, + "rejected_moves": 1204, + "states": 1338 + }, + "subspace": { + "legal_orders": 14860, + "states": 1864 + } + }, + { + "omitted": "carrier-X2", + "signature": { + "example": [ + 631, + 799, + 807, + 945, + 1154, + 1160, + 1267, + "carrier-X4", + 745 + ], + "legal_orders": 14860, + "rejected_moves": 1204, + "states": 1338 + }, + "subspace": { + "legal_orders": 14860, + "states": 1864 + } + }, + { + "omitted": "carrier-X4", + "signature": { + "example": [ + 631, + 745, + 799, + 807, + 945, + 1154, + 1267, + "carrier-X2", + 1160 + ], + "legal_orders": 14860, + "rejected_moves": 1204, + "states": 1338 + }, + "subspace": { + "legal_orders": 14860, + "states": 1864 + } + } + ], + "source_labels": { + "X2": [ + 228 + ], + "X4": [ + 196 + ], + "X58": [ + 333 + ], + "X76": [ + 289 + ], + "X88": [ + 458 + ] + }, + "source_sha256": "0f541bef7f19fdeffd67157684e9f03d785f42c89973632f508fc1a0452b580e", + "subspace_census": { + "legal_orders": 0, + "states": 3948 + } +} diff --git a/research/p104-carrier-capture-order/README.md b/research/p104-carrier-capture-order/README.md new file mode 100644 index 0000000000..2ca6094116 --- /dev/null +++ b/research/p104-carrier-capture-order/README.md @@ -0,0 +1,197 @@ +# P104 fixed-room carrier: a ten-contact ordering obstruction + +**No ordering completes the fixed capture stage proposed in +[Discussion #2131](https://github.com/CrocSwap/integer-mult-bounds/discussions/2131).** +Retaining the original G captures and query caps, with monotone frame paths, +prevents the added carrier from gathering `X2 + X4` before delivery in +`R = span(32,196)`. Eight original captures and the two carrier captures already +force a contradiction. This resolves that discussion's released ordering +handoff, including orderings that start before either failed greedy prefix. + +This is a **scoped proof with an exact finite certificate**, not a complete +side correction, supplier, or new κ. No solver result is trusted by the replay. +The claim is in discussion #2131. Base, sources and task refinement are recorded +in [SOURCES.json](SOURCES.json) and [TASK.json](TASK.json). + +## Contract and source binding + +The scientific input is PR #1972's 4,058-event witness, retained by +[PR #1991's native channel](../p104-native-channel/README.md), at SHA256 +`0f541bef7f19fdeffd67157684e9f03d785f42c89973632f508fc1a0452b580e`. +Event indices below are **zero based** in its `program` array. + +Frames are subspaces of the recorded binary nine-dimensional label space. +A contact requires identical canonical charts on its two registers. Between +contacts a register may move to any containing frame. Every source retains +its initial line; G helpers stay inside their prescribed positive-query cap +until their captures finish. The carrier starts in frame zero and must remain +inside R until both captures finish, because its subsequent delivery is in R. +Frame zero does **not** mean zero logical contents: all helpers may be dirty. + +Original transports may be replaced and contacts freely reordered. No original +capture is removed, split, redirected through another register or replaced by +a different source form. No register is reset or given a descending frame move. +The proof uses only frame containment; scalar coefficients and logical dirt +cannot repair this contradiction. Arbitrary additional monotone work also +cannot erase the frame vectors used below. + +The three inherited caps and the carrier cap are: + +| Helper | Cap basis | Positive query event | +|---|---|---| +| G1 | 1, 2, 8, 16, 32, 64, 128, 256 | 1563, into Q0 | +| G7 | 1, 2, 4, 8, 16, 64, 128, 256 | 1557, into Q1 | +| G20 | 1, 2, 8, 16, 36, 64, 128, 260 | 1544, into Q5 | +| B0 | 32, 196 | delivery room R | + +For a direct hand check, number bits from zero at the least significant bit. +G1's cap is `bit_2 = 0`, G7's is `bit_5 = 0`, and G20's is +`bit_2 XOR bit_5 XOR bit_8 = 0`. B0's cap is the four-element set +`{0,32,196,228}`. + +The following table is the complete finite premise of the obstruction. +Among these four caps, each source label lies **exactly** in its two listed caps. +Every listed pair of helpers is different. + +| Source | Initial label | Two required helpers | Capture event IDs | +|---|---:|---|---| +| X2 | 228 | G20, B0 | 1160, carrier-X2 | +| X4 | 196 | G7, B0 | 745, carrier-X4 | +| X58 | 333 | G7, G20 | 631, 1154 | +| X76 | 289 | G20, G1 | 807, 1267 | +| X88 | 458 | G1, G7 | 799, 945 | + +The original coefficients, query frames and source lines are reconstructed from +the witness, not copied from a discussion summary. The added carrier coefficients +are both +1. Membership is checked by both binary row reduction and explicit +enumeration of each subspace. [CERTIFICATE.json](CERTIFICATE.json) records every +binding, count and control witness. + +## Proof: five sources cannot use four first contacts + +Here is the general lemma used by this instance. Suppose each source s has two +required contacts with distinct helpers, its nonzero initial label belongs to +exactly those two helper caps, and different sources use different unordered +helper pairs. Frames grow monotonically and every required contact uses a +common frame inside its helper's cap. Then the number of sources is at most +the number of helpers. + +For each source s, take its **earlier** required contact, with helper h; write k +for its other helper. This must be h's first contact among the required contacts. +Otherwise h previously contacted some different source t, so its frame contains +t's initial label. At the h–s contact that label enters s's frame. Monotonicity +retains it until the later k–s contact, where it must belong to k's cap. +But t is incident to h and cannot also be incident to k: its helper pair would +then equal s's pair. The cap-membership hypothesis therefore excludes t's label +from k's cap, a contradiction. + +Thus each source requires the first required contact of a helper. A helper has +only one first contact, so this assignment is injective. In the table there are +five sources and four helpers. Therefore the ten contacts cannot all occur. +Any complete 418-capture schedule would contain these ten contacts in some +order and satisfy the same monotonicity and cap conditions, so it is impossible +as well. The argument does not freeze a greedy prefix or any original climb. + +In the helper graph, the sources are five different edges on four vertices: + +```mermaid +graph LR + G7 ---|X58| G20 + G7 ---|X88| G1 + G1 ---|X76| G20 + G7 ---|X4| B0 + B0 ---|X2| G20 +``` + +## Independent finite corroboration and controls + +For a fixed order it suffices to use the smallest possible common frame at +each contact, the sum of the two current subspaces. By induction these frames +are contained in the corresponding frames of every other monotone realization +of that order. A cap violation in the minimal realization therefore excludes +the order; a cap-respecting minimal realization supplies its frame schedule. + +Two separately implemented recursions count every permutation, pruning only +an actual cap violation. One represents every frame by the bits indicating +which caps fail to contain it; these bits combine by OR under subspace sum. +The other carries the actual sets of binary vectors. They agree: + +* Zero legal orders of the ten contacts: 2,921 signature states and 3,948 actual + subspace states. The dynamic-programming recurrence accounts for all 10! + permutations, including extensions of rejected prefixes. +* Removing any one contact admits legal orders. Counts in displayed certificate + order are `13760,13520,14860,13520,13520,13760,13520,14860,14860,14860`. + Each removal includes a complete nine-contact witness, replayed as actual + subspaces. This proves deletion minimality of this ten-contact core, not a + global minimum obstruction size or feasibility of the remaining full program. +* All 416 original captures pass in their original order with minimal-join + paths and without the carrier. This is a capture-stage control, not a cold replay. +* Enlarging G1's cap alone to FULL, or B0's cap alone to FULL, admits 135,360 + orders in each case. These are controls on the necessary cap hypothesis, + not legal repairs of the original contract. Each has an explicit witness. +* The proof checker rejects all ten contact omissions, both relaxed caps and + an incorrect initial label. Order replay rejects a missing contact. Complete + certificate comparison rejects altered coefficients, counts and JSON types; + duplicate JSON keys are rejected. The direct command checks the source hash. + +The small core was discovered with Z3 5.3.0.0. Z3 is not a package dependency, +and neither its `unsat` answer nor its core-minimization procedure is needed +to reproduce or accept the result. The written injection proof and the two +standard-library enumerations are the evidence. They are author-checked; +independent human review and a proof-assistant formalization remain open. + +## Reproduce + +From the repository root, with Python 3.12 and no third-party dependencies: + +```sh +python3 -I -B scripts/research_package.py --package research/p104-carrier-capture-order --check-only +python3 -I -B scripts/research_package.py --package research/p104-carrier-capture-order +``` + +Expected verifier line (local direct replay takes less than a second): + +```text +PASS_P104_CARRIER_CAPTURE_ORDER contacts=10 sources=5 helpers=4 legal_orders=0 deletion_controls=10 original_captures=416 no_new_kappa +``` + +The registered hook runs normal and optimized replay. Direct replay also works +without Git or network in an export containing this package and the pinned +witness at its relative path. To regenerate the certificate without overwriting +committed evidence, use `verify.py --write-certificate NEW_FILE.json`. + +## Limits + +This closes only the fixed `X2,X4` room component with retained G contacts and +query caps. Its proposed Y0/Y6 deliveries, scattering, restoration, native +phases, paid histogram, owners, precision and all-size admission are not +constructed or checked. The obstruction occurs before those obligations. +It establishes no added-rank tariff, favorable completed moment or κ change. +This account's [PR #2172](https://github.com/CrocSwap/integer-mult-bounds/pull/2172) +prices a different frozen-cut network; its 864-rank bound is not reused here. +The retained-transport bounds in #2082/#2090/#2113/#2127 and the refined-interval +bound in #2148 have different hypotheses. + +## Open next questions + +The next useful test is a different carrier rectangle or changed capture/query +contract. First search its incidence table for a subgraph satisfying this lemma; +reject it before scheduling if it has more source edges than helpers. A survivor +still needs a complete chronological dirty-restored word and a favorable full +bill. Alternatively, explicitly price a nonmonotone move or a replacement of a +required contact that breaks this core; an uncharged reset or enlarged query cap +is not an implementation. Structured questions and blockers are in TASK.json. + +## Credit + +Hope7Happiness's Discussion #2131 supplied the fixed room component, the changed +monotone-path contract, the two unsuccessful prefixes and the released ordering +question. This package supplies the obstruction, not that component proposal. +Rohan Arun's PR #1972 supplies the scalar/frame witness; Chafik Boukhalfa's +PR #1991 supplies the native realization and retained witness. Adam Gall's +PR #1940 supplies the schedule; Josie Elliston's PR #1071 and Ali Romman's +PR #1125 supply the fixture/reconstruction, with their retained E8 and compiler +lineage. Source files and source-specific notices remain unchanged. + +Prepared for commdata2338 (@commdata2338), with substantial OpenAI Codex assistance. +Apache-2.0. No independent human review or complete multiplication theorem is claimed. diff --git a/research/p104-carrier-capture-order/SOURCES.json b/research/p104-carrier-capture-order/SOURCES.json new file mode 100644 index 0000000000..ac5595c449 --- /dev/null +++ b/research/p104-carrier-capture-order/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "e8870e5917057d59b730eb14721a778639eca050", + "sha256": "d46eb6d5b3e279428753d770653663fbdf1063e55c255ea073d768f344927ef7" + }, + { + "path": "research/p104-native-channel/PROOF.md", + "usage": "input", + "git_blob": "a69311b74f74a2f8e8f411c1451baacd9bacddce", + "sha256": "5d743145d389ffdfaffc66096fa7e32c7155b18f73d74755403151d0435bb94c" + }, + { + "path": "research/p104-native-channel/inputs/LOWRANK-WITNESS.json", + "usage": "input", + "git_blob": "86beaf424e9f0f800ae3a62797d94ec9386b7706", + "sha256": "0f541bef7f19fdeffd67157684e9f03d785f42c89973632f508fc1a0452b580e" + } + ] +} diff --git a/research/p104-carrier-capture-order/TASK.json b/research/p104-carrier-capture-order/TASK.json new file mode 100644 index 0000000000..1b651a1498 --- /dev/null +++ b/research/p104-carrier-capture-order/TASK.json @@ -0,0 +1,130 @@ +{ + "schema_version": 1, + "task_id": "p104-side-correction", + "priority_revision": 4, + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "original_card": { + "id": "p104-side-correction", + "question": "Can the native P104 low-rank channel be completed with a legal, fully charged I-G/2 side correction?", + "starting_points": [ + "research/p104-native-channel/README.md", + "research/p104-native-channel/PROOF.md", + "docs/research/community-efficient1000-review.md" + ], + "methods": [ + "Construct one side-correction word at an explicit chronological cut with the needed frames still available.", + "Derive a lower bound on the side correction and hosting costs that decides whether this channel can beat the selected budget." + ], + "acceptance_gate": "An exact arbitrary-input identity, source/target frame availability and restoration at the chosen cut, plus the complete channel+correction+idle/hosting bill or an explicit favorable bound. The native channel alone is not a supplier.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read the P104 open next questions and its fixed local histogram; inspect why appending I-G/2 after source completion is not justified. #1991 supplies the checked native channel, not the missing correction.", + "scope": "Source-bound orientation only. Read the named package and review before relying on its local evidence; this command is not its replay or supplier admission." + }, + "first_experiment": "Choose one exact side-correction cut and bound its allowed cost from a favorable completed moment at a declared target. Stop or hand off if the necessary source/target access cannot be justified or even the optimistic total misses the target.", + "bottleneck_link": "Completing an already realized changed channel tests a concrete construction opportunity, instead of refining the incumbent packing. A positive local result still needs global and all-size admission.", + "allowed_variations": [ + "One correction factorization, one chronological cut, or one explicit hosting obstruction.", + "A changed correction schedule with an updated full bill and native frame contract." + ], + "scope_change_triggers": [ + "Recompiling the already certified low-rank channel without closing a new obligation.", + "Treating a pending ancestor, local histogram or unpriced side correction as an admitted global supplier." + ], + "overlap_terms": [ + "P104", + "I-G/2", + "side correction", + "native channel", + "1972", + "1991" + ] + }, + "scope_status": "changed", + "actual_scope": "Prove or refute capture-order feasibility for Discussion2131 fixed room span(32,196), X2/X4 carrier, all original G captures and fixed G query caps, with replacement monotone frame paths.", + "scope_change_reason": "The suggested central card is narrowed to the released concrete scheduling handoff, rather than claiming a complete side correction. A ten-contact obstruction resolves that necessary stage for every order.", + "bottleneck_link": "Avoid another greedy search on this exact P104 correction component: its capture stage is impossible even with all scalar, hosting and precision expenses waived. A useful successor must change a proved premise.", + "budget_minutes": 60, + "stop_rule": "Stop this component once a complete capture prefix or exact all-order obstruction is established; do not synthesize scattering or a full supplier after a necessary-stage obstruction.", + "outcome": "negative-result", + "evidence": "README.md first-contact injection proof; CERTIFICATE.json source-bound ten-contact core; exact cap-signature and explicit-subspace permutation counts; ten deletion witnesses; original 416-capture positive control; relaxed-cap and corruption controls.", + "author": "commdata2338", + "ai_assistance": "Prepared for commdata2338 (@commdata2338), with substantial OpenAI Codex assistance. Author-checked; no independent human review.", + "open_questions": [ + { + "question": "Does a different candidate carrier rectangle escape the first-contact incidence obstruction?", + "why_it_matters": "A surviving capture interface is necessary before constructing a full P104 side correction.", + "first_step": "Bind its source labels, original capture occurrences and query caps; look for distinct two-helper source pairs whose labels belong exactly to their incident caps and with more sources than helpers.", + "blocked_by": "Passing this necessary test does not supply a legal capture order, scatter/restoration schedule, native recipes or complete favorable bill." + }, + { + "question": "Can an explicitly paid changed trajectory or replacement capture break this fixed ten-contact core within a favorable complete budget?", + "why_it_matters": "The proof identifies which monotonicity, fixed-cap and retained-contact premises must change.", + "first_step": "Specify one descending move or one replacement contact and check its arbitrary-input effect and native cost before running a wider synthesis.", + "blocked_by": "No changed query/capture implementation, owner/idle credit or complete moment has been supplied." + } + ], + "selection": { + "nonce": "fc691d86141767f8847a504c7bd1b4fa", + "track": "complex-mechanisms", + "scope_key": "c5367b1a1b7bed20db53", + "refined_scope_key": "P104/single-room-32-196/X2-X4/capture-order/all416-fixed-caps", + "choice": "Second suggestion; take the released Discussion2131 capture-order handoff.", + "passed_over": { + "complex-new-helper-inventory": "No comparably concrete new contract.", + "complex-rank-shape-decoder": "Prefer the specific central handoff; prior P112 and fixed-word scopes are covered." + } + }, + "discussion": "https://github.com/CrocSwap/integer-mult-bounds/discussions/2131", + "predecessors": [ + { + "pr": 1972, + "head": "fd82d172f46933fd253c2c6de4bd5eaff5429cfd", + "role": "Rohan Arun scalar/frame channel witness" + }, + { + "pr": 1991, + "retained_commit": "6e222517e182e98499239bc9a4009f540e1c5520", + "role": "Chafik Boukhalfa native realization; witness retained unchanged" + }, + { + "pr": 1940, + "head": "a9b7dfe2809092a9a4c90784d12bb60061e995e8", + "role": "Adam Gall schedule" + }, + { + "discussion": 2131, + "role": "Hope7Happiness fixed-component proposal and released exact-ordering handoff; no unpublished code imported" + } + ], + "discovery": { + "method": "Z3 finite infection-time model nominated an unsatisfiable core, then deletion reduction exposed ten contacts.", + "z3_version": "5.3.0.0", + "acceptance": "No solver dependency. Written first-contact proof and two exact standard-library enumerations." + }, + "result_kind": "scoped proof with exact finite certificate", + "upstream_refresh": { + "checked_utc": "2026-10-14T22:47:26Z", + "commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "priority_revision": 4, + "relevant_changes": "None: main, contribution guidance, selected record and native-channel inputs unchanged. Continue the scoped capture obstruction." + }, + "overlap": { + "queries": [ + "--task p104-side-correction", + "first-contact / capture-order / X58 / single-room" + ], + "open_prs_fetched_at": "2026-10-14T22:41:55.402359+00:00", + "open_prs": 429, + "discussions_fetched_at": "2026-10-14T22:44:37.402621+00:00", + "discussion_records": 867, + "complete_pagination": true, + "nearest": "Discussion2131 fixed component and its released ordering handoff; this claim is comment18935509. PR2172 and PR2178 study different retained-chronology and transcript models.", + "limits": "Cached open PR bodies including drafts, discussions and local package metadata; may miss subsequent changes or code-only overlap. Not a novelty certificate." + } +} diff --git a/research/p104-carrier-capture-order/VERIFY.json b/research/p104-carrier-capture-order/VERIFY.json new file mode 100644 index 0000000000..3a7267f639 --- /dev/null +++ b/research/p104-carrier-capture-order/VERIFY.json @@ -0,0 +1,33 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/p104-native-channel/PROOF.md", + "research/p104-native-channel/inputs/LOWRANK-WITNESS.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Source binding, finite proof premises, two exact order censuses, all single-contact deletions, original capture positive control, relaxed caps and certificate mutations." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Same read-only mathematical replay and controls with Python assertions disabled." + } + ] +} diff --git a/research/p104-carrier-capture-order/verify.py b/research/p104-carrier-capture-order/verify.py new file mode 100644 index 0000000000..8c8f1089f7 --- /dev/null +++ b/research/p104-carrier-capture-order/verify.py @@ -0,0 +1,328 @@ +"""Exact, read-only verification of a ten-contact P104 capture obstruction. + +Standard library only. No producer, scheduler, SMT solver or native compiler is +imported. The written first-contact proof is in README.md. Two finite engines +independently count legal orders: cap-membership signatures and actual subspaces. +Prepared for commdata2338 with substantial OpenAI Codex assistance. Apache-2.0. +""" + +import argparse +from collections import Counter +from copy import deepcopy +from fractions import Fraction +from functools import lru_cache +import hashlib +import json +from pathlib import Path + + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parents[1] +WITNESS = "research/p104-native-channel/inputs/LOWRANK-WITNESS.json" +WITNESS_SHA256 = "0f541bef7f19fdeffd67157684e9f03d785f42c89973632f508fc1a0452b580e" +CORE_IDS = (631, 745, 799, 807, 945, 1154, 1160, 1267) +ROOM = (32, 196) +FULL = frozenset(range(512)) + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def strict_json(raw): + def pairs(items): + result = {} + for key, value in items: + need(key not in result, "duplicate JSON key: " + key) + result[key] = value + return result + + def nonfinite(value): + raise ValueError("nonfinite JSON value: " + value) + + return json.loads(raw, object_pairs_hook=pairs, parse_constant=nonfinite) + + +def canonical(value): + # Comparing serialized JSON also distinguishes True from 1. + return json.dumps(value, sort_keys=True, separators=(",", ":")) + + +def basis(vectors): + """Independent binary row reduction, using highest-bit pivots.""" + rows = {} + for value in vectors: + need(type(value) is int and 0 <= value < 512, "invalid frame vector") + for pivot in sorted(rows, reverse=True): + if value >> pivot & 1: + value ^= rows[pivot] + if value: + pivot = value.bit_length() - 1 + for old in rows: + if rows[old] >> pivot & 1: + rows[old] ^= value + rows[pivot] = value + return tuple(rows[p] for p in sorted(rows, reverse=True)) + + +def contains(rows, value): + for row in rows: + if value >> (row.bit_length() - 1) & 1: + value ^= row + return value == 0 + + +def span(vectors): + """Independent explicit-vector implementation; no row reduction.""" + result = {0} + for value in vectors: + result |= {x ^ value for x in tuple(result)} + return frozenset(result) + + +def join(left, right): + return frozenset(x ^ y for x in left for y in right) + + +def dimension(space): + size = len(space) + need(size > 0 and size & (size - 1) == 0, "not a power-of-two space") + return size.bit_length() - 1 + + +def extract(witness): + program = witness["program"] + need(len(program) == 4058, "wrong source program length") + queries = {} + for index, event in enumerate(program): + if (event[0] == "add" and event[1].startswith("Q") + and event[2].startswith("G") and Fraction(event[3]) == 1): + need(event[2] not in queries, "duplicate positive G query") + queries[event[2]] = {"event_id": index, "query": event[1], + "frame": event[4]} + need(len(queries) == 32, "wrong query-cap inventory") + first_query = min(q["event_id"] for q in queries.values()) + captures = [] + for index, event in enumerate(program[:first_query]): + if event[0] == "add" and event[1].startswith("G") and event[2].startswith("X"): + captures.append({"event_id": index, "helper": event[1], + "source": event[2], "coefficient": str(Fraction(event[3]))}) + need(len(captures) == 416, "wrong original capture inventory") + by_id = {e["event_id"]: e for e in captures} + core = [by_id[i] for i in CORE_IDS] + core += [{"event_id": "carrier-X2", "helper": "B0", "source": "X2", "coefficient": "1"}, + {"event_id": "carrier-X4", "helper": "B0", "source": "X4", "coefficient": "1"}] + names = sorted({e[k] for e in core for k in ("helper", "source")}) + helpers = sorted({e["helper"] for e in core}) + initial = {v: span(witness["initial_frames"].get(v, [])) for v in names} + cap_rows = {g: queries[g]["frame"] if g != "B0" else list(ROOM) for g in helpers} + caps = {g: span(rows) for g, rows in cap_rows.items()} + for g in helpers: + need(initial[g] == frozenset({0}), "helper must start in frame zero") + return core, names, helpers, initial, caps, cap_rows, queries, captures + + +def check_first_contact_premises(core, helpers, initial, caps): + """Check the finite hypotheses of the written injection argument.""" + sources = sorted({e["source"] for e in core}) + pairs = [] + for source in sources: + neighbors = [e["helper"] for e in core if e["source"] == source] + need(len(neighbors) == 2 and len(set(neighbors)) == 2, + "each source must have two distinct required contacts") + need(len(initial[source]) == 2, "source must start in a nonzero line") + allowed = [h for h in helpers if initial[source] <= caps[h]] + need(sorted(neighbors) == allowed, "a nonincident cap admits a source label") + pairs.append(tuple(sorted(neighbors))) + need(len(set(pairs)) == len(pairs), "two sources use the same helper pair") + need(len(sources) > len(helpers), "no first-contact pigeonhole deficit") + return {"sources": len(sources), "helpers": len(helpers), "deficit": len(sources) - len(helpers)} + + +def signature_census(core, names, helpers, initial, caps): + """Count every legal permutation via exact cap-membership signatures.""" + width = len(helpers) + mask = (1 << width) - 1 + index = {v: i for i, v in enumerate(names)} + edges = [(index[e["helper"]], index[e["source"]]) for e in core] + forbidden = [1 << helpers.index(v) if v in helpers else 0 for v in names] + initial_state = sum(sum((not initial[v] <= caps[h]) << k for k, h in enumerate(helpers)) + << (width * i) for i, v in enumerate(names)) + rejected = 0 + + @lru_cache(None) + def visit(remaining, state): + nonlocal rejected + if not remaining: + return 1, () + count, example = 0, () + for i, (a, b) in enumerate(edges): + if not remaining >> i & 1: + continue + merged = (state >> (width * a) & mask) | (state >> (width * b) & mask) + if merged & (forbidden[a] | forbidden[b]): + rejected += 1 + continue + updated = state & ~((mask << (width * a)) | (mask << (width * b))) + updated |= (merged << (width * a)) | (merged << (width * b)) + ways, tail = visit(remaining ^ (1 << i), updated) + count += ways + if ways and not example: + example = (i,) + tail + return count, example + + count, example = visit((1 << len(core)) - 1, initial_state) + return {"legal_orders": count, "states": visit.cache_info().currsize, + "rejected_moves": rejected, + "example": [core[i]["event_id"] for i in example]} + + +def subspace_census(core, names, initial, caps): + """Second implementation: actual sets of vectors, with no signature code.""" + index = {name: i for i, name in enumerate(names)} + endpoints = [(index[e["helper"]], index[e["source"]]) for e in core] + + @lru_cache(None) + def count(todo, frames): + if not todo: + return 1 + total = 0 + for event in todo: + a, b = endpoints[event] + common = join(frames[a], frames[b]) + if any(names[v] in caps and not common <= caps[names[v]] for v in (a, b)): + continue + after = list(frames) + after[a] = after[b] = common + total += count(tuple(i for i in todo if i != event), tuple(after)) + return total + + answer = count(tuple(range(len(core))), tuple(initial[v] for v in names)) + return {"legal_orders": answer, "states": count.cache_info().currsize} + + +def replay_order(core, order, initial, caps): + need(len(order) == len(core) and Counter(order) == Counter(e["event_id"] for e in core), + "order omits or repeats a required contact") + by_id = {e["event_id"]: e for e in core} + frames = dict(initial) + for event_id in order: + event = by_id[event_id] + a, b = event["helper"], event["source"] + common = join(frames[a], frames[b]) + need(common <= caps.get(a, FULL) and common <= caps.get(b, FULL), + "contact exceeds its fixed cap") + frames[a] = frames[b] = common + return frames + + +def must_reject(function): + try: + function() + except ValueError: + return + raise ValueError("a rejection control was accepted") + + +def build(witness): + core, names, helpers, initial, caps, cap_rows, queries, captures = extract(witness) + premise = check_first_contact_premises(core, helpers, initial, caps) + sources = sorted({e["source"] for e in core}) + membership = {} + for source in sources: + label = next(x for x in initial[source] if x) + membership[source] = {h: contains(basis(cap_rows[h]), label) for h in helpers} + need(all(membership[source][h] == (label in caps[h]) for h in helpers), + "row-reduction / explicit-span membership disagreement") + fast = signature_census(core, names, helpers, initial, caps) + exact = subspace_census(core, names, initial, caps) + need(fast["legal_orders"] == exact["legal_orders"] == 0, "core is feasible") + deletions = [] + for i, omitted in enumerate(core): + reduced = core[:i] + core[i + 1:] + a = signature_census(reduced, names, helpers, initial, caps) + b = subspace_census(reduced, names, initial, caps) + need(a["legal_orders"] == b["legal_orders"] > 0, "deletion control failed") + replay_order(reduced, a["example"], initial, caps) + must_reject(lambda: check_first_contact_premises(reduced, helpers, initial, caps)) + deletions.append({"omitted": omitted["event_id"], "signature": a, "subspace": b}) + + # Every original capture remains possible without the added carrier. + all_initial = {v: span(rows) for v, rows in witness["initial_frames"].items()} + all_caps = {g: span(q["frame"]) for g, q in queries.items()} + baseline = replay_order(captures, [e["event_id"] for e in captures], all_initial, all_caps) + baseline_summary = {"captures": len(captures), "helpers": len(all_caps), + "final_G_dimensions": dict(sorted((g, dimension(baseline[g])) for g in all_caps))} + + relaxed = [] + for helper in ("G1", "B0"): + enlarged = dict(caps) + enlarged[helper] = FULL + must_reject(lambda: check_first_contact_premises(core, helpers, initial, enlarged)) + a = signature_census(core, names, helpers, initial, enlarged) + b = subspace_census(core, names, initial, enlarged) + need(a["legal_orders"] == b["legal_orders"] > 0, "relaxed-cap control failed") + replay_order(core, a["example"], initial, enlarged) + relaxed.append({"helper": helper, "legal_orders": a["legal_orders"], "example": a["example"]}) + + wrong_initial = dict(initial) + wrong_initial["X4"] = initial["X2"] + must_reject(lambda: check_first_contact_premises(core, helpers, wrong_initial, caps)) + must_reject(lambda: replay_order(core, [e["event_id"] for e in core][:-1], initial, caps)) + return {"schema_version": 1, "source_sha256": WITNESS_SHA256, + "room": list(ROOM), "contacts": core, + "source_labels": {v: sorted(initial[v] - {0}) for v in sources}, + "helper_caps": cap_rows, + "query_bindings": {g: queries[g] for g in helpers if g != "B0"}, + "membership": membership, "first_contact_premises": premise, + "signature_census": fast, "subspace_census": exact, + "single_contact_deletions": deletions, + "original_capture_control": baseline_summary, + "relaxed_cap_controls": relaxed, + "rejected_controls": ["ten_single_contact_deletions_in_proof_checker", + "G1_cap_enlargement_in_proof_checker", + "B0_cap_enlargement_in_proof_checker", + "wrong_initial_source_label", "omitted_contact_in_order", + "changed_coefficient_in_certificate", "changed_count_in_certificate", + "boolean_for_integer_in_certificate", "duplicate_JSON_key"]} + + +def compare(expected, supplied): + need(canonical(expected) == canonical(supplied), "certificate differs from exact reconstruction") + + +def certificate_controls(expected): + wrong = deepcopy(expected) + wrong["contacts"][0]["coefficient"] = "-2" + must_reject(lambda: compare(expected, wrong)) + wrong = deepcopy(expected) + wrong["signature_census"]["legal_orders"] = 1 + must_reject(lambda: compare(expected, wrong)) + wrong = deepcopy(expected) + wrong["first_contact_premises"]["deficit"] = True + must_reject(lambda: compare(expected, wrong)) + must_reject(lambda: strict_json('{"a": 0, "a": 1}')) + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--certificate", type=Path, default=PACKAGE / "CERTIFICATE.json") + parser.add_argument("--write-certificate", type=Path, + help="write the exact reconstruction exclusively to a new file") + args = parser.parse_args() + raw = (ROOT / WITNESS).read_bytes() + need(hashlib.sha256(raw).hexdigest() == WITNESS_SHA256, "pinned witness changed") + expected = build(strict_json(raw)) + certificate_controls(expected) + if args.write_certificate: + with args.write_certificate.open("x") as handle: + handle.write(json.dumps(expected, sort_keys=True, indent=2) + "\n") + else: + compare(expected, strict_json(args.certificate.read_bytes())) + print("PASS_P104_CARRIER_CAPTURE_ORDER contacts=10 sources=5 helpers=4 " + "legal_orders=0 deletion_controls=10 original_captures=416 no_new_kappa") + + +if __name__ == "__main__": + main()