Lower the G20 carry leaf to 1115V/3 transitions and 24V cells (no new κ)

research/unit-modulus-carry-bypass/PROOF.md

@@ -0,0 +1,133 @@
+# The prefix and its uniform physical bounds
+
+This is a scoped construction in the nineteen-tape, seven-symbol machine
+of the retained PR5849 quarter-carry leaf. One literal branch, write, unit
+move, goto or halt costs one transition. Space is the sum of visited tape
+interval lengths, including all nineteen initial head positions and erased
+storage. These are the predecessor's currencies.
+
+## Declared interface and dependencies
+
+Let P,Q,S be positive canonical LSB-first binary descriptors. Q is odd.
+Tape0 contains the complete original-owner Boolean stream of volume V=PQS.
+Tape5 starts on the first Q bit. The valid supplied packet encodes k+16 in
+five bits, with -16<=k<=12. All private and spectator contracts are exactly
+those of the pinned source. The requested permutation is a rotation by
+plus or minus k*4^-1 modulo Q in the Q coordinate, with all other state
+restored. At Q=1 this is the identity, since there is only one coordinate.
+
+For odd Q>=3, cite the following nonunit conclusions from the section
+"Physically supplied quarter code" of PR5849's retained PROOF.md:
+
+```text
+T_old <= (1111/3)V,
+W_old <= 24V.
+```
+
+These are used as predecessor results, not re-proved or independently
+replayed. In particular the old offset producer, payload permutation,
+restoration, and its analytic count remain that contribution. The two
+source tables, interpreters and proof statements are bound in SOURCES.json.
+
+## A fixed seven-row table
+
+The following rows are prepended. All source destinations are increased by
+seven, and the fallback goto targets seven plus the source entry.
+
+```text
+0: move tape5 right
+1: branch tape5: RIGHT -> 2, ZERO -> 4, ONE -> 4, other -> 6
+2: move tape5 left
+3: halt
+4: move tape5 left
+5: goto relocated source entry
+6: reject
+```
+
+This construction receives a source table and alphabet constants only.
+It receives no runtime Q, packet, extent, payload or head position.
+Selection occurs by a physical read on tape5.
+
+A canonical positive odd Q has first bit ONE. The next symbol is RIGHT
+exactly when Q=1. In this case the executed rows are 0,1,2,3, costing
+exactly four transitions. No tape is written. Tape5 moves one step right
+and one step left, and every head therefore returns. The only visited
+position beyond the nineteen initial positions is tape5's next position,
+so W_new=20. Arbitrary payloads, descriptors and spectators are unchanged.
+This proves the required endpoint for every P,S and valid packet at Q=1.
+
+For odd Q>=3, the next symbol is ZERO or ONE. The executed prefix rows are
+0,1,4,5. These cost exactly four transitions and enter the retained program
+in its original complete configuration, after relocation. Induction on
+the old program's transitions proves that relocation preserves each tape
+operation, branch choice, halt and rejection. Thus
+
+```text
+T_new = T_old + 4          for Q>=3.
+```
+
+The prefix visits just the first two Q positions. The retained nonunit
+descriptor producer already visits those positions: it checks tape5's first
+ONE, moves right and reads the next bit before entering its general branch.
+Thus the prefix adds no visited positions to a complete valid nonunit run,
+and W_new=W_old there.
+
+## Improved complete bounds
+
+For Q>=3, V=PQS>=3, so the cited nonunit inequality gives
+
+```text
+T_new <= (1111/3)V + 4 <= (1115/3)V,
+W_new <= 24V.
+```
+
+For Q=1, V>=1, and the exact new counts give
+
+```text
+T_new = 4 <= (1115/3)V,
+W_new = 20 <= 24V.
+```
+
+Both directions therefore satisfy the displayed complete bounds for every
+valid input. The transition coefficient decreases by exactly 289/3 from
+the old tight uniform bound 468, and the sufficient visited-cell coefficient
+decreases from 49 to 24. The new bounds need not be tight. Nonunit executions
+pay four extra transitions; this is an improvement to the worst-case uniform
+envelope over the whole interface, not a claim that each invocation is cheaper.
+
+The result preserves the successful-input contract. It does not promise
+to diagnose invalid unused packets or private state in the unit branch.
+Source-to-caller legality and the remaining G20 obligations in the README
+are separate from this proof.
+
+## Implementation limits and verification choices
+
+The assembler transforms the pinned 31,873-row tables and rejects more than
+100,000 input rows. Its loops are finite table traversals with at most seven
+branch destinations per row. It neither interprets runtime descriptors nor
+introduces a new runtime loop. Each changed function is under sixty lines.
+Internal invariants use explicit checks that remain active under optimized
+Python. The suffix checker independently reverses relocation before comparing
+every row, rather than comparing the wrapper to a second call to itself.
+
+Managed Python allocation is a rule-3 deviation in the finite assembler and
+verifier. Live allocations are bounded by the authenticated fixed table,
+at most four payload bits for unit cases, 513 descriptor bits for prefix-only
+cases, and 125 payload bits for complete compositions. Each simulated run
+has at most 200,000 transitions. These verification limits do not restrict
+the mathematical input domain. The retained interpreter owns any dynamic
+simulation storage; no source runtime behavior is changed to satisfy them.
+
+Direct compilation of two authenticated interpreter sources and the local
+wrapper is a rule-8 deviation. It prevents stale bytecode from replacing
+the declared bytes, has three fixed module targets, checks fresh names,
+and removes each temporary module entry on every exit. Negative-control
+callbacks are a rule-9 deviation limited to six immediate checks with no
+retained state. Follow-on changes to these bounds or targets require
+revisiting the controls. The finite table, fixtures and execution caps
+bound allocations and all loops. Warning-strict normal and optimized
+registered replays check this scope. No static analyzer is configured for
+this isolated package; diagnostics on the two new files are run if available.
+
+No predecessor verification suite, formal proof-kernel check or independent
+human review is claimed.

