Lower inverse-code arithmetic to a smaller complete local tape bound

research/factored-code-tape/PROOF.md

@@ -0,0 +1,128 @@
+# A complete local tariff for the factored mode code
+
+This is a conditional arithmetic construction on a fixed classical multitape
+machine. It does not establish common-coordinate access in a Gaussian caller.
+The source matrix, rounding rule and original tape contract are the inputs in
+SOURCES.json. The scalar factorization was first recorded in
+[Discussion #5314](https://github.com/CrocSwap/integer-mult-bounds/discussions/5314).
+This package adds a fixed-word instruction table, temporary allocation and a
+complete local tariff.
+
+## Domain and schedule
+
+Use the same integer grid, input bound H>=0 and word width
+W=bit_length(56H+2)+1 as the source kernel. Each of 112 owner tapes contains N
+signed W-bit words, with one delimiter per word and a final end marker.
+Real and imaginary components are separate records. The source mode matrix
+is fixed in the finite control. The emitter checks its fourteen sign cubes;
+it is a certificate generator, not a variable-matrix machine oracle.
+
+There are eight mode tapes, eight temporary tapes, one division tape and one
+readonly bound tape: 130 tapes in total. The 17 owned words start with arbitrary
+bits. Initialize them once. On each coordinate validate all 112 owner values,
+run the 308-instruction gather, run the eight source ROUND52 transducers,
+run the 280-instruction scatter, clear the 16 mode/temporary words and advance
+all owner heads. The division word is already zero after each source range or
+division operation. Rewind all owner tapes at the end. For N=0, initialization
+and final framing still run.
+
+All gathers finish before the first owner update. The emitted gather and
+scatter programs use separate temporary identifiers. The allocator computes
+last uses, then reuses a last-used input slot for an output when possible.
+It rejects a read before definition, an allocation above eight words and
+any live temporary at the end. It emits literal tape indices 0,...,127 for
+signed sums. Division uses tape 128 and the readonly bound is tape 129.
+No arbitrary native helper tape appears.
+
+The actual matrix has fourteen four-mode supports, each with the eight
+projective sign patterns. For one group, signed source views identify the
+rows with (1,+/-1,+/-1,+/-1). Four pair sums and four pair differences cost 8.
+The sum of differences costs 3. Three selected transforms of the four sums
+cost 7. Four updates to global modes cost 4. Thus gather costs14*22=308.
+For scatter, form a+b,a-b,c+d,c-d in 4 sums, form each of the eight corrections
+in one sum, and perform eight owner updates:14*20=280. Source signs are part
+of each signed binary instruction. Copies or sign maps are not extra hidden
+instructions: the next section gives a direct two-input signed primitive.
+
+## Finite signed primitive and range
+
+An instruction is z=a*x+b*y, with a,b in {-1,1}. Read the two source bits
+before writing the destination bit. Start carry at [a=-1]+[b=-1]. At bit j,
+add (x_j xor [a=-1]), (y_j xor [b=-1]) and the carry; write the low bit and
+retain the remaining carry. Carry is in {0,1,2}. This is the usual two's
+complement identity for the sum of two signed words. The destination may
+be a last-used source word: the current bits are read first, and later bits
+are not changed. A forward scan and a return sweep cost at most 2W+4
+transitions. All addressed heads move together; unaddressed heads stay put.
+The destination is written in full, so its prior contents do not matter.
+
+Each temporary gather sum has magnitude at most8H; each partial mode has
+magnitude at most56H. The source division returns q with
+|q|<=14H/13+1/2. A scatter temporary is a signed sum of at most four such
+values. Its magnitude is at most56H/13+2. An updated owner has magnitude at
+most69H/13+2. All are at most56H+2. Hence every mathematical signed result
+fits W bits and the modular carry loop equals that result. Division and
+range validation are the authenticated source bit loops. Rounding occurs
+at exactly the same eight mode values as before. The final owner words
+therefore agree for every valid input, including signed ties.
+
+The allocator attains eight temporary words. One can also see this directly:
+form the four sums and differences; reduce the differences first; form each
+sum-pair's sum before its difference releases the old pair; then form the
+three required coefficients and consume all four outputs. Scatter needs
+only four pair values and one current correction. The runtime representation
+is a reference interpreter of these fixed words. It is not a measured
+physical TM or a benchmark of the full Gaussian caller.
+
+## Complete tariff
+
+Reuse the source primitive bounds: validation 8W+16, ROUND52 at most 24W+64,
+and CLEAR/INIT at most 2W+4. Signed binary sums have the bound proved above.
+All primitives return their participating heads to the current word start.
+Owner advance costs W+1 with all 112 heads moving together. Final rewind
+costs N(W+1)+2. Include 62 further framing transitions.
+
+```text
+T <= 17(2W+4)
+   + N[112(8W+16) + 588(2W+4) + 8(24W+64)
+        + 16(2W+4) + (W+1)]
+   + N(W+1) + 64
+  = N(2298W+4722) + 34W+132.
+```
+
+At most 130T individual head moves, symbol reads and symbol writes suffice.
+The storage bound is 112[N(W+1)+1] owner cells, 17(W+1) owned scratch cells,
+and W+1 readonly bound cells, plus fixed framing. There are 144N+17 complete
+zero-writing scans: 112 range clears, 16 internal division clears and 16 final
+mode/temporary clears per coordinate, plus 17 initial clears. This cleanup
+is paid classical writing, not reversible uncomputation.
+
+The old bound is N(2898W+5922)+18W+100. Old minus new equals
+N(600W+1200)-16W-32, which is positive for every N>=1 and W>=3. This compares
+constructive upper bounds in two stated fixed-tape models. The new machine
+has130 tapes rather than122 and uses eight more temporary words. It is not
+an optimality or measured speed claim. The rounded map, two-grid-unit local
+error and noninjectivity are unchanged.
+
+## Evidence and remaining obligations
+
+The verifier checks all 112 gather and eight scatter basis columns with the
+emitted finite-word instructions. It compares 48 mixed/extreme coordinate
+vectors in 36 batches, including N=0,1,3 and H=0,1,6,26,51,250, against the
+actual source kernel. It starts every owned scratch bit dirty and requires
+all 17 words clean. An independent primitive invoice sums to the displayed
+formula. A changed numerical sign and owner alias are rejected. Hash pins
+bind every external input; source modules load from their authenticated
+source bytes, without a bytecode-cache import.
+
+The written range, carry, schedule and sweep arguments give the quantified
+local result. Finite replay does not establish the full physical caller,
+common-coordinate field access, native Gaussian accuracy, compiler reserve,
+reversible ownership, a new supplier or a new kappa. Extra wrappers and
+field movement remain charged caller obligations.
+
+Credit JoyboyBrian's PR #5035 for the source divider, validation, rounding and
+classical sweep contract; Dillon's PR #4933 for the physical mode factorization;
+Dugongue and retained native/precision/compiler authors for their source work.
+The Walsh transform is standard. New emitted schedule, allocation, tariff,
+proof and checks: Ali Romman with OpenAI Codex assistance. Apache-2.0.

research/factored-code-tape/README.md

@@ -0,0 +1,63 @@
+# A smaller local tape bound for inverse recoding
+
+This conditional arithmetic construction lowers the actual source mode code
+to a 130-tape classical machine. Its complete local bound is
+`N(2298W+4722)+34W+132`, compared with the source bound
+`N(2898W+5922)+18W+100`. The new bound is smaller for every N>=1.
+The machine uses eight extra temporary words. Its rounded numerical map,
+eight division calls and two-grid-unit local error are unchanged.
+
+[PROOF.md](PROOF.md) gives the fixed-word schedule, range and sweep proof.
+[kernel.py](kernel.py) emits 308 gather and 280 scatter instructions and
+allocates at most eight temporary words. [RESULT.json](RESULT.json) records
+the exact replay. [SOURCES.json](SOURCES.json) pins all consumed input bytes
+at canonical main ff3cc58e370d0f678e529246f8c73e8094e18fcf, priority 7.
+
+This adds the physical arithmetic bill left open by
+[Discussion #5314](https://github.com/CrocSwap/integer-mult-bounds/discussions/5314),
+whose scalar factorization is reused with credit. The
+[scoped claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/5314#discussioncomment-19150518)
+excludes the complete coded caller. All112 owner tapes are distinct and
+provided at common coordinates. All17 owned scratch words return zero;
+this is paid classical overwriting, not reversible cleanup.
+
+## Reproduce
+
+Use CPython 3.12 and the standard library from the repository root:
+
+```sh
+python3.12 -B scripts/research_package.py --package research/factored-code-tape
+python3.12 -I -O -W error -B research/factored-code-tape/verify.py
+```
+
+Expected marker: PASS_FACTORED_CODE_TAPE. Both registered modes check all 112
+and eight basis columns, 36 batches, 48 mixed/extreme source comparisons,
+N=0/1/3, dirty scratch return, independent tariff addition and numerical-sign
+and alias controls. Source imports use authenticated bytes. The emitted bit
+instructions execute; the complete target TM is specified by a sweep proof,
+not measured as a full physical caller.
+
+No native Gaussian, compiler, outer ledger, Lean or selected replay ran.
+The Gaussian paid profile and complete kappa calculation are unchanged.
+Common-coordinate access, wrappers, field movement and full error funding
+remain caller obligations. This is author-checked evidence; independent
+human or proof-kernel acceptance is not claimed.
+
+## Open next questions
+
+Bind the tariff and 17-word workspace to one affordable complete caller with
+legal common-coordinate access. First charge its wrappers and physical
+movement and retain its error budget. Those missing caller contracts block
+admission; they are not zero-cost operations. The structured question is in
+TASK.json.
+
+## Credit
+
+[PR #5035](https://github.com/CrocSwap/integer-mult-bounds/pull/5035) by JoyboyBrian
+supplies the finite divider, rounding, validation and original sweep tariff.
+[PR #4933](https://github.com/CrocSwap/integer-mult-bounds/pull/4933) by Dillon
+supplies the source physical mode factorization. Dugongue and retained
+native, ownership, precision and compiler authors keep their source credit.
+Standard Walsh butterflies are not claimed as new. New lowering, allocation,
+tariff and checks: Ali Romman with substantial OpenAI Codex assistance.
+Apache-2.0. Frozen sources and notices remain unchanged.

research/factored-code-tape/RESULT.json

@@ -0,0 +1,18 @@
+{
+  "status": "PASS_FACTORED_CODE_TAPE",
+  "gather_columns": 112,
+  "scatter_columns": 8,
+  "mixed_and_extreme_vectors": 48,
+  "batch_cases": 36,
+  "signed_sums": 588,
+  "temporary_words": 8,
+  "tapes": 130,
+  "scratch_words": 17,
+  "transition_upper": "N(2298W+4722)+34W+132",
+  "zero_scans": "144N+17",
+  "controls": [
+    "wrong_sign",
+    "owner_alias"
+  ],
+  "physical_caller_run": false
+}

research/factored-code-tape/SOURCES.json

@@ -0,0 +1,36 @@
+{
+  "schema_version": 1,
+  "base_commit": "ff3cc58e370d0f678e529246f8c73e8094e18fcf",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395",
+      "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602",
+      "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72"
+    },
+    {
+      "path": "research/coded-inverse-fixed-grid/PROOF.md",
+      "usage": "input",
+      "git_blob": "a465ed5ce6b0bd7ac03bc79e72003380a839d7f4",
+      "sha256": "2bf523cf4f4b3e6bd90805e86f2cbf5d1d85142c16e751e72f09480bcdbee5cd"
+    },
+    {
+      "path": "research/coded-inverse-fixed-grid/kernel.py",
+      "usage": "input",
+      "git_blob": "70b5d65cae9a8f19cfda4a862c7ecc0bdc42c89b",
+      "sha256": "bc0e9f705665d6981c0f9176dad0f2d71471735e866c44643cb6835423435303"
+    },
+    {
+      "path": "research/coded-native-caller/NORMALIZERS.json",
+      "usage": "input",
+      "git_blob": "bca92c222c395d3d75c047fbb678f3cd0947c60f",
+      "sha256": "ae8aad06aa5d1811d725895b3ab5a4f4daa9dcdd88294aa0d5f723e78bb1e0da"
+    }
+  ]
+}

research/factored-code-tape/TASK.json

@@ -0,0 +1,74 @@
+{
+  "schema_version": 1,
+  "task_id": "uniform-transfer-audit",
+  "priority_revision": 7,
+  "base_commit": "ff3cc58e370d0f678e529246f8c73e8094e18fcf",
+  "original_card": {
+    "id": "uniform-transfer-audit",
+    "question": "Does one quantified step of the proposed #4100 all-size construction hold at its actual caller?",
+    "starting_points": [
+      "docs/research/research-family-status.md",
+      "certificates/selected-result.json",
+      "research/unconditional-batched-crt/README.md"
+    ],
+    "methods": [
+      "Prove one missing implication with explicit quantified hypotheses.",
+      "Find an exact counterexample at the claimed interface boundary."
+    ],
+    "acceptance_gate": "Identify the proposition and what would change downstream; do not equate a finite replay with a universal proof.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Read PROOF.md and AUDIT.md in #4100. Select one distinct obligation: CRT total repair, native/free-algebra lifting, precision/conditioning, or complete fixed-tape cost. This is an author-submitted proof, not an accepted unconditional theorem.",
+      "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately."
+    },
+    "first_experiment": "Check live handoffs; name one proposition, its caller, quantified domain and dependency closure. Independently prove the implication or exhibit a precise gap/counterexample. Prioritize CRT.md total repair or COMPLEX.md free-algebra lift only if unclaimed. Stop at the chosen obligation; do not substitute finite samples or root arithmetic for an all-size proof, or launch the complete package by default.",
+    "bottleneck_link": "Finite supplier improvements are useful only under the retained transfer obligations.",
+    "allowed_variations": [
+      "One CRT repair, native lift, precision/conditioning or tape-cost proposition, with its exact caller."
+    ],
+    "scope_change_triggers": [
+      "Replacing a quantified obligation with another finite smoke test.",
+      "Treating archive intake, an author PASS receipt or a finite composed fixture as discharge of the universal hypotheses."
+    ],
+    "overlap_terms": [
+      "uniform transfer",
+      "all-size",
+      "precision",
+      "4100",
+      "unconditional-batched-crt"
+    ],
+    "existing_checks": [
+      {
+        "scope": "PR #4100: proposed unconditional construction and finite checks, without independent acceptance.",
+        "evidence": "research/unconditional-batched-crt/README.md",
+        "remaining": "Independent proof audit of one caller-bound all-size implication; all other premises remain explicit.",
+        "status": "author-checked",
+        "source_commit": "337d04939571a637aeab54a0f58f54fde811663a",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      }
+    ]
+  },
+  "scope_status": "refined",
+  "actual_scope": "A fixed-word lowering and complete classical 130-tape tariff for the actual 588-sum inverse-code schedule.",
+  "scope_change_reason": "The live inverse-code caller needs a complete local bit/tape bill. Discussion5314 gave only the scalar factorization. This result supplies emitted instructions, temporary allocation, input validation and paid cleanup.",
+  "bottleneck_link": "Physical coded callers need bounded finite recoding with all ordinary work and owned state charged.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop after the source-bound local fixed-tape bound and exact numerical-map comparison; do not change Gaussian jobs or selected kappa.",
+  "outcome": "completed",
+  "evidence": "PROOF.md and RESULT.json: complete basis checks, 36 bounded batches, 48 source-kernel coordinate comparisons, dirty scratch return, independent invoice and sign/alias controls.",
+  "author": "Ali Romman with OpenAI Codex assistance",
+  "ai_assistance": "Substantial OpenAI Codex assistance; no subagents or independent human review.",
+  "open_questions": [
+    {
+      "question": "Can an affordable complete caller supply the common-coordinate owner layout and fund all wrappers and movement?",
+      "why_it_matters": "The local arithmetic bound does not include physical field access or recursive Gaussian calls.",
+      "first_step": "Bind this tariff and its 17-word workspace to one named caller layout and its error budget.",
+      "blocked_by": "Complete physical caller and common-coordinate ownership contracts."
+    }
+  ]
+}

research/factored-code-tape/VERIFY.json

@@ -0,0 +1,38 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/coded-inverse-fixed-grid/PROOF.md",
+    "research/coded-inverse-fixed-grid/kernel.py",
+    "research/coded-native-caller/NORMALIZERS.json"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 60,
+      "checks": "Source pins, all linear basis columns, complete bounded batches, source word equality, paid scratch return, independent tariff and semantic controls."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-O",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 60,
+      "checks": "Source pins, all linear basis columns, complete bounded batches, source word equality, paid scratch return, independent tariff and semantic controls."
+    }
+  ]
+}