Record a one-scale zero-swap word for the helper-462 matcher.

research/helper462-one-scale-word/README.md

@@ -0,0 +1,217 @@
+# One-scale zero-swap word for the helper-462 matcher
+
+**Constructive witness, plus a scoped integer-coefficient proof. No new κ.**
+The selected record stays `781451/250000000`.
+
+## Scope
+
+Original card: `supplier-boundary-audit`, priority revision 8, base
+`7c49fe32c55de02c2c873655c804b16e4c3fef0a`. Scope status: **refined**.
+
+Handoff comment
+[19137812](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19137812)
+leaves the literal stock/role/route generator open. Finding
+[19492596](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19492596)
+and fork draft PR 150 answer one letter-count piece of that handoff: the pinned
+helper-462 matcher has a zero-swap word with 7 scales and 27 shears, and at
+least one scale is necessary because `det(S) = -16`. This package takes the
+remaining one-scale question from that finding's open remainder and from PR 150's
+second open question. It does not rebuild the 7-scale word, price inherited P2
+tariffs, or search for a word with fewer than 27 shears at two or more scales.
+
+`current-priorities.md` on this base still quotes the older selected value from
+PR #5599. The verifier reads `certificates/selected-result.json`. That record is
+`781451/250000000`. This package does not edit it.
+
+## Alphabet
+
+Rows are numbered `0..7`. A letter is one of:
+
+- a shear `row_a += c * row_b` with `a ≠ b` and `c ∈ Q`;
+- a single-coordinate scale `row_a *= c` with `c ∈ Q \ {0}`;
+- an axis swap of two rows.
+
+A word is applied to `I` from the first letter through the last. Shears
+contribute determinant 1, a swap contributes `-1`, and a scale by `c`
+contributes `c`. For every word,
+
+`(product of the scale coefficients) * (-1)^{number of swaps} = det(product)`.
+
+The pinned matcher `S` is the `matcher` field of
+`research/bit-completed-backend-api/science/RESULT.json`. The same file's
+24 elementary factors multiply to `S` and use 5 swaps, 5 scales and 14 shears.
+That published word is rechecked as a source control. Its five swaps stay a
+valid schedule.
+
+## Witness
+
+`det(S) = -16`. Let `D` be the diagonal matrix that scales row 0 by `-16` and
+fixes the other rows. Then `W = D^{-1} S` has determinant 1. The elimination
+below writes `W` as 53 rational shears. Appending the scale by `-16` on row 0
+therefore multiplies to `S`.
+
+The frozen letters are `WORD.json`. Counts: **0 swaps, 1 scale, 53 shears**.
+The scale is the last letter, on row 0, with coefficient `-16`. Every shear
+coefficient lies in `Z[1/2]`; the denominators that occur are `1, 2, 4, 16`.
+The same elimination with the final scale placed on any other single row also
+multiplies to `S`, again with 53 shears. Those eight schedules are explicit
+words. Fifty-three is the length of this elimination, not a minimum.
+
+The witness is checked by exact rational arithmetic in two multiplications:
+successive row operations, and the product of the corresponding elementary
+matrices. Dropping any one of the 54 letters, changing the scale to `-8` or
+`+16`, or adding 1 to the first shear coefficient misses `S`.
+
+The determinant identity is a proof for every word in this alphabet: a
+zero-swap word has scale-product `-16`, so it uses at least one scale, and a
+single scale must have coefficient `-16`. The word above shows that one scale
+is also sufficient. The minimum number of scale letters in a zero-swap word is
+therefore exactly one. That minimum is not a statement about shear length.
+
+### Balanced scale
+
+For `u ∈ Q \ {0}` and two distinct rows `(R, S)`, the shears
+
+1. `R := R - (1/u) S`
+2. `S := S + (u - 1) R`
+3. `R := R + S`
+4. `S := S + (1/u - 1) R`
+
+replace `(R, S)` by `(u R, S/u)`. The verifier checks this identity on
+`2, -16, 1/2, 3/7, -1`. Expanding step 2 gives
+`S = (u-1)R_old + S_old/u`, and step 3 then collapses the first row to `u R_old`.
+Step 4 cancels the `(u-1) R_old` term against `(1/u - 1) u R_old`.
+
+### Signed exchange
+
+The three shears `R := R + S`, `S := S - R`, `R := R + S` send `(R, S)` to
+`(S, -R)`. No swap letter is used. The determinant of this `2×2` action is 1.
+
+### Elimination
+
+Start from a matrix of determinant 1. For each column `k` from `0` through `6`:
+
+- If the pivot is `0`, signed-exchange row `k` with the first later nonzero row
+  in that column. The processed columns `0..k-1` are already zero on every row
+  `≥ k`, so the exchange stays inside the trailing block.
+- If the pivot `p` is not `1`, apply the balanced scale on rows `(k, k+1)` with
+  unit `1/p`. Row `k` is multiplied by `1/p` and row `k+1` by `p`, so the pivot
+  becomes `1`.
+- Clear strictly below the pivot by shears.
+
+After column `k-1`, the leading `k×k` block is upper triangular with unit
+diagonal, hence determinant 1, and the block under it is zero. The whole
+determinant is 1, so the trailing minor has determinant 1 and its first column
+is not zero. The last diagonal entry is that final `1×1` minor, so it equals 1
+and needs no scale. Back-substitution from column `7` down to column `0` clears
+above each pivot. Reversing the reduction and negating each coefficient is a
+shear word for the determinant-1 matrix.
+
+Controls: the identity reduces to the empty word, and `diag(2, 1/2, 1, …, 1)`
+reduces to shears only.
+
+## Integer coefficients are impossible
+
+This is a proof under stated hypotheses. It is not a proof that every larger
+alphabet fails, and it is not a census of rational words.
+
+**Hypotheses.** Zero axis swaps, exactly one scale, and every shear coefficient
+an ordinary integer. The determinant identity forces that scale coefficient to
+be `-16`. The matrix of the word is therefore `E1 * D_i * E2`, where `D_i`
+scales coordinate `i` by `-16` and fixes the others, and `E1, E2` are products
+of integer elementary shears. Each shear is invertible over `Z`, so left or
+right multiplication by it preserves the gcd `Δ_6` of the `6×6` minors.
+
+`D_i` has at least six diagonal entries equal to `1`. The corresponding `6×6`
+minor is `I_6`, so `Δ_6(D_i) = 1`. The verifier checks the case `i = 0` on rows
+and columns `1..6`.
+
+`S` has rank `5` over `F_2`, by the following reduction. Entries of `S` mod 2:
+
+```
+row 0: 0 0 0 0 1 0 0 0
+row 1: 0 0 1 1 0 1 0 0
+row 2: 0 0 1 1 0 1 0 0
+row 3: 0 0 0 0 0 0 1 0
+row 4: 0 0 1 0 0 0 0 1
+row 5: 0 0 0 1 0 0 0 0
+row 6: 0 0 0 1 0 0 0 0
+row 7: 0 0 1 0 0 0 0 1
+```
+
+Rows `2, 6, 7` repeat rows `1, 5, 4`. Columns `0` and `1` are identically zero.
+On the five remaining rows, add row 5 into row 1 and then the new row 1 into
+row 4. The leading ones sit in columns `4, 3, 6, 2, 5`, all different, so these
+five rows are independent and the rank is exactly 5. Every six rows are
+dependent over `F_2`, every `6×6` minor is even, and `Δ_6(S)` is even. It
+cannot equal `Δ_6(D_i)`.
+
+So no integer-shear, zero-swap, one-scale word multiplies to `S`. The dyadic
+witness above uses a denominator `16`, which is consistent with this
+obstruction: the witness is not an integer word.
+
+## Minor census
+
+Separately, every `k×k` minor is enumerated. There are `C(8,k)^2` of them for
+each `k`, and the loops have no early exit. Exact Gaussian elimination produces
+the determinantal divisors
+
+`Δ = (1, 1, 1, 1, 1, 2, 4, 16)`.
+
+The invariant factors are `Δ_k / Δ_{k-1}` with `Δ_0 = 1`:
+
+`(1, 1, 1, 1, 1, 2, 2, 4)`.
+
+Each divides the next, and the product is `16 = |det(S)|`. This is an exhaustive
+finite census of minors. It is not a census of words. The impossibility proof
+above uses only that `Δ_6(S)` is even; the census records the exact value `2`.
+
+The single scale `diag(-16, 1, …, 1)` has `F_2`-rank 7, so the rank test does
+not reject every matrix of determinant `-16`.
+
+## What this does not say
+
+Fifty-three shears is the length of this elimination. A zero-swap word with at
+least two scales and fewer than 27 shears was not searched. Inherited P2
+tariffs were not evaluated, so no completed ordinary bill is claimed. No owner,
+ROW, fallback, tape, precision, or physical generator is emitted. No supplier
+is admitted. The selected frontier is unchanged.
+
+## Reproduce
+
+From the repository root, Python 3.12.3, standard library only:
+
+```sh
+python3 -B research/helper462-one-scale-word/verify.py
+python3 -I -B research/helper462-one-scale-word/verify.py
+python3 -O -B research/helper462-one-scale-word/verify.py
+python3 -B scripts/research_package.py --package research/helper462-one-scale-word
+```
+
+Expected first-line token: `PASS_HELPER462_ONE_SCALE_WORD`.
+
+No Lean, Docker, or selected cold replay was run.
+
+## Open next questions
+
+1. What is the minimal number of shears in a zero-swap word that uses exactly
+   one scale? The elimination above has length 53 on every coordinate. A shorter
+   one-scale word would still be an upper bound unless the search is exhaustive.
+   Keeping the scale count at one separates this question from a search at two
+   or more scales.
+2. Is there a zero-swap word whose scale coefficients multiply to `-16`, with
+   at least two scales and fewer than 27 shears? The 7-scale schedule has 27
+   shears and this witness has 53. Neither schedule answers that question, and
+   this package does not search it.
+3. With the inherited P2 tariffs, does any legal word beat the published pair on
+   the completed ordinary bill? Letter counts do not determine that bill. This
+   package records no tariff.
+
+## Credit
+
+The matcher and the five-swap elimination are from
+`research/bit-completed-backend-api` (Chris R / Clear1nsight, PR #4957), using
+the helper-462 witness of ai-nanachi #4760/#4814. The zero-swap 7-scale,
+27-shear schedule and the determinant lower bound of one scale are finding
+19492596 / fork draft PR 150. Prepared by unpaidmoon with substantial Cursor
+Grok assistance. Apache-2.0.

research/helper462-one-scale-word/SOURCES.json

@@ -0,0 +1,24 @@
+{
+  "schema_version": 1,
+  "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "input",
+      "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a",
+      "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    },
+    {
+      "path": "research/bit-completed-backend-api/science/RESULT.json",
+      "usage": "input",
+      "git_blob": "55dca30281e3375d63a128c3de041e46c8a3c5ba",
+      "sha256": "965b650c0e49572e028f89a60943c64ad8dff9032fc93272b86cd1f9715a77b7"
+    }
+  ]
+}

