Research: prove a sharp P112 mixed-rank anchor bound

research/p112-mixed-rank-anchor/CHECKS.json

@@ -0,0 +1,66 @@
+{
+  "status": "PASS_AUTHOR_CHECKED_P112_MIXED_RANK_ANCHOR",
+  "checked_at_utc": "2026-10-17T13:27:21.151324+00:00",
+  "canonical_main": "997e6a9ca7b4f95d50e366f61412fd640d72a88a",
+  "priority_revision": 6,
+  "environment": {
+    "platform": "Linux-6.6.87.2-microsoft-standard-WSL2-x86_64-with-glibc2.41",
+    "python": [
+      "3.12.15",
+      "3.13.5"
+    ],
+    "gcc": "Debian 14.2.0-19",
+    "clang": "Debian 19.1.7",
+    "python_dependencies": "standard library only"
+  },
+  "checks": [
+    {
+      "command": "python3.12 -B scripts/research_package.py --package research/p112-mixed-rank-anchor",
+      "result": "PASS_REGISTERED_RESEARCH_PACKAGE; complete scan and 14 behavioral test groups; mathematical receipt equal"
+    },
+    {
+      "command": "python3.13 -O -W error -B research/p112-mixed-rank-anchor/test_verify.py",
+      "result": "14 tests pass, including two compiled semantic/coverage mutants"
+    },
+    {
+      "command": "ruff check --select E,F,B,UP,SIM,C4,ISC,PIE,PGH,RUF research/p112-mixed-rank-anchor/verify.py research/p112-mixed-rank-anchor/test_verify.py",
+      "result": "All checks passed with Ruff 0.17.1"
+    },
+    {
+      "command": "Warnings-as-errors byte compilation to an external cache; AST function-length inspection",
+      "result": "PASS; largest new Python function is audit_census at 54 lines"
+    },
+    {
+      "command": "clang++ -std=c++17 -O2 -g -fsanitize=address,undefined -fno-omit-frame-pointer -Wall -Wextra -Wpedantic -Wconversion -Wsign-conversion -Wshadow -Werror research/p112-mixed-rank-anchor/scan.cpp -o EXTERNAL/scan; EXTERNAL/scan EXTERNAL/fixture.txt --self-test; EXTERNAL/scan EXTERNAL/fixture.txt",
+      "result": "PASS; no sanitizer finding; full census stdout byte-identical to GCC replay"
+    },
+    {
+      "command": "Compare every SOURCES.json retained_files copy with git show COMMIT:SOURCE and recorded Git blob/SHA256",
+      "result": "PASS all six exact origin-byte comparisons"
+    },
+    {
+      "command": "python3.13 -O -W error -B EXTERNAL_READ_ONLY_GIT_FREE_EXPORT/research/p112-mixed-rank-anchor/verify.py",
+      "result": "PASS; identical receipt; no Git history, checkout writes or third-party Python modules needed"
+    }
+  ],
+  "measurement": {
+    "scope": "Python 3.12 full verifier including GCC compilation and independent Python checks",
+    "wall_seconds": 7.634217109000019,
+    "maximum_child_rss_kib": 119428,
+    "test_suite_seconds": 25.243
+  },
+  "review": {
+    "kind": "Author checking, independent Python versus native oracle/rank checks and local read-only mathematical/source audit",
+    "subagent_review": "Unavailable in this session",
+    "independent_human_review": false,
+    "proof_kernel_verification": false,
+    "concurrent_PR3164": "Proof read at 857384079ab640a949fb7618b7909664d3e737e5 for overlap only, not cold-replayed; beta application is corroboration."
+  },
+  "unrun": [
+    "Other P112 C1-C7 obligations and beta cells",
+    "Full inherited TWOSIDE feasibility/filter ledger",
+    "Selected native/supplier/outer cold replay",
+    "Independent human or proof-kernel review"
+  ],
+  "publication": "Run scripts/check_research_commit.py after committing; this file does not predeclare publication-byte or hosted-CI success."
+}

research/p112-mixed-rank-anchor/CONTROL14.json

