Prove three Gaussian blocks need five internally restoring stages (no κ)

research/moving-stage-restoration-tariff/PROOF.md

@@ -0,0 +1,113 @@
+# Exact restoration tariff for positive moving stages
+
+This scoped proof is produced by Nick Petalas. Apache-2.0.
+
+## Contract
+
+Take finitely many coordinate blocks indexed by `0,1,...,m-1`, each of
+the same positive width `w`. Block 0 is the anchor. Let `D_j` be the
+normalized Gaussian on block j. The `D_j` commute, and `D_j^2` is a
+block-local monomial. Let `P_s` exchange blocks 0 and s, with `P_0=I`.
+The only charged stages are the positive operators
+
+    E_s = P_s D_0,    s=0,...,m-1.
+
+This is Cinna Davis's #5113 moving-coordinate interface, with the terminal
+anchor stage used by Chris R / Clear1nsight's #5133. These premises are
+cited, not independently audited here. Their native and coded-owner
+semantics remain their premises.
+
+Write an endpoint in the exact normal form
+
+    P_pi product_j D_j^(a_j),    a_j >= 0.
+
+The requested boundary requires `pi=identity`. It requests odd Gaussian
+exponent on precisely a set S of nonanchor blocks and anchor parity b
+in `{0,1}`. All other blocks must have even exponent. The whole-block
+permutation must restore inside the charged word. The even powers are
+explicit residual block-local monomials. They are not removed for free.
+This is a Gaussian-support quotient with internal block-permutation
+restoration, not exact identity restoration of every address and phase.
+
+## Theorem
+
+For `k=|S|`, the least number of positive stages is
+
+    L(S,b) = 2k + ((k+b) mod 2).
+
+It is independent of the number of unrequested spectator blocks.
+For all m blocks requested, the value is `2m-2+(m mod 2)`.
+
+## Lower bound
+
+In any prefix normal form, left multiplication by `E_s` adds one to
+`a_(pi^-1(0))`, then replaces `pi` by `(0 s) pi`. This follows by moving
+`D_0` through `P_pi`. Consequently `sum_j a_j` is exactly the word length.
+Its parity at the requested endpoint is `k+b` modulo two.
+
+Every requested nonanchor label j must occur among the stage indices.
+If it never occurs, every block permutation fixes j, so `pi^-1(0)`
+can never be j. Its Gaussian exponent stays zero, contradicting the
+requested odd exponent.
+
+Moreover j cannot occur exactly once when the final permutation is the
+identity. Before that occurrence the coordinate initially at j is still
+at j. That occurrence moves it to block 0. No later transposition touches
+position j, so that coordinate cannot return to j. Thus every member of
+S needs at least two nonanchor stages. The length is at least `2k` and
+has parity `k+b`. These two conditions give the displayed bound. The
+argument allows arbitrarily many additional unrequested blocks and visits.
+
+## Attaining word and its exact residual
+
+For every j in S, use the consecutive pair `E_j E_j`. Since
+`D_0 P_j = P_j D_j`, this pair is exactly
+
+    E_j^2 = D_j D_0.
+
+Each pair restores its entire block permutation. Use all k pairs, then
+append `delta=((k+b) mod 2)` copies of `E_0`. The exact endpoint is
+
+    D_0^(k+delta) product_(j in S) D_j
+      = M_0 D_0^b product_(j in S) D_j,
+    M_0 = (D_0^2)^((k+delta-b)/2).
+
+The exponent of `M_0` is a nonnegative integer. Thus the word meets
+every requested parity and restores all block permutations, with exactly
+`2k+delta` charged stages. All unrequested nonanchor coordinates are
+untouched. `M_0` is part of the explicit endpoint, not a waived fee.
+This proves equality for every block width w and every finite number of
+spectators. For w=8 it applies to #5113's eight-axis Gaussian blocks.
+
+## Consequence for an internally restored three-block word
+
+Request all three blocks, with `k=2,b=1`. The exact minimum is five
+stages. The three-stage word `E_0 E_2 E_1` in #5133 obtains the same
+Gaussian support after an external block permutation is removed. Its
+permutation is `P_2 P_1`, not identity, so it is outside this theorem's
+return boundary. This is a changed requirement, not a disagreement with
+that source. The five-stage constructor has residual `D_0^2`.
+
+The theorem prices stage occurrences only. It does not establish a
+minimal physical tape tariff or compare stages against the price of an
+external permutation. It gives no main-owner independence, helper-target
+credit, legal consumer, new signed invoice, supplier admission, new kappa
+or complete multiplication theorem. Arbitrary nonmonomial free maps,
+independently available `D_j`, and a boundary accepting a residual block
+permutation change the model.
+
+## Finite corroboration
+
+The verifier implements the constructor and exact nonnegative exponent
+normal form. An independent breadth-first search instead stores the
+output-frame representation `D_mask P_pi`. It enumerates the full finite
+quotient for one through six blocks, permits every stage at every state,
+and obtains the distances to every permutation-restored support. It
+imports no predecessor implementation.
+
+A separate literal address-array interpreter uses the Gaussian
+`[[a,b],[b,a]]` over F_65537 with `a=(1+i)/2`, `b=(1-i)/2`, `i=256`.
+Here `i^2=-1`, `D^2=X` and `D^4=I`. It checks every operator column for
+all support requests on the declared one-axis and two-axis block fixtures,
+including the explicit `M_0`. This is finite-field corroboration; the
+all-width theorem is the algebraic argument above.