research/helper462-one-scale-word/TASK.json

@@ -0,0 +1,103 @@
+{
+  "schema_version": 1,
+  "task_id": "supplier-boundary-audit",
+  "priority_revision": 8,
+  "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a",
+  "original_card": {
+    "id": "supplier-boundary-audit",
+    "question": "Does one changed supplier have complete source-bound native, caller, ordinary and outer admission coverage?",
+    "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": "Pin the current sources and one obligation; the historical owner audit is an example, not evidence of a current bug.",
+    "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": "Choose one latest uncovered candidate and build a delta coverage map against the selected review. For P104, #5717 changes owned-lifetime assumptions and #5719 covers exact #5713 causal premises; neither automatically transfers to #5718. For BIT, #5679/#5708 need component admission and compatible outer use. Check controls and exact source identity before reuse; stop with one resolved gap or explicit remaining obligation. A heavy full replay requires a separate serial resource budget.",
+    "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": [
+      "supplier admission",
+      "5717",
+      "5719",
+      "5708",
+      "owned lifetime"
+    ],
+    "existing_checks": [
+      {
+        "scope": "PR #4088: author-checked local words, native receipts, owner/phase fill and exact moment.",
+        "evidence": "research/staged544-mixed-fourth-entry/README.md",
+        "remaining": "Rebind and validate ordinary/outer admission with all four providers; full mixed release not established.",
+        "status": "author-checked",
+        "source_commit": "72d7efc181edb21806a878f174847c96dd410ab0",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "scope": "PR #3801: successor scatter-boundary decision package.",
+        "evidence": "research/scatter-boundary-decision/README.md",
+        "remaining": "Consult its exact acceptance scope before any new exporter audit; not proof of a selected failure.",
+        "status": "author-checked",
+        "source_commit": "911f8800ba7a4b03603ef62c5ffc6240e53cb5fd",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "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": "refined",
+  "actual_scope": "For the pinned helper-462 matcher, the rational elementary alphabet of shears, single-coordinate scales and axis swaps contains a zero-swap word with exactly one scale. The exhibited word has 53 dyadic shears and one final scale by -16. Under the additional hypothesis that every shear coefficient is an integer, no zero-swap one-scale word exists. No supplier admission, tariff comparison, or new kappa.",
+  "scope_change_reason": "Handoff comment 19137812 asks for one literal N-dimensional stock/owner/route generator. Finding 19492596 and fork draft PR 150 already give a 0-swap, 7-scale, 27-shear word and the determinant lower bound of one scale. This package answers only the remaining one-scale existence question for that pinned matcher. It does not audit #5717/#5719, price inherited P2 tariffs, or search for fewer than 27 shears at two or more scales.",
+  "bottleneck_link": "The route ledger is one charged part of the missing physical generator. One scale is necessary by the determinant identity and sufficient in the rational alphabet, so a later generator cannot treat seven scales as forced. The integer-coefficient obstruction says that sufficiency uses a genuine dyadic shear. Shear length and the interchange/shear tariff remain open, so this is not a supplier admission.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop after the explicit one-scale word, the determinant identity, the integer-coefficient obstruction, the minor census, and the failure controls. Do not shorten the shear count, price P2 tariffs, or build the N-dimensional compiler.",
+  "outcome": "completed",
+  "evidence": "Exact rational product of the frozen 0-swap, 1-scale, 53-shear word equals the pinned matcher. The same elimination works with the scale on every row. Rank 5 over F2 makes every 6x6 minor even, while every one-coordinate integer scale by -16 has a 6x6 identity minor, so no integer-shear zero-swap one-scale word exists. The exhaustive minor census gives determinantal divisors (1,1,1,1,1,2,4,16).",
+  "author": "unpaidmoon",
+  "ai_assistance": "Prepared by unpaidmoon with substantial Cursor Grok assistance.",
+  "open_questions": [
+    {
+      "question": "What is the minimal number of shears in a zero-swap word that uses exactly one scale?",
+      "why_it_matters": "The elimination in this package has 53 shears on every coordinate. That length is an upper bound. It sits above the known 7-scale schedule of 27 shears, so it does not improve the shear count.",
+      "first_step": "Keep exactly one scale of coefficient -16 and replace one balanced-scale block by a shorter shear identity, then recheck the product against the pinned matcher.",
+      "blocked_by": "This package stops at existence. A shorter explicit word would still be an upper bound unless the search is exhaustive."
+    },
+    {
+      "question": "Is there a zero-swap word for this matcher with at least two scales and fewer than 27 shears?",
+      "why_it_matters": "The published swap-free schedule uses 7 scales and 27 shears. The one-scale witness uses 53 shears. Neither answers the two-or-more-scale shortening question.",
+      "first_step": "Search words whose scale coefficients multiply to -16, with scale count at least 2 and shear count at most 26.",
+      "blocked_by": "That search is a separate question. This package does not run it."
+    },
+    {
+      "question": "With the inherited P2 tariffs, does any legal word beat the published pair on the completed ordinary bill?",
+      "why_it_matters": "Letter counts do not determine the signed moment. Removing swaps and adding shears can move the bill in either direction.",
+      "first_step": "Pin the inherited ordered-affine, unit-scaling and completed-interchange costs used by research/bit-completed-backend-api and evaluate one legal word at that invocation.",
+      "blocked_by": "Those primitive tariffs are a separate comparison. This package records no bill."
+    }
+  ]
+}

research/helper462-one-scale-word/VERIFY.json

@@ -0,0 +1,21 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "certificates/selected-result.json",
+    "research/bit-completed-backend-api/science/RESULT.json"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 60,
+      "checks": "Pinned matcher equals the published 5-swap word and an explicit 0-swap 1-scale 53-shear word; the same elimination works on every scale row; determinant identity; balanced-scale and signed-exchange identities; dropped-letter, mutated-scale and mutated-shear controls; F2 rank 5; exhaustive determinantal divisors (1,1,1,1,1,2,4,16); the one-integer-scale matrix has a 6x6 identity minor."
+    }
+  ]
+}