@@ -0,0 +1,109 @@
+{
+  "scope": "Counterexample to the separate-fourteen-deletion rank-five-anchor span-four relaxation, not to a common deletion or beta conjecture.",
+  "first": [
+    298398672570286131,
+    52776760246272
+  ],
+  "second": [
+    368712,
+    24234763680
+  ],
+  "anchor": {
+    "vector": [
+      0,
+      0,
+      0,
+      0,
+      1,
+      0,
+      -1,
+      0
+    ],
+    "cut": [
+      9331885590326542336,
+      10170482589700
+    ]
+  },
+  "directions": [
+    {
+      "vector": [
+        0,
+        0,
+        0,
+        0,
+        0,
+        1,
+        0,
+        -1
+      ],
+      "cut": [
+        108519598638235648,
+        7146859266058
+      ]
+    },
+    {
+      "vector": [
+        0,
+        0,
+        0,
+        0,
+        1,
+        0,
+        -1,
+        0
+      ],
+      "cut": [
+        2493515008,
+        10170501464064
+      ]
+    },
+    {
+      "vector": [
+        1,
+        1,
+        -1,
+        -1,
+        1,
+        1,
+        -1,
+        -1
+      ],
+      "cut": [
+        274928243200,
+        206162627154
+      ]
+    },
+    {
+      "vector": [
+        1,
+        1,
+        -1,
+        1,
+        1,
+        1,
+        1,
+        -1
+      ],
+      "cut": [
+        78953733651841024,
+        11003707294208
+      ]
+    },
+    {
+      "vector": [
+        1,
+        1,
+        1,
+        1,
+        1,
+        1,
+        -1,
+        -1
+      ],
+      "cut": [
+        688008463360,
+        3298555871237
+      ]
+    }
+  ]
+}

research/p112-mixed-rank-anchor/ENGINEERING.md

