diff --git a/research/p104-helper-subspace-splits/NOTICE b/research/p104-helper-subspace-splits/NOTICE new file mode 100644 index 0000000000..f34687ff7e --- /dev/null +++ b/research/p104-helper-subspace-splits/NOTICE @@ -0,0 +1,21 @@ +New helper-subspace construction, proof and replay: +Ali Romman with substantial OpenAI Codex assistance. Apache-2.0. +The same assistant performed the construction and author-side checks. + +Retained contributions: +Pierre-Loic Doulcet (hexapode): PR5565 commuting-contact construction, used as the exact source. +Ali Romman: PR5580 contact step and PR5544/5545 complete P104 caller. +Joel Pulikkan (GamingPuzzled): PR5569 priced helper handoff. +DreamingOfClouds: PR5561 free helper endpoints and PR5568 search tools. +thu-nmrc: PR5551 contact improvements. +Gareth Davidson (bitplane): PR2305 source composition. +David Arias: PR2152 coalesced P104 word. +Cinna Davis: PR2219 private reuse and the controller lineage. +Jacob Alan Sussman: productive mixed-target recursion. +zxv and Cao Yifan: exact intervals, compiler and native/pricing lineage. +GamingPuzzled: PR5472 successor handoff, a predecessor to the split concept. +The retained source notices preserve earlier geometry, BIT and analytic credit. + +The elementary rank-one basis identity is not claimed as a new general +linear-algebra theorem. The contribution is its explicit independent-target +use on this P104 word and the complete conditional kappa improvement. diff --git a/research/p104-helper-subspace-splits/PROOF.md b/research/p104-helper-subspace-splits/PROOF.md new file mode 100644 index 0000000000..ca97998444 --- /dev/null +++ b/research/p104-helper-subspace-splits/PROOF.md @@ -0,0 +1,208 @@ +# Independent helper splits and the complete cost + +This proof changes the helper input and output contract of the exact PR5565 +word. It retains every main endpoint, paid Gaussian call and owned lifetime. +All scalar identities below are over the rationals. The native check supplies +exact phases and the rule for every positive tensor width. + +## 1. A split criterion + +Let a group of helpers have the same initial chart U and final chart V. +The complete source word returns each of these helpers unchanged in normalized +coordinates and has no helper contribution to any other output. +Let F be a strict intermediate chart, with U contained in F and F contained +in V. At one chronological cut, let P be the scalar prefix matrix and S the +scalar suffix matrix. The matrices include every public input and output. +Owned fields follow the source initialization and erasure contract. + +Suppose a row a and a column b use only fields at chart F. Suppose c and d +use only the specified helper group, and + +```math +aP=c,\qquad Sb=d,\qquad ab=cd=1. +``` + +Choose a helper role p at F. There are invertible scalar matrices G and J +with + +```math +e_p^T G=c,\quad Gd=e_p,\qquad e_p^T J=a,\quad Jb=e_p. +``` + +Here G acts only on helpers with boundary charts U and V. J acts only on +fields at F. The construction emits these matrices as ADD and dyadic-unit +SCALE operations. Its row and column elimination uses the unit pairings. +The emitted program and its inverse are explicit; no dense matrix operation +is assigned zero implementation cost. + +Apply G inverse at the input. At the cut, apply J. Role p then contains the +independent coordinate t=c h. Retain p as an output at F. Introduce one new +independent input z at F. Use its new role in place of p in J inverse and in +the complete suffix. Finally apply G at V, with the same role substitution. +The suffix state changes by b(z-a P h), so its helper output is + +```math +h+d(z-ch). +``` + +The final change of basis gives + +```math +G[h+d(z-ch)]=Gh+e_p(z-t). +``` + +Thus the former p coordinate is replaced by the independent z coordinate; +all other helper coordinates and every main output retain their required +values. The old t coordinate has already been returned at F. This replaces +one U-to-V target by a U-to-F target and an F-to-V target. + +This uses a new input, not two outputs computed from one input. It does not +assume a helper is zero. The early output is a public field and stays live +until the caller returns. The successor input is public from the start and +is first used at the cut. No new COPY, CLEAR or owned lifetime is introduced. +The source's owned erasures remain charged under the inherited contract. + +All three basis changes use common physical charts. They therefore commute +with the relevant chart operator. Native normalization gives ranks +`dim(F)-dim(U)` and `dim(V)-dim(F)` with their exact phases. Scalar coefficients +stay outside the tensor substitution. The frame induction applies at every +positive width; it is not a test at width one alone. + +## 2. The first explicit split + +The source is PR5565 at `9af814164b9dfc21f19ec737959d67cb71488c95`. +Use the cut after zero-based event 13775, chart 120 of dimension five, and +pivot 648. The boundary group has initial chart 3 (dimension zero) and final +chart 127 (dimension nine). With e_r the coordinate at role r, the exact +vectors are + +```math +a=e_{652}^T,\quad b=e_{652}-e_{648}+e_{650}-e_{649}, +``` + +```math +c=e_{652}^T,\quad d=e_{652}-2e_{205}-e_{648}+e_{650}-e_{649}. +``` + +The complete prefix gives aP=c; the complete suffix gives Sb=d. +Both pairings are one. The boundary basis uses six scalar events and the +local basis uses five. With their inverses, the split adds eighteen ADDs +and four sign SCALEs. It replaces H9 by independent H5 and H4 targets. +The full sequence, including each updated event index, is in `SPLITS.json`. + +`check_cut` reconstructs each prefix functional and propagates each suffix +column. It checks that all other input and output coefficients are zero. +The verifier then checks every public and owned row after each complete +split. A separate dense-integer transpose replay checks all 571,536 entries +of the final 756 by 756 interface. + +## 3. The complete target change + +The thirteen splits are + +- six H9 to H4 + H5; +- five H9 to H2 + H7; +- two H9 to H1 + H8. + +They add 13 independent helper inputs. The source's 735 public fields become +748, of which 540 are helpers and 208 are main fields. Eight owned lifetime +roles remain; only one is live at a time. The 25,133 source events become +25,475. Every source paid occurrence remains, with the same ordered pair of +charts, rank and ownership. Some register names change to identify the +successor input. The new local helper profile is + +```text +{1:2, 2:5, 4:89, 5:11, 7:5, 8:16, 9:412}. +``` + +The verifier also replays the retained PR5580 source. It checks that PR5565 +changes its local paid profile by `-8H1-H3-2H4+4H5` and its helper profile +by `-H8+H9`. These source changes are by Pierre-Loic Doulcet (hexapode). The new splits retain +that paid profile. The earlier fifteen-split component on PR5580 is frozen +at `31a4de233bbdd65c04c63dc3398ecf0eed8e1375`. Two of its cuts are absent +from the PR5565 composition, but the lower paid cost gives a larger kappa. + +For every 0(a+b)^t`. Each split strictly increases the target moment and leaves +the paid moment fixed. The signed local target change is + +```math +2H_1+5H_2+6H_4+6H_5+5H_7+2H_8-13H_9. +``` + +Its rank mass is zero, as required. A source-bound complete caller, not a +standalone packing relaxation, supplies the resulting exponent claim. + +## 4. Native maps and the caller + +The exact signed-Pauli and phase verifiers check every paid chart change, +every helper target and every main adapter. The local replay checks a strict +nested chart relation on each public move and the source's descending owned +moves. Each helper target is strictly productive. + +Cinna Davis's p16/a7 controller and Ali Romman's all-forward implementation +from PR5544 remain literal inputs. All 18 full calls use the new local word +with fresh independent helpers. Sixteen backward main interfaces use the +retained signed exchanges and central-square translations. These wrappers +act only on the main pair. They do not alter a new helper output. + +The physical caller check retains all 104 central ports, 7,488 boundary +contacts, 53,248 central-square column checks, 3,328 main Gaussian targets, +15 thin query sites and 3,120 whole idle jobs. It checks native routes, +spectators, exact phases and every whole target. The complete counts are + +```text +paid calls: 66726 +productive fields: 13048 = 18*540 + 32*104 +rank mass surplus: 760 +maximum target: 145 +maximum paid rank: 72 +``` + +The invoice is counted twice, once from literal events and once from the +controller path lengths. Input and output normalizers, added scalar basis +operations, routes, owned allocation and erasure, queries and idles are all +included. The new independent field count enters the completion-tail bound. +It is not left at the old 12,814 value. + +## 5. Strictification, compiler and outer transfer + +Two independent rational interval engines evaluate the complete moments. +The exact raw crossing is in (0.00310045630724, 0.00310045630725). +`RESULT.json` gives its rational endpoints and the strict tested margin. The claimed kappa is 0.00310045 and the tested saving is +0.0031004505. Their gap funds the finite compiler and outer parameters. An exact negative +derivative bound on [0,0.0034] makes this crossing the raw ceiling for this +fixed invoice under the retained BIT cap. It is not a global optimum. + +Power 1024, cutoff 17, target floor 18 and tail offset 1/5 are retained. +The extra independent fields require a different tail bound: both charged +tail ratios are below 39/40, and `(39/40)^128 < 1/16`. Eight such blocks still +give the retained `2^-32` remainder. The fixed reserve is `10^-10`. +The complete normalized cost is strictly less than one. The old cutoff 20 +fails and is retained as a control. + +The compiler checks its finite integer threshold, initial range, shifted +exits, complement capacity, logarithm power 1024 and predecessor integer point. The old logarithm +power 1000 does not meet the new complement-capacity inequality. +The ordinary BIT saving remains 0.0034. All 54 strict outer conditions and +four functional conditions are checked with exact rational arithmetic. +The scalar growth bound uses fewer than 26,000 local operations and the +retained per-operation bound. The native growth bound uses the actual sum +of local paid ranks. The complete ordinary-work allowance remains below +`10^9`; the local scalar and route allowance remains below `10^7` per call. + +## 6. Scope of acceptance + +The five selected framework assumptions remain: native implementation at +all widths, owned erasure, uniform compiler closure, precision and tape +cost, and analytic integer recovery. The source helper-endpoint contract +also remains. This package proves the new finite interface, the chart +identities and every new numerical condition within that framework. + +The enormous uniform word and complete rounded multiplier are not +materialized. These are author-side checks by the same AI-assisted author. +They are not independent human acceptance or a proof-kernel theorem. +The final exact discovery screen tests 52 boundary groups and finds no +further candidate in its finite basis-pair class. It does not prove a maximum +over bases, cuts, scalar programs, +frames, controllers or multiplication algorithms. diff --git a/research/p104-helper-subspace-splits/README.md b/research/p104-helper-subspace-splits/README.md new file mode 100644 index 0000000000..f6303a8813 --- /dev/null +++ b/research/p104-helper-subspace-splits/README.md @@ -0,0 +1,167 @@ +# Conditional kappa 0.00310045 from independent helper splits + +This construction raises complete conditional **kappa to 0.00310045**. +The gain over [PR5565](https://github.com/CrocSwap/integer-mult-bounds/pull/5565) +(0.00308520) is **0.00001525**, about **0.4943%**. The gain over selected +0.003027288235 is **0.000073161765**. The selected record is unchanged. + +The mechanism changes the independent helper basis. At a common-frame cut, +one helper combination can finish early and a fresh independent input can +use the remaining program. Thirteen explicit splits replace 527 helper +jobs by 540 helper jobs. They add 342 scalar events and no recursive Gaussian +call. Both input and output support are checked over every field; a local +pure row alone does not earn a new target. + +Read the [proof](PROOF.md), [exact cuts](SPLITS.json), [complete word](WORD.json.gz), +[receipt](RESULT.json), [source pins](SOURCES.json), and [validation record](VALIDATION.md). +The first split is an explicit 22-event change from one H9 target to independent +H5 and H4 targets. The complete caller uses the new word at all 18 full sites. + +| Quantity | Result | +| --- | ---: | +| Local public inputs | 748 | +| Independent helpers per full call | 540 | +| Owned lifetimes / peak owned fields | 8 / 1 | +| Local events | 25,475 | +| Complete paid calls | 66,726, unchanged | +| Complete productive fields | 13,048 | +| Complete rank-mass surplus | 760, unchanged | +| Tested saving | 0.0031004505 | +| Complete conditional kappa | 0.00310045 | +| Raw crossing | (0.00310045630724, 0.00310045630725) | +| Exact native maps | 2,923 | + +The added helpers enter the complete completion-tail calculation. The tail +bound changes to 39/40, with `(39/40)^128 < 1/16`. The compiler logarithm +power changes from 1000 to 1024. Every native map, helper normalizer, main +adapter, scalar basis operation, route, COPY/CLEAR cost, thin query and +whole idle is included. The ordinary BIT saving remains 0.0034. Two exact +moment engines and all 54 strict plus four functional outer conditions are +checked. The receipt gives the raw crossing and the finite compiler threshold. +A negative derivative bound supplies the raw ceiling for this fixed invoice +on [0,0.0034]; it does not bound other constructions. + +## Reproduce + +Use Python 3.12 and the standard library, from the repository root: + +```sh +python3 -B scripts/research_package.py --package research/p104-helper-subspace-splits --check-only +python3 -B scripts/research_package.py --package research/p104-helper-subspace-splits +``` + +The registered hook runs normally and with `-O`. Its success markers are +`PASS_P104_HELPER_SUBSPACE_KAPPA_00310045` and +`PASS_REGISTERED_RESEARCH_PACKAGE`. Direct replay needs no Git or network: + +```sh +python3 -I -B research/p104-helper-subspace-splits/verify.py +python3 -I -O -B research/p104-helper-subspace-splits/verify.py +``` + +Normal replay is read-only. `--write` explicitly regenerates the two result +artifacts. Inputs are authenticated before imported source code executes. +Each replay uses a fresh bytecode-cache path. The checks reject contaminated +prefix and suffix vectors, missing boundary basis operations, an unearned +whole target, extra helper credit, a missing paid call, a wrong native phase, +a missing central translation, an inadequate cutoff and insufficient BIT stock. + +## Scope and coordination + +The scientific base is canonical main +`5e0052ca0aa3036a3afa8b0438927377c8d97d53`, priority revision 7. +The [canonical claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/5125#discussioncomment-19183208) +records the changed question and local screens. The final publication overlap +cache covered 334 open PRs and 4,863 Discussion records, with complete remote +pagination and incomplete sparse local coverage. Source and coverage details +are coordination evidence, not a novelty proof. + +The consumed PR5565 word is pinned to +`9af814164b9dfc21f19ec737959d67cb71488c95`. It includes Pierre-Loic Doulcet's published +commuting-contact cascade and the released PR5580/PR5569/PR5561 lineage. +The source copy is retained in this branch at commit +`bf64e66656843a64e798b8374cd9f53add3f6f46`. Its SHA256 and Git blob match +the recorded PR5565 source. The PR5580 copy remains an active comparison +input: replay checks the exact paid and helper changes supplied by PR5565. +Registered replay needs this branch history and its main base; it does not +need cached objects from unmerged PR branches. + +The earlier fifteen-split component on PR5580 remains frozen at +`31a4de233bbdd65c04c63dc3398ecf0eed8e1375`. Two cuts are absent from this +composition. PR5565's lower paid cost more than offsets that lost target +gain. The complete claim increases by 0.00000206 over that component. +This package introduces no new commuting-contact search. +No new Gaussian itinerary is introduced. Active frame-extension work in +[Discussion5575](https://github.com/CrocSwap/integer-mult-bounds/discussions/5575) +is a separate investigation. + +The final refresh also found [parallel coupled-basis and handoff work](https://github.com/CrocSwap/integer-mult-bounds/discussions/5125#discussioncomment-19154639). +It uses the same rank-one mechanism and separately changes paid boundary +work. The [public composition handoff](https://github.com/CrocSwap/integer-mult-bounds/discussions/5125#discussioncomment-19183908) +releases the earlier fifteen cuts and leaves the six paid-boundary changes +with the parallel claim. That claim is testing their composition. This +package composes only the released PR5565 source with helper splits. No +exclusive method novelty or gain from the parallel paid changes is claimed. +The new scalar contacts and input count change the hypotheses of +[PR5590](https://github.com/CrocSwap/integer-mult-bounds/pull/5590)’s fixed-contact floor. + +The scope changes the scalar word, the input count and the target contract. +It therefore differs from a scalar-only simplification or a fixed-input +helper stop. The unchanged paid histogram now supports a different, +fully independent target histogram. + +The five selected framework assumptions remain: native implementation at +all widths, owned erasure, uniform compiler closure, precision and tape cost, +and analytic recovery. The helper-endpoint contract also remains. +The complete rounded multiplier and enormous uniform compiler word are not +materialized. The same AI-assisted author constructed and checked this +package. Independent human review, proof-kernel acceptance and global +optimality are not claimed. + +## Sources and credit + +- **Pierre-Loic Doulcet / hexapode**: [PR5565](https://github.com/CrocSwap/integer-mult-bounds/pull/5565) + supplies the exact commuting-contact source word. +- **Ali Romman**: [PR5580](https://github.com/CrocSwap/integer-mult-bounds/pull/5580) + supplies its preceding contact step; [PR5544](https://github.com/CrocSwap/integer-mult-bounds/pull/5544) + and [PR5545](https://github.com/CrocSwap/integer-mult-bounds/pull/5545) supply + the complete P104 caller and source replay. +- **Joel Pulikkan / GamingPuzzled**: [PR5569](https://github.com/CrocSwap/integer-mult-bounds/pull/5569) + supplies the priced helper handoff; [PR5472](https://github.com/CrocSwap/integer-mult-bounds/pull/5472) + supplies an earlier successor-handoff construction. +- **DreamingOfClouds**: [PR5561](https://github.com/CrocSwap/integer-mult-bounds/pull/5561) + supplies free helper endpoints and PR5568 supplies search tools. + **thu-nmrc** supplies the PR5551 contact improvements. +- **Gareth Davidson / bitplane**, **David Arias** and **Cinna Davis** supply + the PR2305 composition, PR2152 coalesced word and PR2219 private reuse. + Cinna Davis also supplies the controller lineage. +- **Jacob Alan Sussman** supplies productive mixed-target recursion. + **zxv** and **Cao Yifan** supply the retained interval, compiler and + native/pricing lineage. Source notices preserve earlier geometry, BIT + and analytic credit. + +The elementary rank-one basis identity is not claimed as a new general +linear-algebra theorem. The contribution is this explicit independent-target +construction and its complete conditional price. New work is by Ali Romman +with substantial OpenAI Codex assistance; no subagents. Apache-2.0. +See [NOTICE](NOTICE). + +## Open next questions + +An independent reviewer can check the first split and then replay the complete +package. Further gains could use a different compatible cut order, basis or +frame itinerary. Both prefix and suffix support must be proved before a +new target receives credit. The finite discovery screen does not establish a global +maximum. [TASK.json](TASK.json) gives the first checks and remaining obligations. + +The optional continuation screen is reproducible with: + +```sh +python3 -I -B research/p104-helper-subspace-splits/search.py +``` + +It tests exact elimination-basis pairs at cuts immediately after MOVE events, +inside equal-boundary helper groups. On the final word it finds no further +candidate in 52 groups. This result covers those tested pairs. It does not +exclude different cut sequences, arbitrary basis combinations or new frames. +The complete-kappa verifier does not depend on a discovery search failure. diff --git a/research/p104-helper-subspace-splits/RESULT.json b/research/p104-helper-subspace-splits/RESULT.json new file mode 100644 index 0000000000..35f75c8555 --- /dev/null +++ b/research/p104-helper-subspace-splits/RESULT.json @@ -0,0 +1,487 @@ +{ + "authenticated_inputs": 13, + "complete_cost": { + "compiler": { + "H": 707182000000000, + "N": "2^707182000000000", + "eta": { + "lower": "0.000000136964415492079857925247", + "upper": "0.000000136964415492079857925248" + }, + "gap": "1/14000000000", + "integer_test_exponent": 50513, + "logarithm_power": 1024, + "theta": "63/64", + "uniform_saving": "21703153/7000000000", + "word_materialized": false + }, + "full_forward_calls": 18, + "gain": "61/4000000", + "kappa": "62009/20000000", + "kappa_decimal": ".00310045", + "margin_at_previous": { + "lower": "3.715057037515374246068780385152", + "upper": "3.715057037515374246068780385153" + }, + "negative_controls": { + "old_BIT": "Rejected by outer inequalities", + "old_cutoff": "Rejected by completion-tail ratio greater than one" + }, + "nonrecursive": { + "fixed_scalar_growth_bound": "At most 2^(16*26000) before native factors; a declared constant, not an attained norm.", + "local_paid_rank_mass": 6014, + "local_routes": 5183000, + "local_scalar": 220232, + "peak_owned_fields": 1, + "raw_budget": 1000000000, + "raw_scalar_upper": 184647552, + "tensor_native_growth_bound": "Each rank-r Gaussian has row l1 norm at most 2^(rf); use local_paid_rank_mass for the whole word." + }, + "ordinary_BIT": { + "admitted": "17/5000", + "after_cover": "69/20000", + "atom": "1/250", + "before_cover": "3459/1000000", + "ordinary_saving": "8590884599/2500000000000", + "prime_rule": "odd q > 2^26*N^5 avoiding all fixed denominators and rank witnesses" + }, + "outer": { + "functional_checks": { + "actual_new_BIT_stock_sublinear": "3485999999253/3500000000000", + "fixed_halo_explicit_metadata_branch": "269500000001/3500000000", + "new_BIT_row_stock_sublinear_in_active_group": "13957999997009/14000000000000", + "new_semantic_group_guard": "3/14000000000" + }, + "margins": { + "boundary_algebraic_matrix": "607688255956593697/196000000000000000000", + "fused_gaussian": "607688255869781091/196000000000000000000", + "global_coordinate_router": "1356447/437500000", + "group_bit_router": "18990258433430659/6125000000000000000", + "group_scans": "6999999999/7000000000", + "main_transform": "607688241956593697/196000000000000000000", + "microbox_face_corrections": "269500000001/3500000000", + "polynomial_products": "13999999999/14000000000", + "sparse_union_movement": "80232688255956593697/196000000000000000000" + }, + "parameters": { + "a": "1356447/437500000", + "b": "8681261/2800000000", + "beta": "13999999997/14000000000", + "bit_saving": "17/5000", + "cap_xi": "178232688241956593697/196000000000000000000", + "complex_uniform_saving": "21703153/7000000000", + "d": "1/14000000000", + "epsilon": "13999999999/14000000000", + "kappa": "62009/20000000", + "lambda_": "3987598199/4000000000", + "lambda_prime": "13956593697/14000000000", + "layout": "1/14000000000", + "q": "43406303/14000000000", + "r0": "1/140000000000", + "stop": "1/14000000000", + "tested_saving": "6200901/2000000000" + }, + "strict_checks": { + "actual_bit_above_effective": "131053/437500000", + "actual_logarithmic_gamma_guard": "1/14000000000", + "actual_logarithmic_group_guard": "17767311779043406303/98000000000000000000", + "alpha_logarithm_absorption": "1/140000000000", + "boundary_algebraic_matrix_above_kappa": "55956593697/196000000000000000000", + "cap_above_band": "80232688241956593697/196000000000000000000", + "cap_below_cell": "17767311744043406303/196000000000000000000", + "cap_below_phase_cell_power": "213767311758043406303/196000000000000000000", + "complex_above_effective": "1/14000000000", + "complex_below_one_over_32": "78818739/2800000000", + "complex_endpoint": "1/7000000000", + "epsilon_below_one": "1/14000000000", + "epsilon_positive": "13999999999/14000000000", + "fine_prime_halo_umbrella": "7/2", + "fused_gaussian_above_kappa": "55869781091/196000000000000000000", + "gaussian_above_main": "6956593697/98000000000000000000", + "global_coordinate_router_above_kappa": "1/3500000000", + "global_gamma_power_slack": "9/140000000000", + "group_below_dimension": "1/7000000000", + "group_bit_router_above_kappa": "2183430659/6125000000000000000", + "group_gauge_power_slack": "17767311778343406303/98000000000000000000", + "group_key_fits_record": "1/7000000000", + "group_positive": "13999999997/14000000000", + "group_scans_above_kappa": "6978296849/7000000000", + "halo_covers_generic_inverse_radius": "5", + "improvement_over_user_baseline": "684739790400418148631/500000000000000000000000", + "lambda_above_internal": "1/28000000000", + "lambda_above_sigma": "3/28000000000", + "lambda_above_tau": "1/28000000000", + "lambda_prime_above_lambda": "1/28000000000", + "lambda_prime_above_leaf": "5591318739/39200000000000000000", + "leaf_saving_above_effective": "2791318739/39200000000000000000", + "main_transform_above_kappa": "41956593697/196000000000000000000", + "membership_arithmetic_fits_record": "1/14000000000", + "microbox_face_corrections_above_kappa": "134744574213/1750000000", + "microbox_halo_volume": "1106000000003/14000000000", + "new_complex_uniform_saving_above_b": "1/14000000000", + "new_semantic_guard_with_C1_one": "1/14000000000", + "polynomial_products_above_kappa": "13956593699/14000000000", + "positive_layout_slack": "1/14000000000", + "q_below_effective": "1/14000000000", + "q_below_internal": "1/14000000000", + "q_below_leaf": "5591318739/39200000000000000000", + "q_positive": "43406303/14000000000", + "short_record_fallback": "2791318739/2800000000", + "source_axis_superpolynomial": "1/14000000000", + "sparse_union_movement_above_kappa": "79625000055956593697/196000000000000000000", + "stop_below_one": "13999999999/14000000000", + "stop_positive": "1/14000000000", + "strassen_integer_power_gap": "1951441519231", + "support_router_span": "3/14000000000", + "theta_positive_polynomial_power": "2", + "union_header_fits_record": "3/14000000000", + "union_tag_work_per_visit_fits_record": "3/14000000000" + } + }, + "paid": { + "1": 41214, + "16": 416, + "2": 8262, + "24": 416, + "3": 8874, + "32": 416, + "4": 1656, + "40": 416, + "48": 416, + "5": 3024, + "56": 416, + "6": 324, + "64": 416, + "7": 252, + "72": 208 + }, + "paid_calls": 66726, + "previous_open_pr5565": "7713/2500000", + "productive_fields": 13048, + "query_shears": 15, + "rank_mass_surplus": 760, + "raw_ceiling": { + "derivative_upper": "-741665511346505619707405027113237790341393747177503845065075007/3138550867693340381917894711603833208051177722232017256448", + "interval": [ + "0", + "17/5000" + ] + }, + "raw_headroom": [ + "157681/25000000000000", + "25229/4000000000000" + ], + "raw_root_interval": [ + "77511407681/25000000000000", + "12401825229/4000000000000" + ], + "relative_gain_percent": "7625/15426", + "strictification": { + "alpha": { + "lower": "0.999999994094860604597376680636", + "upper": "0.999999994094860604597376680637" + }, + "cutoff": 17, + "delta": { + "lower": "0.972208404163139976829701213167", + "upper": "0.972208404163139976829701213168" + }, + "floor": 18, + "gamma": { + "lower": "0.967537821927968182942254182934", + "upper": "0.967537821927968182942254182935" + }, + "normalized_paid_upper": "5242880004882813/5242880536870912", + "power": 1024, + "reserve": "1/10000000000", + "tail_block": 128, + "tail_decay": "39/40", + "tail_offset": "1/5", + "tested": "6200901/2000000000" + }, + "targets": { + "1": 36, + "145": 208, + "17": 416, + "2": 90, + "25": 416, + "33": 416, + "4": 1602, + "41": 416, + "49": 416, + "5": 198, + "57": 416, + "65": 416, + "7": 90, + "73": 208, + "8": 288, + "9": 7416 + }, + "whole_idle_jobs": 3120 + }, + "limits": [ + "The five selected framework assumptions and helper-endpoint contract remain.", + "No complete rounded multiplier or enormous uniform compiler word is materialized.", + "No independent human or proof-kernel acceptance or global optimality is claimed." + ], + "local": { + "endpoint_coefficients": 571536, + "helpers": { + "1": 2, + "2": 5, + "4": 89, + "5": 11, + "7": 5, + "8": 16, + "9": 412 + }, + "owned_lifetimes": 8, + "paid": { + "1": 2203, + "2": 459, + "3": 493, + "4": 92, + "5": 168, + "6": 18, + "7": 14 + }, + "paid_rank_mass": 6014, + "peak_owned_fields": 1, + "public_inputs": 748, + "real_scalar_allowance": 220232 + }, + "local_helper_delta": { + "1": 2, + "2": 5, + "4": 6, + "5": 6, + "7": 5, + "8": 2, + "9": -13 + }, + "native": { + "distinct_maps": 2923, + "helper_normalizers": 1080, + "helpers": { + "1": 2, + "2": 5, + "4": 89, + "5": 11, + "7": 5, + "8": 16, + "9": 412 + }, + "main_adapters": 208, + "proof": "Every signed Pauli image and exact global phase; frame induction at every positive tensor width", + "recipe_payload_sha256": "b2e6b538f6152ccf0024ca57381e46b2fe6b75b89504d935009dade234cc3f18", + "wrong_phase_rejected": true + }, + "negative_controls": { + "contaminated_prefix": "Exact prefix functional; no other input", + "contaminated_suffix": "Exact suffix direction; no other output", + "extra_helper_credit": "Every productive helper has a native target", + "missing_central_translation": "Rejected by the complete Laurent endpoint", + "missing_input_basis": "All public and owned rows", + "missing_output_basis": "All public and owned rows", + "unearned_whole_target": "All public and owned exits", + "unpaid_gaussian": "Complete field and call counts" + }, + "physical_caller": { + "central_square_columns": 53248, + "full_calls": 18, + "main_targets": { + "145": 208, + "17": 416, + "25": 416, + "33": 416, + "41": 416, + "49": 416, + "57": 416, + "65": 416, + "73": 208 + }, + "new_paid_jobs": 0, + "physical_contacts": 7488, + "ports": 104, + "route_payload_sha256": "7f4f0ca768ffbc4f93dcff575592c4c67411f46b4289e45b73f715a2ad47b142", + "tensor_rule": "Factorwise native maps; scalar signs stay outside the tensor power.", + "whole_idle_jobs": { + "16": 416, + "24": 416, + "32": 416, + "40": 416, + "48": 416, + "56": 416, + "64": 416, + "72": 208 + }, + "wrapper_sites": [ + 1, + 3, + 5, + 7, + 9, + 11, + 13, + 15, + 17, + 19, + 21, + 23, + 25, + 27, + 29, + 31 + ] + }, + "published_source_delta": { + "helpers": { + "8": -1, + "9": 1 + }, + "paid": { + "1": -8, + "3": -1, + "4": -2, + "5": 4 + } + }, + "separate_columns": { + "arithmetic": "Dense integer rows with binary denominators; reverse chronology", + "coefficients": 571536, + "columns": 756 + }, + "splits": [ + { + "cut_after": 13775, + "events": 25155, + "pivot": 648, + "public": 736, + "ranks": [ + 5, + 4 + ] + }, + { + "cut_after": 13765, + "events": 25177, + "pivot": 592, + "public": 737, + "ranks": [ + 5, + 4 + ] + }, + { + "cut_after": 13706, + "events": 25195, + "pivot": 664, + "public": 738, + "ranks": [ + 5, + 4 + ] + }, + { + "cut_after": 13673, + "events": 25217, + "pivot": 680, + "public": 739, + "ranks": [ + 5, + 4 + ] + }, + { + "cut_after": 12526, + "events": 25253, + "pivot": 259, + "public": 740, + "ranks": [ + 4, + 5 + ] + }, + { + "cut_after": 12448, + "events": 25285, + "pivot": 432, + "public": 741, + "ranks": [ + 4, + 5 + ] + }, + { + "cut_after": 13961, + "events": 25299, + "pivot": 722, + "public": 742, + "ranks": [ + 2, + 7 + ] + }, + { + "cut_after": 13647, + "events": 25317, + "pivot": 14, + "public": 743, + "ranks": [ + 2, + 7 + ] + }, + { + "cut_after": 13648, + "events": 25335, + "pivot": 76, + "public": 744, + "ranks": [ + 2, + 7 + ] + }, + { + "cut_after": 13648, + "events": 25369, + "pivot": 345, + "public": 745, + "ranks": [ + 2, + 7 + ] + }, + { + "cut_after": 13637, + "events": 25419, + "pivot": 573, + "public": 746, + "ranks": [ + 2, + 7 + ] + }, + { + "cut_after": 12078, + "events": 25445, + "pivot": 405, + "public": 747, + "ranks": [ + 8, + 1 + ] + }, + { + "cut_after": 12610, + "events": 25475, + "pivot": 225, + "public": 748, + "ranks": [ + 8, + 1 + ] + } + ], + "status": "PASS_P104_HELPER_SUBSPACE_KAPPA_00310045" +} diff --git a/research/p104-helper-subspace-splits/SOURCES.json b/research/p104-helper-subspace-splits/SOURCES.json new file mode 100644 index 0000000000..f83bf3c818 --- /dev/null +++ b/research/p104-helper-subspace-splits/SOURCES.json @@ -0,0 +1,132 @@ +{ + "schema_version": 1, + "base_commit": "5e0052ca0aa3036a3afa8b0438927377c8d97d53", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "fc3d4ba105e1f097d0d7d051a308281e86ab1446", + "sha256": "66974efdced4083c00025f97d95d83909a226cdf801edb9301c195c6641f6903" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "research/p104-productive-controller/caller.py", + "usage": "input", + "git_blob": "6ac5e735691555ecafe2afbcff71edd923178113", + "sha256": "300d40043953e4f6aecfde8f2d1004b8ad6dc5a79ec3c7666c9908c2466c91c8" + }, + { + "path": "research/p104-productive-controller/CONTROLLER.json", + "usage": "input", + "git_blob": "cc539db709cf7a6c42872c4380902736ad453af3", + "sha256": "a84f6bbd547379597464e56c420cc665f96bc43a9a1351eed4b7cd0fce3cc4b9" + }, + { + "path": "research/joint-helper-lattice/CONTROLLER.json", + "usage": "input", + "git_blob": "49a2f0675819f9deeea27ed77be2c2b6ff2e87e5", + "sha256": "1f5d6aa267e4e66048818714b5d3b5eae17a58abe91d15deeaa34574f7391a5f" + }, + { + "path": "research/p104-native-channel/vendor/clifford_exact.py", + "usage": "input", + "git_blob": "166841a037f069249f6f7f6dedb89248812f59e2", + "sha256": "2982ead07721e83358dc67c6f49c2b4c16a236a6bebdfd72f58221be1f5d0962" + }, + { + "path": "research/p104-native-channel/vendor/native_verify.py", + "usage": "input", + "git_blob": "2c209dfa9cfade3bc20ac5fc9d876b433a147f8c", + "sha256": "3049471905b47b385c88378a1a3be7a18b8858aadd035b8a6da2f4a03b470f38" + }, + { + "path": "research/pr4359-p7-padding/native_inventory.py", + "usage": "input", + "git_blob": "8d2d96e3998254c2333c43fe47cdfd074cbd811e", + "sha256": "65539acaf45bdfe8c5aee6830f9c9b3d1107c442a60842ef803fdd7688de8f32" + }, + { + "path": "research/kappa-0023-productive-jobs/dependencies/kappa-next-regime/direct-decoder/sources/DATA-PHASES.json", + "usage": "input", + "git_blob": "d9a4f84211182ca200c081ea061d724c8a2cfb70", + "sha256": "c5916ff312678f12aba403847643fbbc29f643acec60bdf836fa56cd3e8251fa" + }, + { + "path": "research/higher-moment-strictification/verify.py", + "usage": "input", + "git_blob": "4b24a5096154736ce060474eb8c72dc64c303699", + "sha256": "0ce7e7137422d5ffeda22085c81fa88471bbe963100fdad62e659f1e3bf89326" + }, + { + "path": "research/kappa-rebuild/architecture/mixed_target_probe.py", + "usage": "input", + "git_blob": "4fc05ab08138218ba9f09e5c89b649afae7c914e", + "sha256": "011c3c9d0cf81103dc84d709a0e36793eb7c5ae3f23c85eac27650ef13afa04a" + }, + { + "path": "research/pr4359-p7-padding/dependencies/compiler-refill/endpoint.py", + "usage": "input", + "git_blob": "340e1f0ffb8a1a9c38fbbd9119580b6d23e01b59", + "sha256": "d097e55f06c3f244f2074ffd7c1a0a5f3c4b4b6a6accf9619d1dde5c0ae85e15" + }, + { + "path": "research/query-thinned-controllers/RESULT.json", + "usage": "input", + "git_blob": "e0695152c98d727edfd0d2034b58a1c7e8682c0c", + "sha256": "6ebfc8c0f09166f4834e9d7427410cb31aefff2cd4d4ce588c8e52c9c70e9a0f" + }, + { + "path": "research/p104-helper-subspace-splits/inputs/PR5580-WORD.json.gz", + "usage": "input", + "git_blob": "9434855e7dad0d0236d23210b3e71a2b83a9ae64", + "sha256": "b2a98c4bd0dbe86c09e9d15ee060dcf1aab09dbef90aa1e2127676f4039f406b", + "pin": "head:29fe88ba218b5d2192d8e31f07a01d1141afdacd:research/p104-helper-subspace-splits/inputs/PR5580-WORD.json.gz" + }, + { + "path": "research/p104-productive-controller/local.py", + "usage": "provenance", + "git_blob": "dbb3d56a4f5b733bb0c32a91249d1f6a7e1ab5d2", + "sha256": "878734dfd64c4b9d362d0ae476cc5c2a19fe93e48b7378763b23f3e0dd0a5a71" + }, + { + "path": "research/p104-helper-subspace-splits/inputs/PR5565-WORD.json.gz", + "usage": "input", + "git_blob": "4ebe6fcb7adf319bf6b247cf23d89eb1ca4cd914", + "sha256": "3d62828f53e654e3db218bf4611a47aed4a677d48043713dc004db0f8a32990d", + "pin": "head:bf64e66656843a64e798b8374cd9f53add3f6f46:research/p104-helper-subspace-splits/inputs/PR5565-WORD.json.gz" + } + ], + "external_inputs": [ + { + "local_path": "inputs/PR5580-WORD.json.gz", + "source_repository": "aliromman/integer-mult-bounds", + "source_commit": "6efa248cf456d6101d757e9d09ba29711d18a13a", + "source_path": "research/p104-event-contact-step/WORD.json.gz", + "sha256": "b2a98c4bd0dbe86c09e9d15ee060dcf1aab09dbef90aa1e2127676f4039f406b", + "git_blob": "9434855e7dad0d0236d23210b3e71a2b83a9ae64" + }, + { + "local_path": "inputs/PR5565-WORD.json.gz", + "source_repository": "CrocSwap/integer-mult-bounds", + "source_commit": "9af814164b9dfc21f19ec737959d67cb71488c95", + "source_path": "research/p104-commuting-contact/WORD.json.gz", + "sha256": "3d62828f53e654e3db218bf4611a47aed4a677d48043713dc004db0f8a32990d", + "git_blob": "4ebe6fcb7adf319bf6b247cf23d89eb1ca4cd914" + } + ], + "code_derivation": [ + { + "source_repository": "GamingPuzzled/integer-mult-bounds", + "source_commit": "af9f091ac6f30c6eaacb9c27777bfbe2d0e5ffdf", + "source_path": "research/p104-priced-handoff/pricing.py", + "sha256": "a4df92b46234bb56a966df30d9c1d43251e1346e9a1ad06cf5ee30a79c7ae591", + "git_blob": "bb135338f1c57c48147cb214d14f542cdfe4e533", + "scope": "Pricing code attribution; this predecessor file is not executed." + } + ] +} diff --git a/research/p104-helper-subspace-splits/SPLITS.json b/research/p104-helper-subspace-splits/SPLITS.json new file mode 100644 index 0000000000..5108daabf7 --- /dev/null +++ b/research/p104-helper-subspace-splits/SPLITS.json @@ -0,0 +1,407 @@ +[ + { + "cut_after": 13775, + "frame": 120, + "pivot": 648, + "a": { + "652": "1" + }, + "b": { + "652": "1", + "648": "-1", + "650": "1", + "649": "-1" + }, + "c": { + "652": "1" + }, + "d": { + "652": "1", + "205": "-2", + "648": "-1", + "650": "1", + "649": "-1" + }, + "ranks": [ + 5, + 4 + ] + }, + { + "cut_after": 13765, + "frame": 1053, + "pivot": 592, + "a": { + "596": "1" + }, + "b": { + "596": "1", + "594": "1", + "592": "-1", + "593": "1" + }, + "c": { + "596": "1" + }, + "d": { + "596": "1", + "594": "1", + "188": "-1", + "592": "-1", + "593": "1" + }, + "ranks": [ + 5, + 4 + ] + }, + { + "cut_after": 13706, + "frame": 1051, + "pivot": 664, + "a": { + "668": "1" + }, + "b": { + "668": "1", + "665": "1", + "666": "-1", + "664": "1" + }, + "c": { + "668": "1" + }, + "d": { + "668": "1", + "115": "2", + "665": "1", + "666": "-1", + "664": "1" + }, + "ranks": [ + 5, + 4 + ] + }, + { + "cut_after": 13673, + "frame": 1049, + "pivot": 680, + "a": { + "684": "1" + }, + "b": { + "684": "1", + "681": "1", + "680": "-1", + "682": "1" + }, + "c": { + "684": "1" + }, + "d": { + "684": "1", + "681": "1", + "126": "2", + "680": "-1", + "682": "1" + }, + "ranks": [ + 5, + 4 + ] + }, + { + "cut_after": 12526, + "frame": 306, + "pivot": 259, + "a": { + "261": "1", + "256": "1/2", + "9": "1/2", + "259": "2" + }, + "b": { + "259": "1/2" + }, + "c": { + "259": "2", + "61": "2", + "265": "2" + }, + "d": { + "262": "1/2", + "270": "-1/2", + "265": "1/2", + "264": "1/2", + "256": "-1/2", + "271": "-1/2", + "263": "1/2" + }, + "ranks": [ + 4, + 5 + ] + }, + { + "cut_after": 12448, + "frame": 516, + "pivot": 432, + "a": { + "437": "1", + "20": "-1", + "435": "-1/2" + }, + "b": { + "432": "1", + "20": "-1" + }, + "c": { + "435": "-1", + "21": "-1" + }, + "d": { + "443": "1/2", + "434": "-1", + "432": "1/2", + "442": "1/2", + "439": "1/2", + "435": "-1", + "444": "-1/2", + "438": "1/2", + "445": "-1/2", + "433": "1/2" + }, + "ranks": [ + 4, + 5 + ] + }, + { + "cut_after": 13961, + "frame": 424, + "pivot": 722, + "a": { + "722": "1", + "3": "1/4", + "67": "1/8" + }, + "b": { + "722": "1" + }, + "c": { + "3": "1/4" + }, + "d": { + "722": "1", + "115": "-4", + "3": "4", + "372": "-4", + "370": "-4" + }, + "ranks": [ + 2, + 7 + ] + }, + { + "cut_after": 13647, + "frame": 462, + "pivot": 14, + "a": { + "52": "1", + "14": "-1/2" + }, + "b": { + "727": "-1/4", + "52": "1/2", + "14": "-1" + }, + "c": { + "14": "-1" + }, + "d": { + "727": "-1/4", + "14": "-1", + "403": "1", + "126": "1", + "402": "1" + }, + "ranks": [ + 2, + 7 + ] + }, + { + "cut_after": 13648, + "frame": 252, + "pivot": 76, + "a": { + "87": "1", + "76": "-1/2" + }, + "b": { + "717": "-1/4", + "87": "1/2", + "76": "-1" + }, + "c": { + "76": "-1" + }, + "d": { + "717": "-1/4", + "76": "-1", + "227": "1", + "188": "1", + "226": "1" + }, + "ranks": [ + 2, + 7 + ] + }, + { + "cut_after": 13648, + "frame": 391, + "pivot": 345, + "a": { + "351": "1", + "345": "-1/2" + }, + "b": { + "712": "-1/4", + "351": "1/2", + "345": "-1" + }, + "c": { + "93": "-1" + }, + "d": { + "712": "-1/4", + "351": "-1/2", + "344": "1/2", + "205": "1", + "350": "-1/2", + "343": "1/2", + "93": "-1", + "341": "-1", + "347": "1/2", + "349": "1/2", + "348": "1/2", + "345": "1/2" + }, + "ranks": [ + 2, + 7 + ] + }, + { + "cut_after": 13637, + "frame": 603, + "pivot": 573, + "a": { + "710": "1", + "573": "-1/2", + "572": "1/2" + }, + "b": { + "710": "1/2", + "573": "-1" + }, + "c": { + "573": "-1/2", + "572": "1/2" + }, + "d": { + "710": "1/2", + "115": "1", + "572": "1", + "498": "2", + "306": "-1", + "499": "1", + "502": "-1", + "457": "-2", + "249": "1", + "243": "-1", + "242": "1", + "456": "2", + "252": "-1", + "247": "-1", + "311": "-2", + "205": "-1", + "126": "-1", + "573": "-1", + "317": "-1", + "503": "1" + }, + "ranks": [ + 2, + 7 + ] + }, + { + "cut_after": 12078, + "frame": 477, + "pivot": 405, + "a": { + "405": "1", + "42": "-1", + "403": "-1/2" + }, + "b": { + "405": "1", + "41": "2" + }, + "c": { + "403": "-1" + }, + "d": { + "415": "1", + "403": "-1", + "402": "-1", + "405": "-1", + "400": "2", + "404": "-1", + "414": "1", + "409": "-1", + "408": "-1" + }, + "ranks": [ + 8, + 1 + ] + }, + { + "cut_after": 12610, + "frame": 267, + "pivot": 225, + "a": { + "234": "1", + "224": "-1/4", + "81": "1/4", + "225": "-1/2", + "57": "1/4", + "92": "1/4" + }, + "b": { + "225": "-2" + }, + "c": { + "227": "1" + }, + "d": { + "229": "1", + "226": "1", + "230": "-1", + "225": "-1", + "224": "-1", + "231": "-1", + "228": "1", + "227": "1" + }, + "ranks": [ + 8, + 1 + ] + } +] diff --git a/research/p104-helper-subspace-splits/TASK.json b/research/p104-helper-subspace-splits/TASK.json new file mode 100644 index 0000000000..a230fe5b90 --- /dev/null +++ b/research/p104-helper-subspace-splits/TASK.json @@ -0,0 +1,78 @@ +{ + "schema_version": 1, + "task_id": "complex-new-helper-inventory", + "priority_revision": 7, + "base_commit": "5e0052ca0aa3036a3afa8b0438927377c8d97d53", + "original_card": { + "id": "complex-new-helper-inventory", + "question": "Can a new local cost interface change the deficit-to-recursive-cost ratio beyond current packing?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/complex-local-word-ceiling/README.md", + "research/heterogeneous-owner-assembly/README.md", + "certificates/selected-result.json", + "research/selected-k8-unrestricted-ends/README.md" + ], + "methods": [ + "Propose a changed helper inventory and derive an optimistic exact moment.", + "Design a small completed instance and independently verify its endpoint and rank bill." + ], + "acceptance_gate": "A new physically realizable contract outside the frozen catalogue whose per-call profile, screened with ceiling.ceiling(), beats the selected word's packing ceiling; a lower cap does not establish identical circuitry or order attainable optima, and is insufficient to pass the stronger-budget target under this model. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "research/complex-local-word-ceiling/verify.py" + ], + "expected": "PASS_COMPLEX_LOCAL_WORD_CEILING", + "inspect": "Read the selected word's per-call local profile, its packing ceiling and the lever table; run levers.py for the ideal budget of the lever you target.", + "scope": "Positive control and planning budget only; this is not a new construction or full cold replay." + }, + "first_experiment": "Before any synthesis, write the candidate per-call local profile (and centre charge / unpaid coordinates if changed) and screen it with ceiling.ceiling(); reject it if even the ideal ceiling does not beat the selected word's by your stated margin.", + "bottleneck_link": "Packing of the selected word is capped at +0.87% (ceiling model); only a lower local excess spend or a changed coverage law raises the cap.", + "allowed_variations": [ + "Narrow to one changed boundary or helper type with explicit counts.", + "If the coverage law, template or guard changes, derive an applicable fully charged replacement bound instead of applying the incumbent ceiling outside its scope." + ], + "scope_change_triggers": [ + "Mixing only providers already inside the pinned catalogue.", + "Only changing helper terminal subspaces and monotone frames within the fixed scalar word, entrances and cleanup contract already covered by #1995/#2013.", + "Continuing a partial cost improvement while leaving the same unpriced consumer, restoration or central-readout obligation unresolved; refresh the family expansion decision first. Local product-retiming evidence has a narrow scope and is not a ban on changed graphs or contracts." + ], + "overlap_terms": [ + "helper inventory", + "heterogeneous-owner", + "mutable leaver" + ] + }, + "scope_status": "changed", + "actual_scope": "Change the independent P104 helper basis and split 13 targets into two independent targets at common-frame cuts. Verify a complete conditional kappa gain on the published PR5565 word.", + "scope_change_reason": "The donor explicitly requested a different mechanism and a kappa gain. This changes the scalar word, independent input count and helper target contract. It is outside fixed-endpoint retiming and the historical frozen provider catalogue. The card classifies this assigned work; no task was rerolled.", + "bottleneck_link": "At unchanged recursive paid cost relative to PR5565, 13 independent target splits strictly increase the concave target moment. Every new input has an explicit returned Gaussian target.", + "budget_minutes": null, + "stop_rule": "Require full arbitrary-input and native identities and a complete improved kappa. Stop the finite discovery scan after no further tested split remains; do not claim global optimality.", + "outcome": "completed", + "evidence": "SPLITS.json, PROOF.md and RESULT.json bind each cut, the complete word, native maps and full price. VALIDATION.md records executed checks.", + "author": "Ali Romman with OpenAI Codex assistance", + "ai_assistance": "Substantial OpenAI Codex assistance. The same assistant constructed and checked the result. No subagents or independent human review.", + "open_questions": [ + { + "question": "Can an independent reviewer accept the new helper basis, every returned independent target and the complete conditional price?", + "why_it_matters": "Author-side exact checks do not replace independent scientific review.", + "first_step": "Check the first rank-one split in PROOF.md, then replay all cuts, native maps and the complete price.", + "blocked_by": "No missing technical input; independent review is pending." + }, + { + "question": "Can a different compatible cut order or changed common frame support more independent target splits?", + "why_it_matters": "The finite exact screen does not prove a global maximum.", + "first_step": "Use the new word and test both prefix and suffix support before assigning credit. Coordinate with Discussion5575 for any changed frame itinerary.", + "blocked_by": "Every added target must have a clean independent input/output contract and a complete caller bill." + }, + { + "question": "Can the fifteen released target splits compose with the six paid-boundary changes in the parallel Discussion claim?", + "why_it_matters": "The target gain and paid gain could be compatible, but the input bases and cuts must be checked together.", + "first_step": "Use the public handoff at discussioncomment-19183908. The parallel claim has released its word at 8384fb9eda5a2fd47556364b26185f3ba3cbd050 and is testing the earlier fifteen-split component. Coordinate there before testing any further composition.", + "blocked_by": "The parallel claim owns the paid-boundary synthesis. This package does not assert a combined certificate with that work." + } + ] +} diff --git a/research/p104-helper-subspace-splits/VALIDATION.md b/research/p104-helper-subspace-splits/VALIDATION.md new file mode 100644 index 0000000000..7f73fd1454 --- /dev/null +++ b/research/p104-helper-subspace-splits/VALIDATION.md @@ -0,0 +1,51 @@ +# Validation record + +Environment: macOS, CPython 3.12.14, standard library only. Scientific +replays run serially in the isolated `codex/kappa-structural-20261025` worktree. +The scientific base is canonical main +`5e0052ca0aa3036a3afa8b0438927377c8d97d53`. + +## Current composition + +The direct isolated normal replay passed with explicit artifact generation: + +```sh +python3 -I -B research/p104-helper-subspace-splits/verify.py --write +``` + +It checked 13 prefix and suffix witnesses, each complete arbitrary-input +interface, 571,536 final transpose coefficients, 2,923 exact native maps, +1,080 helper normalizers, 208 main adapters and the complete physical caller. +Two exact moment engines, all compiler conditions, 54 strict outer conditions +and four functional conditions passed. All eight local/controller mutation +controls rejected. The retained wrong-phase, old-cutoff and old-BIT controls +also rejected. The raw crossing is in +(0.00310045630724, 0.00310045630725). + +The verifier authenticates 13 live inputs before importing any source code. +It replays both retained source words and checks the exact paid and helper +deltas supplied by PR5565. All new splits preserve the PR5565 paid profile. +The new local paid rank mass is 6014 and enters the native growth bound. +The exact discovery run tested 52 final boundary groups and found no further +candidate in its finite basis-pair class. This is not a global optimum. + +Registered normal/optimized replay is in progress. The committed-byte check +and fresh read-only Git-free export will follow. These checks are not yet +claimed for this composition in this revision. + +## Retained evidence + +The earlier fifteen-split component on PR5580 passed normal, optimized, +registered and read-only Git-free replay at scientific commit +`31a4de233bbdd65c04c63dc3398ecf0eed8e1375`. That evidence applies to its +0.00309839 claim. It is not substituted for the new composition checks. + +The source copies are pinned to their retained paths at ancestor commits +`29fe88ba218b5d2192d8e31f07a01d1141afdacd` (PR5580) and +`bf64e66656843a64e798b8374cd9f53add3f6f46` (PR5565). Each SHA256 and Git blob +equals the recorded published source. Registered replay needs no cached +unmerged-branch objects. Full-history preflight was not run because this +checkout is shallow. + +Independent human review and hosted CI are pending. No complete rounded +multiplier or enormous uniform word was materialized. diff --git a/research/p104-helper-subspace-splits/VERIFY.json b/research/p104-helper-subspace-splits/VERIFY.json new file mode 100644 index 0000000000..f02fe9b970 --- /dev/null +++ b/research/p104-helper-subspace-splits/VERIFY.json @@ -0,0 +1,42 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/p104-productive-controller/caller.py", + "research/p104-productive-controller/CONTROLLER.json", + "research/joint-helper-lattice/CONTROLLER.json", + "research/p104-native-channel/vendor/clifford_exact.py", + "research/p104-native-channel/vendor/native_verify.py", + "research/pr4359-p7-padding/native_inventory.py", + "research/kappa-0023-productive-jobs/dependencies/kappa-next-regime/direct-decoder/sources/DATA-PHASES.json", + "research/higher-moment-strictification/verify.py", + "research/kappa-rebuild/architecture/mixed_target_probe.py", + "research/pr4359-p7-padding/dependencies/compiler-refill/endpoint.py", + "research/query-thinned-controllers/RESULT.json", + "research/p104-helper-subspace-splits/inputs/PR5580-WORD.json.gz", + "research/p104-helper-subspace-splits/inputs/PR5565-WORD.json.gz" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 600, + "checks": "Check all 13 independent cuts, every rational row and reverse column, native maps, complete caller and invoice, two moment engines, compiler and outer predicates; reject false inputs, outputs, target credit and cost." + }, + { + "argv": [ + "{python}", + "-B", + "-O", + "{package}/verify.py" + ], + "timeout_seconds": 600, + "checks": "Check all 13 independent cuts, every rational row and reverse column, native maps, complete caller and invoice, two moment engines, compiler and outer predicates; reject false inputs, outputs, target credit and cost." + } + ] +} diff --git a/research/p104-helper-subspace-splits/WORD.json.gz b/research/p104-helper-subspace-splits/WORD.json.gz new file mode 100644 index 0000000000..e325091e30 Binary files /dev/null and b/research/p104-helper-subspace-splits/WORD.json.gz differ diff --git a/research/p104-helper-subspace-splits/construct.py b/research/p104-helper-subspace-splits/construct.py new file mode 100644 index 0000000000..698a4cbcc0 --- /dev/null +++ b/research/p104-helper-subspace-splits/construct.py @@ -0,0 +1,157 @@ +"""Split independent helper jobs with three scalar basis changes. + +Ali Romman with substantial OpenAI Codex assistance. Apache-2.0. +The source word and caller retain the credits in README.md. +""" +from copy import deepcopy +from fractions import Fraction as Q +import local as L + + +def inverse(program): + return [[e[0], *e[1:-2], + str(1/Q(e[-2]) if e[0] == 'SCALE' else -Q(e[-2])), e[-1]] + for e in reversed(program)] + + +def basis(a, b, pivot, frame): + """Return B with row pivot equal to a and B b equal to e_pivot.""" + L.need(sum(v*b.get(k, 0) for k, v in a.items()) == 1, 'Unit basis pairing') + roles = sorted(set(a) | set(b) | {pivot}) + values, program = dict(b), [] + + def emit(event): + program.append(event) + r, q = event[1], Q(event[-2]) + if event[0] == 'SCALE': + values[r] = values.get(r, 0)*q + else: + values[r] = values.get(r, 0)+q*values.get(event[2], 0) + + j = pivot if b.get(pivot) else next(r for r in roles if b.get(r)) + if j != pivot: + for event in [['ADD', pivot, j, '1', frame], + ['ADD', j, pivot, '-1', frame], + ['ADD', pivot, j, '1', frame], + ['SCALE', j, '-1', frame]]: + emit(event) + if values[pivot] != 1: + emit(['SCALE', pivot, str(1/values[pivot]), frame]) + for r in roles: + if r != pivot and values.get(r): + emit(['ADD', r, pivot, str(-values[r]), frame]) + L.need(all(values.get(r, 0) == int(r == pivot) for r in roles), 'Basis column') + inverse_rows = {r: {r: Q(1)} for r in roles} + for e in inverse(program): + if e[0] == 'SCALE': + inverse_rows[e[1]] = {k: Q(e[-2])*v for k, v in inverse_rows[e[1]].items()} + else: + L.add(inverse_rows[e[1]], inverse_rows[e[2]], Q(e[-2])) + row = {} + for r, q in a.items(): + L.add(row, inverse_rows[r], q) + L.need(row[pivot] == 1, 'Basis row coefficient') + for r in roles: + if r != pivot and row.get(r): + program.append(['ADD', pivot, r, str(row[r]), frame]) + return program + + +def check_cut(word, h): + """Check the whole prefix row and suffix column over the rationals.""" + n, cut, f, p = word['public'], h['cut_after'], h['frame'], h['pivot'] + a, b, c, d = ({int(k): Q(v) for k, v in h[s].items()} for s in ('a', 'b', 'c', 'd')) + main = set(word['live']) | {r+112 for r in word['live']} + L.need(p < n and p not in main, 'A helper supplies the retained output role') + u, v = word['initial'][p], word['final'][p] + group = {r for r in range(n) if r not in main and + (word['initial'][r], word['final'][r]) == (u, v)} + L.need(set(c) | set(d) <= group, 'Both boundary vectors use one helper group') + L.need(L.span(word['frames'][u]) < L.span(word['frames'][f]) < L.span(word['frames'][v]), + 'Two strictly productive nested targets') + L.need(h['ranks'] == [len(word['frames'][f])-len(word['frames'][u]), + len(word['frames'][v])-len(word['frames'][f])], 'Declared split ranks') + rows = [{r: Q(1)} if r < n else {} for r in range(n+8)] + current = word['initial']+[None]*8 + for e in word['program'][:cut+1]: + op, r = e[:2] + if op == 'MOVE': + current[r] = e[3] + elif op in ('INIT', 'CLEAR'): + rows[r] = {} + current[r] = e[2] if op == 'INIT' else None + elif op == 'SCALE': + rows[r] = {k: Q(e[-2])*x for k, x in rows[r].items()} + elif op == 'COPY': + rows[r] = {k: Q(e[-2])*x for k, x in rows[e[2]].items()} + else: + L.add(rows[r], rows[e[2]], Q(e[-2])) + L.need(all(current[r] == f for r in set(a) | set(b) | {p}), 'One intermediate chart') + total = {} + for r, q in a.items(): + L.add(total, rows[r], q) + L.need(total == c, 'Exact prefix functional; no other input') + column = [b.get(r, Q(0)) for r in range(n+8)] + for e in word['program'][cut+1:]: + op, r = e[:2] + if op in ('INIT', 'CLEAR'): + column[r] = Q(0) + elif op == 'SCALE': + column[r] *= Q(e[-2]) + elif op == 'COPY': + column[r] = Q(e[-2])*column[e[2]] + elif op == 'ADD': + column[r] += Q(e[-2])*column[e[2]] + L.need(column == [d.get(r, Q(0)) for r in range(n+8)], 'Exact suffix direction; no other output') + L.need(sum(x*b.get(r, 0) for r, x in a.items()) == + sum(x*d.get(r, 0) for r, x in c.items()) == 1, 'Both independent pairings') + return a, b, c, d + + +def split(word, h): + a, b, c, d = check_cut(word, h) + n, p, f, cut = word['public'], h['pivot'], h['frame'], h['cut_after'] + u, v = word['initial'][p], word['final'][p] + + def shift_owned(event): + e = event.copy() + e[1] += int(e[1] >= n) + if e[0] in ('ADD', 'COPY'): + e[2] += int(e[2] >= n) + return e + + def use_successor(event): + e = event.copy() + if e[1] == p: + e[1] = n + if e[0] in ('ADD', 'COPY') and e[2] == p: + e[2] = n + return e + + boundary, middle = basis(c, d, p, u), basis(a, b, p, f) + out = deepcopy(word) + out['public'] = n+1 + out['initial'].append(f) + out['final'].append(v) + out['final'][p] = f + out['program'] = inverse(boundary) + out['program'] += [shift_owned(e) for e in word['program'][:cut+1]] + out['program'] += [shift_owned(e) for e in middle] + out['program'] += [use_successor(shift_owned(e)) for e in inverse(middle)] + out['program'] += [use_successor(shift_owned(e)) for e in word['program'][cut+1:]] + out['program'] += [use_successor([*e[:-1], v]) for e in boundary] + return out + + +def construct(source, witnesses): + word = deepcopy(source) + baseline = L.replay(source) + receipts = [] + for h in witnesses: + word = split(word, h) + result = L.replay(word) + L.need(result['paid'] == baseline['paid'], 'Every paid Gaussian occurrence retained') + receipts.append({'cut_after': h['cut_after'], 'pivot': h['pivot'], + 'ranks': h['ranks'], 'public': word['public'], + 'events': len(word['program'])}) + return word, receipts diff --git a/research/p104-helper-subspace-splits/inputs/PR5565-WORD.json.gz b/research/p104-helper-subspace-splits/inputs/PR5565-WORD.json.gz new file mode 100644 index 0000000000..4ebe6fcb7a Binary files /dev/null and b/research/p104-helper-subspace-splits/inputs/PR5565-WORD.json.gz differ diff --git a/research/p104-helper-subspace-splits/inputs/PR5580-WORD.json.gz b/research/p104-helper-subspace-splits/inputs/PR5580-WORD.json.gz new file mode 100644 index 0000000000..9434855e7d Binary files /dev/null and b/research/p104-helper-subspace-splits/inputs/PR5580-WORD.json.gz differ diff --git a/research/p104-helper-subspace-splits/local.py b/research/p104-helper-subspace-splits/local.py new file mode 100644 index 0000000000..e6e28bacda --- /dev/null +++ b/research/p104-helper-subspace-splits/local.py @@ -0,0 +1,206 @@ +"""Check the complete P104 word with an independent helper inventory. + +Adapted from Ali Romman's PR5544/5545. David Arias supplied the word; +Cinna Davis supplied private reuse; Gareth Davidson supplied composition. +Prepared by Ali Romman with substantial OpenAI Codex assistance. Apache-2.0. +""" +from collections import Counter +from fractions import Fraction as Q +from functools import lru_cache +from hashlib import sha256 +from pathlib import Path +import gzip +import importlib.util +import json +import sys + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] + +def need(ok, why): + if not ok: + raise ValueError(why) + +def read(path): + raw = path.read_bytes() + return json.loads(gzip.decompress(raw) if path.suffix == '.gz' else raw) + +def load(path, name): + spec = importlib.util.spec_from_file_location(name, path) + module = importlib.util.module_from_spec(spec) + sys.modules[name] = module + spec.loader.exec_module(module) + return module + +def add(dst, src, q): + for k, v in tuple(src.items()): + value = dst.get(k, 0) + q*v + if value: + dst[k] = value + else: + dst.pop(k, None) + +def span(basis): + out = {0} + for v in basis: + need(type(v) is int and 0 < v < 512 and v not in out, 'Independent binary basis') + out |= {x ^ v for x in tuple(out)} + return frozenset(out) + +def replay(w): + public = w['public'] + need(type(public) is int and 735 <= public <= 750, 'Public inventory bound') + need(len(w['initial']) == len(w['final']) == public, 'Public boundary size') + need(len(w['program']) < 26000, 'Fixed operation bound') + frames = [span(x) for x in w['frames']] + rows = [{r:Q(1)} for r in range(public+8)] + current = list(w['initial']) + [None]*8 + paid, scalar, live_owned, peak = Counter(), 0, set(), 0 + lifetimes = 0 + for e in w['program']: + op, r = e[:2] + need(0 <= r < public+8, 'Role index') + if op == 'MOVE': + _, r, a, b, private = e + need(current[r] == a and (r in live_owned) == private, 'Transport source and ownership') + need(frames[b] < frames[a] if private else frames[a] < frames[b], 'Nested chronological transport') + paid[abs(len(w['frames'][b])-len(w['frames'][a]))] += 1 + current[r] = b + elif op == 'INIT': + need(r >= public and r not in live_owned, 'Owned initialization') + live_owned.add(r) + lifetimes += 1 + peak = max(peak, len(live_owned)) + rows[r] = {} + current[r] = e[2] + scalar += 2 + elif op == 'CLEAR': + need(r in live_owned and current[r] == e[2], 'Owned erasure at declared frame') + rows[r] = {} + current[r] = None + live_owned.remove(r) + scalar += 2 + else: + q, f = Q(e[-2]), e[-1] + need(q and current[r] == f, 'Scalar destination and coefficient') + n, d = abs(q.numerator), q.denominator + need(d & (d-1) == 0, 'Dyadic scalar coefficient') + need(abs(q)+1 < 2**16, 'Fixed scalar growth bound') + if op == 'SCALE': + need(n & (n-1) == 0, 'Dyadic unit SCALE') + rows[r] = {k:q*x for k,x in rows[r].items()} + scalar += 2*(abs(n.bit_length()-d.bit_length()) + int(q < 0)) + else: + s = e[2] + need(s != r and 0 <= s < public+8 and current[s] == f, 'Common scalar chart') + if op == 'COPY': + need(r in live_owned and not rows[r], 'COPY into cleared owned field') + rows[r] = {k:q*x for k,x in rows[s].items()} + else: + need(op == 'ADD', 'Scalar opcode') + add(rows[r], rows[s], q) + scalar += 2*(3+n.bit_length()-1+n.bit_count()+d.bit_length()-1) + need(not live_owned and peak == 1 and current[:public] == w['final'], 'All public and owned exits') + live = set(w['live']) + for r,row in enumerate(rows): + expected = {r:Q(1)} if r < public else {} + if r-112 in live: + expected[r-112] = Q(1) + need(row == expected, 'All public and owned rows') + main = live | {r+112 for r in live} + helpers = Counter(len(w['frames'][w['final'][r]])-len(w['frames'][w['initial'][r]]) for r in range(public) if r not in main) + need(len(live) == len(w['ports']) == 104 and len(main) == 208 and min(helpers) > 0, 'Independent productive inputs') + return {'paid':dict(paid), 'helpers':dict(helpers), 'public_inputs':public, 'owned_lifetimes':lifetimes, + 'peak_owned_fields':peak, 'real_scalar_allowance':scalar, 'endpoint_coefficients':(public+8)*(public+8), + 'paid_rank_mass':sum(r*count for r,count in paid.items())} + +def reverse_columns(w): + """Check the transpose with dense dyadic rows and the reverse chronology.""" + public = w['public'] + n = public+8 + rows = [[int(i == j) for j in range(n)] for i in range(n)] + exponents = [0]*n + for e in reversed(w['program']): + op,r = e[:2] + if op == 'MOVE': + continue + if op in ('INIT','CLEAR'): + rows[r] = [0]*n + exponents[r] = 0 + continue + q = Q(e[-2]) + qe = q.denominator.bit_length()-1 + if op == 'SCALE': + rows[r] = [q.numerator*x for x in rows[r]] + exponents[r] += qe + else: + s = e[2] + level = max(exponents[s], exponents[r]+qe) + a, b = 1 << (level-exponents[s]), q.numerator << (level-exponents[r]-qe) + rows[s] = [a*x+b*y for x,y in zip(rows[s],rows[r])] + exponents[s] = level + if op == 'COPY': + rows[r] = [0]*n + exponents[r] = 0 + r = s + while exponents[r] and not any(x & 1 for x in rows[r]): + rows[r] = [x//2 for x in rows[r]] + exponents[r] -= 1 + for r,row in enumerate(rows): + expected = [0]*n + if r < public: + expected[r] = 1 << exponents[r] + if r in w['live']: + expected[r+112] = 1 << exponents[r] + need(row == expected, 'Independent dense transpose columns') + return {'columns':n, 'coefficients':n*n, 'arithmetic':'Dense integer rows with binary denominators; reverse chronology'} + +def native(w): + n = w['public'] + C = load(ROOT/'research/p104-native-channel/vendor/clifford_exact.py', 'p104_productive_clifford') + V = load(ROOT/'research/p104-native-channel/vendor/native_verify.py', 'p104_productive_gaussian') + @lru_cache(None) + def chart(i): + return C.canonical_frame(9, tuple(w['frames'][i])) + recipes = {} + def check(a,b): + if (a,b) not in recipes: + recipe,_ = C.lower_child(chart(a).adjoint().then(chart(b))) + expected = V.adjoint(V.frame(w['frames'][a],9)) + V.frame(w['frames'][b],9) + V.equal(V.recipe(recipe),expected,'Native chart change and exact global phase') + need(recipe['rank'] == abs(len(w['frames'][a])-len(w['frames'][b])), 'Native boundary rank') + recipes[a,b] = recipe + return recipes[a,b] + for e in w['program']: + if e[0] == 'MOVE': + check(e[2],e[3]) + main = set(w['live']) | {r+112 for r in w['live']} + helper_profile = Counter() + for r in range(n): + if r not in main: + helper_profile[check(w['initial'][r],w['final'][r])['rank']] += 1 + adapters = [] + for r,q in zip(w['live'],w['ports']): + need(w['frames'][w['initial'][r]] == [q], 'Literal central port') + need(span(w['frames'][w['final'][r+112]]) == frozenset(x for x in range(512) if not (x&q).bit_count()%2), 'Literal output hyperplane') + tests = [ + (C.cgate(9,q,1).adjoint().then(chart(w['initial'][r])), V.adjoint((('C',q,1),))+V.frame(w['frames'][w['initial'][r]],9)), + (chart(w['final'][r+112]).adjoint().then(C.cgate(9,q,-1).then(C.fourier(9))), V.adjoint(V.frame(w['frames'][w['final'][r+112]],9))+(('C',q,-1),)+V.fourier(9))] + for actual,expected in tests: + recipe,_ = C.lower_child(actual) + need(recipe['rank'] == 0, 'Free intrinsic main adapter') + V.equal(V.recipe(recipe),expected,'Main endpoint phase') + adapters.append(recipe) + bad = json.loads(json.dumps(next(iter(recipes.values())))) + bad['left']['phase'] = (bad['left']['phase']+1)%4 + a,b = next(iter(recipes)) + try: + V.equal(V.recipe(bad),V.adjoint(V.frame(w['frames'][a],9))+V.frame(w['frames'][b],9),'Wrong phase control') + except ValueError: + pass + else: + raise ValueError('Wrong native phase accepted') + payload = [[a,b,recipes[a,b]] for a,b in sorted(recipes)] + adapters + return {'distinct_maps':len(recipes),'main_adapters':len(adapters),'helper_normalizers':2*sum(helper_profile.values()), + 'helpers':dict(helper_profile),'recipe_payload_sha256':sha256(json.dumps(payload,sort_keys=True,separators=(',',':')).encode()).hexdigest(), + 'wrong_phase_rejected':True, 'proof':'Every signed Pauli image and exact global phase; frame induction at every positive tensor width'} diff --git a/research/p104-helper-subspace-splits/pricing.py b/research/p104-helper-subspace-splits/pricing.py new file mode 100644 index 0000000000..0b54ad3f16 --- /dev/null +++ b/research/p104-helper-subspace-splits/pricing.py @@ -0,0 +1,170 @@ +"""Complete mixed-target price, compiler and outer transfer. + +The interval and compiler bounds follow zxv and Cao Yifan. The productive +recursion is by Jacob Alan Sussman. The controller is by Cinna Davis. +Adapted from Ali Romman's PR5544/5545 for the two coupled contact changes. +Successor choices were prepared for thu-nmrc with OpenAI Codex assistance. +Helper-subspace targets were added by Ali Romman with OpenAI Codex assistance. +The source commuting-contact construction is by Pierre-Loic Doulcet (hexapode) in PR5565. +Ali Romman's complete caller/price proof and all predecessor credit are retained. +Apache-2.0. +""" +from collections import Counter +from fractions import Fraction as Q +import local as L + +KAPPA, TESTED = Q('.00310045'), Q('.0031004505') +PREVIOUS = Q('.00308520') + + +def encode(x): + if isinstance(x,Q): + return str(x) + if isinstance(x,dict): + return {str(k):encode(v) for k,v in x.items()} + if isinstance(x,(list,tuple)): + return [encode(v) for v in x] + return x + + +def assemble(local, native, word, physical): + paid, targets = Counter(), Counter() + counts = Counter() + L.need(local['helpers'] == native['helpers'], 'Every productive helper has a native target') + for e in word['physical_events']: + counts[e[0]] += 1 + if e[0] == 'LOCAL': + L.need(e[3] is False, 'Every source invocation is forward') + paid.update(local['paid']) + targets.update(local['helpers']) + elif e[0] == 'QUERY_SHEAR': + paid[1] += 104 + elif e[0] == 'IDLE': + paid[8*len(e[2])] += 208 + main = Counter() + idle = Counter({8*len(e[2]):0 for e in word['physical_events'] if e[0] == 'IDLE'}) + for e in word['physical_events']: + if e[0] == 'IDLE': + idle[8*len(e[2])] += 208 + L.need(idle == physical['whole_idle_jobs'], 'Every whole idle has a native Gaussian and full rank') + for term in word['diagonal']: + main[1+8*sum(term[1:])] += 104 + L.need(main == physical['main_targets'], 'Every main target has its full native phase') + targets.update(main) + L.need(counts['LOCAL'] == 18 and counts['QUERY_SHEAR'] == counts['IDLE'] == 15, 'Complete call census') + # Recount by the two path lengths, without using emitted main diagonals. + second_t = Counter({r:18*n for r,n in local['helpers'].items()}) + second_p = Counter({r:18*n for r,n in local['paid'].items()}) + second_t[145] += 208 + second_p[1] += 15*104 + for length in (7,8): + for j in range(1,length+1): + second_t[1+8*(j+1)] += 208 + second_p[8*(j+1)] += 208 + L.need((targets,paid) == (second_t,second_p), 'Independent full invoice') + L.need(max(targets) == 145 and max(paid) == 72, 'Maximum recursive ranks') + L.need(sum(targets.values()) == 13048 and sum(paid.values()) == 66726, 'Complete field and call counts') + L.need(sum(r*n for r,n in targets.items())-sum(r*n for r,n in paid.items()) == 760, 'Complete rank surplus') + return targets,paid,counts + + +def run(local,native,word,physical): + T,P,counts = assemble(local,native,word,physical) + E = L.load(L.ROOT/'research/higher-moment-strictification/verify.py','p104_productive_intervals') + other = L.load(L.ROOT/'research/kappa-rebuild/architecture/mixed_target_probe.py','p104_productive_second_intervals') + def margin(k): + a,b = E.moment(T,1-k), E.moment(P,1-k) + return a[0]-b[1],a[1]-b[0] + lo,hi,grid = 0,10**12,10**14 + while hi-lo > 1: + m=(lo+hi)//2 + if margin(Q(m,grid))[0] > 0: + lo=m + else: + hi=m + lower,upper = Q(lo,grid),Q(hi,grid) + signed = Counter(T) + signed.subtract(P) + cap = Q('.0034') + derivative_upper = Q(0) + for rank, count in signed.items(): + logarithm = E.log_bounds(rank) + low = E.mul(E.power(rank, 1-cap), logarithm)[0] + high = rank*logarithm[1] + derivative_upper -= count*(low if count >= 0 else high) + L.need(derivative_upper < 0, 'Unique raw crossing below the retained BIT cap') + L.need(margin(lower)[0] > 0 and margin(upper)[1] < 0, 'Strict rational crossing enclosure') + L.need(PREVIOUS < KAPPA < TESTED < lower and margin(PREVIOUS)[0] > 0, 'Changed complete bill improves the source claim') + t,u,v,c,b = 1-TESTED,Q(1,5),1024,17,18 + target,paid = E.moment(T,t),E.moment(P,t) + tl,th = other.moment(T,TESTED) + pl,ph = other.moment(P,TESTED) + L.need(tl > ph and max(tl,target[0]) <= min(th,target[1]) and max(pl,paid[0]) <= min(ph,paid[1]), 'Two exact moment engines') + alpha = E.divide(paid,target) + gamma = E.divide(E.moment(P,t+u),E.mul(E.power(c,u),target)) + delta = E.divide((Q(sum(T.values())*b),)*2,E.mul(E.power(c,TESTED),target)) + reserve,decay = Q(1,10**10),Q(39,40) + L.need(alpha[1] < 1-reserve and gamma[1] < decay and delta[1] < decay, 'All three charged tail ratios') + L.need(decay**128 < Q(1,16), 'Both tail decay blocks') + normalized = 1/(1+v*reserve)+Q(4,2**32) + L.need(normalized < 1 and c**64 < b**63, 'Full completion, splitting and rounding charges') + theta,power = Q(63,64),1024 + eta = E.scale(E.power(145,-v*TESTED),t) + L.need(2*(c**v)**64 <= (145**v)**63 and eta[0] > theta**power, 'Shifted exits and complement capacity') + L.need(E.power(145,v*TESTED)[1] < 2**power, 'Compiler initial range') + gap = (TESTED-KAPPA)/7 + L.need(gap.numerator == 1, 'Exact compiler integer grid') + step = gap.denominator + def wins(j): + return (step*j+1)**power < 2**j + left,right=1,2 + while not wins(right): + left,right=right,2*right + while right-left > 1: + m=(left+right)//2 + if wins(m): + right=m + else: + left=m + H=step*right + L.need(H > 8*v and wins(right) and not wins(right-1), 'Finite uniform threshold with predecessor rejection') + local_routes = (sum(local['paid'].values())+native['helper_normalizers']+native['main_adapters']+4*104+4*local['owned_lifetimes'])*1000 + L.need(local['real_scalar_allowance']+local_routes < 10**7, 'Every local scalar, route and owned operation is funded') + boundary = sum(len(word['boundaries'][side+'_program']) for side in ('left','right')) + raw = 18*10**7 + 15*1664 + 32*104*(len(word['physical_events'])+boundary) + raw += 32*104*(26+1000) + L.need(raw < 10**9, 'Complete nonrecursive raw bound') + bit = L.read(L.ROOT/'research/query-thinned-controllers/RESULT.json')['ordinary_BIT'] + atom = Q(bit['atom']) + ordinary=(1-atom)*Q(bit['after_cover'])+atom*Q('.0000384599') + admitted=Q(bit['admitted']) + L.need(atom > ordinary > admitted > TESTED and atom < 1-ordinary, 'Retained BIT admission and stock') + outer_module=L.load(L.ROOT/'research/pr4359-p7-padding/dependencies/compiler-refill/endpoint.py','p104_productive_outer') + params={'kappa':KAPPA,'tested_saving':TESTED,'complex_uniform_saving':KAPPA+6*gap, + 'b':KAPPA+5*gap,'a':KAPPA+4*gap,'q':KAPPA+3*gap,'bit_saving':admitted, + 'epsilon':1-gap,'beta':1-3*gap,'r0':gap/10,'stop':gap,'layout':gap,'d':gap} + outer=outer_module.ledger(params) + outer['functional_checks']['actual_new_BIT_stock_sublinear']=params['beta']*(1-atom) + L.need(len(outer['strict_checks']) == 54 and len(outer['functional_checks']) == 4, 'Complete outer predicate inventory') + L.need(all(x > 0 for key in ('strict_checks','functional_checks') for x in outer[key].values()), 'All outer inequalities strict') + wrong_cutoff = E.divide((Q(sum(T.values())*21),)*2,E.mul(E.power(20,TESTED),target)) + L.need(wrong_cutoff[0] > 1, 'Old cutoff fails with this helper inventory') + bad=outer_module.ledger(dict(params,bit_saving=Q('.0027'))) + L.need(any(x <= 0 for x in bad['strict_checks'].values()), 'Insufficient BIT contract rejected') + return encode({'kappa':KAPPA,'kappa_decimal':'.00310045','previous_open_pr5565':PREVIOUS,'gain':KAPPA-PREVIOUS, + 'relative_gain_percent':100*(KAPPA/PREVIOUS-1),'raw_root_interval':[lower,upper], + 'raw_headroom':[lower-KAPPA,upper-KAPPA], + 'raw_ceiling':{'interval':[Q(0),cap],'derivative_upper':derivative_upper},'margin_at_previous':E.display(margin(PREVIOUS)), + 'targets':T,'paid':P,'productive_fields':sum(T.values()),'paid_calls':sum(P.values()), + 'rank_mass_surplus':760,'full_forward_calls':18,'query_shears':15,'whole_idle_jobs':3120, + 'strictification':{'tested':TESTED,'power':v,'cutoff':c,'floor':b,'tail_offset':u,'reserve':reserve,'tail_decay':decay,'tail_block':128, + 'alpha':E.display(alpha),'gamma':E.display(gamma),'delta':E.display(delta),'normalized_paid_upper':normalized}, + 'compiler':{'theta':theta,'logarithm_power':power,'eta':E.display(eta),'gap':gap,'H':H,'N':'2^'+str(H), + 'integer_test_exponent':right,'uniform_saving':params['complex_uniform_saving'],'word_materialized':False}, + 'nonrecursive':{'local_scalar':local['real_scalar_allowance'],'local_routes':local_routes, + 'raw_scalar_upper':raw,'raw_budget':10**9,'peak_owned_fields':1, + 'fixed_scalar_growth_bound':'At most 2^(16*26000) before native factors; a declared constant, not an attained norm.', + 'local_paid_rank_mass':local['paid_rank_mass'], + 'tensor_native_growth_bound':'Each rank-r Gaussian has row l1 norm at most 2^(rf); use local_paid_rank_mass for the whole word.'}, + 'ordinary_BIT':bit,'outer':outer, + 'negative_controls':{'old_cutoff':'Rejected by completion-tail ratio greater than one','old_BIT':'Rejected by outer inequalities'}}) diff --git a/research/p104-helper-subspace-splits/search.py b/research/p104-helper-subspace-splits/search.py new file mode 100644 index 0000000000..1bf5329658 --- /dev/null +++ b/research/p104-helper-subspace-splits/search.py @@ -0,0 +1,154 @@ +"""Screen exact helper-basis pairs after MOVE events. + +This is a finite discovery screen, not an optimality certificate. +Ali Romman with substantial OpenAI Codex assistance. Apache-2.0. +""" +import argparse +from collections import defaultdict +from fractions import Fraction as Q +import gzip +import json +from pathlib import Path +import sys + +HERE = Path(__file__).resolve().parent +sys.path.insert(0, str(HERE)) +from construct import basis +from local import add, span + + +def pure_combinations(rows, roles, group): + """Eliminate coordinates outside the group; retain field coefficients.""" + pivots, output = {}, [] + for role in roles: + outside = {k:v for k,v in rows[role].items() if k not in group} + inside = {k:v for k,v in rows[role].items() if k in group} + coefficients = {role:Q(1)} + while outside: + pivot = min(outside) + if pivot not in pivots: + scale = 1/outside[pivot] + pivots[pivot] = [{k:v*scale for k,v in row.items()} + for row in (outside, inside, coefficients)] + break + scale = -outside[pivot] + for target, source in zip((outside, inside, coefficients), pivots[pivot]): + add(target, source, scale) + if not outside and inside: + output.append((inside, coefficients)) + return output + + +def dyadic_program(program): + for event in program: + q = Q(event[-2]) + numerator, denominator = abs(q.numerator), q.denominator + if denominator & (denominator-1): + return False + if event[0] == 'SCALE' and numerator & (numerator-1): + return False + return True + + +def candidates(word, group, entry, exit_frame): + frames = [span(b) for b in word['frames']] + valid = {f for f,frame in enumerate(frames) if frames[entry] < frame < frames[exit_frame]} + if not valid: + return [] + public = word['public'] + snapshots, at = defaultdict(list), defaultdict(set) + rows = [{r:Q(1)} if r < public else {} for r in range(public+8)] + for r,f in enumerate(word['initial']): + at[f].add(r) + for index,event in enumerate(word['program']): + op,r = event[:2] + if op == 'MOVE': + old,new = event[2:4] + at[old].remove(r) + at[new].add(r) + for frame in (old,new): + if frame in valid and at[frame] & group: + roles = sorted(at[frame]) + combinations = pure_combinations(rows, roles, group) + if combinations: + snapshots[index].append((frame,roles,combinations)) + elif op == 'INIT': + rows[r] = {} + at[event[2]].add(r) + elif op == 'CLEAR': + rows[r] = {} + at[event[2]].remove(r) + elif op == 'COPY': + rows[r] = {k:v*Q(event[-2]) for k,v in rows[event[2]].items()} + elif op == 'SCALE': + rows[r] = {k:v*Q(event[-2]) for k,v in rows[r].items()} + else: + add(rows[r], rows[event[2]], Q(event[-2])) + columns = [{r:Q(1)} if r < public else {} for r in range(public+8)] + hits = [] + for index in range(len(word['program'])-1, -1, -1): + for frame,roles,prefix_basis in snapshots.get(index, []): + suffix_basis = pure_combinations(columns, roles, group) + for c,a in prefix_basis: + for raw_d,raw_b in suffix_basis: + pairing = sum(v*raw_d.get(k,0) for k,v in c.items()) + if not pairing: + continue + b = {k:v/pairing for k,v in raw_b.items()} + d = {k:v/pairing for k,v in raw_d.items()} + if sum(v*b.get(k,0) for k,v in a.items()) != 1: + continue + available = group & set(roles) + pivot = next((r for r in sorted(available) if b.get(r)), min(available)) + if not dyadic_program(basis(c,d,pivot,entry)+basis(a,b,pivot,frame)): + continue + ranks = [len(word['frames'][frame])-len(word['frames'][entry]), + len(word['frames'][exit_frame])-len(word['frames'][frame])] + hits.append({'cut_after':index, 'frame':frame, 'pivot':pivot, + 'a':a, 'b':b, 'c':c, 'd':d, 'ranks':ranks}) + event = word['program'][index] + op,r = event[:2] + if op == 'INIT': + columns[r] = {} + elif op == 'CLEAR': + columns[r] = {} + elif op == 'COPY': + add(columns[event[2]], columns[r], Q(event[-2])) + columns[r] = {} + elif op == 'SCALE': + columns[r] = {k:v*Q(event[-2]) for k,v in columns[r].items()} + elif op == 'ADD': + add(columns[event[2]], columns[r], Q(event[-2])) + return hits + + +def encode(value): + if isinstance(value,Q): + return str(value) + if isinstance(value,dict): + return {k:encode(v) for k,v in value.items()} + if isinstance(value,list): + return [encode(v) for v in value] + return value + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--word', type=Path, default=HERE/'WORD.json.gz') + args = parser.parse_args() + word = json.loads(gzip.decompress(args.word.read_bytes())) + mains = set(word['live']) | {r+112 for r in word['live']} + groups = defaultdict(set) + for r in range(word['public']): + if r not in mains: + groups[word['initial'][r],word['final'][r]].add(r) + hits, tested = [], 0 + for (entry,exit_frame),roles in groups.items(): + if len(word['frames'][exit_frame])-len(word['frames'][entry]) > 1: + hits.extend(candidates(word, roles, entry, exit_frame)) + tested += 1 + print(json.dumps(encode({'tested_boundary_groups':tested, 'candidates':hits}), sort_keys=True)) + + +if __name__ == '__main__': + main() diff --git a/research/p104-helper-subspace-splits/verify.py b/research/p104-helper-subspace-splits/verify.py new file mode 100644 index 0000000000..547751915a --- /dev/null +++ b/research/p104-helper-subspace-splits/verify.py @@ -0,0 +1,146 @@ +"""Verify independent helper splits, all native maps and complete kappa. + +Ali Romman with substantial OpenAI Codex assistance. Apache-2.0. +""" +import argparse +from collections import Counter +from copy import deepcopy +from hashlib import sha1, sha256 +import gzip +import json +from pathlib import Path +import sys +import tempfile + +sys.dont_write_bytecode = True +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] + + +def need(ok, why): + if not ok: + raise ValueError(why) + + +def authenticate(): + count = 0 + manifest = json.loads((HERE/'SOURCES.json').read_bytes()) + for row in manifest['files']: + if row['usage'] == 'input': + raw = (ROOT/row['path']).read_bytes() + need(sha256(raw).hexdigest() == row['sha256'], 'Source SHA256: '+row['path']) + need(sha1(b'blob '+str(len(raw)).encode()+b'\0'+raw).hexdigest() == row['git_blob'], + 'Source Git blob: '+row['path']) + count += 1 + for row in manifest['external_inputs']: + retained_path = (HERE.relative_to(ROOT)/row['local_path']).as_posix() + retained, = [r for r in manifest['files'] if r['path'] == retained_path] + need(retained['usage'] == 'input', 'Copied source is a declared live input') + need((retained['sha256'],retained['git_blob']) == (row['sha256'],row['git_blob']), + 'Retained bytes equal the recorded published source') + return count + + +def rejected(action): + try: + action() + except ValueError as error: + return str(error) + raise ValueError('An invalid claim was accepted') + + +def run(): + pins = authenticate() + sys.path.insert(0, str(HERE)) + import local as L + import construct as R + import pricing as P + C = L.load(ROOT/'research/p104-productive-controller/caller.py', 'subspace_p104_caller') + predecessor = L.replay(L.read(HERE/'inputs/PR5580-WORD.json.gz')) + source = L.read(HERE/'inputs/PR5565-WORD.json.gz') + witnesses = L.read(HERE/'SPLITS.json') + need(len(witnesses) == 13, 'Thirteen explicit independent splits') + baseline = L.replay(source) + source_delta = {} + for name, expected in (('paid', {1:-8, 3:-1, 4:-2, 5:4}), + ('helpers', {8:-1, 9:1})): + delta = Counter(baseline[name]) + delta.subtract(predecessor[name]) + source_delta[name] = {r:n for r,n in delta.items() if n} + need(source_delta[name] == expected, 'Exact published PR5565 '+name+' change') + word, cuts = R.construct(source, witnesses) + local = L.replay(word) + need((local['public_inputs'], local['owned_lifetimes'], local['peak_owned_fields']) == (748, 8, 1), + 'Complete public and owned inventory') + need(local['helpers'] == {1:2, 2:5, 4:89, 5:11, 7:5, 8:16, 9:412}, 'Exact helper histogram') + delta = Counter(local['helpers']) + delta.subtract(baseline['helpers']) + delta = {r:n for r,n in delta.items() if n} + need(delta == {1:2, 2:5, 4:6, 5:6, 7:5, 8:2, 9:-13}, 'All split credits and removed targets') + need(local['paid'] == baseline['paid'], 'Same complete local paid histogram') + columns = L.reverse_columns(word) + print('PASS 13 prefix/suffix cuts, every independent row and dense reverse columns', flush=True) + native = L.native(word) + controller = C.construct() + need(controller == L.read(ROOT/'research/p104-productive-controller/CONTROLLER.json'), 'Same complete caller') + physical = C.physical(controller, word) + print('PASS every native phase, productive target and physical caller contact', flush=True) + costs = P.run(local, native, controller, physical) + controls = C.controls(controller) + bad = deepcopy(witnesses[0]) + key = next(iter(bad['a'])) + bad['a'][key] = str(L.Q(bad['a'][key])+1) + controls['contaminated_prefix'] = rejected(lambda: R.check_cut(source, bad)) + bad = deepcopy(witnesses[0]) + key = next(iter(bad['b'])) + bad['b'][key] = str(L.Q(bad['b'][key])+1) + controls['contaminated_suffix'] = rejected(lambda: R.check_cut(source, bad)) + bad = deepcopy(word) + bad['program'].pop(0) + controls['missing_input_basis'] = rejected(lambda: L.replay(bad)) + bad = deepcopy(word) + bad['program'].pop() + controls['missing_output_basis'] = rejected(lambda: L.replay(bad)) + bad = deepcopy(word) + bad['final'][648] = 127 + controls['unearned_whole_target'] = rejected(lambda: L.replay(bad)) + bad = deepcopy(local) + bad['helpers'][1] += 1 + controls['extra_helper_credit'] = rejected(lambda: P.assemble(bad, native, controller, physical)) + bad = deepcopy(local) + bad['paid'][1] -= 1 + controls['unpaid_gaussian'] = rejected(lambda: P.assemble(bad, native, controller, physical)) + result = {'status':'PASS_P104_HELPER_SUBSPACE_KAPPA_00310045', + 'authenticated_inputs':pins, 'splits':cuts, 'local_helper_delta':delta, + 'published_source_delta':source_delta, + 'local':local, 'separate_columns':columns, 'native':native, + 'physical_caller':physical, 'complete_cost':costs, 'negative_controls':controls, + 'limits':['The five selected framework assumptions and helper-endpoint contract remain.', + 'No complete rounded multiplier or enormous uniform compiler word is materialized.', + 'No independent human or proof-kernel acceptance or global optimality is claimed.']} + return P.encode(result), word + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--write', action='store_true') + args = parser.parse_args() + with tempfile.TemporaryDirectory(prefix='p104-subspace-bytecode-') as cache: + sys.pycache_prefix = cache + result, word = run() + for name, value in (('RESULT.json', result), ('WORD.json.gz', word)): + path = HERE/name + if args.write: + raw = (json.dumps(value, sort_keys=True, indent=None if name.endswith('.gz') else 2)+'\n').encode() + path.write_bytes(gzip.compress(raw, mtime=0) if name.endswith('.gz') else raw) + else: + raw = path.read_bytes() + need(json.loads(gzip.decompress(raw) if name.endswith('.gz') else raw) == value, + 'Exact saved artifact: '+name) + print(result['status']) + print(json.dumps({k:result['complete_cost'][k] for k in + ('kappa', 'gain', 'raw_root_interval', 'productive_fields', 'paid_calls')}, sort_keys=True)) + + +if __name__ == '__main__': + main()