diff --git a/research/p104-coupled-helper-bases/PRICING-CHANGES.diff b/research/p104-coupled-helper-bases/PRICING-CHANGES.diff new file mode 100644 index 0000000000..f3dedd2f79 --- /dev/null +++ b/research/p104-coupled-helper-bases/PRICING-CHANGES.diff @@ -0,0 +1,52 @@ +--- PR5580/pricing.py ++++ pricing.py +@@ -2,8 +2,9 @@ + + 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 prepared for thu-nmrc with substantial OpenAI Codex assistance. ++The contact versions are by thu-nmrc, DreamingOfClouds, GamingPuzzled and ++Ali Romman. The coupled-basis counts and compiler power are by Ali Romman ++with substantial OpenAI Codex assistance. + Ali Romman's complete caller/price proof and all predecessor credit are retained. + Apache-2.0. + """ +@@ -11,8 +12,8 @@ + from fractions import Fraction as Q + import local as L + +-KAPPA, TESTED = Q('.00308189'), Q('.0030818905') +-PREVIOUS = Q('.00308181') ++KAPPA, TESTED = Q('.00309980'), Q('.0030998005') ++PREVIOUS = Q('.00308189') + + + def encode(x): +@@ -61,7 +62,7 @@ + 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()) == 12814 and sum(paid.values()) == 66852, 'Complete field and call counts') ++ L.need(sum(targets.values()) == 12976 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 + +@@ -96,7 +97,7 @@ + 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),1000 ++ 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') +@@ -139,7 +140,7 @@ + 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':'.00308189','previous_open_pr5569':PREVIOUS,'gain':KAPPA-PREVIOUS, ++ return encode({'kappa':KAPPA,'kappa_decimal':'.00309980','previous_open_pr5580':PREVIOUS,'gain':KAPPA-PREVIOUS, + 'relative_gain_percent':100*(KAPPA/PREVIOUS-1),'raw_root_interval':[lower,upper], + 'raw_headroom':[lower-KAPPA,upper-KAPPA],'margin_at_previous':E.display(margin(PREVIOUS)), + 'targets':T,'paid':P,'productive_fields':sum(T.values()),'paid_calls':sum(P.values()), diff --git a/research/p104-coupled-helper-bases/PROOF.md b/research/p104-coupled-helper-bases/PROOF.md new file mode 100644 index 0000000000..168733f6c4 --- /dev/null +++ b/research/p104-coupled-helper-bases/PROOF.md @@ -0,0 +1,272 @@ +# Coupled helper bases and productive handoffs + +## Statement and source + +This construction changes the complete P104 invoice. The conditional claim +is kappa = 0.00309980, tested at 0.0030998005. The predecessor claim is +0.00308189 in [PR #5580](https://github.com/CrocSwap/integer-mult-bounds/pull/5580). +Its exact source commit is `6efa248cf456d6101d757e9d09ba29711d18a13a`. +[SOURCES.json](SOURCES.json) binds the source bytes. The selected record +stays at 0.003027288235. + +Six helper boundary basis changes remove seven paid transports per local +call. Nine coupled handoffs add nine independent helper inputs without +adding a paid transport. The 104 main shears, their literal native ports, +the caller and all eight owned paths remain fixed. Each new helper is an +arbitrary independent input. None is initialized as zero. + +This result uses the five inherited framework assumptions: native +all-column realization, owned erasure, uniform compiler closure, precision +and fixed-tape execution, and analytic recovery. It also uses the inherited +free helper endpoint contract. It is an author-checked conditional bound, +not independent scientific acceptance or a change to the selected frontier. + +## Chart convention + +A field at frame F represents an abstract row in the chart C_F. A MOVE +changes its native chart and preserves its abstract row. An ADD or SCALE +acts on abstract rows only when all operands share the declared chart. +Scalar coefficients are dyadic. SCALE coefficients are dyadic units. + +The source word has main endpoint matrix M and identity helper endpoints. +M is the direct sum of 104 invertible shears and the helper identity. +Every construction step preserves this form, with one more identity factor +for each new input. The exact endpoint replay tests arbitrary inputs, not +just inputs with zero helper values. + +## Boundary basis change + +Choose a helper h after its last source read. At a cut in frame F, suppose +free additions from fields at F change its row to + +```text +c h + sum(a_j h_j), j != h. +``` + +The inputs h and h_j are helpers at one common input frame S, and c is a +dyadic unit. Prepend `h += -(a_j/c) h_j` at S. At the cut, do the stated +cancellation and scale h by 1/c. The row is now exactly h. Delete all +later instructions with destination h and retire it at F. There is no +later source read of h. The final helper map on every input remains the +identity, so the added input basis change does not change other outputs. +The full endpoint check independently confirms this conclusion. + +The same construction can be applied to the transpose of the logical +word. Reverse the order, transpose ADD, interchange INIT and CLEAR, and +reverse each MOVE. A COPY into a zero owned field can be written as ADD +before this transpose. Transpose the changed word back. This changes a +helper's initial boundary. It does not add an inverse local call to the +physical caller. Every final public MOVE is ascending, every owned MOVE +is descending, and the final native replay checks all maps and phases. + +The six fixed changes are: + +| Helper | Orientation used to construct the change | Cut frame | +| --- | --- | --- | +| 652 | Transpose | 120 | +| 341 | Forward | 240 | +| 596 | Transpose | 1053 | +| 668 | Transpose | 1051 | +| 684 | Transpose | 1049 | +| 649 | Transpose | 597 | + +[WITNESS.json](WITNESS.json) gives the exact event cuts, cancellation rows +and helper boundary relations. Cuts refer to the current word at each +step. The constructor derives these relations again from the prefix. +It checks frame availability, helper support and the last-read condition. + +## Coupled handoff lemma + +Take a cut with no live owned field. Let A be its public prefix matrix and +B its suffix matrix. Then B A = M. Both square matrices are invertible. +Let G be a set of helpers with the same initial frame S and final frame T. +Choose a common cut frame F with S strictly contained in F and F strictly +contained in T. + +Choose a row v and a column u supported on public fields at F. Require + +```text +v u = 1, a = v A, b = B u, +support(a), support(b) contained in G, a b = 1. +``` + +Pick a helper field p in G that is at F. Construct scalar matrices R on +G and J on the fields at F such that + +```text +a R = e_p^T, R e_p = b, +v J = e_p^T, J e_p = u. +``` + +The supplied witnesses have dyadic unit pivots. `basis` emits ADD and SCALE +operations for each matrix and checks the exact pairing. The inverse is +the reversed instruction list with negated ADD coefficients and inverse +SCALE coefficients. All operations at each boundary share one chart. + +Because b has only helper support, M b = b. The equations B A b = b and +B u = b imply A b = u. Thus the transformed prefix J^-1 A R has first +row e_p^T and first column e_p. It is a direct sum of the scalar 1 on p +and a map on the remaining fields. The transformed complete map is +R^-1 M R = M, since R acts only on helper coordinates. Consequently the +transformed suffix R^-1 B J also has the isolated identity factor on p. + +Execute R at the input, the original prefix, and J^-1 at the cut. Retire +p at F. Supply a new independent public input n at F. Use n in place of +p in J, the suffix and R^-1 at the output. The retired output is the old +input p. The new output is the new input n. Every other helper and main +output is unchanged. This proves the arbitrary-input identity and the +independence of both productive targets. + +The scalar basis matrices act on whole fields, with coefficients outside +the tensor power. At every positive tensor width, common-chart scalar +operations and the exact native chart identities give the same abstract +row identity. The finite native recipe checks include the tensor rule; +no tensor power of a scalar coefficient is substituted for that coefficient. + +The old target rank dim(T)-dim(S) becomes two positive target ranks +dim(F)-dim(S) and dim(T)-dim(F). No MOVE is inserted. R and its inverse +use only helpers with one common boundary chart. J may mix main and +helper fields at the cut; its inverse and the isolated-channel argument +restore the exact main contract. There is no owned COPY at any cut. + +The nine cuts are: + +| Retired field | Frame F | New target ranks | +| --- | --- | --- | +| 61 | 306 | 4, 5 | +| 432 | 516 | 4, 5 | +| 572 | 603 | 2, 7 | +| 345 | 391 | 2, 7 | +| 14 | 462 | 2, 7 | +| 3 | 424 | 2, 7 | +| 76 | 252 | 2, 7 | +| 224 | 267 | 8, 1 | +| 400 | 477 | 8, 1 | + +Fields 3, 14, 61 and 76 are helpers in this source word. The source removed +their original ports. They are not among the 104 retained main ports. + +The checker recomputes v A and B u from the complete prefix and suffix, +checks their helper support, checks every cut chart, and replays the full +word after each step. It also checks the final transpose with dense integer +rows and binary denominators, separately from the sparse Fraction replay. + +## Exact gain and complete bill + +Write H_r for one rank-r job and let g(a,b) denote +a^(1-kappa) + b^(1-kappa) - (a+b)^(1-kappa). This is strictly positive +for a,b > 0 and 0 < kappa < 1. + +The local paid change from PR5580 is `-2 H1 - H4 - 4 H5`. +The local target change is + +```text +2 H1 + 5 H2 + 7 H4 + 2 H5 + 5 H7 + 3 H8 - 15 H9. +``` + +Thus the increase in the complete target-minus-paid moment is + +```text +18 * [7 g(4,5) + 5 g(2,7) + 3 g(1,8) + g(1,4)] > 0. +``` + +The rank masses of both local profiles fall by 26. Their difference is +unchanged. This exact identity also distinguishes the construction from +more digits of the same root. + +| Quantity | PR5580 | This construction | +| --- | ---: | ---: | +| Local public inputs | 735 | 744 | +| Local helper targets | 527 | 536 | +| Local paid jobs | 3454 | 3447 | +| Local paid rank mass | 6013 | 5987 | +| Local events | 25140 | 25472 | +| Complete productive fields | 12814 | 12976 | +| Complete paid jobs | 66852 | 66726 | +| Complete target rank mass | 242010 | 241542 | +| Complete paid rank mass | 241250 | 240782 | +| Rank-mass surplus | 760 | 760 | + +The complete caller has 18 forward local calls, 15 rank-one query shears +per port, and 3120 whole idle jobs. Maximum paid rank is 72 and maximum +target rank is 145. The physical event invoice is checked against the two +controller path lengths and a third count in the verifier. + +All eight owned paths remain. They use one field at a time and have total +local paid rank 56. The new public inputs are charged as productive fields, +including both native normalizers for each helper. The native checker +also covers every paid map and all 208 main adapters, with exact signed +Pauli images and absolute phases. The physical caller checks its contacts, +routes, central squares, target phases and whole idle phases. + +The local real scalar allowance is 220332. The route allowance is 5175000. +Their sum is below 10000000. The full nonrecursive bound is 184647552, +below 1000000000. This includes local scalar work and routes, the owned +operations, thin queries, caller boundaries and the retained layout terms. +The scalar growth bound remains 2^(16*26000). The actual local native +rank sum 5987 is used in the tensor growth bound. + +## Comparison with the released parallel split component + +[PR #5599](https://github.com/CrocSwap/integer-mult-bounds/pull/5599), head +`0644592d421b375c221045954fdf13932575ffa8`, independently uses the same +input/cut/output basis mechanism. Its author released the 15-split component +for composition. The present package credits that work and makes no claim +of exclusive method discovery. The six paid-boundary changes remain a +separate construction component. + +The parallel word has 750 public inputs, 542 local helper targets, 66852 +complete paid calls and 13084 complete productive fields. Its exact raw +crossing is (0.00309839352211, 0.00309839352212). Its local targets are +`{1:4, 2:5, 4:90, 5:10, 7:5, 8:18, 9:410}` and its paid profile is the +PR5580 profile. Relative to that word, this construction has local changes + +```text +targets: -2 H1 - 3 H5 - H9 +paid: -2 H1 - H4 - 4 H5. +``` + +The complete signed-moment gain is therefore exactly `18 * g(4,5) > 0`. +The raw gain lies in (0.00000140768321, 0.00000140768323). The claimed +endpoint increases by 0.00000141. It also removes 108 productive fields +and 126 paid calls from the complete bill. The comparison checker binds +that exact word, replays its arbitrary inputs, recounts its full invoice +and isolates its crossing. It does not repeat that package's native and +compiler checks or count them as independent review. + +The nine handoffs here and the 15 parallel splits are not additive gains. +This package retains its fully verified smaller construction. Any different +combined word still needs its own full replay and compiler bounds. + +## Compiler and outer transfer + +Two exact rational moment engines check the endpoint. The complete +compiler retains power 1024, cutoff 17, floor 18, tail offset 1/5, +reserve 1e-10 and tail decay 0.97. The logarithm power increases from +1000 to 1024. The old logarithm power fails the complement-capacity test +at the new endpoint; the checker records this negative control. + +The checker verifies all three tail ratios, completion, splitting, +rounding, shifted exits, complement capacity, the initial range and the +finite integer threshold. It rejects the preceding integer threshold. +The ordinary BIT contract remains 0.0034. All 54 strict and four +functional outer predicates must be positive. The old cutoff, insufficient +BIT contract and old complete invoice also fail their control tests. + +The raw crossing lies in (0.00309980120533, 0.00309980120534). Its increase +over the parent crossing lies in (0.00001790623666, 0.00001790623668). +The headroom above the claimed endpoint is between 1.20533e-9 and +1.20534e-9. The finite threshold is N = 2^707182000000000, with integer +test exponent 50513 and gap 1/14000000000. + +The exact interval bounds are in [RESULT.json](RESULT.json). A rational derivative bound proves a +unique crossing on [0,0.0034]. That interval is the funding ceiling only +for this fixed invoice under the retained BIT cap. No optimum for other +words, helper bases, controllers or suppliers is claimed. + +The enormous uniform word and a complete rounded multiplier are not +materialized. The replay and algebraic lemmas do not discharge the inherited +framework assumptions. Independent scientific review remains required. + +Ali Romman with substantial OpenAI Codex assistance. Apache-2.0. +The retained sources preserve their original notices and predecessor credit. diff --git a/research/p104-coupled-helper-bases/README.md b/research/p104-coupled-helper-bases/README.md new file mode 100644 index 0000000000..e5e59219a6 --- /dev/null +++ b/research/p104-coupled-helper-bases/README.md @@ -0,0 +1,163 @@ +# Conditional kappa 0.00309980 from coupled helper bases + +This construction increases complete conditional kappa from 0.00308189 in +[PR #5580](https://github.com/CrocSwap/integer-mult-bounds/pull/5580) to +**0.00309980**, a gain of **0.00001791**. The exact raw crossing is in +(0.00309980120533, 0.00309980120534). The selected record remains +0.003027288235. + +Six helper boundary basis changes remove seven paid transports per local +call. Nine coupled handoffs split independent helper channels at common +interior frames. The new word has nine more arbitrary helper inputs and +no added paid transport. The input, cut and output bases isolate each new +channel and restore every main and helper input. All eight owned paths +remain fully charged. + +Read [the proof](PROOF.md), [the fixed witness](WITNESS.json), +[the constructor](construct.py), [the complete receipt](RESULT.json), +[the source pins](SOURCES.json) and [the verification record](VALIDATION.md). +The complete bill has **66726 paid jobs and 12976 productive fields**. +This is a changed invoice. Its rank-mass surplus remains 760. + +The final overlap refresh found parallel helper splitting in +[PR #5599](https://github.com/CrocSwap/integer-mult-bounds/pull/5599), head +`0644592d421b375c221045954fdf13932575ffa8`, with complete claim 0.00309839. +Its author [released the 15 splits for composition](https://github.com/CrocSwap/integer-mult-bounds/discussions/5125#discussioncomment-19183908) +and left the paid-boundary work with this claim. This package credits the +shared mechanism and claims no exclusive discovery of it. + +Against that pinned word, the new complete moment improves by exactly +`18 * g(4,5)`, where `g(a,b) = a^(1-k) + b^(1-k) - (a+b)^(1-k)`. +The claimed gain is **0.00000141**. It uses **126 fewer paid calls and +108 fewer productive fields**. The source word is retained for an exact +arbitrary-input and complete-invoice comparison. It is not a constructor +input. A direct composition screen gave the same raw moment with more +fields and calls, so this package retains the smaller complete construction. + +The separate commuting-contact result in +[PR #5565](https://github.com/CrocSwap/integer-mult-bounds/pull/5565) +claims 0.00308520. Composition with that scalar-order change is not checked. + +## Reproduction + +Python 3.12 and the standard library suffice. No solver, network or Git +command is needed by the scientific replay. + +```sh +python3.12 -B scripts/research_package.py --package research/p104-coupled-helper-bases +``` + +Both registered modes must print: + +```text +PASS_P104_COUPLED_HELPER_KAPPA_00309980 +``` + +The launcher must print `PASS_REGISTERED_RESEARCH_PACKAGE`. Each replay +reconstructs all 15 changes, checks arbitrary-input endpoints after every +step, checks 565504 dense transpose coefficients, checks 2926 exact native +maps, and replays the complete physical caller. It derives the invoice +three ways, checks two exact moment engines, the full compiler bounds and +all 58 outer predicates, then compares the complete committed receipt. + +The negative controls reject a missing input basis operation, a wrong +new-helper coefficient, the old retired exit, an independent input treated +as an owned zero, a false cut witness, a missing central translation, a +wrong native phase, the old invoice at the new claim, the old logarithm +power, the old cutoff and an insufficient BIT contract. + +The PR5545 source capsule is unchanged. Its SHA256, export manifest and +all 33 payload files are checked before import. The PR5580 word and price +source and the PR5599 comparison word are checked by SHA256 and Git blob ID. The caller is unchanged. +[VERIFIER-CHANGES.diff](VERIFIER-CHANGES.diff) shows the explicit public +width change and removal of the unused old constructor. It does not change +the endpoint, frame, native-phase or scalar-cost rules. The old and new +checkers must agree on the predecessor word. + +[PRICING-CHANGES.diff](PRICING-CHANGES.diff) records the new counts and +claim, plus the logarithm-power increase from 1000 to 1024. This increase +is required to fund the compiler at the new endpoint. The native engines, +both moment engines and outer ledger remain unchanged. + +## Limits and ceiling + +The five framework assumptions remain: native all-column realization, +owned erasure, uniform compiler closure, precision and fixed-tape execution, +and analytic recovery. The source's free helper endpoint contract remains +inherited. This construction changes helper endpoints and adds independent +helper targets within that contract. No independent human or proof-kernel +acceptance is claimed. The enormous uniform word and a complete rounded +multiplier are not materialized. + +The fixed invoice has a strictly decreasing signed moment on [0,0.0034]. +Its raw funding ceiling is the crossing interval above. The headroom above +the claimed endpoint is between 1.20533e-9 and 1.20534e-9. This is not a +ceiling for other words, bases, helper inventories or controllers. + +The claim concerns the complete P104 caller line. It does not resolve +the additional native-compiler premise in the larger p19 numerical +proposals. A local construction, a complete conditional price and an +accepted integer multiplication theorem are distinct claims. + +## Coordination and credit + +The branch starts at canonical main +`5e0052ca0aa3036a3afa8b0438927377c8d97d53`, priority revision 7. +The [canonical claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/5125#discussioncomment-19154639) +reserves the coupled helper basis scope. [TASK.json](TASK.json) records +the overlap checkpoint and exclusions. The final refresh covers 338 open PRs and all Discussion records listed +in TASK.json, with complete remote pagination. +Local note coverage is sparse; this is not an exhaustive novelty claim. + +The fixed-contact price floor in +[PR #5590](https://github.com/CrocSwap/integer-mult-bounds/pull/5590) +keeps scalar contacts fixed. This construction changes scalar bases, +independent input expressions and target inventory. The owned recoding +work in [PR #5591](https://github.com/CrocSwap/integer-mult-bounds/pull/5591) +and the native-history, changed-contact and global controller claims +remain separate. The former private-fanout claim changed scope to the +released PR5599 helper-split component and is credited above. No other contributor's files are edited. + +- Ali Romman supplied the complete caller and source closure in + [PR #5544](https://github.com/CrocSwap/integer-mult-bounds/pull/5544) and + [PR #5545](https://github.com/CrocSwap/integer-mult-bounds/pull/5545), and + the consumed contact step in PR #5580 linked above. +- Joel Pulikkan, @GamingPuzzled, supplied the priced helper-706 handoff in + [PR #5569](https://github.com/CrocSwap/integer-mult-bounds/pull/5569) + and the successor-handoff method in + [PR #5472](https://github.com/CrocSwap/integer-mult-bounds/pull/5472). +- @DreamingOfClouds supplied free helper endpoints in + [PR #5561](https://github.com/CrocSwap/integer-mult-bounds/pull/5561) + and earlier single-helper handoffs in + [PR #5553](https://github.com/CrocSwap/integer-mult-bounds/pull/5553). +- @thu-nmrc supplied the coupled contacts in + [PR #5551](https://github.com/CrocSwap/integer-mult-bounds/pull/5551). +- Gareth Davidson supplied the composed P104 word in + [PR #2305](https://github.com/CrocSwap/integer-mult-bounds/pull/2305). + David Arias supplied coalescing in + [PR #2152](https://github.com/CrocSwap/integer-mult-bounds/pull/2152). + Cinna Davis supplied private reuse in + [PR #2219](https://github.com/CrocSwap/integer-mult-bounds/pull/2219) + and the retained controller. Jacob Alan Sussman supplied productive + recursion. The source notices credit zxv and Cao Yifan for the interval, + compiler and native framework. The capsule preserves the earlier + geometry, BIT and analytic notices. + +Credit the parallel PR5599 helper-split construction and public composition +handoff. The paid-boundary changes and the cheaper complete construction +are this package's contribution. The elementary scalar basis identity is +not claimed as a new general theorem. + +New coupled-basis construction, proof and verification by Ali Romman with +substantial OpenAI Codex assistance. Apache-2.0. The same assistant performed +the search, proof and checks. No subagent or independent reviewer was used. + +## Open next questions + +Independently review the coupled handoff lemma and its free boundary +operations, then replay the complete price. A further gain needs a changed +word or a compatible composition, with live overlap checked first. The +fixed 15-step witness does not prove optimality of the larger basis class. +Composition with PR #5565 or the active coupled-frame witness needs a new +source-bound construction and full replay. Structured questions are in +[TASK.json](TASK.json). diff --git a/research/p104-coupled-helper-bases/RESULT.json b/research/p104-coupled-helper-bases/RESULT.json new file mode 100644 index 0000000000..17a9ec06a8 --- /dev/null +++ b/research/p104-coupled-helper-bases/RESULT.json @@ -0,0 +1,697 @@ +{ + "construction": [ + { + "events": 25141, + "helpers": { + "4": 84, + "5": 5, + "8": 15, + "9": 423 + }, + "kind": "boundary_basis", + "paid": { + "1": 2210, + "2": 459, + "3": 494, + "4": 93, + "5": 164, + "6": 18, + "7": 14 + }, + "public": 735 + }, + { + "events": 25138, + "helpers": { + "4": 85, + "5": 5, + "8": 15, + "9": 422 + }, + "kind": "boundary_basis", + "paid": { + "1": 2210, + "2": 459, + "3": 494, + "4": 93, + "5": 163, + "6": 18, + "7": 14 + }, + "public": 735 + }, + { + "events": 25140, + "helpers": { + "4": 86, + "5": 5, + "8": 15, + "9": 421 + }, + "kind": "boundary_basis", + "paid": { + "1": 2210, + "2": 459, + "3": 494, + "4": 93, + "5": 162, + "6": 18, + "7": 14 + }, + "public": 735 + }, + { + "events": 25142, + "helpers": { + "4": 87, + "5": 5, + "8": 15, + "9": 420 + }, + "kind": "boundary_basis", + "paid": { + "1": 2210, + "2": 459, + "3": 494, + "4": 93, + "5": 161, + "6": 18, + "7": 14 + }, + "public": 735 + }, + { + "events": 25144, + "helpers": { + "4": 88, + "5": 5, + "8": 15, + "9": 419 + }, + "kind": "boundary_basis", + "paid": { + "1": 2210, + "2": 459, + "3": 494, + "4": 93, + "5": 160, + "6": 18, + "7": 14 + }, + "public": 735 + }, + { + "events": 25142, + "helpers": { + "4": 88, + "5": 5, + "8": 16, + "9": 418 + }, + "kind": "boundary_basis", + "paid": { + "1": 2209, + "2": 459, + "3": 494, + "4": 93, + "5": 160, + "6": 18, + "7": 14 + }, + "public": 735 + }, + { + "events": 25180, + "helpers": { + "4": 89, + "5": 6, + "8": 16, + "9": 417 + }, + "kind": "coupled_handoff", + "paid": { + "1": 2209, + "2": 459, + "3": 494, + "4": 93, + "5": 160, + "6": 18, + "7": 14 + }, + "public": 736 + }, + { + "events": 25230, + "helpers": { + "4": 90, + "5": 7, + "8": 16, + "9": 416 + }, + "kind": "coupled_handoff", + "paid": { + "1": 2209, + "2": 459, + "3": 494, + "4": 93, + "5": 160, + "6": 18, + "7": 14 + }, + "public": 737 + }, + { + "events": 25280, + "helpers": { + "2": 1, + "4": 90, + "5": 7, + "7": 1, + "8": 16, + "9": 415 + }, + "kind": "coupled_handoff", + "paid": { + "1": 2209, + "2": 459, + "3": 494, + "4": 93, + "5": 160, + "6": 18, + "7": 14 + }, + "public": 738 + }, + { + "events": 25318, + "helpers": { + "2": 2, + "4": 90, + "5": 7, + "7": 2, + "8": 16, + "9": 414 + }, + "kind": "coupled_handoff", + "paid": { + "1": 2209, + "2": 459, + "3": 494, + "4": 93, + "5": 160, + "6": 18, + "7": 14 + }, + "public": 739 + }, + { + "events": 25336, + "helpers": { + "2": 3, + "4": 90, + "5": 7, + "7": 3, + "8": 16, + "9": 413 + }, + "kind": "coupled_handoff", + "paid": { + "1": 2209, + "2": 459, + "3": 494, + "4": 93, + "5": 160, + "6": 18, + "7": 14 + }, + "public": 740 + }, + { + "events": 25354, + "helpers": { + "2": 4, + "4": 90, + "5": 7, + "7": 4, + "8": 16, + "9": 412 + }, + "kind": "coupled_handoff", + "paid": { + "1": 2209, + "2": 459, + "3": 494, + "4": 93, + "5": 160, + "6": 18, + "7": 14 + }, + "public": 741 + }, + { + "events": 25372, + "helpers": { + "2": 5, + "4": 90, + "5": 7, + "7": 5, + "8": 16, + "9": 411 + }, + "kind": "coupled_handoff", + "paid": { + "1": 2209, + "2": 459, + "3": 494, + "4": 93, + "5": 160, + "6": 18, + "7": 14 + }, + "public": 742 + }, + { + "events": 25422, + "helpers": { + "1": 1, + "2": 5, + "4": 90, + "5": 7, + "7": 5, + "8": 17, + "9": 410 + }, + "kind": "coupled_handoff", + "paid": { + "1": 2209, + "2": 459, + "3": 494, + "4": 93, + "5": 160, + "6": 18, + "7": 14 + }, + "public": 743 + }, + { + "events": 25472, + "helpers": { + "1": 2, + "2": 5, + "4": 90, + "5": 7, + "7": 5, + "8": 18, + "9": 409 + }, + "kind": "coupled_handoff", + "paid": { + "1": 2209, + "2": 459, + "3": 494, + "4": 93, + "5": 160, + "6": 18, + "7": 14 + }, + "public": 744 + } + ], + "controls": { + "false_cut_witness": "Exact prefix and suffix handoff witnesses", + "fresh_input_treated_as_owned_zero": "Owned initialization", + "missing_central_translation": "Rejected by the complete Laurent endpoint", + "missing_input_basis_operation": "All public and owned rows", + "old_invoice_at_new_kappa": "Strict negative complete moment", + "old_logarithm_power_1000": "Insufficient complement capacity", + "old_retired_helper_exit": "All public and owned exits", + "wrong_new_helper_coefficient": "All public and owned rows" + }, + "fixed_invoice_ceiling": { + "kappa_interval": [ + "0", + "17/5000" + ], + "moment_derivative": [ + "-796205006234619347545066529772939425482360371994985825314715967/3138550867693340381917894711603833208051177722232017256448", + "-185459398837304902328285171125421705062080707612874684325549331/784637716923335095479473677900958302012794430558004314112" + ], + "scope": "This fixed paid and target invoice under the retained BIT cap." + }, + "inventory": { + "all_main_boundaries_fixed": true, + "events": 25472, + "local_paid_delta": { + "1": -2, + "4": -1, + "5": -4 + }, + "local_target_delta": { + "1": 2, + "2": 5, + "4": 7, + "5": 2, + "7": 5, + "8": 3, + "9": -15 + }, + "owned_paid_paths_fixed": true, + "owned_paid_rank_mass": 56, + "source_events": 25140 + }, + "local": { + "endpoint_coefficients": 565504, + "helpers": { + "1": 2, + "2": 5, + "4": 90, + "5": 7, + "7": 5, + "8": 18, + "9": 409 + }, + "owned_lifetimes": 8, + "paid": { + "1": 2209, + "2": 459, + "3": 494, + "4": 93, + "5": 160, + "6": 18, + "7": 14 + }, + "peak_owned_fields": 1, + "public_inputs": 744, + "real_scalar_allowance": 220332 + }, + "native": { + "distinct_maps": 2926, + "helper_normalizers": 1072, + "helpers": { + "1": 2, + "2": 5, + "4": 90, + "5": 7, + "7": 5, + "8": 18, + "9": 409 + }, + "main_adapters": 208, + "proof": "Every signed Pauli image and exact global phase; frame induction at every positive tensor width", + "recipe_payload_sha256": "7a9003650ed834a233a0f7416976e245c0df0bf93db8eab3a03a462475eb021e", + "wrong_phase_rejected": true + }, + "parallel_comparison": { + "claim": "309839/100000000", + "claim_gain": "141/100000000", + "paid_calls": 66852, + "pr": 5599, + "productive_fields": 13084, + "raw_gain_interval": [ + "140768321/100000000000000", + "140768323/100000000000000" + ], + "raw_interval": [ + "309839352211/100000000000000", + "77459838053/25000000000000" + ], + "scope": "Pinned parallel word; exact scalar endpoint and full invoice comparison. Its native and compiler checks are not repeated.", + "signed_moment_delta": { + "4": 18, + "5": 18, + "9": -18 + }, + "source_commit": "0644592d421b375c221045954fdf13932575ffa8" + }, + "parent_raw_interval": [ + "154094748433/50000000000000", + "308189496867/100000000000000" + ], + "physical": { + "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 + ] + }, + "raw_gain_interval": [ + "895311833/50000000000000", + "447655917/25000000000000" + ], + "result": { + "compiler": { + "H": 707182000000000, + "N": "2^707182000000000", + "eta": { + "lower": "0.000000137418953901550108649586", + "upper": "0.000000137418953901550108649587" + }, + "gap": "1/14000000000", + "integer_test_exponent": 50513, + "logarithm_power": 1024, + "theta": "63/64", + "uniform_saving": "21698603/7000000000", + "word_materialized": false + }, + "full_forward_calls": 18, + "gain": "1791/100000000", + "kappa": "15499/5000000", + "kappa_decimal": ".00309980", + "margin_at_previous": { + "lower": "4.362515302813760389738140460227", + "upper": "4.362515302813760389738140460228" + }, + "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_routes": 5175000, + "local_scalar": 220332, + "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); sum of local ranks is 5987." + }, + "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": "607560855956602797/196000000000000000000", + "fused_gaussian": "607560855869808391/196000000000000000000", + "global_coordinate_router": "10849301/3500000000", + "group_bit_router": "151890217467452097/49000000000000000000", + "group_scans": "6999999999/7000000000", + "main_transform": "607560841956602797/196000000000000000000", + "microbox_face_corrections": "269500000001/3500000000", + "polynomial_products": "13999999999/14000000000", + "sparse_union_movement": "80232560855956602797/196000000000000000000" + }, + "parameters": { + "a": "10849301/3500000000", + "b": "8679441/2800000000", + "beta": "13999999997/14000000000", + "bit_saving": "17/5000", + "cap_xi": "178232560841956602797/196000000000000000000", + "complex_uniform_saving": "21698603/7000000000", + "d": "1/14000000000", + "epsilon": "13999999999/14000000000", + "kappa": "15499/5000000", + "lambda_": "3987600799/4000000000", + "lambda_prime": "13956602797/14000000000", + "layout": "1/14000000000", + "q": "43397203/14000000000", + "r0": "1/140000000000", + "stop": "1/14000000000", + "tested_saving": "6199601/2000000000" + }, + "strict_checks": { + "actual_bit_above_effective": "1050699/3500000000", + "actual_logarithmic_gamma_guard": "1/14000000000", + "actual_logarithmic_group_guard": "17767439179043397203/98000000000000000000", + "alpha_logarithm_absorption": "1/140000000000", + "boundary_algebraic_matrix_above_kappa": "55956602797/196000000000000000000", + "cap_above_band": "80232560841956602797/196000000000000000000", + "cap_below_cell": "17767439144043397203/196000000000000000000", + "cap_below_phase_cell_power": "213767439158043397203/196000000000000000000", + "complex_above_effective": "1/14000000000", + "complex_below_one_over_32": "78820559/2800000000", + "complex_endpoint": "1/7000000000", + "epsilon_below_one": "1/14000000000", + "epsilon_positive": "13999999999/14000000000", + "fine_prime_halo_umbrella": "7/2", + "fused_gaussian_above_kappa": "55869808391/196000000000000000000", + "gaussian_above_main": "6956602797/98000000000000000000", + "global_coordinate_router_above_kappa": "1/3500000000", + "global_gamma_power_slack": "9/140000000000", + "group_below_dimension": "1/7000000000", + "group_bit_router_above_kappa": "17467452097/49000000000000000000", + "group_gauge_power_slack": "17767439178343397203/98000000000000000000", + "group_key_fits_record": "1/7000000000", + "group_positive": "13999999997/14000000000", + "group_scans_above_kappa": "6978301399/7000000000", + "halo_covers_generic_inverse_radius": "5", + "improvement_over_user_baseline": "684414790400418148631/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": "5591320559/39200000000000000000", + "leaf_saving_above_effective": "2791320559/39200000000000000000", + "main_transform_above_kappa": "41956602797/196000000000000000000", + "membership_arithmetic_fits_record": "1/14000000000", + "microbox_face_corrections_above_kappa": "269489150701/3500000000", + "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": "13956602799/14000000000", + "positive_layout_slack": "1/14000000000", + "q_below_effective": "1/14000000000", + "q_below_internal": "1/14000000000", + "q_below_leaf": "5591320559/39200000000000000000", + "q_positive": "43397203/14000000000", + "short_record_fallback": "2791320559/2800000000", + "source_axis_superpolynomial": "1/14000000000", + "sparse_union_movement_above_kappa": "79625000055956602797/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": 41322, + "16": 416, + "2": 8262, + "24": 416, + "3": 8892, + "32": 416, + "4": 1674, + "40": 416, + "48": 416, + "5": 2880, + "56": 416, + "6": 324, + "64": 416, + "7": 252, + "72": 208 + }, + "paid_calls": 66726, + "previous_open_pr5580": "308189/100000000", + "productive_fields": 12976, + "query_shears": 15, + "rank_mass_surplus": 760, + "raw_headroom": [ + "120533/100000000000000", + "60267/50000000000000" + ], + "raw_root_interval": [ + "309980120533/100000000000000", + "154990060267/50000000000000" + ], + "relative_gain_percent": "179100/308189", + "strictification": { + "alpha": { + "lower": "0.999999999281171745636548629142", + "upper": "0.999999999281171745636548629143" + }, + "cutoff": 17, + "delta": { + "lower": "0.968797631748530123162487428735", + "upper": "0.968797631748530123162487428736" + }, + "floor": 18, + "gamma": { + "lower": "0.967786492830639562745171256785", + "upper": "0.967786492830639562745171256786" + }, + "normalized_paid_upper": "5242880004882813/5242880536870912", + "power": 1024, + "reserve": "1/10000000000", + "tail_offset": "1/5", + "tested": "6199601/2000000000" + }, + "targets": { + "1": 36, + "145": 208, + "17": 416, + "2": 90, + "25": 416, + "33": 416, + "4": 1620, + "41": 416, + "49": 416, + "5": 126, + "57": 416, + "65": 416, + "7": 90, + "73": 208, + "8": 324, + "9": 7362 + }, + "whole_idle_jobs": 3120 + }, + "status": "PASS_P104_COUPLED_HELPER_KAPPA_00309980", + "transpose": { + "arithmetic": "Dense integer rows with binary denominators; reverse chronology", + "coefficients": 565504, + "columns": 752 + } +} diff --git a/research/p104-coupled-helper-bases/SOURCES.json b/research/p104-coupled-helper-bases/SOURCES.json new file mode 100644 index 0000000000..60343b4dca --- /dev/null +++ b/research/p104-coupled-helper-bases/SOURCES.json @@ -0,0 +1,71 @@ +{ + "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" + } + ], + "retained_source": { + "path": "research/p104-coupled-helper-bases/inputs/pr5545-source-closure.tar.gz", + "sha256": "59768da554e11b11fae52d07f520f50684cc7a9ee0bec2873edbcd6b63814837", + "export_manifest_sha256": "0a20358f9c089be1f5606c78077314e30a72998fb3c5123848d921a8d1814e76", + "commit": "18968423711fd902aaee1099979497d55603e1dc", + "files": 33, + "source_url": "https://github.com/CrocSwap/integer-mult-bounds/pull/5545", + "note": "The capsule is unchanged. The new local verifier permits nine more public helper fields. The caller and native and interval engines are unchanged." + }, + "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/pr5580-pricing.py", + "source_repository": "aliromman/integer-mult-bounds", + "source_commit": "6efa248cf456d6101d757e9d09ba29711d18a13a", + "source_path": "research/p104-event-contact-step/pricing.py", + "sha256": "e8ffdadf454639fd434a17e276b062d9d6df8310b1aa0ef15e5fb6a4468d6ba2", + "git_blob": "f8f09be7a16542b924bba903867f71f2a092840f" + }, + { + "local_path": "common.py", + "source_repository": "aliromman/integer-mult-bounds", + "source_commit": "6efa248cf456d6101d757e9d09ba29711d18a13a", + "source_path": "research/p104-event-contact-step/common.py", + "sha256": "e7c1bd9bfc0060d2d55da5c6e61cd3fae756e0fc8facacc2a074061d2f73c800", + "git_blob": "bd244313fc023a737055415f87003f2963c290f6" + }, + { + "local_path": "inputs/pr5545-source-closure.tar.gz", + "source_repository": "aliromman/integer-mult-bounds", + "source_commit": "6efa248cf456d6101d757e9d09ba29711d18a13a", + "source_path": "research/p104-event-contact-step/inputs/pr5545-source-closure.tar.gz", + "sha256": "59768da554e11b11fae52d07f520f50684cc7a9ee0bec2873edbcd6b63814837", + "git_blob": "3084088544d1e3136e1f38b8011b9e24edc969c6" + }, + { + "local_path": "inputs/pr5599-WORD.json.gz", + "source_repository": "aliromman/integer-mult-bounds", + "source_commit": "0644592d421b375c221045954fdf13932575ffa8", + "source_path": "research/p104-helper-subspace-splits/WORD.json.gz", + "sha256": "4924640fa7fcbb3895a43bf5f07e7274260feac06ecc95285f77dd8eaee30fa1", + "git_blob": "d9ebf6cace13279bba2fd662d941ddebb4c61278", + "usage": "Comparison with released parallel work; not a constructor input" + } + ], + "retained_source_scope": "The unchanged official PR5545 export supplies the caller, native compiler, independent phase interpreter, moment engines, BIT input and outer ledger. All 33 files are authenticated before import." +} diff --git a/research/p104-coupled-helper-bases/TASK.json b/research/p104-coupled-helper-bases/TASK.json new file mode 100644 index 0000000000..ca5c39215a --- /dev/null +++ b/research/p104-coupled-helper-bases/TASK.json @@ -0,0 +1,166 @@ +{ + "schema_version": 1, + "task_id": "p104-side-correction", + "priority_revision": 7, + "base_commit": "5e0052ca0aa3036a3afa8b0438927377c8d97d53", + "original_card": { + "id": "p104-side-correction", + "question": "Can a changed P104 producer/consumer contract escape the scoped slot, chart and completion obstructions with a favorable full bill?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/p104-literal-slot-defect/README.md", + "research/p104-uniform-commutation-gap/README.md", + "research/p104-uniform-encoding-gap/README.md", + "research/p104-source-chart-shortcut/README.md", + "research/p104-fiber-tag-seam/README.md" + ], + "methods": [ + "Construct one side-correction word at an explicit chronological cut with the needed frames still available.", + "Derive a lower bound on the side correction and hosting costs that decides whether this channel can beat the selected budget." + ], + "acceptance_gate": "An exact arbitrary-input identity, source/target frame availability and restoration at the chosen cut, plus the complete channel+correction+idle/hosting bill or an explicit favorable bound. The native channel alone is not a supplier. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read the named successor obstructions before extending #2981 static flags. Distinguish literal-slot action, commutation, uniform encoding, source-chart shortcut and fiber-tag seam scopes; none excludes all P104 mechanisms.", + "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately." + }, + "first_experiment": "Name one hypothesis changed from these exact interfaces. Write a literal producer-to-consumer timeline and an arbitrary-dirty-input positive/control pair, then charge acquisition, coefficients, completion, hosting and restoration. Stop if the same slot/fiber mismatch persists or the favorable full budget already fails. A scoped independent audit remains useful; another static count is not a new completion.", + "bottleneck_link": "Completing an already realized changed channel tests a concrete construction opportunity, instead of refining the incumbent packing. A positive local result still needs global and all-size admission.", + "allowed_variations": [ + "One correction factorization, one chronological cut, or one explicit hosting obstruction.", + "A changed correction schedule with an updated full bill and native frame contract." + ], + "scope_change_triggers": [ + "Recompiling the already certified low-rank channel without closing a new obligation.", + "Treating a pending ancestor, local histogram or unpriced side correction as an admitted global supplier.", + "Repeating a correction or physical conversion already supplied by a pending follow-up without adding independent coverage or a different unresolved obligation.", + "Repeating the 208-flag static matching or calling a static nested cover a chronological correction program. Independent audit of that certificate is distinct and remains useful.", + "Repeating a static cover, source-chart shortcut or fiber-tag seam without changing the hypothesis responsible for its obstruction." + ], + "overlap_terms": [ + "P104", + "I-G/2", + "side correction", + "native channel", + "1972", + "1991", + "2586", + "endpoint transport", + "physical dual", + "relay composition", + "2981", + "joint unit flags", + "acquisition delivery", + "static nesting", + "4133", + "4136", + "4140", + "4153", + "4154", + "p104-literal-slot-defect", + "p104-uniform-commutation-gap", + "p104-uniform-encoding-gap", + "p104-source-chart-shortcut", + "p104-fiber-tag-seam" + ], + "existing_checks": [ + { + "scope": "PR #4133: literal-slot defect", + "evidence": "research/p104-literal-slot-defect/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "status": "author-checked", + "source_commit": "88666f1dee93fbd85b31fd5d6f91a219e111b5f4", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4136: uniform commutation gap", + "evidence": "research/p104-uniform-commutation-gap/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "status": "author-checked", + "source_commit": "281ce601a8be9db470de630759179c23e1dfaa88", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4140: uniform encoding gap", + "evidence": "research/p104-uniform-encoding-gap/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "status": "author-checked", + "source_commit": "de25c6525aa866962309df5d107b32d55e6e5628", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4153: source-chart shortcut exhausts its optimistic allowance", + "evidence": "research/p104-source-chart-shortcut/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "status": "author-checked", + "source_commit": "9123241fea53df77e51ffe30d9aca1625d4bf3a8", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4154: fiber-tag seam mismatch", + "evidence": "research/p104-fiber-tag-seam/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "status": "author-checked", + "source_commit": "4ffcdaee5d6255a9cea1fe53a5424435068089d0", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Six helper boundary basis changes and nine coupled productive handoffs on the exact PR5580 P104 word. Certify the changed complete invoice and conditional kappa 0.00309980. Credit the released parallel PR5599 split component and prove the additional eighteen g(4,5) complete moment gain with fewer fields and calls.", + "scope_change_reason": "The user requires a further complete kappa improvement. Coupled helper input, cut and output bases change the independent channel contract beyond fixed helper coordinates and fixed scalar contacts. The final refresh found overlapping helper splitting in PR5599. Its public handoff releases composition; the submitted paid-boundary construction is credited and compared against it.", + "bottleneck_link": "https://github.com/CrocSwap/integer-mult-bounds/discussions/5125#discussioncomment-19154639", + "budget_minutes": null, + "stop_rule": "Finish only after the changed full invoice, native caller, compiler and outer calculation pass, then publish one focused reviewable PR. Do not change the selected frontier.", + "outcome": "completed", + "evidence": "PROOF.md, WITNESS.json, WORD.json.gz and RESULT.json bind the exact construction, complete caller and conditional price. VALIDATION.md records replay and publication limits.", + "author": "Ali Romman", + "ai_assistance": "Substantial OpenAI Codex assistance for discovery, construction, proof, verification and publication. The same assistant performed these checks; no subagents or independent reviewer.", + "coordination": { + "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/5125#discussioncomment-19154639", + "base_main": "5e0052ca0aa3036a3afa8b0438927377c8d97d53", + "priority_revision": 7, + "open_prs_checked": 338, + "discussion_records_checked": 4866, + "remote_pagination_complete": true, + "open_prs_checked_utc": "2026-10-25T21:34:30.115889+00:00", + "discussions_checked_utc": "2026-10-25T21:35:33.495718+00:00", + "local_coverage": "Sparse; relevant source words and proof scopes were read. No exhaustive novelty claim.", + "presubmission_main": "5e0052ca0aa3036a3afa8b0438927377c8d97d53", + "excluded_scopes": [ + "PR5565 commuting contact cascade", + "Discussion5575 coupled frame composition", + "PR5590 fixed-contact path floor", + "PR5591 fixed owned-producer recoding", + "Discussion5595 complete native query history", + "Discussion5593 advancing native controllers", + "Literal-slot repairs", + "Global120", + "Global border grading", + "p19 compiler" + ], + "parallel_component": "https://github.com/CrocSwap/integer-mult-bounds/pull/5599", + "composition_release": "https://github.com/CrocSwap/integer-mult-bounds/discussions/5125#discussioncomment-19183908", + "resolution": "The former private-fanout claim changed scope to helper splitting. Its released PR5599 component is credited; no exclusive discovery or additive composition gain is claimed." + }, + "open_questions": [ + { + "question": "Can an independent reviewer accept the coupled handoff lemma and the complete bound?", + "why_it_matters": "Exact author replay is not independent scientific acceptance.", + "first_step": "Inspect the prefix and suffix witnesses, common-chart basis operations and full invoice; run the registered replay.", + "blocked_by": "Independent review remains pending." + }, + { + "question": "Can a source-bound composition with a released changed-contact construction improve the full invoice?", + "why_it_matters": "This package does not establish optimality of the helper basis class or compatibility with other changed words.", + "first_step": "Refresh live claims, pin the proposed input word, reconstruct a compatible witness and recheck all costs.", + "blocked_by": "Composition with PR5565 and the active coupled-frame witness is not checked." + } + ] +} diff --git a/research/p104-coupled-helper-bases/VALIDATION.md b/research/p104-coupled-helper-bases/VALIDATION.md new file mode 100644 index 0000000000..0af0d9493b --- /dev/null +++ b/research/p104-coupled-helper-bases/VALIDATION.md @@ -0,0 +1,71 @@ +# Verification record + +The exact construction and complete price passed on Python 3.12 with the +standard library. The author run used `-W error -B verify.py --write` to +create RESULT.json. It ended with: + +```text +PASS_P104_COUPLED_HELPER_KAPPA_00309980 +``` + +The checked source is PR5580 commit +`6efa248cf456d6101d757e9d09ba29711d18a13a`. Canonical main was refreshed +before submission and remains `5e0052ca0aa3036a3afa8b0438927377c8d97d53`. +The selected record and priority revision 7 are unchanged. + +## Scientific coverage + +- SHA256 and Git blob checks authenticate every external input. The + unchanged PR5545 capsule checks its manifest and all 33 payload files. +- The fixed witness regenerates every word event. All 15 changes pass + arbitrary-input replay. The final word has 744 public inputs, eight + owned lifetimes and one peak owned field. +- A separate dense integer transpose checks all 565504 coefficients. +- The native engines check 2926 distinct maps, 1072 helper normalizers + and 208 main adapters, including signs, global phases and ranks. +- The complete physical caller checks 18 forward local calls, 15 query + shears, 3120 whole idle jobs, routes, central squares and main outputs. +- Three invoice counts agree. Two exact moment engines check the funded + endpoint and the predecessor crossing. The new raw crossing lies in + (0.00309980120533, 0.00309980120534). +- The full compiler checks completion, rounding, tail ratios, complement + capacity, initial range and the finite threshold. All 54 strict and + four functional outer predicates pass. Every listed negative control + in RESULT.json is rejected. + +## Registered and export checks + +The registered command passed in normal and optimized modes, with warnings +as errors and bytecode disabled. Both commands compared the full saved +receipt and printed `PASS_P104_COUPLED_HELPER_KAPPA_00309980`. The launcher +printed `PASS_REGISTERED_RESEARCH_PACKAGE research/p104-coupled-helper-bases +outcome=completed`. Metadata and source-pin validation also passed. + +Separate copies with one changed byte in the PR5580 word or the retained +source capsule were rejected before construction in normal and optimized +modes. Each rejection identified the corrupted source path. + +The scientific package at commit +`8384fb9eda5a2fd47556364b26185f3ba3cbd050` also passed an official Git-free +export check and optimized replay with empty PATH. All 21 exported files, +including the export manifest, were read-only and retained their hashes. +That replay took 99.87 seconds. Exact checks matched all 20 package files +to the commit and confirmed its immediate canonical-main parent. + +The final comparison extension adds the pinned PR5599 word. Its exact +scalar endpoint, complete invoice, crossing and signed difference pass. +The final registered and export checks include this extension. +The full-history ancestry mode cannot run in this shallow checkout. +Exact retained bytes and the branch's immediate canonical-main parent +are checked separately. + +## Limits + +The search and all author checks used the same assistant. No independent +human or proof-kernel review is claimed. Hosted CI is separate from local +verification. The five framework assumptions and the source helper-endpoint +contract remain inherited. The huge uniform word and a complete rounded +multiplier were not materialized. Composition with other active changed +words was not tested. The selected frontier was not edited. + +Ali Romman with substantial OpenAI Codex assistance. Apache-2.0. diff --git a/research/p104-coupled-helper-bases/VERIFIER-CHANGES.diff b/research/p104-coupled-helper-bases/VERIFIER-CHANGES.diff new file mode 100644 index 0000000000..75e9df1d0e --- /dev/null +++ b/research/p104-coupled-helper-bases/VERIFIER-CHANGES.diff @@ -0,0 +1,178 @@ +--- PR5545/local.py ++++ local.py +@@ -2,7 +2,8 @@ + + David Arias supplied the coalesced word. Cinna Davis supplied private reuse. + Gareth Davidson supplied their composition. Ali Romman prepared this caller +-with substantial OpenAI Codex assistance. Apache-2.0. ++with substantial OpenAI Codex assistance. The coupled-basis package retains ++this checker and makes the public field count explicit. Apache-2.0. + """ + from collections import Counter + from fractions import Fraction as Q +@@ -13,17 +14,9 @@ + import importlib.util + import json + import sys +-import tarfile +-import tempfile + + HERE = Path(__file__).resolve().parent + ROOT = HERE.parents[1] +-PREFIX = 'research/p104-coalesced-private-reuse/' +-GEOMETRY = ('research/complex-block-rank-optimum/inputs/selected.json.gz', +- 'research/frame-sa504/inputs/hamming/PROTOTYPE.json', +- 'research/p104-native-channel/inputs/P104-FIXTURE.json') +- +- + def need(ok, why): + if not ok: + raise ValueError(why) +@@ -59,67 +52,17 @@ + return frozenset(out) + + +-def construct(): +- """Rebuild the published source without its obsolete owner-price engine.""" +- manifest = read(ROOT / (PREFIX+'SOURCES.json')) +- archive, = manifest['archives'] +- raw = (ROOT / (PREFIX+'predecessor2152.tar.gz')).read_bytes() +- need(sha256(raw).hexdigest() == archive['sha256'], 'Exact predecessor archive') +- pins = {x['path']: x for x in archive['members']} +- with tempfile.TemporaryDirectory(prefix='p104-source-') as tmp: +- root = Path(tmp) +- with tarfile.open(ROOT / (PREFIX+'predecessor2152.tar.gz')) as data: +- members = data.getmembers() +- need(len(members) == len(pins) == 11 and {m.name for m in members} == set(pins), 'Archive inventory') +- for m in members: +- need(m.isfile() and not Path(m.name).is_absolute() and '..' not in Path(m.name).parts, 'Archive file') +- raw = data.extractfile(m).read() +- need(sha256(raw).hexdigest() == pins[m.name]['sha256'], 'Archive member pin') +- path = root/m.name +- path.parent.mkdir(parents=True, exist_ok=True) +- path.write_bytes(raw) +- for path in GEOMETRY: +- target = root/path +- target.parent.mkdir(parents=True, exist_ok=True) +- target.write_bytes((ROOT/path).read_bytes()) +- C = load(root/'research/p104-interleaved-search/coalesced.py', 'productive_p104_coalesced') +- A = load(ROOT/(PREFIX+'compose.py'), 'productive_p104_composition') +- built = A.construct(C, C.construct()) +- need(built['report'] == read(ROOT/(PREFIX+'RESULT.json'))['composition'], 'Published complete source report') +- frames, numbers = [], {} +- def frame(basis): +- key = tuple(basis) +- if key not in numbers: +- numbers[key] = len(frames) +- frames.append(list(key)) +- return numbers[key] +- initial = [frame(C.F.basis(x)) for x in built['initial']] +- final = [frame(C.F.basis(x)) for x in built['final']] +- live = [r for r in range(112) if len(built['initial'][r]) == 2] +- edges = built['transport_edges'] +- program = [] +- for e in built['scalar_operations']: +- op = e['kind'] +- if op == 'transport': +- edge = edges[e['occurrence']] +- program.append(['MOVE', edge['register'], frame(edge['source_frame']), frame(edge['target_frame']), edge['private']]) +- elif op in ('private_init', 'private_discard'): +- program.append(['INIT' if op == 'private_init' else 'CLEAR', e['register'], frame(e['frame'])]) +- else: +- program.append([{'add':'ADD', 'scale':'SCALE', 'private_copy':'COPY'}[op], *e['registers'], e['coefficient'], frame(e['frame'])]) +- return {'schema':'p104-productive-source/1', 'public':735, 'live':live, 'ports':built['ports'], +- 'frames':frames, 'initial':initial, 'final':final, 'program':program} +- +- + def replay(w): ++ public, width = w['public'], w['public'] + 8 ++ need(public >= 735 and len(w['initial']) == len(w['final']) == public, 'Public field inventory') + need(len(w['program']) < 26000, 'Fixed operation bound') + frames = [span(x) for x in w['frames']] +- rows = [{r:Q(1)} for r in range(743)] ++ rows = [{r:Q(1)} for r in range(width)] + current = list(w['initial']) + [None]*8 + paid, scalar, live_owned, peak = Counter(), 0, set(), 0 + for e in w['program']: + op, r = e[:2] +- need(0 <= r < 743, 'Role index') ++ need(0 <= r < width, 'Role index') + if op == 'MOVE': + _, r, a, b, private = e + need(current[r] == a and (r in live_owned) == private, 'Transport source and ownership') +@@ -127,7 +70,7 @@ + paid[abs(len(w['frames'][b])-len(w['frames'][a]))] += 1 + current[r] = b + elif op == 'INIT': +- need(r >= 735 and r not in live_owned, 'Owned initialization') ++ need(r >= public and r not in live_owned, 'Owned initialization') + live_owned.add(r) + peak = max(peak, len(live_owned)) + rows[r] = {} +@@ -151,7 +94,7 @@ + scalar += 2*(abs(n.bit_length()-d.bit_length()) + int(q < 0)) + else: + s = e[2] +- need(s != r and 0 <= s < 743 and current[s] == f, 'Common scalar chart') ++ need(s != r and 0 <= s < width 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()} +@@ -159,23 +102,24 @@ + 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[:735] == w['final'], 'All public and owned exits') ++ 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 < 735 else {} ++ expected = {r:Q(1)} if r < public else {} + if r-112 in live: + expected[r-112] = Q(1) +- need(row == expected, 'All 743 public and owned rows') ++ 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(735) if r not in main) ++ 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':735, 'owned_lifetimes':8, +- 'peak_owned_fields':peak, 'real_scalar_allowance':scalar, 'endpoint_coefficients':743*743} ++ return {'paid':dict(paid), 'helpers':dict(helpers), 'public_inputs':public, 'owned_lifetimes':8, ++ 'peak_owned_fields':peak, 'real_scalar_allowance':scalar, 'endpoint_coefficients':width*width} + + + def reverse_columns(w): + """Check the transpose with dense dyadic rows and the reverse chronology.""" +- n = 743 ++ n = w['public'] + 8 ++ public = w['public'] + rows = [[int(i == j) for j in range(n)] for i in range(n)] + exponents = [0]*n + for e in reversed(w['program']): +@@ -206,7 +150,7 @@ + exponents[r] -= 1 + for r,row in enumerate(rows): + expected = [0]*n +- if r < 735: ++ if r < public: + expected[r] = 1 << exponents[r] + if r in w['live']: + expected[r+112] = 1 << exponents[r] +@@ -215,6 +159,7 @@ + + + def native(w): ++ public = 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) +@@ -234,7 +179,7 @@ + check(e[2],e[3]) + main = set(w['live']) | {r+112 for r in w['live']} + helper_profile = Counter() +- for r in range(735): ++ for r in range(public): + if r not in main: + helper_profile[check(w['initial'][r],w['final'][r])['rank']] += 1 + adapters = [] diff --git a/research/p104-coupled-helper-bases/VERIFY.json b/research/p104-coupled-helper-bases/VERIFY.json new file mode 100644 index 0000000000..bb84f6b397 --- /dev/null +++ b/research/p104-coupled-helper-bases/VERIFY.json @@ -0,0 +1,32 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 600, + "checks": "Authenticate source bytes and all 33 retained payloads; reconstruct fifteen basis changes; replay all arbitrary inputs, dense transpose, exact native maps and physical caller; check the complete invoice, two rational moment engines, compiler, fixed-invoice ceiling, pinned PR5599 comparison, 58 outer predicates and negative controls; compare the complete receipt." + }, + { + "argv": [ + "{python}", + "-W", + "error", + "-B", + "-O", + "{package}/verify.py" + ], + "timeout_seconds": 600, + "checks": "Authenticate source bytes and all 33 retained payloads; reconstruct fifteen basis changes; replay all arbitrary inputs, dense transpose, exact native maps and physical caller; check the complete invoice, two rational moment engines, compiler, fixed-invoice ceiling, pinned PR5599 comparison, 58 outer predicates and negative controls; compare the complete receipt." + } + ] +} diff --git a/research/p104-coupled-helper-bases/WITNESS.json b/research/p104-coupled-helper-bases/WITNESS.json new file mode 100644 index 0000000000..8073b3c977 --- /dev/null +++ b/research/p104-coupled-helper-bases/WITNESS.json @@ -0,0 +1,981 @@ +{ + "schema": "p104-coupled-helper-bases/1", + "steps": [ + { + "kind": "boundary_basis", + "reverse": true, + "helper": 652, + "cut": 11360, + "frame": 120, + "output": [ + [ + 205, + "-2" + ], + [ + 648, + "-1" + ], + [ + 649, + "-1" + ], + [ + 650, + "1" + ], + [ + 652, + "1" + ] + ], + "cancel": [ + [ + 648, + "1" + ], + [ + 649, + "1" + ], + [ + 650, + "-1" + ] + ] + }, + { + "kind": "boundary_basis", + "reverse": false, + "helper": 341, + "cut": 11151, + "frame": 240, + "output": [ + [ + 93, + "-2" + ], + [ + 339, + "-2" + ], + [ + 341, + "1" + ], + [ + 351, + "2" + ] + ], + "cancel": [ + [ + 337, + "2" + ] + ] + }, + { + "kind": "boundary_basis", + "reverse": true, + "helper": 596, + "cut": 11378, + "frame": 1053, + "output": [ + [ + 188, + "-1" + ], + [ + 592, + "-1" + ], + [ + 593, + "1" + ], + [ + 594, + "1" + ], + [ + 596, + "1" + ] + ], + "cancel": [ + [ + 592, + "1" + ], + [ + 593, + "-1" + ], + [ + 594, + "-1" + ] + ] + }, + { + "kind": "boundary_basis", + "reverse": true, + "helper": 668, + "cut": 11449, + "frame": 1051, + "output": [ + [ + 115, + "2" + ], + [ + 664, + "1" + ], + [ + 665, + "1" + ], + [ + 666, + "-1" + ], + [ + 668, + "1" + ] + ], + "cancel": [ + [ + 664, + "-1" + ], + [ + 665, + "-1" + ], + [ + 666, + "1" + ] + ] + }, + { + "kind": "boundary_basis", + "reverse": true, + "helper": 684, + "cut": 11493, + "frame": 1049, + "output": [ + [ + 126, + "2" + ], + [ + 680, + "-1" + ], + [ + 681, + "1" + ], + [ + 682, + "1" + ], + [ + 684, + "1" + ] + ], + "cancel": [ + [ + 680, + "1" + ], + [ + 681, + "-1" + ], + [ + 682, + "-1" + ] + ] + }, + { + "kind": "boundary_basis", + "reverse": true, + "helper": 649, + "cut": 11525, + "frame": 597, + "output": [ + [ + 649, + "1" + ], + [ + 650, + "-1" + ] + ], + "cancel": [ + [ + 198, + "1/2" + ], + [ + 650, + "1" + ] + ] + }, + { + "kind": "coupled_handoff", + "cut": 10053, + "frame": 306, + "group": [ + 3, + 127 + ], + "pivot": 61, + "v": [ + [ + 257, + "-1/2" + ], + [ + 261, + "1" + ] + ], + "u": [ + [ + 257, + "1" + ] + ], + "source_functional": [ + [ + 61, + "2" + ], + [ + 259, + "2" + ], + [ + 265, + "2" + ] + ], + "output_direction": [ + [ + 115, + "-1/2" + ], + [ + 173, + "1/2" + ], + [ + 188, + "-1/2" + ], + [ + 205, + "-1/2" + ], + [ + 257, + "1/2" + ], + [ + 258, + "-1/2" + ], + [ + 263, + "1/2" + ], + [ + 265, + "1/2" + ], + [ + 268, + "-1/2" + ], + [ + 269, + "-1/2" + ], + [ + 271, + "1/2" + ] + ] + }, + { + "kind": "coupled_handoff", + "cut": 12429, + "frame": 516, + "group": [ + 3, + 127 + ], + "pivot": 432, + "v": [ + [ + 20, + "1" + ], + [ + 110, + "-2" + ], + [ + 435, + "1" + ] + ], + "u": [ + [ + 37, + "2" + ], + [ + 110, + "1" + ] + ], + "source_functional": [ + [ + 21, + "-1" + ], + [ + 435, + "-1" + ] + ], + "output_direction": [ + [ + 432, + "2" + ], + [ + 433, + "2" + ], + [ + 434, + "-1" + ], + [ + 435, + "-1" + ], + [ + 436, + "-1" + ], + [ + 437, + "-1" + ], + [ + 440, + "-1" + ], + [ + 441, + "-1" + ], + [ + 446, + "1" + ], + [ + 447, + "1" + ] + ] + }, + { + "kind": "coupled_handoff", + "cut": 13584, + "frame": 603, + "group": [ + 3, + 127 + ], + "pivot": 572, + "v": [ + [ + 572, + "1/4" + ], + [ + 573, + "-1/4" + ], + [ + 710, + "1" + ] + ], + "u": [ + [ + 710, + "1" + ] + ], + "source_functional": [ + [ + 572, + "1/4" + ], + [ + 573, + "-1/4" + ] + ], + "output_direction": [ + [ + 115, + "2" + ], + [ + 126, + "-2" + ], + [ + 205, + "-2" + ], + [ + 242, + "2" + ], + [ + 243, + "-2" + ], + [ + 247, + "-2" + ], + [ + 249, + "2" + ], + [ + 252, + "-2" + ], + [ + 306, + "-2" + ], + [ + 311, + "-4" + ], + [ + 317, + "-2" + ], + [ + 456, + "4" + ], + [ + 457, + "-4" + ], + [ + 498, + "4" + ], + [ + 499, + "2" + ], + [ + 502, + "-2" + ], + [ + 503, + "2" + ], + [ + 572, + "2" + ], + [ + 573, + "-2" + ], + [ + 710, + "1" + ] + ] + }, + { + "kind": "coupled_handoff", + "cut": 13638, + "frame": 391, + "group": [ + 3, + 127 + ], + "pivot": 345, + "v": [ + [ + 345, + "1/8" + ], + [ + 351, + "-1/4" + ], + [ + 712, + "1" + ] + ], + "u": [ + [ + 712, + "1" + ] + ], + "source_functional": [ + [ + 93, + "1/4" + ] + ], + "output_direction": [ + [ + 93, + "4" + ], + [ + 205, + "-4" + ], + [ + 343, + "-2" + ], + [ + 344, + "-2" + ], + [ + 345, + "-2" + ], + [ + 347, + "-2" + ], + [ + 348, + "-2" + ], + [ + 349, + "-2" + ], + [ + 350, + "2" + ], + [ + 351, + "2" + ], + [ + 712, + "1" + ] + ] + }, + { + "kind": "coupled_handoff", + "cut": 13670, + "frame": 462, + "group": [ + 3, + 127 + ], + "pivot": 14, + "v": [ + [ + 14, + "1/8" + ], + [ + 52, + "-1/4" + ], + [ + 727, + "1" + ] + ], + "u": [ + [ + 727, + "1" + ] + ], + "source_functional": [ + [ + 14, + "1/4" + ] + ], + "output_direction": [ + [ + 14, + "4" + ], + [ + 126, + "-4" + ], + [ + 402, + "-4" + ], + [ + 403, + "-4" + ], + [ + 727, + "1" + ] + ] + }, + { + "kind": "coupled_handoff", + "cut": 13975, + "frame": 424, + "group": [ + 3, + 127 + ], + "pivot": 3, + "v": [ + [ + 3, + "1/4" + ], + [ + 67, + "1/8" + ], + [ + 722, + "1" + ] + ], + "u": [ + [ + 722, + "1" + ] + ], + "source_functional": [ + [ + 3, + "1/4" + ] + ], + "output_direction": [ + [ + 3, + "4" + ], + [ + 115, + "-4" + ], + [ + 370, + "-4" + ], + [ + 372, + "-4" + ], + [ + 722, + "1" + ] + ] + }, + { + "kind": "coupled_handoff", + "cut": 14010, + "frame": 252, + "group": [ + 3, + 127 + ], + "pivot": 76, + "v": [ + [ + 76, + "1/8" + ], + [ + 87, + "-1/4" + ], + [ + 717, + "1" + ] + ], + "u": [ + [ + 717, + "1" + ] + ], + "source_functional": [ + [ + 76, + "1/4" + ] + ], + "output_direction": [ + [ + 76, + "4" + ], + [ + 188, + "-4" + ], + [ + 226, + "-4" + ], + [ + 227, + "-4" + ], + [ + 717, + "1" + ] + ] + }, + { + "kind": "coupled_handoff", + "cut": 9716, + "frame": 267, + "group": [ + 3, + 127 + ], + "pivot": 224, + "v": [ + [ + 57, + "1" + ] + ], + "u": [ + [ + 57, + "-1" + ], + [ + 81, + "1" + ] + ], + "source_functional": [ + [ + 227, + "-1" + ] + ], + "output_direction": [ + [ + 115, + "1/2" + ], + [ + 146, + "1/2" + ], + [ + 151, + "1/2" + ], + [ + 188, + "-1" + ], + [ + 205, + "1/2" + ], + [ + 225, + "1/2" + ], + [ + 226, + "-1/2" + ], + [ + 227, + "-1" + ], + [ + 229, + "1/2" + ], + [ + 230, + "1/2" + ], + [ + 233, + "1/2" + ], + [ + 234, + "1/2" + ], + [ + 236, + "-1" + ], + [ + 237, + "-1/2" + ], + [ + 238, + "1/2" + ] + ] + }, + { + "kind": "coupled_handoff", + "cut": 12126, + "frame": 477, + "group": [ + 3, + 127 + ], + "pivot": 400, + "v": [ + [ + 42, + "1" + ] + ], + "u": [ + [ + 41, + "1" + ], + [ + 42, + "1" + ] + ], + "source_functional": [ + [ + 403, + "1" + ] + ], + "output_direction": [ + [ + 126, + "3/2" + ], + [ + 133, + "1/2" + ], + [ + 146, + "1/2" + ], + [ + 151, + "-1/2" + ], + [ + 400, + "1" + ], + [ + 401, + "-1" + ], + [ + 403, + "1" + ], + [ + 404, + "-1/2" + ], + [ + 405, + "-1/2" + ], + [ + 406, + "-1/2" + ], + [ + 407, + "-1/2" + ], + [ + 408, + "-1/2" + ], + [ + 409, + "-1" + ], + [ + 410, + "-1/2" + ], + [ + 412, + "1/2" + ], + [ + 413, + "1" + ], + [ + 414, + "1/2" + ] + ] + } + ] +} diff --git a/research/p104-coupled-helper-bases/WORD.json.gz b/research/p104-coupled-helper-bases/WORD.json.gz new file mode 100644 index 0000000000..48a91124eb Binary files /dev/null and b/research/p104-coupled-helper-bases/WORD.json.gz differ diff --git a/research/p104-coupled-helper-bases/caller.py b/research/p104-coupled-helper-bases/caller.py new file mode 100644 index 0000000000..6ac5e73569 --- /dev/null +++ b/research/p104-coupled-helper-bases/caller.py @@ -0,0 +1,175 @@ +"""An all-forward caller for the credited P104 supplier. + +The Laurent controller is by Cinna Davis. Its replay and signed-swap +identity follow Ali Romman's PR5398. This inverse wrapper and source binding +are by Ali Romman with substantial OpenAI Codex assistance. Apache-2.0. +""" +from copy import deepcopy +from fractions import Fraction as Q +from collections import Counter +from hashlib import sha256 +import json +import local as L +need = L.need + +def replay(word): + """Check the literal p16 word and both rational boundary programs.""" + need((word['kind'], word['pairs'], word['prefix_pairs'], word['ambient_rank']) == ('complex', 16, 7, 145), 'Source p16/a7 controller') + zero = (0,) * 34 + def plus(dst, src, q): + for k, v in src.items(): + value = dst.get(k, Q(0)) + q * v + if value: dst[k] = value + else: dst.pop(k, None) + def shifted(row, term, sign=1): + return [{tuple(a + b for a, b in zip(k, term)): sign * v for k, v in cell.items()} for cell in row] + for side in ('left', 'right'): + matrix = [[Q(i == j) for j in range(32)] for i in range(32)] + for e in word['boundaries'][side + '_program']: + if e[0] == 'SWAP': matrix[e[1]], matrix[e[2]] = matrix[e[2]], matrix[e[1]] + elif e[0] == 'SCALE': matrix[e[1]] = [Q(e[2]) * x for x in matrix[e[1]]] + else: + need(e[0] == 'ADD', 'Boundary scalar opcode') + matrix[e[1]] = [x + Q(e[3]) * y for x, y in zip(matrix[e[1]], matrix[e[2]])] + need(matrix == [[Q(x) for x in row] for row in word['boundaries'][side]], 'Exact scalar boundary program') + rows = [[{zero: Q(x)} if Q(x) else {} for x in row] for row in word['boundaries']['right']] + for e in word['physical_events']: + if e[0] in ('LOCAL', 'QUERY_SHEAR'): + _, stage, pair, back = e + x, y = 2 * pair, 2 * pair + 1 + if back: x, y = y, x + term = (1 if back else -1,) + (0,) * 33 + for dst, src in zip(rows[y], shifted(rows[x], term)): + plus(dst, src, Q(-1 if back else 1)) + if e[0] == 'LOCAL': + term = (0,) + tuple(int(s == stage) for s in range(33)) + for r in (x, y): rows[r] = shifted(rows[r], term) + elif e[0] == 'Q_POWER': + need(e[2] in (-2, 2), 'Only even central powers are free') + rows[e[1]] = shifted(rows[e[1]], (e[2],) + (0,) * 33) + elif e[0] == 'IDLE': + term = (0,) + tuple(int(s in e[2]) for s in range(33)) + for r in (2 * e[1], 2 * e[1] + 1): rows[r] = shifted(rows[r], term) + elif e[0] == 'ADD': + for dst, src in zip(rows[e[1]], rows[e[2]]): plus(dst, src, Q(e[3])) + else: + need(e[0] in ('SWAP', 'SIGNED_SWAP'), 'Controller physical opcode') + rows[e[1]], rows[e[2]] = rows[e[2]], shifted(rows[e[1]], zero, -1 if e[0] == 'SIGNED_SWAP' else 1) + out = [[{} for _ in range(32)] for _ in range(32)] + for i, row in enumerate(word['boundaries']['left']): + for k, q in enumerate(row): + if Q(q): + for j in range(32): plus(out[i][j], rows[k][j], Q(q)) + expected = [[{tuple(word['diagonal'][i]): Q(1)} if i == j else {} for j in range(32)] for i in range(32)] + need(out == expected, 'All p16 Laurent coefficients, central signs and boundary factors') + return word + + + +def construct(): + source = L.read(L.ROOT/'research/joint-helper-lattice/CONTROLLER.json') + replay(source) + word = deepcopy(source) + events, sites = [], [] + for e in source['physical_events']: + if e[0] == 'LOCAL' and e[3]: + _, stage, pair, _ = e + x, y = 2*pair, 2*pair+1 + events += [['Q_POWER',x,-2], ['SIGNED_SWAP',x,y], ['LOCAL',stage,pair,False], + ['Q_POWER',y,2], ['SIGNED_SWAP',y,x]] + sites.append(stage) + else: + events.append(deepcopy(e)) + word['physical_events'] = events + word['wrapper_sites'] = sites + word.pop('invoice') + need(len(sites) == 16 and all(not e[3] for e in events if e[0] == 'LOCAL'), 'Eighteen forward suppliers') + replay(word) + return word + + +def physical(word, local): + N = L.load(L.ROOT/'research/pr4359-p7-padding/native_inventory.py', 'productive_p104_phase_polynomial') + source = L.read(L.ROOT/'research/kappa-0023-productive-jobs/dependencies/kappa-next-regime/direct-decoder/sources/DATA-PHASES.json') + recipes = {r['q']:r for r in source['recipes']} + dimension = 265 + axes = tuple(1 << i for i in range(dimension)) + def completed(stage): + return N.norm((axis,1) for axis in axes[:9+8*stage]) + contacts, squares, target_profile = [], 0, Counter() + idle_jobs = Counter() + for _,stage,pair,back in (e for e in word['physical_events'] if e[0] == 'LOCAL'): + need(not back, 'No inverse-transpose local implementation') + spectator = N.norm((axis,1) for axis in axes[9:9+8*stage]) + for q in local['ports']: + basis = recipes[q]['idle_children'][0]['orthogonal_axes'][:8] + need(all((x&q).bit_count()%2 == 0 for x in basis), 'Fresh-block basis fixes central port') + need(all((a&b).bit_count()%2 == int(i==j) for i,a in enumerate(basis) for j,b in enumerate(basis)), 'Actual orthonormal basis') + swaps = [] if stage == 0 else [b ^ axes[9+8*(stage-1)+i] for i,b in enumerate(basis)] + route = tuple(e ^ N.act(swaps,sum(((e&v).bit_count()%2) << i for i,v in enumerate(swaps))) for e in axes) + need(all(N.act(route,route[i]) == axes[i] for i in range(dimension)), 'Route inverse') + need(all((a&b).bit_count()%2 == int(i==j) for i,a in enumerate(route) for j,b in enumerate(route)), 'Orthogonal physical route') + need(N.act(route,q) == q, 'Route preserves Q') + raw_x = N.norm([(q,1)]) if stage == 0 else completed(stage-1) + raw_y = () if stage == 0 else N.norm(list(raw_x)+[(q,-1)]) + entry_x, entry_y = N.norm(list(spectator)+[(q,1)]), spectator + out0 = N.norm(list(spectator)+[(axis,1) for axis in axes[:9]]) + exit_x, exit_y = out0, N.norm(list(out0)+[(q,-1)]) + out_x, out_y = completed(stage), N.norm(list(completed(stage))+[(q,-1)]) + maps = [N.contact(a,b,route,dimension) for a,b in [(raw_x,entry_x),(raw_y,entry_y),(exit_x,out_x),(exit_y,out_y)]] + delta = N.norm([(axis,1) for axis in axes[:9]]+[(q,-1)]) if stage == 0 else N.norm((axis,1) for axis in axes[9+8*(stage-1):9+8*stage]) + for incoming,outgoing in [(raw_x,out_x),(raw_y,out_y)]: + need(N.polynomial(N.norm(list(outgoing)+[(a,-c) for a,c in incoming]),dimension) == N.polynomial(delta,dimension), 'Actual diagonal D_s') + cross = N.norm(list(out_y)+[(a,-c) for a,c in raw_x]) + need(N.polynomial(cross,dimension) == N.polynomial(N.norm(list(delta)+[(q,-1)]),dimension), 'Actual cross term D_s Q^-1') + need(sum(route[i] != axes[i] for i in range(dimension)) <= 17 and all(m['translation'].bit_count() <= 17 and m['inverse_translation'].bit_count() <= 17 for m in maps), 'Fixed seventeen-axis route allowance') + contacts.append([stage,q,maps]) + for q in local['ports']: + # Multiply the Gaussian pair twice with exact real and imaginary parts. + a,b = (Q(1,2),Q(1,2)), (Q(1,2),Q(-1,2)) + mul = lambda z,w: (z[0]*w[0]-z[1]*w[1],z[0]*w[1]+z[1]*w[0]) + plus = lambda z,w: (z[0]+w[0],z[1]+w[1]) + diagonal,off = plus(mul(a,a),mul(b,b)), plus(mul(a,b),mul(b,a)) + need(diagonal == (0,0) and off == (1,0), 'Q^2 is translation with phase +1') + for address in range(512): + need({address:diagonal,address^q:off}[address^q] == (1,0), 'Every central square column') + squares += 1 + for term in word['diagonal']: + qp,selected = term[0],term[1:] + physical = N.norm([(q,qp)]+[(axis,1) for s,yes in enumerate(selected) if yes for axis in (axes[:9] if s == 0 else axes[9+8*(s-1):9+8*s])]+[(q,-1)]*selected[0]) + positive = list(axes[:9]) if selected[0] else [q] + positive += [axis for s in range(1,len(selected)) if selected[s] for axis in axes[9+8*(s-1):9+8*s]] + need(N.polynomial(physical,dimension) == N.polynomial(N.norm([(x,1) for x in positive]+[(q,2)]*(qp == -1)),dimension), 'Full main output phase and rank') + target_profile[len(positive)] += 1 + for e in word['physical_events']: + if e[0] != 'IDLE': + continue + stages = e[2] + need(len(stages) == len(set(stages)), 'Whole idle has no repeated stage') + for q in local['ports']: + positive, physical = [], [] + for stage in stages: + if stage == 0: + positive += recipes[q]['idle_children'][0]['orthogonal_axes'][:8] + physical += [(x,1) for x in axes[:9]]+[(q,-1)] + else: + block = axes[9+8*(stage-1):9+8*stage] + positive += block + physical += [(x,1) for x in block] + need(len(positive) == 8*len(stages), 'All idle Gaussian axes') + need(all((a&b).bit_count()%2 == int(i==j) for i,a in enumerate(positive) for j,b in enumerate(positive)), 'Independent orthonormal idle axes') + N.contact(N.norm(physical),N.norm((x,1) for x in positive),axes,dimension) + idle_jobs[len(positive)] += 2 + return {'ports':104,'full_calls':18,'physical_contacts':4*len(contacts),'central_square_columns':squares, + 'main_targets':dict(target_profile),'whole_idle_jobs':dict(idle_jobs),'route_payload_sha256':sha256(json.dumps(contacts,separators=(',',':')).encode()).hexdigest(), + 'wrapper_sites':word['wrapper_sites'],'new_paid_jobs':0,'tensor_rule':'Factorwise native maps; scalar signs stay outside the tensor power.'} + + +def controls(word): + bad = deepcopy(word) + bad['physical_events'].remove(next(e for e in bad['physical_events'] if e[0] == 'Q_POWER')) + try: + replay(bad) + except ValueError: + return {'missing_central_translation':'Rejected by the complete Laurent endpoint'} + raise ValueError('Missing central translation accepted') diff --git a/research/p104-coupled-helper-bases/common.py b/research/p104-coupled-helper-bases/common.py new file mode 100644 index 0000000000..bd244313fc --- /dev/null +++ b/research/p104-coupled-helper-bases/common.py @@ -0,0 +1,47 @@ +"""Open the byte-pinned PR5545 source closure (same pins as PR5551/PR5561); Apache-2.0. + +Copied from PR5561's research/p104-free-endpoint-retime/common.py (DreamingOfClouds), package path +renamed only. Mechanism and all predecessor credit: see README.md. +""" +from contextlib import contextmanager +from hashlib import sha256 +from io import BytesIO +from pathlib import Path,PurePosixPath +import gzip,importlib.util,json,sys,tarfile,tempfile + +HERE=Path(__file__).resolve().parent +def need(ok,why): + if not ok: + raise ValueError(why) + +def read(path): + raw=Path(path).read_bytes() + return json.loads(gzip.decompress(raw) if str(path).endswith('.gz') else raw) + +def load(path,name): + spec=importlib.util.spec_from_file_location(name,path) + mod=importlib.util.module_from_spec(spec);sys.modules[name]=mod;spec.loader.exec_module(mod);return mod + +@contextmanager +def closure(): + pins=json.loads((HERE/'SOURCES.json').read_bytes())['retained_source'] + raw=(HERE/'inputs'/Path(pins['path']).name).read_bytes() + need(sha256(raw).hexdigest()==pins['sha256'],'Retained PR5545 capsule byte pin') + with tempfile.TemporaryDirectory(prefix='p104-priced-handoff-')as tmp: + root=Path(tmp) + with tarfile.open(fileobj=BytesIO(gzip.decompress(raw)),mode='r:')as archive: + members=archive.getmembers();names=[m.name for m in members] + need(len(names)==len(set(names)),'Unique retained source paths') + for m in members: + n=PurePosixPath(m.name) + need(m.isfile()and not n.is_absolute()and '..'not in n.parts,'Regular retained source path') + t=root/m.name;t.parent.mkdir(parents=True,exist_ok=True);t.write_bytes(archive.extractfile(m).read()) + mraw=(root/'.research-export.json').read_bytes() + need(sha256(mraw).hexdigest()==pins['export_manifest_sha256'],'Exact export inventory') + man=json.loads(mraw) + need(man['commit']==pins['commit']and len(man['files'])==pins['files']==33,'Exact predecessor closure') + need(set(names)=={'.research-export.json'}|{r['path']for r in man['files']},'No omitted or extra file') + for r in man['files']: + b=(root/r['path']).read_bytes() + need(len(b)==r['size']and sha256(b).hexdigest()==r['sha256'],'Source file '+r['path']) + yield root diff --git a/research/p104-coupled-helper-bases/construct.py b/research/p104-coupled-helper-bases/construct.py new file mode 100644 index 0000000000..ef5936ca89 --- /dev/null +++ b/research/p104-coupled-helper-bases/construct.py @@ -0,0 +1,215 @@ +"""Construct the fixed helper basis changes and coupled handoffs. + +Ali Romman with substantial OpenAI Codex assistance. Apache-2.0. +The source word and its contributors are recorded in SOURCES.json. +""" +from copy import deepcopy +from fractions import Fraction as Q +import local as L + + +def row(pairs): + out = {r: Q(q) for r, q in pairs} + L.need(len(out) == len(pairs) and all(out.values()), 'Unique nonzero witness row') + return out + + +def unit(q): + n, d = abs(q.numerator), q.denominator + return n > 0 and n & (n-1) == 0 and d & (d-1) == 0 + + +def main_fields(w): + return set(w['live']) | {r+112 for r in w['live']} + + +def prefix(w, cut): + n = w['public'] + rows = [{i: Q(1)} for i in range(n)] + [{} for _ in range(8)] + frames = w['initial'][:] + [None]*8 + L.need(0 <= cut < len(w['program']), 'Cut in the literal word') + for e in w['program'][:cut+1]: + op, r = e[:2] + if op == 'MOVE': + L.need(frames[r] == e[2], 'Prefix transport source') + frames[r] = e[3] + elif op in ('INIT', 'CLEAR'): + rows[r] = {} + frames[r] = e[2] if op == 'INIT' else None + else: + L.need(frames[r] == e[-1], 'Prefix scalar chart') + if op == 'SCALE': + rows[r] = {k: Q(e[-2])*v for k, v in rows[r].items()} + else: + L.need(frames[e[2]] == e[-1], 'Prefix source chart') + if op == 'COPY': + L.need(not rows[r], 'Source COPY into zero') + L.add(rows[r], rows[e[2]], Q(e[-2])) + return rows, frames + + +def suffix_columns(w, cut): + cols = [{i: Q(1)} for i in range(w['public'])] + [{} for _ in range(8)] + for e in reversed(w['program'][cut+1:]): + op, r = e[:2] + if op == 'MOVE': + continue + if op in ('INIT', 'CLEAR'): + cols[r] = {} + elif op == 'SCALE': + cols[r] = {k: Q(e[-2])*v for k, v in cols[r].items()} + else: + L.add(cols[e[2]], cols[r], Q(e[-2])) + if op == 'COPY': + cols[r] = {} + return cols + + +def transpose(w): + program = [] + for e in reversed(w['program']): + op, r = e[:2] + if op == 'MOVE': + z = ['MOVE', r, e[3], e[2], e[4]] + elif op in ('ADD', 'COPY'): + z = ['ADD', e[2], r, e[3], e[4]] + elif op == 'SCALE': + z = e[:] + else: + L.need(op in ('INIT', 'CLEAR'), 'Transpose opcode') + z = ['CLEAR' if op == 'INIT' else 'INIT', r, e[2]] + program.append(z) + return dict(w, initial=w['final'][:], final=w['initial'][:], program=program) + + +def boundary_basis(w, c): + w = transpose(w) if c['reverse'] else deepcopy(w) + h, cut, frame = c['helper'], c['cut'], c['frame'] + output, cancel = row(c['output']), row(c['cancel']) + helpers = set(range(w['public'])) - main_fields(w) + L.need(h in helpers and unit(output.get(h, Q(0))), 'Helper unit boundary pivot') + source = w['initial'][h] + L.need(set(output) <= {r for r in helpers if w['initial'][r] == source}, + 'Boundary basis uses one helper input chart') + rows, frames = prefix(w, cut) + L.need(frames[h] == frame and h not in cancel and + all(frames[r] == frame for r in cancel), 'Available boundary cancellation') + value = rows[h].copy() + for r, q in cancel.items(): + L.add(value, rows[r], -q) + L.need(value == output, 'Exact boundary helper relation') + tail = w['program'][cut+1:] + L.need(not any(e[0] in ('ADD', 'COPY') and e[2] == h for e in tail), + 'Retired helper has no later source read') + coefficient = output[h] + before = [['ADD', h, r, str(-q/coefficient), source] + for r, q in sorted(output.items()) if r != h] + middle = [['ADD', h, r, str(-q), frame] for r, q in sorted(cancel.items())] + if coefficient != 1: + middle.append(['SCALE', h, str(1/coefficient), frame]) + w['program'] = before + w['program'][:cut+1] + middle + [e for e in tail if e[1] != h] + w['final'][h] = frame + return transpose(w) if c['reverse'] else w + + +def inverse(ops): + out = [] + for e in reversed(ops): + z = e[:] + z[-2] = str(1/Q(e[-2]) if e[0] == 'SCALE' else -Q(e[-2])) + out.append(z) + return out + + +def basis(a, b, p, frame): + """Return a matrix R with a R = e_p^T and R e_p = b.""" + L.need(sum(a.get(h, 0)*q for h, q in b.items()) == 1, 'Dual basis pairing') + q = next((h for h in sorted(a) if unit(a[h])), None) + L.need(q is not None, 'Dyadic basis pivot') + ops = [] if p == q else [ + ['ADD', p, q, '1', frame], ['ADD', q, p, '-1', frame], + ['ADD', p, q, '1', frame], ['SCALE', q, '-1', frame]] + ops += [['ADD', j, q, str(c), frame] for j, c in sorted(b.items()) if j != q] + if a[q] != 1: + ops.append(['SCALE', q, str(1/a[q]), frame]) + ops += [['ADD', q, j, str(-c/a[q]), frame] for j, c in sorted(a.items()) if j != q] + return ops + + +def relabel(e, mapping): + z = e[:] + z[1] = mapping(z[1]) + if z[0] in ('ADD', 'COPY'): + z[2] = mapping(z[2]) + return z + + +def handoff(w, c): + n, cut, frame, p = w['public'], c['cut'], c['frame'], c['pivot'] + source, target = c['group'] + group = {h for h in range(n) if h not in main_fields(w) and + (w['initial'][h], w['final'][h]) == (source, target)} + v, u = row(c['v']), row(c['u']) + pairing = sum(v.get(h, 0)*q for h, q in u.items()) + L.need(unit(pairing), 'Nonzero dyadic handoff pairing') + v = {h: q/pairing for h, q in v.items()} + rows, frames = prefix(w, cut) + L.need(all(f is None for f in frames[n:]), 'No owned field at handoff cut') + L.need(p in group and frames[p] == frame and + all(0 <= h < n and frames[h] == frame for h in v.keys() | u.keys()), + 'Public handoff fields share the cut chart') + L.need(L.span(w['frames'][source]) < L.span(w['frames'][frame]) < + L.span(w['frames'][target]), 'Strict nested handoff boundaries') + cols, a, b = suffix_columns(w, cut), {}, {} + for r, q in v.items(): + L.add(a, rows[r], q) + for r, q in u.items(): + L.add(b, cols[r], q) + L.need(a == row(c['source_functional']) and b == row(c['output_direction']), + 'Exact prefix and suffix handoff witnesses') + L.need(set(a) <= group and set(b) <= group, 'Handoff has only helper boundary support') + input_ops, cut_basis = basis(a, b, p, source), basis(v, u, p, frame) + output_ops = inverse(input_ops) + for e in output_ops: + e[-1] = target + old = lambda r: r+1 if r >= n else r + tail = lambda r: n if r == p else old(r) + out = deepcopy(w) + out['public'] = n+1 + out['initial'].append(frame) + out['final'][p] = frame + out['final'].append(target) + out['program'] = input_ops + [relabel(e, old) for e in w['program'][:cut+1]] + out['program'] += inverse(cut_basis) + [relabel(e, tail) for e in cut_basis] + out['program'] += [relabel(e, tail) for e in w['program'][cut+1:]] + out['program'] += [relabel(e, tail) for e in output_ops] + return out + + +def restore_copy_opcodes(w): + fresh, copies = set(), 0 + for e in w['program']: + op, r = e[:2] + if op == 'INIT': + fresh.add(r) + elif r in fresh and op != 'MOVE': + L.need(op == 'ADD', 'First owned write is the retained copy') + e[0] = 'COPY' + fresh.remove(r) + copies += 1 + L.need(not fresh and copies == 8, 'All eight owned copy paths remain') + + +def construct(base, witness): + L.need(witness['schema'] == 'p104-coupled-helper-bases/1', 'Witness schema') + L.need([s['kind'] for s in witness['steps']] == + ['boundary_basis']*6 + ['coupled_handoff']*9, 'Fixed fifteen changes') + word, evidence = deepcopy(base), [] + for step in witness['steps']: + word = boundary_basis(word, step) if step['kind'] == 'boundary_basis' else handoff(word, step) + check = L.replay(word) + evidence.append(dict(kind=step['kind'], public=word['public'], + events=len(word['program']), paid=check['paid'], helpers=check['helpers'])) + restore_copy_opcodes(word) + L.replay(word) + return word, evidence diff --git a/research/p104-coupled-helper-bases/inputs/pr5545-source-closure.tar.gz b/research/p104-coupled-helper-bases/inputs/pr5545-source-closure.tar.gz new file mode 100644 index 0000000000..3084088544 Binary files /dev/null and b/research/p104-coupled-helper-bases/inputs/pr5545-source-closure.tar.gz differ diff --git a/research/p104-coupled-helper-bases/inputs/pr5580-WORD.json.gz b/research/p104-coupled-helper-bases/inputs/pr5580-WORD.json.gz new file mode 100644 index 0000000000..9434855e7d Binary files /dev/null and b/research/p104-coupled-helper-bases/inputs/pr5580-WORD.json.gz differ diff --git a/research/p104-coupled-helper-bases/inputs/pr5580-pricing.py b/research/p104-coupled-helper-bases/inputs/pr5580-pricing.py new file mode 100644 index 0000000000..f8f09be7a1 --- /dev/null +++ b/research/p104-coupled-helper-bases/inputs/pr5580-pricing.py @@ -0,0 +1,156 @@ +"""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 prepared for thu-nmrc with substantial OpenAI Codex assistance. +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('.00308189'), Q('.0030818905') +PREVIOUS = Q('.00308181') + + +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()) == 12814 and sum(paid.values()) == 66852, '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) + 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 selected kappa') + 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(97,100) + 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),1000 + 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':'.00308189','previous_open_pr5569':PREVIOUS,'gain':KAPPA-PREVIOUS, + 'relative_gain_percent':100*(KAPPA/PREVIOUS-1),'raw_root_interval':[lower,upper], + 'raw_headroom':[lower-KAPPA,upper-KAPPA],'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, + '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.', + 'tensor_native_growth_bound':f'Each rank-r Gaussian has row l1 norm at most 2^(rf); sum of local ranks is {sum(r*n for r,n in local["paid"].items())}.'}, + '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-coupled-helper-bases/inputs/pr5599-WORD.json.gz b/research/p104-coupled-helper-bases/inputs/pr5599-WORD.json.gz new file mode 100644 index 0000000000..d9ebf6cace Binary files /dev/null and b/research/p104-coupled-helper-bases/inputs/pr5599-WORD.json.gz differ diff --git a/research/p104-coupled-helper-bases/local.py b/research/p104-coupled-helper-bases/local.py new file mode 100644 index 0000000000..9556e86744 --- /dev/null +++ b/research/p104-coupled-helper-bases/local.py @@ -0,0 +1,209 @@ +"""Replay the credited P104 word and its complete native interfaces. + +David Arias supplied the coalesced word. Cinna Davis supplied private reuse. +Gareth Davidson supplied their composition. Ali Romman prepared this caller +with substantial OpenAI Codex assistance. The coupled-basis package retains +this checker and makes the public field count explicit. 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, width = w['public'], w['public'] + 8 + need(public >= 735 and len(w['initial']) == len(w['final']) == public, 'Public field inventory') + need(len(w['program']) < 26000, 'Fixed operation bound') + frames = [span(x) for x in w['frames']] + rows = [{r:Q(1)} for r in range(width)] + current = list(w['initial']) + [None]*8 + paid, scalar, live_owned, peak = Counter(), 0, set(), 0 + for e in w['program']: + op, r = e[:2] + need(0 <= r < width, '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) + 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 < width 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':8, + 'peak_owned_fields':peak, 'real_scalar_allowance':scalar, 'endpoint_coefficients':width*width} + + +def reverse_columns(w): + """Check the transpose with dense dyadic rows and the reverse chronology.""" + n = w['public'] + 8 + public = w['public'] + 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): + public = 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(public): + 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-coupled-helper-bases/pricing.py b/research/p104-coupled-helper-bases/pricing.py new file mode 100644 index 0000000000..493c7a8a0d --- /dev/null +++ b/research/p104-coupled-helper-bases/pricing.py @@ -0,0 +1,157 @@ +"""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. +The contact versions are by thu-nmrc, DreamingOfClouds, GamingPuzzled and +Ali Romman. The coupled-basis counts and compiler power are by Ali Romman +with substantial OpenAI Codex assistance. +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('.00309980'), Q('.0030998005') +PREVIOUS = Q('.00308189') + + +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()) == 12976 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) + 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 selected kappa') + 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(97,100) + 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':'.00309980','previous_open_pr5580':PREVIOUS,'gain':KAPPA-PREVIOUS, + 'relative_gain_percent':100*(KAPPA/PREVIOUS-1),'raw_root_interval':[lower,upper], + 'raw_headroom':[lower-KAPPA,upper-KAPPA],'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, + '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.', + 'tensor_native_growth_bound':f'Each rank-r Gaussian has row l1 norm at most 2^(rf); sum of local ranks is {sum(r*n for r,n in local["paid"].items())}.'}, + '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-coupled-helper-bases/verify.py b/research/p104-coupled-helper-bases/verify.py new file mode 100644 index 0000000000..54bd574139 --- /dev/null +++ b/research/p104-coupled-helper-bases/verify.py @@ -0,0 +1,208 @@ +"""Check the coupled helper word and its complete conditional price. + +Ali Romman with substantial OpenAI Codex assistance. Apache-2.0. +The fixed-invoice derivative check follows the credited PR5580 checker. +""" +from collections import Counter +from copy import deepcopy +from fractions import Fraction as Q +from hashlib import sha1, sha256 +from pathlib import Path +import difflib +import json +import sys + +sys.dont_write_bytecode = True +HERE = Path(__file__).resolve().parent +sys.path.insert(0, str(HERE)) +from common import closure, load, need, read +import local as L +from construct import construct + + +def inventory(base, word, old, new): + need(base['frames'] == word['frames'] and base['ports'] == word['ports'] and + base['live'] == word['live'], 'Same native charts and 104 literal ports') + main = set(base['live']) | {h+112 for h in base['live']} + for h in main: + need((base['initial'][h], base['final'][h]) == + (word['initial'][h], word['final'][h]), 'Same main boundary contract') + need((base['public'], word['public']) == (735, 744), 'Nine additional independent inputs') + need(new['paid'] == {1: 2209, 2: 459, 3: 494, 4: 93, 5: 160, 6: 18, 7: 14}, + 'Exact new paid profile') + need(new['helpers'] == {1: 2, 2: 5, 4: 90, 5: 7, 7: 5, 8: 18, 9: 409}, + 'Exact new target profile') + def owned(w): + return [[e[0], e[1]-w['public'], *e[2:]] for e in w['program'] + if e[1] >= w['public'] and e[0] in ('INIT', 'CLEAR', 'MOVE')] + need(owned(base) == owned(word), 'Same eight owned lifetimes and paid paths') + need(sum(e[0] == 'COPY' for e in word['program']) == 8, 'Eight owned copies') + def delta(key): + return {r: new[key].get(r, 0)-old[key].get(r, 0) + for r in sorted(new[key].keys() | old[key].keys()) + if new[key].get(r, 0) != old[key].get(r, 0)} + need(sum(new['paid'].values()) == sum(old['paid'].values())-7, 'Seven fewer local transports') + need(sum(r*n for r, n in delta('paid').items()) == -26 and + sum(r*n for r, n in delta('helpers').items()) == -26, 'Both rank masses fall by 26') + return {'source_events': len(base['program']), 'events': len(word['program']), + 'local_paid_delta': delta('paid'), 'local_target_delta': delta('helpers'), + 'all_main_boundaries_fixed': True, 'owned_paid_paths_fixed': True, + 'owned_paid_rank_mass': sum(abs(len(word['frames'][e[2]])-len(word['frames'][e[3]])) + for e in word['program'] if e[0] == 'MOVE' and e[4])} + + +def controls(base, witness, word): + variants = {} + bad = deepcopy(word) + bad['program'].pop(next(i for i, e in enumerate(bad['program']) if e[0] == 'ADD')) + variants['missing_input_basis_operation'] = bad + bad = deepcopy(word) + event = next(e for e in bad['program'] if e[0] == 'ADD' and 735 in e[1:3]) + event[-2] = str(2*Q(event[-2])) + variants['wrong_new_helper_coefficient'] = bad + bad = deepcopy(word) + bad['final'][61] = base['final'][61] + variants['old_retired_helper_exit'] = bad + bad = deepcopy(word) + bad['program'].insert(0, ['INIT', 735, bad['initial'][735]]) + variants['fresh_input_treated_as_owned_zero'] = bad + rejected = {} + for name, bad in variants.items(): + try: + L.replay(bad) + except ValueError as error: + rejected[name] = str(error) + else: + raise ValueError('Invalid word accepted: '+name) + bad = deepcopy(witness) + bad['steps'][6]['source_functional'][0][1] = '3' + try: + construct(base, bad) + except ValueError as error: + rejected['false_cut_witness'] = str(error) + else: + raise ValueError('False cut witness accepted') + return rejected + + +def complete_profiles(local): + targets = Counter({r: 18*n for r, n in local['helpers'].items()}) + paid = Counter({r: 18*n for r, n in local['paid'].items()}) + targets[145] += 208 + paid[1] += 1560 + for length in (7, 8): + for j in range(1, length+1): + targets[8*(j+1)+1] += 208 + paid[8*(j+1)] += 208 + return targets, paid + + +def ceiling(E, targets, paid): + cap, lower, upper = Q('.0034'), Q(0), Q(0) + for rank in targets.keys() | paid.keys(): + coefficient = paid.get(rank, 0)-targets.get(rank, 0) + power = (E.power(rank, 1-cap)[0], Q(rank)) + term = E.scale(E.mul(power, E.log_bounds(rank)), coefficient) + lower += term[0] + upper += term[1] + need(upper < 0, 'Strictly decreasing complete moment on the retained BIT band') + return {'kappa_interval': [Q(0), cap], 'moment_derivative': [lower, upper], + 'scope': 'This fixed paid and target invoice under the retained BIT cap.'} + + +def main(): + for pin in read(HERE/'SOURCES.json')['external_inputs']: + raw = (HERE/pin['local_path']).read_bytes() + need(sha256(raw).hexdigest() == pin['sha256'], 'Source bytes: '+pin['local_path']) + need(sha1(('blob '+str(len(raw))+'\0').encode()+raw).hexdigest() == pin['git_blob'], + 'Source Git object: '+pin['local_path']) + base, witness, word = (read(HERE/p) for p in + ('inputs/pr5580-WORD.json.gz', 'WITNESS.json', 'WORD.json.gz')) + regenerated, steps = construct(base, witness) + need(regenerated == word, 'Deterministic complete word reconstruction') + print('PASS source pins and all fifteen exact construction steps', flush=True) + with closure() as root: + L.ROOT = root + old_path = root/'research/p104-productive-controller/local.py' + old_checker = load(old_path, 'p104_legacy_local') + old = old_checker.replay(base) + need(L.replay(base) == old, 'Generalized checker agrees with source checker') + for source, target, label in ((old_path, HERE/'local.py', 'VERIFIER'), + (HERE/'inputs/pr5580-pricing.py', HERE/'pricing.py', 'PRICING')): + names = ('PR5545/local.py', 'local.py') if label == 'VERIFIER' else ('PR5580/pricing.py', 'pricing.py') + diff = ''.join(difflib.unified_diff(source.read_text().splitlines(True), + target.read_text().splitlines(True), + fromfile=names[0], tofile=names[1])) + need(diff == (HERE/(label+'-CHANGES.diff')).read_text(), 'Exact '+label+' review diff') + need((HERE/'caller.py').read_bytes() == (root/'research/p104-productive-controller/caller.py').read_bytes(), + 'Unchanged source caller') + local = L.replay(word) + inv, rejected = inventory(base, word, old, local), controls(base, witness, word) + reverse = L.reverse_columns(word) + print('PASS arbitrary-input endpoints, ownership, controls and dense transpose', flush=True) + native = L.native(word) + print('PASS exact signed native maps', native['distinct_maps'], flush=True) + C = load(HERE/'caller.py', 'coupled_helper_caller') + caller = C.construct() + need(caller == read(root/'research/p104-productive-controller/CONTROLLER.json'), 'Exact physical caller') + physical = C.physical(caller, word) + rejected.update(C.controls(caller)) + print('PASS complete physical caller', flush=True) + P = load(HERE/'pricing.py', 'coupled_helper_pricing') + result = P.run(local, native, caller, physical) + print('PASS complete price, compiler and outer transfer', result['raw_root_interval'], flush=True) + E = load(root/'research/higher-moment-strictification/verify.py', 'coupled_helper_margin') + targets, paid = complete_profiles(local) + need(P.encode(targets) == result['targets'] and P.encode(paid) == result['paid'], 'Third complete invoice') + old_t, old_p = complete_profiles(old) + parent_interval = [Q('.00308189496866'), Q('.00308189496867')] + def margin(t, p, k): + a, b = E.moment(t, 1-k), E.moment(p, 1-k) + return a[0]-b[1], a[1]-b[0] + need(margin(old_t, old_p, parent_interval[0])[0] > 0 > + margin(old_t, old_p, parent_interval[1])[1], 'Exact PR5580 crossing') + need(margin(old_t, old_p, P.KAPPA)[1] < 0, 'Old complete invoice rejects the new claim') + old_power = E.scale(E.power(145, -1024*P.TESTED), 1-P.TESTED) + need(old_power[1] < Q(63, 64)**1000, 'Old logarithm power is insufficient') + rejected['old_invoice_at_new_kappa'] = 'Strict negative complete moment' + rejected['old_logarithm_power_1000'] = 'Insufficient complement capacity' + lo, hi = map(Q, result['raw_root_interval']) + gain = [lo-parent_interval[1], hi-parent_interval[0]] + need(gain[0] > 0, 'Strict gain over the parent raw ceiling') + fixed_ceiling = ceiling(E, targets, paid) + split_word = read(HERE/'inputs/pr5599-WORD.json.gz') + split_local = L.replay(split_word) + split_t, split_p = complete_profiles(split_local) + split_interval = [Q('.00309839352211'), Q('.00309839352212')] + need(margin(split_t, split_p, split_interval[0])[0] > 0 > + margin(split_t, split_p, split_interval[1])[1], 'Exact PR5599 crossing') + difference = {r: targets.get(r, 0)-paid.get(r, 0)-split_t.get(r, 0)+split_p.get(r, 0) + for r in targets.keys() | paid.keys() | split_t.keys() | split_p.keys()} + need({r: c for r, c in difference.items() if c} == {4: 18, 5: 18, 9: -18}, + 'Strict gain of eighteen g(4,5) over the released split component') + need(sum(split_p.values())-sum(paid.values()) == 126 and + sum(split_t.values())-sum(targets.values()) == 108, + 'Fewer paid calls and productive fields than PR5599') + parallel = {'pr': 5599, 'source_commit': '0644592d421b375c221045954fdf13932575ffa8', + 'claim': Q('.00309839'), 'claim_gain': P.KAPPA-Q('.00309839'), + 'raw_interval': split_interval, + 'raw_gain_interval': [lo-split_interval[1], hi-split_interval[0]], + 'paid_calls': sum(split_p.values()), 'productive_fields': sum(split_t.values()), + 'signed_moment_delta': {4: 18, 5: 18, 9: -18}, + 'scope': 'Pinned parallel word; exact scalar endpoint and full invoice comparison. Its native and compiler checks are not repeated.'} + receipt = P.encode({'status': 'PASS_P104_COUPLED_HELPER_KAPPA_00309980', + 'construction': steps, 'inventory': inv, 'local': local, + 'transpose': reverse, 'native': native, 'physical': physical, + 'controls': rejected, 'parent_raw_interval': parent_interval, + 'raw_gain_interval': gain, 'fixed_invoice_ceiling': fixed_ceiling, + 'parallel_comparison': parallel, + 'result': result}) + if '--write' in sys.argv: + (HERE/'RESULT.json').write_text(json.dumps(receipt, indent=2, sort_keys=True)+'\n') + else: + need(receipt == read(HERE/'RESULT.json'), 'Exact complete committed receipt') + print('PASS_P104_COUPLED_HELPER_KAPPA_00309980', flush=True) + + +if __name__ == '__main__': + main()