diff --git a/research/p104-prefix-minrank/README.md b/research/p104-prefix-minrank/README.md new file mode 100644 index 0000000000..f9ce345f3e --- /dev/null +++ b/research/p104-prefix-minrank/README.md @@ -0,0 +1,203 @@ +# Exact early-prefix dimensions for the P104 pooled correction + +The rational shared correction dimension for the unchanged P104 trace is: + +| Completed original events `c` | Exact minimum `h(c)` | +|---|---:| +| 0–2525 | 104 | +| 2526–2555 | 103 | +| 2556–2571 | 102 | +| 2572–2617 | 101 | +| 2618–2645 | 100 | +| 2646–2717 | 99 | + +This answers an early-prefix part of the open question in +[the prefix-boundary handoff](https://github.com/CrocSwap/integer-mult-bounds/discussions/2245#discussioncomment-18940216). +It also gives an exact eight-dimensional minimum-rank formulation for any +prefix satisfying the checked lifting hypotheses. The earlier +[PR #2251](https://github.com/CrocSwap/integer-mult-bounds/pull/2251) establishes +the full-pool minimum 96; the handoff reports 97 on 2824–2911 and 96 from 2912. +Those late-prefix results are credited, not independently recertified here. + +**No chronological correction circuit or paid transport saving follows.** +The model pools snapshots from different times and permits arbitrary new +rational shared directions for free. It does not construct, transport, host +or restore those directions. No new supplier, exponent or selected result is +proposed. Cuts 2718–2823 are deliberately left unresolved in this package. + +## Model and immutable inputs + +Use Rohan Arun's 4,058-event PR #1972 channel, as frozen by Chafik Boukhalfa's +native PR #1991. A cut counts completed events, so cut zero is the initial +state. There are 104 source inputs `X`, 104 target inputs `Y` and 72 arbitrary +dirty helper inputs. For each target `t`, set + +``` +S_t(c) = span_Q { v_r(d) : 0 <= d <= c, r != Y_t, + frame(r,d) = frame(Y_t,d) as binary subspaces }. +``` + +Here `v_r(d)` is the logical row in the **unchanged original trace**. No added +row is fed back into that trace. Basis changes inside a binary frame are free +in this pooled model. Let `R` be the 8-by-104 doubled root-coordinate matrix, +`C = I_104 - R^T R/8`, and define `h(c)` as the least dimension of a rational +space `H` in all 280 boundary coordinates with `C_t in S_t(c)+H` for every `t`. +All coefficient fields in the result are **Q**. We make no assertion equating +constrained rational minimum rank with real or complex minimum rank. + +[SOURCES.json](SOURCES.json) pins the two actual JSON inputs by Git blob and +SHA-256 at main `0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2`. The input witness +hash is `0f541bef7f19fdeffd67157684e9f03d785f42c89973632f508fc1a0452b580e`. +No pending predecessor program is imported; frozen packages are unchanged. + +## Exact reduction, including arbitrary dirty components + +The checker reconstructs the roots and verifies `R R^T = 104 I_8`. Hence +`C` is invertible, with inverse `I_104-R^T R/96`, and `R C = -12 R`. +It checks the following facts against **every** original cut: + +1. Every eligible snapshot's source projection lies in `row(R)`. +2. At cut zero all 175 non-source coordinate units other than `Y_t` are + available to target `t` in the zero frame. +3. No eligible snapshot contains its own target input `Y_t`. + +Write `pi_X` for projection to the source coordinates. Facts 2–3 let us subtract +the entire nuisance part of any eligible row using available initial units. +Therefore `pi_X(S_t(c)) = S_t(c) intersect X`. This lifting equality is needed: +projection containment alone does not justify replacing a shared space with +dirty components by a source-only space. The control suite gives two small +counterexamples when either lifting premise is dropped. + +Define `L_t(c) = { a in Q^8 : a R in S_t(c) intersect X }`. Any serving `H` +gives rows `C_t-s_t in H`; projecting them yields a serving source-only space +of dimension at most `dim H`. Conversely a source-only space is an allowed +full-space choice. Thus the two minima agree, and choosing one local row per +target gives exactly + +``` +h(c) = min_{B_t in L_t(c)} rank(C - B R). +``` + +The residual row span attains each candidate rank. A minimum exists because +the possible ranks form a nonempty finite set of integers. Since each `L_t` +is a linear space, substitute `B=-12 A`. With `D=R^T/8-12 A`, the residual +is `I_104-D R`. The maps `R` and `D` restrict to mutually inverse maps between +`ker(I_104-D R)` and `ker(I_8-R D)`: if `x=D R x`, then `R x=R D R x`, and +conversely `z=R D z` gives `D z=D R D z`. These are kernel isomorphisms, not +claims that either rectangular map is globally injective. Since +`R D=13 I_8-12 R A`, rank-nullity gives + +``` +h(c) = 96 + min_{A_t in L_t(c)} rank(I_8 - R A). (1) +``` + +Let `E(c)=span_Q { r_t a : a in L_t(c) }` be the space of 8-by-8 matrices, +where `r_t` is column `t` of `R` and `a` is a row. The matrices `R A` are +exactly `E(c)`; row choices for distinct targets are independent. + +## A linear test that certifies the early staircase + +Let `U(c)` be the union span of all coefficient rows in all `L_t(c)`, of +dimension `r`, and also use `U` for any full-row-rank basis matrix. Every +`M in E(c)` has row space contained in `U`. Therefore `M z=0` on `ker U`, +so `I-M` fixes that `(8-r)`-dimensional space pointwise: + +``` +rank(I-M) >= 8-r. +``` + +Equality holds **if and only if** `U M=U`. For necessity, equality forces +`image(I-M)=ker U`, so `U(I-M)=0`. For sufficiency, this identity puts the +image inside `ker U`, while the fixed-point property supplies the reverse +inclusion. Thus feasibility of `U M=U`, `M in E(c)`, is an ordinary rational +linear-system question. Infeasibility strengthens `h(c)>=104-r` by one. + +The verifier reconstructs every distinct eligible source projection through +cut 2717, forms `U` and `E`, and checks exact coefficient/augmented ranks at +the following right endpoints: + +| Cut | `rank U` | `dim E` | `U M=U` feasible | Certified lower `h` | +|---:|---:|---:|:---:|---:| +| 2525 | 0 | 0 | yes | 104 | +| 2555 | 2 | 8 | no | 103 | +| 2571 | 2 | 13 | yes | 102 | +| 2617 | 4 | 27 | no | 101 | +| 2645 | 5 | 33 | no | 100 | +| 2717 | 6 | 45 | no | 99 | + +[WITNESS.json](WITNESS.json) supplies respectively 1, 4, 6, 14 and 18 weighted +contacts at the five nontrivial **left** endpoints. A contact +`[target, cut, register, weight]` contributes its source coefficient +`weight * pi_X(v_register(cut)) R^T/104` to the corresponding row of `A`. +Each contact's availability and every dirty-input lifting premise are replayed. +The checker computes the exact rank both of `I_8-R A` and of the actual +104-by-104 matrix `K=C+12 A R`. Their ranks agree with (1); `row(K)` is a +serving space because `K_t-C_t` lies in `S_t(c)`. + +The source-only 104-dimensional space is the trivial first upper witness. +Pools grow with the prefix, so `h(c)` is nonincreasing. Matching a left-end +upper bound to a right-end lower bound certifies every cut in each interval. +This is not a floating-point or finite-field search inference. + +## Reproduce and inspect + +Standard-library Python, read-only by default; the registered runner uses 3.12: + +```sh +python3.12 -I -O -B research/p104-prefix-minrank/verify.py +python3.12 -I -O -B research/p104-prefix-minrank/test_verify.py +python3.12 scripts/research_package.py --package research/p104-prefix-minrank +``` + +Expected primary output: `PASS_P104_EARLY_PREFIX_MINRANK intervals=6 cuts=4059 columns=280`. +[RESULT.json](RESULT.json) is compared in full, including the six bounds, +110,814 distinct target/snapshot pairs and unchanged local profile. The dense +replay checks 280 independent columns on a checked denominator-eight integer +lattice, all frame transitions, owned private lifetimes, source/dirty helper +restoration and the original `G/2` endpoint. This is an algebraic trace replay; +it does not rerun the predecessor's native Clifford recipes. + +`build.py --out NEW.json` optionally regenerates the contact certificate using +an independently written eight-coordinate rational projection search. It +imports no mathematical routines from the acceptance verifier. Its output must +equal `WITNESS.json`; it alone is not a check of arbitrary dirty inputs. +All output options refuse to replace an existing file. + +Controls cover incorrect contact coefficients, unavailable/self or future +contacts, wrong paid rank, missing initial compensation and final cleanup, +the rectangular rank identity, and failures of both lifting hypotheses. +Checks use explicit exceptions/unittest assertions and run with `-O`. + +## Open next questions + +- **Resolve cuts 2718–2823.** Apply (1) to the exact small operator spaces. + The one-step projector obstruction may leave a gap; seek rank-one/two + residual certificates or stronger dual obstructions. This would complete + the interval before the predecessor's `h=97` result at 2824. The blocker + is constrained rational minimum rank, not another root/Gram calculation. +- **Realize an affordable chronological correction.** Choose a serving space + and provide actual creation, frame paths, source reads, dirty restoration, + owner scheduling and a complete recursive invoice. A dimension such as 99 + or 96 cannot be substituted for a paid transport count. Fixed-path + obstructions and precision/all-size obligations remain applicable. + +## Credit and scope + +Gonzalo Mier / #2173 supplied the pooled-snapshot model and lower96/upper97 +question. Gareth Davidson (@bitplane) / #2251 supplied the rational complement +construction and full-pool minimum96. The prefix-boundary handoff by @josecarlosgonzalezroque-design at +Discussion #2245 comment 18940216 supplied the prefix formulation, earliest96 +cut and 97 interval, and explicitly left earlier prefixes open. This package +extends that algebraic problem; it does not claim their model, 96 lower bound, +or late-prefix result as new. + +Rohan Arun / #1972 supplied the scalar/frame channel; Chafik Boukhalfa / #1991 +its native realization; Adam Gall / #1940 the schedule; Josie Elliston / #1071 +the fixture, with Ali Romman / #1125 and their retained geometry/decoder +lineage. Their original files and notices are unchanged. + +AAAmirinu with substantial OpenAI Codex assistance in mathematics, code, +checking and writing, including separate AI-assisted exploration and proof +review. Evidence is author-checked, not independent human review or formal +proof-assistant verification. Apache-2.0. No native regeneration, global +hosting/moment, precision/all-size proof or selected cold replay is claimed. diff --git a/research/p104-prefix-minrank/RESULT.json b/research/p104-prefix-minrank/RESULT.json new file mode 100644 index 0000000000..fa5fcbd4da --- /dev/null +++ b/research/p104-prefix-minrank/RESULT.json @@ -0,0 +1,68 @@ +{ + "schema": "p104-prefix-minrank-result/1", + "status": "PASS_P104_EARLY_PREFIX_MINRANK", + "cuts_replayed": 4059, + "boundary_columns": 280, + "distinct_target_snapshots": 110814, + "intervals": [ + { + "start": 0, + "end": 2525, + "minimum": 104, + "union_rank_at_end": 0, + "operator_rank_at_end": 0, + "projector_feasible_at_end": true + }, + { + "start": 2526, + "end": 2555, + "minimum": 103, + "union_rank_at_end": 2, + "operator_rank_at_end": 8, + "projector_feasible_at_end": false + }, + { + "start": 2556, + "end": 2571, + "minimum": 102, + "union_rank_at_end": 2, + "operator_rank_at_end": 13, + "projector_feasible_at_end": true + }, + { + "start": 2572, + "end": 2617, + "minimum": 101, + "union_rank_at_end": 4, + "operator_rank_at_end": 27, + "projector_feasible_at_end": false + }, + { + "start": 2618, + "end": 2645, + "minimum": 100, + "union_rank_at_end": 5, + "operator_rank_at_end": 33, + "projector_feasible_at_end": false + }, + { + "start": 2646, + "end": 2717, + "minimum": 99, + "union_rank_at_end": 6, + "operator_rank_at_end": 45, + "projector_feasible_at_end": false + } + ], + "local_profile": { + "1": 1074, + "2": 58, + "3": 86, + "4": 104, + "5": 48, + "6": 24, + "7": 8, + "8": 8 + }, + "scope": "Rational unchanged-trace pooled snapshots only; no chronological correction or paid cost result." +} diff --git a/research/p104-prefix-minrank/SOURCES.json b/research/p104-prefix-minrank/SOURCES.json new file mode 100644 index 0000000000..3bb2451581 --- /dev/null +++ b/research/p104-prefix-minrank/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "e8870e5917057d59b730eb14721a778639eca050", + "sha256": "d46eb6d5b3e279428753d770653663fbdf1063e55c255ea073d768f344927ef7" + }, + { + "path": "research/p104-native-channel/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" + } + ] +} diff --git a/research/p104-prefix-minrank/TASK.json b/research/p104-prefix-minrank/TASK.json new file mode 100644 index 0000000000..727d7e6130 --- /dev/null +++ b/research/p104-prefix-minrank/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 rational shared correction dimensions at unchanged-trace pooled prefixes 0..2717, via an eight-dimensional affine minimum-rank reduction.", + "scope_change_reason": "Take the explicit early-prefix algebraic handoff in Discussion2245 comment18940216. This is a relaxation of chronological side correction and does not meet the complete supplier gate.", + "bottleneck_link": "Bounds the information space required before chosen P104 correction cuts; avoids mistaking pooled access for a chronological implementation or dimension for paid rank.", + "budget_minutes": 60, + "stop_rule": "Certify matching exact upper/lower dimensions for prefixes through2717; leave later constrained-minimum-rank and chronological realization open.", + "outcome": "completed", + "evidence": "RESULT.json and WITNESS.json: six exact intervals; all4059 cuts and280 input columns; independently generated contacts and full dense acceptance replay.", + "author": "AAAmirinu", + "ai_assistance": "Substantial OpenAI Codex assistance, including delegated source-projection exploration and separate mathematical proof review; no independent human review.", + "open_questions": [ + { + "question": "What are exact h(c) on cuts2718..2823?", + "why_it_matters": "Completes the gap before the reported h=97 late-prefix interval.", + "first_step": "Use the pinned trace to derive the small operator spaces and seek rank-one/two residual witnesses with matching lower certificates.", + "blocked_by": "Constrained rational minimum rank may require stronger obstructions than the projector test." + }, + { + "question": "Can a shared complement be realized with favorable complete chronological cost?", + "why_it_matters": "Pooled dimension alone is not a completed P104 supplier.", + "first_step": "Construct and charge creation, source reads, native frames, restoration and chronological hosting for one complement.", + "blocked_by": "No priced chronological producer or precision/all-size admission." + } + ], + "assignment": { + "nonce": "04b2bbe7a3fb0b4faf78715dbf6ffb24", + "track": "complex-mechanisms", + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/2245#discussioncomment-18941843" + }, + "overlap": { + "entry_utc": "2026-10-15T05:48:20.130660+00:00", + "open_prs": 546, + "discussion_records": 1053, + "complete_pagination": true, + "warnings": [], + "nearest": [ + "#2173", + "#2251", + "Discussion2245 comment18940216" + ], + "limits": "Bodies/comments/local notes, not all code diffs; metadata matches do not prove novelty." + }, + "predecessors": [ + { + "pr": 2173, + "head": "d9b784ca86fba060f0264370536ccd322c89998a", + "author": "Gonzalo Mier", + "contribution": "Pooled-span model and shared dimension96..97." + }, + { + "pr": 2251, + "head": "822bceef780d8da9605798f0836ae5320e8e291e", + "author": "Gareth Davidson / bitplane", + "contribution": "Full-pool minimum96 and complement construction." + }, + { + "url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/2245#discussioncomment-18940216", + "author": "josecarlosgonzalezroque-design", + "updated_at": "2026-10-15T04:01:08Z", + "contribution": "Prefix model, sharp late96/97 boundary and earlier-prefix handoff." + } + ], + "freshness": { + "checked_utc": "2026-10-15T06:02:04.599866+00:00", + "canonical_main": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "priority_revision": 4, + "relevant_upstream_changes": false, + "final_overlap_utc": "2026-10-15T06:00:37.201126+00:00", + "open_prs": 553, + "discussion_records": 1063, + "complete_pagination": true, + "warnings": [], + "adjacent_active_claims": [ + "EdDiboi:chronological lift of the41-contact complement, comment18941894", + "kumagi:fixed-frame relay-floor audit, comment18941961" + ], + "distinction": "This package proves rational early pooled-prefix dimensions, not either adjacent chronological interface." + }, + "validation": { + "python": "CPython3.12.11 native Windows", + "primary_command": "python3.12 -I -O -B research/p104-prefix-minrank/verify.py", + "primary_seconds": 48.465, + "controls_command": "python3.12 -B -O research/p104-prefix-minrank/test_verify.py", + "controls_tests": 11, + "controls_seconds": 182.396, + "controls_result": "OK", + "generator": "Optimized independent generator exactly reproduced WITNESS.json; existing-output refusal passed.", + "package_metadata": "PASS_PACKAGE_METADATA_AND_PINS", + "unrun": [ + "native Clifford regeneration", + "global hosting/moment", + "precision/all-size admission", + "selected cold replay", + "source-export runtime", + "hosted CI at submission" + ] + } +} diff --git a/research/p104-prefix-minrank/VERIFY.json b/research/p104-prefix-minrank/VERIFY.json new file mode 100644 index 0000000000..ba5fe45f7c --- /dev/null +++ b/research/p104-prefix-minrank/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/p104-native-channel/inputs/LOWRANK-WITNESS.json", + "research/p104-native-channel/inputs/P104-FIXTURE.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 300, + "checks": "All4059 cuts and280 columns; exact early-prefix lower/upper certificates; source pins and full expected receipt." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/test_verify.py" + ], + "timeout_seconds": 600, + "checks": "Semantic coefficient, contact, compensation, cleanup, rank and lifting-premise controls." + } + ] +} diff --git a/research/p104-prefix-minrank/WITNESS.json b/research/p104-prefix-minrank/WITNESS.json new file mode 100644 index 0000000000..5f7b90f6c5 --- /dev/null +++ b/research/p104-prefix-minrank/WITNESS.json @@ -0,0 +1,288 @@ +{ + "schema": "p104-prefix-minrank/1", + "witnesses": [ + { + "cut": 2526, + "terms": [ + [ + 7, + 2526, + "D5", + "1/2" + ] + ] + }, + { + "cut": 2556, + "terms": [ + [ + 7, + 2526, + "D5", + "1/2" + ], + [ + 13, + 2532, + "Y7", + "-2" + ], + [ + 14, + 2552, + "D8", + "-1/2" + ], + [ + 68, + 2556, + "Y14", + "2" + ] + ] + }, + { + "cut": 2572, + "terms": [ + [ + 7, + 2526, + "D5", + "-1/2" + ], + [ + 8, + 2528, + "Y7", + "4" + ], + [ + 13, + 2532, + "Y7", + "-2" + ], + [ + 14, + 2552, + "D8", + "-1/2" + ], + [ + 69, + 2558, + "Y14", + "2" + ], + [ + 0, + 2572, + "D12", + "-1/2" + ] + ] + }, + { + "cut": 2618, + "terms": [ + [ + 7, + 2526, + "D5", + "-1/2" + ], + [ + 8, + 2528, + "Y7", + "4" + ], + [ + 15, + 2534, + "Y7", + "2" + ], + [ + 14, + 2552, + "D8", + "-1/2" + ], + [ + 66, + 2554, + "Y14", + "-2" + ], + [ + 69, + 2558, + "Y14", + "2" + ], + [ + 0, + 2572, + "D12", + "-1/4" + ], + [ + 6, + 2576, + "Y0", + "1" + ], + [ + 11, + 2578, + "Y0", + "1" + ], + [ + 19, + 2582, + "Y0", + "1" + ], + [ + 3, + 2604, + "D16", + "1/2" + ], + [ + 24, + 2608, + "Y3", + "2" + ], + [ + 32, + 2616, + "Y3", + "2" + ], + [ + 43, + 2618, + "Y3", + "2" + ] + ] + }, + { + "cut": 2646, + "terms": [ + [ + 7, + 2526, + "D5", + "-1/2" + ], + [ + 8, + 2528, + "Y7", + "2" + ], + [ + 10, + 2530, + "Y7", + "2" + ], + [ + 15, + 2534, + "Y7", + "2" + ], + [ + 14, + 2552, + "D8", + "-1/2" + ], + [ + 66, + 2554, + "Y14", + "-2" + ], + [ + 70, + 2560, + "Y14", + "2" + ], + [ + 0, + 2572, + "D12", + "-3/4" + ], + [ + 2, + 2574, + "Y0", + "-2" + ], + [ + 6, + 2576, + "Y0", + "1" + ], + [ + 11, + 2578, + "Y0", + "1" + ], + [ + 19, + 2582, + "Y0", + "1" + ], + [ + 5, + 2606, + "Y3", + "2" + ], + [ + 24, + 2608, + "Y3", + "2" + ], + [ + 32, + 2616, + "Y3", + "2" + ], + [ + 43, + 2618, + "Y3", + "2" + ], + [ + 22, + 2638, + "D20", + "-1/2" + ], + [ + 31, + 2646, + "Y22", + "2" + ] + ] + } + ] +} diff --git a/research/p104-prefix-minrank/build.py b/research/p104-prefix-minrank/build.py new file mode 100644 index 0000000000..9410d525f2 --- /dev/null +++ b/research/p104-prefix-minrank/build.py @@ -0,0 +1,230 @@ +"""Generate exact early-prefix contact candidates using source projections. + +This optional search does not import the acceptance checker. It tracks only +the eight coordinates x R^T; verify.py separately validates all 280 boundary +columns, availability, dirty cancellation, and the resulting rank claims. + +Rohan Arun / PR1972 supplies the frozen scalar/frame channel, retained by +Chafik Boukhalfa / PR1991. Adam Gall / PR1940 supplies the schedule and Josie +Elliston / PR1071 supplies the P104 fixture and retained decoder lineage. +The pooled-space model follows Gonzalo Mier / PR2173 and Gareth Davidson / +PR2251. New early-prefix generation was prepared for AAAmirinu with +substantial OpenAI Codex assistance. Apache-2.0. +""" + +import argparse +import hashlib +import json +from fractions import Fraction +from functools import lru_cache +from itertools import combinations, product +from pathlib import Path + + +HERE = Path(__file__).resolve().parent +UPPER_CUTS = (2526, 2556, 2572, 2618, 2646) +SOURCE_NAMES = ("LOWRANK-WITNESS.json", "P104-FIXTURE.json") + + +def load_sources(source_dir): + """Bind both inputs to this package's source manifest before calculation.""" + manifest = json.loads((HERE / "SOURCES.json").read_bytes()) + pins = {} + for entry in manifest["files"]: + if entry.get("usage") != "input": + continue + name = Path(entry["path"]).name + if name in SOURCE_NAMES: + if name in pins: + raise ValueError("duplicate input source pin: " + name) + pins[name] = entry["sha256"] + if set(pins) != set(SOURCE_NAMES): + raise ValueError("missing channel or fixture source pin") + + inputs = {} + for name in SOURCE_NAMES: + raw = (source_dir / name).read_bytes() + if hashlib.sha256(raw).hexdigest() != pins[name]: + raise ValueError("input source hash mismatch: " + name) + inputs[name] = json.loads(raw) + return inputs["LOWRANK-WITNESS.json"], inputs["P104-FIXTURE.json"] + + +def root_ports(fixture): + """Reconstruct the 104 doubled E8 roots without predecessor code.""" + lines = set() + for first, second in combinations(range(8), 2): + for sign in (-1, 1): + row = [0] * 8 + row[first], row[second] = 2, 2 * sign + lines.add(tuple(row)) + for tail in product((-1, 1), repeat=7): + if tail.count(-1) % 2 == 0: + lines.add((1, *tail)) + removed = {tuple(row) for row in fixture["F0"] + fixture["C"]} + if len(lines) != 120 or len(removed) != 16 or not removed <= lines: + raise ValueError("invalid P104 root fixture") + return sorted(lines - removed) + + +@lru_cache(maxsize=None) +def subspace(vectors): + values = {0} + for vector in vectors: + values |= {old ^ vector for old in tuple(values)} + return tuple(sorted(values)) + + +def insert_basis(basis, row): + """Insert one rational row while retaining deterministic pivot order.""" + row = list(row) + for pivot, previous in sorted(basis.items()): + coefficient = row[pivot] + if coefficient: + row = [x - coefficient * y for x, y in zip(row, previous)] + pivot = next((i for i, value in enumerate(row) if value), None) + if pivot is None: + return False + divisor = row[pivot] + basis[pivot] = [value / divisor for value in row] + return True + + +def solve(matrix, rhs): + """Return an exact solution with free variables zero, or None.""" + basis = {} + for row, target in zip(matrix, rhs): + augmented = list(row) + [target] + for pivot, previous in sorted(basis.items()): + coefficient = augmented[pivot] + if coefficient: + augmented = [x - coefficient * y + for x, y in zip(augmented, previous)] + pivot = next((i for i, value in enumerate(augmented[:-1]) if value), None) + if pivot is None: + if augmented[-1]: + return None + else: + divisor = augmented[pivot] + basis[pivot] = [value / divisor for value in augmented] + + answer = [Fraction(0)] * (len(matrix[0]) if matrix else 0) + for pivot, row in sorted(basis.items(), reverse=True): + answer[pivot] = row[-1] - sum( + x * y for x, y in zip(row[pivot + 1:-1], answer[pivot + 1:]) + ) + return answer + + +def projector_contacts(cut, roots, contacts, union_basis): + """Solve U M = U in the space spanned by captured rank-one operators.""" + operators = [ + [Fraction(value) * component for value in roots[target] + for component in projection] + for target, _, _, projection in contacts + ] + equations, rhs = [], [] + for row in union_basis.values(): + for column in range(8): + equations.append([ + sum(row[i] * operator[8 * i + column] for i in range(8)) + for operator in operators + ]) + rhs.append(row[column]) + solution = solve(equations, rhs) + if solution is None: + raise ValueError("no required projector solution at cut " + str(cut)) + + # Projections above are x R^T. Actual code coefficients are x R^T / 104, + # so these contact weights satisfy M = R A and K = C + 12 A R. + terms = [ + [target, contact_cut, register, str(104 * weight)] + for (target, contact_cut, register, _), weight in zip(contacts, solution) + if weight + ] + return {"cut": cut, "terms": terms} + + +def generate(channel, fixture): + roots = root_ports(fixture) + projections = { + name: ([Fraction(value) for value in roots[int(name[1:])]] + if name.startswith("X") else [Fraction(0)] * 8) + for name in channel["initial_frames"] + } + frames = {name: subspace(tuple(vectors)) + for name, vectors in channel["initial_frames"].items()} + pools = [set() for _ in roots] + operator_basis, union_basis = {}, {} + contacts, witnesses = [], [] + + def capture(cut): + groups = {} + for name, frame in frames.items(): + groups.setdefault(frame, []).append(name) + for names in groups.values(): + targets = [int(name[1:]) for name in names if name.startswith("Y")] + if not targets: + continue + nonzero = [(name, tuple(projections[name])) + for name in names if any(projections[name])] + for target in targets: + for name, projection in nonzero: + if name == "Y" + str(target) or projection in pools[target]: + continue + pools[target].add(projection) + insert_basis(union_basis, projection) + operator = [Fraction(value) * component + for value in roots[target] + for component in projection] + if insert_basis(operator_basis, operator): + contacts.append((target, cut, name, projection)) + if cut in UPPER_CUTS: + witnesses.append(projector_contacts(cut, roots, contacts, union_basis)) + + capture(0) + for index, event in enumerate(channel["program"][:max(UPPER_CUTS)]): + operation, name = event[:2] + if operation == "transport": + frames[name] = subspace(tuple(event[3])) + elif operation == "zero": + projections[name] = [Fraction(0)] * 8 + frames[name] = subspace(tuple(event[2])) + elif operation == "copy": + projections[name] = projections[event[2]][:] + elif operation == "erase": + del projections[name] + del frames[name] + elif operation == "add": + projections[name] = [ + x + Fraction(event[3]) * y + for x, y in zip(projections[name], projections[event[2]]) + ] + else: + raise ValueError("unknown channel operation: " + str(operation)) + capture(index + 1) + if tuple(witness["cut"] for witness in witnesses) != UPPER_CUTS: + raise ValueError("channel ended before every requested witness cut") + return {"schema": "p104-prefix-minrank/1", "witnesses": witnesses} + + +def main(): + parser = argparse.ArgumentParser( + description="Generate P104 prefix contacts; validate separately with verify.py." + ) + parser.add_argument("--source-dir", type=Path, + default=HERE.parent / "p104-native-channel" / "inputs") + parser.add_argument("--out", type=Path, required=True, + help="new output path; existing files are never overwritten") + args = parser.parse_args() + if args.out.exists(): + raise FileExistsError("output already exists: " + str(args.out)) + channel, fixture = load_sources(args.source_dir) + output = generate(channel, fixture["section4_explicit_P104"]) + with args.out.open("x", encoding="utf-8") as stream: + stream.write(json.dumps(output, indent=2) + "\n") + print("PASS_P104_EARLY_CONTACT_GENERATION", len(output["witnesses"]), "witnesses") + + +if __name__ == "__main__": + main() diff --git a/research/p104-prefix-minrank/test_verify.py b/research/p104-prefix-minrank/test_verify.py new file mode 100644 index 0000000000..5615b68b1c --- /dev/null +++ b/research/p104-prefix-minrank/test_verify.py @@ -0,0 +1,228 @@ +"""Exact positive fixtures and rejecting controls for the pooled-prefix audit. + +AAAmirinu with substantial OpenAI Codex assistance. Apache-2.0. +Run directly with Python 3.12; unittest assertions also remain active under -O. +Frozen inputs are read only. Trace mutations live in independent in-memory copies. +""" +from copy import deepcopy +from fractions import Fraction as Q +from importlib.util import module_from_spec, spec_from_file_location +from pathlib import Path +import unittest +from unittest.mock import patch + + +HERE = Path(__file__).resolve().parent +SPEC = spec_from_file_location("p104_prefix_minrank_verify", HERE / "verify.py") +verify = module_from_spec(SPEC) +SPEC.loader.exec_module(verify) + + +def exact_rank(rows): + """Independent small-matrix Gauss-Jordan oracle, not the verifier's basis code.""" + matrix = [[Q(value) for value in row] for row in rows] + if not matrix: + return 0 + width = len(matrix[0]) + if any(len(row) != width for row in matrix): + raise ValueError("ragged independent rank input") + next_row = 0 + for column in range(width): + pivot = next((i for i in range(next_row, len(matrix)) + if matrix[i][column]), None) + if pivot is None: + continue + matrix[next_row], matrix[pivot] = matrix[pivot], matrix[next_row] + scale = matrix[next_row][column] + matrix[next_row] = [value / scale for value in matrix[next_row]] + for i in range(len(matrix)): + if i != next_row: + scale = matrix[i][column] + matrix[i] = [a - scale * b + for a, b in zip(matrix[i], matrix[next_row])] + next_row += 1 + return next_row + + +def product(left, right): + return [[sum(a * b for a, b in zip(row, column)) + for column in zip(*right)] for row in left] + + +def identity(size): + return [[Q(i == j) for j in range(size)] for i in range(size)] + + +def subtract(left, right): + return [[a - b for a, b in zip(x, y)] for x, y in zip(left, right)] + + +def add(left, right): + return [a + b for a, b in zip(left, right)] + + +def scale(coefficient, vector): + return [coefficient * value for value in vector] + + +def in_span(vector, rows): + return exact_rank(rows + [vector]) == exact_rank(rows) + + +class AlgebraControls(unittest.TestCase): + def test_rectangular_rank_identity_and_noninjective_global_map(self): + # n=4, k=2, RR^T=2I and C=I-R^TR. The reparameterization factor is 1. + roots = [[1, 1, 0, 0], [0, 0, 1, 1]] + transpose = [list(column) for column in zip(*roots)] + correction = subtract(identity(4), product(transpose, roots)) + self.assertEqual(product(roots, transpose), [[2, 0], [0, 2]]) + self.assertEqual(exact_rank(correction), 4) + fixtures = [ + ([[0, 0]] * 4, 4, 2), + ([[1, 0], [0, 0], [0, 0], [0, 0]], 3, 1), + ([[Q(1, 2), 0], [Q(1, 2), 0], + [0, Q(1, 2)], [0, Q(1, 2)]], 2, 0), + (transpose, 4, 2), # U=R^T-A=0; global U injectivity is false. + ] + for coefficients, expected_large, expected_small in fixtures: + with self.subTest(coefficients=coefficients): + actual = [add(row, adjustment) for row, adjustment in + zip(correction, product(coefficients, roots))] + reduced = subtract(identity(2), product(roots, coefficients)) + self.assertEqual(exact_rank(actual), expected_large) + self.assertEqual(exact_rank(reduced), expected_small) + self.assertEqual(exact_rank(actual), 2 + exact_rank(reduced)) + self.assertEqual(verify.rank(actual), exact_rank(actual)) + self.assertEqual(verify.rank(reduced), exact_rank(reduced)) + kernel_vector = [[1], [-1], [0], [0]] + self.assertEqual(product(roots, kernel_vector), [[0], [0]]) + self.assertEqual(product(correction, kernel_vector), kernel_vector) + + def check_lifting_counterexample(self, spaces, shared, local_parts): + # Both targets have C=I-R^TR for R=(1,1); C is invertible. + size = len(shared) + pure_sources = identity(size)[:2] + targets = [[0, -1] + [0] * (size - 2), + [-1, 0] + [0] * (size - 2)] + root_code = [[1, 1]] + for space, local in zip(spaces, local_parts): + intersection_dimension = (exact_rank(space) + exact_rank(pure_sources) + - exact_rank(space + pure_sources)) + self.assertEqual(intersection_dimension, 0) + self.assertTrue(all(in_span(row[:2], root_code) for row in space)) + self.assertTrue(in_span(local, space)) + self.assertEqual(add(local_parts[0], shared), targets[0]) + self.assertEqual(add(local_parts[1], scale(-1, shared)), targets[1]) + self.assertEqual(exact_rank([shared]), 1) + self.assertEqual(exact_rank(targets), 2) + # h=0 is impossible even after source projection: c_1 is outside row(R). + self.assertFalse(in_span(targets[0][:2], root_code)) + # Pure intersections force A=0, so the inapplicable formula would give 2. + self.assertEqual(2 - 1 + exact_rank([[1]]), 2) + + def test_missing_dirty_unit_breaks_projection_lifting(self): + # Coordinates: X1,X2,Y1,Y2,z. No own-target dirt occurs, but z is not free. + first, second = [1, 1, 0, 0, 2], [1, 1, 0, 0, -2] + spaces = [[[0, 0, 0, 1, 0], first], + [[0, 0, 1, 0, 0], second]] + for target, space in enumerate(spaces): + self.assertTrue(all(row[2 + target] == 0 for row in space)) + self.assertFalse(in_span([0, 0, 0, 0, 1], space)) + self.check_lifting_counterexample( + spaces, [Q(1, 2), Q(-1, 2), 0, 0, 1], + [scale(Q(-1, 2), first), scale(Q(-1, 2), second)]) + + def test_own_target_dirt_breaks_projection_lifting(self): + # All nuisance units other than Y_t are available, but Y_t occurs mixed. + first, second = [1, 1, 2, 0], [1, 1, 0, -2] + spaces = [[[0, 0, 0, 1], first], [[0, 0, 1, 0], second]] + units = identity(4) + for target, space in enumerate(spaces): + self.assertTrue(in_span(units[3 - target], space)) + self.assertTrue(any(row[2 + target] != 0 for row in space)) + self.check_lifting_counterexample( + spaces, [Q(1, 2), Q(-1, 2), 1, 1], + [add(scale(Q(-1, 2), first), [0, 0, 0, -1]), + add(scale(Q(-1, 2), second), [0, 0, 1, 0])]) + + def test_extra_source_access_invalidates_common_code_floor(self): + # Dropping source-code containment allows local service with H=0. + first, second = [0, -1], [-1, 0] + self.assertEqual(exact_rank([first, second]), 2) + self.assertFalse(in_span(first, [[1, 1]])) + self.assertFalse(in_span(second, [[1, 1]])) + self.assertTrue(in_span(first, [first])) + self.assertTrue(in_span(second, [second])) + self.assertEqual(exact_rank([[0, 0], [0, 0]]), 0) + + +class FrozenTraceControls(unittest.TestCase): + @classmethod + def setUpClass(cls): + data = verify.sources() + cls.ports = verify.geometry(data['P104-FIXTURE.json']['section4_explicit_P104']) + cls.word = data['LOWRANK-WITNESS.json'] + cls.certificate = verify.read(HERE / 'WITNESS.json') + wanted = [tuple(term[:3]) for witness in cls.certificate['witnesses'] + for term in witness['terms']] + # All positive/contact tests share this exact source-bound trace replay. + cls.trace = verify.replay(cls.word, cls.ports, wanted) + + def test_positive_certificate_all_six_intervals(self): + with patch.object(verify, 'replay', return_value=self.trace) as replay: + result = verify.run(self.certificate) + replay.assert_called_once() + self.assertEqual(result['status'], 'PASS_P104_EARLY_PREFIX_MINRANK') + self.assertEqual([row['minimum'] for row in result['intervals']], + [104, 103, 102, 101, 100, 99]) + self.assertEqual(result['cuts_replayed'], 4059) + self.assertEqual(result['boundary_columns'], 280) + + def test_wrong_contact_sign_rejected_by_matching_bounds(self): + bad = deepcopy(self.certificate) + bad['witnesses'][0]['terms'][0][3] = '-1/2' + with patch.object(verify, 'replay', return_value=self.trace) as replay: + with self.assertRaisesRegex(ValueError, 'matching exact bounds'): + verify.run(bad) + replay.assert_called_once() + + def test_future_contact_rejected(self): + witness = deepcopy(self.certificate['witnesses'][0]) + witness['terms'][0][1] = witness['cut'] + 1 + with self.assertRaisesRegex(ValueError, 'future cut'): + verify.upper_bound(witness['terms'], self.trace[1], self.ports, + witness['cut']) + + def test_self_contact_excluded_by_actual_trace_replay(self): + # Replay the real trace with a requested own-target row. This tests the + # snapshot filter itself, not only an absent key in a hand-built mapping. + with self.assertRaisesRegex(ValueError, 'contact absent or self-contact'): + verify.replay(self.word, self.ports, [(7, 0, 'Y7')]) + + def test_missing_initial_query_compensation_rejected_at_endpoint(self): + bad = deepcopy(self.word) + self.assertEqual(bad['program'][0], ['add', 'Y0', 'Q0', '-1/4', []]) + bad['program'][0][3] = '0' + # Preserve all 4058 events and valid charts so this cannot pass merely + # by detecting a shortened program or a transport-profile mismatch. + with self.assertRaisesRegex(ValueError, 'arbitrary-input endpoint Y0'): + verify.replay(bad, self.ports) + + def test_missing_final_query_cleanup_rejected_at_endpoint(self): + bad = deepcopy(self.word) + self.assertEqual(bad['program'][-1][:4], ['add', 'Q7', 'X103', -2]) + bad['program'][-1][3] = '0' + with self.assertRaisesRegex(ValueError, 'arbitrary-input endpoint Q7'): + verify.replay(bad, self.ports) + + def test_invalid_paid_transport_rank_rejected(self): + bad = deepcopy(self.word) + first = next(event for event in bad['program'] if event[0] == 'transport') + self.assertEqual(first[-1], 3) + first[-1] = 4 + with self.assertRaisesRegex(ValueError, 'transport rank'): + verify.replay(bad, self.ports) + + +if __name__ == '__main__': + unittest.main(verbosity=2) diff --git a/research/p104-prefix-minrank/verify.py b/research/p104-prefix-minrank/verify.py new file mode 100644 index 0000000000..71cc7df145 --- /dev/null +++ b/research/p104-prefix-minrank/verify.py @@ -0,0 +1,287 @@ +"""Exact pooled-prefix audit; stdlib only, no predecessor checker imports. + +AAAmirinu with substantial OpenAI Codex assistance. Apache-2.0. +The proof in README.md supplies the universal implication; this checks its +source-bound premises and finite upper/lower certificates over Q. +""" +from collections import Counter, defaultdict +from fractions import Fraction as Q +from functools import lru_cache +from itertools import combinations, product +from pathlib import Path +import argparse +import hashlib +import json + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +INTERVALS = [(0, 2525, 104), (2526, 2555, 103), (2556, 2571, 102), + (2572, 2617, 101), (2618, 2645, 100), (2646, 2717, 99)] + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def unique(pairs): + answer = {} + for key, value in pairs: + need(key not in answer, 'duplicate JSON key') + answer[key] = value + return answer + + +def read(path): + return json.loads(path.read_bytes(), object_pairs_hook=unique) + + +def rank(rows): + basis = {} + for row in rows: + add_basis(basis, row) + return len(basis) + + +def add_basis(basis, row): + row = list(map(Q, row)) + for pivot, old in sorted(basis.items()): + coefficient = row[pivot] + if coefficient: + row = [x - coefficient * y for x, y in zip(row, old)] + pivot = next((i for i, value in enumerate(row) if value), None) + if pivot is None: + return False + divisor = row[pivot] + basis[pivot] = [x / divisor for x in row] + return True + + +def solvable(matrix, rhs): + return rank(matrix) == rank([list(row) + [value] + for row, value in zip(matrix, rhs)]) + + +@lru_cache(maxsize=None) +def frame(vectors): + values = {0} + for value in vectors: + need(type(value) is int and 0 < value < 512, 'binary frame vector') + values |= {value ^ old for old in tuple(values)} + need(len(values) == 2 ** len(vectors), 'independent binary frame basis') + return frozenset(values) + + +def geometry(fixture): + lines = set() + for first, second in combinations(range(8), 2): + for sign in [-1, 1]: + row = [0] * 8 + row[first], row[second] = 2, 2 * sign + lines.add(tuple(row)) + for tail in product([-1, 1], repeat=7): + if sum(x < 0 for x in tail) % 2 == 0: + lines.add((1, *tail)) + removed = {tuple(row) for row in fixture['F0'] + fixture['C']} + need(len(lines) == 120 and len(removed) == 16 and removed <= lines, + 'P104 punctured E8 fixture') + ports = sorted(lines - removed) + need(len(ports) == 104, '104 ports') + need(all(sum(row[i] * row[j] for row in ports) == 104 * (i == j) + for i in range(8) for j in range(8)), 'R R^T = 104 I') + return ports + + +def replay(word, ports, wanted=()): + """Dense integer rows on an exactly checked denominator-eight lattice. + + Track all 280 inputs, not just code projections. Enumerate same-frame + snapshots at EVERY cut. Pool only up to 2717; replay the whole endpoint. + """ + names = list(word['initial_frames']) + need(len(names) == 280 and set(names) == set(word['final_frames']), 'boundary names') + need(names[:104] == ['X' + str(i) for i in range(104)], 'source column order') + need(names[104:208] == ['Y' + str(i) for i in range(104)], 'target column order') + indices = {name: i for i, name in enumerate(names)} + state = {name: tuple(8 * (i == j) for j in range(280)) + for i, name in enumerate(names)} + frames = {name: frame(tuple(value)) for name, value in word['initial_frames'].items()} + initial = dict(state) + need(all(frames[name] == frozenset({0}) for name in names[104:]), 'initial nuisance units') + pools = [set() for _ in ports] + snapshots = {} + desired = set(wanted) + checkpoints = {} + projection_cache = {} + observed = set() + profile, operations = Counter(), Counter() + + def inspect(cut): + groups = defaultdict(list) + for name, value in frames.items(): + groups[value].append(name) + for group in groups.values(): + targets = [int(name[1:]) for name in group if name.startswith('Y')] + if not targets: + continue + for name in group: + row = state[name] + if row not in projection_cache: + x = row[:104] + coeff = tuple(Q(sum(x[s] * ports[s][j] for s in range(104)), 832) + for j in range(8)) + need(all(sum(coeff[j] * ports[s][j] for j in range(8)) == Q(x[s], 8) + for s in range(104)), 'eligible source projection outside root code') + projection_cache[row] = coeff + coeff = projection_cache[row] + for target in targets: + if name == 'Y' + str(target): + continue + need(row[104 + target] == 0, 'eligible snapshot contains own target dirt') + observed.add((target, row)) + if any(coeff) and cut <= 2717: + pools[target].add(coeff) + key = target, cut, name + if key in desired: + snapshots[key] = coeff + if cut in {end for _, end, _ in INTERVALS}: + checkpoints[cut] = [set(pool) for pool in pools] + + inspect(0) + for cut, event in enumerate(word['program'], 1): + op, name = event[:2] + operations[op] += 1 + if op == 'transport': + _, _, old, new, paid = event + before, after = frame(tuple(old)), frame(tuple(new)) + need(frames[name] == before, 'transport entry frame') + need(before <= after or after <= before, 'nested transport') + need(type(paid) is int and paid == abs(len(new) - len(old)) and paid > 0, + 'transport rank') + frames[name] = after + profile[paid] += 1 + elif op == 'zero': + need(name == 'C' and name not in state, 'owned private allocation') + state[name] = (0,) * 280 + frames[name] = frame(tuple(event[2])) + elif op == 'erase': + need(name == 'C' and frames[name] == frame(tuple(event[2])), 'owned private discard') + del state[name], frames[name] + elif op == 'copy': + _, _, source, chart = event + need(name == 'C' and not any(state[name]), 'copy into owned zero') + need(frames[name] == frames[source] == frame(tuple(chart)), 'copy chart') + state[name] = state[source] + else: + need(op == 'add', 'known operation') + _, _, source, weight, chart = event + need(name != source and frames[name] == frames[source] == frame(tuple(chart)), 'add chart') + factor = Q(weight) + scaled = [factor.numerator * x for x in state[source]] + need(all(x % factor.denominator == 0 for x in scaled), 'denominator-eight lattice') + state[name] = tuple(x + y // factor.denominator for x, y in zip(state[name], scaled)) + inspect(cut) + need(len(word['program']) == 4058 and set(state) == set(names), 'full trace closure') + for name in names: + expected = list(initial[name]) + if name.startswith('Y'): + target = int(name[1:]) + for source in range(104): + expected[source] += sum(a * b for a, b in zip(ports[target], ports[source])) + need(state[name] == tuple(expected), 'arbitrary-input endpoint ' + name) + need(frames[name] == frame(tuple(word['final_frames'][name])), 'final frame ' + name) + need(dict(profile) == {1: 1074, 2: 58, 3: 86, 4: 104, 5: 48, 6: 24, 7: 8, 8: 8}, + 'unchanged local paid profile') + need(set(snapshots) == desired, 'contact absent or self-contact') + return checkpoints, snapshots, len(observed), dict(profile) + + +def lower_bound(pools, ports): + union, operators = {}, {} + for target, pool in enumerate(pools): + for coeff in sorted(pool): + add_basis(union, coeff) + add_basis(operators, [x * y for x in ports[target] for y in coeff]) + u = list(union.values()) + e = list(operators.values()) + equations = [[sum(row[i] * op[i * 8 + j] for i in range(8)) for op in e] + for row in u for j in range(8)] + rhs = [row[j] for row in u for j in range(8)] + possible = solvable(equations, rhs) + # I-M fixes ker(U). Equality rank(I-M)=8-rank(U) forces U M=U. + return 104 - len(u) + (not possible), len(u), len(e), possible + + +def upper_bound(terms, snapshots, ports, start): + a = [[Q(0)] * 8 for _ in ports] + seen = set() + for target, cut, register, weight in terms: + need(type(target) is int and 0 <= target < 104 and type(cut) is int and 0 <= cut <= start, + 'upper contact index or future cut') + key = target, cut, register + need(key not in seen and key in snapshots, 'duplicate or unavailable upper contact') + seen.add(key) + need(isinstance(weight, str) and Q(weight) != 0, 'nonzero rational contact weight') + a[target] = [x + Q(weight) * y for x, y in zip(a[target], snapshots[key])] + matrix = [[Q(i == j) - sum(ports[t][i] * a[t][j] for t in range(104)) + for j in range(8)] for i in range(8)] + small = rank(matrix) + # Independently measure the actual 104-source correction-row rank. + correction = [[Q(t == s) - Q(sum(ports[t][j] * ports[s][j] for j in range(8)), 8) + + 12 * sum(a[t][j] * ports[s][j] for j in range(8)) + for s in range(104)] for t in range(104)] + large = rank(correction) + need(large == 96 + small, 'small/large rank identity') + return large + + +def sources(): + values = {} + for item in read(HERE / 'SOURCES.json')['files']: + if item['usage'] != 'input': + continue + path = ROOT / item['path'] + need(hashlib.sha256(path.read_bytes()).hexdigest() == item['sha256'], 'input hash ' + item['path']) + values[path.name] = read(path) + return values + + +def run(certificate=None): + data = sources() + ports = geometry(data['P104-FIXTURE.json']['section4_explicit_P104']) + certificate = read(HERE / 'WITNESS.json') if certificate is None else certificate + need(set(certificate) == {'schema', 'witnesses'} and certificate['schema'] == 'p104-prefix-minrank/1', + 'certificate schema') + witnesses = certificate['witnesses'] + need([x['cut'] for x in witnesses] == [x[0] for x in INTERVALS[1:]], 'witness cut coverage') + wanted = [tuple(term[:3]) for item in witnesses for term in item['terms']] + pools, snaps, count, profile = replay(data['LOWRANK-WITNESS.json'], ports, wanted) + results = [] + for index, (start, end, expected) in enumerate(INTERVALS): + low, row_rank, operator_rank, possible = lower_bound(pools[end], ports) + high = 104 if index == 0 else upper_bound(witnesses[index - 1]['terms'], snaps, ports, start) + need(low == high == expected, 'interval does not have matching exact bounds') + results.append(dict(start=start, end=end, minimum=low, union_rank_at_end=row_rank, + operator_rank_at_end=operator_rank, projector_feasible_at_end=possible)) + return dict(schema='p104-prefix-minrank-result/1', status='PASS_P104_EARLY_PREFIX_MINRANK', + cuts_replayed=4059, boundary_columns=280, distinct_target_snapshots=count, + intervals=results, local_profile={str(k): v for k, v in sorted(profile.items())}, + scope='Rational unchanged-trace pooled snapshots only; no chronological correction or paid cost result.') + + +def main(): + 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'), 'exact receipt mismatch') + if args.out: + with args.out.open('x', encoding='utf-8') as handle: + json.dump(result, handle, indent=2, sort_keys=True) + handle.write('\n') + print(result['status'], 'intervals=6 cuts=4059 columns=280') + + +if __name__ == '__main__': + main()