diff --git a/research/z4-typed-window-schedule-seed25ad/NOTICE.md b/research/z4-typed-window-schedule-seed25ad/NOTICE.md new file mode 100644 index 0000000000..da9ee65857 --- /dev/null +++ b/research/z4-typed-window-schedule-seed25ad/NOTICE.md @@ -0,0 +1,30 @@ +# Notice + +Prepared by **Aaron Wang**, with help from opencode (substantial AI +assistance; no independent human review claimed). Apache-2.0; the project +license is retained. + +Pinned predecessor material is loaded unchanged from the repository at base +`0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2` (see SOURCES.json): + +- PR #1391's exact verifier and certificate (Cinna Davis, with OpenAI Codex + assistance), byte-pinned through `research/z4-persistent-pair-seed57/inputs` + (the PR #1410 package's own pins, re-checked before import). +- `research/split-centres-global/proofs/PR386-BIT-GEOMETRY.txt` (the + bit-geometry artifact in [PR 386](https://github.com/CrocSwap/integer-mult-bounds/pull/386) + by Zhihao Chen (jacklightChen, with OpenAI Codex assistance), whose local E8 + bit word is Dylan Crow's from [PR 370](https://github.com/CrocSwap/integer-mult-bounds/pull/370) + (with Anthropic Claude assistance)): the "COPY/ERASE windows remain + sequential and immutable" sentence under test. +- `research/selected-suppliers-de-diagnostic/RESULT.json` (Navinor): the + published `D/E` diagnostic. +- `research/centre-sharing-overhead-budget/RESULT.json` (rtyu193-rgb): the + shared-centre ledger table and sharp overhead budgets. +- `research/z4-distinct-source-seed55/README.md` (Cinna Davis): the + phase-indexed reader family and the boundary recurrence decomposed here. + +Direct predecessor of this task: **PR #2464** +(`research/z4-typed-echo-supplier-instance`), which priced the fused pair and +named the ERASE-deferral obstruction; its declared tape model and priced +baseline are reproduced here from the same pinned emitter. Adjacent same-day +work distinguished: PR #2500, PR #2491, PR #2543, PR #2502. diff --git a/research/z4-typed-window-schedule-seed25ad/README.md b/research/z4-typed-window-schedule-seed25ad/README.md new file mode 100644 index 0000000000..3bf9f9a4c2 --- /dev/null +++ b/research/z4-typed-window-schedule-seed25ad/README.md @@ -0,0 +1,280 @@ +# The ERASE-deferral window question of the fused z4 typed-echo pair + +**KB1b: a legal realization of the pair exists; the ERASE deferral is not +necessary for any whole-construction saving.** PR +https://github.com/CrocSwap/integer-mult-bounds/pull/2464 priced the fused z4 +typed-echo pair (112 primitives / 232 reads / 16,080 travel row steps saved +per fused pair) and stopped on exactly one obligation: the fused pair defers +the first wrapper's ERASE across the second call's window (its exact k=2 +witness: 24 dirty work rows at block-2 entry), while the pinned contract +(`research/split-centres-global/proofs/PR386-BIT-GEOMETRY.txt`, "COPY/ERASE +windows remain sequential and immutable") delivers totals per call. This +package constructs, at the smallest falsifying instance (the k=2 pair, all 56 +basis columns = every dirty state), schedules of the same pair with **per-call +sequential immutable windows and per-call totals delivery** that keep a +positive saving under the full priced budget: **384 records per pair on the +pinned literal window reading and 304 with one bounded, priced typed-window +extension, against the priced 608-record baseline**. The deferral is not the +saving vehicle: at equal window width it buys 0 records at k=2 typed (128 +descriptor bits of call-record bookkeeping) and is 32 records *worse* at k=2 +literal. + +Agent: **Aaron Wang**, with help from opencode (substantial AI assistance; no +independent human review). Task card: [TASK.json](TASK.json) (card +`centre-path-sharing`, scope changed to the assigned kappa-blocker KB1b +request; see the recorded reason). Claim: +[discussion comment](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-18951711). + +## What is actually at stake + +The typed echo composes children `C_i(D,W) = (D + R_i W, P W)` with the +order-four intertwiner `R_i P = Q R_i`; a complete root echo maps +`(D, X, W) -> (D + sum R_i X, X, W)` for arbitrary dirty `D`, `X`, `W`. The +wrapper copies the source into the work rows (`W += X`, the COPY window) and +removes it after the body (`W -= X`, the ERASE window). PR 2464's fusion wraps +both calls of a pair in one window, deferring the first call's ERASE past the +second call's window; the pinned contract keeps one window per call, +sequential and immutable, with the call's totals delivered at its end. + +The question is not whether the *word* is legal — the joint word is an exact +map (reproduced here). The question is whether any schedule that keeps the +contract can keep a saving. This package answers yes, and then shows that the +fusion's own saving decomposes into artifacts. + +## Schedules of the k=2 pair (smallest falsifying instance) + +Declared family: words over the pinned PR #1391 alphabet built from the +certified child words, per-octet work-frame words `P^u`, and window COPY/ERASE +records (one independent source row per work row); each call region is a +sandwich `COPY + body + ERASE + literal inverse(body)`. Two sandwiches = +per-call windows (legal); one sandwich spanning both calls = the ERASE +deferral (PR 2464's fusion). Every schedule below is checked as an exact +integer map on all 56 basis columns with its literal inverse, and the legal +ones additionally check that the state at call a's region end equals call a's +complete echo map exactly (per-call totals delivery, temporary restored). + +| schedule | windows | primitives | reads | travel (row steps) | descriptor bits | storage | +|---|---|---:|---:|---:|---:|---:| +| PR 2464 two separate calls (priced baseline) | per-call, 24 rows | 608 | 1,168 | 53,024 | 9,984 | 4,088 | +| PR 2464 fused pair (the deferral) | one window, 24 rows | 496 | 936 | 36,944 | 8,064 | 4,088 | +| **legal, literal windows** | per-call, 8 rows | **384** | 736 | 32,512 | 6,400 | 4,088 | +| **legal, typed windows (extension)** | per-call, 8 rows | **304** | 584 | 26,128 | 5,120 | 4,088 | +| deferral, typed windows (equal width) | one window, 16 rows | 304 | 584 | 26,128 | 4,992 | 4,088 | +| deferral, literal windows (equal width) | one window, 16 rows | 416 | 792 | 35,488 | 6,784 | 4,088 | + +Saving of the legal schedules against the priced 608-record baseline (the +full priced budget of PR 2464's declared tape model, one machine for all +schedules): **224 primitives / 432 reads / 20,512 travel row steps / 3,584 +descriptor bits** (literal windows), **304 / 584 / 26,896 / 4,864** (typed +windows); storage is unchanged in every schedule. This is a positive saving +on every charged quantity of the whole-construction budget with the contract +intact. + +Three ingredients, each exact: + +1. **Window row selection.** The k=2 calls read disjoint work octets (call a + reads octet 0, call b octet 1), so each call's window only needs its own 8 + rows. The 24-row wrapper copies two octets of source rows that a one-block + call never reads. PR 2464's 48-record "wrapper fusion saving" is exactly + this over-copy on both sides; at equal window width it vanishes. +2. **Typed windows (the one bounded contract extension, priced).** The ERASE + need only remove the copied content *as the typed frame carries it*: at + the call's end the work rows hold `P^s`-rotated content, and the ERASE's + source rows are relabelled by `P^s` (a signed/permuted source list; `P` is + an unsigned permutation, so the records are ordinary ADDs). This absorbs + the boundary frame restoration entirely. Cost of the extension: **0 extra + records, 0 extra descriptor bits**; the literal fallback (frame restored + before a row-aligned ERASE) costs **+80 records per k=2 pair** in + frame-restoration words. +3. **Per-call sandwiches.** Each call is `COPY + body + ERASE + + inverse(body)`, so its totals are final in `D` and its temporary is + restored at its own region end — the contract's per-call delivery, checked + exactly. + +**Witness at block-2 entry** (call b's entry state), both PR 2464's dirty-row +measure and the X-carrying-row measure (work rows carrying un-erased source +content): + +| schedule | X-carrying rows | dirty rows | +|---|---:|---:| +| PR 2464 fused pair | 24 | 24 | +| deferral, typed/literal (row-minimal window) | 16 | 24 | +| legal per-call (typed and literal) | **0** | **0** | + +The named "24 dirty work rows" witness is a window-width artifact: with +per-call windows the first call's ERASE has run and the temporary is restored +*before* the second call opens, so nothing is deferred. + +## What the deferral actually buys + +At equal window width and equal alphabet, the residual fusion saving is: + +- **k=2 typed: 0 records** (128 descriptor bits: one 128-bit call record for + the fused call instead of two). The calls' windows are on disjoint octets; + the deferral shares nothing. +- **k=2 literal: −32 records** (the deferral is *more* expensive; see + RESULT.json). +- **k=5+5 persistent pair (the bounded pivot), typed windows: exactly + `2d = 48` window records** per pair, where `d = 24`: the two calls' windows + share all three work octets, so per-call windows must erase and re-copy the + same 24 source rows at the call boundary while one window pays them once. + This matches a scoped record lower bound: inside the X-reading window + family (one independent source row installed per work row), each call pays + at least `2d` window records, so per-call windows pay at least `4d` per + pair and a single window at least `2d`; the gap `2d = 48` is exactly the + measured window-record residual. The **net** k=5+5 saving is reader-family + dependent: `+48` records for phase-indexed readers (1,456 separate against + 1,408 fused) and `-56` records for fixed readers (1,616 separate against + 1,672 fused), because the fused fixed-reader body pays 264 per-octet + frame-word records against the two separate calls' 160, a 104-record + fusion penalty that more than absorbs the 48 shared-window records. The 48 + window records are the one fusion saving that needs the deferral (or an + ownership-transfer rule), and they are the exact content of the demotion. + +Pivot prices (k=5+5 persistent pair, same priced model): + +| schedule | primitives | reads | travel | descriptor bits | +|---|---:|---:|---:|---:| +| PR 2464 two separate calls (priced baseline) | 2,016 | 3,856 | 150,688 | 32,512 | +| PR 2464 fused pair (the deferral) | 1,904 | 3,624 | 134,608 | 30,592 | +| legal per-call, typed windows, fixed readers | 1,616 | 3,096 | 139,888 | 26,112 | +| legal per-call, typed windows, phase-indexed readers | 1,456 | 2,792 | 127,120 | 23,552 | +| legal per-call, literal windows | 1,984 | 3,776 | 173,632 | 32,000 | +| deferral, typed, phase-indexed readers | 1,408 | 2,696 | 122,944 | 22,656 | + +The phase-indexed reader family is `research/z4-distinct-source-seed55`'s +declared child-contract change (`C_(i,t)(D,W) = (D + Q^(-t) R_i W, P W)`); the +fixed-reader rows use only PR #1391's certified children plus per-octet frame +words, with the exact per-octet gap programs recorded in RESULT.json. The +deferral's 48-record window residual is the same `2d` window row-sharing in +both families; the net saving follows the reader family (`+48` phase-indexed, +`-56` fixed). + +## The 144-primitive saving decomposes too + +`research/z4-distinct-source-seed55` (Cinna Davis) composes two five-child +calls on distinct source banks and reports 1,696 separate vs 1,552 joint, +saving 144. Recomputing its published boundary recurrence exactly gives +`g(5) = 60`, `g(10) = 48`, and the saving is `2 g(5) - g(10) = 72` per +direction, `x2 = 144`: pure **boundary endpoint restoration**, not window +lifetime (its handoff already closes and reopens the windows at the +boundary). With typed windows both sides reach 1,456 and the saving is 0. So +the 144 needs neither the deferral nor fusion; it is the same endpoint +freedom the typed windows give both sides for free. + +## Hosted ledgers and `a < D/E` + +The legal realization keeps per-call windows, hence one centre path per call: +the hosted ledger keeps `n_8 = 1,152`, i.e. the selected histogram, and the +moment is the selected one. Exact rational enclosures (independent atanh/ +Taylor engine, no import of the retained pricing engines), host `m = 73`, +`W = 14,336`, `N = 144`: + +| ledger | D | `a < D/E` | +|---|---:|---:| +| selected baseline (the admitted realization) | 5,120 | 0.0016805907097543218 | +| shared ledger (widened-window variant) | 9,728 | 0.003203836729943888 | + +The baseline `D/E` matches the published +0.001680590709754321699421 to its printing precision (control), and a control +enforces that `D/E` is only a screen (the exact moment at `D/E` exceeds 1 +strictly). The saving that survives is scalar, so the demotion "scalar-only" +is **exact for the moment ledger and only for it**: moving `n_8` (the shared +ledger, and the +3.4536% bit-limited figure of +`research/centre-sharing-overhead-budget`) still requires the widened-window +/ common-sink contract change — consistent with +https://github.com/CrocSwap/integer-mult-bounds/pull/2500's finding that the +typed contract alone does not imply fewer recursive children. + +## Scope, limits, and what is not claimed + +The minimality statements are scoped: the gap programs are exact optima +inside the declared family (per-octet frame words, fixed or phase-indexed +certified children, sandwich windows); the window lower bound is scoped to +X-reading window records. This is not a lower bound for arbitrary ADD/NEG +programs, not a host admission, not a native or hosted emission, not an +all-size/compiler or analytic result, and not a multiplication theorem. The +prefix row-L1 peaks (precision proxy) are 4 for the legal k=2 schedules vs 10 +for PR 2464's fused word, and 16/21 for the pivot's separate/joint +phase-indexed words; the carry's precision envelope is +https://github.com/CrocSwap/integer-mult-bounds/pull/2502's object, not +settled here. The selected record is unchanged; no kappa claim. + +## Reproduce + +Python 3.12+ standard library and `git`, from the repository root: + +```sh +python3 -B research/z4-typed-window-schedule-seed25ad/verify.py +python3 scripts/research_package.py --package research/z4-typed-window-schedule-seed25ad --check-only +``` + +Expected final line: + +```text +PASS_Z4_TYPED_WINDOW_SCHEDULE kb1b legal_literal=384 legal_typed=304 baseline=608 joint=496 witness_x=24_deferred_vs_0_legal pivot_residual=48 controls=73 no_new_kappa +``` + +`--write` regenerates [RESULT.json](RESULT.json); the default run recomputes +and rejects drift. The engine re-checks the pinned PR #1391 emitter and +certificate hashes before importing the word emitter; all other arithmetic +(window content maps, schedules, gap programs, invoices, tape prices, ledger +enclosures) is implemented independently in this package. 73 controls cover +the pinned invoice reproductions (608/496/1008/2016/1904), the intertwiner +identities, every schedule's exact map and literal inverse, per-call delivery +at the boundary, the 24/16/0 witness rows, four window mutants (wrong +relabeling, wrong frame power, omitted ERASE, deferral breaking per-call +delivery), the priced savings and residuals, the pivot gap programs and +prices, the `2d` window lower bound, the seed55 recurrence and its 144 +decomposition, both coverage identities, the published `D/E`, the +`D/E`-is-not-acceptance control, and storage invariance. + +## Open next questions + +- **Does any named selected supplier admit typed (frame-relabelled) COPY/ERASE + windows, and at what charge?** This settles the scalar side: typed windows + remove every boundary frame restoration from the typed echo and make + per-call windows as cheap as the deferring fusion at k=2. First step: + inspect one retained supplier's window definition for whether window source + rows may be scheduled in the typed frame, and price the relabeling + (records, descriptor bits, live families). Blocked by the same named gap as + PR 2464's: no named host child exposes the order-four intertwiner + `R P = Q R`. +- **When two calls' windows share rows (the persistent pair), can the forced + erase-and-re-copy of identical content transfer between sequential windows + at zero record cost?** That `2d`-per-pair item is the only fusion saving + left once windows are typed; it is exactly what the ERASE deferral buys. + First step: ask the contract owner whether a temporary's erased-and-recopied + content may pass between sequential windows, and price the alternative (48 + window records per pair at `d = 24`) against the widened window's extra live + families. Blocked by the pinned sentence ("windows remain sequential and + immutable"; each call's temporary erased within that call). + +## Credit and scope + +Mechanism and certified child family: **PR #1391** and **PR #1410** (Cinna +Davis with OpenAI Codex assistance), extending Ross Richardson's PR #1287 and +Sagar Thakrar's PR #1227; the phase-indexed reader family and the distinct- +source composition are `research/z4-distinct-source-seed55` (Cinna Davis). +The priced whole-construction model, the shared-centre ledgers, the `a < D/E` +diagnostic framing and the named obstruction are **PR #2464**'s (this task's +direct predecessor). The sharp overhead budgets are +`research/centre-sharing-overhead-budget` (rtyu193-rgb); the moment enclosure +technique and the published `D/E` are `research/selected-suppliers-de-diagnostic` +(Navinor) and the pricing model is Douglas Colkitt's +`research/complex-local-word-ceiling`; the immutable-window sentence is the +bit-geometry artifact `PR386-BIT-GEOMETRY.txt` in +[PR 386](https://github.com/CrocSwap/integer-mult-bounds/pull/386) by Zhihao Chen +(jacklightChen, with OpenAI Codex assistance), whose local E8 bit word is Dylan +Crow's from [PR 370](https://github.com/CrocSwap/integer-mult-bounds/pull/370) +(with Anthropic Claude assistance), pinned in +`research/split-centres-global`. Adjacent same-day work is distinguished, not +overlapped: PR #2500 (typed contract vs recursive children), PR #2491 and PR +#2543 (unitary paired cycles for the full dirty reader), PR #2502 (carry +error envelopes). + +New package material is Apache-2.0. Prepared by **Aaron Wang** with help from +opencode (substantial AI assistance in derivation, implementation, checking +and prose); no independent human review or proof-assistant formalization is +claimed. The selected record, upstream files and predecessor packages are +unchanged. diff --git a/research/z4-typed-window-schedule-seed25ad/RESULT.json b/research/z4-typed-window-schedule-seed25ad/RESULT.json new file mode 100644 index 0000000000..3b371fcf81 --- /dev/null +++ b/research/z4-typed-window-schedule-seed25ad/RESULT.json @@ -0,0 +1,550 @@ +{ + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "control_count": 73, + "controls": [ + "phase_cost_table", + "octet_frame_costs", + "intertwiner_Qinv_t_R_P_t_0", + "intertwiner_Qinv_t_R_P_t_1", + "intertwiner_Qinv_t_R_P_t_2", + "intertwiner_Qinv_t_R_P_t_3", + "pr2464_k1_invoice_304", + "pr2464_separate_invoice_608", + "pr2464_joint_invoice_496", + "pr2464_k5_invoice_1008", + "pr2464_k5_pair_invoice_2016", + "pr2464_k10_joint_invoice_1904", + "exact_map_pr2464_k2_joint", + "literal_inverse_pr2464_k2_joint", + "exact_map_pr2464_k5_pair", + "literal_inverse_pr2464_k5_pair", + "k1_literal_gap_cost_20", + "k2_literal_joint_gap_cost_56", + "k2_typed_joint_gap_cost_0", + "exact_map_legal_typed_call_a", + "literal_inverse_legal_typed_call_a", + "exact_map_legal_typed_call_b", + "literal_inverse_legal_typed_call_b", + "exact_map_legal_typed_pair", + "literal_inverse_legal_typed_pair", + "exact_map_legal_min_literal_call_a", + "literal_inverse_legal_min_literal_call_a", + "exact_map_legal_min_literal_pair", + "literal_inverse_legal_min_literal_pair", + "exact_map_joint_typed_pair", + "literal_inverse_joint_typed_pair", + "exact_map_joint_min_literal_pair", + "literal_inverse_joint_min_literal_pair", + "per_call_delivery_at_boundary_legal_typed_pair", + "per_call_delivery_at_boundary_legal_min_literal_pair", + "legal_witness_zero_rows", + "pr2464_witness_24_dirty_rows", + "joint_typed_witness_16_x_rows", + "joint_literal_witness_16_x_rows", + "wrong_erase_relabeling_rejected", + "wrong_erase_power_rejected", + "omitted_erase_rejected", + "deferral_breaks_per_call_delivery", + "legal_literal_positive_saving", + "legal_typed_positive_saving", + "k2_deferral_residual_zero_typed", + "k2_deferral_pessimization_literal", + "typed_extension_price_80", + "exact_map_pivot_separate5_typed_fixed", + "literal_inverse_pivot_separate5_typed_fixed", + "exact_map_pivot_joint10_typed_fixed", + "literal_inverse_pivot_joint10_typed_fixed", + "exact_map_pivot_separate5_typed_phase", + "literal_inverse_pivot_separate5_typed_phase", + "exact_map_pivot_joint10_typed_phase", + "literal_inverse_pivot_joint10_typed_phase", + "exact_map_pivot_separate5_min_literal", + "literal_inverse_pivot_separate5_min_literal", + "pivot_window_sharing_residual_48_phase", + "pivot_legal_beats_priced_baseline", + "pivot_literal_also_beats_priced_baseline", + "window_lower_bound_matches_measured_residual", + "seed55_g5_reproduced_60", + "seed55_g10_reproduced_48", + "seed55_invoices_reproduced", + "seed55_144_is_endpoint_restoration", + "baseline_coverage_identity", + "shared_coverage_identity", + "baseline_D_over_E_matches_published", + "shared_D_over_E_exceeds_baseline", + "D_over_E_is_a_screen_not_acceptance", + "storage_unchanged_legal_typed_pair", + "storage_unchanged_legal_min_literal_pair" + ], + "declared_family": "sandwiches COPY + body + ERASE + literal inverse(body) over the pinned PR1391 children (or seed55's phase-indexed children), per-octet work-frame words P^u, and window COPY/ERASE records with optional typed-frame source relabeling; per-call windows (two sandwiches) versus one window spanning the pair (the ERASE deferral)", + "distinct_source_144_decomposition": { + "E1_5_literal": 848, + "E1_5_typed": 728, + "E2_5_5_literal": 1552, + "E2_5_5_typed": 1456, + "decomposition": "2*g(5) - g(10) = 120 - 48 = 72 per direction, x2 = 144: boundary endpoint restoration, not window lifetime; with typed windows both sides reach 1456 and the saving is 0", + "g10_literal": 48, + "g10_typed": 0, + "g5_literal": 60, + "g5_typed": 0, + "saving_literal": 144, + "saving_typed": 0, + "source": "research/z4-distinct-source-seed55 (phase-indexed children)" + }, + "hosted_ledgers": { + "admitted_realization": "per-call sequential windows keep one centre path per call: n_8 stays 1152 and the ledger moment is the selected baseline (a < D/E above); the shared ledger needs the widened window", + "baseline": { + "D": 5120, + "D_over_E_hi": "160968610544946079445318143167323658305063677319743/95780971304118053647396689196894323976171195136475136", + "D_over_E_lo": "80484305272473039722659071583661829152531838659871/47890485652059026823698344598447161988085597568237568", + "E_hi": "2279697745517583168032536301680066887920711431707044007319/748288838313422294120286634350736906063837462003712", + "E_lo": "36475163928281330688520580826881070206731382907312682366777/11972621413014756705924586149611790497021399392059392" + }, + "baseline_histogram": { + "1": 349604, + "2": 60192, + "3": 62585, + "4": 20448, + "5": 11808, + "7": 7, + "8": 1152, + "48": 4866 + }, + "live_stock_W": 14336, + "shared_k2_histogram": { + "1": 349604, + "2": 60192, + "3": 62585, + "4": 20448, + "5": 11808, + "7": 7, + "8": 576, + "48": 4866 + }, + "shared_widened_window": { + "D": 9728, + "D_over_E_hi": "306866593893834978883114841401737599624288907847049/95780971304118053647396689196894323976171195136475136", + "D_over_E_lo": "38358324236729372360389355175217199953036113480881/11972621413014756705924586149611790497021399392059392", + "E_hi": "2272073901606235161826833324823673133924767607590102362903/748288838313422294120286634350736906063837462003712", + "E_lo": "36353182425699762589229333197178770142796281721441616147129/11972621413014756705924586149611790497021399392059392" + }, + "width_m": 73 + }, + "k2_pair": { + "basis_columns_checked": 56, + "blocks": { + "call_a": [ + 0 + ], + "call_b": [ + 1 + ] + }, + "deferral_residual_equal_windows": { + "literal_records": -32, + "typed_records": 0 + }, + "gap_programs": { + "k1_literal": [ + 20, + { + "0": 3 + } + ], + "k2_literal_joint": [ + 56, + [ + { + "1": 3 + } + ], + { + "0": 2, + "1": 3 + } + ], + "k2_typed_joint": [ + 0, + [ + {} + ] + ] + }, + "invoices_ADD_NEG_total": { + "joint_min_literal_pair": [ + 376, + 40, + 416 + ], + "joint_typed_pair": [ + 280, + 24, + 304 + ], + "legal_min_literal_a": [ + 176, + 16, + 192 + ], + "legal_min_literal_b": [ + 176, + 16, + 192 + ], + "legal_min_literal_pair": [ + 352, + 32, + 384 + ], + "legal_typed_a": [ + 140, + 12, + 152 + ], + "legal_typed_b": [ + 140, + 12, + 152 + ], + "legal_typed_pair": [ + 280, + 24, + 304 + ], + "pr2464_k2_joint": [ + 440, + 56, + 496 + ], + "pr2464_k2_separate": [ + 560, + 48, + 608 + ] + }, + "per_call_totals_delivery": "the state at call a's region end equals call a's complete echo map exactly (56 columns)", + "prefix_row_l1_peak": { + "legal_min_literal_pair": 4, + "legal_typed_pair": 4, + "pivot_joint10_typed_phase": 21, + "pivot_separate5_typed_phase": 16, + "pr2464_k2_joint": 10, + "pr2464_k2_separate": 4 + }, + "price": { + "joint_min_literal_pair": { + "ADD": 376, + "NEG": 40, + "address_travel_row_steps": 35488, + "coefficient_fetches": 416, + "data_storage_cells": 4088, + "descriptor_bits": 6784, + "dispatches": 416, + "instruction_fetches": 416, + "primitives": 416, + "reads": 792, + "writes": 416 + }, + "joint_typed_pair": { + "ADD": 280, + "NEG": 24, + "address_travel_row_steps": 26128, + "coefficient_fetches": 304, + "data_storage_cells": 4088, + "descriptor_bits": 4992, + "dispatches": 304, + "instruction_fetches": 304, + "primitives": 304, + "reads": 584, + "writes": 304 + }, + "legal_min_literal_pair": { + "ADD": 352, + "NEG": 32, + "address_travel_row_steps": 32512, + "coefficient_fetches": 384, + "data_storage_cells": 4088, + "descriptor_bits": 6400, + "dispatches": 384, + "instruction_fetches": 384, + "primitives": 384, + "reads": 736, + "writes": 384 + }, + "legal_typed_pair": { + "ADD": 280, + "NEG": 24, + "address_travel_row_steps": 26128, + "coefficient_fetches": 304, + "data_storage_cells": 4088, + "descriptor_bits": 5120, + "dispatches": 304, + "instruction_fetches": 304, + "primitives": 304, + "reads": 584, + "writes": 304 + }, + "pr2464_k2_joint": { + "ADD": 440, + "NEG": 56, + "address_travel_row_steps": 36944, + "coefficient_fetches": 496, + "data_storage_cells": 4088, + "descriptor_bits": 8064, + "dispatches": 496, + "instruction_fetches": 496, + "primitives": 496, + "reads": 936, + "writes": 496 + }, + "pr2464_k2_separate": { + "ADD": 560, + "NEG": 48, + "address_travel_row_steps": 53024, + "coefficient_fetches": 608, + "data_storage_cells": 4088, + "descriptor_bits": 9984, + "dispatches": 608, + "instruction_fetches": 608, + "primitives": 608, + "reads": 1168, + "writes": 608 + } + }, + "saving_vs_pr2464_priced_baseline": { + "legal_min_literal_pair": { + "ADD": 208, + "NEG": 16, + "address_travel_row_steps": 20512, + "coefficient_fetches": 224, + "data_storage_cells": 0, + "descriptor_bits": 3584, + "dispatches": 224, + "instruction_fetches": 224, + "primitives": 224, + "reads": 432, + "writes": 224 + }, + "legal_typed_pair": { + "ADD": 280, + "NEG": 24, + "address_travel_row_steps": 26896, + "coefficient_fetches": 304, + "data_storage_cells": 0, + "descriptor_bits": 4864, + "dispatches": 304, + "instruction_fetches": 304, + "primitives": 304, + "reads": 584, + "writes": 304 + } + }, + "witness_at_block2_entry_x_carrying_and_dirty_rows": { + "joint_min_literal_pair": [ + 16, + 24 + ], + "joint_typed_pair": [ + 16, + 24 + ], + "legal_min_literal_pair": [ + 0, + 0 + ], + "legal_typed_pair": [ + 0, + 0 + ], + "pr2464_k2_joint": [ + 24, + 24 + ] + } + }, + "obstruction": { + "deferral_residual": "at equal window width the deferral saves 0 records at k=2 typed (disjoint window octets) and is 32 records worse at k=2 literal; at k=5+5 typed it saves exactly 2d = 48 (shared window rows), matching the X-reading window record lower bound", + "demotion_exact_part": "the moment ledger: per-call windows imply per-call centre paths, so n_8 stays 1152 and no kappa change follows without the widened-window/common-sink change", + "extension_priced": "typed windows (COPY/ERASE source rows relabelled by the typed frame path) cost 0 extra records and 0 extra descriptor bits; the literal fallback costs +80 records per k=2 pair (frame restorations)", + "named_obstruction": "PR 2464: the fused pair defers the first wrapper's ERASE across the second call's window", + "outcome": "(a) realized: per-call sequential immutable windows with per-call totals delivery keep a positive whole-construction saving (224 records on the pinned literal reading, 304 with the priced typed-window extension); the deferral is not necessary for any saving" + }, + "pivot_k5k10": { + "gap_programs": { + "k10_typed_fixed_reader": [ + 132, + [ + {}, + {}, + { + "0": 1 + }, + { + "1": 1 + }, + { + "0": 2 + }, + { + "1": 2 + }, + { + "2": 3 + }, + { + "0": 1 + }, + { + "1": 1 + } + ], + { + "0": 0, + "1": 3, + "2": 2 + } + ], + "k5_literal": [ + 132, + [ + { + "1": 3 + }, + { + "2": 2 + }, + { + "0": 1 + }, + { + "1": 1 + } + ], + { + "0": 2, + "1": 3, + "2": 1 + } + ], + "k5_typed_fixed_reader": [ + 40, + [ + {}, + {}, + { + "0": 1 + }, + { + "1": 1 + } + ], + { + "0": 0, + "1": 3, + "2": 2 + } + ] + }, + "price": { + "pivot_joint10_typed_fixed": { + "ADD": 1516, + "NEG": 156, + "address_travel_row_steps": 145048, + "coefficient_fetches": 1672, + "data_storage_cells": 4088, + "descriptor_bits": 26880, + "dispatches": 1672, + "instruction_fetches": 1672, + "primitives": 1672, + "reads": 3188, + "writes": 1672 + }, + "pivot_joint10_typed_phase": { + "ADD": 1288, + "NEG": 120, + "address_travel_row_steps": 122944, + "coefficient_fetches": 1408, + "data_storage_cells": 4088, + "descriptor_bits": 22656, + "dispatches": 1408, + "instruction_fetches": 1408, + "primitives": 1408, + "reads": 2696, + "writes": 1408 + }, + "pivot_pr2464_joint_full": { + "ADD": 1720, + "NEG": 184, + "address_travel_row_steps": 134608, + "coefficient_fetches": 1904, + "data_storage_cells": 4088, + "descriptor_bits": 30592, + "dispatches": 1904, + "instruction_fetches": 1904, + "primitives": 1904, + "reads": 3624, + "writes": 1904 + }, + "pivot_pr2464_separate_full": { + "ADD": 1840, + "NEG": 176, + "address_travel_row_steps": 150688, + "coefficient_fetches": 2016, + "data_storage_cells": 4088, + "descriptor_bits": 32512, + "dispatches": 2016, + "instruction_fetches": 2016, + "primitives": 2016, + "reads": 3856, + "writes": 2016 + }, + "pivot_separate5_min_literal": { + "ADD": 1792, + "NEG": 192, + "address_travel_row_steps": 173632, + "coefficient_fetches": 1984, + "data_storage_cells": 4088, + "descriptor_bits": 32000, + "dispatches": 1984, + "instruction_fetches": 1984, + "primitives": 1984, + "reads": 3776, + "writes": 1984 + }, + "pivot_separate5_typed_fixed": { + "ADD": 1480, + "NEG": 136, + "address_travel_row_steps": 139888, + "coefficient_fetches": 1616, + "data_storage_cells": 4088, + "descriptor_bits": 26112, + "dispatches": 1616, + "instruction_fetches": 1616, + "primitives": 1616, + "reads": 3096, + "writes": 1616 + }, + "pivot_separate5_typed_phase": { + "ADD": 1336, + "NEG": 120, + "address_travel_row_steps": 127120, + "coefficient_fetches": 1456, + "data_storage_cells": 4088, + "descriptor_bits": 23552, + "dispatches": 1456, + "instruction_fetches": 1456, + "primitives": 1456, + "reads": 2792, + "writes": 1456 + } + }, + "window_lower_bound": { + "deferral_only_saving_records": 48, + "per_call_windows_pair_records_min": 96, + "scope": "X-reading COPY/ERASE window records with one independent source row installed per work row; not a lower bound for arbitrary ADD/NEG programs", + "single_window_pair_records_min": 48 + } + }, + "result": "PASS_Z4_TYPED_WINDOW_SCHEDULE", + "schema_version": 1 +} diff --git a/research/z4-typed-window-schedule-seed25ad/SOURCES.json b/research/z4-typed-window-schedule-seed25ad/SOURCES.json new file mode 100644 index 0000000000..89cb019527 --- /dev/null +++ b/research/z4-typed-window-schedule-seed25ad/SOURCES.json @@ -0,0 +1,54 @@ +{ + "schema_version": 1, + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "e8870e5917057d59b730eb14721a778639eca050", + "sha256": "d46eb6d5b3e279428753d770653663fbdf1063e55c255ea073d768f344927ef7" + }, + { + "path": "research/z4-persistent-pair-seed57/inputs/PR1391-verify.py", + "usage": "input", + "git_blob": "9d866bbf57a6d1f012a21687bde2e231c90efd14", + "sha256": "c3d8e76dad9b3cc159affa5e56dbf73612eab0c0ce4a4464f523d4cf47669c05" + }, + { + "path": "research/z4-persistent-pair-seed57/inputs/PR1391-CERTIFICATE.json", + "usage": "input", + "git_blob": "0132b117d90f1a7a97c40af3e38503c117604e00", + "sha256": "2a6ac306ddc6f58514b89f680d8ff3027b4195e2754574f8f04ac1f17785c9d3" + }, + { + "path": "research/split-centres-global/proofs/PR386-BIT-GEOMETRY.txt", + "usage": "input", + "git_blob": "31efe312680fdafba0ccfb630bb6b711acad5944", + "sha256": "c5f077b849e9add9957ab4ee36095dd47bc678dee7e09baa146dac4c0a0d66b2" + }, + { + "path": "research/selected-suppliers-de-diagnostic/RESULT.json", + "usage": "input", + "git_blob": "af8875af8a8b73382180d6f71a3357d613af8046", + "sha256": "731f77e404c18e3c1329d1ad084b3e0e3752579ae83fcb4e48a2b749d405c7a1" + }, + { + "path": "research/centre-sharing-overhead-budget/RESULT.json", + "usage": "input", + "git_blob": "a3758cbd5f157a85e741912783b7203f4061429c", + "sha256": "44fc848b984dbca3aa8ee66898f64f35c305855d0158f1cb4bec0d4d0b28d2b2" + }, + { + "path": "research/z4-distinct-source-seed55/README.md", + "usage": "input", + "git_blob": "485ca1205a7f29f6b1512af7dfddc35a27e1a4f6", + "sha256": "b275de0a626313e33d904071e0becfa33ef4f3472a2a060d83101d159e90e65e" + } + ] +} diff --git a/research/z4-typed-window-schedule-seed25ad/TASK.json b/research/z4-typed-window-schedule-seed25ad/TASK.json new file mode 100644 index 0000000000..a584a0f8bf --- /dev/null +++ b/research/z4-typed-window-schedule-seed25ad/TASK.json @@ -0,0 +1,107 @@ +{ + "schema_version": 1, + "task_id": "centre-path-sharing", + "priority_revision": 4, + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "assignment_seed": "25ad54a0e7bd1aee23a74e39261929b8", + "selected_record_sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32", + "catalog_sha256": "d46eb6d5b3e279428753d770653663fbdf1063e55c255ea073d768f344927ef7", + "original_card": { + "id": "centre-path-sharing", + "question": "Can the 64-per-call centre path (eight rank-8 COPY/ERASE totals through the private temporary) be shared across calls or shrunk?", + "starting_points": [ + "research/complex-local-word-ceiling/README.md", + "research/split-centres-global/proofs/PR386-BIT-GEOMETRY.txt", + "certificates/selected-result.json" + ], + "methods": [ + "Derive a fully charged favorable relaxation for sharing one centre path across k calls, including restoration, hosting and precision.", + "Prove a lower bound on copied information per call for the selected decoder contract." + ], + "acceptance_gate": "Show the changed centre charge and copy profile per call with every added restoration or hosting cost charged, and its ceiling via ceiling.ceiling(centre=...).", + "first_step": { + "command": [ + "python3", + "-B", + "research/complex-local-word-ceiling/verify.py" + ], + "expected": "PASS_COMPLEX_LOCAL_WORD_CEILING", + "inspect": "Read the selected word's per-call local profile, its packing ceiling and the lever table; run levers.py for the ideal budget of the lever you target.", + "scope": "Positive control and planning budget only; this is not a new construction or full cold replay." + }, + "first_experiment": "Write the per-call centre charge and copy children for sharing across k = 2 calls, charge the sharing overhead, and screen it; stop this route if even the ideal sharing gains under 10%. Ideal budgets: free 2.80x, shared by two 1.90x (levers.py).", + "bottleneck_link": "The centre path consumes 64 of about 99.6 unpaid coordinates per call, i.e. about 64% of the raw deficit.", + "allowed_variations": [ + "One sharing pattern across a fixed number of calls.", + "One reduced copied-total contract for the existing decoder.", + "If the coverage law, template or guard changes, derive an applicable fully charged replacement bound instead of applying the incumbent ceiling outside its scope." + ], + "scope_change_triggers": [ + "Removing copies without a replacement contract for the decoder's copied totals." + ], + "overlap_terms": [ + "centre path", + "copied totals", + "private temporary", + "shared centre", + "batching" + ] + }, + "scope_status": "changed", + "scope_change_reason": "The drawn card was bit-new-register-model / bit-helper-contract (drawn track bit-mechanisms, chooser OS nonce 25ad54a0e7bd1aee23a74e39261929b8, SUGGESTIONS_ONLY_NOT_RESERVED). This session takes the explicitly assigned kappa-blocker KB1b request instead: attack the single named obstruction of https://github.com/CrocSwap/integer-mult-bounds/pull/2464 (the first hosted supplier instantiation of the certified z4 typed echo), i.e. the fused pair's deferred first-wrapper ERASE versus the pinned sequential immutable COPY/ERASE window contract (exact k=2 witness: 24 dirty work rows at block-2 entry). Taking an explicit open request from discussion 1166 (comment 18947906, 'Next useful task: find one named supplier owner map admitting a widened COPY/ERASE window with per-pair totals delivery ... and price the widened window as extra live families') in place of the drawn card is the recorded scope change (autoresearch.md section 3; the assignment authorizes it explicitly). The drawn bit cards are also saturated territory on 2026-10-15 (bit-new-register-model and bit-helper-contract carry same-day Q8 / five-SWAP / R439 claims in discussions 1317 and 1166), and one parallel research agent owns the universal f(7) singleton connector question. The package registers under the centre-path-sharing card because that is the lever whose window contract this task prices.", + "actual_scope": "Smallest falsifying instance first: the k=2 typed pair of PR 2464 (two one-child echoes on disjoint work octets, one shared source). Decide the single named obstruction, the COPY/ERASE window-lifetime and per-call totals-delivery contract, in both directions: (a) construct a legal realization of the pair with per-call sequential immutable windows and per-call totals delivery that keeps a positive whole-construction saving under PR 2464's full priced tape budget (schedule, window relabeling, or one bounded contract extension whose cost is priced), or (b) prove the ERASE deferral necessary for every fusion realizing the pair saving. One bounded pivot: the k=5+5 persistent pair, whose two calls share all three work octets, to test the same questions when the calls' windows overlap in rows.", + "bottleneck_link": "PR 2464 priced a complete typed-echo pair saving (112 primitives / 232 reads / 16,080 travel steps per fused pair) and stopped on exactly one obligation: the deferral of the first wrapper's ERASE across the second call's window. If a legal schedule keeps any positive part of that saving, the demotion 'scalar-only under the pinned contract' must be restated; if the deferral is necessary, the demotion becomes exact and the widened-window request can be scoped precisely.", + "budget_minutes": 90, + "cost_model": { + "whole_construction_price_m73": { + "model": "PR 2464's declared model: rows of width 73 on a row-indexed tape; dispatch + instruction fetch + coefficient fetch per record; ADD reads 2 writes 1, NEG reads 1 writes 1; address travel 2*max(src,dst) row steps per record (mutable-source-persistent-connector convention); 16-bit descriptor per record + 128-bit call record; 56*width data cells", + "baseline_pair": "two separate k=1 calls (k=2 pair) priced at 608 primitives per PR 2464's table", + "required_observable_improvement": "any strict positive saving of the legal realization against the 608-primitive priced baseline on the summed charged budget, with every window, restoration, frame and delivery charge included" + }, + "complete_charged_scope": "Mechanism word records + PR 2464's declared tape model + the hosted ledger moment diagnostic (a < D/E) reported unchanged or moved as the windows allow. Not charged: native compilation, tape streaming widths, coefficient magnitudes beyond the prefix row-L1 proxy, all-size/compiler and analytic obligations." + }, + "search_domain": { + "pair_k2": "two one-child echoes, blocks (0,) and (1,), one shared 24-row source, 56 basis columns (every dirty state), all 16 phase paths of the pinned family", + "pivot_k5k10": "two five-child echoes (blocks (0,1,2,0,1)) sharing all three work octets", + "schedule_families": [ + "PR 2464 literal windows (24-row wrapper) and row-minimal windows (only the octets a call's certified reader consumes)", + "window source relabeling by the typed frame path (COPY/ERASE at frame P^s, signed/permuted sources), one bounded contract extension whose cost is priced", + "per-call windows (COPY_i ... ERASE_i sequential, per-call totals delivery) versus one window spanning the pair (the ERASE deferral)" + ], + "arithmetic": "exact integer maps on all basis columns; exact ADD/NEG/read/travel/descriptor invoices; exact rational ln/exp enclosures only if a ledger diagnostic is reported" + }, + "stop_rule": "Stop at the first decisive outcome: a legal realization with a positive priced saving (option (a)) or a necessity result for the deferral inside the searched schedule families (option (b)); record the exact obstruction; at most one bounded pivot (k=5+5); then verify, register and hand off.", + "outcome": "completed", + "evidence": "verify.py and RESULT.json: 73 controls. Option (a) realized at the smallest falsifying instance: the k=2 pair admits per-call sequential immutable windows with per-call totals delivery (state at call a's region end equals call a's complete echo map exactly on all 56 basis columns) at 384 records per pair on the pinned literal window reading and 304 with the priced typed-window extension, against PR 2464's priced 608-record baseline (positive saving on every charged quantity of the full priced budget: 224/432/20512/3584 literal, 304/584/26896/4864 typed; storage unchanged). Witness at block-2 entry: 24 X-carrying/24 dirty rows for PR 2464's fused word, 16/24 for row-minimal deferral windows, 0/0 for the legal schedules. The deferral is not the saving vehicle: 0 records residual at k=2 typed (128 descriptor bits of call-record bookkeeping), -32 at k=2 literal. One bounded pivot (k=5+5 persistent pair, shared window rows): the deferral residual is exactly 2d = 48 records per pair, matching the scoped X-reading window record lower bound; legal per-call typed schedules price 1616 (fixed readers) / 1456 (phase-indexed) against the 2016 baseline. research/z4-distinct-source-seed55's 144-primitive saving decomposes as 2g(5)-g(10) = 72 per direction (boundary endpoint restoration, not window lifetime); with typed windows both sides reach 1456 and the saving is 0. Hosted ledgers: per-call windows keep one centre path per call (n_8 = 1152), baseline D = 5120, a < D/E = 0.0016805907097543218 (published value matched); the widened-window shared ledger D = 9728, a < D/E = 0.003203836729943888. The demotion 'scalar-only' is exact for the moment ledger only.", + "author": "Aaron Wang", + "ai_assistance": "with help from opencode (substantial AI assistance; no independent human review claimed)", + "open_questions": [ + { + "question": "Does any named selected supplier admit typed (frame-relabeled) COPY/ERASE windows, and what does it charge for them?", + "why_it_matters": "Typed windows remove the boundary frame restoration from every typed echo call and make per-call sequential windows as cheap as the deferring fusion at k=2; a named host that prices them would settle the scalar side of the obstruction.", + "first_step": "Inspect one retained supplier's window definition for whether window source rows may be scheduled in the typed frame, and price the relabeling (records, descriptor bits, live families).", + "blocked_by": "No named host child exposes the order-four intertwiner R P = Q R (PR 2464's stated blocker)." + }, + { + "question": "When two calls' windows share rows (the k=5+5 persistent pair), can the forced erase-and-re-copy of identical content be waived by an ownership-transfer rule priced at its record cost?", + "why_it_matters": "That 2d-per-pair item is the only fusion saving left once windows are typed; it is exactly what the ERASE deferral buys.", + "first_step": "Ask the host contract owner whether a temporary's erased-and-recopied content may transfer between sequential windows at zero record cost, and price the alternative (48 records per pair at d=24).", + "blocked_by": "The pinned contract says windows are immutable and each call's temporary is erased within that call." + } + ], + "coordination": { + "claim_status": "posted", + "discussion": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-18951711", + "claim_created_at": "2026-10-15T14:25:00Z", + "claim_expiry": "2026-10-15T16:30:00Z", + "pair_collision_check": "disc-comments with nested replies on discussions 1166 and 1317 at 2026-10-15 14:05-14:12 UTC (no CLAIM on the ERASE-deferral/window object in the recent window; PR 2464's own claim is released), find_overlap.py --refresh at 14:09-14:11 UTC (typed echo / ERASE window / COPY window / fusion schedule / z4 / fused pair / ERASE deferral) and the refined re-run at 15:00-15:03 UTC (typed window / window relabeling / wrapper ERASE / totals delivery / persistent pair / phase-indexed reader / dirty work rows / typed echo window): only this package's own claim and the predecessors PR 2464 and PR 2502 matched. Adjacent same-day work distinguished: PR 2500 (Discussion 2488) audits PR 2464's recursive-children implication, PR 2491/PR 2543 exclude unitary paired cycles for the full dirty reader, PR 2502 prices chronological ADD error envelopes; none takes the window-schedule question.", + "closest_prior": "PR 2464 (research/z4-typed-echo-supplier-instance) names this exact obstruction and prices the fusion; research/z4-distinct-source-seed55 (Cinna Davis) gives the phase-indexed child family and the distinct-source handoff, whose 144-primitive saving this package decomposes; research/z4-persistent-pair-seed57 pins the PR1391 emitter and the persistent pair; research/selected-centre-adjacent-pair-seed01fcb1 censused adjacent call owners; research/split-centres-global/proofs/PR386-BIT-GEOMETRY.txt states the immutable-window sentence." + }, + "selected_record": { + "kappa": "836330098538459/500000000000000000", + "review": "docs/research/community-batch1099-review.md", + "source_manifest": "research/community-frontier1094-audit/SELECTED-SOURCE.json", + "certificate": "research/community-frontier1094-audit/ASSEMBLY.json", + "reproduce": "make frontier1094-verify" + } +} diff --git a/research/z4-typed-window-schedule-seed25ad/VERIFY.json b/research/z4-typed-window-schedule-seed25ad/VERIFY.json new file mode 100644 index 0000000000..4e422bfc1c --- /dev/null +++ b/research/z4-typed-window-schedule-seed25ad/VERIFY.json @@ -0,0 +1,28 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/z4-persistent-pair-seed57/inputs/PR1391-verify.py", + "research/z4-persistent-pair-seed57/inputs/PR1391-CERTIFICATE.json", + "research/split-centres-global/proofs/PR386-BIT-GEOMETRY.txt", + "research/selected-suppliers-de-diagnostic/RESULT.json", + "research/centre-sharing-overhead-budget/RESULT.json", + "research/z4-distinct-source-seed55/README.md", + "certificates/selected-result.json", + "docs/research/agent-task-catalog.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 300, + "checks": "Rebuild PR 2464's typed-echo invoices and words from the pinned PR1391 emitter, construct the legal per-call-window schedules (literal and typed windows) and the deferral comparators at k=2, verify every exact 56-column map and literal inverse, per-call totals delivery at the boundary, the 24/16/0 window witness rows, reject four window mutants, price the whole construction in PR 2464's declared tape model, run the k=5+5 pivot with exact per-octet gap programs and the 2d window lower bound, decompose research/z4-distinct-source-seed55's 144-primitive saving via its published recurrence, and compute both hosted ledgers' a < D/E diagnostics (73 controls)." + } + ] +} diff --git a/research/z4-typed-window-schedule-seed25ad/verify.py b/research/z4-typed-window-schedule-seed25ad/verify.py new file mode 100644 index 0000000000..1998d091c8 --- /dev/null +++ b/research/z4-typed-window-schedule-seed25ad/verify.py @@ -0,0 +1,900 @@ +#!/usr/bin/env python3 +"""KB1b: the COPY/ERASE window question of the fused z4 typed-echo pair. + +Object: the single named obstruction of PR #2464 (research/ +z4-typed-echo-supplier-instance): the fused pair defers the first wrapper's +ERASE across the second call's window (exact k=2 witness: 24 dirty work rows +at block-2 entry) while the pinned contract (research/split-centres-global/ +proofs/PR386-BIT-GEOMETRY.txt) keeps COPY/ERASE windows sequential and +immutable and delivers totals per call. This package decides the question in +both directions: it constructs legal realizations of the pair with per-call +sequential immutable windows and per-call totals delivery (schedule, window +row selection, and one bounded typed-window extension whose cost is priced), +prices every charged quantity of PR #2464's declared tape model, and isolates +the exact residual fusion item (window row-sharing on overlapping pairs) with +a scoped record-count lower bound. + +Declared schedule family: words over the pinned PR #1391 alphabet (ADD/NEG +records) built from the certified child words C_b (fixed readers) or the +phase-indexed children C_(b,t) of research/z4-distinct-source-seed55 (its +declared contract change), per-octet work-frame words P^u, and window +COPY/ERASE records (one independent source row per work row, optionally +relabelled by the typed frame). Call regions are sandwiches COPY + body + +ERASE + literal inverse(body); a fused pair is one sandwich spanning both +calls (the ERASE deferral) and a legal pair is two sandwiches (per-call +windows). Every schedule is checked as an exact integer map on all 56 basis +columns (every dirty state of (D, X, W)) with its literal inverse. + +Smallest falsifying instance first: the k=2 pair (two one-child echoes on +disjoint work octets, one shared source). One bounded pivot: the k=5+5 +persistent pair, whose two calls share all three work octets. + +Exact integer arithmetic and certified rational ln/exp enclosures only. +Standard library only. Prepared by Aaron Wang with help from opencode. +Apache-2.0. +""" + +import hashlib +import importlib.util +import itertools +import json +import sys +from fractions import Fraction as Q +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +BASE = "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2" + +# Pinned predecessor emitter (PR #1391), byte-for-byte as carried by the +# PR #1410 package (research/z4-persistent-pair-seed57/inputs). Hashes are +# the PR #1410 package's own pins, re-checked here before import. +PRE_DIR = ROOT / "research" / "z4-persistent-pair-seed57" / "inputs" +CERT_PATH = PRE_DIR / "PR1391-CERTIFICATE.json" +CODE_PATH = PRE_DIR / "PR1391-verify.py" +PREDECESSOR_CERT_SHA256 = "2a6ac306ddc6f58514b89f680d8ff3027b4195e2754574f8f04ac1f17785c9d3" +PREDECESSOR_CODE_SHA256 = "c3d8e76dad9b3cc159affa5e56dbf73612eab0c0ce4a4464f523d4cf47669c05" + +OW = 8 # output D rows +WW = 24 # source X rows and work W rows (3 octets of 8) +ECHO_WIDTH = OW + WW + WW # 56: D rows 0..8, X rows 8..32, W rows 32..56 +MAPPING = list(range(OW)) + [OW + WW + i for i in range(WW)] +OCT_COST = [0, 20, 16, 20] # octet_word(u) records per work octet + +CONTROLS = [] + + +def require(ok, message): + if not ok: + raise ValueError(message) + + +def control(name, ok, detail): + require(ok, "control failed: " + name + ": " + detail) + CONTROLS.append(name) + + +# -------------------------------------------------------------------------- +# S0. Pinned predecessor emitter +# -------------------------------------------------------------------------- + + +def load_legacy(): + cert_raw = CERT_PATH.read_bytes() + code_raw = CODE_PATH.read_bytes() + require(hashlib.sha256(cert_raw).hexdigest() == PREDECESSOR_CERT_SHA256, + "PR1391 certificate SHA") + require(hashlib.sha256(code_raw).hexdigest() == PREDECESSOR_CODE_SHA256, + "PR1391 verifier SHA") + spec = importlib.util.spec_from_file_location("pr1391_pinned", CODE_PATH) + legacy = importlib.util.module_from_spec(spec) + spec.loader.exec_module(legacy) + return legacy, json.loads(cert_raw) + + +# -------------------------------------------------------------------------- +# S1. Window records and typed-frame relabeling. +# +# A window is a set of work octets; COPY installs one independent source row +# per work row and ERASE removes exactly the installed content. Typed +# windows (the one bounded contract extension priced here) allow the COPY and +# ERASE source rows to be relabelled by the typed frame P^s; literal windows +# fix both to row alignment (the ERASE must then run at frame 0 on its +# octets, which forces the boundary frame-restoration words). +# -------------------------------------------------------------------------- + + +def frame_pre(power): + """Row map of P^power on one octet: (P^s X)[base+j] = X[base+pre[j]]. + P is two disjoint 4-cycles (0,1,2,3) and (4,5,6,7), each (a,b,c,d)->(d,a,b,c).""" + four = [(0, 1, 2, 3), (3, 0, 1, 2), (2, 3, 0, 1), (1, 2, 3, 0)][power % 4] + return four + tuple(4 + x for x in four) + + +def copy_window(legacy, sigma): + """COPY records: W[32+8o+j] += X[8o+pre_{sigma[o]}(j)]. sigma: octet -> s.""" + recs = [] + for o, s in sorted(sigma.items()): + pre = frame_pre(s) + for j in range(8): + recs.append(legacy.add(OW + WW + 8 * o + j, OW + 8 * o + pre[j])) + return recs + + +def x_content_map(legacy, word): + """X-content of every work row from the exact state: [(x_index, sign), ...].""" + state = legacy.apply_word_matrix(word, ECHO_WIDTH) + out = [] + for i in range(WW): + row = state[OW + WW + i] + nz = [(OW + j, row[OW + j]) for j in range(WW) if row[OW + j] != 0] + out.append(nz) + return out + + +def erase_window(legacy, prefix, octets): + """ERASE records: remove exactly the X-content the typed frame leaves in W.""" + content = x_content_map(legacy, prefix) + recs = [] + for o in sorted(octets): + for j in range(8): + r = 8 * o + j + nz = content[r] + require(len(nz) == 1 and nz[0][1] in (-1, 1), + "window row must carry one signed source row") + x_index, sign = nz[0] + recs.append(legacy.add(OW + WW + r, x_index, -sign)) + return recs + + +def gap_word(legacy, gap): + """Per-octet work-frame words: P^u on work octet o for each (o, u).""" + recs = [] + for o, u in sorted(gap.items()): + if u: + recs += list(legacy.lift_word(legacy.octet_word(u), + [OW + WW + 8 * o + j for j in range(8)])) + return recs + + +def child(legacy, block): + return list(legacy.lift_word(legacy.child_word(block), MAPPING)) + + +def child_typed(legacy, block, t): + """Phase-indexed child (research/z4-distinct-source-seed55's declared + family): (D, W) -> (D + Q^(-t) R_block W, P W). Retargeted output rows + only; the child keeps its eight ADDs and 24-coordinate P update.""" + p1 = legacy.expected_octet_frame() + target = legacy.matmul(legacy.matrix_power(p1, (-t) % 4), + legacy.reader_matrix(block)) + recs = [] + for j in range(OW): + hits = [k for k in range(WW) if target[j][k] != 0] + require(len(hits) == 1 and target[j][hits[0]] == 1, + "typed reader must be a selector") + recs.append(legacy.add(j, OW + WW + hits[0])) + recs += list(legacy.lift_word(legacy.workspace_word(1), MAPPING[OW:])) + return recs + + +def inverse_of(legacy, word): + return list(legacy.inverse_word(word)) + + +# -------------------------------------------------------------------------- +# S2. Schedules: per-call windows (legal) versus one window spanning the +# pair (the ERASE deferral), and the per-octet gap programs. +# -------------------------------------------------------------------------- + + +def expected_echo_map(legacy, blocks): + """(D, X, W) -> (D + sum_b R_b X, X, W) as exact integer rows.""" + rows = legacy.identity(ECHO_WIDTH) + for block in blocks: + for j in range(OW): + rows[j][OW + 8 * block + j] += 1 + return rows + + +def call_map_ok(legacy, word, blocks, label): + got = legacy.apply_word_matrix(word, ECHO_WIDTH) + want = expected_echo_map(legacy, blocks) + control("exact_map_" + label, got == want, "map differs on 56 basis columns") + inv = inverse_of(legacy, word) + control("literal_inverse_" + label, + legacy.matmul(legacy.apply_word_matrix(inv, ECHO_WIDTH), got) + == legacy.identity(ECHO_WIDTH), "inverse does not restore") + return got + + +def x_carrying_rows(legacy, word): + return sum(1 for nz in x_content_map(legacy, word) if nz) + + +def dirty_rows(legacy, word): + """PR #2464's witness measure: work rows differing from the identity state.""" + state = legacy.apply_word_matrix(word, ECHO_WIDTH) + return sum(1 for r in range(OW + WW, ECHO_WIDTH) + if any(state[r][c] != (1 if r == c else 0) for c in range(ECHO_WIDTH))) + + +def typed_call(legacy, blocks, octets, sigma, gaps, terminal=None, phase_indexed=False): + """One region: COPY + body + ERASE + literal inverse of the body. + + gaps[i] = {octet: u} frame words between child i and i+1; terminal = + {octet: u} trailing frame word inside the body (literal windows use it to + restore frame 0 before the ERASE). The ERASE is generated from the exact + typed frame at the body exit, so the window always closes inside the + region and the temporary is restored exactly; sigma is the COPY + relabeling. + """ + body = [] + frame = [0, 0, 0] + for i, block in enumerate(blocks): + body += child_typed(legacy, block, frame[block]) if phase_indexed \ + else child(legacy, block) + frame = [f + 1 for f in frame] + if i < len(blocks) - 1: + gap = gaps[i] if i < len(gaps) else {} + body += gap_word(legacy, gap) + for o, u in gap.items(): + frame[o] += u + if terminal: + body += gap_word(legacy, terminal) + word = copy_window(legacy, sigma) + body + word += erase_window(legacy, word, octets) + word += inverse_of(legacy, body) + return word + + +def optimal_gaps(blocks, literal): + """Exact per-octet gap optimum in the declared family. + + Read i sees work octet b at frame i + sum_{j= 1, "ln domain") + if k == 1: + out = (Q(0), Q(0)) + else: + lo, hi = ln_int(k - 1) + a, b = atanh(Q(1, 2 * k - 1)) + out = (down(lo + 2 * a), up(hi + 2 * b)) + _LN[k] = out + return out + + +def ln_ratio(m, r): + lm, um = ln_int(m) + lr, ur = ln_int(r) + return down(lm - ur), up(um - lr) + + +def exp_enc(lo, hi): + require(0 <= lo <= hi <= Q(1, 2), "exp range") + + def series(y, upper): + s, t, k = Q(1), Q(1), 0 + while True: + k += 1 + t = t * y / k + s += t + if t * y < Q(1, 1 << (PREC + 8)): + return up(s + 2 * t * y / (k + 1)) if upper else down(s) + + return series(lo, False), series(hi, True) + + +def child_power(m, r, a): + lo, hi = ln_ratio(m, r) + return exp_enc(a * lo, a * hi) + + +def moment_bill(hist, m, W, a): + lo = hi = Q(0) + for r, n in hist.items(): + e = child_power(m, r, a) + lo += Q(n) * r * e[0] + hi += Q(n) * r * e[1] + return down(lo / (m * W)), up(hi / (m * W)) + + +def de_diagnostic(hist, m, W): + require(all(isinstance(r, int) and 0 < r < m for r in hist), + "child rank outside (0, m)") + mass = sum(n * r for r, n in hist.items()) + D = m * W - mass + lo = hi = Q(0) + for r, n in hist.items(): + l_lo, l_hi = ln_ratio(m, r) + lo += Q(n) * r * l_lo + hi += Q(n) * r * l_hi + require(D > 0, "zero-deficit ledger rejected") + return D, (lo, hi), (down(Q(D) / hi), up(Q(D) / lo)) + + +# -------------------------------------------------------------------------- +# S5. research/z4-distinct-source-seed55 boundary recurrence and the +# decomposition of its 144-primitive saving. +# -------------------------------------------------------------------------- + + +def g_literal(legacy, k): + """seed55's recurrence: entry charge A(t), terminal phase fixed at 0.""" + A = [sum(legacy.word_counts(legacy.workspace_word(r))) for r in range(4)] + f = {t: A[t] for t in range(4)} + for _ in range(k): + f = {s: min(f[t] + A[(s - t - 1) % 4] for t in range(4)) for s in range(4)} + return f[0] + + +def g_typed(legacy, k): + """Typed windows: entry and terminal frames are absorbed by window + relabeling, so only inter-child transitions are charged.""" + A = [sum(legacy.word_counts(legacy.workspace_word(r))) for r in range(4)] + f = {t: 0 for t in range(4)} + for _ in range(k): + f = {s: min(f[t] + A[(s - t - 1) % 4] for t in range(4)) for s in range(4)} + return min(f.values()) + + +# -------------------------------------------------------------------------- +# Main +# -------------------------------------------------------------------------- + + +def build_result(): + legacy, cert = load_legacy() + m_host, W_host = 73, 14336 + + # ---- positive controls: pinned tables and PR #2464's words ----------- + per_octet = [legacy.word_counts(legacy.octet_word(p)) for p in range(4)] + control("phase_cost_table", per_octet == [(0, 0), (18, 2), (12, 4), (18, 2)], + str(per_octet)) + control("octet_frame_costs", [sum(v) for v in per_octet] == OCT_COST, + str([sum(v) for v in per_octet])) + + p1 = legacy.expected_octet_frame() + ws3 = legacy.block_diag([p1] * 3) + for t in range(4): + lhs = legacy.matmul(legacy.matrix_power(p1, (-t) % 4), + legacy.matmul(legacy.reader_matrix(0), + legacy.matrix_power(ws3, t))) + control("intertwiner_Qinv_t_R_P_t_%d" % t, + lhs == legacy.reader_matrix(0), "Q^-t R P^t != R") + + words = {} + words["pr2464_k1_a"] = pr2464_echo_word(legacy, [0, 0], (0,)) + words["pr2464_k2_separate"] = words["pr2464_k1_a"] + pr2464_echo_word(legacy, [0, 0], (1,)) + words["pr2464_k2_joint"] = pr2464_echo_word(legacy, [0, 3, 0], (0, 1)) + words["pr2464_k5"] = pr2464_echo_word(legacy, [0, 1, 2, 3, 0, 0], (0, 1, 2, 0, 1)) + words["pr2464_k5_pair"] = words["pr2464_k5"] + words["pr2464_k5"] + words["pr2464_k10_joint"] = pr2464_echo_word( + legacy, [0, 1, 2, 3, 0, 1, 2, 3, 0, 1, 0], (0, 1, 2, 0, 1, 0, 1, 2, 0, 1)) + inv_counts = {n: legacy.word_counts(w) for n, w in words.items()} + control("pr2464_k1_invoice_304", sum(inv_counts["pr2464_k1_a"]) == 304, + str(inv_counts["pr2464_k1_a"])) + control("pr2464_separate_invoice_608", sum(inv_counts["pr2464_k2_separate"]) == 608, + str(inv_counts["pr2464_k2_separate"])) + control("pr2464_joint_invoice_496", sum(inv_counts["pr2464_k2_joint"]) == 496, + str(inv_counts["pr2464_k2_joint"])) + control("pr2464_k5_invoice_1008", sum(inv_counts["pr2464_k5"]) == 1008, + str(inv_counts["pr2464_k5"])) + control("pr2464_k5_pair_invoice_2016", sum(inv_counts["pr2464_k5_pair"]) == 2016, + str(inv_counts["pr2464_k5_pair"])) + control("pr2464_k10_joint_invoice_1904", sum(inv_counts["pr2464_k10_joint"]) == 1904, + str(inv_counts["pr2464_k10_joint"])) + call_map_ok(legacy, words["pr2464_k2_joint"], (0, 1), "pr2464_k2_joint") + call_map_ok(legacy, words["pr2464_k5_pair"], + (0, 1, 2, 0, 1, 0, 1, 2, 0, 1), "pr2464_k5_pair") + + # ---- the k=2 legal realizations (smallest falsifying instance) ------- + gaps_l_a, term_l_a, cost_l_a = optimal_gaps((0,), True) + gaps_l_ab, term_l_ab, cost_l_ab = optimal_gaps((0, 1), True) + gaps_t_ab, term_t_ab, cost_t_ab = optimal_gaps((0, 1), False) + control("k1_literal_gap_cost_20", cost_l_a == 20, str(cost_l_a)) + control("k2_literal_joint_gap_cost_56", cost_l_ab == 56, str(cost_l_ab)) + control("k2_typed_joint_gap_cost_0", cost_t_ab == 0, str(cost_t_ab)) + + words["legal_typed_a"] = typed_call(legacy, (0,), {0}, {0: 0}, []) + words["legal_typed_b"] = typed_call(legacy, (1,), {1}, {1: 0}, []) + words["legal_typed_pair"] = words["legal_typed_a"] + words["legal_typed_b"] + words["legal_min_literal_a"] = typed_call(legacy, (0,), {0}, {0: 0}, [], + terminal=term_l_a) + words["legal_min_literal_b"] = typed_call(legacy, (1,), {1}, {1: 0}, [], + terminal={1: term_l_a[0]}) + words["legal_min_literal_pair"] = (words["legal_min_literal_a"] + + words["legal_min_literal_b"]) + words["joint_typed_pair"] = typed_call(legacy, (0, 1), {0, 1}, {0: 0, 1: 3}, gaps_t_ab) + words["joint_min_literal_pair"] = typed_call( + legacy, (0, 1), {0, 1}, {0: 0, 1: 0}, gaps_l_ab, terminal=term_l_ab) + + call_map_ok(legacy, words["legal_typed_a"], (0,), "legal_typed_call_a") + call_map_ok(legacy, words["legal_typed_b"], (1,), "legal_typed_call_b") + call_map_ok(legacy, words["legal_typed_pair"], (0, 1), "legal_typed_pair") + call_map_ok(legacy, words["legal_min_literal_a"], (0,), "legal_min_literal_call_a") + call_map_ok(legacy, words["legal_min_literal_pair"], (0, 1), "legal_min_literal_pair") + call_map_ok(legacy, words["joint_typed_pair"], (0, 1), "joint_typed_pair") + call_map_ok(legacy, words["joint_min_literal_pair"], (0, 1), "joint_min_literal_pair") + + # per-call totals delivery: at call a's region end the state is exactly + # call a's complete echo map (totals final in D, temporary restored). + want_a = expected_echo_map(legacy, (0,)) + for name, prefix in (("legal_typed_pair", words["legal_typed_a"]), + ("legal_min_literal_pair", words["legal_min_literal_a"])): + boundary = legacy.apply_word_matrix(prefix, ECHO_WIDTH) + control("per_call_delivery_at_boundary_" + name, boundary == want_a, + "boundary state differs from call a's echo map") + + # witness at block-2 entry (call b's entry state). + witness = {} + for name, prefix in (("legal_typed_pair", words["legal_typed_a"]), + ("legal_min_literal_pair", words["legal_min_literal_a"])): + witness[name] = [x_carrying_rows(legacy, prefix), dirty_rows(legacy, prefix)] + control("legal_witness_zero_rows", witness["legal_typed_pair"] == [0, 0] + and witness["legal_min_literal_pair"] == [0, 0], str(witness)) + + def block2_cut(word): + ins = [i for i, (k2, t, s, sgn) in enumerate(word) + if k2 == "ADD" and OW + WW <= t < OW + 2 * WW and s is not None + and OW <= s < OW + WW and sgn == 1] + c2 = None + for i, (k2, t, s, sgn) in enumerate(word): + if c2 is None and i > max(ins) and t < OW and s is not None \ + and OW + WW + 8 <= s < OW + WW + 16: + c2 = i + break + require(c2 is not None, "block-2 entry located") + return c2 + + for name in ("pr2464_k2_joint", "joint_typed_pair", "joint_min_literal_pair"): + c2 = block2_cut(words[name]) + witness[name] = [x_carrying_rows(legacy, words[name][:c2]), + dirty_rows(legacy, words[name][:c2])] + control("pr2464_witness_24_dirty_rows", witness["pr2464_k2_joint"][1] == WW, + "dirty rows at block-2 entry=" + str(witness["pr2464_k2_joint"])) + control("joint_typed_witness_16_x_rows", + witness["joint_typed_pair"] == [2 * OW, WW], + str(witness["joint_typed_pair"])) + control("joint_literal_witness_16_x_rows", + witness["joint_min_literal_pair"] == [2 * OW, WW], + str(witness["joint_min_literal_pair"])) + + # negative controls: window mutants must fail + body0 = child(legacy, 0) + prefix0 = copy_window(legacy, {0: 0}) + body0 + wrong_p1 = prefix0 + [legacy.add(OW + WW + j, OW + j, -1) for j in range(8)] \ + + inverse_of(legacy, body0) + control("wrong_erase_relabeling_rejected", + legacy.apply_word_matrix(wrong_p1, ECHO_WIDTH) + != expected_echo_map(legacy, (0,)), "row-aligned mid-frame erase accepted") + wrong_p2 = prefix0 + [legacy.add(OW + WW + j, OW + (j + 2) % 8, -1) for j in range(8)] \ + + inverse_of(legacy, body0) + control("wrong_erase_power_rejected", + legacy.apply_word_matrix(wrong_p2, ECHO_WIDTH) + != expected_echo_map(legacy, (0,)), "P^2 erase accepted at frame P") + omit = prefix0 + inverse_of(legacy, body0) + control("omitted_erase_rejected", + legacy.apply_word_matrix(omit, ECHO_WIDTH) + != expected_echo_map(legacy, (0,)), "omitted erase accepted") + c2 = block2_cut(words["joint_typed_pair"]) + boundary_joint = legacy.apply_word_matrix(words["joint_typed_pair"][:c2], ECHO_WIDTH) + control("deferral_breaks_per_call_delivery", + boundary_joint != want_a, + "the joint boundary state must not equal call a's map") + + # ---- whole-construction prices (the full priced budget) -------------- + width = m_host + price = {} + for name, calls in (("pr2464_k2_separate", 2), ("pr2464_k2_joint", 1), + ("legal_typed_pair", 2), ("legal_min_literal_pair", 2), + ("joint_typed_pair", 1), ("joint_min_literal_pair", 1)): + price[name] = physical_price(words[name], width, calls) + control("legal_literal_positive_saving", + price["pr2464_k2_separate"]["primitives"] + - price["legal_min_literal_pair"]["primitives"] == 224, + str(price_delta(price["pr2464_k2_separate"], + price["legal_min_literal_pair"])["primitives"])) + control("legal_typed_positive_saving", + price["pr2464_k2_separate"]["primitives"] + - price["legal_typed_pair"]["primitives"] == 304, + str(price_delta(price["pr2464_k2_separate"], + price["legal_typed_pair"])["primitives"])) + control("k2_deferral_residual_zero_typed", + price["legal_typed_pair"]["primitives"] + - price["joint_typed_pair"]["primitives"] == 0, + "deferral buys nothing at equal typed windows") + control("k2_deferral_pessimization_literal", + price["legal_min_literal_pair"]["primitives"] + - price["joint_min_literal_pair"]["primitives"] == -32, + "at equal literal windows the deferral is more expensive") + control("typed_extension_price_80", + price["legal_typed_pair"]["primitives"] + 80 + == price["legal_min_literal_pair"]["primitives"], + "typed windows cost 0 extra records; literal fallback pays the " + "frame restorations") + + # ---- bounded pivot: the k=5+5 persistent pair (windows share rows) --- + gaps5_t, term5_t, cost5_t = optimal_gaps((0, 1, 2, 0, 1), False) + gaps10_t, term10_t, cost10_t = optimal_gaps((0, 1, 2, 0, 1, 0, 1, 2, 0, 1), False) + gaps5_l, term5_l, cost5_l = optimal_gaps((0, 1, 2, 0, 1), True) + sigma5 = sigma_from_gaps((0, 1, 2, 0, 1), gaps5_t) + sigma10 = sigma_from_gaps((0, 1, 2, 0, 1, 0, 1, 2, 0, 1), gaps10_t) + + call5_fixed = typed_call(legacy, (0, 1, 2, 0, 1), {0, 1, 2}, sigma5, gaps5_t) + words["pivot_separate5_typed_fixed"] = call5_fixed + call5_fixed + words["pivot_joint10_typed_fixed"] = typed_call( + legacy, (0, 1, 2, 0, 1, 0, 1, 2, 0, 1), {0, 1, 2}, sigma10, gaps10_t) + call5_phase = typed_call(legacy, (0, 1, 2, 0, 1), {0, 1, 2}, {0: 0, 1: 0, 2: 0}, + [], phase_indexed=True) + words["pivot_separate5_typed_phase"] = call5_phase + call5_phase + words["pivot_joint10_typed_phase"] = typed_call( + legacy, (0, 1, 2, 0, 1, 0, 1, 2, 0, 1), {0, 1, 2}, {0: 0, 1: 0, 2: 0}, + [], phase_indexed=True) + call5_lit = typed_call(legacy, (0, 1, 2, 0, 1), {0, 1, 2}, + {0: 0, 1: 0, 2: 0}, gaps5_l, terminal=term5_l) + words["pivot_separate5_min_literal"] = call5_lit + call5_lit + for name in ("pivot_separate5_typed_fixed", "pivot_joint10_typed_fixed", + "pivot_separate5_typed_phase", "pivot_joint10_typed_phase", + "pivot_separate5_min_literal"): + call_map_ok(legacy, words[name], (0, 1, 2, 0, 1, 0, 1, 2, 0, 1), name) + + price["pivot_pr2464_separate_full"] = physical_price(words["pr2464_k5_pair"], width, 2) + price["pivot_pr2464_joint_full"] = physical_price(words["pr2464_k10_joint"], width, 1) + for name, calls in (("pivot_separate5_typed_fixed", 2), + ("pivot_joint10_typed_fixed", 1), + ("pivot_separate5_typed_phase", 2), + ("pivot_joint10_typed_phase", 1), + ("pivot_separate5_min_literal", 2)): + price[name] = physical_price(words[name], width, calls) + control("pivot_window_sharing_residual_48_phase", + price["pivot_separate5_typed_phase"]["primitives"] + - price["pivot_joint10_typed_phase"]["primitives"] == 48, + str(price["pivot_separate5_typed_phase"]["primitives"] + - price["pivot_joint10_typed_phase"]["primitives"])) + control("pivot_legal_beats_priced_baseline", + price["pivot_pr2464_separate_full"]["primitives"] + - price["pivot_separate5_typed_phase"]["primitives"] == 560, + str(price["pivot_pr2464_separate_full"]["primitives"] + - price["pivot_separate5_typed_phase"]["primitives"])) + control("pivot_literal_also_beats_priced_baseline", + price["pivot_pr2464_separate_full"]["primitives"] + - price["pivot_separate5_min_literal"]["primitives"] > 0, + str(price["pivot_pr2464_separate_full"]["primitives"] + - price["pivot_separate5_min_literal"]["primitives"])) + + # Window record lower bound inside the X-reading window family: each call + # of the persistent pair installs 24 independent source rows (>= 24 + # X-reading ADDs) and removes them (>= 24 ERASE ADDs), so per-call windows + # pay >= 4d per pair while one window spanning the pair pays >= 2d. The + # gap 2d = 48 records is exactly the deferral-only saving measured above. + window_lower_bound = { + "per_call_windows_pair_records_min": 4 * WW, + "single_window_pair_records_min": 2 * WW, + "deferral_only_saving_records": 2 * WW, + "scope": "X-reading COPY/ERASE window records with one independent " + "source row installed per work row; not a lower bound for " + "arbitrary ADD/NEG programs", + } + control("window_lower_bound_matches_measured_residual", + window_lower_bound["deferral_only_saving_records"] + == price["pivot_separate5_typed_phase"]["primitives"] + - price["pivot_joint10_typed_phase"]["primitives"], + "counting bound != measured residual") + + # ---- research/z4-distinct-source-seed55's 144, decomposed ------------ + gl5, gl10 = g_literal(legacy, 5), g_literal(legacy, 10) + gt5, gt10 = g_typed(legacy, 5), g_typed(legacy, 10) + control("seed55_g5_reproduced_60", gl5 == 60, str(gl5)) + control("seed55_g10_reproduced_48", gl10 == 48, str(gl10)) + T = 68 + e1_lit = 2 * 5 * T + 2 * WW + 2 * gl5 + e2_lit = 2 * 10 * T + 4 * WW + 2 * gl10 + e1_typ = 2 * 5 * T + 2 * WW + 2 * gt5 + e2_typ = 2 * 10 * T + 4 * WW + 2 * gt10 + control("seed55_invoices_reproduced", (e1_lit, e2_lit) == (848, 1552), + "E1=%d E2=%d" % (e1_lit, e2_lit)) + control("seed55_144_is_endpoint_restoration", + 2 * e1_lit - e2_lit == 144 and 2 * e1_typ == e2_typ, + "literal saving=%d typed E1=%d E2=%d" % (2 * e1_lit - e2_lit, e1_typ, e2_typ)) + seed55 = { + "source": "research/z4-distinct-source-seed55 (phase-indexed children)", + "g5_literal": gl5, "g10_literal": gl10, + "g5_typed": gt5, "g10_typed": gt10, + "E1_5_literal": e1_lit, "E2_5_5_literal": e2_lit, + "E1_5_typed": e1_typ, "E2_5_5_typed": e2_typ, + "saving_literal": 2 * e1_lit - e2_lit, + "saving_typed": 2 * e1_typ - e2_typ, + "decomposition": "2*g(5) - g(10) = 120 - 48 = 72 per direction, x2 = 144: " + "boundary endpoint restoration, not window lifetime; with " + "typed windows both sides reach 1456 and the saving is 0", + } + + # ---- hosted ledgers: a < D/E diagnostics ------------------------------ + hist_base = {1: 349604, 2: 60192, 3: 62585, 4: 20448, 5: 11808, 7: 7, 8: 1152, + 48: 4866} + hist_shared = dict(hist_base) + hist_shared[8] = 576 + mass_base = sum(n * r for r, n in hist_base.items()) + mass_shared = sum(n * r for r, n in hist_shared.items()) + control("baseline_coverage_identity", m_host * W_host - mass_base == W_host - 64 * 144, + "D=%d" % (m_host * W_host - mass_base)) + control("shared_coverage_identity", m_host * W_host - mass_shared == W_host - 32 * 144, + "D=%d" % (m_host * W_host - mass_shared)) + D_b, E_b, DE_b = de_diagnostic(hist_base, m_host, W_host) + D_s, E_s, DE_s = de_diagnostic(hist_shared, m_host, W_host) + published_de = Q("0.001680590709754321699421") + control("baseline_D_over_E_matches_published", + abs(DE_b[0] - published_de) < Q(1, 10 ** 24) + and abs(DE_b[1] - published_de) < Q(1, 10 ** 24), + "distance check: [%s, %s]" % (DE_b[0], DE_b[1])) + control("shared_D_over_E_exceeds_baseline", DE_s[0] > DE_b[1], + "shared=%s baseline=%s" % (DE_s[0], DE_b[1])) + control("D_over_E_is_a_screen_not_acceptance", + moment_bill(hist_base, m_host, W_host, DE_b[1])[0] > 1, + "f(D/E) must exceed 1 strictly") + + for name in ("legal_typed_pair", "legal_min_literal_pair"): + control("storage_unchanged_" + name, + price[name]["data_storage_cells"] + == price["pr2464_k2_separate"]["data_storage_cells"], "storage moved") + + l1 = {n: legacy.prefix_row_l1_peak(words[n], ECHO_WIDTH) + for n in ("pr2464_k2_separate", "pr2464_k2_joint", "legal_typed_pair", + "legal_min_literal_pair", "pivot_separate5_typed_phase", + "pivot_joint10_typed_phase")} + + inv_all = {n: list(legacy.word_counts(w)) + [len(w)] for n, w in words.items()} + + return { + "schema_version": 1, + "base_commit": BASE, + "result": "PASS_Z4_TYPED_WINDOW_SCHEDULE", + "declared_family": "sandwiches COPY + body + ERASE + literal inverse(body) " + "over the pinned PR1391 children (or seed55's phase-indexed " + "children), per-octet work-frame words P^u, and window " + "COPY/ERASE records with optional typed-frame source " + "relabeling; per-call windows (two sandwiches) versus one " + "window spanning the pair (the ERASE deferral)", + "k2_pair": { + "blocks": {"call_a": [0], "call_b": [1]}, + "basis_columns_checked": ECHO_WIDTH, + "gap_programs": {"k1_literal": [cost_l_a, term_l_a], + "k2_literal_joint": [cost_l_ab, gaps_l_ab, term_l_ab], + "k2_typed_joint": [cost_t_ab, gaps_t_ab]}, + "invoices_ADD_NEG_total": {n: inv_all[n] for n in inv_all + if n.startswith(("pr2464_k2", "legal_", "joint_"))}, + "witness_at_block2_entry_x_carrying_and_dirty_rows": witness, + "per_call_totals_delivery": "the state at call a's region end equals " + "call a's complete echo map exactly (56 columns)", + "price": {n: price[n] for n in price if not n.startswith("pivot_")}, + "saving_vs_pr2464_priced_baseline": { + "legal_min_literal_pair": price_delta(price["pr2464_k2_separate"], + price["legal_min_literal_pair"]), + "legal_typed_pair": price_delta(price["pr2464_k2_separate"], + price["legal_typed_pair"]), + }, + "deferral_residual_equal_windows": { + "typed_records": price["legal_typed_pair"]["primitives"] + - price["joint_typed_pair"]["primitives"], + "literal_records": price["legal_min_literal_pair"]["primitives"] + - price["joint_min_literal_pair"]["primitives"], + }, + "prefix_row_l1_peak": l1, + }, + "pivot_k5k10": { + "gap_programs": {"k5_typed_fixed_reader": [cost5_t, gaps5_t, sigma5], + "k10_typed_fixed_reader": [cost10_t, gaps10_t, sigma10], + "k5_literal": [cost5_l, gaps5_l, term5_l]}, + "price": {n: price[n] for n in price if n.startswith("pivot_")}, + "window_lower_bound": window_lower_bound, + }, + "distinct_source_144_decomposition": seed55, + "hosted_ledgers": { + "width_m": m_host, "live_stock_W": W_host, + "baseline_histogram": hist_base, "shared_k2_histogram": hist_shared, + "baseline": { + "D": D_b, + "D_over_E_lo": str(DE_b[0]), "D_over_E_hi": str(DE_b[1]), + "E_lo": str(E_b[0]), "E_hi": str(E_b[1]), + }, + "shared_widened_window": { + "D": D_s, + "D_over_E_lo": str(DE_s[0]), "D_over_E_hi": str(DE_s[1]), + "E_lo": str(E_s[0]), "E_hi": str(E_s[1]), + }, + "admitted_realization": "per-call sequential windows keep one centre path " + "per call: n_8 stays 1152 and the ledger moment is " + "the selected baseline (a < D/E above); the shared " + "ledger needs the widened window", + }, + "obstruction": { + "named_obstruction": "PR 2464: the fused pair defers the first wrapper's " + "ERASE across the second call's window", + "outcome": "(a) realized: per-call sequential immutable windows with " + "per-call totals delivery keep a positive whole-construction " + "saving (224 records on the pinned literal reading, 304 with " + "the priced typed-window extension); the deferral is not " + "necessary for any saving", + "deferral_residual": "at equal window width the deferral saves 0 records " + "at k=2 typed (disjoint window octets) and is 32 " + "records worse at k=2 literal; at k=5+5 typed it " + "saves exactly 2d = 48 (shared window rows), " + "matching the X-reading window record lower bound", + "extension_priced": "typed windows (COPY/ERASE source rows relabelled by " + "the typed frame path) cost 0 extra records and 0 " + "extra descriptor bits; the literal fallback costs " + "+80 records per k=2 pair (frame restorations)", + "demotion_exact_part": "the moment ledger: per-call windows imply per-call " + "centre paths, so n_8 stays 1152 and no kappa " + "change follows without the widened-window/" + "common-sink change", + }, + "controls": CONTROLS, + "control_count": len(CONTROLS), + } + + +def main(): + sys.stdout.reconfigure(encoding="utf-8") + result = build_result() + out = HERE / "RESULT.json" + if "--write" in sys.argv: + out.write_text(json.dumps(result, indent=1, sort_keys=True) + "\n", encoding="utf-8") + else: + require(out.exists(), "RESULT.json missing; run with --write first") + stored = json.loads(out.read_text(encoding="utf-8")) + require(stored == json.loads(json.dumps(result)), + "RESULT.json drift: rerun --write after review") + k2 = result["k2_pair"] + print("PASS_Z4_TYPED_WINDOW_SCHEDULE kb1b " + "legal_literal=%d legal_typed=%d baseline=%d joint=%d " + "witness_x=%d_deferred_vs_0_legal pivot_residual=%d controls=%d no_new_kappa" + % (k2["price"]["legal_min_literal_pair"]["primitives"], + k2["price"]["legal_typed_pair"]["primitives"], + k2["price"]["pr2464_k2_separate"]["primitives"], + k2["price"]["pr2464_k2_joint"]["primitives"], + k2["witness_at_block2_entry_x_carrying_and_dirty_rows"] + ["pr2464_k2_joint"][0], + result["pivot_k5k10"]["window_lower_bound"]["deferral_only_saving_records"], + result["control_count"])) + + +if __name__ == "__main__": + main()