From f364b97ff4700147fc06e622b79952b9fe6c4fa8 Mon Sep 17 00:00:00 2001 From: Aaron Wang Date: Thu, 15 Oct 2026 07:31:42 -0400 Subject: [PATCH 1/2] KB1 supplier instantiation of the certified z4 typed echo: priced whole construction, exact moments and a < D/E, one hosting obstruction (no new kappa) --- .../z4-typed-echo-supplier-instance/NOTICE.md | 15 + .../z4-typed-echo-supplier-instance/README.md | 246 ++++++ .../RESULT.json | 319 ++++++++ .../SOURCES.json | 84 ++ .../z4-typed-echo-supplier-instance/TASK.json | 113 +++ .../VERIFY.json | 33 + .../z4-typed-echo-supplier-instance/verify.py | 720 ++++++++++++++++++ 7 files changed, 1530 insertions(+) create mode 100644 research/z4-typed-echo-supplier-instance/NOTICE.md create mode 100644 research/z4-typed-echo-supplier-instance/README.md create mode 100644 research/z4-typed-echo-supplier-instance/RESULT.json create mode 100644 research/z4-typed-echo-supplier-instance/SOURCES.json create mode 100644 research/z4-typed-echo-supplier-instance/TASK.json create mode 100644 research/z4-typed-echo-supplier-instance/VERIFY.json create mode 100644 research/z4-typed-echo-supplier-instance/verify.py diff --git a/research/z4-typed-echo-supplier-instance/NOTICE.md b/research/z4-typed-echo-supplier-instance/NOTICE.md new file mode 100644 index 0000000000..1c804d39cc --- /dev/null +++ b/research/z4-typed-echo-supplier-instance/NOTICE.md @@ -0,0 +1,15 @@ +This package's own files (verify.py, README.md, TASK.json, SOURCES.json, +RESULT.json) are original work prepared by Aaron Wang with help from opencode, +released under Apache-2.0 (see the repository LICENSE). + +The pinned predecessor emitter and certificate loaded at runtime from +`research/z4-persistent-pair-seed57/inputs/` are PR #1391 material (Cinna +Davis, with OpenAI Codex assistance), carried unchanged and byte-pinned in +`SOURCES.json`. Retain that package's `NOTICE.md` and `LICENSE` for the +imported predecessor material. The PR #1410 persistent-pair result +(`research/z4-persistent-pair-seed57`) supplies the certified joint-echo +invoices reproduced here; the moment enclosure technique follows +`research/selected-suppliers-de-diagnostic` (Navinor) and +`research/complex-local-word-ceiling` (Douglas Colkitt), both reimplemented +rather than imported. Substantial AI assistance is disclosed above; no +independent human review is claimed. diff --git a/research/z4-typed-echo-supplier-instance/README.md b/research/z4-typed-echo-supplier-instance/README.md new file mode 100644 index 0000000000..2ebd3eb145 --- /dev/null +++ b/research/z4-typed-echo-supplier-instance/README.md @@ -0,0 +1,246 @@ +# z4 typed echo as a supplier instance: priced, and blocked in one obligation + +**Supplier instantiation of a certified mechanism; no new kappa and no change to +the selected record.** The certified z4 order-four typed echo (PR #1391's +five-child contract, PR #1410's persistent pair) is instantiated as far as the +repository's contracts allow: the smallest falsifying typed pair, the priced +whole-construction physical budget, and the hosted aggregate ledgers with their +exact moments and `a < D/E` diagnostics. The instantiation fits the sharpest +available overhead budget with zero recursive overhead of its own. It is +blocked in exactly one obligation, **hosting**: the named host's contract keeps +`COPY/ERASE` windows sequential and immutable and delivers totals per call, +while the typed echo must defer the first wrapper's restoration across the +second call's window. Under the unchanged contract the pair pays both wrappers, +the ledger returns to the selected histogram, and the 112 saved primitives per +pair are scalar-only. + +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 KB1 request; +see the recorded reason). Claim: +[discussion comment](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-18947139). + +## The mechanism, rebuilt and falsified at the smallest instance + +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 +boundary schedule costs `g(k)`; this package re-derives it by an independent +dynamic program and checks it against the pinned brute force: + +| children k | 1 | 2 | 3 | 5 | 10 | +|---:|---:|---:|---:|---:|---:| +| boundary g(k) | 60 | 88 | 116 | 140 | 248 | + +**Smallest falsifying instance first: the `k = 2` typed pair.** Two one-child +echoes on children 0 and 1, fused into one two-child echo. All `4^2 = 16` phase +paths enumerated; the minimum is `g(2) = 88`. The joint word, the two separate +words and their sequential composition agree exactly as integer maps on all 56 +basis columns, which by linearity is every dirty state of `(D, X, W)`; the +literal reversed word is an exact inverse. Three schedule mutants (wrong first +output phase, omitted terminal gap, forward word substituted for the inverse) +all produce different maps and are rejected. + +Complete invoices (ADD, NEG), reproduced from the pinned predecessor numbers: + +| schedule | ADD | NEG | total | comparison | +|---|---:|---:|---:|---| +| five-child echo | 920 | 88 | 1,008 | eager 1,328 (PR #1391) | +| ten-child joint echo | 1,720 | 184 | 1,904 | two separate 2,016 (PR #1410) | +| two-child joint echo | 440 | 56 | 496 | two separate 608 (this package) | + +Prefix row-L1 peaks (the precision proxy of the predecessor packages) are 4 at +`k = 1`, 10 at `k = 2`, 20 at `k = 5`, 30 for two separate five-child calls and +42 for the joint ten-child call, reproducing PR #1410's 30/42 exactly. + +## Priced whole-construction budget + +The predecessor packages price primitives, reads and writes, and leave +"address travel, coefficient fetches and descriptor storage" unpriced. Declared +model (one machine, both schedules priced in it): rows of width 73 on a +row-indexed tape; one dispatch, one instruction fetch and one coefficient fetch +per record; ADD reads two rows and writes one, NEG reads and writes one; address +travel is `2 * max(source, target)` row-index steps per record, the +visit-source/visit-target/return convention of +`research/mutable-source-persistent-connector`; descriptor storage is 16 bits +per record plus one 128-bit call record; data storage is `56 * width` cells. + +| quantity | two separate calls (k=2) | joint k=2 | saving per pair | +|---|---:|---:|---:| +| primitives | 608 | 496 | 112 | +| dispatches | 608 | 496 | 112 | +| instruction fetches | 608 | 496 | 112 | +| coefficient fetches | 608 | 496 | 112 | +| reads | 1,168 | 936 | 232 | +| writes | 608 | 496 | 112 | +| address travel (row steps) | 53,024 | 36,944 | 16,080 | +| descriptor bits | 9,984 | 8,064 | 1,920 | +| data storage cells | 4,088 | 4,088 | 0 | + +The `k = 5+5` versus `k = 10` pair has identical savings. The saving is real at +every charged level of this model except storage, and it is scalar: no charged +quantity in the moment ledger moves. + +## Hosted ledgers, exact moments, and `a < D/E` + +The named host is the binding selected complex ledger (width `m = 73`, live +stock `W = 14,336`, `N = 144` calls, published histogram, no surcharge). The +typed echo applied to consecutive same-source call pairs is the shared-centre +ledger of `research/centre-sharing-overhead-budget`: the shared rank-8 centre +children go from 1,152 to 576 and the coverage identity from `72W + 64N` to +`72W + 32N`. Exact rational enclosures (independent atanh/Taylor engine, no +import of the retained pricing engines): + +| ledger | rank mass | D | `a < D/E` | exact moment root `a*` | +|---|---:|---:|---:|---| +| selected baseline | 1,041,408 | 5,120 | 0.0016805907097543218 | [0.001675462676, 0.001675462677] | +| shared k=2 typed echo | 1,036,800 | 9,728 | 0.003203836729943888 | [0.003185242415, 0.003185242416] | + +The baseline `D/E` matches the published 0.001680590709754321699421 to 2.4e-25 +(printing precision) and the baseline root is the recorded complex endpoint +0.0016754626768081035, whose moment residual sits in the published +`-1.30e-24` band; the next `10^-24` grid point is rejected. At the recorded bit +endpoint 0.0017334270395898442 the shared ledger gives `f(a) - 1 = -4.25e-3`, +matching `research/centre-sharing-overhead-budget`'s table entry for `k = 2`. +So with sharing the complex side stops binding and the whole bound becomes +bit-limited at `kappa = 0.001730427469823602` (+3.4536% on the selected +0.001672660197076918), which is that package's published figure, here reached +by a concrete mechanism rather than a relaxation. + +**`a < D/E` is a screen, not the acceptance test** (a control enforces this: +the exact moment at `D/E` exceeds 1 strictly). The exact moments above are the +acceptance tests. + +## Delta-H: the instantiation fits the sharpest overhead budget + +`research/centre-sharing-overhead-budget` prices the sharing lever's overhead +`Delta-H` as extra paid children: sharing saves 32 rank units per call, and the +overhead must stay under about 30.5-30.8 units per call to keep the full ++3.4536% gain, or 31.9-32.0 for any gain. The typed echo eliminates one +wrapper per pair: 8 rank-8 children, 64 rank units per pair, 32 per call. Its +own added work is scalar (frame powers, the two 24-ADD copy edges, the boundary +schedule), so its recursive overhead is 0 rank units and the elimination lands +entirely inside the budget. The measured scalar side also falls (table above). + +## The one obstruction: hosting (window lifetime and totals delivery) + +The fused pair defers the first call wrapper's `W -= X` (the ERASE analogue) +past the second call's child block. The smallest instance exhibits it exactly: +in the `k = 2` joint word all 24 work rows are dirty at the second block's +entry, where the separate schedule has already restored. The named host's +pinned contract, `research/split-centres-global/proofs/PR386-BIT-GEOMETRY.txt`, +states that `COPY/ERASE` windows remain sequential and immutable, and the +coverage identity charges one centre path per call because each call's totals +are copied out and its private temporary erased within that call. The typed +carry needs the opposite: one window spanning the pair, the first call's totals +delivered at the pair end, and uninterrupted ownership of the temporary across +the boundary. + +Everything else is charged and closes: + +- **Moment:** the shared ledger above, with `Delta-H` inside the sharp budget. +- **Scalar price:** fully paid, and smaller than the separate schedule. +- **Dirty state and restoration:** exact on all 56 basis columns. +- **Precision:** quantified but not closed (see the open questions); the carry + raises prefix row-L1 from 30 to 42 at the persistent pair. + +Under the unchanged contract the pair pays both wrappers: the histogram stays +`n_8 = 1152`, the moment is exactly the selected one, and no kappa change +follows from 112 saved primitives. The contract change would also require a +child exposing the order-four intertwiner `R P = Q R` (the certified typed +contract; no named host child exposes one) and a common sink for the pair's +totals, the first blocker of PR #1748. + +The source-bound side of the same obstruction is already recorded on the named +schedule: `research/selected-centre-adjacent-pair-seed01fcb1` censused all 143 +adjacent ordered call pairs of the pinned selected 144-call schedule and found +no pair sharing a single physical owner among its eight centre source rows, so +no adjacent pair meets even a zero-transport shared-source boundary. That +census leaves aliases, copied values, nontrivial linear maps between owners, +nonadjacent calls and a changed schedule open; those escapes are paid owner or +chart transport, which is this same hosting obligation. This package does not +rerun that census; it adds the window-lifetime and delivery side at the word +level and prices the mechanism. + +**Bounded pivot (one): the single-call realization.** Make the pair one +supplier call from the start, so its single window stays sequential and +immutable. The per-call totals-delivery contract then makes the fused call copy +both calls' totals: 16 rank-8 children per pair, 128 rank units, exactly the +two-wrapper baseline. The ledger returns to the selected histogram and the +moment is identical (checked exactly). Delivering one shared set of totals +instead is the same common-sink contract change the obstruction names, so the +pivot does not escape the obligation. The route stops here. + +## Reproduce + +Python 3.12+ standard library and `git`, from the repository root: + +```sh +python3 -B research/z4-typed-echo-supplier-instance/verify.py +python3 scripts/research_package.py --package research/z4-typed-echo-supplier-instance --check-only +``` + +Expected final line: + +```text +PASS_Z4_TYPED_ECHO_SUPPLIER_INSTANCE smallest_k2 whole_price saved=112 D_over_E_shared=306866593893834978883114841401737599624288907847049/95780971304118053647396689196894323976171195136475136 controls=51 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 +(boundary recurrence, maps, invoices, tape model, ledger moments, `ln`/`exp` +enclosures) is implemented independently in this package. 51 controls cover the +mechanism reproductions, the smallest-instance map and inverse identities, +three schedule mutants, the wrapper counts and the deferred-restoration +witness, the whole-price dispatch charges, the row-L1 reproduction, both +coverage identities, the published `D/E` and moment-residual bands, the +`D/E`-is-not-acceptance control, the `Delta-H` budget fit, the pivot's +identical moment, and three mutated-ledger rejections. + +**Not checked:** any native or hosted emission, the registered 3.12 replay +environment beyond this file's commands, the complex host's precision bucket +law, all-size/compiler, common-label/mutable-source realization, tape, +analytic transfer and the bit H1-H5 obligations. This is not a multiplication +theorem and does not admit any supplier. + +## Open next questions + +- **Does a named selected supplier admit a widened `COPY/ERASE` window with + per-pair totals delivery?** This is the single contract change the + instantiation needs; the shared ledger would then accept at `a* = 0.0031852` + and move the binding side to the bit primitive. First step: inspect one + retained supplier's owner-map window definitions and totals schedule for a + consecutive same-sink pair, and price the widened window as extra live + families. Blocked by the pinned immutable-window sentence and the absence of + a child exposing `R P = Q R`. +- **Can a named host price the carry's precision envelope?** The measured cost + is the prefix row-L1 rise 30 to 42. First step: propagate the joint word's + exact prefix coefficient envelope through a host's fixed precision buckets + (the 192/512-bit conventions used in the bit invoice). Blocked by the complex + host's bucket law not being pinned in a chargeable form. + +## Credit and scope + +Mechanism and certified invoices: **PR #1391** (order-four paired frames) and +**PR #1410** (persistent pair), both by Cinna Davis with OpenAI Codex +assistance, extending Ross Richardson's PR #1287 and Sagar Thakrar's PR #1227; +the heterogeneous variants are PR #1768 and PR #2098. The shared-centre +scalar-macro halves are **PR #1708** (1337isnot1337) and **PR #1748** +(ToikY). The lever's sharp overhead budgets and the bit-limited kappa figure +are `research/centre-sharing-overhead-budget` (rtyu193-rgb); the adjacent-pair +owner census is `research/selected-centre-adjacent-pair-seed01fcb1`; 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` with PR #1012's coverage identity. The +immutable-window sentence is from the PR #386 bit geometry (Dylan Crow lineage) +as pinned in `research/split-centres-global`. The tape convention is +`research/mutable-source-persistent-connector` (woklerx). The task-draw scope +change and its reason are recorded in [TASK.json](TASK.json); the pair-collision +check and overlap refresh are recorded there and in the claim. + +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-echo-supplier-instance/RESULT.json b/research/z4-typed-echo-supplier-instance/RESULT.json new file mode 100644 index 0000000000..f3d190d7dc --- /dev/null +++ b/research/z4-typed-echo-supplier-instance/RESULT.json @@ -0,0 +1,319 @@ +{ + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "control_count": 51, + "controls": [ + "phase_cost_table", + "g5_reproduces_pr1391", + "g10_reproduces_pr1410", + "g2_is_the_smallest_pair_boundary", + "dp_agrees_with_pinned_brute_k5", + "dp_agrees_with_pinned_brute_k3", + "canonical_path_is_optimal_k5", + "canonical_path_is_optimal_k10", + "exhaustive_census_matches_dp_k2", + "exhaustive_census_matches_dp_k5", + "k5_echo_invoice_1008", + "k10_joint_invoice_1904", + "two_separate_k5_invoice_2016", + "two_separate_k1_invoice", + "k2_joint_invoice_496", + "k5_eager_invoice_1328", + "exact_map_k2_joint", + "exact_map_k1_a", + "exact_map_k1_b", + "exact_map_k5_joint", + "exact_map_k10_joint", + "k2_joint_equals_sequential_composition", + "literal_inverse_k2_joint", + "literal_inverse_k5_joint", + "wrong_first_output_phase_rejected", + "omitted_terminal_gap_rejected", + "forward_for_inverse_rejected", + "joint_word_has_one_wrapper", + "separate_words_have_two_wrappers", + "deferred_restoration_witness_at_smallest_instance", + "whole_price_primitives_positive", + "dispatch_charge_is_not_free", + "persistent_pair_row_l1_matches_pr1410", + "row_l1_charge_is_not_free", + "baseline_coverage_identity", + "shared_coverage_identity", + "baseline_D_over_E_matches_published", + "shared_D_over_E_exceeds_baseline", + "baseline_accepts_recorded_endpoint", + "baseline_rejects_next_grid_point", + "baseline_residual_matches_published_magnitude", + "shared_accepts_bit_endpoint_with_published_margin", + "D_over_E_overestimates_the_root", + "baseline_root_tracks_recorded_endpoint", + "delta_h_fits_sharp_budget", + "both_wrappers_keep_selected_histogram", + "pivot_single_call_delivery_returns_baseline_ledger", + "pivot_moment_identical_to_baseline", + "histogram_mutation_breaks_coverage_identity", + "child_rank_outside_0_m_rejected", + "zero_deficit_ledger_rejected" + ], + "hosted_ledgers": { + "baseline": { + "D": 5120, + "D_over_E_hi": "160968610544946079445318143167323658305063677319743/95780971304118053647396689196894323976171195136475136", + "D_over_E_lo": "80484305272473039722659071583661829152531838659871/47890485652059026823698344598447161988085597568237568", + "E_hi": "2279697745517583168032536301680066887920711431707044007319/748288838313422294120286634350736906063837462003712", + "E_lo": "36475163928281330688520580826881070206731382907312682366777/11972621413014756705924586149611790497021399392059392", + "moment_at_complex_endpoint": [ + "95780971304118053647396564277883365209759359443725985/95780971304118053647396689196894323976171195136475136", + "95780971304118053647396564277883365209759359443725987/95780971304118053647396689196894323976171195136475136" + ], + "moment_root_hi": "1675462677/1000000000000", + "moment_root_lo": "418865669/250000000000", + "rank_mass": 1041408 + }, + "baseline_histogram": { + "1": 349604, + "2": 60192, + "3": 62585, + "4": 20448, + "5": 11808, + "7": 7, + "8": 1152, + "48": 4866 + }, + "delta_h_budget": { + "eliminated_rank_units_per_pair": 64, + "fits": true, + "sharp_budget_any_gain_units_per_pair": "64", + "sharp_budget_full_gain_units_per_pair": "308/5", + "typed_echo_recursive_overhead_units": 0 + }, + "live_stock_W": 14336, + "shared_k2": { + "D": 9728, + "D_over_E_hi": "306866593893834978883114841401737599624288907847049/95780971304118053647396689196894323976171195136475136", + "D_over_E_lo": "38358324236729372360389355175217199953036113480881/11972621413014756705924586149611790497021399392059392", + "E_hi": "2272073901606235161826833324823673133924767607590102362903/748288838313422294120286634350736906063837462003712", + "E_lo": "36353182425699762589229333197178770142796281721441616147129/11972621413014756705924586149611790497021399392059392", + "moment_at_bit_endpoint": [ + "95373878511347614136401418458557602426842690595871071/95780971304118053647396689196894323976171195136475136", + "95373878511347614136401418458557602426842690595871073/95780971304118053647396689196894323976171195136475136" + ], + "moment_root_hi": "199077651/62500000000", + "moment_root_lo": "637048483/200000000000", + "rank_mass": 1036800 + }, + "shared_k2_histogram": { + "1": 349604, + "2": 60192, + "3": 62585, + "4": 20448, + "5": 11808, + "7": 7, + "8": 576, + "48": 4866 + }, + "width_m": 73 + }, + "mechanism": { + "exhaustive_census": { + "2": { + "min_total": 88, + "paths": 16 + }, + "5": { + "min_total": 140, + "paths": 1024 + } + }, + "g_boundary_paths": { + "1": [ + 0, + 0 + ], + "10": [ + 0, + 1, + 2, + 3, + 0, + 1, + 2, + 3, + 0, + 1, + 0 + ], + "2": [ + 0, + 1, + 0 + ], + "3": [ + 0, + 1, + 2, + 0 + ], + "5": [ + 0, + 1, + 2, + 3, + 0, + 0 + ] + }, + "g_boundary_total": { + "1": 60, + "10": 248, + "2": 88, + "3": 116, + "5": 140 + }, + "invoices_ADD_NEG": { + "k10_joint": [ + 1720, + 184 + ], + "k1_a": [ + 280, + 24 + ], + "k1_b": [ + 280, + 24 + ], + "k2_joint": [ + 440, + 56 + ], + "k2_separate": [ + 560, + 48 + ], + "k5_eager": [ + 1208, + 120 + ], + "k5_joint": [ + 920, + 88 + ] + } + }, + "obstruction": { + "obligation": "hosting: COPY/ERASE window-lifetime and per-call delivery", + "pinned_contract": "research/split-centres-global/proofs/PR386-BIT-GEOMETRY.txt: 'COPY/ERASE windows remain sequential and immutable'", + "pivot": "single-call realization: the per-call totals-delivery contract makes the fused call copy both calls' totals (16 rank-8 children per pair, 128 units), exactly the two-wrapper baseline; the ledger returns to the selected histogram and the moment is unchanged. Sharing one set of totals needs the same common-sink/window contract change.", + "pivots_tested": 1, + "smallest_instance_witness": "the k=2 joint word defers the first wrapper's copy-out past the second child block; all 24 work rows are dirty at the second block's entry", + "unchanged_contract_price": "both wrappers paid: n_8 stays 1152 and the moment is identical to the selected ledger" + }, + "result": "PASS_Z4_TYPED_ECHO_SUPPLIER_INSTANCE", + "schema_version": 1, + "smallest_falsifying_instance": { + "basis_columns_checked": 56, + "deferred_restoration_dirty_work_rows": 24, + "joint_blocks": [ + 0, + 1 + ], + "joint_equals_sequential_composition": true, + "phase_paths_enumerated": 16, + "separate_calls": [ + [ + 0 + ], + [ + 1 + ] + ] + }, + "whole_construction_price": { + "k10_joint": { + "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 + }, + "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 + }, + "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 + }, + "k5_separate_pair": { + "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 + }, + "model": "rows of width 73 on a row-indexed tape; dispatch, instruction fetch and coefficient fetch per record; ADD reads 2 writes 1, NEG reads 1 writes 1; address travel 2*max(src,dst) per record; 16-bit descriptor per record + 128-bit call record; 56*width data cells", + "pair_saving_k2": { + "ADD": 120, + "NEG": -8, + "address_travel_row_steps": 16080, + "coefficient_fetches": 112, + "data_storage_cells": 0, + "descriptor_bits": 1920, + "dispatches": 112, + "instruction_fetches": 112, + "primitives": 112, + "reads": 232, + "writes": 112 + }, + "pair_saving_k5k10": { + "ADD": 120, + "NEG": -8, + "address_travel_row_steps": 16080, + "coefficient_fetches": 112, + "data_storage_cells": 0, + "descriptor_bits": 1920, + "dispatches": 112, + "instruction_fetches": 112, + "primitives": 112, + "reads": 232, + "writes": 112 + }, + "prefix_row_l1_peak": { + "k10_joint": 42, + "k1_a": 4, + "k2_joint": 10, + "k5_joint": 20, + "k5_separate_pair_concat": 30 + } + } +} diff --git a/research/z4-typed-echo-supplier-instance/SOURCES.json b/research/z4-typed-echo-supplier-instance/SOURCES.json new file mode 100644 index 0000000000..6d642c76ab --- /dev/null +++ b/research/z4-typed-echo-supplier-instance/SOURCES.json @@ -0,0 +1,84 @@ +{ + "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/community-frontier1094-audit/ASSEMBLY.json", + "usage": "input", + "git_blob": "5fd676df060f3b450782fdf5ff5f6beb63a5eeb0", + "sha256": "1122cb3a575f8c788345fc1bf4c108ac7c3250fb81a5988671f5eb04b3ab3045" + }, + { + "path": "research/z4-paired-frame-restoration-seed56/CERTIFICATE.json", + "usage": "input", + "git_blob": "0132b117d90f1a7a97c40af3e38503c117604e00", + "sha256": "2a6ac306ddc6f58514b89f680d8ff3027b4195e2754574f8f04ac1f17785c9d3" + }, + { + "path": "research/z4-persistent-pair-seed57/inputs/PR1391-CERTIFICATE.json", + "usage": "input", + "git_blob": "0132b117d90f1a7a97c40af3e38503c117604e00", + "sha256": "2a6ac306ddc6f58514b89f680d8ff3027b4195e2754574f8f04ac1f17785c9d3" + }, + { + "path": "research/z4-persistent-pair-seed57/inputs/PR1391-verify.py", + "usage": "input", + "git_blob": "9d866bbf57a6d1f012a21687bde2e231c90efd14", + "sha256": "c3d8e76dad9b3cc159affa5e56dbf73612eab0c0ce4a4464f523d4cf47669c05" + }, + { + "path": "research/z4-persistent-pair-seed57/RESULT.json", + "usage": "input", + "git_blob": "65f59761eb03321f1c6c5cd3b0801d8f5601e658", + "sha256": "c6cc95467a6fb6d8c94ec4ea1e2db78d029dfe4136863582bfd83cadf1f2d485" + }, + { + "path": "research/z4-persistent-pair-seed57/README.md", + "usage": "provenance", + "git_blob": "001929a89cd64f4bbb0d4194c6bde96f45b7ded2", + "sha256": "6dda7d5b83b41c71d73711401edbc146271a546a518ef6b038b0bdbb6578d405" + }, + { + "path": "research/z4-heterogeneous-pair-seed3x7/CERTIFICATE.json", + "usage": "provenance", + "git_blob": "db07d83cb06d2fb735d244e98317b7b5a560095f", + "sha256": "f737ac223d3ead20fec9d3bb6d7ede3a75b3d0f699e417c06cf2938b2c55d6d1" + }, + { + "path": "research/centre-sharing-overhead-budget/RESULT.json", + "usage": "input", + "git_blob": "a3758cbd5f157a85e741912783b7203f4061429c", + "sha256": "44fc848b984dbca3aa8ee66898f64f35c305855d0158f1cb4bec0d4d0b28d2b2" + }, + { + "path": "research/selected-suppliers-de-diagnostic/RESULT.json", + "usage": "input", + "git_blob": "af8875af8a8b73382180d6f71a3357d613af8046", + "sha256": "731f77e404c18e3c1329d1ad084b3e0e3752579ae83fcb4e48a2b749d405c7a1" + }, + { + "path": "research/complex-local-word-ceiling/ceiling.py", + "usage": "provenance", + "git_blob": "6c0f54527d879396f689523bfde19928a9b6157c", + "sha256": "86a1432870b3b21d8454106ec9162fddc0471472d9214c590a1420f2426cedfc" + }, + { + "path": "research/split-centres-global/proofs/PR386-BIT-GEOMETRY.txt", + "usage": "input", + "git_blob": "31efe312680fdafba0ccfb630bb6b711acad5944", + "sha256": "c5f077b849e9add9957ab4ee36095dd47bc678dee7e09baa146dac4c0a0d66b2" + } + ] +} diff --git a/research/z4-typed-echo-supplier-instance/TASK.json b/research/z4-typed-echo-supplier-instance/TASK.json new file mode 100644 index 0000000000..a49f8e0e9c --- /dev/null +++ b/research/z4-typed-echo-supplier-instance/TASK.json @@ -0,0 +1,113 @@ +{ + "schema_version": 1, + "task_id": "centre-path-sharing", + "priority_revision": 4, + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "assignment_seed": "8f02a1b1e58bb7d46704bd83df0442e2", + "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 connector-alphabet-change (scope key ff4f5113ed2256ab19ed; drawn track recursive-interfaces). This session takes the explicitly assigned kappa-blocker KB1 request instead: every mechanism package ends with 'no supplier instance exists, so no kappa change follows', so build a physical or hosted supplier instantiation of one certified mechanism with the priced whole-construction budget and the a < D/E diagnostic. Taking an explicit open request in place of the drawn card is the recorded scope change (autoresearch.md section 3). The drawn connector-alphabet-change and joint-query-controller cards are also live-claimed on 2026-10-15 (Cycle 43/44 claims, PRs 2249/2259/2391), and two of the three named KB1 candidates (DUO connector words, R439 star absorption) carry fresh same-day claims, so the instantiated mechanism is the unclaimed z4 order-four typed echo, registered under the centre-path-sharing card because that is the lever the instantiation prices.", + "actual_scope": "Instantiate the certified z4 order-four typed echo (PR1391 five-child contract; PR1410 persistent pair) as a supplier instance for two-call centre sharing: smallest falsifying typed pair k=2 first (all 16 phase paths, all 56 basis columns = every dirty state, literal inverse, three schedule mutants), the priced whole-construction physical budget in one declared tape model (dispatch, instruction fetch, coefficient fetch, reads, writes, address travel, descriptor storage, data storage) for joint vs separate schedules at k=2 and k=5+5, and the hosted aggregate ledgers with exact moments and the a < D/E diagnostic on the selected complex ledger (m=73, W=14336, N=144). One documented obstruction (hosting: COPY/ERASE window-lifetime and per-call totals delivery) and one bounded pivot (single-call realization).", + "bottleneck_link": "The centre path consumes 64 of the ~99.6 unpaid coordinates per call on the binding complex side; the certified typed echo is a concrete candidate mechanism for the 'centre path shared by two calls' lever (levers.py: 1.90x). Instantiating it converts the lever from a planning relaxation into a priced word-level construction with its exact overhead, or fails precisely where hosting blocks it.", + "budget_minutes": 90, + "cost_model": { + "mechanism_invoices": { + "k5_joint_ADD_NEG": [920, 88], + "k5_eager_ADD_NEG": [1208, 120], + "k10_joint_ADD_NEG": [1720, 184], + "two_separate_k5_ADD_NEG": [1840, 176], + "k2_joint_ADD_NEG": [440, 56], + "two_separate_k1_ADD_NEG": [560, 48] + }, + "whole_construction_price_m73": { + "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", + "pair_saving": "112 primitives, 112 dispatches, 232 reads, 112 writes, 16080 travel steps, 1920 descriptor bits per fused pair (identical at k=2 and k=5+5); 0 storage change" + }, + "prefix_row_l1_peak": {"k1": 4, "k2_joint": 10, "k5": 20, "two_separate_k5": 30, "k10_joint": 42}, + "complete_charged_scope": "Mechanism word + declared tape model + hosted aggregate ledger moment. Not charged: native compilation, tape streaming widths, coefficient magnitudes beyond the row-L1 proxy, all-size/compiler and analytic obligations." + }, + "search_domain": { + "phase_group": "Z/4Z", + "children_joint": 2, + "children_fixtures": [5, 10], + "phase_paths_enumerated": {"2": 16, "5": 1024}, + "basis_columns": 56, + "ledgers": "selected complex aggregate (m=73, W=14336, N=144) and its k=2 shared-centre variant (n_8: 1152 -> 576)" + }, + "stop_rule": "Stop at the first failing obligation (hosting, tape/precision, or an unfavourable exact moment), record the exact obstruction, allow at most one bounded pivot, and stop.", + "outcome": "completed", + "evidence": "verify.py and RESULT.json: 51 controls. Mechanism reproduced exactly (g(5)=140, g(10)=248, echo 1008 vs 1328, joint 1904 vs 2016). Smallest falsifying pair k=2 checked on all 56 basis columns and all 16 phase paths with joint = sequential composition, literal inverse and three rejected mutants; deferred-restoration witness: 24 dirty work rows at the second block's entry. Whole construction priced. Hosted ledgers: baseline D=5120, D/E=0.0016805907097543218, exact moment root 0.001675462676..277 (the recorded complex endpoint, residual in the published -1.30e-24 band); shared k=2 ledger D=9728, D/E=0.003203836729943888, exact root 0.003185242415..416, f(bit endpoint)-1 = -4.25e-3 (matches research/centre-sharing-overhead-budget). Delta-H: 64 rank units eliminated per pair against the sharp 61.6-unit full-gain budget, typed echo recursive overhead 0. Obstruction: hosting window-lifetime/delivery contract. Bounded pivot (single-call realization) returns the baseline ledger.", + "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 a widened COPY/ERASE window with per-pair totals delivery, keeping sequential immutable windows inside each call?", + "why_it_matters": "That single contract change admits the typed-echo shared-centre ledger (exact moment root 0.0031852 vs 0.0016755), which moves the binding side to the bit primitive at kappa 0.001730427469823602 (+3.4536% whole-bound, per research/centre-sharing-overhead-budget).", + "first_step": "Inspect one retained supplier's owner-map window definitions and its totals-delivery schedule for a consecutive same-sink call pair; price the widened window as extra live families.", + "blocked_by": "The pinned contract states COPY/ERASE windows remain sequential and immutable, and no named child exposes the order-four intertwiner R P = Q R." + }, + { + "question": "Can the typed-echo carry survive the precision envelope of a named host (prefix row-L1 30 -> 42 at the persistent pair)?", + "why_it_matters": "The row-L1 rise is the one measured cost of the carry; a fixed-precision host must price it before the saving counts.", + "first_step": "Propagate the joint word's exact prefix coefficient envelope through the host's precision charge buckets (the 192/512-bit conventions of the bit invoice).", + "blocked_by": "The complex host's precision bucket law is not pinned in a form this package could charge." + } + ], + "coordination": { + "claim_status": "posted", + "discussion": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-18947139", + "claim_created_at": "2026-10-15T10:45:00Z", + "claim_expiry": "2026-10-15T13:00:00Z", + "pair_collision_check": "disc-comments with nested replies on #1166 and #1317 at 2026-10-15 10:35-10:40 UTC plus find_overlap.py at 10:35 UTC; DUO connector words (PRs 2396/2397, comment 18943467) and R439 star absorption (claim 18944326, PRs 2407/2421/2428) carry fresh same-day claims; no z4/typed-echo claim in the recent window.", + "closest_prior": "research/centre-sharing-overhead-budget prices the same lever on the actual selected histograms and leaves construction/hosting open; PR1708/PR1748 are its scalar-macro sharing halves; research/selected-centre-adjacent-pair-seed01fcb1 censused the pinned 144-call schedule and found no adjacent pair sharing a physical owner among its eight centre source rows (the source-bound side of the same hosting obstruction); this package supplies a typed-echo instantiation with its whole-construction price and one exact hosting obstruction." + }, + "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-echo-supplier-instance/VERIFY.json b/research/z4-typed-echo-supplier-instance/VERIFY.json new file mode 100644 index 0000000000..d298df0941 --- /dev/null +++ b/research/z4-typed-echo-supplier-instance/VERIFY.json @@ -0,0 +1,33 @@ +{ + "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/z4-paired-frame-restoration-seed56/CERTIFICATE.json", + "research/z4-persistent-pair-seed57/RESULT.json", + "research/z4-persistent-pair-seed57/README.md", + "research/z4-heterogeneous-pair-seed3x7/CERTIFICATE.json", + "research/centre-sharing-overhead-budget/RESULT.json", + "research/selected-suppliers-de-diagnostic/RESULT.json", + "research/complex-local-word-ceiling/ceiling.py", + "research/community-frontier1094-audit/ASSEMBLY.json", + "research/split-centres-global/proofs/PR386-BIT-GEOMETRY.txt", + "certificates/selected-result.json", + "docs/research/agent-task-catalog.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 300, + "checks": "Rebuild the pinned typed-echo invoices and boundary recurrence, exhaust the k=2 and k=5 phase paths, verify the 56-basis-column dirty maps and literal inverses, reject three schedule mutants, extract the deferred-restoration witness, price the whole construction in the declared tape model, and compute both hosted ledgers' exact moments, D/E screens and the Delta-H budget fit, including the pivot and three mutated-ledger rejections (51 controls)." + } + ] +} diff --git a/research/z4-typed-echo-supplier-instance/verify.py b/research/z4-typed-echo-supplier-instance/verify.py new file mode 100644 index 0000000000..1ed1585829 --- /dev/null +++ b/research/z4-typed-echo-supplier-instance/verify.py @@ -0,0 +1,720 @@ +#!/usr/bin/env python3 +"""KB1 supplier instantiation of the certified z4 order-four typed echo. + +Object: the certified order-four paired-frame typed echo (PR #1391 five-child +contract, PR #1410 persistent pair, both pinned through +research/z4-persistent-pair-seed57/inputs). This package builds the missing +supplier instantiation: the smallest falsifying typed pair, the priced +whole-construction physical budget (dispatch, reads, writes, address travel, +instruction fetch, coefficient fetch, descriptor storage, storage), the hosted +aggregate ledgers with their exact moments and the a < D/E diagnostic, and the +exact witness for the one obligation the instantiation does not close +(hosting: the named host's COPY/ERASE window-lifetime and delivery contract). + +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 subprocess +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. Hashes are the PR #1410 package's own pins. +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" + +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. Pins and 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) + cert = json.loads(cert_raw) + return legacy, cert + + +def git_blob(path): + out = subprocess.run(["git", "hash-object", str(path)], cwd=ROOT, check=True, + capture_output=True, text=True).stdout.strip() + return out + + +def base_blob(path): + out = subprocess.run(["git", "rev-parse", BASE + ":" + path], cwd=ROOT, check=True, + capture_output=True, text=True).stdout.strip() + return out + + +# -------------------------------------------------------------------------- +# Exact enclosures: ln (atanh chain), exp (Taylor with tail), moment bill. +# Technique credited to research/complex-local-word-ceiling/ceiling.py and +# research/selected-suppliers-de-diagnostic/verify.py; re-implemented here so +# this package imports neither engine. +# -------------------------------------------------------------------------- + +PREC = 176 + + +def down(x): + return Q((x.numerator << PREC) // x.denominator, 1 << PREC) + + +def up(x): + return -down(-x) + + +_ATANH = {} + + +def atanh(t): + if t in _ATANH: + return _ATANH[t] + require(0 < t <= Q(1, 3), "atanh range") + s, p, k = Q(0), t, 0 + while True: + s += p / (2 * k + 1) + p *= t * t + k += 1 + tail = p / ((2 * k + 1) * (1 - t * t)) + if tail < Q(1, 1 << (PREC + 8)): + out = (down(s), up(s + tail)) + _ATANH[t] = out + return out + + +_LN = {} + + +def ln_int(k): + """Enclosure of ln k for integer k >= 1.""" + if k in _LN: + return _LN[k] + require(isinstance(k, int) and k >= 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): + """Enclosure of ln(m/r) = ln m - ln r.""" + lm, um = ln_int(m) + lr, ur = ln_int(r) + return down(lm - ur), up(um - lr) + + +def exp_enc(lo, hi): + """Enclosure of exp([lo, hi]) for 0 <= lo <= hi <= 1/2.""" + 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): + """Enclosure of (m/r)^a = exp(a ln(m/r)) for rational 0 <= a <= 1/20.""" + lo, hi = ln_ratio(m, r) + return exp_enc(a * lo, a * hi) + + +def moment_bill(hist, m, W, a, surcharge=None): + """Enclosure of f(a) = (1/(mW)) sum n_r r (m/r)^a + c_s m^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] + if surcharge: + e = child_power(m, 1, a) + lo += surcharge * e[0] + hi += surcharge * e[1] + return down(lo / (m * W)), up(hi / (m * W)) + + +def de_diagnostic(hist, m, W): + """(D, E-enclosure, D/E-enclosure) with D = mW - sum n_r r, E = sum n_r r ln(m/r).""" + 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)) + + +def moment_root(hist, m, W, grid): + """Bracket the exact moment root a* with f(a_lo) < 1 < f(a_hi).""" + lo, hi = Q(0), Q(1, 20) + require(moment_bill(hist, m, W, hi)[0] > 1, "root search window too small") + require(moment_bill(hist, m, W, lo)[1] < 1, "ledger has no positive saving") + while hi - lo > grid: + mid = Q(int((lo + hi) / 2 / grid)) * grid + if mid <= lo: + mid = lo + grid + v = moment_bill(hist, m, W, mid) + if v[1] < 1: + lo = mid + elif v[0] > 1: + hi = mid + else: + raise ValueError("enclosure too wide at grid " + str(mid)) + return lo, hi + + +# -------------------------------------------------------------------------- +# S1/S2. Typed-echo words: smallest instance, invoices, exact maps. +# -------------------------------------------------------------------------- + + +def echo_word(legacy, states, blocks): + """One complete dirty root echo: W += X; batch; W -= X; inverse batch.""" + ow, ww = legacy.OUTPUT_WIDTH, legacy.WORK_WIDTH + body_local = legacy.batch_word(states, blocks=blocks) + mapping = list(range(ow)) + [ow + ww + i for i in range(ww)] + body = legacy.lift_word(body_local, mapping) + copy_in = [legacy.add(ow + ww + i, ow + i) for i in range(ww)] + copy_out = [legacy.add(ow + ww + i, ow + i, -1) for i in range(ww)] + return copy_in + body + copy_out + legacy.inverse_word(body) + + +def wrapper_word(legacy): + ow, ww = legacy.OUTPUT_WIDTH, legacy.WORK_WIDTH + copy_in = [legacy.add(ow + ww + i, ow + i) for i in range(ww)] + copy_out = [legacy.add(ow + ww + i, ow + i, -1) for i in range(ww)] + return copy_in, copy_out + + +def expected_echo_map(legacy, blocks): + """(D, X, W) -> (D + sum R_i X, X, W) as exact integer rows.""" + ow, ww = legacy.OUTPUT_WIDTH, legacy.WORK_WIDTH + width = ow + ww + ww + rows = legacy.identity(width) + for block in blocks: + for j in range(ow): + rows[j][ow + 8 * block + j] += 1 + return rows + + +def my_dp(k, work_cost, out_cost): + """Independent re-derivation of the boundary recurrence g(k).""" + def step(old, new): + return (work_cost[(new - old - 1) % 4] + out_cost[(new - old) % 4], (old, new)) + + f = {t: (work_cost[t] + out_cost[t], (t,)) for t in range(4)} + for _ in range(k): + nxt = {} + for s in range(4): + best = None + for t in range(4): + c, _ = step(t, s) + cand = (f[t][0] + c, f[t][1] + (s,)) + if best is None or cand < best: + best = cand + nxt[s] = best + f = nxt + return f[0] + + +def path_total(states, work_vec, out_vec): + v = tuple(a + b for a, b in zip(work_vec[states[0]], out_vec[states[0]])) + for old, new in zip(states, states[1:]): + w = work_vec[(new - old - 1) % 4] + o = out_vec[(new - old) % 4] + v = tuple(x + y + z for x, y, z in zip(v, w, o)) + return sum(v) + + +# -------------------------------------------------------------------------- +# S3. Whole-construction physical price (declared machine model). +# -------------------------------------------------------------------------- + + +def physical_price(word, width, calls): + """Charge every quantity the repo's physical models charge for this word. + + Declared model: rows of width m on a row-indexed tape. Each record is one + dispatch and one instruction fetch and one coefficient fetch (constants + +-1); ADD reads two rows and writes one, NEG reads and writes one; address + travel is 2*max(source, target) row-index steps per record (NEG: 2*target), + the visit-source/visit-target/return convention of + research/mutable-source-persistent-connector. Descriptor storage is 16 + bits per record plus one 128-bit call record per call. Data storage is + width * 56 cells (8 output + 24 source + 24 work coordinates). + """ + adds = negs = reads = writes = movement = 0 + for kind, target, source, sign in word: + if kind == "ADD": + adds += 1 + reads += 2 + movement += 2 * max(target, source) + else: + negs += 1 + reads += 1 + movement += 2 * target + writes += 1 + records = len(word) + return { + "primitives": records, + "ADD": adds, + "NEG": negs, + "dispatches": records, + "instruction_fetches": records, + "coefficient_fetches": records, + "reads": reads, + "writes": writes, + "address_travel_row_steps": movement, + "descriptor_bits": 16 * records + 128 * calls, + "data_storage_cells": width * 56, + } + + +# -------------------------------------------------------------------------- +# Main +# -------------------------------------------------------------------------- + + +def build_result(): + legacy, cert = load_legacy() + m_host, W_host = 73, 14336 # selected complex aggregate ledger + + # ---- S1: mechanism reproduction (positive controls) -------------------- + 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)) + work_cost = [3 * sum(v) for v in per_octet] + out_cost = [sum(v) for v in per_octet] + + g = {} + paths = {} + for k in (1, 2, 3, 5, 10): + total, states = my_dp(k, work_cost, out_cost) + g[k] = total + paths[k] = list(states) + control("g5_reproduces_pr1391", g[5] == 140, "g(5)=" + str(g[5])) + control("g10_reproduces_pr1410", g[10] == 248, "g(10)=" + str(g[10])) + control("g2_is_the_smallest_pair_boundary", g[2] == 88, "g(2)=" + str(g[2])) + control("dp_agrees_with_pinned_brute_k5", + legacy.brute_boundary_min(5) == g[5], "brute=" + str(legacy.brute_boundary_min(5))) + control("dp_agrees_with_pinned_brute_k3", + legacy.brute_boundary_min(3) == g[3], "brute=" + str(legacy.brute_boundary_min(3))) + + # Certified canonical optimal paths (PR #1391/#1410): use them for emission + # after re-checking their cost against the independent DP. + canonical = {5: [0, 1, 2, 3, 0, 0], 10: [0, 1, 2, 3, 0, 1, 2, 3, 0, 1, 0]} + work_vec = [tuple(3 * x for x in v) for v in per_octet] + out_vec = [tuple(v) for v in per_octet] + for k, cand in canonical.items(): + control("canonical_path_is_optimal_k%d" % k, + path_total(cand, work_vec, out_vec) == g[k], + "canonical=%d dp=%d" % (path_total(cand, work_vec, out_vec), g[k])) + paths[k] = cand + + # exhaustive phase-path census: smallest instance k=2 and fixture k=5 + census = {} + for k in (2, 5): + best = None + count = 0 + work_vec = [tuple(3 * x for x in v) for v in per_octet] + out_vec = [tuple(v) for v in per_octet] + for prefix in itertools.product(range(4), repeat=k): + states = list(prefix) + [0] + t = path_total(states, work_vec, out_vec) + if best is None or t < best: + best = t + count += 1 + census[k] = {"paths": count, "min_total": best} + control("exhaustive_census_matches_dp_k%d" % k, best == g[k], + "census=" + str(best) + " dp=" + str(g[k])) + + # exact maps and invoices for the certified fixtures and the smallest pair + words = {} + words["k5_joint"] = echo_word(legacy, paths[5], (0, 1, 2, 0, 1)) + words["k10_joint"] = echo_word(legacy, paths[10], (0, 1, 2, 0, 1, 0, 1, 2, 0, 1)) + words["k2_joint"] = echo_word(legacy, paths[2], (0, 1)) + words["k1_a"] = echo_word(legacy, [0, 0], (0,)) + words["k1_b"] = echo_word(legacy, [0, 0], (1,)) + words["k2_separate"] = words["k1_a"] + words["k1_b"] + words["k5_eager"] = None # built below from eager states [0]*6 + + inv = {name: legacy.word_counts(w) for name, w in words.items() if w is not None} + control("k5_echo_invoice_1008", sum(inv["k5_joint"]) == 1008, str(inv["k5_joint"])) + control("k10_joint_invoice_1904", sum(inv["k10_joint"]) == 1904, str(inv["k10_joint"])) + control("two_separate_k5_invoice_2016", 2 * sum(inv["k5_joint"]) == 2016, str(inv["k5_joint"])) + control("two_separate_k1_invoice", sum(inv["k2_separate"]) == 608, str(inv["k2_separate"])) + control("k2_joint_invoice_496", sum(inv["k2_joint"]) == 496, str(inv["k2_joint"])) + + # eager restoration control (schedule mutant): each child followed by P^-1 + eager_states = [0] * 6 + eager_local = legacy.batch_word(tuple(eager_states), blocks=(0, 1, 2, 0, 1), + omit_last_gap=False) + ow, ww = legacy.OUTPUT_WIDTH, legacy.WORK_WIDTH + mapping = list(range(ow)) + [ow + ww + i for i in range(ww)] + eager_body = legacy.lift_word(eager_local, mapping) + cin, cout = wrapper_word(legacy) + words["k5_eager"] = cin + eager_body + cout + legacy.inverse_word(eager_body) + inv["k5_eager"] = legacy.word_counts(words["k5_eager"]) + control("k5_eager_invoice_1328", sum(inv["k5_eager"]) == 1328, str(inv["k5_eager"])) + + # exact linear maps on all 56 basis columns (this is every dirty state) + for name, blocks in (("k2_joint", (0, 1)), ("k1_a", (0,)), ("k1_b", (1,)), + ("k5_joint", (0, 1, 2, 0, 1)), + ("k10_joint", (0, 1, 2, 0, 1, 0, 1, 2, 0, 1))): + got = legacy.apply_word_matrix(words[name], legacy.ECHO_WIDTH) + want = expected_echo_map(legacy, blocks) + control("exact_map_" + name, got == want, "map mismatch on 56 basis columns") + + # smallest falsifying instance: joint == sequential composition, exactly + seq = legacy.matmul(legacy.apply_word_matrix(words["k1_b"], legacy.ECHO_WIDTH), + legacy.apply_word_matrix(words["k1_a"], legacy.ECHO_WIDTH)) + control("k2_joint_equals_sequential_composition", + seq == legacy.apply_word_matrix(words["k2_joint"], legacy.ECHO_WIDTH), + "composed maps differ") + + # literal inverse restores identity + for name in ("k2_joint", "k5_joint"): + w = words[name] + inv_word = legacy.inverse_word(w) + m = legacy.matmul(legacy.apply_word_matrix(inv_word, legacy.ECHO_WIDTH), + legacy.apply_word_matrix(w, legacy.ECHO_WIDTH)) + control("literal_inverse_" + name, m == legacy.identity(legacy.ECHO_WIDTH), + "inverse does not restore") + + # negative controls on the smallest instance: schedule mutants must fail + s2 = list(paths[2]) + mutant_local = legacy.batch_word(tuple(s2), blocks=(0, 1), wrong_first_output_phase=True) + mutant_body = legacy.lift_word(mutant_local, mapping) + mutant_word = cin + mutant_body + cout + legacy.inverse_word(mutant_body) + control("wrong_first_output_phase_rejected", + legacy.apply_word_matrix(mutant_word, legacy.ECHO_WIDTH) + != expected_echo_map(legacy, (0, 1)), "mutant map accepted") + no_terminal = legacy.batch_word(tuple(s2), blocks=(0, 1), omit_last_gap=True) + nt_body = legacy.lift_word(no_terminal, mapping) + nt_word = cin + nt_body + cout + legacy.inverse_word(nt_body) + control("omitted_terminal_gap_rejected", + legacy.apply_word_matrix(nt_word, legacy.ECHO_WIDTH) + != expected_echo_map(legacy, (0, 1)), "mutant map accepted") + fwd_word = cin + mutant_body + cout + mutant_body + control("forward_for_inverse_rejected", + legacy.apply_word_matrix(fwd_word, legacy.ECHO_WIDTH) + != expected_echo_map(legacy, (0, 1)), "mutant map accepted") + + # ---- S2: smallest-instance window witness (the obstruction) ----------- + # The joint word has exactly one wrapper (copy-in/copy-out pair) around both + # child blocks; the separate schedule has one wrapper per block. The + # deferred copy-out is the window-lifetime change the named host forbids. + def wrapper_positions(word): + ins, outs = [], [] + for i, (kind, target, source, sign) in enumerate(word): + if (kind == "ADD" and ow + ww <= target < ow + 2 * ww + and source is not None and ow <= source < ow + ww): + (ins if sign == 1 else outs).append(i) + return ins, outs + + jin, jout = wrapper_positions(words["k2_joint"]) + ain, aout = wrapper_positions(words["k1_a"]) + bin_, bout = wrapper_positions(words["k1_b"]) + control("joint_word_has_one_wrapper", len(jin) == ww and len(jout) == ww, + "copy records=%d/%d" % (len(jin), len(jout))) + control("separate_words_have_two_wrappers", + len(ain) == ww and len(aout) == ww and len(bin_) == ww and len(bout) == ww, "counts") + # deferred-restoration witness: at the entry of the second child block in + # the joint word, the work rows still carry first-block state (the first + # wrapper's copy-out has not run). Locate the block-1 reader: the first + # D-row write whose source is workspace octet 1 after the copy-in region. + jw = words["k2_joint"] + state = legacy.identity(legacy.ECHO_WIDTH) + cut = None + dirty = None + for i, (kind, target, source, sign) in enumerate(jw): + if (cut is None and i > max(jin) and target < ow and source is not None + and ow + ww + 8 <= source < ow + ww + 16): + cut = i + dirty = sum(1 for r in range(ow + ww, legacy.ECHO_WIDTH) + if any(state[r][c] != (1 if r == c else 0) + for c in range(legacy.ECHO_WIDTH))) + if kind == "ADD": + state[target] = [a + sign * b for a, b in zip(state[target], state[source])] + else: + state[target] = [-x for x in state[target]] + require(cut is not None and dirty is not None, "second child block located") + control("deferred_restoration_witness_at_smallest_instance", dirty == ww, + "dirty work rows at block-2 entry=" + str(dirty)) + + # ---- S3: whole-construction physical price ---------------------------- + width = m_host + price = {} + price["k2_separate"] = physical_price(words["k2_separate"], width, 2) + price["k2_joint"] = physical_price(words["k2_joint"], width, 1) + price["k5_separate_pair"] = physical_price(words["k5_joint"] + words["k5_joint"], width, 2) + price["k10_joint"] = physical_price(words["k10_joint"], width, 1) + pair_saving = {k: price["k2_separate"][k] - price["k2_joint"][k] for k in price["k2_separate"]} + pair_saving_510 = {k: price["k5_separate_pair"][k] - price["k10_joint"][k] + for k in price["k5_separate_pair"]} + control("whole_price_primitives_positive", + pair_saving["primitives"] == 112 and pair_saving_510["primitives"] == 112, + "k2=%s k5k10=%s" % (pair_saving["primitives"], pair_saving_510["primitives"])) + control("dispatch_charge_is_not_free", + pair_saving["dispatches"] == 112 and price["k2_joint"]["dispatches"] > 0, + str(pair_saving["dispatches"])) + + # precision proxy: certified prefix row-L1 peaks + l1 = {} + for name in ("k1_a", "k2_joint", "k5_joint", "k10_joint"): + l1[name] = legacy.prefix_row_l1_peak(words[name], legacy.ECHO_WIDTH) + l1["k5_separate_pair_concat"] = legacy.prefix_row_l1_peak( + words["k5_joint"] + words["k5_joint"], legacy.ECHO_WIDTH) + control("persistent_pair_row_l1_matches_pr1410", + l1["k10_joint"] == 42 and l1["k5_separate_pair_concat"] == 30, + "joint=%d separate=%d" % (l1["k10_joint"], l1["k5_separate_pair_concat"])) + control("row_l1_charge_is_not_free", l1["k2_joint"] > l1["k1_a"], + "k2=%d k1=%d" % (l1["k2_joint"], l1["k1_a"])) + + # ---- S4: hosted ledgers, exact moments, a < D/E ----------------------- + 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 # k=2 shared centre: 1,152 -> 576 rank-8 children + + # coverage identities + 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])) + + a_complex = Q("0.001675462676808103522925") # recorded complex endpoint + a_bit = Q("0.001733427039589844234749") # recorded bit endpoint + f_base = moment_bill(hist_base, m_host, W_host, a_complex) + f_base_next = moment_bill(hist_base, m_host, W_host, a_complex + Q(1, 10 ** 24)) + f_shared_bit = moment_bill(hist_shared, m_host, W_host, a_bit) + control("baseline_accepts_recorded_endpoint", f_base[1] < 1, str(f_base)) + control("baseline_rejects_next_grid_point", f_base_next[0] > 1, str(f_base_next)) + control("baseline_residual_matches_published_magnitude", + Q("-1.30422e-24") < f_base[0] - 1 and f_base[1] - 1 < Q("-1.30421e-24"), + "residual band check: [%s, %s]" % (f_base[0] - 1, f_base[1] - 1)) + control("shared_accepts_bit_endpoint_with_published_margin", + Q("-0.00430") < f_shared_bit[1] - 1 < Q("-0.00420"), + "f(c_bit)-1 in (%s, %s)" % (f_shared_bit[0] - 1, f_shared_bit[1] - 1)) + control("D_over_E_overestimates_the_root", + moment_bill(hist_base, m_host, W_host, DE_b[1])[0] > 1, + "f(D/E) must exceed 1 strictly") + + root_base = moment_root(hist_base, m_host, W_host, Q(1, 10 ** 12)) + root_shared = moment_root(hist_shared, m_host, W_host, Q(1, 10 ** 12)) + control("baseline_root_tracks_recorded_endpoint", + root_base[0] - Q(1, 10 ** 11) <= a_complex <= root_base[1] + Q(1, 10 ** 11), + "root=[%s, %s]" % (root_base[0], root_base[1])) + + # typed-echo Delta-H accounting against the sharp budget + eliminated_units_per_pair = 64 # one wrapper = 8 rank-8 children + budget_full_gain_per_pair = Q("61.6") # 2 x 30.8 units/call (centre-sharing-overhead-budget) + budget_any_gain_per_pair = Q("64.0") # 2 x 32.0 units/call + typed_echo_recursive_overhead = 0 # the typed word adds only scalar records + net_per_pair = eliminated_units_per_pair - typed_echo_recursive_overhead + control("delta_h_fits_sharp_budget", + net_per_pair >= budget_full_gain_per_pair and + typed_echo_recursive_overhead <= budget_any_gain_per_pair, + "net=%s budget=%s" % (net_per_pair, budget_full_gain_per_pair)) + + # histogram-identical control: paying both wrappers gives no moment change + control("both_wrappers_keep_selected_histogram", + mass_base - mass_shared == 72 * 8 * 8 == 4608, + "wrapper mass identity: %d" % (mass_base - mass_shared)) + + # ---- bounded pivot: single-call realization --------------------------- + # Pivot: make the pair one supplier call from the start (one window, no + # reorder). The per-call totals-delivery contract then requires the fused + # call to copy both calls' totals: 16 rank-8 children per pair = 128 units, + # exactly the two-wrapper baseline, so the ledger returns to the selected + # histogram and the moment is unchanged. The alternative (one shared set + # of totals) is the common-sink delivery contract change already named in + # the obstruction, so the pivot does not escape the same obligation. + hist_pivot = dict(hist_base) + pivot_pair_units = 16 * 8 + control("pivot_single_call_delivery_returns_baseline_ledger", + pivot_pair_units == 2 * eliminated_units_per_pair + and sum(n * r for r, n in hist_pivot.items()) == mass_base, + "pivot pair units=%d" % pivot_pair_units) + f_pivot = moment_bill(hist_pivot, m_host, W_host, a_complex) + control("pivot_moment_identical_to_baseline", + f_pivot == f_base, "pivot moment differs") + + # mutated-ledger controls + bad = dict(hist_base) + bad[1] = bad[1] - 1 + D_bad, E_bad, DE_bad = de_diagnostic(bad, m_host, W_host) + control("histogram_mutation_breaks_coverage_identity", + m_host * W_host - sum(n * r for r, n in bad.items()) != W_host - 64 * 144, + "mutation detected") + try: + de_diagnostic({999: 1}, m_host, W_host) + ok = False + except ValueError: + ok = True + control("child_rank_outside_0_m_rejected", ok, "rank 999 must be rejected") + try: + de_diagnostic({1: m_host * W_host}, m_host, W_host) + ok = False + except ValueError: + ok = True + control("zero_deficit_ledger_rejected", ok, "D must be positive") + + return { + "schema_version": 1, + "base_commit": BASE, + "result": "PASS_Z4_TYPED_ECHO_SUPPLIER_INSTANCE", + "mechanism": { + "g_boundary_total": {str(k): g[k] for k in g}, + "g_boundary_paths": {str(k): paths[k] for k in g}, + "exhaustive_census": {str(k): census[k] for k in census}, + "invoices_ADD_NEG": {name: list(inv[name]) for name in inv}, + }, + "smallest_falsifying_instance": { + "joint_blocks": [0, 1], + "separate_calls": [[0], [1]], + "basis_columns_checked": 56, + "phase_paths_enumerated": census[2]["paths"], + "joint_equals_sequential_composition": True, + "deferred_restoration_dirty_work_rows": dirty, + }, + "whole_construction_price": { + "model": "rows of width 73 on a row-indexed tape; dispatch, instruction " + "fetch and coefficient fetch per record; ADD reads 2 writes 1, " + "NEG reads 1 writes 1; address travel 2*max(src,dst) per record; " + "16-bit descriptor per record + 128-bit call record; 56*width " + "data cells", + "k2_separate": price["k2_separate"], + "k2_joint": price["k2_joint"], + "k5_separate_pair": price["k5_separate_pair"], + "k10_joint": price["k10_joint"], + "pair_saving_k2": pair_saving, + "pair_saving_k5k10": pair_saving_510, + "prefix_row_l1_peak": l1, + }, + "hosted_ledgers": { + "width_m": m_host, + "live_stock_W": W_host, + "baseline_histogram": hist_base, + "shared_k2_histogram": hist_shared, + "baseline": { + "rank_mass": mass_base, + "D": D_b, + "E_lo": str(E_b[0]), "E_hi": str(E_b[1]), + "D_over_E_lo": str(DE_b[0]), "D_over_E_hi": str(DE_b[1]), + "moment_at_complex_endpoint": [str(f_base[0]), str(f_base[1])], + "moment_root_lo": str(root_base[0]), "moment_root_hi": str(root_base[1]), + }, + "shared_k2": { + "rank_mass": mass_shared, + "D": D_s, + "E_lo": str(E_s[0]), "E_hi": str(E_s[1]), + "D_over_E_lo": str(DE_s[0]), "D_over_E_hi": str(DE_s[1]), + "moment_at_bit_endpoint": [str(f_shared_bit[0]), str(f_shared_bit[1])], + "moment_root_lo": str(root_shared[0]), "moment_root_hi": str(root_shared[1]), + }, + "delta_h_budget": { + "eliminated_rank_units_per_pair": eliminated_units_per_pair, + "typed_echo_recursive_overhead_units": typed_echo_recursive_overhead, + "sharp_budget_full_gain_units_per_pair": str(budget_full_gain_per_pair), + "sharp_budget_any_gain_units_per_pair": str(budget_any_gain_per_pair), + "fits": True, + }, + }, + "obstruction": { + "obligation": "hosting: COPY/ERASE window-lifetime and per-call delivery", + "pinned_contract": "research/split-centres-global/proofs/PR386-BIT-GEOMETRY.txt: " + "'COPY/ERASE windows remain sequential and immutable'", + "smallest_instance_witness": "the k=2 joint word defers the first wrapper's " + "copy-out past the second child block; all 24 work " + "rows are dirty at the second block's entry", + "unchanged_contract_price": "both wrappers paid: n_8 stays 1152 and the moment " + "is identical to the selected ledger", + "pivots_tested": 1, + "pivot": "single-call realization: the per-call totals-delivery contract makes " + "the fused call copy both calls' totals (16 rank-8 children per pair, " + "128 units), exactly the two-wrapper baseline; the ledger returns to " + "the selected histogram and the moment is unchanged. Sharing one set " + "of totals needs the same common-sink/window contract 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") + print("PASS_Z4_TYPED_ECHO_SUPPLIER_INSTANCE " + "smallest_k2 whole_price saved=112 D_over_E_shared=%s controls=%d no_new_kappa" + % (result["hosted_ledgers"]["shared_k2"]["D_over_E_hi"], result["control_count"])) + + +if __name__ == "__main__": + main() From 5c44715b6fa0806ad828e42fb53b84f6b5f7ddc6 Mon Sep 17 00:00:00 2001 From: Aaron Wang Date: Fri, 16 Oct 2026 06:30:27 -0400 Subject: [PATCH 2/2] Reconcile README admission language with its own obligation inventory Maintainer review of f364b97 on PR 2464 (comment 6204698882) found the README claiming "blocked in exactly one obligation, hosting" and "Everything else is charged and closes" while the same README records three unclosed realization obligations. Reproduced against research/z4-typed-echo-supplier-instance/README.md: the opening and the obstruction section contradicted the reader/intertwiner realization, delivery/lifetime and precision admissions elsewhere in the file and in TASK.json open_questions. README.md only: - opening now states one documented obstruction on this branch's own terms plus three open realization obligations recorded in TASK.json open_questions and the Not checked list; the checked object is the abstract 56-column typed echo word, not a realized selected-supplier instantiation - shared histogram row and the projected kappa exponent labeled conditional pricing; the "concrete mechanism rather than a relaxation" sentence now states the mechanism delivers the figure only if the widened window, common sink and intertwiner child are admitted - "Everything else is charged and closes" replaced by a closed list (moment, scalar price, dirty state) and a recorded-not-closed list (reader/intertwiner, delivery/lifetime, precision); "single contract change" demoted to the hosting side Finite certificates, priced construction, exact moments, a < D/E math, RESULT.json, verify.py and predecessor credit are unchanged. Fresh replay output PASS_Z4_TYPED_ECHO_SUPPLIER_INSTANCE smallest_k2 whole_price saved=112 D_over_E_shared=306866593893834978883114841401737599624288907847049/95780971304118053647396689196894323976171195136475136 controls=51 no_new_kappa matches the declared expected line exactly; scripts/research_package.py --check-only prints PASS_PACKAGE_METADATA_AND_PINS. --- .../z4-typed-echo-supplier-instance/README.md | 77 ++++++++++++------- 1 file changed, 50 insertions(+), 27 deletions(-) diff --git a/research/z4-typed-echo-supplier-instance/README.md b/research/z4-typed-echo-supplier-instance/README.md index 2ebd3eb145..20f5cbb289 100644 --- a/research/z4-typed-echo-supplier-instance/README.md +++ b/research/z4-typed-echo-supplier-instance/README.md @@ -1,18 +1,27 @@ -# z4 typed echo as a supplier instance: priced, and blocked in one obligation - -**Supplier instantiation of a certified mechanism; no new kappa and no change to -the selected record.** The certified z4 order-four typed echo (PR #1391's -five-child contract, PR #1410's persistent pair) is instantiated as far as the -repository's contracts allow: the smallest falsifying typed pair, the priced -whole-construction physical budget, and the hosted aggregate ledgers with their -exact moments and `a < D/E` diagnostics. The instantiation fits the sharpest -available overhead budget with zero recursive overhead of its own. It is -blocked in exactly one obligation, **hosting**: the named host's contract keeps +# z4 typed echo as a supplier instance: priced, one documented obstruction, open realization obligations + +**Conditional supplier instantiation of a certified mechanism; no new kappa and +no change to the selected record.** The certified z4 order-four typed echo +(PR #1391's five-child contract, PR #1410's persistent pair) is instantiated as +far as the repository's contracts allow: the smallest falsifying typed pair, the +priced whole-construction physical budget, and the hosted aggregate ledgers with +their exact moments and `a < D/E` diagnostics. What is checked is the abstract +typed echo word on all 56 basis columns; no named selected supplier is shown to +implement the typed child, so this is not a realized selected-supplier +instantiation. The instantiation fits the sharpest available overhead budget +with zero recursive overhead of its own. It carries one documented obstruction +on this branch's own terms, **hosting**: the named host's contract keeps `COPY/ERASE` windows sequential and immutable and delivers totals per call, while the typed echo must defer the first wrapper's restoration across the second call's window. Under the unchanged contract the pair pays both wrappers, the ledger returns to the selected histogram, and the 112 saved primitives per -pair are scalar-only. +pair are scalar-only. One obstruction is not one remaining obligation. Three +realization obligations stay open, recorded in [TASK.json](TASK.json) +`open_questions` and in the **Not checked** list below: reader/intertwiner +realization (no named host child exposes `R P = Q R`), delivery/lifetime (a +widened window and a common sink for the pair's totals, the first blocker of +PR #1748), and precision (the host bucket law, quantified by the row-L1 proxy +but not closed). None of the three follows from the arithmetic below. Agent: **Aaron Wang**, with help from opencode (substantial AI assistance; no independent human review). Task card: [TASK.json](TASK.json) (card @@ -85,8 +94,9 @@ quantity in the moment ledger moves. The named host is the binding selected complex ledger (width `m = 73`, live stock `W = 14,336`, `N = 144` calls, published histogram, no surcharge). The -typed echo applied to consecutive same-source call pairs is the shared-centre -ledger of `research/centre-sharing-overhead-budget`: the shared rank-8 centre +typed echo applied to consecutive same-source call pairs would be the +shared-centre ledger of `research/centre-sharing-overhead-budget` (conditional +pricing, pending the open realization obligations): the shared rank-8 centre children go from 1,152 to 576 and the coverage identity from `72W + 64N` to `72W + 32N`. Exact rational enclosures (independent atanh/Taylor engine, no import of the retained pricing engines): @@ -94,7 +104,7 @@ import of the retained pricing engines): | ledger | rank mass | D | `a < D/E` | exact moment root `a*` | |---|---:|---:|---:|---| | selected baseline | 1,041,408 | 5,120 | 0.0016805907097543218 | [0.001675462676, 0.001675462677] | -| shared k=2 typed echo | 1,036,800 | 9,728 | 0.003203836729943888 | [0.003185242415, 0.003185242416] | +| shared k=2 typed echo (conditional) | 1,036,800 | 9,728 | 0.003203836729943888 | [0.003185242415, 0.003185242416] | The baseline `D/E` matches the published 0.001680590709754321699421 to 2.4e-25 (printing precision) and the baseline root is the recorded complex endpoint @@ -102,10 +112,14 @@ The baseline `D/E` matches the published 0.001680590709754321699421 to 2.4e-25 `-1.30e-24` band; the next `10^-24` grid point is rejected. At the recorded bit endpoint 0.0017334270395898442 the shared ledger gives `f(a) - 1 = -4.25e-3`, matching `research/centre-sharing-overhead-budget`'s table entry for `k = 2`. -So with sharing the complex side stops binding and the whole bound becomes +So with sharing the complex side stops binding and the whole bound would become bit-limited at `kappa = 0.001730427469823602` (+3.4536% on the selected -0.001672660197076918), which is that package's published figure, here reached -by a concrete mechanism rather than a relaxation. +0.001672660197076918), which is that package's published figure. The typed echo +reaches that figure with a concrete word-level mechanism in place of the +relaxation, but the shared histogram and the projected exponent are conditional +pricing: the mechanism delivers them only if a widened `COPY/ERASE` window with +per-pair totals delivery, a common sink, and a reader exposing the intertwiner +`R P = Q R` are admitted, and none of those is established here. **`a < D/E` is a screen, not the acceptance test** (a control enforces this: the exact moment at `D/E` exceeds 1 strictly). The exact moments above are the @@ -122,7 +136,7 @@ own added work is scalar (frame powers, the two 24-ADD copy edges, the boundary schedule), so its recursive overhead is 0 rank units and the elimination lands entirely inside the budget. The measured scalar side also falls (table above). -## The one obstruction: hosting (window lifetime and totals delivery) +## The documented obstruction: hosting (window lifetime and totals delivery) The fused pair defers the first call wrapper's `W -= X` (the ERASE analogue) past the second call's child block. The smallest instance exhibits it exactly: @@ -136,20 +150,29 @@ carry needs the opposite: one window spanning the pair, the first call's totals delivered at the pair end, and uninterrupted ownership of the temporary across the boundary. -Everything else is charged and closes: +What is charged in this package closes: -- **Moment:** the shared ledger above, with `Delta-H` inside the sharp budget. +- **Moment:** the shared ledger above (conditional pricing), with `Delta-H` + inside the sharp budget. - **Scalar price:** fully paid, and smaller than the separate schedule. - **Dirty state and restoration:** exact on all 56 basis columns. + +Three realization obligations are recorded but not closed +([TASK.json](TASK.json) `open_questions`): + +- **Reader/intertwiner realization:** the contract change requires a child + exposing the order-four intertwiner `R P = Q R` (the certified typed + contract; no named host child exposes one), so no selected reader is shown to + implement the typed child. +- **Delivery/lifetime:** one window spanning the pair and a common sink for the + pair's totals, the first blocker of PR #1748. - **Precision:** quantified but not closed (see the open questions); the carry - raises prefix row-L1 from 30 to 42 at the persistent pair. + raises prefix row-L1 from 30 to 42 at the persistent pair, and the complex + host's bucket law is not pinned in a chargeable form. Under the unchanged contract the pair pays both wrappers: the histogram stays `n_8 = 1152`, the moment is exactly the selected one, and no kappa change -follows from 112 saved primitives. The contract change would also require a -child exposing the order-four intertwiner `R P = Q R` (the certified typed -contract; no named host child exposes one) and a common sink for the pair's -totals, the first blocker of PR #1748. +follows from 112 saved primitives. The source-bound side of the same obstruction is already recorded on the named schedule: `research/selected-centre-adjacent-pair-seed01fcb1` censused all 143 @@ -207,8 +230,8 @@ theorem and does not admit any supplier. ## Open next questions - **Does a named selected supplier admit a widened `COPY/ERASE` window with - per-pair totals delivery?** This is the single contract change the - instantiation needs; the shared ledger would then accept at `a* = 0.0031852` + per-pair totals delivery?** This is the contract change the instantiation's + hosting side needs; the shared ledger would then accept at `a* = 0.0031852` and move the binding side to the bit primitive. First step: inspect one retained supplier's owner-map window definitions and totals schedule for a consecutive same-sink pair, and price the widened window as extra live