Research: metered QQ16 Gaussian axis on six bit tapes

.github/workflows/p112-common-slice.yml

@@ -15,9 +15,9 @@ jobs:
     if: github.repository == 'CrocSwap/integer-mult-bounds'
     runs-on: ubuntu-24.04
     timeout-minutes: 20
-    env:
-      TMPDIR: ${{ runner.temp }}/p112-common-slice
     steps:
+      - name: Initialise P112 work directory
+        run: echo "TMPDIR=$RUNNER_TEMP/p112-common-slice" >> "$GITHUB_ENV"
       - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1
         with:
           fetch-depth: 0

research/qq16-gaussian-axis-tapes/README.md

@@ -0,0 +1,52 @@
+# QQ16 Gaussian-axis arithmetic on six physical bit tapes
+
+**Scope:** one exactly divisible, nonuniform tensor-axis line primitive, not an F0/B1 producer or an admitted recursive supplier.
+
+The [native reference](../qq16-native-rounded-components/vendor/native.py) defines, for every coordinate `x` and its partner `y=x xor (1<<axis)`, the exact pair
+```
+r'[x] = (r[x]+r[y]+s*(i[y]-i[x]))/2
+i'[x] = (i[x]+i[y]+s*(r[x]-r[y]))/2
+```
+for `s in {-1,1}`. This package gives a literal sequential bit-tape implementation of that map, including data movement, scratch zeroing, head returns, and a cell-action invoice. It deliberately uses the *pinned source* formula rather than the rotated displayed second output noted by #3652/#3671.
+
+## Result and contract
+
+Given `N=2^n` coordinates, `n>=1`, signed two's-complement little-endian component width `W>=2`, and an axis `0<=axis<n`, the algorithm transforms two **owned, separately based** `NW`-cell data tapes. Four further owned, discardable `NW/2`-cell scratch tapes may contain arbitrary initial bits. All six tape heads start at their individual origins. Each numerator above must be even and within signed W-bit range; this is a **caller precondition**, not a condition checked non-destructively by the tape program.
+
+On successful completion the two data streams contain the exact pair transform, all scratch cells are zero, all six heads return to their origins, and the exterior cells are never accessed. A finite-state carry in `{-1,0,1,2}` and a fixed index/controller schedule suffice for each local step. The implementation has an exact counted cell-action tariff:
+
+| Tape class | READ | WRITE | MOVE | Total |
+| --- | ---: | ---: | ---: | ---: |
+| Two data tapes combined | `2NW` | `2NW` | `8NW` | `12NW` |
+| Four scratch tapes combined | `4NW` | `4NW` | `12NW` | `20NW` |
+| **Total** | **`6NW`** | **`6NW`** | **`20NW`** | **`32NW`** |
+
+In addition, the caller must supply `2NW` data bits and `2NW` cleanable owned scratch bits, and pay for obtaining the input layout, encoding, addressing/finite control, neighbouring native recipe monomials, cover maps, producer scalar instructions, restoration, F17 consumption, and recursive/tape transfers. Bit-operation counts and Gaussian rank-one child tariffs are not interchangeable. The 11,076 axis factors per layer in #3303 imply the **conditional axis-only** subtotal `354432 lambda N W` single-cell actions, *only if* every required axis step is supplied in this layout with the stated preconditions. No complete-producer physical bill is inferred.
+
+## Proof idea
+
+The packing pass streams coordinate blocks in order, separating each axis-bit lane into four half-length scratch arrays without touching external cells. For each axis block, low-lane output and high-lane output use the same input bits with opposite sign. A streamed numerator bit has `t = carry + a - s*b + c + s*d` (and the corresponding imaginary expression), `out = t mod 2`, `carry' = floor(t/2)`. The carry range is invariant since the signed sum of four bits lies in `[-1,3]` and the carry lies in `[-1,2]`. Exact divisibility makes the lowest output bit zero. Dropping that bit and sign-extending the highest one performs exact division by two on a signed W-bit numerator. The high-lane pass is the last scratch reader, so it clears every scratch cell without destroying an earlier read. All traversals are closed and contribute the counts above. The argument works for all positive n and W under the explicit range/divisibility premises, not merely the finite fixtures.
+
+## Reproduction
+
+From the repository root with Python 3.12+ and no third-party packages:
+
+```sh
+python3 -I -B research/qq16-gaussian-axis-tapes/verify.py
+python3 -I -O -B research/qq16-gaussian-axis-tapes/test_verify.py
+python3 -B scripts/research_package.py --package research/qq16-gaussian-axis-tapes
+```
+
+The first command verifies the complete published `RESULT.json`. The second runs behavioural rejecting controls. The registered command additionally validates metadata/source pins. The primary check loads and hashes the exact native source and all-depth arithmetic receipt. It checks 8,192 signed pair cases, 56 routed axis/sign cases at dimensions 2 through 128, 72 signed boundary cases at widths through 545, 18 comparisons against the actual 512-coordinate pinned native line (both signs on all nine axes), and four consecutive axis/inverse operations sharing scratch. It meters every tape cell operation. Sources are authenticated before execution. No full F0/B1/native/selected cold replay, Lean proof, hosted CI, or human review is asserted.
+
+## Relationship to predecessors
+
+Ali Romman's QQ16 construction and native/geometry lineage supply the operator. Nick Petalas' #3303 and #3270 supply the all-depth producer and factor-count envelope; #3652 (ToikY) independently checks its primitive ledger, and #3671 documents the output-turn convention. Sagar Thakrar's #3241/#3377 address different physical access boundaries, while Dugongue's #3394 prices owner-cover permutations rather than the present Gaussian coordinate primitive. The recorded missing caller and consumer in #3339 remain missing. This is a separate local implementation, not a replacement for these results. New work by Clear1nsight with substantial OpenAI ChatGPT assistance. Apache-2.0.
+
+## Open next questions
+
+1. **Actual caller layout.** Can the literal F0/B1 source establish the six separately based owned windows, the exact signed grid, and available scratch before each axis factor? First bind a specific native event to real owner/frame/tape intervals. Missing caller ownership and entrance protocol block this.
+2. **Whole-producer bill.** What physical layout transitions are required between the 11,076 axis factors, monomial permutations, cover maps and scalar steps? First price one adjacent event pair without gifting relocation or addressing. The full source and its consumer remain uncharged.
+3. **Dirty helper semantics.** Can each caller borrow helper fields whose endpoint is frame-relative rather than literal common-coordinate restoration (#3293)? First bind one named borrowed caller interface and test arbitrary nonconstant input. No full QQ16 helper restoration follows from this package.
+
+**Decision:** close this bounded local tape primitive and stop. Unknown costs are not zero, and no new `kappa` or selected-frontier change is claimed.

research/qq16-gaussian-axis-tapes/RESULT.json

@@ -0,0 +1,25 @@
+{
+  "status": "PASS_QQ16_GAUSSIAN_AXIS_TAPES",
+  "source_base": "20ecf2891d80b5acf18d980b2164fb44ea7faa90",
+  "scope": "Nonuniform six-tape axis kernel on supplied owned windows",
+  "exhaustive_scaled_signed_pair_cases": 8192,
+  "routed_cases_n1_through_n7": 56,
+  "signed_boundary_cases": 72,
+  "pinned_native_cases": 18,
+  "native_output_digest": "202a896bd27c275ba90e2a284874b74f19b6f750c6012dc07a1e0f24d8e7f175",
+  "same_scratch_composed_axes": 4,
+  "total_metered_actions": 8663040,
+  "cell_actions_per_NW": {
+    "read": 6,
+    "write": 6,
+    "move": 20,
+    "total": 32
+  },
+  "data_bits_per_NW": 2,
+  "discardable_scratch_bits_per_NW": 2,
+  "inherited_axis_factors_per_tensor_layer": 11076,
+  "conditional_axis_only_actions_per_lambda_NW": 354432,
+  "complete_producer": false,
+  "caller_layout_admitted": false,
+  "new_kappa": false
+}

research/qq16-gaussian-axis-tapes/SOURCES.json

@@ -0,0 +1,30 @@
+{
+  "schema_version": 1,
+  "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81",
+      "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "67f085acd86acd7d4e03922d9cf4b26bca66fed5",
+      "sha256": "47b42433f5a85809a3aadd29c2c339da2c6ed728e4f7762df6b88bccb7874cf0"
+    },
+    {
+      "path": "research/qq16-native-rounded-components/vendor/native.py",
+      "usage": "input",
+      "git_blob": "e1976b3a55a40206808405b99a4c443093378bef",
+      "sha256": "999eb1230798b25821de7771ecfa86381e137124059b30ccef167169d176ee8e"
+    },
+    {
+      "path": "research/qq16-all-depth-producer-grid/RESULT.json",
+      "usage": "input",
+      "git_blob": "372809009d835ce707eace8d514a667f2301b1d8",
+      "sha256": "b954ab5c5a720b21a9ab49bda2e1a0824ab184a482243d6263dab3c4bddb91bb"
+    }
+  ]
+}

