From eeb4ae73ff0d6b049fb72608074be78d623cb51d Mon Sep 17 00:00:00 2001 From: Chris R Date: Mon, 19 Oct 2026 18:11:12 +1100 Subject: [PATCH] research: audit P104 private-copy lifetimes and price direct query replacement --- research/p104-copy-retirement/PROOF.md | 139 ++++ research/p104-copy-retirement/README.md | 84 +++ research/p104-copy-retirement/RESULT.json | 696 ++++++++++++++++++ .../p104-copy-retirement/RETURN-RECIPES.json | 642 ++++++++++++++++ research/p104-copy-retirement/SOURCES.json | 58 ++ research/p104-copy-retirement/TASK.json | 88 +++ research/p104-copy-retirement/VERIFY.json | 62 ++ .../inputs/pr3882_verify.py | 291 ++++++++ research/p104-copy-retirement/native.py | 58 ++ .../p104-copy-retirement/test_controls.py | 39 + research/p104-copy-retirement/verify.py | 188 +++++ 11 files changed, 2345 insertions(+) create mode 100644 research/p104-copy-retirement/PROOF.md create mode 100644 research/p104-copy-retirement/README.md create mode 100644 research/p104-copy-retirement/RESULT.json create mode 100644 research/p104-copy-retirement/RETURN-RECIPES.json create mode 100644 research/p104-copy-retirement/SOURCES.json create mode 100644 research/p104-copy-retirement/TASK.json create mode 100644 research/p104-copy-retirement/VERIFY.json create mode 100644 research/p104-copy-retirement/inputs/pr3882_verify.py create mode 100644 research/p104-copy-retirement/native.py create mode 100644 research/p104-copy-retirement/test_controls.py create mode 100644 research/p104-copy-retirement/verify.py diff --git a/research/p104-copy-retirement/PROOF.md b/research/p104-copy-retirement/PROOF.md new file mode 100644 index 0000000000..3026729cac --- /dev/null +++ b/research/p104-copy-retirement/PROOF.md @@ -0,0 +1,139 @@ +# Literal private-copy lifetimes and a paid replacement + +All indices below are zero-based in the pinned 4,058-event PR1972 word retained +by PR1991. This is a fixed-word ownership and changed-local-route result. +It is not a universal lower bound on P104 copies, encoders or suppliers. + +## The actual eight lifetimes + +Let q_j be the exact normalized row in Q_j when it is copied. Sparse rational +induction from all 280 independent inputs gives + + q_j = h_Qj + sum_i a_ji x_i, + +with coefficient 1 on h_Qj, coefficient 0 on all other dirty inputs, and the +source coefficients recorded in RESULT.json. No zero-input assumption is used. +The original source gather produces these rows; they are not an assumed query. + +| Query | C initialization | Copy | Rank-seven descent | Last C read | C erase | Delivery helpers | +|---|---:|---:|---:|---:|---:|---| +| Q0 | 2461 | 2462 | 2463 | 2468 | 2469 | D0–D4 | +| Q1 | 2470 | 2471 | 2472 | 2475 | 2476 | D5–D7 | +| Q2 | 2477 | 2478 | 2479 | 2483 | 2484 | D8–D11 | +| Q3 | 2485 | 2486 | 2487 | 2491 | 2492 | D12–D15 | +| Q4 | 2493 | 2494 | 2495 | 2499 | 2500 | D16–D19 | +| Q5 | 2501 | 2502 | 2503 | 2506 | 2507 | D20–D22 | +| Q6 | 2508 | 2509 | 2510 | 2514 | 2515 | D23–D26 | +| Q7 | 2516 | 2517 | 2518 | 2523 | 2524 | D27–D31 | + +Each private C starts at zero in the same eight-dimensional chart W_j as Q_j. +Copying sets its normalized row to q_j. The literal transport takes C to a +one-dimensional chart L_j contained in W_j; every reader is an addition +D_k += C in that L_j chart. The private row remains q_j until erase. Since its +h_Qj coefficient is 1, it is not zero. The inherited owned-private erase +semantics permit discarding C; this does not permit discarding a public dirty +Q_j or D_k. Only one C is live at a time, and none is live after event 2524. +There is therefore no surviving C role at the completed #3882 boundary whose +future lifetime can be silently credited as retirement of the paid descent. + +The 32 D helpers are actual consumers, not hypothetical available banks. +RESULT.json records their first downstream reads and their cleanup events +3579, 3581, ..., 3641. The cleanup subtracts the corresponding q_j after both +roles reach FULL. Q_j itself remains unchanged from copying until its FULL +transport at 3570+j, and is restored by the final source cleanup. + +## Removing delivery is observable downstream + +Remove all eight private intervals while retaining every public event. +At each D_k in the j-th group, the missing addition leaves normalized defect +−q_j. The later public program is linear. The exact complete replay shows: + +* X, Q and G final rows are unchanged; +* all 32 D returns have defect −q_j; +* the target defect and the complete public defect each have rational rank 8. + +The eight independent h_Qj columns already attain rank 8. In particular, take +one h_Qj arbitrary and every other logical input zero. This is an explicit +permitted dirty input, not a probability or generic-rank argument. + +Continue both original and mutilated words through the actual pinned #3882 +schedule. That schedule acts only on X/Y and is invertible in normalized rows. +Our new evaluator uses its unchanged geometry/program builders but not its +arithmetic evaluator. The 104 physical sum slots (Y_J, X_N) still have defect +rank 8. All 32 D defects survive unchanged because the tail never touches D. +Thus correct sums and dirty returns cannot be obtained by simply deleting the +copies or their 32 uses. This is not a proof against changing the producer, +consumer, other delivery operations or output contract. + +## A concrete copy-free local replacement + +Write T_j = Gamma_Lj Gamma_Wj^{-1}. Replace each private interval by: + +1. apply T_j directly to Q_j; +2. perform the same D_k += Q_j additions in L_j; +3. apply T_j^{-1} to Q_j. + +At the entrance let the physical query be Gamma_Wj q_j and each D value be +Gamma_Lj d_k. The exact endpoint is + + Q_j -> Gamma_Wj q_j, + D_k -> Gamma_Lj (d_k + q_j). + +Every other role is untouched. This equals the original private-copy block on +all arbitrary inputs. Eight block substitutions consequently preserve the full +280-row channel endpoint and the actual #3882 continuation. There are no +private zero/copy/erase events, and no dirty role is erased. The maximum local +register count drops from 281 to 280; this is a local workspace observation, +not a global width or recursive saving. + +The source certificate supplies the forward native recipes. RETURN-RECIPES.json +contains eight newly lowered reverse recipes. native.py independently checks +the physical label mapping at each literal event, exact signed Clifford action, +global phase, both rank-seven child charges, 8,192 Gaussian columns (512 in each +direction for each block), and the identity T_j^{-1} T_j. It rejects a changed +global phase. It reuses the credited exact compiler/interpreter and does not +repeat the complete inherited channel's native proof. + +## The price and its scope + +The original eight private descents cost 8*7 = 56 rank mass. The replacement +uses eight descents and eight returns, costing 112. The query-freeing saving +is eight zero operations, eight copies, eight private erases and one peak +local array; the positive recursive-child bill increases by 56. + +For the restricted direct-Q route, this rank cost is sharp under the retained +nested transport tariff. A path from dimension 8 through dimension 1 and back +to dimension 8 has sum of absolute dimension jumps at least 7+7. The two direct +transports attain that bound. If restoration is delayed until the existing +FULL consumer, the 8 -> 1 -> 9 path costs at least 15, versus the original +private drop 7 plus Q's existing 8 -> 9 lift 1, again seven extra. This bound +fixes the same delivery chart, same Q owner and same later public consumers. +It excludes replacement encodings, coupled roles, altered production or new +non-nested/native primitives. + +| Complete local bill | Original channel | Copy-free replacement | +|---|---:|---:| +| Native profile, ranks 1 through 8 | 1074,58,86,104,48,24,8,8 | 1074,58,86,104,48,24,16,8 | +| Rank mass | 2368 | 2424 | +| Scalar array additions | 2624 | 2624 | +| Native transport occurrences | 1410 | 1418 | +| zero / copy / erase | 8 / 8 / 8 | 0 / 0 / 0 | +| Total events | 4058 | 4042 | +| With the unchanged #3882 208-H1 tail | 2576 | 2632 | + +The positive-child counts include all eight returns. Their actual Gaussian +monomial wrappers are retained in the recipe file, not treated as positive +recursive children. We do not claim a runtime saving: wrapper execution, +precision, signed-floor behavior, memory/routing/control and all-size admission +remain separate obligations. Unknown physical costs are not assigned zero. + +As a conditional substitution into #3954's stated 208-call, m=81, W=36608 +scaffold and the same persistent-progress allowance, its already failing +M_0 numerator excess grows from 44096 to 55744. Granting all 208 correction +rank units per local call for free would leave 832 excess for the original +COPY56 channel and 12480 for this replacement. These are scoped favorable +relaxations, not an actual two-axis construction or a general P104 barrier. +For 0 <= a < 1, (r/81)^(1-a) >= r/81, so failure at zero also fails every such +moment under those same hypotheses. The replacement does not justify another +dependent construction round. A new route must eliminate real work with a +changed producer/consumer or coverage contract and price every obligation. diff --git a/research/p104-copy-retirement/README.md b/research/p104-copy-retirement/README.md new file mode 100644 index 0000000000..07d692d531 --- /dev/null +++ b/research/p104-copy-retirement/README.md @@ -0,0 +1,84 @@ +# P104 private-copy lifetime and retirement audit + +The eight inherited COPY lifetimes are live deliveries of arbitrary dirty +queries. Deleting them breaks all 32 delivery-helper returns and leaves a +rank-eight defect in the actual #3882 sum outputs. A concrete copy-free +replacement restores every public input/output and removes one peak local +private array, but costs **56 extra native rank units**. It cannot repair the +failed #3954 two-axis budget. + +This source-bound result adds the exact lifetime/consumer map, deletion +counterexamples, a fully priced direct-query replacement, and eight phase-exact +native return recipes. It does not rediscover or generalize the old COPY56 +floor. The lower bound is restricted to taking the same Q role through the +same delivery chart and returning it to its fixed later consumer. + +See [PROOF.md](PROOF.md), [RESULT.json](RESULT.json) and +[RETURN-RECIPES.json](RETURN-RECIPES.json). All 280 independent logical rows and +72 arbitrary dirty helpers are explicit. The normal and optimized Python +checks require only Python 3.12's standard library: + +```sh +python3.12 -B scripts/research_package.py --package research/p104-copy-retirement +python3.12 -B scripts/check_research_commit.py --package research/p104-copy-retirement --check-source-history +``` + +The first command checks exact scalar/frame composition, the unchanged actual +#3882 tail, and the eight local native reverses on all 512 Gaussian columns in +each direction, with ownership/frame/rank/global-phase controls and seven actual optimized CLI +rejection fixtures for malformed receipts and changed/missing sources. It does not +repeat the full inherited native channel, signed-floor or supplier proof. +RETURN-RECIPES.json can be independently regenerated with +`python3.12 -B research/p104-copy-retirement/native.py --generate`; ordinary +verification is read-only. The compiler and independent native interpreter +remain separate retained predecessor implementations; they are not new here. + +`SOURCES.json` pins canonical inputs at main +`20ecf2891d80b5acf18d980b2164fb44ea7faa90`, priority revision 6. The exact PR3882 +schedule builder is a self-contained unchanged source export with its original +head/path/hash; cold replay does not require an unmerged Git object. Its builder +is reused, while the row evaluator and ownership audit are new. Original task +card and bounded changed scope are retained in `TASK.json`. + +## Scope and remaining obligations + +The replacement is a finite local native rewrite with the inherited endpoint +contract. No new kappa, source-preserving correction improvement, scalar +optimum, universal copy lower bound, actual global owner map, opposite-orientation +supplier or selected-frontier change is claimed. General resynthesis may change +these conclusions by changing their stated contract. The conditional #3954 +arithmetic is a losing complete-cost relaxation, not supplier admission. + +Entry overlap used all 662 open PR bodies including drafts over seven pages, +a bounded read of current Discussions by the coordinating agent, and the +repository helper. The helper had no Discussion cache and sparse local notes; +this is not proof of novelty. PR3956 already completes the 960-versus-1152 ADD +comparison, which this package does not repeat. Sibling adjacent-encoding and +coverage audits are separate scopes. + +## Open next questions + +Can one concrete changed delivery consumer avoid the Q descent/return pair +while still restoring every actual dirty D helper? This matters because the +source-bound copy-free replacement worsens the recursive invoice. First derive +one replacement block on all Q/D inputs and its physical charts, then test a +complete cost gate before expanding it. Fixed lifetime deletion and direct-Q +retiming are closed only within the restricted contracts above. A changed +encoding, producer or coverage obligation is required to reopen this route. + +## Credit + +Rohan Arun / PR1972 owns the complete dirty-restored gather, query production, +COPY56 word and cleanup. Chafik Boukhalfa / PR1991 owns its concrete finite +native realization and complete channel induction. Adam Gall / PR1940 supplies +the retained 32-chain delivery schedule. Chris R / Clear1nsight owns PR3882's +source-consuming correction and PR3940/PR3943/PR3954 caller work; PR3956's +matched return comparison is credited to ToikY. Josie Elliston's E8 fixture, +Sagar Thakrar, Douglas Colkitt, Dominik Scholz, the retained Clifford compiler +(icekylinx PR531 and its lineage), and PR1862's independent interpreter retain +their source attribution. Existing notices in p104-native-channel are unchanged. + +New lifetime audit, local rewrite, eight return recipes and tests prepared for +Chris R / Clear1nsight with substantial OpenAI Codex assistance, including a +separate coordinating-agent dirty-column check. No independent human or formal +proof-assistant review is claimed. Apache-2.0. diff --git a/research/p104-copy-retirement/RESULT.json b/research/p104-copy-retirement/RESULT.json new file mode 100644 index 0000000000..537b013734 --- /dev/null +++ b/research/p104-copy-retirement/RESULT.json @@ -0,0 +1,696 @@ +{ + "arbitrary_dirty_inputs": 72, + "baseline_mass": 2368, + "baseline_profile": { + "1": 1074, + "2": 58, + "3": 86, + "4": 104, + "5": 48, + "6": 24, + "7": 8, + "8": 8 + }, + "broken_dirty_returns_on_deletion": 32, + "combined_3882_mass": 2576, + "deletion_defect_rank": 8, + "deletion_sum_defect_rank_after_actual_3882_tail": 8, + "direct_query_combined_mass": 2632, + "events_after": 4042, + "events_before": 4058, + "lifetime_records": [ + { + "copy": 2462, + "delivery_helpers": [ + "D0", + "D1", + "D2", + "D3", + "D4" + ], + "drop": 2463, + "erase": 2469, + "first_downstream_reads": { + "D0": 2746, + "D1": 2780, + "D2": 3168, + "D3": 3176, + "D4": 2860 + }, + "fixed_cleanup_events": { + "D0": 3579, + "D1": 3581, + "D2": 3583, + "D3": 3585, + "D4": 3587 + }, + "last_read": 2468, + "nonzero_private_at_erase": true, + "query": "Q0", + "query_source_coefficients": { + "X0": "-2", + "X1": "-2", + "X100": "-2", + "X11": "2", + "X12": "-2", + "X15": "2", + "X16": "-2", + "X19": "2", + "X20": "-2", + "X24": "2", + "X25": "-2", + "X28": "2", + "X29": "-2", + "X3": "-2", + "X33": "2", + "X34": "-2", + "X37": "2", + "X38": "-2", + "X41": "2", + "X42": "-2", + "X45": "2", + "X46": "-2", + "X48": "2", + "X49": "-2", + "X52": "2", + "X53": "-2", + "X56": "2", + "X57": "-2", + "X6": "2", + "X60": "2", + "X61": "-2", + "X64": "2", + "X65": "-2", + "X68": "2", + "X69": "-2", + "X7": "2", + "X72": "2", + "X73": "-2", + "X76": "2", + "X77": "-2", + "X8": "-2", + "X80": "2", + "X81": "-2", + "X83": "2", + "X84": "-2", + "X87": "2", + "X88": "-2", + "X90": "2", + "X91": "-2", + "X96": "2", + "X97": "-2", + "X99": "2" + }, + "zero": 2461 + }, + { + "copy": 2471, + "delivery_helpers": [ + "D5", + "D6", + "D7" + ], + "drop": 2472, + "erase": 2476, + "first_downstream_reads": { + "D5": 2526, + "D6": 2763, + "D7": 3106 + }, + "fixed_cleanup_events": { + "D5": 3589, + "D6": 3591, + "D7": 3593 + }, + "last_read": 2475, + "nonzero_private_at_erase": true, + "query": "Q1", + "query_source_coefficients": { + "X10": "2", + "X101": "-2", + "X102": "2", + "X11": "2", + "X12": "2", + "X14": "2", + "X21": "-2", + "X22": "-2", + "X23": "2", + "X3": "-2", + "X30": "-2", + "X31": "2", + "X36": "-2", + "X37": "-2", + "X38": "-2", + "X39": "-2", + "X4": "-2", + "X40": "2", + "X41": "2", + "X42": "2", + "X43": "2", + "X5": "-2", + "X51": "-2", + "X52": "-2", + "X53": "-2", + "X54": "-2", + "X55": "2", + "X56": "2", + "X57": "2", + "X58": "2", + "X6": "-2", + "X67": "-2", + "X68": "-2", + "X69": "-2", + "X7": "2", + "X70": "-2", + "X71": "2", + "X72": "2", + "X73": "2", + "X74": "2", + "X8": "2", + "X82": "-2", + "X83": "-2", + "X84": "-2", + "X85": "-2", + "X86": "2", + "X87": "2", + "X88": "2", + "X89": "2", + "X9": "2", + "X94": "-2", + "X95": "2" + }, + "zero": 2470 + }, + { + "copy": 2478, + "delivery_helpers": [ + "D8", + "D9", + "D10", + "D11" + ], + "drop": 2479, + "erase": 2484, + "first_downstream_reads": { + "D10": 2824, + "D11": 3117, + "D8": 2552, + "D9": 2976 + }, + "fixed_cleanup_events": { + "D10": 3599, + "D11": 3601, + "D8": 3595, + "D9": 3597 + }, + "last_read": 2483, + "nonzero_private_at_erase": true, + "query": "Q2", + "query_source_coefficients": { + "X10": "2", + "X102": "2", + "X103": "-2", + "X11": "2", + "X12": "2", + "X13": "2", + "X14": "-2", + "X15": "-2", + "X16": "-2", + "X17": "-2", + "X18": "-2", + "X19": "-2", + "X20": "-2", + "X21": "-2", + "X22": "-2", + "X31": "2", + "X32": "-2", + "X40": "2", + "X41": "2", + "X42": "2", + "X43": "2", + "X44": "2", + "X45": "2", + "X46": "2", + "X47": "-2", + "X48": "-2", + "X49": "-2", + "X50": "-2", + "X51": "-2", + "X52": "-2", + "X53": "-2", + "X54": "-2", + "X7": "2", + "X71": "2", + "X72": "2", + "X73": "2", + "X74": "2", + "X75": "2", + "X76": "2", + "X77": "2", + "X78": "2", + "X79": "-2", + "X8": "2", + "X80": "-2", + "X81": "-2", + "X82": "-2", + "X83": "-2", + "X84": "-2", + "X85": "-2", + "X9": "2", + "X93": "2", + "X94": "-2" + }, + "zero": 2477 + }, + { + "copy": 2486, + "delivery_helpers": [ + "D12", + "D13", + "D14", + "D15" + ], + "drop": 2487, + "erase": 2492, + "first_downstream_reads": { + "D12": 2572, + "D13": 2992, + "D14": 2849, + "D15": 3083 + }, + "fixed_cleanup_events": { + "D12": 3603, + "D13": 3605, + "D14": 3607, + "D15": 3609 + }, + "last_read": 2491, + "nonzero_private_at_erase": true, + "query": "Q3", + "query_source_coefficients": { + "X0": "-2", + "X1": "-2", + "X100": "-2", + "X101": "-2", + "X12": "-2", + "X13": "-2", + "X14": "2", + "X15": "2", + "X2": "-2", + "X20": "-2", + "X21": "-2", + "X23": "2", + "X24": "2", + "X29": "-2", + "X3": "-2", + "X30": "-2", + "X33": "2", + "X38": "-2", + "X39": "-2", + "X4": "-2", + "X40": "2", + "X41": "2", + "X46": "-2", + "X47": "2", + "X48": "2", + "X5": "-2", + "X53": "-2", + "X54": "-2", + "X55": "2", + "X56": "2", + "X6": "-2", + "X61": "-2", + "X62": "-2", + "X63": "2", + "X64": "2", + "X69": "-2", + "X7": "2", + "X70": "-2", + "X71": "2", + "X72": "2", + "X77": "-2", + "X78": "-2", + "X79": "2", + "X80": "2", + "X84": "-2", + "X85": "-2", + "X86": "2", + "X87": "2", + "X91": "-2", + "X92": "-2", + "X95": "2", + "X96": "2" + }, + "zero": 2485 + }, + { + "copy": 2494, + "delivery_helpers": [ + "D16", + "D17", + "D18", + "D19" + ], + "drop": 2495, + "erase": 2500, + "first_downstream_reads": { + "D16": 2604, + "D17": 2797, + "D18": 2983, + "D19": 3315 + }, + "fixed_cleanup_events": { + "D16": 3611, + "D17": 3613, + "D18": 3615, + "D19": 3617 + }, + "last_read": 2499, + "nonzero_private_at_erase": true, + "query": "Q4", + "query_source_coefficients": { + "X0": "-2", + "X1": "-2", + "X100": "-2", + "X101": "2", + "X12": "-2", + "X13": "2", + "X14": "-2", + "X15": "2", + "X2": "-2", + "X20": "-2", + "X21": "2", + "X23": "-2", + "X24": "2", + "X29": "-2", + "X3": "2", + "X30": "2", + "X34": "-2", + "X35": "-2", + "X36": "2", + "X37": "2", + "X4": "2", + "X42": "-2", + "X43": "-2", + "X44": "2", + "X45": "2", + "X49": "-2", + "X5": "2", + "X50": "-2", + "X51": "2", + "X52": "2", + "X57": "-2", + "X58": "-2", + "X59": "2", + "X6": "2", + "X60": "2", + "X65": "-2", + "X66": "-2", + "X67": "2", + "X68": "2", + "X7": "2", + "X73": "-2", + "X74": "-2", + "X75": "2", + "X76": "2", + "X81": "-2", + "X82": "2", + "X83": "2", + "X88": "-2", + "X89": "-2", + "X90": "2", + "X95": "-2", + "X96": "2" + }, + "zero": 2493 + }, + { + "copy": 2502, + "delivery_helpers": [ + "D20", + "D21", + "D22" + ], + "drop": 2503, + "erase": 2507, + "first_downstream_reads": { + "D20": 2638, + "D21": 3025, + "D22": 3286 + }, + "fixed_cleanup_events": { + "D20": 3619, + "D21": 3621, + "D22": 3623 + }, + "last_read": 2506, + "nonzero_private_at_erase": true, + "query": "Q5", + "query_source_coefficients": { + "X1": "2", + "X10": "2", + "X100": "2", + "X101": "2", + "X102": "2", + "X11": "2", + "X12": "2", + "X13": "2", + "X14": "-2", + "X15": "-2", + "X16": "-2", + "X17": "-2", + "X2": "2", + "X22": "-2", + "X23": "-2", + "X24": "-2", + "X25": "-2", + "X26": "-2", + "X32": "-2", + "X35": "2", + "X37": "2", + "X38": "2", + "X39": "2", + "X41": "2", + "X42": "2", + "X43": "2", + "X44": "2", + "X45": "2", + "X46": "2", + "X47": "-2", + "X5": "2", + "X54": "2", + "X58": "2", + "X6": "2", + "X60": "2", + "X61": "2", + "X62": "2", + "X63": "-2", + "X70": "2", + "X74": "2", + "X76": "2", + "X77": "2", + "X78": "2", + "X79": "-2", + "X80": "-2", + "X81": "-2", + "X82": "-2", + "X86": "-2", + "X92": "2", + "X93": "2", + "X98": "2", + "X99": "2" + }, + "zero": 2501 + }, + { + "copy": 2509, + "delivery_helpers": [ + "D23", + "D24", + "D25", + "D26" + ], + "drop": 2510, + "erase": 2515, + "first_downstream_reads": { + "D23": 2672, + "D24": 3048, + "D25": 3217, + "D26": 2938 + }, + "fixed_cleanup_events": { + "D23": 3625, + "D24": 3627, + "D25": 3629, + "D26": 3631 + }, + "last_read": 2514, + "nonzero_private_at_erase": true, + "query": "Q6", + "query_source_coefficients": { + "X0": "2", + "X1": "-2", + "X10": "-2", + "X11": "-2", + "X16": "2", + "X17": "2", + "X18": "-2", + "X19": "-2", + "X2": "-2", + "X25": "2", + "X26": "2", + "X27": "-2", + "X28": "-2", + "X3": "2", + "X34": "2", + "X35": "-2", + "X36": "2", + "X37": "-2", + "X4": "2", + "X40": "2", + "X41": "-2", + "X46": "2", + "X47": "2", + "X48": "-2", + "X5": "-2", + "X53": "2", + "X54": "-2", + "X57": "2", + "X58": "-2", + "X59": "2", + "X6": "-2", + "X60": "-2", + "X63": "2", + "X64": "-2", + "X69": "2", + "X70": "-2", + "X73": "2", + "X74": "-2", + "X75": "2", + "X76": "-2", + "X8": "2", + "X81": "2", + "X82": "2", + "X83": "-2", + "X86": "2", + "X87": "-2", + "X9": "2", + "X91": "2", + "X92": "-2", + "X97": "2", + "X98": "-2", + "X99": "-2" + }, + "zero": 2508 + }, + { + "copy": 2517, + "delivery_helpers": [ + "D27", + "D28", + "D29", + "D30", + "D31" + ], + "drop": 2518, + "erase": 2524, + "first_downstream_reads": { + "D27": 2718, + "D28": 2908, + "D29": 3090, + "D30": 3156, + "D31": 3318 + }, + "fixed_cleanup_events": { + "D27": 3633, + "D28": 3635, + "D29": 3637, + "D30": 3639, + "D31": 3641 + }, + "last_read": 2523, + "nonzero_private_at_erase": true, + "query": "Q7", + "query_source_coefficients": { + "X1": "2", + "X100": "2", + "X103": "2", + "X13": "-2", + "X14": "2", + "X18": "2", + "X19": "2", + "X2": "2", + "X20": "2", + "X22": "2", + "X23": "2", + "X27": "2", + "X28": "2", + "X29": "2", + "X3": "-2", + "X32": "2", + "X35": "2", + "X36": "-2", + "X4": "-2", + "X40": "-2", + "X44": "-2", + "X45": "-2", + "X46": "-2", + "X48": "2", + "X49": "2", + "X50": "2", + "X54": "2", + "X58": "2", + "X59": "-2", + "X64": "2", + "X65": "2", + "X66": "2", + "X7": "-2", + "X70": "2", + "X74": "2", + "X75": "-2", + "X79": "2", + "X8": "-2", + "X80": "2", + "X81": "2", + "X83": "2", + "X84": "2", + "X85": "2", + "X87": "2", + "X88": "2", + "X89": "2", + "X9": "-2", + "X92": "2", + "X94": "2", + "X95": "2", + "X98": "2", + "X99": "2" + }, + "zero": 2516 + } + ], + "native_retirement_general_lower_bound_claimed": false, + "net_extra_mass": 56, + "private_allocations_after": 0, + "private_copies_after": 0, + "private_erases_after": 0, + "replacement_adds": 2624, + "replacement_mass": 2424, + "replacement_profile": { + "1": 1074, + "2": 58, + "3": 86, + "4": 104, + "5": 48, + "6": 24, + "7": 16, + "8": 8 + }, + "replacement_transports": 1418, + "schema_version": 1, + "scope": "literal private COPY retirement and direct-query replacement; no supplier", + "two_axis_all_correction_forgiven_direct_query_gap": 12480, + "two_axis_all_correction_forgiven_original_gap": 832, + "two_axis_calls": 208, + "two_axis_direct_query_gap": 55744, + "two_axis_original_gap": 44096 +} diff --git a/research/p104-copy-retirement/RETURN-RECIPES.json b/research/p104-copy-retirement/RETURN-RECIPES.json new file mode 100644 index 0000000000..d8d40ca9ee --- /dev/null +++ b/research/p104-copy-retirement/RETURN-RECIPES.json @@ -0,0 +1,642 @@ +[ + { + "event": 2479, + "recipe": { + "left": { + "linear_Z4": [ + 2, + 2, + 2, + 2, + 2, + 2, + 2, + 0, + 0 + ], + "matrix_rows": [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ], + "offset": 0, + "phase": 0, + "quadratic_rows": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ] + }, + "rank": 7, + "right": { + "linear_Z4": [ + 2, + 2, + 2, + 2, + 2, + 2, + 2, + 0, + 0 + ], + "matrix_rows": [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ], + "offset": 127, + "phase": 3, + "quadratic_rows": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ] + } + } + }, + { + "event": 2487, + "recipe": { + "left": { + "linear_Z4": [ + 3, + 2, + 3, + 2, + 2, + 2, + 3, + 0, + 0 + ], + "matrix_rows": [ + 184, + 2, + 261, + 8, + 16, + 32, + 65, + 1, + 125 + ], + "offset": 0, + "phase": 0, + "quadratic_rows": [ + 57, + 0, + 124, + 69, + 69, + 69, + 124, + 0, + 0 + ] + }, + "rank": 7, + "right": { + "linear_Z4": [ + 3, + 2, + 3, + 2, + 2, + 2, + 3, + 2, + 2 + ], + "matrix_rows": [ + 196, + 2, + 4, + 461, + 469, + 485, + 320, + 197, + 256 + ], + "offset": 446, + "phase": 3, + "quadratic_rows": [ + 313, + 0, + 252, + 453, + 453, + 453, + 252, + 380, + 185 + ] + } + } + }, + { + "event": 2503, + "recipe": { + "left": { + "linear_Z4": [ + 3, + 2, + 2, + 2, + 2, + 3, + 2, + 0, + 0 + ], + "matrix_rows": [ + 129, + 2, + 264, + 12, + 16, + 32, + 64, + 45, + 4 + ], + "offset": 0, + "phase": 0, + "quadratic_rows": [ + 45, + 0, + 33, + 33, + 0, + 45, + 0, + 0, + 0 + ] + }, + "rank": 7, + "right": { + "linear_Z4": [ + 0, + 2, + 1, + 3, + 2, + 0, + 2, + 3, + 0 + ], + "matrix_rows": [ + 1, + 2, + 392, + 388, + 16, + 160, + 64, + 128, + 268 + ], + "offset": 211, + "phase": 3, + "quadratic_rows": [ + 128, + 0, + 140, + 140, + 0, + 128, + 0, + 173, + 0 + ] + } + } + }, + { + "event": 2518, + "recipe": { + "left": { + "linear_Z4": [ + 2, + 2, + 3, + 2, + 2, + 2, + 3, + 0, + 0 + ], + "matrix_rows": [ + 1, + 2, + 232, + 268, + 16, + 36, + 68, + 40, + 4 + ], + "offset": 0, + "phase": 0, + "quadratic_rows": [ + 0, + 0, + 108, + 68, + 0, + 68, + 108, + 0, + 0 + ] + }, + "rank": 7, + "right": { + "linear_Z4": [ + 2, + 2, + 1, + 1, + 2, + 1, + 1, + 2, + 0 + ], + "matrix_rows": [ + 1, + 2, + 488, + 484, + 16, + 332, + 428, + 492, + 128 + ], + "offset": 499, + "phase": 3, + "quadratic_rows": [ + 0, + 0, + 236, + 108, + 0, + 108, + 236, + 68, + 0 + ] + } + } + }, + { + "event": 2510, + "recipe": { + "left": { + "linear_Z4": [ + 2, + 2, + 2, + 3, + 2, + 3, + 3, + 0, + 0 + ], + "matrix_rows": [ + 1, + 2, + 4, + 144, + 272, + 40, + 72, + 8, + 120 + ], + "offset": 0, + "phase": 0, + "quadratic_rows": [ + 0, + 0, + 0, + 24, + 104, + 112, + 112, + 0, + 0 + ] + }, + "rank": 7, + "right": { + "linear_Z4": [ + 2, + 2, + 2, + 1, + 0, + 3, + 3, + 2, + 3 + ], + "matrix_rows": [ + 1, + 2, + 4, + 480, + 504, + 288, + 320, + 488, + 256 + ], + "offset": 15, + "phase": 0, + "quadratic_rows": [ + 0, + 0, + 0, + 24, + 232, + 240, + 240, + 368, + 384 + ] + } + } + }, + { + "event": 2463, + "recipe": { + "left": { + "linear_Z4": [ + 2, + 2, + 2, + 2, + 3, + 2, + 2, + 0, + 0 + ], + "matrix_rows": [ + 129, + 2, + 4, + 8, + 365, + 32, + 64, + 16, + 125 + ], + "offset": 0, + "phase": 0, + "quadratic_rows": [ + 16, + 0, + 16, + 16, + 125, + 16, + 16, + 0, + 0 + ] + }, + "rank": 7, + "right": { + "linear_Z4": [ + 0, + 2, + 0, + 0, + 3, + 0, + 0, + 2, + 3 + ], + "matrix_rows": [ + 401, + 2, + 148, + 152, + 384, + 176, + 208, + 256, + 400 + ], + "offset": 131, + "phase": 1, + "quadratic_rows": [ + 144, + 0, + 144, + 144, + 125, + 144, + 144, + 365, + 384 + ] + } + } + }, + { + "event": 2472, + "recipe": { + "left": { + "linear_Z4": [ + 3, + 2, + 3, + 2, + 2, + 3, + 3, + 0, + 0 + ], + "matrix_rows": [ + 129, + 2, + 4, + 8, + 16, + 320, + 96, + 5, + 32 + ], + "offset": 0, + "phase": 0, + "quadratic_rows": [ + 5, + 0, + 5, + 0, + 0, + 96, + 96, + 0, + 0 + ] + }, + "rank": 7, + "right": { + "linear_Z4": [ + 0, + 2, + 0, + 2, + 2, + 1, + 3, + 1, + 0 + ], + "matrix_rows": [ + 1, + 2, + 132, + 8, + 16, + 320, + 288, + 128, + 352 + ], + "offset": 155, + "phase": 3, + "quadratic_rows": [ + 128, + 0, + 128, + 0, + 0, + 96, + 96, + 133, + 0 + ] + } + } + }, + { + "event": 2495, + "recipe": { + "left": { + "linear_Z4": [ + 2, + 2, + 2, + 2, + 2, + 2, + 3, + 0, + 0 + ], + "matrix_rows": [ + 1, + 2, + 132, + 8, + 16, + 32, + 284, + 64, + 92 + ], + "offset": 0, + "phase": 0, + "quadratic_rows": [ + 0, + 0, + 64, + 64, + 64, + 0, + 92, + 0, + 0 + ] + }, + "rank": 7, + "right": { + "linear_Z4": [ + 2, + 2, + 0, + 0, + 0, + 2, + 3, + 2, + 3 + ], + "matrix_rows": [ + 1, + 2, + 452, + 200, + 208, + 32, + 384, + 256, + 448 + ], + "offset": 35, + "phase": 3, + "quadratic_rows": [ + 0, + 0, + 192, + 192, + 192, + 0, + 92, + 284, + 384 + ] + } + } + } +] diff --git a/research/p104-copy-retirement/SOURCES.json b/research/p104-copy-retirement/SOURCES.json new file mode 100644 index 0000000000..9baac8cd39 --- /dev/null +++ b/research/p104-copy-retirement/SOURCES.json @@ -0,0 +1,58 @@ +{ + "schema_version": 1, + "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81", + "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "67f085acd86acd7d4e03922d9cf4b26bca66fed5", + "sha256": "47b42433f5a85809a3aadd29c2c339da2c6ed728e4f7762df6b88bccb7874cf0" + }, + { + "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" + }, + { + "path": "research/p104-native-channel/NATIVE-RECIPES.json.gz", + "usage": "input", + "git_blob": "ab129678c2df4f0d39b02b88457d02c37de0d9b6", + "sha256": "a1c4d83d3d5fe1338e99b59272e8cf5d43244c33888597da340b2aa7fef5b3e8" + }, + { + "path": "research/p104-native-channel/vendor/native_verify.py", + "usage": "input", + "git_blob": "2c209dfa9cfade3bc20ac5fc9d876b433a147f8c", + "sha256": "3049471905b47b385c88378a1a3be7a18b8858aadd035b8a6da2f4a03b470f38" + }, + { + "path": "research/p104-native-channel/vendor/clifford_exact.py", + "usage": "input", + "git_blob": "166841a037f069249f6f7f6dedb89248812f59e2", + "sha256": "2982ead07721e83358dc67c6f49c2b4c16a236a6bebdfd72f58221be1f5d0962" + } + ], + "source_exports": [ + { + "path": "inputs/pr3882_verify.py", + "sha256": "599274dbff5eefd8800e4cf39a25a7675edaaed93dc1490692bdfdbfb703ec3d", + "upstream_head": "9d56eeedbed5e3e9bbbc8c189d66f14cf15b6067", + "upstream_path": "research/p104-role-exchange-residue/verify.py", + "usage": "Unchanged source export. Reuse only geometry and actual tail schedule builder, not its evaluator.", + "upstream_git_blob": "093e21df60f5f1a02aaa1495da22d881e0c53fa1" + } + ] +} diff --git a/research/p104-copy-retirement/TASK.json b/research/p104-copy-retirement/TASK.json new file mode 100644 index 0000000000..3f2f9e37d4 --- /dev/null +++ b/research/p104-copy-retirement/TASK.json @@ -0,0 +1,88 @@ +{ + "schema_version": 1, + "task_id": "p104-side-correction", + "priority_revision": 6, + "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "original_card": { + "id": "p104-side-correction", + "question": "Can the proposed P104 joint endpoint flags be realized by a chronological correction program with coefficients, dirty restoration and an affordable complete bill?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/p104-native-channel/README.md", + "research/p104-native-channel/PROOF.md", + "docs/research/community-efficient1000-review.md", + "research/p104-joint-unit-flags/README.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. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read the revision-6 family record and #2981 static joint flags, alongside the reviewed #1991 channel. #2981 is an author-checked source archive, not an independently validated executable correction or a refutation of program-level lifetime floors.", + "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": "After checking live handoffs, pin one named collection from #2981 and attach acquisition/delivery times, source dependencies and coefficient requirements. Test legal access and arbitrary dirty restoration; price any completion against the full channel/endpoint/hosting allowance. Stop with the exact missing implication or a scoped counterexample rather than expanding the static cover census.", + "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.", + "Repeating a correction or physical conversion already supplied by a pending follow-up without adding independent coverage or a different unresolved obligation.", + "Repeating the 208-flag static matching or calling a static nested cover a chronological correction program. Independent audit of that certificate is distinct and remains useful." + ], + "overlap_terms": [ + "P104", + "I-G/2", + "side correction", + "native channel", + "1972", + "1991", + "2586", + "endpoint transport", + "physical dual", + "relay composition", + "2981", + "joint unit flags", + "acquisition delivery", + "static nesting" + ], + "existing_checks": [ + { + "scope": "PR #2981 reports static joint endpoint flags and a matching of 208 departure and arrival flags; archival intake is not independent verification.", + "evidence": "research/p104-joint-unit-flags/README.md", + "remaining": "Independent flag check and a chronological coefficient program with dirty restoration and a complete cost.", + "status": "author-checked", + "source_commit": "3d24b92d8ba057b57cb2d480170ec407520e6882", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "refined", + "actual_scope": "Audit literal private COPY ownership and actual consumers, then verify and completely price a direct-query copy-free replacement.", + "scope_change_reason": "User assigned next bounded P104 activities following PR3954. This closes a specific source-bound ownership/cost implication instead of another static flag census.", + "bottleneck_link": "The rejected two-axis gate retains COPY56; test whether claimed retirement removes paid work or merely moves it onto dirty query restoration.", + "budget_minutes": 50, + "stop_rule": "Stop dependent construction if the changed ownership route fails the complete favorable budget. Retain a scoped actual-word counterexample and local replacement.", + "outcome": "negative-result", + "evidence": "PROOF.md; RESULT.json; RETURN-RECIPES.json; exact registered checks", + "author": "Chris R / Clear1nsight with substantial OpenAI Codex assistance", + "ai_assistance": "Substantial OpenAI Codex assistance for derivation, code, exact checks and publication; coordinating agent independently checked dirty-column deletion.", + "open_questions": [ + { + "question": "Can an actual changed delivery consumer remove the Q descent/return pair and restore every dirty D helper?", + "why_it_matters": "The verified copy-free replacement increases rank mass by56 and fails the same complete cost gate.", + "first_step": "Specify one replacement block on all query and delivery inputs, bind physical charts and price the full change before native expansion.", + "blocked_by": "No favorable changed producer/consumer or coverage contract has been supplied." + } + ] +} diff --git a/research/p104-copy-retirement/VERIFY.json b/research/p104-copy-retirement/VERIFY.json new file mode 100644 index 0000000000..5bacba6d0f --- /dev/null +++ b/research/p104-copy-retirement/VERIFY.json @@ -0,0 +1,62 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/p104-native-channel/PROOF.md", + "research/p104-native-channel/inputs/LOWRANK-WITNESS.json", + "research/p104-native-channel/NATIVE-RECIPES.json.gz", + "research/p104-native-channel/vendor/native_verify.py", + "research/p104-native-channel/vendor/clifford_exact.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact280-row channel and actual tail; lifetime/dirty/rank controls." + }, + { + "argv": [ + "{python}", + "-B", + "{package}/native.py" + ], + "timeout_seconds": 300, + "checks": "Eight source-bound forward/reverse rank7 native recipes;8192 exact Gaussian columns and global phase fault." + }, + { + "argv": [ + "{python}", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Optimized-mode identity and ownership failures remain enforced." + }, + { + "argv": [ + "{python}", + "-O", + "-B", + "{package}/native.py" + ], + "timeout_seconds": 300, + "checks": "Optimized-mode exact native columns and phase rejection." + }, + { + "argv": [ + "{python}", + "-B", + "{package}/test_controls.py" + ], + "timeout_seconds": 120, + "checks": "Seven actual optimized CLI rejection fixtures: Boolean/float receipt types, false mass, duplicate JSON, changed/missing source and altered tail export." + } + ] +} diff --git a/research/p104-copy-retirement/inputs/pr3882_verify.py b/research/p104-copy-retirement/inputs/pr3882_verify.py new file mode 100644 index 0000000000..093e21df60 --- /dev/null +++ b/research/p104-copy-retirement/inputs/pr3882_verify.py @@ -0,0 +1,291 @@ +#!/usr/bin/env python3 +"""Exact P104 changed-boundary experiment. Apache-2.0; see README for scope.""" +from __future__ import annotations + +import argparse +import hashlib +import itertools +import json +from collections import Counter +from fractions import Fraction as F +from pathlib import Path + +HERE = Path(__file__).resolve().parent +REPO = HERE.parents[1] +BASE = "20ecf2891d80b5acf18d980b2164fb44ea7faa90" +F0 = [[0,0,0,0,0,0,2,-2],[0,0,0,0,0,0,2,2], + [0,0,0,0,2,-2,0,0],[0,0,0,0,2,2,0,0], + [0,0,2,-2,0,0,0,0],[0,0,2,2,0,0,0,0], + [2,-2,0,0,0,0,0,0],[2,2,0,0,0,0,0,0]] +PUNCTURE_C = [[0,0,0,0,0,2,-2,0],[0,0,0,2,-2,0,0,0], + [0,2,-2,0,0,0,0,0],[1,-1,-1,-1,-1,-1,-1,1], + [1,-1,-1,1,1,1,1,1],[1,1,1,-1,-1,1,1,1], + [1,1,1,1,1,-1,-1,1],[2,0,0,0,0,0,0,-2]] +SOURCE_HASHES = { + "research/p104-native-channel/inputs/P104-FIXTURE.json": + "516c06f6ec3cb84be588c546108de897650288576dd5fbf5fe44b9c5546ad8a4", + "research/p104-native-channel/inputs/LOWRANK-WITNESS.json": + "0f541bef7f19fdeffd67157684e9f03d785f42c89973632f508fc1a0452b580e", + "research/p104-native-channel/PROOF.md": + "5d743145d389ffdfaffc66096fa7e32c7155b18f73d74755403151d0435bb94c", +} + + +def need(condition: bool, message: str) -> None: + if not condition: + raise ValueError(message) + + +def load(path: Path): + def unique(pairs): + out = {} + for key, value in pairs: + need(key not in out, f"duplicate JSON key: {key}") + out[key] = value + return out + return json.loads(path.read_text(), object_pairs_hook=unique) + + +def encoded(value) -> bytes: + return (json.dumps(value, sort_keys=True, separators=(",", ":")) + "\n").encode() + + +def digest(value) -> str: + return hashlib.sha256(encoded(value)).hexdigest() + + +def geometry(): + roots = set() + for i, j in itertools.combinations(range(8), 2): + for sign in (-1, 1): + row = [0] * 8 + row[i], row[j] = 2, 2 * sign + roots.add(tuple(row)) + for tail in itertools.product((-1, 1), repeat=7): + if sum(t < 0 for t in tail) % 2 == 0: + roots.add((1,) + tail) + removed = {tuple(r) for r in F0 + PUNCTURE_C} + need(len(roots) == 120 and len(removed) == 16 and removed <= roots, + "root universe or puncture changed") + ports = sorted(roots - removed) + R = list(map(list, zip(*ports))) + need(len(ports) == 104, "wrong port count") + for a in range(8): + for b in range(8): + need(sum(R[a][i] * R[b][i] for i in range(104)) == 104 * (a == b), + "RR^t is not 104 I") + J = [] + for a, b in ((0, 2), (1, 3), (4, 6), (5, 7)): + for sign in (-1, 1): + r = [0] * 8 + r[a], r[b] = 2, 2 * sign + J.append(ports.index(tuple(r))) + J.sort() + N = [i for i in range(104) if i not in J] + A = [[F(sum(x*y for x,y in zip(r,s)), 8) for s in ports] for r in ports] + need(all(A[i][j] == (i == j) for i in J for j in J), "J not orthogonal") + B = [[A[j][i] for i in N] for j in J] + need(all(v in (F(-1,2), 0, F(1,2)) for row in B for v in row), "B alphabet") + need(sum(v != 0 for row in B for v in row) == 384, "B support") + for a, i in enumerate(N): + for b, k in enumerate(N): + need(A[i][k] == sum(B[j][a] * B[j][b] for j in range(8)), + "A_NN != B^t B") + return R, A, J, N, B + + +def source_binding(J): + data = {} + for path, expected in SOURCE_HASHES.items(): + raw = (REPO / path).read_bytes() + need(hashlib.sha256(raw).hexdigest() == expected, f"source hash: {path}") + data[path] = raw + fixture = json.loads(data[next(iter(SOURCE_HASHES))]) + section = fixture["section4_explicit_P104"] + need(section["F0"] == F0 and section["C"] == PUNCTURE_C, "source extraction") + word = json.loads(data["research/p104-native-channel/inputs/LOWRANK-WITNESS.json"]) + full = [1 << i for i in range(9)] + final = word["final_frames"] + need(all(final[f"X{i}"] == full for i in range(104)), "source exit frame") + helpers = [f"Q{i}" for i in range(8)] + [f"G{i}" for i in range(32)] + [f"D{i}" for i in range(32)] + need(all(final[h] == full for h in helpers), "dirty helper exit frames") + need(all(len(final[f"Y{i}"]) == 8 and binary_rank(final[f"Y{i}"]) == 8 + for i in range(104)), "target exit hyperplane") + proof = data["research/p104-native-channel/PROOF.md"] + need(b"y_t + sum_s x_s/2" in proof, "inherited channel statement") + return {"bound_sources": len(data), "target_frame_digest": digest([final[f"Y{i}"] for i in range(104)]), + "pivot_input_frames": [word["initial_frames"][f"X{i}"] for i in J]} + + +def binary_rank(rows): + pivots = {} + for row in rows: + need(type(row) is int and 0 < row < 512, "invalid binary vector") + while row: + k = row.bit_length() - 1 + if k in pivots: + row ^= pivots[k] + else: + pivots[k] = row + break + return len(pivots) + + +def program(J, N, B): + ops = [("lift", 104+i) for i in range(104)] + for a, i in enumerate(N): + ops.append(("half", i)) + for b, j in enumerate(J): + if B[b][a]: + s = int(2 * B[b][a]) + ops.extend([("add", j, i, s), ("add", 104+j, i, -s)]) + ops.append(("double", i)) + for b, j in enumerate(J): + ops.append(("half", j)) + for a, i in enumerate(N): + if B[b][a]: + ops.append(("add", i, j, -int(2 * B[b][a]))) + ops.append(("double", j)) + ops.extend(("add", i, 104+i, 1) for i in N) + ops.extend(("drop", i) for i in N) + ops.extend(("drop", 104+j) for j in J) + return ops + + +def execute(A, ops): + # The 72 arbitrary dirty inputs are explicit independent columns, not zero. + state = [[F(i == j) for j in range(280)] for i in range(280)] + for i in range(104): + state[104+i][:104] = A[i][:] + frames = [9]*104 + [8]*104 + [9]*72 + max_denominator = max(x.denominator for row in state for x in row) + peak_row_norm = max(sum(abs(x) for x in row) for row in state) + for op in ops: + kind, target = op[:2] + need(type(target) is int and 0 <= target < 208, "helper mutation or bad register") + if kind == "lift": + need(frames[target] == 8, "lift source frame") + frames[target] = 9 + continue + if kind == "drop": + need(frames[target] == 9, "drop source frame") + frames[target] = 8 + continue + need(frames[target] == 9, "arithmetic target not FULL") + if kind == "add": + source, sign = op[2:] + need(source != target and 0 <= source < 208 and frames[source] == 9, + "arithmetic source or frame") + need(type(sign) is int and sign in (-1, 1), "ADD coefficient") + state[target] = [x + sign*y for x,y in zip(state[target], state[source])] + else: + need(kind in ("half", "double"), "unknown operation") + scalar = F(1, 2) if kind == "half" else F(2) + state[target] = [scalar*x for x in state[target]] + max_denominator = max(max_denominator, *(x.denominator for x in state[target])) + peak_row_norm = max(peak_row_norm, sum(abs(x) for x in state[target])) + return state, frames, max_denominator, peak_row_norm + + +def mod_rank(matrix, prime=3): + a = [[int(F(x).numerator * pow(F(x).denominator, -1, prime) % prime) + for x in row] for row in matrix] + rank = 0 + for col in range(len(a[0])): + pivot = next((i for i in range(rank, len(a)) if a[i][col]), None) + if pivot is None: + continue + a[rank], a[pivot] = a[pivot], a[rank] + inv = pow(a[rank][col], -1, prime) + a[rank] = [(v*inv) % prime for v in a[rank]] + for i in range(rank+1, len(a)): + c = a[i][col] + if c: + a[i] = [(x-c*y) % prime for x,y in zip(a[i], a[rank])] + rank += 1 + if rank == len(a): + break + return rank + + +def verify_endpoint(state, frames, A, J, N, B): + for i in range(104): + target = 104+i if i in J else i + expected = [F(k in (i,104+i)) for k in range(280)] + need(state[target] == expected and frames[target] == 8, f"sum endpoint {i}") + for b,j in enumerate(J): + expected = [F(k == j) for k in range(280)] + for a,i in enumerate(N): + expected[i] = B[b][a] + need(state[j] == expected and frames[j] == 9, f"q residual {j}") + for i in N: + expected = [F(k == 104+i) for k in range(280)] + expected[:104] = A[i][:] + need(state[104+i] == expected and frames[104+i] == 9, f"v residual {i}") + for i in range(208,280): + need(state[i] == [F(i == k) for k in range(280)] and frames[i] == 9, + f"dirty helper {i}") + + +def calculate(): + R,A,J,N,B = geometry() + ops = program(J,N,B) + state,frames,den,norm = execute(A,ops) + verify_endpoint(state,frames,A,J,N,B) + # Separate endpoint formula and explicit inverse, not the gate interpreter. + xs = [] + for a,i in enumerate(N): + w = state[i] + v = state[104+i] + xs.append([w[k]-v[k]+sum(B[b][a]*state[j][k] for b,j in enumerate(J)) + for k in range(280)]) + for a,i in enumerate(N): + need(xs[a] == [F(k == i) for k in range(280)], "inverse x_N") + for b,j in enumerate(J): + restored = [state[j][k]-sum(B[b][a]*xs[a][k] for a in range(96)) + for k in range(280)] + need(restored == [F(k == j) for k in range(280)], "inverse x_J") + C = [[F(i == j)-A[i][j] for j in range(104)] for i in range(104)] + naive = [[F(i == j) for j in range(104)]+[F(i == j) for j in range(104)] + for i in range(104)] + naive += [A[i][:]+[F(i == j) for j in range(104)] for i in range(104)] + need(mod_rank(C) == 96 and mod_rank(naive) == 200, "mod-three obstruction") + need(mod_rank([r[:208] for r in state[:208]]) == 208, "repaired rank") + need(mod_rank(R) == 8, "root rank modulo three") + counts = Counter(op[0] for op in ops) + need(counts == Counter(add=1248,half=104,double=104,lift=104,drop=104), "invoice") + need(den == 4, "two-bit transient bound") + return { + "schema_version": 1, "base_commit": BASE, "scope": "changed source-consuming boundary; no supplier or kappa", + "ports": 104, "pivots": J, "nonpivots": N, "root_nonzeros": sum(v != 0 for r in R for v in r), + "B_nonzeros": 384, "program_sha256": digest(ops), "endpoint_sha256": digest([[str(v) for v in r] for r in state]), + "operation_counts": dict(sorted(counts.items())), "total_tail_events": len(ops), + "tail_native_profile": {"1": 208}, "inherited_channel_mass": 2368, "combined_mass": 2576, + "combined_native_profile": [1282,58,86,104,48,24,8,8], + "scalar_real_adds_at_512_complex_words": 1248*1024, + "scalar_real_halves_at_512_complex_words": 104*1024, + "scalar_real_doubles_at_512_complex_words": 104*1024, + "maximum_scalar_coefficient_denominator": den, "maximum_scalar_row_l1": str(norm), + "sum_outputs": 104, "dirty_helpers_restored": 72, + "rank_C_mod3": 96, "rank_naive_mod3": 200, "rank_repaired_mod3": 208, + "minimum_replaced_residual_arrays_in_stated_linear_model": 8, + "det_naive": str(12**8), "native_lowering_replayed": False, "complete_consumer_admitted": False, + } + + +def main(): + parser = argparse.ArgumentParser() + parser.add_argument("--algebra-only", action="store_true", help="Do not claim full-repository source authentication.") + args = parser.parse_args() + result = calculate() + need(encoded(result) == encoded(load(HERE/"RESULT.json")), "typed result mismatch") + if args.algebra_only: + marker = "PASS_P104_ROLE_EXCHANGE_ALGEBRA_ONLY" + else: + print(json.dumps(source_binding(result["pivots"]), sort_keys=True)) + marker = "PASS_P104_ROLE_EXCHANGE_SOURCE_BOUND" + print(f"{marker} replaced=8 sums=104 dirt=72 tail_H1=208 result={digest(result)}") + + +if __name__ == "__main__": + main() diff --git a/research/p104-copy-retirement/native.py b/research/p104-copy-retirement/native.py new file mode 100644 index 0000000000..ce0b3c4964 --- /dev/null +++ b/research/p104-copy-retirement/native.py @@ -0,0 +1,58 @@ +#!/usr/bin/env python3 +"""Eight changed local query returns, exact Gaussian operators including phase.""" +import argparse,gzip,hashlib,importlib.util,json,sys +from pathlib import Path +P=Path(__file__).resolve().parent;ROOT=P.parents[1];NATIVE=ROOT/'research/p104-native-channel' +def need(ok,msg): + if not ok:raise ValueError(msg) +def module(name,path): + spec=importlib.util.spec_from_file_location(name,path);m=importlib.util.module_from_spec(spec);sys.modules[name]=m;spec.loader.exec_module(m);return m +def sources(): + pins=json.loads((P/'SOURCES.json').read_text()) + for row in pins['files']: + if row['usage']=='input':need(hashlib.sha256((ROOT/row['path']).read_bytes()).hexdigest()==row['sha256'],'native source pin') + return json.loads(gzip.decompress((NATIVE/'NATIVE-RECIPES.json.gz').read_bytes())) +def main(): + ap=argparse.ArgumentParser();ap.add_argument('--generate',action='store_true');args=ap.parse_args() + cert=sources();word=json.loads((NATIVE/'inputs/LOWRANK-WITNESS.json').read_text());N=module('copy_native_independent',NATIVE/'vendor/native_verify.py') + drops=[r for r in cert['transports'] if any(word['program'][i][1]=='C' for i in r['events'])] + need(len(drops)==8,'eight native private drops') + if args.generate: + C=module('copy_native_compiler',NATIVE/'vendor/clifford_exact.py');reverses=[] + for d in drops: + op=C.canonical_frame(9,tuple(d['new'])).adjoint().then(C.canonical_frame(9,tuple(d['old']))) + recipe,_=C.lower_child(op);reverses.append({'event':d['events'][0],'recipe':recipe}) + (P/'RETURN-RECIPES.json').write_text(json.dumps(reverses,sort_keys=True,indent=2)+'\n') + recipes=json.loads((P/'RETURN-RECIPES.json').read_text());by={r['event']:r['recipe'] for r in recipes};need(len(by)==8,'eight unique returns') + iso=cert['label_isometry'];dual=iso['compressed_dual_gram'];orth=iso['orthonormal_basis_compressed'] + mv=lambda rows,x:sum(((r&x).bit_count()&1)<