diff --git a/.github/workflows/p112-common-slice.yml b/.github/workflows/p112-common-slice.yml new file mode 100644 index 0000000000..b36f56bd89 --- /dev/null +++ b/.github/workflows/p112-common-slice.yml @@ -0,0 +1,39 @@ +name: P112 common-deletion slice + +on: + pull_request: + paths: + - 'research/p112-common-deletion-slice/**' + - '.github/workflows/p112-common-slice.yml' + push: + branches: [main] + paths: + - 'research/p112-common-deletion-slice/**' + - '.github/workflows/p112-common-slice.yml' + workflow_dispatch: + +permissions: + contents: read + +jobs: + exact-slice: + runs-on: ubuntu-24.04 + timeout-minutes: 20 + env: + TMPDIR: ${{ runner.temp }}/p112-common-slice + steps: + - uses: actions/checkout@v4 + - uses: actions/setup-python@v5 + with: + python-version: '3.12' + - name: Install native checker dependencies + run: | + sudo apt-get update -qq + sudo apt-get install -y --no-install-recommends g++ libboost-dev + mkdir -p "$TMPDIR" + g++ --version + python --version + - name: Replay the complete slice + run: python -B research/p112-common-deletion-slice/verify.py + - name: Run boundary and semantic controls + run: python -O -B research/p112-common-deletion-slice/test_verify.py diff --git a/research/p112-common-deletion-slice/EVIDENCE.md b/research/p112-common-deletion-slice/EVIDENCE.md new file mode 100644 index 0000000000..1e2062e282 --- /dev/null +++ b/research/p112-common-deletion-slice/EVIDENCE.md @@ -0,0 +1,116 @@ +# Evidence and verification limits + +## Established result + +At canonical baseline `997e6a9ca7b4f95d50e366f61412fd640d72a88a`, priority +revision 6, this package proves the sharp shared-deletion span four for the +literal first space in FIXTURE.json, every six-dimensional partner and all +real or complex directions. README.md gives the coverage argument. + +RESULT.json is a deterministic receipt, not a log copied from a predecessor. +It records 788,035 partner spaces, 776,806 distinct live masks, 5,680 parabolic +systems, 795,182 common-cut states and 197 nontrivial rational-rank checks. +The exact boundary trace is regenerated and independently checked on every +replay; its canonical SHA-256 is recorded in the receipt. + +## Checks performed + +The local environment was Linux x86-64 under WSL2, CPython 3.12.15 and 3.13.5, +GCC 14.2.0, with system Boost.Multiprecision headers. + +- Registered CPython 3.12 replay passes, including all fifteen behavioral + groups. The final native build uses `-std=c++17 -O3 -mpopcnt -Wall -Wextra + -Wpedantic -Wconversion -Wshadow -Werror`. +- The second six-flat enumerator agrees on every live mask and the complete + multiplicity histogram. It uses canonical least coset representatives; + the first uses RREF pivot and free-entry enumeration. +- The Python checker separately evaluates every one of the 197 nontrivial + scanner boundaries. Ascending-pivot binary ranks and Fraction elimination + agree with descending-pivot binary ranks and arbitrary-precision integer + elimination in C++. +- The literal sharpness witness has four independent directions, with + residual ranks `[7,7,7,7]`. Removing its common cut fails. Duplicate directions, + false claimed ranks, malformed deletion sets and dependent annihilators + reject rather than reporting a theorem. +- All 512 subsets of a dependent nine-vector fixture agree with exhaustive + XOR-span cardinalities. Root reconstruction, distinct labels and normal-plane + coverage have separate behavioral checks. +- Three compiled mutants reject under scanner controls: a free cut at rank + eight, a single-character cut at rank nine, and combining separate cuts + into a six-line purported common budget. Malformed scanner streams, JSON + shapes, oversized JSON and CLI inputs also reject. +- Ruff, formatting, warnings-as-errors Python compilation, package metadata + and provenance validation, and the sixteen assignment tests pass locally. +- Before the final native optimization, normal Python 3.12 and optimized + Python 3.13 full scans produced identical receipts. The final registered + replay requires that same receipt. The POPCNT optimization changes only + execution and has an explicit CPU-support guard. + +Exact replay commands, from the repository root with external TMPDIR: + +```sh +python3.12 -B scripts/research_package.py --package research/p112-common-deletion-slice +python3.13 -O -B research/p112-common-deletion-slice/verify.py +python3.12 -B tests/test_research_assignment.py +ruff check research/p112-common-deletion-slice +ruff format --check research/p112-common-deletion-slice +``` + +Two early outer command wrappers hit their wall limits. Their remaining child +scans or controls finished and were drained before further replay. Neither +wrapper is counted as a successful registered invocation. +The later registered command completed with exit zero. Temporary outputs and +compiled mutants stay outside the checkout and are disposable after publication. + +## Resource and implementation decisions + +The new scan has no recursion, global mutable state, dynamic evaluation or +unbounded search. Root geometry has 120 lines, eight simple reflections, +255 parabolic seeds, at most 4,000 members per orbit and 6,000 total systems. +The four actual orbit sizes are 1,120, 120, 3,360 and 1,080. + +Scanner capacities are explicit: 788,035 flat records, 128 separately qualifying +systems, 256 admitted normal rows, 65,536 states per pair and 4,096 nontrivial +rank records. Every capacity breach fails the run. Observed maxima are 32 +qualifying systems, 16 states per pair and 197 rank records. Python separately +bounds an emitted rank case to 120 rows. JSON/model input is at most two MiB. +Compile, scan and control subprocesses have finite timeouts. Standard sorting +and membership algorithms only operate on these bounded collections. + +The first-space cardinality filter is a necessary condition, not a changed +acceptance gate. A partner contributes at most 20 live labels, so a system with +more than `20+36+4` residual lines after the first space cannot qualify. The +independent flat enumeration checks this 20-line premise before the scan. + +Power-of-Ten rule 3 deviation: Python's managed runtime, C++ standard containers +and Boost integer arithmetic allocate during computation. They cannot meet a +literal allocation-free steady phase without replacing these language/library +facilities. The finite capacities above bound collection growth; rank arithmetic +has dimension eight and input entries bounded by 64. The Euclidean loop has a +4,096-step fail-closed cap. Compensating controls exercise malformed boundaries, +rank identities and input-size exhaustion. Any extension beyond this finite +model must reassess the capacities and memory use. + +Rules 8 and 9 use the language's normal fixed-target standard-library algorithms, +not generated code or an extensible callback registry. Their comparator and +predicate targets are visible lambdas over bounded vectors. The only platform +extension is the documented fixed-width `unsigned __int128`, plus the guarded +x86-64 POPCNT instruction. No source files are rewritten by the native build. + +Build the lever shaped the result into a rerunnable complete slice checker +rather than a failed search report. Prove it works required literal boundary +replays and independent arithmetic at every nontrivial rank decision. These +checks do not make the whole search engine an independently reimplemented proof. + +## Not established + +No full C5 census, orbit-representative coverage for other first spaces, +uniform exclusion of normal planes, decoder construction, supplier admission, +selected-frontier update, native outer compiler replay or multiplication +theorem is claimed. Concurrent PR3161 now reports closure of the historical +b=5 application by a different global rank-six theorem. This rank-seven slice +is not claimed as another new exclusion for that cell. The package reuses +PR3160 geometry with explicit attribution; +there is no independent human or proof-kernel review. Historical provenance +hashes were compared locally, but standalone replay does not fetch pending PR +heads. Hosted CI and maintainer review are separate from the local evidence. diff --git a/research/p112-common-deletion-slice/FIXTURE.json b/research/p112-common-deletion-slice/FIXTURE.json new file mode 100644 index 0000000000..5014d36454 --- /dev/null +++ b/research/p112-common-deletion-slice/FIXTURE.json @@ -0,0 +1,14 @@ +{ + "schema": "p112-common-slice/v1", + "omitted_frame": [ + [0, 0, 0, 0, 0, 0, 2, -2], + [0, 0, 0, 0, 0, 0, 2, 2], + [0, 0, 0, 0, 2, -2, 0, 0], + [0, 0, 0, 0, 2, 2, 0, 0], + [0, 0, 2, -2, 0, 0, 0, 0], + [0, 0, 2, 2, 0, 0, 0, 0], + [2, -2, 0, 0, 0, 0, 0, 0], + [2, 2, 0, 0, 0, 0, 0, 0] + ], + "V1_basis": [436, 6, 66, 138, 2, 57] +} diff --git a/research/p112-common-deletion-slice/README.md b/research/p112-common-deletion-slice/README.md new file mode 100644 index 0000000000..88b483aebb --- /dev/null +++ b/research/p112-common-deletion-slice/README.md @@ -0,0 +1,188 @@ +# One complete common-deletion slice of C5 + +Fix the P112 root frame and six-dimensional binary label space `V1` in +[FIXTURE.json](FIXTURE.json). For **every** six-dimensional `V2` in `F2^9` +and every common set `P` of at most four live root lines, put + +```text +X = Lambda(V1) union Lambda(V2) union P +H(X) = {h : binary_rank(labels(Off(h) minus X)) <= 7}. +``` + +**Result.** The sharp maximum of `dim span H(X)` is **four**, over either the +real or complex numbers. This completes one first-space slice of the +[C5 handoff](https://github.com/CrocSwap/integer-mult-bounds/discussions/3156). +It does not settle the other first spaces, C5, the full decoder-cost conjecture, +or a multiplication exponent. The selected frontier is unchanged. + +[PR3160](https://github.com/CrocSwap/integer-mult-bounds/pull/3160) fixed **both** +spaces and proved sharp span three. Here only its first space is fixed; all +788,035 partner spaces are covered. The shared four-line budget is essential. +No direction gets its own deletion set. + +Concurrent [PR3161](https://github.com/CrocSwap/integer-mult-bounds/pull/3161), +head `a1aba8389b87412e6f72ccf4d11f31e0ea232327`, now reports a global rank-six, +eight-deletion result and closure of the historical `(5,3)` beta cell. That +moves the original application forward; this package does not claim another +missing implication for that cell. Its new result is the sharp **rank-seven**, +common-four-deletion first-space slice, a different statement not implied by +the reported rank-six bound. This also supplies a complete calibration slice +for a future all-first-space rank-seven computation. The PR3161 theorem and +its newer follow-ups were not independently replayed here. + +## Proof and exact computation + +The executable certificate follows these implications. The written argument is +part of the result, not a claim of proof-kernel verification. + +1. **Bound the possible orthogonality systems.** Independently enumerate all + 43,435 seven-dimensional binary spaces, obtaining a maximum of 36 live + labels. The scanner enumerates all six-dimensional spaces and obtains a + maximum of 20. Thus every admitted direction has + `|Off(h)| <= 20 + 20 + 4 + 36 = 80`, and at least 32 live roots orthogonal + to it. +2. **Cover all directions, including planes.** The E8 Weyl group is finite + because it permutes the spanning root set. Choose `rho` with strictly + positive simple-root pairings. A maximum of `rho dot w(h)` moves any real + direction into the closed dominant chamber. Otherwise reflecting a negative + simple pairing increases the maximum. There a positive root is orthogonal + exactly when its simple support is contained in the zero simple pairings. + Consequently every orthogonality system is a Weyl translate of a proper + parabolic subsystem. + + Check all 255 proper simple-support subsets. Those with at least 32 root + lines give four orbits, with sizes 1,120, 120, 3,360 and 1,080. All their + live intersections have size at least 32. There are 4,560 rank-seven systems + and **1,120 rank-six systems**. The latter have two-dimensional normal + spaces. For each system the model uses the union of the nonzero supports + of an exact integral normal basis. This is the generic support in that + space. If it qualifies, every vector in the normal space qualifies by + monotonicity. An exceptional vector has additional orthogonal roots and + occurs under its own parabolic system. No catalogue-only or root-only + restriction remains. +3. **Enumerate every partner space.** Every three-dimensional annihilator has + a unique reduced row-echelon matrix. Enumerating its pivots and free entries + covers 788,035 six-dimensional kernels. Their live-label masks have 776,806 + distinct values. Merging equal masks is sound because `H(X)` depends only + on these live intersections. A second implementation, using successive + least coset representatives instead of RREF, checks the full mask list + and the multiplicity histogram. +4. **Find all relevant cuts.** A residual label set has rank at most nine. + Rank at most seven needs no cut. At rank eight, a cut lowers the rank to + seven exactly when it contains the nonzero support of a restricted binary + character. At rank nine, it must contain the union of two distinct nonzero + restricted character supports. The restriction map is injective in this + case, so the two characters are independent. Enumerating all 512 characters + and all relevant pairs therefore covers every cut of size at most four. +5. **Preserve one common set.** Start with the empty cut, and successively + retain each old state or its union with a cut option for one system, only + when the union has at most four lines. For any actual `P`, select one cut + contained in `P` for each system it admits. Their union is a generated state, + is contained in `P`, and admits exactly the same systems. Hence it suffices + to check these states, without enumerating irrelevant supersets of `P`. +6. **Check the span.** There are 795,182 states across all partner masks, at + most 16 per pair. At most 32 orthogonality systems qualify separately; no + normal plane qualifies. Each admitted list with no more vectors than the + running maximum has that immediate dimension upper bound. The remaining + 197 cases use arbitrary-precision integer elimination. The Python checker + separately interprets every one of those boundaries, recomputes its + residual binary ranks and checks its rational rank using `Fraction`. + The maximum is four. [RESULT.json](RESULT.json) records the exact receipt. + +For complex `h = a + ib`, a generic real combination of `a` and `b` has the +same zero pairings on the finite root set. Both components lie in the normal +space of that system. The computation includes its entire complex normal +space whenever its generic support qualifies. Rational basis ranks are the +same over `R` and `C`, so the same upper bound follows. + +## Sharpness witness + +One partner is the common kernel of binary characters `195, 8, 160`. +The common deletion labels are `{297, 299, 361, 363}`. Four independent directions +are the rows of + +```text + 1 -1 0 0 0 0 0 0 + 1 -1 1 1 1 1 -1 1 + 1 -1 1 1 -1 -1 -1 1 + 1 -1 1 -1 1 1 1 1 +``` + +Their four residual binary ranks are all seven. Removing the common deletion +set invalidates this fixture. The checker independently reconstructs these +claims from the literal roots and labels. + +## Reproduction + +The tested environment is Linux x86-64, CPython 3.12.15, GCC 14.2.0 and +Boost.Multiprecision headers. Python has no third-party dependencies. GCC or +Clang must support `unsigned __int128`. The optimized scanner requires x86-64 +POPCNT and rejects an unsupported CPU before scanning. This is not a native +Windows package. The dedicated workflow installs the compiler and Boost headers +on Ubuntu. + +From the repository root, with an existing external scratch directory: + +```sh +export TMPDIR="$RUN/tmp" +mkdir -p "$TMPDIR" +python3.12 -B scripts/research_package.py --package research/p112-common-deletion-slice +``` + +The registered commands run the complete scan and fifteen behavioral groups. +Direct commands also work in a Git-free export: + +```sh +python3.12 -B research/p112-common-deletion-slice/verify.py --output "$RUN/replay.json" +python3.12 -O -B research/p112-common-deletion-slice/test_verify.py +``` + +Expected marker: + +```text +PASS_P112_COMMON_SLICE flats=788035 masks=776806 systems=5680 common_span=4 +``` + +Builds and temporary exports go under `TMPDIR` and are removed on exit. The +verifier does not regenerate committed files. `--bootstrap` still runs every +mathematical check but skips comparison with a prior receipt; it is only for +explicit receipt generation. [EVIDENCE.md](EVIDENCE.md) lists checks, resource +bounds and remaining verification limits. + +## Open next questions + +- Can the same shared-cut calculation cover the other first-space orbits? + That would complete the stronger rank-seven relaxation. First identify a + remaining caller that needs it, then bind the representative list and its + frame-preserving action to these labels before scheduling disjoint slices. + Their coverage, total cost and present application are not certified here. +- Can the absence of qualifying normal planes be proved uniformly in `V1`? + That could remove an entire continuous family from later slices. Start + with the rank-six parabolic orbit and its exact character cuts. This slice + alone gives no uniform exclusion. + +## Sources and credit + +DreamingOfClouds's [PR3154](https://github.com/CrocSwap/integer-mult-bounds/pull/3154), +head `708f0ad8928c383de8294aea3c126e9461d2066d`, supplies C5, FINITE/FINITE2, +the TWOSIDE application and the retained decoder-floor lineage. Its two +implementations establish the earlier `p=2` result, not this common-`p=4` slice. + +Nick Petalas's [PR3158](https://github.com/CrocSwap/integer-mult-bounds/pull/3158), +head `8e2167bac550bd653bb74c50c1f7c3f14b6c1f70`, supplies the literal first +space and frame through the quantifier fixture. His +[PR3160](https://github.com/CrocSwap/integer-mult-bounds/pull/3160), head +`9ab8c4cc2aed4a87293d7d04b2abfdf854ae43e2`, supplies the geometry implementation +adapted here. This successor lowers its orthogonality cutoff from 40 to 32 and +retains normal planes. The new scanner imports neither FINITE implementation +nor their direction tables. + +[SOURCES.json](SOURCES.json) records exact historical blobs and hashes. +Historical source heads are provenance, not runtime dependencies; the standalone +checker cannot authenticate those remote commits without Git objects or network +access. Local source comparisons were performed before publication. + +Canonical baseline is `997e6a9ca7b4f95d50e366f61412fd640d72a88a`, priority +revision 6. Apache-2.0. Development and internal checking used substantial +automated assistance. This is author-checked finite evidence, not independent +human review, supplier admission or a full multiplication theorem. diff --git a/research/p112-common-deletion-slice/RESULT.json b/research/p112-common-deletion-slice/RESULT.json new file mode 100644 index 0000000000..b8d2cecb75 --- /dev/null +++ b/research/p112-common-deletion-slice/RESULT.json @@ -0,0 +1,174 @@ +{ + "V1_live_labels": [ + 257, + 261, + 312, + 314, + 316, + 318, + 323, + 327, + 376, + 378, + 380, + 382, + 393, + 395, + 434, + 436, + 457, + 459, + 496, + 502 + ], + "independent_rank_trace": { + "cases": 197, + "maximum_residual_rank": 7, + "sha256": "a31f31f5655ad5b6f7b2f55ddb0ff6fc9136023261b99f8b4db0bdb61c628c70" + }, + "independent_witness_check": { + "rational_span": 4, + "residual_ranks": [ + 7, + 7, + 7, + 7 + ] + }, + "model_sha256": "167b66b99772e93ed98745b904baa0b1bb64b093b0c6a63aea9b6e6a662e4891", + "normal_dimensions": { + "1": 4560, + "2": 1120 + }, + "parabolic_orbits": [ + { + "full_root_lines": 36, + "live_intersection_histogram": { + "32": 224, + "34": 896 + }, + "orbit_size": 1120, + "seed_zero_set": 63, + "simple_rank": 6 + }, + { + "full_root_lines": 63, + "live_intersection_histogram": { + "56": 8, + "59": 112 + }, + "orbit_size": 120, + "seed_zero_set": 127, + "simple_rank": 7 + }, + { + "full_root_lines": 37, + "live_intersection_histogram": { + "32": 224, + "33": 448, + "35": 2688 + }, + "orbit_size": 3360, + "seed_zero_set": 191, + "simple_rank": 7 + }, + { + "full_root_lines": 42, + "live_intersection_histogram": { + "36": 56, + "39": 896, + "42": 128 + }, + "orbit_size": 1080, + "seed_zero_set": 254, + "simple_rank": 7 + } + ], + "scan": { + "all_flats": 788035, + "distinct_live_masks": 776806, + "exact_rank_checks": 197, + "maximum_common_span": 4, + "maximum_qualified_systems": 32, + "maximum_states_per_pair": 16, + "qualified_plane_occurrences": 0, + "six_flat_size_histogram": { + "0": 10796, + "10": 56448, + "11": 86016, + "12": 124040, + "14": 131712, + "15": 143360, + "16": 141491, + "18": 33152, + "19": 28672, + "20": 19152, + "4": 56, + "6": 896, + "7": 4096, + "8": 8148 + }, + "states_checked": 795182, + "witness": { + "V2_annihilator": [ + 195, + 8, + 160 + ], + "deleted_labels": [ + 299, + 363, + 361, + 297 + ], + "directions": [ + [ + 1, + -1, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + 1, + -1, + 1, + 1, + 1, + 1, + -1, + 1 + ], + [ + 1, + -1, + 1, + 1, + -1, + -1, + -1, + 1 + ], + [ + 1, + -1, + 1, + -1, + 1, + 1, + 1, + 1 + ] + ], + "rank": 4 + } + }, + "schema": "p112-common-slice-result/v1", + "seven_flat_cap": { + "flats": 43435, + "maximum_lines": 36 + } +} diff --git a/research/p112-common-deletion-slice/SOURCES.json b/research/p112-common-deletion-slice/SOURCES.json new file mode 100644 index 0000000000..a1a70c8d54 --- /dev/null +++ b/research/p112-common-deletion-slice/SOURCES.json @@ -0,0 +1,80 @@ +{ + "schema_version": 1, + "base_commit": "997e6a9ca7b4f95d50e366f61412fd640d72a88a", + "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" + } + ], + "fixture_sha256": "2d8f2cc7bbf02d24d955f43a4880d0225b2cb0e54dce4fe5dcb34ec131649907", + "predecessors": [ + { + "pr": 3154, + "head": "708f0ad8928c383de8294aea3c126e9461d2066d", + "path": "research/p112-reduction-to-conjectures/CONJECTURES.md", + "git_blob": "4d41043842b30f4f741caf198f72d2920b70d382", + "sha256": "998a97f29bffbf4d2cfa8a0f36f4ce1e2759d992b1158b794cce58cabd796791", + "usage": "historical provenance; not a runtime dependency" + }, + { + "pr": 3154, + "head": "708f0ad8928c383de8294aea3c126e9461d2066d", + "path": "research/p112-reduction-to-conjectures/checks/TWOSIDE/NOTES.md", + "git_blob": "e3fd3f2b1dfd77b597f000b38ec2dbec3dbca931", + "sha256": "226cd59ccc6bc065319e5e4c4768c889206169ff58f74ef4053eeadc5b2e03c8", + "usage": "historical provenance; not a runtime dependency" + }, + { + "pr": 3154, + "head": "708f0ad8928c383de8294aea3c126e9461d2066d", + "path": "research/p112-reduction-to-conjectures/checks/FINITE/NOTES.md", + "git_blob": "afbb86f136ff79d238bb3c38d58e7ea9b35845ac", + "sha256": "d31b2a79a547d7159ce30fea3424c782771e3d786000bf7309301bd8619b06f4", + "usage": "historical provenance; not a runtime dependency" + }, + { + "pr": 3160, + "head": "9ab8c4cc2aed4a87293d7d04b2abfdf854ae43e2", + "path": "research/p112-common-deletion-span/geometry.py", + "git_blob": "c0adb4d03df29c9cd84f0544667652eb277374ee", + "sha256": "09e046a32de65282c11b99aa1fdff4494ed85967ae8fbcfe833858cfa1425d54", + "usage": "historical provenance; not a runtime dependency" + }, + { + "pr": 3160, + "head": "9ab8c4cc2aed4a87293d7d04b2abfdf854ae43e2", + "path": "research/p112-common-deletion-span/FIXTURE.json", + "git_blob": "7e0e3587079b0cce7a2da85b6ffb6f1de6408c7b", + "sha256": "b8f4f2587a7ec17cc67acc97f22714e520e20620fc7d992465d855ede6d506a9", + "usage": "historical provenance; not a runtime dependency" + } + ], + "parallel_work": { + "pr": 3161, + "head": "a1aba8389b87412e6f72ccf4d11f31e0ea232327", + "status": "Author-reported global rank-six/eight-deletion result and historical (5,3) beta closure; not replayed here. Distinct from this rank-seven/common-four-deletion slice." + }, + "fixture_extraction": "Copies omitted_frame and V1_basis from PR3160 FIXTURE.json verbatim; changes schema and drops the fixed V2.", + "upstream_checkpoint": { + "commit": "997e6a9ca7b4f95d50e366f61412fd640d72a88a", + "priority_revision": 6, + "checked_utc": "2026-10-17T12:54:39Z" + }, + "overlap_checkpoint": { + "checked_utc": "2026-10-17T12:54:39Z", + "open_pr_records": 282, + "discussion_records": 1927, + "complete_pagination": true, + "nearest_overlap": [3154, 3158, 3160, 3161], + "novelty_limit": "Titles, bodies, comments, local notes and ledger, not every code diff. Prior packages fix both spaces or use per-direction relaxations; this package keeps one first space and covers all partners with common cuts." + } +} diff --git a/research/p112-common-deletion-slice/TASK.json b/research/p112-common-deletion-slice/TASK.json new file mode 100644 index 0000000000..bb9d9d4c7b --- /dev/null +++ b/research/p112-common-deletion-slice/TASK.json @@ -0,0 +1,66 @@ +{ + "schema_version": 1, + "task_id": "formal-interface-lemma", + "priority_revision": 6, + "base_commit": "997e6a9ca7b4f95d50e366f61412fd640d72a88a", + "original_card": { + "id": "formal-interface-lemma", + "question": "Can one small, precisely scoped interface lemma be formalized with its actual hypotheses?", + "starting_points": [ + "certificates/selected-result.json", + "research/hyperplane-end-lean/PROOF.md" + ], + "methods": [ + "Formalize a missing boundary lemma identified by the selected review.", + "Audit a formal theorem-to-certificate binding independently." + ], + "acceptance_gate": "State the exact formalized proposition and remaining assumptions; avoid duplicate arithmetic formalizations already present.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read the exact hypotheses in the hyperplane-end proof and distinguish Lean theorems from finite supplier assumptions.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "State one missing boundary lemma in full before starting a proof-assistant build.", + "bottleneck_link": "A missing interface proof can reduce the conditional gap even if it does not change kappa.", + "allowed_variations": [ + "Narrow to one formal lemma or one theorem-to-certificate binding." + ], + "scope_change_triggers": [ + "Formalizing already-covered arithmetic and claiming the full multiplication theorem." + ], + "overlap_terms": [ + "hyperplane end", + "formal interface", + "Lean binding" + ] + }, + "scope_status": "changed", + "actual_scope": "C5 handoff: fix PR3160's first six-dimensional P112 label space and certify the sharp common-four-deletion span over every six-dimensional partner and all real or complex directions.", + "scope_change_reason": "Took the live Discussion3156 geometry handoff before drawing a task. This is an exact computational lemma, not a Lean formalization of the catalogue interface card. After a bounded unsuccessful witness search, complete one shared-cut slice rather than claim a global exclusion.", + "bottleneck_link": "The C5 decoder-floor handoff motivated this rank-seven/common-four-deletion slice. Concurrent PR3161 now reports closure of the historical b=5 application through a different global rank-six/eight-deletion theorem. This result remains a sharp rank-seven calibration slice, not a new missing implication for that closed cell or a kappa improvement.", + "budget_minutes": 60, + "stop_rule": "Stop at a literal common-set rank-five witness or a useful complete first-space slice; reserve the final quarter for verification and publication. Do not expand into a full orbit census.", + "outcome": "completed", + "evidence": "All 788035 partner spaces, 776806 distinct live masks, 5680 parabolic systems and 795182 common-cut states; sharp span four. Independent flat enumeration and 197 rational-rank/boundary checks; RESULT.json and EVIDENCE.md.", + "author": "Nick Petalas", + "ai_assistance": "Development and internal checking used substantial automated assistance; no independent human review is claimed.", + "open_questions": [ + { + "question": "Does the same shared-cut span bound hold for the remaining first-space orbits?", + "why_it_matters": "A uniform rank-seven relaxation needs all first spaces. A remaining caller requiring that stronger relaxation must be identified before expanding beyond the reported rank-six cell closures.", + "first_step": "Bind the predecessor representative list and frame-preserving action to these labels, then schedule bounded disjoint slices.", + "blocked_by": "The other representatives, their coverage and total replay budget have not been certified here." + }, + { + "question": "Can qualifying normal planes be excluded uniformly in the first space?", + "why_it_matters": "A uniform exclusion could remove the continuous E6 family from future scans.", + "first_step": "Analyze the rank-six parabolic orbit and its exact character cuts with both six-dimensional spaces variable.", + "blocked_by": "This slice's zero plane occurrences are not a proof for other first spaces." + } + ] +} diff --git a/research/p112-common-deletion-slice/VERIFY.json b/research/p112-common-deletion-slice/VERIFY.json new file mode 100644 index 0000000000..af96766db6 --- /dev/null +++ b/research/p112-common-deletion-slice/VERIFY.json @@ -0,0 +1,23 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 600, + "checks": "All partner spaces and common cuts, full parabolic direction coverage, independent flat enumeration, 197 independent rational-rank/boundary checks and sharpness witness. Requires g++ and Boost.Multiprecision headers; the dedicated workflow installs them." + }, + { + "argv": ["{python}", "-O", "-B", "{package}/test_verify.py"], + "timeout_seconds": 300, + "checks": "Fifteen behavioral groups, including malformed boundaries, deletion quantifier controls and three compiled semantic mutants." + } + ] +} diff --git a/research/p112-common-deletion-slice/geometry.py b/research/p112-common-deletion-slice/geometry.py new file mode 100644 index 0000000000..c642dea747 --- /dev/null +++ b/research/p112-common-deletion-slice/geometry.py @@ -0,0 +1,209 @@ +"""E8 geometry adapted from Nick Petalas's PR3160, Apache-2.0. + +This successor expands the parabolic cutoff from 40 to 32 orthogonal lines +and retains two-dimensional normal spaces as well as individual directions. +""" + +from fractions import Fraction +from itertools import combinations, product +from math import gcd, lcm + +SIMPLE = ( + (1, -1, -1, -1, -1, -1, -1, 1), + (2, 2, 0, 0, 0, 0, 0, 0), + (-2, 2, 0, 0, 0, 0, 0, 0), + (0, -2, 2, 0, 0, 0, 0, 0), + (0, 0, -2, 2, 0, 0, 0, 0), + (0, 0, 0, -2, 2, 0, 0, 0), + (0, 0, 0, 0, -2, 2, 0, 0), + (0, 0, 0, 0, 0, -2, 2, 0), +) + + +def require(condition: bool, message: str) -> None: + if not condition: + raise ValueError(message) + + +def dot(a: tuple[int, ...], b: tuple[int, ...]) -> int: + assert len(a) == len(b) == 8 + return sum(a[j] * b[j] for j in range(8)) + + +def canonical(vector: tuple[int, ...]) -> tuple[int, ...]: + assert len(vector) == 8 and any(vector) + divisor = gcd(*vector) + if next(x for x in vector if x) < 0: + divisor = -divisor + return tuple(x // divisor for x in vector) + + +def roots() -> tuple[tuple[int, ...], ...]: + """Doubled E8 root lines, with first nonzero coordinate positive.""" + result = [] + for i, j in combinations(range(8), 2): + for sign in (-2, 2): + row = [0] * 8 + row[i], row[j] = 2, sign + result.append(tuple(row)) + for tail in product((-1, 1), repeat=7): + row = (1,) + tail + if sum(x < 0 for x in row) % 2 == 0: + result.append(row) + assert len(result) == len(set(result)) == 120 + assert all(dot(row, row) == 8 for row in result) + return tuple(sorted(result)) + + +def coordinates(row: tuple[int, ...]) -> tuple[int, ...]: + """Solve the triangular Bourbaki simple-root equations over the integers.""" + c = [0] * 8 + c[0] = row[7] + c[7] = (row[6] + c[0]) // 2 + for j in range(6, 2, -1): + c[j] = (row[j - 1] + c[0]) // 2 + c[j + 1] + c[1] = (row[0] + row[1] + 2 * c[3]) // 4 + c[2] = (-row[0] + row[1] + 2 * c[0] + 2 * c[3]) // 4 + require( + all(sum(c[i] * SIMPLE[i][j] for i in range(8)) == row[j] for j in range(8)), + "simple-root reconstruction failed", + ) + require(min(c) >= 0 or max(c) <= 0, "root has mixed simple-coordinate signs") + return tuple(c) + + +def label(row: tuple[int, ...]) -> int: + return 256 + sum((x % 2) << j for j, x in enumerate(coordinates(row))) + + +def reflection_permutations(lines: tuple[tuple[int, ...], ...]) -> list[list[int]]: + lookup = {row: i for i, row in enumerate(lines)} + permutations = [] + for alpha in SIMPLE: + permutation = [] + for row in lines: + pairing = dot(alpha, row) + require(pairing % 4 == 0, "nonintegral root reflection") + reflected = tuple(row[j] - pairing // 4 * alpha[j] for j in range(8)) + if next(x for x in reflected if x) < 0: + reflected = tuple(-x for x in reflected) + require(reflected in lookup, "reflection left the E8 roots") + permutation.append(lookup[reflected]) + require(sorted(permutation) == list(range(120)), "reflection is not bijective") + require( + all(permutation[permutation[i]] == i for i in range(120)), "not involutive" + ) + permutations.append(permutation) + return permutations + + +def permute(mask: int, permutation: list[int]) -> int: + assert 0 <= mask < 1 << 120 and len(permutation) == 120 + result = 0 + for _ in range(120): + if not mask: + break + bit = mask & -mask + result |= 1 << permutation[bit.bit_length() - 1] + mask ^= bit + assert mask == 0 + return result + + +def orbit(seed: int, permutations: list[list[int]]) -> set[int]: + """Breadth-first closure with a hard 4,000-state capacity.""" + queue = [seed] + seen = {seed} + for cursor in range(4000): + if cursor == len(queue): + return seen + for permutation in permutations: + image = permute(queue[cursor], permutation) + if image not in seen: + require(len(queue) < 4000, "Weyl orbit exceeded capacity") + seen.add(image) + queue.append(image) + # Exactly 4,000 states also close: every queued state was processed. + return seen + + +def orthogonality_systems(lines: tuple, live: int) -> tuple[list[int], list[dict]]: + """All Weyl translates of proper parabolics with at least 32 root lines.""" + supports = [ + sum(1 << j for j, c in enumerate(coordinates(row)) if c) for row in lines + ] + permutations = reflection_permutations(lines) + seen: set[int] = set() + candidates = [] + reports = [] + for zero_set in range(255): + seed = sum( + 1 << i for i, support in enumerate(supports) if not support & ~zero_set + ) + if seed.bit_count() < 32 or seed in seen: + continue + family = orbit(seed, permutations) + require(len(seen | family) <= 6000, "parabolic inventory exceeded capacity") + seen |= family + histogram = {} + for member in family: + count = (member & live).bit_count() + histogram[count] = histogram.get(count, 0) + 1 + if count >= 32: + candidates.append(member) + reports.append( + { + "seed_zero_set": zero_set, + "simple_rank": zero_set.bit_count(), + "full_root_lines": seed.bit_count(), + "orbit_size": len(family), + "live_intersection_histogram": { + str(k): histogram[k] for k in sorted(histogram) + }, + } + ) + require(len(candidates) == len(set(candidates)), "overlapping parabolic orbits") + return sorted(candidates), reports + + +def echelon(rows: list[tuple[int, ...]]) -> dict[int, list[Fraction]]: + assert len(rows) <= 120 and all(len(row) == 8 for row in rows) + basis: dict[int, list[Fraction]] = {} + for row in rows: + vector = list(map(Fraction, row)) + for pivot, old in sorted(basis.items()): + factor = vector[pivot] + vector = [vector[j] - factor * old[j] for j in range(8)] + pivot = next((j for j in range(8) if vector[j]), None) + if pivot is not None: + scale = vector[pivot] + basis[pivot] = [x / scale for x in vector] + return basis + + +def normals(lines: tuple, mask: int) -> tuple[tuple[int, ...], ...]: + """Return an exact primitive integral basis of a normal line or plane.""" + rows = [lines[i] for i in range(120) if mask >> i & 1] + basis = echelon(rows) + require(len(basis) in (6, 7), "unexpected parabolic rank") + result = [] + for free in range(8): + if free in basis: + continue + vector = [Fraction(0)] * 8 + vector[free] = Fraction(1) + for pivot, row in sorted(basis.items(), reverse=True): + vector[pivot] = -sum(row[j] * vector[j] for j in range(pivot + 1, 8)) + denominator = lcm(*(x.denominator for x in vector)) + result.append(canonical(tuple(int(x * denominator) for x in vector))) + require( + sum( + 1 << i + for i, row in enumerate(lines) + if all(dot(row, vector) == 0 for vector in result) + ) + == mask, + "normal space has a different orthogonality system", + ) + require(len(echelon(result)) == len(result), "dependent normal basis") + return tuple(result) diff --git a/research/p112-common-deletion-slice/scan.cpp b/research/p112-common-deletion-slice/scan.cpp new file mode 100644 index 0000000000..caa56795bd --- /dev/null +++ b/research/p112-common-deletion-slice/scan.cpp @@ -0,0 +1,464 @@ +// Exact, bounded C5 slice. Nick Petalas. Apache-2.0. +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include + +// GCC and Clang provide this fixed-width integer on the supported POSIX host. +__extension__ typedef unsigned __int128 Mask; +using Integer = boost::multiprecision::cpp_int; +using Row = std::array; +constexpr std::size_t flat_limit = 788035; +constexpr std::size_t state_limit = 65536; +constexpr Mask live = (Mask{1} << 112) - 1; + +void require(bool condition, const char* message) { + if (!condition) throw std::runtime_error(message); +} + +int weight(Mask mask) { + return __builtin_popcountll(static_cast(mask)) + + __builtin_popcountll(static_cast(mask >> 64)); +} + +struct System { + Mask off = 0; + std::vector normals; +}; + +struct Model { + std::array labels{}; + std::array characters{}; + Mask first = 0; + std::vector systems; +}; + +Model read_model() { + Model model; + for (int& label : model.labels) { + require(static_cast(std::cin >> label), "missing label"); + require(label > 0 && label < 512, "invalid label"); + } + auto sorted = model.labels; + std::sort(sorted.begin(), sorted.end()); + require(std::adjacent_find(sorted.begin(), sorted.end()) == sorted.end(), + "duplicate label"); + std::uint64_t low = 0, high = 0; + require(static_cast(std::cin >> low >> high), "missing first mask"); + model.first = Mask{low} | (Mask{high} << 64); + require((model.first & ~live) == 0 && weight(model.first) == 20, + "invalid first mask"); + int count = 0; + require(static_cast(std::cin >> count) && count == 5680, + "incomplete system inventory"); + model.systems.reserve(5680); + for (int i = 0; i < count; ++i) { + int dimension = 0; + require(static_cast(std::cin >> low >> high >> dimension), + "missing system"); + require(dimension == 1 || dimension == 2, "invalid normal dimension"); + System system; + system.off = Mask{low} | (Mask{high} << 64); + require((system.off & ~live) == 0, "system outside live roots"); + for (int j = 0; j < dimension; ++j) { + Row row{}; + for (int& entry : row) { + require(static_cast(std::cin >> entry), "missing normal"); + require(entry >= -64 && entry <= 64, "normal out of range"); + } + system.normals.push_back(row); + } + // Any partner contributes at most 20 live lines. A residual set + // larger than 36 + 4 cannot be repaired. The independent flat + // enumeration verifies the 20-line premise before scanning. + if (weight(system.off & ~model.first) <= 20 + 36 + 4) + model.systems.push_back(system); + } + char extra = 0; + require(!(std::cin >> extra), "trailing model input"); + for (int c = 0; c < 512; ++c) + for (int i = 0; i < 112; ++i) + if (__builtin_parity(static_cast(model.labels[i] & c))) + model.characters[c] |= Mask{1} << i; + return model; +} + +int binary_rank(Mask mask, const Model& model) { + assert((mask & ~live) == 0); + std::array basis{}; + int rank = 0; + for (int i = 0; i < 112; ++i) { + if (((mask >> i) & 1) == 0) continue; + int value = model.labels[i]; + for (int bit = 8; bit >= 0; --bit) { + if (((value >> bit) & 1) == 0) continue; + if (basis[bit]) value ^= basis[bit]; + else { + basis[bit] = value; + ++rank; + break; + } + } + } + return rank; +} + +void deduplicate(std::vector& masks) { + std::sort(masks.begin(), masks.end()); + masks.erase(std::unique(masks.begin(), masks.end()), masks.end()); +} + +std::vector cuts(Mask residual, const Model& model) { + const int rank = binary_rank(residual, model); + if (rank <= 7) return {0}; + std::vector small; + small.reserve(511); + for (int c = 1; c < 512; ++c) { + const Mask cut = residual & model.characters[c]; + if (weight(cut) > 0 && weight(cut) <= 4) small.push_back(cut); + } + deduplicate(small); + if (rank == 8) return small; + require(rank == 9, "invalid residual rank"); + std::vector result; + result.reserve(511 * 511); + for (std::size_t i = 0; i < small.size(); ++i) + for (std::size_t j = 0; j < i; ++j) + if (weight(small[i] | small[j]) <= 4) + result.push_back(small[i] | small[j]); + deduplicate(result); + return result; +} + +Integer gcd_integer(Integer a, Integer b) { + if (a < 0) a = -a; + if (b < 0) b = -b; + // Euclidean division halves the larger argument within two steps. + for (int iteration = 0; iteration < 4096; ++iteration) { + if (b == 0) return a; + Integer remainder = a % b; + a = b; + b = remainder; + } + throw std::runtime_error("integer gcd capacity exhausted"); +} + +std::vector real_basis(const std::vector& rows) { + require(rows.size() <= 256, "normal-row capacity exhausted"); + std::array, 8> basis{}; + std::vector independent; + for (const Row& original : rows) { + std::array row{}; + std::copy(original.begin(), original.end(), row.begin()); + for (int pivot = 0; pivot < 8; ++pivot) { + if (row[pivot] == 0) continue; + if (basis[pivot][pivot] == 0) { + basis[pivot] = row; + independent.push_back(original); + break; + } + const Integer a = basis[pivot][pivot], b = row[pivot]; + Integer divisor = 0; + for (int k = pivot; k < 8; ++k) { + row[k] = a * row[k] - b * basis[pivot][k]; + divisor = gcd_integer(divisor, row[k]); + } + if (divisor != 0) + for (int k = pivot; k < 8; ++k) row[k] /= divisor; + } + if (independent.size() == 8) break; + } + return independent; +} + +struct Flat { + Mask mask; + std::array annihilator; +}; + +std::vector all_flats(const Model& model, std::map& histogram) { + std::vector flats; + flats.reserve(flat_limit); + for (int a = 0; a < 9; ++a) + for (int b = a + 1; b < 9; ++b) + for (int c = b + 1; c < 9; ++c) { + std::vector> free; + const std::array pivots{a, b, c}; + for (int i = 0; i < 3; ++i) + for (int j = pivots[i] + 1; j < 9; ++j) + if (j != a && j != b && j != c) free.emplace_back(i, j); + require(free.size() <= 18, "RREF free-entry capacity exhausted"); + const unsigned limit = 1U << free.size(); + for (unsigned pattern = 0; pattern < limit; ++pattern) { + std::array ann{1 << a, 1 << b, 1 << c}; + for (std::size_t k = 0; k < free.size(); ++k) + if ((pattern >> k) & 1U) + ann[free[k].first] |= 1 << free[k].second; + const Mask mask = live & ~(model.characters[ann[0]] | + model.characters[ann[1]] | model.characters[ann[2]]); + require(flats.size() < flat_limit, "flat capacity exhausted"); + flats.push_back({mask, ann}); + ++histogram[weight(mask)]; + } + } + require(flats.size() == flat_limit, "incomplete six-flat enumeration"); + require(histogram.rbegin()->first == 20, "six-flat cap changed"); + std::sort(flats.begin(), flats.end(), [](const Flat& a, const Flat& b) { + if (a.mask != b.mask) return a.mask < b.mask; + return a.annihilator < b.annihilator; + }); + flats.erase(std::unique(flats.begin(), flats.end(), + [](const Flat& a, const Flat& b) { return a.mask == b.mask; }), flats.end()); + return flats; +} + +void independently_check_flats(const Model& model, const std::vector& flats, + const std::map& expected_histogram) { + // Different enumeration: choose the successive least coset representatives + // of each 3-space, not pivot columns and free RREF entries. + std::vector masks; + masks.reserve(flat_limit); + std::map histogram; + for (int a = 1; a < 512; ++a) + for (int b = a + 1; b < 512; ++b) { + if (b >= (a ^ b)) continue; + for (int c = b + 1; c < 512; ++c) { + if (c >= (c ^ a) || c >= (c ^ b) || c >= (c ^ a ^ b)) continue; + const Mask mask = live & ~(model.characters[a] | + model.characters[b] | model.characters[c]); + require(masks.size() < flat_limit, "independent flat capacity exhausted"); + masks.push_back(mask); + ++histogram[weight(mask)]; + } + } + require(masks.size() == flat_limit, "incomplete independent flat enumeration"); + require(histogram == expected_histogram, "independent flat histogram differs"); + deduplicate(masks); + require(masks.size() == flats.size(), "independent mask count differs"); + for (std::size_t i = 0; i < masks.size(); ++i) + require(masks[i] == flats[i].mask, "independent partner mask differs"); +} + +struct Qualified { + std::size_t index; + std::vector cuts; +}; + +std::vector qualify(const Model& model, Mask cover) { + std::vector result; + result.reserve(128); + for (std::size_t i = 0; i < model.systems.size(); ++i) { + const Mask residual = model.systems[i].off & ~cover; + // The independently checked seven-flat cap is 36, and |P| <= 4. + if (weight(residual) > 40) continue; + auto options = cuts(residual, model); + if (options.empty()) continue; + require(result.size() < 128, "qualified-system capacity exhausted"); + result.push_back({i, std::move(options)}); + } + return result; +} + +std::vector common_states(const std::vector& qualified) { + std::vector states{0}; + states.reserve(state_limit); + for (const auto& item : qualified) { + const std::size_t old_size = states.size(); + std::vector additions; + additions.reserve(state_limit); + for (std::size_t i = 0; i < old_size; ++i) + for (Mask cut : item.cuts) { + const Mask next = states[i] | cut; + if (weight(next) > 4) continue; + if (additions.size() == state_limit) deduplicate(additions); + require(additions.size() < state_limit, "union capacity exhausted"); + additions.push_back(next); + } + states.insert(states.end(), additions.begin(), additions.end()); + deduplicate(states); + require(states.size() <= state_limit, "state capacity exhausted"); + } + return states; +} + +std::vector admitted_rows(const Model& model, + const std::vector& qualified, Mask state) { + std::vector rows; + rows.reserve(256); + for (const auto& item : qualified) { + const bool admitted = std::any_of(item.cuts.begin(), item.cuts.end(), + [state](Mask cut) { return (cut & ~state) == 0; }); + if (admitted) { + const auto& normals = model.systems[item.index].normals; + rows.insert(rows.end(), normals.begin(), normals.end()); + } + } + require(rows.size() <= 256, "admitted-row capacity exhausted"); + return rows; +} + +struct RankCheck { + std::array annihilator; + Mask deletion; + std::vector rows; + int rank; +}; + +struct Result { + std::vector checks; + int maximum = 0; + std::uint64_t states = 0, ranks = 0, planes = 0; + std::size_t maximum_qualified = 0, maximum_states = 0; + Flat witness{}; + Mask deletion = 0; + std::vector witness_rows; +}; + +Result scan(const Model& model, const std::vector& flats) { + Result result; + for (const Flat& flat : flats) { + const auto qualified = qualify(model, model.first | flat.mask); + const auto states = common_states(qualified); + result.maximum_qualified = std::max(result.maximum_qualified, qualified.size()); + result.maximum_states = std::max(result.maximum_states, states.size()); + for (const auto& item : qualified) + if (model.systems[item.index].normals.size() == 2) ++result.planes; + result.states += states.size(); + for (Mask state : states) { + const auto rows = admitted_rows(model, qualified, state); + // A list of at most M vectors cannot exceed the current maximum M. + if (rows.size() <= static_cast(result.maximum)) continue; + ++result.ranks; + const auto basis = real_basis(rows); + require(result.checks.size() < 4096, "rank-check capacity exhausted"); + result.checks.push_back({flat.annihilator, state, rows, + static_cast(basis.size())}); + if (basis.size() > static_cast(result.maximum)) { + result.maximum = static_cast(basis.size()); + result.witness = flat; + result.deletion = state; + result.witness_rows = basis; + } + } + } + return result; +} + +void print_case(const Model& model, const std::array& annihilator, + Mask deletion, const std::vector& rows, int rank) { + std::cout << "{\"V2_annihilator\":["; + for (int j = 0; j < 3; ++j) { + if (j) std::cout << ','; + std::cout << annihilator[j]; + } + std::cout << "],\"deleted_labels\":["; + bool first = true; + for (int i = 0; i < 112; ++i) { + if (((deletion >> i) & 1) == 0) continue; + if (!first) std::cout << ','; + first = false; + std::cout << model.labels[i]; + } + std::cout << "],\"directions\":["; + for (std::size_t i = 0; i < rows.size(); ++i) { + if (i) std::cout << ','; + std::cout << '['; + for (int j = 0; j < 8; ++j) { + if (j) std::cout << ','; + std::cout << rows[i][j]; + } + std::cout << ']'; + } + std::cout << "],\"rank\":" << rank << '}'; +} + +void print_result(const Model& model, const std::vector& flats, + const std::map& histogram, const Result& result) { + std::cout << "{\"all_flats\":" << flat_limit + << ",\"distinct_live_masks\":" << flats.size() + << ",\"maximum_common_span\":" << result.maximum + << ",\"states_checked\":" << result.states + << ",\"exact_rank_checks\":" << result.ranks + << ",\"qualified_plane_occurrences\":" << result.planes + << ",\"maximum_qualified_systems\":" << result.maximum_qualified + << ",\"maximum_states_per_pair\":" << result.maximum_states + << ",\"six_flat_size_histogram\":{"; + bool first = true; + for (const auto& [size, count] : histogram) { + if (!first) std::cout << ','; + first = false; + std::cout << '\"' << size << "\":" << count; + } + std::cout << "},\"witness\":"; + print_case(model, result.witness.annihilator, result.deletion, + result.witness_rows, result.maximum); + std::cout << ",\"rank_checks\":["; + for (std::size_t i = 0; i < result.checks.size(); ++i) { + if (i) std::cout << ','; + const auto& check = result.checks[i]; + print_case(model, check.annihilator, check.deletion, check.rows, check.rank); + } + std::cout << "]}\n"; + require(static_cast(std::cout), "output failure"); +} + +void self_test() { + Model model; + for (int i = 0; i < 112; ++i) model.labels[i] = 1 << (i % 9); + for (int c = 0; c < 512; ++c) + for (int i = 0; i < 112; ++i) + if (__builtin_parity(static_cast(model.labels[i] & c))) + model.characters[c] |= Mask{1} << i; + require(binary_rank(511, model) == 9, "rank-nine control failed"); + const auto options = cuts(511, model); + require(!options.empty(), "rank-nine deletion control failed"); + for (Mask cut : options) + require(weight(cut) >= 2 && binary_rank(Mask{511} & ~cut, model) <= 7, + "unsound deletion control"); + require(std::find(options.begin(), options.end(), Mask{3}) != options.end(), + "missing two-character cut"); + const auto one = cuts(255, model); + require(std::find(one.begin(), one.end(), Mask{1}) != one.end(), + "missing one-character cut"); + require(cuts(127, model) == std::vector{0}, "rank-seven control failed"); + require(real_basis({Row{1, 2, 3, 4, 0, 0, 0, 0}, + Row{2, 4, 6, 8, 0, 0, 0, 0}}).size() == 1, + "dependent rational-rank control failed"); + require(real_basis({Row{1, 2, 0, 0, 0, 0, 0, 0}, + Row{2, 1, 0, 0, 0, 0, 0, 0}}).size() == 2, + "independent rational-rank control failed"); + const std::vector q{{0, {Mask{3}}}, {1, {Mask{12}}}, {2, {Mask{48}}}}; + const auto states = common_states(q); + require(std::find(states.begin(), states.end(), Mask{15}) != states.end(), + "shared four-cut missing"); + require(std::find(states.begin(), states.end(), Mask{63}) == states.end(), + "separate cuts mistaken for shared cut"); + std::cout << "PASS_SCAN_CONTROLS\n"; +} + +int main(int argc, char** argv) { + try { + require(__builtin_cpu_supports("popcnt"), "CPU POPCNT support is required"); + if (argc == 2 && std::string(argv[1]) == "--self-test") { + self_test(); + return 0; + } + require(argc == 1, "unexpected scanner argument"); + const Model model = read_model(); + std::map histogram; + const auto flats = all_flats(model, histogram); + independently_check_flats(model, flats, histogram); + const Result result = scan(model, flats); + print_result(model, flats, histogram, result); + return 0; + } catch (const std::exception& error) { + std::cerr << "FAIL: " << error.what() << '\n'; + return 2; + } +} diff --git a/research/p112-common-deletion-slice/test_verify.py b/research/p112-common-deletion-slice/test_verify.py new file mode 100644 index 0000000000..e0cc690063 --- /dev/null +++ b/research/p112-common-deletion-slice/test_verify.py @@ -0,0 +1,213 @@ +#!/usr/bin/env python3 +"""Behavioral, arithmetic, quantifier and failure controls for the C5 slice.""" + +import copy +import subprocess +import tempfile +import unittest +from pathlib import Path + +import geometry +import verify + + +class SliceTests(unittest.TestCase): + @classmethod + def setUpClass(cls): + cls.temporary = tempfile.TemporaryDirectory(prefix="p112-slice-tests-") + cls.directory = Path(cls.temporary.name) + cls.fixture = verify.read_json(verify.PACKAGE / "FIXTURE.json") + cls.result = verify.read_json(verify.PACKAGE / "RESULT.json") + cls.model, cls.geometry_report = verify.build_model(cls.fixture) + cls.executable = verify.compile_scanner(cls.directory) + + @classmethod + def tearDownClass(cls): + cls.temporary.cleanup() + + def test_literal_sharpness_boundary(self): + checked = verify.check_case(self.fixture, self.result["scan"]["witness"]) + self.assertEqual(checked, {"residual_ranks": [7, 7, 7, 7], "rational_span": 4}) + + def test_common_cut_is_required(self): + witness = copy.deepcopy(self.result["scan"]["witness"]) + witness["deleted_labels"] = [] + with self.assertRaisesRegex(ValueError, "residual rank"): + verify.check_case(self.fixture, witness) + + def test_dependent_direction_is_rejected(self): + witness = copy.deepcopy(self.result["scan"]["witness"]) + witness["directions"][1] = witness["directions"][0] + with self.assertRaisesRegex(ValueError, "false rational rank"): + verify.check_case(self.fixture, witness) + + def test_wrong_declared_rank_is_rejected(self): + witness = copy.deepcopy(self.result["scan"]["witness"]) + witness["rank"] = 3 + with self.assertRaisesRegex(ValueError, "false rational rank"): + verify.check_case(self.fixture, witness) + + def test_bad_common_sets_are_rejected(self): + for deleted in ([299] * 4, [0], [299, 363, 361, 297, 1]): + with self.subTest(deleted=deleted): + witness = copy.deepcopy(self.result["scan"]["witness"]) + witness["deleted_labels"] = deleted + with self.assertRaises(ValueError): + verify.check_case(self.fixture, witness) + + witness = copy.deepcopy(self.result["scan"]["witness"]) + witness["V2_annihilator"] = [8, 8, 160] + with self.assertRaisesRegex(ValueError, "dependent annihilator"): + verify.check_case(self.fixture, witness) + + def test_invalid_fixture_boundaries(self): + for key, value in ( + ("schema", "wrong"), + ("V1_basis", [1] * 6), + ("V1_basis", [True, 6, 66, 138, 2, 57]), + ("omitted_frame", [[0] * 8] * 8), + ): + with self.subTest(key=key, value=value): + fixture = copy.deepcopy(self.fixture) + fixture[key] = value + with self.assertRaises(ValueError): + verify.fixture_geometry(fixture) + + def test_coverage_includes_normal_planes(self): + self.assertEqual( + self.geometry_report["normal_dimensions"], {"1": 4560, "2": 1120} + ) + self.assertEqual( + [row["orbit_size"] for row in self.geometry_report["parabolic_orbits"]], + [1120, 120, 3360, 1080], + ) + self.assertEqual( + self.geometry_report["model_sha256"], self.result["model_sha256"] + ) + + def test_independent_root_and_label_invariants(self): + roots = geometry.roots() + self.assertEqual(len(roots), 120) + self.assertEqual({sum(x * x for x in row) for row in roots}, {8}) + self.assertEqual(len({geometry.label(row) for row in roots}), 120) + for row in roots: + coordinates = geometry.coordinates(row) + reconstructed = tuple( + sum(coordinates[i] * geometry.SIMPLE[i][j] for i in range(8)) + for j in range(8) + ) + self.assertEqual(reconstructed, row) + + def test_binary_rank_against_complete_xor_spans(self): + # Exhaust every subset of a nine-vector dependent fixture. + values = [1, 2, 4, 8, 16, 3, 5, 9, 17] + for mask in range(512): + rows = [value for i, value in enumerate(values) if mask >> i & 1] + self.assertEqual( + 1 << verify.binary_rank(rows), len(verify.binary_span(rows)) + ) + + def test_scanner_positive_and_quantifier_controls(self): + process = subprocess.run( + [str(self.executable), "--self-test"], + capture_output=True, + text=True, + timeout=30, + check=True, + ) + self.assertEqual(process.stdout, "PASS_SCAN_CONTROLS\n") + + def test_scanner_rejects_malformed_streams(self): + lines = self.model.splitlines() + duplicate = lines[0].split() + duplicate[1] = duplicate[0] + wrong_count = lines.copy() + wrong_count[2] = "5679" + for model in ( + "", + " ".join(duplicate) + "\n", + "\n".join(wrong_count), + self.model + "unexpected trailing bytes\n", + ): + with self.subTest(prefix=model[:30]): + process = subprocess.run( + [str(self.executable)], + input=model, + capture_output=True, + text=True, + timeout=30, + check=False, + ) + self.assertEqual(process.returncode, 2) + self.assertIn("FAIL:", process.stderr) + self.assertEqual(process.stdout, "") + + def test_semantic_mutants_fail_controls(self): + source = (verify.PACKAGE / "scan.cpp").read_text() + mutants = ( + ("if (rank == 8) return small;", "if (rank == 8) return {0};"), + ( + 'require(rank == 9, "invalid residual rank");', + 'require(rank == 9, "invalid residual rank"); return small;', + ), + ("if (weight(next) > 4) continue;", "if (weight(next) > 6) continue;"), + ) + for index, (old, new) in enumerate(mutants): + with self.subTest(mutant=index): + self.assertEqual(source.count(old), 1) + path = self.directory / f"mutant-{index}.cpp" + path.write_text(source.replace(old, new)) + mutant = verify.compile_scanner(self.directory, path) + process = subprocess.run( + [str(mutant), "--self-test"], + capture_output=True, + text=True, + timeout=30, + check=False, + ) + self.assertEqual(process.returncode, 2) + self.assertIn("FAIL:", process.stderr) + # Later tests must not accidentally reuse the last mutant. + self.executable = verify.compile_scanner(self.directory) + + def test_json_capacity_and_shape(self): + path = self.directory / "bad.json" + for data in ("[]", "{bad", " " * (2 * 1024 * 1024 + 1)): + path.write_text(data) + with self.assertRaises(ValueError): + verify.read_json(path) + + def test_cli_rejects_bad_fixture_and_receipt(self): + bad = self.directory / "bad.json" + bad.write_text("[]") + for option in ("--fixture", "--expected"): + process = subprocess.run( + ["python3", "-B", str(verify.PACKAGE / "verify.py"), option, str(bad)], + capture_output=True, + text=True, + timeout=30, + check=False, + ) + self.assertEqual(process.returncode, 2) + self.assertIn("JSON must be an object", process.stderr) + self.assertNotIn("PASS_", process.stdout) + + def test_rank_trace_rejects_false_or_missing_cases(self): + case = copy.deepcopy(self.result["scan"]["witness"]) + checked = verify.check_rank_trace( + self.fixture, {"rank_checks": [case], "exact_rank_checks": 1} + ) + self.assertEqual(checked["cases"], 1) + with self.assertRaisesRegex(ValueError, "incomplete"): + verify.check_rank_trace( + self.fixture, {"rank_checks": [case], "exact_rank_checks": 2} + ) + case["rank"] = 3 + with self.assertRaisesRegex(ValueError, "false rational rank"): + verify.check_rank_trace( + self.fixture, {"rank_checks": [case], "exact_rank_checks": 1} + ) + + +if __name__ == "__main__": + unittest.main() diff --git a/research/p112-common-deletion-slice/verify.py b/research/p112-common-deletion-slice/verify.py new file mode 100644 index 0000000000..34df3fd071 --- /dev/null +++ b/research/p112-common-deletion-slice/verify.py @@ -0,0 +1,279 @@ +#!/usr/bin/env python3 +"""Check one complete C5 space slice, including continuous normal planes.""" + +import argparse +import hashlib +import json +import subprocess +import tempfile +from collections import Counter +from itertools import combinations +from pathlib import Path + +from geometry import dot, echelon, label, normals, orthogonality_systems, require, roots + +PACKAGE = Path(__file__).resolve().parent +FLAGS = [ + "-std=c++17", + "-O3", + "-mpopcnt", + "-Wall", + "-Wextra", + "-Wpedantic", + "-Wconversion", + "-Wshadow", + "-Werror", +] + + +def read_json(path: Path) -> dict: + with path.open("rb") as stream: + raw = stream.read(2 * 1024 * 1024 + 1) + require(len(raw) <= 2 * 1024 * 1024, "JSON exceeds two MiB") + value = json.loads(raw) + require(isinstance(value, dict), "JSON must be an object") + return value + + +def binary_span(basis: list[int]) -> set[int]: + assert len(basis) <= 9 and all(0 <= x < 512 for x in basis) + span = {0} + for value in basis: + span |= {x ^ value for x in span} + return span + + +def binary_rank(values: list[int]) -> int: + """Ascending pivots, unlike the scanner's descending-pivot algorithm.""" + assert len(values) <= 120 and all(0 <= x < 512 for x in values) + basis = [0] * 9 + for value in values: + for bit in range(9): + if not value >> bit & 1: + continue + if basis[bit]: + value ^= basis[bit] + else: + basis[bit] = value + break + return sum(bool(value) for value in basis) + + +def fixture_geometry(fixture: dict) -> tuple: + require(fixture.get("schema") == "p112-common-slice/v1", "wrong fixture schema") + frame = fixture.get("omitted_frame") + require(isinstance(frame, list) and len(frame) == 8, "frame needs eight roots") + require(all(isinstance(row, list) and len(row) == 8 for row in frame), "bad frame") + require(all(type(x) is int for row in frame for x in row), "nonintegral frame") + frame = {tuple(row) for row in frame} + lines = roots() + require(len(frame) == 8 and frame <= set(lines), "invalid frame roots") + require( + all(dot(a, b) == 0 for a, b in combinations(frame, 2)), "nonorthogonal frame" + ) + basis = fixture.get("V1_basis") + require(isinstance(basis, list) and len(basis) == 6, "basis needs six entries") + require(all(type(x) is int and 0 < x < 512 for x in basis), "invalid basis entry") + span = binary_span(basis) + require(len(span) == 64, "dependent first basis") + live_lines = tuple(row for row in lines if row not in frame) + labels = [label(row) for row in live_lines] + require(len(labels) == len(set(labels)) == 112, "invalid live labels") + covered = sum(1 << i for i, value in enumerate(labels) if value in span) + require(covered.bit_count() == 20, "first space needs twenty live lines") + return lines, live_lines, labels, covered + + +def seven_flat_cap(labels: list[int]) -> dict: + """Separate, exhaustive codimension-two cardinality control.""" + assert len(labels) == 112 + characters = [ + sum(1 << i for i, value in enumerate(labels) if (c & value).bit_count() % 2) + for c in range(512) + ] + histogram = Counter() + for a, b in combinations(range(1, 512), 2): + if b >= a ^ b: + continue + histogram[112 - (characters[a] | characters[b]).bit_count()] += 1 + require(sum(histogram.values()) == 43435, "incomplete seven-flat enumeration") + require(max(histogram) == 36, "seven-flat cardinality cap changed") + return {"flats": sum(histogram.values()), "maximum_lines": max(histogram)} + + +def build_model(fixture: dict) -> tuple[str, dict]: + lines, live_lines, labels, covered = fixture_geometry(fixture) + live = sum(1 << i for i, row in enumerate(lines) if row in live_lines) + systems, orbits = orthogonality_systems(lines, live) + require(len(systems) == 5680, "incomplete parabolic inventory") + text = [" ".join(map(str, labels)), f"{covered & ((1 << 64) - 1)} {covered >> 64}"] + text.append(str(len(systems))) + dimensions = Counter() + for system in systems: + basis = normals(lines, system) + dimensions[len(basis)] += 1 + off = sum( + 1 << i + for i, row in enumerate(live_lines) + if any(dot(row, h) for h in basis) + ) + text.append(f"{off & ((1 << 64) - 1)} {off >> 64} {len(basis)}") + text.extend(" ".join(map(str, row)) for row in basis) + require(dict(dimensions) == {1: 4560, 2: 1120}, "normal dimensions changed") + model = "\n".join(text) + "\n" + require(len(model) < 2 * 1024 * 1024, "model capacity exceeded") + report = { + "schema": "p112-common-slice-result/v1", + "model_sha256": hashlib.sha256(model.encode()).hexdigest(), + "V1_live_labels": sorted( + value for i, value in enumerate(labels) if covered >> i & 1 + ), + "seven_flat_cap": seven_flat_cap(labels), + "parabolic_orbits": orbits, + "normal_dimensions": {str(k): dimensions[k] for k in sorted(dimensions)}, + } + return model, report + + +def compile_scanner(directory: Path, source: Path | None = None) -> Path: + executable = directory / "scan" + subprocess.run( + ["g++", *FLAGS, str(source or PACKAGE / "scan.cpp"), "-o", str(executable)], + check=True, + capture_output=True, + text=True, + timeout=60, + ) + return executable + + +def check_case(fixture: dict, witness: dict) -> dict: + """Independently interpret a scanner boundary and its rational rank.""" + _, live_lines, labels, covered = fixture_geometry(fixture) + ann = witness["V2_annihilator"] + require(isinstance(ann, list) and len(ann) == 3, "invalid annihilator shape") + require(all(type(x) is int and 0 < x < 512 for x in ann), "invalid annihilator") + require(len(binary_span(ann)) == 8, "dependent annihilator") + second = {x for x in range(512) if all((x & a).bit_count() % 2 == 0 for a in ann)} + require(len(second) == 64, "second space is not six-dimensional") + deleted = witness["deleted_labels"] + require(isinstance(deleted, list) and len(deleted) <= 4, "excess common deletions") + require(all(type(x) is int for x in deleted), "invalid deleted label") + require( + len(set(deleted)) == len(deleted) and set(deleted) <= set(labels), "bad cut" + ) + directions = witness["directions"] + require( + isinstance(directions, list) and 0 < len(directions) <= 120, + "invalid direction count", + ) + require( + all(isinstance(row, list) and len(row) == 8 for row in directions), + "bad direction", + ) + require( + all(type(x) is int and abs(x) <= 64 for row in directions for x in row), + "bad entry", + ) + ranks = [] + for direction in directions: + residual = [ + value + for i, (row, value) in enumerate(zip(live_lines, labels, strict=True)) + if dot(row, direction) + and not covered >> i & 1 + and value not in second + and value not in deleted + ] + ranks.append(binary_rank(residual)) + require(all(rank <= 7 for rank in ranks), "witness violates residual rank") + rank = len(echelon(directions)) + require( + type(witness.get("rank")) is int and witness["rank"] == rank, + "false rational rank", + ) + require(rank <= 4, "slice span exceeds four") + return {"residual_ranks": ranks, "rational_span": rank} + + +def check_rank_trace(fixture: dict, result: dict) -> dict: + trace = result.pop("rank_checks") + require(isinstance(trace, list) and 0 < len(trace) <= 4096, "invalid rank trace") + require(len(trace) == result["exact_rank_checks"], "rank trace is incomplete") + largest_residual = 0 + for case in trace: + checked = check_case(fixture, case) + largest_residual = max(largest_residual, max(checked["residual_ranks"])) + payload = json.dumps(trace, sort_keys=True, separators=(",", ":")).encode() + return { + "cases": len(trace), + "sha256": hashlib.sha256(payload).hexdigest(), + "maximum_residual_rank": largest_residual, + } + + +def verify(fixture: dict, directory: Path, expected: dict | None) -> dict: + model, report = build_model(fixture) + executable = compile_scanner(directory) + control = subprocess.run( + [str(executable), "--self-test"], + check=True, + capture_output=True, + text=True, + timeout=30, + ) + require(control.stdout == "PASS_SCAN_CONTROLS\n", "scanner controls failed") + scan = subprocess.run( + [str(executable)], + input=model, + check=True, + capture_output=True, + text=True, + timeout=300, + ) + require(len(scan.stdout) < 2 * 1024 * 1024, "scanner result exceeds capacity") + result = json.loads(scan.stdout) + require(result["all_flats"] == 788035, "incomplete partner-space coverage") + require(result["distinct_live_masks"] == 776806, "partner-mask coverage changed") + require(result["maximum_common_span"] == 4, "common span bound changed") + report["independent_rank_trace"] = check_rank_trace(fixture, result) + report["scan"] = result + report["independent_witness_check"] = check_case(fixture, result["witness"]) + require(report["independent_witness_check"]["rational_span"] == 4, "sharpness lost") + if expected is not None: + require(report == expected, "committed receipt or model changed") + return report + + +def main() -> None: + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--fixture", type=Path, default=PACKAGE / "FIXTURE.json") + parser.add_argument("--output", type=Path, help="write an external replay receipt") + parser.add_argument("--expected", type=Path, default=PACKAGE / "RESULT.json") + parser.add_argument( + "--bootstrap", action="store_true", help="do not compare a prior receipt" + ) + args = parser.parse_args() + try: + fixture = read_json(args.fixture) + expected = None if args.bootstrap else read_json(args.expected) + with tempfile.TemporaryDirectory(prefix="p112-slice-") as temporary: + report = verify(fixture, Path(temporary), expected) + if args.output is not None: + args.output.write_text(json.dumps(report, indent=2, sort_keys=True) + "\n") + print( + "PASS_P112_COMMON_SLICE flats=788035 masks=776806 systems=5680 common_span=4" + ) + except ( + ValueError, + OSError, + KeyError, + TypeError, + subprocess.SubprocessError, + ) as error: + diagnostic = getattr(error, "stderr", None) or str(error) + parser.exit(2, f"FAIL: {diagnostic}\n") + + +if __name__ == "__main__": + main()