diff --git a/research/p112-a6-five-flat/CHECKS.json b/research/p112-a6-five-flat/CHECKS.json new file mode 100644 index 0000000000..0b4febb24f --- /dev/null +++ b/research/p112-a6-five-flat/CHECKS.json @@ -0,0 +1,90 @@ +{ + "schema": "p112-a6-five-flat-checks/v1", + "observed_at": "2026-10-17T16:22:44.562297+00:00", + "base_commit": "997e6a9ca7b4f95d50e366f61412fd640d72a88a", + "result_sha256": "f323b66cce53b45f92e9b6dcbe31a80332dff7a82f615498b35b1f92d0b8b464", + "environment": { + "platform": "macOS-27.0.1-arm64-arm-64bit-Mach-O", + "python312": "3.12.15 (main, Oct 14 2026, 00:55:37) [Clang 23.1.3 ]", + "python313": "3.13.16 (main, Oct 14 2026, 00:55:38) [Clang 23.1.3 ]" + }, + "commands": [ + { + "argv": [ + "uv", + "run", + "--python", + "3.12", + "--no-project", + "python", + "-W", + "error", + "-B", + "scripts/research_package.py", + "--package", + "research/p112-a6-five-flat" + ], + "exit_code": 0, + "output": "CHECK Authenticates all retained source bytes; replays both endpoint branches, flat capacities, the weighted predecessor and all64839 affine transfer subsets; exact receipt comparison.\nPASS_A6_FIVE_FLAT profile=5,6^8 mixed=142 root=141 allowance=140 errors=0 six_flats=788035 five_flats=3309747 frames=2025 transfer_subsets=64839\nCHECK Fourteen behavioral groups including source, input, receipt, embedding and strict-boundary failure controls with optimization enabled.\n..............\n----------------------------------------------------------------------\nRan 14 tests in 0.561s\n\nOK\nPASS_REGISTERED_RESEARCH_PACKAGE research/p112-a6-five-flat outcome=completed\n" + }, + { + "argv": [ + "uv", + "run", + "--python", + "3.13", + "--no-project", + "python", + "-W", + "error", + "-O", + "-B", + "research/p112-a6-five-flat/verify.py" + ], + "exit_code": 0, + "output": "PASS_A6_FIVE_FLAT profile=5,6^8 mixed=142 root=141 allowance=140 errors=0 six_flats=788035 five_flats=3309747 frames=2025 transfer_subsets=64839\n" + }, + { + "argv": [ + "ruff", + "check", + "--no-cache", + "--select", + "E4,E7,E9,F,B,I,UP,C4,SIM", + "research/p112-a6-five-flat/verify.py", + "research/p112-a6-five-flat/cover_transfer.py", + "research/p112-a6-five-flat/test_verify.py" + ], + "exit_code": 0, + "output": "All checks passed!" + }, + { + "check": "Compile every package Python source with warnings as errors; AST function bound on new source", + "exit_code": 0, + "output": "8 Python files compile; every new function has at most30 physical lines." + } + ], + "source_origin_check": { + "retained_files": 10, + "context_pins": 2, + "method": "Each retained local file and context pin compared with exact original commit:path bytes, Git blob ID and SHA256. Local replay authenticates retained bytes without requiring pending PR objects.", + "result": "PASS" + }, + "internal_review": { + "mathematics": "No substantiated correctness gap in affine transfer, quotient normalization, field extension or predecessor contract.", + "artifact": "No substantiated source-binding or replay blocker;14 optimized behavioral groups independently rerun.", + "resolved_findings": [ + "Underlying root-simplex proof retained and pinned; original relative links explained.", + "CHECKS.json now supplies the referenced validation evidence.", + "Exploratory scratch log used manually entered future timestamps. They were explicitly superseded by a parent-observed correction and were not used as chronological evidence. The abandoned independent full census was never run.", + "The first read-only committed export passed the mathematical replay but its mutation test failed because copytree preserved source permissions. The test now grants write permission only to its disposable copy; the complete export replay is rerun before publication." + ], + "attention": "Only maximal5,6^8 is counted as a new profile. Four dominated shapes use the earlier cut theorem; the fifth follows the existing132-versus137/142 bounds. Initial new five-flat census was omitted after a structural transfer reused the existing weighted theorem." + }, + "limits": [ + "Author-checked proof with internal review, not independent human or proof-kernel review.", + "Standard Weyl-chamber theorem, rational-kernel classification and original decoder reduction remain dependencies.", + "No full C5, complete decoder floor, supplier admission or new kappa.", + "Hosted CI is separate from these local checks." + ] +} diff --git a/research/p112-a6-five-flat/ENGINEERING.md b/research/p112-a6-five-flat/ENGINEERING.md new file mode 100644 index 0000000000..5a37385894 --- /dev/null +++ b/research/p112-a6-five-flat/ENGINEERING.md @@ -0,0 +1,74 @@ +# Implementation scope and checks + +The kept change is one isolated opt-in package. It contains a written affine +cover transfer and a source-bound application to one P112 profile. It changes +no shared verifier, canonical input, priority or selected-result record. + +## Engineering decisions + +Build the Lever shaped `cover_transfer.py`: the reviewer can rerun every +four-cube subset and all affine hyperplane controls. Prove It Works shaped the +receipt and source-byte checks: the registered runner executes the actual +retained geometric and weighted statements used by this caller. + +The initial exploratory five-flat census also reached 141, but the structural +cover proof makes that new census unnecessary. Its code and temporary outputs +are omitted. The final result reuses the predecessor's stated rank-four cover +contract through a new rank-five transfer. + +## Power of Ten inspection + +1. New paths have structured branches and finite loops, with no recursion. + I/O failures and failed contracts propagate. Temporary test files use scoped + cleanup. The only subprocess runs an authenticated fixed predecessor. +2. `cover` scans at most sixteen points, fifteen normals and three differences. + Binary elimination uses at most sixteen rows and five bits. The exhaustive + transfer visits exactly 65,536 masks and thirty hyperplanes per mask. + Profile enumeration has four lengths, at most 2,002 weight multisets for + each length, six distance levels and eight basis packings. The predecessor + subprocess has a 120-second timeout. Registered commands have finite bounds. +3. Python allocates during operation. See the managed-runtime deviation below. +4. Each new function has at most thirty physical lines, including comments and + blanks. Frozen predecessor functions retain their original layout. +5. `require` checks support, rank, inventory, source, receipt and coverage + invariants even under `python -O`. The tests exercise invalid values and the + sharp thirteen-point failure boundary. +6. New mutable state is local to the computation. Module values are immutable + paths, tuples, or read-only-by-convention tables. No concurrent writers share + research outputs; fresh receipts require an absent external destination. +7. Files are bounded to two megabytes, ordinary regular files and exact hashes. + Missing data, linked data, source changes, receipt changes and predecessor + failures reject. No proof-relevant subprocess result is ignored. +8. New code uses no dynamic evaluation or generated source. Test framework hooks + and scoped mocks have the standard unittest lifecycle. +9. New data access is shallow. The only dynamic test calls are bounded unittest + dispatch and scoped mocks; production imports name exact retained modules. +10. Verification runs warnings as errors, compilation, applicable Ruff rules, + source/pin checks and behavioral tests. CHECKS.json records actual commands. + Frozen sources are byte-authenticated rather than reformatted by lint. + +## Managed-runtime and frozen-source deviations + +Rule 3, fixed allocation. Python, Fraction, JSON and itertools allocate during +replay. Replacing them would exceed this mathematical package's scope. Inputs +are fixed to eight root coordinates, nine binary bits and at most two megabytes +per file. The largest enumerations stream their masks instead of retaining all +3,309,747 flats. The new transfer keeps only thirty planes and a finite histogram. +The inherited graph has 58 vertices and at most 40,000 traversal states; its +root/frame queues have explicit capacity checks. Registered replay and boundary +controls verify these limits. A native fixed-allocation verifier would require +separate implementation and equivalence review. + +Rules 4/8/9/10, frozen sources and test framework. The retained modules include +unused predecessor application helpers and their original formatting. Their +exact bytes preserve attribution and bind the statements being reused; this +package does not edit them to satisfy local style rules. New code does not call +the unrelated applications. Unittest supplies bounded test dispatch, class hooks +and two scoped path mocks. Ruff is applied to new Python sources; warnings-as- +errors compilation and authenticated replay include the retained sources. A +future shared-library extraction must carry its own equivalence and source- +binding review. No assertion is disabled to pass verification. + +These checks corroborate the finite premises. They are not independent human +review, proof-kernel verification of the Weyl-chamber theorem, or a proof of +full C5 or multiplication. diff --git a/research/p112-a6-five-flat/PROOF.md b/research/p112-a6-five-flat/PROOF.md new file mode 100644 index 0000000000..be24fe5306 --- /dev/null +++ b/research/p112-a6-five-flat/PROOF.md @@ -0,0 +1,191 @@ +# A rank-five cover transfer excludes the P112 profile `5,6^8` + +Let `K` be a characteristic-zero field. Use the pinned 112 nonframe E8 root +lines `r_t` and their nine-bit labels `ell(t)`. Put + +``` +C = {c_h : c_h(t)=, h in K^8}, +w(q) = rank_F2 {ell(t) : q(t) != 0}. +``` + +**Theorem.** Nine independent pieces spanning `T`, with +`dim(T intersect C)>=6`, cannot have weight upper bounds `5,6^8`. + +This is the maximal profile without weight seven in the original TWOSIDE +`(b,t)=(6,3)` cell. The new ingredient is a small affine cover transfer. +It lets the existing weighted A6 theorem of Nick Petalas/PR3186 apply to a +rank-five support. The mixed branch and the geometric classification are +retained from that predecessor. This does not settle the full cell or C5. + +## The new affine cover lemma + +Every set `A` of at most twelve points of affine `F2^4` is contained in an +affine hyperplane together with at most four extra points. + +Choose four distinct points outside `A`. Their affine span has dimension +at most three, so some affine hyperplane `H0` contains all four. Its opposite +half `H1` is another affine hyperplane. Since `H0` has eight points and at +least four are outside `A`, at most four points of `A` lie outside `H1`. +This proves the lemma. The bound four is sharp for any twelve-point `A`, +since a hyperplane has only eight points. A thirteen-point set needs at +least five extras, so the twelve-point hypothesis cannot be increased. + +**Odd-label consequence.** Suppose the labels of an actual support `A` +span at most five binary dimensions and `|A|<=12`. A support of rank at +most four already lies in a four-flat. Otherwise let `V` be its +five-dimensional span. All support labels have leading bit one, so +`Q={x in V : x_0=1}` is an affine four-space. Apply the lemma inside `Q`. +The affine three-space `H1` spans a linear four-space `U`, and its odd part +is exactly `H1`. Therefore + +``` +A subset Lambda(U) union E, dim_F2 U=4, |E|<=4. +``` + +Here `E` consists of actual support coordinates. Missing cube points used +to choose `H0` may be punctured roots or labels that are not roots. Their +absence causes no difficulty. The claim covers only the actual support, +not every root label in its five-dimensional extension. The larger +four-flat may contain extra root coordinates, which is permitted. + +`cover_transfer.py` constructs a half-space from four absent points. It +checks all 64,839 subsets of size at most twelve. A separate finite oracle +tries all thirty affine hyperplanes for each of all 65,536 subsets. It +checks the sharp four-point bound and all 560 thirteen-point failure +controls. Each affine hyperplane's eight odd labels have binary rank four. +These finite checks corroborate the written proof; the proof itself is +independent of the enumeration. + +## Inherited geometric and support premises + +The unchanged [predecessor proof](vendor/PREDECESSOR-PROOF.md) supplies the +following statements with their written arguments and finite inputs: + +- The live Gram sum is `112 I`, so `h -> c_h` is injective. A nonzero codeword + has at least 53 live coordinates. +- A weight-five support has at most twelve live coordinates; weight six + has at most twenty. The replay checks all 3,309,747 five-flats and all + 788,035 six-flats against the canonical puncture. +- Every nonzero direction of live support at most 72 is a scalar multiple + of one of 120 root rays or 128 eligible D7-normal rays. This holds over + every characteristic-zero field by rational-kernel reduction. +- Independent root rays with root-ray differences have a common scale and + form a root simplex. A6 root stars have one Weyl orbit. +- Weyl transformations act invertibly and linearly on the nine-bit label + space and preserve its leading-bit functional. + +The replay checks root reconstruction against the live input, simple-system +positivity, all 960 simple reflections, all 7,140 root planes, the D7-normal +support spectrum and the complete star stabilizer partitions. The standard +Weyl-chamber theorem remains a written mathematical dependency. These tests +do not formalize it or the original decoder reduction. + +## Quotient normalization produces seven endpoints + +Choose the weight-five piece and one weight-six piece, denoting their +support union by `S`. Then `|S|<=12+20=32`. The remaining seven pieces +`q_0,...,q_6` have weight at most six. Write `D=T intersect C`. + +The quotient `T/D` has dimension at most `9-6=3`. The selected two pieces +together with any `q_i` have total support at most `32+20=52<53`. Their +quotient images are independent. Otherwise a nonzero combination of the +independent original pieces would give a nonzero codeword supported on +fewer than 53 coordinates. Thus `dim(T/D)=3` and `dim D=6`. + +Modulo the two selected images, all seven remaining quotient images are +nonzero in a one-dimensional space. Rescale them to have equal images. +Subtract suitable combinations `s_i` of the selected two pieces and set + +``` +c_0=0, c_i=q_i-q_0-s_i in D, i=1,...,6. +``` + +The six codewords are independent by their distinct coefficients on +`q_1,...,q_6`. Injective evaluation gives seven affinely independent +vertices `h_0=0,h_1,...,h_6` in `K^8`. Each nonzero edge has support at most +`32+20+20=72`, so its direction is in the complete root/D7 alphabet. + +At a coordinate outside `S`, the seven endpoint evaluations equal the +seven vertex evaluations after one common shift. Consequently at least + +``` +7 - maximum equality multiplicity +``` + +endpoints are nonzero there. Their total support allowance is `7*20=140`. + +## The two inherited geometric branches + +If an edge has a D7 direction, the pinned predecessor normalizes it to +`a=(1,0,1,0,1,0,1,0)` by a frame-preserving signed permutation and scaling. +All other vertices belong to its exact 58-vertex anchored graph. Among +all 7,350 five-cliques, exactly 3,360 have the required rank six. Removing +the 32 largest coordinate costs leaves at least 142 support incidences +in every such case. The unchanged `vendor/endpoint.py: mixed_six` replays +that census, including its complete rank and support histograms. +Thus this branch exceeds the allowance 140. + +If all edges are root directions, the vertices are one scaled A6 root +simplex. Its full120 minimum-nonzero cost spectrum is + +``` +0:1, 1:21, 2:63, 3:35, total 252. +``` + +Arbitrary removal of forty full-root coordinates leaves only 137. That +relaxation fails to contradict 140 and is retained as a losing control. +A Weyl normalization maps the actual puncture to an orthogonal eight-line +frame `F`, while preserving all binary support ranks. + +PR3186 proves the following weighted cover statement for the A6 cost `c`: +for every such frame, binary six-flat `V`, binary four-flat `U` and at most +four extra root coordinates `E`, + +``` +sum_{r outside F union Lambda(V) union Lambda(U) union E} c(r) >= 141. +``` + +The unchanged `vendor/cover.py: weighted_cover` replays its finite proof. +It covers all 2,025 orthogonal frames and all 788,035 six-flats. The +63 six-flat masks with cost at least 55 give 7,140 relevant frame prefixes. +A potentially violating four-flat must contain at least seven cost-three +labels; all 135 such masks are tested, giving 963,900 residual tests. +The removed cost is at most 111, so at least `252-111=141` remains. +The retained proof explains the threshold pruning and completeness. + +Apply the new odd-label consequence to the actual weight-five support +after Weyl normalization. Its size is still at most twelve, and it lies +inside a four-flat plus four extra coordinates. The other selected support +lies in a six-flat. The inherited weighted cover therefore applies to a +set containing the actual small-support union. At least 141 endpoint +incidences remain outside `S`, exceeding 140. This closes the root branch +and proves the theorem over every characteristic-zero field. + +## Actual residue, overlap and limits + +The original unmodified `vendor/bk2b.py` and a separate transcription +both retain this excess-35 profile among seventeen historical `(6,3)` +survivors. Exactly six have maximum weight at most six, and each is +componentwise bounded by `5,6^8`. This theorem excludes all six original +profiles as a corollary. Four smaller profiles already follow from PR3162 +with at most eight cuts. +The fifth, `5,5,6^7`, permits only 132 endpoint incidences, below both the +inherited mixed bound 142 and arbitrary-cut root bound 137. Six is not a +claim of six newly resolved profiles or a complete current residue count. +The eleven historical profiles containing weight seven are outside this +theorem. + +The earlier root cover accepted rank four plus four arbitrary coordinates. +It did not state the rank-five transfer above or this maximal profile +application. The earlier two-six-flat, ten-cut theorem does not accept the +rank-five support's twelve paid cuts, and the twelve-cut anchor theorem +requires a rank-four nonbasis piece, absent here. These are checks of +named sufficient routes, not a universal novelty claim. The active +fourteen-common-cut question on `2,3,4,6^8` is separate. + +No full C5, `C(P112)>=64`, supplier admission, complete multiplication +theorem or new kappa is proved. The selected frontier remains unchanged. +The source classification, standard Weyl-chamber theorem and original +decoder reduction remain explicit dependencies. This is an author-checked +written proof and finite replay, not independent human or proof-kernel +review. diff --git a/research/p112-a6-five-flat/README.md b/research/p112-a6-five-flat/README.md new file mode 100644 index 0000000000..16e2ad97d6 --- /dev/null +++ b/research/p112-a6-five-flat/README.md @@ -0,0 +1,81 @@ +# A rank-five cover transfer excludes P112 `5,6^8` + +Nine independent P112 pieces with weights bounded by `5,6^8` cannot span a +space whose intersection with the root code has dimension at least six, +over any characteristic-zero field. This is the maximal profile without +weight seven in the original TWOSIDE `(6,3)` residue. + +The new [affine cover lemma](PROOF.md) puts any twelve odd rank-five support +labels inside a rank-four flat plus four coordinates. That connects the +actual profile to Nick Petalas/PR3186's existing weighted A6 bound. Seven +endpoints permit 140 support incidences; the root branch requires 141 and +the mixed branch 142. The old arbitrary-cut relaxation gives only 137. + +The proof is author-checked with exact replay. It does not settle full C5, +the complete P112 decoder floor, supplier admission or kappa. The standard +Weyl-chamber theorem and original decoder reduction remain dependencies. + +## Reproduce + +From the repository root, using Python 3.12 and only the standard library: + +```sh +python3.12 -W error -B scripts/research_package.py --package research/p112-a6-five-flat +``` + +With uv selecting the interpreter: + +```sh +uv run --python 3.12 --no-project python -W error -B scripts/research_package.py \ + --package research/p112-a6-five-flat +``` + +`verify.py` authenticates retained sources and the declared input, reconstructs +the geometry, replays the relevant predecessor bounds, exhausts all 64,839 +admissible four-cube supports and compares the exact receipt in `RESULT.json`. +The thirty-hyperplane oracle also checks all 560 thirteen-point boundary +failures. `test_verify.py` exercises source, input and receipt failures and +separate algebraic controls. `CHECKS.json` records the actual validation. + +For an external fresh receipt, supply an absent path outside the checkout: + +```sh +python3.12 -B research/p112-a6-five-flat/verify.py --output "$RUN_DIR/result.json" +``` + +`RUN_DIR` must be your own external scratch directory. The command refuses +to overwrite a receipt. The registered replay writes no research outputs +inside the checkout. Implementation bounds and deviations are in +[ENGINEERING.md](ENGINEERING.md). + +## Sources and credit + +DreamingOfClouds/PR3154 at `708f0ad8928c383de8294aea3c126e9461d2066d` +supplies TWOSIDE and the C5 handoff. Nick Petalas/PR3186 at +`92675b36a8e0ea41b40f0bcda2a3dd9f313abb0e` supplies the retained weighted +cover and seven-vertex routines, building on PR3176 at +`1111a074414c4d2be8b4e230133d873432780814`. The retained notice preserves +the E8/P112 decoder lineage, including joaqcoo's model. +[SOURCES.json](SOURCES.json) pins exact heads, blobs and SHA256 hashes. Retained proof +links use their original package layout; the underlying root-simplex proof +is also retained at `vendor/ROOT-SIMPLEX-PROOF.md`. The generic runner needs +base history and the live input; vendored source checks do not require pending +PR Git objects. Context-only prior-proof pins record applicability checks. + +The six original rank-at-most-six profiles are consequences of the new +maximal-profile theorem. Some were previously excluded; this package does +not count them as six new results. The original rank-seven residue and +concurrent common-cut question remain separate. + +## Open next questions + +- Which actual weight-seven `(6,3)` profile can use a changed support contract? + First bind its quotient independence and complete edge alphabet. The + present support-72 classification and 140-incidence invoice do not apply + automatically. Full C5 remains the wider blocker. +- Does the affine transfer yield another genuinely new caller? First compare + its exact rank/support hypotheses with existing exclusions. Do not launch + another flat census merely to restate this finite cover theorem. + +[TASK.json](TASK.json) records the changed card scope, handoff and bounded +follow-up questions. [Canonical investigation](https://github.com/CrocSwap/integer-mult-bounds/discussions/3156#discussioncomment-19000918). diff --git a/research/p112-a6-five-flat/RESULT.json b/research/p112-a6-five-flat/RESULT.json new file mode 100644 index 0000000000..1a2c627365 --- /dev/null +++ b/research/p112-a6-five-flat/RESULT.json @@ -0,0 +1,746 @@ +{ + "schema": "p112-a6-five-flat/v1", + "input_sha256": "ac4a48851b922f2a433684b60c74768ae3bb4fc5e8990ffe63e3942bb3c2ea34", + "alphabet": { + "directions": 248, + "anchor_symmetries": 128, + "D7_support_histogram": { + "70": 128, + "73": 896, + "76": 56 + } + }, + "mixed": { + "ranks": { + "4": 630, + "5": 3360, + "6": 3360 + }, + "bounds": { + "142": 1344, + "145": 336, + "146": 336, + "147": 112, + "148": 448, + "149": 560, + "150": 224 + }, + "witness": { + "lower": 142, + "indices": [ + 53, + 54, + 55, + 56, + 57 + ], + "spectrum": { + "0": 2, + "1": 26, + "2": 40, + "3": 26, + "4": 18 + } + } + }, + "all_root": { + "steps": [ + { + "rank": 0, + "orbit_sizes": [ + 240 + ] + }, + { + "rank": 1, + "orbit_sizes": [ + 56 + ] + }, + { + "rank": 2, + "orbit_sizes": [ + 27 + ] + }, + { + "rank": 3, + "orbit_sizes": [ + 16 + ] + }, + { + "rank": 4, + "orbit_sizes": [ + 10 + ] + }, + { + "rank": 5, + "orbit_sizes": [ + 6 + ] + } + ], + "spectrum": { + "0": 1, + "1": 21, + "2": 63, + "3": 35 + }, + "losing_after_40_cuts": 137, + "representative": [ + [ + -2, + -2, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + -2, + 0, + -2, + 0, + 0, + 0, + 0, + 0 + ], + [ + -2, + 0, + 0, + -2, + 0, + 0, + 0, + 0 + ], + [ + -2, + 0, + 0, + 0, + -2, + 0, + 0, + 0 + ], + [ + -2, + 0, + 0, + 0, + 0, + -2, + 0, + 0 + ], + [ + -2, + 0, + 0, + 0, + 0, + 0, + -2, + 0 + ] + ] + }, + "weighted": { + "six_flat_histogram": { + "0": 10795, + "12": 525, + "14": 378, + "15": 1050, + "16": 3780, + "17": 1890, + "18": 4578, + "19": 630, + "20": 1890, + "21": 12000, + "22": 19593, + "23": 27195, + "24": 32060, + "25": 28665, + "26": 57561, + "27": 58884, + "28": 22050, + "29": 13650, + "30": 26845, + "31": 15288, + "32": 72870, + "33": 98245, + "34": 34125, + "35": 44163, + "36": 75075, + "37": 23499, + "38": 12495, + "39": 12740, + "40": 5523, + "41": 11088, + "42": 27405, + "43": 14490, + "44": 3150, + "45": 4753, + "46": 4305, + "47": 2205, + "48": 350, + "49": 735, + "50": 819, + "51": 315, + "52": 315, + "57": 35, + "60": 28 + }, + "selected_six_flats": 63, + "high_four_flats": 135, + "mask_sha256": "30448edfd932d91f3c56b3590ee73b39db59ec85ce3a044a648b04f80374ff95", + "label_reflection_checks": 960, + "cover": { + "frame_costs": { + "14": 210, + "16": 735, + "17": 630, + "19": 420, + "21": 30 + }, + "prefix_costs": { + "76": 4620, + "77": 2520 + }, + "maximum_prefix": 77, + "four_flat_tests": 963900, + "residual_maxima": [ + [ + 76, + 12, + 4620 + ], + [ + 77, + 12, + 2520 + ] + ], + "removed_upper": 111, + "surviving_lower": 141, + "losing_arbitrary12_lower": 139, + "losing_witness": { + "frame": [ + 19, + 27, + 36, + 52, + 62, + 80, + 98, + 114 + ], + "six_mask": 156589743630174343786926178304 + } + } + }, + "chamber": { + "simple_reflection_checks": 960, + "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 + } + }, + "root_planes": { + "2": 3780, + "3": 3360 + }, + "flat_capacities": [ + { + "dimension": 5, + "subspaces": 3309747, + "maximum": 12, + "histogram": { + "0": 99593, + "2": 6720, + "3": 71680, + "4": 300076, + "5": 258048, + "6": 729344, + "7": 442368, + "8": 826770, + "9": 200704, + "10": 287168, + "11": 43008, + "12": 44268 + } + }, + { + "dimension": 6, + "subspaces": 788035, + "maximum": 20, + "histogram": { + "0": 10796, + "4": 56, + "6": 896, + "7": 4096, + "8": 8148, + "10": 56448, + "11": 86016, + "12": 124040, + "14": 131712, + "15": 143360, + "16": 141491, + "18": 33152, + "19": 28672, + "20": 19152 + } + } + ], + "cover_transfer": { + "all_subsets": 65536, + "admissible_subsets": 64839, + "errors": 0, + "hyperplanes": 30, + "maximum_extra": 4, + "histogram": [ + [ + 0, + 0, + 1 + ], + [ + 1, + 0, + 16 + ], + [ + 2, + 0, + 120 + ], + [ + 3, + 0, + 560 + ], + [ + 4, + 0, + 1820 + ], + [ + 5, + 0, + 1680 + ], + [ + 5, + 1, + 2688 + ], + [ + 6, + 0, + 840 + ], + [ + 6, + 1, + 6720 + ], + [ + 6, + 2, + 448 + ], + [ + 7, + 0, + 240 + ], + [ + 7, + 1, + 6720 + ], + [ + 7, + 2, + 4480 + ], + [ + 8, + 0, + 30 + ], + [ + 8, + 1, + 1920 + ], + [ + 8, + 2, + 10920 + ], + [ + 9, + 1, + 240 + ], + [ + 9, + 2, + 6720 + ], + [ + 9, + 3, + 4480 + ], + [ + 10, + 2, + 840 + ], + [ + 10, + 3, + 6720 + ], + [ + 10, + 4, + 448 + ], + [ + 11, + 3, + 1680 + ], + [ + 11, + 4, + 2688 + ], + [ + 12, + 4, + 1820 + ], + [ + 13, + 5, + 560 + ], + [ + 14, + 6, + 120 + ], + [ + 15, + 7, + 16 + ], + [ + 16, + 8, + 1 + ] + ], + "sharp_witness": { + "support": 4095, + "half": 3855, + "extra": 240, + "minimum_extra": 4 + }, + "thirteen_point_controls": 560 + }, + "application": { + "cell": [ + 6, + 3 + ], + "weights": [ + 5, + 6, + 6, + 6, + 6, + 6, + 6, + 6, + 6 + ], + "small_weights": [ + 5, + 6 + ], + "small_support_cap": 32, + "quotient_basis_cap": 52, + "edge_support_cap": 72, + "endpoint_allowance": 140, + "mixed_lower": 142, + "root_lower": 141, + "original_survivors": 17, + "original_no_seven_profiles": [ + [ + 2, + 6, + 6, + 6, + 6, + 6, + 6, + 6, + 6 + ], + [ + 3, + 6, + 6, + 6, + 6, + 6, + 6, + 6, + 6 + ], + [ + 4, + 5, + 6, + 6, + 6, + 6, + 6, + 6, + 6 + ], + [ + 4, + 6, + 6, + 6, + 6, + 6, + 6, + 6, + 6 + ], + [ + 5, + 5, + 6, + 6, + 6, + 6, + 6, + 6, + 6 + ], + [ + 5, + 6, + 6, + 6, + 6, + 6, + 6, + 6, + 6 + ] + ], + "scope": "One maximal profile; six original no-seven profiles dominated. Earlier exclusions may already cover some dominated profiles." + }, + "original_table": [ + [ + 5, + 1, + 0, + 0 + ], + [ + 5, + 2, + 0, + 0 + ], + [ + 5, + 3, + 4, + 1 + ], + [ + 5, + 4, + 15, + 1 + ], + [ + 5, + 5, + 38, + 1 + ], + [ + 5, + 6, + 77, + 1 + ], + [ + 6, + 1, + 0, + 0 + ], + [ + 6, + 2, + 1, + 1 + ], + [ + 6, + 3, + 17, + 1 + ], + [ + 6, + 4, + 69, + 1 + ], + [ + 6, + 5, + 174, + 1 + ], + [ + 6, + 6, + 364, + 1 + ], + [ + 7, + 1, + 0, + 0 + ], + [ + 7, + 2, + 2, + 1 + ], + [ + 7, + 3, + 37, + 1 + ], + [ + 7, + 4, + 154, + 1 + ], + [ + 7, + 5, + 403, + 1 + ], + [ + 7, + 6, + 885, + 1 + ], + [ + 8, + 1, + 0, + 0 + ], + [ + 8, + 2, + 3, + 1 + ], + [ + 8, + 3, + 60, + 1 + ], + [ + 8, + 4, + 251, + 1 + ], + [ + 8, + 5, + 684, + 1 + ], + [ + 8, + 6, + 1556, + 1 + ] + ] +} diff --git a/research/p112-a6-five-flat/SOURCES.json b/research/p112-a6-five-flat/SOURCES.json new file mode 100644 index 0000000000..37d37e5a2b --- /dev/null +++ b/research/p112-a6-five-flat/SOURCES.json @@ -0,0 +1,113 @@ +{ + "schema_version": 1, + "base_commit": "997e6a9ca7b4f95d50e366f61412fd640d72a88a", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81", + "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "67f085acd86acd7d4e03922d9cf4b26bca66fed5", + "sha256": "47b42433f5a85809a3aadd29c2c339da2c6ed728e4f7762df6b88bccb7874cf0" + }, + { + "path": "research/one-sided-six-multisets/data/data.txt", + "usage": "input", + "git_blob": "dc591a4e0252bac096e6c63c51058f6caee66bfe", + "sha256": "ac4a48851b922f2a433684b60c74768ae3bb4fc5e8990ffe63e3942bb3c2ea34" + } + ], + "retained_files": [ + { + "local_path": "vendor/geometry.py", + "path": "research/p112-a6-weighted-cover/vendor/geometry.py", + "pin": "head:92675b36a8e0ea41b40f0bcda2a3dd9f313abb0e:research/p112-a6-weighted-cover/vendor/geometry.py", + "git_blob": "222ea556faf2b275f73815c4e7d0d5f1e3294f2f", + "sha256": "b8ac379e41f5ad83bdb6c7f7c55129fc3d9c07801ea61591478f25d72ff0b021" + }, + { + "local_path": "vendor/mixed.py", + "path": "research/p112-a6-weighted-cover/vendor/mixed.py", + "pin": "head:92675b36a8e0ea41b40f0bcda2a3dd9f313abb0e:research/p112-a6-weighted-cover/vendor/mixed.py", + "git_blob": "e79086db5cdd77aaa28602e649cf1ed21b34d759", + "sha256": "7edd4f7fee0db1b4d38e0b8d9fbd71448950045add9773dc8db4084d6550f11e" + }, + { + "local_path": "vendor/cover.py", + "path": "research/p112-a6-weighted-cover/weighted.py", + "pin": "head:92675b36a8e0ea41b40f0bcda2a3dd9f313abb0e:research/p112-a6-weighted-cover/weighted.py", + "git_blob": "de5ab021ec2d90cec5ae61c0ff0662c519c32e2e", + "sha256": "6ba9b8e06708835ad91eabefb46de83df0c8bf117e2218a60bd2785ca30ea132" + }, + { + "local_path": "vendor/endpoint.py", + "path": "research/p112-a6-weighted-cover/bound.py", + "pin": "head:92675b36a8e0ea41b40f0bcda2a3dd9f313abb0e:research/p112-a6-weighted-cover/bound.py", + "git_blob": "14b05de535be5044b3d7938abccefad7ac938fce", + "sha256": "ec6324523c8d00022707df1d48c8996cdef213ca2036c370d795c179b37e6419" + }, + { + "local_path": "vendor/PREDECESSOR-PROOF.md", + "path": "research/p112-a6-weighted-cover/PROOF.md", + "pin": "head:92675b36a8e0ea41b40f0bcda2a3dd9f313abb0e:research/p112-a6-weighted-cover/PROOF.md", + "git_blob": "8a129bc0179e142c5b557ca0766bed780eca4785", + "sha256": "8c25ddf5430682f2a97520cae9ee070c711bf70c393a36471bf200fbe6300ff4" + }, + { + "local_path": "vendor/PREDECESSOR-NOTICE.md", + "path": "research/p112-a6-weighted-cover/vendor/PREDECESSOR-NOTICE.md", + "pin": "head:92675b36a8e0ea41b40f0bcda2a3dd9f313abb0e:research/p112-a6-weighted-cover/vendor/PREDECESSOR-NOTICE.md", + "git_blob": "c6f3494c2c746242020ed1b7959bc48988239d6d", + "sha256": "1ea58e398f40239c0945d495a807b33bcadeb6d5dcd147a12bf71ff06a9ed7ec" + }, + { + "local_path": "vendor/LICENSE", + "path": "research/p112-a6-weighted-cover/vendor/LICENSE", + "pin": "head:92675b36a8e0ea41b40f0bcda2a3dd9f313abb0e:research/p112-a6-weighted-cover/vendor/LICENSE", + "git_blob": "261eeb9e9f8b2b4b0d119366dda99c6fd7d35c64", + "sha256": "c71d239df91726fc519c6eb72d318ec65820627232b2f796219e87dcf35d0ab4" + }, + { + "local_path": "vendor/bk2b.py", + "path": "research/p112-a6-weighted-cover/vendor/bk2b.py", + "pin": "head:92675b36a8e0ea41b40f0bcda2a3dd9f313abb0e:research/p112-a6-weighted-cover/vendor/bk2b.py", + "git_blob": "3394029014bb13f16225587a153fa7b70016de6d", + "sha256": "dff16eff255c883db372a587cf3f34e6f35c08f75c60af9d11952be5a5838807" + }, + { + "local_path": "vendor/TWOSIDE-NOTES.md", + "path": "research/p112-a6-weighted-cover/vendor/TWOSIDE-NOTES.md", + "pin": "head:92675b36a8e0ea41b40f0bcda2a3dd9f313abb0e:research/p112-a6-weighted-cover/vendor/TWOSIDE-NOTES.md", + "git_blob": "e3fd3f2b1dfd77b597f000b38ec2dbec3dbca931", + "sha256": "226cd59ccc6bc065319e5e4c4768c889206169ff58f74ef4053eeadc5b2e03c8" + }, + { + "local_path": "vendor/ROOT-SIMPLEX-PROOF.md", + "path": "research/p112-a6-weighted-cover/vendor/ROOT-SIMPLEX-PROOF.md", + "pin": "head:92675b36a8e0ea41b40f0bcda2a3dd9f313abb0e:research/p112-a6-weighted-cover/vendor/ROOT-SIMPLEX-PROOF.md", + "git_blob": "ccae08212784114e732da1192b336e47fc6a2091", + "sha256": "2b5d70570e3a13d2ccc71c1fc7eef113f0d049993cb9bb24007166223ac7b734" + } + ], + "attribution": "DreamingOfClouds/PR3154 for TWOSIDE; Nick Petalas/PR3176 and PR3186 for retained geometry, classification, mixed seven-vertex bound and weighted six-flat/frame routines; original notices retain the E8/P112 lineage including joaqcoo.", + "context_pins": [ + { + "path": "research/p112-ten-deletion-span/PROOF.md", + "usage": "provenance", + "pin": "head:ebd7fd275288e4a9f658e77fa77a0119a8322e74:research/p112-ten-deletion-span/PROOF.md", + "git_blob": "fb45b45d0ced71d3c9ed0b6523f8edaef28ded35", + "sha256": "6978f53d37a8e262bd9a443425441922c13508e19cb564e37f369f690ef4bfe8" + }, + { + "path": "research/p112-mixed-rank-anchor/PROOF.md", + "usage": "provenance", + "pin": "head:c2c7508f2d731feea550f1628601aebd35c6e147:research/p112-mixed-rank-anchor/PROOF.md", + "git_blob": "230c852f7e2033d50e3c1133c32cc1cf6efaaedb", + "sha256": "53bcf6a09b9a4119c1270c2a2d5d3339d97e3e3727e53917cb6a0684d49673f4" + } + ] +} diff --git a/research/p112-a6-five-flat/TASK.json b/research/p112-a6-five-flat/TASK.json new file mode 100644 index 0000000000..44ed4f92bd --- /dev/null +++ b/research/p112-a6-five-flat/TASK.json @@ -0,0 +1,91 @@ +{ + "schema_version": 1, + "task_id": "formal-interface-lemma", + "priority_revision": 6, + "base_commit": "997e6a9ca7b4f95d50e366f61412fd640d72a88a", + "original_card": { + "id": "formal-interface-lemma", + "question": "Can one small, precisely scoped interface lemma be formalized with its actual hypotheses?", + "starting_points": [ + "certificates/selected-result.json", + "research/hyperplane-end-lean/PROOF.md" + ], + "methods": [ + "Formalize a missing boundary lemma identified by the selected review.", + "Audit a formal theorem-to-certificate binding independently." + ], + "acceptance_gate": "State the exact formalized proposition and remaining assumptions; avoid duplicate arithmetic formalizations already present.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read the exact hypotheses in the hyperplane-end proof and distinguish Lean theorems from finite supplier assumptions.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "State one missing boundary lemma in full before starting a proof-assistant build.", + "bottleneck_link": "A missing interface proof can reduce the conditional gap even if it does not change kappa.", + "allowed_variations": [ + "Narrow to one formal lemma or one theorem-to-certificate binding." + ], + "scope_change_triggers": [ + "Formalizing already-covered arithmetic and claiming the full multiplication theorem." + ], + "overlap_terms": [ + "hyperplane end", + "formal interface", + "Lean binding" + ] + }, + "scope_status": "changed", + "actual_scope": "Prove an affine-four-cube cover transfer and exclude the actual nine-piece P112 TWOSIDE (6,3) profile 5,6^8 over characteristic-zero fields.", + "scope_change_reason": "Take the live C5 handoff through a written interface lemma and source-bound exact replay, rather than another Lean arithmetic formalization. The original profile and quotient contract are checked before extending the predecessor.", + "bottleneck_link": "A new maximal-profile exclusion closes one part of the P112 decoder-floor reduction; no supplier admission or kappa gain follows.", + "budget_minutes": 60, + "stop_rule": "One scoped profile exclusion or a checked failed premise within a roughly 60-minute session; no larger mechanism expansion.", + "outcome": "completed", + "evidence": "PROOF.md; RESULT.json; CHECKS.json; test_verify.py; exact retained source pins in SOURCES.json.", + "author": "Nick Petalas", + "ai_assistance": "Automated drafting and exact finite checks; no independent human review is claimed.", + "open_questions": [ + { + "question": "Which actual weight-seven (6,3) profile admits a useful changed support contract?", + "why_it_matters": "The original eleven profiles containing seven are outside the theorem and full C5 remains unresolved.", + "first_step": "Pin one actual profile and derive its quotient-independence and full edge-alphabet hypotheses before another census.", + "blocked_by": "Support-72 classification and the seven rank-six endpoint invoice do not automatically apply." + }, + { + "question": "Does the affine rank5 transfer have a genuinely new additional caller?", + "why_it_matters": "The small structural lemma may reuse an established weighted theorem without a new flat enumeration.", + "first_step": "Compare one explicit caller against existing support/rank and anchor exclusions.", + "blocked_by": "No additional caller is validated or assigned in this package." + } + ], + "upstream_checkpoint": { + "commit": "997e6a9ca7b4f95d50e366f61412fd640d72a88a", + "priority_revision": 6, + "checked_at": "2026-10-17T16:23:07.108608+00:00", + "overlap": { + "open_prs": { + "fetched_at": "2026-10-17T16:22:12.740556+00:00", + "complete_pagination": true, + "records": 310 + }, + "discussions": { + "fetched_at": "2026-10-17T16:22:41.643630+00:00", + "complete_pagination": true, + "records": 1976 + } + }, + "exact_scope_matches": [ + { + "url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/3156#discussioncomment-19000918", + "title": "C(P112) >= 64: what is left (for the swarm)", + "head": null + } + ], + "warnings": [] + } +} diff --git a/research/p112-a6-five-flat/VERIFY.json b/research/p112-a6-five-flat/VERIFY.json new file mode 100644 index 0000000000..cfb8b836be --- /dev/null +++ b/research/p112-a6-five-flat/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/one-sided-six-multisets/data/data.txt" + ], + "commands": [ + { + "argv": [ + "{python}", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 180, + "checks": "Authenticates all retained source bytes; replays both endpoint branches, flat capacities, the weighted predecessor and all 64839 affine transfer subsets; exact receipt comparison." + }, + { + "argv": [ + "{python}", + "-W", + "error", + "-O", + "-B", + "{package}/test_verify.py" + ], + "timeout_seconds": 60, + "checks": "Fourteen behavioral groups including source, input, receipt, embedding and strict-boundary failure controls with optimization enabled." + } + ] +} diff --git a/research/p112-a6-five-flat/cover_transfer.py b/research/p112-a6-five-flat/cover_transfer.py new file mode 100644 index 0000000000..293f64b538 --- /dev/null +++ b/research/p112-a6-five-flat/cover_transfer.py @@ -0,0 +1,87 @@ +"""Construct and exhaustively check the affine four-cube cover transfer.""" + +from collections import Counter + +from vendor.geometry import require + +ALL = (1 << 16) - 1 + + +def cover(mask): + """Return an affine hyperplane mask and at most four uncovered points.""" + require(type(mask) is int and 0 <= mask <= ALL, "four-cube support mask") + require(mask.bit_count() <= 12, "support exceeds twelve points") + absent = tuple(x for x in range(16) if not (mask >> x & 1))[:4] + require(len(absent) == 4, "four absent points required") + differences = tuple(x ^ absent[0] for x in absent[1:]) + normal = next(n for n in range(1, 16) + if all((n & x).bit_count() % 2 == 0 for x in differences)) + value = (normal & absent[0]).bit_count() % 2 + half = sum(1 << x for x in range(16) if (normal & x).bit_count() % 2 != value) + extra = mask & ~half + require(half.bit_count() == 8 and extra.bit_count() <= 4, "affine cover invariant") + return half, extra + + +def binary_rank(rows): + require(len(rows) <= 16 and all(type(x) is int and 0 <= x < 32 for x in rows), + "five-bit rank domain") + basis = [0] * 5 + for row in rows: + for bit in range(4, -1, -1): + if not row >> bit & 1: + continue + if basis[bit]: + row ^= basis[bit] + else: + basis[bit] = row + break + return sum(x != 0 for x in basis) + + +def hyperplanes(): + masks = tuple(sum(1 << x for x in range(16) + if (normal & x).bit_count() % 2 == value) + for normal in range(1, 16) for value in (0, 1)) + require(len(masks) == len(set(masks)) == 30, "affine hyperplane inventory") + for half in masks: + labels = tuple(1 | (x << 1) for x in range(16) if half >> x & 1) + require(half.bit_count() == 8 and binary_rank(labels) == 4, + "odd affine hyperplane has linear rank four") + return masks + + +def exhaustive_transfer(): + """Check all 2^16 supports against the independent 30-hyperplane oracle.""" + planes = hyperplanes() + histogram = Counter() + admissible, failures, maximum = 0, 0, 0 + sharp = None + for mask in range(1 << 16): + size = mask.bit_count() + minimum = min((mask & ~half).bit_count() for half in planes) + histogram[size, minimum] += 1 + if size > 12: + require(minimum > 4, "cardinality boundary must fail") + continue + admissible += 1 + half, extra = cover(mask) + valid = half in planes and mask == (mask & half) | extra + valid = valid and extra.bit_count() <= 4 and not extra & half + failures += not valid + maximum = max(maximum, extra.bit_count()) + if minimum == 4 and sharp is None: + sharp = {"support": mask, "half": half, "extra": extra, + "minimum_extra": minimum} + require(admissible == 64839 and failures == 0 and maximum == 4, + "complete affine transfer coverage") + require(sharp is not None and histogram[13, 5] == 560, "sharp boundary controls") + return {"all_subsets": 65536, "admissible_subsets": admissible, + "errors": failures, "hyperplanes": len(planes), "maximum_extra": maximum, + "histogram": [[s, k, n] for (s, k), n in sorted(histogram.items())], + "sharp_witness": sharp, "thirteen_point_controls": 560} + + +if __name__ == "__main__": + result = exhaustive_transfer() + print("PASS_AFFINE_COVER_TRANSFER subsets=64839 boundary_controls=560 errors=0") diff --git a/research/p112-a6-five-flat/test_verify.py b/research/p112-a6-five-flat/test_verify.py new file mode 100644 index 0000000000..a12da11ead --- /dev/null +++ b/research/p112-a6-five-flat/test_verify.py @@ -0,0 +1,145 @@ +"""Behavioral controls for the affine transfer and its source bindings.""" + +import copy +import json +import shutil +import tempfile +import unittest +from itertools import combinations +from pathlib import Path +from unittest.mock import patch + +import cover_transfer as transfer +import verify +from vendor.geometry import root_data + + +class TransferTests(unittest.TestCase): + def test_all_subsets_and_boundary(self): + result = transfer.exhaustive_transfer() + self.assertEqual(result["admissible_subsets"], 64839) + self.assertEqual(result["errors"], 0) + self.assertEqual(result["thirteen_point_controls"], 560) + + def test_twelve_points_need_four_extras(self): + mask = (1 << 12) - 1 + half, extra = transfer.cover(mask) + self.assertEqual(extra.bit_count(), 4) + self.assertEqual(mask & ~(half | extra), 0) + self.assertEqual(min((mask & ~h).bit_count() for h in transfer.hyperplanes()), 4) + + def test_empty_and_singleton(self): + for mask in (0, 1, 1 << 15): + half, extra = transfer.cover(mask) + self.assertEqual(mask & ~(half | extra), 0) + self.assertLessEqual(extra.bit_count(), 1) + + def test_invalid_supports_reject(self): + for mask in (-1, 1 << 16, True, 1.0, (1 << 13) - 1): + with self.subTest(mask=mask), self.assertRaises(ValueError): + transfer.cover(mask) + + def test_binary_rank_domain(self): + self.assertEqual(transfer.binary_rank((1, 2, 4, 8, 16)), 5) + self.assertEqual(transfer.binary_rank((1, 2, 3)), 2) + for rows in ((-1,), (32,), (True,), (0,) * 17): + with self.subTest(rows=rows), self.assertRaises(ValueError): + transfer.binary_rank(rows) + + def test_noncoordinate_embedding(self): + # An injective affine map of the four-cube into the nine-bit odd half. + origin, directions = 33, (258, 68, 136, 48) + for half in transfer.hyperplanes(): + labels = [] + for x in range(16): + if half >> x & 1: + label = origin + for i in range(4): + if x >> i & 1: + label ^= directions[i] + labels.append(label) + basis = {} + for label in labels: + for bit in range(8, -1, -1): + if label >> bit & 1: + if bit in basis: + label ^= basis[bit] + else: + basis[bit] = label + break + self.assertEqual(len(basis), 4) + self.assertTrue(all(label & 1 for label in labels)) + + def test_hyperplane_oracle_uses_all_normals(self): + planes = transfer.hyperplanes() + self.assertEqual(set(planes), {transfer.ALL ^ h for h in planes}) + self.assertEqual(len(planes), 30) + self.assertTrue(all(h.bit_count() == 8 for h in planes)) + + +class BindingTests(unittest.TestCase): + @classmethod + def setUpClass(cls): + cls.roots, cls.points, cls.labels, _ = root_data() + cls.sources = verify.bind_sources() + + def test_actual_pins(self): + self.assertEqual(len(self.sources["retained_files"]), 10) + self.assertEqual(verify.bind_data(verify.ROOT / verify.DATA, self.points, + self.labels, self.sources), + self.sources["files"][2]["sha256"]) + + def test_changed_source_rejects(self): + with tempfile.TemporaryDirectory(prefix="source-mutant-") as name: + package = Path(name) / "package" + shutil.copytree(verify.PACKAGE / "vendor", package / "vendor") + shutil.copyfile(verify.PACKAGE / "SOURCES.json", package / "SOURCES.json") + source = package / "vendor/geometry.py" + source.chmod(0o600) # Only this disposable copy must be mutable. + source.write_bytes(source.read_bytes() + b"\n# mutant\n") + with patch.object(verify, "PACKAGE", package), self.assertRaises(ValueError): + verify.bind_sources() + + def test_changed_input_rejects(self): + with tempfile.TemporaryDirectory(prefix="input-mutant-") as name: + source = Path(name) / "data.txt" + source.write_bytes((verify.ROOT / verify.DATA).read_bytes() + b"mutant") + with self.assertRaises(ValueError): + verify.bind_data(source, self.points, self.labels, self.sources) + + def test_missing_and_linked_inputs_reject(self): + with tempfile.TemporaryDirectory(prefix="missing-input-") as name: + source = Path(name) / "input" + with self.assertRaises(ValueError): + verify.read_bytes(source) + source.symlink_to(verify.PACKAGE / "RESULT.json") + with self.assertRaises(ValueError): + verify.read_bytes(source) + + def test_receipt_change_rejects(self): + result = json.loads(verify.read_bytes(verify.PACKAGE / "RESULT.json")) + verify.check_receipt(result, copy.deepcopy(result)) + mutant = copy.deepcopy(result) + mutant["cover_transfer"]["maximum_extra"] = 3 + with self.assertRaises(ValueError): + verify.check_receipt(result, mutant) + + def test_actual_profile_and_predecessor_cell(self): + actual = verify.application() + self.assertEqual(actual["weights"], (5,) + (6,) * 8) + self.assertEqual(actual["quotient_basis_cap"], 52) + self.assertEqual(actual["endpoint_allowance"], 140) + self.assertEqual(len(actual["original_no_seven_profiles"]), 6) + self.assertEqual(verify.predecessor_table()[8][2], 17) + + def test_only_rank_five_rank_six_quotient_basis(self): + choices = set(combinations(verify.PROFILE, 3)) + certified = [row for row in choices if sum(verify.CAP[w] for w in row) < 53] + self.assertEqual(certified, [(5, 6, 6)]) + # Both whole six-flats leave the five-piece's twelve-coordinate cap. + self.assertEqual(verify.CAP[5], 12) + self.assertGreater(verify.CAP[5], 10) + + +if __name__ == "__main__": + unittest.main() diff --git a/research/p112-a6-five-flat/vendor/LICENSE b/research/p112-a6-five-flat/vendor/LICENSE new file mode 100644 index 0000000000..261eeb9e9f --- /dev/null +++ b/research/p112-a6-five-flat/vendor/LICENSE @@ -0,0 +1,201 @@ + Apache License + Version 2.0, January 2004 + http://www.apache.org/licenses/ + + TERMS AND CONDITIONS FOR USE, REPRODUCTION, AND DISTRIBUTION + + 1. Definitions. + + "License" shall mean the terms and conditions for use, reproduction, + and distribution as defined by Sections 1 through 9 of this document. + + "Licensor" shall mean the copyright owner or entity authorized by + the copyright owner that is granting the License. + + "Legal Entity" shall mean the union of the acting entity and all + other entities that control, are controlled by, or are under common + control with that entity. For the purposes of this definition, + "control" means (i) the power, direct or indirect, to cause the + direction or management of such entity, whether by contract or + otherwise, or (ii) ownership of fifty percent (50%) or more of the + outstanding shares, or (iii) beneficial ownership of such entity. + + "You" (or "Your") shall mean an individual or Legal Entity + exercising permissions granted by this License. + + "Source" form shall mean the preferred form for making modifications, + including but not limited to software source code, documentation + source, and configuration files. + + "Object" form shall mean any form resulting from mechanical + transformation or translation of a Source form, including but + not limited to compiled object code, generated documentation, + and conversions to other media types. + + "Work" shall mean the work of authorship, whether in Source or + Object form, made available under the License, as indicated by a + copyright notice that is included in or attached to the work + (an example is provided in the Appendix below). + + "Derivative Works" shall mean any work, whether in Source or Object + form, that is based on (or derived from) the Work and for which the + editorial revisions, annotations, elaborations, or other modifications + represent, as a whole, an original work of authorship. For the purposes + of this License, Derivative Works shall not include works that remain + separable from, or merely link (or bind by name) to the interfaces of, + the Work and Derivative Works thereof. + + "Contribution" shall mean any work of authorship, including + the original version of the Work and any modifications or additions + to that Work or Derivative Works thereof, that is intentionally + submitted to Licensor for inclusion in the Work by the copyright owner + or by an individual or Legal Entity authorized to submit on behalf of + the copyright owner. For the purposes of this definition, "submitted" + means any form of electronic, verbal, or written communication sent + to the Licensor or its representatives, including but not limited to + communication on electronic mailing lists, source code control systems, + and issue tracking systems that are managed by, or on behalf of, the + Licensor for the purpose of discussing and improving the Work, but + excluding communication that is conspicuously marked or otherwise + designated in writing by the copyright owner as "Not a Contribution." + + "Contributor" shall mean Licensor and any individual or Legal Entity + on behalf of whom a Contribution has been received by Licensor and + subsequently incorporated within the Work. + + 2. Grant of Copyright License. Subject to the terms and conditions of + this License, each Contributor hereby grants to You a perpetual, + worldwide, non-exclusive, no-charge, royalty-free, irrevocable + copyright license to reproduce, prepare Derivative Works of, + publicly display, publicly perform, sublicense, and distribute the + Work and such Derivative Works in Source or Object form. + + 3. Grant of Patent License. Subject to the terms and conditions of + this License, each Contributor hereby grants to You a perpetual, + worldwide, non-exclusive, no-charge, royalty-free, irrevocable + (except as stated in this section) patent license to make, have made, + use, offer to sell, sell, import, and otherwise transfer the Work, + where such license applies only to those patent claims licensable + by such Contributor that are necessarily infringed by their + Contribution(s) alone or by combination of their Contribution(s) + with the Work to which such Contribution(s) was submitted. If You + institute patent litigation against any entity (including a + cross-claim or counterclaim in a lawsuit) alleging that the Work + or a Contribution incorporated within the Work constitutes direct + or contributory patent infringement, then any patent licenses + granted to You under this License for that Work shall terminate + as of the date such litigation is filed. + + 4. Redistribution. You may reproduce and distribute copies of the + Work or Derivative Works thereof in any medium, with or without + modifications, and in Source or Object form, provided that You + meet the following conditions: + + (a) You must give any other recipients of the Work or + Derivative Works a copy of this License; and + + (b) You must cause any modified files to carry prominent notices + stating that You changed the files; and + + (c) You must retain, in the Source form of any Derivative Works + that You distribute, all copyright, patent, trademark, and + attribution notices from the Source form of the Work, + excluding those notices that do not pertain to any part of + the Derivative Works; and + + (d) If the Work includes a "NOTICE" text file as part of its + distribution, then any Derivative Works that You distribute must + include a readable copy of the attribution notices contained + within such NOTICE file, excluding those notices that do not + pertain to any part of the Derivative Works, in at least one + of the following places: within a NOTICE text file distributed + as part of the Derivative Works; within the Source form or + documentation, if provided along with the Derivative Works; or, + within a display generated by the Derivative Works, if and + wherever such third-party notices normally appear. The contents + of the NOTICE file are for informational purposes only and + do not modify the License. You may add Your own attribution + notices within Derivative Works that You distribute, alongside + or as an addendum to the NOTICE text from the Work, provided + that such additional attribution notices cannot be construed + as modifying the License. + + You may add Your own copyright statement to Your modifications and + may provide additional or different license terms and conditions + for use, reproduction, or distribution of Your modifications, or + for any such Derivative Works as a whole, provided Your use, + reproduction, and distribution of the Work otherwise complies with + the conditions stated in this License. + + 5. Submission of Contributions. Unless You explicitly state otherwise, + any Contribution intentionally submitted for inclusion in the Work + by You to the Licensor shall be under the terms and conditions of + this License, without any additional terms or conditions. + Notwithstanding the above, nothing herein shall supersede or modify + the terms of any separate license agreement you may have executed + with Licensor regarding such Contributions. + + 6. Trademarks. This License does not grant permission to use the trade + names, trademarks, service marks, or product names of the Licensor, + except as required for reasonable and customary use in describing the + origin of the Work and reproducing the content of the NOTICE file. + + 7. Disclaimer of Warranty. Unless required by applicable law or + agreed to in writing, Licensor provides the Work (and each + Contributor provides its Contributions) on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or + implied, including, without limitation, any warranties or conditions + of TITLE, NON-INFRINGEMENT, MERCHANTABILITY, or FITNESS FOR A + PARTICULAR PURPOSE. You are solely responsible for determining the + appropriateness of using or redistributing the Work and assume any + risks associated with Your exercise of permissions under this License. + + 8. Limitation of Liability. In no event and under no legal theory, + whether in tort (including negligence), contract, or otherwise, + unless required by applicable law (such as deliberate and grossly + negligent acts) or agreed to in writing, shall any Contributor be + liable to You for damages, including any direct, indirect, special, + incidental, or consequential damages of any character arising as a + result of this License or out of the use or inability to use the + Work (including but not limited to damages for loss of goodwill, + work stoppage, computer failure or malfunction, or any and all + other commercial damages or losses), even if such Contributor + has been advised of the possibility of such damages. + + 9. Accepting Warranty or Additional Liability. While redistributing + the Work or Derivative Works thereof, You may choose to offer, + and charge a fee for, acceptance of support, warranty, indemnity, + or other liability obligations and/or rights consistent with this + License. However, in accepting such obligations, You may act only + on Your own behalf and on Your sole responsibility, not on behalf + of any other Contributor, and only if You agree to indemnify, + defend, and hold each Contributor harmless for any liability + incurred by, or claims asserted against, such Contributor by reason + of your accepting any such warranty or additional liability. + + END OF TERMS AND CONDITIONS + + APPENDIX: How to apply the Apache License to your work. + + To apply the Apache License to your work, attach the following + boilerplate notice, with the fields enclosed by brackets "[]" + replaced with your own identifying information. (Don't include + the brackets!) The text should be enclosed in the appropriate + comment syntax for the file format. We also recommend that a + file or class name and description of purpose be included on the + same "printed page" as the copyright notice for easier + identification within third-party archives. + + Copyright [yyyy] [name of copyright owner] + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + http://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. diff --git a/research/p112-a6-five-flat/vendor/PREDECESSOR-NOTICE.md b/research/p112-a6-five-flat/vendor/PREDECESSOR-NOTICE.md new file mode 100644 index 0000000000..c6f3494c2c --- /dev/null +++ b/research/p112-a6-five-flat/vendor/PREDECESSOR-NOTICE.md @@ -0,0 +1,3 @@ +# Notice + +Prepared by DreamingOfClouds with Claude Opus 5.5 (Anthropic), via Claude Code; Apache-2.0 (`LICENSE`, copied from the repository root). diff --git a/research/p112-a6-five-flat/vendor/PREDECESSOR-PROOF.md b/research/p112-a6-five-flat/vendor/PREDECESSOR-PROOF.md new file mode 100644 index 0000000000..8a129bc017 --- /dev/null +++ b/research/p112-a6-five-flat/vendor/PREDECESSOR-PROOF.md @@ -0,0 +1,239 @@ +# The P112 `3,4,6^8` profile is impossible + +## Statement + +Use the pinned 112 live E8 root lines `r_t` and their nine-bit labels `ell(t)`. +For any characteristic-zero field `K`, define + +``` +C = {c_h : c_h(t)=, h in K^8}, +w(q) = rank_F2 {ell(t) : q(t) != 0}. +``` + +There do not exist ten independent pieces spanning `T`, with +`dim(T intersect C)>=6`, whose respective weight upper bounds are + +``` +3,4,6,6,6,6,6,6,6,6. +``` + +This is one actual TWOSIDE `(b,t)=(6,4)` profile from DreamingOfClouds's +PR3154 at `708f0ad8928c383de8294aea3c126e9461d2066d`. It is not the whole +cell, C5, the P112 decoder floor or a supplier theorem. + +## Retained geometry and exact coverage + +The source-bound [root-simplex proof](vendor/ROOT-SIMPLEX-PROOF.md) and +Nick Petalas's PR3176 supply these geometric arguments: + +- Weight-three and weight-four supports have at most four and eight lines. + Every label has leading bit one, so a binary `d`-flat contains at most + `2^(d-1)` labels. A weight-six support has at most twenty live lines. + The replay enumerates all 788,035 three-dimensional annihilators in + `F2^9` to check this last bound. +- `h -> c_h` is injective and every nonzero codeword has at least 53 live + coordinates. +- A real subspace of dimension at most six contains at most 36 E8 root lines. + The eight seven-node chamber faces contain respectively + `42,28,22,14,16,23,37,63` root lines. The 42-line face has a D7 normal; + the 63-line face has a root normal. +- Independent scalar-root directions whose pair differences are scalar + roots have one common scale and orientations making a root star, with + squared norm two and distinct inner products one. + +The standard Weyl-chamber theorem remains an explicit dependency, not a +formalized consequence of a finite test. The replay checks simple-system +positivity, 960 simple reflections and all 7,140 root planes. It reconstructs +root and label bytes independently of the predecessor's binary data tables, +then checks their equality to the declared input. + +A nonzero direction with support at most 72 has at least forty perpendicular +live roots. Their rational span cannot have rank at most six by the 36-line +bound. It therefore has rank seven and a one-dimensional rational kernel. +This also proves that a field-valued direction is a scalar multiple of a +rational vector, over any `K` of characteristic zero. The chamber-face counts +leave only a root direction or a Weyl transform of the D7 normal. + +The retained program constructs a reflection-closed inventory of 1,080 D7 +normal lines containing that chamber normal. Their live support histogram is +`70:128, 73:896, 76:56`. Thus the complete support-72 alphabet is contained in +120 root lines plus 128 eligible non-root lines. Those 128 normals have one +entry `+1` or `-1` in each coordinate pair, up to common sign. Explicit even +signed permutations preserving the deleted frame normalize each to +`a=(1,0,1,0,1,0,1,0)`. All 128 normalizations are checked. + +## Seven affine endpoints + +Choose small pieces of weights `3,4,6`, with support union `S` of size at most +`4+8+20=32`. Call the seven remaining weight-six pieces `q_0,...,q_6`. +Let `D=T intersect C`. The quotient `T/D` has dimension at most four. + +The small pieces and any one `q_i` have support union at most `32+20=52<53`. +Their quotient images are independent: a dependence would be a nonzero +codeword supported on fewer than 53 lines, since the original pieces are +independent. The quotient therefore has dimension exactly four. Modulo the +three small images, the seven remaining images are nonzero in a +one-dimensional quotient. Rescale the `q_i` to give them equal images there. +Subtract suitable small-piece combinations `s_i` and write + +``` +c_0=0, c_i=q_i-q_0-s_i in D, i=1,...,6. +``` + +The six codewords are independent by their distinct coefficients on +`q_1,...,q_6`. They give seven affinely independent vertices in `K^8`. +Every edge is supported on at most `32+20+20=72` lines, so its direction is +in the complete root/D7 alphabet. + +At any coordinate outside `S`, the endpoint evaluations differ from the +vertex evaluations by one common shift. For seven scalar values, every +common shift leaves at least + +``` +7 - maximum equality multiplicity +``` + +nonzero entries. Cancelling a largest equality class attains this minimum. +The seven endpoints permit at most `7*20=140` support incidences. Both +branches below require more. + +## Mixed root/D7 branch + +Translate and rescale a non-root edge to the segment `0,a`. Any other vertex +`x` has `x=s*u`, `a-x=t*v` for distinct allowed rays `u,v` and nonzero +coefficients. Solving `a=s*u+t*v` gives exactly 58 possible vertices. +The solution is rational even when initially sought over `K`, by an +invertible rational two-by-two coordinate minor. The compatibility graph +has 595 edges, testing whether each difference is an allowed ray. + +Five further vertices form a five-clique. The complete exact census gives + +| Rank with the anchor | Five-cliques | +|---|---:| +| 4 | 630 | +| 5 | 3,360 | +| 6 | 3,360 | + +Only rank six is admissible. For each of these 3,360 cases, sum the minimum +nonzero costs after removing the 32 largest live costs. This relaxes the +actual `S` and allows arbitrary coordinate shifts. The surviving-cost +histogram is + +``` +142:1344, 145:336, 146:336, 147:112, 148:448, 149:560, 150:224. +``` + +Thus the mixed branch requires at least 142 incidences. A separate program +uses Gram intersections, a two-plus-three clique join, fraction-free integer +elimination and frequency-based deletion. It obtains the same graph, ranks +and costs, without calling those primary algorithms. + +## Root-only A6 branch and its losing relaxation + +The root-plane lemma identifies the vertices with one scaled affine root +A6 simplex. Extend each star prefix by every root having the prescribed +inner products. Reflections perpendicular to the prefix fix it pointwise. +Retaining every orbit of this subgroup is complete, even if the subgroup +is smaller than the full stabilizer. The extension orbit sizes are +`240;56;27;16;10;6`, leaving one rank-six star. + +Evaluate its seven vertices on all 120 root lines. The minimum nonzero-cost +spectrum is + +``` +0:1, 1:21, 2:63, 3:35, total cost 252. +``` + +Arbitrary removal of eight frame lines and 32 small-support lines leaves +only 137, below the allowance 140. This is a losing control. A proof cannot +replace the small supports by forty arbitrary deletions. + +A Weyl transformation taking the star to its representative moves the +puncture to an orthogonal eight-line frame. It maps binary label flats to +flats of the same dimension. Indeed, a root reflection is an invertible +integral automorphism of the simple-root lattice; reduce its coordinates +modulo two and leave the leading one fixed. Canonical root signs do not +matter modulo two. The replay checks all 960 simple-reflection label +relations. We must retain the actual rank-six and rank-four support flats. + +## New weighted cover lemma + +Let `c` be the full120 A6 cost function above. For any orthogonal eight-line +frame `F`, binary six-flat `V`, binary four-flat `U`, and set `A` of at most +four root coordinates, + +``` +sum_{r outside F union Lambda(V) union Lambda(U) union A} c(r) >= 141. +``` + +This relaxes the weight-three support to four arbitrary coordinates. The +following finite argument proves the lemma. + +All 2,025 orthogonal frames are enumerated. Their cost histogram is +`14:210,16:735,17:630,19:420,21:30`, so a frame costs at most 21. +A four-flat contains at most eight odd labels, costing at most 24; `A` costs +at most twelve. Suppose the union removed cost at least 112. Then `V` must +have full cost at least `112-21-24-12=55`. + +The complete six-flat enumeration has maximum cost 60. Exactly 63 distinct +masks have cost at least 55: 35 cost 57, and 28 cost 60. For every one of +these masks and every frame, the prefix `B=F union Lambda(V)` has cost at +most 77. A prefix costing at most 75 is impossible, since adding `U` and +`A` removes at most another 36. The remaining prefixes are exactly + +``` +B cost 76: 4,620 pairs; B cost 77: 2,520 pairs. +``` + +For these prefixes, `U` outside `B` would need cost at least +`112-c(B)-12`, hence 24 or 23. A four-flat containing at most six cost-three +labels has cost at most `6*3+2*2=22`. Any relevant four-flat must therefore +contain at least seven of the 35 cost-three labels. Those seven labels span +four dimensions: a three-flat contains at most four odd labels. Four of +them are a basis, so enumerating all four-element subsets of the 35 labels +covers every possible relevant four-flat. + +This construction gives exactly 135 masks: thirty contain seven cost-three +labels and 105 contain eight. Every one is checked against every relevant +prefix, a total of 963,900 tests. Their maximum residual cost is twelve for +both prefix costs, strictly below the necessary 23 or 24. All other +four-flats cost at most 22 even before subtracting `B`. Thus no removed +cost reaches 112. Integrality gives removed cost at most 111 and surviving +cost at least `252-111=141`. + +The separate checker enumerates all 788,035 six-flats and all 3,309,747 +four-flats using forward-echelon annihilators, instead of the primary +reverse-echelon/high-label construction. It recovers the exact same 63 +and 135 masks and the complete six-flat weight histogram. Its frames are +the 2,025-element simple-reflection orbit of the fixed frame, not the +primary orthogonality-clique traversal. It checks every relevant pair and +reproduces both residual maxima. The shared root reconstruction and +Weyl-chamber dependency remain explicit. + +## Finish, overlap and limits + +The actual root-only supports lie inside the sets of the weighted lemma, +so at least 141 endpoint incidences remain outside the small support. The +mixed branch requires 142. Both exceed 140. This proves the statement over +all characteristic-zero fields. + +The original unmodified TWOSIDE program and a separate transcription +retain this profile among the original 69 `(6,4)` survivors. Every +weight-certified four-piece quotient basis has weights `3,4,6,6`. Its +best two-six-flat packing leaves twelve certified cuts and six rank-six +nonbasis pieces. PR3162's ten-cut theorem and PR3167's twelve-cut theorem +with a rank-four nonbasis anchor do not supply this exclusion by that +route. This is an applicability check, not a universal novelty proof. + +The first session candidate `2,4,6^8` was discarded as already covered by +PR3162 through basis `2,4,6,6`. The present result changes that candidate +and repairs two losing relaxations: forty arbitrary cuts give 137; retaining +only the frame and six-flat but allowing twelve arbitrary small coordinates +gives 139. Neither alone proves the exclusion. + +This is an author-checked mathematical exclusion with separately implemented +finite checks, not independent human or proof-kernel review. The standard +Weyl-chamber theorem, inherited root-plane argument and original decoder +reduction remain dependencies. Full C5, other profiles, `C(P112)>=64`, +physical realization and any improved multiplication exponent remain open +or unchanged. No physical costs are assumed to be zero. diff --git a/research/p112-a6-five-flat/vendor/ROOT-SIMPLEX-PROOF.md b/research/p112-a6-five-flat/vendor/ROOT-SIMPLEX-PROOF.md new file mode 100644 index 0000000000..ccae082127 --- /dev/null +++ b/research/p112-a6-five-flat/vendor/ROOT-SIMPLEX-PROOF.md @@ -0,0 +1,176 @@ +# A root-simplex incidence obstruction + +## Statement and scope + +Let `K` be any characteristic-zero field. On the 112 live E8 root lines, +let `ell(t)` be the pinned binary label and let + +``` +C = {c_h : c_h(t) = , h in K^8}, +w(q) = rank_F2 {ell(t) : q(t) != 0}. +``` + +The coordinate representatives `r_t` may be doubled roots, as in the replay. +This changes no supports. Suppose nine linearly independent pieces span `T` +and `dim(T intersect C) >= 5`. Their weights cannot be bounded respectively by +either of these multisets: + +``` +3,4,4,6,6,6,6,6,6 +2,5,5,5,6,6,6,6,6. +``` + +These are precisely the two remaining `(b,t)=(5,4)` TWOSIDE beta shapes +reported by [PR3162](https://github.com/CrocSwap/integer-mult-bounds/pull/3162). The new theorem excludes them directly, without a +space-pair or deletion-set census. Combining it with that predecessor's +thirteen exclusions removes its fifteen-shape residue. That combination +inherits the predecessor's finite theorem and TWOSIDE reduction. Neither +full C5, the other beta cells, `C(P112)>=64`, supplier admission nor kappa +is established here. + +## Geometry used, with bounded replay + +The replay reconstructs the 120 E8 root lines and removes the eight pinned +frame lines. All 960 simple reflections preserve the root inventory. +Simple-root coordinates modulo two, with a leading one, give +the nine-bit labels. Their bytes agree with the declared main-branch input. +All 3,309,747 four-dimensional annihilators and all 788,035 three-dimensional +annihilators in `F2^9` are enumerated in unique reverse row-echelon form. +Their kernels establish the sharp support capacities `g(5)=12`, `g(6)=20`. +For `d=2,3,4`, the leading-one coordinate gives the elementary upper bound +`g(d)<=2^(d-1)`, hence capacities `2,4,8`. A lower-dimensional support extends +to a flat of the stated dimension, so upper bounds on piece weights suffice. + +Every nonzero codeword has support at least 53. Moreover, a codeword with +support below 70 is proportional to an E8 root codeword. Here is the +Weyl-chamber argument, with its finite quantities checked by the replay. +Below 70 means at least 43 live root lines are perpendicular. In a closed +Weyl chamber, perpendicular roots are generated by vanishing simple roots. +All 28 choices of six simple nodes contain at most 36 root lines. Thus +at least seven simple roots vanish. The eight seven-node faces have root-line +counts `42,28,22,14,16,23,37,63`. Only the last can reach 43; its normal is +a root direction. Weyl transformations preserve roots. Root directions have +live support 53 for 112 lines, or 56 for the eight removed frame lines. +This also proves the distance 53, since any putative smaller support would +be a root direction. The standard finite-root-system Weyl-chamber theorem +is used here, not formally proved by the executable. + +This argument extends to `K`. The rational roots perpendicular to a nonzero +field-valued direction have rational rank at most seven. If that rank were +at most six, a generic real normal to their span would have exactly the +roots in that span perpendicular, contradicting the rank-six bound of 36. +Thus the rank is seven, the rational kernel is one-dimensional, and the +direction is proportional over `K` to its rational generator. Apply the real +argument to that generator. The P112 roots span eight dimensions, so the +map `h -> c_h` is injective. + +## From nine pieces to six affine vertices + +Split the basis into three small pieces `s_1,s_2,s_3` and six remaining +pieces `q_0,...,q_5`. Put `S=union supp(s_j)`, `s=|S|`, and +`U=sum_i |supp(q_i)|`. In the first shape choose small weights `3,4,4`; +in the second choose `2,5,5`. + +Write `D=T intersect C` and let `lambda:T -> T/D`. Since `dim T=9` and +`dim D>=5`, the quotient has dimension at most four. For either split, +`S` together with the support of any one `q_i` has fewer than 53 lines. +The corresponding four quotient images are independent. Otherwise a +nonzero combination of four independent pieces would be a nonzero +codeword supported on fewer than 53 lines. Hence `dim(T/D)=4`, and the +three small quotient images are independent. + +Modulo their span, all six images of the `q_i` are nonzero in a +one-dimensional space. Rescale each `q_i` to give them the same image. +Supports and independence are preserved. There are unique small-piece +combinations `a_i` such that + +``` +c_i = q_i - q_0 - a_i belongs to D, i=1,...,5. +``` + +Set `c_0=0` and `a_0=0`. The five `c_i` are independent, by their distinct unit +coefficients on the nonbasis pieces `q_1,...,q_5`. Every edge + +``` +c_i-c_j = q_i-q_j-(a_i-a_j) +``` + +is nonzero and supported on `S union supp(q_i) union supp(q_j)`. +The support caps are at most 60 for the first shape and 66 for the second. +They are below 70, so all fifteen edges are root directions. By injectivity, +there are five independent vectors `h_i` with `c_i=c_{h_i}`, and each +nonzero difference among `0,h_1,...,h_5` is a scalar root. + +## Root-simplex lemma + +Normalize the real E8 roots to norm squared two. For two distinct root +lines, the only possible third root line in their rational plane occurs +in an A2 subsystem. It is represented by `alpha +/- beta` with coefficients +of absolute value one. The replay checks all 7,140 root-line pairs against +all 120 root lines using exact Gram determinants. It finds 3,780 planes +with two root lines and 3,360 with three. Alternatively this is the usual +rank-two simply-laced root-system fact. + +This fact applies to a plane over `K` as well: any rational root in the +`K`-span of two independent rational roots is already in their rational +span, by solving a nonsingular rational two-by-two coordinate minor. + +Write `h_i=b_i alpha_i`. Independence makes every pair of `alpha_i` +nonparallel. Since `h_i-h_j` is a third root line, the plane fact gives +`b_i/b_j=+1` or `-1`. Absorb these signs into the oriented roots. Thus +`h_i=b alpha_i` for one `b!=0`. Applying the same plane fact to their +differences gives `=1` and makes each +`alpha_i-alpha_j` an actual norm-two root. The six vertices +`0,alpha_1,...,alpha_5` form a root A5 simplex. + +Fix any E8 root `r` and evaluate it on those vertices. The six values + +``` +v = (0, , ..., ) +``` + +are integers. Every difference is the inner product of two roots, hence +lies in `{-2,-1,0,1,2}`. If some difference has absolute value two, +equality in Cauchy-Schwarz makes `r` the corresponding oriented edge root. +The six values then have multiplicities `1,1,4`, giving nine unequal pairs. +If no difference has absolute value two, all values occupy at most two +consecutive integer levels. There are at most `3*3=9` unequal pairs again. +Thus every live coordinate belongs to at most nine of the fifteen edge +supports. Multiplication by the common field scalar `b` changes no zeros. +This bound is universal; the literal A5 fixture in the replay is only a +sharp positive control, not a replacement for the argument. + +## Count incidences and exclude both shapes + +Each edge codeword has at least 53 nonzero coordinates. At most `9s` edge +incidences occur in `S`. Outside `S`, its coordinate is exactly +`q_i(t)-q_j(t)`. An unequal pair has a nonzero endpoint, and each nonzero +one of the six `q_i(t)` can meet only five pairs. Summing over coordinates, + +``` +15*53 - 9s <= outside edge incidences <= 5U. +``` + +The support capacities give the following contradictions. Upper bounds on +`s` decrease the left side and upper bounds on `U` increase the right side, +so overlaps or smaller actual supports only strengthen them. + +| Nine-piece shape | Small pieces | s cap | U cap | Required inequality | +|---|---|---:|---:|---| +| `3,4^2,6^6` | `3,4,4` | 20 | 120 | `615 <= 600` | +| `2,5^3,6^5` | `2,5,5` | 26 | 112 | `561 <= 560` | + +The second exclusion has margin exactly one under these bounds. Increasing +its small-support allowance from 26 to 27 would remove this contradiction; +the boundary control deliberately checks that case. No hypothesis that +the common deletion union lies in a five-flat is used. + +## Remaining obligations + +The proof concerns these two nine-piece configurations under the stated +intersection hypothesis. It uses the standard Weyl-chamber theorem and +finite exact capacity checks. There is no proof-kernel verification or +independent human review. The separate PR3162 reductions, the original +TWOSIDE feasibility filters and all other conjectures in PR3154 remain +their own dependencies. A closed weight residue does not certify a +decoder floor, a complete multiplication theorem or an improved exponent. diff --git a/research/p112-a6-five-flat/vendor/TWOSIDE-NOTES.md b/research/p112-a6-five-flat/vendor/TWOSIDE-NOTES.md new file mode 100644 index 0000000000..e3fd3f2b1d --- /dev/null +++ b/research/p112-a6-five-flat/vendor/TWOSIDE-NOTES.md @@ -0,0 +1,65 @@ +# TWOSIDE — K1 two-sided residues R-b (b_Q>=5), R-dep, CONJ-G cost-64 residue (Oct 16) +Labels PROVEN / CHECKED (two implementations) / CHECKED-1 (single implementation) / OPEN. python = W/venv/bin/python. +## STATE +- TWOSIDE: read #3029 README, CONJ-G, R-B, SIX §1-3 (Lemma B, S66, Basis-kill), SMALL2 §4. +- TWOSIDE: bk1.py (impl 1): Basis-kill (Lemma B + S66) applied to all size/cap-feasible σ-multisets for b=5..8. Closes (5,1),(5,2) [ (b,1) already vacuous by WALL 8.3 b_Q<=1 ]. + +- TWOSIDE: F7 lemma CHECKED (f7.py/f7r.py, rank + explicit-cover impls agree). bk1b/bk2b (BK + F7) survivor counts agree in all 24 cells. R-dep reformulated exactly (§2, PROVEN). CONJ-G residue restated (§3). Card DONE at ~115k. + +## §1 R-b (b_Q >= 5): Basis-kill transfer (PROVEN mod S66, which is CHECKED twice in SIX) +**Lemma BK.** Let B be a basis of span q(Lo) (|B| = ρ + b, b = b_Q), all pieces low (w <= 7). If some ρ pieces X0 ⊆ B have +Σ_{X0} g(w) < 53 and their weights pack into two groups of total weight <= 6 (+ at most one 1-piece), then b <= 3. +*Proof.* |∪_{X0} A_k| < 53 = d_1, so span q(X0) ∩ 𝒞 = 0: X0 is λ-independent for λ: span q(B) → span q(B)/(span ∩ 𝒞) ≅ K^ρ, hence a λ-basis. +SIX Lemma B (valid for every d; it uses only that B is a basis) gives b independent h_y (y ∉ X0) with Off(h_y) ⊆ U_{X0} ∪ Λ(F_y), w_y <= 7, so +rank ℓ(Off(h_y) ∖ X) <= 7 with X = Λ(V_1) ∪ Λ(V_2) [∪ t] ⊇ U_{X0}. S66 / S66+t: such h span <= 3. ∎ +bk1.py table (impl 1; σ=0 pieces treated as weight 2, X0 = ρ smallest; level 1/2 caps (32,20,12) on |Off|<=72 / E6 targets, global otherwise): +| b \ t | 1 | 2 | 3 | 4 | 5 | 6 | (min-Σσ survivor deficit; #survivors) +| 5 | 0 | 0 | 2 (4) | 2 (15) | 3 (38) | 3 (77) | +| 6 | 1 (1) | 1 (2) | 4 | 4 | 5 | 5 | +| 7 | 2 | 2 | 6 | 6 | 7 | 7 | +| 8 | 3 | 3 | 8 | 8 | 10 | 10 | +These are single-implementation survivor lists, NOT bounds on anything beyond "BX can fail only on these multisets". +- TWOSIDE: bk2.py (impl 2, own caps/brute packing) agrees: (5,1),(5,2) no survivors; (5,3) same 4 survivors. (5,2) CHECKED. ~75k tokens used. + +**Lemma F7 (CHECKED, two implementations: f7r.py rank = Gaussian elimination; f7r.py cover = explicit 7-flat pair search).** For every +7-dim label space V (all 43435), the directions h with rank ℓ(Off(h) ∖ Λ(V)) <= 7 are at most 2, and they are frame directions. +Completeness: such h has Off(h) ⊆ Λ(V) ∪ Λ(G), G 7-dim; |Off| >= 73 is impossible (36+36), |Off| <= 72 gives |Off| <= 32+32 = 64 (C11), +so h is one of the 120 root/frame directions (SIX §3 list), all tested. Histogram: 0:41431, 1:1976, 2:28 (roots never qualify). +**Corollary BK7 (PROVEN mod F7).** If some ρ pieces X0 with Σ_{X0} g < 53 have Σ_{X0} w <= 7, then b <= 2 (Lemma B gives b independent h_y). +bk1b.py (impl 1) / bk2b.py (impl 2): BK + BK7. Survivor counts agree in all 24 cells (CHECKED; full lists cross-checked only at (5,3), bk2): +| b \ t | 1 | 2 | 3 | 4 | 5 | 6 | (max deficit of a survivor; #survivors) | +| 5 | closed | closed | 2 (4) | 2 (15) | 3 (38) | 3 (77) | +| 6 | closed | 1 (1: 5^7,0) | 4 (17) | 4 (69) | 5 (174) | 5 (364) | +| 7 | closed | 2 (2: 5^8,0/1) | 6 (37) | 6 (154) | 7 (403) | 7 (885) | +| 8 | closed | 3 (3: 5^9,0/1/2) | 8 (60) | 8 (251) | 10 (684) | 10 (1556) | +So **BX holds at (5,1),(5,2) and every (b,1)** (CHECKED; (b,1) also by WALL 8.3). +**Exact residue R-b (OPEN).** Every survivor has a λ-basis X0 = ρ smallest pieces with |U_X0| < 53 that fails both packings. The two shapes: +(α) t = 2, b >= 6: all pieces weight 7 plus one piece of weight <= 4 (X0 = {small, 7}). Needed lemma F7+P: for V 7-dim and a set P of <= 4 lines + (a weight-<=4 piece: <= 8 lines, P ⊆ a 4-flat), the h with rank ℓ(Off(h) ∖ (Λ(V) ∪ P)) <= 7 span <= 5. +(β) t >= 3: weight-6 majority, X0 = {6,6,small...} (e.g. (5,3): [6^7,2], [7,6^6,2], [6^7,3], [6^6,5,4]). Needed lemma S66+P: for V1,V2 6-dim and P a + common set of <= 2 (resp. <= 4) lines, the h with rank ℓ(Off(h) ∖ X) <= w_y (w_y = 6 for the weight-6 non-basis pieces) span <= b − 1. + Both are kill46-shaped finite computations (orbit reps of V1 + all V2 + P), not attempted here (S66 mode t took 7 min in C; +2 lines ~ x50). + +## §2 R-dep, exactly (PROVEN algebra) +cost_k = ρ(R_k,A_k) = rank of Ω on U_{R_k} × U_{A_k} = w(A_k) − dim(U_{A_k} ∩ Z_{R_k}) (rank of a bilinear pairing is symmetric), so +**ε^row_k = w(A_k) − cost_k** exactly. The R-dep condition "for every k0 ∈ J: Σ_{k≠k0} ε^row_k >= cost_k0 + 1" becomes +Σ_J ε − (w_k0 − cost_k0) >= cost_k0 + 1 ⇔ **Σ_{k∈J} ε^row_k >= w(A_k0) + 1 for all k0 ⇔ Σ_J ε^row_k >= max_J w(A_k) + 1.** +(The "every k0" quantifier collapses to the heaviest column.) With ε^row_k <= min(w(A_k), 9 − w(R_k)): +rows of weight 9 give 0, weight 8 give <= 1 (Z_R = , corrected iff z ∈ U_A), weight 7 <= 2. +s = 1 (J = J_P ⊆ Lo_Q): row-side WALL Lemma 8.2 (transposed; PROVEN there from kpr15 CHECKED cover facts) gives two cases: + (i) no row of weight <= 6: Σ ε <= 2 n_7 + n_8^corr with all weight-7 rows on one frame line ⇒ **#corrected rows >= ⌈(w_max+1)/2⌉**; + (ii) exactly one row k1 of weight r <= 6 (the only low row), the rest weight >= 8: **n_8^corr >= w_max + 1 − min(w_{k1}, 9 − r)**. +Exact residue (OPEN): a low column circuit J at tight m meeting (i) or (ii) together with the cost-63 budget (N2). Not closed: the +circuit structure of the columns (A_k0 ⊆ ∪_{k≠k0} A_k) carries no codeword, so the cover tables bite only on the row side (pair lemma). +For s >= 2 the transposed Lemma 8.2 is not available (rows of J_P are a coset of an s-dim outside space): residue stated only via the boxed condition. + +## §3 CONJ-G residue (exact restatement; not closed) +D′: one-sided, 8+t terms (t = 2,3), corrected cost 64, n_c >= 4 (>= 3 unconditionally), so raw/ε-free cost Σw = 64 + n_c >= 67. +(a) #2816 uniqueness (Theorem U) is about ε-free cost 64 (δ = 0); D′ has ε-free cost >= 67, outside its scope: it gives nothing. +(b) #3074 padding sends D′ to a one-sided P120 decoder of cost exactly 64 + 8 = 72 = the L120 floor (equality case). L120 is not + unique at 72: the padded k = 4 root-swap family (t = 4) also attains it. So padding + uniqueness cannot kill D′ unless the L120 + equality case is classified; that classification (for 16 + t <= 19 terms) is the exact open statement. +(c) Branch d = 0, x = 0, m_T = 0 and no D7-type weight-8 member (|supp T| <= 4 suffices; SIX §7(b)) (NOT forced by peeling here, since slack = n_c >= 3): Δ_D = n_c gives cost_w(T) + c_9 = n_c <= |R| + c_9', + so |R| >= cost_w(T); the (k,g) mechanism of CONJ-G (A)/(B) yields a further swap line v ∉ R, so |R ∪ {v}| > cost_w(T), contradicting the + Swap Conjecture (SIX §7: #swap lines <= cost_w(T); PROVEN for κ <= 3, dim T = 1, or A nonsingular). This only re-derives CONJ-G's remark. + Open branches, exactly: m_T >= 1 (carriers in T), x >= 1, a D7-type weight-8 member, or d >= 1 with cost(T) − 8d + 8x + c_8 <= n_c (DP: d <= 5 ⇒ cost(T) − 8d >= 2). diff --git a/research/p112-a6-five-flat/vendor/bk2b.py b/research/p112-a6-five-flat/vendor/bk2b.py new file mode 100644 index 0000000000..3394029014 --- /dev/null +++ b/research/p112-a6-five-flat/vendor/bk2b.py @@ -0,0 +1,29 @@ +# TWOSIDE bk2: independent re-implementation of bk1 on cells (5,1),(5,2) (and prints (5,3) survivors for comparison). +# Works with weights w in {2..7} directly; own cap tables; brute-force packing over all bin assignments. +from itertools import product, combinations_with_replacement as cwr +CAPG={2:2,3:4,4:8,5:12,6:20,7:36}; CAPT={2:2,3:4,4:8,5:12,6:20,7:32} +DH=[None,53,78,92,100,106,109,111,112] +def feasible(W,b): + W=sorted(W) # ascending + for lev in range(1,b+1): # keep the len-(b-lev) smallest... i.e. drop the b-lev largest + X=W[:len(W)-(b-lev)] + sg=sum(CAPG[w] for w in X); st=sum(CAPT[w] for w in X) + if lev==1 and not (st>=53 or sg>=73): return False + if lev==2 and not (st>=78 or sg>=82): return False + if lev>=3 and sg=53: return False + if sum(X)<=7: return True + for asg in product((0,1),repeat=rho): + if all(sum(w for w,a in zip(X,asg) if a==k)<=6 for k in (0,1)): return True + return False +import sys +for b in range(5,9): + for t in range(1,7): + S=[] + for n in range(b,b+t+1): + for W in cwr(range(2,8),n): + if sum(w-2 for w in W)<6*b and feasible(W,b) and not killed(W,b): S.append(tuple(sorted((w-2 for w in W),reverse=True))) + print(b,t,len(S),min((6*b-sum(x) for x in S),default=0),flush=True) diff --git a/research/p112-a6-five-flat/vendor/cover.py b/research/p112-a6-five-flat/vendor/cover.py new file mode 100644 index 0000000000..de5ab021ec --- /dev/null +++ b/research/p112-a6-five-flat/vendor/cover.py @@ -0,0 +1,185 @@ +"""A6 weighted frame/six-flat/four-flat cover certificate. + +The rank-three support is relaxed to four arbitrary coordinates. Frame +traversal is adapted from Nick Petalas's PR3180; all weighted bounds here +are new. Apache-2.0. +""" + +import hashlib +import json +from collections import Counter +from itertools import combinations, product + +from vendor.geometry import SIMPLE, canonical, dot, require + +ALL = (1 << 120) - 1 + + +def full_labels(coordinates): + labels = tuple(1 | sum((int(x) % 2) << (i + 1) for i, x in enumerate(row)) + for row in coordinates) + require(len(labels) == len(set(labels)) == 120, "full120 labels") + require(all(0 < x < 512 and x & 1 for x in labels), "odd full120 labels") + return labels + + +def label_reflections(roots, labels): + index = {r: i for i, r in enumerate(roots)} + for r, label in zip(roots, labels, strict=True): + for j, simple in enumerate(SIMPLE): + factor = dot(r, simple) // 4 + reflected = canonical(tuple(x - factor * y + for x, y in zip(r, simple, strict=True))) + require(labels[index[reflected]] == label ^ ((factor & 1) << (j + 1)), + "Weyl label-linear relation") + return 960 + + +def cost_layers(costs): + require(len(costs) == 120 and Counter(costs) == {0: 1, 1: 21, 2: 63, 3: 35}, + "A6 cost inventory") + return tuple(sum(1 << i for i, c in enumerate(costs) if c >= level) + for level in (1, 2, 3)) + + +def weight(mask, layers): + return sum((mask & layer).bit_count() for layer in layers) + + +def frame_inventory(roots): + require(len(roots) == 120, "frame root count") + adjacency = tuple(sum(1 << j for j, s in enumerate(roots) if dot(r, s) == 0) + for r in roots) + stack, frames = [((), ALL)], [] + for _ in range(2_000_000): + if not stack: + break + chosen, candidates = stack.pop() + if len(chosen) == 8: + frames.append(chosen) + continue + for _ in range(120): + if not candidates: + break + bit = candidates & -candidates + candidates ^= bit + i = bit.bit_length() - 1 + stack.append(((*chosen, i), candidates & adjacency[i])) + require(len(stack) <= 961, "frame stack capacity") + require(not stack and len(frames) == len(set(frames)) == 2025, + "complete orthogonal-frame inventory") + return tuple(frames) + + +def selected_six_flats(labels, layers): + require(len(labels) == 120 and len(layers) == 3, "six-flat input dimensions") + kernels = tuple(ALL ^ sum(1 << i for i, label in enumerate(labels) + if (label & x).bit_count() & 1) for x in range(512)) + selected, histogram = set(), Counter() + for pivots in combinations(range(9), 3): + choices = [] + for pivot in pivots: + free = tuple(c for c in range(pivot) if c not in pivots) + rows = tuple((1 << pivot) | sum(((code >> i) & 1) << c + for i, c in enumerate(free)) + for code in range(1 << len(free))) + choices.append(tuple(kernels[row] for row in rows)) + for chosen in product(*choices): + mask = chosen[0] & chosen[1] & chosen[2] + cost = weight(mask, layers) + histogram[cost] += 1 + if cost >= 55: + selected.add(mask) + require(sum(histogram.values()) == 788035 and max(histogram) == 60, + "complete weighted six-flat census") + require(len(selected) == 63 + and Counter(weight(m, layers) for m in selected) == {57: 35, 60: 28}, + "high-weight six-flat inventory") + return tuple(sorted(selected)), dict(sorted(histogram.items())) + + +def high_four_flats(labels, layers): + high = tuple(label for i, label in enumerate(labels) if layers[2] >> i & 1) + require(len(high) == 35, "cost-three labels") + index = {label: i for i, label in enumerate(labels)} + masks = set() + for basis in combinations(high, 4): + span = {0} + for label in basis: + span.update(tuple(x ^ label for x in tuple(span))) + if len(span) != 16: + continue + mask = sum(1 << index[x] for x in span if x in index) + if (mask & layers[2]).bit_count() >= 7: + masks.add(mask) + require(len(masks) == 135 + and Counter((m & layers[2]).bit_count() for m in masks) == {7: 30, 8: 105}, + "high-cost four-flat inventory") + return tuple(sorted(masks)) + + +def arbitrary_extra(prefix, layers, removed): + require(type(removed) is int and 0 <= removed <= 120, "arbitrary-cut budget") + extra = 0 + for level in (3, 2, 1): + exact = layers[level - 1] ^ (layers[level] if level < 3 else 0) + taken = min(removed, (exact & ~prefix).bit_count()) + extra += level * taken + removed -= taken + return extra + + +def cover_pairs(frames, six_flats, four_flats, layers): + require(len(frames) == 2025 and len(six_flats) == 63 and len(four_flats) == 135, + "cover inventory sizes") + frame_histogram, prefix_histogram, quad_maxima = Counter(), Counter(), Counter() + maximum_prefix, tested, losing_maximum = 0, 0, 0 + losing_witness = None + for frame in frames: + frame_mask = sum(1 << i for i in frame) + frame_histogram[weight(frame_mask, layers)] += 1 + for six in six_flats: + prefix = frame_mask | six + cost = weight(prefix, layers) + maximum_prefix = max(maximum_prefix, cost) + relaxed = cost + arbitrary_extra(prefix, layers, 12) + if relaxed > losing_maximum: + losing_maximum = relaxed + losing_witness = {"frame": frame, "six_mask": six} + if cost < 76: + continue + prefix_histogram[cost] += 1 + required = 100 - cost # 112 total, allowing 12 for four arbitrary roots. + residual_maximum = 0 + for four in four_flats: + tested += 1 + residual = weight(four & ~prefix, layers) + residual_maximum = max(residual_maximum, residual) + require(residual < required, "weighted cover reaches 112") + quad_maxima[(cost, residual_maximum)] += 1 + require(frame_histogram == {14: 210, 16: 735, 17: 630, 19: 420, 21: 30}, + "A6 frame cost spectrum") + require(maximum_prefix == 77 and prefix_histogram == {76: 4620, 77: 2520}, + "frame/six-flat prefix boundary") + require(tested == 963900, "four-flat check coverage") + require(losing_maximum == 113, "arbitrary-twelve-cut losing control") + return {"frame_costs": dict(sorted(frame_histogram.items())), + "prefix_costs": dict(sorted(prefix_histogram.items())), + "maximum_prefix": maximum_prefix, "four_flat_tests": tested, + "residual_maxima": [[a, b, n] for (a, b), n in sorted(quad_maxima.items())], + "removed_upper": 111, "surviving_lower": 141, + "losing_arbitrary12_lower": 139, "losing_witness": losing_witness} + + +def weighted_cover(roots, coordinates, star): + costs = tuple(7 - max(Counter((0, *(dot(r, v) for v in star))).values()) + for r in roots) + labels = full_labels(coordinates) + layers = cost_layers(costs) + six, histogram = selected_six_flats(labels, layers) + four = high_four_flats(labels, layers) + raw = json.dumps({"six": six, "four": four}, separators=(",", ":")).encode() + return {"six_flat_histogram": histogram, "selected_six_flats": len(six), + "high_four_flats": len(four), "mask_sha256": hashlib.sha256(raw).hexdigest(), + "label_reflection_checks": label_reflections(roots, labels), + "cover": cover_pairs(frame_inventory(roots), six, four, layers)} diff --git a/research/p112-a6-five-flat/vendor/endpoint.py b/research/p112-a6-five-flat/vendor/endpoint.py new file mode 100644 index 0000000000..14b05de535 --- /dev/null +++ b/research/p112-a6-five-flat/vendor/endpoint.py @@ -0,0 +1,115 @@ +"""Seven-endpoint exclusion for the actual P112 3,4,6^8 profile. + +Nick Petalas. Apache-2.0. Geometry and mixed-edge routines retain PR3176's +exact source; this five-clique application and its support budget are new. +""" + +from collections import Counter +from itertools import combinations_with_replacement, product + +from vendor.geometry import dot, require +from vendor.mixed import ANCHOR, CAP, cliques, rational_rank, root_extensions + +PROFILE = (3, 4) + (6,) * 8 + + +def support_lower(costs, removed): + require(len(costs) in (112, 120), "support inventory size") + require(type(removed) is int and 0 <= removed <= len(costs), "deletion budget") + require(all(type(c) is int and 0 <= c <= 6 for c in costs), "support costs") + return sum(sorted(costs)[:len(costs) - removed]) + + +def mixed_six(vertices, adjacency, points): + anchor = tuple(2 * x for x in ANCHOR) + evaluations = tuple( + (0, dot(p, anchor), *(dot(p, v) for v in vertices)) for p in points + ) + ranks, bounds = Counter(), Counter() + witness = None + for chosen in cliques(adjacency, 5): + rank = rational_rank((anchor, *(vertices[i] for i in chosen))) + ranks[rank] += 1 + if rank != 6: + continue + costs = [ + 7 - max(Counter(row[:2] + tuple(row[i + 2] for i in chosen)).values()) + for row in evaluations + ] + lower = support_lower(costs, 32) + bounds[lower] += 1 + if witness is None or lower < witness["lower"]: + witness = {"lower": lower, "indices": chosen, + "spectrum": dict(sorted(Counter(costs).items()))} + require(ranks == {4: 630, 5: 3360, 6: 3360}, "five-clique rank census") + require(bounds == {142: 1344, 145: 336, 146: 336, 147: 112, + 148: 448, 149: 560, 150: 224}, "mixed support census") + require(witness is not None and witness["lower"] == 142, "minimum witness") + return {"ranks": dict(sorted(ranks.items())), + "bounds": dict(sorted(bounds.items())), "witness": witness} + + +def all_root_six(roots): + level, steps = [()], [] + for rank in range(6): + following = [] + for prefix in level: + representatives, sizes = root_extensions(prefix, roots) + steps.append({"rank": rank, "orbit_sizes": sizes}) + following.extend((*prefix, v) for v in representatives) + level = following + require(len(level) == 1, "root A6 branch count") + costs = tuple( + 7 - max(Counter((0, *(dot(r, v) for v in level[0]))).values()) + for r in roots + ) + require(Counter(costs) == {0: 1, 1: 21, 2: 63, 3: 35}, "A6 spectrum") + losing = support_lower(costs, 40) + require(losing == 137, "A6 arbitrary-deletion losing control") + return {"steps": steps, "spectrum": dict(sorted(Counter(costs).items())), + "losing_after_40_cuts": losing, "representative": level[0]} + + +def original_survivors(): + """Independent transcription of the pinned filter, only for (b,t)=(6,4).""" + distance = (0, 53, 78, 92, 100, 106, 109) + rows = [] + for size in range(6, 11): + for weights in combinations_with_replacement(range(2, 8), size): + if sum(w - 2 for w in weights) >= 36: + continue + feasible = True + for level in range(1, 7): + prefix = weights[:size - 6 + level] + total = sum(CAP[w] for w in prefix) + target = sum(32 if w == 7 else CAP[w] for w in prefix) + if ((level == 1 and target < 53 and total < 73) + or (level == 2 and target < 78 and total < 82) + or (level >= 3 and total < distance[level])): + feasible = False + break + basis = weights[:size - 6] + killed = False + if sum(CAP[w] for w in basis) < 53: + killed = sum(basis) <= 7 or any( + all(sum(w for w, g in zip(basis, assignment, strict=True) + if g == group) <= 6 for group in (0, 1)) + for assignment in product(range(2), repeat=len(basis)) + ) + if feasible and not killed: + rows.append(weights) + require(len(rows) == 69 and PROFILE in rows, "original (6,4) residue changed") + return rows + + +def application(): + rows = original_survivors() + small = (3, 4, 6) + support = sum(CAP[w] for w in small) + require(support == 32 and support + 20 < 53, "quotient basis budget") + require(support + 40 == 72, "edge alphabet boundary") + return {"b": 6, "t": 4, "weights": PROFILE, "original_survivors": len(rows), + "small_weights": small, "small_support_cap": support, + "quotient_basis_cap": support + 20, "edge_support_cap": 72, + "endpoints": 7, "endpoint_support_cap": 140, + "mixed_lower": 142, "all_root_lower": 141, "margin": 1} diff --git a/research/p112-a6-five-flat/vendor/geometry.py b/research/p112-a6-five-flat/vendor/geometry.py new file mode 100644 index 0000000000..222ea556fa --- /dev/null +++ b/research/p112-a6-five-flat/vendor/geometry.py @@ -0,0 +1,188 @@ +"""Exact E8/P112 geometry; coordinates follow PR3162's retained convention. + +Root and label reconstruction derive from Nick Petalas's PR3161/PR3162, +with the E8/P112 lineage retained in SOURCES.json. Apache-2.0. +""" + +from fractions import Fraction +from itertools import combinations, product +from math import gcd, lcm + +SIMPLE = ( + (1, -1, -1, -1, -1, -1, -1, 1), + (2, 2, 0, 0, 0, 0, 0, 0), + (-2, 2, 0, 0, 0, 0, 0, 0), + (0, -2, 2, 0, 0, 0, 0, 0), + (0, 0, -2, 2, 0, 0, 0, 0), + (0, 0, 0, -2, 2, 0, 0, 0), + (0, 0, 0, 0, -2, 2, 0, 0), + (0, 0, 0, 0, 0, -2, 2, 0), +) + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def dot(a, b): + return sum(x * y for x, y in zip(a, b, strict=True)) + + +def canonical(row): + return max(tuple(row), tuple(-x for x in row)) + + +def primitive(row): + denominator = lcm(*(x.denominator for x in row)) + integers = tuple(int(x * denominator) for x in row) + divisor = gcd(*integers) + require(divisor != 0, "zero projective direction") + return canonical(tuple(x // divisor for x in integers)) + + +def root_lines(): + roots = set() + for i, j in combinations(range(8), 2): + for sign in (-2, 2): + row = [0] * 8 + row[i], row[j] = 2, sign + roots.add(canonical(row)) + for row in product((-1, 1), repeat=8): + if sum(x == -1 for x in row) % 2 == 0: + roots.add(canonical(row)) + require(len(roots) == 120, "E8 root-line count") + return tuple(sorted(roots)) + + +def frame_lines(): + frame = [] + for i in range(0, 8, 2): + for sign in (-2, 2): + row = [0] * 8 + row[i], row[i + 1] = 2, sign + frame.append(canonical(row)) + return tuple(frame) + + +def solve(matrix, rhs): + """Exact eight-dimensional elimination, also used by the chamber check.""" + require(len(matrix) == len(rhs) == 8, "linear-system dimension") + rows = [[Fraction(x) for x in row] + [Fraction(y)] + for row, y in zip(matrix, rhs, strict=True)] + require(all(len(row) == 9 for row in rows), "linear-system row dimension") + for col in range(8): + pivot = next((i for i in range(col, 8) if rows[i][col]), None) + require(pivot is not None, "singular linear system") + rows[col], rows[pivot] = rows[pivot], rows[col] + scale = rows[col][col] + rows[col] = [x / scale for x in rows[col]] + for i in range(8): + if i != col: + scale = rows[i][col] + rows[i] = [x - scale * y + for x, y in zip(rows[i], rows[col], strict=True)] + return tuple(row[8] for row in rows) + + +def root_data(): + roots, frame = root_lines(), frame_lines() + points = tuple(row for row in roots if row not in frame) + matrix = tuple(zip(*SIMPLE, strict=True)) + coordinates = tuple(solve(matrix, row) for row in roots) + require(all(x.denominator == 1 for row in coordinates for x in row), + "nonintegral simple-root coordinates") + by_root = dict(zip(roots, coordinates, strict=True)) + labels = tuple(1 | sum((int(x) % 2) << (i + 1) + for i, x in enumerate(by_root[row])) for row in points) + require(len(points) == len(set(labels)) == 112, "P112 inventory") + require(all(0 < x < 512 and x & 1 for x in labels), "odd binary labels") + require(all(sum(r[i] * r[j] for r in points) == 112 * (i == j) + for i in range(8) for j in range(8)), "P112 spans eight dimensions") + return roots, points, labels, coordinates + + +def chamber_receipt(roots, points, coordinates): + for root in roots: + for simple in SIMPLE: + pairing = dot(root, simple) + require(dot(simple, simple) == 8 and pairing % 4 == 0, + "simple reflection normalization") + reflected = canonical(tuple(x - (pairing // 4) * y + for x, y in zip(root, simple, strict=True))) + require(reflected in roots, "root system is not reflection closed") + require(all(all(x >= 0 for x in c) or all(x <= 0 for x in c) + for c in coordinates), "simple system positivity") + six_counts = [sum(all(c[i] == 0 for i in omitted) for c in coordinates) + for omitted in combinations(range(8), 2)] + rays = [primitive(solve(SIMPLE, [int(i == j) for i in range(8)])) + for j in range(8)] + ray_zeros = [sum(dot(h, r) == 0 for r in roots) for h in rays] + require(max(six_counts) == 36, "rank-six parabolic cap") + require(ray_zeros == [42, 28, 22, 14, 16, 23, 37, 63], "chamber rays") + root_directions = {primitive(tuple(map(Fraction, r))) for r in roots} + require(rays[7] in root_directions, "qualifying ray is not a root") + support_sizes = [sum(dot(r, t) != 0 for t in points) for r in roots] + require(sorted(support_sizes) == [53] * 112 + [56] * 8, "root support sizes") + # These finite facts support the Weyl-chamber proof in PROOF.md. + return {"simple_reflection_checks": 960, + "rank_six_parabolic_counts": six_counts, "ray_zero_counts": ray_zeros, + "root_support_histogram": {"53": 112, "56": 8}} + + +def root_plane_receipt(roots): + """Every third root line in a root plane is the A2 sum/difference.""" + require(len(roots) == len(set(roots)) == 120 + and all(len(r) == 8 and dot(r, r) == 8 for r in roots), + "normalized root-plane input") + gram = tuple(tuple(dot(a, b) for b in roots) for a in roots) + histogram = {2: 0, 3: 0} + for i, j in combinations(range(120), 2): + d = gram[i][j] + require(d in (-4, 0, 4), "nonparallel root inner product") + in_plane = [] + for k in range(120): + x, y = gram[i][k], gram[j][k] + determinant = 512 + 2 * d * x * y - 8 * (d*d + x*x + y*y) + if determinant == 0: + in_plane.append(k) + expected = {i, j} + if d: + third = canonical(tuple(a - (d // 4) * b + for a, b in zip(roots[i], roots[j], strict=True))) + require(third in roots, "missing A2 root") + expected.add(roots.index(third)) + require(set(in_plane) == expected, "unexpected third root line") + histogram[len(in_plane)] += 1 + return {str(k): v for k, v in histogram.items()} + + +def flat_capacity(labels, dimension): + require(dimension in (5, 6), "only five/six-flat capacities are supported") + require(len(labels) == len(set(labels)) == 112 + and all(type(x) is int and 0 < x < 512 and x & 1 for x in labels), + "invalid P112 labels") + all_lines = (1 << 112) - 1 + kernels = tuple(all_lines ^ sum(1 << i for i, label in enumerate(labels) + if (label & x).bit_count() & 1) for x in range(512)) + histogram = [0] * 113 + annihilator_dimension = 9 - dimension + for pivots in combinations(range(9), annihilator_dimension): + row_kernels = [] + for pivot in pivots: + free = tuple(c for c in range(pivot) if c not in pivots) + rows = tuple((1 << pivot) | sum(((code >> i) & 1) << col + for i, col in enumerate(free)) + for code in range(1 << len(free))) + row_kernels.append(tuple(kernels[row] for row in rows)) + for chosen in product(*row_kernels): + mask = all_lines + for row in chosen: + mask &= row + histogram[mask.bit_count()] += 1 + expected = {5: (3309747, 12), 6: (788035, 20)}[dimension] + require(sum(histogram) == expected[0], "incomplete annihilator census") + maximum = max(i for i, n in enumerate(histogram) if n) + require(maximum == expected[1], "flat capacity changed") + return {"dimension": dimension, "subspaces": sum(histogram), "maximum": maximum, + "histogram": {str(i): n for i, n in enumerate(histogram) if n}} diff --git a/research/p112-a6-five-flat/vendor/mixed.py b/research/p112-a6-five-flat/vendor/mixed.py new file mode 100644 index 0000000000..e79086db5c --- /dev/null +++ b/research/p112-a6-five-flat/vendor/mixed.py @@ -0,0 +1,358 @@ +"""Exact 72-support direction alphabet and anchored P112 simplex census. + +Root-star stabilizer coverage follows Nick Petalas's PR3175. The mixed-edge +alphabet, rational two-ray intersections and application are new here. +""" + +from collections import Counter +from fractions import Fraction +from itertools import combinations, combinations_with_replacement, product + +from vendor.geometry import SIMPLE, canonical, dot, primitive, require, solve + +ANCHOR = (1, 0, 1, 0, 1, 0, 1, 0) +CAP = {2: 2, 3: 4, 4: 8, 5: 12, 6: 20, 7: 36} +PROFILE = (4, 5, 5) + (6,) * 9 + + +def projective(row): + require(len(row) == 8 and any(row), "invalid projective vector") + return primitive(tuple(map(Fraction, row))) + + +def alphabet(roots, points): + require(len(roots) == 120 and len(points) == 112, "incomplete root inventory") + norm_four = { + canonical(tuple(x + sign * y for x, y in zip(a, b, strict=True))) + for a, b in combinations(roots, 2) + if dot(a, b) == 0 + for sign in (-1, 1) + } + require( + len(norm_four) == 1080 and all(dot(v, v) == 16 for v in norm_four), + "norm-four projective inventory", + ) + for normal in norm_four: + for simple in SIMPLE: + pairing = dot(normal, simple) + require(pairing % 4 == 0, "nonintegral norm-four reflection") + reflected = canonical( + tuple(x - pairing // 4 * y for x, y in zip(normal, simple, strict=True)) + ) + require(reflected in norm_four, "norm-four inventory not Weyl closed") + ray = projective(solve(SIMPLE, [1] + [0] * 7)) + require(ray in {projective(v) for v in norm_four}, "missing D7 chamber ray") + histogram = Counter(sum(dot(v, p) != 0 for p in points) for v in norm_four) + require(histogram == {70: 128, 73: 896, 76: 56}, "D7 support spectrum") + short = { + projective(v) for v in norm_four if sum(dot(v, p) != 0 for p in points) <= 72 + } + expected = { + canonical( + tuple(signs[i // 2] if i % 2 == choices[i // 2] else 0 for i in range(8)) + ) + for choices in product(range(2), repeat=4) + for signs in product((-1, 1), repeat=4) + } + require(short == expected and len(short) == 128, "non-root anchor orbit") + directions = tuple(sorted({projective(v) for v in roots} | short)) + require(len(directions) == 248 and ANCHOR in short, "72-support alphabet") + return directions, tuple(sorted(short)), dict(sorted(histogram.items())) + + +def anchor_orbit(roots, frame, normals): + """An even signed permutation maps every short D7 normal to ANCHOR.""" + require(len(normals) == 128 and len(frame) == 8, "anchor-orbit input") + for normal in normals: + permutation = [0] * 8 + signs = [1] * 8 + for pair in range(4): + positions = (2 * pair, 2 * pair + 1) + live = next(i for i in positions if normal[i]) + permutation[2 * pair], permutation[2 * pair + 1] = ( + live, + sum(positions) - live, + ) + signs[2 * pair] = normal[live] + if signs.count(-1) % 2: + signs[1] = -1 # This position has zero anchor value. + image = tuple(signs[i] * normal[permutation[i]] for i in range(8)) + require(image == ANCHOR and signs.count(-1) % 2 == 0, "anchor normalization") + transformed = { + canonical(tuple(signs[i] * r[permutation[i]] for i in range(8))) + for r in roots + } + moved_frame = { + canonical(tuple(signs[i] * r[permutation[i]] for i in range(8))) + for r in frame + } + require( + transformed == set(roots) and moved_frame == set(frame), + "anchor symmetry changes P112", + ) + return len(normals) + + +def intersections(directions): + """Solve a=s*u+t*v for each pair of distinct projective directions.""" + require(len(directions) == len(set(directions)) == 248, "incomplete alphabet") + vertices = set() + for u, v in combinations(directions, 2): + i, j = next( + (i, j) for i, j in combinations(range(8), 2) if u[i] * v[j] != u[j] * v[i] + ) + determinant = u[i] * v[j] - u[j] * v[i] + s = Fraction(ANCHOR[i] * v[j] - ANCHOR[j] * v[i], determinant) + t = Fraction(u[i] * ANCHOR[j] - u[j] * ANCHOR[i], determinant) + if s and t and all(s * u[k] + t * v[k] == ANCHOR[k] for k in range(8)): + vertices.add(tuple(s * x for x in u)) + vertices.add(tuple(t * x for x in v)) + require(len(vertices) == 58, "anchored vertex inventory changed") + require( + all((2 * x).denominator == 1 for v in vertices for x in v), + "non-half-integral anchored vertex", + ) + return tuple(sorted(tuple(int(2 * x) for x in v) for v in vertices)) + + +def compatibility(vertices, directions): + require(len(vertices) == len(set(vertices)) == 58, "invalid vertex inventory") + allowed = set(directions) + adjacency = [0] * 58 + for i, j in combinations(range(58), 2): + difference = tuple(x - y for x, y in zip(vertices[i], vertices[j], strict=True)) + if projective(difference) in allowed: + adjacency[i] |= 1 << j + adjacency[j] |= 1 << i + require( + sum(row.bit_count() for row in adjacency) == 1190, "compatibility graph changed" + ) + return tuple(adjacency) + + +def cliques(adjacency, size): + """Unique increasing cliques; at most 34,834 states for size seven.""" + require(len(adjacency) == 58 and 0 <= size <= 7, "unsupported clique domain") + require( + all(type(row) is int and 0 <= row < 1 << 58 for row in adjacency), + "invalid adjacency bits", + ) + stack = [((), (1 << 58) - 1)] + for _ in range(40_000): + if not stack: + return + chosen, candidates = stack.pop() + if len(chosen) == size: + yield chosen + continue + for _ in range(58): + if not candidates: + break + bit = candidates & -candidates + candidates ^= bit + index = bit.bit_length() - 1 + stack.append(((*chosen, index), candidates & adjacency[index])) + require(len(stack) <= 407, "clique work-stack capacity") + require(not stack, "clique state budget exhausted") + + +def rational_rank(rows): + require( + 1 <= len(rows) <= 8 and all(len(row) == 8 for row in rows), + "rank input dimension", + ) + matrix = [list(map(Fraction, row)) for row in rows] + pivot = 0 + for col in range(8): + selected = next((i for i in range(pivot, len(matrix)) if matrix[i][col]), None) + if selected is None: + continue + matrix[pivot], matrix[selected] = matrix[selected], matrix[pivot] + scale = matrix[pivot][col] + matrix[pivot] = [x / scale for x in matrix[pivot]] + for i in range(pivot + 1, len(matrix)): + scale = matrix[i][col] + matrix[i] = [ + x - scale * y for x, y in zip(matrix[i], matrix[pivot], strict=True) + ] + pivot += 1 + return pivot + + +def surviving_support(values, removed): + require( + len(values) == 112 and type(removed) is int and 0 <= removed <= 112, + "invalid support/deletion domain", + ) + require(all(len(row) == 9 for row in values), "nine vertex values required") + costs = [9 - max(Counter(row).values()) for row in values] + return sum(sorted(costs)[: 112 - removed]), dict(sorted(Counter(costs).items())) + + +def mixed_census(vertices, adjacency, points): + anchor = tuple(2 * x for x in ANCHOR) + evaluations = tuple( + (0, dot(p, anchor), *(dot(p, v) for v in vertices)) for p in points + ) + ranks, bounds = Counter(), Counter() + witness, minimum, count = None, 1000, 0 + for chosen in cliques(adjacency, 7): + count += 1 + rank = rational_rank((anchor, *(vertices[i] for i in chosen))) + ranks[rank] += 1 + if rank != 8: + continue + values = tuple( + row[:2] + tuple(row[i + 2] for i in chosen) for row in evaluations + ) + lower, spectrum = surviving_support(values, 32) + bounds[lower] += 1 + if lower < minimum: + minimum, witness = ( + lower, + { + "indices": chosen, + "spectrum": spectrum, + "vertices_doubled": [anchor] + [vertices[i] for i in chosen], + }, + ) + require( + count == 10520 and ranks == {5: 840, 6: 5040, 7: 4032, 8: 608}, + "incomplete mixed-simplex rank census", + ) + require( + minimum == 182 + and bounds == {182: 112, 184: 16, 190: 112, 191: 128, 194: 128, 199: 112}, + "mixed-simplex support bound changed", + ) + return { + "cliques": count, + "rank_histogram": dict(sorted(ranks.items())), + "support_histogram": dict(sorted(bounds.items())), + "minimum_after_32_cuts": minimum, + "witness": witness, + } + + +def root_extensions(prefix, roots): + signed = tuple(v for r in roots for v in (r, tuple(-x for x in r))) + candidates = {r for r in signed if all(dot(r, p) == 4 for p in prefix)} + normals = tuple(r for r in roots if all(dot(r, p) == 0 for p in prefix)) + unseen, representatives, sizes = set(candidates), [], [] + for _ in range(240): + if not unseen: + break + first = min(unseen) + queue, seen = [first], {first} + for index in range(240): + if index >= len(queue): + break + for normal in normals: + pairing = dot(queue[index], normal) + require(pairing % 4 == 0, "nonintegral root-star reflection") + image = tuple( + x - pairing // 4 * y + for x, y in zip(queue[index], normal, strict=True) + ) + require(image in candidates, "root-star reflection leaves candidates") + if image not in seen: + seen.add(image) + queue.append(image) + require(len(queue) <= 240, "root-star orbit capacity") + require(seen <= unseen, "overlapping root-star orbits") + unseen.difference_update(seen) + representatives.append(first) + sizes.append(len(seen)) + require(not unseen, "incomplete root-star partition") + return representatives, sizes + + +def all_root_census(roots): + level, steps = [()], [] + for rank in range(8): + following = [] + for prefix in level: + representatives, sizes = root_extensions(prefix, roots) + steps.append({"rank": rank, "orbit_sizes": sizes}) + following.extend((*prefix, v) for v in representatives) + level = following + require(len(level) == 1, "rank-eight root-star orbit inventory") + costs = [ + 9 - max(Counter([0] + [dot(r, v) for v in level[0]]).values()) for r in roots + ] + require(Counter(costs) == {2: 36, 3: 84}, "A8 evaluation spectrum") + lower = sum(sorted(costs)[:80]) # Relax frame + small support to any 40 root lines. + require(lower == 204, "all-root support budget") + return {"steps": steps, "spectrum": {2: 36, 3: 84}, "minimum_after_40_cuts": lower} + + +def original_survivors(): + distance = (0, 53, 78, 92, 100, 106, 109, 111, 112) + rows = [] + for size in range(8, 13): + for weights in combinations_with_replacement(range(2, 8), size): + if sum(w - 2 for w in weights) >= 48: + continue + feasible = True + for level in range(1, 9): + prefix = weights[: size - 8 + level] + total = sum(CAP[w] for w in prefix) + target = sum(32 if w == 7 else CAP[w] for w in prefix) + if ( + (level == 1 and target < 53 and total < 73) + or (level == 2 and target < 78 and total < 82) + or (level >= 3 and total < distance[level]) + ): + feasible = False + break + basis = weights[: size - 8] + killed = False + if sum(CAP[w] for w in basis) < 53: + killed = sum(basis) <= 7 or any( + all( + sum( + w + for w, g in zip(basis, assignment, strict=True) + if g == group + ) + <= 6 + for group in (0, 1) + ) + for assignment in product(range(2), repeat=len(basis)) + ) + if feasible and not killed: + rows.append(weights) + require(len(rows) == 251 and PROFILE in rows, "original (8,4) residue changed") + return rows + + +def application(): + original = original_survivors() + bases = sorted( + {basis for basis in combinations(PROFILE, 4) if sum(CAP[w] for w in basis) < 53} + ) + require(bases == [PROFILE[:4]], "weight-certified quotient bases changed") + basis = bases[0] + cuts = [ + sum(CAP[w] for w, g in zip(basis, assignment, strict=True) if g == 2) + for assignment in product(range(3), repeat=4) + if all( + sum(w for w, g in zip(basis, assignment, strict=True) if g == group) <= 6 + for group in (0, 1) + ) + ] + require(min(cuts) == 20, "old weight-cover boundary changed") + return { + "b": 8, + "t": 4, + "weights": PROFILE, + "original_survivors": len(original), + "small_support_cap": 32, + "quotient_basis_cap": 52, + "edge_support_cap": 72, + "endpoint_support_cap": 180, + "mixed_lower": 182, + "all_root_lower": 204, + "margin": 2, + "weight_only_two_six_flat_cut_allowance": min(cuts), + } diff --git a/research/p112-a6-five-flat/verify.py b/research/p112-a6-five-flat/verify.py new file mode 100644 index 0000000000..4f63af3842 --- /dev/null +++ b/research/p112-a6-five-flat/verify.py @@ -0,0 +1,178 @@ +"""Exact replay of the characteristic-zero P112 profile 5,6^8 exclusion.""" + +import argparse +import hashlib +import json +import subprocess +import sys +from itertools import combinations_with_replacement, product +from pathlib import Path + +from cover_transfer import exhaustive_transfer +from vendor.cover import weighted_cover +from vendor.endpoint import all_root_six, mixed_six +from vendor.geometry import ( + chamber_receipt, + flat_capacity, + frame_lines, + require, + root_data, + root_plane_receipt, +) +from vendor.mixed import alphabet, anchor_orbit, compatibility, intersections + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parents[1] +DATA = "research/one-sided-six-multisets/data/data.txt" +PROFILE = (5,) + (6,) * 8 +CAP = {2: 2, 3: 4, 4: 8, 5: 12, 6: 20, 7: 36} + + +def read_bytes(path): + require(path.is_file() and not path.is_symlink(), "missing/linked input: " + str(path)) + require(path.stat().st_size <= 2_000_000, "oversized input: " + str(path)) + return path.read_bytes() + + +def bind_sources(): + sources = json.loads(read_bytes(PACKAGE / "SOURCES.json")) + rows = sources["retained_files"] + expected = {"geometry.py", "mixed.py", "cover.py", "endpoint.py", "bk2b.py", + "PREDECESSOR-PROOF.md", "PREDECESSOR-NOTICE.md", "LICENSE", + "TWOSIDE-NOTES.md", "ROOT-SIMPLEX-PROOF.md"} + require(len(rows) == 10 and {r["local_path"] for r in rows} + == {"vendor/" + name for name in expected}, "retained source inventory") + for row in rows: + raw = read_bytes(PACKAGE / row["local_path"]) + require(hashlib.sha256(raw).hexdigest() == row["sha256"], "retained SHA256") + blob = hashlib.sha1(b"blob " + str(len(raw)).encode() + b"\0" + raw, + usedforsecurity=False).hexdigest() + require(blob == row["git_blob"], "retained Git blob") + return sources + + +def bind_data(path, points, labels, sources): + pins = [row for row in sources["files"] if row["usage"] == "input"] + require(len(pins) == 1 and pins[0]["path"] == DATA, "live-input inventory") + raw = read_bytes(path) + digest = hashlib.sha256(raw).hexdigest() + require(digest == pins[0]["sha256"], "changed P112 input") + lines = raw.decode("utf-8").splitlines() + require(len(lines) >= 114, "truncated P112 input") + require(tuple(map(int, lines[0].split())) == labels, "P112 labels differ") + require(tuple(tuple(map(int, line.split())) for line in lines[2:114]) == points, + "P112 roots differ") + return digest + + +def original_survivors(): + """Separate transcription of the original (6,3) weight filter.""" + distance = (0, 53, 78, 92, 100, 106, 109) + survivors = [] + for size in range(6, 10): + for weights in combinations_with_replacement(range(2, 8), size): + if sum(w - 2 for w in weights) >= 36: + continue + feasible = True + for level in range(1, 7): + prefix = weights[:size - 6 + level] + total = sum(CAP[w] for w in prefix) + target = sum(32 if w == 7 else CAP[w] for w in prefix) + if ((level == 1 and target < 53 and total < 73) + or (level == 2 and target < 78 and total < 82) + or (level >= 3 and total < distance[level])): + feasible = False + break + basis = weights[:size - 6] + killed = False + if sum(CAP[w] for w in basis) < 53: + killed = sum(basis) <= 7 or any( + all(sum(w for w, a in zip(basis, assignment, strict=True) if a == k) + <= 6 for k in (0, 1)) + for assignment in product((0, 1), repeat=len(basis)) + ) + if feasible and not killed: + survivors.append(weights) + require(len(survivors) == 17 and PROFILE in survivors, "original (6,3) residue") + return survivors + + +def application(): + survivors = original_survivors() + no_seven = [row for row in survivors if max(row) <= 6] + require(len(no_seven) == 6 and all(len(row) == 9 for row in no_seven), + "original rank-at-most-six residue") + require(all(all(a <= b for a, b in zip(row, PROFILE, strict=True)) + for row in no_seven), "componentwise consequence") + small, endpoints = CAP[5] + CAP[6], 7 * CAP[6] + require(small == 32 and small + 20 < 53 and small + 40 == 72, + "quotient and edge hypotheses") + return {"cell": [6, 3], "weights": PROFILE, "small_weights": [5, 6], + "small_support_cap": small, "quotient_basis_cap": small + 20, + "edge_support_cap": small + 40, "endpoint_allowance": endpoints, + "mixed_lower": 142, "root_lower": 141, + "original_survivors": len(survivors), + "original_no_seven_profiles": no_seven, + "scope": "One maximal profile; six original no-seven profiles dominated." + " Earlier exclusions may already cover some dominated profiles."} + + +def predecessor_table(): + result = subprocess.run([sys.executable, "-I", "-B", str(PACKAGE / "vendor/bk2b.py")], + capture_output=True, text=True, check=True, timeout=120) + require(not result.stderr and len(result.stdout) <= 4096, "original table output") + rows = [tuple(map(int, line.split())) for line in result.stdout.splitlines()] + require(len(rows) == 24 and all(len(row) == 4 for row in rows), "table dimensions") + require([(r[0], r[1]) for r in rows] + == [(b, t) for b in range(5, 9) for t in range(1, 7)], "table order") + require(rows[8][2] == 17, "original (6,3) count") + return rows + + +def receipt(): + sources = bind_sources() + roots, points, labels, coordinates = root_data() + digest = bind_data(ROOT / DATA, points, labels, sources) + directions, normals, normal_histogram = alphabet(roots, points) + symmetries = anchor_orbit(roots, frame_lines(), normals) + vertices = intersections(directions) + adjacency = compatibility(vertices, directions) + root_bound = all_root_six(roots) + return { + "schema": "p112-a6-five-flat/v1", "input_sha256": digest, + "alphabet": {"directions": len(directions), "anchor_symmetries": symmetries, + "D7_support_histogram": normal_histogram}, + "mixed": mixed_six(vertices, adjacency, points), + "all_root": root_bound, + "weighted": weighted_cover(roots, coordinates, root_bound["representative"]), + "chamber": chamber_receipt(roots, points, coordinates), + "root_planes": root_plane_receipt(roots), + "flat_capacities": [flat_capacity(labels, d) for d in (5, 6)], + "cover_transfer": exhaustive_transfer(), + "application": application(), "original_table": predecessor_table(), + } + + +def check_receipt(actual, expected): + require(json.dumps(actual, sort_keys=True) == json.dumps(expected, sort_keys=True), + "committed mathematical receipt differs") + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--output", type=Path, help="write a new external receipt") + args = parser.parse_args() + result = receipt() + if args.output is None: + check_receipt(result, json.loads(read_bytes(PACKAGE / "RESULT.json"))) + else: + output = args.output.expanduser().resolve() + require(not output.is_relative_to(ROOT), "receipt output must be outside checkout") + with output.open("x", encoding="utf-8") as stream: + stream.write(json.dumps(result, indent=2) + "\n") + print("PASS_A6_FIVE_FLAT profile=5,6^8 mixed=142 root=141 allowance=140 errors=0" + " six_flats=788035 five_flats=3309747 frames=2025 transfer_subsets=64839") + + +if __name__ == "__main__": + main()