diff --git a/research/p112-mixed-support38/CHECKS.json b/research/p112-mixed-support38/CHECKS.json new file mode 100644 index 0000000000..adb92ded3b --- /dev/null +++ b/research/p112-mixed-support38/CHECKS.json @@ -0,0 +1,36 @@ +{ + "status": "local registered replay, committed export and designated peer check passed", + "utc": "2026-10-17T20:01:52.057442+00:00", + "baseline": "463113d675af7410ac91d53a4fed51ec6494eb9a", + "environment": "CPython3.12.15 macOS arm64; standard library", + "registered": "PASS all three commands with -W error; controls under -O", + "primary": "3780orthogonalplanes,896live-axis fibers times10795sixspaces; A2 and chamber receipts match RESULT.json", + "independent": "788035ambient sixspaces,16support20sets,120fourframes,1920intersections and3780orthogonal-pair orbit", + "controls": "7groups passed; includes malformed inventory, corrupted source, symlink, oversized file and absent-puncture control", + "diagnostics": "Ruff check and format check passed", + "limits": [ + "Global g(5)=12/g(6)=20 historical censuses inherited, not rerun", + "Weyl-chamber theorem is a written dependency", + "Independent checker shares authenticated geometry; no independent A2/global-capacity proof", + "No Lean, Docker, full selected cold replay, supplier or kappa claim" + ], + "peer_review": { + "reviewer_worker": 1, + "reviewed_commit": "fb75f16629b3d664488e9f9a186c9933b0901235", + "result": "No blocking issue at stated characteristic-zero commoncut38 ranks5,5,6 scope after singleton-domain clarification.", + "resolved": "Singleton sites/J_i explicitly restricted to U outsideS in PROOF.md; proportional recheck accepted SHA25674b3e610a69a2f5e372595efbc17f3215c3f1af53a0f536dbbc12e5abb821327.", + "receipt": "REVIEW.json" + }, + "committed_export": { + "commit": "fb75f16629b3d664488e9f9a186c9933b0901235", + "file_count": 18, + "sha256": "1b6780a64e025756c347930849aa2eb25bd5f1ca59cc30e520d1099df2629f30", + "result": "All3directcommands passed optimized Python3.13.16 in exact committed read-only Git-free export. Final accepted proof-only correction and review-metadata update do not change executables/sources/RESULT." + }, + "submission_refresh": { + "canonical_main": "463113d675af7410ac91d53a4fed51ec6494eb9a", + "priority_revision": 6, + "cutoff": "2026-10-17T20:03:02Z", + "coverage": "Complete311openPRs/2101discussionrecords,no warnings. Worker2 near-synonym duplicate released. No novel-coverage inference from no-match." + } +} diff --git a/research/p112-mixed-support38/ENGINEERING.md b/research/p112-mixed-support38/ENGINEERING.md new file mode 100644 index 0000000000..f457f2352e --- /dev/null +++ b/research/p112-mixed-support38/ENGINEERING.md @@ -0,0 +1,60 @@ +# Verification design + +The executable claim is finite geometry supporting the written mixed-rank +support 38 theorem. No supplier implementation is changed. + +Separate Before Serializing Shared State shaped the workspace boundary. This +package, branch, status file and session cache have one writer. Shared Git +metadata operations use the batch's OS-released lock. Research arithmetic runs +without that lock. Peer checks read frozen source and write only reviewer-owned +receipts. + +Prove It Works shaped the publication gate. Run the actual registered commands, +then replay exact committed export bytes from a read-only Git-free tree under +a second Python version before freezing the peer-review tree. + +## Power of Ten + +1. The three scripts use structured loops and explicit ValueError exits. There + is no recursion. File contexts and temporary-directory contexts own cleanup. +2. Root inventories have 120 full/112 live entries. Binary inputs have at most 512 + labels of at most 18 bits. D6 has 3780 planes,448 minimum planes and 896 live-axis + fibers. A fiber has 256 functionals and 10795 dual two-spaces. The alternate + ambient census has 788035 three-dimensional annihilators. A2 has 1120 planes + and its orbit queue can contain at most 1120 items. The alternate D6 orbit + queue has at most 3780 items. Source inventories have 5 rows and 4 retained rows. + Registered command timeouts are 120 seconds, sequentially. +3. CPython requires dynamic allocation. This managed-runtime deviation covers + only the bounded inventories above. Source files are at most 1 MB each; the + largest retained primary census serialization has 896 rows with bounded + histograms. Bit masks have at most 33 bits for D6 fibers. The alternate full + inventory retains only 16 maximal supports. No asynchronous work or subprocess + remains after a command. Direct allocation instrumentation is unrun. +4. The largest new function is a 2_receipt at 60 physical lines after Ruff format. + Other functions are below 60 lines. It owns one plane classification and + orbit/fiber receipt; splitting it further would add a single-use forwarding + boundary without a separate ownership requirement. +5. Runtime require checks validate source pins, exact cardinalities, label + ranges, census totals, orbit coverage and arithmetic implications. They + remain active with Python optimization. Controls run with -O. +6. Module globals identify immutable paths and finite expected inventories. + Geometry, bit masks, queues and receipts stay local. No peer artifact is + writable through the verifier. +7. Read and parse failures propagate. Output uses exclusive creation. Source + inventory lengths and exact allowed paths are checked before reading or + importing sources. Hash and Git-blob checks bind retained bytes without Git. +8. The fixed geometry module is loaded after authentication. No input supplies + code, module names or call targets. No generated code or eval is used. +9. The import loader is the sole dynamic call boundary and loads one fixed + authenticated local module. All mathematical helpers otherwise have visible + direct call targets. This Python import boundary is a bounded runtime + deviation from a ban on indirect calls. +10. Registered replays enable -W error. Ruff check and formatting checks cover + every new Python file. There is no compiled component or compiler warning + configuration. The standard-library runtime and inherited geometry internals + retain their existing contracts. + +The managed-runtime allocation and fixed import-loader deviations stay confined +to these offline checks. Revisit them if inputs become user-sized, the module +path becomes configurable, or the verifier becomes a service. Keep the bounds +and authentication tests when changing the implementation. diff --git a/research/p112-mixed-support38/PROOF.md b/research/p112-mixed-support38/PROOF.md new file mode 100644 index 0000000000..3b45a13600 --- /dev/null +++ b/research/p112-mixed-support38/PROOF.md @@ -0,0 +1,173 @@ +# Mixed-rank shortening through common support 38 + +Let K be any characteristic-zero field. On the fixed 112 nonframe E8 root +lines, let C be the root-evaluation code, using doubled roots r_t: + +``` +C = {(r_t dot h)_t : h in K^8}. +``` + +Binary support rank is the rank over F2 of the pinned nine-bit labels in a +vector's support. Let pi_S delete ONE common coordinate set S. + +**Theorem.** If |S| <= 38, and three residual pieces q_1,q_2,q_3 have binary +support ranks at most 5,5,6, then + +``` +dim_K(pi_S(C) intersect span_K(q_1,q_2,q_3)) <= 1. +``` + +The pieces can be dependent and have arbitrary coefficients. Rank constraints +apply only outside S. The theorem is sufficient; sharpness is not claimed. +PR3260 proves support 37 and leaves the 30-root D6 classification branch +open. This proof closes that branch at 38. It supplies no new historical +profile exclusion, full C5, decoder-floor theorem, supplier or kappa. + +## Dependencies and exact finite coverage + +The source-pinned root-simplex proof and receipt supply global P112 capacities +12 and 20 for binary ranks five and six. Their complete historical flat +censuses are inherited, not rerun here. The standard real Weyl-chamber theorem +and the rational-nullspace transfer below are written dependencies. + +The new replay checks the 28 six-node parabolics. Only D6 and E6 have at +least 30 root lines, with counts 30 and 36. All 56 five-node parabolics have +at most 20 root lines. The normal planes of the two qualifying six-node +parabolics contain respectively two orthogonal root lines and an A2 triple. +Thus their Weyl images are covered by orthogonal root pairs and A2 planes. +The source module also checks all 960 simple reflections. + +The replay checks all 1,120 A2 planes, their live union spectrum 78/80, +and transitivity under eight simple reflections. Each reflection induces +an invertible linear map of the nine-bit labels. The three representative +27-line projective fibers each span a binary seven-space. Their 2,667 +five-spaces have fiber capacity ten. Their 127 hyperplanes have the following +complete full-E8 support / fiber-support counts: + +``` +(0,0):1, (12,11):27, (12,12):36, (16,15):36, (16,16):27. +``` + +These joint counts follow PR3262's support-plus-singleton argument; they are +rechecked here. The independent D6 check does not independently re-prove +these A2 premises or the global 12/20 capacities. + +## Classify a two-dimensional intersection + +Suppose the displayed intersection has dimension at least two. Choose two +independent restricted codewords and lifts c_h,c_k. Their full support union U +lies in S together with the three piece supports. Extend each residual piece +by zero on S. The global capacities give + +``` +|U| <= |S| + 12 + 12 + 20 <= 82. +``` + +The lifts are independent, since their restrictions are independent. Therefore +the rational span Z of all full E8 roots perpendicular to h and k has rank +at most six. At least 112-82=30 live roots belong to Z. + +Every root in the rational span of Z is also perpendicular to h,k. A generic +real vector perpendicular to Z therefore has exactly those full E8 roots as +its perpendicular root set. Indeed, finitely many additional hyperplanes can +be avoided. Move this real vector into a closed Weyl chamber. Its perpendicular +root system is a parabolic subsystem of rank at most six. The checked counts +force rank six and type D6 or E6. Its two-dimensional normal plane equals the +K-span of h,k, since rational matrix rank is unchanged by characteristic-zero +extension. In particular it has a rational basis. + +This argument uses the full perpendicular root system, even though the count +30 comes from live roots. It does not assume any individual piece is a +restricted codeword or any quotient-basis normalization. + +## Exclude E6 using joint incidence capacity + +In this branch the normal plane is an A2 root plane. Replace h,k by a rational +basis of that plane. Their live support union has at least 78 coordinates. +On the complement of S there is a fixed two-by-three matrix A with + +``` +(c_h(t), c_k(t))^T = A (q_1(t), q_2(t), q_3(t))^T. +``` + +At a coordinate in U outside S where exactly one piece q_i is nonzero, +the nonzero evaluation pair is proportional to column i of A. Such singleton +sites for q_i lie in ONE projective fiber. A zero column has no such sites. Besides three large +27-line fibers, the A2 plane has three one-line fibers. + +Let M_i be total residual support of piece i and let J_i count its singleton +sites in U outside S. +For i=1,2, the global capacity 12 and fiber capacity ten give M_i+J_i<=22. +For the rank-six piece, M_3+J_3<=32. To see the latter, a one-line fiber gives +the stronger bound 21. For a large fiber in a seven-space W, let V be the +actual binary support span of q_3. If dim(V intersect W)<=5, then J_3<=10 +and M_3<=20, giving at most 30. Otherwise V is a six-space contained in W. +The complete hyperplane inventory above gives M_3+J_3<=32. Supports can be +proper subsets of their binary closures; this only lowers these quantities. + +Let N=|U minus S|. Each union coordinate has at least one piece incidence; +a nonsingleton has at least two. Thus + +``` +2N <= sum_i(M_i+J_i) <= 22+22+32 = 76. +2N >= 2*(78-38) = 80. +``` + +This contradiction permits cancellations, arbitrary columns of A, and piece +support outside U. Extra support only increases M_i. No common shift is +assumed modal. + +## Exclude the D6 equality case with the actual puncture + +Every D6 normal plane is spanned by two orthogonal E8 roots a,b. The full E8 +nonzero evaluation union has 90 lines. Its four projective fibers have sizes +33,33,12,12. The two large fibers are the two coordinate axes. The exact live +union histogram over all 3,780 orthogonal root pairs is + +``` +82:448, 84:2688, 85:448, 86:168, 88:28. +``` + +Since |U|<=82, only the 448 minimum planes can occur. Then |U|=82 and |S|=38 +are forced. Their residual union has at least 44 coordinates, while the +three pieces have at most 12+12+20=44 incidences in total. Equality follows +throughout. The pieces have disjoint supports of sizes 12,12,20, every support +coordinate lies in U outside S, and every coordinate is a singleton. + +Consequently the rank-six piece's entire support of size 20 lies in ONE +projective fiber. A small fiber has only twelve full E8 coordinates. Each +large fiber in a minimum plane has 29 live labels of binary rank eight. +For each of the 448 planes and both large fibers, the primary replay checks +all 10,795 six-spaces in that eight-space via unique two-dimensional dual +spaces. Their maximum live intersection is always 18. A binary space of rank +at most six meets the fiber in a subset of one such six-space. This contradicts +support size 20 and proves the theorem. + +The puncture is essential to this finite premise. A full 33-line axis has +six-space capacity 20, with sixteen maximizing supports. A separate checker +enumerates all 788,035 ambient six-spaces, rather than using the primary +fiber coordinates, and reconstructs those sixteen sets. It checks all 120 +orthogonal four-root subsets inside the axis. Each support 20 meets each such +four-frame in two or four roots, with multiplicities 1,440 and 480. All 896 +actual minimum-plane axis punctures are such four-frames. A separate orbit +check covers all 3,780 orthogonal pairs under the simple reflections. + +This alternate check excludes a surviving support 20. It does not by itself +establish the stronger punctured capacity 18 for subsets of smaller full +intersections; the primary complete census supplies that stronger value. + +## Credit and limits + +Nick Petalas's PR3260 supplies the mixed 5,5,6 question and support 37 proof. +PR3262 supplies the joint A2 support/singleton argument. The source-pinned +root-simplex work, PR3249 and PR3255 supply the capacity and geometry lineage. +DreamingOfClouds/PR3154 supplies the TWOSIDE motivation; the retained E8/P112 +lineage includes joaqcoo. Worker1's simultaneous uniform 5,5,5 support 46 audit +identified the same D6 prerequisite and has a distinct equality obligation. +The present theorem uses no unpublished sibling result. + +The finite certificate and written characteristic-zero proof do not constitute +proof-kernel or independent human verification. Support39, global sharpness, +a fresh caller, the original C5 reductions, physical/recursive realization, +restoration, the complete consumer bill and multiplication transfer remain +separate obligations. No selected result is changed. diff --git a/research/p112-mixed-support38/README.md b/research/p112-mixed-support38/README.md new file mode 100644 index 0000000000..06af9afb0b --- /dev/null +++ b/research/p112-mixed-support38/README.md @@ -0,0 +1,70 @@ +# P112 mixed-rank shortening at common support 38 + +Three residual P112 pieces of binary support ranks at most 5,5,6, after ONE +common deletion set of size at most 38, meet the restricted root-evaluation +code in dimension at most one over every characteristic-zero field. This +improves PR3260's sufficient threshold 37. It does not prove sharpness or a +new historical profile exclusion. [PROOF.md](PROOF.md) gives the complete +argument and inherited dependencies. + +The new step closes the D6 boundary. A putative equality requires a rank-six +piece supported on 20 singleton coordinates in one projective fiber. All 896 +relevant live axis fibers have rank-six capacity 18. An independent ambient +annihilator/puncture check also excludes support 20. The E6 branch uses +PR3262's rechecked joint incidence argument, with allowance76 versus80. +Exact coverage and full-census digest are in [RESULT.json](RESULT.json). + +## Reproduce + +Python 3.12 or later, standard library only, from the repository root: + +```sh +python3.12 -W error -B scripts/research_package.py \ + --package research/p112-mixed-support38 +``` + +The three registered commands run sequentially with 120-second limits. Direct +Git-free export replay uses these commands, from the exported root: + +```sh +python3 -W error -B research/p112-mixed-support38/verify.py +python3 -W error -B research/p112-mixed-support38/independent_check.py +python3 -W error -O -B research/p112-mixed-support38/test_verify.py +``` + +The export needs the package and its three declared baseline inputs at their +original relative paths. Pending PR proof/receipt bytes are retained locally +with exact commit, Git blob and SHA256 pins in [SOURCES.json](SOURCES.json). +No pending Git objects or Git subprocesses are needed for direct replay. +Authentication bounds inventory length, paths and source sizes before import. +`verify.py --output NEW_EXTERNAL_PATH` creates an external receipt and refuses +to overwrite an existing file. Set TMPDIR to an external session directory to +keep control-fixture files outside the checkout. + +## Open next questions + +Does support 39 admit a counterexample or a larger sufficient theorem? The D6 +incidence equality used here no longer follows at 39. First bind the actual +puncture and mixed support-overlap patterns before another census. This is +unrun and not evidence that 38 is sharp. A new TWOSIDE application also needs +a named caller, current public-exclusion reconciliation and its exact retained +code dimension. [TASK.json](TASK.json) records these questions and blockers. + +## Sources and verification limits + +Credit Nick Petalas/PR3260/3262, DreamingOfClouds/PR3154 and the retained +root-simplex/E8/P112 lineage including joaqcoo. Worker1's concurrent uniform +rank-five support 46 theorem shares the D6 prerequisite but proves a different +predicate. This package uses no unpublished sibling theorem. All copied +predecessor bytes stay unchanged. New work and retained sources are Apache-2.0. + +The global five-/six-flat capacities 12/20 and standard Weyl-chamber theorem +are inherited; their historical global censuses are not rerun. The independent +checker shares authenticated root/label reconstruction and does not independently +establish A2 capacities or characteristic-zero classification. Internal review +is not independent human or proof-kernel review. [CHECKS.json](CHECKS.json) +records executed commands, export evidence and review limits. + +No full C5, decoder floor, native or physical supplier, restoration, complete +consumer, all-size multiplication theorem, new kappa or selected-frontier +update is claimed. Lean, Docker and the selected full cold replay are unrun. diff --git a/research/p112-mixed-support38/RESULT.json b/research/p112-mixed-support38/RESULT.json new file mode 100644 index 0000000000..4bde18468f --- /dev/null +++ b/research/p112-mixed-support38/RESULT.json @@ -0,0 +1,130 @@ +{ + "A2": { + "fibers": [ + { + "five_fiber_maximum": 10, + "five_spaces": 2667, + "hyperplanes": 127, + "joint_maximum": 32 + }, + { + "five_fiber_maximum": 10, + "five_spaces": 2667, + "hyperplanes": 127, + "joint_maximum": 32 + }, + { + "five_fiber_maximum": 10, + "five_spaces": 2667, + "hyperplanes": 127, + "joint_maximum": 32 + } + ], + "planes": 1120, + "reflection_maps": 8, + "union_histogram": { + "78": 896, + "80": 224 + } + }, + "D6": { + "axis_maximum_histogram": { + "18": 896 + }, + "full_census_sha256": "23df8c455d435fece68b0e141c3809e30b0e37ae937764a1e69a8e0f64fea25f", + "live_axis_fibers": 896, + "orthogonal_planes": 3780, + "six_spaces_per_fiber": 10795, + "union_histogram": { + "82": 448, + "84": 2688, + "85": 448, + "86": 168, + "88": 28 + } + }, + "budgets": { + "D6_fiber_maximum": 18, + "D6_rank6_required": 20, + "D6_required": 44, + "D6_total_support": 44, + "E6_allowance": 76, + "E6_required": 80 + }, + "chamber": { + "chamber": { + "rank_six_parabolic_counts": [ + 21, + 21, + 12, + 12, + 15, + 21, + 30, + 16, + 13, + 12, + 13, + 16, + 21, + 12, + 10, + 10, + 12, + 16, + 10, + 8, + 8, + 10, + 13, + 12, + 13, + 21, + 21, + 36 + ], + "ray_zero_counts": [ + 42, + 28, + 22, + 14, + 16, + 23, + 37, + 63 + ], + "root_support_histogram": { + "53": 112, + "56": 8 + }, + "simple_reflection_checks": 960 + }, + "large_parabolics": [ + { + "kind": "D6", + "omitted": [ + 0, + 7 + ], + "root_lines": 30 + }, + { + "kind": "E6", + "omitted": [ + 6, + 7 + ], + "root_lines": 36 + } + ], + "rank_five_maximum": 20 + }, + "common_support": 38, + "endpoint_ranks": [ + 5, + 5, + 6 + ], + "intersection_upper_bound": 1, + "status": "PASS_MIXED_P112_SUPPORT38" +} diff --git a/research/p112-mixed-support38/REVIEW.json b/research/p112-mixed-support38/REVIEW.json new file mode 100644 index 0000000000..2539982057 --- /dev/null +++ b/research/p112-mixed-support38/REVIEW.json @@ -0,0 +1,49 @@ +{ + "reviewer_worker": 1, + "reviewer_thread": "mcp:f639c67a-1cb9-465e-9940-bf34459d52a6", + "author_worker": 4, + "reviewed_commit": "fb75f16629b3d664488e9f9a186c9933b0901235", + "base": "463113d675af7410ac91d53a4fed51ec6494eb9a", + "reviewed_diff_sha256": "818fba85e0a5be25021eaf5279012e7cc3236931a69c451bbee9db921ad4c5db", + "frozen_files": { + "research/p112-mixed-support38/CHECKS.json": "e2da2d0f30948221e13f9401ce91c71814ddbe83ee9f88c5db3c035faf8907db", + "research/p112-mixed-support38/ENGINEERING.md": "106539a51fb97d179a1813f2975287b62870a1eab2c24bbcd03050a37bfaf3c5", + "research/p112-mixed-support38/PROOF.md": "2f3b311559783fa14fa87707809e312819b8f02404ed763afbfc308852eefdd6", + "research/p112-mixed-support38/README.md": "98d5741073571aee5510a690df4a4e16821ae5b5f344dad73a6dafe76ecd8455", + "research/p112-mixed-support38/RESULT.json": "877feb226afef1f36fce8762c7df092869b289aab10efb78e69d9d3b5e5f3f76", + "research/p112-mixed-support38/SOURCES.json": "1b16751c170c322abab41bba96a0199601554dbd2b5423f9df6f819d9e790e30", + "research/p112-mixed-support38/TASK.json": "207b7b02781e4bcd3cab18cb4ec7e41333cbff9db6a854d3290df5bc1225257b", + "research/p112-mixed-support38/VERIFY.json": "f443a1209a2d54ed785b0398f39841d2a314568fc6e27637fbd4596e799afc87", + "research/p112-mixed-support38/independent_check.py": "43f0fa02393b86e32bd07ec55fa9976ff2abb013e03f368fb52ff88b03530f69", + "research/p112-mixed-support38/test_verify.py": "5cab5c3c2fcd3f20bd4c5217be275b1a05b55de124c64bc256a843f255d521a7", + "research/p112-mixed-support38/vendor/pr3260-PROOF.md": "75f0eb563b86f7e4aeeb0c11a1a18a901d4b01ac54e999e238e4021300b26fa1", + "research/p112-mixed-support38/vendor/pr3260-RESULT.json": "6b2dbe26183651a98d43654f2dadef20606b462328519a960bf705bee7e177eb", + "research/p112-mixed-support38/vendor/pr3262-PROOF.md": "9d717f803b7218501ea6c019aff2c42570a8a53027ecfebc60ff79ef336f3d9b", + "research/p112-mixed-support38/vendor/pr3262-RESULT.json": "6a8c8552eae67f6fdc10681203292aa9f9df1376be37b67f7e22a1799f6d9fac", + "research/p112-mixed-support38/verify.py": "6e7970d07c6041b5afe43d50989dd3cdf11d3e465ae3d507e817c73d29e3acb0" + }, + "proportional_proof_correction": [ + { + "path": "research/p112-mixed-support38/PROOF.md", + "old_sha256": "2f3b311559783fa14fa87707809e312819b8f02404ed763afbfc308852eefdd6", + "new_sha256": "74b3e610a69a2f5e372595efbc17f3215c3f1af53a0f536dbbc12e5abb821327" + } + ], + "result": "No blocking issue at stated characteristic-zero commoncut38 ranks5,5,6 scope after singleton-domain clarification.", + "reasoning": "Reviewed rational-nullspace/Weyl-parabolic normalization, mixed76<80 A2 incidence bound, D6 forced12+12+20 disjoint singleton equality and actual896axis cap18; alternate ambient20set puncture argument checked. Distinct from reviewer uniform555cut46 theorem.", + "finding_resolved": "PROOF now limits singleton sites and J_i to U outsideS, retaining M_i as total residual support. Only2 prose passages changed; all code, finite receipts and source bytes stayed frozen.", + "checks": { + "source_bytes": "15frozen package files checked before review; all4retained pending sources equal pinned Git objects; after correction onlyPROOF differs.", + "primary": "CPython3.12.15 verify.py PASS planes3780/livefibers896/rank6cap18", + "independent": "CPython3.12.15 independent_check.py PASS ambient788035/fullaxis20sets16/orthogonal4frames120/intersections2:1440,4:480/actualpunctures896/orbit3780", + "controls": "CPython3.12.15 -O test_verify.py PASS7groups including sourcecorruption,missing/duplicate/escape/extra inventory and size/link controls", + "execution": "Read-only peer source paths with -B and private pycache prefix; all temporary writes in reviewer-owned TMPDIR. No peer files regenerated or edited." + }, + "unrun": [ + "Inherited globalrank5/6 capacities12/20 historicalcensuses", + "Weyl-chamber theorem formalization or independent human review", + "Registered metadata/export rerun, since author supplied exactexport receipt and directcommands passed", + "Actualcaller, sharpness, fullC5, decoderfloor, physical/native/consumer/supplier/kappa, selectedcold, Lean, Docker" + ], + "created": "2026-10-17T20:03:53.367197+00:00" +} diff --git a/research/p112-mixed-support38/SOURCES.json b/research/p112-mixed-support38/SOURCES.json new file mode 100644 index 0000000000..4b76c60d2c --- /dev/null +++ b/research/p112-mixed-support38/SOURCES.json @@ -0,0 +1,70 @@ +{ + "schema_version": 1, + "base_commit": "463113d675af7410ac91d53a4fed51ec6494eb9a", + "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/p112-root-simplex-exclusion/geometry.py", + "usage": "input", + "git_blob": "222ea556faf2b275f73815c4e7d0d5f1e3294f2f", + "sha256": "b8ac379e41f5ad83bdb6c7f7c55129fc3d9c07801ea61591478f25d72ff0b021" + }, + { + "path": "research/p112-root-simplex-exclusion/PROOF.md", + "usage": "input", + "git_blob": "ccae08212784114e732da1192b336e47fc6a2091", + "sha256": "2b5d70570e3a13d2ccc71c1fc7eef113f0d049993cb9bb24007166223ac7b734" + }, + { + "path": "research/p112-root-simplex-exclusion/RESULT.json", + "usage": "input", + "git_blob": "7d0b1ea5a196983821bedc596089e5e92174daf4", + "sha256": "da2ccf45b60fd66f5fcb829cd4da281ae31233dcae7a7bc260d574c89af2f871" + } + ], + "retained_files": [ + { + "local_path": "vendor/pr3260-PROOF.md", + "source_path": "research/p112-mixed-a2-caller/PROOF.md", + "commit": "cdeee42ba34d4da3db8c2b1fc9cbc134c7172fed", + "pr": 3260, + "git_blob": "3b013e786a36cc9fc841b85fdefa8e38f6581bb5", + "sha256": "75f0eb563b86f7e4aeeb0c11a1a18a901d4b01ac54e999e238e4021300b26fa1" + }, + { + "local_path": "vendor/pr3260-RESULT.json", + "source_path": "research/p112-mixed-a2-caller/RESULT.json", + "commit": "cdeee42ba34d4da3db8c2b1fc9cbc134c7172fed", + "pr": 3260, + "git_blob": "12e77eb5b765d07cbf1e36936863d242b77ed10f", + "sha256": "6b2dbe26183651a98d43654f2dadef20606b462328519a960bf705bee7e177eb" + }, + { + "local_path": "vendor/pr3262-PROOF.md", + "source_path": "research/p112-a2-rank6-sharp-shortening/PROOF.md", + "commit": "f7af207c5e8eabc4524448a0f7c6f77a03c059ba", + "pr": 3262, + "git_blob": "315adf2b2a6f0fbadb588f781f45f97cc48f556e", + "sha256": "9d717f803b7218501ea6c019aff2c42570a8a53027ecfebc60ff79ef336f3d9b" + }, + { + "local_path": "vendor/pr3262-RESULT.json", + "source_path": "research/p112-a2-rank6-sharp-shortening/RESULT.json", + "commit": "f7af207c5e8eabc4524448a0f7c6f77a03c059ba", + "pr": 3262, + "git_blob": "cf90559a4e82ee180568e072c0961ef7c38e8faf", + "sha256": "6a8c8552eae67f6fdc10681203292aa9f9df1376be37b67f7e22a1799f6d9fac" + } + ] +} diff --git a/research/p112-mixed-support38/TASK.json b/research/p112-mixed-support38/TASK.json new file mode 100644 index 0000000000..4513454b3e --- /dev/null +++ b/research/p112-mixed-support38/TASK.json @@ -0,0 +1,86 @@ +{ + "schema_version": 1, + "task_id": "complex-rank-shape-decoder", + "priority_revision": 6, + "base_commit": "463113d675af7410ac91d53a4fed51ec6494eb9a", + "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": "Prove or falsify the released PR3260 mixed5,5,6 common-support38 shortening obligation over characteristic zero.", + "scope_change_reason": "Take the specific public handoff rather than synthesize another decoder. PR3260 stops at a D6 classification boundary; this closes that named implication without a construction expansion.", + "bottleneck_link": "Scoped decoder geometry useful to the C5 reduction; no claimed paid-profile or kappa improvement. Physical/consumer costs remain unknown.", + "budget_minutes": 60, + "stop_rule": "Stop after the support38 implication, bounded exact checks, source-export proof, internal peer review and focused publication; no support39 round.", + "outcome": "completed", + "evidence": "PROOF.md and RESULT.json; all3780 D6planes,896live-axis censuses and separate ambient-annihilator/puncture check.", + "author": "Nick Petalas", + "ai_assistance": "Computational development and internal automated checks; no independent human or proof-kernel verification.", + "open_questions": [ + { + "question": "Does common support39 admit a mixed5,5,6 counterexample or a stronger theorem?", + "why_it_matters": "Determine whether the next D6 overlap case changes the useful shortening allowance.", + "first_step": "Analyze actual D6 punctured support-overlap patterns before a bounded search.", + "blocked_by": "At39 the support38 equality argument no longer forces disjoint saturated supports." + }, + { + "question": "Which actual still-open caller benefits from this theorem?", + "why_it_matters": "A geometric bound alone does not close a new TWOSIDE profile.", + "first_step": "Reconcile a named original profile with current public exclusions and derive its retained code dimension.", + "blocked_by": "No new caller is bound in this package." + } + ], + "overlap": { + "cutoff": "2026-10-17T19:54:48Z", + "open_prs": 310, + "discussion_records": 2095, + "complete_pagination": true, + "limits": "No exhaustive arbitrary diff, unpublished work or closedPR search. Prior ten published heads checked open/unchanged. Worker2 later duplicate mixed38 claim released; worker1 uniform46 is distinct." + }, + "family_expansion_gate": "Narrow the released support38 implication; no larger census campaign, supplier or dependent optimization. Stop at the bounded proof." +} diff --git a/research/p112-mixed-support38/VERIFY.json b/research/p112-mixed-support38/VERIFY.json new file mode 100644 index 0000000000..f36a5bf00d --- /dev/null +++ b/research/p112-mixed-support38/VERIFY.json @@ -0,0 +1,47 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/p112-root-simplex-exclusion/geometry.py", + "research/p112-root-simplex-exclusion/PROOF.md", + "research/p112-root-simplex-exclusion/RESULT.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "All3780D6planes,896live-axis rank6censuses, A2 joint capacities, chamber classification and proof budget." + }, + { + "argv": [ + "{python}", + "-W", + "error", + "-B", + "{package}/independent_check.py" + ], + "timeout_seconds": 120, + "checks": "Separately written binary elimination and six-space generator check fullaxis20maximizers against every orthogonal four-frame subset." + }, + { + "argv": [ + "{python}", + "-W", + "error", + "-O", + "-B", + "{package}/test_verify.py" + ], + "timeout_seconds": 120, + "checks": "Optimized source-inventory rejections, puncture necessity, budget boundaries and rank limits." + } + ] +} diff --git a/research/p112-mixed-support38/independent_check.py b/research/p112-mixed-support38/independent_check.py new file mode 100644 index 0000000000..a4a91663b6 --- /dev/null +++ b/research/p112-mixed-support38/independent_check.py @@ -0,0 +1,151 @@ +"""Separate ambient-annihilator and puncture check. Apache-2.0.""" + +import json +from collections import Counter +from itertools import combinations, product + +import verify + + +def binary_rank(values): + pivots = [0] * 9 + for original in values: + if type(original) is not int or not 0 <= original < 512: + raise ValueError("invalid label") + value = original + for bit in range(8, -1, -1): + if value >> bit & 1: + if pivots[bit]: + value ^= pivots[bit] + else: + pivots[bit] = value + break + return sum(v != 0 for v in pivots) + + +def maximal_axis_subsets(labels): + """Enumerate all 788035 ambient six-spaces without local coordinates.""" + if len(labels) != 33 or binary_rank(labels) != 8: + raise ValueError("expected full D6 axis") + kernels = [ + sum( + 1 << i + for i, label in enumerate(labels) + if (label & functional).bit_count() % 2 == 0 + ) + for functional in range(512) + ] + counts, maximizers = Counter(), set() + for pivots in combinations(range(9), 3): + choices = [] + for pivot in pivots: + free = [i for i in range(pivot) if i not in pivots] + choices.append( + [ + (1 << pivot) | sum(((v >> j) & 1) << i for j, i in enumerate(free)) + for v in range(1 << len(free)) + ] + ) + for a, b, c in product(*choices): + mask = kernels[a] & kernels[b] & kernels[c] + counts[mask.bit_count()] += 1 + if mask.bit_count() == 20: + maximizers.add(mask) + if sum(counts.values()) != 788035 or max(counts) != 20 or len(maximizers) != 16: + raise ValueError("full-axis rank-six census differs") + return maximizers + + +def orthogonal_frames(roots): + if len(roots) != 33: + raise ValueError("expected 33 axis roots") + gram = [ + [sum(x * y for x, y in zip(a, b, strict=True)) for b in roots] for a in roots + ] + frames = [] + for chosen in combinations(range(33), 4): + if all(gram[a][b] == 0 for a, b in combinations(chosen, 2)): + frames.append(sum(1 << i for i in chosen)) + if not frames: + raise ValueError("missing frame controls") + return frames + + +def orthogonal_orbit(g, roots): + index = {r: i for i, r in enumerate(roots)} + perms = [] + for simple in g.SIMPLE: + perm = [] + for r in roots: + reflected = g.canonical( + tuple( + x - g.dot(r, simple) // 4 * y + for x, y in zip(r, simple, strict=True) + ) + ) + perm.append(index[reflected]) + perms.append(perm) + start = next( + (i, j) for i, j in combinations(range(120), 2) if g.dot(roots[i], roots[j]) == 0 + ) + seen, queue = {start}, [start] + for cursor in range(3780): + if cursor >= len(queue): + raise ValueError("orthogonal orbit ended early") + for perm in perms: + pair = tuple(sorted(perm[i] for i in queue[cursor])) + if g.dot(*(roots[i] for i in pair)): + raise ValueError("reflection left orthogonal pairs") + if pair not in seen: + seen.add(pair) + queue.append(pair) + if len(seen) != 3780 or len(queue) != 3780: + raise ValueError("orthogonal-pair transitivity failed") + return len(seen) + + +def check(): + g = verify.geometry() + roots, points, _labels, coordinates = g.root_data() + full_labels = [ + 1 | sum((int(x) & 1) << (i + 1) for i, x in enumerate(c)) for c in coordinates + ] + a = (0, 0, 0, 0, 0, 2, -2, 0) + b = (0, 2, -2, 0, 0, 0, 0, 0) + axis = [i for i, r in enumerate(roots) if g.dot(a, r) and not g.dot(b, r)] + maxima = maximal_axis_subsets([full_labels[i] for i in axis]) + frames = orthogonal_frames([roots[i] for i in axis]) + intersections = Counter((m & f).bit_count() for m in maxima for f in frames) + if min(intersections) < 2: + raise ValueError("a full support20 survives a four-frame puncture") + # Every actual minimum-union plane removes four orthogonal roots per axis. + gram = [[g.dot(x, y) for y in roots] for x in roots] + frame = [i for i, r in enumerate(roots) if r not in points] + live = [i for i, r in enumerate(roots) if r in points] + checked = 0 + for x, y in combinations(range(120), 2): + if gram[x][y] or sum(bool(gram[x][t] or gram[y][t]) for t in live) != 82: + continue + for j, k in ((x, y), (y, x)): + removed = [t for t in frame if gram[j][t] and not gram[k][t]] + if len(removed) != 4 or any( + gram[u][v] for u, v in combinations(removed, 2) + ): + raise ValueError("actual axis puncture is not an orthogonal four-frame") + checked += 1 + if checked != 896: + raise ValueError("minimum-plane coverage differs") + return { + "ambient_six_spaces": 788035, + "full_axis_maximum": 20, + "twenty_label_sets": 16, + "orthogonal_four_frames": len(frames), + "intersection_histogram": dict(sorted(intersections.items())), + "actual_axis_punctures": checked, + "orthogonal_pair_orbit": orthogonal_orbit(g, roots), + } + + +if __name__ == "__main__": + result = check() + print("PASS_INDEPENDENT_D6_PUNCTURE", json.dumps(result, sort_keys=True)) diff --git a/research/p112-mixed-support38/test_verify.py b/research/p112-mixed-support38/test_verify.py new file mode 100644 index 0000000000..6e31facf03 --- /dev/null +++ b/research/p112-mixed-support38/test_verify.py @@ -0,0 +1,106 @@ +"""Behavioral controls, including optimized authentication failures.""" + +import json +import shutil +import tempfile +import unittest +from pathlib import Path + +import independent_check +import verify + + +class Controls(unittest.TestCase): + def test_binary_rank_boundary(self): + self.assertEqual(len(verify.basis([1, 2, 3, 4])), 3) + self.assertEqual(independent_check.binary_rank([1, 2, 3, 4]), 3) + with self.assertRaises(ValueError): + verify.basis([512]) + with self.assertRaises(ValueError): + independent_check.binary_rank([-1]) + + def test_live_axis_contract(self): + with self.assertRaises(ValueError): + verify.rank6_capacity(tuple(range(29))) + with self.assertRaises(ValueError): + verify.rank6_capacity((1,) * 29) + + def test_threshold_budget(self): + self.assertGreater(2 * (78 - 38), 22 + 22 + 32) + self.assertEqual(82 - 38, 12 + 12 + 20) + self.assertLess(82 - 39, 12 + 12 + 20) + self.assertGreater(20, 18) + + def test_unpunctured_control(self): + g = verify.geometry() + roots, _, _, coordinates = g.root_data() + full_labels = [ + 1 | sum((int(x) & 1) << (i + 1) for i, x in enumerate(c)) + for c in coordinates + ] + a, b = (0, 0, 0, 0, 0, 2, -2, 0), (0, 2, -2, 0, 0, 0, 0, 0) + values = [ + v + for r, v in zip(roots, full_labels, strict=True) + if g.dot(a, r) and not g.dot(b, r) + ] + self.assertEqual(len(independent_check.maximal_axis_subsets(values)), 16) + + def source_fixture(self, temporary): + root = Path(temporary) + package = root / "research/p112-mixed-support38" + package.mkdir(parents=True) + shutil.copyfile(verify.PACKAGE / "SOURCES.json", package / "SOURCES.json") + for path in verify.INPUTS: + destination = root / path + destination.parent.mkdir(parents=True, exist_ok=True) + shutil.copyfile(verify.ROOT / path, destination) + for path in verify.RETAINED: + destination = package / path + destination.parent.mkdir(parents=True, exist_ok=True) + shutil.copyfile(verify.PACKAGE / path, destination) + return root, package + + def test_corrupt_source(self): + with tempfile.TemporaryDirectory() as temporary: + root, package = self.source_fixture(temporary) + verify.authenticate(package, root) + (root / verify.GEOMETRY).write_text("altered") + with self.assertRaisesRegex(ValueError, "source SHA256"): + verify.authenticate(package, root) + + def test_inventory_rejections(self): + for mutation in ("missing", "duplicate", "escape", "extra"): + with ( + self.subTest(mutation=mutation), + tempfile.TemporaryDirectory() as temporary, + ): + root, package = self.source_fixture(temporary) + path = package / "SOURCES.json" + sources = json.loads(path.read_text()) + if mutation == "missing": + sources["retained_files"].pop() + elif mutation == "duplicate": + sources["retained_files"][1] = sources["retained_files"][0] + elif mutation == "escape": + sources["files"][-1]["path"] = "../../outside" + else: + sources["unexpected"] = [] + path.write_text(json.dumps(sources)) + with self.assertRaises(ValueError): + verify.authenticate(package, root) + + def test_link_and_size_rejections(self): + with tempfile.TemporaryDirectory() as temporary: + path = Path(temporary) / "large" + path.write_bytes(b"x" * 100) + with self.assertRaisesRegex(ValueError, "size limit"): + verify.read_bytes(path, limit=10) + linked = Path(temporary) / "linked" + linked.symlink_to(path) + with self.assertRaisesRegex(ValueError, "linked"): + verify.read_bytes(linked) + + +if __name__ == "__main__": + unittest.main(verbosity=2) diff --git a/research/p112-mixed-support38/vendor/pr3260-PROOF.md b/research/p112-mixed-support38/vendor/pr3260-PROOF.md new file mode 100644 index 0000000000..3b013e786a --- /dev/null +++ b/research/p112-mixed-support38/vendor/pr3260-PROOF.md @@ -0,0 +1,142 @@ +# Mixed endpoints and a literal TWOSIDE caller + +Let K be a characteristic-zero field. On the fixed 112 nonframe E8 root +lines, let C be the root-evaluation code. Binary support rank means the rank +over F2 of the nine-bit labels in a vector's support. Write pi_S for deletion +of one common set S of coordinates. + +**Mixed shortening theorem.** If |S| <= 37 and three vectors q_1,q_2,q_3 +have binary support ranks at most 5,5,6 respectively, then + +``` +dim_K(pi_S(C) intersect span_K(pi_S(q_1),pi_S(q_2),pi_S(q_3))) <= 1. +``` + +No independence, quotient-basis, modal-shift or real-coefficient hypothesis is +imposed on the pieces. The bound also applies when the rank conditions hold +only after deletion. This is a sufficient threshold, with no sharpness claim. + +## Exact inherited premises + +PR3249 at `22c7bf316d55e59f381cc9ba833afccc7702fd58` supplies the rank-five +live-support capacity 12 and full E8 A2 projective-fiber capacity 10. +PR3255 at `2977a895c35fa019f53f181edee45177c77ec436` supplies the rank-six +live-support capacity 20 and fiber capacity 16. Their proofs and complete +receipts are retained byte for byte. The global 3,309,747 five-flat and +788,035 six-flat censuses are inherited and are not rerun here. + +This package rechecks the 1,120 A2 planes, their P112 union sizes 78 or 80, +the chamber inventories and the three 27-line fibers of a representative +A2 plane. It checks every 2,667 codimension-two subspace and every 127 +hyperplanes in each fiber's seven-dimensional binary span, giving maxima +10 and 16. Every nonzero projective fiber has size 27 or 1. As proved in +the retained sources, simple reflections preserve label rank and are +transitive on A2 planes. These uniform transport facts are inherited here. + +The standard real Weyl-chamber theorem and the characteristic-zero +rational-nullspace transfer remain written dependencies. Neither finite +checks nor this proof constitute proof-kernel verification. + +## Prove classification before counting + +Suppose the displayed intersection contains two independent vectors. Choose +codeword lifts c_h,c_k, and let U be the union of their full supports. +Their restricted coordinates are linear combinations of the three pieces. +The global capacities give + +``` +|U| <= |S| + 12 + 12 + 20 <= 81. +``` + +For ranks bounded only after deletion, replace each q_i by its zero extension +from the remaining coordinates. This preserves the restricted span and gives +the same capacity bounds. In particular the two lifted directions h,k are +independent. At least 31 live root lines are perpendicular to both. The +rational span of all perpendicular full E8 roots has rank at most six, +since its rational matrix has the two independent vectors h,k in its kernel +over K. Rational matrix rank is unchanged by characteristic-zero extension. + +Choose a generic real vector perpendicular to this rational root span. Its +perpendicular roots are exactly the same set: an additional root cannot lie +in the rational span without being perpendicular to h,k, and the other +finitely many coincidences can be avoided. Weyl-chamber classification makes +this subsystem conjugate to a parabolic subsystem of rank at most six. +Among the rank-six parabolics, only E6 has more than 30 root lines. All +lower-rank parabolics embed in one of these. Thus the subsystem is E6 and +the two-dimensional normal plane is an A2 plane. Its P112 nonzero evaluation +union has size at least 78. + +This argument does not use the inequality |S|+20<53, which fails at this +support size. It does not use the rank-six quotient-normalization proof in +PR3255. At support 38, the bound becomes 82 and leaves only 30 perpendicular +live roots. The present classification argument then stops. This is not a +counterexample or a sharp boundary for the theorem. + +## Count singleton coordinates + +Replace h,k by a rational basis of the A2 normal plane. For every t outside +S, a fixed two-by-three matrix A satisfies + +``` +(c_h(t),c_k(t))^T = A * (q_1(t),q_2(t),q_3(t))^T. +``` + +Let N=|U minus S|, so N>=78-|S|. At a site in this union where exactly one +piece is nonzero, the evaluation pair is proportional to the corresponding +column of A. The singleton sites assigned to one piece therefore lie in +one A2 projective fiber. A zero column has no singleton sites. The rank +conditions and inherited fiber capacities give at most 10,10,16 such sites +for the three pieces. Their total L is at most 36. + +Let M count all piece incidences on U minus S. The global support capacities +give M<=12+12+20=44. Each nonsingleton site has at least two incidences, so + +``` +2N <= M+L <= 44+36 = 80. +``` + +But |S|<=37 gives N>=41, hence 82<=80, a contradiction. Arbitrary piece +values, dependencies, cancellations, and incidences outside U are permitted. +No common shift is optimized or assumed modal. + +## Apply the theorem to 5^5,6^5 + +Suppose ten independent pieces span T with dim(T intersect C)>=6 and binary +rank bounds `5,5,5,5,5,6,6,6,6,6`. Delete four weight-six pieces and let T' +be the span of the other six. Projection onto the four deleted coefficients +has rank at most four on T intersect C. Thus + +``` +dim(T' intersect C) >= 6-4 = 2. +``` + +The three first rank-five pieces have one common support S with +|S|<=3*12=36. The remaining endpoints have ranks 5,5,6. Restriction to the +complement of S is injective on C because every nonzero codeword has support +at least 53 and 36<53. The two code dimensions therefore survive restriction +and lie in the span of the three restricted endpoints. The theorem gives +dimension at most one. Numerically its contradiction here is 84<=80. + +The deleted pieces need no support or coefficient restriction for this +projection argument. Their stated rank-six bounds matter only for binding +the original literal profile. All statements are over K. + +## Historical binding, scope and credit + +The profile belongs to PR3154's historical TWOSIDE `(b,t)=(6,4)` cell. Its +excess is 35<36. The local transcription and unchanged original bk 2 b functions +agree on every multiset in that cell and reproduce all 69 historical survivors. +The original root/label data bind to the current convention by an invertible +nine-bit map, checked on all 112 entries. Historical survival is not a claim +that the other 68 profiles remain unresolved. + +Earlier uniform support thresholds for A2/A3/A4/A5 do not directly cover the +common support 36. A pre-reservation `4,5^9` candidate was rejected because +PR3171 already covers it. No result for that profile is counted here. The +public overlap scan is not an exhaustive logical implication or novelty audit. + +The contribution is the mixed-rank proof and this literal caller implication. +It does not establish full C5, the decoder floor, a physical supplier, native +restoration, an all-size multiplication theorem, new kappa or a selected result. +Credit DreamingOfClouds/PR3154, Nick Petalas/PR3249/3255 and the retained +root-simplex/E8/P112 lineage including joaqcoo. Frozen predecessors are unchanged. diff --git a/research/p112-mixed-support38/vendor/pr3260-RESULT.json b/research/p112-mixed-support38/vendor/pr3260-RESULT.json new file mode 100644 index 0000000000..12e77eb5b7 --- /dev/null +++ b/research/p112-mixed-support38/vendor/pr3260-RESULT.json @@ -0,0 +1,1010 @@ +{ + "application": { + "bound": { + "A2_classification_valid": true, + "code_union_cap": 80, + "common_support": 36, + "excluded": true, + "global_piece_capacity": 44, + "incidence_plus_singletons_cap": 80, + "ranks": [ + 5, + 5, + 6 + ], + "required_twice_residual_union": 84, + "singleton_capacity": 36 + }, + "cell": [ + 6, + 4 + ], + "deleted": 4, + "profile": [ + 5, + 5, + 5, + 5, + 5, + 6, + 6, + 6, + 6, + 6 + ], + "retained": [ + 5, + 5, + 5, + 5, + 5, + 6 + ], + "retained_code_dimension": 2, + "small": [ + 5, + 5, + 5 + ] + }, + "geometry": { + "A2_union_histogram": { + "78": 896, + "80": 224 + }, + "chamber": { + "rank_six_parabolic_counts": [ + 21, + 21, + 12, + 12, + 15, + 21, + 30, + 16, + 13, + 12, + 13, + 16, + 21, + 12, + 10, + 10, + 12, + 16, + 10, + 8, + 8, + 10, + 13, + 12, + 13, + 21, + 21, + 36 + ], + "ray_zero_counts": [ + 42, + 28, + 22, + 14, + 16, + 23, + 37, + 63 + ], + "root_support_histogram": { + "53": 112, + "56": 8 + }, + "simple_reflection_checks": 960 + }, + "fibers": [ + { + "rank5": { + "0": 63, + "10": 216, + "3": 45, + "4": 270, + "5": 216, + "6": 792, + "7": 270, + "8": 675, + "9": 120 + }, + "rank6": { + "0": 1, + "11": 27, + "12": 36, + "15": 36, + "16": 27 + } + }, + { + "rank5": { + "0": 63, + "10": 216, + "3": 45, + "4": 270, + "5": 216, + "6": 792, + "7": 270, + "8": 675, + "9": 120 + }, + "rank6": { + "0": 1, + "11": 27, + "12": 36, + "15": 36, + "16": 27 + } + }, + { + "rank5": { + "0": 63, + "10": 216, + "3": 45, + "4": 270, + "5": 216, + "6": 792, + "7": 270, + "8": 675, + "9": 120 + }, + "rank6": { + "0": 1, + "11": 27, + "12": 36, + "15": 36, + "16": 27 + } + } + ] + }, + "global_flat_censuses_replayed": false, + "historical_cell_survivors": [ + [ + 2, + 7, + 7, + 7, + 7, + 7, + 7, + 7 + ], + [ + 2, + 2, + 7, + 7, + 7, + 7, + 7, + 7, + 7 + ], + [ + 2, + 6, + 6, + 6, + 6, + 6, + 6, + 6, + 6 + ], + [ + 2, + 6, + 6, + 6, + 6, + 6, + 6, + 6, + 7 + ], + [ + 2, + 6, + 6, + 6, + 6, + 6, + 6, + 7, + 7 + ], + [ + 2, + 6, + 6, + 6, + 6, + 6, + 7, + 7, + 7 + ], + [ + 3, + 6, + 6, + 6, + 6, + 6, + 6, + 6, + 6 + ], + [ + 3, + 6, + 6, + 6, + 6, + 6, + 6, + 6, + 7 + ], + [ + 3, + 6, + 6, + 6, + 6, + 6, + 6, + 7, + 7 + ], + [ + 4, + 5, + 6, + 6, + 6, + 6, + 6, + 6, + 6 + ], + [ + 4, + 5, + 6, + 6, + 6, + 6, + 6, + 6, + 7 + ], + [ + 4, + 5, + 6, + 6, + 6, + 6, + 6, + 7, + 7 + ], + [ + 4, + 6, + 6, + 6, + 6, + 6, + 6, + 6, + 6 + ], + [ + 4, + 6, + 6, + 6, + 6, + 6, + 6, + 6, + 7 + ], + [ + 5, + 5, + 6, + 6, + 6, + 6, + 6, + 6, + 6 + ], + [ + 5, + 5, + 6, + 6, + 6, + 6, + 6, + 6, + 7 + ], + [ + 5, + 6, + 6, + 6, + 6, + 6, + 6, + 6, + 6 + ], + [ + 2, + 2, + 2, + 7, + 7, + 7, + 7, + 7, + 7, + 7 + ], + [ + 2, + 2, + 3, + 6, + 7, + 7, + 7, + 7, + 7, + 7 + ], + [ + 2, + 2, + 4, + 5, + 7, + 7, + 7, + 7, + 7, + 7 + ], + [ + 2, + 2, + 6, + 6, + 6, + 6, + 6, + 6, + 6, + 6 + ], + [ + 2, + 2, + 6, + 6, + 6, + 6, + 6, + 6, + 6, + 7 + ], + [ + 2, + 2, + 6, + 6, + 6, + 6, + 6, + 6, + 7, + 7 + ], + [ + 2, + 2, + 6, + 6, + 6, + 6, + 6, + 7, + 7, + 7 + ], + [ + 2, + 3, + 3, + 5, + 7, + 7, + 7, + 7, + 7, + 7 + ], + [ + 2, + 3, + 4, + 4, + 7, + 7, + 7, + 7, + 7, + 7 + ], + [ + 2, + 3, + 5, + 6, + 6, + 6, + 6, + 6, + 6, + 6 + ], + [ + 2, + 3, + 5, + 6, + 6, + 6, + 6, + 6, + 6, + 7 + ], + [ + 2, + 3, + 5, + 6, + 6, + 6, + 6, + 6, + 7, + 7 + ], + [ + 2, + 3, + 5, + 6, + 6, + 6, + 6, + 7, + 7, + 7 + ], + [ + 2, + 3, + 6, + 6, + 6, + 6, + 6, + 6, + 6, + 6 + ], + [ + 2, + 3, + 6, + 6, + 6, + 6, + 6, + 6, + 6, + 7 + ], + [ + 2, + 3, + 6, + 6, + 6, + 6, + 6, + 6, + 7, + 7 + ], + [ + 2, + 4, + 4, + 6, + 6, + 6, + 6, + 6, + 6, + 6 + ], + [ + 2, + 4, + 4, + 6, + 6, + 6, + 6, + 6, + 6, + 7 + ], + [ + 2, + 4, + 4, + 6, + 6, + 6, + 6, + 6, + 7, + 7 + ], + [ + 2, + 4, + 4, + 6, + 6, + 6, + 6, + 7, + 7, + 7 + ], + [ + 2, + 4, + 5, + 6, + 6, + 6, + 6, + 6, + 6, + 6 + ], + [ + 2, + 4, + 5, + 6, + 6, + 6, + 6, + 6, + 6, + 7 + ], + [ + 2, + 4, + 5, + 6, + 6, + 6, + 6, + 6, + 7, + 7 + ], + [ + 2, + 4, + 6, + 6, + 6, + 6, + 6, + 6, + 6, + 6 + ], + [ + 2, + 4, + 6, + 6, + 6, + 6, + 6, + 6, + 6, + 7 + ], + [ + 2, + 5, + 5, + 5, + 6, + 6, + 6, + 6, + 6, + 6 + ], + [ + 2, + 5, + 5, + 5, + 6, + 6, + 6, + 6, + 6, + 7 + ], + [ + 2, + 5, + 5, + 5, + 6, + 6, + 6, + 6, + 7, + 7 + ], + [ + 2, + 5, + 5, + 6, + 6, + 6, + 6, + 6, + 6, + 6 + ], + [ + 2, + 5, + 5, + 6, + 6, + 6, + 6, + 6, + 6, + 7 + ], + [ + 2, + 5, + 6, + 6, + 6, + 6, + 6, + 6, + 6, + 6 + ], + [ + 3, + 3, + 5, + 6, + 6, + 6, + 6, + 6, + 6, + 6 + ], + [ + 3, + 3, + 5, + 6, + 6, + 6, + 6, + 6, + 6, + 7 + ], + [ + 3, + 3, + 5, + 6, + 6, + 6, + 6, + 6, + 7, + 7 + ], + [ + 3, + 3, + 6, + 6, + 6, + 6, + 6, + 6, + 6, + 6 + ], + [ + 3, + 3, + 6, + 6, + 6, + 6, + 6, + 6, + 6, + 7 + ], + [ + 3, + 4, + 4, + 6, + 6, + 6, + 6, + 6, + 6, + 6 + ], + [ + 3, + 4, + 4, + 6, + 6, + 6, + 6, + 6, + 6, + 7 + ], + [ + 3, + 4, + 4, + 6, + 6, + 6, + 6, + 6, + 7, + 7 + ], + [ + 3, + 4, + 5, + 6, + 6, + 6, + 6, + 6, + 6, + 6 + ], + [ + 3, + 4, + 5, + 6, + 6, + 6, + 6, + 6, + 6, + 7 + ], + [ + 3, + 4, + 6, + 6, + 6, + 6, + 6, + 6, + 6, + 6 + ], + [ + 3, + 5, + 5, + 5, + 6, + 6, + 6, + 6, + 6, + 6 + ], + [ + 3, + 5, + 5, + 5, + 6, + 6, + 6, + 6, + 6, + 7 + ], + [ + 3, + 5, + 5, + 6, + 6, + 6, + 6, + 6, + 6, + 6 + ], + [ + 4, + 4, + 4, + 6, + 6, + 6, + 6, + 6, + 6, + 6 + ], + [ + 4, + 4, + 4, + 6, + 6, + 6, + 6, + 6, + 6, + 7 + ], + [ + 4, + 4, + 5, + 5, + 6, + 6, + 6, + 6, + 6, + 6 + ], + [ + 4, + 4, + 5, + 5, + 6, + 6, + 6, + 6, + 6, + 7 + ], + [ + 4, + 4, + 5, + 6, + 6, + 6, + 6, + 6, + 6, + 6 + ], + [ + 4, + 5, + 5, + 5, + 6, + 6, + 6, + 6, + 6, + 6 + ], + [ + 5, + 5, + 5, + 5, + 5, + 6, + 6, + 6, + 6, + 6 + ] + ], + "historical_count": 69, + "schema": "p112-mixed-a2-caller/v1", + "theorem_support37": { + "A2_classification_valid": true, + "code_union_cap": 81, + "common_support": 37, + "excluded": true, + "global_piece_capacity": 44, + "incidence_plus_singletons_cap": 80, + "ranks": [ + 5, + 5, + 6 + ], + "required_twice_residual_union": 82, + "singleton_capacity": 36 + }, + "unclaimed_support38": { + "A2_classification_valid": false, + "code_union_cap": 82, + "common_support": 38, + "excluded": false, + "global_piece_capacity": 44, + "incidence_plus_singletons_cap": 80, + "ranks": [ + 5, + 5, + 6 + ], + "required_twice_residual_union": 80, + "singleton_capacity": 36 + } +} diff --git a/research/p112-mixed-support38/vendor/pr3262-PROOF.md b/research/p112-mixed-support38/vendor/pr3262-PROOF.md new file mode 100644 index 0000000000..315adf2b2a --- /dev/null +++ b/research/p112-mixed-support38/vendor/pr3262-PROOF.md @@ -0,0 +1,190 @@ +# Sharp rank-six three-piece shortening on P112 + +Fix the 112 nonframe E8 root lines and nine-bit labels reconstructed by the +pinned geometry. Let K have characteristic zero. With doubled root +representatives r_t, put + +```text +C = {(r_t dot h)_t : h in K^8}. +``` + +For a common coordinate set S, let pi_S delete S. The binary support rank of +a piece is the F2 rank of its live labels. Coefficients belong to K. + +**Theorem.** If |S| <= 29 and each of three residual pieces has binary support +rank at most six, their span meets pi_S(C) in dimension at most one. The +pieces may be dependent and their coefficients are arbitrary. The uniform +threshold 29 is sharp. The literal common-cut-30 witness in RESULT.json has +three independent pieces of binary rank six and code intersection dimension +two. + +PR3255, pinned at `2977a895c35fa019f53f181edee45177c77ec436`, proved the +sufficient threshold 21 using singleton capacity sixteen. The new step +couples singleton capacity to the endpoint's total support and retains the +actual orthogonal puncture. No historical profile exclusion, full C5, +decoder floor, supplier, all-size multiplication theorem or kappa follows +from this package alone. + +## Geometric dependencies + +The pinned root-simplex proof supplies these characteristic-zero statements. +Every nonzero word of C has support at least 53. Any nonzero word with support +strictly below 70 is proportional to a root word. Every third root line in +a plane through two root lines is the A2 sum or difference. The primary +replay checks the finite chamber counts, all 960 simple reflections and all +7,140 root-line pairs underlying those statements. The Weyl-chamber theorem +and its rational-kernel extension remain written dependencies. + +Every binary six-space contains at most twenty P112 labels. The replay +checks all 788,035 such spaces through unique three-dimensional annihilators. +A lower-dimensional space extends to a six-space, so the bound holds for +binary rank at most six. + +There are 1,120 A2 root planes in E8. The eight simple reflections act +transitively on them. On the fixed P112, their nonzero evaluation unions +have sizes 78 and 80, with multiplicities 896 and 224. The corresponding +full E8 union has 84 lines. Thus the orthogonal eight-line frame removes +at most six positive coordinates, improving the arbitrary-eight-cut +relaxation used in PR3255. + +The replay checks transitivity and verifies that each reflection induces an +invertible linear map on the nine-bit labels. Specifically, the labels span +nine dimensions and the 120 paired input/output labels span the graph of a +nine-dimensional linear map. The root permutation is bijective. Hence +binary ranks and the closure bounds below transport to every A2 plane. + +## Normalize a putative two-dimensional intersection + +Replace each piece by its restriction outside S and call the pieces q_i. +No nonzero scalar multiple of one q_i can belong to pi_S(C). Its unique +code lift would have support at most |S|+20 <=49<53. The same distance +bound makes pi_S injective on C. + +Suppose D = span(q_0,q_1,q_2) intersect pi_S(C) has dimension at least two. +The pieces must be independent. Otherwise their span has dimension at most +two and equals D, contradicting the preceding observation for any nonzero +piece. Their span has dimension three and D has dimension exactly two, +since dimension three would again put every piece in pi_S(C). + +The quotient by D is one-dimensional and each q_i has nonzero image. +Rescale the pieces so that their quotient images agree. Supports and +binary ranks do not change. The two differences q_1-q_0 and q_2-q_0 are +independent restricted codewords. Lift them uniquely to c_h and c_k. +Each of c_h, c_k and c_h-c_k has support at most |S|+40 <=69<70, so each +is a nonzero scalar root word. + +The root-plane fact gives h=z*a and k=z*b for one nonzero z in K and +oriented doubled roots with a dot b=4. Indeed, the third root direction +forces the two scalar coefficients to have ratio +1 or -1. Orient the +roots to absorb the signs. Their difference is then a root. This reasoning +also holds over K by solving a nonsingular rational coordinate minor. +The vertices 0,a,b are an A2 simplex. Outside S the three piece values are +z times its evaluations plus one arbitrary coordinate shift. In particular, +the shift need not minimize support. + +## Joint singleton and total-support capacity + +For the simplex 0,a,b, full E8 has 36 coordinates where the evaluations +agree, three where they are all distinct, and three disjoint singleton +classes A_i of 27 coordinates each. In A_i, endpoint i differs from the +other two equal endpoints. Each A_i spans a binary seven-space W_i. + +Here is the complete hyperplane inventory inside any one W_i. The first +column counts all full E8 labels in a hyperplane V; the second counts +labels from A_i. + +| Full support | Singleton support | Hyperplanes | +|---:|---:|---:| +| 0 | 0 | 1 | +| 12 | 11 | 27 | +| 12 | 12 | 36 | +| 16 | 15 | 36 | +| 16 | 16 | 27 | + +The 127 nonzero functionals of W_i enumerate its 127 hyperplanes exactly +once. Their maximum support-plus-singleton count is 32. The separate +2,667-subspace census in each W_i shows that any binary space of dimension +at most five meets A_i in at most ten labels. These are full E8 statements; +removing frame or common-cut coordinates cannot increase the bounds. + +Consider the actual binary support span V_i of q_i. If +`dim(V_i intersect W_i)<=5`, its singleton support is at most ten and its +total P112 support at most twenty, giving sum at most thirty. Otherwise +V_i has dimension six and is contained in W_i. It is one of the enumerated +hyperplanes, whose total full E8 support plus singleton support is at most +32. The actual supports are subsets of those intersections. Therefore, +with M_i the total residual support and J_i its own singleton support, + +```text +M_i + J_i <= 32. +``` + +This argument covers all ambient six-spaces, including those not contained +in a singleton seven-space. It does not assume that a piece fills its +binary closure or uses a modal shift. A change of simplex orientation +permutes its three large projective fibers, so the checked three classes +and plane transitivity cover every normalized simplex. + +## Count arbitrary shifts + +Let U be the union of the two full code supports. The A2 inventory gives +|U|>=78. Write x_i(t)=1 when q_i(t) is nonzero. At a singleton coordinate +of A_i outside S, an arbitrary common shift satisfies + +```text +x_0(t)+x_1(t)+x_2(t) >= 2-x_i(t). +``` + +If x_i=0, both other values are nonzero. If x_i=1, the sum is at least one. +At an all-distinct coordinate the sum is at least two. Sum over U outside S. +Extra piece support elsewhere only increases M_i. Consequently + +```text +2*|U minus S| <= sum_i (M_i+J_i) <= 96. +``` + +For |S|<=29 the left side is at least `2*(78-29)=98`, a contradiction. +This proves the theorem over every characteristic-zero field. + +## Literal sharpness witness at thirty + +Use the doubled roots + +```text +a = (0,0,0,0,0,2,-2,0), +b = (0,0,0,-2,0,2,0,0). +``` + +Their live union has 78 coordinates. For each singleton class choose the +lexicographically first sixteen-label hyperplane intersection containing +only live labels. Each chosen set has binary rank six. The sets are +disjoint. Delete the other thirty union coordinates as ONE common set S. +On the chosen singleton supports define + +```text +q_0(t) = -(a dot r_t), +q_1(t) = a dot r_t, +q_2(t) = b dot r_t, +``` + +respectively, and set each piece to zero elsewhere. Then outside S, +`q_1-q_0=pi_S(c_a)` and `q_2-q_0=pi_S(c_b)`. All 48 support coefficients +are nonzero. The exact indices and coefficients are committed in +RESULT.json and regenerated from the pinned source ordering. Rational +elimination gives code rank 8, piece rank 3 and joined rank 9. Thus the +intersection dimension is exactly `8+3-9=2`. No finite counting equality +is substituted for this actual witness. + +## Credit and limits + +The affine quotient and arbitrary-shift argument follows Nick Petalas's +PR3255. The rank-five capacity and projective-fiber perspective follow +PR3249, with the root-simplex geometry from the retained PR3161/3162/3164 +lineage. DreamingOfClouds/PR3154 supplies the C5 motivation. The original +E8/P112 lineage, including joaqcoo, retains its credit. + +Worker1's concurrent rank-five equality audit and worker5's mixed-rank +caller have distinct endpoint hypotheses. No result from either is needed +here. A use in TWOSIDE still needs a separately checked caller reduction. +This proof is written and supported by finite exact checks. It is not a +proof-kernel or independent human verification. diff --git a/research/p112-mixed-support38/vendor/pr3262-RESULT.json b/research/p112-mixed-support38/vendor/pr3262-RESULT.json new file mode 100644 index 0000000000..cf90559a4e --- /dev/null +++ b/research/p112-mixed-support38/vendor/pr3262-RESULT.json @@ -0,0 +1,327 @@ +{ + "a2_planes": { + "planes": 1120, + "reflection_maps": 8, + "union_histogram": { + "78": 896, + "80": 224 + } + }, + "chamber": { + "rank_six_parabolic_counts": [ + 21, + 21, + 12, + 12, + 15, + 21, + 30, + 16, + 13, + 12, + 13, + 16, + 21, + 12, + 10, + 10, + 12, + 16, + 10, + 8, + 8, + 10, + 13, + 12, + 13, + 21, + 21, + 36 + ], + "ray_zero_counts": [ + 42, + 28, + 22, + 14, + 16, + 23, + 37, + 63 + ], + "root_support_histogram": { + "53": 112, + "56": 8 + }, + "simple_reflection_checks": 960 + }, + "claim": "sharp-three-rank6-common-support29-intersection-at-most-one", + "class_receipts": [ + { + "five_spaces": 2667, + "hyperplanes": 127, + "joint_total_singleton_histogram": { + "0,0": 1, + "12,11": 27, + "12,12": 36, + "16,15": 36, + "16,16": 27 + }, + "maximizing_sets_sha256": "ed525c23b52e841337e30acf77569978270e3859c22e3a58bf120c90764c357e", + "rank_five_singleton_maximum": 10, + "support_plus_singleton_maximum": 32 + }, + { + "five_spaces": 2667, + "hyperplanes": 127, + "joint_total_singleton_histogram": { + "0,0": 1, + "12,11": 27, + "12,12": 36, + "16,15": 36, + "16,16": 27 + }, + "maximizing_sets_sha256": "53c4fc5d54d26eeb985bdfa0555e8a198d873c7061bc345ff9c42e38874e297e", + "rank_five_singleton_maximum": 10, + "support_plus_singleton_maximum": 32 + }, + { + "five_spaces": 2667, + "hyperplanes": 127, + "joint_total_singleton_histogram": { + "0,0": 1, + "12,11": 27, + "12,12": 36, + "16,15": 36, + "16,16": 27 + }, + "maximizing_sets_sha256": "6a0df306511fd230bfc87dc22886a57a8f40bb312b09e4d2bb5ae178cb7e239a", + "rank_five_singleton_maximum": 10, + "support_plus_singleton_maximum": 32 + } + ], + "root_planes": { + "2": 3780, + "3": 3360 + }, + "scope": "fixed P112; characteristic zero; arbitrary residual coefficients", + "six_flat_capacity": { + "dimension": 6, + "histogram": { + "0": 10796, + "10": 56448, + "11": 86016, + "12": 124040, + "14": 131712, + "15": 143360, + "16": 141491, + "18": 33152, + "19": 28672, + "20": 19152, + "4": 56, + "6": 896, + "7": 4096, + "8": 8148 + }, + "maximum": 20, + "subspaces": 788035 + }, + "support29": { + "allowed": 96, + "required_twice_union": 98 + }, + "support30_counting_boundary": { + "allowed": 96, + "required_twice_union": 96 + }, + "witness30": { + "code_difference_coefficients": [ + [ + -1, + 1, + 0 + ], + [ + -1, + 0, + 1 + ] + ], + "common_cut_indices": [ + 0, + 3, + 4, + 7, + 9, + 10, + 13, + 14, + 18, + 21, + 28, + 31, + 38, + 44, + 48, + 49, + 54, + 55, + 59, + 65, + 70, + 76, + 80, + 81, + 86, + 87, + 91, + 97, + 104, + 107 + ], + "directions": [ + [ + 0, + 0, + 0, + 0, + 0, + 2, + -2, + 0 + ], + [ + 0, + 0, + 0, + -2, + 0, + 2, + 0, + 0 + ] + ], + "intersection_dimension": 2, + "piece_binary_ranks": [ + 6, + 6, + 6 + ], + "piece_coefficients": [ + [ + -4, + -4, + 4, + -4, + 4, + -4, + -4, + 4, + -4, + 4, + -4, + 4, + -4, + 4, + 4, + -4 + ], + [ + -4, + -4, + 4, + 4, + -4, + -4, + 4, + 4, + -4, + -4, + 4, + 4, + -4, + -4, + 4, + 4 + ], + [ + -4, + -4, + -4, + -4, + 4, + -4, + 4, + 4, + -4, + -4, + 4, + 4, + -4, + -4, + 4, + -4 + ] + ], + "piece_support_indices": [ + [ + 1, + 2, + 17, + 22, + 27, + 32, + 42, + 45, + 58, + 61, + 74, + 77, + 90, + 93, + 103, + 108 + ], + [ + 37, + 41, + 46, + 50, + 53, + 57, + 62, + 66, + 69, + 73, + 78, + 82, + 85, + 89, + 94, + 98 + ], + [ + 8, + 11, + 12, + 15, + 25, + 34, + 39, + 43, + 60, + 64, + 71, + 75, + 92, + 96, + 101, + 110 + ] + ], + "rational_ranks_code_pieces_join": [ + 8, + 3, + 9 + ] + } +} diff --git a/research/p112-mixed-support38/verify.py b/research/p112-mixed-support38/verify.py new file mode 100644 index 0000000000..b4bf0200e1 --- /dev/null +++ b/research/p112-mixed-support38/verify.py @@ -0,0 +1,330 @@ +"""Mixed-rank P112 support38 boundary. Nick Petalas. Apache-2.0.""" + +import argparse +import hashlib +import importlib.util +import json +from collections import Counter +from itertools import combinations +from pathlib import Path + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parents[1] +GEOMETRY = "research/p112-root-simplex-exclusion/geometry.py" +INPUTS = { + GEOMETRY, + "research/p112-root-simplex-exclusion/PROOF.md", + "research/p112-root-simplex-exclusion/RESULT.json", +} +RETAINED = { + f"vendor/pr{pr}-{name}" + for pr in (3260, 3262) + for name in ("PROOF.md", "RESULT.json") +} + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def read_bytes(path, limit=1_000_000): + require(path.is_file() and not path.is_symlink(), "missing or linked file") + require(path.stat().st_size <= limit, "file size limit") + return path.read_bytes() + + +def authenticate(package=PACKAGE, root=ROOT): + source = json.loads(read_bytes(package / "SOURCES.json")) + require( + set(source) == {"schema_version", "base_commit", "files", "retained_files"}, + "source inventory fields", + ) + rows, retained = source["files"], source["retained_files"] + require(type(rows) is list and len(rows) == 5, "source inventory length") + require(type(retained) is list and len(retained) == 4, "retained inventory length") + live = [r for r in rows if r["usage"] == "input"] + require( + len(live) == 3 and {r["path"] for r in live} == INPUTS, "live source inventory" + ) + require({r["local_path"] for r in retained} == RETAINED, "retained path inventory") + for row in live + retained: + path = root / row["path"] if "path" in row else package / row["local_path"] + raw = read_bytes(path) + require(hashlib.sha256(raw).hexdigest() == row["sha256"], "source SHA256") + blob = hashlib.sha1(b"blob " + str(len(raw)).encode() + b"\0" + raw).hexdigest() + require(blob == row["git_blob"], "source Git blob") + return source + + +def geometry(): + authenticate() + spec = importlib.util.spec_from_file_location("p112_authenticated", ROOT / GEOMETRY) + require(spec is not None and spec.loader is not None, "geometry loader") + module = importlib.util.module_from_spec(spec) + spec.loader.exec_module(module) + return module + + +def basis(values, bits=9): + require(len(values) <= 512 and 1 <= bits <= 18, "binary capacity") + require(all(type(v) is int and 0 <= v < 1 << bits for v in values), "binary input") + rows = [] + for value in values: + for row in rows: + value = min(value, value ^ row) + if value: + rows = sorted( + [min(row, row ^ value) for row in rows] + [value], reverse=True + ) + return tuple(rows) + + +def coordinates(values): + rows = basis(values) + result = {0: 0} + for i, row in enumerate(rows): + result.update({v ^ row: c | (1 << i) for v, c in tuple(result.items())}) + require(len(result) == 1 << len(rows), "independent binary coordinates") + return rows, result + + +def rank6_capacity(values): + """Every six-space in an eight-space, via its unique dual two-space.""" + require(len(values) == len(set(values)) == 29, "live D6 axis size") + rows, codes = coordinates(values) + require(len(rows) == 8, "live D6 axis rank") + masks = [ + sum(1 << i for i, v in enumerate(values) if not (codes[v] & f).bit_count() % 2) + for f in range(256) + ] + counts = Counter( + (masks[f] & masks[h]).bit_count() + for f, h in combinations(range(1, 256), 2) + if h < (f ^ h) + ) + require(sum(counts.values()) == 10795, "complete dual two-space census") + require(max(counts) == 18, "live D6 rank-six capacity") + return counts + + +def d6_receipt(g, roots, points, labels): + gram = [[g.dot(a, b) for b in roots] for a in roots] + live_indices = [roots.index(p) for p in points] + unions, capacities = Counter(), Counter() + records = [] + for a, b in combinations(range(120), 2): + if gram[a][b]: + continue + union = sum(bool(gram[a][t] or gram[b][t]) for t in live_indices) + unions[union] += 1 + if union != 82: + continue + for x, y in ((a, b), (b, a)): + values = tuple( + label + for t, label in zip(live_indices, labels, strict=True) + if gram[x][t] and not gram[y][t] + ) + counts = rank6_capacity(values) + capacities[max(counts)] += 1 + records.append([a, b, x, sorted(counts.items())]) + require( + dict(unions) == {82: 448, 84: 2688, 85: 448, 86: 168, 88: 28}, + "orthogonal-pair puncture spectrum", + ) + require(dict(capacities) == {18: 896}, "minimum-plane axis coverage") + return { + "orthogonal_planes": sum(unions.values()), + "union_histogram": dict(unions), + "live_axis_fibers": 896, + "six_spaces_per_fiber": 10795, + "axis_maximum_histogram": dict(capacities), + "full_census_sha256": hashlib.sha256( + json.dumps(records, separators=(",", ":")).encode() + ).hexdigest(), + } + + +def a2_fiber(values, all_labels): + require(len(values) == 27, "A2 fiber size") + rows, codes = coordinates(values) + require(len(rows) == 7, "A2 fiber rank") + five = Counter() + for f, h in combinations(range(1, 128), 2): + if h < (f ^ h): + five[ + sum( + not (codes[v] & f).bit_count() % 2 + and not (codes[v] & h).bit_count() % 2 + for v in values + ) + ] += 1 + require(sum(five.values()) == 2667 and max(five) == 10, "A2 rank-five capacity") + joint = Counter() + for f in range(1, 128): + space = {v for v, c in codes.items() if not (c & f).bit_count() % 2} + joint[sum(v in space for v in all_labels), sum(v in space for v in values)] += 1 + require( + dict(joint) + == {(0, 0): 1, (12, 11): 27, (12, 12): 36, (16, 15): 36, (16, 16): 27}, + "A2 joint inventory", + ) + return { + "five_spaces": sum(five.values()), + "five_fiber_maximum": max(five), + "hyperplanes": sum(joint.values()), + "joint_maximum": max(sum(k) for k in joint), + } + + +def a2_receipt(g, roots, points, full_labels): + index = {r: i for i, r in enumerate(roots)} + planes = set() + for i, j in combinations(range(120), 2): + d = g.dot(roots[i], roots[j]) + if abs(d) == 4: + third = g.canonical( + tuple(a - d // 4 * b for a, b in zip(roots[i], roots[j], strict=True)) + ) + planes.add(tuple(sorted((i, j, index[third])))) + require(len(planes) == 1120, "A2 plane inventory") + permutations = [] + for simple in g.SIMPLE: + perm = [ + index[ + g.canonical( + tuple( + x - g.dot(r, simple) // 4 * y + for x, y in zip(r, simple, strict=True) + ) + ) + ] + for r in roots + ] + pairs = [full_labels[i] | full_labels[perm[i]] << 9 for i in range(120)] + require( + len(set(perm)) == 120 and len(basis(pairs, 18)) == 9, + "reflection is an invertible label map", + ) + permutations.append(perm) + orbit, queue = {min(planes)}, [min(planes)] + for cursor in range(1120): + require(cursor < len(queue), "A2 orbit ended early") + for perm in permutations: + image = tuple(sorted(perm[i] for i in queue[cursor])) + require(image in planes, "reflection left A2 planes") + if image not in orbit: + orbit.add(image) + queue.append(image) + require(orbit == planes and len(queue) == 1120, "A2 transitivity") + unions = Counter( + sum(any(g.dot(roots[i], p) for i in plane) for p in points) for plane in planes + ) + require(dict(unions) == {78: 896, 80: 224}, "A2 punctured unions") + a, b = (roots[i] for i in min(planes)[:2]) + if g.dot(a, b) == -4: + b = tuple(-x for x in b) + classes = [[] for _ in range(3)] + for r, label in zip(roots, full_labels, strict=True): + values = (0, g.dot(a, r), g.dot(b, r)) + for i in range(3): + other = [j for j in range(3) if j != i] + if values[other[0]] == values[other[1]] != values[i]: + classes[i].append(label) + return { + "planes": 1120, + "union_histogram": dict(unions), + "reflection_maps": 8, + "fibers": [a2_fiber(v, full_labels) for v in classes], + } + + +def chamber_receipt(g, roots, points, coordinates_): + result = g.chamber_receipt(roots, points, coordinates_) + lower_max = max( + sum(all(c[i] == 0 for i in omitted) for c in coordinates_) + for omitted in combinations(range(8), 3) + ) + require(lower_max == 20, "rank-five parabolic bound") + large = [] + for omitted in combinations(range(8), 2): + count = sum(all(c[i] == 0 for i in omitted) for c in coordinates_) + if count >= 30: + normals = [ + r + for r in roots + if all( + g.dot(r, s) == 0 for i, s in enumerate(g.SIMPLE) if i not in omitted + ) + ] + require(len(normals) in (2, 3), "normal root-plane inventory") + kind = "D6" if count == 30 else "E6" + require( + (kind, omitted) in (("D6", (0, 7)), ("E6", (6, 7))), + "rank-six classification changed", + ) + require( + g.dot(normals[0], normals[1]) == 0 if kind == "D6" else True, + "D6 normal roots must be orthogonal", + ) + large.append({"omitted": omitted, "root_lines": count, "kind": kind}) + require(len(large) == 2, "large parabolic coverage") + return { + "large_parabolics": large, + "rank_five_maximum": lower_max, + "chamber": result, + } + + +def receipt(): + g = geometry() + roots, points, labels, coordinates_ = g.root_data() + full_labels = tuple( + 1 | sum((int(x) % 2) << (i + 1) for i, x in enumerate(c)) for c in coordinates_ + ) + result = { + "status": "PASS_MIXED_P112_SUPPORT38", + "common_support": 38, + "endpoint_ranks": [5, 5, 6], + "intersection_upper_bound": 1, + "chamber": chamber_receipt(g, roots, points, coordinates_), + "A2": a2_receipt(g, roots, points, full_labels), + "D6": d6_receipt(g, roots, points, labels), + "budgets": { + "E6_required": 80, + "E6_allowance": 76, + "D6_required": 44, + "D6_total_support": 44, + "D6_rank6_required": 20, + "D6_fiber_maximum": 18, + }, + } + budgets = result["budgets"] + require(budgets["E6_required"] > budgets["E6_allowance"], "E6 contradiction") + require( + budgets["D6_required"] == budgets["D6_total_support"] + and budgets["D6_fiber_maximum"] < budgets["D6_rank6_required"], + "D6 equality contradiction", + ) + return json.loads(json.dumps(result)) + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--output", type=Path) + args = parser.parse_args() + result = receipt() + if args.output: + with args.output.open("x") as f: + json.dump(result, f, indent=2, sort_keys=True) + f.write("\n") + else: + require( + result == json.loads(read_bytes(PACKAGE / "RESULT.json")), "receipt changed" + ) + print(result["status"], "planes=3780 live_fibers=896 rank6_cap=18 no_new_kappa") + + +if __name__ == "__main__": + main()