diff --git a/research/p104-temporal-cut-obstruction/README.md b/research/p104-temporal-cut-obstruction/README.md new file mode 100644 index 0000000000..73b84c40b6 --- /dev/null +++ b/research/p104-temporal-cut-obstruction/README.md @@ -0,0 +1,264 @@ +# A sharp temporal information cut for the native P104 channel + +**Scoped obstruction: the frozen P104 frame schedule carries at most eight +independent source ports to its 104 targets, even after arbitrary same-frame +linear redesign. Its existing `G/2` channel attains this bound.** Completing +identity transfer requires a changed information-access schedule. + +There is also a cost obstruction for a precise completion class: retain the +original events and storage lifetimes, and insert paid frame excursions that +return every register to its original frame before the next original event. +Any such completion needs at least **96 additional positive-rank transports**. +Under the retained fully hosted, four-pair, nine-stage coverage contract, even +their minimum mass makes the zero-saving moment at least **7659/7592 > 1**. +No packing of idle children can repair this deficit within that contract. + +This answers the `p104-side-correction` card for these two classes. It is not a +general P104 impossibility theorem, an admitted supplier, or a new kappa. +Persistent frame changes across checkpoints, retiming, new storage and changed +coverage remain open. The selected result is unchanged. + +## Exact object and contribution + +The input is Rohan Arun's [PR1972](https://github.com/CrocSwap/integer-mult-bounds/pull/1972) +word at `fd82d172f46933fd253c2c6de4bd5eaff5429cfd`, retained byte-for-byte in +[PR1991's native package](../p104-native-channel/README.md), by Chafik Boukhalfa, +head `6e222517e182e98499239bc9a4009f540e1c5520`. +It has 4,058 events, 104 sources, 104 targets, 72 arbitrary dirty helpers and +eight separate lifetimes of one private copy register `C`. + +The predecessor proves the existing word's endpoint. This package proves an +upper bound for **every linear program on its chronological common-frame +access graph**, allowing substantially more communication than the published +scalar word. It also derives a conditional cost lower bound for restoring +excursions inserted into that graph. These are new implications rather than +another native compilation or another endpoint audit. + +The independent forward and backward graph checks identify exactly these +zero-based event indices as a separating cut: + +```text +2463 2472 2479 2487 2495 2503 2510 2518 +``` + +Each is a private `C` descent from a dimension-eight frame to dimension one, +charged native rank seven. Each edge has **information capacity one register**; +the information-capacity count eight and the native invoice COPY56 are different +quantities. The cut disconnects every source from every final target. Restoring +any one edge restores paths from 52 sources; restoring all eight restores paths +from all 104. Reachability counts do not themselves assert achievable ranks. + +## 1. Temporal-cut theorem + +At every cut before and after each frozen event, group all live registers by +their actual binary subspace, independently of the supplied basis. Grant +arbitrary linear mixing within every group. Retain the frozen transport order, +entry/exit frames, private allocations and discards. A transport carries the +register's information between two consecutive cuts; allocation starts with +no source information, and discard ends that lifetime. Literal additions and +copies are contained in the common-frame mixing relaxation. + +The executable certificate deletes the eight edges above and propagates source +reachability through **every** common-frame group at **all 4,059 cuts**. None of +the targets is reached. A separately implemented reverse propagation starts +from all targets and reaches no source. This is a finite graph-cut certificate, +not a bounded search for favorable scalar coefficients. + +**Cut lemma.** Fix all other inputs and let each register hold a vector of +dimension `D`. If `c` through-register edges separate the source inputs from the +target outputs of a linear chronological circuit, its source-to-target linear +map has rank at most `cD`. + +To prove it, expose the `c` values crossing the deleted edges as separate +`D`-dimensional signals. Every output depends linearly on those signals and +on source-independent data: otherwise its dependency graph would contain an +uncut source-to-output path. Thus the source-to-output map factors through a +space of dimension at most `cD`. Same-cut mixing can be regarded as one linear +map per common-frame group; there is no requirement to execute cyclic graph +edges simultaneously. Giving that group arbitrary mixing only enlarges the +admissible class. + +The certificate therefore bounds the P104 transfer rank by **8D**, even if +source/helper restoration is waived and all scalar coefficients are changed. +For scalar logical rows this is rank at most eight. For the finite native +nine-coordinate address space, `D=512`. Invertible intrinsic endpoint adapters +do not change the rank. This linear-algebra statement for arbitrary finite `D` +does not establish an all-size implementation or compiler theorem. + +**Sharpness.** Reconstruct the 104 retained E8 root lines from doubled integer +coordinates, and write `A` for the matrix of ordinary root rows. Direct integer +arithmetic gives `A^t A = 26 I_8`, hence `G=AA^t` has rank eight and +`G^2=26G`. An independent rational replay of all 280 input columns confirms +the predecessor endpoint `y <- y+(G/2)x`, including dirty-helper restoration. +Its native realization is inherited from PR1991. It attains rank `8D`, so the +cut bound is sharp. + +The desired endpoint `y <- y+x` has rank `104D` from source to target. +Consequently no coefficient changes, extra same-frame additions, helper/target +mixing or same-frame linear processing on this frozen timeline can complete it. +This conclusion does not follow merely from the existing decoder's rank eight; +the saturated temporal graph is what excludes other decoder choices. + +For an explicit lost-information witness, `z_t=26 e_t-G e_t` satisfies +`G z_t=0` and `(I-G/2)z_t=z_t`, with coordinate `t` equal to 24. The checker +verifies all 104 such witnesses. It also checks + +```text +(I-G/2)^(-1) = I-G/24. +``` + +Thus the correction itself has rank 104, despite its zero diagonal. + +## 2. Restoring excursions need at least 96 added transports + +The following additional hypotheses are essential: + +1. Every original event, its frame endpoints and its order are retained. +2. Extra blocks may be inserted at any frozen cut, but **all live registers + return to that cut's prescribed frames before the next original event**. +3. No additional storage lifetimes or external input channels are introduced. +4. Added frame changes are positive-rank nested transports, charged at least + one each. No free cross-frame operation is introduced. Original paid + transports are not removed, fused away or given an accounting credit. + +Within these rules, scalar operations may be redesigned arbitrarily. Let `K` +be the number of added transport occurrences, summed over all insertion blocks. +Delete all `K` of these edges and the original eight cut edges. Every surviving +path through an inserted block stays in a single frame. Its entry and exit +registers therefore belonged to the same frozen common-frame group, so that +path contracts to an edge already granted in the original saturated graph. +The `8+K` edges consequently separate source and target in the augmented graph. + +By the cut lemma, identity transfer requires `104D <= (8+K)D`, so **K >= 96**. +Since each added positive transport costs at least one rank, the added rank +mass is at least 96. This is a necessary bound, not an assertion that a +96-transport completion exists or that the bound is sharp. + +**Why the checkpoint restriction matters.** A register that stays in a changed +frame across original events can receive source data later and retain it until +a target becomes available. Its data path can avoid both the transport into +that frame and the eventual transport back. Such persistent buffers can also +stream multiple forms. Deleting the added transport edges does not prove the +same bound for that model. No general long-lived-detour lower bound is claimed. + +## 3. Conditional complete-mass screen + +Use the retained width-73, nine-stage, four-pair template with 104 ports and +all helpers hosted on the live data families. This gives `W=8*104=832` families +and `N=9` calls per replica. Assume the original coverage is charged as + +```text +baseline paid mass = 72 W + 56 N, +``` + +and every added local transport contributes excess mass without reducing that +baseline. This is the explicitly stated application of the coverage model in +[the packing-ceiling package](../complex-local-word-ceiling/README.md), with +COPY56 in place of the selected word's COPY64. It is an optimistic retained +hosting contract, **not** a claim to have constructed chronological owners for +P104. An alternative template or an accounting cancellation requires a new bill. + +The exact integer calculation is: + +| Quantity per replica | Value | +|---|---:| +| Baseline mass `72*832+56*9` | 60,408 | +| Available mass `73*832` | 60,736 | +| Baseline headroom | 328 | +| Minimum added mass `96*9` | 864 | +| Minimum completed mass | 61,272 | + +There are only `328/9` spare ranks per call. At saving zero the normalized +moment is at least `61272/60736 = 7659/7592 > 1`. For every nonnegative saving +`a` and admissible child rank `0 < r <= 73`, +`(r/73)^(1-a) >= r/73`; therefore its moment is also greater than one. +The class fails before any exponential/logarithm approximation, regardless of +idle packing or how the extra mass is grouped into children. Positive overhead +charges can only worsen this favorable screen. + +Do not put the added transports into a fixed-coverage calculator while silently +subtracting their mass from the idle remainder. These restoring excursions +retain the original paid word and add excess; they do not replace idle work. +For example, **208 added ranks per call** would give +`(60408+9*208)/60736 = 7785/7592 > 1` already at saving zero under this contract. +A favorable screen obtained by retaining COPY56 as the only excess charge while +increasing the local profile is pricing a different model: it implicitly +credits an equal reduction in idle mass. Such a reduction needs a construction +and proof; it does not follow from the completed local profile alone. + +## Reproduce and inspect + +Standard-library Python 3.10 or later; registered CI uses Python 3.12: + +```sh +python3 -I -O -B research/p104-temporal-cut-obstruction/verify.py +python3 scripts/research_package.py --package research/p104-temporal-cut-obstruction --check-only +python3.12 scripts/research_package.py --package research/p104-temporal-cut-obstruction +``` + +The first command compares the complete recomputed receipt with +[RESULT.json](RESULT.json), authenticates all external inputs and writes nothing. +`--write` deliberately regenerates only this package's receipt. No network, +Git or predecessor producer/compiler is used by the direct replay. The generic +metadata check separately requires the pinned Git provenance. + +Checks include actual frame subspaces, all 4,058 chronological operations, +private lifetimes, forward and independently implemented backward cuts, the +intact-graph positive control, all eight single-edge restorations, exact Gram +identities, 280-column dirty scalar replay and the rational budget. Mutations +remove dirty compensation, falsify a transport rank, falsify an endpoint and +insert a real two-transport source-to-target bridge; each is rejected for its +intended mathematical reason. The bridge control demonstrates that new paid +access really can invalidate the original eight-edge cut. + +Native Clifford recipes, chronological owner assignment, precision/tape bounds, +all-size admission, outer transfer and the selected full cold replay are not +rerun or newly established here. None is needed to certify this finite access +obstruction. This is a written proof with finite exact certificates, not a +proof-assistant formalization. + +## Open next questions + +- **Can a persistent changed-frame schedule deliver the missing information + within the full budget?** This is the direct escape from the theorem. Start + with one source/helper kept at a useful frame across a frozen checkpoint and + re-run the saturated reachability test. Then count total added and displaced + transports and test arbitrary dirty-state restoration. A new graph, full + invoice and physical realization are the blockers. +- **Can retiming replace existing transport work rather than adding restoring + excursions?** Interleave correction reads with gather/delivery before sources + finish. The first useful artifact is a changed timeline with a larger + source-to-target cut and an explicit accounting of removed versus added + children. The frozen proof cannot price these cancellations automatically. +- **Does a different global coverage contract admit a completed changed word?** + Recompute families per call, unpaid coordinates, private-copy costs and all + idle children before claiming a moment gain. A legal completed local word and + chronological hosting remain prerequisites. + +Structured scopes, exact provenance and overlap freshness are recorded in +[TASK.json](TASK.json) and [SOURCES.json](SOURCES.json). + +## Credit and overlap + +Rohan Arun / PR1972 owns the scalar/frame channel; Chafik Boukhalfa / PR1991 +owns its concrete native realization; Adam Gall / PR1940 +(`a9b7dfe2809092a9a4c90784d12bb60061e995e8`) owns the delivery schedule. The +P104 fixture and decoder come from Josie Elliston / PR1071 and Ali Romman / +PR1125, with the retained PR968/717/446/595/620 lineage. The global coverage +identity is PR1012's; the packing-ceiling exposition is Douglas Colkitt's. +No predecessor files are modified or copied into a new package. + +At entry, [the concurrent final-query-cut claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1167#discussioncomment-18931651) +proposed a concrete side correction using added target excursions. Its +[terminal-cut update](https://github.com/CrocSwap/integer-mult-bounds/discussions/1167#discussioncomment-18931708) +and [a second terminal-cut claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1167#discussioncomment-18931718) +were also read before submission. This package does not construct or validate +those unpublished words. The 208-rank illustration above explains the complete +accounting condition that their favorable local-profile screens still need to +justify. The graph theorem and lower bound concern the broader precisely +defined classes above. Discussion claims remain provisional overlap evidence. + +Prepared for David Arias with substantial OpenAI Codex assistance, including +separate mathematical derivations and independently written reverse checking. +Apache-2.0. No independent human review or literature-priority guarantee is +claimed. diff --git a/research/p104-temporal-cut-obstruction/RESULT.json b/research/p104-temporal-cut-obstruction/RESULT.json new file mode 100644 index 0000000000..b484e4aeb6 --- /dev/null +++ b/research/p104-temporal-cut-obstruction/RESULT.json @@ -0,0 +1,225 @@ +{ + "algebra": { + "correction_inverse": "I-G/24", + "correction_rank": 104, + "gram_rank": 8, + "gram_square_multiplier": 26, + "kernel_witnesses": 104, + "nonzero_correction_entries": 4992, + "ports": 104 + }, + "backward": { + "algorithm": "reverse relevance with explicitly enumerated F2 span classes", + "blocked_source_count": 0, + "deleted_transport_indices": [ + 2463, + 2472, + 2479, + 2487, + 2495, + 2503, + 2510, + 2518 + ], + "event_count": 4058, + "intact_source_count": 104, + "private_lifetimes": 8, + "scope": "Frozen frame chronology, arbitrary scalar mixing within each exact frame class; no supplier or kappa claim.", + "single_restored_edge_controls": [ + { + "restored_edge": 2463, + "source_count": 52 + }, + { + "restored_edge": 2472, + "source_count": 52 + }, + { + "restored_edge": 2479, + "source_count": 52 + }, + { + "restored_edge": 2487, + "source_count": 52 + }, + { + "restored_edge": 2495, + "source_count": 52 + }, + { + "restored_edge": 2503, + "source_count": 52 + }, + { + "restored_edge": 2510, + "source_count": 52 + }, + { + "restored_edge": 2518, + "source_count": 52 + } + ], + "status": "PASS_P104_BACKWARD_TEMPORAL_CUT", + "transport_profile": { + "1": 1074, + "2": 58, + "3": 86, + "4": 104, + "5": 48, + "6": 24, + "7": 8, + "8": 8 + } + }, + "conditional_budget": { + "baseline_headroom_per_call": "328/9", + "baseline_paid_mass": 60408, + "calls": 9, + "capacity": 60736, + "example_208_added_rank_moment_at_zero": "7785/7592", + "families": 832, + "minimum_added_transport_occurrences_per_call": 96, + "minimum_completed_paid_mass": 61272, + "minimum_moment_excess": "67/7592", + "model": "checkpoint-preserving insertions; retained fully hosted nine-stage four-pair coverage", + "omitted_extra_charge_positive_control": "7551/7592", + "positive_saving_possible_in_this_model": false, + "private_copy_rank_per_call": 56, + "width": 73, + "zero_saving_moment_lower_bound": "7659/7592" + }, + "controls": [ + "missing_dirty_compensation", + "incorrect_transport_rank", + "dependent_frame_basis", + "incorrect_common_gate_frame", + "erasure_outside_owned_private_role", + "all_frame_basis_orders_reversed_same_certificate", + "incorrect_claimed_endpoint", + "new_paid_bridge_invalidates_old_cut" + ], + "forward": { + "backward_ever_reachable_sources": [], + "backward_reachable_initial_sources": [], + "common_frame_groups_saturated": 219637, + "deleted_edge_count": 8, + "deleted_edges": [ + { + "event_index": 2463, + "native_rank": 7, + "new_dimension": 1, + "old_dimension": 8, + "reachable_source_inputs_before_deletion": 52, + "reachable_target_outputs_after_deletion": 52, + "register": "C" + }, + { + "event_index": 2472, + "native_rank": 7, + "new_dimension": 1, + "old_dimension": 8, + "reachable_source_inputs_before_deletion": 52, + "reachable_target_outputs_after_deletion": 52, + "register": "C" + }, + { + "event_index": 2479, + "native_rank": 7, + "new_dimension": 1, + "old_dimension": 8, + "reachable_source_inputs_before_deletion": 52, + "reachable_target_outputs_after_deletion": 52, + "register": "C" + }, + { + "event_index": 2487, + "native_rank": 7, + "new_dimension": 1, + "old_dimension": 8, + "reachable_source_inputs_before_deletion": 52, + "reachable_target_outputs_after_deletion": 52, + "register": "C" + }, + { + "event_index": 2495, + "native_rank": 7, + "new_dimension": 1, + "old_dimension": 8, + "reachable_source_inputs_before_deletion": 52, + "reachable_target_outputs_after_deletion": 52, + "register": "C" + }, + { + "event_index": 2503, + "native_rank": 7, + "new_dimension": 1, + "old_dimension": 8, + "reachable_source_inputs_before_deletion": 52, + "reachable_target_outputs_after_deletion": 52, + "register": "C" + }, + { + "event_index": 2510, + "native_rank": 7, + "new_dimension": 1, + "old_dimension": 8, + "reachable_source_inputs_before_deletion": 52, + "reachable_target_outputs_after_deletion": 52, + "register": "C" + }, + { + "event_index": 2518, + "native_rank": 7, + "new_dimension": 1, + "old_dimension": 8, + "reachable_source_inputs_before_deletion": 52, + "reachable_target_outputs_after_deletion": 52, + "register": "C" + } + ], + "dirty_helper_count": 72, + "event_boundary_count": 4059, + "event_count": 4058, + "forward_ever_reachable_targets": [], + "forward_reachable_final_targets": [], + "initial_register_count": 280, + "maximum_live_register_count": 281, + "operation_counts": { + "add": 2624, + "copy": 8, + "erase": 8, + "transport": 1410, + "zero": 8 + }, + "paid_profile": { + "1": 1074, + "2": 58, + "3": 86, + "4": 104, + "5": 48, + "6": 24, + "7": 8, + "8": 8 + }, + "private_lifetime_count": 8, + "rank_mass": 2368, + "relaxation": "Arbitrary common-frame linear mixing among all live registers at every event boundary; the native transport sequence and private lifetimes are fixed.", + "source_count": 104, + "source_to_target_coefficient_rank_upper_bound": 8, + "status": "PASS_P104_FROZEN_TEMPORAL_EIGHT_EDGE_CUT", + "target_count": 104 + }, + "scalar_positive_control": { + "arbitrary_input_columns": 280, + "dirty_helpers_restored": 72, + "events": { + "add": 2624, + "copy": 8, + "erase": 8, + "transport": 1410, + "zero": 8 + } + }, + "scope": "Sharp rank-eight obstruction for the frozen chronological common-frame access graph; conditional no-saving result for checkpoint-preserving paid transport insertions. No general P104 impossibility, supplier admission or new kappa.", + "status": "PASS_P104_TEMPORAL_CUT_OBSTRUCTION" +} diff --git a/research/p104-temporal-cut-obstruction/SOURCES.json b/research/p104-temporal-cut-obstruction/SOURCES.json new file mode 100644 index 0000000000..ee5137b083 --- /dev/null +++ b/research/p104-temporal-cut-obstruction/SOURCES.json @@ -0,0 +1,130 @@ +{ + "schema_version": 1, + "base_commit": "564148b82ae9df72163f22106f15e73efca8aff2", + "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/SUMMARY.json", + "usage": "input", + "git_blob": "fba272d33b0040074c130e4072875b55bb01d8a1", + "sha256": "5631a08e4500c0b66dc6d91e86c3006863a120eb364eeeb33943c16e233797d8" + }, + { + "path": "research/p104-native-channel/inputs/LOWRANK-WITNESS.json", + "usage": "input", + "git_blob": "86beaf424e9f0f800ae3a62797d94ec9386b7706", + "sha256": "0f541bef7f19fdeffd67157684e9f03d785f42c89973632f508fc1a0452b580e" + }, + { + "path": "research/p104-native-channel/inputs/P104-FIXTURE.json", + "usage": "input", + "git_blob": "2e16f99b295bb386fd13bd8fbd57b42ef54143a9", + "sha256": "516c06f6ec3cb84be588c546108de897650288576dd5fbf5fe44b9c5546ad8a4" + }, + { + "path": "research/complex-local-word-ceiling/README.md", + "usage": "input", + "git_blob": "f5f742f8196da29d2c3f4dffb3c27685ca9401f6", + "sha256": "b60be039cb0e03e064a27407d0bce9e58908d793da5ee405c876de5aebfa5f81" + }, + { + "path": "research/complex-local-word-ceiling/ceiling.py", + "usage": "input", + "git_blob": "6c0f54527d879396f689523bfde19928a9b6157c", + "sha256": "86a1432870b3b21d8454106ec9162fddc0471472d9214c590a1420f2426cedfc" + } + ], + "predecessors": [ + { + "pr": 1972, + "author": "Rohan Arun", + "head": "fd82d172f46933fd253c2c6de4bd5eaff5429cfd", + "role": "Complete scalar and frame channel; exact witness retained by PR1991" + }, + { + "pr": 1991, + "author": "Chafik Boukhalfa", + "head": "6e222517e182e98499239bc9a4009f540e1c5520", + "role": "Native realization and exact retained inputs" + }, + { + "pr": 1940, + "author": "Adam Gall", + "head": "a9b7dfe2809092a9a4c90784d12bb60061e995e8", + "role": "Chronological P104 delivery schedule" + } + ], + "entry_overlap": { + "searched_at": "2026-10-14T18:47:31.575567+00:00", + "coverage": { + "open_prs": { + "fetched_at": "2026-10-14T18:45:20.698398+00:00", + "complete_pagination": true, + "records": 349 + }, + "discussions": { + "fetched_at": "2026-10-14T18:47:31.477525+00:00", + "complete_pagination": true, + "records": 727 + } + }, + "limits": "Remote PR scope is open PRs including drafts. Closed work is searched through local READMEs, TASK metadata and ledger only. No code diffs or arbitrary package files are searched. Recheck relevant heads before submission.", + "concurrent_claim": { + "url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1167#discussioncomment-18931651", + "observed_at_utc": "2026-10-14T18:43:56Z", + "author": "1337isnot1337", + "scope": "Final query-live cut correction with target excursions; provisional claim only; not reproduced here", + "distinct_delta": "All-same-frame scalar redesign temporal cut and general checkpoint-preserving insertion lower bound, with conditional whole-mass screen." + } + }, + "submission_overlap": { + "searched_at": "2026-10-14T18:58:26.811196+00:00", + "coverage": { + "open_prs": { + "fetched_at": "2026-10-14T18:56:23.803387+00:00", + "complete_pagination": true, + "records": 352 + }, + "discussions": { + "fetched_at": "2026-10-14T18:58:26.646089+00:00", + "complete_pagination": true, + "records": 732 + } + }, + "warnings": [], + "limits": "Remote PR scope is open PRs including drafts. Closed work is searched through local READMEs, TASK metadata and ledger only. No code diffs or arbitrary package files are searched. Recheck relevant heads before submission.", + "upstream_commit": "564148b82ae9df72163f22106f15e73efca8aff2", + "priority_revision": 4, + "relevant_source_changes_since_base": false, + "decision": "Continue: complementary temporal cut and conditional mass obstruction; final-query-cut construction is credited and not duplicated. No matching obstruction found in the stated coverage.", + "additional_concurrent_claims": [ + { + "url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1167#discussioncomment-18931708", + "updated_at": "2026-10-14T18:46:57Z", + "scope": "Terminal correction via208 extra rank-one target transports; favorable fixed-coverage profile screen remains provisional" + }, + { + "url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1167#discussioncomment-18931718", + "updated_at": "2026-10-14T18:47:35Z", + "scope": "Second terminal correction construction with208 target transports; distinct from this information-cut and full-excess-mass bound" + } + ] + } +} diff --git a/research/p104-temporal-cut-obstruction/TASK.json b/research/p104-temporal-cut-obstruction/TASK.json new file mode 100644 index 0000000000..6722961bf3 --- /dev/null +++ b/research/p104-temporal-cut-obstruction/TASK.json @@ -0,0 +1,109 @@ +{ + "schema_version": 1, + "task_id": "p104-side-correction", + "priority_revision": 4, + "base_commit": "564148b82ae9df72163f22106f15e73efca8aff2", + "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": "refined", + "actual_scope": "Sharp rank-eight bound for all linear common-frame redesigns of the frozen P104 chronological access graph; at least96 added positive transports for checkpoint-preserving completion blocks; conditional failure at saving zero under retained fully hosted coverage.", + "scope_change_reason": "The final query-live correction is concurrently claimed in Discussion1167 comment18931651. This complementary obstruction targets every unchanged-frame scalar redesign, not that particular construction.", + "bottleneck_link": "The missing correction must deliver 104 independent source inputs. A temporal cut can distinguish scalar redesign from genuinely changed transport architecture and price the information missing from the native low-rank channel.", + "budget_minutes": 60, + "stop_rule": "Stop after a certified temporal cut and independent confirmation, or a counterexample to the claimed cut. One session about60 minutes; do not claim a universal P104 barrier.", + "outcome": "completed", + "evidence": "RESULT.json and README proof: exact eight-edge cut, independently implemented reverse graph, source Gram and280-column scalar replay, adverse controls; conditional moment7659/7592>1.", + "author": "David Arias", + "ai_assistance": "Substantial OpenAI Codex assistance including parallel mathematical analysis and independent review; no independent human review or formal proof assistant.", + "open_questions": [ + { + "question": "Can a persistent changed-frame schedule carry the missing source information within the complete budget?", + "why_it_matters": "A frame held across frozen checkpoints changes the information graph and escapes the proven insertion class.", + "first_step": "Keep one source/helper at an explicit frame across a frozen checkpoint, rerun saturated reachability, then price all added and displaced transports with dirty restoration.", + "blocked_by": "Requires a new chronological word, exact endpoints and full physical invoice." + }, + { + "question": "Can retiming replace existing work instead of inserting restoring excursions?", + "why_it_matters": "The no-saving corollary assumes the original coverage remains charged.", + "first_step": "Interleave side reads with gather/delivery and provide a transport-by-transport cancellation and cost ledger.", + "blocked_by": "No revised legal frame schedule and owner assignment is supplied." + }, + { + "question": "Does a changed global coverage contract allow a completed P104 word?", + "why_it_matters": "The arithmetic exclusion is specific to retained fully hosted four-pair nine-stage coverage.", + "first_step": "Derive families per call, unpaid coordinates, private-copy and idle costs from an actual new construction.", + "blocked_by": "Needs a completed local word, chronological hosting and all-size admission." + } + ], + "selection_nonce": "93db30a7529c26e21e5c6a6e4c251073", + "scope_key": "c5367b1a1b7bed20db53:p104-frozen-temporal-information-cut", + "coordination": "Local claim only: supplied user instructions require authorization for public coordination messages; no Discussion post made.", + "optimistic_budget": "Retained m=73, W=832, N=9 coverage: baseline mass72W+56N=60408 versus capacity60736. At least96 additional ranks/call raise mass to61272 and moment at saving0 to7659/7592>1. Conditional on unchanged baseline coverage and positive charges; persistent frame changes, retiming and different global models excluded.", + "validation": { + "registered_replay": { + "command": "/Users/david/.cache/codex-runtimes/codex-primary-runtime/dependencies/python/bin/python3.12 -B scripts/research_package.py --package research/p104-temporal-cut-obstruction", + "python": "3.12.14", + "status": "PASS_REGISTERED_RESEARCH_PACKAGE", + "platform": "macOS-27.0.1-arm64-arm-64bit-Mach-O", + "architecture": "arm64" + }, + "independent_review": { + "scope": "Code/proof consistency and exact read-only receipt replay by a separate AI agent", + "status": "passed", + "python": "3.14.7", + "not_human_review": true + }, + "not_run": [ + "Selected frontier1094 complete cold replay (selected construction unchanged)", + "Native Clifford recompilation (inherited PR1991 evidence)", + "All-size, physical hosting, precision or outer transfer proof" + ], + "source_export": { + "command": "Isolated Python3.12.14 -I -O -B direct replay from a read-only export containing only the package and pinned live inputs; run outside the export", + "status": "PASS_READ_ONLY_SOURCE_EXPORT", + "files": 14, + "git_available_in_export": false, + "hashes_unchanged": true + } + } +} diff --git a/research/p104-temporal-cut-obstruction/VERIFY.json b/research/p104-temporal-cut-obstruction/VERIFY.json new file mode 100644 index 0000000000..1197404ad1 --- /dev/null +++ b/research/p104-temporal-cut-obstruction/VERIFY.json @@ -0,0 +1,27 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/complex-local-word-ceiling/README.md", + "research/complex-local-word-ceiling/ceiling.py", + "research/p104-native-channel/PROOF.md", + "research/p104-native-channel/SUMMARY.json", + "research/p104-native-channel/inputs/LOWRANK-WITNESS.json", + "research/p104-native-channel/inputs/P104-FIXTURE.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Complete source-bound exact receipt: saturated temporal cut, independent reverse graph, all8 restored-edge controls, exact Gram identities,280-column dirty boundary and zero-saving budget; semantic mutation controls." + } + ] +} diff --git a/research/p104-temporal-cut-obstruction/backward.py b/research/p104-temporal-cut-obstruction/backward.py new file mode 100644 index 0000000000..df9a4fb2ad --- /dev/null +++ b/research/p104-temporal-cut-obstruction/backward.py @@ -0,0 +1,226 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Independent reverse information-flow check for the frozen P104 frame word. + +Uses explicit F2 span sets and backwards target relevance. Imports no channel +producer, native compiler, or forward reachability checker. No files are +modified. This checks a temporal scalar-register cut, not a universal barrier. +""" +from __future__ import annotations + +import argparse +from collections import Counter +from fractions import Fraction +import hashlib +import json +from pathlib import Path + +WITNESS_SHA256 = "0f541bef7f19fdeffd67157684e9f03d785f42c89973632f508fc1a0452b580e" +CUT_INDICES = (2463, 2472, 2479, 2487, 2495, 2503, 2510, 2518) + + +def require(condition: bool, message: str) -> None: + if not condition: + raise ValueError(message) + + +def span(generators) -> frozenset[int]: + """Enumerate the full subspace; no canonical-basis routine is used.""" + values = {0} + for generator in generators: + require(isinstance(generator, int) and 0 <= generator < 512, + "frame generator is outside F2^9") + values |= {value ^ generator for value in tuple(values)} + return frozenset(values) + + +def dimension(frame: frozenset[int]) -> int: + require(len(frame) > 0 and len(frame) & (len(frame) - 1) == 0, + "frame size is not a power of two") + return len(frame).bit_length() - 1 + + +def parse_word(witness: dict) -> tuple[dict, dict, list, dict]: + """Check the chronological frame word and normalize each literal event.""" + initial = {register: span(gens) + for register, gens in witness["initial_frames"].items()} + final = {register: span(gens) + for register, gens in witness["final_frames"].items()} + require(len(initial) == 280 and set(initial) == set(final), + "unexpected boundary register inventory") + current = dict(initial) + events = [] + positive_ranks = Counter() + private_births = private_deaths = 0 + for index, event in enumerate(witness["program"]): + kind = event[0] + if kind == "transport": + _, register, before_basis, after_basis, rank = event + before, after = span(before_basis), span(after_basis) + require(current.get(register) == before, + f"incorrect transport source frame at {index}") + require(before <= after or after <= before, + f"nonnested transport at {index}") + require(rank == abs(dimension(after) - dimension(before)) and rank > 0, + f"incorrect positive rank at {index}") + events.append((kind, register, before, after, rank)) + current[register] = after + positive_ranks[rank] += 1 + elif kind == "add": + _, target, source, coefficient, frame_basis = event + frame = span(frame_basis) + require(current.get(target) == current.get(source) == frame, + f"unequal-frame scalar addition at {index}") + Fraction(coefficient) # Require an exact rational literal. + events.append((kind, target, source, frame)) + elif kind == "zero": + _, register, frame_basis = event + frame = span(frame_basis) + require(register not in current and register == "C", + f"private allocation overwrites a live register at {index}") + current[register] = frame + events.append((kind, register, frame)) + private_births += 1 + elif kind == "copy": + _, target, source, frame_basis = event + frame = span(frame_basis) + require(current.get(target) == current.get(source) == frame, + f"unequal-frame private copy at {index}") + require(target == "C", f"copy destination outside private role at {index}") + events.append((kind, target, source, frame)) + elif kind == "erase": + _, register, frame_basis = event + frame = span(frame_basis) + require(current.get(register) == frame and register == "C", + f"invalid private discard at {index}") + del current[register] + events.append((kind, register, frame)) + private_deaths += 1 + else: + raise ValueError(f"unknown event kind {kind}") + require(current == final, "final frames mismatch") + require(private_births == private_deaths == 8, "private lifetime count mismatch") + derived_cut = tuple(index for index, event in enumerate(events) + if event[0] == "transport" and event[1] == "C" + and dimension(event[2]) == 8 and dimension(event[3]) == 1) + require(derived_cut == CUT_INDICES, "private drop edge indices mismatch") + return initial, final, events, { + "event_count": len(events), + "transport_profile": {str(rank): count for rank, count in sorted(positive_ranks.items())}, + "private_lifetimes": private_births, + } + + +def backwards(initial: dict, final: dict, events: list, + blocked: frozenset[int]) -> dict: + """Propagate arbitrary output dependence backwards through the supergraph. + + At every time cut, one relevant register makes *every* live register with + the same complete F2 frame relevant. These complete frame classes admit + more scalar communication than the published word. Blocked transport + events delete only their through-register edge; all other registers retain + their through-time identity edges. + """ + frames = dict(final) + relevant = {register for register in final if register.startswith("Y")} + require(len(relevant) == 104, "target count mismatch") + cut_relevance = [] + maximal_relevant = len(relevant) + + def mix() -> None: + nonlocal maximal_relevant + visible_frames = {frames[register] for register in relevant} + relevant.update(register for register, frame in frames.items() + if frame in visible_frames) + maximal_relevant = max(maximal_relevant, len(relevant)) + + mix() + for index in range(len(events) - 1, -1, -1): + event = events[index] + kind = event[0] + if kind == "transport": + _, register, before, after, _ = event + require(frames[register] == after, + f"reverse frame mismatch at {index}") + if index in blocked: + cut_relevance.append({"index": index, + "relevant_after_edge": register in relevant}) + relevant.discard(register) + frames[register] = before + elif kind == "copy": + _, target, source, _ = event + if target in relevant: + relevant.add(source) + # Assignment overwrites C. The complete common-frame mix before + # this event will independently restore any permitted dependence. + relevant.discard(target) + elif kind == "zero": + _, register, frame = event + require(frames[register] == frame, "reverse allocation mismatch") + relevant.discard(register) + del frames[register] + elif kind == "erase": + _, register, frame = event + require(register not in frames, "reverse erase finds live private role") + frames[register] = frame + elif kind == "add": + _, target, source, _ = event + if target in relevant: + relevant.add(source) + mix() + require(frames == initial, "backwards replay did not reach initial frames") + reached_sources = sorted((register for register in relevant + if register.startswith("X")), key=lambda name: int(name[1:])) + return { + "source_count": len(reached_sources), + "sources": reached_sources, + "maximum_relevant_registers": maximal_relevant, + "cut_relevance": sorted(cut_relevance, key=lambda row: row["index"]), + } + + +def analyze(witness: dict) -> dict: + """Check a caller-supplied witness; the caller owns source authentication.""" + initial, final, events, metadata = parse_word(witness) + barrier = backwards(initial, final, events, frozenset(CUT_INDICES)) + require(barrier["source_count"] == 0, + "a source-to-target path survives deletion of the eight drops") + intact = backwards(initial, final, events, frozenset()) + require(intact["source_count"] == 104, + "intact information graph lacks some source-to-target paths") + restored = [] + for restored_index in CUT_INDICES: + result = backwards(initial, final, events, + frozenset(set(CUT_INDICES) - {restored_index})) + require(result["source_count"] > 0, + "restoring one drop unexpectedly leaves a separating cut") + restored.append({"restored_edge": restored_index, + "source_count": result["source_count"]}) + return { + "status": "PASS_P104_BACKWARD_TEMPORAL_CUT", + "algorithm": "reverse relevance with explicitly enumerated F2 span classes", + **metadata, + "deleted_transport_indices": list(CUT_INDICES), + "blocked_source_count": barrier["source_count"], + "intact_source_count": intact["source_count"], + "single_restored_edge_controls": restored, + "scope": "Frozen frame chronology, arbitrary scalar mixing within each exact frame class; no supplier or kappa claim.", + } + + +def main() -> None: + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("witness", nargs="?", type=Path, + default=Path(__file__).resolve().parents[1] / + "p104-native-channel" / "inputs" / "LOWRANK-WITNESS.json") + args = parser.parse_args() + payload = args.witness.read_bytes() + require(hashlib.sha256(payload).hexdigest() == WITNESS_SHA256, + "source witness SHA256 mismatch") + result = analyze(json.loads(payload)) + result["witness_sha256"] = WITNESS_SHA256 + print(json.dumps(result, indent=2, sort_keys=True)) + + +if __name__ == "__main__": + main() diff --git a/research/p104-temporal-cut-obstruction/temporal.py b/research/p104-temporal-cut-obstruction/temporal.py new file mode 100644 index 0000000000..8632261adc --- /dev/null +++ b/research/p104-temporal-cut-obstruction/temporal.py @@ -0,0 +1,275 @@ +# SPDX-License-Identifier: Apache-2.0 +"""Saturated information flow through the frozen P104 chronological skeleton. + +The relaxation allows arbitrary linear mixing among *all* live registers in +the same canonical frame at every event boundary. It thus contains every +scalar redesign with the fixed transports and private-register lifetimes. +No channel producer or native compiler is imported. +""" + +from collections import Counter +from fractions import Fraction + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def canonical_frame(vectors): + """Return the actual binary subspace, rejecting a dependent input basis.""" + require(isinstance(vectors, list), "frame basis must be a list") + require(len(vectors) <= 9, "frame exceeds the nine-dimensional label space") + space = {0} + for vector in vectors: + require(type(vector) is int and 0 < vector < 512, + "frame vector must be a nonzero nine-bit integer") + require(vector not in space, "dependent frame basis") + space.update(value ^ vector for value in tuple(space)) + return tuple(sorted(space)) + + +def _normalize(witness): + """Check every literal operation before considering the larger relaxation.""" + require(isinstance(witness, dict), "witness must be an object") + initial = witness["initial_frames"] + final = witness["final_frames"] + program = witness["program"] + require(isinstance(initial, dict) and isinstance(final, dict), + "endpoint frames must be objects") + require(isinstance(program, list), "program must be a list") + expected = ({f"X{i}" for i in range(104)} + | {f"Y{i}" for i in range(104)} + | {f"Q{i}" for i in range(8)} + | {f"G{i}" for i in range(32)} + | {f"D{i}" for i in range(32)}) + require(set(initial) == set(final) == expected, + "P104 requires 104 sources, 104 targets and 72 dirty helpers") + frames = {name: canonical_frame(frame) for name, frame in initial.items()} + start = dict(frames) + finish = {name: canonical_frame(frame) for name, frame in final.items()} + normalized = [] + profile = Counter() + operations = Counter() + lifetime = None + lifetimes = 0 + maximum_live = len(frames) + cut_edges = [] + + for index, event in enumerate(program): + require(isinstance(event, list) and event, f"malformed event {index}") + operation = event[0] + operations[operation] += 1 + if operation == "transport": + require(len(event) == 5, f"transport arity at {index}") + _, name, old, new, rank = event + old_frame = canonical_frame(old) + new_frame = canonical_frame(new) + require(name in frames and frames[name] == old_frame, + f"transport entry frame at {index}") + require(type(rank) is int and rank > 0 + and rank == abs(len(old) - len(new)), + f"positive transport rank at {index}") + require(set(old_frame) <= set(new_frame) + or set(new_frame) <= set(old_frame), + f"transport frames are not nested at {index}") + if name == "C" and len(old) == 8 and len(new) == 1: + require(lifetime is not None and lifetime["copied"] + and not lifetime["dropped"], + f"private descent lifetime at {index}") + lifetime["dropped"] = True + cut_edges.append(index) + frames[name] = new_frame + profile[rank] += 1 + normalized.append((operation, name, old_frame, new_frame, rank)) + elif operation == "zero": + require(len(event) == 3, f"zero arity at {index}") + _, name, frame = event + common = canonical_frame(frame) + require(name == "C" and name not in frames and lifetime is None, + f"owned private allocation at {index}") + frames[name] = common + lifetime = {"copied": False, "dropped": False, "clean": True} + lifetimes += 1 + maximum_live = max(maximum_live, len(frames)) + normalized.append((operation, name, common)) + elif operation == "erase": + require(len(event) == 3, f"erase arity at {index}") + _, name, frame = event + common = canonical_frame(frame) + require(name == "C" and name in frames and frames[name] == common + and lifetime is not None and lifetime["copied"] + and lifetime["dropped"], + f"owned private discard at {index}") + del frames[name] + lifetime = None + normalized.append((operation, name, common)) + elif operation == "copy": + require(len(event) == 4, f"copy arity at {index}") + _, target, source, frame = event + common = canonical_frame(frame) + require(target == "C" and target != source and source in frames + and target in frames + and frames[target] == frames[source] == common + and lifetime is not None and lifetime["clean"] + and not lifetime["copied"], + f"owned common-frame copy at {index}") + lifetime["copied"] = True + lifetime["clean"] = False + normalized.append((operation, target, source, common)) + elif operation == "add": + require(len(event) == 5, f"add arity at {index}") + _, target, source, coefficient, frame = event + common = canonical_frame(frame) + require(target != source and target in frames and source in frames + and frames[target] == frames[source] == common, + f"common-frame addition at {index}") + try: + value = Fraction(coefficient) + except (TypeError, ValueError, ZeroDivisionError) as error: + raise ValueError(f"invalid rational coefficient at {index}") from error + if target == "C" and value: + lifetime["clean"] = False + normalized.append((operation, target, source, value, common)) + else: + raise ValueError(f"unknown operation at {index}: {operation}") + + require(lifetime is None and frames == finish, "final frame/lifetime mismatch") + require(lifetimes == 8 and len(cut_edges) == 8, + "expected eight separate rank-seven private descents") + return start, finish, normalized, cut_edges, { + "event_count": len(program), + "event_boundary_count": len(program) + 1, + "initial_register_count": len(start), + "maximum_live_register_count": maximum_live, + "private_lifetime_count": lifetimes, + "operation_counts": dict(sorted(operations.items())), + "paid_profile": {str(rank): count for rank, count in sorted(profile.items())}, + "rank_mass": sum(rank * count for rank, count in profile.items()), + } + + +def _saturate(frames, information): + """Allow unrestricted common-chart mixing, including feedback within a cut.""" + groups = {} + for name, frame in frames.items(): + groups.setdefault(frame, []).append(name) + for names in groups.values(): + union = 0 + for name in names: + union |= information[name] + for name in names: + information[name] = union + return len(groups) + + +def _forward(initial, events, deleted): + frames = dict(initial) + information = {name: (1 << int(name[1:]) if name.startswith("X") else 0) + for name in frames} + counts = {} + ever_targets = set() + groups_visited = 0 + + def close(): + nonlocal groups_visited + groups_visited += _saturate(frames, information) + ever_targets.update(name for name in frames + if name.startswith("Y") and information[name]) + + close() + for index, event in enumerate(events): + operation, name = event[:2] + if operation == "transport": + if index in deleted: + counts[index] = information[name].bit_count() + information[name] = 0 + frames[name] = event[3] + elif operation == "zero": + frames[name] = event[2] + information[name] = 0 + elif operation == "erase": + del frames[name] + del information[name] + # Literal add/copy edges are already contained in saturated common-frame + # access. Retaining all input dependencies makes this an upper bound. + close() + return information, counts, sorted(ever_targets), groups_visited + + +def _backward(final, events, deleted): + frames = dict(final) + information = {name: (1 << int(name[1:]) if name.startswith("Y") else 0) + for name in frames} + counts = {} + ever_sources = set() + groups_visited = 0 + + def close(): + nonlocal groups_visited + groups_visited += _saturate(frames, information) + ever_sources.update(name for name in frames + if name.startswith("X") and information[name]) + + close() + for index in range(len(events) - 1, -1, -1): + event = events[index] + operation, name = event[:2] + if operation == "transport": + if index in deleted: + counts[index] = information[name].bit_count() + information[name] = 0 + frames[name] = event[2] + elif operation == "zero": + del frames[name] + del information[name] + elif operation == "erase": + frames[name] = event[2] + information[name] = 0 + close() + return information, counts, sorted(ever_sources), groups_visited + + +def analyze(witness): + """Return a deterministic exact receipt for the eight-edge temporal cut.""" + initial, final, events, cut_edges, totals = _normalize(witness) + deleted = set(cut_edges) + forward, incoming, ever_targets, forward_groups = _forward(initial, events, deleted) + backward, outgoing, ever_sources, backward_groups = _backward(final, events, deleted) + reached_targets = sorted(name for name in final + if name.startswith("Y") and forward[name]) + reached_sources = sorted(name for name in initial + if name.startswith("X") and backward[name]) + require(not reached_targets, "deleted edges do not cut every source-to-target path") + require(not reached_sources, "backward replay found a source-to-target bypass") + require(forward_groups == backward_groups, "forward/backward frame census differs") + return { + "status": "PASS_P104_FROZEN_TEMPORAL_EIGHT_EDGE_CUT", + **totals, + "source_count": 104, + "target_count": 104, + "dirty_helper_count": 72, + "common_frame_groups_saturated": forward_groups, + "deleted_edge_count": len(cut_edges), + "deleted_edges": [ + { + "event_index": index, + "register": events[index][1], + "old_dimension": 8, + "new_dimension": 1, + "native_rank": events[index][4], + "reachable_source_inputs_before_deletion": incoming[index], + "reachable_target_outputs_after_deletion": outgoing[index], + } + for index in cut_edges + ], + "forward_reachable_final_targets": reached_targets, + "backward_reachable_initial_sources": reached_sources, + "forward_ever_reachable_targets": ever_targets, + "backward_ever_reachable_sources": ever_sources, + "source_to_target_coefficient_rank_upper_bound": len(cut_edges), + "relaxation": ( + "Arbitrary common-frame linear mixing among all live registers at every " + "event boundary; the native transport sequence and private lifetimes are fixed." + ), + } diff --git a/research/p104-temporal-cut-obstruction/verify.py b/research/p104-temporal-cut-obstruction/verify.py new file mode 100644 index 0000000000..2a5f01be35 --- /dev/null +++ b/research/p104-temporal-cut-obstruction/verify.py @@ -0,0 +1,263 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Exact read-only P104 temporal-cut certificate and adverse controls. + +Only the standard library is used. No predecessor producer, native compiler, +network access, Git command, or floating-point acceptance test is used. +""" +from __future__ import annotations + +import argparse +import copy +from fractions import Fraction as Q +import hashlib +import importlib.util +from itertools import combinations, product +import json +from pathlib import Path + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parents[1] +WITNESS = "research/p104-native-channel/inputs/LOWRANK-WITNESS.json" +FIXTURE = "research/p104-native-channel/inputs/P104-FIXTURE.json" + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def module(name): + spec = importlib.util.spec_from_file_location(name, PACKAGE / (name + ".py")) + loaded = importlib.util.module_from_spec(spec) + spec.loader.exec_module(loaded) + return loaded + + +def check_sources(): + sources = json.loads((PACKAGE / "SOURCES.json").read_text()) + for item in sources["files"]: + if item["usage"] == "input": + digest = hashlib.sha256((ROOT / item["path"]).read_bytes()).hexdigest() + require(digest == item["sha256"], "source changed: " + item["path"]) + + +def gram_certificate(fixture): + """Reconstruct roots, tight-frame identity, correction inverse, witnesses.""" + roots = set() + for i, j in combinations(range(8), 2): + for sign in (-1, 1): + row = [0] * 8 + row[i], row[j] = 2, 2 * sign + roots.add(tuple(row)) + for signs in product((-1, 1), repeat=7): + if signs.count(-1) % 2 == 0: + roots.add((1, *signs)) + require(len(roots) == 120, "E8 root-line count") + removed = {tuple(row) for row in fixture["F0"] + fixture["C"]} + require(len(removed) == 16 and removed <= roots, "two deleted frames") + ports = sorted(roots - removed) + require(len(ports) == 104, "P104 port count") + for i in range(8): + for j in range(8): + require(sum(row[i] * row[j] for row in ports) == 104 * (i == j), + "doubled coordinate tight-frame identity") + dots = [[sum(a * b for a, b in zip(x, y)) for y in ports] for x in ports] + require(all(value % 4 == 0 for row in dots for value in row), "integral Gram") + gram = [[value // 4 for value in row] for row in dots] + # A^t A = 26 I proves rank(G)=8 without numerical rank thresholds. + for i in range(104): + for j in range(104): + square = sum(gram[i][k] * gram[k][j] for k in range(104)) + require(square == 26 * gram[i][j], "G squared equals 26 G") + # Clear denominators in (I-G/2)(I-G/24)=I. + require(48 * (i == j) - 26 * gram[i][j] + square == 48 * (i == j), + "correction inverse") + for t in range(104): + z = [26 * (s == t) - gram[s][t] for s in range(104)] + require(all(sum(row[s] * z[s] for s in range(104)) == 0 for row in gram), + "lost source direction") + require(z[t] == 24, "visible correction witness") + return gram, { + "ports": 104, "gram_rank": 8, "gram_square_multiplier": 26, + "correction_rank": 104, "correction_inverse": "I-G/24", + "kernel_witnesses": 104, + "nonzero_correction_entries": sum(i != j and gram[i][j] != 0 + for i in range(104) for j in range(104)), + } + + +def replay_scalar(witness, gram): + """Independent sparse rational replay over every arbitrary dirty input.""" + initial = witness["initial_frames"] + rows = {reg: {reg: Q(1)} for reg in initial} + counts = {} + for event in witness["program"]: + op = event[0] + counts[op] = counts.get(op, 0) + 1 + if op == "transport": + continue + if op == "zero": + require(event[1] not in rows, "private lifetime overlaps") + rows[event[1]] = {} + elif op == "erase": + require(event[1] == "C" and event[1] in rows, "private erasure") + del rows[event[1]] + elif op == "copy": + _, dest, source, _ = event + require(not rows[dest], "copy into nonzero logical register") + rows[dest] = dict(rows[source]) + elif op == "add": + _, dest, source, coefficient, _ = event + require(dest != source, "self addition outside original word") + for key, value in list(rows[source].items()): + result = rows[dest].get(key, Q(0)) + Q(coefficient) * value + if result: + rows[dest][key] = result + else: + rows[dest].pop(key, None) + else: + raise ValueError("unknown scalar event") + require(set(rows) == set(initial), "unclosed private lifetime") + for reg in rows: + expected = {reg: Q(1)} + if reg.startswith("Y"): + t = int(reg[1:]) + expected.update({"X" + str(s): Q(value, 2) + for s, value in enumerate(gram[t]) if value}) + require(rows[reg] == expected, "scalar endpoint " + reg) + return {"arbitrary_input_columns": len(initial), "events": counts, + "dirty_helpers_restored": sum(reg[0] in "GDQ" for reg in initial)} + + +def budget_certificate(): + """Conditional retained-template accounting; no numerical root finding.""" + width, families, calls, centre, missing = 73, 832, 9, 56, 104 - 8 + baseline = (width - 1) * families + calls * centre + capacity = width * families + minimum = baseline + calls * missing + require(baseline < capacity < minimum, "added excess must decide the sign") + return { + "model": "checkpoint-preserving insertions; retained fully hosted nine-stage four-pair coverage", + "width": width, "families": families, "calls": calls, + "private_copy_rank_per_call": centre, + "baseline_paid_mass": baseline, "capacity": capacity, + "baseline_headroom_per_call": str(Q(capacity - baseline, calls)), + "minimum_added_transport_occurrences_per_call": missing, + "minimum_completed_paid_mass": minimum, + "zero_saving_moment_lower_bound": str(Q(minimum, capacity)), + "minimum_moment_excess": str(Q(minimum - capacity, capacity)), + "example_208_added_rank_moment_at_zero": str(Q(baseline + calls * 208, capacity)), + "positive_saving_possible_in_this_model": False, + "omitted_extra_charge_positive_control": str(Q(baseline, capacity)), + } + + +def rejects(function, label, expected_reason): + try: + function() + except ValueError as error: + require(expected_reason in str(error), "wrong rejection reason for " + label) + return label + raise ValueError("control accepted: " + label) + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--write", action="store_true", help="regenerate this package's RESULT.json") + args = parser.parse_args() + check_sources() + witness = json.loads((ROOT / WITNESS).read_text()) + fixture = json.loads((ROOT / FIXTURE).read_text())["section4_explicit_P104"] + gram, algebra = gram_certificate(fixture) + scalar = replay_scalar(witness, gram) + forward = module("temporal") + backward = module("backward") + fwd = forward.analyze(witness) + rev = backward.analyze(witness) + require([edge["event_index"] for edge in fwd["deleted_edges"]] + == rev["deleted_transport_indices"], "independent cut agreement") + require(fwd["paid_profile"] == rev["transport_profile"], "independent invoice agreement") + require(fwd["source_count"] == fwd["target_count"] == algebra["ports"] == 104, + "algebra and temporal boundary inventory disagree") + require(fwd["event_count"] == rev["event_count"] == 4058 + and fwd["event_boundary_count"] == 4059, + "complete frozen event-boundary coverage") + require(fwd["deleted_edge_count"] == algebra["gram_rank"] == 8, + "cut capacity and attained rank disagree") + require(all(edge["reachable_source_inputs_before_deletion"] == 52 + and edge["reachable_target_outputs_after_deletion"] == 52 + for edge in fwd["deleted_edges"]), + "private cut source/target support census") + result = { + "status": "PASS_P104_TEMPORAL_CUT_OBSTRUCTION", + "algebra": algebra, "scalar_positive_control": scalar, + "forward": fwd, "backward": rev, + "conditional_budget": budget_certificate(), "controls": [], + "scope": "Sharp rank-eight obstruction for the frozen chronological common-frame access graph; conditional no-saving result for checkpoint-preserving paid transport insertions. No general P104 impossibility, supplier admission or new kappa.", + } + bad = copy.deepcopy(witness) + bad["program"][0][3] = "0" + result["controls"].append(rejects(lambda: replay_scalar(bad, gram), "missing_dirty_compensation", "scalar endpoint Y0")) + bad_frame = copy.deepcopy(witness) + event = next(e for e in bad_frame["program"] if e[0] == "transport") + event[4] += 1 + result["controls"].append(rejects(lambda: forward.analyze(bad_frame), "incorrect_transport_rank", "positive transport rank")) + dependent = copy.deepcopy(witness) + event = next(e for e in dependent["program"] + if e[0] == "transport" and len(e[2]) >= 2) + event[2][1] = event[2][0] + result["controls"].append(rejects( + lambda: forward.analyze(dependent), "dependent_frame_basis", + "dependent frame basis")) + wrong_gate_frame = copy.deepcopy(witness) + event = next(e for e in wrong_gate_frame["program"] + if e[0] == "add" and e[4] == []) + event[4] = [1] + result["controls"].append(rejects( + lambda: forward.analyze(wrong_gate_frame), "incorrect_common_gate_frame", + "common-frame addition")) + wrong_erasure = copy.deepcopy(witness) + event = next(e for e in wrong_erasure["program"] if e[0] == "erase") + event[1] = "Q0" + result["controls"].append(rejects( + lambda: forward.analyze(wrong_erasure), "erasure_outside_owned_private_role", + "owned private discard")) + reordered = copy.deepcopy(witness) + for endpoint in ("initial_frames", "final_frames"): + for basis in reordered[endpoint].values(): + basis.reverse() + for event in reordered["program"]: + for field in event[2:]: + if isinstance(field, list): + field.reverse() + require(reordered != witness, "basis-order positive control made no change") + require(forward.analyze(reordered) == fwd, + "forward certificate depends on listed frame basis order") + require(backward.analyze(reordered) == rev, + "independent reverse certificate depends on listed frame basis order") + result["controls"].append("all_frame_basis_orders_reversed_same_certificate") + bad_gram = copy.deepcopy(gram) + bad_gram[0][0] = 0 + result["controls"].append(rejects(lambda: replay_scalar(witness, bad_gram), "incorrect_claimed_endpoint", "scalar endpoint Y0")) + bypass = copy.deepcopy(witness) + frame = list(witness["initial_frames"]["X0"]) + bypass["program"][:0] = [ + ["transport", "Y0", [], frame, 1], + ["add", "Y0", "X0", 1, frame], + ["transport", "Y0", frame, [], 1], + ] + result["controls"].append(rejects( + lambda: forward.analyze(bypass), "new_paid_bridge_invalidates_old_cut", + "deleted edges do not cut every source-to-target path")) + payload = json.dumps(result, sort_keys=True, indent=2) + "\n" + path = PACKAGE / "RESULT.json" + if args.write: + path.write_text(payload) + else: + require(json.loads(path.read_text()) == result, "complete certificate differs; review changes") + print(payload, end="") + + +if __name__ == "__main__": + main()