@@ -0,0 +1,95 @@
+# Execution and verification boundary
+
+## Exit predicate and playbook
+
+Exit when one named beta shape has a precise proof, a source-bound complete
+finite check with meaningful rejection controls, reproduction instructions and
+a focused published PR. Do not claim a supplier or exponent improvement.
+
+The autonomous local run playbook was applied as follows.
+
+1. State the exit predicate before the first iteration.
+   The predicate above narrowed the live PR3162 handoff to one beta exclusion.
+2. Choose a local wake method. Prefer an event-aware watcher for process completion or file changes. Otherwise use a bounded polling interval appropriate to the task. Use the host's recurring wake capability only when the user explicitly asks for future or repeated execution.
+   Bounded synchronous commands supplied process completion; no recurring job.
+3. Start a decision trail with `show-me-your-work` when installed. Otherwise create an append-only `decisions.tsv` with timestamp, phase, decision, reason, evidence, and result columns.
+   A session-owned external trail recorded scope, the probe, controls and checks.
+4. Each iteration makes the smallest evidence-supported change, checks the predicate, logs the result, and discards changes that did not help.
+   Retain the successful rank-four/twelve-line theorem. Do not extend it to the
+   failed rank-five/fourteen-line relaxation; retain its exact counterexample.
+5. Handle reversible local blockers within scope. Under an explicit full-autonomy grant, apply a default for a reversible user preference, explain it, and give one reply word that reverses it. Pause for missing authority, an irreversible decision, or a user-named gate.
+   Reuse the clean existing worker and branch from fetched canonical main. No
+   additional checkout, force operation or selected-record change was needed.
+6. Continue through a plateau by changing the hypothesis or measurement. Stop at the predicate or a documented dead end. Never weaken the predicate.
+   Preserve the rank-four anchor rather than dropping it to obtain a generic
+   twelve-line statement. The resulting proof excludes exactly one shape.
+   The submission overlap refresh found PR3164's different proof of both beta
+   exclusions. Preserve the distinct sharp mixed-rank theorem and label the
+   application as corroboration; do not claim a still-open-cell closure.
+
+Build the Lever produced `scan.cpp` and `verify.py` rather than a hand-checked
+claim. Prove It Works required all recorded anchor decisions and positive pairs
+to receive Python checks. Test Behavior, Not Implementation required actual CLI,
+source, cut and compiled-code mutants, not tests of copied constants alone.
+
+## Code constraints
+
+The changed execution path is `verify.py`, `scan.cpp`, and their test driver.
+The frozen vendor supplies data reconstruction, flat/orbit enumeration and the
+rank-six oracle. Its hashes are checked; it is not silently refactored.
+
+- Rules 1 and 2. No new recursion, asynchronous workers or unstructured jumps.
+  Native bounds are 112 labels, 248 directions, 120 root anchors, 511 character
+  words, 788,035 flats and 159 orbits. The anchor examines at most 4,845 bases.
+  Exhaustive controls stop at 2^20 subsets. Python's census parser consumes at
+  most 10,000 bounded output lines, advancing its cursor on every iteration.
+  Every subprocess has a timeout. Capacity failures reject, never truncate.
+- Rule 3 deviation. Python and STL allocate managed containers. Eliminating
+  that allocation would require a different runtime and rewrite frozen inputs.
+  Scope is this finite replay only. Fixed input sizes and capacities bound live
+  containers; subprocesses and temporary directories have scoped lifetimes.
+  The measured Python/GCC replay, including compilation, has maximum child RSS
+  119,428 KiB. Native sanitizer controls and the full census pass. If dimensions
+  are generalized, replace these capacities and measure memory before adoption.
+- Rule 4. Each new function is at most sixty physical lines after formatting.
+  The streaming record boundary was split into `anchor_check`, which validates
+  one anchor, and `audit_census`, which owns chronological coverage accounting.
+  Unchanged vendored routines retain their source shape and attribution.
+- Rule 5. Runtime contracts check source inventories, all-direction coverage,
+  record counts, witness cuts, field ranks and exact receipt equality. Native
+  guards remain active with optimization; Python does not rely on `assert`.
+- Rules 6 and 7. Mathematical state is local and passed explicitly. Globals are
+  immutable paths/flags. Compiler and scanner statuses are checked, and failures
+  propagate. Regular-file Path writes either complete or raise; their integer
+  return counts are intentionally unused, and generated evidence is read back.
+- Rule 8. One simple macro renames the retained standalone `main` before a fixed
+  source inclusion. There is no token construction, variadic macro, recursion
+  through callbacks or generated executable logic.
+- Rule 9. No new function pointers or nested pointer ownership. Native tables
+  and vectors have one local owner. Python imports one static vendor module;
+  its source bytes are authenticated before mathematical acceptance. This is
+  not a sandbox against concurrent hostile code replacement.
+- Rule 10. Every replay compiles with `-Wall -Wextra -Wpedantic -Wconversion
+  -Wsign-conversion -Wshadow -Werror`. Python runs with warnings as errors.
+  Local checks also run Ruff's E,F,B,UP,SIM,C4,ISC,PIE,PGH,RUF diagnostics,
+  warnings-as-errors byte compilation, and a Clang ASan/UBSan full replay.
+  No diagnostic is suppressed in source. Ruff ALL additionally reports optional
+  annotations/docstrings, unittest-versus-pytest style, domain literals,
+  namespace/CLI conventions and trusted subprocess warnings. Requiring those
+  unrelated conventions or adding a CI lint dependency is outside this isolated
+  scientific package. Revisit that policy if this code becomes shared tooling.
+
+## Review limits
+
+The independent implementation boundary is the Python anchor/span and deletion
+checks versus the C++ scanner. Flat/orbit generation and the Weyl geometry are
+credited inherited code, not a separately reimplemented proof. ASan/UBSan,
+optimized Python and negative controls are not independent human review.
+
+No internal subagent review capability was available. A local read-only audit
+checked the proof against the actual pruning inequalities, the new cutoff gap,
+empty-mask coverage, the quotient basis, and the declared source/CI boundary.
+Attention remains on the standard Weyl-chamber theorem, the finite enumerator,
+and TWOSIDE's inherited reduction hypotheses. Those dependencies do not vanish
+when this isolated result is accepted. PR3164's newly reported beta closure was
+read for overlap, not independently cold-replayed here.