research/moving-stage-restoration-tariff/README.md

@@ -0,0 +1,109 @@
+# Sharp positive moving-stage restoration count
+
+Scoped mathematical proof with exact finite corroboration. For the moving
+Gaussian stages `E_s=P_(0,s) D_0`, including `E_0=D_0`, request Gaussian
+parity on k nonanchor blocks and anchor parity b. If the entire block
+permutation must restore inside the charged word, the exact minimum is
+
+```text
+L(k,b) = 2k + ((k+b) mod 2).
+```
+
+Unused spectator blocks cannot shorten it. In particular, requesting all
+m blocks costs `2m-2+(m mod 2)` stages. The internally restored three-block
+boundary needs five stages. This gives an explicit cost for one restoration
+method; it does not establish an improved recursive invoice or kappa.
+
+[PROOF.md](PROOF.md) gives the lower bound and an attaining word. Each
+requested nonanchor stage is used twice. At most one anchor stage corrects
+parity. The exact residual is an explicitly stated block-local monomial
+`(D_0^2)^((k+delta-b)/2)`, with `delta=(k+b) mod 2`. That monomial remains
+part of the output contract and is not a free cleanup operation.
+
+## Relation to predecessors
+
+Cinna Davis / 1337isnot1337's [PR #5113](https://github.com/CrocSwap/integer-mult-bounds/pull/5113)
+supplies the common-code moving-coordinate interface and its native/caller
+limitations. Chris R / Clear1nsight's [PR #5133](https://github.com/CrocSwap/integer-mult-bounds/pull/5133)
+uses a terminal anchor stage and rejects a fixed optimistic three-stage
+invoice. Its three-stage word accepts an external whole-block permutation.
+This result imposes internal permutation restoration instead and proves
+the exact count for every target support and every number of blocks.
+It does not replay, audit or claim either predecessor's result.
+
+Credit Dillon #4933, Dugongue #4929, Cao Yifan, Cayden Burkart, JoyboyBrian,
+zxv, Jacob Alan Sussman and the retained native/compiler/precision lineage
+through #5113. Elementary permutation and tensor-product identities are
+standard. The new scoped tariff, proof and verifier are produced by Nick Petalas.
+Independent human and formal proof-kernel review are unclaimed. Apache-2.0.
+
+## Reproduce
+
+From the repository root, use CPython 3.12 and the standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -I -B research/moving-stage-restoration-tariff/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -I -O -B research/moving-stage-restoration-tariff/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/moving-stage-restoration-tariff
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/moving-stage-restoration-tariff --check-source-history
+```
+
+Both direct modes print `PASS_MOVING_STAGE_RESTORATION_TARIFF` with
+50,362 quotient states, 126 permutation-restored endpoints, 916 literal
+operator columns and 12 controls. The independent BFS uses an output-frame
+state rather than the constructor's input-frame exponent representation.
+Every stage is allowed at every quotient state. Literal finite-field
+operators check every basis column on the declared fixtures, including
+two-axis blocks and the residual local monomial. No predecessor executable
+is imported. These are checks of the new theorem, not source replays.
+
+Default verification writes nothing and needs no Git or network. Optional
+`--receipt NEW_PATH` creates a receipt bound to the six package file hashes
+and refuses an occupied path. The registered commands time out at 120
+seconds each. All controls remain active under optimized Python.
+
+## Scope and limits
+
+The theorem covers every positive block width and finite spectator count.
+The executable constructor and quotient oracle are bounded to six blocks;
+the literal operator fixtures use one-axis blocks through four blocks and
+two-axis blocks through three blocks. Finite enumeration corroborates the
+written proof and does not replace it.
+
+Only positive stages of this stated alphabet are charged. The endpoint
+permits explicit block-local monomials and requires internal restoration
+of the permutation of whole blocks. A caller accepting an external
+permutation has a different contract. Full local-monomial cleanup, physical
+movement, owner independence, helper targets, native/caller/compiler and
+precision costs remain unpriced. No selected cold replay, Lean proof,
+complete supplier, new kappa or complete multiplication theorem is claimed.
+The selected frontier is unchanged.
+
+Base is canonical main `19fdb086ea96af9a9f87936a2b888e10af4ed810`, priority
+revision 8. The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19226084)
+and [TASK.json](TASK.json) state the changed boundary and overlap coverage.
+[SOURCES.json](SOURCES.json) pins both predecessor texts and the historical
+card/selected record. Live open PRs, recent account PRs, handoffs, main
+README terms and merged searches were checked; unpublished work and notes
+outside those searches are not excluded.
+
+## Open next questions
+
+- Price internal restoration against an external block permutation in one
+  actual complete caller. Start with that caller's exact endpoints and
+  paid/target inventories, including the residual local monomial. The
+  physical permutation tariff and consumer are missing here.
+- Determine the minimum under a stricter contract that eliminates every
+  residual local monomial. Start with exponents modulo four and fix whether
+  inverse stages are legal. That different alphabet/endpoint contract is
+  not answered by the present parity theorem.
+
+## Implementation bounds
+
+All loops have finite bounds from the declared block domains. The BFS has
+at most `6! * 2^6` states and six outgoing stages per state. Literal vectors
+have at most 64 entries. No function recurses and every function fits within
+60 lines. Explicit exceptions enforce contracts in both Python modes.
+Python integers and collections allocate dynamically; this is a bounded
+managed-runtime verifier, not a fixed-allocation physical implementation.
+Warning-strict normal and optimized replay provide interpreter diagnostics.

research/moving-stage-restoration-tariff/SOURCES.json

@@ -0,0 +1,30 @@
+{
+  "schema_version": 1,
+  "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8",
+      "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    },
+    {
+      "path": "research/common-code-moving-stages/PROOF.md",
+      "usage": "input",
+      "git_blob": "60fecc67b7847e2f40d31710e49de3a4c23eeab2",
+      "sha256": "46b427b0834aa513bba6244e3b44a089597fdb0546d0fda8c5e41130e6881eeb"
+    },
+    {
+      "path": "research/moving-anchor-no-q-ceiling/README.md",
+      "usage": "input",
+      "git_blob": "130f7b7c638be69b88f0ad83181027b082b59ac4",
+      "sha256": "40673b8a0561c2fcd690ab7d10ac44269361b5fd3d788b84e44dbbf44374e1aa"
+    }
+  ]
+}

research/moving-stage-restoration-tariff/TASK.json

@@ -0,0 +1,91 @@
+{
+  "schema_version": 1,
+  "task_id": "complex-rank-shape-decoder",
+  "priority_revision": 8,
+  "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810",
+  "original_card": {
+    "id": "complex-rank-shape-decoder",
+    "question": "Can a legal decoder or coframe change improve the full signed moment, including changed helper targets?",
+    "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",
+      "docs/research/recursive-invoice-preflight.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": "Price one complete changed itinerary with both paid and productive histograms. Check #5693/#5698 for overlap and their exact hypotheses before another coframe search. Use the signed invoice preflight where its boundary contract agrees; an inconclusive concave comparison is not a power crossing. Stop if an optimistic complete budget fails at the chosen target or native delivery remains unspecified.",
+    "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": [
+      "coframe",
+      "signed moment",
+      "5693",
+      "5698"
+    ],
+    "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": "Exact minimum positive moving-stage count with internally restored whole-block permutation and specified Gaussian parity support, modulo explicit block-local monomials.",
+  "scope_change_reason": "Original restoration-boundary question building on the moving-coordinate interface of PR5113. No full signed-moment improvement is asserted; stage count isolates a previously unpriced return obligation.",
+  "bottleneck_link": "The current new-decoder track requires complete restoration. This theorem prices stage-only internal block-permutation return instead of assuming an external whole-field permutation is free. Local monomial and caller costs remain unknown.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop research at the first verified original scoped result; package this exact tariff without seeking a larger result.",
+  "outcome": "completed",
+  "evidence": "PROOF.md supplies an all-width proof. verify.py checks 50362 quotient states, 126 restored endpoints, 916 literal finite-field operator columns and 12 controls in normal and optimized modes.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "For one actual moving-coordinate caller, is an external block permutation cheaper than the extra internally restoring stages?",
+      "why_it_matters": "The exact stage count alone cannot choose a physical restoration method or establish a recursive gain.",
+      "first_step": "Pin a complete caller and charge its external block permutation, the additional stages, residual local monomial and all productive helper targets on the same boundary.",
+      "blocked_by": "No complete caller or physical permutation tariff is supplied here."
+    },
+    {
+      "question": "What is the minimum if every residual block-local monomial must also be eliminated by the charged alphabet?",
+      "why_it_matters": "The present optimum permits a specified anchor monomial at the output, which a stricter consumer may reject.",
+      "first_step": "Retain Gaussian exponents modulo four and specify whether inverse stages are available before deriving a new bound.",
+      "blocked_by": "A stricter endpoint contract and native stage alphabet must be fixed first."
+    }
+  ],
+  "claim_type": "scoped mathematical proof with exact finite corroboration",
+  "coordination": {
+    "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19226084",
+    "overlap": "Live open PR list, latest 30 handoff comments, active Discussions, recent account PRs, merged PR searches and main README searches consulted. Cached local note coverage is sparse; no exhaustive novelty claim."
+  },
+  "environment": {
+    "python": "3.12.15 (main, Oct 14 2026, 00:55:37) [Clang 23.1.3 ]",
+    "platform": "macOS-27.0.1-arm64-arm-64bit",
+    "dependencies": "standard library only"
+  }
+}

research/moving-stage-restoration-tariff/VERIFY.json

@@ -0,0 +1,37 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/common-code-moving-stages/PROOF.md",
+    "research/moving-anchor-no-q-ceiling/README.md"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-W",
+        "error",
+        "-I",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Full finite quotient BFS, explicit attaining words, all operator columns and malformed-input/endpoint controls."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-W",
+        "error",
+        "-I",
+        "-O",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Same complete checks with Python assertions disabled; all contracts use explicit exceptions."
+    }
+  ]
+}