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..20f5cbb289 --- /dev/null +++ b/research/z4-typed-echo-supplier-instance/README.md @@ -0,0 +1,269 @@ +# 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. 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 +`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 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): + +| 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 (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 +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 would become +bit-limited at `kappa = 0.001730427469823602` (+3.4536% on the selected +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 +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 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: +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. + +What is charged in this package closes: + +- **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, 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 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 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 + 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()