diff --git a/research/p104-minimum-shared-space/README.md b/research/p104-minimum-shared-space/README.md new file mode 100644 index 0000000000..35bc8bcd1a --- /dev/null +++ b/research/p104-minimum-shared-space/README.md @@ -0,0 +1,188 @@ +# The fixed P104 shared correction space has minimum dimension 96 + +This closes the **96-versus-97 algebraic question** in +[Gonzalo Mier's PR #2173](https://github.com/CrocSwap/integer-mult-bounds/pull/2173), +head `d9b784ca86fba060f0264370536ccd322c89998a`. An explicit rational space of +dimension **96** supplies every `I-G/2` correction row modulo that target's +fixed pooled snapshot span. The predecessor proves the lower bound 96 and +exhibits a 97-dimensional space generated by natural correction rows. Our +witness allows arbitrary rational directions and attains the lower bound. + +**This is a relaxed algebraic interface, not a chronological correction word +or a cheaper supplier.** Snapshot pooling grants access at different times; +constructing, transporting and restoring the new shared directions is not +priced here. No new κ or selected-frontier change is claimed. + +## Exact model and evidence + +The frozen 4,058-event PR #1972 channel, retained in PR #1991's native package, +has 104 source inputs, 104 target inputs and 72 arbitrary dirty helper inputs. +We replay all **280 independent input columns**, every frame and private +lifetime, and the original `G/2` endpoint. The inherited paid rank mass remains +2,368; no new native invoice is inferred from the dimension calculation. + +At each of the 4,059 cuts, let `v_r(c)` be the current logical row of live +register `r` in the original channel. For target `t`, define + +``` +S_t = span_Q { v_r(c) : r != Y_t, + frame(r,c) = frame(Y_t,c) as binary subspaces }. +C = I - G/2. +``` + +All live sources, helpers, private copies and other targets are eligible. +Rows from different cuts are pooled, and chart-basis changes within the same +subspace are free in this model. The snapshots themselves remain unchanged: +new shared rows are not fed back through the old word to create new snapshots. +The question is the least dimension of any rational subspace `H` of the full +280-coordinate boundary space for which `C_t in S_t + H` for all 104 targets. + +The two checkers reconstruct 1,488 distinct rows seen in target-containing +frame classes. Individual pools have 1,053–1,080 distinct eligible rows. +Their source-coordinate ranks have histogram +`{2:12, 3:24, 4:32, 5:24, 6:12}`; the full ranks are these numbers plus 175. +These agree with the predecessor's 177–181 full-span ranks. + +[WITNESS.json](WITNESS.json) contains only **41 weighted contacts** +`[target, cut, register, rational_weight]`, on 23 target rows. A cut is the +number of completed original events: cut zero is the initial state. All 41 +contacts use dirty `D` helpers, and all weights are `±1/2` or `±1`. +The contacts are a certificate of vector-space membership, not 41 new +chronologically executable operations. + +## Proof + +Let `R` be the 8-by-104 matrix of **doubled integer root coordinates**, with +ports in the pinned lexicographic order. Exact enumeration gives + +``` +R R^T = 104 I_8, G = R^T R / 4, +C = I_104 - R^T R / 8, C^-1 = I_104 - R^T R / 96. +``` + +In particular, `C` is nonsingular and `R C = -12 R`. + +**The fixed-span lemma.** Every captured snapshot's source-coordinate +projection lies in `row(R)`. At cut zero, `S_t` contains all 175 non-source +coordinate units except its own target input `Y_t`. No eligible snapshot has +a coefficient on that missing input. These statements are checked on the +full frozen trace, not inferred from just its final `G/2` identity. Thus any +captured row can have all its non-source coefficients removed using those +175 units. In particular `pi_X(S_t) = S_t intersect X`, and this space is +contained in `row(R)`. + +**Lower bound (the predecessor's bound, with a direct certificate).** If an +arbitrary full-boundary space `H` serves every target, then +`C_t in row(R) + pi_X(H)` for every `t`. The rows of `C` span all of `X`, so + +``` +104 <= 8 + dim(pi_X(H)) <= 8 + dim(H). +``` + +This also permits shared directions with dirty or target coordinates; those +coordinates cannot evade the projection bound. + +**Attainment.** For a certified contact with projected row `x`, its unique +root-code coefficient row is `a = x R^T / 104`. Sum those coefficient rows +with the recorded weights, separately for each target, to form a rational +104-by-8 matrix `A`. The contacts and the fixed-span lemma give +`(A R)_t in S_t intersect X`. Both checkers verify the exact identity + +``` +R A = I_8. +``` + +Consequently `E = I_104 - A R` is an idempotent of rank 96. Define + +``` +K = E C = C + 12 A R, H = row(K), +``` + +embedded in the first 104 boundary coordinates. Since `C` is invertible, +`rank(K)=96`. Also `K_t - C_t = 12(AR)_t` lies in `S_t`, so this single +96-dimensional space serves every target. The lower and upper bounds match. +Both checkers additionally compute the exact rank of the explicit `K`. +The independent checker verifies each of the 104 identities in all 280 +coordinates, including cancellation of the snapshot's original dirty input. +The sparse checker also verifies the right kernel `C^-1 A = A - R^T/96`; +right multiplication by `C` changes the kernel of `E`. + +The optional generator searches the 416 available local basis directions +using a rational linear system with 64 equations. It finds a full-rank +system and a 41-term solution. Acceptance does not rerun or trust that search: +the recorded contacts, `RA=I`, full-space memberships and ranks suffice. + +## Reproduce and controls + +Standard library, no network or predecessor checker imports: + +```sh +python3 -I -B research/p104-minimum-shared-space/verify.py +python3 -I -O -B research/p104-minimum-shared-space/independent.py +python3.12 scripts/research_package.py --package research/p104-minimum-shared-space +``` + +The first checker uses sparse rational rows, reduced binary bases and sparse +elimination. The second uses dense integer rows on the independently checked +denominator-four lattice, explicit enumeration of every binary subspace, and +dense rational elimination. Only strict I/O and receipt encoding are shared. +Both compare against [RESULT.json](RESULT.json). `--out NEW.json` writes a +receipt exclusively to a fresh caller-selected path; default replay is read-only. + +`test_package.py` tests all 41 coefficient sign changes, unavailable contacts, +use of a target's own row, missing initial dirty compensation and final helper +cleanup, a missing puncture, an incorrect transport rank, JSON/schema faults, +source and receipt drift, occupied outputs, and a read-only export without Git. +Reversing every frame basis is a positive representation-invariance control. +These checks also run with optimization enabled in the exported replay. + +To regenerate the witness without modifying committed evidence: + +```sh +python3 -I -B research/p104-minimum-shared-space/build.py --out /tmp/NEW-WITNESS.json +``` + +The registered replay uses CPython 3.12; source-export validation on CPython +3.14 is recorded in the PR. No native Clifford regeneration, chronological +owner assignment, new private-copy contract, global recursive moment, +precision/all-size argument, selected cold replay or formal proof assistant +check is part of this package. The predecessor's finite native realization +is inherited, not re-certified by our scalar replay. + +## Open next questions + +Dimension is an information-space quantity, not a count of paid child ranks. +The already known 208-rank end-cut correction is unfavorable under the +unchanged coverage contract (only `328/9` surplus rank units per call, as +reported in [PR #2082](https://github.com/CrocSwap/integer-mult-bounds/pull/2082)). +This package does not substitute 96 for 208 in that bill or rerun that cost +model. It resolves the explicitly requested dimension handoff only. + +Can a changed chronological producer realize this complement, or another +96-dimensional complement, with useful transport sharing? Start by assigning +actual frame paths and source reads to the certificate's 23 nonzero `A` rows, +then replay arbitrary dirty restoration and charge every changed transport, +COPY, idle child and owner obligation. The existing fixed-path/retained-cost +obstructions remain applicable to their models. The present witness grants +pooled access and arbitrary new shared directions, so it supplies neither +such a schedule nor a favorable cost bound. See `TASK.json` for the handoff. + +## Attribution and provenance + +Gonzalo Mier / PR #2173 posed this exact minimum-dimension question, proved +96 as a lower bound, and supplied the 97-dimensional witness. No part of that +lower-bound idea or the fixed pooled-span model is claimed new. No pending +predecessor code is imported or copied; its exact head is pinned for credit. + +Rohan Arun / PR #1972 supplies the scalar/frame channel +(`fd82d172f46933fd253c2c6de4bd5eaff5429cfd`), Chafik Boukhalfa / PR #1991 its +native realization, Adam Gall / PR #1940 the schedule, and Josie Elliston / +PR #1071 the fixture, with Ali Romman / PR #1125 and the retained geometry, +decoder and compiler lineage. Frozen inputs and their notices remain unchanged. + +The scientific base is `0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2`, priority +revision 4. `TASK.json` records the preserved random draw, scoped handoff +override and Discussion links; `SOURCES.json` binds every external input. +New mathematics, implementation and prose were prepared by Gareth Davidson +(@bitplane) with substantial OpenAI Codex assistance. Both checkers are +AI-assisted implementations, not independent human review. Apache-2.0. diff --git a/research/p104-minimum-shared-space/RESULT.json b/research/p104-minimum-shared-space/RESULT.json new file mode 100644 index 0000000000..52b5e91d3d --- /dev/null +++ b/research/p104-minimum-shared-space/RESULT.json @@ -0,0 +1,142 @@ +{ + "A_sha256": "05d1386b2386a35d11a9df7fc2eba20c5cb18e66985c7140eb66575fe88f3998", + "H_sha256": "e0d953df50999619b5a7823b3d4ed4490ddd0b9c50e0fedb96e99094e3d55dac", + "arbitrary_input_columns": 280, + "captured_snapshot_rows": 1488, + "certificate_terms": 41, + "cuts": 4059, + "minimum_dimension": 96, + "nonzero_A_rows": 23, + "original_paid_profile": { + "1": 1074, + "2": 58, + "3": 86, + "4": 104, + "5": 48, + "6": 24, + "7": 8, + "8": 8 + }, + "original_scalar_events": { + "add": 2624, + "copy": 8, + "erase": 8, + "zero": 8 + }, + "pool_sizes": [ + 1063, + 1071, + 1064, + 1063, + 1072, + 1065, + 1062, + 1063, + 1064, + 1072, + 1064, + 1063, + 1062, + 1067, + 1053, + 1064, + 1064, + 1071, + 1063, + 1063, + 1063, + 1066, + 1068, + 1067, + 1065, + 1063, + 1075, + 1065, + 1066, + 1067, + 1064, + 1068, + 1067, + 1068, + 1068, + 1069, + 1064, + 1064, + 1063, + 1063, + 1075, + 1059, + 1061, + 1066, + 1062, + 1075, + 1074, + 1077, + 1067, + 1067, + 1066, + 1066, + 1077, + 1078, + 1066, + 1068, + 1077, + 1080, + 1069, + 1080, + 1070, + 1069, + 1076, + 1062, + 1063, + 1062, + 1055, + 1066, + 1056, + 1056, + 1055, + 1063, + 1055, + 1055, + 1053, + 1054, + 1065, + 1064, + 1054, + 1064, + 1056, + 1055, + 1057, + 1064, + 1064, + 1056, + 1058, + 1067, + 1066, + 1055, + 1057, + 1058, + 1068, + 1078, + 1063, + 1075, + 1074, + 1061, + 1062, + 1074, + 1075, + 1075, + 1074, + 1079 + ], + "pooled_x_rank_histogram": { + "2": 12, + "3": 24, + "4": 32, + "5": 24, + "6": 12 + }, + "schema": "p104-minimum-shared-space/1", + "scope": "Exact algebraic pooled-span minimum only; no chronological producer, transport price, supplier or new kappa.", + "targets": 104 +} diff --git a/research/p104-minimum-shared-space/SOURCES.json b/research/p104-minimum-shared-space/SOURCES.json new file mode 100644 index 0000000000..80832b2510 --- /dev/null +++ b/research/p104-minimum-shared-space/SOURCES.json @@ -0,0 +1,51 @@ +{ + "schema_version": 1, + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "e8870e5917057d59b730eb14721a778639eca050", + "sha256": "d46eb6d5b3e279428753d770653663fbdf1063e55c255ea073d768f344927ef7" + }, + { + "path": "research/p104-native-channel/inputs/LOWRANK-RESULT.json", + "usage": "input", + "git_blob": "cbd1c6bdc9e34b25c64b2636ccd6acd2392232d4", + "sha256": "7143ec7780f6f38a8c294df8009c3621936b281d05ae79946ce22f581b73d1b1" + }, + { + "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" + } + ], + "predecessors": [ + { + "pr": 2173, + "author": "Gonzalo Mier", + "head": "d9b784ca86fba060f0264370536ccd322c89998a", + "role": "Fixed pooled-span model, lower96 and upper97; explicit arbitrary-direction minimum handoff." + }, + { + "pr": 1972, + "author": "Rohan Arun", + "head": "fd82d172f46933fd253c2c6de4bd5eaff5429cfd", + "role": "Frozen4058-event scalar/frame word." + } + ], + "credit": "Gonzalo Mier/2173 model and96..97 handoff; Rohan Arun/1972 scalar channel; Chafik Boukhalfa/1991 native binding; Adam Gall/1940 schedule; Josie Elliston/1071 fixture; retained Ali Romman/1125 and geometry lineage. No predecessor code imported." +} diff --git a/research/p104-minimum-shared-space/TASK.json b/research/p104-minimum-shared-space/TASK.json new file mode 100644 index 0000000000..1774c95c0e --- /dev/null +++ b/research/p104-minimum-shared-space/TASK.json @@ -0,0 +1,145 @@ +{ + "schema_version": 1, + "task_id": "p104-side-correction", + "priority_revision": 4, + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "original_card": { + "id": "p104-side-correction", + "question": "Can the native P104 low-rank channel be completed with a legal, fully charged I-G/2 side correction?", + "starting_points": [ + "research/p104-native-channel/README.md", + "research/p104-native-channel/PROOF.md", + "docs/research/community-efficient1000-review.md" + ], + "methods": [ + "Construct one side-correction word at an explicit chronological cut with the needed frames still available.", + "Derive a lower bound on the side correction and hosting costs that decides whether this channel can beat the selected budget." + ], + "acceptance_gate": "An exact arbitrary-input identity, source/target frame availability and restoration at the chosen cut, plus the complete channel+correction+idle/hosting bill or an explicit favorable bound. The native channel alone is not a supplier.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read the P104 open next questions and its fixed local histogram; inspect why appending I-G/2 after source completion is not justified. #1991 supplies the checked native channel, not the missing correction.", + "scope": "Source-bound orientation only. Read the named package and review before relying on its local evidence; this command is not its replay or supplier admission." + }, + "first_experiment": "Choose one exact side-correction cut and bound its allowed cost from a favorable completed moment at a declared target. Stop or hand off if the necessary source/target access cannot be justified or even the optimistic total misses the target.", + "bottleneck_link": "Completing an already realized changed channel tests a concrete construction opportunity, instead of refining the incumbent packing. A positive local result still needs global and all-size admission.", + "allowed_variations": [ + "One correction factorization, one chronological cut, or one explicit hosting obstruction.", + "A changed correction schedule with an updated full bill and native frame contract." + ], + "scope_change_triggers": [ + "Recompiling the already certified low-rank channel without closing a new obligation.", + "Treating a pending ancestor, local histogram or unpriced side correction as an admitted global supplier." + ], + "overlap_terms": [ + "P104", + "I-G/2", + "side correction", + "native channel", + "1972", + "1991" + ] + }, + "scope_status": "changed", + "actual_scope": "Exact minimum arbitrary rational shared correction-space dimension in PR2173 fixed pooled spans; attempt rank-eight projector complement and independently certify against all 104 targets.", + "scope_change_reason": "Revision4 central handoff preference; PR2173 explicitly leaves 96 versus97 open. Original gather scope uncompleted and released at Discussion2032. No reroll.", + "bottleneck_link": "Closes PR2173 exact 96-versus97 shared-space handoff for the central P104 correction; partial algebraic interface only, not the card complete-circuit acceptance gate.", + "budget_minutes": 60, + "stop_rule": "Stop the bounded linear-complement formulation if infeasible; do not infer arbitrary-H impossibility. Successful witness requires independent exact all-input and full-span verification.", + "outcome": "completed", + "evidence": "WITNESS.json:41 exact snapshot contacts construct RA=I; RESULT.json:minimum96 with all4059cuts and280inputs, independent sparse/dense replays.", + "author": "Gareth Davidson", + "ai_assistance": "Substantial OpenAI Codex assistance in mathematics, implementation, verification and writing. No subagents, human review or proof assistant.", + "open_questions": [ + { + "question": "Can this96-dimensional complement be realized by a changed chronological P104 producer at a useful complete price?", + "why_it_matters": "Dimension attainment alone does not provide a side correction or cheaper supplier.", + "first_step": "Assign real source reads/frame paths to the23 nonzeroArows, then check all dirty endpoints and a complete channel+correction+idle/hosting bill.", + "blocked_by": "Snapshot pooling and arbitrary shared directions are free only in the algebraic model; no new path/owner/native realization or budget is supplied." + } + ], + "seed": "04a0b5296b007400a2e6d4c67da47ad2", + "track": "complex-mechanisms", + "discussion": "https://github.com/CrocSwap/integer-mult-bounds/discussions/2245", + "assignment_history": { + "original_base": "c676548106012571fefa1dce0ec16f1bcfe11dce", + "original_priority_revision": 3, + "original_task": "complex-new-helper-inventory", + "original_scope_key": "f3b0895a4f9f1cc62e75", + "drawn_at_utc": "2026-10-14T17:34:49.907742+00:00", + "released_gather_claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/2032", + "reason": "Resume read revision4; unimplemented gather census released and central PR2173 handoff taken within original complex track. No reroll." + }, + "first_step": "scripts/research_baseline.py passed PASS_RESEARCH_BASELINE_BINDINGS_ONLY; PR1991 README/PROOF and PR2173 exact-head handoff read.", + "cost_scope": "Algebraic minimum only; no equation between space dimension and paid transport cost. Existing 208-rank tail exceeds unchanged-coverage allowance328/9.", + "predecessors": [ + { + "pr": 2173, + "author": "Gonzalo Mier", + "head": "d9b784ca86fba060f0264370536ccd322c89998a", + "role": "Fixed pooled-span model, lower96 and upper97; explicit arbitrary-direction minimum handoff." + }, + { + "pr": 1972, + "author": "Rohan Arun", + "head": "fd82d172f46933fd253c2c6de4bd5eaff5429cfd", + "role": "Frozen4058-event scalar/frame word." + } + ], + "overlap_entry": { + "searched_at": "2026-10-15T01:50:42.087073+00:00", + "coverage": { + "open_prs": { + "fetched_at": "2026-10-15T01:49:14.745325+00:00", + "complete_pagination": true, + "records": 476 + }, + "discussions": { + "fetched_at": "2026-10-15T01:50:42.013262+00:00", + "complete_pagination": true, + "records": 946 + } + }, + "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.", + "matches_total": 176 + }, + "publication_checkpoint": { + "checked_utc": "2026-10-15T02:07:53.053908+00:00", + "canonical_main": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "priority_revision": 4, + "relevant_input_and_guidance_changes": false, + "overlap": { + "searched_at": "2026-10-15T02:07:20.038289+00:00", + "coverage": { + "open_prs": { + "fetched_at": "2026-10-15T02:05:52.295826+00:00", + "complete_pagination": true, + "records": 480 + }, + "discussions": { + "fetched_at": "2026-10-15T02:07:19.971349+00:00", + "complete_pagination": true, + "records": 956 + } + }, + "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.", + "matches_total": 14 + }, + "decision": "Continue; predecessor still97upper bound and no competing exact dimension follow-up in targeted matches." + }, + "validation": { + "registered_runtime": "CPython3.12.3", + "registered_replay": "Passed both mathematical checkers and seven control groups; tests48.332seconds.", + "export_runtime": "CPython3.14.4", + "export": "Both isolated optimized read-only checkers passed;14files unchanged;noGit.", + "receipt_sha256": "a8b78ea543762bb03984b2e228fc2652e9036153b7ad0ab51354cedff5766f1a", + "native_global_precision_selected_cold_replays": "unrun; outside algebraic claim" + } +} diff --git a/research/p104-minimum-shared-space/VERIFY.json b/research/p104-minimum-shared-space/VERIFY.json new file mode 100644 index 0000000000..fb6649d641 --- /dev/null +++ b/research/p104-minimum-shared-space/VERIFY.json @@ -0,0 +1,43 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/p104-native-channel/inputs/LOWRANK-RESULT.json", + "research/p104-native-channel/inputs/LOWRANK-WITNESS.json", + "research/p104-native-channel/inputs/P104-FIXTURE.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Full4059-cut sparse rational replay, pool rank bound and explicit rank96 projector complement." + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/independent.py" + ], + "timeout_seconds": 120, + "checks": "Separate integer/dense full-input replay, enumerated binary frames and104 full-space identities." + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/test_package.py" + ], + "timeout_seconds": 240, + "checks": "Seven control groups including41 coefficient faults, dirty corruption, wrong contacts and optimized read-only source export." + } + ] +} diff --git a/research/p104-minimum-shared-space/WITNESS.json b/research/p104-minimum-shared-space/WITNESS.json new file mode 100644 index 0000000000..88ac211fa4 --- /dev/null +++ b/research/p104-minimum-shared-space/WITNESS.json @@ -0,0 +1,251 @@ +{ + "schema": "p104-shared-complement/1", + "terms": [ + [ + 0, + 2983, + "D18", + "-1/2" + ], + [ + 0, + 3217, + "D25", + "-1" + ], + [ + 1, + 2672, + "D23", + "1" + ], + [ + 1, + 2860, + "D4", + "-1/2" + ], + [ + 2, + 2574, + "D12", + "-1/2" + ], + [ + 2, + 2985, + "D18", + "1" + ], + [ + 2, + 2748, + "D0", + "1/2" + ], + [ + 3, + 2604, + "D16", + "1/2" + ], + [ + 4, + 2674, + "D23", + "1/2" + ], + [ + 7, + 2797, + "D17", + "-1/2" + ], + [ + 8, + 2799, + "D17", + "1" + ], + [ + 9, + 3043, + "D12", + "-1/2" + ], + [ + 9, + 2676, + "D23", + "1/2" + ], + [ + 12, + 2580, + "D12", + "1/2" + ], + [ + 13, + 2532, + "D5", + "1/2" + ], + [ + 14, + 2735, + "D5", + "1/2" + ], + [ + 14, + 2552, + "D8", + "-1/2" + ], + [ + 15, + 2805, + "D17", + "1/2" + ], + [ + 17, + 2678, + "D23", + "1/2" + ], + [ + 22, + 2638, + "D20", + "-1/2" + ], + [ + 22, + 3278, + "D28", + "-1/2" + ], + [ + 23, + 2826, + "D10", + "1/2" + ], + [ + 23, + 2640, + "D20", + "-1/2" + ], + [ + 23, + 3124, + "D28", + "-1/2" + ], + [ + 24, + 2608, + "D16", + "1/2" + ], + [ + 24, + 3286, + "D22", + "-1/2" + ], + [ + 24, + 2919, + "D27", + "-1/2" + ], + [ + 25, + 3384, + "D22", + "1/2" + ], + [ + 25, + 3099, + "D27", + "-1/2" + ], + [ + 26, + 2680, + "D23", + "1/2" + ], + [ + 26, + 3420, + "D31", + "1/2" + ], + [ + 27, + 3246, + "D20", + "1/2" + ], + [ + 27, + 3459, + "D31", + "1" + ], + [ + 32, + 3395, + "D21", + "1/2" + ], + [ + 32, + 2923, + "D27", + "1/2" + ], + [ + 33, + 2996, + "D13", + "1/2" + ], + [ + 33, + 2813, + "D17", + "1/2" + ], + [ + 33, + 3198, + "D21", + "1" + ], + [ + 33, + 3438, + "D23", + "1/2" + ], + [ + 34, + 3369, + "D23", + "1/2" + ], + [ + 63, + 3253, + "D29", + "1" + ] + ] +} diff --git a/research/p104-minimum-shared-space/build.py b/research/p104-minimum-shared-space/build.py new file mode 100644 index 0000000000..e472fc5bb9 --- /dev/null +++ b/research/p104-minimum-shared-space/build.py @@ -0,0 +1,72 @@ +"""Optional deterministic rational witness discovery; not used for acceptance. + +Gareth Davidson with OpenAI Codex assistance. Apache-2.0. +""" +from fractions import Fraction as Q +from pathlib import Path +import argparse +import json +import sys + +sys.path.insert(0, str(Path(__file__).resolve().parent)) +from common import need, sources +from verify import replay, verify_witness + + +def subtract(row, other, factor): + for j, value in other.items(): + new = row.get(j, Q(0)) - factor * value + if new: + row[j] = new + else: + row.pop(j, None) + + +def build(): + trace = replay(sources(), []) + pivots, witnesses, variables = {}, {}, [] + for target, ids in enumerate(trace["local_bases"]): + for row_id in ids: + coeff = trace["coefficients"][row_id] + row = {8 * i + j: Q(trace["ports"][target][i]) * coeff[j] + for i in range(8) for j in range(8) + if trace["ports"][target][i] * coeff[j]} + combination = {len(variables): Q(1)} + variables.append((target, row_id)) + while row: + pivot = min(row) + factor = row[pivot] + if pivot not in pivots: + pivots[pivot] = {j: v / factor for j, v in row.items()} + witnesses[pivot] = {j: v / factor for j, v in combination.items()} + break + subtract(row, pivots[pivot], factor) + subtract(combination, witnesses[pivot], factor) + row, solution = {9 * i: Q(1) for i in range(8)}, {} + while row: + pivot = min(row) + need(pivot in pivots, "no projector complement in this family") + factor = row[pivot] + subtract(row, pivots[pivot], factor) + subtract(solution, witnesses[pivot], -factor) + terms = [] + for index, weight in sorted(solution.items()): + target, row_id = variables[index] + cut, reg = trace["occurrences"][target][row_id] + terms.append([target, cut, reg, str(weight)]) + result = {"schema": "p104-shared-complement/1", "terms": terms} + # Acceptance still reconstructs these contacts independently of discovery. + print("LINEAR_SYSTEM", len(variables), "variables", len(pivots), "rank", + len(terms), "terms") + return result + + +if __name__ == "__main__": + parser = argparse.ArgumentParser() + parser.add_argument("--out", type=Path, required=True) + args = parser.parse_args() + need(not args.out.exists(), "output already exists") + result = build() + with args.out.open("x") as handle: + json.dump(result, handle, indent=2) + handle.write("\n") diff --git a/research/p104-minimum-shared-space/common.py b/research/p104-minimum-shared-space/common.py new file mode 100644 index 0000000000..9e57d39fc8 --- /dev/null +++ b/research/p104-minimum-shared-space/common.py @@ -0,0 +1,80 @@ +"""Strict I/O only; no mathematical routines shared by the two checkers. + +Gareth Davidson with OpenAI Codex assistance. Apache-2.0. +""" +from pathlib import Path +import argparse +import hashlib +import json + +HERE = Path(__file__).resolve().parent +REPO = HERE.parents[1] + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def unique(items): + result = {} + for key, value in items: + need(key not in result, "duplicate JSON key") + result[key] = value + return result + + +def read(path): + def bad(value): + raise ValueError("nonfinite JSON number: " + value) + return json.loads(Path(path).read_bytes(), object_pairs_hook=unique, + parse_constant=bad) + + +def digest(value): + raw = json.dumps(value, sort_keys=True, separators=(",", ":")).encode() + return hashlib.sha256(raw).hexdigest() + + +def sources(root=REPO): + result = {} + for pin in read(HERE / "SOURCES.json")["files"]: + if pin["usage"] == "input": + path = root / pin["path"] + need(hashlib.sha256(path.read_bytes()).hexdigest() == pin["sha256"], + "source bytes changed: " + pin["path"]) + result[path.name] = read(path) + return result + + +def certificate(value): + need(isinstance(value, dict) and set(value) == {"schema", "terms"}, "certificate fields") + need(value["schema"] == "p104-shared-complement/1", "certificate schema") + need(isinstance(value["terms"], list) and bool(value["terms"]), "terms list") + seen = set() + for term in value["terms"]: + need(isinstance(term, list) and len(term) == 4, "term shape") + target, cut, reg, weight = term + need(type(target) is int and 0 <= target < 104, "target index") + need(type(cut) is int and 0 <= cut <= 4058, "cut index") + need(isinstance(reg, str) and bool(reg), "register name") + need(isinstance(weight, str) and bool(weight), "rational string") + key = target, cut, reg + need(key not in seen, "duplicate contact") + seen.add(key) + return value + + +def cli(run, status): + parser = argparse.ArgumentParser() + parser.add_argument("--out", type=Path) + args = parser.parse_args() + need(args.out is None or not args.out.exists(), "output already exists") + result = run() + need(result == read(HERE / "RESULT.json"), "receipt differs from exact replay") + if args.out: + with args.out.open("x") as handle: + json.dump(result, handle, indent=2, sort_keys=True) + handle.write("\n") + print(status, "minimum=96 targets=104 cuts=4059 terms=" + + str(result["certificate_terms"]), "receipt=" + digest(result)) diff --git a/research/p104-minimum-shared-space/independent.py b/research/p104-minimum-shared-space/independent.py new file mode 100644 index 0000000000..b461ed9419 --- /dev/null +++ b/research/p104-minimum-shared-space/independent.py @@ -0,0 +1,232 @@ +"""Separate dense integer replay, enumerated subspaces and dense matrix audit. + +All frozen scalar rows have denominator dividing four, checked at every ADD. +No producer, predecessor, sparse checker or its linear algebra is imported. +Gareth Davidson with OpenAI Codex assistance. Apache-2.0. +""" +from collections import Counter, defaultdict +from fractions import Fraction +from functools import lru_cache +from pathlib import Path +import sys + +sys.path.insert(0, str(Path(__file__).resolve().parent)) +from common import HERE, certificate, cli, digest, need, read, sources + + +@lru_cache(None) +def subspace(vectors): + points = {0} + for vector in vectors: + need(type(vector) is int and 0 < vector < 512, "binary label") + points.update(x ^ vector for x in tuple(points)) + need(len(points) == 2 ** len(vectors), "independent binary frame") + return frozenset(points) + + +def geometry(fixture): + oriented = [] + for i in range(8): + for j in range(i + 1, 8): + for si in (-2, 2): + for sj in (-2, 2): + v = [0] * 8 + v[i], v[j] = si, sj + oriented.append(v) + for bits in range(256): + if bits.bit_count() % 2 == 0: + oriented.append([1 - 2 * ((bits >> j) & 1) for j in range(8)]) + lines = set() + for v in oriented: + sign = 1 if next(x for x in v if x) > 0 else -1 + lines.add(tuple(sign * x for x in v)) + removed = {tuple(v) for v in fixture["F0"] + fixture["C"]} + need(len(oriented) == 240 and len(lines) == 120 and + len(removed) == 16 and removed <= lines, "root enumeration") + return sorted(lines - removed) + + +def dense_rank(matrix): + if not matrix: + return 0 + a = [[Fraction(x) for x in row] for row in matrix] + pivot = 0 + for col in range(len(a[0])): + found = next((i for i in range(pivot, len(a)) if a[i][col]), None) + if found is None: + continue + a[pivot], a[found] = a[found], a[pivot] + value = a[pivot][col] + a[pivot] = [x / value for x in a[pivot]] + for i in range(pivot + 1, len(a)): + value = a[i][col] + if value: + a[i] = [x - value * y for x, y in zip(a[i], a[pivot])] + pivot += 1 + if pivot == len(a): + break + return pivot + + +def analyze(data, cert): + word = data["LOWRANK-WITNESS.json"] + ports = geometry(data["P104-FIXTURE.json"]["section4_explicit_P104"]) + names = list(word["initial_frames"]) + need(len(names) == len(set(names)) == 280 and + names[:104] == ["X" + str(i) for i in range(104)], "boundary coordinates") + x_columns = [names.index("X" + str(i)) for i in range(104)] + y_columns = [names.index("Y" + str(i)) for i in range(104)] + need(all(sum(p[i] * p[j] for p in ports) == 104 * (i == j) + for i in range(8) for j in range(8)), "tight root frame") + vectors, vector_ids = [], {} + + def intern(row): + row = tuple(row) + if row not in vector_ids: + vector_ids[row] = len(vectors) + vectors.append(row) + return vector_ids[row] + + current = {name: intern([4 * (j == i) for j in range(280)]) + for i, name in enumerate(names)} + frames = {n: subspace(tuple(f)) for n, f in word["initial_frames"].items()} + pools, captured, contacts = [set() for _ in range(104)], set(), {} + at_cut = defaultdict(list) + for index, (target, cut, reg, weight) in enumerate(cert["terms"]): + at_cut[cut].append((index, target, reg)) + + def observe(cut): + classes = defaultdict(dict) + for reg in current: + classes[frames[reg]][reg] = current[reg] + for group in classes.values(): + targets = [(int(r[1:]), r) for r in group if r.startswith("Y")] + if targets: + captured.update(group.values()) + for target, name in targets: + pools[target].update(rid for reg, rid in group.items() if reg != name) + for index, target, reg in at_cut[cut]: + need(reg in current and reg != "Y" + str(target), "live contact register") + need(frames[reg] == frames["Y" + str(target)], "actual contact frame") + contacts[index] = vectors[current[reg]] + + paid, scalar = Counter(), Counter() + observe(0) + need(len(word["program"]) == 4058, "event count") + for index, event in enumerate(word["program"]): + op, reg = event[:2] + if op == "transport": + before, after = subspace(tuple(event[2])), subspace(tuple(event[3])) + need(frames[reg] == before, "transport old frame") + need(before <= after or after <= before, "nested frame change") + rank = abs(len(before).bit_length() - len(after).bit_length()) + need(type(event[4]) is int and rank == event[4] > 0, "priced rank") + frames[reg] = after + paid[rank] += 1 + elif op == "add": + _, _, src, raw, frame = event + need(reg != src and frames[reg] == frames[src] == subspace(tuple(frame)), + "ADD equality of full subspaces") + factor = Fraction(raw) + source, dest = vectors[current[src]], vectors[current[reg]] + scaled = [factor.numerator * x for x in source] + need(all(x % factor.denominator == 0 for x in scaled), + "exact denominator-four lattice") + current[reg] = intern([a + b // factor.denominator for a, b in zip(dest, scaled)]) + scalar[op] += 1 + elif op == "zero": + need(reg == "C" and reg not in current, "private lifetime allocation") + current[reg], frames[reg] = intern([0] * 280), subspace(tuple(event[2])) + scalar[op] += 1 + elif op == "copy": + need(reg == "C" and not any(vectors[current[reg]]) and + frames[reg] == frames[event[2]] == subspace(tuple(event[3])), "private COPY") + current[reg] = current[event[2]] + scalar[op] += 1 + elif op == "erase": + need(reg == "C" and frames[reg] == subspace(tuple(event[2])), "private discard") + del current[reg], frames[reg] + scalar[op] += 1 + else: + raise ValueError("unknown operation") + observe(index + 1) + need(set(current) == set(names), "closed private lifetimes") + gram = [[sum(a * b for a, b in zip(p, q)) // 4 for q in ports] for p in ports] + for index, name in enumerate(names): + expected = [4 * (j == index) for j in range(280)] + if name.startswith("Y"): + target = int(name[1:]) + for j in range(104): + expected[x_columns[j]] = 2 * gram[target][j] + need(tuple(expected) == vectors[current[name]], "dense endpoint " + name) + need(frames[name] == subspace(tuple(word["final_frames"][name])), "terminal frame") + need(dict(paid) == {int(k): v for k, v in data["LOWRANK-RESULT.json"]["paid_profile"].items()} + and sum(k * v for k, v in paid.items()) == 2368, "original native invoice") + # Numerators of the eight root-code coordinates, with denominator 416. + projected = {} + for rid in captured: + row = vectors[rid] + coordinates = [sum(row[x_columns[j]] * ports[j][k] for j in range(104)) + for k in range(8)] + need(all(sum(coordinates[k] * ports[j][k] for k in range(8)) == + 104 * row[x_columns[j]] for j in range(104)), "projected root code") + projected[rid] = coordinates + dims = [] + for target, pool in enumerate(pools): + for col in range(104, 280): + if col != y_columns[target]: + unit = tuple(4 * (j == col) for j in range(280)) + need(vector_ids[unit] in pool, "initial outside coordinate") + need(all(vectors[r][y_columns[target]] == 0 for r in pool), "missing own target input") + # Deduplicate the 8-vectors before separate dense rational elimination. + dims.append(dense_rank(sorted({tuple(projected[r]) for r in pool}))) + A = [[Fraction(0)] * 8 for _ in range(104)] + representatives = [[Fraction(0)] * 280 for _ in range(104)] + for index, (target, cut, reg, weight) in enumerate(cert["terms"]): + weight = Fraction(weight) + need(weight and str(weight) == cert["terms"][index][3], "rational normalization") + row = contacts[index] + for j in range(280): + representatives[target][j] += weight * Fraction(row[j], 4) + for t in range(104): + for k in range(8): + A[t][k] = sum(representatives[t][x_columns[j]] * ports[j][k] + for j in range(104)) / 104 + need(all(sum(ports[t][i] * A[t][j] for t in range(104)) == int(i == j) + for i in range(8) for j in range(8)), "dense right inverse") + C = [[Fraction(t == j) - Fraction(gram[t][j], 2) for j in range(104)] for t in range(104)] + H = [[C[t][j] + 12 * representatives[t][x_columns[j]] for j in range(104)] for t in range(104)] + need(dense_rank(C) == 104 and dense_rank(H) == 96, "both exact matrix ranks") + # Direct 280-coordinate certificate: H_t - 12 times the full snapshot + # combination, plus its 175 available outside-unit corrections, is C_t. + for t in range(104): + full = [Fraction(0)] * 280 + for j in range(104): + full[x_columns[j]] = H[t][j] + for col in range(280): + full[col] -= 12 * representatives[t][col] + if col >= 104: + need(col != y_columns[t] or representatives[t][col] == 0, + "cannot cancel own Y by a free snapshot") + full[col] += 12 * representatives[t][col] + need(full == C[t] + [Fraction(0)] * 176, "full-space correction identity") + return {"schema": "p104-minimum-shared-space/1", "minimum_dimension": 96, + "targets": 104, "arbitrary_input_columns": 280, "cuts": 4059, + "captured_snapshot_rows": len(captured), + "pooled_x_rank_histogram": {str(k): v for k, v in sorted(Counter(dims).items())}, + "pool_sizes": list(map(len, pools)), "certificate_terms": len(cert["terms"]), + "nonzero_A_rows": sum(any(row) for row in A), + "A_sha256": digest([[str(x) for x in row] for row in A]), + "H_sha256": digest([[str(x) for x in row] for row in H]), + "original_paid_profile": {str(k): v for k, v in sorted(paid.items())}, + "original_scalar_events": dict(scalar), + "scope": "Exact algebraic pooled-span minimum only; no chronological producer, transport price, supplier or new kappa."} + + +def run(data=None, cert=None): + return analyze(sources() if data is None else data, + certificate(read(HERE / "WITNESS.json") if cert is None else cert)) + + +if __name__ == "__main__": + cli(run, "PASS_P104_MINIMUM_SHARED_SPACE_INDEPENDENT") diff --git a/research/p104-minimum-shared-space/test_package.py b/research/p104-minimum-shared-space/test_package.py new file mode 100644 index 0000000000..93b1ef1284 --- /dev/null +++ b/research/p104-minimum-shared-space/test_package.py @@ -0,0 +1,140 @@ +"""Semantic controls for the precise fixed-snapshot claim. + +Gareth Davidson with OpenAI Codex assistance. Apache-2.0. +""" +from pathlib import Path +import copy +import json +import shutil +import subprocess +import sys +import tempfile +import unittest + +sys.path.insert(0, str(Path(__file__).resolve().parent)) +import independent +import verify +from common import HERE, REPO, certificate, read, sources + + +class Controls(unittest.TestCase): + @classmethod + def setUpClass(cls): + cls.data = sources() + cls.cert = certificate(read(HERE / "WITNESS.json")) + cls.expected = read(HERE / "RESULT.json") + cls.trace = verify.replay(cls.data, cls.cert["terms"]) + + def test_41_essential_coefficients(self): + for i in range(len(self.cert["terms"])): + bad = copy.deepcopy(self.cert) + bad["terms"][i][3] = str(-verify.Q(bad["terms"][i][3])) + with self.subTest(term=i), self.assertRaisesRegex(ValueError, "right inverse"): + verify.verify_witness(self.trace, bad) + + def test_contact_and_own_target(self): + for checker in (verify.run, independent.run): + bad = copy.deepcopy(self.cert) + bad["terms"][0][1] = 4058 + with self.assertRaisesRegex(ValueError, "contact.*frame|chart contact"): + checker(self.data, bad) + bad["terms"][0][1] = 0 + bad["terms"][0][2] = "Y0" + with self.assertRaisesRegex(ValueError, "live.*register"): + checker(self.data, bad) + + def test_arbitrary_dirty_endpoints(self): + for event in (0, 4057): + data = copy.deepcopy(self.data) + data["LOWRANK-WITNESS.json"]["program"][event][3] = "0" + for checker in (verify.run, independent.run): + with self.subTest(event=event, checker=checker.__module__), \ + self.assertRaisesRegex(ValueError, "endpoint"): + checker(data, self.cert) + + def test_geometry_and_rank_guards(self): + data = copy.deepcopy(self.data) + data["P104-FIXTURE.json"]["section4_explicit_P104"]["F0"].pop() + for checker in (verify.run, independent.run): + with self.assertRaisesRegex(ValueError, "puncture|root enumeration"): + checker(data, self.cert) + data = copy.deepcopy(self.data) + event = next(e for e in data["LOWRANK-WITNESS.json"]["program"] if e[0] == "transport") + event[4] += 1 + for checker in (verify.run, independent.run): + with self.assertRaisesRegex(ValueError, "rank"): + checker(data, self.cert) + + def test_frame_basis_order_positive(self): + data = copy.deepcopy(self.data) + word = data["LOWRANK-WITNESS.json"] + for key in ("initial_frames", "final_frames"): + for frame in word[key].values(): + frame.reverse() + for e in word["program"]: + indices = {"add": (4,), "transport": (2, 3), "copy": (3,), + "zero": (2,), "erase": (2,)}[e[0]] + for i in indices: + e[i].reverse() + for checker in (verify.run, independent.run): + self.assertEqual(checker(data, self.cert), self.expected) + + def test_schema(self): + for field in (0, 1): + bad = copy.deepcopy(self.cert) + bad["terms"][0][field] = True + with self.assertRaisesRegex(ValueError, "index"): + certificate(bad) + bad = copy.deepcopy(self.cert) + bad["terms"].append(bad["terms"][0]) + with self.assertRaisesRegex(ValueError, "duplicate contact"): + certificate(bad) + with tempfile.TemporaryDirectory() as temp: + path = Path(temp) / "bad.json" + for raw in ('{"a":1,"a":2}', '{"a":NaN}'): + path.write_text(raw) + with self.assertRaises(ValueError): + read(path) + + def test_source_export_and_receipt(self): + with tempfile.TemporaryDirectory() as temp: + root = Path(temp) + package = root / "research/p104-minimum-shared-space" + shutil.copytree(HERE, package, ignore=shutil.ignore_patterns("__pycache__")) + pins = [p for p in read(HERE / "SOURCES.json")["files"] if p["usage"] == "input"] + for pin in pins: + dest = root / pin["path"] + dest.parent.mkdir(parents=True, exist_ok=True) + shutil.copyfile(REPO / pin["path"], dest) + saved = {p: p.read_bytes() for p in root.rglob("*") if p.is_file()} + for path in saved: + path.chmod(0o444) + for checker in ("verify.py", "independent.py"): + command = [sys.executable, "-I", "-O", "-B", str(package / checker)] + result = subprocess.run(command, cwd=root, capture_output=True, text=True, timeout=90) + self.assertEqual(result.returncode, 0, result.stderr) + self.assertIn("minimum=96", result.stdout) + result = subprocess.run(command + ["--out", str(package / "RESULT.json")], + capture_output=True, text=True, timeout=90) + self.assertNotEqual(result.returncode, 0) + self.assertIn("output already exists", result.stderr) + self.assertEqual(saved, {p: p.read_bytes() for p in root.rglob("*") if p.is_file()}) + bad_source = root / pins[0]["path"] + bad_source.chmod(0o644) + bad_source.write_bytes(bad_source.read_bytes() + b" ") + with self.assertRaisesRegex(ValueError, "source bytes changed"): + sources(root) + # Independently mutate the expected result without changing any input. + for p, raw in saved.items(): + p.chmod(0o644) + p.write_bytes(raw) + receipt = dict(self.expected, minimum_dimension=95) + (package / "RESULT.json").write_text(json.dumps(receipt)) + result = subprocess.run([sys.executable, "-I", "-O", "-B", str(package / "independent.py")], + capture_output=True, text=True, timeout=90) + self.assertNotEqual(result.returncode, 0) + self.assertIn("receipt differs", result.stderr) + + +if __name__ == "__main__": + unittest.main(verbosity=2) diff --git a/research/p104-minimum-shared-space/verify.py b/research/p104-minimum-shared-space/verify.py new file mode 100644 index 0000000000..96e24a6c50 --- /dev/null +++ b/research/p104-minimum-shared-space/verify.py @@ -0,0 +1,251 @@ +"""Sparse rational replay at all cuts and projector certificate acceptance. + +No predecessor checker or optimizer is imported. +Gareth Davidson with OpenAI Codex assistance. Apache-2.0. +""" +from collections import Counter, defaultdict +from fractions import Fraction as Q +from itertools import combinations, product +from pathlib import Path +import sys + +sys.path.insert(0, str(Path(__file__).resolve().parent)) +from common import HERE, certificate, cli, digest, need, read, sources + + +def basis(frame): + pivots = {} + for value in frame: + need(type(value) is int and 0 < value < 512, "binary frame value") + while value: + bit = value.bit_length() - 1 + if bit in pivots: + value ^= pivots[bit] + else: + pivots[bit] = value + break + need(len(pivots) == len(frame), "dependent frame") + for bit in sorted(pivots): + for other in pivots: + if other > bit and pivots[other] >> bit & 1: + pivots[other] ^= pivots[bit] + return tuple(pivots[bit] for bit in sorted(pivots)) + + +def contained(left, right): + pivots = {v.bit_length() - 1: v for v in right} + for value in left: + while value: + bit = value.bit_length() - 1 + if bit not in pivots: + return False + value ^= pivots[bit] + return True + + +def roots(fixture): + result = set() + for i, j in combinations(range(8), 2): + for sign in (-1, 1): + row = [0] * 8 + row[i], row[j] = 2, 2 * sign + result.add(tuple(row)) + for signs in product((-1, 1), repeat=7): + if signs.count(-1) % 2 == 0: + result.add((1, *signs)) + removed = {tuple(r) for r in fixture["F0"] + fixture["C"]} + need(len(result) == 120 and len(removed) == 16 and removed <= result, + "P104 puncture binding") + ports = sorted(result - removed) + need(all(sum(p[i] * p[j] for p in ports) == 104 * (i == j) + for i in range(8) for j in range(8)), "R R^T = 104 I") + return ports + + +def insert(pivots, source): + row = {i: Q(v) for i, v in source.items() if v} + while row: + pivot = min(row) + factor = row[pivot] + if pivot not in pivots: + pivots[pivot] = {j: v / factor for j, v in row.items()} + return True + for j, value in pivots[pivot].items(): + new = row.get(j, Q(0)) - factor * value + if new: + row[j] = new + else: + row.pop(j, None) + return False + + +def replay(data, terms): + word = data["LOWRANK-WITNESS.json"] + ports = roots(data["P104-FIXTURE.json"]["section4_explicit_P104"]) + names = list(word["initial_frames"]) + need(len(names) == len(set(names)) == 280 and + names[:104] == ["X" + str(t) for t in range(104)], "boundary names") + need({n for n in names if n.startswith("Y")} == + {"Y" + str(t) for t in range(104)}, "104 targets") + state = {n: {j: Q(1)} for j, n in enumerate(names)} + frames = {n: basis(f) for n, f in word["initial_frames"].items()} + pools = [set() for _ in range(104)] + identities, rows, occurrences = {}, [], [{} for _ in range(104)] + requested = defaultdict(list) + for index, (target, cut, reg, weight) in enumerate(terms): + requested[cut].append((index, target, reg)) + contacts = {} + + def capture(cut): + groups = defaultdict(list) + for name, frame in frames.items(): + groups[frame].append(name) + for group in groups.values(): + targets = [int(n[1:]) for n in group if n.startswith("Y")] + if not targets: + continue + group_rows = {} + for name in group: + row = tuple(sorted(state[name].items())) + if row not in identities: + identities[row] = len(rows) + rows.append(row) + group_rows[name] = identities[row] + for target in targets: + for name, row_id in group_rows.items(): + if name != "Y" + str(target): + pools[target].add(row_id) + occurrences[target].setdefault(row_id, (cut, name)) + for index, target, reg in requested[cut]: + need(reg in state and reg != "Y" + str(target), "live other register") + need(frames[reg] == frames["Y" + str(target)], "certificate chart contact") + contacts[index] = tuple(sorted(state[reg].items())) + + profile, scalar = Counter(), Counter() + capture(0) + need(len(word["program"]) == 4058, "fixed word length") + for index, event in enumerate(word["program"]): + op, reg = event[:2] + if op == "transport": + _, _, old, new, rank = event + old, new = basis(old), basis(new) + need(reg in frames and frames[reg] == old, "transport entry") + need(contained(old, new) or contained(new, old), "nested transport") + need(type(rank) is int and rank == abs(len(old) - len(new)) > 0, + "transport rank") + frames[reg] = new + profile[rank] += 1 + elif op == "add": + _, _, src, factor, frame = event + need(reg != src and frames[reg] == frames[src] == basis(frame), "ADD common chart") + for col, value in state[src].items(): + new = state[reg].get(col, Q(0)) + Q(factor) * value + if new: + state[reg][col] = new + else: + state[reg].pop(col, None) + scalar[op] += 1 + elif op == "zero": + need(reg == "C" and reg not in state, "private allocation") + state[reg], frames[reg] = {}, basis(event[2]) + scalar[op] += 1 + elif op == "copy": + need(reg == "C" and not state[reg] and + frames[reg] == frames[event[2]] == basis(event[3]), "private COPY") + state[reg] = dict(state[event[2]]) + scalar[op] += 1 + elif op == "erase": + need(reg == "C" and frames[reg] == basis(event[2]), "private discard") + del state[reg], frames[reg] + scalar[op] += 1 + else: + raise ValueError("unknown event") + capture(index + 1) + need(set(state) == set(names), "private storage closed") + for col, name in enumerate(names): + wanted = {col: Q(1)} + if name.startswith("Y"): + target = int(name[1:]) + for j, port in enumerate(ports): + value = Q(sum(x * y for x, y in zip(ports[target], port)), 8) + if value: + wanted[j] = value + need(state[name] == wanted, "all-input endpoint " + name) + need(frames[name] == basis(word["final_frames"][name]), "endpoint frame") + native = data["LOWRANK-RESULT.json"] + need(dict(profile) == {int(k): v for k, v in native["paid_profile"].items()} + and sum(k * v for k, v in profile.items()) == 2368, "inherited invoice") + coefficients = [] + for row in rows: + xx = {j: v for j, v in row if j < 104} + coeff = [sum((v * ports[j][k] for j, v in xx.items()), Q(0)) / 104 + for k in range(8)] + need(all(sum(coeff[k] * ports[j][k] for k in range(8)) == xx.get(j, 0) + for j in range(104)), "every pooled X row lies in row(R)") + coefficients.append(coeff) + dimensions, local_bases = [], [] + for target, pool in enumerate(pools): + missing = names.index("Y" + str(target)) + need(all(identities[((j, Q(1)),)] in pool + for j in range(104, 280) if j != missing), "initial dirty units") + need(all(not dict(rows[r]).get(missing) for r in pool), "own Y excluded") + pivots, chosen = {}, [] + for row_id in sorted(pool): + if insert(pivots, dict(enumerate(coefficients[row_id]))): + chosen.append(row_id) + dimensions.append(len(pivots)) + local_bases.append(chosen) + return dict(ports=ports, names=names, rows=rows, pools=pools, + coefficients=coefficients, contacts=contacts, + dimensions=dimensions, occurrences=occurrences, + local_bases=local_bases, scalar=dict(scalar), profile=dict(profile)) + + +def verify_witness(trace, cert): + A = [[Q(0)] * 8 for _ in range(104)] + for index, (target, cut, reg, weight) in enumerate(cert["terms"]): + weight = Q(weight) + need(weight and str(weight) == cert["terms"][index][3], "canonical weight") + row = trace["contacts"][index] + coeff = [sum((v * trace["ports"][j][k] for j, v in row if j < 104), Q(0)) / 104 + for k in range(8)] + for k in range(8): + A[target][k] += weight * coeff[k] + ports = trace["ports"] + need(all(sum(ports[t][i] * A[t][j] for t in range(104)) == int(i == j) + for i in range(8) for j in range(8)), "right inverse R A = I") + C = [[Q(int(t == j)) - Q(sum(x * y for x, y in zip(ports[t], ports[j])), 8) + for j in range(104)] for t in range(104)] + H = [[C[t][j] + 12 * sum(A[t][k] * ports[j][k] for k in range(8)) + for j in range(104)] for t in range(104)] + pivots = {} + for row in H: + insert(pivots, dict(enumerate(row))) + need(len(pivots) == 96, "explicit H rank") + # Right multiplication by C changes the kernel: C^-1 A = A - R^T/96. + need(all(sum(H[t][j] * (A[j][k] - Q(ports[j][k], 96)) for j in range(104)) == 0 + for t in range(104) for k in range(8)), "explicit eight-column kernel") + return A, H + + +def run(data=None, cert=None): + data = sources() if data is None else data + cert = certificate(read(HERE / "WITNESS.json") if cert is None else cert) + trace = replay(data, cert["terms"]) + A, H = verify_witness(trace, cert) + return {"schema": "p104-minimum-shared-space/1", "minimum_dimension": 96, + "targets": 104, "arbitrary_input_columns": 280, "cuts": 4059, + "captured_snapshot_rows": len(trace["rows"]), + "pooled_x_rank_histogram": {str(k): v for k, v in sorted(Counter(trace["dimensions"]).items())}, + "pool_sizes": list(map(len, trace["pools"])), + "certificate_terms": len(cert["terms"]), + "nonzero_A_rows": sum(any(row) for row in A), + "A_sha256": digest([[str(x) for x in row] for row in A]), + "H_sha256": digest([[str(x) for x in row] for row in H]), + "original_paid_profile": {str(k): v for k, v in sorted(trace["profile"].items())}, + "original_scalar_events": trace["scalar"], + "scope": "Exact algebraic pooled-span minimum only; no chronological producer, transport price, supplier or new kappa."} + + +if __name__ == "__main__": + cli(run, "PASS_P104_MINIMUM_SHARED_SPACE")