research/qq16-gaussian-axis-tapes/TASK.json

@@ -0,0 +1,101 @@
+{
+  "schema_version": 1,
+  "task_id": "joint-query-controller",
+  "priority_revision": 6,
+  "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90",
+  "original_card": {
+    "id": "joint-query-controller",
+    "question": "Can a literal QQ16 producer meet the proposed completed-output error budgets with dirty helpers and an affordable physical consumer?",
+    "starting_points": [
+      "docs/research/research-family-status.md",
+      "research/joint-query/README.md",
+      "research/joint-query/evidence/QQ16-SELECTED-WITNESS.md",
+      "research/joint-query/evidence/JOINT-QUERY-TRANSFER.md",
+      "docs/research/community-efficient1000-review.md",
+      "research/qq16-producer-defect-transfer/README.md"
+    ],
+    "methods": [
+      "Derive one literal producer's completed-output defects and intermediate dirty-helper bounds, with its physical bill.",
+      "Design or audit one consumer, retention or hosting boundary and its complete cost for the pinned producer/decoder."
+    ],
+    "acceptance_gate": "Name the changed premise of the fixed F0/B1 observation obstruction. Show exactly which query is recovered, legal native reads and restoration, and a full favorable budget including cover maps, helpers and endpoints. Local inverse identities alone do not close the global controller. 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_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Read the revision-6 family record and #2965 producer-defect transfer after the local QQ16 decoder contract. Its author-checked output-error estimate does not implement producer interiors, bound dirty helpers, or pay for the consumer; independently check the implication used.",
+      "scope": "Source-bound orientation only. Read the named package and review before relying on its local evidence; this command is not its replay or supplier admission."
+    },
+    "first_experiment": "Pin one literal F0/B1 producer and its native-child contracts; derive the actual intermediate magnitude ledger and completed-output defects, including dirty helpers and correlations. Compare with #2965 budgets and price storage, movement, cleanup and F17 consumption. Stop with a precise missing bound if no producer contract supplies it; do not optimize another decoder precision constant in isolation.",
+    "bottleneck_link": "The native local words exist; retained query information and its physical access are the missing link to a composed recursive interface.",
+    "allowed_variations": [
+      "One paid query, one changed first pair, or one precisely specified affine helper state.",
+      "A counterexample or lower bound for that exact proposed repair.",
+      "One unresolved obligation of a newer local decoder, with exact source heads and a distinct claim/domain."
+    ],
+    "scope_change_triggers": [
+      "Retaining the fixed first pair and ordinary schedule while allowing only homogeneous selected-only control, already excluded by the witness.",
+      "Treating cover-map counts as zero-cost physical address operations.",
+      "Recreating the pending complete local decoder or early-record/output-bank coalescing already under investigation without a distinct audit or changed premise.",
+      "Treating a completed-output defect inequality as a producer-interior, dirty-range or physical-cost certificate."
+    ],
+    "overlap_terms": [
+      "QQ16",
+      "joint-query",
+      "changing-chart controller",
+      "selected observation",
+      "1969",
+      "2540",
+      "early record",
+      "output-bank retention",
+      "complete native decoder",
+      "2965",
+      "producer defect",
+      "dirty-helper range",
+      "F17 consumer"
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "One exact, metered six-tape Gaussian coordinate axis step on supplied owned data/scratch windows for the pinned QQ16 native reference",
+  "scope_change_reason": "The original producer+consumer card remains unsolved, while numerical producer and cover-routing packages already cover those subcontracts. This bounded physical coordinate primitive changes the object to one explicit missing tape boundary; it does not claim a complete producer or recursive cost.",
+  "bottleneck_link": "Physical scalar Gaussian execution is one unpriced ingredient between the all-depth QQ16 numeric reference and an actual caller, but further work must bind this ingredient to legal producer windows and an affordable F17 consumer.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop after exact six-tape value/cleanup/head/count verification and source-pinned controls. Do not extrapolate axis-only cell counts to a physical QQ16 producer without a charged caller and complete supplier invoice.",
+  "outcome": "partial",
+  "evidence": "Executable six-tape algorithm with 32NW metered actions, exact native-line agreement at 18 cases, 8,192 finite pairs and 12 behavioural test groups. No full producer or kappa claim.",
+  "author": "Clear1nsight",
+  "ai_assistance": "Substantial OpenAI ChatGPT assistance in derivation, code, tests, and documentation. No independent human or proof-kernel review.",
+  "open_questions": [
+    {
+      "question": "Does a literal F0/B1 native event admit the required six supplied bit-tape windows?",
+      "why_it_matters": "Local physical execution is not source admission or bounded global movement.",
+      "first_step": "Bind one selected Gaussian child to an owner/frame and explicit data/scratch tape intervals.",
+      "blocked_by": "Actual caller allocation, layout conversion, and borrowed-helper lifetime."
+    },
+    {
+      "question": "Can consecutive axis/monomial/cover events be executed at an affordable complete tariff?",
+      "why_it_matters": "Repacking and consumer costs can erase the local tariff advantage.",
+      "first_step": "Price one adjacent axis and monomial pair from literal source.",
+      "blocked_by": "Physical address/control and full F0/B1/F17 invoice."
+    },
+    {
+      "question": "Are dirty helpers restored in the caller's required coordinate frame?",
+      "why_it_matters": "Arbitrary helper return may be frame-relative, not literal numeric identity.",
+      "first_step": "Bind one caller L224 entry/exit frame, using PR3293 as calibrated test.",
+      "blocked_by": "Legal caller borrowed-state semantics and paid adapter."
+    }
+  ],
+  "selection": {
+    "method": "Explicit assigned QQ16 physical-producer task, no random reroll.",
+    "base_main": "20ecf2891d80b5acf18d980b2164fb44ea7faa90",
+    "overlap": "Consulted #3303/#3652 numeric, #3394 cover routing, #3241 physical SCALE, #3374 F17 bill and #3339 missing caller. Live title-only PR search found no identical six-tape Gaussian axis; hidden discussion coverage not complete."
+  },
+  "family_decision": {
+    "decision": "narrow and stop",
+    "proved": "Conditional per-axis signed-binary implementation under explicit divisible, nonoverflowing operands and supplied six owned windows, exact counted cell operations.",
+    "unknown": "Caller encoding/admission, layout transitions, address/control operations, physical producer aggregation, borrowed-helper semantics, F17 consumer, recursive moment and all-size transfer."
+  }
+}

research/qq16-gaussian-axis-tapes/VERIFY.json

@@ -0,0 +1,35 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/qq16-native-rounded-components/vendor/native.py",
+    "research/qq16-all-depth-producer-grid/RESULT.json"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-Werror",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 240,
+      "checks": "Hash authentic source bytes; test native operator, exact pair and routed fixture values, all tape movement/cleanup/counts and frozen result."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-Werror",
+        "-O",
+        "-B",
+        "{package}/test_verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Twelve behavioural controls including source tamper, scratch leak, missing movement invoice, malformed alias/head and invalid arithmetic domains."
+    }
+  ]
+}