Research: exclude P112 4^3,6^6,7 by deleting one piece

research/p112-weight-seven-deletion/CHECKS.json

@@ -0,0 +1,154 @@
+{
+  "schema": "p112-weight-seven-deletion-checks/v1",
+  "environment": {
+    "primary_python": "3.12.15 (main, Oct 14 2026, 01:05:27) [Clang 23.1.3 ]",
+    "secondary_python": "Python 3.13.5",
+    "platform": "Linux-6.6.87.2-microsoft-standard-WSL2-x86_64-with-glibc2.41",
+    "ruff": "ruff 0.17.1"
+  },
+  "scientific_source_sha256": {
+    "geometry.py": "b8ac379e41f5ad83bdb6c7f7c55129fc3d9c07801ea61591478f25d72ff0b021",
+    "obstruction.py": "6ab2507c39d46e21a168da7fb75778e40e3cf72a37480374243e69c75bae1909",
+    "verify.py": "7c370b618ca280bea29bc664b55529b57a656365d357267059bf8b19e95040c6",
+    "test_verify.py": "eb02cd02958e2fafbfe452c1d689b21522a424dcbdff3739afff87be4f2805a8",
+    "PROOF.md": "209512bc56c21a5621ab34bb1ffd4df82a093c63526bb6496730e8f66bddfe41",
+    "RESULT.json": "d0bc2126bd28187978aa17816e7a386579196fa305c87608beef3f35a96a2078",
+    "SOURCES.json": "793fd4a4428aeb146ede42e4c140e0415c80a2cf6d5df071630a139b6d81ac13",
+    "TASK.json": "aaeeef313bc9304bb3fcc6670a06765d42c6e0ee0e9f24824c0974de3d25627e",
+    "VERIFY.json": "6c120e1d288f96685cb945c4959861a321affff9bc1577065d14751789e3186f"
+  },
+  "scope": {
+    "profile": [
+      4,
+      4,
+      4,
+      6,
+      6,
+      6,
+      6,
+      6,
+      6,
+      7
+    ],
+    "intersection_lower": 6,
+    "new_profile_exclusions": 1,
+    "concurrent_PR3195_profile_counted_as_new": false,
+    "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/3156#discussioncomment-19001119"
+  },
+  "checks": [
+    {
+      "command": [
+        "python3.12",
+        "-B",
+        "scripts/research_package.py",
+        "--package",
+        "research/p112-weight-seven-deletion"
+      ],
+      "result": "PASS_REGISTERED_RESEARCH_PACKAGE outcome=partial; complete finite replay and all fifteen behavioral groups"
+    },
+    {
+      "command": [
+        "python3.12",
+        "-W",
+        "error",
+        "-B",
+        "research/p112-weight-seven-deletion/test_verify.py"
+      ],
+      "result": "PASS 15 tests"
+    },
+    {
+      "command": [
+        "ruff",
+        "check",
+        "--no-cache",
+        "--select",
+        "E,F,B,UP,C4",
+        "research/p112-weight-seven-deletion/geometry.py",
+        "research/p112-weight-seven-deletion/obstruction.py",
+        "research/p112-weight-seven-deletion/verify.py",
+        "research/p112-weight-seven-deletion/test_verify.py"
+      ],
+      "result": "All checks passed"
+    },
+    {
+      "command": [
+        "python3.12",
+        "-W",
+        "error",
+        "-m",
+        "py_compile",
+        "research/p112-weight-seven-deletion/geometry.py",
+        "research/p112-weight-seven-deletion/obstruction.py",
+        "research/p112-weight-seven-deletion/verify.py",
+        "research/p112-weight-seven-deletion/test_verify.py"
+      ],
+      "result": "PASS; bytecode redirected outside checkout"
+    }
+  ],
+  "read_only_source_export": {
+    "git_checkout": false,
+    "commands": [
+      "python3.13 -O -W error -B research/p112-weight-seven-deletion/verify.py",
+      "python3.13 -O -W error -B research/p112-weight-seven-deletion/test_verify.py"
+    ],
+    "result": "PASS identical receipt and all fifteen tests from read-only package plus sole declared input; bytecode and temporary files external"
+  },
+  "mutants": [
+    {
+      "mutation": "free_dimension",
+      "test": "test_intersection_loss_is_sharp_not_free",
+      "rejected": true,
+      "exit": 1
+    },
+    {
+      "mutation": "wrong_coordinate",
+      "test": "test_new_bound_and_losing_old_bound",
+      "rejected": true,
+      "exit": 1
+    },
+    {
+      "mutation": "nonstrict_edge",
+      "test": "test_quotient_and_root_cutoffs_are_strict",
+      "rejected": true,
+      "exit": 1
+    },
+    {
+      "mutation": "nonstrict_budget",
+      "test": "test_original_profile_is_a_strict_budget_survivor",
+      "rejected": true,
+      "exit": 1
+    }
+  ],
+  "retained_origin_checks": "All four exact retained source heads, Git blobs, SHA256 digests and raw byte comparisons pass. Concurrent PR3195 proof is pinned as historical overlap evidence, not imported at runtime.",
+  "internal_review": [
+    "Dimension lens: codimension-one deletion guarantees five, not six, surviving code dimensions; nine retained pieces give quotient dimension four.",
+    "Geometry lens: all fifteen edges have support at most 64<70, so only the inherited root/A2 classification is used; no A5 orbit census or weight-seven endpoint tariff is assumed.",
+    "Artifact lens: fixed inventory, strict support boundaries, unchanged predecessor execution and mutated input/source/output controls pass."
+  ],
+  "freshness": {
+    "upstream_commit": "997e6a9ca7b4f95d50e366f61412fd640d72a88a",
+    "priority_revision": 6,
+    "checked_at": "2026-10-17T16:43:15.740266+00:00",
+    "coverage": {
+      "open_prs": {
+        "fetched_at": "2026-10-17T16:42:45.083425+00:00",
+        "complete_pagination": true,
+        "records": 315
+      },
+      "discussions": {
+        "fetched_at": "2026-10-17T16:43:15.674823+00:00",
+        "complete_pagination": true,
+        "records": 1983
+      }
+    },
+    "warnings": [],
+    "scope": "No other exact ten-piece-profile match beyond the local package and its canonical claim; the helper does not search every code diff."
+  },
+  "limits": [
+    "Standard Weyl-chamber theorem is a written dependency, not proof-kernel verified.",
+    "Original decoder-level filters and full C1-C7 reduction are inherited, not re-proved.",
+    "No full supplier cold replay, physical construction, selected-frontier change or new kappa.",
+    "No independent human review or hosted CI result is claimed."
+  ],
+  "publication": "Post-commit raw-byte and exact committed source-export checks are reported with the PR; this record identifies the tested source bytes without a self-referential commit hash."
+}

