diff --git a/research/p104-native-input-lifting/NOTICE b/research/p104-native-input-lifting/NOTICE new file mode 100644 index 0000000000..038cff9afd --- /dev/null +++ b/research/p104-native-input-lifting/NOTICE @@ -0,0 +1,139 @@ +Native helper input lifting +Copyright 2026 Ali Romman. Apache-2.0. + +New construction, code, calculations and prose: Ali Romman with substantial +OpenAI Codex assistance. No subagents. All new checks are author checks. + +The direct source is PR6314 at 36533d4d1b4e2dd8672427461b12de3001b85810, +by DreamingOfClouds with Claude Opus 5.5 (Anthropic), via Claude Code. +It compresses the scalar word of PR6167 without a kappa change. +The four native input lifts and their complete conditional price are new here. +The basis identity is elementary linear algebra; no new general theorem +for that identity is claimed. + +The PR6167 source notice follows unchanged. Its nested source archive also +retains the earlier notices. + +Retained-operand descent: Ali Romman, with substantial OpenAI Codex assistance. +Apache-2.0. + +The exact source word and price are from DreamingOfClouds, PR6144 and PR6143, +with Claude Opus 5.5 (Anthropic), via Claude Code. They extend PR6030 and PR5907. +The source reader is adapted from that work. The gzip portability controls +retain Douglas Colkitt and Maxime Fleury credit. + +The pinned PR5827 checker and all earlier source notices are retained below. + +Unread-register path resynthesis +Copyright 2026 Ali Romman. Apache-2.0. + +New construction, code, calculations and prose: Ali Romman with substantial +OpenAI Codex assistance. No subagents. All new checks are author-side. + +Mason Hale supplied PR5811, the complete two-block composition and the exact +role92 remapping and fourth accumulation. The earlier elementary accumulation, +retained-copy and second-block work is by Ali Romman. Joel Pulikkan supplied +R22. Dugongue supplied the concurrent baseline composition proof. Their source +notice and proof are retained byte for byte under inputs/pr5811-*. + +The source closure retains flyingviper, Cinna Davis, David Arias, Gareth +Davidson, Jacob Alan Sussman, zxv, Cao Yifan, Pierre-Loic Doulcet, thu-nmrc, +Scratch-net and all native/helper/controller/compiler/geometry/analytic +predecessors. The exact PR5786 source archive and its nested notices remain. +This package does not claim any predecessor construction as new. + +Exact PR5811 vendor/accumulated/NOTICE follows. Source head: +33d7760d0a6fea6394aefd014eea68f0af02a92e + +Accumulated native updates +New work: Ali Romman with substantial OpenAI Codex assistance. Apache-2.0. +No subagents. The same assistant made the construction and the author checks. + +Concurrent scope: Discussion5125 now tests retained copies in the transposed +supplier. That route uses the same source/destination duality. This package +claims the three fixed forward-supplier groups and their complete result, +not the elementary accumulation identity or the broader transposed search. + +Exact source: PR5786 at 6b936acd68a7e0f9062037900f0fe9bc4b6fdd25. +The complete predecessor notice follows unchanged. + +Asynchronous helper hubs +New work: Ali Romman with substantial OpenAI Codex assistance. Apache-2.0. + +Retained native copies from PR5774 at 7d6ec0cdef31d0c37b7d2563e709979caa0d5eae. +All prior credit follows unchanged. + +Paid intermediate meetings and collective helper splits. +Ali Romman, with substantial OpenAI Codex assistance. Apache-2.0. +No subagents. All checks are author-side calculations. + +The complete PR5718 notice follows unchanged. + +Four paid interior public-basis changes. +Ali Romman, with substantial OpenAI Codex assistance. Apache-2.0. +No subagents. + +The following exact notice is retained from PR5660. + +New helper-subspace construction, proof and replay: +Ali Romman with substantial OpenAI Codex assistance. Apache-2.0. +The same assistant performed the construction and author-side checks. + +Retained contributions: +flyingviper: PR5605 shared relay, PR5612 delayed relay, and the PR5608/PR5613 +relay/split compositions. +Scratch-net: PR5606 prepared-helper identities and target debit. +Pierre-Loic Doulcet (hexapode): PR5565 commuting-contact construction, used as the exact source. +Ali Romman: PR5602 fixed boundary relations, PR5601 three-contact frame +change, PR5580 contact step, +and PR5544/5545 complete P104 caller. +Joel Pulikkan (GamingPuzzled): PR5569 priced helper handoff. +DreamingOfClouds: PR5561 free helper endpoints and PR5568 search tools. +thu-nmrc: PR5551 contact improvements. +Gareth Davidson (bitplane): PR2305 source composition. +David Arias: PR2152 coalesced P104 word. +Cinna Davis: PR2219 private reuse and the controller lineage. +Jacob Alan Sussman: productive mixed-target recursion. +zxv and Cao Yifan: exact intervals, compiler and native/pricing lineage. +GamingPuzzled: PR5472 successor handoff, a predecessor to the split concept. +The retained source notices preserve earlier geometry, BIT and analytic credit. + +The elementary rank-one basis identity is not claimed as a new general +linear-algebra theorem. The contribution is its explicit independent-target +use on this P104 word and the complete conditional kappa improvement. + +New contribution: Ali Romman, with substantial OpenAI Codex assistance. +The four-gate source-version rewrite composes zxv PR5643 and Ali Romman PR5644. +The A2 method retains Chris R/Clear1nsight PR3998 and ToikY PR4019 credit. +The compensated triangle method retains Cinna Davis PR4692 credit. +No subagents were used for this contribution. Apache-2.0. + +Concurrent PR5650 by zxv publishes the PR5643/PR5644 composition. PR5651 by +Ali Romman corroborates it. This package credits that released composition +and contributes the further four-gate placement. + +New work: distributed scalar updates on an unobserved public field interval, the exact witness and complete conditional price. Prepared for Ali Romman with substantial OpenAI Codex assistance. No subagents. Apache-2.0. The source archive retains all predecessor notices. + +Two-boundary main-assisted helper split and early cleanup: flyingviper with substantial +OpenAI Codex assistance, including independent AI review agents. Apache-2.0. + +Retained native-copy construction +Prepared by Ali Romman with substantial OpenAI Codex assistance. No subagents. +The paid-meeting source is PR5751 by Ali Romman with OpenAI Codex assistance. +The dimension-four span [265,194,164,75] is from Joel Pulikkan / GamingPuzzled +PR5739, with Claude Opus 5.5 assistance. The R22 block edits are not included. +The retained-copy mechanism, exact constructor, source-specific verification, +new price and proof are the contribution of this package. Apache-2.0. + +Exact PR5811 vendor/blocks/NOTICE follows. Source head: +33d7760d0a6fea6394aefd014eea68f0af02a92e + +The second block is PR5796 at4b30391e633ba0c7c674f03586ae97d443e9bc9c, by Ali Romman with substantial OpenAI Codex assistance, following Joel Pulikkan/GamingPuzzled R22. Exact notice, plan, proof and source words are retained in source/SECOND-* unchanged. + +The final immediate source is PR5786 asynchronous helper hubs by Ali Romman with substantial OpenAI Codex assistance. Its three temporal helper splits and complete completion parameters are retained and credited. The earlier PR5774-only composition is a superseded checkpoint, not a separate contribution. + +New complete retained-copy and R22 composition: Ali Romman with substantial OpenAI Codex assistance. No subagents. Apache-2.0. + +The thirteen retained native conversions and changed helper targets are by Ali Romman with OpenAI Codex assistance in PR5774. The R22 block and rank-four basis are by Joel Pulikkan (GamingPuzzled), with Claude Opus5.5 assistance, in PR5739/5756. The complete source archive and R22 notice remain unchanged. + +The construction retains Ali Romman PR5751 paid intermediate meetings, flyingviper PR5718 boundary splits, Cinna Davis's productive controller, Jacob Alan Sussman's productive recursion, zxv and Cao Yifan's interval/compiler line, and every P104/native/BIT predecessor in the source notices. The source engines are reused under exact byte bindings, not claimed as new implementations. diff --git a/research/p104-native-input-lifting/PRICING-EDITS.json b/research/p104-native-input-lifting/PRICING-EDITS.json new file mode 100644 index 0000000000..28f5322788 --- /dev/null +++ b/research/p104-native-input-lifting/PRICING-EDITS.json @@ -0,0 +1,18 @@ +[ + [ + "KAPPA, TESTED = Q('0.003128645'), Q('0.003128650')", + "KAPPA, TESTED = Q('0.003129111'), Q('0.003129116')" + ], + [ + "PREVIOUS = Q('0.003128386')", + "PREVIOUS = Q('0.003128645')" + ], + [ + "sum(paid.values()) == 66762", + "sum(paid.values()) == 66780" + ], + [ + "'kappa_decimal':'0.003128645','previous_pr6144':PREVIOUS", + "'kappa_decimal':'0.003129111','previous_pr6167':PREVIOUS" + ] +] diff --git a/research/p104-native-input-lifting/PROOF.md b/research/p104-native-input-lifting/PROOF.md new file mode 100644 index 0000000000..85499c9eb7 --- /dev/null +++ b/research/p104-native-input-lifting/PROOF.md @@ -0,0 +1,231 @@ +# Native helper input lifting + +## Claim and source + +Under the five inherited framework assumptions, the emitted supplier and +the unchanged p16/a7 caller give kappa `0.003129111`. The comparison is +PR6167's complete claim `0.003128645`. The direct word is PR6314's scalar +compression of PR6167. The source has 17,445 events. The new word has 17,452. + +Write `Z` for the zero subspace, frame ID 3, and `Omega` for the full +nine-dimensional space, frame ID 127. Frame ID 0 is not `Z`. +All frame labels below are literal IDs in the emitted word. +Let `H_r = r^(1-kappa)` and `H_0 = 0`. + +## Basis identity + +Let `A` be the source preparation map from the inputs in `Z` to their scalar +values at their first departures. A helper direction `h` has support only on +helpers that start in `Z` and finish in `Omega`. Choose a primary helper `p` +with `h_p = 1`. In each construction, the preparation never writes to `p`. +Let `a = A h`. Suppose the first destination frame for each nonzero component +of `a` contains one subspace `F`. + +Define + +```text +B = I + (h - e_p) e_p^T. +B^-1 = I - (h - e_p) e_p^T. +``` + +The square of `(h - e_p) e_p^T` is zero. Thus `B` is invertible and has +determinant one. It changes only helper inputs. The source endpoint is the +identity on these helpers, so it commutes with `B`. + +Start the existing independent input `x_p` in frame `F`. Omit its uses in the +initial preparation. This gives the response `A(x - e_p x_p)`. Deliver the +response `a x_p` at the stated later common frames. The sum is `A B x`. +Apply `B^-1` at the full output frame. This restores the source endpoint for +every input. No helper input is set to zero or replaced by a copy. + +This identity alone does not establish a legal schedule. The constructor +states every delivery, move and output correction. The replay checks the +actual source frame of every operand and all independent input columns. + +## Four directions and schedules + +The four supports of `h` are disjoint. Their basis matrices commute. +Every coefficient is dyadic. + +| Primary | New initial frame and basis | Input direction `h` | Departure response `a` | +| --- | --- | --- | --- | +| 496 | 595, `[52]` | `e496 - e639 - e643/2` | `h` | +| 649 | 597, `[82]` | `e649 - e648` | `h + e198` | +| 663 | 105, `[51]` | `e663 - e665` | `h + e179/2` | +| 508 | 1093, `[30,42,384]` | `e508 - e631 - e635/2` | `h` | + +The verifier computes each response from the full scalar chronology. +It does not accept the displayed responses without a check. +Frame 1093 is the intersection of frames 118 and 733. It has dimension three. +Each other listed common frame has dimension one. + +For primary 496, roles 639 and 643 first move from `Z` to frame 1027. +Role 496 first reaches frame 595 in the source. Replace these movements by: + +```text +at Z: 639 -= 2 * 643 + move 639 from Z to 1027 + move 643 from Z to 595 +at 595: 643 -= 496 / 2 + move 643 from 595 to 1027 +at 1027: 639 += 2 * 643 +``` + +Role 496 now starts at 595, so its old `Z -> 595` move is removed. +If roles 639 and 643 hold arbitrary values `v` and `z`, the displayed block +leaves `v - x496` and `z - x496/2`. The subtraction at `Z` removes the +carrier's old value from the later delivery. That value is not assumed zero. + +Use the same block for primary 508 with roles `(631,635)`, destination 118 +and intermediate frame 1093. Role 508 starts at 1093 and then moves to its +old first destination 733. No new owned field is used. + +For primary 649, add its value to role 198 when role 198 reaches frame 597. +Move role 648 to frame 120 before role 649 arrives there. Move 649 from 597 +to 120 and subtract it from 648. The original later move of 648 is removed. +The value of 649 is still its independent input at this subtraction. + +For primary 663, move role 179 to frame 105 before role 663 leaves it and +add half of 663 to 179. Move role 665 to frame 1051, then move 663 from 105 +to 1051 and subtract it from 665. Remove the two original later moves. +All later reads of roles 179 and 665 remain in their source order. + +At frame 127, emit the six inverse-basis additions: + +```text +639 += 496; 643 += 496/2; 648 += 649; +665 += 663; 631 += 508; 635 += 508/2. +``` + +`construct.py` guards all source event indices and all ten omitted initial +uses. It changes four initial frame declarations, appends frame 1093, +replaces twelve movement sites and appends the six output additions. +Every other event is copied. Protected contact events and frames 1091/1092 +remain fixed. + +## Exact scalar and native checks + +The unchanged checker replays all 770 arbitrary public inputs and all 29 owned +columns. Each helper has its required independent output. Each main output +has its required input and shear contribution. Every owned lifetime is +initialized and cleared at its declared frame. Peak ownership is 13. + +A separate reverse-chronology checker uses dense integer rows with binary +denominators. It checks all 799 columns and 638,401 endpoint coefficients. +The source and dense checks use different representations and directions. +Both are author checks made with credited predecessor code. + +The native checker lowers every distinct chart change to a signed Clifford +recipe. A separate exact phase representation checks its signed Pauli images +and global phase. The 2,930 distinct maps include the changed helper +normalizers. It also checks 208 free main adapters and 1,124 helper +normalizers. Its tensor argument applies at each positive tensor width. +No free native transition is inferred from scalar endpoint equality. + +Negative controls omit a carrier subtraction, reverse an injection, omit an +output correction, use the wrong input chart or intersection, or omit a +carrier move. Each fails the scalar or frame check. Native phase, caller +translation, missing price, missing target debit and damaged source controls +also fail. Explicit checks remain active with Python `-O`. + +## Paid and productive profiles + +Each of the three one-dimensional lifts has paid change `H4 - H5` and +target change `H8 - H9`. Its signed margin gain is + +```text +H5 + H8 - H4 - H9. +``` + +This is positive for `0 < kappa < 1`: strict concavity gives +`H5 - H4 > H9 - H8`. + +The three-dimensional lift has paid change +`H1 + H2 + H3 - H4 - H5` and target change `H6 - H9`. +Its signed margin gain is + +```text +H4 + H5 + H6 - H1 - H2 - H3 - H9. +``` + +The exact complete price establishes the required total gain at the tested +kappa. No claim of positivity for this last expression at every kappa is needed. + +The combined local paid change is +`H1 + H2 + H3 + 2 H4 - 4 H5`. The target change is +`H6 + 3 H8 - 4 H9`. Both rank totals decrease by six. +The general concave-order preflight is inconclusive for the complete bill: +its paid-minus-target hinge change is 18 at cap 1 and -108 at cap 5. +The claim therefore uses the exact power-moment checks below. + +| Rank | Local paid jobs | Local productive targets | +| --- | ---: | ---: | +| 1 | 2217 | 14 | +| 2 | 457 | 8 | +| 3 | 497 | 4 | +| 4 | 100 | 107 | +| 5 | 161 | 14 | +| 6 | 8 | 3 | +| 7 | 9 | 9 | +| 8 | 1 | 22 | +| 9 | 0 | 381 | + +The paid rank total is 5946. The scalar allowance is 127088. There are +770 independent public inputs, 29 owned labels and 32 owned lifetimes. + +## Complete caller and price + +The source p16/a7 caller is unchanged. Its literal Laurent replay checks all +boundary programs and all 18 forward local calls. The physical replay checks +7,488 contacts, all 53,248 central-square columns, main target phases and +every whole idle. Let `P_local` and `T_local` denote the table above. The +complete invoice is + +```text +P = 18 P_local + 1560 H1 + + 208 sum_(l in {7,8}) sum_(j=1..l) H_(8(j+1)), +T = 18 T_local + 208 H145 + + 208 sum_(l in {7,8}) sum_(j=1..l) H_(1+8(j+1)). +``` + +It has 66,780 paid calls and 13,444 productive fields. Its rank surplus is +760. The maximum paid and productive ranks are 72 and 145. Two independent +censuses agree with the emitted caller. The target debit is included in both. + +The strict raw crossing is in +`(0.00312911821812, 0.00312911821813)`. A rational derivative bound gives +uniqueness below the retained BIT cap `0.0034`. Two rational moment engines +give compatible intervals and a strict positive margin at +`TESTED = 0.003129116`. The old complete profile has a negative margin at +`KAPPA = 0.003129111`. + +The inherited strictification uses power 1024, cutoff 16, floor 17, tail +offset `1/7`, reserve `10^-12` and decay `125/128`. All completion, tail, +splitting and rounding inequalities pass with the new invoice. The compiler +gap is `1/1400000000`. The integer threshold exponent is 47005 and +`H = 65807000000000`, so its declared uniform threshold is `N = 2^H`. +The predecessor integer threshold fails the same test. No such large word +is materialized. + +The local scalar allowance plus the route and adapter allowance is below +`10^7`. The complete nonrecursive bound is 184647552, below the funded +budget `10^9`. It includes native helpers, adapters, routes, owned operations, +queries and caller boundaries. All 54 strict and four functional outer +predicates pass with the retained BIT admission. + +`pricing.py` is the exact PR6167 price program with four declared text edits: +the two new kappa constants, the previous claim, the paid call count and the +result labels. `PRICING-EDITS.json` binds these edits. The verifier rejects +any other price-program change. + +## Remaining obligations + +The five framework assumptions remain `native_all_columns`, `owned_erasure`, +`compiler`, `precision_tape` and `analytic_recovery`. Native replay verifies +this finite construction inside that framework. It does not remove those +assumptions. The rounded integer multiplier is not constructed or benchmarked. +No independent scientific review or selected-frontier change is claimed. + +The small gain does not establish that this mechanism scales to a large gain. +The published word and exact checks are the contribution. Finite discovery +screens are not lower bounds or proofs that other lifts are impossible. diff --git a/research/p104-native-input-lifting/README.md b/research/p104-native-input-lifting/README.md new file mode 100644 index 0000000000..cce28939e2 --- /dev/null +++ b/research/p104-native-input-lifting/README.md @@ -0,0 +1,94 @@ +# Four native helper input lifts + +This package gives conditional **kappa 0.003129111**, up from PR6167's +**0.003128645**. The increase is **0.000000466**, or about **0.0149%**. +This is a small gain. It does not meet the donor's request for a large gain. + +Four existing helper inputs start at later native frames. Exact scalar +corrections carry their correlated input directions to the source word. +An inverse helper basis at the output restores every independent input. +The four reduced productive targets are charged. The word still has +770 public inputs, 29 owned labels, 32 owned lifetimes and peak ownership 13. + +The exact source is the compressed PR6167 word in +[PR6314](https://github.com/CrocSwap/integer-mult-bounds/pull/6314), head +`36533d4d1b4e2dd8672427461b12de3001b85810`. PR6314 changes scalar cost but +does not change kappa. This package starts from canonical main +`626e936ce4d61f2584316914fc71baf96940c512`, priority revision 8. +[SOURCES.json](SOURCES.json) pins all five live inputs. The source reader +authenticates them before it imports any predecessor code. + +## Evidence and limits + +[PROOF.md](PROOF.md) gives the basis identity, each native edit, the complete +invoice and the inherited assumptions. [construct.py](construct.py) regenerates +all 17,452 events from the pinned source. [RESULT.json](RESULT.json) records +the exact scalar replay, a separate dense transpose, all 2,930 native maps +with absolute phases, the physical caller, two rational price engines, +compiler bounds and 54 strict plus four functional outer predicates. + +The raw crossing lies strictly in +`(0.00312911821812, 0.00312911821813)`. The previous complete profile fails +at the new claimed kappa. Thus the gain comes from the changed invoice. +It does not come from a smaller safety margin or omitted helper credit. + +All five framework assumptions remain: `native_all_columns`, `owned_erasure`, +`compiler`, `precision_tape` and `analytic_recovery`. The large uniform word +and rounded integer multiplier are not materialized. These are author checks; +they do not establish independent acceptance or practical speed. The selected +frontier remains unchanged. + +Coordination is in the +[canonical Discussion claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/5645#discussioncomment-19205459). +The latest direct checks distinguish this input-boundary change from +Discussion5600's fixed-boundary public-prefix rewrite and Discussion5593's +tree caller. Protected contact events and frames 1091/1092 remain fixed. +The overlap cache had complete remote pagination; sparse local notes and +unpublished work remain coverage limits. + +## Reproduce + +Use Python 3.12 and the standard library. From the repository root: + +```sh +python3.12 -W error -B research/p104-native-input-lifting/verify.py +python3.12 -O -W error -B research/p104-native-input-lifting/verify.py +python3.12 scripts/research_package.py --package research/p104-native-input-lifting --check-only +python3.12 scripts/research_package.py --package research/p104-native-input-lifting +``` + +The final status is `PASS_P104_NATIVE_INPUT_LIFTING_KAPPA_003129111`. +The direct verifier creates a fresh bytecode-cache namespace before it imports +package or source modules. It writes no package files unless `--write` is +specified. It checks the decompressed word bytes, so gzip header differences +do not affect the certificate. `--build-only` checks the construction, exact +scalar endpoint, ownership and scalar controls; it does not check the full claim. + +An official export needs this package and the five inputs in +[VERIFY.json](VERIFY.json). The direct verifier also works without Git or +network access. The registered runner needs Git for provenance checks. + +## Open next questions + +Can several new correlated directions share one native input lift? Start with +one exact helper group and its departure map, then emit every correction and +charge the complete bill. The present finite searches do not prove optimality. + +Can a helper output basis support an extra native exit reduction? A bounded +output-direction screen found no accepted word. A new test needs a different +explicit basis or correction, an arbitrary-input proof and full pricing. +Check the live Discussion claims before work. [TASK.json](TASK.json) gives +the first steps and missing obligations for both questions. + +## Credit + +New work: Ali Romman with substantial OpenAI Codex assistance. No subagents. +The same assistant made the construction and the author checks. Apache-2.0. + +The direct word is by DreamingOfClouds, with Claude Opus 5.5 assistance, in +PR6314. It retains Ali Romman's PR6167 and the PR6144/6143 source work. +The unchanged checker and price chain retain Cinna Davis, David Arias, +Gareth Davidson, Jacob Alan Sussman, zxv, Cao Yifan, flyingviper, +Pierre-Loic Doulcet, Joel Pulikkan, Scratch-net and all earlier source credit. +[NOTICE](NOTICE) retains the source notice. No predecessor construction or +general basis identity is claimed as new. diff --git a/research/p104-native-input-lifting/RESULT.json b/research/p104-native-input-lifting/RESULT.json new file mode 100644 index 0000000000..467f941331 --- /dev/null +++ b/research/p104-native-input-lifting/RESULT.json @@ -0,0 +1,468 @@ +{ + "base_commit": "626e936ce4d61f2584316914fc71baf96940c512", + "complete_cost": { + "compiler": { + "H": 65807000000000, + "N": "2^65807000000000", + "eta": { + "lower": "0.000000118345460840316825594594", + "upper": "0.000000118345460840316825594595" + }, + "gap": "1/1400000000", + "integer_test_exponent": 47005, + "logarithm_power": 1024, + "theta": "63/64", + "uniform_saving": "21903807/7000000000", + "word_materialized": false + }, + "full_forward_calls": 18, + "gain": "233/500000000", + "kappa": "3129111/1000000000", + "kappa_decimal": "0.003129111", + "margin_at_previous": { + "lower": "0.114166232020664834808227839008", + "upper": "0.114166232020664834808227839009" + }, + "negative_controls": { + "old_BIT": "Rejected by outer inequalities", + "old_cutoff": "Rejected by completion-tail ratio greater than one", + "source_completion": "Rejected at cutoff17, floor18 and decay39/40", + "source_offset": "Rejected at cutoff16 with tail offset1/5" + }, + "nonrecursive": { + "fixed_scalar_growth_bound": "At most 2^(16*26000) before native factors; a declared constant, not an attained norm.", + "local_paid_rank_mass": 5946, + "local_routes": 5326000, + "local_scalar": 127088, + "peak_owned_fields": 13, + "raw_budget": 1000000000, + "raw_scalar_upper": 184647552, + "tensor_native_growth_bound": "Each rank-r Gaussian has row l1 norm at most 2^(rf); use local_paid_rank_mass for the whole word." + }, + "ordinary_BIT": { + "admitted": "17/5000", + "after_cover": "69/20000", + "atom": "1/250", + "before_cover": "3459/1000000", + "ordinary_saving": "8590884599/2500000000000", + "prime_rule": "odd q > 2^26*N^5 avoiding all fixed denominators and rank witnesses" + }, + "outer": { + "functional_checks": { + "actual_new_BIT_stock_sublinear": "348599999253/350000000000", + "fixed_halo_explicit_metadata_branch": "26950000001/350000000", + "new_BIT_row_stock_sublinear_in_active_group": "1395799997009/1400000000000", + "new_semantic_group_guard": "3/1400000000" + }, + "margins": { + "boundary_algebraic_matrix": "1916582236131013/612500000000000000", + "fused_gaussian": "1916582233393039/612500000000000000", + "global_coordinate_router": "21903797/7000000000", + "group_bit_router": "30665322734288609/9800000000000000000", + "group_scans": "699999999/700000000", + "main_transform": "1916581798631013/612500000000000000", + "microbox_face_corrections": "26950000001/350000000", + "polynomial_products": "1399999999/1400000000", + "sparse_union_movement": "250744707236131013/612500000000000000" + }, + "parameters": { + "a": "21903797/7000000000", + "b": "10951901/3500000000", + "beta": "1399999997/1400000000", + "bit_saving": "17/5000", + "cap_xi": "556994706798631013/612500000000000000", + "complex_uniform_saving": "21903807/7000000000", + "d": "1/1400000000", + "epsilon": "1399999999/1400000000", + "kappa": "3129111/1000000000", + "lambda_": "1993741773/2000000000", + "lambda_prime": "436131013/437500000", + "layout": "1/1400000000", + "q": "1368987/437500000", + "r0": "1/14000000000", + "stop": "1/1400000000", + "tested_saving": "782279/250000000" + }, + "strict_checks": { + "actual_bit_above_effective": "1896203/7000000000", + "actual_logarithmic_gamma_guard": "1/1400000000", + "actual_logarithmic_group_guard": "55505293857618987/306250000000000000", + "alpha_logarithm_absorption": "1/14000000000", + "boundary_algebraic_matrix_above_kappa": "1748631013/612500000000000000", + "cap_above_band": "250744706798631013/612500000000000000", + "cap_below_cell": "55505292763868987/612500000000000000", + "cap_below_phase_cell_power": "668005293201368987/612500000000000000", + "complex_above_effective": "1/1400000000", + "complex_below_one_over_32": "98423099/3500000000", + "complex_endpoint": "1/700000000", + "epsilon_below_one": "1/1400000000", + "epsilon_positive": "1399999999/1400000000", + "fine_prime_halo_umbrella": "7/2", + "fused_gaussian_above_kappa": "1745893039/612500000000000000", + "gaussian_above_main": "217381013/306250000000000000", + "global_coordinate_router_above_kappa": "1/350000000", + "global_gamma_power_slack": "9/14000000000", + "group_below_dimension": "1/700000000", + "group_bit_router_above_kappa": "34934288609/9800000000000000000", + "group_gauge_power_slack": "55505293835743987/306250000000000000", + "group_key_fits_record": "1/700000000", + "group_positive": "1399999997/1400000000", + "group_scans_above_kappa": "6978096213/7000000000", + "halo_covers_generic_inverse_radius": "5", + "improvement_over_user_baseline": "699070290400418148631/500000000000000000000000", + "lambda_above_internal": "1/2800000000", + "lambda_above_sigma": "3/2800000000", + "lambda_above_tau": "1/2800000000", + "lambda_prime_above_lambda": "1/2800000000", + "lambda_prime_above_leaf": "6989048099/4900000000000000000", + "leaf_saving_above_effective": "3489048099/4900000000000000000", + "main_transform_above_kappa": "1311131013/612500000000000000", + "membership_arithmetic_fits_record": "1/1400000000", + "microbox_face_corrections_above_kappa": "538978096243/7000000000", + "microbox_halo_volume": "110600000003/1400000000", + "new_complex_uniform_saving_above_b": "1/1400000000", + "new_semantic_guard_with_C1_one": "1/1400000000", + "polynomial_products_above_kappa": "3489048109/3500000000", + "positive_layout_slack": "1/1400000000", + "q_below_effective": "1/1400000000", + "q_below_internal": "1/1400000000", + "q_below_leaf": "6989048099/4900000000000000000", + "q_positive": "1368987/437500000", + "short_record_fallback": "3489048099/3500000000", + "source_axis_superpolynomial": "1/1400000000", + "sparse_union_movement_above_kappa": "248828126748631013/612500000000000000", + "stop_below_one": "1399999999/1400000000", + "stop_positive": "1/1400000000", + "strassen_integer_power_gap": "1951441519231", + "support_router_span": "3/1400000000", + "theta_positive_polynomial_power": "2", + "union_header_fits_record": "3/1400000000", + "union_tag_work_per_visit_fits_record": "3/1400000000" + } + }, + "paid": { + "1": 41466, + "16": 416, + "2": 8226, + "24": 416, + "3": 8946, + "32": 416, + "4": 1800, + "40": 416, + "48": 416, + "5": 2898, + "56": 416, + "6": 144, + "64": 416, + "7": 162, + "72": 208, + "8": 18 + }, + "paid_calls": 66780, + "previous_pr6167": "625729/200000000", + "productive_fields": 13444, + "query_shears": 15, + "rank_mass_surplus": 760, + "raw_ceiling": { + "derivative_upper": "-183709566445935704978840182941609952096373888509850921830221383/784637716923335095479473677900958302012794430558004314112", + "interval": [ + "0", + "17/5000" + ] + }, + "raw_headroom": [ + "180453/25000000000000", + "721813/100000000000000" + ], + "raw_root_interval": [ + "78227955453/25000000000000", + "312911821813/100000000000000" + ], + "relative_gain_percent": "9320/625729", + "strictification": { + "alpha": { + "lower": "0.999999997753741211225010509708", + "upper": "0.999999997753741211225010509709" + }, + "cutoff": 16, + "delta": { + "lower": "0.951057530932807200661841013951", + "upper": "0.951057530932807200661841013952" + }, + "floor": 17, + "gamma": { + "lower": "0.975667744092639322686002893166", + "upper": "0.975667744092639322686002893167" + }, + "normalized_paid_upper": "1048576000976562501/1048576001073741824", + "power": 1024, + "reserve": "1/1000000000000", + "tail_block": 128, + "tail_decay": "125/128", + "tail_offset": "1/7", + "tested": "782279/250000000" + }, + "targets": { + "1": 252, + "145": 208, + "17": 416, + "2": 144, + "25": 416, + "3": 72, + "33": 416, + "4": 1926, + "41": 416, + "49": 416, + "5": 252, + "57": 416, + "6": 54, + "65": 416, + "7": 162, + "73": 208, + "8": 396, + "9": 6858 + }, + "whole_idle_jobs": 3120 + }, + "controls": { + "damaged_research/p104-frontier-compression-2/WORD.json.gz": "Exact source SHA256: research/p104-frontier-compression-2/WORD.json.gz", + "damaged_research/p104-retained-operand-descent/SOURCES.json": "Exact source SHA256: research/p104-retained-operand-descent/SOURCES.json", + "damaged_research/p104-retained-operand-descent/inputs/pr5827-source.tar": "Exact source SHA256: research/p104-retained-operand-descent/inputs/pr5827-source.tar", + "damaged_research/p104-retained-operand-descent/pricing.py": "Exact source SHA256: research/p104-retained-operand-descent/pricing.py", + "damaged_research/p104-retained-operand-descent/sources.py": "Exact source SHA256: research/p104-retained-operand-descent/sources.py", + "missing_carrier_move": "Scalar destination and coefficient", + "missing_central_translation": "Rejected by the complete Laurent endpoint", + "missing_first_carrier_subtraction": "All public and owned rows", + "missing_output_basis": "All public and owned rows", + "missing_second_carrier_subtraction": "All public and owned rows", + "missing_target_debit": "Every productive helper has a native target", + "old_input_chart": "Common scalar chart", + "unpaid_carrier_move": "Complete field and call counts", + "wrong_649_injection": "All public and owned rows", + "wrong_663_injection": "All public and owned rows", + "wrong_intersection": "Nested chronological transport" + }, + "directions": [ + { + "basis": [ + 52 + ], + "departure_response": { + "496": "1", + "639": "-1", + "643": "-1/2" + }, + "frame": 595, + "input_direction": { + "496": "1", + "639": "-1", + "643": "-1/2" + }, + "primary": 496 + }, + { + "basis": [ + 82 + ], + "departure_response": { + "198": "1", + "648": "-1", + "649": "1" + }, + "frame": 597, + "input_direction": { + "648": "-1", + "649": "1" + }, + "primary": 649 + }, + { + "basis": [ + 51 + ], + "departure_response": { + "179": "1/2", + "663": "1", + "665": "-1" + }, + "frame": 105, + "input_direction": { + "663": "1", + "665": "-1" + }, + "primary": 663 + }, + { + "basis": [ + 30, + 42, + 384 + ], + "departure_response": { + "508": "1", + "631": "-1", + "635": "-1/2" + }, + "frame": 1093, + "input_direction": { + "508": "1", + "631": "-1", + "635": "-1/2" + }, + "primary": 508 + } + ], + "events": 17452, + "limits": [ + "All five inherited framework assumptions remain.", + "The uniform word and rounded multiplier are not materialized.", + "Author checks do not establish independent acceptance.", + "The selected frontier is unchanged." + ], + "local": { + "endpoint_coefficients": 638401, + "helpers": { + "1": 14, + "2": 8, + "3": 4, + "4": 107, + "5": 14, + "6": 3, + "7": 9, + "8": 22, + "9": 381 + }, + "owned_fields": 29, + "owned_lifetimes": 32, + "paid": { + "1": 2217, + "2": 457, + "3": 497, + "4": 100, + "5": 161, + "6": 8, + "7": 9, + "8": 1 + }, + "paid_rank_mass": 5946, + "peak_owned_fields": 13, + "public_inputs": 770, + "real_scalar_allowance": 127088 + }, + "native": { + "distinct_maps": 2930, + "helper_normalizers": 1124, + "helpers": { + "1": 14, + "2": 8, + "3": 4, + "4": 107, + "5": 14, + "6": 3, + "7": 9, + "8": 22, + "9": 381 + }, + "main_adapters": 208, + "proof": "Every signed Pauli image and exact global phase; frame induction at every positive tensor width", + "recipe_payload_sha256": "18631697cf96cfcd625fd0210939bc40f095657324730955d15719b9c7385513", + "wrong_phase_rejected": true + }, + "paid_delta": { + "1": 1, + "2": 1, + "3": 1, + "4": 2, + "5": -4 + }, + "physical_caller": { + "central_square_columns": 53248, + "full_calls": 18, + "main_targets": { + "145": 208, + "17": 416, + "25": 416, + "33": 416, + "41": 416, + "49": 416, + "57": 416, + "65": 416, + "73": 208 + }, + "new_paid_jobs": 0, + "physical_contacts": 7488, + "ports": 104, + "route_payload_sha256": "7f4f0ca768ffbc4f93dcff575592c4c67411f46b4289e45b73f715a2ad47b142", + "tensor_rule": "Factorwise native maps; scalar signs stay outside the tensor power.", + "whole_idle_jobs": { + "16": 416, + "24": 416, + "32": 416, + "40": 416, + "48": 416, + "56": 416, + "64": 416, + "72": 208 + }, + "wrapper_sites": [ + 1, + 3, + 5, + 7, + 9, + 11, + 13, + 15, + 17, + 19, + 21, + 23, + 25, + 27, + 29, + 31 + ] + }, + "separate_columns": { + "arithmetic": "Dense integer rows with binary denominators; reverse chronology", + "coefficients": 638401, + "columns": 799 + }, + "source_local": { + "endpoint_coefficients": 638401, + "helpers": { + "1": 14, + "2": 8, + "3": 4, + "4": 107, + "5": 14, + "6": 2, + "7": 9, + "8": 19, + "9": 385 + }, + "owned_fields": 29, + "owned_lifetimes": 32, + "paid": { + "1": 2216, + "2": 456, + "3": 496, + "4": 98, + "5": 165, + "6": 8, + "7": 9, + "8": 1 + }, + "paid_rank_mass": 5952, + "peak_owned_fields": 13, + "public_inputs": 770, + "real_scalar_allowance": 127042 + }, + "source_margin_upper_at_new_claim": "-21724354416852642076420555890660965661122037090691207971/196159429230833773869868419475239575503198607639501078528", + "status": "PASS_P104_NATIVE_INPUT_LIFTING_KAPPA_003129111", + "target_delta": { + "6": 1, + "8": 3, + "9": -4 + } +} diff --git a/research/p104-native-input-lifting/SOURCES.json b/research/p104-native-input-lifting/SOURCES.json new file mode 100644 index 0000000000..bc7876a86e --- /dev/null +++ b/research/p104-native-input-lifting/SOURCES.json @@ -0,0 +1,48 @@ +{ + "schema_version": 1, + "base_commit": "626e936ce4d61f2584316914fc71baf96940c512", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a", + "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/p104-frontier-compression-2/WORD.json.gz", + "usage": "input", + "git_blob": "cb3aed1d5604eb290f18759b37becaad428ac27a", + "sha256": "889f0f5d193d993dabee1e20dcfbcf63f9d88cfe5bd6973d564276c744d1e190" + }, + { + "path": "research/p104-retained-operand-descent/SOURCES.json", + "usage": "input", + "git_blob": "0c574b6026a7239aac7365c433d3760928748edb", + "sha256": "7c7b6fac64005eb8932283a902069d672d98c52bda2b63cc7eaa4a2cac13ce8f" + }, + { + "path": "research/p104-retained-operand-descent/inputs/pr5827-source.tar", + "usage": "input", + "git_blob": "1e10936044959f81a4c5fcd5bdb7b9e4c060ec8e", + "sha256": "7af5908a4d83e83e28f59523fd7494841f669b7295311cfdbc3027fa65c5826d" + }, + { + "path": "research/p104-retained-operand-descent/pricing.py", + "usage": "input", + "git_blob": "cd8220ca7a393f03341f08a93b9d1287f0bb3689", + "sha256": "bba1611b05b6cc35279aa1667dcc62ce0e7f27f0ba21f20eb68244fa772e0ae7" + }, + { + "path": "research/p104-retained-operand-descent/sources.py", + "usage": "input", + "git_blob": "bef6542243a082755a881dff42097434e6370609", + "sha256": "a62fefda1709614157ba440d38c164c366a8b3322ab8f866b6b4bd47b9d83dbc" + } + ] +} diff --git a/research/p104-native-input-lifting/TASK.json b/research/p104-native-input-lifting/TASK.json new file mode 100644 index 0000000000..608ca892aa --- /dev/null +++ b/research/p104-native-input-lifting/TASK.json @@ -0,0 +1,123 @@ +{ + "schema_version": 1, + "task_id": "p104-side-correction", + "priority_revision": 8, + "base_commit": "626e936ce4d61f2584316914fc71baf96940c512", + "original_card": { + "id": "p104-side-correction", + "question": "Can joint helper bases and a legal causal split improve the complete P104 productive/paid invoice?", + "starting_points": [ + "docs/research/current-priorities.md", + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "research/p104-helper-subspace-splits/README.md", + "research/dyadic-helper-channel-capacity/README.md" + ], + "methods": [ + "Construct and independently check one source-bound instance of the stated first experiment.", + "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change." + ], + "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_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.", + "scope": "Source-bound orientation only, not a supplier replay or theorem proof." + }, + "first_experiment": "Start with the selected #5599 emitted word and review pending #5718 distinct input/output bases plus #5717/#5719 coverage before claiming work. Pick one uncovered source word, helper group and cut region. Prove the arbitrary-input relation and legal entry/exit corrections, then compare full target and paid profiles. Reject if completion, owned lifetimes or consumer costs repay the gain. A static pairing rank alone is not a physical split.", + "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.", + "allowed_variations": [ + "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes." + ], + "scope_change_triggers": [ + "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.", + "Treating an archived proposal or local numerical pass as complete supplier admission." + ], + "overlap_terms": [ + "P104", + "helper basis", + "helper split", + "5718", + "dyadic capacity" + ], + "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": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.", + "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.", + "status": "reviewed", + "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137", + "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Lift four existing independent helper inputs to native subspaces on the exact PR6314 word; emit the inverse helper basis and charge the reduced targets and complete caller.", + "scope_change_reason": "The retained-operand extension found a distinct boundary mechanism. This preserves all independent inputs but changes four initial native charts. The live claim records the change and excludes concurrent fixed-boundary stop removal and tree callers.", + "bottleneck_link": "The complete signed target and paid invoice improves. Each changed helper target is debited before strictification and compiler checks.", + "budget_minutes": 240, + "stop_rule": "Reject a candidate if any arbitrary-input, native, ownership or complete-cost check fails. Submit one source-bound positive word with all required checks.", + "outcome": "completed", + "evidence": "PROOF.md, WORD.json.gz, RESULT.json and the registered verifier", + "author": "Ali Romman", + "ai_assistance": "Substantial OpenAI Codex assistance. No subagents. The same assistant made the construction and the author checks.", + "open_questions": [ + { + "question": "Can a larger set of correlated helper directions share one native input lift?", + "why_it_matters": "The four present directions give a small improvement. More directions could change the complete invoice further.", + "first_step": "Pin this word, check the live Discussion scopes, and compute exact departure responses for one new helper group. Then construct all scalar corrections and price every target debit.", + "blocked_by": "A complete arbitrary-input word and its full native and caller checks are required." + }, + { + "question": "Can a helper output basis support an additional native exit reduction?", + "why_it_matters": "The source has a separate final scalar map. Its useful directions need not equal the input directions.", + "first_step": "Check the current Discussion5645 claim and test one exact output direction with explicit initial restoration and reduced productive targets.", + "blocked_by": "The bounded output-direction screen found no accepted word. A broader exact exit construction and complete price remain open." + } + ] +} diff --git a/research/p104-native-input-lifting/VERIFY.json b/research/p104-native-input-lifting/VERIFY.json new file mode 100644 index 0000000000..24021f331c --- /dev/null +++ b/research/p104-native-input-lifting/VERIFY.json @@ -0,0 +1,38 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/p104-frontier-compression-2/WORD.json.gz", + "research/p104-retained-operand-descent/SOURCES.json", + "research/p104-retained-operand-descent/inputs/pr5827-source.tar", + "research/p104-retained-operand-descent/pricing.py", + "research/p104-retained-operand-descent/sources.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 600, + "checks": "Exact regeneration and helper bases; all 799 columns; ownership; every native map and phase; full caller; two interval engines; complete costs; compiler; 58 outer predicates; semantic and source controls." + }, + { + "argv": [ + "{python}", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 600, + "checks": "Repeat the full check with Python assertions disabled." + } + ] +} diff --git a/research/p104-native-input-lifting/WORD.json.gz b/research/p104-native-input-lifting/WORD.json.gz new file mode 100644 index 0000000000..f21f7ac451 Binary files /dev/null and b/research/p104-native-input-lifting/WORD.json.gz differ diff --git a/research/p104-native-input-lifting/construct.py b/research/p104-native-input-lifting/construct.py new file mode 100644 index 0000000000..1a8a1e9881 --- /dev/null +++ b/research/p104-native-input-lifting/construct.py @@ -0,0 +1,91 @@ +"""Lift four existing helper inputs to native frames. + +Prepared by Ali Romman with substantial OpenAI Codex assistance. Apache-2.0. +The source word is PR6314 by DreamingOfClouds with Claude Opus 5.5 assistance. +""" +from copy import deepcopy +import gzip +import json + +from support import HERE, WORD, inputs, need + +ENTRIES = {496: 595, 649: 597, 663: 105, 508: 1093} +OMIT = { + 85: ['ADD', 113, 649, '-1/2', 3], + 223: ['ADD', 194, 649, '-1/2', 3], + 228: ['ADD', 187, 649, '-1/2', 3], + 239: ['ADD', 205, 649, '-1/2', 3], + 591: ['ADD', 138, 663, '1/2', 3], + 595: ['ADD', 120, 663, '-1/2', 3], + 687: ['ADD', 178, 663, '-1/2', 3], + 793: ['ADD', 192, 663, '1/2', 3], + 1090: ['ADD', 157, 508, '1/2', 3], + 4368: ['ADD', 220, 496, '1/2', 3], +} +EDITS = { + 8289: (['MOVE', 639, 3, 1027, False], + [['ADD', 639, 643, '-2', 3], ['MOVE', 639, 3, 1027, False]]), + 8315: (['MOVE', 643, 3, 1027, False], + [['MOVE', 643, 3, 595, False], ['ADD', 643, 496, '-1/2', 595], + ['MOVE', 643, 595, 1027, False], ['ADD', 639, 643, '2', 1027]]), + 9029: (['MOVE', 496, 3, 595, False], []), + 9105: (['MOVE', 198, 3, 597, False], + [['MOVE', 198, 3, 597, False], ['ADD', 198, 649, '1', 597]]), + 9210: (['MOVE', 663, 3, 1051, False], + [['MOVE', 179, 3, 105, False], ['ADD', 179, 663, '1/2', 105], + ['MOVE', 665, 3, 1051, False], ['MOVE', 663, 105, 1051, False], + ['ADD', 665, 663, '-1', 1051]]), + 9212: (['MOVE', 665, 3, 1051, False], []), + 9227: (['MOVE', 631, 3, 118, False], + [['ADD', 631, 635, '-2', 3], ['MOVE', 631, 3, 118, False]]), + 9229: (['MOVE', 649, 3, 120, False], + [['MOVE', 648, 3, 120, False], ['MOVE', 649, 597, 120, False], + ['ADD', 648, 649, '-1', 120]]), + 9245: (['MOVE', 635, 3, 118, False], + [['MOVE', 635, 3, 1093, False], ['ADD', 635, 508, '-1/2', 1093], + ['MOVE', 635, 1093, 118, False], ['ADD', 631, 635, '2', 118]]), + 9284: (['MOVE', 648, 3, 120, False], []), + 9304: (['MOVE', 179, 3, 105, False], []), + 9867: (['MOVE', 508, 3, 733, False], [['MOVE', 508, 1093, 733, False]]), +} +RESTORE = [['ADD', 639, 496, '1', 127], ['ADD', 643, 496, '1/2', 127], + ['ADD', 648, 649, '1', 127], ['ADD', 665, 663, '1', 127], + ['ADD', 631, 508, '1', 127], ['ADD', 635, 508, '1/2', 127]] + + +def construct(source): + need(len(source['frames']) == 1093 and len(source['program']) == 17445, + 'Exact source dimensions') + word = deepcopy(source) + word['frames'].append([30, 42, 384]) + for role, frame in ENTRIES.items(): + need(source['initial'][role] == 3 and source['final'][role] == 127, + 'Full helper target before the lift') + word['initial'][role] = frame + initial_uses = {i: e for i, e in enumerate(source['program']) + if e[0] in ('ADD', 'COPY', 'SCALE') and e[-1] == 3 and + (e[1] in ENTRIES or e[0] in ('ADD', 'COPY') and e[2] in ENTRIES)} + need(initial_uses == OMIT, 'Every use of a lifted input in the initial chart') + program = [] + for i, event in enumerate(source['program']): + if i in OMIT: + need(event == OMIT[i], 'Exact omitted preparation event') + elif i in EDITS: + before, after = EDITS[i] + need(event == before, 'Exact native edit at source event ' + str(i)) + program.extend(deepcopy(after)) + else: + program.append(deepcopy(event)) + program.extend(deepcopy(RESTORE)) + word['program'] = program + need(len(program) == 17452, 'Exact event count') + return word + + +def payload(word): + return (json.dumps(word, sort_keys=True, separators=(',', ':')) + '\n').encode() + + +if __name__ == '__main__': + source = json.loads(gzip.decompress(inputs()[WORD])) + (HERE / 'WORD.json.gz').write_bytes(gzip.compress(payload(construct(source)), mtime=0)) diff --git a/research/p104-native-input-lifting/pricing.py b/research/p104-native-input-lifting/pricing.py new file mode 100644 index 0000000000..af470932c6 --- /dev/null +++ b/research/p104-native-input-lifting/pricing.py @@ -0,0 +1,184 @@ +"""Complete mixed-target price, compiler and outer transfer. + +The interval and compiler bounds follow zxv and Cao Yifan. The productive +recursion is by Jacob Alan Sussman. The controller is by Cinna Davis. +Adapted from Ali Romman's PR5544/5545 for the two coupled contact changes. +Successor choices were prepared for thu-nmrc with OpenAI Codex assistance. +Helper-subspace targets were added by Ali Romman with OpenAI Codex assistance. +The source commuting-contact construction is by Pierre-Loic Doulcet (hexapode) in PR5565. +The source coupled-frame change is by Ali Romman with OpenAI Codex in PR5601. +Five fixed boundary relations are from Ali Romman's PR5602. +The shared and delayed relays are from flyingviper's PR5605 and PR5612. The preparation is from +Scratch-net's PR5606. Their costs and target debit are included. +Ali Romman's complete caller/price proof and all predecessor credit are retained. +The paid A2 change is from zxv PR5643. The three helper relations are from +Ali Romman PR5644. The four-gate change is by Ali Romman with Codex assistance. +The four interior basis changes are by Ali Romman with Codex assistance. +Paid intermediate meetings: Ali Romman with substantial OpenAI Codex assistance. +Apache-2.0. +""" +from collections import Counter +from fractions import Fraction as Q +import local as L + +KAPPA, TESTED = Q('0.003129111'), Q('0.003129116') +PREVIOUS = Q('0.003128645') + + +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()) == 13444 and sum(paid.values()) == 66780, 'Complete field and call counts') + L.need(sum(r*n for r,n in targets.items())-sum(r*n for r,n in paid.items()) == 760, 'Complete rank surplus') + return targets,paid,counts + + +def run(local,native,word,physical): + T,P,counts = assemble(local,native,word,physical) + E = L.load(L.ROOT/'research/higher-moment-strictification/verify.py','p104_productive_intervals') + other = L.load(L.ROOT/'research/kappa-rebuild/architecture/mixed_target_probe.py','p104_productive_second_intervals') + def margin(k): + a,b = E.moment(T,1-k), E.moment(P,1-k) + return a[0]-b[1],a[1]-b[0] + lo,hi,grid = 0,10**12,10**14 + while hi-lo > 1: + m=(lo+hi)//2 + if margin(Q(m,grid))[0] > 0: + lo=m + else: + hi=m + lower,upper = Q(lo,grid),Q(hi,grid) + signed = Counter(T) + signed.subtract(P) + cap = Q('.0034') + derivative_upper = Q(0) + for rank, count in signed.items(): + logarithm = E.log_bounds(rank) + low = E.mul(E.power(rank, 1-cap), logarithm)[0] + high = rank*logarithm[1] + derivative_upper -= count*(low if count >= 0 else high) + L.need(derivative_upper < 0, 'Unique raw crossing below the retained BIT cap') + L.need(margin(lower)[0] > 0 and margin(upper)[1] < 0, 'Strict rational crossing enclosure') + L.need(PREVIOUS < KAPPA < TESTED < lower and margin(PREVIOUS)[0] > 0, 'Changed complete bill improves the source claim') + t,u,v,c,b = 1-TESTED,Q(1,7),1024,16,17 + 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**12),Q(125,128) + 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') + old_completion = E.divide((Q(sum(T.values())*18),)*2,E.mul(E.power(17,TESTED),target)) + L.need(old_completion[0] > Q(39,40), 'PR5718 completion-tail bound fails with the new target count') + old_offset = E.divide(E.moment(P,t+Q(1,5)),E.mul(E.power(16,Q(1,5)),target)) + L.need(old_offset[0] > decay, 'The old tail offset fails at the new cutoff') + 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':'0.003129111','previous_pr6167':PREVIOUS,'gain':KAPPA-PREVIOUS, + 'relative_gain_percent':100*(KAPPA/PREVIOUS-1),'raw_root_interval':[lower,upper], + 'raw_headroom':[lower-KAPPA,upper-KAPPA], + 'raw_ceiling':{'interval':[Q(0),cap],'derivative_upper':derivative_upper},'margin_at_previous':E.display(margin(PREVIOUS)), + 'targets':T,'paid':P,'productive_fields':sum(T.values()),'paid_calls':sum(P.values()), + 'rank_mass_surplus':760,'full_forward_calls':18,'query_shears':15,'whole_idle_jobs':3120, + 'strictification':{'tested':TESTED,'power':v,'cutoff':c,'floor':b,'tail_offset':u,'reserve':reserve,'tail_decay':decay,'tail_block':128, + 'alpha':E.display(alpha),'gamma':E.display(gamma),'delta':E.display(delta),'normalized_paid_upper':normalized}, + 'compiler':{'theta':theta,'logarithm_power':power,'eta':E.display(eta),'gap':gap,'H':H,'N':'2^'+str(H), + 'integer_test_exponent':right,'uniform_saving':params['complex_uniform_saving'],'word_materialized':False}, + 'nonrecursive':{'local_scalar':local['real_scalar_allowance'],'local_routes':local_routes, + 'raw_scalar_upper':raw,'raw_budget':10**9,'peak_owned_fields':local['peak_owned_fields'], + 'fixed_scalar_growth_bound':'At most 2^(16*26000) before native factors; a declared constant, not an attained norm.', + 'local_paid_rank_mass':local['paid_rank_mass'], + 'tensor_native_growth_bound':'Each rank-r Gaussian has row l1 norm at most 2^(rf); use local_paid_rank_mass for the whole word.'}, + 'ordinary_BIT':bit,'outer':outer, + 'negative_controls':{'source_completion':'Rejected at cutoff17, floor18 and decay39/40', + 'source_offset':'Rejected at cutoff16 with tail offset1/5', + 'old_cutoff':'Rejected by completion-tail ratio greater than one','old_BIT':'Rejected by outer inequalities'}}) diff --git a/research/p104-native-input-lifting/support.py b/research/p104-native-input-lifting/support.py new file mode 100644 index 0000000000..b528d2a451 --- /dev/null +++ b/research/p104-native-input-lifting/support.py @@ -0,0 +1,70 @@ +"""Read the pinned word and open the unchanged checker chain. + +Prepared by Ali Romman with substantial OpenAI Codex assistance. Apache-2.0. +The archive reader and checker chain retain the credits in NOTICE. +""" +from contextlib import ExitStack, contextmanager +from hashlib import sha1, sha256 +from pathlib import Path +import gzip +import importlib.util +import json +import sys + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +SOURCE = 'research/p104-retained-operand-descent/' +WORD = 'research/p104-frontier-compression-2/WORD.json.gz' +INPUTS = {WORD, *(SOURCE + name for name in + ('sources.py', 'SOURCES.json', 'inputs/pr5827-source.tar', 'pricing.py'))} + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +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) + module = importlib.util.module_from_spec(spec) + sys.modules[name] = module + spec.loader.exec_module(module) + return module + + +def authenticate(raw, pin): + need(sha256(raw).hexdigest() == pin['sha256'], 'Exact source SHA256: ' + pin['path']) + blob = b'blob ' + str(len(raw)).encode() + b'\0' + raw + need(sha1(blob).hexdigest() == pin['git_blob'], 'Exact source Git blob: ' + pin['path']) + + +def inputs(): + pins = [pin for pin in read(HERE / 'SOURCES.json')['files'] if pin['usage'] == 'input'] + need(len(pins) == len(INPUTS) and {p['path'] for p in pins} == INPUTS, + 'Complete live source inventory') + out = {} + for pin in pins: + raw = (ROOT / pin['path']).read_bytes() + authenticate(raw, pin) + out[pin['path']] = raw + return out + + +@contextmanager +def checkers(): + inputs() + source = load(ROOT / SOURCE / 'sources.py', 'lift_source_reader') + with ExitStack() as contexts: + parent = contexts.enter_context(source.sources()) + cursor = contexts.enter_context(load(parent / 'sources.py', 'lift_source_top').sources()) + for depth in range(7): + reader = load(cursor / 'sources.py', 'lift_source_' + str(depth)) + cursor, root = contexts.enter_context(reader.sources()) + local = load(parent / 'local.py', 'local') + local.ROOT = root + yield local, root diff --git a/research/p104-native-input-lifting/verify.py b/research/p104-native-input-lifting/verify.py new file mode 100644 index 0000000000..70b3beae8f --- /dev/null +++ b/research/p104-native-input-lifting/verify.py @@ -0,0 +1,209 @@ +"""Check the four lifts, native maps, complete price and compiler. + +Prepared by Ali Romman with substantial OpenAI Codex assistance. Apache-2.0. +The unchanged proof engines and source word retain the credits in NOTICE. +""" +from collections import Counter +from copy import deepcopy +from fractions import Fraction as Q +from pathlib import Path +import gzip +import json +import sys +import tempfile + +sys.dont_write_bytecode = True +HERE = Path(__file__).resolve().parent +STATUS = 'PASS_P104_NATIVE_INPUT_LIFTING_KAPPA_003129111' +PROTECTED = {41, 42, 65, 106, 240, 400, 401, 403, 405, 410, 741, + 57, 81, 92, 224, 225, 227, 229, 234, 742} +DIRECTIONS = [ + (496, {496: '1', 639: '-1', 643: '-1/2'}, + {496: '1', 639: '-1', 643: '-1/2'}), + (649, {649: '1', 648: '-1'}, {649: '1', 648: '-1', 198: '1'}), + (663, {663: '1', 665: '-1'}, {663: '1', 665: '-1', 179: '1/2'}), + (508, {508: '1', 631: '-1', 635: '-1/2'}, + {508: '1', 631: '-1', 635: '-1/2'}), +] + + +def reject(action): + try: + action() + except ValueError as error: + return str(error) + raise ValueError('Invalid control accepted') + + +def delta(after, before): + out = Counter(after) + out.subtract(before) + return {rank: count for rank, count in out.items() if count} + + +def protected_events(word): + return [e for e in word['program'] if e[1] in PROTECTED or + (e[0] in ('ADD', 'COPY') and e[2] in PROTECTED)] + + +def preparation(L, source, word): + records = [] + occupied = set() + main = set(source['live']) | {r + 112 for r in source['live']} + for primary, h, a in DIRECTIONS: + h, a = ({r: Q(q) for r, q in row.items()} for row in (h, a)) + L.need(h[primary] == a[primary] == 1 and not occupied.intersection(h), + 'Independent unit input directions') + occupied.update(h) + L.need(all(r not in main | PROTECTED and source['initial'][r] == 3 and + source['final'][r] == 127 for r in h), 'Only full helper inputs in each basis') + values = [h.get(r, Q(0)) for r in range(source['public'] + source['owned_fields'])] + departures, first = {}, {} + for event in source['program']: + op, r = event[:2] + if op == 'MOVE' and event[2] == 3 and not event[4]: + L.need(r not in first, 'One departure from the initial chart') + first[r] = event[3] + if values[r]: + departures[r] = values[r] + elif op in ('INIT', 'CLEAR'): + values[r] = Q(0) + elif op == 'SCALE': + values[r] *= Q(event[2]) + elif op == 'COPY': + values[r] = Q(event[3]) * values[event[2]] + elif op == 'ADD': + values[r] += Q(event[3]) * values[event[2]] + L.need(departures == a, 'Exact initial preparation response') + frame = word['initial'][primary] + common = L.span(word['frames'][frame]) + L.need(all(common <= L.span(source['frames'][first[r]]) for r in a), + 'Common native input subspace') + records.append({'primary': primary, 'frame': frame, 'basis': word['frames'][frame], + 'input_direction': h, 'departure_response': a}) + return records + + +def word_controls(L, word): + controls = {} + bad = deepcopy(word) + bad['initial'][496] = 3 + controls['old_input_chart'] = reject(lambda: L.replay(bad)) + edits = [ + ('missing_first_carrier_subtraction', ['ADD', 639, 643, '-2', 3], None), + ('missing_second_carrier_subtraction', ['ADD', 631, 635, '-2', 3], None), + ('wrong_649_injection', ['ADD', 198, 649, '1', 597], ['ADD', 198, 649, '-1', 597]), + ('wrong_663_injection', ['ADD', 179, 663, '1/2', 105], ['ADD', 179, 663, '-1/2', 105]), + ('missing_output_basis', ['ADD', 635, 508, '1/2', 127], None), + ('missing_carrier_move', ['MOVE', 635, 3, 1093, False], None), + ] + for label, event, replacement in edits: + bad = deepcopy(word) + L.need(bad['program'].count(event) == 1, 'Unique control event: ' + label) + i = bad['program'].index(event) + bad['program'][i:i+1] = [] if replacement is None else [replacement] + controls[label] = reject(lambda: L.replay(bad)) + bad = deepcopy(word) + bad['frames'][1093] = [1, 2, 4] + controls['wrong_intersection'] = reject(lambda: L.replay(bad)) + return controls + + +def run(build_only): + from support import SOURCE, WORD, authenticate, checkers, inputs, load, need, read + from construct import construct, payload + + raw = inputs() + source = json.loads(gzip.decompress(raw[WORD])) + word = construct(source) + need(gzip.decompress((HERE / 'WORD.json.gz').read_bytes()) == payload(word), + 'Every regenerated payload byte') + need(all(type(e[4]) is bool for e in word['program'] if e[0] == 'MOVE'), + 'Boolean ownership flags') + need(protected_events(word) == protected_events(source) and + word['frames'][1091:1093] == source['frames'][1091:1093], + 'Protected events and frames unchanged') + text = raw[SOURCE + 'pricing.py'].decode() + for before, after in read(HERE / 'PRICING-EDITS.json'): + need(text.count(before) == 1, 'Unique declared price edit') + text = text.replace(before, after) + need(text == (HERE / 'pricing.py').read_text(), 'Exact declared price edits') + with checkers() as (L, root): + directions = preparation(L, source, word) + baseline, local = L.replay(source), L.replay(word) + paid_delta, target_delta = delta(local['paid'], baseline['paid']), delta(local['helpers'], baseline['helpers']) + need(paid_delta == {1: 1, 2: 1, 3: 1, 4: 2, 5: -4}, 'Exact local paid change') + need(target_delta == {6: 1, 8: 3, 9: -4}, 'Exact productive target debit') + need(tuple(local[k] for k in ('public_inputs', 'owned_fields', 'owned_lifetimes', + 'peak_owned_fields', 'real_scalar_allowance', 'paid_rank_mass')) == + (770, 29, 32, 13, 127088, 5946), 'Exact local inventory') + controls = word_controls(L, word) + print('PASS regeneration, input bases, arbitrary inputs, ownership and controls', flush=True) + if build_only: + return None + columns = L.reverse_columns(word) + need(columns['columns'] == 799 and columns['coefficients'] == 638401, + 'Every input column and output coefficient') + print('PASS separate dense transpose', flush=True) + native = L.native(word) + C = load(root / 'research/p104-productive-controller/caller.py', 'lift_caller') + caller = C.construct() + need(caller == read(root / 'research/p104-productive-controller/CONTROLLER.json'), + 'Exact physical caller') + physical = C.physical(caller, word) + print('PASS native maps, absolute phases and complete physical caller', flush=True) + P = load(HERE / 'pricing.py', 'lift_price') + price = P.run(local, native, caller, physical) + need(price['raw_root_interval'] == + ['78227955453/25000000000000', '312911821813/100000000000000'], + 'Exact rational crossing interval') + E = load(root / 'research/higher-moment-strictification/verify.py', 'lift_comparison') + old_paid = {int(r): n for r, n in price['paid'].items()} + old_targets = {int(r): n for r, n in price['targets'].items()} + for before, change in ((old_paid, paid_delta), (old_targets, target_delta)): + for rank, count in change.items(): + before[rank] -= 18 * count + old_margin = E.moment(old_targets, 1 - P.KAPPA)[1] - E.moment(old_paid, 1 - P.KAPPA)[0] + need(old_margin < 0, 'The full source profile fails at the new claim') + controls.update(C.controls(caller)) + bad = deepcopy(local) + bad['paid'][3] -= 1 + controls['unpaid_carrier_move'] = reject(lambda: P.assemble(bad, native, caller, physical)) + bad = deepcopy(local) + bad['helpers'][9] += 1 + bad['helpers'][6] -= 1 + controls['missing_target_debit'] = reject(lambda: P.assemble(bad, native, caller, physical)) + for pin in read(HERE / 'SOURCES.json')['files']: + if pin['usage'] == 'input': + data = raw[pin['path']] + controls['damaged_' + pin['path']] = reject( + lambda data=data, pin=pin: authenticate(bytes([data[0] ^ 1]) + data[1:], pin)) + print('PASS two interval engines, complete costs, compiler, outer checks and controls', flush=True) + return P.encode(dict( + status=STATUS, base_commit=read(HERE / 'SOURCES.json')['base_commit'], + events=len(word['program']), directions=directions, source_local=baseline, local=local, + paid_delta=paid_delta, target_delta=target_delta, separate_columns=columns, native=native, + physical_caller=physical, complete_cost=price, source_margin_upper_at_new_claim=old_margin, + controls=controls, + limits=['All five inherited framework assumptions remain.', + 'The uniform word and rounded multiplier are not materialized.', + 'Author checks do not establish independent acceptance.', + 'The selected frontier is unchanged.'])) + + +def main(): + with tempfile.TemporaryDirectory(prefix='native-input-lift-cache-') as cache: + sys.pycache_prefix = cache + sys.path.insert(0, str(HERE)) + from support import need, read + result = run('--build-only' in sys.argv) + if result is not None: + if '--write' in sys.argv: + (HERE / 'RESULT.json').write_text(json.dumps(result, sort_keys=True, indent=2) + '\n') + else: + need(read(HERE / 'RESULT.json') == result, 'Exact retained result') + print(STATUS + ('_BUILD' if result is None else ''), flush=True) + + +if __name__ == '__main__': + main()