diff --git a/research/p104-prefix-tail/README.md b/research/p104-prefix-tail/README.md new file mode 100644 index 0000000000..6543fa9f6a --- /dev/null +++ b/research/p104-prefix-tail/README.md @@ -0,0 +1,216 @@ +# The P104 pooled correction first reaches dimension 98 at cut 2754 + +This resolves the interval left open by +[PR #2345](https://github.com/CrocSwap/integer-mult-bounds/pull/2345): + +| Completed original events | Exact rational shared correction dimension | +|---|---:| +| 2718–2753 | 99 | +| 2754–2823 | 98 | + +The lower proof uses fixed compressed determinants **−2** and **−1**. +A new 46-contact certificate attains dimension 98 at cut **2754**. The +rank-99 witness at cut 2646 is retained from #2345 and independently replayed. +In particular, **no earlier prefix can attain dimension 98**. This fills the +gap before the reported late-prefix results in +[Discussion #2245](https://github.com/CrocSwap/integer-mult-bounds/discussions/2245#discussioncomment-18940216). +We do not recertify that separate late-prefix package here. + +**This is a rational pooled-snapshot model, not an executable correction or +a transport-cost reduction.** Pooling grants access at different times; the +new directions have no implemented creation, restoration or hosting bill. +There is no supplier or κ claim and no selected-frontier change. + +## Exact model and independent replay + +Use the unchanged PR #1972 word retained by the native PR #1991 package: +104 source inputs, 104 target inputs, 72 independent dirty helper inputs, +4,058 events and 4,059 cuts. A cut counts completed events. For each target, + +``` +S_t(c) = span_Q { v_r(d) : d <= c, r != Y_t, + frame(r,d) = frame(Y_t,d) as binary subspaces }. +``` + +All snapshots come from the original word; inserted rows do not change later +snapshots. Basis changes within a frame are free in this relaxation. Let `R` +be the 8-by-104 doubled root-coordinate matrix and `C=I_104-R^T R/8`. +The number `h(c)` minimizes `dim H` over rational spaces in all 280 boundary +coordinates such that `C_t in S_t(c)+H` for every target. + +[trace.py](trace.py) is a fresh sparse integer/8 implementation, with no +imports from the earlier dense replay or native producer. It checks source +hashes, all 280 independent columns, every frame transition, private-copy +lifetimes, source/dirty restorations, the complete `G/2` endpoint and unchanged +local rank mass 2368. It independently recovers the same 110,814 distinct +target/snapshot pairs as #2345. + +The collector visits each changed frame group. At an unchanged group both +membership and every logical row are unchanged, so revisiting cannot add a +snapshot. Requested contacts are checked separately at their exact cut, +including cuts where nothing in their group changes. This is exact reuse, +not sampling cuts. The relevant prefix pools contain 324 and 427 nonzero +target/coefficient pairs at cuts 2753 and 2823. + +## Reduction to an eight-dimensional residual + +We use the reduction proved in #2345, retaining its hypotheses and giving +the argument for standalone review. The full replay checks `R R^T=104 I`, +source projections in `row(R)`, absence of a target's own dirt from every +eligible donor, and availability of the other 175 independent nuisance units +at cut zero. The last two facts imply `pi_X(S_t)=S_t intersect X`: each +nuisance component can be subtracted inside the pool. Projecting any serving +`H` therefore gives a serving source-only space of no greater dimension, +and source-only spaces are allowed choices. + +Put `L_t={a in Q^8 : aR in S_t intersect X}`. Choosing one local row per target +and taking the residual row span yields + +``` +h(c) = min_{A_t in L_t(c)} rank(C+12 A R) + = 96 + min_{M in E(c)} rank(I_8-M), +E(c) = {R A : A_t in L_t(c)} = span{r_t a : a in L_t(c)}. +``` + +The substitution by −12 preserves each linear `L_t`. To see the rank identity, +write `D=R^T/8-12A`, so `C+12AR=I-DR` and `RD=13I-12RA`. +The restrictions of `R` and `D` are inverse maps between `ker(I-DR)` and +`ker(I-RD)`. Rank-nullity gives `rank(C+12AR)=96+rank(I-RA)`. +These statements quantify rational coefficients, including arbitrary dirty +components of the original `H`; they do not identify rational minimum rank +with a real or complex constrained minimum. + +## Two small universal lower certificates + +Indices below are zero-based, and `e_i` are the standard vectors of Q^8. +Use columns + +``` +p=e1-e0, q=e2-e0, w=e2+e3+e4+e5-e6+e7, +a=e0+e1, b=e0+e2, k=e7-e6. +``` + +For every generator `r_t alpha` of `E(2823)`, the checker establishes + +``` +p^T M a = p^T M b = q^T M a = 0. +``` + +These linear functionals then vanish on all rational linear combinations, +not only sampled matrices. For every residual `N=I-M`, the compression with +left rows `(p^T,q^T)` and right columns `(a,b)` is + +``` +[ 0 -1 ] +[-1 * ] determinant = -1. +``` + +Compression cannot increase rank, so `rank N>=2` and `h(c)>=98` through +cut 2823. At cut 2753 the additional exact functionals are + +``` +p^T M k = q^T M k = w^T M k = 0. +``` + +Since `p^T k=q^T k=0` and `w^T k=2`, left rows `(p^T,q^T,w^T)` and right +columns `(a,b,k)` give + +``` +[ 0 -1 0 ] +[-1 * 0 ] +[ * * 2 ] determinant = -2. +``` + +Thus `rank N>=3` and `h(c)>=99` for every prefix through 2753. No nonlinear +search, optimizer status, approximate rank or characteristic-two determinant +is used for these rational lower bounds. + +## Matching upper certificates and the exact break + +Each entry `[target,cut,register,weight]` in [WITNESS.json](WITNESS.json) +contributes `weight * pi_X(v_register(cut)) R^T/104` to the target's row of +`A`. The code replays its availability, and the lifting facts above remove +nuisance components. The resulting `K=C+12AR` serves every correction row +since `K_t-C_t in S_t`. + +The 18-contact cut-2646 witness from #2345 has `rank K=99`; it remains +available at every later prefix. The new 46-contact cut-2754 witness gives +exactly + +``` +N = x (e1+2e7)^T - e1 e2^T, x=-e2+e3+e7. +``` + +This has rank two: the persistent compression is nonsingular, and the +displayed sum has at most two rank-one terms. The checker independently +computes both `rank N=2` and `rank K=98` by rational elimination. +At this cut the old `q^T M k=0` constraint is no longer true: in the new +residual `q^T N k=-2`, while `p^T N k=0` and `w^T N k=2`. Thus the earlier +3-by-3 argument cannot be extended past its checked prefix. + +Pools grow monotonically. The cut-2646 upper and cut-2753 lower prove 99 +throughout the first interval; the cut-2754 upper and cut-2823 lower prove +98 throughout the second. Contacts are algebraic membership certificates, +not literal added chronological instructions. + +## Reproduce + +Standard-library Python, with read-only default commands and no network, +Git or pending-package code needed for the direct checks: + +```sh +python3.12 -I -O -B research/p104-prefix-tail/verify.py +python3.12 -I -O -B research/p104-prefix-tail/test_verify.py +python3.12 scripts/research_package.py --package research/p104-prefix-tail +``` + +Expected primary line: `PASS_P104_PREFIX_TAIL 99 through2753; 98 from2754 through2823`. +The full [RESULT.json](RESULT.json) must match. `--out NEW.json` writes only +to an unoccupied path. The registered replay also runs failure controls; +its metadata needs Git provenance, unlike the direct replay. Tests cover +corrupt contacts, future/self contacts, nonzero compensation/cleanup faults, +and low-rank counterexamples when required compression constraints are dropped. + +The proof and finite certificates were checked with rational arithmetic and +a separately implemented source-projection exploration. Native Gaussian +recipe regeneration, chronological correction execution, global moment and +owner assignment, precision/all-size admission and selected cold replay are +not performed. Hosted CI and independent human review remain separate. + +## Open next questions + +- **Turn one complement into a fully charged chronological construction.** + The available snapshots do not make its 98 shared directions free. Begin + with source reads, frame paths, creation/restoration and owners, then price + the entire word. Existing fixed-frame/retained-cost obstructions still apply. + No implementation contract is supplied here. +- **Connect the independently published prefix certificates.** The reported + 97 interval from 2824 and 96 interval from 2912 can be combined with #2345 + and this package after checking their exact artifacts and source bindings. + Start with a source-bound replay/index of those certificates; external + late-prefix evidence is not rerun by this package. + +## Sources and attribution + +Scientific base: canonical main `0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2`, +priority revision 4, freshly fetched at the second-round checkpoint. Only +this new package is added; the first-round PR is not a parent dependency. +[TASK.json](TASK.json) records the handoff, scope, freshness and overlap; +[SOURCES.json](SOURCES.json) pins both frozen inputs. + +Gonzalo Mier/#2173 supplied the pooled model and dimension question; +Gareth Davidson/@bitplane/#2251 supplied the full-pool complement; +@josecarlosgonzalezroque-design supplied the late-prefix result and the +handoff in Discussion2245 comment18940216. AAAmirinu/#2345 at +`2a5fa34a967e7567abf01611f92a6ab69e8c901a` supplied the rank reduction and +the reused cut-2646 witness. Those are not new claims here. + +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 the retained geometry/decoder lineage. +Original files and notices remain unchanged. + +Prepared for AAAmirinu with substantial OpenAI Codex assistance in proof, +implementation, testing and prose, including separate projection exploration, +sparse replay and mathematical review. Author-checked evidence; no independent +human review or proof-assistant claim. Apache-2.0. diff --git a/research/p104-prefix-tail/RESULT.json b/research/p104-prefix-tail/RESULT.json new file mode 100644 index 0000000000..c0dec79493 --- /dev/null +++ b/research/p104-prefix-tail/RESULT.json @@ -0,0 +1,79 @@ +{ + "schema": "p104-prefix-tail-result/1", + "status": "PASS_P104_PREFIX_TAIL", + "intervals": [ + { + "start": 2718, + "end": 2753, + "minimum": 99 + }, + { + "start": 2754, + "end": 2823, + "minimum": 98 + } + ], + "lower_certificates": { + "2753": { + "minimum_dimension": 99, + "compression_rank": 3, + "determinant": -2, + "generator_pair_checks": 1944 + }, + "2823": { + "minimum_dimension": 98, + "compression_rank": 2, + "determinant": -1, + "generator_pair_checks": 1281 + } + }, + "upper_certificates": [ + { + "cut": 2646, + "contacts": 18, + "residual_rank": 3, + "full_source_correction_rank": 99 + }, + { + "cut": 2754, + "contacts": 46, + "residual_rank": 2, + "full_source_correction_rank": 98 + } + ], + "trace": { + "schema": "p104-prefix-tail-trace/1", + "cuts_replayed": 4059, + "boundary_columns": 280, + "initial_nuisance_units_per_target": 175, + "distinct_target_snapshots": 110814, + "distinct_source_projections_checked": 118, + "changed_target_groups_checked": 2356, + "local_profile": { + "1": 1074, + "2": 58, + "3": 86, + "4": 104, + "5": 48, + "6": 24, + "7": 8, + "8": 8 + }, + "rank_mass": 2368, + "events": { + "add": 2624, + "copy": 8, + "erase": 8, + "transport": 1410, + "zero": 8 + }, + "endpoint": "G/2; all 104 sources and 72 dirty helpers restored; private storage closed", + "prefix_pool_totals": { + "2753": 324, + "2823": 427 + }, + "requested_contacts": 49, + "input_overrides": false + }, + "scope": "Rational unchanged-trace pooled availability; no chronological or paid-cost claim." +} diff --git a/research/p104-prefix-tail/SOURCES.json b/research/p104-prefix-tail/SOURCES.json new file mode 100644 index 0000000000..3bb2451581 --- /dev/null +++ b/research/p104-prefix-tail/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-tail/TASK.json b/research/p104-prefix-tail/TASK.json new file mode 100644 index 0000000000..ef540f9bfe --- /dev/null +++ b/research/p104-prefix-tail/TASK.json @@ -0,0 +1,146 @@ +{ + "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 P104 pooled-prefix dimensions99 on2718..2753 and98 on2754..2823, including the earliest98 boundary.", + "scope_change_reason": "Explicitly continue the central early-prefix handoff after PR2345. This is an algebraic availability relaxation, not the full chronological correction required for supplier admission.", + "bottleneck_link": "Resolves the remaining information-space boundary before the reported97/96 prefixes; prevents extending an invalid rank-three obstruction or treating pooled dimensions as paid ranks.", + "budget_minutes": 60, + "stop_rule": "Stop when fixed rational compressed minors and exact contact witnesses give matching bounds on the scoped tail; do not extend into global hosting or change frontier.", + "outcome": "completed", + "evidence": "RESULT.json: determinants-2/-1; inherited18-contact rank99 witness; new46-contact rank98 witness at2754; independent all4059cut280column sparse replay.", + "author": "AAAmirinu", + "ai_assistance": "Substantial OpenAI Codex assistance including separate source-projection exploration, sparse collector implementation and mathematical proof review; no independent human review.", + "open_questions": [ + { + "question": "Can one complement be realized with a favorable complete chronological bill?", + "why_it_matters": "A pooled minimum does not implement the identity channel or improve kappa.", + "first_step": "Build and price source reads, frames, creation/restoration and actual owners.", + "blocked_by": "No completed chronological producer, full moment or precision/all-size admission." + }, + { + "question": "Can all published prefix certificates be connected under one exact source binding?", + "why_it_matters": "Would consolidate the complete algebraic staircase without implying chronological implementation.", + "first_step": "Pin and replay the external late-prefix97/96 artifacts alongside PR2345 and this result.", + "blocked_by": "The late-prefix public export is not checked by this package." + } + ], + "assignment": { + "type": "explicit central-handoff continuation", + "task": "p104-side-correction", + "original_round1_nonce": "04b2bbe7a3fb0b4faf78715dbf6ffb24", + "task_card_retrieval_nonce": "088e68080bed53efaeae26f1587783f7", + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/2245#discussioncomment-18942121" + }, + "predecessors": [ + { + "pr": 2345, + "head": "2a5fa34a967e7567abf01611f92a6ab69e8c901a", + "contribution": "Exact rank reduction and reused18-contact cut2646 upper witness; no runtime code dependency." + }, + { + "pr": 2251, + "head": "822bceef780d8da9605798f0836ae5320e8e291e", + "contribution": "Full-pool complement and model lineage." + }, + { + "pr": 2173, + "head": "d9b784ca86fba060f0264370536ccd322c89998a", + "contribution": "Pooled-span model and dimension96..97 question." + }, + { + "url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/2245#discussioncomment-18940216", + "author": "josecarlosgonzalezroque-design", + "contribution": "Late-prefix result and early-prefix handoff." + } + ], + "verification": { + "environment": "Windows CPython 3.12.11; standard library; -I -O -B", + "primary_command": "python3.12 -I -O -B research/p104-prefix-tail/verify.py", + "primary_status": "PASS_P104_PREFIX_TAIL", + "primary_seconds": 12.023, + "controls_command": "python3.12 -I -O -B research/p104-prefix-tail/test_verify.py", + "controls": "All 13 controls covered: 11 passed in the initial 41.424-second run; two test-fixture issues were corrected and both affected controls passed in a 10.599-second targeted rerun. No acceptance-engine change was needed.", + "independent_evidence": "Separate rational source-projection exploration reconstructed the cut-2754 operator space (dimension 57), verified the proposed residual lies in it, and checked every lower functional. Separate AI-assisted proof review found no issues.", + "unrun": ["native Gaussian regeneration", "chronological correction execution", "global moment and owners", "precision and all-size admission", "selected cold replay", "hosted CI", "independent human review"] + }, + "submission_checkpoint": { + "utc": "2026-10-15T06:24:37Z", + "canonical_main": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "priority_revision": 4, + "guidance_and_selected_and_native_inputs_changed": false, + "overlap_command": "python3.12 -B scripts/find_overlap.py P104 prefix --all-terms --refresh --limit 100 --json", + "open_prs": 564, + "open_prs_fetched_at": "2026-10-15T06:20:00.569436+00:00", + "discussion_records": 1078, + "discussions_fetched_at": "2026-10-15T06:22:18.219753+00:00", + "complete_pagination": true, + "warnings": [], + "targeted_matches_inspected": 33, + "live_thread_and_relevant_heads_rechecked": true, + "distinct_from": [ + "EdDiboi chronological 41-contact lift, comment 18941894", + "kumagi monotone relay floor audit, PR 2353 at 2704eadf6b5205d4b965e9c6fc6dce28b89783cf" + ], + "coverage_limit": "PR bodies, Discussion records and local package metadata; not every code diff or arbitrary historical artifact. No novelty guarantee is inferred from this search." + }, + "entry_checkpoint": { + "utc": "2026-10-15T06:04:06Z", + "canonical_main": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "priority_revision": 4, + "guidance_and_selected_and_native_inputs_changed": false, + "live_thread_read": true, + "overlap_snapshot_utc": "2026-10-15T06:00:37.201126Z", + "open_prs": 553, + "discussion_records": 1063, + "complete_pagination": true, + "distinct_from": [ + "chronological41-contact lift:comment18941894", + "monotone-relay-floor audit:comment18941961" + ] + } +} diff --git a/research/p104-prefix-tail/VERIFY.json b/research/p104-prefix-tail/VERIFY.json new file mode 100644 index 0000000000..5867ca452f --- /dev/null +++ b/research/p104-prefix-tail/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": 180, + "checks": "Pinned full280-column trace, availability, compressed determinant lower bounds and direct/reduced upper ranks." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/test_verify.py" + ], + "timeout_seconds": 300, + "checks": "Positive controls and coefficient/contact/dirty-restoration/constraint-omission failure controls." + } + ] +} diff --git a/research/p104-prefix-tail/WITNESS.json b/research/p104-prefix-tail/WITNESS.json new file mode 100644 index 0000000000..6f948ed2dd --- /dev/null +++ b/research/p104-prefix-tail/WITNESS.json @@ -0,0 +1,465 @@ +{ + "schema": "p104-prefix-tail/1", + "upper_witnesses": [ + { + "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" + ] + ], + "minimum": 99, + "origin": "PR2345 commit2a5fa34a967e7567abf01611f92a6ab69e8c901a" + }, + { + "cut": 2754, + "terms": [ + [ + 7, + 2526, + "D5", + "1/4" + ], + [ + 13, + 2532, + "Y7", + "1" + ], + [ + 15, + 2534, + "Y7", + "1" + ], + [ + 33, + 2542, + "Y7", + "-2" + ], + [ + 66, + 2554, + "Y14", + "-4" + ], + [ + 68, + 2556, + "Y14", + "-2" + ], + [ + 70, + 2560, + "Y14", + "2" + ], + [ + 72, + 2562, + "Y14", + "2" + ], + [ + 0, + 2572, + "D12", + "-1/4" + ], + [ + 2, + 2574, + "Y0", + "-4" + ], + [ + 6, + 2576, + "Y0", + "3" + ], + [ + 11, + 2578, + "Y0", + "-4" + ], + [ + 12, + 2580, + "Y0", + "1" + ], + [ + 19, + 2582, + "Y0", + "3" + ], + [ + 36, + 2586, + "Y0", + "-3" + ], + [ + 63, + 2592, + "Y0", + "1" + ], + [ + 3, + 2604, + "D16", + "3/4" + ], + [ + 5, + 2606, + "Y3", + "-1" + ], + [ + 24, + 2608, + "Y3", + "2" + ], + [ + 25, + 2610, + "Y3", + "-1" + ], + [ + 32, + 2616, + "Y3", + "2" + ], + [ + 43, + 2618, + "Y3", + "-1" + ], + [ + 50, + 2620, + "Y3", + "3" + ], + [ + 22, + 2638, + "D20", + "1/4" + ], + [ + 23, + 2640, + "Y22", + "2" + ], + [ + 28, + 2642, + "Y22", + "2" + ], + [ + 29, + 2644, + "Y22", + "-2" + ], + [ + 31, + 2646, + "Y22", + "-1" + ], + [ + 41, + 2648, + "Y22", + "-4" + ], + [ + 1, + 2672, + "D23", + "1/2" + ], + [ + 4, + 2674, + "Y1", + "2" + ], + [ + 9, + 2676, + "Y1", + "-2" + ], + [ + 17, + 2678, + "Y1", + "4" + ], + [ + 26, + 2680, + "Y1", + "-2" + ], + [ + 45, + 2684, + "Y1", + "-2" + ], + [ + 59, + 2698, + "Y1", + "-2" + ], + [ + 80, + 2718, + "D27", + "1/4" + ], + [ + 81, + 2720, + "Y80", + "1" + ], + [ + 82, + 2722, + "Y80", + "1" + ], + [ + 85, + 2724, + "Y80", + "1" + ], + [ + 14, + 2735, + "D5", + "1/4" + ], + [ + 66, + 2737, + "Y14", + "2" + ], + [ + 0, + 2746, + "D0", + "-1/2" + ], + [ + 2, + 2748, + "Y0", + "2" + ], + [ + 11, + 2752, + "Y0", + "4" + ], + [ + 19, + 2754, + "Y0", + "-4" + ] + ], + "minimum": 98, + "origin": "New explicit rank-two residual" + } + ], + "lower_vectors": { + "p": [ + -1, + 1, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "q": [ + -1, + 0, + 1, + 0, + 0, + 0, + 0, + 0 + ], + "w": [ + 0, + 0, + 1, + 1, + 1, + 1, + -1, + 1 + ], + "a": [ + 1, + 1, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "b": [ + 1, + 0, + 1, + 0, + 0, + 0, + 0, + 0 + ], + "k": [ + 0, + 0, + 0, + 0, + 0, + 0, + -1, + 1 + ] + } +} diff --git a/research/p104-prefix-tail/test_verify.py b/research/p104-prefix-tail/test_verify.py new file mode 100644 index 0000000000..b6720e2b04 --- /dev/null +++ b/research/p104-prefix-tail/test_verify.py @@ -0,0 +1,216 @@ +"""Semantic and algebraic controls for the exact tail-prefix certificates. + +AAAmirinu with substantial OpenAI Codex assistance. Apache-2.0. +All checks use unittest assertions or explicit exceptions, also under -O. +The immutable channel is read only; fault controls mutate 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 subprocess +import sys +import unittest + + +HERE = Path(__file__).resolve().parent +SPEC = spec_from_file_location('p104_tail_control_verify', HERE / 'verify.py') +verify = module_from_spec(SPEC) +SPEC.loader.exec_module(verify) +trace = verify.trace + + +def unit(index): + return [int(i == index) for i in range(8)] + + +def outer(left, right): + return [[x * y for y in right] for x in left] + + +def matrix_sum(left, right): + return [[x + y for x, y in zip(a, b)] for a, b in zip(left, right)] + + +def compression(matrix, lefts, rights): + return [[sum(left[i] * matrix[i][j] * right[j] + for i in range(8) for j in range(8)) + for right in rights] for left in lefts] + + +def determinant2(matrix): + return matrix[0][0] * matrix[1][1] - matrix[0][1] * matrix[1][0] + + +def determinant3(matrix): + a, b, c = matrix + return (a[0] * (b[1] * c[2] - b[2] * c[1]) + - a[1] * (b[0] * c[2] - b[2] * c[0]) + + a[2] * (b[0] * c[1] - b[1] * c[0])) + + +class CompressionPremiseControls(unittest.TestCase): + """Explicit low-rank counterexamples when a required equality is omitted.""" + p = [-1, 1, 0, 0, 0, 0, 0, 0] + q = [-1, 0, 1, 0, 0, 0, 0, 0] + w = [0, 0, 1, 1, 1, 1, -1, 1] + a = [1, 1, 0, 0, 0, 0, 0, 0] + b = [1, 0, 1, 0, 0, 0, 0, 0] + k = [0, 0, 0, 0, 0, 0, -1, 1] + x = [0, 0, -1, 1, 0, 0, 0, 1] + + def test_missing_zero_entry_allows_rank_one(self): + # The two off-diagonal entries alone do not force rank two. + left = [0, 1, 1, 0, 0, 0, 0, -1] + matrix = outer(left, [-1, 0, 0, 0, 0, 0, 0, 0]) + small = compression(matrix, [self.p, self.q], [self.a, self.b]) + self.assertEqual(small, [[-1, -1], [-1, -1]]) + self.assertEqual(determinant2(small), 0) + self.assertEqual(verify.rank(matrix), 1) + self.assertNotEqual(small[0][0], 0) + self.assertEqual(compression(matrix, [[1, 0, 0, 0, 0, 0, 0, 1]], + [self.a]), [[1]]) + + def test_missing_q_kernel_entry_allows_rank_two(self): + # This is the actual new residual: q^T N k=-2, not zero. Omitting + # that premise would falsely extend the rank-three lower bound. + matrix = matrix_sum(outer(self.x, [0, 1, 0, 0, 0, 0, 0, 2]), + outer([0, -1, 0, 0, 0, 0, 0, 0], unit(2))) + small = compression(matrix, [self.p, self.q, self.w], + [self.a, self.b, self.k]) + self.assertEqual(small, [[0, -1, 0], [-1, 0, -2], [1, 0, 2]]) + self.assertEqual(determinant3(small), 0) + self.assertEqual(determinant2([row[:2] for row in small[:2]]), -1) + self.assertEqual(verify.rank(matrix), 2) + self.assertEqual(small[0][2], 0) + self.assertEqual(small[2][2], 2) + self.assertNotEqual(small[1][2], 0) + + def test_missing_nonzero_third_entry_allows_rank_two(self): + matrix = matrix_sum(outer(self.x, unit(1)), + outer([0, -1, 0, 0, 0, 0, 0, 0], unit(2))) + small = compression(matrix, [self.p, self.q, self.w], + [self.a, self.b, self.k]) + self.assertEqual(small, [[0, -1, 0], [-1, 0, 0], [1, 0, 0]]) + self.assertEqual(determinant3(small), 0) + self.assertEqual(verify.rank(matrix), 2) + # Restoring the required nonzero entry gives the certified determinant. + forced = [row[:] for row in small] + forced[2][2] = 2 + self.assertEqual(determinant3(forced), -2) + self.assertEqual(verify.rank(forced), 3) + + +class FrozenTraceControls(unittest.TestCase): + @classmethod + def setUpClass(cls): + cls.certificate = trace.read(HERE / 'WITNESS.json') + cls.wanted = verify.validate_certificate(cls.certificate) + # Certificate controls share one full, pinned 280-input replay. + cls.collected = trace.collect([2753, 2823], cls.wanted) + cls.word = trace.sources()['LOWRANK-WITNESS.json'] + + def test_positive_result_matches_complete_receipt(self): + result = verify.run(self.certificate, self.collected) + self.assertEqual(result, trace.read(HERE / 'RESULT.json')) + self.assertEqual(result['intervals'], [ + {'start': 2718, 'end': 2753, 'minimum': 99}, + {'start': 2754, 'end': 2823, 'minimum': 98}, + ]) + self.assertEqual(result['trace']['cuts_replayed'], 4059) + self.assertEqual(result['trace']['boundary_columns'], 280) + + def test_wrong_new_contact_weight_rejected(self): + bad = deepcopy(self.certificate) + self.assertEqual(bad['upper_witnesses'][1]['terms'][-1], + [19, 2754, 'Y0', '-4']) + bad['upper_witnesses'][1]['terms'][-1][3] = '4' + verify.validate_certificate(bad) + with self.assertRaisesRegex(ValueError, 'explicit rank-two residual differs'): + verify.check_upper(bad['upper_witnesses'][1], self.collected) + + def test_future_contact_rejected_before_replay(self): + bad = deepcopy(self.certificate) + bad['upper_witnesses'][1]['terms'][-1][1] = 2755 + with self.assertRaisesRegex(ValueError, 'future contact'): + verify.validate_certificate(bad) + + def test_self_contact_rejected_by_real_initial_state(self): + with self.assertRaisesRegex(ValueError, 'contact absent or self-contact'): + trace.collect([], [(7, 0, 'Y7')]) + + def test_initial_compensation_sign_fault_rejected_at_endpoint(self): + bad = deepcopy(self.word) + self.assertEqual(bad['program'][0], ['add', 'Y0', 'Q0', '-1/4', []]) + bad['program'][0][3] = '1/4' + # Keep a nonzero, lattice-compatible scalar and the same event count: + # rejection must come from semantics, not the zero-weight syntax guard. + with self.assertRaisesRegex(ValueError, 'arbitrary-input endpoint: Y0'): + trace.collect([], word_override=bad) + + def test_final_cleanup_sign_fault_rejected_at_endpoint(self): + bad = deepcopy(self.word) + self.assertEqual(bad['program'][-1][:4], ['add', 'Q7', 'X103', -2]) + bad['program'][-1][3] = 2 + with self.assertRaisesRegex(ValueError, 'arbitrary-input endpoint: Q7'): + trace.collect([], word_override=bad) + + def test_equivalent_scalar_and_frame_representations_preserve_trace(self): + equivalent = deepcopy(self.word) + for field in ('initial_frames', 'final_frames'): + equivalent[field] = {name: list(reversed(chart)) + for name, chart in reversed(list(equivalent[field].items()))} + for event in equivalent['program']: + if event[0] == 'transport': + event[2] = list(reversed(event[2])) + event[3] = list(reversed(event[3])) + else: + event[-1] = list(reversed(event[-1])) + if event[0] == 'add': + value = Q(event[3]) + event[3] = str(2 * value.numerator) + '/' + str(2 * value.denominator) + replay = trace.collect([2753, 2823], self.wanted, word_override=equivalent) + for key in ('ports', 'pools', 'contacts'): + self.assertEqual(replay[key], self.collected[key]) + expected_receipt = dict(self.collected['receipt'], input_overrides=True) + self.assertEqual(replay['receipt'], expected_receipt) + # Semantic equivalence does not grant acceptance to unpinned overrides. + with self.assertRaisesRegex(ValueError, 'acceptance requires pinned inputs'): + verify.run(self.certificate, replay) + + def test_first_new_contact_invalidates_old_rank_three_premise(self): + key = (19, 2754, 'Y0') + coefficient = self.collected['contacts'][key] + self.assertEqual(coefficient, (Q(0), Q(0), Q(0), Q(0), + Q(1, 4), Q(0), Q(1, 4), Q(0))) + vectors = self.certificate['lower_vectors'] + self.assertEqual(verify.dot(vectors['q'], self.collected['ports'][19]) * + verify.dot(coefficient, vectors['k']), Q(-1, 2)) + one_new_contact = [set() for _ in range(104)] + one_new_contact[19].add(coefficient) + with self.assertRaisesRegex(ValueError, 'annihilator is violated'): + verify.check_lower(one_new_contact, self.collected['ports'], vectors, True) + + def test_degenerate_compression_vector_rejected(self): + vectors = deepcopy(self.certificate['lower_vectors']) + vectors['q'] = [0] * 8 + # Zero q annihilates everything, but cannot prove the required minor. + with self.assertRaisesRegex(ValueError, 'fixed nonzero two-dimensional compression'): + verify.check_lower(self.collected['pools'][2823], self.collected['ports'], + vectors, False) + + def test_occupied_output_directory_is_rejected(self): + # An existing directory exercises the early existence guard without + # writing temporary files or risking any scientific artifact contents. + self.assertTrue(HERE.is_dir()) + result = subprocess.run( + [sys.executable, '-I', '-O', '-B', str(HERE / 'verify.py'), + '--out', str(HERE)], capture_output=True, text=True, + timeout=15, check=False) + self.assertNotEqual(result.returncode, 0) + self.assertIn('output already exists', result.stderr) + self.assertTrue(HERE.is_dir()) + + +if __name__ == '__main__': + unittest.main(verbosity=2) diff --git a/research/p104-prefix-tail/trace.py b/research/p104-prefix-tail/trace.py new file mode 100644 index 0000000000..922ac46845 --- /dev/null +++ b/research/p104-prefix-tail/trace.py @@ -0,0 +1,313 @@ +"""Sparse, exact collector for the unchanged P104 scalar/frame trace. + +This is a fresh implementation of the pooled-snapshot premise used in +AAAmirinu's PR2345. The channel and schedule are inherited from Rohan Arun +(PR1972), Adam Gall (PR1940), and Chafik Boukhalfa (PR1991); the E8 fixture +derives from Josie Elliston (PR1071). Substantial OpenAI Codex assistance. +Apache-2.0. Native physical recipes and global hosting are not replayed here. +""" + +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 +import time + + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +INPUT_NAMES = {"LOWRANK-WITNESS.json", "P104-FIXTURE.json"} +PROFILE = {1: 1074, 2: 58, 3: 86, 4: 104, 5: 48, 6: 24, 7: 8, 8: 8} +EVENTS = {"add": 2624, "transport": 1410, "zero": 8, "copy": 8, "erase": 8} + + +def need(condition, message): + """Keep every mathematical check enabled under python -O.""" + if not condition: + raise ValueError(message) + + +def _unique_json(pairs): + answer = {} + for key, value in pairs: + need(key not in answer, "duplicate JSON key: " + key) + answer[key] = value + return answer + + +def read(path): + return json.loads(Path(path).read_bytes(), object_pairs_hook=_unique_json) + + +def sources(): + """Read the two immutable JSON inputs through this package's own pins.""" + answer = {} + for item in read(HERE / "SOURCES.json")["files"]: + if item["usage"] != "input": + continue + path = ROOT / item["path"] + if path.name not in INPUT_NAMES: + continue + need(path.name not in answer, "duplicate input pin") + payload = path.read_bytes() + need(hashlib.sha256(payload).hexdigest() == item["sha256"], + "input hash mismatch: " + item["path"]) + answer[path.name] = json.loads(payload, object_pairs_hook=_unique_json) + need(set(answer) == INPUT_NAMES, "both frozen input pins are required") + return answer + + +@lru_cache(maxsize=None) +def frame(vectors): + """Compare actual binary subspaces, independently of a chosen basis.""" + span = {0} + for vector in vectors: + need(type(vector) is int and 0 < vector < 512, "binary frame vector") + need(vector not in span, "dependent binary frame basis") + span.update(vector ^ previous for previous in tuple(span)) + return frozenset(span) + + +def geometry(fixture): + """Reconstruct canonical doubled E8 root lines, then remove F0 and C.""" + roots = set() + for i, j in combinations(range(8), 2): + for sign in (-1, 1): + root = [0] * 8 + root[i], root[j] = 2, 2 * sign + roots.add(tuple(root)) + for signs in product((-1, 1), repeat=7): + if signs.count(-1) % 2 == 0: + roots.add((1, *signs)) + removed = {tuple(row) for row in fixture["F0"] + fixture["C"]} + need(len(roots) == 120 and len(removed) == 16 and removed <= roots, + "P104 punctured E8 fixture") + ports = sorted(roots - removed) + need(len(ports) == 104, "P104 root count") + need(all(sum(root[i] * root[j] for root in ports) == 104 * (i == j) + for i in range(8) for j in range(8)), "root tight-frame identity") + return ports + + +def collect(prefix_cuts, contacts=(), word_override=None, fixture_override=None): + """Return nonzero source-code rows available through each prefix cut. + + All 280 arbitrary-input columns are carried as sparse integers divided + by eight. Every scalar update checks that this lattice remains exact. + For target t, an eligible donor is any *other* live register in its exact + binary frame. Its 104 source coefficients must equal alpha R and its + own-target dirt coefficient must vanish. The returned alpha is an exact + eight-tuple over Q. Zero alpha is omitted from pools (it changes no span). + + Pools are a relaxation: contacts from different cuts may be combined + without establishing that an inserted correction preserves the trace. + The 175 initial independent nuisance units for each target are checked. + + Only changed frame groups require reinspection: an unchanged group's + full rows and memberships are identical to its preceding cut. Exact-cut + requested contacts are checked separately, even on unchanged cuts. + Overrides exist solely for rejecting controls; original source pins are + still checked before applying them. The entire endpoint is always run. + """ + cuts = tuple(sorted(set(prefix_cuts))) + need(all(type(cut) is int and 0 <= cut <= 4058 for cut in cuts), + "prefix cut outside full trace") + requested = {tuple(contact) for contact in contacts} + for contact in requested: + need(len(contact) == 3, "contact must have target, cut, register") + target, cut, register = contact + need(type(target) is int and 0 <= target < 104 and + type(cut) is int and 0 <= cut <= 4058 and isinstance(register, str), + "contact index outside full trace") + by_cut = defaultdict(list) + for target, cut, register in sorted(requested): + by_cut[cut].append((target, register)) + pinned = sources() + word = pinned["LOWRANK-WITNESS.json"] if word_override is None else word_override + fixture = pinned["P104-FIXTURE.json"] if fixture_override is None else fixture_override + ports = geometry(fixture["section4_explicit_P104"]) + names = (["X" + str(i) for i in range(104)] + + ["Y" + str(i) for i in range(104)] + + ["Q" + str(i) for i in range(8)] + + ["G" + str(i) for i in range(32)] + + ["D" + str(i) for i in range(32)]) + need(set(word) == {"initial_frames", "final_frames", "program"}, "trace fields") + need(set(word["initial_frames"]) == set(word["final_frames"]) == set(names), + "280 boundary register names") + need(len(word["program"]) == 4058, "4058 channel events") + state = {name: {index: 8} for index, name in enumerate(names)} + frames = {name: frame(tuple(word["initial_frames"][name])) for name in names} + need(all(len(frames[name]) == (2 if index < 104 else 1) + for index, name in enumerate(names)), "initial source and nuisance frames") + groups = defaultdict(set) + for name in names: + groups[frames[name]].add(name) + need(len(groups[frame(())]) == 176, "175 initial nuisance donors per target") + pools = [set() for _ in range(104)] + checkpoints, captured = {}, {} + projection_cache, row_cache = {}, {} + observed = set() + profile, events = Counter(), Counter() + group_checks = 0 + private_copied = False + + def project(register): + row = state[register] + source = tuple(sorted((column, value) for column, value in row.items() if column < 104)) + if source not in projection_cache: + alpha = tuple(Q(sum(value * ports[column][j] for column, value in source), 832) + for j in range(8)) + need(all(sum(alpha[j] * root[j] for j in range(8)) == Q(row.get(i, 0), 8) + for i, root in enumerate(ports)), "eligible source projection outside row R") + projection_cache[source] = alpha + return projection_cache[source] + + def donor(target, register): + target_name = "Y" + str(target) + need(register in state and register != target_name and + frames[register] == frames[target_name], "contact absent or self-contact") + need(state[register].get(104 + target, 0) == 0, "eligible donor contains own target dirt") + return project(register) + + def inspect(cut, changed): + nonlocal group_checks + for chart in changed: + members = groups.get(chart, ()) + targets = [int(name[1:]) for name in members if name.startswith("Y")] + if not targets: + continue + group_checks += 1 + for register in members: + eligible_targets = [target for target in targets if register != "Y" + str(target)] + if not eligible_targets: + continue + alpha = project(register) + key = tuple(sorted(state[register].items())) + # Share the immutable row object between observed target pairs. + key = row_cache.setdefault(key, key) + for target in eligible_targets: + need(state[register].get(104 + target, 0) == 0, + "eligible donor contains own target dirt") + observed.add((target, key)) + if any(alpha): + pools[target].add(alpha) + for target, register in by_cut.get(cut, ()): + captured[target, cut, register] = donor(target, register) + if cut in cuts: + checkpoints[cut] = [set(pool) for pool in pools] + + inspect(0, set(groups)) + for cut, event in enumerate(word["program"], 1): + need(isinstance(event, list) and len(event) >= 2, "malformed trace event") + op, register = event[:2] + need(op in EVENTS, "unknown trace operation") + events[op] += 1 + if op == "zero": + need(len(event) == 3 and register == "C" and register not in state, + "owned private allocation") + chart = frame(tuple(event[2])) + need(len(chart) == 256, "private allocation rank eight") + state[register], frames[register] = {}, chart + groups[chart].add(register) + private_copied = False + changed = {chart} + else: + need(register in state, "operation on absent register") + old = frames[register] + changed = {old} + if op == "transport": + need(len(event) == 5, "transport fields") + before, after, paid = frame(tuple(event[2])), frame(tuple(event[3])), event[4] + need(old == before, "transport entry frame") + need(before < after or after < before, "strict nested transport") + need(type(paid) is int and paid == abs(len(event[3]) - len(event[2])), + "transport rank") + groups[old].remove(register) + groups[after].add(register) + frames[register] = after + profile[paid] += 1 + changed.add(after) + elif op == "erase": + need(len(event) == 3 and register == "C" and private_copied and + old == frame(tuple(event[2])) and len(old) == 2, + "owned private discard after copied rank-one descent") + groups[old].remove(register) + del state[register], frames[register] + else: + need(len(event) == (4 if op == "copy" else 5), "scalar event fields") + source, chart = event[2], frame(tuple(event[-1])) + need(source in state and register != source and frames[source] == old == chart, + "common scalar frame") + if op == "copy": + need(register == "C" and not private_copied and not state[register], + "copy into owned private zero") + state[register] = dict(state[source]) + private_copied = True + else: + need(type(event[3]) in (int, str), "exact scalar coefficient") + weight = Q(event[3]) + need(weight != 0, "nonzero scalar update") + row = dict(state[register]) + for column, value in state[source].items(): + scaled = weight.numerator * value + need(scaled % weight.denominator == 0, "denominator-eight lattice") + updated = row.get(column, 0) + scaled // weight.denominator + if updated: + row[column] = updated + else: + row.pop(column, None) + state[register] = row + inspect(cut, changed) + + need(set(state) == set(frames) == set(names), "private storage closed at endpoint") + need(dict(profile) == PROFILE and dict(events) == EVENTS, "unchanged full local invoice") + for index, register in enumerate(names): + expected = {index: 8} + if register.startswith("Y"): + target = int(register[1:]) + for source, root in enumerate(ports): + value = sum(x * y for x, y in zip(ports[target], root)) + if value: + expected[source] = value + need(state[register] == expected, "arbitrary-input endpoint: " + register) + need(frames[register] == frame(tuple(word["final_frames"][register])), + "final frame: " + register) + need(len(frames[register]) == (256 if register.startswith("Y") else 512), + "final source, target or helper dimension") + need(set(captured) == requested and set(checkpoints) == set(cuts), "requested cut coverage") + receipt = { + "schema": "p104-prefix-tail-trace/1", + "cuts_replayed": 4059, + "boundary_columns": 280, + "initial_nuisance_units_per_target": 175, + "distinct_target_snapshots": len(observed), + "distinct_source_projections_checked": len(projection_cache), + "changed_target_groups_checked": group_checks, + "local_profile": {str(k): v for k, v in sorted(profile.items())}, + "rank_mass": sum(rank * count for rank, count in profile.items()), + "events": dict(sorted(events.items())), + "endpoint": "G/2; all 104 sources and 72 dirty helpers restored; private storage closed", + "prefix_pool_totals": {str(cut): sum(map(len, checkpoints[cut])) for cut in cuts}, + "requested_contacts": len(captured), + "input_overrides": word_override is not None or fixture_override is not None, + } + return {"ports": ports, "pools": checkpoints, "contacts": captured, "receipt": receipt} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--self-check", action="store_true") + args = parser.parse_args() + need(args.self_check, "use --self-check or import collect") + started = time.monotonic() + result = collect([2753, 2823]) + print(json.dumps(result["receipt"], indent=2, sort_keys=True)) + print("elapsed_seconds=%.3f" % (time.monotonic() - started)) + + +if __name__ == "__main__": + main() diff --git a/research/p104-prefix-tail/verify.py b/research/p104-prefix-tail/verify.py new file mode 100644 index 0000000000..c0df7c642a --- /dev/null +++ b/research/p104-prefix-tail/verify.py @@ -0,0 +1,154 @@ +"""Exact P104 tail-prefix certificates; no search or predecessor imports. + +AAAmirinu with substantial OpenAI Codex assistance. Apache-2.0. +The shared-space/minimum-rank reduction is credited to PR2345. +""" +from fractions import Fraction as Q +from importlib.util import module_from_spec, spec_from_file_location +from pathlib import Path +import argparse +import json + +HERE = Path(__file__).resolve().parent +SPEC = spec_from_file_location('p104_tail_trace', HERE / 'trace.py') +trace = module_from_spec(SPEC) +SPEC.loader.exec_module(trace) +need = trace.need + + +def dot(left, right): + return sum(x * y for x, y in zip(left, right)) + + +def rank(rows): + """Exact rational Gauss-Jordan elimination.""" + matrix = [list(map(Q, row)) for row in rows] + if not matrix: + return 0 + width, pivot_row = len(matrix[0]), 0 + need(all(len(row) == width for row in matrix), 'rectangular rank input') + for column in range(width): + pivot = next((i for i in range(pivot_row, len(matrix)) if matrix[i][column]), None) + if pivot is None: + continue + matrix[pivot], matrix[pivot_row] = matrix[pivot_row], matrix[pivot] + divisor = matrix[pivot_row][column] + matrix[pivot_row] = [x / divisor for x in matrix[pivot_row]] + for i, row in enumerate(matrix): + if i != pivot_row and row[column]: + coefficient = row[column] + matrix[i] = [x - coefficient * y for x, y in zip(row, matrix[pivot_row])] + pivot_row += 1 + if pivot_row == len(matrix): + break + return pivot_row + + +def validate_certificate(certificate): + need(set(certificate) == {'schema', 'upper_witnesses', 'lower_vectors'} and + certificate['schema'] == 'p104-prefix-tail/1', 'certificate schema') + witnesses = certificate['upper_witnesses'] + need([(x['cut'], x['minimum']) for x in witnesses] == [(2646, 99), (2754, 98)], + 'upper interval coverage') + wanted = [] + for item in witnesses: + seen = set() + for term in item['terms']: + need(isinstance(term, list) and len(term) == 4, 'contact shape') + target, cut, register, weight = term + need(type(target) is int and 0 <= target < 104, 'contact target') + need(type(cut) is int and 0 <= cut <= item['cut'], 'future contact') + need(isinstance(register, str) and isinstance(weight, str) and Q(weight) != 0, + 'contact register or rational weight') + key = (target, cut, register) + need(key not in seen, 'duplicate contact') + seen.add(key) + wanted.append(key) + vectors = certificate['lower_vectors'] + need(set(vectors) == {'p', 'q', 'w', 'a', 'b', 'k'}, 'lower vector names') + for row in vectors.values(): + need(len(row) == 8 and all(type(x) is int for x in row), 'integer 8-vector') + return wanted + + +def check_lower(pools, ports, vectors, three): + p, q, w = (vectors[x] for x in ('p', 'q', 'w')) + a, b, k = (vectors[x] for x in ('a', 'b', 'k')) + pairs = [(p, a), (p, b), (q, a)] + if three: + pairs += [(p, k), (q, k), (w, k)] + checks = 0 + for target, pool in enumerate(pools): + for coefficient in pool: + for left, right in pairs: + need(dot(left, ports[target]) * dot(coefficient, right) == 0, + 'annihilator is violated by an eligible snapshot') + checks += 1 + # These exact entries force a nonsingular compression for EVERY I-M. + need(dot(p, a) == 0 and dot(p, b) == -1 and dot(q, a) == -1, + 'fixed nonzero two-dimensional compression') + determinant = -1 + if three: + need(dot(p, k) == dot(q, k) == 0 and dot(w, k) == 2, + 'fixed nonzero third compression entry') + determinant = -2 + return dict(minimum_dimension=99 if three else 98, + compression_rank=3 if three else 2, determinant=determinant, + generator_pair_checks=checks) + + +def check_upper(item, collected): + ports, contacts = collected['ports'], collected['contacts'] + a = [[Q(0)] * 8 for _ in ports] + for target, cut, register, weight in item['terms']: + key = target, cut, register + need(key in contacts, 'unavailable upper contact') + a[target] = [x + Q(weight) * y for x, y in zip(a[target], contacts[key])] + residual = [[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 = rank(residual) + if item['cut'] == 2754: + u, v = [0, 0, -1, 1, 0, 0, 0, 1], [0, -1, 0, 0, 0, 0, 0, 0] + alpha, beta = [0, 1, 0, 0, 0, 0, 0, 2], [0, 0, 1, 0, 0, 0, 0, 0] + explicit = [[u[i] * alpha[j] + v[i] * beta[j] for j in range(8)] for i in range(8)] + need(residual == explicit, 'explicit rank-two residual differs') + correction = [[Q(t == s) - Q(dot(ports[t], ports[s]), 8) + + 12 * dot(a[t], ports[s]) for s in range(104)] for t in range(104)] + large_rank = rank(correction) + need(large_rank == 96 + small_rank == item['minimum'], 'upper correction rank') + return dict(cut=item['cut'], contacts=len(item['terms']), residual_rank=small_rank, + full_source_correction_rank=large_rank) + + +def run(certificate=None, collected=None): + certificate = trace.read(HERE / 'WITNESS.json') if certificate is None else certificate + wanted = validate_certificate(certificate) + collected = trace.collect([2753, 2823], wanted) if collected is None else collected + need(not collected['receipt']['input_overrides'], 'acceptance requires pinned inputs') + lower99 = check_lower(collected['pools'][2753], collected['ports'], certificate['lower_vectors'], True) + lower98 = check_lower(collected['pools'][2823], collected['ports'], certificate['lower_vectors'], False) + upper = [check_upper(item, collected) for item in certificate['upper_witnesses']] + return dict(schema='p104-prefix-tail-result/1', status='PASS_P104_PREFIX_TAIL', + intervals=[dict(start=2718, end=2753, minimum=99), + dict(start=2754, end=2823, minimum=98)], + lower_certificates={'2753': lower99, '2823': lower98}, + upper_certificates=upper, trace=collected['receipt'], + scope='Rational unchanged-trace pooled availability; no chronological or paid-cost claim.') + + +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 == trace.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'], '99 through2753; 98 from2754 through2823') + + +if __name__ == '__main__': + main()