research/unit-modulus-carry-bypass/README.md

@@ -0,0 +1,106 @@
+# A literal unit-modulus bypass for the G20 quarter-carry leaf
+
+**Scoped physical construction and written proof; no new kappa.** A fixed
+seven-instruction prefix lowers the complete runtime quarter-carry leaf's
+uniform bounds from **468V to 1115V/3 transitions** and from **49V to 24V
+visited cells**, where V=PQS. The new bounds are sufficient upper bounds,
+with no claim that they are optimal.
+
+For Q=1 the required rotation is the identity. The prefix physically reads
+the next symbol of the canonical Q descriptor, restores its head and halts
+in exactly four transitions. It visits exactly 20 cells under the retained
+convention that all nineteen initial head positions count. For every odd
+Q>=3 it restores the head and enters the original table after exactly four
+additional transitions. Every retained instruction is unchanged apart from
+the relocation of its finite program-counter destinations.
+
+The [proof](PROOF.md) combines this construction with Ali Romman's cited
+nonunit bounds in [PR #5849](https://github.com/CrocSwap/integer-mult-bounds/pull/5849).
+The predecessor's arithmetic, general carry implementation and all-route
+envelope are dependencies, not results re-audited here. The delivered step
+is the physical prefix and its improved uniform envelope. Earlier high-route
+callers already skip high operations at Q=1, as documented by Sagar Thakrar
+in [PR #3265](https://github.com/CrocSwap/integer-mult-bounds/pull/3265).
+No priority for that general observation is claimed.
+
+The same valid interface is retained: positive canonical P,Q,S with Q odd,
+the complete original-owner Boolean payload, a valid five-bit packet for
+-16<=k<=12, the declared blank private tapes, and arbitrary spectators.
+Both directions implement x -> x +/- k*4^-1 mod Q, preserve all descriptors
+and spectators, restore every head, and return private storage blank.
+
+## Evidence and reproduction
+
+From the repository root, run these standard-library CPython 3.12 commands:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/unit-modulus-carry-bypass/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/unit-modulus-carry-bypass/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/unit-modulus-carry-bypass
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/unit-modulus-carry-bypass --check-source-history
+```
+
+The direct verifier prints a generated JSON receipt with status
+`PASS_UNIT_MODULUS_CARRY_BYPASS`, hashes of its package and six declared
+inputs, and these enumerated checks:
+
+- 1,972 unit-modulus executions cover both directions, every valid packet,
+  and every Boolean payload for shapes (1,1,1), (1,1,4) and (2,1,2).
+  All cells and heads agree with their entry state; the exact bill is 4
+  transitions and 20 visited cells. A separate interpreter covers 58 of them.
+- Eight descriptor-only prefix fixtures, including 513-bit Q, check the
+  exact four-transition return or four-transition fallback overhead with
+  occupied spectators, in both interpreters.
+- Every fallback row in both 31,873-instruction source tables is compared
+  after independently undoing relocation.
+- Six complete nonunit compositions in both interpreters cover Q=3,5,125
+  and both directions, with a direct coordinate-gather oracle, full head
+  return and private erasure. The source's port9 fixture k=-3,Q=125 uses
+  residue 93. The new composition takes 16,694 transitions and visits 625
+  cells in either direction.
+- Six rejection controls cover each omitted descriptor-head return, an
+  altered fallback instruction, an understated transition bill, a wrong
+  tape count and an invalid entry state.
+
+The verifier writes no files. The source table, both interpreters and cited
+source statements are pinned by Git blob and SHA-256 in [SOURCES.json](SOURCES.json).
+The registered normal and optimized commands are in [VERIFY.json](VERIFY.json).
+The finite checks corroborate the proof; they do not establish its unbounded
+claims by extrapolation.
+
+## Limits
+
+Nonunit correctness and bounds are inherited from the exact retained #5849
+table and proof. This package does not repeat that predecessor's broad replay.
+The Q=1 branch assumes valid descriptors and a valid packet; it does not
+validate the unused payload, packet or private tapes. Invalid-input rejection
+behavior is outside the successful-execution contract.
+
+This is a component improvement. The complete G20 caller has not been
+installed or repriced with it. Low-cache packet formation and selection,
+whole-T staging, low-type commit, physical ROW presentation, ancestor
+stock/P3, and the full caller invoice remain open. All five framework
+assumptions retain their status. There is no selected-frontier change,
+new recursive saving, or complete multiplication theorem.
+
+## Open next questions
+
+Can a real low-cache row be joined to the supplied packet and this wrapped
+leaf in one paid physical execution? Begin with the retained port9 witness
+and include low-row selection, the homogeneous route, packet formation,
+cache erasure and low-type commit. Whole-T staging and the actual ROW caller
+map are the blockers. [TASK.json](TASK.json) records this question structurally.
+
+## Sources and credit
+
+Base canonical main is `19fdb086ea96af9a9f87936a2b888e10af4ed810`, priority
+revision 8. The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19226097)
+states this physical-leaf scope.
+
+This package was produced by Nick Petalas. Apache-2.0. Credit Ali Romman for
+#5849's complete carry leaf, physical bounds, retained interpreters and source
+envelope; David Arias for the literal machine and counter/stream macros;
+JoyboyBrian for quarter arithmetic and affine owner reuse; Sagar Thakrar for
+the earlier high-route Q=1 branch; Charles Bethin, Jose Manuel, Tekalign,
+ToikY, and the retained tape/ROW/G20 contributors for the predecessor chain.
+All retained source files and their original credit lines are unchanged.

research/unit-modulus-carry-bypass/SOURCES.json

@@ -0,0 +1,54 @@
+{
+  "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/high-route-setup-invoice/README.md",
+      "usage": "input",
+      "git_blob": "fa28cf6792d57a8a07dff64b2837f321c2369a5d",
+      "sha256": "126f252765f99dbde98c57dadfac0fdae616de34409d84af3767b83ce96a5b9f"
+    },
+    {
+      "path": "research/runtime-quarter-carry/PROOF.md",
+      "usage": "input",
+      "git_blob": "028a7777a3fc4a14dce28b555242c8e0a744b9a3",
+      "sha256": "bd51dd2ad2401fd68a4a5bfe1e4ae7009bc38f255badd6cecc4fbc7c6b905da6"
+    },
+    {
+      "path": "research/runtime-quarter-carry/README.md",
+      "usage": "input",
+      "git_blob": "d3cfcbe49fc1416dc9799d55c56f7f033f7674dc",
+      "sha256": "d02d8dab32ca6dfda95666ee7c32720b2b90cf14ada7744e0ee1adb49ad1efe6"
+    },
+    {
+      "path": "research/runtime-quarter-carry/TABLE.json.gz",
+      "usage": "input",
+      "git_blob": "f26183d28d8337863516eebfd5a48e2659b1eadc",
+      "sha256": "7222965c79faca34ad43af7e65dfb74e55b6fd0f7625658e82f9a580d5d20204"
+    },
+    {
+      "path": "research/runtime-quarter-carry/inputs/independent.py",
+      "usage": "input",
+      "git_blob": "0d93b49039465369e79075c0ad93a3d389aa7678",
+      "sha256": "82ba16fae207f2141f986c7cc5788771b6a372a34b90cab67260bc4c7effc500"
+    },
+    {
+      "path": "research/runtime-quarter-carry/inputs/machine.py",
+      "usage": "input",
+      "git_blob": "6ed03865cdb646d40573c132f841afbe335daba0",
+      "sha256": "04b7b76b9f06653d94d2158196cdd1bed7883dd1f59fcbc81a486e3ffb248681"
+    }
+  ]
+}

research/unit-modulus-carry-bypass/TASK.json

@@ -0,0 +1,92 @@
+{
+  "schema_version": 1,
+  "task_id": "bit-helper-contract",
+  "priority_revision": 8,
+  "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810",
+  "original_card": {
+    "id": "bit-helper-contract",
+    "question": "Can a changed G20 helper path or independent-target split improve the complete BIT moment without losing its physical endpoint?",
+    "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",
+      "research/g20-helper-split/README.md",
+      "research/g20-conjugation-admission/README.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 full boundary contract and paid profile; unchanged scalar counts alone are insufficient. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.",
+    "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": "First read #5679/#5708 and their audits as pending component proposals. Choose one uncovered helper group/cut on an exact word; compare arbitrary-input native action, targets, owned storage, both orientations and full signed bill. Stop if the gain is only a scalar count or repaid by lost targets. Do not rerun the frozen #5609 common-frame domain without changing its hypothesis.",
+    "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": [
+      "G20",
+      "helper split",
+      "5679",
+      "5708",
+      "independent target"
+    ],
+    "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": "A fixed unit-modulus bypass for the literal PR5849 quarter-carry leaf, preserving its valid input/output interface and improving its uniform physical transition and visited-cell bounds.",
+  "scope_change_reason": "This is a physical leaf construction rather than a changed helper split or a complete BIT moment improvement. It addresses the implementation-cost part of the current BIT contract.",
+  "bottleneck_link": "The G20 caller still needs complete physical route costs. This reduces one declared carry-leaf bound while leaving low-cache production, whole-T staging, ROW presentation, stock/P3 and the full caller invoice open.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop at the first verified original wrapper improvement; package it without optimizing the remaining nonunit program.",
+  "outcome": "completed",
+  "evidence": "PROOF.md gives the scoped construction and all-size bound; wrapper.py builds it; verify.py enumerates all declared controls and emits a hash-bound receipt.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Can the supplied quarter-code packet be formed from a real low-cache row and composed with this wrapped leaf?",
+      "why_it_matters": "The packet producer remains outside the complete G20 carry-layer contract.",
+      "first_step": "Use the PR5849 port9 k=-3,Q=125 witness; include low-row selection, homogeneous route, packet formation and low-type commit in one paid physical execution.",
+      "blocked_by": "Whole-T staging and the actual ROW caller map remain unspecified at this leaf boundary."
+    }
+  ],
+  "coordination": {
+    "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19226097",
+    "source": "PR #5849",
+    "source_author": "aliromman",
+    "upstream_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810",
+    "checked_at": "2026-10-27T19:30:00Z"
+  },
+  "verification_environment": {
+    "implementation": "CPython",
+    "python": "3.12.15",
+    "system": "Darwin",
+    "release": "27.0.0",
+    "machine": "arm64",
+    "dependencies": "standard library only"
+  }
+}