From 77ee317339e4bf355d32207719a6d951c945d51c Mon Sep 17 00:00:00 2001 From: Chris R Date: Mon, 26 Oct 2026 16:20:35 +1100 Subject: [PATCH] Prove a typed inverse-commutator exclusion for the PR5660 rewrite delta --- .../NOTICE | 26 +++ .../PROOF.md | 83 +++++++++ .../README.md | 39 ++++ .../SOURCES.json | 138 ++++++++++++++ .../inputs/pr5660-PROOF.md | 176 ++++++++++++++++++ .../inputs/pr5660-SOURCES.json | 121 ++++++++++++ .../inputs/pr5660-WITNESS.json | 16 ++ .../inputs/pr5660-construct.py | 130 +++++++++++++ 8 files changed, 729 insertions(+) create mode 100644 research/p104-rewrite-delta-commutator-exclusion/NOTICE create mode 100644 research/p104-rewrite-delta-commutator-exclusion/PROOF.md create mode 100644 research/p104-rewrite-delta-commutator-exclusion/README.md create mode 100644 research/p104-rewrite-delta-commutator-exclusion/SOURCES.json create mode 100644 research/p104-rewrite-delta-commutator-exclusion/inputs/pr5660-PROOF.md create mode 100644 research/p104-rewrite-delta-commutator-exclusion/inputs/pr5660-SOURCES.json create mode 100644 research/p104-rewrite-delta-commutator-exclusion/inputs/pr5660-WITNESS.json create mode 100644 research/p104-rewrite-delta-commutator-exclusion/inputs/pr5660-construct.py diff --git a/research/p104-rewrite-delta-commutator-exclusion/NOTICE b/research/p104-rewrite-delta-commutator-exclusion/NOTICE new file mode 100644 index 0000000000..ecd68a79a1 --- /dev/null +++ b/research/p104-rewrite-delta-commutator-exclusion/NOTICE @@ -0,0 +1,26 @@ +PR5660 typed rewrite-delta inverse-commutator exclusion + +New contribution prepared with substantial OpenAI Codex assistance for the donor. +The local independent paper review also used OpenAI Codex. This notice makes no +claim of independent human scientific acceptance or novelty of the classical +commutator/transvection identity. + +The unmodified files inputs/pr5660-construct.py, inputs/pr5660-WITNESS.json, +inputs/pr5660-PROOF.md and inputs/pr5660-SOURCES.json are retained from Ali +Romman's PR5660 publication at commit 3b0b4f37d5005f381ed9cfcccebfbe1ab35c71aa, +research/p104-contact-rewrite/. The constructor's original notice is preserved: + +The A2 identity is from PR3998/4019 and zxv's PR5643 paid construction. +PR5644 supplies the three helper relations. Ali Romman prepared the new +four-gate construction with substantial OpenAI Codex assistance. Apache-2.0. + +The retained PR5660 manifest preserves further source pins and predecessor +attribution for PR5627, PR5643, PR5644, PR5650 and PR5651. Their P104, native, +helper, caller, controller and compiler lineage is not claimed as new here. +Related scalar reassociation and bounded local screen work in Discussion5600 +is credited in README.md. Later successor work receives no transferred claim. + +This package and the copied source files are under Apache-2.0, consistently +with the repository contribution policy and retained source notice. The +repository-root LICENSE supplies the license text in the intended overlay. +Retain this notice and the original source notices when redistributing. diff --git a/research/p104-rewrite-delta-commutator-exclusion/PROOF.md b/research/p104-rewrite-delta-commutator-exclusion/PROOF.md new file mode 100644 index 0000000000..25f14c6aff --- /dev/null +++ b/research/p104-rewrite-delta-commutator-exclusion/PROOF.md @@ -0,0 +1,83 @@ +# A typed exclusion for the fixed PR5660 delta + +## The programs and edit + +Let P and Q be typed public programs with the same frame inventory. A public role's required scalar contacts follow a nondecreasing chain of subspaces; a public MOVE either changes nothing or strictly increases the subspace. Every ADD uses a common chart for both operands. These are premises on both programs. Source code declaring or checking a condition is not by itself an independent replay of an actual word. + +Work in the scalar-plus-owned skeleton: omit public MOVEs, retain owned MOVEs and every scalar, lifetime and protected observation event. Public transport remains governed by the typed path premise. An observer below means a skeleton event or protected observation touching a specified role; the public MOVEs required to reach the next chart are not forbidden observers. + +Write `C=165`, `H=586`, `S=733`, `X=21`. The indices are zero-based indices in the old skeleton, not full-word event indices. The exact edit deletes: + +| Label | Old index | ADD | Frame | Dimension | +| --- | --- | --- | --- | --- | +| O1 | 12513 | `H += -4 S` | 597 | 1 | +| O2 | 12753 | `C += 2 S` | 597 | 1 | +| O3 | 12754 | `C += -1/2 X` | 652 | 2 | +| O4 | 12755 | `X += H` | 652 | 2 | + +At the old O4 position it inserts this consecutive skeleton block: + +| Label | ADD | Frame | Dimension | +| --- | --- | --- | --- | +| E1 | `C += 1/2 H` | 3 | 0 | +| E2 | `H += -4 S` | 597 | 1 | +| E3 | `X += H` | 652 | 2 | +| E4 | `C += -1/2 X` | 652 | 2 | + +The bases are exactly `[]`, `[82]`, `[82,268]` for frames 3, 597, 652. Every other skeleton event is preserved unchanged and in order. Every surviving event strictly between old indices 12513 and 12755 is disjoint from `{C,H,S}`. There is no assumed isolation for X. The exact indices imply that O2,O3,O4 are consecutive, stronger than merely asserting adjacency of the last pair. + +These premises are bound to [the copied witness](inputs/pr5660-WITNESS.json) and [constructor](inputs/pr5660-construct.py): skeleton at lines 20–21; frame-preserving rebuild and public monotonicity at 24–58; exact anchors/roles/replacement at 92–110; isolation and final-pair adjacency at 111–115; ordered deletion/insertion at 117–123. The frame inventory is preserved by `deepcopy` and replacement of only `program` in `rebuild` (the later schema tag is irrelevant). The published code's replay and cost checks are not premises proven here. + +Let φ be the order-preserving survivor map from old events outside `{O1,O2,O3,O4}` to their unchanged new occurrences. E1–E4 are new occurrences. In particular O1 and E2 are different provenance labels even though their instruction bytes agree. Equal-looking instructions elsewhere do not define φ. + +## The motif and the meaning of new incidence + +Let a,b,d be distinct public roles, and let α,β be nonzero exact coefficients. The motif has four ordered scalar anchors: + +$$ +\begin{aligned} +M_1 &: a \mathrel{+}= \alpha b && (\dim=1),\\ +M_2 &: b \mathrel{+}= \beta d && (\dim=3),\\ +M_3 &: a \mathrel{-}= \alpha b && (\dim=5),\\ +M_4 &: b \mathrel{-}= \beta d && (\dim=7). +\end{aligned} +$$ + +The middle role b follows the complete absolute dimension-zero to dimension-nine route with five positive MOVE ranks `(1,2,2,2,2)`. The four anchors are its only interior required contacts. Extra scalar contacts to b before the corridor at its unchanged dimension-zero endpoint, and after it at its unchanged dimension-nine endpoint, are allowed. Every other skeleton event or protected observation strictly between M1 and M4 is disjoint from `{a,b,d}`. The absolute starting dimension zero is essential: the rank partition alone would not fix anchor dimensions 1,3,5,7. + +The familiar scalar identity replaces these four gates by `a -= αβ d`, restoring b. We assert no novelty for that identity, and prove no positive native or economic realization of it. Other retained operand, endpoint, target and native conditions can only restrict this necessary typed motif class further. + +A **new incidence under this edit** is a motif in Q satisfying either: + +1. One of its four anchors is an inserted E event; or +2. All four anchors are survivors under φ, with the same old role/edge/coefficient pattern, and their old corridor failed the strict observer condition solely because at least one removed O event touched `{a,b,d}`. + +An old valid motif, changed economics of an existing motif, newly excused surviving observers and changed route predicates are outside this definition. + +**Proposition.** For every typed P and valid Q satisfying the fixed edit, frame, isolation and adjacency premises above, there is no new incidence in this motif class. + +## Case 1: an inserted anchor + +The inserted dimensions are 0,1,2,2. The motif anchor dimensions are 1,3,5,7. Thus only E2 could be a motif anchor, and it must be M1. This fixes `a=H`, `b=S`, `α=-4`. + +The immediately next skeleton event E3 reads H=a and writes X. It cannot be M2 or M4, whose destination must be S. It cannot be M3, whose destination/source must be H/S at dimension five. No remaining anchors fit before the immediately following event. E3 is consequently a forbidden observer inside the unfinished motif corridor. This contradiction excludes every inserted-anchor incidence. Additional endpoint contacts and intervening public transport do not remove the E3 read. + +## Case 2: a removed old barrier + +All anchors now survive. Let R=`{a,b,d}`. Some deleted O touches R by the case definition. The union of roles touched by the deleted events equals the union touched by the inserted block, namely `{C,H,S,X}`. Hence at least one E event touches R. + +The E block is consecutive in the skeleton and contains no motif anchor in this case. It cannot lie inside the new corridor, since its R-touching event would be a forbidden observer. Therefore all motif anchors lie before the block or all lie after it. If they all lay after it, their old preimages would follow O4; every deleted event would precede the old corridor and none could be its barrier. All four anchors must therefore precede the block. + +The last possible surviving old index before O4 is 12752, because 12753,12754,12755 are consecutive deleted positions. O2,O3,O4 therefore cannot lie inside this old corridor. Only O1 can be the lost barrier. This closes X-only possibilities without assuming X isolation: both deleted events involving X are in the terminal cluster, outside the corridor. + +For the old corridor to contain O1, M4's old preimage lies strictly between O1 and O2, hence within the isolation interval. M4 touches b,d and survives, so both b,d lie outside `{C,H,S}`. O1 touches R but only has roles H,S. Thus `a=H` or `a=S`. + +M3 touches that a in `{C,H,S}`. Isolation prevents M3 from lying strictly between O1 and O4. It precedes M4 in that interval and is a survivor, so M3 must precede O1. But M3 requires a at dimension five and later O1 requires the same a at dimension one. The typed old public chronology forbids that decrease. This contradiction excludes the removed-barrier case. + +The two cases exhaust the stated definition of new incidence. The proposition follows. + +## What follows from the proposition + +No occurrence lookup can discover a newly created motif in this closed delta class if the premises hold. This is the useful source-specific stop decision. It neither counts nor excludes motifs already present in P, and it says nothing about other rank partitions, translated starting charts, observer contracts, changed economics, changed scalar graphs or successor releases. + +The proof needs no inversion of the final WORD. Although the declared edit has a deterministic skeleton preimage once a final E block is bound, invertibility does not identify that preimage with the historical PR5650 payload. No equality with that payload is claimed. Actual word custody, typing/native validity and whole-word coverage remain separate obligations. diff --git a/research/p104-rewrite-delta-commutator-exclusion/README.md b/research/p104-rewrite-delta-commutator-exclusion/README.md new file mode 100644 index 0000000000..b2630d2c18 --- /dev/null +++ b/research/p104-rewrite-delta-commutator-exclusion/README.md @@ -0,0 +1,39 @@ +# The PR5660 rewrite cannot create this typed inverse commutator + +For any typed old program P and valid rewritten program Q satisfying the exact PR5660 edit premises, the edit cannot create an inverse-commutator motif whose middle role has the absolute dimension-zero to dimension-nine route with MOVE increments `(1,2,2,2,2)` and four interior anchor dimensions `1,3,5,7`. The proof covers a motif using an inserted anchor and a survivor-anchor motif made admissible solely by deleting an old observer barrier. It permits extra middle-role contacts at the unchanged endpoints. The [proof](PROOF.md) gives the quantified statement and all premises. + +This is a conditional source-delta exclusion. It makes the proposed occurrence lookup for this exact historical delta unnecessary. It supplies no whole-word census, equality with the old PR5650 payload, absence of all commutators, paid-profile improvement, κ gain, full native replay or proof-kernel verification. The elementary commutator identity is classical. The contribution is the source-bound exclusion for the specified edit and typed route. + +## Sources and evidence + +The historical object is [PR5660](https://github.com/CrocSwap/integer-mult-bounds/pull/5660) at immutable head `3b0b4f37d5005f381ed9cfcccebfbe1ab35c71aa`. The four small text files in [inputs/](inputs/) are unmodified copies of that publication's constructor, witness, author proof and source manifest. [SOURCES.json](SOURCES.json) records their immutable paths, content hashes and Git blobs. The copied Python file is read as source text; this package does not import or run it. The copied author proof and manifest preserve provenance context; their construction/replay claims are author evidence rather than checks performed by this package. + +| Layer | Evidence | Status and limit | +| --- | --- | --- | +| Text custody | Copied bytes match the SHA256, Git-blob and length records in the supplied authenticated PR5660 packet. | Recomputed as packaging bookkeeping; no new network authentication. | +| Declared source contract | Constructor lines 20–21, 24–58 and 92–123, plus the complete witness. | Read as text. These declare the skeleton, monotone public paths, fixed edit, frame bases and isolation predicate. | +| Mathematical statement | The two exhaustive incidence cases in [PROOF.md](PROOF.md). | A universal conditional paper argument. A supplied independent local review accepted this argument; review of the final publication bytes is still required. | +| Actual published programs | The PR5660 package describes source composition and author replay. | Neither old nor new WORD was decoded here. The typed-P/Q premise and actual-word instantiation have not been independently replayed by this package. | +| Whole-word coverage | Existing public discussion describes related scalar reassociation and broader local screens. | The complete matcher domain and its binding to final PR5660 remain unknown. This result does not close that question. | + +This is an unregistered static proof package. Its custody manifest uses the explicitly named package-specific schema in `SOURCES.json`; it is not a declaration that the optional generic research-package runner has accepted metadata or run a verifier. No `VERIFY.json`, task-card claim or CI-ready hook is supplied. + +No occurrence search, scientific numeric calculation, source import, constructor, native interpreter, endpoint replay, old-word comparison or math test was executed to prepare this package. No runnable checker, test receipt or `RESULT.json` is supplied. The paper proof does not need a scientific execution receipt. Any future automated qualification should report custody and source-contract checks separately from the theorem and actual-word validity. + +## Attribution and nearby work + +Ali Romman's [PR5660](https://github.com/CrocSwap/integer-mult-bounds/pull/5660) supplies the exact four-gate edit. Its constructor credits the A2 identity in [PR3998](https://github.com/CrocSwap/integer-mult-bounds/pull/3998) and [PR4019](https://github.com/CrocSwap/integer-mult-bounds/pull/4019), zxv's paid construction [PR5643](https://github.com/CrocSwap/integer-mult-bounds/pull/5643), and the three helper relations in [PR5644](https://github.com/CrocSwap/integer-mult-bounds/pull/5644). The retained source manifest additionally pins [PR5627](https://github.com/CrocSwap/integer-mult-bounds/pull/5627), [PR5650](https://github.com/CrocSwap/integer-mult-bounds/pull/5650) and [PR5651](https://github.com/CrocSwap/integer-mult-bounds/pull/5651). Their P104, native-chart, helper, caller, controller and compiler lineage remains credited through those retained sources. + +Ali Romman's [Discussion5600 scope statement](https://github.com/CrocSwap/integer-mult-bounds/discussions/5600#discussioncomment-19184345) already describes corrected noncommuting transvection reassociation and disclaims novelty of the elementary identity. Later [boundary-resynthesis work](https://github.com/CrocSwap/integer-mult-bounds/discussions/5600#discussioncomment-19187633) and the [release of bounded scalar screens](https://github.com/CrocSwap/integer-mult-bounds/discussions/5600#discussioncomment-19188254) are relevant prior discovery work. This package neither repeats those claimed screens nor establishes what they exhausted. Its result is the two-case typed exclusion under the fixed published edit. + +The later [PR5678](https://github.com/CrocSwap/integer-mult-bounds/pull/5678) construction at `af814f6f3c477fdd13b8f04380a33cf32004966b`, identified by the parent coordinator, is outside this theorem's edit premises. This exclusion does not transfer to that successor. No successor source or artifact is an input here. + +Prepared for the donor's contribution with substantial OpenAI Codex assistance, including the local independent paper review. Source notices and the Apache-2.0 terms are retained; see [NOTICE](NOTICE). There is no human-independent scientific acceptance claim. + +## Open next questions + +1. **Can the exact historical words instantiate the typed premise?** This would connect the universal conditional statement to a fully replayed source object. The first step is authenticated old/new word custody and the published complete typing/replay procedure, under a separately scoped request. This package supplies no word payloads and does not require that stronger claim. +2. **What did the prior scalar screens cover?** A source-pinned matcher or tested-domain receipt should specify coefficient/role conditions, protected corridors, chart choices, paid-path eligibility and exact tested head. This can resolve duplication without another blind word scan. The public statements alone leave it open. +3. **Does a successor satisfy a related exclusion?** Start by identifying its actual edit and contact premises, then seek a new proof or bounded question. The PR5660 theorem provides no inherited result for a changed word or schedule. + +The smallest useful follow-up for this submission is review of the final proof and source-premise bindings. No further occurrence lookup is justified for the exact delta class proved empty here. diff --git a/research/p104-rewrite-delta-commutator-exclusion/SOURCES.json b/research/p104-rewrite-delta-commutator-exclusion/SOURCES.json new file mode 100644 index 0000000000..920f4cf7cf --- /dev/null +++ b/research/p104-rewrite-delta-commutator-exclusion/SOURCES.json @@ -0,0 +1,138 @@ +{ + "schema": "p104-rewrite-delta-commutator-exclusion-sources/1", + "status": "publication-draft", + "upstream_repository": "https://github.com/CrocSwap/integer-mult-bounds", + "historical_object": { + "pull_request": "https://github.com/CrocSwap/integer-mult-bounds/pull/5660", + "commit": "3b0b4f37d5005f381ed9cfcccebfbe1ab35c71aa" + }, + "source_custody": { + "basis": "Existing authenticated source packet supplied by parent; this package does not perform a fresh network capture", + "packaging_check": "Recomputed SHA256, Git blob hash and byte length of copied text inputs against supplied pins", + "scientific_status": "Text custody only; no source import, word decode, constructor or replay" + }, + "files": [ + { + "local_path": "inputs/pr5660-construct.py", + "repository_path": "research/p104-contact-rewrite/construct.py", + "commit": "3b0b4f37d5005f381ed9cfcccebfbe1ab35c71aa", + "url": "https://github.com/CrocSwap/integer-mult-bounds/blob/3b0b4f37d5005f381ed9cfcccebfbe1ab35c71aa/research/p104-contact-rewrite/construct.py", + "git_blob": "1207c370448732436e5dd697c6309a71a27a9075", + "sha256": "485eefe102fa94de58512d4a05f437a4213ff8b7e1fd8bed45824af374f9d4c3", + "bytes": 5311, + "use": "Textual edit and typed-path premise binding; never imported", + "license": "Apache-2.0" + }, + { + "local_path": "inputs/pr5660-WITNESS.json", + "repository_path": "research/p104-contact-rewrite/WITNESS.json", + "commit": "3b0b4f37d5005f381ed9cfcccebfbe1ab35c71aa", + "url": "https://github.com/CrocSwap/integer-mult-bounds/blob/3b0b4f37d5005f381ed9cfcccebfbe1ab35c71aa/research/p104-contact-rewrite/WITNESS.json", + "git_blob": "4671283b4fa00fe444cd61353863d14b0e7ac774", + "sha256": "12085b340d4d3ef76a70e4c92b6188c4e6eb6962815cc3e5d1da009ca52abb48", + "bytes": 384, + "use": "Exact old/replacement records and old skeleton indices", + "license": "Apache-2.0" + }, + { + "local_path": "inputs/pr5660-PROOF.md", + "repository_path": "research/p104-contact-rewrite/PROOF.md", + "commit": "3b0b4f37d5005f381ed9cfcccebfbe1ab35c71aa", + "url": "https://github.com/CrocSwap/integer-mult-bounds/blob/3b0b4f37d5005f381ed9cfcccebfbe1ab35c71aa/research/p104-contact-rewrite/PROOF.md", + "git_blob": "5eab6148f782d11cc5d8d0ec923997fb81bf94f8", + "sha256": "18088012842ae0ef1d120dd7681aa8ec064f8ed7ecc457f909ff2dc49f010745", + "bytes": 7801, + "use": "Author source context and predecessor attribution only", + "license": "Apache-2.0" + }, + { + "local_path": "inputs/pr5660-SOURCES.json", + "repository_path": "research/p104-contact-rewrite/SOURCES.json", + "commit": "3b0b4f37d5005f381ed9cfcccebfbe1ab35c71aa", + "url": "https://github.com/CrocSwap/integer-mult-bounds/blob/3b0b4f37d5005f381ed9cfcccebfbe1ab35c71aa/research/p104-contact-rewrite/SOURCES.json", + "git_blob": "2a5c2b8015ece09e4788b7742d1351aa87545299", + "sha256": "6d3fa5d28d1022703dd853b107e700664f88203e3b7858fc92b48e45b3744367", + "bytes": 5807, + "use": "Author predecessor pins and attribution only", + "license": "Apache-2.0" + } + ], + "guidance_read": { + "historical_snapshot_commit": "df0137efd35e11b4445734bf612bdd4c7ebc330c", + "meaning": "Preparation snapshot only; root must refresh applicable guidance before submission", + "files": [ + { + "url": "https://github.com/CrocSwap/integer-mult-bounds/blob/df0137efd35e11b4445734bf612bdd4c7ebc330c/AGENTS.md", + "git_blob": "fa006ceb6b6b9d6c0e799f210963f4587ecfb162", + "sha256": "fbee67ab9e0ae4629a35fd9dba69c8f7e29e4a15392eb2d0f75d8768ffb65f40", + "bytes": 5963 + }, + { + "url": "https://github.com/CrocSwap/integer-mult-bounds/blob/df0137efd35e11b4445734bf612bdd4c7ebc330c/CONTRIBUTING.md", + "git_blob": "5185786f2ec00f215019fb5777d70979429690a9", + "sha256": "fcd1a8d0e52342a23b8ffa9e905e85ccc539fb084145ef016dfc93cedfb3d924", + "bytes": 7505 + }, + { + "url": "https://github.com/CrocSwap/integer-mult-bounds/blob/df0137efd35e11b4445734bf612bdd4c7ebc330c/autoresearch.md", + "git_blob": "2fe84a7b30b1e26e60ce0ec4775894eb1831c5d6", + "sha256": "d16f0d3bb4d4b213d06c128db6d6460b0fe9ec1ac5a6c1ea1febf1db40e7b60d", + "bytes": 5986 + }, + { + "url": "https://github.com/CrocSwap/integer-mult-bounds/blob/df0137efd35e11b4445734bf612bdd4c7ebc330c/.github/pull_request_template.md", + "git_blob": "ae656e706bf992a3c26c710611ff92dde75efe21", + "sha256": "6fffbdcc80d32daa5d6940b21f4c0e61df7e5f588a120374269ff28dac26c562", + "bytes": 1505 + } + ] + }, + "predecessors": { + "PR5627": "ed4dc88a09a7d201971f6603b8c2074e95dd9c32", + "PR5643": "a3ff5c628bfc8825553d62d913f3e91f75d6825f", + "PR5644": "c5871955d89bf73506fd68b0a5bf1cf2b3153c02", + "PR5650": "7916490124ac946704339a6a332bb76f06e5db5c", + "PR5651": "853192167b27d44aea0d4bc2b0d52d695fadc7c6" + }, + "local_paper_review": { + "status": "The argument was accepted as an explicitly conditional source-delta theorem in the supplied independent local review; final publication bytes not yet reviewed", + "artifact_required_for_final_publication_review": true + }, + "excluded_inputs": [ + "Old and new WORD payloads", + "Transient local chart-feasibility receipts", + "Successor construction sources" + ], + "remaining_before_publication": [ + "Delta-exclusion-specific semantic overlap/ownership gate by root; the h586 gate covers a different finding", + "Final publication-format decision and exact submission base by root", + "Independent review of final proof and exact immutable source bindings", + "Final author attribution wording and repository license text supplied by upstream overlay; include license separately if distributing standalone" + ], + "registration": { + "status": "unregistered-static-proof-package", + "generic_runner_compatible": false, + "reason": "No legitimate task-card/ready-verifier registration is asserted; custom custody schema is explicit" + }, + "publication_guidance_read": { + "canonical_main": "df0137efd35e11b4445734bf612bdd4c7ebc330c", + "basis": "Fresh authenticated packet supplied by parent; no independent fetch by this publication agent", + "files": [ + { + "url": "https://github.com/CrocSwap/integer-mult-bounds/blob/df0137efd35e11b4445734bf612bdd4c7ebc330c/docs/research/research-package-guide.md", + "git_blob": "b2856d694070644e25df5bf5680aeb80d1458c25", + "sha256": "d731952a85d1f9d95341ffc3ee0095a97dfbe6226c9dfc70bfee4a3b0727791d" + }, + { + "url": "https://github.com/CrocSwap/integer-mult-bounds/blob/df0137efd35e11b4445734bf612bdd4c7ebc330c/scripts/new_research_package.py", + "git_blob": "eb1bdf8ff46b9ad2de1f85aa058a028735800395", + "sha256": "7d300bf45baffced49d2bbea795ce3abe5f860f0dc1172845fc352b398331f34" + }, + { + "url": "https://github.com/CrocSwap/integer-mult-bounds/blob/df0137efd35e11b4445734bf612bdd4c7ebc330c/scripts/research_package.py", + "git_blob": "48fe9feb4699c09e95505d95c327ea998ac8b3a7", + "sha256": "84a45190a6a96c20993a0d4a1045fbf24de660d2e6fef8f8a447bb3d1aa78db6" + } + ] + } +} diff --git a/research/p104-rewrite-delta-commutator-exclusion/inputs/pr5660-PROOF.md b/research/p104-rewrite-delta-commutator-exclusion/inputs/pr5660-PROOF.md new file mode 100644 index 0000000000..5eab6148f7 --- /dev/null +++ b/research/p104-rewrite-delta-commutator-exclusion/inputs/pr5660-PROOF.md @@ -0,0 +1,176 @@ +# A complete conditional contact rewrite + +The claimed value is **kappa = 0.00310676333**. The comparison is the open +PR5651 value 0.00310644469. The increase is 0.00000031864. This construction +keeps the five selected framework assumptions and the helper endpoint +contract. It does not change the selected record. + +## 1. Exact sources and composition + +The retained export is PR5627 at +`ed4dc88a09a7d201971f6603b8c2074e95dd9c32`. It contains 36 source files and +one export manifest. Authenticate the archive, its complete inventory and +each file before import. Also authenticate the retained PR5644 constructor, +witness, word and the PR5643 word. + +First apply the three fixed PR5644 helper relations. Compare the result with +the complete published word. Each relation changes the local paid profile +by `-H1-H5+H6`. All public inputs, targets and owned instructions stay fixed. + +Then apply zxv's PR5643 A2 change. Check its entire scalar-program difference +against the published PR5643 word. Locate the same two gates in the PR5644 +word. Replace them by the three published gates and rebuild the nested public +paths. The complete local paid change is `H2+H6-H3-H5`. Full replay checks the +composition; numerical headline gains are not added. PR5650 already publishes +this composition, and PR5651 checks it again. Compare with the retained +PR5650 word after rebuilding the same public MOVE order. Each changed order +only swaps consecutive MOVEs on different public fields. The scalar and +owned chronology stays fixed. No new composition result is claimed here. + +## 2. The new four-gate identity + +Let `c=165`, `h=586`, `s=733` and `x=21`. The old gates are + +```text +h <- h - 4s at frame 597 +c <- c + 2s at frame 597 +c <- c - x/2 at frame 652 +x <- x + h at frame 652 +``` + +The first two sites are separated by other operations. The witness checks +that none of the intervening operations reads or writes c, h or s. The two +late gates are consecutive in the scalar skeleton. Operations on x before +the late pair retain their order. + +Use these gates instead: + +```text +c <- c + h/2 at frame 3 +h <- h - 4s at frame 597 +x <- x + h at frame 652 +c <- c - x/2 at frame 652 +``` + +Here frame 3 is `{0}`, frame 597 has basis `[82]`, and frame 652 has basis +`[82,268]`. The new early read uses the old value of h. The new gates are +placed at the old late pair after the two early updates are removed. + +Write the values before these updates as c, h, s and x. Both programs give + +```text +c_out = c + 2s - x/2 +h_out = h - 4s +s_out = s +x_out = x + h - 4s +``` + +The verifier also compares both full 4 by 4 rational matrices. More generally, +this identity holds for coefficients alpha, beta, gamma and delta when +`beta = alpha*gamma*delta`; the early coefficient is `-gamma*delta`. +The A2 identity and compensated triangle method are prior work. The new +result is this source-bound four-gate schedule and its paid native path. + +The new schedule lets c remain in dimension zero until its dimension-two +contact. Its old two rank-one requests become one rank-two request. Every +other paid count has the same value. Thus + +```text +new local paid delta = -2 H1 + H2 +new local target delta = 0 +``` + +For every `00`. The complete caller uses the local word 18 times, +so this new component improves the signed moment by `18*(2-2^t)`. + +For this fixed dimension-zero to dimension-two path of c, the new transport +also has the minimum cost among strictly nested subdivisions. Such a path +has either one rank-two step or two rank-one steps. For `0= word['public']] + + +def rebuild(word, program, L): + """Keep the owned paths and rebuild each nested public path.""" + out = deepcopy(word) + n = word['public'] + current = word['initial'] + [None]*word['owned_fields'] + spaces = [L.span(b) for b in word['frames']] + events = [] + + def move(role, frame): + old = current[role] + if old == frame: + return + L.need(role < n and spaces[old] < spaces[frame], 'Strict nested public path') + events.append(['MOVE', role, old, frame, False]) + current[role] = frame + + for event in program: + op, role = event[:2] + if op == 'MOVE': + L.need(role >= n and current[role] == event[2], 'Unchanged owned transport') + current[role] = event[3] + elif op == 'INIT': + L.need(current[role] is None, 'Fresh owned lifetime') + current[role] = event[2] + elif op == 'CLEAR': + L.need(current[role] == event[2], 'Owned erasure frame') + current[role] = None + else: + for operand in sorted(roles(event)): + move(operand, event[-1]) + events.append(event[:]) + for role, frame in enumerate(word['final']): + move(role, frame) + out['program'] = events + return out + + +def replace_a2(program, L): + old = [['ADD', 388, 715, '-4', 825], ['ADD', 340, 388, '1', 825]] + sites = [i for i in range(len(program)-1) if program[i:i+2] == old] + L.need(len(sites) == 1, 'Unique published A2 pair') + i = sites[0] + return program[:i] + [['ADD', 340, 715, '-4', 396], old[1], + ['ADD', 388, 715, '-4', 127]] + program[i+2:] + + +def check_a2_source(source, published, L): + for key in source: + if key not in ('program', 'schema'): + L.need(source[key] == published[key], 'Published A2 boundary: '+key) + L.need(replace_a2(scalar_word(source), L) == scalar_word(published), + 'Exact released PR5643 scalar change') + before, after = L.replay(source), L.replay(published) + delta = Counter(after['paid']) + delta.subtract(before['paid']) + L.need({r:v for r,v in delta.items() if v} == {2:1,3:-1,5:-1,6:1}, + 'Exact released PR5643 paid change') + + +def matrix(gates, labels): + at = {r:i for i,r in enumerate(labels)} + rows = [[Q(i == j) for j in range(len(labels))] for i in range(len(labels))] + for event in gates: + a, b, q = at[event[1]], at[event[2]], Q(event[3]) + rows[a] = [x+q*y for x,y in zip(rows[a], rows[b])] + return rows + + +def rewrite(word, witness, L): + """Use the old helper value before its source update.""" + p = skeleton(word) + indices = witness['indices'] + old, new = witness['old'], witness['replacement'] + L.need(indices == sorted(set(indices)) and len(indices) == 4, 'Four ordered source sites') + L.need([p[i] for i in indices] == old, 'Exact four-gate source anchors') + c, h, s, x = witness['roles'] + L.need(len({c,h,s,x}) == 4 and max(c,h,s,x) < word['public'], 'Four public roles') + L.need([e[1:3] for e in old] == [[h,s],[c,s],[c,x],[x,h]], 'Declared source pattern') + alpha, beta, gamma, delta = (Q(e[3]) for e in old) + L.need(beta == alpha*gamma*delta, 'Exact compensation coefficient') + expected = [['ADD', c, h, str(-gamma*delta), 3], + ['ADD', h, s, str(alpha), 597], + ['ADD', x, h, str(delta), 652], + ['ADD', c, x, str(gamma), 652]] + L.need(new == expected, 'Declared complete replacement') + L.need([word['frames'][f] for f in (3,597,652)] == [[],[82],[82,268]], + 'Exact zero, one and two dimensional charts') + omitted = set(indices) + L.need(not any(roles(e) & {c,h,s} for i,e in enumerate(p) + if indices[0] < i < indices[-1] and i not in omitted), + 'No intervening read or write of the three moved roles') + L.need(indices[-1] == indices[-2]+1, 'The two late gates are consecutive') + L.need(matrix(old, [c,h,s,x]) == matrix(new, [c,h,s,x]), 'Independent four-column identity') + changed = [] + for i,event in enumerate(p): + if i == indices[-1]: + changed.extend(new) + elif i not in omitted: + changed.append(event) + result = rebuild(word, changed, L) + result['schema'] = 'p104-contact-rewrite/1' + before, after = L.replay(word), L.replay(result) + delta_paid = Counter(after['paid']) + delta_paid.subtract(before['paid']) + L.need({r:v for r,v in delta_paid.items() if v} == {1:-2,2:1}, 'Two H1 calls become one H2') + L.need(before['helpers'] == after['helpers'], 'Every independent target is retained') + return result, after