From af26d5be8e1f684e96da080160593bd3bd7accd8 Mon Sep 17 00:00:00 2001 From: Chris R Date: Mon, 19 Oct 2026 15:32:37 +1100 Subject: [PATCH 1/3] research: exclude a C5 caller with a common-cut23 bound --- research/p112-common-cut23-caller/CHECKS.json | 74 ++++++ research/p112-common-cut23-caller/PROOF.md | 187 +++++++++++++ research/p112-common-cut23-caller/README.md | 107 ++++++++ research/p112-common-cut23-caller/RESULT.json | 247 ++++++++++++++++++ .../p112-common-cut23-caller/SOURCES.json | 60 +++++ research/p112-common-cut23-caller/TASK.json | 78 ++++++ research/p112-common-cut23-caller/VERIFY.json | 50 ++++ .../p112-common-cut23-caller/independent.py | 180 +++++++++++++ .../p112-common-cut23-caller/test_controls.py | 148 +++++++++++ research/p112-common-cut23-caller/verify.py | 227 ++++++++++++++++ 10 files changed, 1358 insertions(+) create mode 100644 research/p112-common-cut23-caller/CHECKS.json create mode 100644 research/p112-common-cut23-caller/PROOF.md create mode 100644 research/p112-common-cut23-caller/README.md create mode 100644 research/p112-common-cut23-caller/RESULT.json create mode 100644 research/p112-common-cut23-caller/SOURCES.json create mode 100644 research/p112-common-cut23-caller/TASK.json create mode 100644 research/p112-common-cut23-caller/VERIFY.json create mode 100644 research/p112-common-cut23-caller/independent.py create mode 100644 research/p112-common-cut23-caller/test_controls.py create mode 100644 research/p112-common-cut23-caller/verify.py diff --git a/research/p112-common-cut23-caller/CHECKS.json b/research/p112-common-cut23-caller/CHECKS.json new file mode 100644 index 0000000000..207c344f9c --- /dev/null +++ b/research/p112-common-cut23-caller/CHECKS.json @@ -0,0 +1,74 @@ +{ + "schema_version": 1, + "recorded_utc": "2026-10-19T04:32:00Z", + "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "environment": { + "python": "3.12.3", + "platform": "Linux-7.0.0-38-generic-x86_64-with-glibc2.39", + "machine": "x86_64", + "dependencies": "Python standard library only" + }, + "mathematics": { + "primary": "PASS_P112_COMMON_CUT23_CALLER;43,435seven-spaces;5,212,200root-flat pairs;8,214,570fourfold intersections", + "separate_implementation": "PASS_COMMON_CUT23_INDEPENDENT;separate lattice shell/rational coordinates/RREF annihilators/pair join;complete histograms agree", + "positive_fixture": "Two independent directions with one22-site cut and residual binary ranks7,7;no three-direction attainment claimed", + "controls": { + "optimized_rejecting_cli_runs": 8, + "optimized_positive_cli_runs": 1, + "invalid_proof_budget_rejections": 4, + "actual_fourfold_semantic_mutations_rejected": 1, + "separate_cut_union": 66, + "final_controls_exit": 0, + "final_controls_seconds": 39.92337548199794, + "terminal": "PASS_COMMON_CUT23_CONTROLS 8 rejecting optimized CLI runs; {'rejected_budget_cases': 4, 'separate_cut_union': 66, 'fourfold_semantic_mutations': 1}" + } + }, + "verification": { + "registered_package": "PASS_REGISTERED_RESEARCH_PACKAGE research/p112-common-cut23-caller;all three commands;final added semantic control separately rerun after its addition", + "predecessor_composition": "PR3289 registered bounded package and its separate indexed-role scan/controls passed. This rechecks65/69conditional composition, not all inherited geometric theorems.", + "syntax_and_json": "All three Python sources compile;all four scientific/metadata JSON files parse;new files pass whitespace check.", + "ruff": "Attempted local Ruff returned signal11/exit139 without diagnostics;lint PASS is not claimed.", + "publication_checks": "Post-publication byte/history and committed Git-free export results will be reported in the PR/discussion;not yet claimed in this pre-publication record." + }, + "overlap": { + "entry_open_prs": 633, + "entry_complete_rest_pages": 7, + "entry_empty_next_page": 8, + "prepublication_open_prs": 633, + "prepublication_unique_prs": 633, + "prepublication_complete_rest_pages": 7, + "prepublication_empty_next_page": 8, + "prepublication_utc": "2026-10-19T04:30:00Z", + "local_records": 2487, + "canonical_discussion": "https://github.com/CrocSwap/integer-mult-bounds/discussions/3156#discussioncomment-19030442", + "discussion_coverage": "Partial browser coverage:71-comment header at entry;72after own claim;41 rendered comment permalinks measured on refresh. Loaded text and replies inspected, including latest canonical results. Load-more attempted;not an all-comment/all-board snapshot.", + "helper_warnings": [ + "discussions: refresh failed; using old data if available: [Errno 2] No such file or directory: 'gh'", + "discussions: no usable remote snapshot" + ], + "limits": "No exhaustive arbitrary-diff,closed-PR body,unpublished-work or all-board Discussion search;no novelty certificate." + }, + "upstream_checkpoint": { + "fetched_again": true, + "origin_main": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "priority_revision": 6, + "changed_guidance_paths": [] + }, + "scope": { + "new_result": "Common-cut23 upper bound3 and explicit 2,3,4^2,7^6 caller exclusion", + "fixed_inventory": "68/69conditional on the named prior contracts;not a global unresolved count", + "inherited": "Standard E8 Weyl-chamber theorem. The inventory tally additionally reuses all PR3289/3322/3405 mathematical premises,without fresh heavy replays.", + "unrun": [ + "independent human review", + "formal proof kernel", + "full original FINITE/C5 suites", + "selected cold replay", + "physical native/supplier admission", + "upstream manual P112 workflow", + "Lean", + "Docker" + ], + "selected_record_changed": false, + "kappa_changed": false + } +} diff --git a/research/p112-common-cut23-caller/PROOF.md b/research/p112-common-cut23-caller/PROOF.md new file mode 100644 index 0000000000..95a1eb2060 --- /dev/null +++ b/research/p112-common-cut23-caller/PROOF.md @@ -0,0 +1,187 @@ +# A common cut of 23 sites admits at most three rank-seven directions + +## Model and statement + +Let P be the 112 E8 root lines left after deleting the eight frame lines +in the pinned PR3163 fixture. Use the doubled integral representatives r_t +and their simple-root parity labels ell(t) in F2^9, with affine bit one. +The replay checks every root row against the canonical +`research/one-sided-six-multisets/data/data.txt`. Its label convention moves +the affine bit from bit 0 to bit 8; the invertible bit permutation is checked +on all 112 labels. This changes no binary support rank. + +For a characteristic-zero field K, put + + c_h(t) = r_t dot h, + C = {c_h : h in K^8}, + w(q) = rank_F2 {ell(t) : q(t) != 0}, + Off(h) = {t : c_h(t) != 0}. + +The pairing is bilinear, including over C. The live-row Gram matrix is +112 I_8, checked exactly, so evaluation is injective over K. + +**Common-cut theorem.** Fix ONE subset S of P with |S| <= 23. The nonzero +directions h satisfying + + rank_F2 ell(Off(h) outside S) <= 7 + +belong to at most three distinct projective lines. In particular, their +K-linear span has dimension at most three. The bound three is an upper +bound: attainment by three directions and sharpness of 23 are unclaimed. +A literal two-independent-direction fixture at 22 cuts is checked. + +The proof uses the standard finite E8 Weyl-chamber theorem and exact finite +checks described below. It is not proof-kernel verification. The new result +is the combination of the root-restricted flat cap and fourfold overlap +with one common deletion set, and its named caller application. The E8 model, +Weyl reduction and earlier flat-cap lineage retain predecessor credit. + +## 1. Completeness: qualifying directions are root normals + +There are exactly 43,435 binary seven-spaces. Their live traces have maximum +size 36. The primary enumerates all two-dimensional annihilators by their +three nonzero functionals a,b,a XOR b, using a= 21. + +The 32 cap is a fresh exhaustive check of an earlier type of local capacity +bound, not a newly claimed root/label model. Both implementations reproduce +it using their separate geometry and seven-space enumeration. + +## 3. Four distinct root normals share at most 14 live off-sites + +The exact finite identity needed is + + max |Off(alpha_1) intersect ... intersect Off(alpha_4)| = 14, + +over every four DISTINCT projective E8 root normals. No independence +restriction is needed. The primary checks all C(120,4)=8,214,570 quadruples. +The second reconstructs roots from the doubled E8 lattice shell, and joins +ordered pairs with a=21 and every A_i is contained in that SAME S, + + |A_1 intersect A_2 intersect A_3 intersect A_4| + >= sum_i |A_i| - 3|S| + >= 84 - 3*23 = 15. + +This contradicts the exact upper bound 14. Hence at most three projective +directions qualify. At the actual caller's budget 22, the lower bound is 18. +Per-direction cuts would not imply this inequality. The controls explicitly +exhibit four independent normals with individual 21-site cuts whose common +union has 66 sites; pooling them is rejected. + +## 4. Excluding the named historical caller 2,3,4,4,7,7,7,7,7,7 + +Suppose ten K-linearly independent pieces span T, have these binary weight +bounds, and dim(T intersect C)>=6. Their first four supports have union S +with + + |S| <= 2+4+8+8 = 22. + +These low-rank cardinality bounds follow directly from the distinct labels' +affine bit: a d-dimensional binary linear space meets that affine +hyperplane in at most 2^(d-1) points. No rank-five or rank-six census is used. + +Write D=T intersect C. The quotient T/D has dimension at most four. The +four small pieces have independent quotient images. Otherwise a nonzero +linear combination would be a nonzero codeword supported on S, contradicting +distance 53. They are therefore a quotient basis; dim D=6. + +Each of the six other pieces q_i has a unique combination a_i of the four +small pieces with c_i=q_i-a_i in C. These six c_i are independent, by their +coefficients on the six distinct q_i in the original independent-piece +basis. Evaluation supplies six independent directions h_i. Outside the ONE +common S, c_i agrees with q_i, so its residual binary support rank is at +most seven. The common-cut theorem permits at most three projective +directions. This contradiction excludes the named caller. + +This result concerns the explicit independent-piece/code-intersection +hypotheses. Applying the historical TWOSIDE reduction to a physical decoder +continues to inherit that reduction's other premises. + +## 5. Application audit and decision about normal planes + +The source-bound PR3289 inventory conditionally covers 65 of its 69 +historical (6,4) rows and lists four inventory-uncertified rows. The explicit +PR3322 contract excludes 2^3,7^7; the PR3405 contract excludes 2,5,6^8. +Those two theorems remain inherited conditional premises in this tally; +their heavy scientific replays are not claimed here. The new theorem +excludes 2,3,4^2,7^6. This NAMED contract inventory therefore accounts for +68/69 rows, leaving 4,5^3,6^6 uncertified BY THIS INVENTORY. This is neither +a current global unresolved count nor a proof that the last row is possible. + +The PR3163 global two-six-flat/rank-seven/common-four question has different +hypotheses from this theorem. It is not settled here. For the named caller, +the actual small footprint already excludes normal planes before section 2. +For the other inventory row, its four-small-piece budget 8+12+12+12=44 and +rank-six endpoint cap 20 similarly give support<=64<70, hence root normals, +under those inherited capacities. Uniform normal-plane exclusion would not +close either of these caller gaps by itself. No all-first-space or global +normal-plane census is launched or claimed. + +## Evidence boundaries and credit + +The generic metadata/pin checks authenticate sources; they are not theorem +acceptance. The primary and separate mathematical implementations establish +the stated finite facts. The written arguments discharge the finite-to- +characteristic-zero implication and the caller composition, using the +explicit standard Weyl-chamber theorem. Same-session computational +corroboration is not independent human review or formal-kernel verification. + +Credit DreamingOfClouds/PR3154 for C5, TWOSIDE and the FINITE lineage; Nick +Petalas/PR3160/3161/3163 for geometry, quantifier controls and the completed +slice; PR3282/3289 for the historical caller inventory and exact cover +contracts; PR3253/3322 and PR3397/3405 for the separate inherited exclusions; +and joaqcoo and the retained E8/P112/root-code lineage. All exact live pins +are at canonical main 20ecf2891d80b5acf18d980b2164fb44ea7faa90 in SOURCES.json. +New work is by Chris R / Clear1nsight with substantial OpenAI Codex +assistance, Apache-2.0. No complete C5, global decoder floor, physical +supplier, new kappa or selected-frontier change is claimed. diff --git a/research/p112-common-cut23-caller/README.md b/research/p112-common-cut23-caller/README.md new file mode 100644 index 0000000000..8056e293e7 --- /dev/null +++ b/research/p112-common-cut23-caller/README.md @@ -0,0 +1,107 @@ +# Common-cut23 bound closes one historical C5 caller + +For ONE common set of at most 23 live P112 sites, the directions whose +remaining support has binary rank at most seven occupy at most THREE +projective lines, over every characteristic-zero field, using the standard +E8 Weyl-chamber theorem. This excludes the explicit independent-piece caller +`2,3,4^2,7^6` at code-intersection dimension at least six. Its four small +pieces cover at most 22 sites, but its quotient requires six independent +directions. [PROOF.md](PROOF.md) gives the complete argument and scope. + +This is the requested C5 application audit following workflow repair +[#3885](https://github.com/CrocSwap/integer-mult-bounds/pull/3885) and +[#3163](https://github.com/CrocSwap/integer-mult-bounds/pull/3163)'s slice. +The audit found an actual caller in PR3289. Its small support already forces +root normals, so the global normal-plane question is not needed to close +this gap. The new result instead combines a root-restricted seven-flat +capacity with a four-root off-support overlap bound. Full C5, the global +two-six-flat/common-four bound, uniform normal-plane exclusion, decoder +cost, physical suppliers, kappa and the selected record remain outside scope. + +## Exact evidence + +- All 43,435 binary seven-spaces have at most 36 live labels. Each of the + 120 root normals meets each seven-space in at most 32 of its off-sites: + 5,212,200 exact tests. Live normals need at least 21 deletions; frame + normals need 24 and cannot qualify here. +- Every one of 8,214,570 four-distinct-root-normal intersections has at + most 14 live off-sites. A common cut of 23 would require at least + `4*21 - 3*23 = 15` such sites for four qualifying directions. +- The primary uses the exact authenticated predecessor geometry. A separate + implementation imports no primary routines: it reconstructs the doubled + E8 lattice shell, solves labels over Q, enumerates RREF annihilators, and + joins root pairs. The complete flat and fourfold histograms agree. +- A literal fixture has two independent directions with residual ranks + seven under the same 22-site cut. Attainment of three is unclaimed. +- Controls reject eight actual optimized CLI source/receipt corruptions, + four invalid proof budgets, and the substitution of separate cuts for + a common one. Four independent normals each have a valid 21-site cut, + but those cuts' union has 66 sites. + +PR3289's fixed inventory covers 65/69 historical `(6,4)` rows. Adding the +explicit conditional caller contracts of PR3322 and PR3405 accounts for +67/69. The new lemma raises THIS NAMED INVENTORY to 68/69; it still does not +certify `4,5^3,6^6`. This is not a global public unresolved-row count. The two +successor theorems and their inherited dependencies are reused as written +conditional contracts; their scientific censuses were not freshly replayed. +The PR3289 registered bounded composition replay was separately run and passed. + +## Reproduction + +Standard-library CPython 3.12; no native compiler or external library is needed +for this package. From the repository root: + +```sh +python3.12 -W error -B scripts/research_package.py --package research/p112-common-cut23-caller +``` + +The three registered commands are `verify.py`, `independent.py`, and +`test_controls.py`. All declared inputs are exact canonical-main bytes, pinned +by commit, Git blob and SHA256 in SOURCES.json. The primary compiles only the +authenticated geometry source, bypassing bytecode imports. The second reads +its literal simple system through AST and executes no predecessor code. +Controls use private byte copies under TMPDIR. Default verification does not +write package or input files. The explicit `--write-result NEW_PATH` option +only generates a receipt and refuses to overwrite an existing path. + +CHECKS.json records the actual environment, timings, export checks and unrun +obligations. A metadata/pin PASS authenticates the package, not its mathematics. +The written proof and two finite implementations are same-session AI-assisted +evidence, not independent human or proof-kernel review. No full selected cold +replay, original FINITE suite, upstream P112 manual workflow, Lean or Docker +execution is claimed. + +## Open next questions + +1. Independently review the new common-cut inequality and actual caller + transfer, then reproduce the two complete finite histograms. This is the + smallest useful check before adopting the exclusion. +2. Reconcile the literal `4,5^3,6^6` caller with current exact source contracts. + Its 44-site small-support bound is outside this theorem's 23-site allowance. + Under the inherited rank-six support cap it already has root normals; + normal-plane exclusion alone would not close it. Its actual coefficient + and support compatibility is not supplied here. + +The uniform normal-plane problem for arbitrary two-six-flat covers remains +unsettled by this package. A future census needs a separate caller or decision +that it can change. No continuing research reservation follows this result. + +## Overlap, sources and credit + +Canonical main/base: `20ecf2891d80b5acf18d980b2164fb44ea7faa90`, revision 6. +Entry overlap read 633 open PR bodies through seven REST pages and an empty +eighth page, canonical notes/ledger, loaded C5 discussion text/replies and latest handoffs. +The discussion header had71comments at entry and72after the claim;41rendered +permalinks were measured on refresh. Load-more was attempted; full comment +pagination is not claimed. `find_overlap.py` searched the +PR snapshot and local corpus. Its all-board Discussion refresh failed because +`gh` is unavailable: broader Discussion, arbitrary diffs and unpublished work +are not exhaustively covered. Pre-submission refresh is recorded in CHECKS.json. +The canonical investigation is [discussion3156](https://github.com/CrocSwap/integer-mult-bounds/discussions/3156#discussioncomment-19030442). + +Credit DreamingOfClouds/PR3154 for TWOSIDE, C5 and the FINITE lineage; Nick +Petalas/PR3160/3161/3163 for geometry, quantifier controls and the slice, +PR3282/3289 for caller accounting, PR3253/3322 and PR3397/3405 for the +separate inherited exclusions; joaqcoo and the retained E8/P112/root-code +lineage. The canonical source archive stays unchanged. Chris R / Clear1nsight +with substantial OpenAI Codex assistance. New work is Apache-2.0. diff --git a/research/p112-common-cut23-caller/RESULT.json b/research/p112-common-cut23-caller/RESULT.json new file mode 100644 index 0000000000..93142d0d9f --- /dev/null +++ b/research/p112-common-cut23-caller/RESULT.json @@ -0,0 +1,247 @@ +{ + "schema": "p112-common-cut23-caller/v1", + "chamber": { + "rank_at_most_six_max": 36, + "seven_face_counts": [ + 42, + 28, + 22, + 14, + 16, + 23, + 37, + 63 + ], + "root_face_normal": [ + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 1 + ] + }, + "flat_facts": { + "seven_flats": 43435, + "global_seven_flat_cap": 36, + "flat_size_histogram": { + "0": 255, + "16": 7, + "20": 336, + "22": 3584, + "24": 3752, + "26": 10752, + "28": 6416, + "30": 10752, + "32": 3549, + "34": 3584, + "36": 448 + }, + "root_flat_tests": 5212200, + "root_cut_minima": { + "53,32,21": 112, + "56,32,24": 8 + } + }, + "fourfold": { + "quadruples": 8214570, + "maximum": 14, + "histogram": { + "0": 154056, + "1": 12544, + "2": 127008, + "3": 698880, + "4": 2383164, + "5": 901824, + "6": 1952160, + "7": 1046528, + "8": 354774, + "9": 275520, + "10": 168000, + "11": 10752, + "12": 21840, + "13": 86016, + "14": 21504 + }, + "witness_indices": [ + 2, + 13, + 17, + 44 + ], + "witness_roots": [ + [ + 0, + 0, + 0, + 0, + 0, + 2, + -2, + 0 + ], + [ + 0, + 0, + 0, + 2, + 0, + -2, + 0, + 0 + ], + [ + 0, + 0, + 0, + 2, + 0, + 0, + 2, + 0 + ], + [ + 1, + -1, + -1, + -1, + -1, + 1, + -1, + -1 + ] + ] + }, + "positive_fixture": { + "directions": [ + [ + 0, + 0, + 0, + 0, + 0, + 2, + -2, + 0 + ], + [ + 0, + 0, + 0, + 0, + 0, + 2, + 2, + 0 + ] + ], + "annihilators": [ + [ + 65, + 257 + ], + [ + 64, + 257 + ] + ], + "common_cut_indices": [ + 0, + 1, + 2, + 3, + 4, + 7, + 9, + 10, + 13, + 14, + 17, + 18, + 21, + 22, + 27, + 28, + 31, + 32, + 103, + 104, + 107, + 108 + ], + "residual_ranks": [ + 7, + 7 + ] + }, + "theorem": { + "cut_budget": 23, + "four_cut_intersection_floor": 15, + "fourfold_maximum": 14, + "projective_direction_bound": 3 + }, + "caller": { + "historical_rows": 69, + "inherited_contract_coverage": 65, + "successor_contract_rows": [ + [ + 2, + 2, + 2, + 7, + 7, + 7, + 7, + 7, + 7, + 7 + ], + [ + 2, + 5, + 6, + 6, + 6, + 6, + 6, + 6, + 6, + 6 + ] + ], + "coverage_before_new_lemma": 67, + "new_caller": [ + 2, + 3, + 4, + 4, + 7, + 7, + 7, + 7, + 7, + 7 + ], + "small_support_cap": 22, + "required_directions": 6, + "direction_bound": 3, + "conditional_inventory_coverage": 68, + "inventory_uncertified": [ + [ + 4, + 5, + 5, + 5, + 6, + 6, + 6, + 6, + 6, + 6 + ] + ], + "scope": "Fixed named contract inventory, not a global unresolved count." + } +} diff --git a/research/p112-common-cut23-caller/SOURCES.json b/research/p112-common-cut23-caller/SOURCES.json new file mode 100644 index 0000000000..80a798ec1d --- /dev/null +++ b/research/p112-common-cut23-caller/SOURCES.json @@ -0,0 +1,60 @@ +{ + "schema_version": 1, + "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81", + "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "67f085acd86acd7d4e03922d9cf4b26bca66fed5", + "sha256": "47b42433f5a85809a3aadd29c2c339da2c6ed728e4f7762df6b88bccb7874cf0" + }, + { + "path": "research/one-sided-six-multisets/data/data.txt", + "usage": "input", + "git_blob": "dc591a4e0252bac096e6c63c51058f6caee66bfe", + "sha256": "ac4a48851b922f2a433684b60c74768ae3bb4fc5e8990ffe63e3942bb3c2ea34" + }, + { + "path": "research/p112-b6-t4-original-covers/PROOF.md", + "usage": "input", + "git_blob": "ad52f19e50ebf75e34e5cea097ee21b1e718ff4c", + "sha256": "2e67d3bd92859a94f63107d7805641102e3e55286ad3390651875cc1c0b77984" + }, + { + "path": "research/p112-b6-t4-original-covers/RESULT.json", + "usage": "input", + "git_blob": "bac31b973c01475b76859a62c2b5956b5d156483", + "sha256": "b9fc46f703f0b1fa3227b601805a1fbac4e69610a8106c653dad177c44b93d74" + }, + { + "path": "research/p112-common-deletion-slice/FIXTURE.json", + "usage": "input", + "git_blob": "5014d364542729aa84b359c0905a8293f4cff9a9", + "sha256": "2d8f2cc7bbf02d24d955f43a4880d0225b2cb0e54dce4fe5dcb34ec131649907" + }, + { + "path": "research/p112-common-deletion-slice/geometry.py", + "usage": "input", + "git_blob": "c642dea7477820a2e031e3c4de99b18d92826549", + "sha256": "9c6e8d063837b1543b836ebcf0ed9ea3e1d70ed1b8e553cb0b19cd75bdf18585" + }, + { + "path": "research/p112-common-six-span/PROOF.md", + "usage": "input", + "git_blob": "8ba9d78b89846ae5e70c2eeaab2540ab7f64618a", + "sha256": "c845750bbb4c8447a21f64fe6162e37ddca3b4e6c974539078ed968063f445b4" + }, + { + "path": "research/p112-three-endpoint-sparsity/PROOF.md", + "usage": "input", + "git_blob": "76e0abf1d57f3d3d37ac93bf2fda69c5920fc032", + "sha256": "1e2b43c37240a822886a0f4b550167da2345a671cc01faff41376f5b411b2f25" + } + ] +} diff --git a/research/p112-common-cut23-caller/TASK.json b/research/p112-common-cut23-caller/TASK.json new file mode 100644 index 0000000000..7cc201091a --- /dev/null +++ b/research/p112-common-cut23-caller/TASK.json @@ -0,0 +1,78 @@ +{ + "schema_version": 1, + "task_id": "complex-rank-shape-decoder", + "priority_revision": 6, + "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "original_card": { + "id": "complex-rank-shape-decoder", + "question": "Can a decoder deliver the local paid mass in fewer, larger-rank children (block frame climbs instead of rank-1 to rank-3 steps)?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/complex-local-word-ceiling/README.md", + "research/complex-decoder-field-extension-seed44/README.md", + "research/complex-frame-pair-decoders/README.md", + "research/selected-k8-unrestricted-ends/README.md", + "research/eisenstein-reduction-copy-floor/README.md" + ], + "methods": [ + "Find one exact small decoding identity whose frame path climbs in blocks, and price its complete per-call profile.", + "Bound the best effective child rank achievable for one fixed support alphabet, including copies, frames and restoration." + ], + "acceptance_gate": "A per-call local profile, with all copied information, frames and restoration counted, whose ceiling exceeds the selected word's by at least 5%; masked or overcomplete supports must change an assumption of the eight-term all-pairs bound. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "research/complex-local-word-ceiling/verify.py" + ], + "expected": "PASS_COMPLEX_LOCAL_WORD_CEILING", + "inspect": "Read the selected word's per-call local profile, its packing ceiling and the lever table; run levers.py for the ideal budget of the lever you target.", + "scope": "Positive control and planning budget only; this is not a new construction or full cold replay." + }, + "first_experiment": "Before any synthesis, write the candidate per-call local profile (and centre charge / unpaid coordinates if changed) and screen it with ceiling.ceiling(); reject it if even the ideal ceiling does not beat the selected word's by your stated margin. Ideal budget: rank-16 delivery is 2.31x (levers.py).", + "bottleneck_link": "Rank-1 children are about half of recursive cost; the selected word's effective child rank is about 3.9. Larger-rank delivery lowers recursive cost per unit of paid mass.", + "allowed_variations": [ + "One masked, overcomplete or block decoder family with exact labels and supports.", + "A scoped lower bound on effective rank for one alphabet.", + "If the coverage law, template or guard changes, derive an applicable fully charged replacement bound instead of applying the incumbent ceiling outside its scope." + ], + "scope_change_triggers": [ + "Repacking idle remainders of an unchanged word (covered by the packing ceiling).", + "Repeating the eight-term all-pairs search inside its proved scope.", + "Only changing helper terminal subspaces and monotone frames within the fixed scalar word, entrances and cleanup contract already covered by #1995/#2013.", + "Searching below C=40 in the #2017 Eisenstein binary scalar-rectangle or fixed-support block-linear additive pairing model; specify a changed premise instead. This bound does not cover every complex decoder.", + "Continuing a partial cost improvement while leaving the same unpriced consumer, restoration or central-readout obligation unresolved; refresh the family expansion decision first. Local product-retiming evidence has a narrow scope and is not a ban on changed graphs or contracts." + ], + "overlap_terms": [ + "rank shape", + "block climb", + "masked decoder", + "overcomplete", + "effective rank" + ] + }, + "scope_status": "changed", + "actual_scope": "User-directed C5 caller audit, common-cut23 projective-direction bound and exclusion of the literal independent-piece 2,3,4^2,7^6 caller; conditional fixed-inventory accounting.", + "scope_change_reason": "The assigned application audit finds that actual small supports already exclude normal planes. A bounded root-support intersection lemma closes a named remaining caller without a global normal-plane census.", + "bottleneck_link": "Closes one finite decoder-floor caller obligation. No supplier or kappa improvement is asserted.", + "budget_minutes": 60, + "stop_rule": "Stop after one exact common-cut theorem and caller, relevant controls, source binding, publication and handoff; no new global census.", + "outcome": "completed", + "evidence": "PROOF.md; RESULT.json; verify.py; independent.py; test_controls.py; CHECKS.json", + "author": "Chris R / Clear1nsight, with substantial OpenAI Codex assistance", + "ai_assistance": "Substantial OpenAI Codex assistance for analysis, implementation, checking and publication. Separate implementation is same-session computational corroboration, not independent human review.", + "open_questions": [ + { + "question": "Does independent review confirm the common-cut23 theorem and the six-direction caller transfer?", + "why_it_matters": "Scientific adoption needs review beyond this AI-assisted finite certificate.", + "first_step": "Inspect PROOF.md sections 1-4 and replay both complete finite histograms.", + "blocked_by": "No independent human or proof-kernel review is claimed." + }, + { + "question": "Which current exact contract can handle the literal 4,5^3,6^6 caller?", + "why_it_matters": "It remains uncertified by this explicitly named contract inventory.", + "first_step": "Refresh overlap and bind actual four-small-piece coefficients/supports; the cap44 and residual rank6 already force root normals under the inherited capacity20.", + "blocked_by": "The present theorem covers at most23common sites; actual coefficient/support compatibility and a sufficient root-only theorem are unresolved." + } + ] +} diff --git a/research/p112-common-cut23-caller/VERIFY.json b/research/p112-common-cut23-caller/VERIFY.json new file mode 100644 index 0000000000..1306da7bd7 --- /dev/null +++ b/research/p112-common-cut23-caller/VERIFY.json @@ -0,0 +1,50 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/one-sided-six-multisets/data/data.txt", + "research/p112-b6-t4-original-covers/PROOF.md", + "research/p112-b6-t4-original-covers/RESULT.json", + "research/p112-common-deletion-slice/FIXTURE.json", + "research/p112-common-deletion-slice/geometry.py", + "research/p112-common-six-span/PROOF.md", + "research/p112-three-endpoint-sparsity/PROOF.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 90, + "checks": "Exact source/model binding;43435seven-spaces;5212200root-flat tests;8214570quadruples;positive common-cut fixture;caller inventory." + }, + { + "argv": [ + "{python}", + "-W", + "error", + "-B", + "{package}/independent.py" + ], + "timeout_seconds": 90, + "checks": "Separate lattice, rational label reconstruction, RREF annihilators and pair-join full histograms." + }, + { + "argv": [ + "{python}", + "-W", + "error", + "-B", + "{package}/test_controls.py" + ], + "timeout_seconds": 180, + "checks": "Eight actual optimized rejecting CLI runs, positive optimized export, invalid proof budgets and separate-versus-common deletion boundary." + } + ] +} diff --git a/research/p112-common-cut23-caller/independent.py b/research/p112-common-cut23-caller/independent.py new file mode 100644 index 0000000000..4b83a64242 --- /dev/null +++ b/research/p112-common-cut23-caller/independent.py @@ -0,0 +1,180 @@ +#!/usr/bin/env python3 +"""Separate lattice/RREF/pair-join corroboration; imports no primary routines. + +Same-session computational corroboration, not independent human review. +Chris R / Clear1nsight, with substantial OpenAI Codex assistance. Apache-2.0. +""" + +import ast +from collections import Counter +from fractions import Fraction +import hashlib +from itertools import combinations, product +import json +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +SOURCE_MANIFEST_SHA = "9312885bb9c46b31a199283937b4cf0aec74252f6cd6877f6ef6e27f84f979fb" + + +def check(ok, message): + if not ok: + raise ValueError(message) + + +def authenticated_inputs(): + raw = (HERE / "SOURCES.json").read_bytes() + check(hashlib.sha256(raw).hexdigest() == SOURCE_MANIFEST_SHA, "manifest pin") + result = {} + for row in json.loads(raw)["files"]: + if row["usage"] != "input": + continue + path = ROOT / row["path"] + check(not path.is_symlink() and path.resolve().is_relative_to(ROOT), "input path") + data = path.read_bytes() + check(len(data) <= 2_000_000, "input byte bound") + check(hashlib.sha256(data).hexdigest() == row["sha256"], "input digest") + result[row["path"]] = data + return result + + +def inverse(matrix): + rows = [[Fraction(x) for x in row] + [Fraction(i == j) for j in range(8)] + for i, row in enumerate(matrix)] + for j in range(8): + k = next(i for i in range(j, 8) if rows[i][j]) + rows[j], rows[k] = rows[k], rows[j] + scalar = rows[j][j] + rows[j] = [x / scalar for x in rows[j]] + for i in range(8): + if i != j: + factor = rows[i][j] + rows[i] = [a - factor * b for a, b in zip(rows[i], rows[j])] + return [row[8:] for row in rows] + + +def reconstruct(inputs): + prefix = "research/p112-common-deletion-slice/" + parsed = ast.parse(inputs[prefix + "geometry.py"]) + simple = next(ast.literal_eval(n.value) for n in parsed.body + if isinstance(n, ast.Assign) + and any(isinstance(t, ast.Name) and t.id == "SIMPLE" for t in n.targets)) + # Enumerate the doubled E8 lattice shell, independently of the source generator. + roots = [] + for row in product(range(-2, 3), repeat=8): + if sum(x * x for x in row) != 8 or sum(row) % 4: + continue + if len({x % 2 for x in row}) != 1: + continue + if next(x for x in row if x) > 0: + roots.append(row) + roots.sort() + check(len(roots) == 120, "lattice root shell") + inv = inverse([[simple[j][i] for j in range(8)] for i in range(8)]) + coords = [tuple(sum(inv[i][j] * r[j] for j in range(8)) for i in range(8)) for r in roots] + check(all(x.denominator == 1 for c in coords for x in c), "integral coordinates") + check(all(min(c) >= 0 or max(c) <= 0 for c in coords), "simple-root signs") + frame = {tuple(r) for r in json.loads(inputs[prefix + "FIXTURE.json"])["omitted_frame"]} + live = [r for r in roots if r not in frame] + labels = [256 + sum((int(x) % 2) * 2 ** i for i, x in enumerate(c)) + for r, c in zip(roots, coords) if r not in frame] + check(len(live) == 112 and len(set(labels)) == 112, "live model") + table = inputs["research/one-sided-six-multisets/data/data.txt"].decode().splitlines() + check([tuple(map(int, row.split())) for row in table[2:114]] == live, + "canonical caller root rows") + check(list(map(int, table[0].split())) == [1 + 2 * (label - 256) for label in labels], + "canonical caller label bits") + return roots, live, labels, coords + + +def rref_annihilators(): + rows = [] + for p, q in combinations(range(9), 2): + free = [(0, j) for j in range(p + 1, 9) if j != q] + free += [(1, j) for j in range(q + 1, 9)] + for bits in product((0, 1), repeat=len(free)): + pair = [1 << p, 1 << q] + for (row, j), bit in zip(free, bits): + pair[row] += bit << j + rows.append(tuple(pair)) + check(len(rows) == len(set(rows)) == 43_435, "RREF domain") + return rows + + +def flat_check(roots, live, labels): + chars = [sum((1 << i) for i, label in enumerate(labels) + if bin(a & label).count("1") % 2) for a in range(512)] + flats = [((1 << 112) - 1) - (chars[a] | chars[b]) for a, b in rref_annihilators()] + off = [sum(1 << i for i, r in enumerate(live) if sum(a * b for a, b in zip(r, h))) + for h in roots] + counts = Counter(mask.bit_count() for mask in flats) + maxima = [max((mask & support).bit_count() for mask in flats) for support in off] + check(set(maxima) == {32} and max(counts) == 36, "independent flat capacities") + cuts = Counter((mask.bit_count(), m, mask.bit_count() - m) for mask, m in zip(off, maxima)) + return off, {"seven_flats": len(flats), "global_seven_flat_cap": max(counts), + "flat_size_histogram": {str(k): counts[k] for k in sorted(counts)}, + "root_flat_tests": len(roots) * len(flats), + "root_cut_minima": {",".join(map(str, k)): cuts[k] for k in sorted(cuts)}} + + +def pair_join_check(off): + # Unique ordered split a> j & 1)) for c in coords) + for mask in range(256) if mask.bit_count() <= 6) + check(lower == 36, "independent lower-dimensional chamber cap") + off, flat_summary = flat_check(roots, live, labels) + check(flat_summary == receipt["flat_facts"], "independent flat summary") + check(pair_join_check(off) == receipt["fourfold"]["histogram"], "independent fourfold histogram") + fixture = receipt["positive_fixture"] + common = set(fixture["common_cut_indices"]) + check(len(common) == 22, "fixture common budget") + for h in fixture["directions"]: + residual = [label for i, (r, label) in enumerate(zip(live, labels)) + if i not in common and sum(a * b for a, b in zip(r, h))] + check(rank2(residual) == 7, "independent positive residual") + check(4 * 21 - 3 * 23 == 15 > 14 and 2 + 4 + 8 + 8 == 22 < 53, "proof arithmetic") + prior = json.loads(inputs["research/p112-b6-t4-original-covers/RESULT.json"]) + rows = [tuple(r["weights"]) for r in prior["rows"] if not r["covered"]] + used = {tuple([2, 2, 2] + [7] * 7), tuple([2, 5] + [6] * 8), tuple([2, 3, 4, 4] + [7] * 6)} + check(set(rows) - used == {tuple([4, 5, 5, 5] + [6] * 6)}, "independent caller partition") + check(sum(r["covered"] for r in prior["rows"]) + len(used) == 68, "conditional inventory") + print("PASS_COMMON_CUT23_INDEPENDENT lattice/RREF/pair-join; 8214570 quadruples; conditional68/69") + + +if __name__ == "__main__": + main() diff --git a/research/p112-common-cut23-caller/test_controls.py b/research/p112-common-cut23-caller/test_controls.py new file mode 100644 index 0000000000..00129013cb --- /dev/null +++ b/research/p112-common-cut23-caller/test_controls.py @@ -0,0 +1,148 @@ +#!/usr/bin/env python3 +"""Actual CLI corruption controls and common-cut proof-boundary controls.""" + +import importlib.util +import json +from pathlib import Path +import shutil +import subprocess +import sys +import tempfile + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] + + +def require(ok, message): + if not ok: + raise ValueError(message) + + +def load_checker(): + spec = importlib.util.spec_from_file_location("cut23_controls_target", HERE / "verify.py") + module = importlib.util.module_from_spec(spec) + spec.loader.exec_module(module) + return module + + +def export_to(root): + package = root / "research" / HERE.name + package.mkdir(parents=True) + for path in HERE.iterdir(): + if path.is_file() and not path.is_symlink(): + shutil.copyfile(path, package / path.name) + sources = json.loads((HERE / "SOURCES.json").read_text()) + for row in sources["files"]: + if row["usage"] == "input": + target = root / row["path"] + target.parent.mkdir(parents=True, exist_ok=True) + shutil.copyfile(ROOT / row["path"], target) + return package + + +def run_cli(script, root): + result = subprocess.run([sys.executable, "-I", "-O", "-W", "error", "-B", str(script)], + cwd=root, text=True, capture_output=True, timeout=60) + return result + + +def changed_receipt(package, case): + path = package / "RESULT.json" + receipt = json.loads(path.read_text()) + if case == "understated-fourfold": + receipt["fourfold"]["maximum"] = 13 + elif case == "unproved-direction-bound": + receipt["theorem"]["projective_direction_bound"] = 2 + elif case == "wrong-caller": + receipt["caller"]["new_caller"][0] = 3 + elif case == "boolean-budget": + receipt["theorem"]["cut_budget"] = True + else: + raise ValueError("unknown receipt control") + path.write_text(json.dumps(receipt)) + + +def cli_controls(): + cases = ["source-geometry", "source-frame", "source-inventory", "manifest-usage", + "understated-fourfold", "unproved-direction-bound", "wrong-caller", "boolean-budget"] + with tempfile.TemporaryDirectory(prefix="cut23-controls-") as temporary: + base = Path(temporary) + positive = export_to(base / "positive") + result = run_cli(positive / "verify.py", base / "positive") + require(result.returncode == 0 and "PASS_P112_COMMON_CUT23_CALLER" in result.stdout, + "positive optimized CLI failed: " + result.stderr) + for case in cases: + root = base / case + package = export_to(root) + if case.startswith("source-"): + files = {"source-geometry": "research/p112-common-deletion-slice/geometry.py", + "source-frame": "research/p112-common-deletion-slice/FIXTURE.json", + "source-inventory": "research/p112-b6-t4-original-covers/RESULT.json"} + target = root / files[case] + target.write_bytes(target.read_bytes() + b"\n") + elif case == "manifest-usage": + target = package / "SOURCES.json" + target.write_text(target.read_text().replace('"input"', '"provenance"', 1)) + else: + changed_receipt(package, case) + outcome = run_cli(package / "verify.py", root) + require(outcome.returncode != 0, "CLI accepted corruption: " + case) + expected = "source" if case.startswith("source-") else ( + "source manifest identity" if case == "manifest-usage" else "result receipt mismatch") + require(expected in outcome.stderr, "wrong rejection path: " + case + outcome.stderr) + return len(cases) + + +def proof_controls(): + checker = load_checker() + require(checker.theorem_budget(22)["four_cut_intersection_floor"] == 18, "caller boundary") + failures = [(24, 21, 14), (23, 20, 14), (23, 21, 15), (True, 21, 14)] + for values in failures: + try: + checker.theorem_budget(*values) + except ValueError: + continue + raise ValueError("invalid proof budget accepted") + # Each direction separately passes with its own 21-site cut. Pooling those + # cuts for four independent roots violates the one-common-set allowance. + inputs = checker.authenticate(ROOT) + g, roots, live, labels = checker.model(inputs) + flats, off, _ = checker.flat_facts(g, roots, live, labels) + ids = [2, 13, 17, 44] + require(len(g["echelon"]([roots[i] for i in ids])) == 4, + "separate-cut fixture must contain four independent normals") + cuts = [] + for index in ids: + cut = min((off[index] & ~mask for _, _, mask in flats), key=int.bit_count) + require(cut.bit_count() == 21, "individual deletion fixture") + residual = [labels[i] for i in range(112) if off[index] >> i & 1 and not (cut >> i & 1)] + require(checker.binary_rank(residual) == 7, "separate-cut positive fixture") + cuts.append(cut) + common = cuts[0] | cuts[1] | cuts[2] | cuts[3] + require(common.bit_count() > 23, "separate cuts silently pooled") + # Exercise the actual finite-mathematics gate after authentication, rather + # than counting only receipt/source-hash rejection as semantic coverage. + shared = off[ids[0]] & off[ids[1]] & off[ids[2]] & off[ids[3]] + require(shared.bit_count() == 14, "fourfold attainment fixture") + extra = next(i for i in range(112) if not (shared >> i & 1)) + altered = list(off) + for index in ids: + altered[index] |= 1 << extra + try: + checker.fourfold_facts(roots, altered) + except ValueError as error: + require("fourfold support maximum" in str(error), "wrong semantic rejection") + else: + raise ValueError("fourfold gate accepted an explicit15-site intersection") + return {"rejected_budget_cases": len(failures), "separate_cut_union": common.bit_count(), + "fourfold_semantic_mutations": 1} + + +def main(): + count = cli_controls() + proof = proof_controls() + print("PASS_COMMON_CUT23_CONTROLS", count, "rejecting optimized CLI runs;", proof) + + +if __name__ == "__main__": + main() diff --git a/research/p112-common-cut23-caller/verify.py b/research/p112-common-cut23-caller/verify.py new file mode 100644 index 0000000000..be1fdaaa0b --- /dev/null +++ b/research/p112-common-cut23-caller/verify.py @@ -0,0 +1,227 @@ +#!/usr/bin/env python3 +"""Exact common-cut23 certificate and one historical C5 caller application. + +Chris R / Clear1nsight, with substantial OpenAI Codex assistance. Apache-2.0. +Geometry definitions retain Nick Petalas's PR3163 and E8/P112 lineage. +""" + +import argparse +from collections import Counter +import hashlib +from itertools import combinations +import json +from math import comb +from pathlib import Path + +PACKAGE = Path(__file__).resolve().parent +SOURCE_MANIFEST_SHA = "9312885bb9c46b31a199283937b4cf0aec74252f6cd6877f6ef6e27f84f979fb" +MODEL = "research/p112-common-deletion-slice/" + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def no_duplicates(pairs): + result = {} + for key, value in pairs: + require(key not in result, "duplicate JSON key") + result[key] = value + return result + + +def read_json(path): + raw = path.read_bytes() + require(len(raw) <= 2_000_000, "input size bound") + return json.loads(raw, object_pairs_hook=no_duplicates) + + +def canonical(value): + return json.dumps(value, sort_keys=True, separators=(",", ":")) + + +def authenticate(root): + manifest_raw = (PACKAGE / "SOURCES.json").read_bytes() + require(hashlib.sha256(manifest_raw).hexdigest() == SOURCE_MANIFEST_SHA, + "source manifest identity") + manifest = read_json(PACKAGE / "SOURCES.json") + payloads = {} + for row in manifest["files"]: + if row["usage"] != "input": + continue + path = root / row["path"] + require(path.resolve().is_relative_to(root.resolve()), "input escaped root") + require(all(not parent.is_symlink() for parent in (path, *path.parents) + if parent != root.parent), "source symlink") + raw = path.read_bytes() + require(len(raw) <= 2_000_000, "source size bound") + require(hashlib.sha256(raw).hexdigest() == row["sha256"], "source SHA256") + blob = b"blob " + str(len(raw)).encode() + b"\0" + raw + require(hashlib.sha1(blob).hexdigest() == row["git_blob"], "source Git blob") + payloads[row["path"]] = raw + return payloads + + +def model(payloads): + # Compile the exact authenticated source: no imports or cached bytecode. + namespace = {"__name__": "p112_pinned_geometry"} + raw = payloads[MODEL + "geometry.py"] + exec(compile(raw, MODEL + "geometry.py", "exec"), namespace) + roots = namespace["roots"]() + fixture = json.loads(payloads[MODEL + "FIXTURE.json"]) + frame = {tuple(row) for row in fixture["omitted_frame"]} + live = tuple(row for row in roots if row not in frame) + labels = tuple(namespace["label"](row) for row in live) + require(len(roots) == 120 and len(frame) == 8 and len(live) == 112, "root model") + require(len(set(labels)) == 112 and all(x & 256 for x in labels), "affine labels") + table = payloads["research/one-sided-six-multisets/data/data.txt"].decode().splitlines() + original_labels = tuple(map(int, table[0].split())) + original_roots = tuple(tuple(map(int, row.split())) for row in table[2:114]) + require(original_roots == live, "original caller root coordinates") + require(original_labels == tuple(((x & 255) << 1) | (x >> 8) for x in labels), + "original caller binary-label rotation") + require(all(sum(r[i] * r[j] for r in live) == 112 * (i == j) + for i in range(8) for j in range(8)), "injective evaluation Gram") + namespace["reflection_permutations"](roots) + return namespace, roots, live, labels + + +def chamber_facts(g, roots): + coordinates = [g["coordinates"](r) for r in roots] + supports = [sum(1 << j for j, x in enumerate(c) if x) for c in coordinates] + faces = [sum(s & ~mask == 0 for s in supports) for mask in range(256)] + lower = max(faces[mask] for mask in range(256) if mask.bit_count() <= 6) + seven = [faces[255 ^ (1 << j)] for j in range(8)] + require(lower == 36 and seven == [42, 28, 22, 14, 16, 23, 37, 63], "chamber caps") + mask = sum(1 << i for i, s in enumerate(supports) if s & ~(255 ^ 128) == 0) + normal = g["normals"](roots, mask) + require(len(normal) == 1 and normal[0] in {g["canonical"](r) for r in roots}, + "63-root face must have a root normal") + return {"rank_at_most_six_max": lower, "seven_face_counts": seven, + "root_face_normal": list(normal[0])} + + +def flat_facts(g, roots, live, labels): + all_live = (1 << 112) - 1 + characters = [sum(1 << i for i, label in enumerate(labels) + if (a & label).bit_count() % 2) for a in range(512)] + flats = [(a, b, all_live ^ (characters[a] | characters[b])) + for a in range(1, 512) for b in range(a + 1, 512) if b < (a ^ b)] + require(len(flats) == 43_435, "seven-flat coverage") + histogram = Counter(mask.bit_count() for _, _, mask in flats) + require(max(histogram) == 36, "global rank-seven support cap") + off = [sum(1 << i for i, r in enumerate(live) if g["dot"](r, h)) for h in roots] + maxima = [max((o & mask).bit_count() for _, _, mask in flats) for o in off] + require(set(maxima) == {32}, "root-restricted seven-flat cap") + cuts = Counter((o.bit_count(), m, o.bit_count() - m) for o, m in zip(off, maxima)) + require(dict(cuts) == {(56, 32, 24): 8, (53, 32, 21): 112}, "root cut minima") + return flats, off, { + "seven_flats": len(flats), "global_seven_flat_cap": max(histogram), + "flat_size_histogram": {str(k): histogram[k] for k in sorted(histogram)}, + "root_flat_tests": len(roots) * len(flats), + "root_cut_minima": {",".join(map(str, k)): cuts[k] for k in sorted(cuts)}, + } + + +def fourfold_facts(roots, off): + histogram = Counter() + witness = None + for a, b, c, d in combinations(range(120), 4): + size = (off[a] & off[b] & off[c] & off[d]).bit_count() + histogram[size] += 1 + if size == 14 and witness is None: + witness = [a, b, c, d] + require(sum(histogram.values()) == comb(120, 4) == 8_214_570, "fourfold coverage") + require(max(histogram) == 14 and witness is not None, "fourfold support maximum") + return {"quadruples": sum(histogram.values()), "maximum": max(histogram), + "histogram": {str(k): histogram[k] for k in sorted(histogram)}, + "witness_indices": witness, "witness_roots": [list(roots[i]) for i in witness]} + + +def binary_rank(values): + basis = {} + for value in values: + while value: + pivot = value.bit_length() + if pivot not in basis: + basis[pivot] = value + break + value ^= basis[pivot] + return len(basis) + + +def positive_fixture(g, roots, live, labels, flats, off): + directions = [(0, 0, 0, 0, 0, 2, -2, 0), (0, 0, 0, 0, 0, 2, 2, 0)] + annihilators = [(65, 257), (64, 257)] + lookup = {(a, b): mask for a, b, mask in flats} + cuts = [off[roots.index(h)] & ~lookup[ab] for h, ab in zip(directions, annihilators)] + common = cuts[0] | cuts[1] + ranks = [binary_rank([labels[i] for i, r in enumerate(live) + if g["dot"](r, h) and not (common >> i & 1)]) for h in directions] + require(common.bit_count() == 22 and ranks == [7, 7], "two-direction positive fixture") + require(len(g["echelon"](directions)) == 2, "positive fixture independence") + return {"directions": [list(h) for h in directions], + "annihilators": [list(ab) for ab in annihilators], + "common_cut_indices": [i for i in range(112) if common >> i & 1], + "residual_ranks": ranks} + + +def theorem_budget(cut_budget, live_cut_minimum=21, fourfold_maximum=14): + require(type(cut_budget) is int and 0 <= cut_budget <= 23, "uncertified cut budget") + intersection_floor = 4 * live_cut_minimum - 3 * cut_budget + require(intersection_floor > fourfold_maximum, "no four-direction contradiction") + return {"cut_budget": cut_budget, "four_cut_intersection_floor": intersection_floor, + "fourfold_maximum": fourfold_maximum, "projective_direction_bound": 3} + + +def caller_audit(payloads): + prior = json.loads(payloads["research/p112-b6-t4-original-covers/RESULT.json"]) + require(prior["historical"] == len(prior["rows"]) == 69 and prior["combined"] == 65, + "historical inventory identity") + inherited = [row["weights"] for row in prior["rows"] if row["covered"]] + require(len(inherited) == 65, "inherited covered flags") + successors = [[2, 2, 2] + [7] * 7, [2, 5] + [6] * 8] + target = [2, 3, 4, 4] + [7] * 6 + remaining = [4, 5, 5, 5] + [6] * 6 + require(prior["inventory_uncertified"] == [successors[0], target, successors[1], remaining], + "named caller binding") + cap = sum(2 ** (w - 1) for w in target[:4]) + require(cap == 22 < 53 and len(target) - 6 == 4, "caller quotient budget") + return {"historical_rows": 69, "inherited_contract_coverage": len(inherited), + "successor_contract_rows": successors, "coverage_before_new_lemma": 67, + "new_caller": target, "small_support_cap": cap, "required_directions": 6, + "direction_bound": 3, "conditional_inventory_coverage": 68, + "inventory_uncertified": [remaining], + "scope": "Fixed named contract inventory, not a global unresolved count."} + + +def compute(root): + payloads = authenticate(root) + g, roots, live, labels = model(payloads) + chamber = chamber_facts(g, roots) + flats, off, flat_summary = flat_facts(g, roots, live, labels) + return {"schema": "p112-common-cut23-caller/v1", "chamber": chamber, + "flat_facts": flat_summary, "fourfold": fourfold_facts(roots, off), + "positive_fixture": positive_fixture(g, roots, live, labels, flats, off), + "theorem": theorem_budget(23), "caller": caller_audit(payloads)} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--repository", type=Path, default=PACKAGE.parents[1]) + parser.add_argument("--write-result", type=Path, help="Explicit receipt generation only") + args = parser.parse_args() + result = compute(args.repository) + if args.write_result is not None: + require(not args.write_result.exists(), "refuse to overwrite a receipt") + args.write_result.write_text(json.dumps(result, indent=2) + "\n") + else: + require(canonical(result) == canonical(read_json(PACKAGE / "RESULT.json")), + "result receipt mismatch") + print("PASS_P112_COMMON_CUT23_CALLER flats=43435 root_flat_tests=5212200 " + "quadruples=8214570 bound=3 caller_excluded=true conditional_inventory=68/69") + + +if __name__ == "__main__": + main() From ce148e5aa2bbdc6f420e8a6cf6935e37d5b54cd2 Mon Sep 17 00:00:00 2001 From: Chris R Date: Mon, 19 Oct 2026 15:36:14 +1100 Subject: [PATCH 2/3] fix(actions): apply existing P112 runner-context repair Carry the focused change from 89031d21f01f8b676f87c76443f5afc41457a17c (PR #8) onto this active branch. Initialise TMPDIR after runner setup, preserving workflow triggers, repository guard, permissions, pinned actions, timeouts, replay commands and all research inputs. Validated YAML, exact semantic delta, shell syntax and TMPDIR assignment including spaces. Substantial OpenAI assistance. --- .github/workflows/p112-common-slice.yml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/.github/workflows/p112-common-slice.yml b/.github/workflows/p112-common-slice.yml index 37f99ca573..48047f61c4 100644 --- a/.github/workflows/p112-common-slice.yml +++ b/.github/workflows/p112-common-slice.yml @@ -15,9 +15,9 @@ jobs: if: github.repository == 'CrocSwap/integer-mult-bounds' runs-on: ubuntu-24.04 timeout-minutes: 20 - env: - TMPDIR: ${{ runner.temp }}/p112-common-slice steps: + - name: Initialise P112 work directory + run: echo "TMPDIR=$RUNNER_TEMP/p112-common-slice" >> "$GITHUB_ENV" - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 with: fetch-depth: 0 From 33b6be488be1e9e38f2f3f9bcfc4a7db0e8a332d Mon Sep 17 00:00:00 2001 From: Chris R Date: Mon, 19 Oct 2026 16:45:14 +1100 Subject: [PATCH 3/3] Audit the C5 common-cut proof and credit PR3295's existing caller exclusion Add a code-disjoint table/Fourier check and detailed written proof audit. Reconcile the literal 4,5^3,6^6 row with Nick Petalas's existing PR3295, giving conditional69/69 coverage only in the named historical inventory. Preserve all original scientific and predecessor bytes. No full C5, supplier, kappa or selected-frontier change. Fresh registered audit/controls and original PR3931/3295 registered replays pass. Substantial OpenAI Codex assistance; same-author audit, no independent human/model or proof-kernel acceptance. --- research/p112-c5-followup-audit/AUDIT.md | 166 ++++++++++++++++ research/p112-c5-followup-audit/CHECKS.json | 123 ++++++++++++ research/p112-c5-followup-audit/README.md | 41 ++++ research/p112-c5-followup-audit/RESULT.json | 42 ++++ research/p112-c5-followup-audit/SOURCES.json | 72 +++++++ research/p112-c5-followup-audit/TASK.json | 78 ++++++++ research/p112-c5-followup-audit/VERIFY.json | 43 ++++ research/p112-c5-followup-audit/test_audit.py | 72 +++++++ research/p112-c5-followup-audit/verify.py | 187 ++++++++++++++++++ 9 files changed, 824 insertions(+) create mode 100644 research/p112-c5-followup-audit/AUDIT.md create mode 100644 research/p112-c5-followup-audit/CHECKS.json create mode 100644 research/p112-c5-followup-audit/README.md create mode 100644 research/p112-c5-followup-audit/RESULT.json create mode 100644 research/p112-c5-followup-audit/SOURCES.json create mode 100644 research/p112-c5-followup-audit/TASK.json create mode 100644 research/p112-c5-followup-audit/VERIFY.json create mode 100644 research/p112-c5-followup-audit/test_audit.py create mode 100644 research/p112-c5-followup-audit/verify.py diff --git a/research/p112-c5-followup-audit/AUDIT.md b/research/p112-c5-followup-audit/AUDIT.md new file mode 100644 index 0000000000..75987aae8d --- /dev/null +++ b/research/p112-c5-followup-audit/AUDIT.md @@ -0,0 +1,166 @@ +# Proof audit and correction of the next caller + +This is a fresh, same-author AI-assisted audit of PR3931 at +`ce148e5aa2bbdc6f420e8a6cf6935e37d5b54cd2`. It is independently inspectable +evidence, not an independent human/model review or proof-kernel certificate. +No objection to the common-cut theorem or its literal caller implication was +found. The important correction is research overlap: PR3295 already excludes +the suggested next caller `4,5^3,6^6`, conditional on its stated premises. +The original scientific package is retained byte-for-byte, including its +historical 68/69 named-inventory receipt and superseded follow-up suggestion. + +## PR3931: finite facts and written implication + +The new executable imports no predecessor geometry or checker. It parses the +original canonical caller table, adds the eight literal omitted frame roots, +checks the complete elementary E8 root patterns, and solves the simple-root +coordinates by dense Fraction elimination. It uses the original affine-bit-zero +labels directly. It checks positivity, the evaluation Gram matrix `112 I_8`, +960 simple-reflection images, parabolic face counts and the unique E7 root +normal. These are finite facts, with the standard E8 Weyl-chamber theorem +remaining an explicit mathematical dependency. + +For a support A define its binary character spectrum + + F_A(a) = sum_(t in A) (-1)^(a dot ell(t)). + +For two independent characters a,b, exact character orthogonality gives + + |A intersect ker(a) intersect ker(b)| + = (|A| + F_A(a) + F_A(b) + F_A(a XOR b))/4. + +The three nonzero characters of a two-dimensional annihilator form one +sorted triple, so `a1, a real point of N can additionally avoid the finitely many120 +root lines, while keeping that zero pattern. This contradicts the real +classification. Thus dim(N)=1 and scalar extension contains the original +field-valued normal. No real ordering or Hermitian pairing is assumed for K. +The same argument at support<70 proves the root-only classification and +distance53 used in the quotient step. + +The common-set inequality has the correct quantifier. Live roots need at +least53-32=21 deletions, frame roots need56-32=24 and cannot qualify. Four +distinct qualifying root lines under ONE S of size23 would have joint +off-intersection at least4*21-3*23=15, contradicting14. Four different cuts +would not prove this. The statement is an upper bound of three lines; this +audit supplies no three-line attainment or sharpness of23. + +The literal `2,3,4,4,7^6` caller transfer is also sound. Its four small +supports occupy at most22<53 sites. Their quotient images are independent: +a nonzero relation would be a nonzero codeword of support at most22. Since +the quotient has dimension at most4, these images form a basis and its +dimension is exactly4. Subtracting their unique lifts from the six other +pieces produces six independent codewords. Outside their ONE common small +support union, those codewords have binary support rank at most7. Evaluation +injectivity gives six independent directions, contradicting the theorem. + +## Existing PR3295 already covers 4,5^3,6^6 + +The exact public predecessor is Nick Petalas's +[PR3295](https://github.com/CrocSwap/integer-mult-bounds/pull/3295), head +`4cff8128f0f9ea1e61515b95ddbb884366e9362c`. All16 changed Git blobs match +canonical main `20ecf2891d80b5acf18d980b2164fb44ea7faa90` byte-for-byte. +The central ledger records archival intake as **partially reviewed**, which +must not be interpreted as mathematical approval. Its proof and receipt are +live source-bound inputs to this audit. Its existing registered primary, +separate generating-basis checker and ten behavioral groups all pass here. + +The proof's six-piece statement is stronger than the requested caller: +pieces of ranks at most4,5,5,5,6,6 have code-intersection dimension at most1. +The normal-plane reduction and incidence/concentration argument withstand +written review, conditional on the explicit inherited global12/20 capacities, +all-A2 joint22/32 bounds and standard Weyl-chamber theorem: + +1. Two independent codewords in the six-piece span have union at most84. + Their at least28 common perpendicular live roots span rank6: smaller + parabolic rank allows at most20 root lines. The only qualifying six-node + types are D6 and E6. Rational rank and a generic real normal justify the + same reduction over every characteristic-zero field. +2. In E6 a fixed coefficient column forces each piece's singleton sites into + one projective fiber. Thus required incidence is at least2*78=156, while + the inherited joint bounds permit at most16+3*22+2*32=146. Overlaps and + cancellations only consume more incidence, so do not defeat the bound. +3. In D6 the live union is82 or84. With capacities c=(8,12,12,12,20,20), the + deficit identity bounds total missing capacity, outside-union incidence + and overlap excess by D=84-|U|<=2. For each piece i its nonsingleton + incidences are at most the total overlap excess, hence J_i>=c_i-D. + The five rank5/6 pieces therefore have at least10/18 singleton sites. +4. A rank5/6 piece with that many singleton axis labels has its whole + support in that axis. Arbitrary ambient spaces are covered: ten affine + labels span rank5 and eighteen span rank6, so their ambient span lies in + the axis eight-space. The complete concentration census applies. Small + fibers allow only8/12 sites, so cannot hold those singleton counts. + The five pieces thus lie entirely on the large axes, leaving at least22 + small-fiber sites for the rank4 piece, whose capacity is8. Contradiction. +5. Delete any four of the original six rank6 pieces. The retained span has + codimension4, so code dimension at least6 would leave at least2 in the + retained6-piece span, contradicting the lemma. Independence is sufficient; + there is no assumed disjointness, fixed coefficient value or arbitrary-cut + relaxation in this dimension argument. + +The PR3295 replay rechecks its new concentration and transport facts; it +authenticates, but does not reprove, the inherited global and A2 bounds. +This session likewise does not independently reprove or rerun that entire +inherited source chain. Source hashes and passing programs are not universal +theorem acceptance. + +## Corrected conditional accounting and next research decision + +Within PR3289's fixed historical inventory, the composition is65 original +contracts + PR3322 (`2^3,7^7`) + PR3405 (`2,5,6^8`) + PR3931 +(`2,3,4^2,7^6`) + the existing PR3295 (`4,5^3,6^6`) = **69/69**. +This is a conditional partition of exactly that named inventory, not a +global unresolved count, full C5, a decoder floor or supplier admission. +The last caller exclusion belongs to PR3295, not this audit or PR3931. + +The broader uniform normal-plane question remains unsettled by this work. +This now-complete conditional inventory supplies no remaining gap that needs +it. Before another census, identify a different literal TWOSIDE caller and +bind its quotient, capacities, common-set quantifier and required span bound. +Otherwise the useful next task is independent review of the inherited +universal premises and this finite-to-field argument. No new search is reserved. + +## Evidence, limits and credit + +PR3931 upstream registered CI run39200317292 at head ce148e5 passed on +2026-10-19 at04:48:12UTC. Both plan and replay succeeded; its log contains +the three package PASS markers and outcome=completed. CI does not prove the +written universal arguments. That result concerns the pre-audit head, not a +later follow-up commit's hosted status. + +New Fourier/table replay and controls are registered in VERIFY.json. The +controls compare every43,435 dual space to direct membership for four literal +supports (173,740 comparisons), reject four semantic faults, and run three +actual optimized rejecting CLI corruptions on private copies. CHECKS.json +records source/publication/export evidence as obtained. + +Entry overlap:643 distinct open PR bodies, including drafts, seven REST pages +plus an empty eighth;2,487 local README/ledger records through the repository +helper. Browser-loaded latest C5 replies and handoffs were checked. The helper +could not refresh Discussions without gh; broader Discussion/diff/closed/ +unpublished coverage is partial. The local overlap corpus itself surfaced +PR3295 and the later mixed566-cut32 package that explicitly cites it. The +earlier PR3931 follow-up overlooked that public predecessor; this correction +preserves the original record and credits the actual theorem. + +Credit Nick Petalas/PR3295 and PR3278/3267/3260/3262/3269, PR3283's related +concentration lemma, PR3286's quantifier control, PR3282/3289's accounting, +PR3322 and PR3405's other caller exclusions, DreamingOfClouds/PR3154, +joaqcoo and the retained E8/P112 lineage. The common-cut23 theorem and this +follow-up are by Chris R / Clear1nsight with substantial OpenAI Codex +assistance. No independent human/model or kernel review is claimed. +Full C5, the inherited complete scientific suites, selected cold replay, +physical/native/restoration/consumer/supplier/all-size obligations, Lean and +Docker remain outside this audit. No selected-frontier change or new kappa. diff --git a/research/p112-c5-followup-audit/CHECKS.json b/research/p112-c5-followup-audit/CHECKS.json new file mode 100644 index 0000000000..e1c95126fb --- /dev/null +++ b/research/p112-c5-followup-audit/CHECKS.json @@ -0,0 +1,123 @@ +{ + "schema": "p112-c5-followup-checks/v1", + "environment": { + "python": "3.12.3", + "platform": "Linux-7.0.0-38-generic-x86_64-with-glibc2.39" + }, + "original_PR3931_head": "ce148e5aa2bbdc6f420e8a6cf6935e37d5b54cd2", + "upstream_CI": { + "run": 39200317292, + "head": "ce148e5aa2bbdc6f420e8a6cf6935e37d5b54cd2", + "completed_at": "2026-10-19T04:48:12Z", + "conclusion": "success", + "jobs": [ + "plan", + "replay (research/p112-common-cut23-caller)" + ], + "log_markers": [ + "PASS_P112_COMMON_CUT23_CALLER", + "PASS_COMMON_CUT23_INDEPENDENT", + "PASS_COMMON_CUT23_CONTROLS", + "PASS_REGISTERED_RESEARCH_PACKAGE outcome=completed" + ], + "scope": "Original PR head only; a later audit commit requires its own CI result." + }, + "bounded_replays": { + "p112-common-cut23-caller": "PASS all three original registered commands", + "p112-six-piece-concentration": "PASS primary, separate generating-basis checker and all ten behavioral groups", + "p112-c5-followup-audit": "PASS fresh Fourier/table audit and semantic/primal/actual optimized CLI controls" + }, + "PR3295_source_binding": { + "head": "4cff8128f0f9ea1e61515b95ddbb884366e9362c", + "canonical_main": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "files_checked": [ + { + "path": "research/p112-six-piece-concentration/BASIS-CHECK.json", + "sha": "1e2822b565909dde005ebd988a36bc8047242271" + }, + { + "path": "research/p112-six-piece-concentration/CHECKS.json", + "sha": "aead13d2f036b2bb2511a6aeaefe9699a8b97cee" + }, + { + "path": "research/p112-six-piece-concentration/ENGINEERING.md", + "sha": "efec4f6a8c7e5f982f0a4131bcbed9dfaa195896" + }, + { + "path": "research/p112-six-piece-concentration/PREDECESSORS.json", + "sha": "b5bbae7cc633482fb7c14b00b0f3db8f6bbe4d74" + }, + { + "path": "research/p112-six-piece-concentration/PROOF.md", + "sha": "0728c80d3140b9e0a7d62ffc540d0313ef578eea" + }, + { + "path": "research/p112-six-piece-concentration/README.md", + "sha": "db56b0bbffa8862e43932d69ebb7a7a1bff2d40f" + }, + { + "path": "research/p112-six-piece-concentration/RESULT.json", + "sha": "d68a5599732bc44503a9c56b1f2c54caed98ace5" + }, + { + "path": "research/p112-six-piece-concentration/SOURCES.json", + "sha": "ae564a10d52e473bc2fa4d42ee938ec0deefa15e" + }, + { + "path": "research/p112-six-piece-concentration/TASK.json", + "sha": "ea31a85c41ab910189b953f1233784c9541c7063" + }, + { + "path": "research/p112-six-piece-concentration/VERIFY.json", + "sha": "8a792ea8d64e970a47c0e5d65f2311c7b88127ff" + }, + { + "path": "research/p112-six-piece-concentration/independent.py", + "sha": "2c0f10b5f4a72dabc504e4b2b9b6433ba7fae147" + }, + { + "path": "research/p112-six-piece-concentration/model.py", + "sha": "ce2a4c6c85b555eff21d17409cbf0c7f706141bd" + }, + { + "path": "research/p112-six-piece-concentration/predecessors/PR3278-PROOF.md", + "sha": "bedfda2d1d6babed32eb0abd349723b80a48dfb6" + }, + { + "path": "research/p112-six-piece-concentration/predecessors/PR3282-PROOF.md", + "sha": "d1a2b2057f04120f2661f72bab9c3b1294d35448" + }, + { + "path": "research/p112-six-piece-concentration/test_verify.py", + "sha": "cb8eb9d667cbf2edae644dce4c5ef7c33846a9f2" + }, + { + "path": "research/p112-six-piece-concentration/verify.py", + "sha": "e1ad5d74370cdb6c0f0c797cc2d31c63e234bab0" + } + ], + "result": "All16 PR file Git blobs match canonical main; existing ledger status partially reviewed." + }, + "new_checks": { + "dual_spaces": 43435, + "root_flat_pairs": 5212200, + "fourfold_subsets": 8214570, + "primal_membership_oracle_comparisons": 173740, + "semantic_rejections": 4, + "actual_optimized_CLI_rejections": 3 + }, + "entry_overlap": { + "at": "2026-10-19T05:34:58Z", + "open_PR_bodies": 643, + "complete_PR_pagination": true, + "local_records": 2487, + "Discussion_coverage": "Partial; latest loaded C5 and handoff text inspected, all-board helper refresh unavailable without gh." + }, + "evidence_status": "Fresh same-author AI-assisted audit; no independent human/model or proof-kernel review.", + "unrun_obligations": [ + "Independent reproof and complete replay of inherited global12/20 and all-A2 joint22/32 premises", + "Full C5 and global decoder-floor adoption", + "Independent human/model or formal-kernel acceptance", + "Selected cold replay, physical/native/consumer/restoration/supplier/all-size admission, Lean and Docker" + ] +} diff --git a/research/p112-c5-followup-audit/README.md b/research/p112-c5-followup-audit/README.md new file mode 100644 index 0000000000..1b19006299 --- /dev/null +++ b/research/p112-c5-followup-audit/README.md @@ -0,0 +1,41 @@ +# C5 proof audit and predecessor reconciliation + +The fresh table/Fourier checker reproduces PR3931's complete seven-flat and +fourfold histograms. Written review finds no objection to its characteristic-zero +common-cut23 theorem or `2,3,4^2,7^6` caller transfer. This is a same-author +AI-assisted audit, not independent human/model or proof-kernel verification. + +The key correction: **Nick Petalas's PR3295 already conditionally excludes +`4,5^3,6^6`**. Its registered replay passes here. The named historical contract +inventory composes to **69/69**, conditional on the inherited theorems; this +is not full C5 or a global unresolved count. The original scientific package +and its historical68/69 receipt stay unchanged. [AUDIT.md](AUDIT.md) supplies +the detailed proof review, exact predecessor credit and coverage limits. + +## Reproduce + +```sh +python3.12 -I -Werror -B scripts/research_package.py --package research/p112-c5-followup-audit +``` + +Standard library only. SOURCES.json pins the exact public head/base and all +live input bytes; VERIFY.json declares both bounded commands. The primary +imports no predecessor executable. Its character-sum method and173,740 direct +membership controls test the flat calculation by a different method. The +fourfold enumeration remains a direct complete corroboration. Three actual +optimized CLI mutations on private copies must fail. CHECKS.json records the +separate PR3931/3295 replays, CI scope, source binding and publication evidence. + +## Open next questions + +Independent review of the standard Weyl/scalar-extension implication and +inherited global12/20 and A2 joint22/32 premises would strengthen adoption. +The complete inherited scientific chain was not rerun or independently proved. +Before expanding the uniform normal-plane census, bind a different literal C5 +caller whose actual quotient and common-set budget need that stronger statement. +No such new gap is established here, and no further research claim is reserved. + +Credit Nick Petalas/PR3295 and its retained source chain, PR3282/3289, PR3322, +PR3405, DreamingOfClouds/PR3154, joaqcoo and the E8/P112 lineage. New material +by Chris R / Clear1nsight with substantial OpenAI Codex assistance, Apache-2.0. +No full C5, physical supplier, selected-frontier change or new kappa is claimed. diff --git a/research/p112-c5-followup-audit/RESULT.json b/research/p112-c5-followup-audit/RESULT.json new file mode 100644 index 0000000000..f75a87fc1a --- /dev/null +++ b/research/p112-c5-followup-audit/RESULT.json @@ -0,0 +1,42 @@ +{ + "schema": "p112-c5-followup-audit/v1", + "flats": 43435, + "root_flat_tests": 5212200, + "quadruples": 8214570, + "flat_size_histogram": { + "0": 255, + "16": 7, + "20": 336, + "22": 3584, + "24": 3752, + "26": 10752, + "28": 6416, + "30": 10752, + "32": 3549, + "34": 3584, + "36": 448 + }, + "fourfold_histogram": { + "0": 154056, + "1": 12544, + "2": 127008, + "3": 698880, + "4": 2383164, + "5": 901824, + "6": 1952160, + "7": 1046528, + "8": 354774, + "9": 275520, + "10": 168000, + "11": 10752, + "12": 21840, + "13": 86016, + "14": 21504 + }, + "common_cut_bound": 3, + "common_cut_budget": 23, + "fixed_inventory_conditional_coverage": 69, + "fixed_inventory_rows": 69, + "existing_last_caller_source": "PR3295 / 4cff8128f0f9ea1e61515b95ddbb884366e9362c", + "scope": "Conditional contract composition; no full C5 or human/kernel review." +} diff --git a/research/p112-c5-followup-audit/SOURCES.json b/research/p112-c5-followup-audit/SOURCES.json new file mode 100644 index 0000000000..d1bda3b997 --- /dev/null +++ b/research/p112-c5-followup-audit/SOURCES.json @@ -0,0 +1,72 @@ +{ + "schema_version": 1, + "base_commit": "ce148e5aa2bbdc6f420e8a6cf6935e37d5b54cd2", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81", + "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "67f085acd86acd7d4e03922d9cf4b26bca66fed5", + "sha256": "47b42433f5a85809a3aadd29c2c339da2c6ed728e4f7762df6b88bccb7874cf0" + }, + { + "path": "research/one-sided-six-multisets/data/data.txt", + "usage": "input", + "git_blob": "dc591a4e0252bac096e6c63c51058f6caee66bfe", + "sha256": "ac4a48851b922f2a433684b60c74768ae3bb4fc5e8990ffe63e3942bb3c2ea34" + }, + { + "path": "research/p112-b6-t4-original-covers/RESULT.json", + "usage": "input", + "git_blob": "bac31b973c01475b76859a62c2b5956b5d156483", + "sha256": "b9fc46f703f0b1fa3227b601805a1fbac4e69610a8106c653dad177c44b93d74" + }, + { + "path": "research/p112-common-cut23-caller/PROOF.md", + "usage": "input", + "git_blob": "95a1eb206047ef3fef64439545b995c5467e1d43", + "sha256": "fefcda2bf96571187bdd3b3b2b79d7118a1f2ca9dcd97e7a2924893710509140" + }, + { + "path": "research/p112-common-cut23-caller/RESULT.json", + "usage": "input", + "git_blob": "93142d0d9f0f71ab362923b248ac83f35423e8a3", + "sha256": "a46ec0eb1cb30f6a15c48038ce9691b9ef315fd6a5c375f016d95474e64ccf57" + }, + { + "path": "research/p112-common-six-span/PROOF.md", + "usage": "input", + "git_blob": "8ba9d78b89846ae5e70c2eeaab2540ab7f64618a", + "sha256": "c845750bbb4c8447a21f64fe6162e37ddca3b4e6c974539078ed968063f445b4" + }, + { + "path": "research/p112-six-piece-concentration/PREDECESSORS.json", + "usage": "input", + "git_blob": "b5bbae7cc633482fb7c14b00b0f3db8f6bbe4d74", + "sha256": "9fcedfae4643212ba8d96da858822f7f41a0627e0e744c7ee73707d16d2fa33e" + }, + { + "path": "research/p112-six-piece-concentration/PROOF.md", + "usage": "input", + "git_blob": "0728c80d3140b9e0a7d62ffc540d0313ef578eea", + "sha256": "41bbe6ec7dca13b734579883911bcfc9d3e9fca90b8b6cf2a3448a10786eede3" + }, + { + "path": "research/p112-six-piece-concentration/RESULT.json", + "usage": "input", + "git_blob": "d68a5599732bc44503a9c56b1f2c54caed98ace5", + "sha256": "584d255ed86a5bbed34f494acca025dc9ce5ea9573e2727b32d954bc68dd2b50" + }, + { + "path": "research/p112-three-endpoint-sparsity/PROOF.md", + "usage": "input", + "git_blob": "76e0abf1d57f3d3d37ac93bf2fda69c5920fc032", + "sha256": "1e2b43c37240a822886a0f4b550167da2345a671cc01faff41376f5b411b2f25" + } + ] +} diff --git a/research/p112-c5-followup-audit/TASK.json b/research/p112-c5-followup-audit/TASK.json new file mode 100644 index 0000000000..0bd28cb086 --- /dev/null +++ b/research/p112-c5-followup-audit/TASK.json @@ -0,0 +1,78 @@ +{ + "schema_version": 1, + "task_id": "complex-rank-shape-decoder", + "priority_revision": 6, + "base_commit": "ce148e5aa2bbdc6f420e8a6cf6935e37d5b54cd2", + "original_card": { + "id": "complex-rank-shape-decoder", + "question": "Can a decoder deliver the local paid mass in fewer, larger-rank children (block frame climbs instead of rank-1 to rank-3 steps)?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/complex-local-word-ceiling/README.md", + "research/complex-decoder-field-extension-seed44/README.md", + "research/complex-frame-pair-decoders/README.md", + "research/selected-k8-unrestricted-ends/README.md", + "research/eisenstein-reduction-copy-floor/README.md" + ], + "methods": [ + "Find one exact small decoding identity whose frame path climbs in blocks, and price its complete per-call profile.", + "Bound the best effective child rank achievable for one fixed support alphabet, including copies, frames and restoration." + ], + "acceptance_gate": "A per-call local profile, with all copied information, frames and restoration counted, whose ceiling exceeds the selected word's by at least 5%; masked or overcomplete supports must change an assumption of the eight-term all-pairs bound. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "research/complex-local-word-ceiling/verify.py" + ], + "expected": "PASS_COMPLEX_LOCAL_WORD_CEILING", + "inspect": "Read the selected word's per-call local profile, its packing ceiling and the lever table; run levers.py for the ideal budget of the lever you target.", + "scope": "Positive control and planning budget only; this is not a new construction or full cold replay." + }, + "first_experiment": "Before any synthesis, write the candidate per-call local profile (and centre charge / unpaid coordinates if changed) and screen it with ceiling.ceiling(); reject it if even the ideal ceiling does not beat the selected word's by your stated margin. Ideal budget: rank-16 delivery is 2.31x (levers.py).", + "bottleneck_link": "Rank-1 children are about half of recursive cost; the selected word's effective child rank is about 3.9. Larger-rank delivery lowers recursive cost per unit of paid mass.", + "allowed_variations": [ + "One masked, overcomplete or block decoder family with exact labels and supports.", + "A scoped lower bound on effective rank for one alphabet.", + "If the coverage law, template or guard changes, derive an applicable fully charged replacement bound instead of applying the incumbent ceiling outside its scope." + ], + "scope_change_triggers": [ + "Repacking idle remainders of an unchanged word (covered by the packing ceiling).", + "Repeating the eight-term all-pairs search inside its proved scope.", + "Only changing helper terminal subspaces and monotone frames within the fixed scalar word, entrances and cleanup contract already covered by #1995/#2013.", + "Searching below C=40 in the #2017 Eisenstein binary scalar-rectangle or fixed-support block-linear additive pairing model; specify a changed premise instead. This bound does not cover every complex decoder.", + "Continuing a partial cost improvement while leaving the same unpriced consumer, restoration or central-readout obligation unresolved; refresh the family expansion decision first. Local product-retiming evidence has a narrow scope and is not a ban on changed graphs or contracts." + ], + "overlap_terms": [ + "rank shape", + "block climb", + "masked decoder", + "overcomplete", + "effective rank" + ] + }, + "scope_status": "changed", + "actual_scope": "User-directed fresh audit of PR3931, CI check, then reconciliation of existing PR3295 exclusion of4,5^3,6^6. Fresh Fourier/table implementation and conditional named69/69 inventory.", + "scope_change_reason": "Overlap found an existing exact caller exclusion; audit it and correct the stale next-task guidance instead of duplicating its search.", + "bottleneck_link": "Specific decoder-floor proof audit and predecessor reconciliation; no supplier construction or kappa improvement.", + "budget_minutes": 60, + "stop_rule": "Stop after source/proof audit, bounded replays, independently reviewable correction and handoff; no new global census or selected change.", + "outcome": "completed", + "evidence": "README.md; RESULT.json; verify.py; test_audit.py; CHECKS.json", + "author": "Chris R / Clear1nsight", + "ai_assistance": "Substantial OpenAI Codex assistance. Fresh code and written audit are same-author AI-assisted checking, not independent human/model or proof-kernel review.", + "open_questions": [ + { + "question": "Does independent human or proof-kernel review confirm the characteristic-zero proof and the inherited successor premises?", + "why_it_matters": "Source authentication and executable replay do not discharge inherited universal theorems.", + "first_step": "Audit the rational-kernel/Weyl implication and PR3295 inherited global12/20 and A2 joint22/32 bounds, using exact source heads.", + "blocked_by": "This session checks the new finite facts and written composition; inherited global/A2 premises remain conditional." + }, + { + "question": "Which literal C5 caller outside this fixed69-row inventory still needs a uniform normal-plane theorem?", + "why_it_matters": "The present named inventory is conditionally complete, so it does not motivate a duplicate census.", + "first_step": "Bind a current TWOSIDE caller, quotient dimension and one common set before enumerating any larger geometric domain.", + "blocked_by": "No such additional caller is established here; full C5 is not inferred." + } + ] +} diff --git a/research/p112-c5-followup-audit/VERIFY.json b/research/p112-c5-followup-audit/VERIFY.json new file mode 100644 index 0000000000..421103cc95 --- /dev/null +++ b/research/p112-c5-followup-audit/VERIFY.json @@ -0,0 +1,43 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/one-sided-six-multisets/data/data.txt", + "research/p112-b6-t4-original-covers/RESULT.json", + "research/p112-common-cut23-caller/PROOF.md", + "research/p112-common-cut23-caller/RESULT.json", + "research/p112-common-six-span/PROOF.md", + "research/p112-six-piece-concentration/PREDECESSORS.json", + "research/p112-six-piece-concentration/PROOF.md", + "research/p112-six-piece-concentration/RESULT.json", + "research/p112-three-endpoint-sparsity/PROOF.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-O", + "-Werror", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 90, + "checks": "No predecessor executable imports: original caller table, exact coordinates and Gram/reflection/chamber facts, Fourier character-sum caps, full fourfold histogram and source-bound conditional69/69 contract partition." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-Werror", + "-B", + "{package}/test_audit.py" + ], + "timeout_seconds": 120, + "checks": "All43435 dual spaces against four literal primal supports; invalid Fourier/root/fourfold/JSON controls; three actual optimized rejecting CLI corruptions on private copies." + } + ] +} diff --git a/research/p112-c5-followup-audit/test_audit.py b/research/p112-c5-followup-audit/test_audit.py new file mode 100644 index 0000000000..02d9e5dfac --- /dev/null +++ b/research/p112-c5-followup-audit/test_audit.py @@ -0,0 +1,72 @@ +#!/usr/bin/env python3 +"""Behavioral controls for the new Fourier/table audit. Apache-2.0.""" + +import json +from pathlib import Path +import subprocess +import sys +import tempfile + +HERE = Path(__file__).resolve().parent +sys.path.insert(0, str(HERE)) +import verify # noqa: E402 + + +def rejected(function): + try: + function() + except (ValueError, KeyError): + return + raise ValueError("losing control accepted") + + +def main(): + data = verify.authenticate() + _, live, labels, _ = verify.table_model(data[verify.TABLE]) + # An explicit primal membership oracle checks every dual 7-space against + # several supports, including a single site, complement and irregular set. + samples = [labels[:1], labels[1:], labels[::3], labels] + pairs = [(a,b) for a in range(1,512) for b in range(a+1,512) if a^b > b] + for selected in samples: + spectrum = [sum(1 if (a&x).bit_count()%2 == 0 else -1 for x in selected) + for a in range(512)] + for a,b in pairs: + direct = sum((a&x).bit_count()%2 == 0 and (b&x).bit_count()%2 == 0 + for x in selected) + verify.require(verify.character_section(len(selected),spectrum,a,b) == direct, + "Fourier versus primal membership") + rejected(lambda: verify.character_section(1,[0]*512,1,2)) + rejected(lambda: verify.quadruples([(1<<15)-1]*120)) + rejected(lambda: verify.read_json('{"capacity":32,"capacity":33}')) + changed = data[verify.TABLE].decode().splitlines() + changed[2] = '0 0 0 0 0 0 0 0' + rejected(lambda: verify.table_model('\n'.join(changed).encode())) + verify.require(4*21-3*24 == 12 <= 14, "cut24 is not certified by this argument") + verify.require(6-4 == 2 and 65+3 == 68 < 65+4 == 69, "caller composition boundary") + # Actual optimized verifier processes on private copies; no frozen writes. + with tempfile.TemporaryDirectory(prefix="c5-followup-controls-") as tmp: + root = Path(tmp) + target = root / 'research/p112-c5-followup-audit' + target.mkdir(parents=True) + for name in ('verify.py','SOURCES.json','RESULT.json'): + (target/name).write_bytes((HERE/name).read_bytes()) + for name,raw in data.items(): + path = root/name + path.parent.mkdir(parents=True,exist_ok=True) + path.write_bytes(raw) + mutations = [(root/verify.TABLE, b'fault'), + (target/'SOURCES.json', b'{}'), + (target/'RESULT.json', b'{}')] + for path,mutant in mutations: + original = path.read_bytes() + path.write_bytes(mutant) + run = subprocess.run([sys.executable,'-I','-O','-Werror','-B',str(target/'verify.py')], + capture_output=True,text=True,timeout=90) + path.write_bytes(original) + verify.require(run.returncode != 0 and 'ValueError' in run.stderr, + "actual optimized CLI accepted corruption") + print('PASS_C5_AUDIT_CONTROLS primal_oracle=173740 semantic_rejections=4 optimized_CLI_rejections=3') + + +if __name__ == '__main__': + main() diff --git a/research/p112-c5-followup-audit/verify.py b/research/p112-c5-followup-audit/verify.py new file mode 100644 index 0000000000..41b8a2b686 --- /dev/null +++ b/research/p112-c5-followup-audit/verify.py @@ -0,0 +1,187 @@ +#!/usr/bin/env python3 +"""Table/Fourier proof audit, importing no predecessor executable. + +Chris R / Clear1nsight, substantial OpenAI Codex assistance. Apache-2.0. +Credit Nick Petalas and the retained E8/P112 source and caller lineage. +""" + +from collections import Counter +from fractions import Fraction +import hashlib +from itertools import combinations, product +import json +from pathlib import Path +import sys + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +MANIFEST_SHA = "aaf286296d12499182777926e41e3202baf29ea296050f9135ed3b3872937281" +TABLE = "research/one-sided-six-multisets/data/data.txt" +CUT = "research/p112-common-cut23-caller/" +SIX = "research/p112-six-piece-concentration/" +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(ok, message): + if not ok: + raise ValueError(message) + + +def unique(pairs): + require(len(pairs) == len({key for key, _ in pairs}), "duplicate JSON key") + return dict(pairs) + + +def read_json(raw): + return json.loads(raw, object_pairs_hook=unique) + + +def authenticate(root=ROOT, directory=HERE): + raw = (directory / "SOURCES.json").read_bytes() + require(hashlib.sha256(raw).hexdigest() == MANIFEST_SHA, "manifest identity") + inputs = {} + for row in read_json(raw)["files"]: + if row["usage"] != "input": + continue + path = root / row["path"] + require(path.resolve().is_relative_to(root.resolve()), "escaped input") + require(not any(p.is_symlink() for p in [path, *path.parents]), "input symlink") + data = path.read_bytes() + require(len(data) <= 2_000_000, "input size") + require(hashlib.sha256(data).hexdigest() == row["sha256"], "input SHA256") + require(hashlib.sha1(b"blob " + str(len(data)).encode() + b"\0" + data).hexdigest() + == row["git_blob"], "input Git blob") + inputs[row["path"]] = data + return inputs + + +def dot(a, b): + return sum(x * y for x, y in zip(a, b, strict=True)) + + +def coordinates(roots): + # Solve all columns at once by exact dense Gaussian elimination. + matrix = [[Fraction(SIMPLE[j][i]) for j in range(8)] + + [Fraction(r[i]) for r in roots] for i in range(8)] + for j in range(8): + pivot = next(i for i in range(j, 8) if matrix[i][j]) + matrix[j], matrix[pivot] = matrix[pivot], matrix[j] + scale = matrix[j][j] + matrix[j] = [x / scale for x in matrix[j]] + for i in range(8): + if i != j: + scale = matrix[i][j] + matrix[i] = [x - scale*y for x,y in zip(matrix[i],matrix[j])] + result = list(zip(*(row[8:] for row in matrix), strict=True)) + require(all(x.denominator == 1 for c in result for x in c), "integral coordinates") + require(all(min(c) >= 0 or max(c) <= 0 for c in result), "positive simple system") + return [tuple(map(int, c)) for c in result] + + +def table_model(raw): + lines = raw.decode().splitlines() + labels = list(map(int, lines[0].split())) + live = [tuple(map(int, row.split())) for row in lines[2:114]] + frame = [tuple(2*(i==a) + s*2*(i==a+1) for i in range(8)) + for a in (0,2,4,6) for s in (-1,1)] + roots = sorted(live + frame) + shell = {tuple(2*(k==i) + s*(k==j) for k in range(8)) + for i,j in combinations(range(8),2) for s in (-2,2)} + shell.update((1,*tail) for tail in product((-1,1),repeat=7) if sum(tail)%4 == 3) + require(len(shell) == 120 and roots == sorted(shell), "complete E8 root patterns") + coord = coordinates(roots) + full = [1+sum((x%2) << (j+1) for j,x in enumerate(c)) for c in coord] + require(labels == [x for r,x in zip(roots,full) if r not in frame], "caller labels") + require(len(live) == len(set(labels)) == 112 and all(x&1 for x in labels), + "distinct affine labels") + require(all(sum(r[i]*r[j] for r in live) == 112*(i==j) + for i in range(8) for j in range(8)), "evaluation Gram") + for alpha in SIMPLE: + for r in roots: + require(dot(alpha,r)%4 == 0, "reflection integrality") + image = tuple(x-dot(alpha,r)//4*y for x,y in zip(r,alpha)) + if next(x for x in image if x) < 0: + image = tuple(-x for x in image) + require(image in shell, "reflection closure") + return roots, live, labels, coord + + +def character_section(size, spectrum, a, b): + numerator = size+spectrum[a]+spectrum[b]+spectrum[a^b] + require(numerator%4 == 0, "nonintegral Fourier section") + return numerator//4 + + +def character_caps(labels, supports): + pairs = [(a,b) for a in range(1,512) for b in range(a+1,512) if a^b > b] + require(len(pairs) == 43_435, "dual-space coverage") + spectra = [[sum(1 if (a&x).bit_count()%2 == 0 else -1 for x in selected) + for a in range(512)] for selected in [labels,*supports]] + hist = Counter(character_section(112,spectra[0],a,b) for a,b in pairs) + caps = [max(character_section(len(s),f,a,b) for a,b in pairs) + for s,f in zip(supports,spectra[1:],strict=True)] + require(max(hist) == 36 and set(caps) == {32}, "Fourier capacities") + return {str(k):hist[k] for k in sorted(hist)} + + +def quadruples(off): + hist = Counter((off[a]&off[b]&off[c]&off[d]).bit_count() + for a,b,c,d in combinations(range(len(off)),4)) + require(sum(hist.values()) == 8_214_570 and max(hist) == 14, + "four-direction domain and maximum") + return {str(k):hist[k] for k in sorted(hist)} + + +def audit(inputs): + roots,live,labels,coord = table_model(inputs[TABLE]) + stored = read_json(inputs[CUT+"RESULT.json"]) + faces = [sum(all(c[j] == 0 for j in range(8) if not mask>>j&1) for c in coord) + for mask in range(256)] + require(max(faces[m] for m in range(256) if m.bit_count()<=6) == 36, + "low-rank parabolic cap") + require([faces[255^(1< 14 and 2+4+8+8 == 22 < 53, "caller arithmetic") + return {"schema":"p112-c5-followup-audit/v1", "flats":43_435, + "root_flat_tests":5_212_200, "quadruples":8_214_570, + "flat_size_histogram":flats, "fourfold_histogram":four, + "common_cut_bound":3, "common_cut_budget":23, + "fixed_inventory_conditional_coverage":69, "fixed_inventory_rows":69, + "existing_last_caller_source":"PR3295 / 4cff8128f0f9ea1e61515b95ddbb884366e9362c", + "scope":"Conditional contract composition; no full C5 or human/kernel review."} + + +def main(): + require(not sys.argv[1:], "no arguments") + result = audit(authenticate()) + expected = read_json((HERE/"RESULT.json").read_bytes()) + require(json.dumps(result,sort_keys=True) == json.dumps(expected,sort_keys=True), + "audit receipt mismatch") + print("PASS_C5_FOLLOWUP_AUDIT Fourier43435x120 quadruples8214570 conditional_inventory69/69") + + +if __name__ == "__main__": + main()