Prove longer fixed-route G20 conjugations cannot lower the paid moment (no κ)

research/g20-long-conjugation-obstruction/PROOF.md

@@ -0,0 +1,162 @@
+# Longer fixed-route G20 conjugations have no paid-moment gain
+
+## Claim and boundary
+
+Fix Ali Romman's final PR5708 `WORD.json.gz` and `PATHS.json`, pinned in
+[SOURCES.json](SOURCES.json) at main
+`2485805a6d47f36ea83ddde6327d453ac82d44dc`. Consider a single A2 conjugation
+with at least four noncommuting contacts, with each correction kept at its
+contact's original frame. Every such conjugation either encounters a missing
+published route or has nonnegative paid-query moment change for every
+`0 < t < 1`. The statement covers all contact lengths present on this word,
+including its maximum of 33, rather than a chosen upper cutoff.
+Among emitting candidates the minimum moment change is exactly zero for
+every `0<t<1`. For example, zero-based scalar positions 9,399 and 10,815
+bound a four-contact rewrite of `ADD(560,315)` with an unchanged histogram.
+
+This is a finite certificate with a scoped algebraic sign proof. It extends
+unpaidmoon's PR6290 question and fixed-contact-frame definition. PR6290's
+one-to-three-contact result is cited, not re-established here. No assertion
+about a changed route table, a sequence of rewrites or another word follows.
+
+## Exact candidate class
+
+Remove `Q` and `ZERO_Q` records from the pinned word to obtain 11,930 scalar
+records on 685 roles. Write `G(a,b)` for `ADD(a,b)`, the characteristic-two
+map `x_a <- x_a + x_b`. Choose any two occurrences of the same ordered
+pair `(a,b)`, with positions `left < right`. Their frames may differ.
+
+The open interval must contain no `INIT` or `ERASE` of `a` or `b`. A contact
+is an ADD with destination `b` or source `a`. Every contact must have one
+of the following forms, with the indicated correction:
+
+| Contact | Constraint | Correction |
+|---|---|---|
+| `ADD(b,s)` | `s != a` | `ADD(a,s)` |
+| `ADD(d,a)` | `d != b` | `ADD(d,b)` |
+
+In particular, the reversed gate `ADD(b,a)` is outside this class. Require
+at least four contacts. Delete the two outer gates and insert the correction
+immediately after each contact, at that contact's original frame. All other
+records retain their order and frame. These are the only changes allowed.
+
+Completeness is finite and explicit. Group every ADD position by its ordered
+operand pair, visit every ordered choice of two increasing positions in each
+group, inspect every intervening record, and retain exactly the intervals
+satisfying the conditions above. There is no contact cutoff or node budget.
+The resulting domain has exactly 1,503 intervals. The certificate lists every
+interval's endpoints, operands, contact count and outcome.
+
+## Scalar endpoint
+
+For each valid contact `C`, direct multiplication of elementary matrices gives
+`G C G = C R`, where `R` is the indicated correction. The correction commutes
+with its contact. Every noncontact commutes with `G`, including an erase or
+initialization of a different role. Since `G^2 = I`, conjugation distributes
+over the entire interval. Thus deleting the two outer gates and replacing
+every contact by `C R` preserves the scalar map for any contact count.
+
+The verifier also checks the complete endpoint separately for every one of
+the 1,503 changed words, including those that later fail route emission.
+Each row is a 685-bit coefficient mask, initially `e_i`. ADD is exact XOR;
+only owned roles may be erased, and INIT requires their whole row to be zero.
+The expected final row is zero on owned roles. On other roles it is `e_i`,
+with the additional term `e_(i-111)` for `111 <= i < 222`.
+This tests every independent scalar input column, not a sample of payloads.
+The native address action remains a cited predecessor premise.
+
+## Route contract and certificate
+
+Use precisely the source emitter's rules. An ADD with zero source row is
+omitted. Otherwise move its destination and source to its frame, in that
+order. A published one-edge route incurs its rank once when the moved row
+is nonzero, and zero when that row is zero. A missing edge rejects emission
+even for a zero row. An uninitialized owned zero row may be initialized.
+At the end return every public role to its final frame and require every
+owned role to be zero. Owned cleanup has the source's zero-query convention.
+
+The unchanged word provides the necessary reference histogram
+`{1:1281, 2:1338, 3:58, 4:57, 5:102, 6:10}`. This reference is not a new
+predecessor audit or a claim of full supplier admission. Every changed word
+that emits receives a freshly reconstructed complete paid-query histogram.
+The signed difference is new minus reference.
+
+Exactly 1,450 intervals encounter a missing route. For each, the certificate
+records the first required ordered frame pair absent from the table. These
+are rejection witnesses relative to this table, not proofs that the native
+geometry could never supply another route. The other 53 intervals emit.
+Their entire signed histogram classification is:
+
+| New minus reference | Count | Sign for `0 < t < 1` |
+|---|---:|---|
+| `2H1 - H2` | 15 | Strict loss |
+| `3H1 + 2H2` | 10 | Strict loss |
+| `2H2 - H4` | 5 | Strict loss |
+| `2H1 + H2 + H3` | 4 | Strict loss |
+| `H1 + 3H2` | 2 | Strict loss |
+| `H1 + 2H2 - H5` | 2 | Strict loss |
+| `H1 + H3 - H4` | 1 | Strict loss |
+| Zero | 14 | Neutral |
+
+Here `Hr` contributes `r^t`. All coefficients in three of the nonzero
+shapes are positive, so their moment changes are positive. In each of the
+other four shapes, one negative job of rank `R` is replaced by at least
+two positive jobs whose ranks sum to `R`. For positive `a,b` and `0<t<1`,
+`(a+b)^t < a^t+b^t`. For example, divide by `(a+b)^t` and use
+`u^t > u` for `0<u<1` on `u=a/(a+b)` and `1-u`.
+Iteration proves strict positivity for any such split. This covers the
+whole open exponent interval without floating-point sampling or root search.
+
+The complete canonical candidate certificate has SHA256
+`577323306b7b7f2547ca660e6bbef1badc953959e2f7cd20de9e1f002e254889`.
+Canonical bytes are UTF-8 from `json.dumps(result, sort_keys=True,
+separators=(",", ":"))`. The optional generated receipt includes that whole
+certificate and hashes of all package files and live inputs.
+
+## Controls and limits
+
+The verifier checks all 256 four-contact words over the two allowed contact
+orientations on four roles. It checks their complete input-column endpoints
+and rejects deletion of the first correction in each. Reversed contacts,
+erased operands and short intervals are explicit exclusion controls.
+The exact sign rule rejects the profitable shape `H1 - 2H2 + H3`, whose
+negative sign follows from strict concavity. Routing controls distinguish
+successful charging, a missing edge and a zero source.
+The proof checks use explicit exceptions and remain active under `-O`.
+
+This result concerns one rewrite of the final word and the paid-query part
+of its bill. It provides no new productive target, ordinary BIT saving or
+whole multiplication exponent. No global caller, adjoint/native address
+replay, finite compiler, scalar allowance, physical storage, precision,
+outer ledger, uniform program or rounded multiplier is certified here.
+The five selected framework assumptions remain. Additional routes, correction
+coframes and sequences through neutral words are not excluded.
+
+## Implementation constraints
+
+The verifier uses structured iteration without recursion. Its inputs are
+hash-pinned before decompression and parsing. Each compressed input is below
+two million bytes, the scalar dimensions are checked as 11,930 by 685, the
+candidate list has a fail-closed capacity of 4,096, and XOR rows have at most
+685 bits. Every pair search has the finite upper bound `C(11930,2)`; every
+interval and replay has the corresponding fixed record bound. One changed
+word is live at a time, with no more than `11930-2+33` records on this source.
+No input limit truncates the claimed domain.
+
+Power-of-ten rule 3 deviation: CPython and its standard JSON and gzip readers
+allocate dynamically. This standalone finite checker cannot preallocate those
+runtime internals. The exact authenticated inputs, checked dimensions and
+candidate capacity bound its live data; the normal and optimized complete
+checks exercise those bounds. A future unpinned input interface would require
+bounded streaming parsers before relaxing this contract. All functions fit
+within 60 physical lines. Warning-strict normal and optimized execution are
+the available diagnostics; no static-analysis dependency is introduced.
+
+## Credit
+
+The new longer-contact result and standalone certificate were produced by
+Nick Petalas. Unpaidmoon posed the four-or-more-contact question in PR6290.
+Ali Romman supplied PR5708's word, emitter and scalar A2 construction, following
+Dugongue, ai-nanachi and the native/controller/helper/ordinary/stock lineage
+retained in that package. The A2 identities and strict subadditivity are
+classical and are not claimed as new. No predecessor file or credit is changed.