research/p112-weight-seven-deletion/DECISIONS.tsv

@@ -0,0 +1,6 @@
+timestamp	phase	decision	reason	evidence	result
+2026-10-17T16:28:10Z	intake	reuse worker	no active owner or files	git status, ignored inventory, process cwd	clean; preexisting empty .ruff_cache preserved
+2026-10-17T16:31:58Z	selection	narrow to 5^2,6^6,7	actual weight-seven handoff; other candidates already covered	scope-probe.json; PR3169 coordinate inequality	proposed 795<=784 contradiction
+2026-10-17T16:32:38Z	proof	delete unrestricted ninth piece	intersection drops by at most one; avoids a new weight-seven edge alphabet	PR3169 inequality and quotient dimension	eight pieces give margin 11
+2026-10-17T16:39:14Z	overlap	credit concurrent PR3195 and make one bounded pivot	same original profile and deletion argument already published	PR3195 22f1479; fresh 313 PR/1982 discussion corpus	new target 4^3,6^6,7; no new count for old target
+2026-10-17T16:43:15Z	verification	accept one ten-piece exclusion	full replay and fifteen tests pass; strict and dimension mutants rejected	RESULT.json; export and diagnostic logs	795<=784; no kappa change

research/p112-weight-seven-deletion/ENGINEERING.md

@@ -0,0 +1,59 @@
+# Implementation boundaries
+
+The new entry points are `verify.py` and `test_verify.py`. Only this package
+and its declared immutable P112 input are read. A receipt may be created
+only at an exclusive external path. No selected supplier, shared verifier,
+frozen predecessor or global configuration is changed.
+
+Build the Lever shaped the choice to keep an exact rerunnable receipt rather
+than just a numerical claim. Prove It Works shaped the complete capacity
+replay, literal source binding and losing controls. The mathematical change
+is dimension deletion before the existing coordinate inequality, not a new
+abstraction or a larger search.
+
+## Power-of-ten inspection
+
+- No recursive calls, callbacks or unstructured control flow were introduced.
+  Exceptions propagate; the only output handle uses a context manager.
+- Every search has fixed bounds. Geometry has 120 roots, 112 live lines and
+  nine binary coordinates. Flat enumeration covers 3,309,747 and 788,035
+  subspaces. Endpoint checks cover `7^6` assignments. Historical profiles have
+  six weights and lengths six through ten; prior-cover tests use 210 index
+  quartets and at most 81 assignments per distinct basis.
+- Functions remain below sixty physical lines. Internal assumptions use
+  always-enabled `require` checks; the replay also runs under optimized Python.
+- State is local except fixed geometry/weight tables and package paths.
+  No code mutates those tables. Inputs have explicit size limits and
+  SHA256/semantic checks. CLI failures,
+  invalid dimensions, strict support cutoffs, changed inputs and output
+  conflicts are covered by tests. The CLI has no mutation other than optional
+  receipt creation, so no network or subprocess cleanup is needed there.
+- The one test subprocess executes the retained original fixed checker with a
+  thirty-second timeout, captures its result and propagates failure. The
+  registered runner gives each command a 120-second limit.
+- No generated code, reflection, runtime registration or indirect dispatch was
+  added to the proof path. The retained original checker is tested unchanged.
+- Local diagnostics use Python warning mode and Ruff's applicable error,
+  undefined-name, bugbear, modernization and comprehension checks. No warnings
+  are suppressed. CI uses the registered standard-library replay and tests;
+  no repository-wide lint/build configuration is changed.
+
+## Managed-runtime deviation
+
+Rule: 3, fixed allocation after initialization.
+Location: `geometry.py`, `obstruction.py`, `verify.py`, `test_verify.py`.
+Reason: Python integers, exact rational elimination and collection iteration
+allocate dynamically. Replacing them would expand this research contribution
+into a different runtime implementation.
+Scope: This finite standard-library replay only.
+Compensating control: All combinatorial domains are fixed above; a flat mask
+and histogram are processed at a time, not retained for millions of flats.
+Source input is at most two million bytes and each retained source at most
+100,000 bytes. Temporary test copies are context-managed and bounded to those
+same files. No solver, native build, service or unbounded worklist is used.
+Verification: Full replay, failure controls and a second-interpreter export.
+Follow-up: Reassess allocation and capacity if any dimension or input limit is
+made configurable. Current limits are not performance or memory benchmarks.
+
+The standard Weyl-chamber theorem, original decoder-level reduction and
+independent human/proof-kernel review remain outside executable coverage.