From 815dd9844f1b43a4488ad06d09141a827621078c Mon Sep 17 00:00:00 2001 From: CubeJerry <80299683+CubeJerry@users.noreply.github.com> Date: Wed, 28 Oct 2026 19:11:36 +0800 Subject: [PATCH] Resynthesize selected P104 scalar prefix with 3577 fewer events Exact arbitrary-entry matrix and complete local word checks; scalar allowance 189428 -> 142778. No new kappa. Prepared for @CubeJerry with substantial OpenAI Codex assistance; predecessor credit and source pins in the package. --- research/p104-prefix-row-synthesis/README.md | 233 +++++++++++++ .../p104-prefix-row-synthesis/RESULT.json | 152 ++++++++ .../p104-prefix-row-synthesis/SOURCES.json | 66 ++++ research/p104-prefix-row-synthesis/TASK.json | 165 +++++++++ .../p104-prefix-row-synthesis/VERIFY.json | 32 ++ .../p104-prefix-row-synthesis/synthesize.py | 161 +++++++++ research/p104-prefix-row-synthesis/verify.py | 325 ++++++++++++++++++ 7 files changed, 1134 insertions(+) create mode 100644 research/p104-prefix-row-synthesis/README.md create mode 100644 research/p104-prefix-row-synthesis/RESULT.json create mode 100644 research/p104-prefix-row-synthesis/SOURCES.json create mode 100644 research/p104-prefix-row-synthesis/TASK.json create mode 100644 research/p104-prefix-row-synthesis/VERIFY.json create mode 100644 research/p104-prefix-row-synthesis/synthesize.py create mode 100644 research/p104-prefix-row-synthesis/verify.py diff --git a/research/p104-prefix-row-synthesis/README.md b/research/p104-prefix-row-synthesis/README.md new file mode 100644 index 0000000000..b4d9495d62 --- /dev/null +++ b/research/p104-prefix-row-synthesis/README.md @@ -0,0 +1,233 @@ +# Whole-matrix synthesis saves 3,577 events in the selected P104 prefix + +**Completed local circuit result. No new κ.** On the selected PR6030 word, +replacing its first scalar-only block reduces the complete word from **22,803 +to 19,226 events** and its complete local scalar allowance from **189,428 to +142,778**. Every entry of the block's arbitrary-input matrix is unchanged. +All frame changes, copies, initializations, erasures, helper endpoints and paid +recursive calls retain their original order and values. The selected record +remains κ = 781451/250000000 = 0.003125804. + +The contribution is a reproducible construction and exact certificate for one +local module, not adoption of a new supplier or an implementation benchmark. +It addresses Matarener's [PR5975](https://github.com/CrocSwap/integer-mult-bounds/pull/5975) +open question 2, global ordinary re-synthesis. PR5975 preserves the original +dependency graph through peephole passes; Nick Petalas's +[PR5999](https://github.com/CrocSwap/integer-mult-bounds/pull/5999) shares one +form through a dirty output on PR5907. Here, whole-row sharing and sparse +elimination rebuild the entire 567-role prefix matrix on **PR6030**, crossing +the original internal dependencies while retaining both boundaries. PR6030 +already includes its own substantial ordinary-event rewrite. These savings +are measured against that actual selected word, not the older PR5907 counts. +Classical elimination and row sharing are not claimed as new algorithms. + +## Frozen object and construction + +Base: canonical main `721c03822c421b7f7fcbb2598993b947c4d88419`. +The input is `research/p104-helper470-twin-rung-removal/WORD.json.gz`, SHA256 +`7834725d9e34ee846a9ccc615221ea81e0201613938afa185d2eda0c9a6c232f`. +The selected source head is `772dd10a5859a1d15f4851feb371519789213ad8`, with +portability repair `746ee5e1160ae64a15a81b2a432d5566142db850`; the word is +unchanged by that repair. [SOURCES.json](SOURCES.json) pins every live input +and the historical selected record, source manifest, review, pricing formula, +task card and predecessor notes by Git blob and SHA256. + +Use zero-based event indices. Event 0 is `INIT 778 3`. Events **[1,9896)** +are 9,895 ADD/SCALE instructions in frame 3 (the empty binary basis); event +9896 is the first MOVE. All 567 touched roles are available in that frame. +The other 232 roles are untouched. No observation, COPY, CLEAR or native call +occurs inside this interval. Owned role 778 is live throughout it. + +[synthesize.py](synthesize.py) forms the exact sparse rational matrix M of +this interval, starting with independent symbolic values for all 567 roles, +including role 778. It then: + +1. Greedily subtracts a dyadic multiple of one whole output row from another + when this removes at least two nonzero entries. Ratios have magnitude below + 2^12. Deterministic tie breaks fix the result; the cap is 2,000 steps. +2. Uses sparse Markowitz-style pivots restricted to units of Z[1/2], normalizes + every pivot explicitly, and eliminates its column from every other row. + Failure to find a unit pivot aborts; no general synthesis guarantee is claimed. +3. Removes the final row permutation with charged exchanges. Each exchange is + three ADDs and one SCALE by −1; there are 132, with no free renaming. +4. Reverses the elimination list and inverts each elementary operation. + +The retained run has 419 sharing steps, 795,230 ordered row-pair evaluations +and 567 pivots. The output is 6,039 ADDs and 279 SCALEs. Its maximum absolute +coefficient is 4. Every SCALE is a dyadic unit, every ADD uses distinct roles +already in the same frame, and no extra role or scratch field is introduced. + +The original trial without the sharing pass produced 10,122 events and was +rejected. The refined trial above was the first strict improvement; discovery +stopped there. Only this one matrix was searched. This is neither an exhaustive +circuit search nor an optimality claim. The OS track draw was 31 (complex +supplier), and OS seed 7525094595556296861 modulo three chose this object +from three documented candidates. [TASK.json](TASK.json) records the scope +change from the task card, stopping rules, overlap and checkpoints. + +## Why the substitution is exact + +Write the elementary elimination matrices in chronological order as E1,...,Ek. +The construction checks that Ek...E1 M = I, entry by entry. Chronological +execution of Ek^-1,...,E1^-1 therefore has matrix M. This is a statement about +arbitrary independent entry values, not a test on sample vectors or a use of +the zero value of owned role 778. + +A second implementation in [verify.py](verify.py), using dense integer rows +with binary denominators rather than the synthesizer's sparse Fraction rows, +compares all **321,489** entries of the original and replacement matrices. +The remaining 232 roles are identity in both. The verifier also checks the +replacement followed by its inverse against the literal identity. + +Both programs have the same matrix at the first MOVE, and the original prefix +before the cut and suffix after the cut are kept literally. Thus every later +observation agrees, including every moved field and every helper return. +All scalar operations are in one common chart. Under the inherited common-chart +native contract, this identity acts componentwise at every positive column +multiplicity; the rational scalar coefficients stay outside tensor powers. +No noncommuting native operators are reordered by this replacement. + +As a separate end-to-end finite check, the authenticated, unmodified +`p104-unread-path-resynthesis/local.py` from Ali Romman's PR5827 replays both +complete words using sparse rational rows. Its separate reverse-chronology +dense integer transpose checks all 799 columns and 638,401 coefficients of +the candidate. These are credited predecessor implementations, not newly +independent human review or a formal proof of the multiplication theorem. + +## Complete cost of the local replacement + +For q = ±n/2^d in lowest terms, the retained real ADD allowance is +2(3 + floor(log2 n) + popcount(n) + d). A SCALE by ±2^k costs +2(|k| + [negative sign]). Every source access is an emitted ADD, and every +pivot normalization and permutation operation is included. The prefix needs +no new copy, frame transition, initialization, restoration pass or child call. + +| Quantity | Source | Candidate | +|---|---:|---:| +| Prefix events | 9,895 | 6,318 | +| Prefix scalar allowance | 106,368 | 59,718 | +| Complete local word events | 22,803 | 19,226 | +| Complete local scalar allowance | 189,428 | 142,778 | +| Local routes, normalizers, adapters, lifetime envelope | 5,325,000 | 5,325,000 | +| Complete local ordinary bound | 5,514,428 | 5,467,778 | +| Retained local ordinary allowance | 10,000,000 | 10,000,000 | +| Owned labels / lifetimes / peak occupancy | 29 / 31 / 13 | 29 / 31 / 13 | + +All 3,453 local paid calls are unchanged, with rank counts +`{1:2219, 2:457, 3:496, 4:100, 5:163, 6:11, 7:6, 8:1}` and rank mass 5,952. +The 562 productive helpers retain counts +`{1:14, 2:8, 3:4, 4:107, 5:14, 6:2, 7:9, 8:19, 9:385}`. +Every required scalar source contact is charged and every non-scalar event +remains identical as an ordered sequence, not just a histogram. + +The inherited physical caller makes 18 forward local calls, so the exact +local scalar-allowance reduction sums to **839,700** across those calls. +Its recursive invoice remains 66,834 paid calls and 13,444 productive fields. +The fixed complete ordinary envelope remains **184,647,552 < 10^9**; the +verifier reads this caller envelope from the authenticated source receipt and +recomputes the local routing formula from the unchanged profiles. It does not charge a speculative +new recursive saving or lower that coarse caller envelope. The paid/target +moment, completion, compiler threshold and outer assembly are unchanged. +Therefore no new κ is claimed. + +Both circuits satisfy the same inherited 26,000-event and coefficient bounds. +The conservative scalar growth envelope 2^(16·26000), paid native rank mass, +ownership and storage bounds can be retained. For additional diagnostics, +the exact scalar-prefix maximum row l1 norms are 695/8 before and 343/4 after; +the replacement inverse has maximum 1285/4. These are local matrices relative +to independent cut inputs, not a rounded-error or whole-machine certificate. + +## Reproduce and inspect + +CPython 3.12, standard library only; tested with 3.12.14. From the repository root: + +```sh +python3.12 -B scripts/research_package.py --package research/p104-prefix-row-synthesis +``` + +Expected: both normal and optimized registered commands print +`PASS_P104_PREFIX_ROW_SYNTHESIS`, then the launcher prints +`PASS_REGISTERED_RESEARCH_PACKAGE research/p104-prefix-row-synthesis outcome=completed`. +The launcher also validates exact source provenance and declared live inputs. +Direct scoped verification works without Git after a source export: + +```sh +python3.12 -B research/p104-prefix-row-synthesis/verify.py +python3.12 -O -B research/p104-prefix-row-synthesis/verify.py +``` + +Normal verification writes no repository files. It regenerates the candidate +and compares the entire [RESULT.json](RESULT.json) receipt. To materialize the +complete candidate, add `--emit-word /absolute/external/path/WORD.json`; the +path must be outside the checkout and absent. No compressed candidate copy is +needed. Its canonical JSON payload (sorted keys, compact separators, no trailing +newline) has SHA256 +`537f6c581ee7ebc758d2bba417f6d7b98f1cb9b5fe8916a7ae707575d9b68617`. +The emitted file adds one newline. The receipt also binds the exact prefix and +the dense integer matrix. `--write` is an explicit receipt-generation mode and +refuses to overwrite an existing receipt. + +The positive fixture has matrix `[[1,1/2],[3/4,-13/8]]` and a checked inverse. +Controls reject a wrong ADD sign, omitted SCALE, wrong chart, odd denominator, +unavailable source, whole-word sign fault, and byte corruption of each live +source (word, result and checker). A SCALE by two on the just-initialized owned +role passes the specialized whole-word endpoint check, as expected, but fails +our stronger arbitrary-entry block identity. This explicitly tests the extra +local obligation rather than conflating it with complete-word endpoints. +All checks use explicit exceptions and remain active under `python -O`. +Authenticated executable source is compiled from the bytes just read, so direct +verification cannot silently execute a stale predecessor bytecode cache. + +Executed on 2026-10-28 with CPython 3.12.14: metadata/pins, both registered +replays, committed bytes/source history/executable modes, and the official +10-file export with all three declared inputs passed. Normal and optimized +isolated Python replays of that Git-free export with empty PATH passed in +14.31 and 12.21 seconds. All 11 files including the export manifest retained +their bytes and modes. The export was marked read-only; access-control +enforcement is not claimed. A changed result-receipt saving was rejected in +both modes. These times establish bounded replay, not a circuit runtime gain. +Hosted CI and independent scientific acceptance are not claimed. + +## Scope and inherited obligations + +The selected construction, frozen packages and `upstream/` are unchanged. +This package checks an exact local substitute and the complete scalar word. +It **does not rerun** the full native-map, physical-caller, compiler, precision +or outer-ledger cold replay, and it does not request supplier admission. +Unchanged interfaces and event sequences are the explicit reuse boundary; +changing any source pin, cut, chart, operand set or non-scalar event invalidates +this result. A changed synthesis output must pass the full matrix and word +checks and receive a new committed receipt. + +The five selected framework assumptions remain: `native_all_columns`, +`owned_erasure`, `compiler`, `precision_tape`, `analytic_recovery`. +The uniform word and rounded multiplier are not materialized. No speedup on a +real implementation, stronger exponent, universally optimal circuit, or +independent human acceptance follows from these finite certificates. + +## Open next questions + +- **Adoption through the selected supplier pipeline.** Emit this word, bind it + in a successor package and run the complete selected supplier/native/caller + and precision pipeline. This would make the ordinary saving available to a + later paid-call construction. Independent review and that integration replay + remain blockers; the five framework assumptions are not discharged here. +- **A second disjoint scalar block.** Locate one maximal same-chart interval, + price all permutation and source work, and test its arbitrary-entry matrix. + A fresh overlap check and separate narrow claim are required. No other + interval was searched, and this success gives no guarantee for another one. + +## Credit + +Prepared for **@CubeJerry** with substantial **OpenAI Codex assistance**; +no delegated agents or independent human review. New work is Apache-2.0. +DreamingOfClouds supplied PR6030 and PR5907; Ali Romman supplied PR5827 and +the unmodified local row/transpose checker; Mason Hale supplied PR5811. +Matarener posed the global ordinary-resynthesis question in PR5975, and +Nick Petalas's PR5999 established the earlier dirty-output sharing example. +Those predecessor results are credited, not re-certified here. Douglas +Colkitt supplied the selected application review and portability repair. +David Arias, Cinna Davis, Gareth Davidson, Pierre-Loic Doulcet and the native, +controller, compiler, BIT and analytic contributors retain all predecessor +credit and notices in the source packages. No predecessor files are vendored +or modified by this contribution. diff --git a/research/p104-prefix-row-synthesis/RESULT.json b/research/p104-prefix-row-synthesis/RESULT.json new file mode 100644 index 0000000000..ffec89c42c --- /dev/null +++ b/research/p104-prefix-row-synthesis/RESULT.json @@ -0,0 +1,152 @@ +{ + "after": { + "local": { + "endpoint_coefficients": 638401, + "helpers": { + "1": 14, + "2": 8, + "3": 4, + "4": 107, + "5": 14, + "6": 2, + "7": 9, + "8": 19, + "9": 385 + }, + "owned_fields": 29, + "owned_lifetimes": 31, + "paid": { + "1": 2219, + "2": 457, + "3": 496, + "4": 100, + "5": 163, + "6": 11, + "7": 6, + "8": 1 + }, + "paid_rank_mass": 5952, + "peak_owned_fields": 13, + "public_inputs": 770, + "real_scalar_allowance": 142778 + }, + "max_absolute_prefix_coefficient": "4", + "prefix_events": 6318, + "prefix_opcodes": { + "ADD": 6039, + "SCALE": 279 + }, + "prefix_scalar_allowance": 59718, + "word_events": 19226 + }, + "base_commit": "721c03822c421b7f7fcbb2598993b947c4d88419", + "before": { + "local": { + "endpoint_coefficients": 638401, + "helpers": { + "1": 14, + "2": 8, + "3": 4, + "4": 107, + "5": 14, + "6": 2, + "7": 9, + "8": 19, + "9": 385 + }, + "owned_fields": 29, + "owned_lifetimes": 31, + "paid": { + "1": 2219, + "2": 457, + "3": 496, + "4": 100, + "5": 163, + "6": 11, + "7": 6, + "8": 1 + }, + "paid_rank_mass": 5952, + "peak_owned_fields": 13, + "public_inputs": 770, + "real_scalar_allowance": 189428 + }, + "prefix_events": 9895, + "prefix_opcodes": { + "ADD": 9747, + "SCALE": 148 + }, + "prefix_scalar_allowance": 106368, + "word_events": 22803 + }, + "canonical_sha256": { + "complete_candidate_word": "537f6c581ee7ebc758d2bba417f6d7b98f1cb9b5fe8916a7ae707575d9b68617", + "integer_prefix_matrix": "996f353928fe33d6c9c5f3bf0b326b6e616946b163fc2e3e29ea7384ef294aa9", + "replacement_prefix": "d00621885ffabffe13f71cd680867a04a18b64aaf2b059850c248f9395cb80ab" + }, + "complete_columns": { + "arithmetic": "Dense integer rows with binary denominators; reverse chronology", + "coefficients": 638401, + "columns": 799 + }, + "controls": { + "damaged_RESULT.json": "Source SHA256: research/p104-helper470-twin-rung-removal/RESULT.json", + "damaged_WORD.json.gz": "Source SHA256: research/p104-helper470-twin-rung-removal/WORD.json.gz", + "damaged_local.py": "Source SHA256: research/p104-unread-path-resynthesis/local.py", + "dyadic_inverse_positive_fixture": "PASS", + "missing_SCALE": "Arbitrary-entry prefix matrix", + "odd_denominator": "Nonzero dyadic coefficient", + "owned_zero_specialization": "Arbitrary-entry prefix matrix", + "owned_zero_specialization_whole_word": "PASS as expected; only the stronger local obligation rejects it", + "unavailable_source": "Available distinct source", + "whole_word_wrong_sign": "All public and owned rows", + "wrong_ADD_sign": "Arbitrary-entry prefix matrix", + "wrong_chart": "Available scalar chart" + }, + "cut": { + "explicit_matrix_entries": 321489, + "frame": 3, + "roles": 567, + "start_inclusive": 1, + "stop_exclusive": 9896, + "untouched_roles": 232 + }, + "discovery": { + "charged_exchanges": 132, + "entries_after_pair_steps": 4380, + "pair_evaluations": 795230, + "pair_steps": 419, + "roles": 567, + "unit_pivots": 567 + }, + "inherited_budgets": { + "complete_caller_allowance": 1000000000, + "complete_caller_envelope_recomputed": false, + "complete_caller_ordinary_envelope": 184647552, + "local_allowance": 10000000, + "local_ordinary_after": 5467778, + "local_ordinary_before": 5514428, + "local_routes_normalizers_adapters_and_lifetimes": 5325000, + "native_and_physical_caller_replayed": false, + "paid_calls": 66834, + "productive_fields": 13444 + }, + "kappa": { + "changed": false, + "claim": "No new kappa; isolated scalar-circuit result.", + "selected": "781451/250000000" + }, + "prefix_max_row_l1": { + "candidate": "343/4", + "candidate_inverse": "1285/4", + "scope": "Exact intermediate scalar prefix matrices only; not a rounded error analysis.", + "source": "695/8" + }, + "saved": { + "events_per_local_call": 3577, + "inherited_full_forward_calls": 18, + "scalar_allowance_across_inherited_forward_calls": 839700, + "scalar_allowance_per_local_call": 46650 + }, + "status": "PASS_P104_PREFIX_ROW_SYNTHESIS" +} diff --git a/research/p104-prefix-row-synthesis/SOURCES.json b/research/p104-prefix-row-synthesis/SOURCES.json new file mode 100644 index 0000000000..59ad71f332 --- /dev/null +++ b/research/p104-prefix-row-synthesis/SOURCES.json @@ -0,0 +1,66 @@ +{ + "schema_version": 1, + "base_commit": "721c03822c421b7f7fcbb2598993b947c4d88419", + "files": [ + { + "path": "certificates/frontier6030-source.json", + "usage": "provenance", + "git_blob": "e58847094e2f631665030bb6f045f8bebe638c6c", + "sha256": "95ddc380f6b05499fccd8820ab7f84fb6d287b4e66a721ed41ca9d293c4eaa3e" + }, + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a", + "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "docs/research/pr-intake-evidence/pr6030-audit/PROOF-REVIEW.md", + "usage": "provenance", + "git_blob": "26f2f6324bce57e69e861d2aae5a27c9de325a8e", + "sha256": "8bd158b8ef68202000f167b9b78db0b31531b5b067b5cbd91b5bf35f3ddd1ab6" + }, + { + "path": "research/p104-dirty-anchor-window/README.md", + "usage": "provenance", + "git_blob": "fd4cee7b4afce0717161f9554d7e6e723c14fc53", + "sha256": "786c2c086bc4d81a6e7319a1fc27e5aa58729fa44734dd83dcea759ec23e70e6" + }, + { + "path": "research/p104-helper470-twin-rung-removal/RESULT.json", + "usage": "input", + "git_blob": "e4a03118d585fb80c9ac932281b528ac394ccc5f", + "sha256": "84fcbe2a0b64307b5703c363408042bdd91555b0419509aa50daa43b3b1924ad" + }, + { + "path": "research/p104-helper470-twin-rung-removal/WORD.json.gz", + "usage": "input", + "git_blob": "22f9ab02d1b73ea0aa4b07ce445a14cc2602c760", + "sha256": "7834725d9e34ee846a9ccc615221ea81e0201613938afa185d2eda0c9a6c232f" + }, + { + "path": "research/p104-helper470-twin-rung-removal/pricing.py", + "usage": "provenance", + "git_blob": "65bb723f8558dc60ff92764db1a43d8bf438aa09", + "sha256": "3c6cf2966ccfe5a5fb6c90f89f46ac224ea455127e35dd34975683c68c36d710" + }, + { + "path": "research/p104-ordinary-event-compression/README.md", + "usage": "provenance", + "git_blob": "24b801f472f2bcf7a2afd5d93fceb8da9850e5ce", + "sha256": "932d3342bd1238f25b529f0edc5d841a9c7d1f0cd67200c9b2a1350365f4068c" + }, + { + "path": "research/p104-unread-path-resynthesis/local.py", + "usage": "input", + "git_blob": "b7be846b10c4c54a4e1558d7b563bc8c3a170223", + "sha256": "7201df8e32f5c99f7403150e8664042322037906088bc754c67293a241368597" + } + ] +} diff --git a/research/p104-prefix-row-synthesis/TASK.json b/research/p104-prefix-row-synthesis/TASK.json new file mode 100644 index 0000000000..a8817ae321 --- /dev/null +++ b/research/p104-prefix-row-synthesis/TASK.json @@ -0,0 +1,165 @@ +{ + "schema_version": 1, + "task_id": "complex-new-helper-inventory", + "priority_revision": 8, + "base_commit": "721c03822c421b7f7fcbb2598993b947c4d88419", + "original_card": { + "id": "complex-new-helper-inventory", + "question": "Can a changed helper inventory earn productive credit that survives completion, compilation and the actual caller?", + "starting_points": [ + "docs/research/current-priorities.md", + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md" + ], + "methods": [ + "Construct and independently check one source-bound instance of the stated first experiment.", + "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change." + ], + "acceptance_gate": "A source-bound arbitrary-input identity and legal producer/consumer boundary with the complete paid and productive target invoice, including restoration, ownership, native alignment and extra charges. Price under the actual current model; historical ceiling.py assumptions must be established before use. A favorable optimistic relaxation keeps a route open but is not a completed supplier. A scoped local result remains useful; expansion requires the family-level budget gate.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.", + "scope": "Source-bound orientation only, not a supplier replay or theorem proof." + }, + "first_experiment": "Specify all arbitrary inputs, owned fields, restored outputs and a physically legal consumer. Compare complete P and T, including target debits and precision/stock costs. #5599 is a positive control for target refinement, not permission to split every helper for free. #5614 is a hypothetical compiler budget, not an emitted 145-split word. Stop at the first unpaid boundary or a failing optimistic full bill.", + "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.", + "allowed_variations": [ + "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes." + ], + "scope_change_triggers": [ + "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.", + "Treating an archived proposal or local numerical pass as complete supplier admission." + ], + "overlap_terms": [ + "productive helper", + "target refinement", + "5599", + "5614" + ], + "existing_checks": [ + { + "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.", + "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.", + "status": "reviewed", + "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137", + "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Resynthesize the selected PR6030 all-chart-3 scalar prefix at event indices [1,9896) by sparse dyadic row elimination, preserving its complete matrix on arbitrary entries, all non-scalar events, all 799 whole-word endpoints and the complete ordinary tariff.", + "scope_change_reason": "Take PR5975 open next question 2 (global ordinary resynthesis), beyond its peephole passes and PR5999 single dirty-anchor window. This is a scoped complex-circuit side result; it changes no productive helper inventory or recursive moment.", + "bottleneck_link": "A smaller exact circuit reduces ordinary allowance and event use in the actual selected supplier. No native, caller, compiler or exponent improvement is inferred.", + "budget_minutes": 120, + "stop_rule": "One bounded sparse elimination experiment; retain only a strict reduction in both event count and full scalar allowance with exact local and whole-word checks. Stop discovery by 90 minutes and reserve final 30 for verification/publication.", + "outcome": "completed", + "evidence": "RESULT.json: prefix 9895 -> 6318 events; complete local scalar allowance 189428 -> 142778; arbitrary-entry matrix, full 799 rows/columns, source pins and rejection controls. No new kappa.", + "author": "@CubeJerry, with substantial OpenAI Codex assistance", + "ai_assistance": "Substantial OpenAI Codex assistance; no subagents or independent human review.", + "open_questions": [ + { + "question": "Can this scalar prefix be adopted through the selected full supplier pipeline?", + "why_it_matters": "It reduces ordinary work and leaves more event budget for a future paid-call edit. It does not change any paid or productive histogram.", + "first_step": "Emit the complete candidate word with verify.py --emit-word, bind it as a new successor input, and run the selected cold supplier/caller/native/precision pipeline without editing the frozen predecessor.", + "blocked_by": "Independent review and complete integration replay; five inherited framework assumptions remain." + }, + { + "question": "Does a second, disjoint same-chart scalar block admit a reduction under the same complete tariff?", + "why_it_matters": "The present result supports whole-matrix synthesis beyond the earlier peephole search, but establishes no general optimality or guaranteed extension.", + "first_step": "Locate one maximal scalar-only interval, price its full substitution including permutations, then check its arbitrary-entry matrix before expanding scope.", + "blocked_by": "A fresh overlap check and separate narrow claim; no additional interval was searched here." + } + ], + "claim": { + "recorded_utc": "2026-10-28T10:41:46.538197+00:00", + "track": "complex supplier", + "os_track_seed": 31, + "os_diversification_seed": 7525094595556296861, + "picker_seed": "0000000000000000686f81b4f4d57e9d", + "picker_note": "Explicit track; picker nonce was separately supplied, not an OS draw. Object choice uses OS diversification seed modulo 3 = 0.", + "expected_finish_utc": "2026-10-28T12:31:30Z", + "coordination": "No sprint coordination issue found in live open-issue and sprint searches. Local claim retained. GitHub plugin lacks Discussion writes and gh is unavailable; public handoff/start-here/current board read via HTTPS.", + "candidates": [ + { + "object": "PR6030 chart-3 prefix [1,9896)", + "method": "Whole-matrix sparse dyadic elimination, complete tariff and arbitrary-entry proof", + "decision": "selected; seed mod 3 = 0; takes PR5975 open question 2 with a changed synthesis class" + }, + { + "object": "PR6030 helpers469/471 shared frame593 source acquisition", + "method": "Joint donor/receiver basis modification", + "decision": "deferred; PR6069/6084 already close natural fixed-donor subcases; new physical access not yet priced" + }, + { + "object": "PR5698 restricted-C binary coframe optimum", + "method": "One nonbinary Lagrangian move beyond the closed 423-choice class", + "decision": "deferred; native/caller completion cost unresolved" + } + ], + "result": "Completed exact scalar-prefix substitute: 3577 events and 46650 local scalar allowance units saved; no new kappa. Local claim used because no sprint coordination issue exists in the inspected live open issues.", + "result_branch": "https://github.com/CubeJerry/integer-mult-bounds/tree/research/seed31-p104-prefix-synthesis-20261028" + }, + "checkpoints": [ + { + "utc": "2026-10-28T10:41:46.538214+00:00", + "main": "721c03822c421b7f7fcbb2598993b947c4d88419", + "priority_revision": 8, + "selected": "PR6030, 781451/250000000", + "decision": "Start isolated circuit side result; preserve selected word and all predecessor inputs." + }, + { + "utc": "2026-10-28T11:01:54Z", + "main": "721c03822c421b7f7fcbb2598993b947c4d88419", + "priority_revision": 8, + "selected": "PR6030, 781451/250000000", + "decision": "Canonical origin/main freshly fetched, unchanged from the scientific base. Guidance, selected certificate, review and source pins unchanged. Freeze the verified positive candidate and finish packaging; no second research round." + }, + { + "utc": "2026-10-28T11:10:28.946578+00:00", + "main": "721c03822c421b7f7fcbb2598993b947c4d88419", + "priority_revision": 8, + "selected": "PR6030, 781451/250000000", + "decision": "Before publication: canonical main freshly fetched and still identical to base; final live PR/visible Discussion overlap checked, no same-prefix contribution identified. Registered normal/optimized and Git-free replays pass. Publish one completed local module; preserve all frozen inputs." + } + ], + "milestone": "Completed local module; not supplier adoption or a new exponent claim.", + "optimistic_cost_gate": "Every source access is an emitted ADD; all normalizations and exchanges are charged. No new live field, copy, boundary, restoration, frame change, recursive child or helper is permitted. Require strict savings in both total scalar tariff and event count; retain original fixed routing/precision envelopes.", + "search": { + "domain": "Only selected PR6030 event indices [1,9896), all in frame 3; exact dyadic ADD and dyadic-unit SCALE on its existing 567 roles.", + "seed_use": "OS seed 7525094595556296861 modulo 3 selected object 0. Synthesis and its tie breaks are deterministic, not randomized.", + "methods_tested": [ + "Sparse unit-pivot elimination without prior row sharing: 10122 events, rejected because the 9895-event source was smaller.", + "Whole-row sharing followed by sparse unit-pivot elimination: 6318 events, accepted after exact verification." + ], + "completed_coverage": "One frozen matrix; 795230 ordered row-pair evaluations over 419 greedy reductions, 567 unit pivots and 132 charged exchanges. Not exhaustive over circuits.", + "stopping_rule": "Stop at first verified strict improvement; row-sharing cap 2000, require nonzero-count reduction at least 2, dyadic ratio magnitude < 2^12; abort if no unit pivot. No further search after the positive candidate.", + "optimality_claim": false + }, + "overlap": { + "initial": "Local helper searched 8348 records; live open PRs and targeted all-state searches inspected. Prior selected review and relevant ledger entries read.", + "nearest_predecessors": { + "5975": "Matarener peepholes on PR5907; explicitly hands off global ordinary re-synthesis.", + "5999": "Nick Petalas two-output dirty-anchor sharing on PR5907, not full-prefix matrix synthesis.", + "6030": "DreamingOfClouds selected word includes its own scalar rewrite; this package compares against that exact word." + }, + "related_closed_or_scoped_classes": [ + "PR5698 restricted binary coframe optimum", + "PR6069 fixed incoming-only carrier intervals", + "PR6084 receiver-only helper469 recoding", + "PR6088 helper572 two-ADD seam" + ], + "new_concurrent_work": "PR6115 deferred-layer/stock audit read at final overlap refresh; distinct object and no dependency used.", + "coverage_limits": "Live latest 100 updated open PRs, targeted all-state searches, local notes/ledger and visible public Discussion comments. No claim of complete unpublished or paginated Discussion coverage; gh is unavailable and the plugin exposes no Discussion posting tool.", + "final_visible_discussion_comments": { + "1166": 48, + "1167": 37 + } + } +} diff --git a/research/p104-prefix-row-synthesis/VERIFY.json b/research/p104-prefix-row-synthesis/VERIFY.json new file mode 100644 index 0000000000..b19d4904b6 --- /dev/null +++ b/research/p104-prefix-row-synthesis/VERIFY.json @@ -0,0 +1,32 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/p104-helper470-twin-rung-removal/RESULT.json", + "research/p104-helper470-twin-rung-removal/WORD.json.gz", + "research/p104-unread-path-resynthesis/local.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Pinned inputs; deterministic synthesis; all arbitrary-entry prefix coefficients; source and candidate whole-word rows; all 799 transpose columns; exact full scalar tariff; meaningful invalid-source, arithmetic and chart controls." + }, + { + "argv": [ + "{python}", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Repeat the same proof-relevant coverage and rejection controls with Python assertions disabled." + } + ] +} diff --git a/research/p104-prefix-row-synthesis/synthesize.py b/research/p104-prefix-row-synthesis/synthesize.py new file mode 100644 index 0000000000..7ab0c01971 --- /dev/null +++ b/research/p104-prefix-row-synthesis/synthesize.py @@ -0,0 +1,161 @@ +"""Deterministic dyadic row synthesis of one frozen P104 scalar prefix. + +Prepared for @CubeJerry with substantial OpenAI Codex assistance. +Sparse elimination and row sharing are classical; the source application is new. +Apache-2.0. No claim of circuit optimality. +""" +from collections import Counter, defaultdict +from fractions import Fraction as Q + +START, STOP, FRAME = 1, 9896, 3 +MAX_PAIR_STEPS = 2000 + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def is_unit(value): + numerator = abs(value.numerator) + return bool(numerator) and numerator & (numerator - 1) == 0 + + +def add_row(destination, source, coefficient): + for column, value in source.items(): + result = destination.get(column, 0) + coefficient * value + if result: + destination[column] = result + else: + destination.pop(column, None) + + +def prefix_matrix(program): + roles = sorted({e[1] for e in program} + | {e[2] for e in program if e[0] == "ADD"}) + rows = {role: {role: Q(1)} for role in roles} + for event in program: + need(event[0] in ("ADD", "SCALE") and event[-1] == FRAME, + "Only the fixed scalar chart may be synthesized") + destination, coefficient = event[1], Q(event[-2]) + if event[0] == "ADD": + need(destination != event[2], "Distinct ADD operands") + add_row(rows[destination], rows[event[2]], coefficient) + else: + rows[destination] = {k: coefficient * v + for k, v in rows[destination].items()} + return rows + + +def best_reduction(rows, destination, source): + left, right = rows[destination], rows[source] + common = left.keys() & right.keys() + if 2 * len(common) - len(right) < 2: + return None + ratios = Counter(left[k] / right[k] for k in sorted(common)) + choices = [(len(common) + count - len(right), + -abs(q.numerator).bit_length() - q.denominator.bit_length(), q) + for q, count in ratios.items() + if q.denominator & (q.denominator - 1) == 0 and abs(q) < 2**12] + if not choices: + return None + gain, _, ratio = max(choices) + return (gain, destination, source, -ratio) if gain >= 2 else None + + +def synthesize(program): + """Return a literal replacement and discovery counts, without writing files.""" + rows = prefix_matrix(program) + operations = [] + + def add(destination, source, coefficient): + add_row(rows[destination], rows[source], coefficient) + operations.append(["ADD", destination, source, str(coefficient), FRAME]) + + def scale(destination, coefficient): + rows[destination] = {k: v * coefficient + for k, v in rows[destination].items()} + operations.append(["SCALE", destination, str(coefficient), FRAME]) + + # Whole-row sharing can cross the original dependency graph: both endpoints + # of the entire prefix, rather than its internal observations, are retained. + candidates = {} + evaluations = 0 + for destination in rows: + for source in rows: + if destination != source: + evaluations += 1 + choice = best_reduction(rows, destination, source) + if choice: + candidates[destination, source] = choice + pair_steps = 0 + while candidates: + need(pair_steps < MAX_PAIR_STEPS, "Row-sharing step limit") + _, destination, source, coefficient = max(candidates.values()) + add(destination, source, coefficient) + pair_steps += 1 + for key in [key for key in candidates if destination in key]: + del candidates[key] + for other in rows: + if other == destination: + continue + for left, right in ((destination, other), (other, destination)): + evaluations += 1 + choice = best_reduction(rows, left, right) + if choice: + candidates[left, right] = choice + sparse_entries = sum(map(len, rows.values())) + + # Markowitz-style sparse pivots, restricted to units in Z[1/2]. Every + # pivot normalization and every final permutation is an emitted operation. + remaining_rows, remaining_columns = set(rows), set(rows) + while remaining_columns: + column_rows = defaultdict(list) + for row in sorted(remaining_rows): + for column in rows[row]: + if column in remaining_columns: + column_rows[column].append(row) + choices = [] + for row in sorted(remaining_rows): + for column, value in rows[row].items(): + if column in remaining_columns and is_unit(value): + count = len(column_rows[column]) + choices.append(((len(rows[row]) - 1) * (count - 1), + len(rows[row]), count, + abs(value.numerator).bit_length() + + value.denominator.bit_length(), + row != column, row, column)) + need(bool(choices), "No dyadic-unit pivot; no circuit emitted") + *_, pivot, column = min(choices) + if rows[pivot][column] != 1: + scale(pivot, 1 / rows[pivot][column]) + for destination in rows: + if destination != pivot and column in rows[destination]: + add(destination, pivot, -rows[destination][column]) + remaining_rows.remove(pivot) + remaining_columns.remove(column) + + exchanges = 0 + for row in rows: + if rows[row] == {row: Q(1)}: + continue + other = next(k for k, value in rows.items() if value == {row: Q(1)}) + add(row, other, Q(1)) + add(other, row, Q(-1)) + add(row, other, Q(1)) + scale(other, Q(-1)) + exchanges += 1 + need(all(value == {row: Q(1)} for row, value in rows.items()), + "Elimination must end at the literal identity") + + # If E_k ... E_1 M = I, then M = E_1^-1 ... E_k^-1. Chronological + # execution therefore uses the inverses in reverse list order. + replacement = [] + for original in reversed(operations): + event = original.copy() + event[-2] = str(-Q(event[-2]) if event[0] == "ADD" else 1 / Q(event[-2])) + replacement.append(event) + return replacement, {"roles": len(rows), "pair_steps": pair_steps, + "pair_evaluations": evaluations, + "entries_after_pair_steps": sparse_entries, + "unit_pivots": len(rows), "charged_exchanges": exchanges} diff --git a/research/p104-prefix-row-synthesis/verify.py b/research/p104-prefix-row-synthesis/verify.py new file mode 100644 index 0000000000..71d41588d4 --- /dev/null +++ b/research/p104-prefix-row-synthesis/verify.py @@ -0,0 +1,325 @@ +#!/usr/bin/env python3 +"""Exact, source-bound local circuit check; not a full theorem verification. + +Prepared for @CubeJerry with substantial OpenAI Codex assistance. Apache-2.0. +The whole-word row/column checks are credited, authenticated predecessor code. +The dense integer prefix check below is separate from the sparse synthesizer. +""" +import argparse +from collections import Counter +from copy import deepcopy +from fractions import Fraction as Q +import gzip +from hashlib import sha256 +import json +from pathlib import Path +import tempfile +from types import ModuleType + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +SOURCE = "research/p104-helper470-twin-rung-removal/" +LOCAL = "research/p104-unread-path-resynthesis/local.py" +START, STOP, FRAME = 1, 9896, 3 + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def canonical(value): + # Round-trip first so that all mapping keys have their JSON string form. + return json.dumps(json.loads(json.dumps(value)), sort_keys=True, + separators=(",", ":")).encode() + + +def digest(value): + return sha256(canonical(value)).hexdigest() + + +def load_code(raw, path, name): + """Execute the bytes just read, never a preexisting bytecode cache.""" + module = ModuleType(name) + module.__file__ = str(path) + exec(compile(raw, str(path), "exec"), module.__dict__) + return module + + +def authenticated_inputs(root): + manifest = json.loads((HERE / "SOURCES.json").read_bytes()) + data = {} + for item in manifest["files"]: + if item["usage"] == "input": + raw = (root / item["path"]).read_bytes() + need(sha256(raw).hexdigest() == item["sha256"], + "Source SHA256: " + item["path"]) + data[item["path"]] = raw + need(set(data) == {SOURCE + "WORD.json.gz", SOURCE + "RESULT.json", LOCAL}, + "Complete live source inventory") + return data + + +def check_alphabet(program, available): + for event in program: + need(event[0] in ("ADD", "SCALE"), "Scalar-only prefix") + need(len(event) == (5 if event[0] == "ADD" else 4), "Event arity") + need(event[-1] == FRAME and event[1] in available, "Available scalar chart") + q = Q(event[-2]) + n, d = abs(q.numerator), q.denominator + need(q and d & (d - 1) == 0, "Nonzero dyadic coefficient") + need(abs(q) + 1 < 2**16, "Inherited fixed coefficient bound") + if event[0] == "SCALE": + need(n & (n - 1) == 0, "Invertible dyadic SCALE") + else: + need(event[2] in available and event[1] != event[2], "Available distinct source") + + +def integer_matrix(program, roles): + """All entries, with one integer numerator row and binary denominator. + + This does not call the synthesizer's Fraction/sparse row routines. It + checks arbitrary independent entry values, including the owned role. + """ + index = {role: i for i, role in enumerate(roles)} + size = len(roles) + rows = [[int(i == j) for j in range(size)] for i in range(size)] + exponents = [0] * size + max_l1 = Q(1) + for event in program: + destination = index[event[1]] + q = Q(event[-2]) + numerator, denominator = q.numerator, q.denominator + need(denominator & (denominator - 1) == 0, "Integer engine dyadic input") + shift = denominator.bit_length() - 1 + if event[0] == "SCALE": + rows[destination] = [numerator * x for x in rows[destination]] + exponents[destination] += shift + else: + need(event[0] == "ADD", "Integer engine opcode") + source = index[event[2]] + level = max(exponents[destination], exponents[source] + shift) + a = 1 << (level - exponents[destination]) + b = numerator << (level - exponents[source] - shift) + rows[destination] = [a * x + b * y for x, y in + zip(rows[destination], rows[source])] + exponents[destination] = level + while exponents[destination] and all(x % 2 == 0 for x in rows[destination]): + rows[destination] = [x // 2 for x in rows[destination]] + exponents[destination] -= 1 + max_l1 = max(max_l1, Q(sum(map(abs, rows[destination])), + 1 << exponents[destination])) + return {"rows": rows, "exponents": exponents}, str(max_l1) + + +def inverse(program): + answer = [] + for original in reversed(program): + event = original.copy() + q = Q(event[-2]) + event[-2] = str(-q if event[0] == "ADD" else 1 / q) + answer.append(event) + return answer + + +def scalar_allowance(program): + total = 0 + for event in program: + op = event[0] + if op in ("INIT", "CLEAR"): + total += 2 + elif op == "MOVE": + continue + else: + q = Q(event[-2]) + n, d = abs(q.numerator), q.denominator + if op == "SCALE": + total += 2 * (abs(n.bit_length() - d.bit_length()) + int(q < 0)) + else: + need(op in ("ADD", "COPY"), "Tariff opcode") + total += 2 * (3 + n.bit_length() - 1 + n.bit_count() + d.bit_length() - 1) + return total + + +def rejected(check, label): + try: + check() + except ValueError as error: + return str(error) + raise ValueError("Negative control unexpectedly accepted: " + label) + + +def controls(prefix, roles, matrix, available, candidate, local, inputs): + results = {} + def mismatch(program): + need(integer_matrix(program, roles)[0] == matrix, "Arbitrary-entry prefix matrix") + + wrong_sign = deepcopy(prefix) + add_index = next(i for i, event in enumerate(prefix) if event[0] == "ADD") + wrong_sign[add_index][-2] = str(-Q(wrong_sign[add_index][-2])) + results["wrong_ADD_sign"] = rejected(lambda: mismatch(wrong_sign), "ADD sign") + missing_scale = deepcopy(prefix) + del missing_scale[next(i for i, event in enumerate(prefix) if event[0] == "SCALE")] + results["missing_SCALE"] = rejected(lambda: mismatch(missing_scale), "SCALE omission") + # The actual owned role is initialized to zero immediately before the cut. + # Multiplying it there by two is invisible to that specialization, but must + # fail the stronger arbitrary-entry local certificate. + results["owned_zero_specialization"] = rejected( + lambda: mismatch([["SCALE", 778, "2", FRAME]] + prefix), "Owned zero assumption") + specialized = deepcopy(candidate) + specialized["program"].insert(START, ["SCALE", 778, "2", FRAME]) + local.replay(specialized) + results["owned_zero_specialization_whole_word"] = "PASS as expected; only the stronger local obligation rejects it" + for name, changed in (("wrong_chart", deepcopy(prefix)), + ("odd_denominator", deepcopy(prefix)), + ("unavailable_source", deepcopy(prefix))): + if name == "wrong_chart": + changed[add_index][-1] = 7 + elif name == "odd_denominator": + changed[add_index][-2] = "1/3" + else: + need(0 not in available, "Unavailable-source control fixture") + changed[add_index][2] = 0 + results[name] = rejected(lambda: check_alphabet(changed, available), name) + damaged = deepcopy(candidate) + damaged["program"][START + add_index][-2] = wrong_sign[add_index][-2] + results["whole_word_wrong_sign"] = rejected(lambda: local.replay(damaged), "Whole-word sign") + with tempfile.TemporaryDirectory(prefix="p104-prefix-control-") as temporary: + root = Path(temporary) + for path, raw in inputs.items(): + destination = root / path + destination.parent.mkdir(parents=True, exist_ok=True) + destination.write_bytes(raw) + for path, raw in inputs.items(): + (root / path).write_bytes(raw + b" ") + results["damaged_" + Path(path).name] = rejected( + lambda: authenticated_inputs(root), path) + (root / path).write_bytes(raw) + fixture = [["ADD", 4, 9, "1/2", FRAME], ["SCALE", 9, "-2", FRAME], + ["ADD", 9, 4, "3/4", FRAME]] + need(integer_matrix(fixture, [4, 9])[0] + == {"rows": [[2, 1], [6, -13]], "exponents": [1, 3]}, + "Integer engine explicit positive fixture") + need(integer_matrix(fixture + inverse(fixture), [4, 9])[0] + == integer_matrix([], [4, 9])[0], "Integer engine inverse positive fixture") + results["dyadic_inverse_positive_fixture"] = "PASS" + return results + + +def run(): + inputs = authenticated_inputs(ROOT) + source = json.loads(gzip.decompress(inputs[SOURCE + "WORD.json.gz"])) + source_result = json.loads(inputs[SOURCE + "RESULT.json"]) + local = load_code(inputs[LOCAL], ROOT / LOCAL, "p104_credited_local") + synthesis = load_code((HERE / "synthesize.py").read_bytes(), HERE / "synthesize.py", "prefix_synthesis") + program = source["program"] + need(len(program) == 22803 and program[0] == ["INIT", 778, FRAME], "Frozen prefix entry") + need(program[STOP][0] == "MOVE" and source["frames"][FRAME] == [], "Frozen prefix exit/chart") + old_prefix = program[START:STOP] + roles = sorted({event[1] for event in old_prefix} + | {event[2] for event in old_prefix if event[0] == "ADD"}) + available = {i for i, frame in enumerate(source["initial"]) if frame == FRAME} | {778} + need(set(roles) <= available, "All touched roles available at entry") + check_alphabet(old_prefix, available) + replacement, discovery = synthesis.synthesize(old_prefix) + check_alphabet(replacement, set(roles)) + old_matrix, old_norm = integer_matrix(old_prefix, roles) + new_matrix, new_norm = integer_matrix(replacement, roles) + need(new_matrix == old_matrix, "Exact arbitrary-entry prefix equality") + need(integer_matrix(replacement + inverse(replacement), roles)[0] + == integer_matrix([], roles)[0], "Complete inverse-prefix identity") + _, inverse_norm = integer_matrix(inverse(replacement), roles) + candidate = deepcopy(source) + candidate["program"] = program[:START] + replacement + program[STOP:] + need({k: v for k, v in candidate.items() if k != "program"} + == {k: v for k, v in source.items() if k != "program"}, "All boundary and frame metadata unchanged") + need([e for e in candidate["program"] if e[0] not in ("ADD", "SCALE")] + == [e for e in program if e[0] not in ("ADD", "SCALE")], "All non-scalar events unchanged") + old_local, new_local = local.replay(source), local.replay(candidate) + need(canonical(old_local) == canonical(source_result["local"]), "Pinned source receipt replay") + for key in old_local: + if key != "real_scalar_allowance": + need(old_local[key] == new_local[key], "Unchanged local invoice: " + key) + old_cost, new_cost = scalar_allowance(program), scalar_allowance(candidate["program"]) + need(old_cost == old_local["real_scalar_allowance"] + and new_cost == new_local["real_scalar_allowance"], "Separate complete scalar tariff") + need(len(replacement) < len(old_prefix) and new_cost < old_cost, "Strict event and allowance savings") + columns = local.reverse_columns(candidate) + negative_controls = controls(replacement, roles, old_matrix, available, candidate, local, inputs) + calls = source_result["physical_caller"]["full_calls"] + # Retain, rather than tighten, PR6030 pricing.py's complete envelopes. + # Its native/caller implementation assumptions are inherited, not replayed. + ports = len(candidate["live"]) + local_routes = (sum(new_local["paid"].values()) + 2 * sum(new_local["helpers"].values()) + + 2 * ports + 4 * ports + 4 * new_local["owned_lifetimes"]) * 1000 + need(local_routes == source_result["complete_cost"]["nonrecursive"]["local_routes"], + "Unchanged route, normalizer, adapter and lifetime envelope") + need(new_cost + local_routes < 10**7, "Complete local ordinary budget") + raw = source_result["complete_cost"]["nonrecursive"]["raw_scalar_upper"] + need(raw < 10**9, "Pinned inherited caller ordinary envelope") + receipt = { + "status": "PASS_P104_PREFIX_ROW_SYNTHESIS", + "base_commit": json.loads((HERE / "SOURCES.json").read_bytes())["base_commit"], + "cut": {"start_inclusive": START, "stop_exclusive": STOP, "frame": FRAME, + "roles": len(roles), "explicit_matrix_entries": len(roles)**2, + "untouched_roles": source["public"] + source["owned_fields"] - len(roles)}, + "discovery": discovery, + "before": {"prefix_events": len(old_prefix), "word_events": len(program), + "prefix_opcodes": dict(Counter(e[0] for e in old_prefix)), + "prefix_scalar_allowance": scalar_allowance(old_prefix), "local": old_local}, + "after": {"prefix_events": len(replacement), "word_events": len(candidate["program"]), + "prefix_opcodes": dict(Counter(e[0] for e in replacement)), + "max_absolute_prefix_coefficient": str(max(abs(Q(e[-2])) for e in replacement)), + "prefix_scalar_allowance": scalar_allowance(replacement), "local": new_local}, + "saved": {"events_per_local_call": len(old_prefix) - len(replacement), + "scalar_allowance_per_local_call": old_cost - new_cost, + "inherited_full_forward_calls": calls, + "scalar_allowance_across_inherited_forward_calls": calls * (old_cost - new_cost)}, + "canonical_sha256": {"replacement_prefix": digest(replacement), + "complete_candidate_word": digest(candidate), + "integer_prefix_matrix": digest(new_matrix)}, + "prefix_max_row_l1": {"source": old_norm, "candidate": new_norm, + "candidate_inverse": inverse_norm, + "scope": "Exact intermediate scalar prefix matrices only; not a rounded error analysis."}, + "complete_columns": columns, + "inherited_budgets": {"local_routes_normalizers_adapters_and_lifetimes": local_routes, + "local_ordinary_before": old_cost + local_routes, + "local_ordinary_after": new_cost + local_routes, + "local_allowance": 10**7, + "complete_caller_ordinary_envelope": raw, + "complete_caller_allowance": 10**9, + "complete_caller_envelope_recomputed": False, + "paid_calls": source_result["complete_cost"]["paid_calls"], + "productive_fields": source_result["complete_cost"]["productive_fields"], + "native_and_physical_caller_replayed": False}, + "controls": negative_controls, + "kappa": {"changed": False, "selected": source_result["complete_cost"]["kappa"], + "claim": "No new kappa; isolated scalar-circuit result."}, + } + return receipt, candidate + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--write", action="store_true", help="Create an absent RESULT.json after all checks") + parser.add_argument("--emit-word", type=Path, help="Create an absent JSON word outside the checkout") + args = parser.parse_args() + receipt, candidate = run() + result_path = HERE / "RESULT.json" + if args.write: + with result_path.open("x") as stream: + json.dump(receipt, stream, indent=2, sort_keys=True) + stream.write("\n") + else: + need(canonical(receipt) == canonical(json.loads(result_path.read_bytes())), "Committed result receipt") + if args.emit_word: + path = args.emit_word.resolve() + need(not path.is_relative_to(ROOT), "Emit only outside the source checkout") + with path.open("xb") as stream: + stream.write(canonical(candidate) + b"\n") + print(json.dumps(receipt, sort_keys=True)) + print(receipt["status"]) + + +if __name__ == "__main__": + main()