diff --git a/research/p104-coupled-frame-step/CHANGES.json b/research/p104-coupled-frame-step/CHANGES.json new file mode 100644 index 0000000000..a46098f911 --- /dev/null +++ b/research/p104-coupled-frame-step/CHANGES.json @@ -0,0 +1,50 @@ +{ + "frames": [ + [ + 30, + 44, + 459 + ] + ], + "changes": [ + { + "event": 14374, + "old": [ + "ADD", + 319, + 85, + "1", + 728 + ], + "new_frame": 1089 + }, + { + "event": 14399, + "old": [ + "ADD", + 507, + 319, + "1", + 728 + ], + "new_frame": 1089 + }, + { + "event": 16628, + "old": [ + "ADD", + 307, + 85, + "-1", + 236 + ], + "new_frame": 235 + }, + { + "endpoint": "final", + "register": 307, + "old_frame": 236, + "new_frame": 235 + } + ] +} \ No newline at end of file diff --git a/research/p104-coupled-frame-step/DISCOVERY.md b/research/p104-coupled-frame-step/DISCOVERY.md new file mode 100644 index 0000000000..7fdd8642f0 --- /dev/null +++ b/research/p104-coupled-frame-step/DISCOVERY.md @@ -0,0 +1,37 @@ +# Discovery and source credit + +The construction uses DreamingOfClouds's event-lattice model from PR5568, +exact commit `47a347ff70044615e7be6581d275d12f5df38295`. That package +reports a small retiming gain on PR5561. Its model and reported gain are +prior work, not a discovery claimed here. + +A first composition on PR5580 passed the complete registered checks at +kappa .00308191. Before publication, a fresh PR check found Pierre-Loic +Doulcet's larger PR5565 cascade. The first candidate was preserved locally; +it is not the contribution submitted here. The search was transferred to +PR5565 at `9af814164b9dfc21f19ec737959d67cb71488c95` without changing +its scalar order. + +The new run used OR-Tools 9.14.6206 on CPython 3.12.13, four solver workers, +90 seconds, neighbor radius two and all intermediate subspaces in anchor +quotients of dimension at most three. Its command structure was: + +```sh +HEAVY_THREADS=4 python3.12 -B evlat.py PR5565-WORD.json.gz witness.json.gz 90 2 3 +``` + +The status was `FEASIBLE`. The fast legality check passed and the re-price +was about 0.003085951751. The solver was not an optimality proof, and its +parallel output is not promised to be deterministic. + +The output changed 26 event/endpoint nodes in 20 independent components. +Only one component changed the moment: three ADD charts and helper 307's +final chart. The submitted construction retains exactly that component. +CHANGES.json fixes its four source sites and the new three-dimensional +frame. No solver is needed to reconstruct or verify it. + +Earlier scratch, compensated-scalar, fixed-order and commuting-ADD screens +found no paid-profile gain. Those searches are not submitted as exhaustive +obstructions. In particular, the independent owned-holder obstruction +belongs to PR5579. The submitted claim is this explicit frame step on the +newer cascade, its written chart proof and its complete exact certificate. diff --git a/research/p104-coupled-frame-step/HANDOFF.md b/research/p104-coupled-frame-step/HANDOFF.md new file mode 100644 index 0000000000..de4b5a5de6 --- /dev/null +++ b/research/p104-coupled-frame-step/HANDOFF.md @@ -0,0 +1,33 @@ +# Composition with the independent helper splits + +[PR #5599](https://github.com/CrocSwap/integer-mult-bounds/pull/5599), exact +head `0644592d421b375c221045954fdf13932575ffa8`, reports conditional kappa +.00309839 on a different word with 750 public inputs and 542 helpers. +Its source is PR5580. This package instead consumes both stages of PR5565 +and changes three contacts plus helper 307. No combined gain is claimed. + +The published fifteen-split witness was read at that exact head. None of +registers 85, 307, 319 or 507 occurs in its a, b, c or d basis-operation +supports. This is a useful compatibility screen, not a proof of composition. +The supports do include registers 648, 649, 650, 652 and 198, which occur +in PR5565 Stage A. Some split witnesses use frame 597, whose contacts that +stage removes. Do not apply the complete cascade without rechecking cuts. + +A bounded next test is: + +1. Start from the exact PR5599 word. Authenticate its source and retain + its larger input inventory, owned-register indices and compiler stock. +2. Test PR5565 Stage B separately from Stage A. It supplies the source + frame paths needed by this package. Check its commuting interval against + every inserted basis operation and repeat all split-interface checks. +3. Match this package's three ADDs by their source operands and surrounding + accesses. Add U = `[30,44,459]`, move the first two contacts to U, and + move the last contact and helper 307 exit to frame 235. +4. Reconstruct every transport, then replay all original inputs and the + transpose, every native map, physical caller, both complete moment + engines, compiler and outer inequalities. Count every helper target and + scalar/basis operation. Publish a combined kappa only after those pass. + +Credit Ali Romman's PR5599 independent-helper construction, Pierre-Loic +Doulcet's PR5565 cascade, DreamingOfClouds's event-lattice method and all +retained P104 sources. This handoff reserves no further search. diff --git a/research/p104-coupled-frame-step/LITERAL-CHANGES.diff b/research/p104-coupled-frame-step/LITERAL-CHANGES.diff new file mode 100644 index 0000000000..ef2112d8b1 --- /dev/null +++ b/research/p104-coupled-frame-step/LITERAL-CHANGES.diff @@ -0,0 +1,13 @@ +--- PR5565/pricing.py ++++ pricing.py +@@ -14,2 +14,2 @@ +-KAPPA, TESTED = Q('.00308520'), Q('.0030852005') +-PREVIOUS = Q('.00308189') ++KAPPA, TESTED = Q('.00308595'), Q('.0030859505') ++PREVIOUS = Q('.00308520') +@@ -64 +64 @@ +- L.need(sum(targets.values()) == 12814 and sum(paid.values()) == 66726, 'Complete field and call counts') ++ L.need(sum(targets.values()) == 12814 and sum(paid.values()) == 66708, 'Complete field and call counts') +@@ -142 +142 @@ +- return encode({'kappa':KAPPA,'kappa_decimal':'.00308520','previous_open_pr5580':PREVIOUS,'gain':KAPPA-PREVIOUS, ++ return encode({'kappa':KAPPA,'kappa_decimal':'.00308595','previous_open_pr5565':PREVIOUS,'gain':KAPPA-PREVIOUS, diff --git a/research/p104-coupled-frame-step/PROOF.md b/research/p104-coupled-frame-step/PROOF.md new file mode 100644 index 0000000000..d74e64bfdf --- /dev/null +++ b/research/p104-coupled-frame-step/PROOF.md @@ -0,0 +1,183 @@ +# Three coupled contacts improve the PR5565 P104 cascade + +## Source and statement + +The input is the exact PR5565 word at +`9af814164b9dfc21f19ec737959d67cb71488c95`, by Pierre-Loic Doulcet +(hexapode). It includes both stages of the commuting-contact cascade. +[SOURCES.json](SOURCES.json) pins this word and the retained price engine. +The event-lattice search from DreamingOfClouds's PR5568 supplied the +construction method. This package supplies the new four-site frame step +and its complete certificate on the later word. + +The construction preserves every scalar instruction, coefficient and +position in the scalar sequence. It preserves all 208 main endpoints, +all helper starts, all owned lifetimes and all 104 literal ports. It +changes three ADD charts and the final frame of helper 307. +[CHANGES.json](CHANGES.json) gives these four declarations. All event +indices below refer to the zero-based PR5565 source program. + +At each of 18 local calls, the paid change is + +```text +-2 H2 + 2 H3 - 2 H4 + H5. +``` + +The target change is `H4 - H5`. The complete conditional claim is +kappa = 0.00308595, tested at 0.0030859505. The five framework assumptions +and the source helper-endpoint conditions remain inherited. The selected +record is unchanged. + +## Exact chart geometry + +The new frame U has basis `[30,44,459]` and dimension three. It is frame +1089 in the new word. The source has 1089 frames, indexed 0 through 1088. +The following identities use complete binary spans, not basis-list equality: + +```text +U = span(frame 345 union frame 355) + = frame 728 intersection frame 235. +``` + +The relevant source frames are: + +| Frame | Basis | Dimension | +| --- | --- | --- | +| 3 | `[]` | 0 | +| 345 | `[30,487]` | 2 | +| 355 | `[30,44]` | 2 | +| 728 | `[30,44,76,391]` | 4 | +| 235 | `[30,44,74,385]` | 4 | +| 236 | `[6,24,42,74,385]` | 5 | +| 775 | `[7,25,43,75,139,267]` | 6 | +| 795 | `[12,18,32,64,391]` | 5 | +| 127 | standard nine-axis basis | 9 | + +The changed contacts are: + +| Event | Scalar instruction | Old frame | New frame | +| --- | --- | --- | --- | +| 14374 | `ADD 319 += 85` | 728 | U | +| 14399 | `ADD 507 += 319` | 728 | U | +| 16628 | `ADD 307 -= 85` | 236 | 235 | + +The new first two contacts let register 85 bypass frame 728. It can then +meet helper 307 at frame 235. Helper 307 no longer needs its last rank-one +transport and can finish at dimension four. This is a coupled change: +the last contact cannot move down to frame 235 while 85 retains frame 728. + +The exact paths between unchanged accesses are: + +| Register | Old path | New path | +| --- | --- | --- | +| 85 | `345 -> 728 -> 236 -> 127` | `345 -> U -> 235 -> 127` | +| 319 | `355 -> 728 -> 775` | `355 -> U -> 775` | +| 507 | `3 -> 728 -> 795` | `3 -> U -> 795` | +| 307 | `235 -> 236` | stays at `235` | + +All arrows are strict subspace inclusions. Every unchanged intervening +register access is retained. The constructor checks the four source +values, changes their charts, and replaces transports only in gaps with +a changed endpoint. It removes eight transports and inserts seven. The +result has 25,132 events and the same 21,686 scalar/owned events. + +## Arbitrary-input identity and native interfaces + +Let C_F be the native chart for frame F. Write a physical field as C_F z, +where z is its abstract row. A transport from A to B applies C_B C_A^-1 +and leaves z unchanged. An ADD at one common chart forms the same abstract +row sum. A SCALE has the same property. Thus each legal changed itinerary +implements the same abstract scalar word. + +The exact replay checks a common chart at every scalar contact and strict +nesting at every public transport. It checks all 743 original input +coefficients in every output. Every helper row returns its own arbitrary +input, and the main shears remain unchanged. A separate dense dyadic +transpose replay checks the reverse operator. + +Helper 307 starts at frame 3 in both words. Its target changes from the +rank-five map C_236 to the rank-four map C_235. Its input stays independent +of all other inputs. No helper input is set to zero or discarded. Every +other productive target stays fixed. + +The native replay checks every paid map, helper target and main adapter: +rank, signed Pauli images and absolute phase. The factorwise tensor rule +gives the same chart identity at every positive width under the retained +native framework. These checks do not, by themselves, prove the full +multiplication theorem or provide independent acceptance of the framework. + +## Complete paid and target change + +The four register changes give these local paid deltas: + +| Register | Paid delta | +| --- | --- | +| 85 | `H1 - H2 - H4 + H5` | +| 319 | `H1 - 2H2 + H3` | +| 507 | `-H1 + H2 + H3 - H4` | +| 307 | `-H1` | + +Their sum is `-2H2 + 2H3 - 2H4 + H5`. The local paid rank mass and target +rank mass both decrease by one. The complete rank-mass surplus remains +760. Paid jobs decrease by 18, from 66,726 to 66,708. The 12,814 productive +fields remain independent. + +Write h_r(k) = r^(1-k), with h_0(k) = 0. If M is target moment minus paid +moment, then + +```text +M_new(k) - M_parent(k) + = 18 * (2 h_2(k) - 2 h_3(k) + 3 h_4(k) - 2 h_5(k)). +``` + +For 0 < k < 1, this is strictly positive. To see this, the decreasing +vector `(5,5,3,3,0)` has partial sums `(5,10,13,16,16)`, and +`(4,4,4,2,2)` has partial sums `(4,8,12,14,16)`. The first vector +majorizes the second. Strict concavity of x^(1-k) therefore gives +`2 h_5 + 2 h_3 < 3 h_4 + 2 h_2`. The zero term is used only in this +proof; it is not an uncharged job in the construction. + +The predecessor raw crossing is in +`(0.00308521055201, 0.00308521055202)`. The new crossing is in `(0.00308595175070, 0.00308595175071)`. +The raw gain is between 7.4119868e-7 and 7.4119870e-7. The raw headroom +above the claimed endpoint is between 1.75070e-9 and 1.75071e-9. The verifier reconstructs both +predecessor histograms from the new bill and the declared deltas, then +checks the predecessor crossing again. Two rational moment engines check +the new tested endpoint. + +The derivative certificate proves that the complete new moment is strictly +decreasing on `[0,0.0034]`. Its upper crossing endpoint is the raw funding +ceiling for this fixed invoice on the retained BIT band. No ceiling for +other words or suppliers is claimed. + +## Full caller, verification and limits + +The unchanged caller has 18 forward local calls, 15 query shears and +3,120 whole idle jobs. The physical replay checks the actual 104 ports, +main routes, central squares, output ranks and whole-idle maps. The price +code derives the invoice from those events and checks it again from the +controller paths. It includes helper targets, normalizers, main adapters, +all routes, scalar operations, owned copies and erasures. + +The retained price engine changes only claim, predecessor-comparison and +exact paid-count declarations. LITERAL-CHANGES.diff records every change. +No source checker is weakened or patched at runtime. The PR5545 source +capsule and all 33 payload files are authenticated before import. + +The compiler checks all three tail ratios, completion, splitting, the +integer threshold, retained BIT stock and all 54 strict plus four +functional outer predicates. New negative controls reject a missing +transport, a wrong scalar coefficient, an old contact frame, an old helper +exit, a wrong intermediate subspace and an unchanged word presented as an +improvement. Source controls also reject a wrong native phase, insufficient +BIT saving and an old cutoff. + +The five inherited assumptions remain: native all-column implementation, +owned erasure, uniform compiler closure, precision/fixed-tape costs and +analytic recovery. The helper-endpoint contract retains its source review +status. The uniform word and complete rounded multiplier are not +materialized. The same assistant performed discovery and verification; +this is not independent scientific review or proof-kernel acceptance. + +Ali Romman with substantial OpenAI Codex assistance. Apache-2.0. +All retained source notices and predecessor credit remain in the package. diff --git a/research/p104-coupled-frame-step/README.md b/research/p104-coupled-frame-step/README.md new file mode 100644 index 0000000000..0ece7a298d --- /dev/null +++ b/research/p104-coupled-frame-step/README.md @@ -0,0 +1,135 @@ +# Conditional kappa 0.00308595 from three coupled P104 contacts + +This construction raises complete conditional kappa from **0.00308520** in +[PR #5565](https://github.com/CrocSwap/integer-mult-bounds/pull/5565) to +**0.00308595**. The new raw crossing is in +**(0.00308595175070, 0.00308595175071)**. Its raw gain over the exact +PR5565 crossing is between **7.4119868e-7 and 7.4119870e-7**. +The selected record remains 0.003027288235. + +The later [PR #5599](https://github.com/CrocSwap/integer-mult-bounds/pull/5599) +claims a larger endpoint from independent helper splits. This package is a +verified improvement to its pinned PR5565 source, not a claim to the largest +open bound. The combined word is untested; [HANDOFF.md](HANDOFF.md) gives +the concrete composition check. + +Three ADD contacts use lower-dimensional charts. This lets helper 307 +finish at rank four instead of rank five and removes one paid job per +local call. The complete caller has **66,708 paid jobs**, down from 66,726, +with the same 12,814 independent productive fields and rank-mass surplus +760. All scalar instructions, coefficients, scalar order, 208 main +endpoints and eight owned lifetimes stay fixed. + +Read [the proof](PROOF.md), [the four declarations](CHANGES.json), +[the constructor](construct.py), [the complete receipt](RESULT.json), +[the source pins](SOURCES.json) and [the validation record](VALIDATION.md). +The local paid delta is `-2H2 + 2H3 - 2H4 + H5`, and the target delta is +`H4 - H5`. A majorization argument proves a strict signed-moment gain for +every `0 < kappa < 1`. The new chart is the three-dimensional intersection +of two source frames. + +The construction uses the event-lattice search by @DreamingOfClouds in +[PR #5568](https://github.com/CrocSwap/integer-mult-bounds/pull/5568) on the +newer commuting cascade by Pierre-Loic Doulcet, @hexapode. It retains +both stages of that cascade. Only the positive four-node component of +the search output is retained; unrelated zero-gain edits are omitted. +[DISCOVERY.md](DISCOVERY.md) records the source method and attribution. + +## Reproduction + +Python 3.12 and the standard library suffice. No solver is needed to +construct or verify the submitted word. From the repository root: + +```sh +python3.12 -B scripts/research_package.py --package research/p104-coupled-frame-step +``` + +Both registered modes must print: + +```text +PASS_P104_COUPLED_FRAME_KAPPA_00308595 +``` + +The launcher must print `PASS_REGISTERED_RESEARCH_PACKAGE`. The two modes +check the input pins and complete 33-file source capsule, exact word +reconstruction, all original-input endpoints, dense transpose columns, +every signed native map, the physical caller, two rational moment engines, +the compiler and all 58 outer predicates. They compare the full receipt +and reject the declared negative controls. + +The PR5545 executable capsule remains unchanged. Its archive, inventory +and all payload hashes are checked before import. The word and price +inputs are byte-pinned to PR5565. The price diff changes only the claim, +predecessor comparison and exact paid-count declarations. All mathematical +tests remain. See [LITERAL-CHANGES.diff](LITERAL-CHANGES.diff). + +## Limits and ceiling + +The five inherited assumptions remain: native all-column implementation, +owned erasure, uniform compiler closure, precision and fixed-tape costs, +and analytic recovery. The helper-endpoint contract retains its source +review status. Helper 307's changed native target is explicit and fully +priced; no input is initialized to zero or discarded. + +The fixed invoice has a strictly decreasing signed moment on `[0,0.0034]`. +Its raw crossing is its funding ceiling on that retained BIT band. The +claim is tested at 0.0030859505 and has raw headroom between 1.75070e-9 +and 1.75071e-9. No optimum over other words or contracts is claimed. +The uniform word and complete rounded multiplier are not materialized. +Author-side replay is not independent scientific review or proof-kernel +acceptance. Hosted CI status is separate. + +The p19 proposals have larger numerical headlines. In particular, +[PR #5440](https://github.com/CrocSwap/integer-mult-bounds/pull/5440) retains +an unresolved chain-to-native compiler and physical attachment. This +package improves the complete P104 paid-caller line. It does not exceed +that extra-premise numerical proposal. + +## Coordination and credit + +Base: canonical main `5e0052ca0aa3036a3afa8b0438927377c8d97d53`, priority +revision 7. [Discussion #5575](https://github.com/CrocSwap/integer-mult-bounds/discussions/5575) +is the canonical claim. [TASK.json](TASK.json) records the scope and overlap +coverage. The scope preserves PR5565's scalar order and changes only frames. + +- Pierre-Loic Doulcet, @hexapode, supplied the consumed two-stage cascade in + [PR #5565](https://github.com/CrocSwap/integer-mult-bounds/pull/5565). +- @DreamingOfClouds supplied the event-lattice search in + [PR #5568](https://github.com/CrocSwap/integer-mult-bounds/pull/5568) and + the free-endpoint word in + [PR #5561](https://github.com/CrocSwap/integer-mult-bounds/pull/5561). +- Ali Romman supplied the complete contact certificate in + [PR #5580](https://github.com/CrocSwap/integer-mult-bounds/pull/5580), + the caller in [PR #5544](https://github.com/CrocSwap/integer-mult-bounds/pull/5544) + and the source closure in + [PR #5545](https://github.com/CrocSwap/integer-mult-bounds/pull/5545). +- Joel Pulikkan, @GamingPuzzled, supplied the priced helper-706 handoff in + [PR #5569](https://github.com/CrocSwap/integer-mult-bounds/pull/5569). +- @thu-nmrc supplied the earlier coupled contacts in + [PR #5551](https://github.com/CrocSwap/integer-mult-bounds/pull/5551). +- The retained notices credit Gareth Davidson, David Arias and Cinna Davis + for the source word, coalescing and private reuse; Cinna Davis for the + Laurent controller; Jacob Alan Sussman for productive recursion; and zxv + and Cao Yifan for interval, compiler and native work. The official source + closure retains the earlier geometry, BIT, precision and analytic notices. + +The fixed-word obstruction in +[PR #5579](https://github.com/CrocSwap/integer-mult-bounds/pull/5579) helped +close an earlier search direction. The fixed-contact floor in +[PR #5590](https://github.com/CrocSwap/integer-mult-bounds/pull/5590) is +related work; this construction changes contacts outside its fixed class. +Neither result is counted as a contribution or dependency of this package. + +New construction, proof and verification by Ali Romman with substantial +OpenAI Codex assistance. Apache-2.0. The same assistant did this work and +its checks; no independent reviewer or subagent was used. The source +toolkit credits DreamingOfClouds with Claude Opus 5.5 assistance. + +## Open next questions + +Independently review the frame intersection, helper 307 and the complete +invoice, then replay the registered checks. A further kappa step must +change a paid itinerary or target contract. Another root digit does not +improve this fixed invoice. No general obstruction follows from the +unsuccessful local screens that preceded this construction. Structured +questions are in [TASK.json](TASK.json). diff --git a/research/p104-coupled-frame-step/RESULT.json b/research/p104-coupled-frame-step/RESULT.json new file mode 100644 index 0000000000..e053f713e7 --- /dev/null +++ b/research/p104-coupled-frame-step/RESULT.json @@ -0,0 +1,408 @@ +{ + "controls": { + "missing_transport": "Common scalar chart", + "old_contact_frame": "Scalar destination and coefficient", + "old_helper_exit": "All public and owned exits", + "unchanged_word": "One additional frame", + "wrong_intermediate_subspace": "Nested chronological transport", + "wrong_scalar_coefficient": "All 743 public and owned rows" + }, + "fixed_invoice_ceiling": { + "kappa_interval": [ + "0", + "17/5000" + ], + "moment_derivative": [ + "-399858650967186222392048415655729047303897863682381692466321579/1569275433846670190958947355801916604025588861116008628224", + "-186295632315458241167193479907739297439446647173995485399139829/784637716923335095479473677900958302012794430558004314112" + ], + "scope": "This fixed paid and target invoice; the inherited BIT cap is retained." + }, + "inventory": { + "all_main_endpoints_fixed": true, + "changed_contacts": [ + [ + [ + "ADD", + 319, + 85, + "1", + 728 + ], + [ + "ADD", + 319, + 85, + "1", + 1089 + ] + ], + [ + [ + "ADD", + 507, + 319, + "1", + 728 + ], + [ + "ADD", + 507, + 319, + "1", + 1089 + ] + ], + [ + [ + "ADD", + 307, + 85, + "-1", + 236 + ], + [ + "ADD", + 307, + 85, + "-1", + 235 + ] + ] + ], + "changed_endpoints": { + "final": [ + 307 + ], + "initial": [] + }, + "events": 25132, + "global_paid_delta": { + "2": -36, + "3": 36, + "4": -36, + "5": 18 + }, + "global_target_delta": { + "4": 18, + "5": -18 + }, + "local_paid_delta": { + "2": -2, + "3": 2, + "4": -2, + "5": 1 + }, + "local_target_delta": { + "4": 1, + "5": -1 + }, + "ordered_scalar_events": 21686, + "owned_lifetimes_fixed": true, + "source_events": 25133 + }, + "local": { + "endpoint_coefficients": 552049, + "helpers": { + "4": 84, + "5": 4, + "8": 14, + "9": 425 + }, + "owned_lifetimes": 8, + "paid": { + "1": 2203, + "2": 457, + "3": 495, + "4": 90, + "5": 169, + "6": 18, + "7": 14 + }, + "peak_owned_fields": 1, + "public_inputs": 735, + "real_scalar_allowance": 217428 + }, + "native": { + "distinct_maps": 2915, + "helper_normalizers": 1054, + "helpers": { + "4": 84, + "5": 4, + "8": 14, + "9": 425 + }, + "main_adapters": 208, + "proof": "Every signed Pauli image and exact global phase; frame induction at every positive tensor width", + "recipe_payload_sha256": "8f974b92ae8bad09c1e5486bafa2250f9c8eb0869cbbebb342bfdab493dce18a", + "wrong_phase_rejected": true + }, + "parent_raw_interval": [ + "308521055201/100000000000000", + "154260527601/50000000000000" + ], + "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": [ + "18529967/25000000000000", + "7411987/10000000000000" + ], + "result": { + "compiler": { + "H": 690116000000000, + "N": "2^690116000000000", + "eta": { + "lower": "0.000000147470807177936571922181", + "upper": "0.000000147470807177936571922182" + }, + "gap": "1/14000000000", + "integer_test_exponent": 49294, + "logarithm_power": 1000, + "theta": "63/64", + "uniform_saving": "21601653/7000000000", + "word_materialized": false + }, + "full_forward_calls": 18, + "gain": "3/4000000", + "kappa": "61719/20000000", + "kappa_decimal": ".00308595", + "margin_at_previous": { + "lower": "0.183919896041829490516164716699", + "upper": "0.183919896041829490516164716700" + }, + "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": 5156000, + "local_scalar": 217428, + "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 6013." + }, + "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": "604846255956796697/196000000000000000000", + "fused_gaussian": "604846255870390091/196000000000000000000", + "global_coordinate_router": "5400413/1750000000", + "group_bit_router": "75605783733798761/24500000000000000000", + "group_scans": "6999999999/7000000000", + "main_transform": "604846241956796697/196000000000000000000", + "microbox_face_corrections": "269500000001/3500000000", + "polynomial_products": "13999999999/14000000000", + "sparse_union_movement": "80229846255956796697/196000000000000000000" + }, + "parameters": { + "a": "5400413/1750000000", + "b": "8640661/2800000000", + "beta": "13999999997/14000000000", + "bit_saving": "17/5000", + "cap_xi": "178229846241956796697/196000000000000000000", + "complex_uniform_saving": "21601653/7000000000", + "d": "1/14000000000", + "epsilon": "13999999999/14000000000", + "kappa": "61719/20000000", + "lambda_": "3987656199/4000000000", + "lambda_prime": "13956796697/14000000000", + "layout": "1/14000000000", + "q": "43203303/14000000000", + "r0": "1/140000000000", + "stop": "1/14000000000", + "tested_saving": "6171901/2000000000" + }, + "strict_checks": { + "actual_bit_above_effective": "549587/1750000000", + "actual_logarithmic_gamma_guard": "1/14000000000", + "actual_logarithmic_group_guard": "17770153779043203303/98000000000000000000", + "alpha_logarithm_absorption": "1/140000000000", + "boundary_algebraic_matrix_above_kappa": "55956796697/196000000000000000000", + "cap_above_band": "80229846241956796697/196000000000000000000", + "cap_below_cell": "17770153744043203303/196000000000000000000", + "cap_below_phase_cell_power": "213770153758043203303/196000000000000000000", + "complex_above_effective": "1/14000000000", + "complex_below_one_over_32": "78859339/2800000000", + "complex_endpoint": "1/7000000000", + "epsilon_below_one": "1/14000000000", + "epsilon_positive": "13999999999/14000000000", + "fine_prime_halo_umbrella": "7/2", + "fused_gaussian_above_kappa": "55870390091/196000000000000000000", + "gaussian_above_main": "6956796697/98000000000000000000", + "global_coordinate_router_above_kappa": "1/3500000000", + "global_gamma_power_slack": "9/140000000000", + "group_below_dimension": "1/7000000000", + "group_bit_router_above_kappa": "8733798761/24500000000000000000", + "group_gauge_power_slack": "17770153778343203303/98000000000000000000", + "group_key_fits_record": "1/7000000000", + "group_positive": "13999999997/14000000000", + "group_scans_above_kappa": "6978398349/7000000000", + "halo_covers_generic_inverse_radius": "5", + "improvement_over_user_baseline": "677489790400418148631/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": "5591359339/39200000000000000000", + "leaf_saving_above_effective": "2791359339/39200000000000000000", + "main_transform_above_kappa": "41956796697/196000000000000000000", + "membership_arithmetic_fits_record": "1/14000000000", + "microbox_face_corrections_above_kappa": "33686149897/437500000", + "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": "13956796699/14000000000", + "positive_layout_slack": "1/14000000000", + "q_below_effective": "1/14000000000", + "q_below_internal": "1/14000000000", + "q_below_leaf": "5591359339/39200000000000000000", + "q_positive": "43203303/14000000000", + "short_record_fallback": "2791359339/2800000000", + "source_axis_superpolynomial": "1/14000000000", + "sparse_union_movement_above_kappa": "79625000055956796697/196000000000000000000", + "stop_below_one": "13999999999/14000000000", + "stop_positive": "1/14000000000", + "strassen_integer_power_gap": "1951441519231", + "support_router_span": "3/14000000000", + "theta_positive_polynomial_power": "2", + "union_header_fits_record": "3/14000000000", + "union_tag_work_per_visit_fits_record": "3/14000000000" + } + }, + "paid": { + "1": 41214, + "16": 416, + "2": 8226, + "24": 416, + "3": 8910, + "32": 416, + "4": 1620, + "40": 416, + "48": 416, + "5": 3042, + "56": 416, + "6": 324, + "64": 416, + "7": 252, + "72": 208 + }, + "paid_calls": 66708, + "previous_open_pr5565": "7713/2500000", + "productive_fields": 12814, + "query_shears": 15, + "rank_mass_surplus": 760, + "raw_headroom": [ + "17507/10000000000000", + "175071/100000000000000" + ], + "raw_root_interval": [ + "30859517507/10000000000000", + "308595175071/100000000000000" + ], + "relative_gain_percent": "125/5142", + "strictification": { + "alpha": { + "lower": "0.999999998722139635203844345456", + "upper": "0.999999998722139635203844345457" + }, + "cutoff": 17, + "delta": { + "lower": "0.954850763206838362246260608411", + "upper": "0.954850763206838362246260608412" + }, + "floor": 18, + "gamma": { + "lower": "0.967584253656638271500698905679", + "upper": "0.967584253656638271500698905680" + }, + "normalized_paid_upper": "5242880004882813/5242880536870912", + "power": 1024, + "reserve": "1/10000000000", + "tail_offset": "1/5", + "tested": "6171901/2000000000" + }, + "targets": { + "145": 208, + "17": 416, + "25": 416, + "33": 416, + "4": 1512, + "41": 416, + "49": 416, + "5": 72, + "57": 416, + "65": 416, + "73": 208, + "8": 252, + "9": 7650 + }, + "whole_idle_jobs": 3120 + }, + "status": "PASS_P104_COUPLED_FRAME_KAPPA_00308595", + "transpose": { + "arithmetic": "Dense integer rows with binary denominators; reverse chronology", + "coefficients": 552049, + "columns": 743 + } +} diff --git a/research/p104-coupled-frame-step/SOURCES.json b/research/p104-coupled-frame-step/SOURCES.json new file mode 100644 index 0000000000..50f0168ba5 --- /dev/null +++ b/research/p104-coupled-frame-step/SOURCES.json @@ -0,0 +1,59 @@ +{ + "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-frame-step/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": "Byte-identical copy of the capsule retained by PR5551/PR5561; used UNMODIFIED (the hand-off word keeps 735 public inputs)." + }, + "external_inputs": [ + { + "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/pr5565-WORD.json.gz", + "source_repository": "hexapode/integer-mult-bounds", + "source_commit": "9af814164b9dfc21f19ec737959d67cb71488c95", + "source_path": "research/p104-commuting-contact/WORD.json.gz", + "sha256": "3d62828f53e654e3db218bf4611a47aed4a677d48043713dc004db0f8a32990d", + "git_blob": "4ebe6fcb7adf319bf6b247cf23d89eb1ca4cd914" + }, + { + "local_path": "inputs/pr5565-pricing.py", + "source_repository": "hexapode/integer-mult-bounds", + "source_commit": "9af814164b9dfc21f19ec737959d67cb71488c95", + "source_path": "research/p104-commuting-contact/pricing.py", + "sha256": "8d6bf48e65088b6cc8a342d88fdd885ab1fa6f91936c0dd6628a24db3ffec3b1", + "git_blob": "a99a3d467642d54d8088c1c33499380a07ed937a" + } + ], + "retained_source_scope": "The unchanged PR5545 official source export is an executable dependency. All 33 payloads, the inventory and archive hash are checked before import. This source is not new work.", + "discovery_source": { + "pr": 5568, + "commit": "47a347ff70044615e7be6581d275d12f5df38295", + "scope": "The PR5568 event-lattice search was run on the pinned PR5565 cascade. This package isolates its one positive four-node component and supplies the complete certificate. The earlier reported witness on PR5561 is credited as the research lead." + } +} diff --git a/research/p104-coupled-frame-step/TASK.json b/research/p104-coupled-frame-step/TASK.json new file mode 100644 index 0000000000..7ec397f074 --- /dev/null +++ b/research/p104-coupled-frame-step/TASK.json @@ -0,0 +1,132 @@ +{ + "schema_version": 1, + "task_id": "scalar-to-moment", + "priority_revision": 7, + "base_commit": "5e0052ca0aa3036a3afa8b0438927377c8d97d53", + "original_card": { + "id": "scalar-to-moment", + "question": "Can a changed frame itinerary remove a paid transition beyond the already covered scalar A2 contractions?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/staged544-a2-graph-rewrite/README.md", + "research/staged544-separated-a2/README.md", + "research/staged544-a2-composition-audit/README.md", + "research/staged544-a1858-contraction-audit/README.md" + ], + "methods": [ + "Derive the changed legal frame itinerary and exact child histogram.", + "Prove a scoped obstruction showing why that scalar gain cannot change the paid contract." + ], + "acceptance_gate": "An unchanged histogram is not a kappa gain; record any separate runtime or proof benefit explicitly.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read the A2 and separated-A2 constructions and their composition/contraction audits. Scalar contractions can preserve the complete recursive histogram; fewer ADDs alone do not justify further scans.", + "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately." + }, + "first_experiment": "Identify an actual paid transition to remove and construct a legal replacement frame itinerary, charging restoration, source windows and changed helpers. Compare complete before/after histograms. Stop if only scalar count changes; report that benefit honestly, without expanding the same scalar-only census.", + "bottleneck_link": "A legal change to the histogram, not addition count alone, is the bridge to an exponent gain.", + "allowed_variations": [ + "One existing scalar simplification and one proposed frame-path change." + ], + "scope_change_triggers": [ + "Submitting only another scalar count as completion of a paid-profile task." + ], + "overlap_terms": [ + "scalar simplification", + "paid profile", + "R439", + "3998", + "4019", + "4112", + "4152", + "staged544-a2-graph-rewrite", + "staged544-separated-a2", + "staged544-a2-composition-audit", + "staged544-a1858-contraction-audit" + ], + "existing_checks": [ + { + "scope": "PR #3998: consecutive A2 scalar contraction", + "evidence": "research/staged544-a2-graph-rewrite/README.md", + "remaining": "A genuinely changed paid itinerary or a distinct independent audit; no default scalar-only expansion.", + "status": "author-checked", + "source_commit": "389268a6b5e0373a3125d5c6fcd6995f4ea324f5", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4019: separated A2 sites with unchanged recursive histogram", + "evidence": "research/staged544-separated-a2/README.md", + "remaining": "A genuinely changed paid itinerary or a distinct independent audit; no default scalar-only expansion.", + "status": "author-checked", + "source_commit": "f408e09df300b575235f7f77f81948071397e16d", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4112: composition audit", + "evidence": "research/staged544-a2-composition-audit/README.md", + "remaining": "A genuinely changed paid itinerary or a distinct independent audit; no default scalar-only expansion.", + "status": "author-checked", + "source_commit": "205b7380656ba4b6316a8a493b1a3c679b8f7a0e", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4152: A1858 contraction audit", + "evidence": "research/staged544-a1858-contraction-audit/README.md", + "remaining": "A genuinely changed paid itinerary or a distinct independent audit; no default scalar-only expansion.", + "status": "author-checked", + "source_commit": "caaa14cde5962adc372fdca71f63d0f29e73c8b2", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Change three ADD charts and one helper exit on the exact PR5565 P104 cascade. Certify the complete conditional kappa .00308595 with the scalar program and all main endpoints fixed.", + "scope_change_reason": "The publication refresh found PR5565 above the first verified candidate. The frame search was transferred to that larger complete caller, preserving its scalar order. The new positive component changes only four chart declarations.", + "bottleneck_link": "The local target delta H4 - H5 and paid delta -2H2 + 2H3 - 2H4 + H5 give a strict complete-moment gain. Majorization proves positivity for every 0 < kappa < 1.", + "budget_minutes": null, + "stop_rule": "Publish only after the exact emitted word, all native maps, physical caller, both rational moment engines, compiler and all 58 outer predicates pass. Stop extending this fixed invoice after its crossing is isolated.", + "outcome": "completed", + "evidence": "RESULT.json records the new word, exact crossing, complete invoice and controls. VALIDATION.md records the final registered replay and publication checks.", + "author": "Ali Romman with substantial OpenAI Codex assistance", + "ai_assistance": "Substantial OpenAI Codex assistance for source analysis, witness regeneration, component isolation, composition, proof, verification and publication. The same assistant performed these checks; no independent reviewer or subagent was used.", + "open_questions": [ + { + "question": "Can an independent reviewer accept this composition and the inherited free-helper-endpoint contract?", + "why_it_matters": "The paid-profile gain passes exact author-side checks, but scientific acceptance remains separate.", + "first_step": "Check the three contact windows, the frame intersection, helper 307 and the complete invoice; then run the registered replay.", + "blocked_by": "No missing technical source; independent review remains pending." + }, + { + "question": "Can another changed scalar or frame realization improve this fixed invoice?", + "why_it_matters": "The fixed invoice has a certified raw crossing and only a small reserve above the claimed endpoint.", + "first_step": "Check live claims and propose a new paid itinerary or target contract, with full accounting.", + "blocked_by": "A new word and complete replay are required; no global optimality claim is made." + }, + { + "question": "Can the contact step compose with the independent helper splits in PR5599?", + "why_it_matters": "PR5599 has a larger conditional headline and a different input inventory. No combined bound is certified here.", + "first_step": "Follow HANDOFF.md: test PR5565 Stage B separately, then map the four chart changes and recheck all split witnesses, native maps and complete costs.", + "blocked_by": "The combined physical word and full replay have not been built." + } + ], + "coordination": { + "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/5575", + "base_main": "5e0052ca0aa3036a3afa8b0438927377c8d97d53", + "open_prs_checked": 320, + "discussion_records_checked": 4836, + "remote_pagination_complete": true, + "remote_checked_utc": "2026-10-25T21:24:00Z", + "local_coverage": "Sparse; relevant P104 sources read directly. No exhaustive local novelty claim.", + "presubmission_main": "5e0052ca0aa3036a3afa8b0438927377c8d97d53", + "presubmission_checked_utc": "2026-10-25T21:42:15Z", + "new_related_pr": "https://github.com/CrocSwap/integer-mult-bounds/pull/5565", + "coverage_note": "Initial complete pagination covered 320 open PRs and 4836 Discussion records. The prepublication delta check read 60 newest updated PRs and 60 newest updated Discussions; both lists extended before the previous checkpoint. Sparse local note coverage remains incomplete.", + "concurrent_larger_proposal": "https://github.com/CrocSwap/integer-mult-bounds/pull/5599" + } +} diff --git a/research/p104-coupled-frame-step/VALIDATION.md b/research/p104-coupled-frame-step/VALIDATION.md new file mode 100644 index 0000000000..903998e54c --- /dev/null +++ b/research/p104-coupled-frame-step/VALIDATION.md @@ -0,0 +1,54 @@ +# Validation record + +Checked on 2026-10-25 with CPython 3.12.13 on macOS arm64. Verification +uses the standard library. OR-Tools was used only for discovery. + +## Scientific replay + +The first warning-strict source-bound replay generated RESULT.json and +passed. The final registered command then passed in normal and optimized +modes, with warnings treated as errors in both commands: + +```sh +python3.12 -B scripts/research_package.py --package research/p104-coupled-frame-step +``` + +Each mode printed `PASS_P104_COUPLED_FRAME_KAPPA_00308595`; the launcher +printed `PASS_REGISTERED_RESEARCH_PACKAGE`. + +Both modes authenticated the input Git blobs and SHA256 values, the source +archive, its inventory and all 33 payloads. They reconstructed the complete +word and checked the frame intersection and span. They checked all 743 +arbitrary-input forward rows, 552,049 dense transpose coefficients, +2,915 exact native maps, 1,054 helper normalizers, 208 main adapters and +the full physical caller. The complete invoice, both rational moment +engines, fixed-invoice derivative, compiler and all 58 outer predicates +passed. Six new mutation controls and the retained native/price controls +were rejected as required. The full receipt matched RESULT.json. + +## Source and publication checks + +The branch starts from canonical main +`5e0052ca0aa3036a3afa8b0438927377c8d97d53`, which was still current at +21:42 UTC. The PR5565 input head remains +`9af814164b9dfc21f19ec737959d67cb71488c95`. The input word, price code +and retained common loader are byte-pinned in SOURCES.json. + +The initial overlap check covered complete remote pagination. Later +checks covered the updated PR and Discussion records back through the +previous checkpoint. Sparse local-note coverage is incomplete. The final +check found PR5599's larger independent-helper result; HANDOFF.md records +its separate composition obligation. + +The publication byte check and rendered-description/readback evidence are +saved with the local publication handoff. Full-history preflight was not +run because this checkout is shallow. Immediate-base ancestry and all +consumed source bytes are checked separately; no full-history claim is made. + +## Limits + +No unrelated historical suite, full rounded multiplier, enormous uniform +compiler word, standalone read-only Git-free replay, proof-kernel proof or +independent scientific review was run for this word. The five framework +assumptions retain their source status. Hosted CI is separate from these +local checks. No combined word with PR5599 was built or certified. diff --git a/research/p104-coupled-frame-step/VERIFY.json b/research/p104-coupled-frame-step/VERIFY.json new file mode 100644 index 0000000000..b0832d8907 --- /dev/null +++ b/research/p104-coupled-frame-step/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": 540, + "checks": "Authenticate the source closure and input pins; reconstruct the changed word; replay all arbitrary inputs, the transpose, every native map and the physical caller; check both complete invoices, two exact moment engines, the compiler, all 58 outer predicates and negative controls." + }, + { + "argv": [ + "{python}", + "-W", + "error", + "-B", + "-O", + "{package}/verify.py" + ], + "timeout_seconds": 540, + "checks": "Authenticate the source closure and input pins; reconstruct the changed word; replay all arbitrary inputs, the transpose, every native map and the physical caller; check both complete invoices, two exact moment engines, the compiler, all 58 outer predicates and negative controls." + } + ] +} diff --git a/research/p104-coupled-frame-step/WORD.json.gz b/research/p104-coupled-frame-step/WORD.json.gz new file mode 100644 index 0000000000..3c9a5ce896 Binary files /dev/null and b/research/p104-coupled-frame-step/WORD.json.gz differ diff --git a/research/p104-coupled-frame-step/common.py b/research/p104-coupled-frame-step/common.py new file mode 100644 index 0000000000..bd244313fc --- /dev/null +++ b/research/p104-coupled-frame-step/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-frame-step/construct.py b/research/p104-coupled-frame-step/construct.py new file mode 100644 index 0000000000..2506f4bdc8 --- /dev/null +++ b/research/p104-coupled-frame-step/construct.py @@ -0,0 +1,65 @@ +"""Change three coupled charts on the PR5565 P104 cascade. + +DreamingOfClouds supplied the event-lattice search used for discovery. +Ali Romman prepared this composition and exact certificate with substantial +OpenAI Codex assistance. Apache-2.0. See SOURCES.json and README.md. +""" +from collections import defaultdict +from copy import deepcopy +from pathlib import Path +import json + + +def need(ok, why): + if not ok: + raise ValueError(why) + + +def construct(source): + declaration = json.loads(Path(__file__).with_name('CHANGES.json').read_text()) + changes = declaration['changes'] + need(len(changes) == 4 and len(source['program']) == 25133, + 'Exact source and edit counts') + word = deepcopy(source) + need(len(source['frames']) == 1089, 'Exact source frame count') + word['frames'].extend(declaration['frames']) + old, new = source['program'], word['program'] + for change in changes: + if 'event' in change: + i = change['event'] + need(old[i] == change['old'], 'Exact source event') + new[i][-1] = change['new_frame'] + else: + key, r = change['endpoint'], change['register'] + need(source[key][r] == change['old_frame'], 'Exact source endpoint') + word[key][r] = change['new_frame'] + anchors = {r: [(-1, source['initial'][r], word['initial'][r])] + for r in range(source['public'])} + moves = defaultdict(list) + for i, event in enumerate(old): + op, r = event[:2] + if op == 'MOVE': + moves[r].append(i) + elif op in ('ADD', 'COPY', 'SCALE'): + registers = event[1:3] if op != 'SCALE' else event[1:2] + for r in registers: + if r in anchors: + anchors[r].append((i, event[-1], new[i][-1])) + remove, before = set(), defaultdict(list) + for r, visits in anchors.items(): + visits.append((len(old), source['final'][r], word['final'][r])) + for (i, a, x), (j, b, y) in zip(visits, visits[1:]): + if (a, b) == (x, y): + continue + remove.update(k for k in moves[r] if i < k < j) + if x != y: + before[j].append(['MOVE', r, x, y, False]) + program = [] + for i, event in enumerate(new): + program.extend(before[i]) + if i not in remove: + program.append(event) + program.extend(before[len(old)]) + word['program'] = program + need(len(program) == 25132, 'One fewer paid transport') + return word diff --git a/research/p104-coupled-frame-step/inputs/pr5545-source-closure.tar.gz b/research/p104-coupled-frame-step/inputs/pr5545-source-closure.tar.gz new file mode 100644 index 0000000000..3084088544 Binary files /dev/null and b/research/p104-coupled-frame-step/inputs/pr5545-source-closure.tar.gz differ diff --git a/research/p104-coupled-frame-step/inputs/pr5565-WORD.json.gz b/research/p104-coupled-frame-step/inputs/pr5565-WORD.json.gz new file mode 100644 index 0000000000..4ebe6fcb7a Binary files /dev/null and b/research/p104-coupled-frame-step/inputs/pr5565-WORD.json.gz differ diff --git a/research/p104-coupled-frame-step/inputs/pr5565-pricing.py b/research/p104-coupled-frame-step/inputs/pr5565-pricing.py new file mode 100644 index 0000000000..a99a3d4676 --- /dev/null +++ b/research/p104-coupled-frame-step/inputs/pr5565-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('.00308520'), Q('.0030852005') +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()) == 12814 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),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':'.00308520','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-frame-step/pricing.py b/research/p104-coupled-frame-step/pricing.py new file mode 100644 index 0000000000..827f547656 --- /dev/null +++ b/research/p104-coupled-frame-step/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('.00308595'), Q('.0030859505') +PREVIOUS = Q('.00308520') + + +def encode(x): + if isinstance(x,Q): + return str(x) + if isinstance(x,dict): + return {str(k):encode(v) for k,v in x.items()} + if isinstance(x,(list,tuple)): + return [encode(v) for v in x] + return x + + +def assemble(local, native, word, physical): + paid, targets = Counter(), Counter() + counts = Counter() + L.need(local['helpers'] == native['helpers'], 'Every productive helper has a native target') + for e in word['physical_events']: + counts[e[0]] += 1 + if e[0] == 'LOCAL': + L.need(e[3] is False, 'Every source invocation is forward') + paid.update(local['paid']) + targets.update(local['helpers']) + elif e[0] == 'QUERY_SHEAR': + paid[1] += 104 + elif e[0] == 'IDLE': + paid[8*len(e[2])] += 208 + main = Counter() + idle = Counter({8*len(e[2]):0 for e in word['physical_events'] if e[0] == 'IDLE'}) + for e in word['physical_events']: + if e[0] == 'IDLE': + idle[8*len(e[2])] += 208 + L.need(idle == physical['whole_idle_jobs'], 'Every whole idle has a native Gaussian and full rank') + for term in word['diagonal']: + main[1+8*sum(term[1:])] += 104 + L.need(main == physical['main_targets'], 'Every main target has its full native phase') + targets.update(main) + L.need(counts['LOCAL'] == 18 and counts['QUERY_SHEAR'] == counts['IDLE'] == 15, 'Complete call census') + # Recount by the two path lengths, without using emitted main diagonals. + second_t = Counter({r:18*n for r,n in local['helpers'].items()}) + second_p = Counter({r:18*n for r,n in local['paid'].items()}) + second_t[145] += 208 + second_p[1] += 15*104 + for length in (7,8): + for j in range(1,length+1): + second_t[1+8*(j+1)] += 208 + second_p[8*(j+1)] += 208 + L.need((targets,paid) == (second_t,second_p), 'Independent full invoice') + L.need(max(targets) == 145 and max(paid) == 72, 'Maximum recursive ranks') + L.need(sum(targets.values()) == 12814 and sum(paid.values()) == 66708, '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':'.00308595','previous_open_pr5565':PREVIOUS,'gain':KAPPA-PREVIOUS, + 'relative_gain_percent':100*(KAPPA/PREVIOUS-1),'raw_root_interval':[lower,upper], + 'raw_headroom':[lower-KAPPA,upper-KAPPA],'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-frame-step/verify.py b/research/p104-coupled-frame-step/verify.py new file mode 100644 index 0000000000..99c08931f2 --- /dev/null +++ b/research/p104-coupled-frame-step/verify.py @@ -0,0 +1,198 @@ +"""Check the coupled frames, complete caller and conditional kappa. + +Ali Romman with substantial OpenAI Codex assistance. Apache-2.0. +Retained sources and their contributors are listed in SOURCES.json. +""" +from collections import Counter +from copy import deepcopy +from fractions import Fraction as Q +from hashlib import sha256 +from pathlib import Path +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 +from construct import construct + + +def inventory(base, word): + for key in base: + if key not in ('program', 'initial', 'final', 'frames'): + need(word[key] == base[key], 'Unchanged word field: ' + key) + need(word['frames'] == base['frames']+[[30,44,459]], 'One additional frame') + old = [e for e in base['program'] if e[0] != 'MOVE'] + new = [e for e in word['program'] if e[0] != 'MOVE'] + need([e[:-1] for e in old] == [e[:-1] for e in new], + 'Same ordered scalar and owned operations') + changes = [(a, b) for a, b in zip(old, new) if a != b] + declared = read(HERE/'CHANGES.json')['changes'] + expected = [(c['old'], c['old'][:-1]+[c['new_frame']]) + for c in declared if 'event' in c] + need(changes == expected and len(changes) == 3, 'Exact three changed ADD charts') + endpoints = {} + for key, registers in (('initial', []), ('final', [307])): + changed = [r for r, (a,b) in enumerate(zip(base[key],word[key])) if a != b] + need(changed == registers, 'Exact changed ' + key + ' frames') + endpoints[key] = changed + main = set(base['live']) | {r+112 for r in base['live']} + need(not main.intersection(endpoints['initial']+endpoints['final']), + 'All 208 main endpoints fixed') + def bill(w): + return Counter(abs(len(w['frames'][e[2]])-len(w['frames'][e[3]])) + for e in w['program'] if e[0] == 'MOVE') + before, after = bill(base), bill(word) + delta = {r:after[r]-before[r] for r in before.keys()|after.keys() + if after[r] != before[r]} + need(delta == {2:-2,3:2,4:-2,5:1}, 'Exact changed paid profile') + def targets(w): + return Counter(len(w['frames'][w['final'][r]])-len(w['frames'][w['initial'][r]]) + for r in range(w['public']) if r not in main) + before, after = targets(base), targets(word) + target_delta = {r:after[r]-before[r] for r in before.keys()|after.keys() + if after[r] != before[r]} + need(target_delta == {4:1,5:-1}, 'Exact changed helper targets') + return {'source_events':len(base['program']), 'events':len(word['program']), + 'ordered_scalar_events':len(old), 'changed_contacts':changes, + 'changed_endpoints':endpoints, 'local_paid_delta':delta, + 'global_paid_delta':{r:18*n for r,n in delta.items()}, + 'local_target_delta':target_delta, + 'global_target_delta':{r:18*n for r,n in target_delta.items()}, + 'all_main_endpoints_fixed':True, 'owned_lifetimes_fixed':True} + + +def controls(L, base, word): + variants = {} + bad = deepcopy(word) + event = next(e for e in bad['program'] if e == ['ADD',319,85,'1',1089]) + event[-2] = '2' + variants['wrong_scalar_coefficient'] = bad + bad = deepcopy(word) + bad['final'][307] = 236 + variants['old_helper_exit'] = bad + bad = deepcopy(word) + event = next(e for e in bad['program'] if e == ['ADD',507,319,'1',1089]) + event[-1] = 728 + variants['old_contact_frame'] = bad + bad = deepcopy(word) + bad['program'].remove(['MOVE',85,345,1089,False]) + variants['missing_transport'] = bad + bad = deepcopy(word) + bad['frames'][1089] = [1,2,4] + variants['wrong_intermediate_subspace'] = bad + rejected = {} + for name, bad in variants.items(): + try: + L.replay(bad) + except ValueError as error: + rejected[name] = str(error) + else: + raise ValueError('Accepted invalid word: ' + name) + try: + inventory(base, base) + except ValueError as error: + rejected['unchanged_word'] = str(error) + else: + raise ValueError('Accepted unchanged word as a profile improvement') + print('PASS coupled-frame controls', rejected, flush=True) + return rejected + + +def ceiling(E, targets, paid): + """Bound the moment derivative on the retained BIT band.""" + cap = Q('0.0034') + lower = upper = 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; the inherited BIT cap is retained.'} + + +def main(): + sources = read(HERE/'SOURCES.json') + for pin in sources['external_inputs']: + raw = (HERE/pin['local_path']).read_bytes() + need(sha256(raw).hexdigest() == pin['sha256'], 'Source bytes: ' + pin['local_path']) + header = ('blob ' + str(len(raw)) + '\0').encode() + from hashlib import sha1 + need(sha1(header + raw).hexdigest() == pin['git_blob'], 'Source Git object: ' + pin['local_path']) + base = read(HERE/'inputs/pr5565-WORD.json.gz') + word = read(HERE/'WORD.json.gz') + need(construct(base) == word, 'Regenerated complete word payload') + inv = inventory(base, word) + source_price = (HERE/'inputs/pr5565-pricing.py').read_text() + for before, after in ( + ("KAPPA, TESTED = Q('.00308520'), Q('.0030852005')", + "KAPPA, TESTED = Q('.00308595'), Q('.0030859505')"), + ("PREVIOUS = Q('.00308189')", "PREVIOUS = Q('.00308520')"), + ("'kappa_decimal':'.00308520'", "'kappa_decimal':'.00308595'"), + ("'previous_open_pr5580':PREVIOUS", "'previous_open_pr5565':PREVIOUS"), + ("sum(paid.values()) == 66726", "sum(paid.values()) == 66708")): + need(source_price.count(before) == 1, 'Unique pricing declaration: ' + before) + source_price = source_price.replace(before, after) + need(source_price == (HERE/'pricing.py').read_text(), 'Only declared pricing and census constants change') + print('PASS source pins, exact reconstruction and changed invoice', flush=True) + with closure() as root: + L = load(root/'research/p104-productive-controller/local.py', 'local') + L.ROOT = root + frames = [L.span(b) for b in word['frames']] + need(frames[1089] == frames[728] & frames[235], 'Exact frame intersection') + need(frames[1089] == {a ^ b for a in frames[345] for b in frames[355]}, 'Exact source-frame span') + parent_local = L.replay(base) + local = L.replay(word) + need(sum(parent_local['helpers'].values()) == sum(local['helpers'].values()) == 527, 'Same helper field count') + need(parent_local['real_scalar_allowance'] == local['real_scalar_allowance'], 'Same scalar allowance') + rejected = controls(L, base, word) + print('PASS both exact arbitrary-input endpoints', flush=True) + reverse = L.reverse_columns(word) + print('PASS exact transpose', flush=True) + native = L.native(word) + print('PASS exact signed native maps', native['distinct_maps'], flush=True) + C = load(root/'research/p104-productive-controller/caller.py', 'coupled_frame_caller') + caller = C.construct() + need(caller == read(root/'research/p104-productive-controller/CONTROLLER.json'), 'Exact physical caller') + physical = C.physical(caller, word) + print('PASS full physical caller', flush=True) + P = load(HERE/'pricing.py', 'coupled_frame_pricing') + result = P.run(local, native, caller, physical) + print('PASS complete pricing', result['raw_root_interval'], flush=True) + E = L.load(root/'research/higher-moment-strictification/verify.py', 'coupled_frame_margin') + targets = {int(r): n for r, n in result['targets'].items()} + paid = {int(r): n for r, n in result['paid'].items()} + parent_paid, parent_targets = dict(paid), dict(targets) + for r, n in inv['global_target_delta'].items(): + parent_targets[r] -= n + for r, n in inv['global_paid_delta'].items(): + parent_paid[r] -= n + parent_interval = [Q('0.00308521055201'), Q('0.00308521055202')] + parent_signs = [] + for k in parent_interval: + t, p = E.moment(parent_targets, 1-k), E.moment(parent_paid, 1-k) + parent_signs.append((t[0]-p[1], t[1]-p[0])) + need(parent_signs[0][0] > 0 > parent_signs[1][1], 'Exact predecessor crossing') + lo, hi = map(Q, result['raw_root_interval']) + gain = [lo-parent_interval[1], hi-parent_interval[0]] + need(gain[0] > 0, 'Strict gain over predecessor raw ceiling') + fixed_ceiling = ceiling(E, targets, paid) + receipt = P.encode({'status': 'PASS_P104_COUPLED_FRAME_KAPPA_00308595', + '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, + '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_FRAME_KAPPA_00308595', flush=True) + + +if __name__ == '__main__': + main()