research/g20-long-conjugation-obstruction/README.md

@@ -0,0 +1,97 @@
+# Longer fixed-route G20 conjugations attain a minimum paid-moment change of zero
+
+Every single A2 conjugation with four or more contacts on the final
+[PR5708 word](https://github.com/CrocSwap/integer-mult-bounds/pull/5708)
+either encounters a missing published route or fails to improve the paid-query
+moment for any exponent `0<t<1`. Corrections stay at their original contact
+frames. Among the emitting candidates the minimum change is exactly zero,
+attained by 14 words. No new kappa or supplier admission is claimed.
+
+This answers the longer-contact, fixed-frame part of open question 2 in
+[unpaidmoon's PR6290](https://github.com/CrocSwap/integer-mult-bounds/pull/6290),
+head `9d2916b07402aca2133ab315230b9c761cc9eff7`. The one-to-three-contact
+result remains that predecessor's contribution. This package enumerates only
+the new four-or-more-contact domain. See the model and sign proof in
+[PROOF.md](PROOF.md).
+
+## Exact result and evidence
+
+| Outcome | New candidates |
+|---|---:|
+| Missing published route | 1,450 |
+| Emitted, strictly larger moment throughout `0<t<1` | 39 |
+| Emitted, identical paid histogram | 14 |
+| Total | 1,503 |
+
+All 1,503 changed words retain the exact scalar endpoint on all 685 independent
+input columns. Their contact counts range from 4 to 33. The enumeration has
+no contact cutoff: it visits every equal-gate interval on the fixed 11,930-record
+scalar word. Each missing-route record gives the first absent ordered frame
+pair, and each emission gives its complete signed paid histogram.
+Every strict-loss shape is positive by positivity or strict subadditivity;
+no floating-point or exponent sampling is used.
+
+The standalone checker tests 256 four-contact identities and 256 missing
+correction mutants, plus seven boundary, sign and routing controls. It uses
+explicit exceptions under both normal and optimized Python. A generated
+receipt can contain the complete candidate certificate and SHA256 bindings
+for all six package files and every live input. Its canonical certificate
+digest is `577323306b7b7f2547ca660e6bbef1badc953959e2f7cd20de9e1f002e254889`.
+
+## Reproduce
+
+From the repository root, with CPython 3.12 and the standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/g20-long-conjugation-obstruction/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -O -B research/g20-long-conjugation-obstruction/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/g20-long-conjugation-obstruction
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/g20-long-conjugation-obstruction --check-source-history
+```
+
+Any CPython 3.12 interpreter can replace the local absolute path. Each direct
+check prints `PASS_G20_LONG_CONJUGATION_OBSTRUCTION candidates=1503
+missing_route=1450 emitted=53 neutral=14 strict_loss=39 min_contacts=4
+max_contacts=33`. The registered runner prints `PASS_REGISTERED_RESEARCH_PACKAGE`.
+The optional `--output /absolute/path/outside/checkout/receipt.json` writes a
+generated, source-bound receipt. It never writes into the checkout.
+
+Exact source commits, Git blobs and SHA256 pins are in
+[SOURCES.json](SOURCES.json); the changed card scope and structured follow-ups
+are in [TASK.json](TASK.json). The selected record and catalogue are historical
+provenance. The three live inputs are authenticated before use. Neither the
+predecessor verifier nor its larger caller is executed.
+
+## Limitations
+
+The result fixes the final PR5708 word, one conjugation, original correction
+frames and the published routes. A missing route is not a geometric impossibility.
+Further rewrites through neutral neighbors, added routes and different correction
+frames remain open. The certificate concerns the finite scalar endpoint and
+paid-query component, not a complete signed supplier invoice. Native/adjoint
+address action, the global caller, scalar allowance, target admission, compiler,
+precision, physical tape/storage and outer predicates were not replayed.
+No uniform program, rounded multiplier or proof-kernel verification is supplied.
+The five selected framework assumptions and selected kappa `781451/250000000`
+remain unchanged. Independent human and formal proof-kernel review are unclaimed.
+
+## Open next questions
+
+1. Can one of the 14 new neutral rewrites expose a later paid saving? Generate
+   one listed neutral word, enumerate its changed intervals and price the
+   complete emitted bill. This matters because the theorem permits one rewrite
+   only. No neutral-neighbor search or caller admission is supplied here.
+2. Can a new native route or a moved correction frame rescue a rejected interval?
+   Start with one recorded missing frame pair, construct its actual native
+   action, and charge routes, targets, scalar fees and restoration. These costs
+   and the complete physical caller remain unresolved.
+
+## Credit
+
+The new longer-contact result and certificate were produced by Nick Petalas.
+Credit unpaidmoon for PR6290's question and fixed-frame definition, and
+Ali Romman for PR5708's word, row-sensitive emitter and A2 construction,
+following Dugongue, ai-nanachi and all retained native, controller, helper,
+ordinary and stock sources. The standard A2 identity and subadditivity proof
+are not claimed as new. No predecessor file or credit line is changed.
+New work is Apache-2.0.

research/g20-long-conjugation-obstruction/SOURCES.json

@@ -0,0 +1,36 @@
+{
+  "schema_version": 1,
+  "base_commit": "2485805a6d47f36ea83ddde6327d453ac82d44dc",
+  "files": [
+    {
+      "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": "research/g20-conjugation-admission/PATHS.json",
+      "usage": "input",
+      "git_blob": "efbdf632746a971f9a593f57ccbb7d2cc67a6760",
+      "sha256": "f4dd58b78121040b1f054c0f7a626b25f6ef8d39f3de044d3456ea7dea8a6a5e"
+    },
+    {
+      "path": "research/g20-conjugation-admission/WORD.json.gz",
+      "usage": "input",
+      "git_blob": "3877a72d8a15adb03f6492f7d2fd8fa902ecb639",
+      "sha256": "8dd441fdb9c8923df06eb5ebfda37d03e4539f2305763e688d8c7025d196c4b1"
+    },
+    {
+      "path": "research/g20-conjugation-admission/construct.py",
+      "usage": "input",
+      "git_blob": "c0fe9d080b76171d8ed967cbad337c596d250a23",
+      "sha256": "2922052092d9323de2c715afb66dbd33fb58c7d0eeb3b9298bab5f7b2a930cb1"
+    }
+  ]
+}