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()