diff --git a/research/p104-commuting-contact/CLAIM.md b/research/p104-commuting-contact/CLAIM.md new file mode 100644 index 0000000000..5e4e78c4f1 --- /dev/null +++ b/research/p104-commuting-contact/CLAIM.md @@ -0,0 +1,22 @@ +# CLAIM — P104 commuting-contact cascade on the PR #5580 word + +Base: canonical main `5e0052ca0aa3036a3afa8b0438927377c8d97d53`, priority revision 7. +Exact construction input: [PR #5580](https://github.com/CrocSwap/integer-mult-bounds/pull/5580) at `6efa248cf456d6101d757e9d09ba29711d18a13a` (`research/p104-event-contact-step`, conditional $\kappa = 0.00308189$). + +Question: PR #5580 explicitly left open whether a changed scalar event order within commuting windows can improve the complete paid profile beyond its fixed-order invoice ceiling `(0.00308189496866, 0.00308189496867)`. Because PR #5561, PR #5569, and PR #5580 preserved the exact linear order of the 21,686 scalar instructions from PR #5551, early moves of main ports `113` and `198` to 1-plane `597` (`[82]`) at events `13524` and `13528` (to read helper `710`) trapped subsequent commuting `ADD` writes into `198` (from `648, 649, 650, 652`) and into `113` (from `531`) at frame `597`. + +Result: +1. **Stage A (Fixed-Endpoint Supporting Word `WORD-FIXED-ENDPOINTS.json.gz`, $\kappa = 0.00308415$):** Commuting `13625, 13628, 13631, 13634` (`198 += ±1/2 * 648/649/650/652`) before `13528` (`MOVE 198: 3 -> 597`) to frame `3` (`0D`) vacates frame `597` (`1D`) on all four helpers `648, 649, 650, 652`, collapsing `3 (0D) -> 597 (1D) -> 120 (5D)` (`H1 + H4`) into `3 (0D) -> 120 (5D)` (`H5`). All 735 `initial` and `final` frames and all 527 helper targets remain identical to PR #5580. Local paid delta: `-4 H1 - 4 H4 + 4 H5` (`-72` complete paid calls, `66,852 -> 66,780`), raising the raw crossing to `(0.00308415555080, 0.00308415555081)` (`+2.26058214e-6` over PR #5580). +2. **Stage A+B (Headline Cascade Word `WORD.json.gz`, $\kappa = 0.00308520$):** Commuting `13806` (`113 += 531`) before `13524` (`MOVE 113: 3 -> 597`) to frame `3` (`0D`) allows all three initial read contacts of helper `531` (`13806` with `113`, `13843` with `197`, and `14404` with `507`) to execute at frame `3` (`0D`) with `initial[531] = 3`. Because `197` remains at `3` (`0D`) after `13843`, its next contact `13846` (`197 += 319`) demotes from 3-plane `617` (`[30, 44, 76]`) to 2-plane `355` (`[30, 44]`), vacating `617` on both `197` and `319` and vacating `597` on `531, 197, 507`. Combined local paid delta vs PR #5580: `-8 H1 - H3 - 2 H4 + 4 H5` (`-126` complete paid calls, `66,852 -> 66,726`), with local helper target delta `-H8 + H9` (productive fields `12,814` and rank-mass surplus `760` unchanged), raising the raw crossing to `(0.00308521055201, 0.00308521055202)` and certifying **conditional $\kappa = 0.00308520$** at `TESTED = 0.0030852005` (`+3.31558335e-6` raw over PR #5580). + +```json +{ + "schema": "integer-mult-coordination/v1", + "kind": "CLAIM", + "task": "scalar-to-moment", + "scope": "P104 commuting-write contact cascade on the PR5580 word; complete paid-profile step", + "base": "5e0052ca0aa3036a3afa8b0438927377c8d97d53", + "expiry": "2026-10-25T23:59:59+00:00", + "artifact": "research/p104-commuting-contact" +} +``` diff --git a/research/p104-commuting-contact/LITERAL-CHANGES.diff b/research/p104-commuting-contact/LITERAL-CHANGES.diff new file mode 100644 index 0000000000..caaf7da91f --- /dev/null +++ b/research/p104-commuting-contact/LITERAL-CHANGES.diff @@ -0,0 +1,31 @@ +--- inputs/pr5580-pricing.py 2026-10-25 20:25:29.002478680 +0000 ++++ pricing.py 2026-10-25 21:03:53.929660636 +0000 +@@ -11,8 +11,8 @@ + from fractions import Fraction as Q + import local as L + +-KAPPA, TESTED = Q('.00308189'), Q('.0030818905') +-PREVIOUS = Q('.00308181') ++KAPPA, TESTED = Q('.00308520'), Q('.0030852005') ++PREVIOUS = Q('.00308189') + + + def encode(x): +@@ -61,7 +61,7 @@ + second_p[8*(j+1)] += 208 + L.need((targets,paid) == (second_t,second_p), 'Independent full invoice') + L.need(max(targets) == 145 and max(paid) == 72, 'Maximum recursive ranks') +- L.need(sum(targets.values()) == 12814 and sum(paid.values()) == 66852, 'Complete field and call counts') ++ L.need(sum(targets.values()) == 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 + +@@ -139,7 +139,7 @@ + L.need(wrong_cutoff[0] > 1, 'Old cutoff fails with this helper inventory') + bad=outer_module.ledger(dict(params,bit_saving=Q('.0027'))) + L.need(any(x <= 0 for x in bad['strict_checks'].values()), 'Insufficient BIT contract rejected') +- return encode({'kappa':KAPPA,'kappa_decimal':'.00308189','previous_open_pr5569':PREVIOUS,'gain':KAPPA-PREVIOUS, ++ return encode({'kappa':KAPPA,'kappa_decimal':'.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()), diff --git a/research/p104-commuting-contact/PROOF.md b/research/p104-commuting-contact/PROOF.md new file mode 100644 index 0000000000..29a9567059 --- /dev/null +++ b/research/p104-commuting-contact/PROOF.md @@ -0,0 +1,75 @@ +# Proof of the P104 Commuting-Contact Cascade ($\kappa = 0.00308520$) + +This package modifies the [PR #5580](https://github.com/CrocSwap/integer-mult-bounds/pull/5580) P104 word (`research/p104-event-contact-step`, pinned at `6efa248cf456d6101d757e9d09ba29711d18a13a`) by commuting independent `ADD` instructions across two 1-plane transport barriers at frame `597` (`[82]`, $\dim 1$). Every scalar instruction, register operand, and dyadic coefficient is preserved; only the relative order of commuting `ADD` operations and their chart labels change. + +## 1. Stage A: Fixed-Endpoint Commuting Writes on Port `198` and Helpers `648, 649, 650, 652` + +In the PR #5580 word, main port `198` stays at the 0-dimensional origin chart `3` (`[]`) from initialization through event `13527`, receiving only `ADD` writes (`198 += c * s`). At events `13528..13634`, the relevant events on `198` and helpers `648, 649, 650, 652` are: + +```text +13528: ['MOVE', 198, 3, 597, False] +13529: ['ADD', 198, 710, '2', 597] +13623: ['ADD', 205, 648, '-1/2', 3] +13624: ['MOVE', 648, 3, 597, False] +13625: ['ADD', 198, 648, '1/2', 597] +13626: ['ADD', 205, 649, '-1/2', 3] +13627: ['MOVE', 649, 3, 597, False] +13628: ['ADD', 198, 649, '-1/2', 597] +13629: ['ADD', 205, 650, '-1/2', 3] +13630: ['MOVE', 650, 3, 597, False] +13631: ['ADD', 198, 650, '1/2', 597] +13632: ['ADD', 205, 652, '1/2', 3] +13633: ['MOVE', 652, 3, 597, False] +13634: ['ADD', 198, 652, '1/2', 597] +13770: ['MOVE', 648, 597, 120, False] +13772: ['MOVE', 649, 597, 120, False] +13774: ['MOVE', 650, 597, 120, False] +13778: ['MOVE', 652, 597, 120, False] +``` + +### Commutativity and Subspace Nesting (Stage A) +1. **Write-epoch commutativity on `198`:** Between `13528` and `13634`, register `198` is never read or scaled; its only operations are `13529` (`198 += 2 * 710`) and `13625, 13628, 13631, 13634` (`198 += ±1/2 * r` for `r in {648, 649, 650, 652}`). Additions into a common destination register commute with each other and with chart transport of that destination register. +2. **Read-epoch invariance on `648, 649, 650, 652`:** Each helper `r in {648, 649, 650, 652}` is initialized at chart `3` (`[]`, $\dim 0$) and is only read (never written or scaled) prior to event `13771`. Thus at event `13528`, each `r in {648, 649, 650, 652}` already holds its unmodified initial symbol at chart `3`. +3. **Elimination of chart `597` on `648, 649, 650, 652`:** Executing `13625, 13628, 13631, 13634` at chart `3` immediately before `13528: ['MOVE', 198, 3, 597, False]` eliminates the four climbs `3 -> 597` (`13624, 13627, 13630, 13633`) and replaces the four climbs `597 -> 120` (`13770, 13772, 13774, 13778`, where `120` has 5-dimensional basis `[7, 25, 75, 160, 288]`) with direct climbs `3 -> 120`. +4. **Stage A Paid Delta:** On each of `648, 649, 650, 652`, the paid itinerary `3 (0D) -> 597 (1D) -> 120 (5D)` (`H1 + H4`) becomes `3 (0D) -> 120 (5D)` (`H5`). All 735 `initial` and `final` frames and all 527 helper targets remain unchanged. The Stage A local paid delta is: + $$\Delta P_{\text{Stage A}} = -4 H_1 - 4 H_4 + 4 H_5$$ + which reduces complete paid calls by $72$ (`66,852 -> 66,780`) and raises the raw moment crossing from `(0.00308189496866, 0.00308189496867)` to `(0.00308415555080, 0.00308415555081)`. This supporting word is shipped as `WORD-FIXED-ENDPOINTS.json.gz`. + +--- + +## 2. Stage B: Commuting-Write Domino Cascade on `113, 531, 197, 319, 507` + +In the PR #5580 word, main port `113` stays at chart `3` (`0D`) up to event `13524`, where it moves `3 -> 597` (`[82]`, $\dim 1$) for `13525: ['ADD', 113, 710, '2', 597]`, followed by `13806: ['ADD', 113, 531, '1', 597]`. Because PR #5561's fixed-order solver could not commute `13806` before `13525`, helper `531` was forced to start at `597` (`1D`), which in turn forced `197` and `507` to climb `3 -> 597` for `13843: ['ADD', 197, 531, '-1', 597]` and `14404: ['ADD', 507, 531, '-1', 597]`: + +| Frame | Basis | Dimension | +| --- | --- | --- | +| `3` | `[]` | 0 | +| `355` | `[30, 44]` | 2 | +| `597` | `[82]` | 1 | +| `617` | `[30, 44, 76]` | 3 | +| `728` | `[30, 44, 76, 391]` | 4 | +| `741` | `[13, 19, 65, 423]` | 4 | +| `788` | `[13, 19, 33, 65, 390]` | 5 | + +Note that $30 = 13 \oplus 19 \in \text{span}(788)$ and $44 = 13 \oplus 33 \in \text{span}(788)$, so $\text{span}(3) \subset \text{span}(355) \subset \text{span}(788)$ and $\text{span}(355) \subset \text{span}(728)$ are strict subspace chains. + +### Domino Cascade Steps (Stage B) +1. **Commute `13806` before `13524` at chart `3` (`0D`):** Between `13524` and `13806`, register `113` receives only `ADD` writes (`13525` and `13806`), and helper `531` is in its initial read-only epoch (unmodified until `14478`). Setting `initial[531] = 3` (`0D`) and executing `13806: ['ADD', 113, 531, '1', 3]` immediately before `13524: ['MOVE', 113, 3, 597, False]` preserves `113`'s itinerary `3 (0D) -> 597 (1D) -> 614 (3D)`. +2. **Vacate `597` (`1D`) on `531, 197, 507`:** Because `531` is now at chart `3` (`0D`) during its initial read epoch, `13843: ['ADD', 197, 531, '-1', 3]` and `14404: ['ADD', 507, 531, '-1', 3]` execute at chart `3` (`0D`). Helper `507` skips `597` (`1D`) and climbs directly `3 (0D) -> 728 (4D)` (`H4` instead of `H1 + H3`), and helper `531` climbs `3 (0D) -> 741 (4D)` (`H4` instead of `H3`) while its helper target credit increases from `H8` (`9 - 1`) to `H9` (`9 - 0`). +3. **Demote `13846` (`ADD 197 += 319`) from `617` (`3D`) to `355` (`2D`):** Because `197` stays at `3` (`0D`) after `13843` instead of climbing to `597` (`[82]`, which is not in `span(355) = span([30, 44])`), `197` now climbs directly `3 (0D) -> 355 (2D)` to meet `319` at `355` (`2D`) for `13846: ['ADD', 197, 319, '1', 355]`, and then climbs `355 (2D) -> 788 (5D)`. This vacates `617` (`3D`) on both `197` (`H2 + H3` instead of `H1 + 2 H2`) and `319` (`355 (2D) -> 728 (4D)`, `H2` instead of `2 H1`). + +### Combined Stage A+B Invoice and Strict Concave Gain +Combining Stage A and Stage B across each of the 18 forward local calls gives: +- **Local paid delta:** $\Delta P_{\text{local}} = -8 H_1 - H_3 - 2 H_4 + 4 H_5$ (`-7` local `MOVE` instructions, `25,140 -> 25,133` events). +- **Global paid delta (18 calls):** $\Delta P = -144 H_1 - 18 H_3 - 36 H_4 + 72 H_5$ (`-126` paid calls, `66,852 -> 66,726`). +- **Local target delta:** $\Delta T_{\text{local}} = -H_8 + H_9$ (`-18 H_8 + 18 H_9` globally, keeping `12,814` productive fields and rank-mass surplus `760` invariant). + +The exact rational interval engines enclose the raw moment crossings: + +| Word | Lower endpoint | Upper endpoint | +| --- | --- | --- | +| PR #5580 (`p104-event-contact-step`) | `0.00308189496866` | `0.00308189496867` | +| Stage A (`WORD-FIXED-ENDPOINTS.json.gz`) | `0.00308415555080` | `0.00308415555081` | +| Stage A+B (`WORD.json.gz`, headline) | `0.00308521055201` | `0.00308521055202` | + +The raw gain over PR #5580 is strictly between `0.00000331558334` and `0.00000331558336`. The claimed conditional saving is **$\kappa = 0.00308520$**, tested at `0.0030852005` with raw headroom `1.055201e-8 .. 1.055202e-8`. diff --git a/research/p104-commuting-contact/README.md b/research/p104-commuting-contact/README.md new file mode 100644 index 0000000000..62aa71c92b --- /dev/null +++ b/research/p104-commuting-contact/README.md @@ -0,0 +1,36 @@ +# Conditional kappa 0.00308520 from a P104 commuting-contact cascade + +This construction increases complete conditional kappa from `0.00308189` in [PR #5580](https://github.com/CrocSwap/integer-mult-bounds/pull/5580) to **0.00308520** (`+3.31e-6`, raw crossing gain `+3.31558335e-6`). It also ships the fixed-endpoint supporting word `WORD-FIXED-ENDPOINTS.json.gz` reaching **0.00308415** (`+2.26058214e-6` raw over PR #5580) with all 735 `initial` and `final` frames and all 527 helper targets unchanged. The selected record remains `0.003027288235`. + +PR #5561, PR #5569, and PR #5580 kept the linear execution order of all 21,686 scalar operations fixed. Reordering independent `ADD` instructions within commuting write epochs on main ports `198` and `113` eliminates seven local `MOVE` transports per call (`-126` paid calls globally, `66,852 -> 66,726`) while preserving all 208 main endpoints, all 12,814 productive fields, rank-mass surplus `760`, and all eight owned lifetimes. + +Read [the proof](PROOF.md), [the construction](construct.py), [the complete receipt](RESULT.json), [the source pins](SOURCES.json), and [the verification record](VALIDATION.md). The exact raw crossing of the headline word lies in `(0.00308521055201, 0.00308521055202)` and is tested at `0.0030852005`. + +## Reproduction + +Python 3.10+ and the standard library suffice. No external solver is needed to reconstruct or verify both published words: + +```sh +python3 -B scripts/research_package.py --package research/p104-commuting-contact +``` + +Both registered modes print: + +```text +PASS_P104_COMMUTING_CONTACT_KAPPA_00308520 +``` + +and the launcher prints `PASS_REGISTERED_RESEARCH_PACKAGE`. It authenticates all 33 retained PR #5545 source payloads and the pinned PR #5580 inputs, regenerates both `WORD-FIXED-ENDPOINTS.json.gz` and `WORD.json.gz` from `construct.py`, runs forward arbitrary-input replay on the base, fixed-endpoint, and headline words, verifies all 552,049 dense transpose coefficients, checks all 2,918 signed native Pauli maps, runs the full physical caller, verifies both rational moment engines (`(0.00308415555080, 0.00308415555081)` for Stage A and `(0.00308521055201, 0.00308521055202)` for Stage A+B), and checks the compiler, all 58 outer predicates, and negative controls. + +## Credits + +- Ali Romman (`@aliromman`) supplied [PR #5580](https://github.com/CrocSwap/integer-mult-bounds/pull/5580) (`research/p104-event-contact-step`) and the complete caller/source closure in [PR #5544](https://github.com/CrocSwap/integer-mult-bounds/pull/5544) and [PR #5545](https://github.com/CrocSwap/integer-mult-bounds/pull/5545). +- Joel Pulikkan (`@GamingPuzzled`) supplied [PR #5569](https://github.com/CrocSwap/integer-mult-bounds/pull/5569) (`research/p104-priced-handoff`). +- `@DreamingOfClouds` supplied [PR #5561](https://github.com/CrocSwap/integer-mult-bounds/pull/5561) and [PR #5568](https://github.com/CrocSwap/integer-mult-bounds/pull/5568). +- `@thu-nmrc` supplied [PR #5551](https://github.com/CrocSwap/integer-mult-bounds/pull/5551). +- Retained source notices credit Gareth Davidson, David Arias, Cinna Davis, Jacob Alan Sussman, zxv, and Cao Yifan. +- New commuting-contact cascade construction, proof, and verification by Pierre-Loic Doulcet (`@hexapode`). Apache-2.0. + +## Open next questions + +Independently review the commuting-contact cascade (`Stage A` and `Stage B`) and the inherited helper-endpoint contract, then recompute the complete invoice from `WORD-FIXED-ENDPOINTS.json.gz` and `WORD.json.gz`. Exhaustive commuting-epoch screening on the resulting word leaves zero remaining negative-cost commuting-epoch moves without crossing owned-register `COPY` boundaries (`13401: COPY 737, 146`), so pushing further requires coupling owned-register lifetime timing or multi-register scalar algebraic rewrites. Structured questions are recorded in [TASK.json](TASK.json). diff --git a/research/p104-commuting-contact/RESULT.json b/research/p104-commuting-contact/RESULT.json new file mode 100644 index 0000000000..78a0ea3686 --- /dev/null +++ b/research/p104-commuting-contact/RESULT.json @@ -0,0 +1,387 @@ +{ + "controls": { + "mismatched_commuted_frame": "Scalar destination and coefficient", + "missing_source_transport": "Scalar destination and coefficient", + "non_nested_return": "Scalar destination and coefficient", + "unchanged_word": "Only helper 531 initial frame changes in headline word (597 -> 3)", + "wrong_scalar_coefficient": "All 743 public and owned rows" + }, + "fixed_endpoint_local": { + "endpoint_coefficients": 552049, + "helpers": { + "4": 83, + "5": 5, + "8": 15, + "9": 424 + }, + "owned_lifetimes": 8, + "paid": { + "1": 2207, + "2": 459, + "3": 494, + "4": 90, + "5": 168, + "6": 18, + "7": 14 + }, + "peak_owned_fields": 1, + "public_inputs": 735, + "real_scalar_allowance": 217428 + }, + "fixed_endpoint_raw_interval": [ + "7710388877/2500000000000", + "308415555081/100000000000000" + ], + "fixed_invoice_ceiling": { + "kappa_interval": [ + "0", + "17/5000" + ], + "moment_derivative": [ + "-799900922894856588786300979397572810595897024182819855505172633/3138550867693340381917894711603833208051177722232017256448", + "-186341928116095803919515654269108542645086576446489571024763133/784637716923335095479473677900958302012794430558004314112" + ], + "scope": "This fixed paid and target invoice; the inherited BIT cap is retained." + }, + "inventory": { + "all_main_endpoints_fixed": true, + "events": 25133, + "fixed_endpoint_events": 25136, + "fixed_endpoint_global_paid_delta": { + "1": -72, + "4": -72, + "5": 72 + }, + "fixed_endpoint_local_paid_delta": { + "1": -4, + "4": -4, + "5": 4 + }, + "global_paid_delta": { + "1": -144, + "3": -18, + "4": -36, + "5": 72 + }, + "global_target_delta": { + "8": -18, + "9": 18 + }, + "local_paid_delta": { + "1": -8, + "3": -1, + "4": -2, + "5": 4 + }, + "local_target_delta": { + "8": -1, + "9": 1 + }, + "owned_lifetimes_fixed": true, + "source_events": 25140 + }, + "local": { + "endpoint_coefficients": 552049, + "helpers": { + "4": 83, + "5": 5, + "8": 14, + "9": 425 + }, + "owned_lifetimes": 8, + "paid": { + "1": 2203, + "2": 459, + "3": 493, + "4": 92, + "5": 168, + "6": 18, + "7": 14 + }, + "peak_owned_fields": 1, + "public_inputs": 735, + "real_scalar_allowance": 217428 + }, + "native": { + "distinct_maps": 2918, + "helper_normalizers": 1054, + "helpers": { + "4": 83, + "5": 5, + "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": "e31cbedaa1d6e8e654c29540ce78e58f56278ac68bc621234ddbcc75a3002443", + "wrong_phase_rejected": true + }, + "parent_raw_interval": [ + "154094748433/50000000000000", + "308189496867/100000000000000" + ], + "physical": { + "central_square_columns": 53248, + "full_calls": 18, + "main_targets": { + "145": 208, + "17": 416, + "25": 416, + "33": 416, + "41": 416, + "49": 416, + "57": 416, + "65": 416, + "73": 208 + }, + "new_paid_jobs": 0, + "physical_contacts": 7488, + "ports": 104, + "route_payload_sha256": "7f4f0ca768ffbc4f93dcff575592c4c67411f46b4289e45b73f715a2ad47b142", + "tensor_rule": "Factorwise native maps; scalar signs stay outside the tensor power.", + "whole_idle_jobs": { + "16": 416, + "24": 416, + "32": 416, + "40": 416, + "48": 416, + "56": 416, + "64": 416, + "72": 208 + }, + "wrapper_sites": [ + 1, + 3, + 5, + 7, + 9, + 11, + 13, + 15, + 17, + 19, + 21, + 23, + 25, + 27, + 29, + 31 + ] + }, + "raw_gain_interval": [ + "165779167/50000000000000", + "5180599/1562500000000" + ], + "result": { + "compiler": { + "H": 690116000000000, + "N": "2^690116000000000", + "eta": { + "lower": "0.000000148035649919096176106836", + "upper": "0.000000148035649919096176106837" + }, + "gap": "1/14000000000", + "integer_test_exponent": 49294, + "logarithm_power": 1000, + "theta": "63/64", + "uniform_saving": "21596403/7000000000", + "word_materialized": false + }, + "full_forward_calls": 18, + "gain": "331/100000000", + "kappa": "7713/2500000", + "kappa_decimal": ".00308520", + "margin_at_previous": { + "lower": "0.812592564779117266699646052959", + "upper": "0.812592564779117266699646052960" + }, + "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": 5157000, + "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 6014." + }, + "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": "604699255956807197/196000000000000000000", + "fused_gaussian": "604699255870421591/196000000000000000000", + "global_coordinate_router": "10798201/3500000000", + "group_bit_router": "151174817467605397/49000000000000000000", + "group_scans": "6999999999/7000000000", + "main_transform": "604699241956807197/196000000000000000000", + "microbox_face_corrections": "269500000001/3500000000", + "polynomial_products": "13999999999/14000000000", + "sparse_union_movement": "80229699255956807197/196000000000000000000" + }, + "parameters": { + "a": "10798201/3500000000", + "b": "8638561/2800000000", + "beta": "13999999997/14000000000", + "bit_saving": "17/5000", + "cap_xi": "178229699241956807197/196000000000000000000", + "complex_uniform_saving": "21596403/7000000000", + "d": "1/14000000000", + "epsilon": "13999999999/14000000000", + "kappa": "7713/2500000", + "lambda_": "3987659199/4000000000", + "lambda_prime": "13956807197/14000000000", + "layout": "1/14000000000", + "q": "43192803/14000000000", + "r0": "1/140000000000", + "stop": "1/14000000000", + "tested_saving": "6170401/2000000000" + }, + "strict_checks": { + "actual_bit_above_effective": "1101799/3500000000", + "actual_logarithmic_gamma_guard": "1/14000000000", + "actual_logarithmic_group_guard": "17770300779043192803/98000000000000000000", + "alpha_logarithm_absorption": "1/140000000000", + "boundary_algebraic_matrix_above_kappa": "55956807197/196000000000000000000", + "cap_above_band": "80229699241956807197/196000000000000000000", + "cap_below_cell": "17770300744043192803/196000000000000000000", + "cap_below_phase_cell_power": "213770300758043192803/196000000000000000000", + "complex_above_effective": "1/14000000000", + "complex_below_one_over_32": "78861439/2800000000", + "complex_endpoint": "1/7000000000", + "epsilon_below_one": "1/14000000000", + "epsilon_positive": "13999999999/14000000000", + "fine_prime_halo_umbrella": "7/2", + "fused_gaussian_above_kappa": "55870421591/196000000000000000000", + "gaussian_above_main": "6956807197/98000000000000000000", + "global_coordinate_router_above_kappa": "1/3500000000", + "global_gamma_power_slack": "9/140000000000", + "group_below_dimension": "1/7000000000", + "group_bit_router_above_kappa": "17467605397/49000000000000000000", + "group_gauge_power_slack": "17770300778343192803/98000000000000000000", + "group_key_fits_record": "1/7000000000", + "group_positive": "13999999997/14000000000", + "group_scans_above_kappa": "6978403599/7000000000", + "halo_covers_generic_inverse_radius": "5", + "improvement_over_user_baseline": "677114790400418148631/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": "5591361439/39200000000000000000", + "leaf_saving_above_effective": "2791361439/39200000000000000000", + "main_transform_above_kappa": "41956807197/196000000000000000000", + "membership_arithmetic_fits_record": "1/14000000000", + "microbox_face_corrections_above_kappa": "269489201801/3500000000", + "microbox_halo_volume": "1106000000003/14000000000", + "new_complex_uniform_saving_above_b": "1/14000000000", + "new_semantic_guard_with_C1_one": "1/14000000000", + "polynomial_products_above_kappa": "13956807199/14000000000", + "positive_layout_slack": "1/14000000000", + "q_below_effective": "1/14000000000", + "q_below_internal": "1/14000000000", + "q_below_leaf": "5591361439/39200000000000000000", + "q_positive": "43192803/14000000000", + "short_record_fallback": "2791361439/2800000000", + "source_axis_superpolynomial": "1/14000000000", + "sparse_union_movement_above_kappa": "79625000055956807197/196000000000000000000", + "stop_below_one": "13999999999/14000000000", + "stop_positive": "1/14000000000", + "strassen_integer_power_gap": "1951441519231", + "support_router_span": "3/14000000000", + "theta_positive_polynomial_power": "2", + "union_header_fits_record": "3/14000000000", + "union_tag_work_per_visit_fits_record": "3/14000000000" + } + }, + "paid": { + "1": 41214, + "16": 416, + "2": 8262, + "24": 416, + "3": 8874, + "32": 416, + "4": 1656, + "40": 416, + "48": 416, + "5": 3024, + "56": 416, + "6": 324, + "64": 416, + "7": 252, + "72": 208 + }, + "paid_calls": 66726, + "previous_open_pr5580": "308189/100000000", + "productive_fields": 12814, + "query_shears": 15, + "rank_mass_surplus": 760, + "raw_headroom": [ + "1055201/100000000000000", + "527601/50000000000000" + ], + "raw_root_interval": [ + "308521055201/100000000000000", + "154260527601/50000000000000" + ], + "relative_gain_percent": "33100/308189", + "strictification": { + "alpha": { + "lower": "0.999999989728012798048633869360", + "upper": "0.999999989728012798048633869361" + }, + "cutoff": 17, + "delta": { + "lower": "0.954779111793214281267820227123", + "upper": "0.954779111793214281267820227124" + }, + "floor": 18, + "gamma": { + "lower": "0.967545070726622020281286341642", + "upper": "0.967545070726622020281286341643" + }, + "normalized_paid_upper": "5242880004882813/5242880536870912", + "power": 1024, + "reserve": "1/10000000000", + "tail_offset": "1/5", + "tested": "6170401/2000000000" + }, + "targets": { + "145": 208, + "17": 416, + "25": 416, + "33": 416, + "4": 1494, + "41": 416, + "49": 416, + "5": 90, + "57": 416, + "65": 416, + "73": 208, + "8": 252, + "9": 7650 + }, + "whole_idle_jobs": 3120 + }, + "status": "PASS_P104_COMMUTING_CONTACT_KAPPA_00308520", + "transpose": { + "arithmetic": "Dense integer rows with binary denominators; reverse chronology", + "coefficients": 552049, + "columns": 743 + } +} diff --git a/research/p104-commuting-contact/SOURCES.json b/research/p104-commuting-contact/SOURCES.json new file mode 100644 index 0000000000..a4d5630826 --- /dev/null +++ b/research/p104-commuting-contact/SOURCES.json @@ -0,0 +1,54 @@ +{ + "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-commuting-contact/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/PR5569/PR5580; used UNMODIFIED." + }, + "external_inputs": [ + { + "local_path": "inputs/pr5580-WORD.json.gz", + "source_repository": "aliromman/integer-mult-bounds", + "source_commit": "6efa248cf456d6101d757e9d09ba29711d18a13a", + "source_path": "research/p104-event-contact-step/WORD.json.gz", + "sha256": "b2a98c4bd0dbe86c09e9d15ee060dcf1aab09dbef90aa1e2127676f4039f406b", + "git_blob": "9434855e7dad0d0236d23210b3e71a2b83a9ae64" + }, + { + "local_path": "inputs/pr5580-pricing.py", + "source_repository": "aliromman/integer-mult-bounds", + "source_commit": "6efa248cf456d6101d757e9d09ba29711d18a13a", + "source_path": "research/p104-event-contact-step/pricing.py", + "sha256": "e8ffdadf454639fd434a17e276b062d9d6df8310b1aa0ef15e5fb6a4468d6ba2", + "git_blob": "f8f09be7a16542b924bba903867f71f2a092840f" + }, + { + "local_path": "common.py", + "source_repository": "aliromman/integer-mult-bounds", + "source_commit": "6efa248cf456d6101d757e9d09ba29711d18a13a", + "source_path": "research/p104-event-contact-step/common.py", + "sha256": "e7c1bd9bfc0060d2d55da5c6e61cd3fae756e0fc8facacc2a074061d2f73c800", + "git_blob": "bd244313fc023a737055415f87003f2963c290f6" + } + ], + "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." +} diff --git a/research/p104-commuting-contact/TASK.json b/research/p104-commuting-contact/TASK.json new file mode 100644 index 0000000000..5c032ed644 --- /dev/null +++ b/research/p104-commuting-contact/TASK.json @@ -0,0 +1,125 @@ +{ + "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": "Resolve the open reordered-contact question of PR #5580 on the P104 word: commute four ADD writes into port 198 from helpers 648, 649, 650, 652 before event 13528 to frame 3 (Stage A, fixed endpoints, conditional kappa = 0.00308415), and commute ADD 113 += 531 before event 13524 to frame 3 with helper 531 starting at frame 3 and ADD 197 += 319 demoted from frame 617 to 355 (Stage A+B headline cascade, conditional kappa = 0.00308520).", + "scope_change_reason": "PR #5561, PR #5569 and PR #5580 kept the linear order of all 21,686 scalar operations fixed. Reordering independent ADD operations within commuting read/write epochs vacates intermediate 1-plane and 3-plane stops and reduces total paid calls from 66,852 to 66,726 (-126 paid calls).", + "bottleneck_link": "Stage A replaces 4(H1 + H4) with 4 H5 at each of 18 forward calls (-72 H1 - 72 H4 + 72 H5). Stage B replaces 4 H1 + H3 - 2 H4 in paid transports and upgrades helper 531 from H8 to H9, yielding net local paid delta -8 H1 - H3 - 2 H4 + 4 H5 and target delta -H8 + H9.", + "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": "The exact construction and complete replay pass at conditional kappa = 0.00308520 (tested at 0.0030852005, raw crossing 0.00308521055201..0.00308521055202, +3.31558335e-6 over PR #5580), and the fixed-endpoint supporting word passes with raw crossing 0.00308415555080..0.00308415555081 (+2.26058214e-6 over PR #5580).", + "author": "Pierre-Loic Doulcet (hexapode)", + "ai_assistance": "AI-assisted commuting-epoch DAG analysis, construction, proof and verification.", + "open_questions": [ + { + "question": "Can an independent reviewer accept the contact identity and inherited free-helper-endpoint contract?", + "why_it_matters": "The new paid-profile step is exact, but author-side replay is not independent scientific acceptance.", + "first_step": "Inspect the four source edit sites, unchanged endpoints and the full paid/target census, then run the registered replay.", + "blocked_by": "No missing technical source. Independent scientific review remains pending." + }, + { + "question": "Can a changed event order improve the paid profile beyond this fixed invoice?", + "why_it_matters": "The current raw moment ceiling leaves less than 4.96867e-9 above the claimed endpoint.", + "first_step": "Check live claims, nominate one legal reordered contact window and derive its complete changed invoice.", + "blocked_by": "A new word and full replay are required; the present result proves no optimality for that larger class." + } + ], + "coordination": { + "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/5574", + "base_main": "5e0052ca0aa3036a3afa8b0438927377c8d97d53", + "open_prs_checked": 320, + "discussion_records_checked": 4836, + "remote_pagination_complete": true, + "remote_checked_utc": "2026-10-25T20:04:18.735343+00:00", + "local_coverage": "Sparse; relevant P104 sources read directly. No exhaustive local novelty claim.", + "presubmission_main": "5e0052ca0aa3036a3afa8b0438927377c8d97d53", + "presubmission_checked_utc": "2026-10-25T20:19:42.925159+00:00", + "new_related_pr": "https://github.com/CrocSwap/integer-mult-bounds/pull/5577" + }, + "package": "research/p104-commuting-contact" +} diff --git a/research/p104-commuting-contact/VALIDATION.md b/research/p104-commuting-contact/VALIDATION.md new file mode 100644 index 0000000000..f6d3494f24 --- /dev/null +++ b/research/p104-commuting-contact/VALIDATION.md @@ -0,0 +1,14 @@ +# Verification record + +The source word is PR #5580 (`research/p104-event-contact-step`) at `6efa248cf456d6101d757e9d09ba29711d18a13a`. The base is canonical main `5e0052ca0aa3036a3afa8b0438927377c8d97d53`. The selected record is unchanged. + +The registered warning-strict normal (`-W error -B`) and optimized (`-W error -B -O`) replays both pass and print `PASS_P104_COMMUTING_CONTACT_KAPPA_00308520`. + +Exact checks performed by `verify.py`: +1. SHA256 and Git blob authentication of `inputs/pr5580-WORD.json.gz`, `inputs/pr5580-pricing.py`, `common.py`, and all 33 payloads in `inputs/pr5545-source-closure.tar.gz`. +2. Deterministic regeneration of `WORD-FIXED-ENDPOINTS.json.gz` (25,136 events, local paid delta `-4 H1 - 4 H4 + 4 H5`) and `WORD.json.gz` (25,133 events, local paid delta `-8 H1 - H3 - 2 H4 + 4 H5`, local target delta `-H8 + H9`) from `construct.py`. +3. Arbitrary-input symbolic forward replay (`L.replay`) of the PR #5580 base word, the Stage A fixed-endpoint word, and the Stage A+B headline word across all 743 rows. +4. Dense dyadic reverse-chronology transpose verification (`L.reverse_columns`) across all $743 \times 743 = 552,049$ entries. +5. Exact signed Pauli image and global phase verification (`L.native`) across all 2,918 distinct native chart transitions and 208 free main adapters. +6. Complete physical controller verification (`C.physical`) and dual-moment interval verification (`P.run`) certifying `(0.00308415555080, 0.00308415555081)` for Stage A and `(0.00308521055201, 0.00308521055202)` for Stage A+B (`KAPPA = 0.00308520`, `TESTED = 0.0030852005`, `66,726` paid calls, `12,814` productive fields, surplus `760`). +7. Five negative controls (`missing_source_transport`, `mismatched_commuted_frame`, `wrong_scalar_coefficient`, `non_nested_return`, `unchanged_word`) plus retained native-phase, BIT, and cutoff controls. diff --git a/research/p104-commuting-contact/VERIFY.json b/research/p104-commuting-contact/VERIFY.json new file mode 100644 index 0000000000..66e6ac4e66 --- /dev/null +++ b/research/p104-commuting-contact/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 source bytes and all 33 archive payloads; regenerate both the Stage A fixed-endpoint word and the Stage A+B headline cascade word; replay arbitrary-input endpoints, dense transpose, all 2,918 native maps and the full physical caller; check the complete invoice, two rational moment engines, fixed-invoice derivative, compiler, 58 outer predicates and negative controls; compare the complete receipt." + }, + { + "argv": [ + "{python}", + "-W", + "error", + "-B", + "-O", + "{package}/verify.py" + ], + "timeout_seconds": 540, + "checks": "Authenticate source bytes and all 33 archive payloads; regenerate both the Stage A fixed-endpoint word and the Stage A+B headline cascade word; replay arbitrary-input endpoints, dense transpose, all 2,918 native maps and the full physical caller; check the complete invoice, two rational moment engines, fixed-invoice derivative, compiler, 58 outer predicates and negative controls; compare the complete receipt." + } + ] +} diff --git a/research/p104-commuting-contact/WORD-FIXED-ENDPOINTS.json.gz b/research/p104-commuting-contact/WORD-FIXED-ENDPOINTS.json.gz new file mode 100644 index 0000000000..c8f4da9c66 Binary files /dev/null and b/research/p104-commuting-contact/WORD-FIXED-ENDPOINTS.json.gz differ diff --git a/research/p104-commuting-contact/WORD.json.gz b/research/p104-commuting-contact/WORD.json.gz new file mode 100644 index 0000000000..4ebe6fcb7a Binary files /dev/null and b/research/p104-commuting-contact/WORD.json.gz differ diff --git a/research/p104-commuting-contact/common.py b/research/p104-commuting-contact/common.py new file mode 100644 index 0000000000..bd244313fc --- /dev/null +++ b/research/p104-commuting-contact/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-commuting-contact/construct.py b/research/p104-commuting-contact/construct.py new file mode 100644 index 0000000000..1abbe7659e --- /dev/null +++ b/research/p104-commuting-contact/construct.py @@ -0,0 +1,156 @@ +"""Commuting-write contact cascade on the PR5580 P104 word. + +Pierre-Loic Doulcet (hexapode). Apache-2.0. +The source word is by Ali Romman (PR5580), GamingPuzzled (PR5569), +DreamingOfClouds (PR5561), thu-nmrc (PR5551), and the retained P104 contributors. +""" + +from copy import deepcopy + + +def need(ok, why): + if not ok: + raise ValueError(why) + + +def construct_fixed_endpoints(source): + """Stage A: Commute four ADD writes into port 198 from helpers 648, 649, 650, 652 + before 198's move 3 -> 597 at event 13528, keeping all 735 initial/final frames fixed. + """ + word = deepcopy(source) + old = source['program'] + expected = { + 13528: ['MOVE', 198, 3, 597, False], + 13529: ['ADD', 198, 710, '2', 597], + 13624: ['MOVE', 648, 3, 597, False], + 13625: ['ADD', 198, 648, '1/2', 597], + 13627: ['MOVE', 649, 3, 597, False], + 13628: ['ADD', 198, 649, '-1/2', 597], + 13630: ['MOVE', 650, 3, 597, False], + 13631: ['ADD', 198, 650, '1/2', 597], + 13633: ['MOVE', 652, 3, 597, False], + 13634: ['ADD', 198, 652, '1/2', 597], + 13770: ['MOVE', 648, 597, 120, False], + 13772: ['MOVE', 649, 597, 120, False], + 13774: ['MOVE', 650, 597, 120, False], + 13778: ['MOVE', 652, 597, 120, False], + } + need(len(old) == 25140, 'Exact PR5580 source event count') + need(all(old[i] == e for i, e in expected.items()), 'Exact Stage A source contacts') + replacement = { + 13528: [ + ['ADD', 198, 648, '1/2', 3], + ['ADD', 198, 649, '-1/2', 3], + ['ADD', 198, 650, '1/2', 3], + ['ADD', 198, 652, '1/2', 3], + ['MOVE', 198, 3, 597, False], + ], + 13624: [], + 13625: [], + 13627: [], + 13628: [], + 13630: [], + 13631: [], + 13633: [], + 13634: [], + 13770: [['MOVE', 648, 3, 120, False]], + 13772: [['MOVE', 649, 3, 120, False]], + 13774: [['MOVE', 650, 3, 120, False]], + 13778: [['MOVE', 652, 3, 120, False]], + } + word['program'] = [ + e for i, old_event in enumerate(old) + for e in replacement.get(i, [deepcopy(old_event)]) + ] + need(len(word['program']) == 25136, 'Exact Stage A event count (25136)') + return word + + +def construct(source): + """Full two-group commuting cascade (Stage A + Stage B): + - Stage A: Commute 13625, 13628, 13631, 13634 (on 198 and 648, 649, 650, 652) + before 13528 to frame 3 (0D), vacating 597 (1D) on 648, 649, 650, 652. + - Stage B: Commute 13806 (ADD 113 += 531) before 13524 (MOVE 113: 3 -> 597) to + frame 3 (0D), retime 13843 (ADD 197 += -531) and 14404 (ADD 507 += -531) from + 597 (1D) to 3 (0D) with initial[531] = 3, and demote 13846 (ADD 197 += 319) + from 617 (3D) to 355 (2D), vacating 597 on 531, 197, 507 and vacating 617 on 197, 319. + """ + word = deepcopy(source) + old = source['program'] + expected = { + 13524: ['MOVE', 113, 3, 597, False], + 13525: ['ADD', 113, 710, '2', 597], + 13528: ['MOVE', 198, 3, 597, False], + 13529: ['ADD', 198, 710, '2', 597], + 13624: ['MOVE', 648, 3, 597, False], + 13625: ['ADD', 198, 648, '1/2', 597], + 13627: ['MOVE', 649, 3, 597, False], + 13628: ['ADD', 198, 649, '-1/2', 597], + 13630: ['MOVE', 650, 3, 597, False], + 13631: ['ADD', 198, 650, '1/2', 597], + 13633: ['MOVE', 652, 3, 597, False], + 13634: ['ADD', 198, 652, '1/2', 597], + 13770: ['MOVE', 648, 597, 120, False], + 13772: ['MOVE', 649, 597, 120, False], + 13774: ['MOVE', 650, 597, 120, False], + 13778: ['MOVE', 652, 597, 120, False], + 13806: ['ADD', 113, 531, '1', 597], + 13842: ['MOVE', 197, 3, 597, False], + 13843: ['ADD', 197, 531, '-1', 597], + 13844: ['MOVE', 197, 597, 617, False], + 13845: ['MOVE', 319, 355, 617, False], + 13846: ['ADD', 197, 319, '1', 617], + 14378: ['MOVE', 319, 617, 728, False], + 14403: ['MOVE', 507, 3, 597, False], + 14404: ['ADD', 507, 531, '-1', 597], + 14405: ['MOVE', 507, 597, 728, False], + 14477: ['MOVE', 531, 597, 741, False], + 14684: ['MOVE', 197, 617, 788, False], + } + need(len(old) == 25140, 'Exact PR5580 source event count') + need(source['initial'][531] == 597 and source['final'][531] == 127, 'Exact helper 531 source endpoints') + need(all(old[i] == e for i, e in expected.items()), 'Exact source contacts') + word['initial'][531] = 3 + replacement = { + 13524: [ + ['ADD', 113, 531, '1', 3], + ['MOVE', 113, 3, 597, False], + ], + 13528: [ + ['ADD', 198, 648, '1/2', 3], + ['ADD', 198, 649, '-1/2', 3], + ['ADD', 198, 650, '1/2', 3], + ['ADD', 198, 652, '1/2', 3], + ['MOVE', 198, 3, 597, False], + ], + 13624: [], + 13625: [], + 13627: [], + 13628: [], + 13630: [], + 13631: [], + 13633: [], + 13634: [], + 13770: [['MOVE', 648, 3, 120, False]], + 13772: [['MOVE', 649, 3, 120, False]], + 13774: [['MOVE', 650, 3, 120, False]], + 13778: [['MOVE', 652, 3, 120, False]], + 13806: [], + 13842: [], + 13843: [['ADD', 197, 531, '-1', 3]], + 13844: [['MOVE', 197, 3, 355, False]], + 13845: [], + 13846: [['ADD', 197, 319, '1', 355]], + 14378: [['MOVE', 319, 355, 728, False]], + 14403: [], + 14404: [['ADD', 507, 531, '-1', 3]], + 14405: [['MOVE', 507, 3, 728, False]], + 14477: [['MOVE', 531, 3, 741, False]], + 14684: [['MOVE', 197, 355, 788, False]], + } + word['program'] = [ + e for i, old_event in enumerate(old) + for e in replacement.get(i, [deepcopy(old_event)]) + ] + need(len(word['program']) == 25133, 'Exact cascade event count (25133)') + return word diff --git a/research/p104-commuting-contact/inputs/pr5545-source-closure.tar.gz b/research/p104-commuting-contact/inputs/pr5545-source-closure.tar.gz new file mode 100644 index 0000000000..3084088544 Binary files /dev/null and b/research/p104-commuting-contact/inputs/pr5545-source-closure.tar.gz differ diff --git a/research/p104-commuting-contact/inputs/pr5580-WORD.json.gz b/research/p104-commuting-contact/inputs/pr5580-WORD.json.gz new file mode 100644 index 0000000000..9434855e7d Binary files /dev/null and b/research/p104-commuting-contact/inputs/pr5580-WORD.json.gz differ diff --git a/research/p104-commuting-contact/inputs/pr5580-pricing.py b/research/p104-commuting-contact/inputs/pr5580-pricing.py new file mode 100644 index 0000000000..f8f09be7a1 --- /dev/null +++ b/research/p104-commuting-contact/inputs/pr5580-pricing.py @@ -0,0 +1,156 @@ +"""Complete mixed-target price, compiler and outer transfer. + +The interval and compiler bounds follow zxv and Cao Yifan. The productive +recursion is by Jacob Alan Sussman. The controller is by Cinna Davis. +Adapted from Ali Romman's PR5544/5545 for the two coupled contact changes. +Successor choices prepared for thu-nmrc with substantial OpenAI Codex assistance. +Ali Romman's complete caller/price proof and all predecessor credit are retained. +Apache-2.0. +""" +from collections import Counter +from fractions import Fraction as Q +import local as L + +KAPPA, TESTED = Q('.00308189'), Q('.0030818905') +PREVIOUS = Q('.00308181') + + +def encode(x): + if isinstance(x,Q): + return str(x) + if isinstance(x,dict): + return {str(k):encode(v) for k,v in x.items()} + if isinstance(x,(list,tuple)): + return [encode(v) for v in x] + return x + + +def assemble(local, native, word, physical): + paid, targets = Counter(), Counter() + counts = Counter() + L.need(local['helpers'] == native['helpers'], 'Every productive helper has a native target') + for e in word['physical_events']: + counts[e[0]] += 1 + if e[0] == 'LOCAL': + L.need(e[3] is False, 'Every source invocation is forward') + paid.update(local['paid']) + targets.update(local['helpers']) + elif e[0] == 'QUERY_SHEAR': + paid[1] += 104 + elif e[0] == 'IDLE': + paid[8*len(e[2])] += 208 + main = Counter() + idle = Counter({8*len(e[2]):0 for e in word['physical_events'] if e[0] == 'IDLE'}) + for e in word['physical_events']: + if e[0] == 'IDLE': + idle[8*len(e[2])] += 208 + L.need(idle == physical['whole_idle_jobs'], 'Every whole idle has a native Gaussian and full rank') + for term in word['diagonal']: + main[1+8*sum(term[1:])] += 104 + L.need(main == physical['main_targets'], 'Every main target has its full native phase') + targets.update(main) + L.need(counts['LOCAL'] == 18 and counts['QUERY_SHEAR'] == counts['IDLE'] == 15, 'Complete call census') + # Recount by the two path lengths, without using emitted main diagonals. + second_t = Counter({r:18*n for r,n in local['helpers'].items()}) + second_p = Counter({r:18*n for r,n in local['paid'].items()}) + second_t[145] += 208 + second_p[1] += 15*104 + for length in (7,8): + for j in range(1,length+1): + second_t[1+8*(j+1)] += 208 + second_p[8*(j+1)] += 208 + L.need((targets,paid) == (second_t,second_p), 'Independent full invoice') + L.need(max(targets) == 145 and max(paid) == 72, 'Maximum recursive ranks') + L.need(sum(targets.values()) == 12814 and sum(paid.values()) == 66852, 'Complete field and call counts') + L.need(sum(r*n for r,n in targets.items())-sum(r*n for r,n in paid.items()) == 760, 'Complete rank surplus') + return targets,paid,counts + + +def run(local,native,word,physical): + T,P,counts = assemble(local,native,word,physical) + E = L.load(L.ROOT/'research/higher-moment-strictification/verify.py','p104_productive_intervals') + other = L.load(L.ROOT/'research/kappa-rebuild/architecture/mixed_target_probe.py','p104_productive_second_intervals') + def margin(k): + a,b = E.moment(T,1-k), E.moment(P,1-k) + return a[0]-b[1],a[1]-b[0] + lo,hi,grid = 0,10**12,10**14 + while hi-lo > 1: + m=(lo+hi)//2 + if margin(Q(m,grid))[0] > 0: + lo=m + else: + hi=m + lower,upper = Q(lo,grid),Q(hi,grid) + L.need(margin(lower)[0] > 0 and margin(upper)[1] < 0, 'Strict rational crossing enclosure') + L.need(PREVIOUS < KAPPA < TESTED < lower and margin(PREVIOUS)[0] > 0, 'Changed complete bill improves selected kappa') + t,u,v,c,b = 1-TESTED,Q(1,5),1024,17,18 + target,paid = E.moment(T,t),E.moment(P,t) + tl,th = other.moment(T,TESTED) + pl,ph = other.moment(P,TESTED) + L.need(tl > ph and max(tl,target[0]) <= min(th,target[1]) and max(pl,paid[0]) <= min(ph,paid[1]), 'Two exact moment engines') + alpha = E.divide(paid,target) + gamma = E.divide(E.moment(P,t+u),E.mul(E.power(c,u),target)) + delta = E.divide((Q(sum(T.values())*b),)*2,E.mul(E.power(c,TESTED),target)) + reserve,decay = Q(1,10**10),Q(97,100) + L.need(alpha[1] < 1-reserve and gamma[1] < decay and delta[1] < decay, 'All three charged tail ratios') + L.need(decay**128 < Q(1,16), 'Both tail decay blocks') + normalized = 1/(1+v*reserve)+Q(4,2**32) + L.need(normalized < 1 and c**64 < b**63, 'Full completion, splitting and rounding charges') + theta,power = Q(63,64),1000 + eta = E.scale(E.power(145,-v*TESTED),t) + L.need(2*(c**v)**64 <= (145**v)**63 and eta[0] > theta**power, 'Shifted exits and complement capacity') + L.need(E.power(145,v*TESTED)[1] < 2**power, 'Compiler initial range') + gap = (TESTED-KAPPA)/7 + L.need(gap.numerator == 1, 'Exact compiler integer grid') + step = gap.denominator + def wins(j): + return (step*j+1)**power < 2**j + left,right=1,2 + while not wins(right): + left,right=right,2*right + while right-left > 1: + m=(left+right)//2 + if wins(m): + right=m + else: + left=m + H=step*right + L.need(H > 8*v and wins(right) and not wins(right-1), 'Finite uniform threshold with predecessor rejection') + local_routes = (sum(local['paid'].values())+native['helper_normalizers']+native['main_adapters']+4*104+4*local['owned_lifetimes'])*1000 + L.need(local['real_scalar_allowance']+local_routes < 10**7, 'Every local scalar, route and owned operation is funded') + boundary = sum(len(word['boundaries'][side+'_program']) for side in ('left','right')) + raw = 18*10**7 + 15*1664 + 32*104*(len(word['physical_events'])+boundary) + raw += 32*104*(26+1000) + L.need(raw < 10**9, 'Complete nonrecursive raw bound') + bit = L.read(L.ROOT/'research/query-thinned-controllers/RESULT.json')['ordinary_BIT'] + atom = Q(bit['atom']) + ordinary=(1-atom)*Q(bit['after_cover'])+atom*Q('.0000384599') + admitted=Q(bit['admitted']) + L.need(atom > ordinary > admitted > TESTED and atom < 1-ordinary, 'Retained BIT admission and stock') + outer_module=L.load(L.ROOT/'research/pr4359-p7-padding/dependencies/compiler-refill/endpoint.py','p104_productive_outer') + params={'kappa':KAPPA,'tested_saving':TESTED,'complex_uniform_saving':KAPPA+6*gap, + 'b':KAPPA+5*gap,'a':KAPPA+4*gap,'q':KAPPA+3*gap,'bit_saving':admitted, + 'epsilon':1-gap,'beta':1-3*gap,'r0':gap/10,'stop':gap,'layout':gap,'d':gap} + outer=outer_module.ledger(params) + outer['functional_checks']['actual_new_BIT_stock_sublinear']=params['beta']*(1-atom) + L.need(len(outer['strict_checks']) == 54 and len(outer['functional_checks']) == 4, 'Complete outer predicate inventory') + L.need(all(x > 0 for key in ('strict_checks','functional_checks') for x in outer[key].values()), 'All outer inequalities strict') + wrong_cutoff = E.divide((Q(sum(T.values())*21),)*2,E.mul(E.power(20,TESTED),target)) + L.need(wrong_cutoff[0] > 1, 'Old cutoff fails with this helper inventory') + bad=outer_module.ledger(dict(params,bit_saving=Q('.0027'))) + L.need(any(x <= 0 for x in bad['strict_checks'].values()), 'Insufficient BIT contract rejected') + return encode({'kappa':KAPPA,'kappa_decimal':'.00308189','previous_open_pr5569':PREVIOUS,'gain':KAPPA-PREVIOUS, + 'relative_gain_percent':100*(KAPPA/PREVIOUS-1),'raw_root_interval':[lower,upper], + 'raw_headroom':[lower-KAPPA,upper-KAPPA],'margin_at_previous':E.display(margin(PREVIOUS)), + 'targets':T,'paid':P,'productive_fields':sum(T.values()),'paid_calls':sum(P.values()), + 'rank_mass_surplus':760,'full_forward_calls':18,'query_shears':15,'whole_idle_jobs':3120, + 'strictification':{'tested':TESTED,'power':v,'cutoff':c,'floor':b,'tail_offset':u,'reserve':reserve, + 'alpha':E.display(alpha),'gamma':E.display(gamma),'delta':E.display(delta),'normalized_paid_upper':normalized}, + 'compiler':{'theta':theta,'logarithm_power':power,'eta':E.display(eta),'gap':gap,'H':H,'N':'2^'+str(H), + 'integer_test_exponent':right,'uniform_saving':params['complex_uniform_saving'],'word_materialized':False}, + 'nonrecursive':{'local_scalar':local['real_scalar_allowance'],'local_routes':local_routes, + 'raw_scalar_upper':raw,'raw_budget':10**9,'peak_owned_fields':1, + 'fixed_scalar_growth_bound':'At most 2^(16*26000) before native factors; a declared constant, not an attained norm.', + 'tensor_native_growth_bound':f'Each rank-r Gaussian has row l1 norm at most 2^(rf); sum of local ranks is {sum(r*n for r,n in local["paid"].items())}.'}, + 'ordinary_BIT':bit,'outer':outer, + 'negative_controls':{'old_cutoff':'Rejected by completion-tail ratio greater than one','old_BIT':'Rejected by outer inequalities'}}) diff --git a/research/p104-commuting-contact/pricing.py b/research/p104-commuting-contact/pricing.py new file mode 100644 index 0000000000..a99a3d4676 --- /dev/null +++ b/research/p104-commuting-contact/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-commuting-contact/verify.py b/research/p104-commuting-contact/verify.py new file mode 100644 index 0000000000..b5c189a93f --- /dev/null +++ b/research/p104-commuting-contact/verify.py @@ -0,0 +1,235 @@ +"""Verify the P104 commuting-write contact cascade on the PR5580 word. + +Pierre-Loic Doulcet (hexapode). Apache-2.0. +Retained source notices and predecessor contributors are listed in SOURCES.json. +""" + +from collections import Counter +from copy import deepcopy +from fractions import Fraction as Q +from hashlib import sha1, 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, construct_fixed_endpoints + + +def inventory(base, word_fixed, word): + for key in base: + if key != 'program': + need(word_fixed[key] == base[key], 'Unchanged fixed-endpoint word field: ' + key) + if key not in ('program', 'initial'): + need(word[key] == base[key], 'Unchanged headline word field: ' + key) + need( + [i for i, (a, b) in enumerate(zip(base['initial'], word['initial'])) if a != b] == [531], + 'Only helper 531 initial frame changes in headline word (597 -> 3)' + ) + need(base['initial'][531] == 597 and word['initial'][531] == 3, 'Exact helper 531 initial frame change') + + 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 = bill(base) + after_fixed = bill(word_fixed) + after = bill(word) + delta_fixed = { + r: after_fixed[r] - before[r] + for r in before.keys() | after_fixed.keys() + if after_fixed[r] != before[r] + } + delta = { + r: after[r] - before[r] + for r in before.keys() | after.keys() + if after[r] != before[r] + } + need(delta_fixed == {1: -4, 4: -4, 5: 4}, 'Exact Stage A fixed-endpoint local paid delta') + need(delta == {1: -8, 3: -1, 4: -2, 5: 4}, 'Exact Stage A+B headline local paid delta') + return { + 'source_events': len(base['program']), + 'fixed_endpoint_events': len(word_fixed['program']), + 'events': len(word['program']), + 'fixed_endpoint_local_paid_delta': delta_fixed, + 'fixed_endpoint_global_paid_delta': {r: 18 * n for r, n in delta_fixed.items()}, + 'local_paid_delta': delta, + 'global_paid_delta': {r: 18 * n for r, n in delta.items()}, + 'local_target_delta': {8: -1, 9: 1}, + 'global_target_delta': {8: -18, 9: 18}, + 'all_main_endpoints_fixed': True, + 'owned_lifetimes_fixed': True, + } + + +def controls(L, base, word): + variants = {} + bad = deepcopy(word) + bad['program'].remove(['MOVE', 197, 3, 355, False]) + variants['missing_source_transport'] = bad + + bad = deepcopy(word) + event = next(e for e in bad['program'] if e == ['ADD', 198, 648, '1/2', 3]) + event[-1] = 597 + variants['mismatched_commuted_frame'] = bad + + bad = deepcopy(word) + event = next(e for e in bad['program'] if e == ['ADD', 198, 648, '1/2', 3]) + event[-2] = '1' + variants['wrong_scalar_coefficient'] = bad + + bad = deepcopy(word) + event = next(e for e in bad['program'] if e == ['MOVE', 648, 3, 120, False]) + event[3] = 597 + variants['non_nested_return'] = bad + + rejected = {} + for name, bad_word in variants.items(): + try: + L.replay(bad_word) + except ValueError as error: + rejected[name] = str(error) + else: + raise ValueError('Accepted invalid word: ' + name) + try: + inventory(base, base, base) + except ValueError as error: + rejected['unchanged_word'] = str(error) + else: + raise ValueError('Accepted unchanged word as a profile improvement') + print('PASS contact 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() + need(sha1(header + raw).hexdigest() == pin['git_blob'], 'Source Git object: ' + pin['local_path']) + base = read(HERE / 'inputs/pr5580-WORD.json.gz') + word_fixed = read(HERE / 'WORD-FIXED-ENDPOINTS.json.gz') + word = read(HERE / 'WORD.json.gz') + need(construct_fixed_endpoints(base) == word_fixed, 'Regenerated Stage A fixed-endpoint word payload') + need(construct(base) == word, 'Regenerated full Stage A+B cascade word payload') + inv = inventory(base, word_fixed, word) + + source_price = (HERE / 'inputs/pr5580-pricing.py').read_text() + for before, after in ( + ("KAPPA, TESTED = Q('.00308189'), Q('.0030818905')", + "KAPPA, TESTED = Q('.00308520'), Q('.0030852005')"), + ("PREVIOUS = Q('.00308181')", "PREVIOUS = Q('.00308189')"), + ("'kappa_decimal':'.00308189'", "'kappa_decimal':'.00308520'"), + ("'previous_open_pr5569':PREVIOUS", "'previous_open_pr5580':PREVIOUS"), + ("sum(paid.values()) == 66852", "sum(paid.values()) == 66726"), + ): + 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 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 + parent_local = L.replay(base) + fixed_local = L.replay(word_fixed) + local = L.replay(word) + need(parent_local['helpers'] == fixed_local['helpers'], 'Same helper census on Stage A fixed-endpoint word') + need(local['helpers'] == {9: 425, 4: 83, 5: 5, 8: 14}, 'Exact Stage A+B helper census') + need(parent_local['real_scalar_allowance'] == fixed_local['real_scalar_allowance'] == local['real_scalar_allowance'], 'Same scalar allowance') + rejected = controls(L, base, word) + print('PASS exact arbitrary-input endpoints (base, Stage A fixed-endpoint, Stage A+B headline)', 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', 'commuting_contact_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', 'commuting_contact_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', 'commuting_contact_margin') + targets = {int(r): n for r, n in result['targets'].items()} + paid = {int(r): n for r, n in result['paid'].items()} + parent_targets = dict(targets) + for r, n in inv['global_target_delta'].items(): + parent_targets[r] -= n + parent_paid = dict(paid) + for r, n in inv['global_paid_delta'].items(): + parent_paid[r] -= n + fixed_paid = dict(parent_paid) + for r, n in inv['fixed_endpoint_global_paid_delta'].items(): + fixed_paid[r] += n + + parent_interval = [Q('0.00308189496866'), Q('0.00308189496867')] + 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 PR5580 predecessor crossing') + + fixed_interval = [Q('0.00308415555080'), Q('0.00308415555081')] + fixed_signs = [] + for k in fixed_interval: + t, p = E.moment(parent_targets, 1 - k), E.moment(fixed_paid, 1 - k) + fixed_signs.append((t[0] - p[1], t[1] - p[0])) + need(fixed_signs[0][0] > 0 > fixed_signs[1][1], 'Exact Stage A fixed-endpoint 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 PR5580 raw ceiling') + fixed_ceiling = ceiling(E, targets, paid) + + receipt = P.encode({ + 'status': 'PASS_P104_COMMUTING_CONTACT_KAPPA_00308520', + 'inventory': inv, + 'local': local, + 'fixed_endpoint_local': fixed_local, + 'transpose': reverse, + 'native': native, + 'physical': physical, + 'controls': rejected, + 'parent_raw_interval': parent_interval, + 'fixed_endpoint_raw_interval': fixed_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_COMMUTING_CONTACT_KAPPA_00308520', flush=True) + + +if __name__ == '__main__': + main()