diff --git a/research/p112-common30-span/PREDECESSORS.json b/research/p112-common30-span/PREDECESSORS.json new file mode 100644 index 0000000000..be1c4343af --- /dev/null +++ b/research/p112-common30-span/PREDECESSORS.json @@ -0,0 +1,89 @@ +{ + "schema_version": 1, + "pins": [ + { + "number": 3154, + "head": "708f0ad8928c383de8294aea3c126e9461d2066d", + "title": "C(P112) >= 64: complete reduction to stated conjectures", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/3154", + "state": "open", + "merged": false, + "author": "DreamingOfClouds", + "role": "Original TWOSIDE/C5 and necessary filter, retained by PR3282; original author DreamingOfClouds." + }, + { + "number": 3163, + "head": "89419106cd86896c366e853795978f1bc85f9112", + "title": "test(research): certify a complete P112 common-deletion slice", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/3163", + "state": "closed", + "merged": true, + "author": "petalas", + "role": "Complete fixed-first-space shared-four-deletion predecessor; retains the common-set quantifier and full-direction coverage." + }, + { + "number": 3269, + "head": "ebe02d33157dc6c6d3b35df204e4a39242b7429e", + "title": "Prove analytic E8 binary-support capacities 12 and 20", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/3269", + "state": "closed", + "merged": true, + "author": "petalas", + "role": "Prior global binary support capacities12/20; rank-six20 is rechecked here." + }, + { + "number": 3282, + "head": "9607079de93907d87e6430d6de154f21a66c03e4", + "title": "Certify source-bound P112 caller coverage for the (6,4) cell", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/3282", + "state": "closed", + "merged": true, + "author": "petalas", + "role": "Canonical retention of original filter and TWOSIDE note; conditional caller-inventory predecessor." + }, + { + "number": 3289, + "head": "e8570c50f9591c9ca653a527ed9626aaa703c3bc", + "title": "Reconcile original P112 cover contracts for three caller rows", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/3289", + "state": "closed", + "merged": true, + "author": "petalas", + "role": "Original cover and quotient-composition predecessor, not a claim about the present public frontier." + }, + { + "number": 3931, + "head": "33b6be488be1e9e38f2f3f9bcfc4a7db0e8a332d", + "title": "Exclude a historical C5 caller with a common-cut23 bound", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/3931", + "state": "open", + "merged": false, + "author": "Clear1nsight", + "role": "Same donor's prior common23 bound and different caller. Adjacent ten-piece cut22 reuse is credited, not a new geometric result." + }, + { + "number": 3951, + "head": "9aacf01037f6e19cabb95ccbea15fcc2965dcd4d", + "title": "Independently audit inherited P112 support and A2 bounds", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/3951", + "state": "open", + "merged": false, + "author": "Clear1nsight", + "role": "Same donor's preceding dependency audit and chamber/field argument. model.py is explicitly adapted from its table model; the new core is separate." + } + ], + "geometry": { + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/3164", + "head": "857384079ab640a949fb7618b7909664d3e737e5", + "author": "Nick Petalas", + "role": "Root-simplex/geometry lineage, literal simple-system definition retained in canonical main." + }, + "runtime": "All executable inputs resolve at canonical main20ecf289. No pending predecessor Git object or executable is required. The primary executes only the authenticated original filter definitions for the literal caller.", + "new_pending_predecessor": { + "pr": 3960, + "head": "7e8d98e351ac153d81943218bf168dc8548b1cea", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/3960", + "role": "Common24 result and actual cap30 handoff; model.py and independent shell/Cramer reconstruction explicitly adapted; new graph and common30 theorem here." + }, + "status_scope": "Historical predecessor metadata retained from PR3960; exact heads/roles are bindings, not a refreshed scientific acceptance claim." +} diff --git a/research/p112-common30-span/PROOF.md b/research/p112-common30-span/PROOF.md new file mode 100644 index 0000000000..263cf13987 --- /dev/null +++ b/research/p112-common30-span/PROOF.md @@ -0,0 +1,168 @@ +# Common30 rank-seven span and one literal C5 caller + +Fix the full 120 doubled E8 root lines R, oriented by first nonzero coordinate, +the frame F={2e_0 +/- 2e_1,...,2e_6 +/- 2e_7}, and P=R\F. The original table +orders P lexicographically. Labels are ell(r)=(1,c(r) mod2) in F2^9 for the +pinned integral simple coordinates. Binary support weight is the rank of +these labels, rather than the number of support sites. + +For a characteristic-zero field K let C={c_h:h in K^8}, c_h(r)=r dot h on P, +and write Off(h) for its nonzero support. + +**Theorem.** Under ONE fixed S subset P of size at most30, the normals h with +rank_F2 ell(Off(h)\S)<=7 span a K-space of dimension at most **three**. +An explicit independent triple at a common cut of size30 attains three. +Moreover, for |S|<=29 there are at most **two projective normal directions**. +These are universal common-cut statements, allowing arbitrary S and arbitrary +characteristic-zero coefficient fields. + +**Literal caller.** The eleven collectively independent pieces with binary +weights 2,2,2,2,2,6,7,7,7,7,7 cannot have code-intersection dimension at least5. +This is the named historical TWOSIDE (b,t)=(5,6) profile, not the whole C5 +problem, a decoder theorem, supplier admission or a selected-bound change. + +## 1. Reduction to all120 root normals, including the frame + +The table and simple coordinates are authenticated against canonical main. +The model checks the 56 two-coordinate and64 all-odd root-line patterns, +exact coordinate equations, signs, original112 labels, and the live Gram +matrix112I. Thus evaluation is injective over every characteristic-zero K. + +The reversed-pivot RREF enumeration covers every two-dimensional annihilator +of a seven-space in F2^9 exactly once. All43,435 seven-spaces have full-root +trace at most36. A qualifying direction consequently satisfies + + |Off(h)| <= 30+36 = 66 < 70. + +Here are the full-root chamber and field arguments, adapted with credit from +PR3951/3960. The eight simple reflections permute the240 signed roots; they +therefore generate a finite group, since their action on a spanning set is +faithful. Solve rationally for rho dot alpha_i=1. For a real normal v maximize +rho dot g(v) over the finite group. Any negative simple pairing would make a +simple reflection increase the functional. The maximizing normal is in the +closed chamber. Every positive root has nonnegative simple coordinates, so +its pairing vanishes exactly when its support is in the zero simple nodes. +The zero roots form the corresponding simple face. No Weyl move is assumed +to preserve the removed frame or the binary labels. + +The checked faces on at most six nodes have at most36 root lines. The +seven-node face counts are42,28,22,14,16,23,37,63; the last has a root normal. +For a qualifying h in K^8, let Z be the rational span of its perpendicular +live roots. There are at least112-66=46 such roots. If rank_Q Z<=6, a generic +real normal to Z avoids every root hyperplane not forced by Z, so its zero +roots span Z. Its chamber face has rank at most6, contradicting46>36. +Therefore rank_Q Z=7: rank8 would force h=0 over K by a nonzero rational minor. +Rational elimination preserves rank under extension to any characteristic-zero +K, so h is a K-multiple of a rational generator of the one-dimensional kernel. +That real generator has at least46 perpendicular roots. Only the63-line +seven-node face can occur because46>42. Reflection transport then identifies +its normal with one of the120 root lines. This argument requires no embedding +K into R or C. Direct evaluation gives live-root support53 and frame-root +support56. The same reasoning applied to a hypothetical support below53 +proves the code distance is53, attained by live root normals. + +## 2. Complete completion-cut graph + +For a root normal a and binary seven-space V set + + C(a,V) = Off(a) \ Lambda(V). + +Normal a qualifies for S exactly when C(a,V) subset S for some V: extend its +residual label span to a seven-space. Every one of120*43,435=5,212,200 pairs +is tested. There are24,264 completion records with cut size<=30, and24,264 +distinct (normal,cut) nodes. Their cut-size counts are: + +| Size | Nodes | +|---:|---:| +| 21 | 336 | +| 23 | 5,376 | +| 24 | 504 | +| 25 | 3,136 | +| 27 | 10,752 | +| 28 | 1,024 | +| 29 | 3,136 | + +Join two nodes of distinct normal owners exactly when their cuts have union +size<=30. Exhaustive pair comparison gives9,828 edges. A collection admitted +by the SAME S gives a clique and its total cut union has size<=30; pairwise +compatibility alone is never substituted for this total-union condition. + +The primary walks increasing-index cliques while retaining the total union. +It continues a prefix only when its normals are rationally independent. +Every independent four-tuple has all its ordered prefixes independent, +so pruning dependent prefixes cannot omit a four-dimensional witness. +The full visited counts are: + +| Prefix length | Union size | Rational rank | Count | +|---:|---:|---:|---:| +| 1 | as above | 1 | 24,264 | +| 2 | 22,24,25,26,28,29,30 | 2 | 9,828 | +| 3 | 30 | 2 | 896 | +| 3 | 30 | 3 | 3,584 | +| 4 | 30 | 3 | 2,688 | + +There is no independent four-prefix. Thus if the qualifying directions for +an arbitrary S spanned dimension>=4, choosing four independent root normals +and one contained completion cut for each would produce a visited independent +four-prefix, a contradiction. Rational ranks of these root vectors equal +their ranks over K. This proves the common30 span bound. + +Every triple of distinct root normals has an independent first pair. All +admitted triples are consequently visited, including dependent triples. +Their union size is always30. Hence |S|<=29 permits at most two projective +normal directions. The listed independent triple at30 also shows that the +cut allowance29 is maximal for a uniform span-at-most-two statement. + +A separate finite-core checker imports neither primary nor predecessor +executables. It reconstructs the shell, computes integral coordinates with +Cramer's rule/Bareiss determinants, and enumerates10,795 six-spaces in F2^8 +with four affine cosets each, plus255 leading-zero spaces. All flat, +completion-record, node and edge digests agree. It directly tests all +compatible quadruples with total cut union<=30, including those with a +dependent first triple, using exact Gram determinants rather than the +primary's rational-elimination/prefix-pruning algorithm. This corroboration +is within the same donor/assistant context, not independent human or +formal-kernel acceptance. + +## 3. The actual quotient and intersection dimension + +Let T be the span of the eleven independent pieces in the stated profile, +D=T intersect C, and assume dim D>=5. Then dim(T/D)<=6. The first six pieces +have support union S of size at most5*2+20=30. A binary rank-two support has +at most2 sites because all labels have leading one. The global rank-six +capacity20 is credited to Nick Petalas/PR3269 and rechecked here on every +788,035 binary six-space. Since30<53, every nonzero combination of those +six independent pieces has support below the code distance and is not a +codeword. Their quotient images are independent. Thus dim(T/D)=6 and dim D=5. + +For each of the five remaining rank-seven pieces q_y, its quotient image +has a unique representative a_y in the six-piece span. Then c_y=q_y-a_y lies +in C. These five codewords are independent: their coefficients on the five +distinct nonbasis pieces are the identity matrix in the original independent +piece basis. Injectivity of evaluation gives five independent normals h_y. +Outside the SAME S, their supports lie in support(q_y), so their binary +support ranks are at most7. The theorem allows span dimension at most3, +contradicting5. Coefficients, overlaps and cancellations are unrestricted. + +The authenticated original PR3154 necessary filter retains the literal list. +Its strict excess is29<30. All462 six-piece subsets are checked: the minimum +certified capacity sum is30, attained only by the five rank-two and one +rank-six pieces. This is not a lower bound on an actual support union. + +## 4. Credit and limits + +Nick Petalas supplies the global capacities, root-shortening and common-cut +lineage (including PR3269,3163,3282,3289); DreamingOfClouds/PR3154 supplies +TWOSIDE/C5; David Arias supplies the quadratic model; joaqcoo and retained +E8/P112 sources retain their attribution. This donor's PR3951 audits inherited +bounds and the field step; PR3960 supplies the common24 theorem and two +other callers. The table model and separate shell/Cramer implementation are +explicitly adapted from PR3960, and are not claimed newly independent of it. +The new finite graph, complete common30 span proof and named caller exclusion +are this package's contribution. Frozen predecessors are unchanged. + +No complete cell reconciliation, full C5, complete decoder floor, native +physical/restoration/consumer/all-size/supplier admission, selected cold +replay or new kappa is claimed. Written proof and finite computation remain +subject to mathematical review. Chris R / Clear1nsight, with substantial +OpenAI Codex assistance, Apache-2.0. diff --git a/research/p112-common30-span/README.md b/research/p112-common30-span/README.md new file mode 100644 index 0000000000..70ffe201ec --- /dev/null +++ b/research/p112-common30-span/README.md @@ -0,0 +1,84 @@ +# P112 common30 span and the literal 2^5,6,7^5 caller + +For ONE common set S of at most30 live P112 sites, all characteristic-zero +normals whose residual support labels have binary rank<=7 span at most +**three dimensions**. A literal independent triple at30 attains three. +For |S|<=29 there are at most **two projective directions**. This settles the +exact relaxed geometric obligation for the historical (b,t)=(5,6) independent +piece profile **2^5,6,7^5**: six small pieces have support cap303. + +[PROOF.md](PROOF.md) supplies the complete root-normal/characteristic-zero +reduction, finite graph coverage, threshold29/30 and actual quotient transfer. +[RESULT.json](RESULT.json) stores exact digests, counts, literal normals and +cut labels. The five-direction caller uses linear independence; a count of +projective directions alone is not substituted for span dimension. + +The finite domain contains43,435 seven-spaces,5,212,200 root/space pairs, +24,264 completion records and9,828 compatible distinct-owner pairs. All4,480 +admissible triples require cut30;3,584 are independent. The primary traverses +2,688 four-node extensions of independent triples, all rank3. A separate +implementation directly checks **all3,360 compatible quadruples**, including +those with dependent first triples, and finds zero Gram determinants. It +uses separately coded shell/Cramer labels and affine-generator spaces, +imports no primary/predecessor executable and matches full record/graph +digests. This is computational corroboration within one donor/assistant +context, not independent human or formal-kernel acceptance. + +## Reproduction + +CPython3.12, standard library only, from the repository root: + +``` +python3.12 -I -Werror -B scripts/research_package.py --package research/p112-common30-span +``` + +The three explicit optimized commands are in [VERIFY.json](VERIFY.json). +They read pinned sources and compare results; they do not rewrite evidence. +The direct scripts also work in a source export with the declared input paths. +Controls compare the independence-pruned search with a subset oracle across +all1,024 graphs on five vertices (testing every graph that spans three in this +fixture); they check a real attaining triple, reject a synthetic independent +fourth direction, expose the characteristic-two boundary and reject actual +optimized CLI source/manifest corruption. No selected cold replay, Lean, +Docker or physical/supplier validation is run. + +## Source, scope and overlap + +Canonical main20ecf2891d80b5acf18d980b2164fb44ea7faa90, priority revision6. +The assigned item explicitly follows PR3960's cap30 caller handoff. The parent +coordinator fetched canonical main and checked671 open PR bodies and rendered +C5/start/handoff/active-board discussions before the split; no matching +common30 item was found. This worker checked PR3960's live head and body, +canonical retained caller sources, an open-PR lexical common30 query and the +local overlap helper. That helper searched2,490 local records but had no usable +remote snapshot because the gh executable was unavailable. Closed-work, +arbitrary-diff, discussion-wide and private-work coverage remains partial; +these checks are not a novelty certificate. Publication refresh is reported +in the PR. The scoped package changes no selected record or frozen source. + +The root model and separate shell/Cramer reconstruction are explicitly adapted +from this donor's PR3960, whose model is adapted from PR3951. Their code lineage +is credited; "separate" does not mean newly independent of those predecessors. +Nick Petalas supplies the global capacities and root/common-cut predecessors; +DreamingOfClouds/PR3154 supplies TWOSIDE and C5; David Arias, joaqcoo and the +retained E8/P112 lineage retain their attribution. Exact predecessor heads and +roles are in [PREDECESSORS.json](PREDECESSORS.json). The new contribution is +the complete common30 graph/span proof and this named literal exclusion. + +This is not a full cell reconciliation, full C5, decoder floor, supplier, +multiplication theorem or new kappa. Literal caller survival is independently +checked against the authenticated retained necessary filter; survival alone +is never treated as an actual construction. + +## Open next questions + +Review the generic-normal rational-rank argument and finite graph coverage, +then reconcile a different actual caller against current public contracts +before expanding the search. Each structured question in [TASK.json](TASK.json) +states relevance, first step and blocker. The current session stops at this +one caller; no continuing reservation is made. + +Prepared by Chris R / Clear1nsight with substantial OpenAI Codex assistance, +including parallel research agents. Apache-2.0. diff --git a/research/p112-common30-span/RESULT.json b/research/p112-common30-span/RESULT.json new file mode 100644 index 0000000000..4904823303 --- /dev/null +++ b/research/p112-common30-span/RESULT.json @@ -0,0 +1,292 @@ +{ + "spaces7": 43435, + "flat_inventory_digest": "5009cb750c3a5c0a1f71b0331892b3b34a4fb8f1c025a69c109516428d22efb9", + "maximum_rank7_trace": 36, + "spaces6": 788035, + "maximum_rank6_trace": 20, + "chamber": { + "signed_reflections": 1920, + "rho": [ + "0", + "1/2", + "1", + "3/2", + "2", + "5/2", + "3", + "23/2" + ], + "rank6_face_maximum": 36, + "seven_node_counts": [ + 42, + 28, + 22, + 14, + 16, + 23, + 37, + 63 + ], + "E7_normal": [ + 0, + 0, + 0, + 0, + 0, + 0, + 2, + 2 + ] + }, + "critical_records": 24264, + "critical_record_digest": "b18cd614d77c5b6df267f29503223014f361bf23fd49b02ca77191a8340ad353", + "nodes": 24264, + "node_digest": "a74f2f50038ec6e520f28f6fa105fb131266dca5902a462a4ba550ec33256a6c", + "cut_size_histogram": { + "21": 336, + "23": 5376, + "24": 504, + "25": 3136, + "27": 10752, + "28": 1024, + "29": 3136 + }, + "edges": 9828, + "edge_digest": "40214530c91c53e730db654442432c24bb75b45dd8720b67299fdc1594de22df", + "prefix_histogram": [ + [ + [ + 1, + 21, + 1 + ], + 336 + ], + [ + [ + 1, + 23, + 1 + ], + 5376 + ], + [ + [ + 1, + 24, + 1 + ], + 504 + ], + [ + [ + 1, + 25, + 1 + ], + 3136 + ], + [ + [ + 1, + 27, + 1 + ], + 10752 + ], + [ + [ + 1, + 28, + 1 + ], + 1024 + ], + [ + [ + 1, + 29, + 1 + ], + 3136 + ], + [ + [ + 2, + 22, + 2 + ], + 168 + ], + [ + [ + 2, + 24, + 2 + ], + 2716 + ], + [ + [ + 2, + 25, + 2 + ], + 448 + ], + [ + [ + 2, + 26, + 2 + ], + 672 + ], + [ + [ + 2, + 28, + 2 + ], + 2688 + ], + [ + [ + 2, + 29, + 2 + ], + 448 + ], + [ + [ + 2, + 30, + 2 + ], + 2688 + ], + [ + [ + 3, + 30, + 2 + ], + 896 + ], + [ + [ + 3, + 30, + 3 + ], + 3584 + ], + [ + [ + 4, + 30, + 3 + ], + 2688 + ] + ], + "maximum_span_common30": 3, + "maximum_directions_common29": 2, + "attaining_triple": { + "normal_indices": [ + 2, + 9, + 43 + ], + "normals": [ + [ + 0, + 0, + 0, + 0, + 0, + 2, + -2, + 0 + ], + [ + 0, + 0, + 0, + 0, + 2, + 0, + 0, + 2 + ], + [ + 1, + -1, + -1, + -1, + -1, + -1, + 1, + -1 + ] + ], + "cut_labels": [ + 257, + 425, + 421, + 385, + 293, + 397, + 61, + 29, + 3, + 171, + 427, + 271, + 299, + 399, + 143, + 39, + 135, + 391, + 419, + 163, + 151, + 407, + 435, + 179, + 183, + 439, + 403, + 147, + 25, + 57 + ] + }, + "caller": { + "weights": [ + 2, + 2, + 2, + 2, + 2, + 6, + 7, + 7, + 7, + 7, + 7 + ], + "b": 5, + "t": 6, + "required_intersection_dimension": 5, + "quotient_dimension": 6, + "minimum_six_piece_capacity_sum": 30, + "minimum_basis_choices": 1, + "six_piece_subsets": 462, + "strict_excess_deficit": 1, + "required_independent_directions": 5, + "uniform_available_span_dimension": 3 + } +} diff --git a/research/p112-common30-span/SOURCES.json b/research/p112-common30-span/SOURCES.json new file mode 100644 index 0000000000..e1c527c9c1 --- /dev/null +++ b/research/p112-common30-span/SOURCES.json @@ -0,0 +1,42 @@ +{ + "schema_version": 1, + "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81", + "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "67f085acd86acd7d4e03922d9cf4b26bca66fed5", + "sha256": "47b42433f5a85809a3aadd29c2c339da2c6ed728e4f7762df6b88bccb7874cf0" + }, + { + "path": "research/one-sided-six-multisets/data/data.txt", + "usage": "input", + "git_blob": "dc591a4e0252bac096e6c63c51058f6caee66bfe", + "sha256": "ac4a48851b922f2a433684b60c74768ae3bb4fc5e8990ffe63e3942bb3c2ea34" + }, + { + "path": "research/p112-b6-t4-reconciliation/vendor/PR3154-TWOSIDE.md", + "usage": "input", + "git_blob": "e3fd3f2b1dfd77b597f000b38ec2dbec3dbca931", + "sha256": "226cd59ccc6bc065319e5e4c4768c889206169ff58f74ef4053eeadc5b2e03c8" + }, + { + "path": "research/p112-b6-t4-reconciliation/vendor/bk2b.py", + "usage": "input", + "git_blob": "3394029014bb13f16225587a153fa7b70016de6d", + "sha256": "dff16eff255c883db372a587cf3f34e6f35c08f75c60af9d11952be5a5838807" + }, + { + "path": "research/p112-root-simplex-exclusion/geometry.py", + "usage": "input", + "git_blob": "222ea556faf2b275f73815c4e7d0d5f1e3294f2f", + "sha256": "b8ac379e41f5ad83bdb6c7f7c55129fc3d9c07801ea61591478f25d72ff0b021" + } + ] +} diff --git a/research/p112-common30-span/TASK.json b/research/p112-common30-span/TASK.json new file mode 100644 index 0000000000..0559d851f5 --- /dev/null +++ b/research/p112-common30-span/TASK.json @@ -0,0 +1,78 @@ +{ + "schema_version": 1, + "task_id": "complex-rank-shape-decoder", + "priority_revision": 6, + "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "original_card": { + "id": "complex-rank-shape-decoder", + "question": "Can a decoder deliver the local paid mass in fewer, larger-rank children (block frame climbs instead of rank-1 to rank-3 steps)?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/complex-local-word-ceiling/README.md", + "research/complex-decoder-field-extension-seed44/README.md", + "research/complex-frame-pair-decoders/README.md", + "research/selected-k8-unrestricted-ends/README.md", + "research/eisenstein-reduction-copy-floor/README.md" + ], + "methods": [ + "Find one exact small decoding identity whose frame path climbs in blocks, and price its complete per-call profile.", + "Bound the best effective child rank achievable for one fixed support alphabet, including copies, frames and restoration." + ], + "acceptance_gate": "A per-call local profile, with all copied information, frames and restoration counted, whose ceiling exceeds the selected word's by at least 5%; masked or overcomplete supports must change an assumption of the eight-term all-pairs bound. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "research/complex-local-word-ceiling/verify.py" + ], + "expected": "PASS_COMPLEX_LOCAL_WORD_CEILING", + "inspect": "Read the selected word's per-call local profile, its packing ceiling and the lever table; run levers.py for the ideal budget of the lever you target.", + "scope": "Positive control and planning budget only; this is not a new construction or full cold replay." + }, + "first_experiment": "Before any synthesis, write the candidate per-call local profile (and centre charge / unpaid coordinates if changed) and screen it with ceiling.ceiling(); reject it if even the ideal ceiling does not beat the selected word's by your stated margin. Ideal budget: rank-16 delivery is 2.31x (levers.py).", + "bottleneck_link": "Rank-1 children are about half of recursive cost; the selected word's effective child rank is about 3.9. Larger-rank delivery lowers recursive cost per unit of paid mass.", + "allowed_variations": [ + "One masked, overcomplete or block decoder family with exact labels and supports.", + "A scoped lower bound on effective rank for one alphabet.", + "If the coverage law, template or guard changes, derive an applicable fully charged replacement bound instead of applying the incumbent ceiling outside its scope." + ], + "scope_change_triggers": [ + "Repacking idle remainders of an unchanged word (covered by the packing ceiling).", + "Repeating the eight-term all-pairs search inside its proved scope.", + "Only changing helper terminal subspaces and monotone frames within the fixed scalar word, entrances and cleanup contract already covered by #1995/#2013.", + "Searching below C=40 in the #2017 Eisenstein binary scalar-rectangle or fixed-support block-linear additive pairing model; specify a changed premise instead. This bound does not cover every complex decoder.", + "Continuing a partial cost improvement while leaving the same unpriced consumer, restoration or central-readout obligation unresolved; refresh the family expansion decision first. Local product-retiming evidence has a narrow scope and is not a ban on changed graphs or contracts." + ], + "overlap_terms": [ + "rank shape", + "block climb", + "masked decoder", + "overcomplete", + "effective rank" + ] + }, + "scope_status": "changed", + "actual_scope": "Uniform common30 rank-seven normal span at most3 over every characteristic-zero field; common29 at most2 projective directions; exclusion of literal historical (5,6) caller2^5,6,7^5.", + "scope_change_reason": "Explicit donor-directed parallel follow-up to PR3960; one assigned actual caller requires quotient cap30 and five independent directions.", + "bottleneck_link": "The eleven-piece caller forces five independent code directions after one common30-site cut. A span bound below5 closes this exact profile without general two-flat expansion.", + "budget_minutes": 60, + "stop_rule": "Decide the actual cap30 caller by a bounded exact common-cut graph, then stop search and verify sources, independent implementation and export.", + "outcome": "completed", + "evidence": "43435 seven-spaces;5212200 root/flat pairs;24264 records;9828 compatible pairs;4480 total admissible triples;2688 primary independent-prefix four-continuations;3360 separate-checker all-quadruples. Maximum span3 attained at30; all triples require30. Caller quotient6, intersection5, supportcap30, five required directions.", + "author": "Chris R / Clear1nsight with substantial OpenAI Codex assistance", + "ai_assistance": "Substantial OpenAI Codex assistance, including parallel agents. All checks remain in the same donor/assistant context; no independent human or formal-kernel acceptance.", + "open_questions": [ + { + "question": "Can an independent reviewer validate the root-normal field argument and complete common-cut graph proof?", + "why_it_matters": "Finite record agreement does not itself certify the mathematical reduction and coverage implications.", + "first_step": "Read PROOF.md sections1-2 and compare rational-prefix and direct-Gram quadruple checks.", + "blocked_by": "Independent human or formal-kernel review has not been performed." + }, + { + "question": "Which different actual C5 caller remains after source-bound reconciliation of these new contracts?", + "why_it_matters": "This named exclusion does not establish a full cell or C5 theorem.", + "first_step": "Refresh live overlap and bind another literal caller to its actual quotient, support cut and required intersection dimension.", + "blocked_by": "No new caller census or next expansion is claimed in this package." + } + ] +} diff --git a/research/p112-common30-span/VERIFY.json b/research/p112-common30-span/VERIFY.json new file mode 100644 index 0000000000..5794ecf87b --- /dev/null +++ b/research/p112-common30-span/VERIFY.json @@ -0,0 +1,50 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/one-sided-six-multisets/data/data.txt", + "research/p112-b6-t4-reconciliation/vendor/PR3154-TWOSIDE.md", + "research/p112-b6-t4-reconciliation/vendor/bk2b.py", + "research/p112-root-simplex-exclusion/geometry.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-O", + "-Werror", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 480, + "checks": "All43435seven-spaces,24264completionrecords,9828edges,independent-prefixcoverage;globalrank6capacity and literalcaller quotient binding." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-Werror", + "-B", + "{package}/independent.py" + ], + "timeout_seconds": 480, + "checks": "No primary/predecessor executable imports: Cramer/Bareiss,affineenumeration,all3360compatiblequadrupleGramdeterminants,digestagreement." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-Werror", + "-B", + "{package}/test_controls.py" + ], + "timeout_seconds": 120, + "checks": "All1024five-vertexgraphs screened; qualifying graph-oracle comparison,literal rank3witness,false rank4rejection,char2boundary and optimizedCLI source/manifestrejections." + } + ] +} diff --git a/research/p112-common30-span/independent.py b/research/p112-common30-span/independent.py new file mode 100644 index 0000000000..1c59b35239 --- /dev/null +++ b/research/p112-common30-span/independent.py @@ -0,0 +1,204 @@ +#!/usr/bin/env python3 +"""Separate finite-core check: Cramer's rule, affine generator spaces, all compatible quadruples. + +Shell/Cramer/affine routines adapted with credit from PR3960; new graph and +quadruple check here. No primary or predecessor executable is imported. Same author/assistant context; +this is computational corroboration, not independent human or kernel acceptance. +Chris R / Clear1nsight with substantial OpenAI Codex assistance; Apache-2.0. +""" +import ast +from collections import Counter, defaultdict +import hashlib +from itertools import combinations, product +import json +from pathlib import Path +import sys + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +MANIFEST_SHA = '4d49389e8131d6ec139722f60e12d697e4d0d31eba205b5e6d11543d22b4afd3' + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def unique(pairs): + result = {} + for key,value in pairs: + need(key not in result, 'duplicate JSON key') + result[key] = value + return result + + +def digest(value): + return hashlib.sha256(json.dumps(value,sort_keys=True,separators=(',',':')).encode()).hexdigest() + + +def sources(): + raw = (HERE/'SOURCES.json').read_bytes() + need(hashlib.sha256(raw).hexdigest() == MANIFEST_SHA, 'source manifest identity') + result = {} + for row in json.loads(raw,object_pairs_hook=unique)['files']: + if row['usage'] != 'input': + continue + p = ROOT/row['path'] + need(not any(x.is_symlink() for x in [p,*p.parents]), 'input symlink') + data = p.read_bytes() + need(len(data)<=2_000_000 and hashlib.sha256(data).hexdigest()==row['sha256'], 'source SHA256') + need(hashlib.sha1(b'blob '+str(len(data)).encode()+b'\0'+data).hexdigest()==row['git_blob'], 'Git blob') + result[row['path']] = data + return result + + +def determinant(matrix): + a = [list(row) for row in matrix] + previous,sign = 1,1 + for k in range(len(a)-1): + pivot = next((i for i in range(k,len(a)) if a[i][k]),None) + if pivot is None: + return 0 + if pivot != k: + a[k],a[pivot] = a[pivot],a[k] + sign = -sign + p = a[k][k] + for i in range(k+1,len(a)): + for j in range(k+1,len(a)): + value = p*a[i][j]-a[i][k]*a[k][j] + need(value%previous == 0, 'Bareiss exact division') + a[i][j] = value//previous + a[i][k] = 0 + previous = p + return sign*a[-1][-1] + + +def reconstruct(payloads): + text = payloads['research/one-sided-six-multisets/data/data.txt'].decode().splitlines() + live_rows = [tuple(map(int,line.split())) for line in text[2:114]] + geometry = ast.parse(payloads['research/p112-root-simplex-exclusion/geometry.py']) + simple = next(ast.literal_eval(n.value) for n in geometry.body if isinstance(n,ast.Assign) + and any(isinstance(t,ast.Name) and t.id=='SIMPLE' for t in n.targets)) + frame = {tuple((2 if k==i else 2*s if k==i+1 else 0) for k in range(8)) + for i in range(0,8,2) for s in [-1,1]} + all_rows = set() + for i,j in combinations(range(8),2): + for sign in [-1,1]: + all_rows.add(tuple(2 if k==i else 2*sign if k==j else 0 for k in range(8))) + for tail in product([-1,1],repeat=7): + if sum(x<0 for x in tail)%2 == 0: + all_rows.add((1,*tail)) + roots = sorted(all_rows) + need(len(roots)==120 and sorted(all_rows-frame)==live_rows, 'literal E8 shell/frame') + matrix = [list(row) for row in zip(*simple)] + det = determinant(matrix) + need(det != 0, 'simple system invertible') + labels = [] + for r in roots: + coords = [] + for j in range(8): + modified = [row[:] for row in matrix] + for i in range(8): + modified[i][j] = r[i] + numerator = determinant(modified) + need(numerator%det==0, 'integral Cramer coordinates') + coords.append(numerator//det) + need(all(sum(coords[j]*simple[j][i] for j in range(8))==r[i] for i in range(8)), 'Cramer reconstruction') + labels.append(1+sum((x%2)<<(j+1) for j,x in enumerate(coords))) + live = sum(1<>i&1] == list(map(int,text[0].split())), 'original label binding') + return roots,labels,live + + +def affine_inventory(labels): + point = {x>>1:1<p] + for word in range(1<>bit&1: + rows[i] |= 1<>i&1)<>i&1 and sum(x*y for x,y in zip(r,h))) + for flat,multiplicity in inventory.items(): + cut = word & ~flat + if cut.bit_count() <= 30: + records.extend([(a,flat,cut)]*multiplicity) + records.sort() + nodes = sorted({(a,c) for a,f,c in records}) + adjacent = [set() for _ in nodes] + # A different pair traversal and a direct all-quadruple test, without prefix pruning. + grouped = [[i for i,(a,c) in enumerate(nodes) if a==normal] for normal in range(120)] + edges = [] + for left,right in combinations(grouped,2): + for i in left: + cut = nodes[i][1] + for j in right: + if (cut | nodes[j][1]).bit_count() <= 30: + adjacent[i].add(j); adjacent[j].add(i); edges.append((i,j)) + triangles,quadruples = Counter(),Counter() + for i,j in edges: + for k in adjacent[i] & adjacent[j]: + if k<=j: + continue + cut = nodes[i][1] | nodes[j][1] | nodes[k][1] + if cut.bit_count()>30: + continue + normals = [roots[nodes[q][0]] for q in [i,j,k]] + gram = [[sum(x*y for x,y in zip(a,b)) for b in normals] for a in normals] + det = determinant(gram) + need(det>=0 and cut.bit_count()==30, 'all triples require common30') + triangles[(cut.bit_count(),det>0)] += 1 + for q in adjacent[i] & adjacent[j] & adjacent[k]: + if q<=k: + continue + joined = cut | nodes[q][1] + if joined.bit_count()>30: + continue + four = normals+[roots[nodes[q][0]]] + gram4 = [[sum(x*y for x,y in zip(a,b)) for b in four] for a in four] + need(determinant(gram4)==0, 'independent compatible quadruple') + quadruples[joined.bit_count()] += 1 + need(triangles[(30,True)]>0, 'independent triple exists') + return {'spaces7':sum(inventory.values()),'flat_inventory_digest':digest(sorted(inventory.items())), + 'critical_records':len(records),'critical_record_digest':digest(records), + 'nodes':len(nodes),'node_digest':digest(nodes),'edges':len(edges),'edge_digest':digest(sorted(edges))},triangles,quadruples + + +def main(): + need(not sys.argv[1:], 'no arguments accepted') + observed,triangles,quadruples = compute() + expected = json.loads((HERE/'RESULT.json').read_bytes(),object_pairs_hook=unique) + for key,value in observed.items(): + need(json.dumps(value,sort_keys=True)==json.dumps(expected[key],sort_keys=True),'independent receipt mismatch '+key) + need(triangles=={(30,False):896,(30,True):3584},'complete triangle histogram') + # This includes quadruples whose first three directions are dependent. + need(quadruples=={30:3360},'complete quadruple histogram') + print('PASS_COMMON30_INDEPENDENT Cramer_roots=120 affine_spaces=43435 triangles=4480 all_quadruples=3360 span=3') + + +if __name__=='__main__': + main() diff --git a/research/p112-common30-span/model.py b/research/p112-common30-span/model.py new file mode 100644 index 0000000000..4d7248f52b --- /dev/null +++ b/research/p112-common30-span/model.py @@ -0,0 +1,124 @@ +"""Table model retained from PR3960, adapted there from PR3951 (Chris R / Clear1nsight). +No predecessor executable is imported. New rank-seven computation is in verify.py. + +Chris R / Clear1nsight with substantial OpenAI Codex assistance. Apache-2.0. +Definitions retain Nick Petalas, David Arias and the E8/P112 lineage. +""" + +import ast +from fractions import Fraction +from itertools import combinations, product + +SIMPLE = ((1, -1, -1, -1, -1, -1, -1, 1), (2, 2, 0, 0, 0, 0, 0, 0), + (-2, 2, 0, 0, 0, 0, 0, 0), (0, -2, 2, 0, 0, 0, 0, 0), + (0, 0, -2, 2, 0, 0, 0, 0), (0, 0, 0, -2, 2, 0, 0, 0), + (0, 0, 0, 0, -2, 2, 0, 0), (0, 0, 0, 0, 0, -2, 2, 0)) + + +def require(ok, message): + if not ok: + raise ValueError(message) + + +def dot(a, b): + return sum(x * y for x, y in zip(a, b, strict=True)) + + +def canonical(row): + return row if next(x for x in row if x) > 0 else tuple(-x for x in row) + + +def basis(values, width=9): + rows = [0] * width + for value in values: + for j in range(width - 1, -1, -1): + if value >> j & 1: + if rows[j]: + value ^= rows[j] + else: + rows[j] = value + break + return [row for row in rows if row] + + +def span(rows): + values = [0] + for row in rows: + values += [x ^ row for x in values] + return values + + +def solve(matrix, columns): + """Exact dense simultaneous solve, independent of triangular source formulas.""" + n = len(matrix) + a = [[Fraction(x) for x in row] + [Fraction(c[i]) for c in columns] + for i, row in enumerate(matrix)] + for j in range(n): + p = next(i for i in range(j, n) if a[i][j]) + a[j], a[p] = a[p], a[j] + scale = a[j][j] + a[j] = [x / scale for x in a[j]] + for i in range(n): + if i != j: + scale = a[i][j] + a[i] = [x - scale * y for x, y in zip(a[i], a[j], strict=True)] + return [tuple(row[j] for row in a) for j in range(n, len(a[0]))] + + +def reconstruct(table, geometry): + assignments = ast.parse(geometry).body + literal = next(ast.literal_eval(n.value) for n in assignments + if isinstance(n, ast.Assign) + and any(isinstance(t, ast.Name) and t.id == 'SIMPLE' for t in n.targets)) + require(literal == SIMPLE, 'simple-system definition binding') + lines = table.decode().splitlines() + live = [tuple(map(int, line.split())) for line in lines[2:114]] + original_labels = list(map(int, lines[0].split())) + frame = [tuple(2 * (i == a) + s * 2 * (i == a + 1) for i in range(8)) + for a in (0, 2, 4, 6) for s in (-1, 1)] + roots = sorted(live + frame) + shell = {tuple(2 * (k == i) + s * (k == j) for k in range(8)) + for i, j in combinations(range(8), 2) for s in (-2, 2)} + shell.update((1, *t) for t in product((-1, 1), repeat=7) if sum(t) % 4 == 3) + require(roots == sorted(shell) and len(roots) == 120, 'full E8 root patterns') + coordinates = solve(list(zip(*SIMPLE, strict=True)), roots) + require(all(x.denominator == 1 for c in coordinates for x in c), 'integral coordinates') + coordinates = [tuple(map(int, c)) for c in coordinates] + require(all(tuple(sum(c[i] * SIMPLE[i][j] for i in range(8)) for j in range(8)) == r + for r, c in zip(roots, coordinates, strict=True)), 'exact coordinate equations') + require(all(min(c) >= 0 or max(c) <= 0 for c in coordinates), 'simple-coordinate signs') + labels = [1 + sum((x % 2) << (i + 1) for i, x in enumerate(c)) for c in coordinates] + require(len(set(labels)) == 120 and all(x & 1 for x in labels), 'full affine labels') + require([x for r, x in zip(roots, labels) if r not in frame] == original_labels, + 'original caller label convention') + live_mask = sum(1 << i for i, r in enumerate(roots) if r in live) + require(live_mask.bit_count() == 112 and live == sorted(live), 'literal P112 frame') + require(all(sum(r[i] * r[j] for r in live) == 112 * (i == j) + for i in range(8) for j in range(8)), 'evaluation Gram') + return roots, labels, coordinates, live_mask + + +def annihilators(n, dimension): + """Unique reduced row-echelon annihilators, highest pivot convention.""" + for pivots in combinations(range(n), n - dimension): + choices = [] + for pivot in pivots: + free = [j for j in range(pivot) if j not in pivots] + choices.append([(1 << pivot) | sum(((c >> k) & 1) << j + for k, j in enumerate(free)) for c in range(1 << len(free))]) + yield from product(*choices) + + +def kernels(labels, ambient): + locations = {x: i for i, x in enumerate(span(ambient))} + inside = [(i, locations[x]) for i, x in enumerate(labels) if x in locations] + return [sum(1 << i for i, x in inside if (h & x).bit_count() % 2 == 0) + for h in range(1 << len(ambient))] + + +def masks(ker, rows): + for annihilator in rows: + mask = ker[0] + for h in annihilator: + mask &= ker[h] + yield mask diff --git a/research/p112-common30-span/test_controls.py b/research/p112-common30-span/test_controls.py new file mode 100644 index 0000000000..50a1da4cdf --- /dev/null +++ b/research/p112-common30-span/test_controls.py @@ -0,0 +1,93 @@ +#!/usr/bin/env python3 +"""Small exhaustive graph oracle, literal witnesses, and optimized CLI failures. +Chris R / Clear1nsight with substantial OpenAI Codex assistance; Apache-2.0. +""" +from itertools import combinations +import json +from pathlib import Path +import shutil +import subprocess +import sys +import tempfile +HERE = Path(__file__).resolve().parent +sys.path.insert(0,str(HERE)) +import verify as v +import independent as other + + +def rejected(call,message): + try: + call() + except ValueError: + return + raise ValueError('missing rejection: '+message) + + +def run(): + payloads = v.authenticate() + roots,labels,coords,live = v.m.reconstruct(payloads[v.TABLE],payloads[v.GEOMETRY]) + result = v.load((HERE/'RESULT.json').read_bytes()) + witness = result['attaining_triple'] + cut = set(witness['cut_labels']) + normals = witness['normals'] + gram = [[v.m.dot(a,b) for b in normals] for a in normals] + v.m.require(len(cut)==30 and other.determinant(gram)>0, 'literal independent triple') + for h in normals: + residual = [labels[i] for i,r in enumerate(roots) if live>>i&1 and labels[i] not in cut and v.m.dot(r,h)] + v.m.require(len(v.m.basis(residual))==7, 'literal triple residual ranks') + # Every graph on five directions in a rank-three rational space. Compare + # DFS against direct subsets having independent proper prefixes. + vectors = [(1,0,0,0,0,0,0,0),(0,1,0,0,0,0,0,0),(1,1,0,0,0,0,0,0), + (0,0,1,0,0,0,0,0),(1,0,1,0,0,0,0,0)] + pairs = list(combinations(range(5),2)); checked = 0 + for bits in range(1<>bit&1:adjacent[i].add(j);adjacent[j].add(i) + oracle = {} + for n in range(1,6): + for chosen in combinations(range(5),n): + if not all(j in adjacent[i] for i,j in combinations(chosen,2)): + continue + if n>1 and v.rank_q([vectors[i] for i in chosen[:-1]])>i&1] + v.m.require(any(values) and all(x%2==0 for x in values),'characteristic-two boundary') + for kind in ['source','manifest']: + with tempfile.TemporaryDirectory(prefix='p112-common30-control-') as temporary: + root=Path(temporary);package=root/'research'/HERE.name + shutil.copytree(HERE,package,ignore=shutil.ignore_patterns('__pycache__')) + for owned in package.rglob('*'): + if owned.is_file():owned.chmod(owned.stat().st_mode|0o200) + for row in v.load((HERE/'SOURCES.json').read_bytes())['files']: + if row['usage']=='input': + target=root/row['path'];target.parent.mkdir(parents=True,exist_ok=True) + target.write_bytes(payloads[row['path']]) + if kind=='source': + target=root/v.TABLE; expected='source SHA256' + else: + target=package/'SOURCES.json'; expected='source manifest identity' + target.write_bytes(target.read_bytes()+b'\n') + done=subprocess.run([sys.executable,'-I','-O','-Werror','-B',str(package/'verify.py')], + cwd=root,capture_output=True,text=True,timeout=30) + v.m.require(done.returncode!=0 and expected in done.stderr,'actual optimized CLI '+kind) + print(f'PASS_COMMON30_CONTROLS graph_oracles={checked} literal_rank3=1 fourth_rank_rejection=1 optimized_CLI_rejections=2') + + +if __name__=='__main__': + v.m.require(not sys.argv[1:],'no arguments accepted') + run() diff --git a/research/p112-common30-span/verify.py b/research/p112-common30-span/verify.py new file mode 100644 index 0000000000..f6b1c79400 --- /dev/null +++ b/research/p112-common30-span/verify.py @@ -0,0 +1,213 @@ +#!/usr/bin/env python3 +"""Common30 rank-seven span theorem and literal C5 caller. + +Chris R / Clear1nsight with substantial OpenAI Codex assistance; Apache-2.0. +Credit Nick Petalas, DreamingOfClouds/3154, David Arias and E8/P112 lineage. +""" +from collections import Counter +import hashlib +from itertools import combinations +import json +from pathlib import Path +import sys + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +sys.path.insert(0, str(HERE)) +import model as m + +MANIFEST_SHA = '4d49389e8131d6ec139722f60e12d697e4d0d31eba205b5e6d11543d22b4afd3' +TABLE = 'research/one-sided-six-multisets/data/data.txt' +GEOMETRY = 'research/p112-root-simplex-exclusion/geometry.py' +FILTER = 'research/p112-b6-t4-reconciliation/vendor/bk2b.py' + + +def unique(pairs): + m.require(len(pairs) == len({k for k, _ in pairs}), 'duplicate JSON key') + return dict(pairs) + + +def load(raw): + return json.loads(raw, object_pairs_hook=unique) + + +def digest(value): + return hashlib.sha256(json.dumps(value, sort_keys=True, separators=(',', ':')).encode()).hexdigest() + + +def histogram(values): + return {str(k): n for k, n in sorted(Counter(values).items())} + + +def authenticate(root=ROOT, package=HERE): + raw = (package / 'SOURCES.json').read_bytes() + m.require(hashlib.sha256(raw).hexdigest() == MANIFEST_SHA, 'source manifest identity') + result = {} + for row in load(raw)['files']: + if row['usage'] != 'input': + continue + path = root / row['path'] + m.require(path.resolve().is_relative_to(root.resolve()), 'input escaped root') + m.require(not any(p.is_symlink() for p in [path, *path.parents]), 'input symlink') + data = path.read_bytes() + m.require(len(data) <= 2_000_000, 'source size limit') + m.require(hashlib.sha256(data).hexdigest() == row['sha256'], 'source SHA256') + m.require(hashlib.sha1(b'blob '+str(len(data)).encode()+b'\0'+data).hexdigest() + == row['git_blob'], 'source Git blob') + result[row['path']] = data + return result + + +def chamber(roots, coordinates): + signed = set(roots) | {tuple(-x for x in r) for r in roots} + for alpha in m.SIMPLE: + for r in signed: + p = m.dot(alpha, r) + m.require(p % 4 == 0, 'reflection integrality') + m.require(tuple(x-p//4*y for x, y in zip(r, alpha)) in signed, + 'signed reflection closure') + rho = m.solve(m.SIMPLE, [[1]*8])[0] + m.require(all(m.dot(rho, a) == 1 for a in m.SIMPLE), 'strict chamber functional') + faces = [[r for r, c in zip(roots, coordinates) if all(c[j] == 0 for j in range(8) + if not mask >> j & 1)] for mask in range(256)] + cap6 = max(len(faces[x]) for x in range(256) if x.bit_count() <= 6) + seven = [len(faces[255 ^ (1 << j)]) for j in range(8)] + m.require(cap6 == 36 and seven == [42,28,22,14,16,23,37,63], 'face bounds') + normal = [r for r in roots if all(m.dot(r, z) == 0 for z in faces[127])] + m.require(len(normal) == 1, 'E7 root normal') + return {'signed_reflections': 1920, 'rho': [str(x) for x in rho], + 'rank6_face_maximum': cap6, 'seven_node_counts': seven, + 'E7_normal': normal[0]} + + + +def rank_q(rows): + from fractions import Fraction + a = [[Fraction(x) for x in row] for row in rows] + rank = 0 + for j in range(8): + pivot = next((i for i in range(rank,len(a)) if a[i][j]),None) + if pivot is None: + continue + a[rank],a[pivot] = a[pivot],a[rank] + scale = a[rank][j] + a[rank] = [x/scale for x in a[rank]] + for i in range(rank+1,len(a)): + scale = a[i][j] + a[i] = [x-scale*y for x,y in zip(a[i],a[rank])] + rank += 1 + return rank + + +def completion_records(roots,live,flats): + records = [] + for a,h in enumerate(roots): + word = sum(1<>i&1 and m.dot(r,h)) + m.require(word.bit_count() == (53 if live>>a&1 else 56), 'root support') + for flat in flats: + cut = word & ~flat + if cut.bit_count() <= 30: + records.append((a,flat,cut)) + return sorted(records) + + +def compatible_graph(nodes): + adjacent = [set() for _ in nodes] + edges = [] + owners = [a for a,c in nodes] + cuts = [c for a,c in nodes] + for i,(owner,cut) in enumerate(nodes): + for j in (j for j in range(i) if owner != owners[j] + and (cut|cuts[j]).bit_count() <= 30): + adjacent[i].add(j) + adjacent[j].add(i) + edges.append((j,i)) + return adjacent,sorted(edges) + + +def independent_prefixes(roots,nodes,adjacent): + counts = Counter() + maximum = 0 + witness = None + def visit(chosen,union,candidates): + nonlocal maximum,witness + if chosen: + rank = rank_q([roots[nodes[i][0]] for i in chosen]) + counts[(len(chosen),union.bit_count(),rank)] += 1 + if rank > maximum: + maximum,witness = rank,(chosen,union) + if rank < len(chosen): + return + for i in sorted(candidates): + joined = union | nodes[i][1] + if joined.bit_count() <= 30: + visit(chosen+[i],joined,{j for j in candidates & adjacent[i] if j>i}) + visit([],0,set(range(len(nodes)))) + m.require(maximum == 3, 'common30 span bound and attainment') + m.require(all(size==30 for (n,size,rank) in counts if n>=3), 'common29 at most two directions') + return counts,witness + + +def literal_caller(payloads): + import ast + weights = (2,2,2,2,2,6,7,7,7,7,7) + tree = ast.parse(payloads[FILTER]) + nodes = [n for n in tree.body if isinstance(n,(ast.ImportFrom,ast.Assign,ast.FunctionDef))] + namespace = {} + exec(compile(ast.Module(body=nodes,type_ignores=[]),'','exec'),namespace) + m.require(namespace['feasible'](weights,5) and not namespace['killed'](weights,5), + 'literal historical survivor') + capacity = {2:2,6:20,7:36} + sums = [sum(capacity[weights[i]] for i in chosen) for chosen in combinations(range(11),6)] + m.require(min(sums)==30 and sums.count(30)==1, 'six-piece capacity minimum') + m.require(sum(w-2 for w in weights)==29, 'strict excess') + return {'weights':weights,'b':5,'t':6,'required_intersection_dimension':5, + 'quotient_dimension':6,'minimum_six_piece_capacity_sum':30, + 'minimum_basis_choices':1,'six_piece_subsets':len(sums),'strict_excess_deficit':1, + 'required_independent_directions':5,'uniform_available_span_dimension':3} + + +def compute(): + payloads = authenticate() + roots,labels,coordinates,live = m.reconstruct(payloads[TABLE],payloads[GEOMETRY]) + kernel = m.kernels(labels,[1<>i&1 and not cut>>i&1 and m.dot(r,normal)] + m.require(len(m.basis(residual))==7, 'attaining triple residual rank') + return {'spaces7':len(flats),'flat_inventory_digest':digest(sorted(Counter(flats).items())), + 'maximum_rank7_trace':36,'spaces6':six_count,'maximum_rank6_trace':six_max, + 'chamber':chamber(roots,coordinates),'critical_records':len(records), + 'critical_record_digest':digest(records),'nodes':len(nodes),'node_digest':digest(nodes), + 'cut_size_histogram':histogram(c.bit_count() for a,c in nodes), + 'edges':len(edges),'edge_digest':digest(edges), + 'prefix_histogram':[[list(k),v] for k,v in sorted(counts.items())], + 'maximum_span_common30':3,'maximum_directions_common29':2, + 'attaining_triple':{'normal_indices':[nodes[i][0] for i in indices], + 'normals':normals,'cut_labels':[label for i,label in enumerate(labels) if cut>>i&1]}, + 'caller':literal_caller(payloads)} + + +def main(): + m.require(not sys.argv[1:], 'no arguments accepted') + observed = compute() + expected = load((HERE/'RESULT.json').read_bytes()) + m.require(json.dumps(observed,sort_keys=True)==json.dumps(expected,sort_keys=True), 'result receipt mismatch') + print('PASS_COMMON30_SPAN nodes=24264 edges=9828 maximum_span=3 common29_directions=2 caller=2^5,6,7^5 excluded') + + +if __name__ == '__main__': + main()