Conditional accuracy: all-length cubic precision for the dirty stride inverse

.github/workflows/dirty-stride-precision.yml

@@ -0,0 +1,26 @@
+name: Dirty stride precision
+on:
+  pull_request:
+    paths:
+      - 'research/dirty-stride-precision/**'
+      - '.github/workflows/dirty-stride-precision.yml'
+  push:
+    paths:
+      - 'research/dirty-stride-precision/**'
+      - '.github/workflows/dirty-stride-precision.yml'
+  workflow_dispatch:
+permissions:
+  contents: read
+jobs:
+  verify:
+    runs-on: ubuntu-latest
+    timeout-minutes: 45
+    strategy:
+      matrix:
+        python: ['3.11', '3.14']
+    steps:
+      - uses: actions/checkout@v4
+      - uses: actions/setup-python@v5
+        with:
+          python-version: ${{ matrix.python }}
+      - run: python -I -O -B research/dirty-stride-precision/test_package.py

research/dirty-stride-precision/CHECKS.md

@@ -0,0 +1,29 @@
+# Check ownership and scope
+
+The test authoring gate was read before the new checks were added. Each
+group below protects a mathematical or package contract. No production
+hook, changed dispatcher, or runtime monkey patch was added for a check.
+
+| Owner | Contract and credible defect | Separate evidence |
+| --- | --- | --- |
+| `pins` | The proof applies to the retained word and source dependencies. A transport or word edit can invalidate that proof. | SHA256 and Git blob pins; AST comparison permits only the new admission, helper, and two read-once validation edits. Numerical faults are also tested without this binding check. |
+| `budget_checks` | Fractional, integer, preparation, and feedback inequalities must hold. A missing factor, wrong beta exponent, or omitted inverse-preimage term can understate a width. | Separate count recurrence, Euler-phi formula, and exponent inequalities. Package faults reduce the local exponent and inverse guard and must fail at these checks. |
+| `admission_checks` | Every induced exponent is between `2^k` and the original cycle length. Prepared powers must be exactly zero at the claimed cutoff. | Exact geometry enumeration, real and complex powers, rational non-dyadic margins, and all-length threshold inequalities. A false cutoff is rejected by actual nonzero coefficient output. |
+| `zero_subtrees` | The dirty tail must have the exact addition endpoint and a depth-independent magnitude bound. Endpoint equality alone is insufficient. | Actual `solve` calls with five further structural levels, both signs, two root phases, arbitrary dirty data, and peak-value observation. |
+| `leaf_checks` | Signed source-only accuracy, exact restoration, target dependence, and the unchanged tape bill must hold. A wrong restoration or expansion can break them. | A separate geometric inverse, unmodified PR985 output comparison, actual tape meters, and two target-dependent increments. |
+| `deep_admission` | A finite case beyond the old length gate must execute correctly. The new formula alone is insufficient evidence. | Full `L=5741` word, a residual bound from the Neumann inverse, exact cancellation, and complete movement count. The old public API rejects the same dimensions and width. |
+| `kernel_cases` | Tighter budgets must support the actual dirty word. A missing inner shift or wrong inverse order can corrupt output or restoration. | All ten original factor fixtures, a dense expanded-polynomial oracle, both signs from fresh states, both inverse orders, odd lowest bits, integer guards, and two physical tape heads. |
+| `uniform_kernel_cases` | The stated uniform widths must admit actual coefficient preparation and execution, not only an integer formula. | Roots are rounded to the prescribed factor width. Exact interval coefficient bounds, stable margins, norm hypotheses, dense output, and restoration are checked. |
+| `run_counted` | Literal array accesses must equal the charged reads and writes. Duplicate validation reads were present in the predecessor. | An array observer counts actual indexed accesses independently. It rejects the retained original and a duplicate-read mutation. |
+| `test_package` | The result must run without a checkout or writable source. It must detect source drift and preserve an existing output file. | Twelve faults, a full read-only relocated replay in a path with spaces, and exact receipt regeneration. |
+
+PR985's full original package remains byte-exact. Its power cases are
+reused because the powering implementation is unchanged and extinction
+depends on its norm bound. The new leaf cases own the changed admission
+and signed-error transfer. The new suite does not replay unrelated
+frontier or compiler packages. The selected-record checks protect the
+unchanged current frontier separately.
+
+The written proofs supply the all-size arguments. Finite cases cannot
+replace the return-time induction, zero-subtree induction, common-operator
+theorem, or inherited analytic and preparation hypotheses.

research/dirty-stride-precision/CLAIM.json

@@ -0,0 +1,47 @@
+{
+  "active_depth": "min(K, ceil(log2(1/beta)) + ceil(log2(W+1)))",
+  "actual_structural_recursion_unchanged": true,
+  "additional_word_size_inputs": "Immutable coefficient, margin, multiplier and unit-gauge descriptor lengths; long stride input descriptions are also paid.",
+  "base_commit": "8bddbee377e2f3ce1f1247196c4b290d55767d20",
+  "branch": "codex/s8-dirty-precision",
+  "concurrent_contributions": [
+    {
+      "contribution": "Phase lane array observer",
+      "relation": "It found two PR985 validation expressions that read twice but charge once. The derived solver caches each value once and the retained original is unchanged."
+    },
+    {
+      "contribution": "PR1025",
+      "head": "6ef2168ac90d42926bceb7ac9b2e029463800c76",
+      "relation": "It improves an analytic input and gives a clean-scratch corollary. Its proof was read for overlap. It is not a dependency. A combined dirty budget is a follow-up; see OVERLAP.md."
+    }
+  ],
+  "consumed_pr985_head": "9df42a99dd8497b6e7d46cd2507bb89071372640",
+  "fractional_bound": "W <= max(p,w_input) + m + 18*r^3",
+  "kind": "conditional accuracy theorem and exact-rational verification",
+  "length_independent_leaf_threshold": "W >= 4*ceil(log2(1/beta)) + 16",
+  "nonclaims": [
+    "new kappa",
+    "minimum working width",
+    "measured runtime gain",
+    "nonconstant site phases",
+    "new transport",
+    "all-size root factorizer",
+    "fast bit compiler",
+    "Lean proof",
+    "complete transform or multiplication reduction"
+  ],
+  "pr985_successor": {
+    "checked_utc": "2026-10-13T17:11:38.940368+00:00",
+    "head": "da1cdf8ed4ac9b1b8378dfec73f77ff4e81a4f70",
+    "relation": "Accounting-only successor reported by the coordinator. The exact consumed 9df42a predecessor remains unchanged; see OVERLAP.md."
+  },
+  "prepared_for": "Ali Romman (@aliromman)",
+  "primary_claim": "The actual constant-coefficient PR985 dirty arbitrary-stride word has an all-length sufficient admission and a cubic sufficient kernel precision bound, with exact restoration and its full two-tape bill.",
+  "review_boundary": "The coordinator reviews this local candidate before publication. No independent human review is claimed.",
+  "schema": 1,
+  "seed": null,
+  "selected_kappa_unchanged": "1661960547713947/1000000000000000000",
+  "signed_integer_reserve_bound": "I <= m + 15*r^3",
+  "source_and_dirty_restoration": "exact grid-word restoration in both signs",
+  "substantial_ai_assistance": "OpenAI Codex, assigned Astra Max lane in the eight-contribution sprint"
+}