diff --git a/research/e8-d0-root-swaps/EXTENSION.md b/research/e8-d0-root-swaps/EXTENSION.md new file mode 100644 index 0000000000..99dc1c21b7 --- /dev/null +++ b/research/e8-d0-root-swaps/EXTENSION.md @@ -0,0 +1,383 @@ +# A cost-seven extension and a C1 subcase + +Prepared by **conorholds** with substantial OpenAI Codex assistance. +Use the characteristic-zero model, labels, binary weight and cost in +[PROOF.md](PROOF.md). This note strengthens its restricted root-only filter +and closes one precise subcase of DreamingOfClouds' +[PR3154](https://github.com/CrocSwap/integer-mult-bounds/pull/3154), +`checks/CONJG2/NOTES.md` Section 2 and `checks/CONJ-G/NOTES.md` Section 0. +It does not close C1 in full. The registered replay regenerates the finite +geometry below in two coordinate models: [extension_check.py](extension_check.py) +checks the new cost-seven data and fixtures; the primary geometry checkers +retain the norm-six, A2 and full-root-remainder tables from PROOF.md. +The C1 decoder consequences assume PR3154's d=0 rigid shape, corrected +ledger identity `cost(D') = sum_j w(A_j) - n_c`, pivot rebate +`epsilon_k in {0,1}`, and N8 (at most eight corrections with distinct +corrected frame indices). This package does not validate that broader +reduction. The geometric Theorems C and E have their own stated hypotheses. + +## 1. Root-only filter at cost seven + +**Theorem C.** Let U be a subspace of K^P with dimension at least two and +cost(U) at most seven. If h is nonzero and + + w(p_h|P + tau) <= 8, tau in U, + +then h is proportional to an E8 root, possibly a frame root. + +In particular, applying C with U=T in PR3154's d=0 rigid shape resolves +CONJG2 Section 2(ii) for every minimum correction cost kappa<=7: no +weight-eight high member has a nonroot D7/E6-type normal. This is independent +of the actual low-basis total Sigma. It makes no assertion for kappa=8 or +about the remaining invoice and coefficient obligations. + +Choose a minimum-weight basis q_1,...,q_a, with weights w_j and total k<=7. +Every w_j is positive, a>=2, and hence every w_j<=6. The cap bounds in +PROOF.md imply that the union B of their supports has at most 21 points: +the largest permitted profile is (6,1). Its binary label rank is at most k. +Choose a binary hyperplane H containing the corrected support. Then + + D = Off_P(h) minus H is contained in B, + |D| <= 21, rank(D) <= 7, |Off_P(h)| <= 64+21 = 85. + +Thus at least 27 full E8 root lines are perpendicular to h. The parabolic +argument of PROOF.md Section 4, including its transfer of rational support +patterns to any characteristic-zero field, applies at threshold 27. The +same six proper types qualify: D6, E6, A7, E6+A1, D7 and E7. As before, +their possible nonroot normals reduce to norm-four, norm-six and primitive +norm-eight directions, A2 normal planes, and orthogonal-root normal planes. + +The old tables exclude the norm-six and A2 families by deletion cardinality +at least 24. Their full-E8 Off sizes are respectively 83 and 84, so +restriction to P cannot add any Off-85 rows for either family. Raising the +Off cutoff from 84 to 85 adds exactly these rows: + +| Family | Off size | Minimum deletion | Number | +|---|---:|---:|---:| +| Primitive norm-eight directions | 85 | 25 | 3,584 | +| Orthogonal-root normal planes | 85 | 25 | 448 | + +The earlier rows of these two families also have minimum deletion at least +24. For all 1,080 norm-four directions and all 511 binary hyperplanes, +the complete inventory with deletion size at most 21 is: + +| Deletion size | Binary rank | Number of normal/hyperplane pairs | +|---:|---:|---:| +| 12 | 7 | 56 | +| 13 | 8 | 896 | +| 14 | 8 | 128 | + +Only the first row could meet the correction budget. Its 56 normals are +exactly the lines f_i+f_j and f_i-f_j for distinct frame vectors. For each, +D consists of six disjoint pairs of root labels with a common nonzero XOR. +The union of any two pairs is a four-element binary circuit: the total XOR +is zero, distinct labels exclude two-element dependencies, and their common +first coordinate 1 excludes odd dependencies. These circuits connect every +element of D. Consequently its rank-seven binary matroid is connected: +every nontrivial bipartition D=A union A' satisfies + + rank(A) + rank(A') >= 8. + +This follows directly from the circuit definition of matroid connectedness; +alternatively, a rank-additive partition splits the two spans into a direct +sum, so every circuit would lie wholly in one part, contradicting the +pair-union circuits. Both coordinate implementations check the six-pair +certificate for all 56 configurations. An additional private independent +probe checked all 4,094 nontrivial subsets of each configuration. + +Here is the coefficient-independent covering step, which allows arbitrary +overlap of correction supports. Assign each point of D to one basis member +whose support contains it, producing parts D_j. If there is only one +nonempty part, that basis member has weight at least seven and another +positive-weight member exists, contradicting k<=7. Otherwise select one +nonempty proper part D_i. Connectedness and rank subadditivity give + + 8 <= rank(D_i) + rank(D minus D_i) + <= sum_j rank(D_j) <= sum_j w_j <= 7, + +again a contradiction. This excludes the last nonroot case and proves C. + +## 2. Two sharp boundary examples + +The dimension hypothesis in C is essential. In ordinary norm-two root +coordinates take + + h = (1,1,1,1,0,0,0,0), + H = {labels r : 1+(h,r) = 0 modulo 2}, + tau(r) = -p_h(r) outside H, and 0 inside H, on P. + +Its twelve nonzero entries have label rank seven, so U=span(tau) has +dimension one and cost seven. The corrected support has weight eight and +h is nonroot. Every deleted coordinate is essential, and this H contains +no frame labels. The registered check records literal coefficients and an +eight-label basis of the corrected support. There are no eligible exact +root swaps in this fixture; it does not contradict Theorem A or C7. + +Nor can the cost bound be raised to eight, even for carrying members. Take + + h = (1,1,1,0,1,0,0,0), u = e3+e5, + D = {r in P : |(h,r)|=2}, + q0 = -p_h on D minus {u}, and zero elsewhere, + U = span(q0, delta_u), tau = q0-2 delta_u. + +Here |D|=13, rank(D)=8, rank(D minus {u})=7, and U has profile (7,1). +The corrected support has weight eight and its actual label span contains +four frame labels, those for e3+e4, e3-e4, e5+e6 and e5-e6. The minimum +cost is exactly eight: it is at most eight by the displayed basis, while +the union of supports has binary rank eight, a lower bound on every basis +weight sum. This is a boundary example for the +root-only lemma, not a complete decoder or a counterexample to C1. + +## 3. Four corrected weight-eight root directions + +Retain the d=0 rigid basis shape in PR3154 CONJG2 Section 2. There is a +low basis F_T of T, dim(T) in {2,3}, and eight high members +q_l=p_{h_l}+tau_l of weights eight or nine. Their h_l form a basis of K^8. +The row functional dual to h_l is denoted mu_l. A corrected high member +has mu_l proportional to some frame functional f_j, and its support-label +span contains that frame label z_j. The frame indices of corrected members +are distinct, as in the source's normalization/Lemma D. + +Suppose cost(T)<=7. Theorem C forces every **weight-eight** high direction +to be a root. No claim about weight-nine directions is needed. A frame-root +direction cannot be corrected: every tau in T has support contained in +the union B of the chosen basis supports, of size at most 21. Hence the +56-point P support of its codeword +retains its rank-eight span W_j after at most 21 deletions, since the full +root-remainder minimum deletion is 24. Thus a corrected support of rank +eight has span W_j, which contains no frame labels. + +For m corrected weight-eight members their nonframe root directions r_i +therefore have distinct matched frame indices j_i, with + + (r_i,f_j_i) != 0, (r_i,f_j_s) = 0 for s != i. + +Every nonframe E8 root has exactly four nonzero frame pairings, all +/-1: +the squared pairings sum to four. Any two such four-element incidence +supports have even intersection, since their inner product is one half +the signed sum on the intersection and is integral. + +If m>=6, each root would have to use its own matched index and at least +three of at most two unmatched indices, impossible. If m=5, each must use +all three unmatched indices, so two incidence supports intersect in three +places, also impossible. Hence m<=4. The finite check supplies a sharp +four-index matching. The exclusion of frame roots is necessary: allowing +them admits eight private matched indices. + +## 4. A complete C1 subcase, with one unit of slack + +**Corollary D.** In the preceding d=0 shape, suppose the actual low basis +has total weight + + Sigma = sum_{q in F_T} w(q) = 7. + +Then the corrected one-sided invoice is at least 65, and the pivot invoice +in PR3154's Conjecture G is at least 64. + +Indeed cost(T)<=7 and dim(T)>=2. Let n_T count corrected low members, +n_8 corrected weight-eight high members, c_9 all weight-nine high members, +and c_9,corr their corrected subset. A low member carrying an excluded +frame label has weight at least three: a binary span of rank at most two +contains no first-coordinate-one label other than its generating root +labels. Thus n_T<=2. Section 3 gives n_8<=4, while c_9,corr<=c_9, so + + n_c = n_T+n_8+c_9,corr <= 6+c_9. + +The exact source invoice is the raw weight minus one for each corrected +member; its possible pivot rebate epsilon_k is either zero or one. Hence + + corrected invoice >= 64+Sigma+c_9-n_c >= 65, + pivot invoice >= 65-epsilon_k >= 64. + +The same proof also covers actual Sigma=8 if cost(T)<=7: the corrected +invoice is then at least 66 and the pivot invoice at least 65. The support +bound uses a minimum basis of T, while n_T<=2 uses the actual basis total; +these are distinct quantities. No such conclusion is claimed for cost(T)=8. + +This settles every pivot choice in the stated Sigma=7 subcase. It uses +neither F1 nor the unfinished T_v coefficient step, and it does not assume +an actual-swap conversion on the P112 remainder at union size 21. + +## 5. A sharp F1 support threshold + +The F1 condition in PR3154 CONJ-G Section 1 asks whether vanishing on +O_v forces the normal direction to be v; write O_v for its O_{l_v}. +The source does not explicitly define O_v in its prose. Its identity +`Off(c_v) intersect O_v = {v}` together with +`N(v) = Off(c_v) minus {v} = P minus O_v` +([CONJ-G notes, lines 21 and 39](https://github.com/CrocSwap/integer-mult-bounds/blob/708f0ad8928c383de8294aea3c126e9461d2066d/research/p112-reduction-to-conjectures/checks/CONJ-G/NOTES.md#L21), +[f1.py, lines 2 and 10-12](https://github.com/CrocSwap/integer-mult-bounds/blob/708f0ad8928c383de8294aea3c126e9461d2066d/research/p112-reduction-to-conjectures/checks/CONJ-G/f1.py#L2)) +determines the set used here. Since `Off(c_v) = {r in P : (r,v)!=0}`, +for a nonframe root v it is + + O_v = {r in P : (r,v)=0} union {v}. + +This set has 60 elements; its complement in P has 52, matching the source +checker's assertions. The registered replay constructs and checks it afresh. + +**Theorem E.** If h is nonzero, |supp(tau)|<=24, and p_h|P+tau vanishes +on O_v, then h is proportional to v. The number 24 is sharp. + +The cancellation condition gives + + |Off_P(h)| <= 52+24 = 76. + +Thus at least 120-(76+8)=36 full root lines are perpendicular to h. Exactly four +proper parabolic types qualify: E7, D7, E6+A1 and E6, with respectively +63, 42, 37 and 36 root lines. The same support-pattern/field argument as +in PROOF.md reduces h to root directions, norm-four or norm-six directions, +or a generic A2 normal plane. Norm-six directions have Off_P at least 77 +and generic A2 planes at least 78, so both are excluded by cardinality. +The check also enumerates norm-six directions with Off_P=77 to establish +the sharp boundary below. + +The two coordinate implementations regenerate the following minima for +the required cancellation support Off_P(h) intersect O_v: + +| Direction | Minimum support | Coverage | +|---|---:|---| +| Root other than v, including frame roots | 26 | All 112 pivots and 119 other root lines | +| Norm four | 30 | All 112 pivots and 1,080 normal lines | +| Norm six with Off_P<=77 | 25 | All 112 pivots and 2,688 normal lines | + +Every direction except v therefore needs more than 24 cancellations. +This proves E for any characteristic-zero field. The registered fixture +records the nonroot norm-six normal h=(0,0,0,1,-2,0,-1,0), pivot +v=(0,0,0,1,0,0,1,0), and all 25 literal coefficients +tau=-p_h on Off_P(h) intersect O_v. Their corrected word vanishes on O_v, +so replacing 24 by 25 would be false. This is an actual failure of the F1 +extension, not a decoder counterexample. + +This tau has weight seven. Choose the unit delta_u at the first listed +nonzero coordinate u. The other 24 coordinates still have binary rank +seven. Therefore U=span(tau,delta_u) has dimension two and exact cost eight: +every vector outside the unit line retains those 24 nonzero coordinates +and has weight at least seven; every basis pays at least 7+1. The same g +violates unrestricted F1 in this (7,1) correction space. This does not +construct an admissible complete C1 decoder or its high basis. In this +fixture (h,v)=0, so the extra nonzero evaluation condition in CONJ-G +Section 2 case (A) is absent; pivot-aware replacements remain possible. + +As a consequence, F1 holds for every tau in a correction space of dimension +at least two and cost at most seven (support union at most 21). It also +holds for every correction space of dimension three and cost at most eight: +the cap table bounds its union support by 22, attained by profile (6,1,1). +Thus the entire F1 step for C1's d=0, dim(T)=3 rigid branch is discharged. +This does not settle its other swap/carrier or coefficient conditions. For +dim(T)=2 and cost eight, profile (7,1) can have support 37; no complete F1 +claim is made for that remaining case. + +## 6. The cost-eight (7,1) invoice branch + +**Theorem F.** In the d=0 rigid shape of Section 3, suppose the actual +low-basis total is eight and T admits a minimum basis with weights (7,1). +Then the corrected invoice is at least 65 and the pivot invoice at least 64. +This includes the minimum profile of the F1 counterexample in Section 5; +it does not require the false unrestricted F1 implication there. + +Let delta_u generate the unit line in a minimum (7,1) basis. Every vector +of T outside that line has weight at least seven: a vector of smaller +weight together with delta_u would contradict cost(T)=8. Therefore an +actual basis of total eight also has profile (7,1). At most one low member +can be corrected, because a unit cannot carry an excluded frame label. +The full support B of T has at most 36+1=37 coordinates by the cap table. + +Suppose the corrected invoice were at most 64. Its raw value is 72+c_9, +and normalization gives n_c<=8. Hence c_9=0 and n_c=8: all eight high +members have weight eight and at least seven of them are corrected. Let J +be their distinct matched frame indices. If |J|=8, each high direction is +its own frame direction. If |J|=7, let k be the unused frame index. Duality +forces each corrected high direction with matched index j to lie in +span(f_j,f_k), with nonzero f_j coefficient. + +The Off_P patterns in this plane are exhausted by f_j, f_j+f_k, f_j-f_k, +and a generic f_j+2f_k. Indeed nonframe-root frame pairings are 0 or +/-1, +so the only cancellation ratios with both coefficients nonzero are +/-1. +This classification holds over every characteristic-zero field. + +For each of the 56 ordered frame pairs and each of the 255 binary +hyperplanes H containing z_j, the registered check forms + + D = Off_P(h) minus H. + +For each of the three nonframe strata, all 14,280 cases have rank(D)=8 +and no coloops: removing any one label still leaves rank eight. But any +correction in a (7,1) space has the form alpha*a+beta*delta_u for a +weight-seven word a. Cancellation outside H requires +`D subset supp(alpha*a+beta*delta_u) subset supp(a) union {u}`. +Thus D minus {u} has rank at most seven, a contradiction. Only the frame +stratum can survive. Its genuine survivors are retained as positive controls; +the proof does not exclude +frame directions using this rank test. + +There are therefore at least seven corrected high members whose normal +directions are their own distinct frame directions. Each frame codeword's +56 nonzero P coordinates span W_j, which contains no frame labels. A +corrected member's hyperplane H contains z_j and differs from W_j, so +at least 24 of those original coordinates must be canceled, by the full +root-remainder bound. Every canceled coordinate lies in B. + +Every nonframe root has nonzero pairing with exactly four frame vectors. +Summing the necessary cancellations over the seven corrected frames gives + + 7*24 = 168 <= sum_{r in B} number of selected frames nonorthogonal to r + <= 4*|B| <= 4*37 = 148, + +impossible. The corrected invoice, an integer, is at least 65; subtracting +the possible unit pivot rebate leaves at least 64. + +Both coordinate models check all plane patterns and hyperplanes. The fast +no-coloop test performs binary elimination while retaining dependence +masks: its nullspace-basis supports cover every point exactly when there +is no coloop. Selected cases are compared directly with every one-point +deletion rank; a separate private implementation independently checked every one-point +deletion in all 42,840 nonframe cases. Frame positive controls are retained +by the registered check. + +This closes only the minimum (7,1) profile at actual total eight. Minimum +profiles (6,2), (5,3), (4,4), other dimensions and the other C1 cases require +separate arguments. Section 5's component counterexample remains valid; +the aggregate invoice obstruction excludes the full decoder branch. + +**Residual F1 corollary.** The entire F1 obligation in PR3154 CONJG2 +Section 2(iii) is discharged for surviving d=0 rigid-shape candidates with +corrected invoice at most 64. The source reduction gives kappa=cost(T) +<=Sigma<=8. If kappa<=7, the support union is at most 21. If kappa=8 and +dim(T)=3, it is at most 22. At kappa=8 and dim(T)=2, the complete minimum +profiles are (7,1), (6,2), (5,3) and (4,4). The first forces actual Sigma=8 +and is excluded by F; the other three have union caps 22, 16 and 16. +Every remaining case therefore satisfies E. This is a proof for the +surviving low-invoice candidates, not an unrestricted F1 statement about +the eliminated (7,1) spaces. The other C1 inequalities and coefficient +obligations remain open. + +## 7. What remains open and what Lean checks + +C7 is proved in PROOF.md. Under the inherited rigid-shape assumptions, +Theorem C settles CONJG2 Section 2(ii) for kappa<=7. The exact C1 invoice +cases of Corollary D and Theorem F, and the residual F1 obligation from E/F, +are discharged here. Other C1 cases and C2-C6 remain outside this package's +closure claim. In particular the +cost-eight carrying example prevents simply extrapolating Theorem C. +Other basis totals and C1's coefficient/pivot conditions require further +arguments; the new lemma is not a complete L120 or multiplication proof. + +Two Lean files check separate parts of Theorem A, with actual coefficient +witnesses: [RootSwapOneExceptional.lean](formal/RootSwapOneExceptional.lean) +proves the generating-family rank bound under explicit pairing hypotheses +when every member except a distinguished one has root-support rank at most +label-support rank; [RootSwapQuartet.lean](formal/RootSwapQuartet.lean) proves the +low-overlap two-quartet/singleton case. +[RootSwapConnectedCover.lean](formal/RootSwapConnectedCover.lean) additionally +proves Section 1's generic rank-cover contradiction, with actual label-span +ranks and overlapping supports, assuming the connectedness inequality. +All three were compiled with the +repository's Lean/mathlib v4.21.0 pins, with no warnings, sorry, custom +axioms or unsafe declarations. Their printed axioms are only propext, +Classical.choice and Quot.sound. + +These are partial formalizations: the E8/label instantiation and +characteristic-zero rank bridges, exceptional-support classification, +two-factor lemma, high-overlap quartet bound, finite geometry and final +greedy C7 assembly remain written proofs and executable finite checks. +Theorems C/E/F and Corollary D are not complete Lean formalizations. diff --git a/research/e8-d0-root-swaps/PROOF.md b/research/e8-d0-root-swaps/PROOF.md new file mode 100644 index 0000000000..79051f9f43 --- /dev/null +++ b/research/e8-d0-root-swaps/PROOF.md @@ -0,0 +1,348 @@ +# A root-swap rank bound and the remaining d=0 kernel case + +This is a characteristic-zero theorem in the one-sided E8 lift model of +[PR2816](https://github.com/CrocSwap/integer-mult-bounds/pull/2816). +It closes the `d=0`, `ker(rho) intersect S != 0` branch listed as open in +[PR3074](https://github.com/CrocSwap/integer-mult-bounds/pull/3074). +The subsequent [PR3154](https://github.com/CrocSwap/integer-mult-bounds/pull/3154) +names this same obligation C7; its other reductions are not premises here. +It does not prove L120 for the other branches, the two-sided decoder floor, +a supplier construction, or a multiplication-exponent improvement. + +The proof separates a uniform, coefficient-preserving rank argument from +finite geometric inputs. The latter are recomputed by two implementations. +Exact predecessor versions and their roles are recorded in `SOURCES.json`. + +## 1. Model and statements + +Let Lambda be the even unimodular E8 lattice, with roots of squared norm 2. +Let E be its 120 unoriented root lines, with one root r_t chosen on each line. +Put V = Lambda/2Lambda, Q(x) = (x,x)/2 mod 2, and + + label(t) = (1, r_t mod 2) in F2 direct-sum V. + beta((a,x),(b,y)) = ab + (x,y) mod 2. + +Signs do not change labels or any support in this note. The 120 root classes +are exactly Q^{-1}(1). For distinct root lines, + + beta(label(s),label(t)) = 0 iff (r_s,r_t) != 0; + beta(label(t),label(t)) = 1. + +Fix the orthogonal frame F consisting of e1+e2, e3+e4, e5+e6, e7+e8, +e1-e2, e3-e4, e5-e6, e7-e8, in that order. This is the frame in PR2816. +Choose these displayed roots as the representatives on the frame lines. +Write P = E minus F, and rho for restriction from E to P. +For a vector v with coefficients in a characteristic-zero field K define + + w(v) = rank_F2 {label(t): v(t) != 0}, with w(0) = 0; + cost(L) = min over K-bases B of L of sum_{b in B} w(b). + +The code C_E is {p_h : h in K^8}, where p_h(t) = (r_t,h). +Its restriction is C_P. Each code has dimension eight. Real ranks of sets +of roots equal their ranks over K, because the root coordinates are rational. + +A root t is **swap-eligible for L** if there is tau in L such that + + tau(t) != 0, + supp(tau) subset {t} union {s: (r_s,r_t) != 0}. + +The root t itself is permitted in this support condition. All *other* +orthogonal coordinates must vanish. Denote the eligible root set by R(L). + +**Theorem A (weighted root-swap bound).** For every K-subspace L of K^E, + + rank_K {r_t: t in R(L)} <= cost(L). + +**Theorem B (the d=0 kernel branch).** Let S contain C_E. Set + + T = (rho S)_{<=7}, + d = dim_K(C_P intersect T), + Z = ker(rho) intersect S. + +Here a subscript <=7 means the span of all vectors of weight at most seven, +not the set of such vectors. If d=0 and Z is nonzero, then cost(S) >= 72. +The bound is sharp in this branch: S=C_E+span(delta_f), for any frame root f, +has a basis delta_f, p_f-2delta_f and seven other frame codewords, of weights +1, 8 and seven times 9. Its restricted code is C_P, so d=0, and its kernel +contains delta_f. + +## 2. A two-factor lemma, with its field scope made explicit + +We use [PR1590, Lemma A](https://github.com/CrocSwap/integer-mult-bounds/pull/1590). +Its published proof is stated over Q. The same proof works over any field: +arbitrarily order the finite set of ratio values appearing below. No order +compatible with field addition or multiplication is needed. + +Let M = p1 q1^T + p2 q2^T have nonzero diagonal on a finite index set I. +Let B be a binary matrix with diagonal one, such that B_st=1 for s!=t +implies M_st=0. Put R_j=supp(pj), A_j=supp(qj), and +r_j=rank_F2 B[R_j,A_j]. Then r_1+r_2 >= |I|. + +For completeness, put D_j=R_j intersect A_j, X=D_1 intersect D_2, and +P_j=D_j minus X. Every index belongs to D_1 union D_2. A private index +in P_j supplies a unit row or unit column in B[R_j,A_j], because its +other-factor diagonal product is zero. Peeling these pivots leaves a block +containing B[X,X], so r_j >= |P_j| + rank B[X,X]. + +On X all four factors are nonzero. Set alpha(t)=p1(t)/p2(t) and +eta(t)=-q2(t)/q1(t). Then M_ts=0 iff alpha(t)=eta(s), while +alpha(t)!=eta(t). Choose any total order on the finite union of these +values and partition X into alphaeta. On either part, +the equality alpha(t)=eta(s) for B_ts=1 gives a strict order in one +direction. Ordering by alpha on the first part and eta on the second +makes the corresponding principal block unit triangular. Thus +rank B[X,X] >= max(|X_<|,|X_>|) >= |X|/2. Summing proves the assertion. +Zero factors include the one-factor case. + +In particular, if dim L<=2, take any finite eligible set I and choose its +actual witnesses tau_t in L. Normalize tau_t(t)=1, and form M_st=tau_t(s) +for s,t in I. Its diagonal is one and its entries on orthogonal pairs vanish. +With B_st=beta(label(s),label(t)), write tau_t=c1(t)b1+c2(t)b2 +using at most two basis vectors b1,b2 of L, padding with a zero factor +when needed. In the lemma's notation p_j(s)=b_j(s) and q_j(t)=c_j(t). +Each r_j is at most w(b_j): every row of its binary block is obtained +from the corresponding root label by the same linear map. Hence + + |I| <= w(b1)+w(b2). + +This uses the same coefficient space L for every witness. Replacing L by +all vectors supported on its union support would not justify this step. + +## 3. Proof of Theorem A + +Write k=cost(L). If k>=8 the conclusion follows from the ambient root rank +eight. Suppose k<=7 and choose a minimizing basis q1,...,qa. +Call a basis member exceptional when + + rank_K {r_t: t in supp(qj)} > w(qj). + +**At most one exceptional member.** Let O be the K-span of the supports of +all other members, viewed as root vectors. Then +dim O <= sum of their weights. An eligible root outside O has a witness +whose exceptional coefficient is nonzero; outside O that witness is a +nonzero multiple of the same exceptional vector q. Consequently any two +eligible roots outside O are nonorthogonal: evaluating one witness at +the other's coordinate gives a nonzero value. Their labels are beta- +orthonormal, hence independent over F2. Their number is at most w(q). +Therefore rank R(L) <= dim O+w(q) <= k. With no exceptional member the +union-of-spans bound gives the result directly. + +**The smallest exceptional member.** A weight-one or weight-two support +has at most one or two roots, respectively. A weight-three support has +at most four roots, since all labels have first coordinate one. If its +real rank exceeds three, it consists of four independent roots r1,...,r4 +whose labels sum to zero. Thus every signed half-sum + + v_epsilon = (epsilon1 r1 + ... + epsilon4 r4)/2 + +belongs to Lambda. Independence makes all sixteen half-sums nonzero. +Every one therefore has squared norm at least two. Their average squared +norm is exactly two. All sixteen norms equal two; expanding these +identities and taking the pairwise sign coefficients gives (ri,rj)=0 +for i!=j. A weight-three exceptional support is an orthogonal quartet. +This is a lattice argument, independent of the correction coefficients. + +**Two or more exceptional members.** Each costs at least three. With k<=7 +there are at most two, and the only basis profiles containing two are +(3,3), (4,3), and (3,3,1). The first two have dim L=2 and are covered by +Section 2. In the last case let A and B be the two orthogonal quartets; +the weight-one member is a multiple of one coordinate unit delta_u. + +If |A intersect B|>=2, the whole union support has at most 4+4-2+1=7 +roots, so its rank is at most k=7. Otherwise suppose t!=u is eligible. +Its witness uses a quartet containing t with nonzero coefficient. Among its +three other roots, at most one lies in the other quartet +and at most one is u. At least one coordinate therefore remains nonzero +and orthogonal to t, a contradiction. This also covers t in A intersect B: +either nonzero quartet coefficient leaves such a coordinate. Thus only u +can be eligible. These cases exhaust all profiles and prove Theorem A. + +## 4. Geometric inputs and the root-only reduction + +The following finite E8 facts are recomputed from two coordinate models; +they are not read from predecessor PASS receipts. + +1. Every nonzero p_h in C_E has weight nine. Equivalently, for each of the + 511 binary label hyperplanes, its root complement has real rank eight. +2. Maximum numbers of root lines in label flats of dimensions 1,...,8 are + bounded by (1,2,4,8,12,20,36,64). The uniform proof below gives all eight; + the finite checks cover dimensions 1,...,7 and directly enumerate all + 511 label hyperplanes to check the dimension-eight cap of 64 in both models. +3. For each root r, its 56 nonself nonorthogonal root lines span the + binary hyperplane W_r=label(r)^{perp_beta}. Every nonzero binary + character on this remainder has support at least 24. + +The first two facts agree with the retained E8/P112 code facts of PR2816 +and the full-E8 cap calculation in PR2985. The distinction between full +E8 caps and P112 caps matters here. + +Here is also a short proof of the full cap bounds. The quadratic Gauss sum +of Q on V is 16. A label w-flat either misses first-coordinate-one entirely, +or meets it in an affine (w-1)-flat A=x0+U of V. In the latter case Fourier +summation gives + + sum_{x in A} (-1)^Q(x) + = 16/|U^perp| sum_{y in U^perp} (-1)^(Q(y)+(x0,y)). + +A quadratic function with zero constant term on an n-dimensional binary +space has Gauss sum either zero, positive 2^n when its polar rank is zero, +or plus/minus 2^(n-r/2) with even polar rank r>=2. Its negative sum is +therefore no smaller than -2^(n-1). For w=5,6,7 this bounds the displayed +sum below by -8, giving at most 12,20,36 nonsingular points in A. +For w<=4 use the trivial bound 2^(w-1). For w=8 the dual dimension is +one, where the sum cannot be negative, giving at most 64 points. + +**Root-only lemma.** If a correction space U in K^P has cost(U)<=6 and +w(p_h|P+tau)<=8 for some tau in U and nonzero h, then h is proportional +to one of the 120 E8 roots, including the eight frame directions. + +Choose a minimum basis of U. The cap bounds give union support size<=20 +and union label rank<=6. A hyperplane H containing the corrected support +therefore has + + |Off_P(h)| <= 64+20=84, + Off_P(h) minus H subset supp(tau), + rank_F2 labels(Off_P(h) minus H) <= 6. + +Completeness uses the parabolic root-intersection argument of PR2816 C3, +not the RRC census. The roots perpendicular to h contain at least 28 +nonframe lines. Every root intersection with a real subspace is Weyl- +conjugate to a standard parabolic subsystem: take a generic real normal +whose vanishing roots are precisely that intersection, and use its Weyl +point stabilizer. Among the 256 standard parabolics, ranks<=5 have at +most 20 root lines. The qualifying proper types are exactly + +| rank | subsystem | root lines | normal object | +|---:|---|---:|---| +| 7 | E7 | 63 | a root line | +| 7 | D7 | 42 | a primitive norm-four line | +| 7 | E6+A1 | 37 | a norm-six line | +| 7 | A7 | 28 | a primitive norm-eight line | +| 6 | E6 | 36 | an A2 normal plane | +| 6 | D6 | 30 | an orthogonal-root normal plane | + +The rank-seven normal norms follow from the fundamental-weight calculation. +The rank-six normal planes contain respectively three and two root lines. +Generic members of each plane have one common support; exceptional members +have a larger perpendicular subsystem and are in the rank-seven cases. + +The independently regenerated deletion profiles below consider every +binary hyperplane H and keep all normal objects with |Off_P(h)|<=84. + +| family | total objects | (Off size, minimum deletion size, objects) | +|---|---:|---| +| norm four | 1080 | (70,14,128), (73,13,896), (76,12,56) | +| norm six | 3360 | (77,25,2688), (79,24,448), (80,24,224) | +| primitive norm eight | 8640 | (84,28,1024) | +| A2 normal planes | 1120 | (78,26,896), (80,24,224) | +| orthogonal-root normal planes | 3780 | (82,26,448), (84,24,2688) | + +Every norm-four deletion of size at most twenty has label rank at least seven; +the other families require at least 24 deleted lines. Neither can be supplied +by U. Only root directions remain. The norm-four rank test is essential: its deletion +cardinalities alone are insufficient. + +This argument covers every characteristic-zero field because all the +filter's hypotheses are zero-pattern conditions: they use only which +rational root rows vanish, and the resulting fixed binary supports and ranks. +For any such pattern realized by h over K, let V_Q be the rational kernel +of its zero rows. Each designated nonzero row is nonzero on V_Q; otherwise +it would vanish on V_Q tensor K, which contains h. A finite union of proper +rational hyperplanes cannot cover V_Q, so a rational point realizes exactly +the same zero and nonzero rows. The normal-family and normal-plane tests +therefore apply to it with unchanged hypotheses. Once this rational +representative is forced to a root line, +its zero rows span that root's rank-seven perpendicular system. The original +K-vector has the same zero rows, hence belongs to the same one-dimensional +K-root line. No positivity of the coefficients of h is assumed. + +The parabolic inventory also shows that every proper root intersection has +at most 63 lines. Thus every nonzero word in C_P has at least 112-63=49 +nonzero coordinates, whereas a weight-at-most-seven support has at most 36. +Consequently (C_P)_{<=7}=0. This supplies the d=0 assertion for the sharp +examples in Section 1 without importing a predecessor codeword census. + +## 5. From feasible directions to actual root swaps + +Suppose cost(L)=k<=7 and L contains a nonzero vector supported on F. +Restriction removes at least one positive-weight basis member: choosing +independent restricted basis images gives + + cost(rho L) <= k - dim(ker(rho) intersect L) <= 6. + +If dim L>=2, a minimum basis has at least two positive weight parts, each +at most six. The cap table shows its full union support has size<=21, +maximized by the partition 6+1. If dim L=1, the nonzero kernel forces +L to be supported on the eight frame coordinates, so the bound still holds. + +Let p_h+ell have full weight<=8 for ell in L and h!=0. The root-only lemma +applied after restriction makes h a root direction. Scale h to a root r. +The 56 nonself nonorthogonal coordinates of p_r, after removing supp(L), +still span W_r: fewer than 24 deletions cannot reduce their rank. Any +hyperplane containing supp(p_r+ell) is consequently W_r itself. +Choose r to be the fixed representative r_t of its root line. Its own root +coordinate and every coordinate orthogonal to r lie outside W_r. Thus +ell(r_t)=-2, and ell vanishes at all other orthogonal coordinates. Choosing +the opposite normal representative instead gives +2 at that coordinate; +rescaling the witness leaves exact-swap eligibility unchanged. +It is an actual root-swap witness. Conversely any such witness, after +scaling its own coordinate to -2, gives a vector supported in W_r. + +Therefore the span of all feasible h directions has dimension +rank R(L)<=k by Theorem A. The strict full remainder bound 24>21 is why +the P112 remainder's smaller deletion threshold is not enough here. + +## 6. Proof of Theorem B and exact downstream scope + +Suppose, to obtain a contradiction, that cost(S)<=71. Put L=S_{<=7}. +Since rho L is contained in T and C_P intersect T=0, and rho is injective +on C_E, we have C_E intersect L=0. Thus S/L has dimension at least eight. +A greedy minimum basis of S consists of a minimum basis of L and +at least eight members of weight eight or nine. Nine such members would +already cost 72. There are exactly eight, their code directions are +independent, S=C_E direct-sum L, and k=cost(L)<=7. +Here greedy basis selection uses the nested spans S_{<=j}: at each weight, +extend an independent set to a basis of that span. Any basis must contain +at least dim S-dim S_{<=j} members above weight j, so this construction +minimizes the total weight and justifies the simultaneous basis choice. + +Also T=rho L: T contains rho L, and any additional element of T would, +after subtracting its rho L part, give a nonzero element of C_P intersect T. +Writing a kernel vector as c+ell in C_E direct-sum L similarly shows +Z=ker(rho) intersect L. In particular L has the nonzero frame-supported +vector required by Section 5. + +If t of the eight high basis members have weight eight, the cost is + + k + 8t + 9(8-t) = 72+k-t. + +Cost<=71 forces t>=k+1 independent feasible code directions. Section 5 +and Theorem A bound their span by k. This contradiction proves Theorem B. + +PR3074 originally lists this kernel branch separately from the 38 open d>=4 +rows, seven prior-only rows and seven conditional E6-slack rows. The newer +PR3154 claims further ledger closures and retains the kernel case as C7, +alongside C6 (DEG2) on the one-sided track. Its CONJECTURES.md and +checks/L120D0/NOTES.md Section 4 use the same definitions as Theorem B. +The theorem here removes C7 directly. No other PR3154 closure is imported or +independently validated here; C1-C6 and a complete L120 proof remain outside +this result. + +## 7. Credit and evidence boundary + +DreamingOfClouds' PR2816 supplies the one-sided lift model, weight/peeling +framework and parabolic reduction; PR2862 supplies the predecessor +carrier argument for restricted cost at most three; PR2985 supplies full +E8 cap context; PR3074 states the open kernel branch and padding implication. +PR3095 clarifies the field scope and normalization boundary. PR1590's +two-factor lemma is reused, with the finite-order field clarification above. +PR3154 and Discussion3156 provide the latest C7 statement and handoff. +Classical E8 lattice, quadratic-space and root-system facts retain their +original mathematical status; no new general lattice theorem is claimed. + +The new work is Theorem A's shared-coefficient argument, its application +through the full remainder and restricted normal filters, and the completed +kernel-branch implication. Prepared by conorholds with substantial OpenAI +Codex assistance, including GPT-6.1 SOL agents at xHigh reasoning. +Finite replays support the stated inputs and controls. They are not a +proof-assistant certification or independent human review. diff --git a/research/e8-d0-root-swaps/README.md b/research/e8-d0-root-swaps/README.md new file mode 100644 index 0000000000..094f060a75 --- /dev/null +++ b/research/e8-d0-root-swaps/README.md @@ -0,0 +1,266 @@ +# E8 root swaps close the d=0 kernel branch + +**Result: a characteristic-zero proof of the `d=0`, nonzero-kernel branch +explicitly left open by [PR3074](https://github.com/CrocSwap/integer-mult-bounds/pull/3074).** +The newer [PR3154](https://github.com/CrocSwap/integer-mult-bounds/pull/3154) +and [Discussion3156](https://github.com/CrocSwap/integer-mult-bounds/discussions/3156) +retain this exact obligation as **C7**. +Every lift S of the full E8 root code in that branch has basis weight cost +at least 72. The bound is sharp, including for lifts with nonzero kernel. + +The reusable step is a shared-coefficient root-swap bound: if R(L) consists +of roots whose own coordinate can be changed using L while every other +orthogonal coordinate remains zero, then + + rank_K R(L) <= cost(L). + +This holds for every correction space L over a characteristic-zero field K. +The [proof](PROOF.md) establishes the uniform statement; the finite checks +verify its geometric inputs and actual coefficient-space examples. They do +not enumerate all L. Three checked Lean files formalize coefficient and covering cores; +the complete E8 theorem is not proof-assistant certified. + +## Exact obligation and added value + +Use the fixed dense-pairing/Gram model of +[PR2816](https://github.com/CrocSwap/integer-mult-bounds/pull/2816). +E is the 120 E8 root lines, F its specified orthogonal eight-line frame, +P=E minus F, and rho is restriction to P. Labels are +`(1, r mod 2E8)` in F2^9; a vector's weight is its support's binary label rank. +`cost(S)` minimizes the sum of these weights over bases of S. Let C_E be +the full root code, C_P its restriction, and + + C_E subset S, + T = span{v in rho S : w(v)<=7}, + d = dim_K(C_P intersect T), + Z = ker(rho) intersect S. + +The theorem is **d=0 and Z nonzero imply cost(S)>=72**. +PR3074 originally names this kernel case separately from the 38 open d>=4 +ledger rows, seven prior-only rows and seven conditional E6-slack rows. +PR3154 now claims further ledger closures and retains C6 (DEG2) and C7 on +the one-sided track. Its other claims are neither imported nor audited here. +This package closes C7. The follow-up [EXTENSION.md](EXTENSION.md) also closes +C1's precise d=0 rigid-shape subcase with actual low-basis total Sigma=7. +Theorem F in EXTENSION.md additionally closes actual total eight with a +minimum (7,1) basis. Other C1 cases and C2-C6 remain outside the closure claim. +Every C1 decoder consequence is conditional on PR3154's rigid shape, +the ledger `cost(D') = sum_j w(A_j) - n_c`, the pivot rebate +`epsilon_k in {0,1}`, and N8 (at most eight corrections with distinct +corrected frame indices). This package does not independently validate +that reduction, even where the source marks its premises PROVEN. +The result alone does not establish L120, the one-sided P112 floor for every +correction pattern, a two-sided decoder floor, a supplier, or a new kappa. + +[PR2862](https://github.com/CrocSwap/integer-mult-bounds/pull/2862) proves the +restricted carrier argument only through correction cost kappa<=3. Merely +extending that counting shortcut is unsafe: the algebra checker reproduces +a cost-five correction with six carrying vectors. Here the argument instead +bounds the rank of roots eligible in the *same* coefficient space. + +The proof has three substantive steps: + +1. The root-swap rank bound handles every space of cost at most seven by + separating exceptional basis members. A weight-three exceptional support + is an orthogonal quartet; only profiles (3,3), (4,3) and (3,3,1) require + further cases. The first two reuse PR1590's two-factor lemma with an + explicit finite-order extension to arbitrary fields. +2. A complete parabolic normal classification and deletion-rank filter rule + out nonroot directions at restricted correction cost at most six. On the + full E8 set, every root's 56-line remainder needs at least 24 deletions to + lose rank, while the full correction support has at most 21 lines. This + converts feasible directions into exact root swaps. +3. A hypothetical cost-at-most-71 lift in the named kernel branch would + require at least k+1 independent feasible directions for a correction + space of cost k<=7. The rank bound permits at most k. + +## Stronger filter and a downstream subcase + +The [extension](EXTENSION.md) proves that the restricted root-only filter +also holds at correction cost seven **when the correction space has dimension +at least two**. A connected twelve-point binary matroid excludes the only +new nonroot configuration. All 56 configurations have explicit six-pair +circuit certificates, checked in two coordinate models. Two actual boundary +examples show why the dimension and cost bounds matter: a one-dimensional +cost-seven nonroot survives, and a two-dimensional cost-eight nonroot +survives while carrying four frame labels. + +Theorem C also settles **CONJG2 Section 2(ii) for every kappa<=7** in the +rigid d=0 shape: every weight-eight high normal is an E8 root direction, +so no nonroot D7/E6-type direction survives. This conclusion permits frame +roots and does not require actual low-basis total Sigma=7. The kappa=8 +directions and the remaining invoice/coefficient obligations are separate. + +In PR3154's d=0 rigid basis shape, this limits corrected weight-eight high +members to four. When the **actual low-basis total is Sigma=7**, the corrected +one-sided invoice is at least 65 and the pivot invoice at least 64. This +closes that C1 subcase with one unit of slack, without the unresolved F1 or +T_v coefficient steps. It does not close every cost-seven statement or all +of C1. Actual total eight is also excluded if the minimum space cost is at +most seven. The extension also proves a sharp **F1 support threshold of 24**, +with an actual failure at 25. This settles the F1 input for the entire +d=0, dim(T)=3 rigid C1 branch. Its exact-cost-eight, dimension-two boundary +violates unrestricted F1, but does not construct a complete C1 decoder or +satisfy every additional pivot condition. A separate frame-plane and +incidence argument nevertheless excludes the entire actual-total-eight +minimum-(7,1) decoder branch: at least 168 cancellations would need at most +148 available frame incidences. The other minimum-cost-eight profiles +remain open. Combining the support bound with that exclusion discharges +C1's entire F1 obligation on surviving d=0 rigid low-invoice candidates. +Exact hypotheses and limitations are in EXTENSION.md. + +## Reproduce + +From the repository root, with Python 3.12 and no external dependencies: + +```sh +python3.12 -I -B scripts/research_package.py --package research/e8-d0-root-swaps --check-only +python3.12 -I -B scripts/research_package.py --package research/e8-d0-root-swaps +``` + +For a source export containing only this package: + +```sh +python3.12 -I -B research/e8-d0-root-swaps/verify.py +``` + +The registered replay checks pinned Git provenance, recomputes +the finite geometry by both methods below, runs the exact algebra and extension controls, +and compares its result and scientific source hashes with [RESULT.json](RESULT.json). +It does not edit the receipt. `verify.py --emit NEW_PATH` creates a new +receipt for deliberate regeneration and refuses to overwrite an existing file. + +The final registered replay, including the new extension and F1 checks, +passed after the audit fixes on CPython 3.12.11 in 8.40 seconds; the read-only +Git-free optimized export passed in 7.97 seconds. Two additional source +mutants changing the dimension-eight cap to 65 were rejected by the respective +mathematical guards under optimized Python. An earlier optimized extension +replay and five mathematical mutants (wrong pair mate, unit coefficient, +admitted frame roots, F1 cancellation sign and cycle elimination) passed in +9.29 seconds; that extension code is unchanged. + +The original C7 replay passed in 4.45 seconds. A read-only +Git-free export also passed with `-O -Werror`. Separate temporary-copy probes +rejected a changed receipt, changed proof bytes, an existing emit destination, +an intersection substituted for the normal-plane union, and a support-only +coefficient shortcut. The last two failed in the mathematical checks before +the final source-hash comparison. Those temporary probes are additional local +evidence; the updated registered command runs eighteen rejection controls, plus the +positive and boundary fixtures listed below. + +| Evidence | Coverage | +|---|---| +| Euclidean coordinate checker, `verify.py` | All 120 roots, 511 binary hyperplanes (including the dimension-eight cap 64), 256 standard parabolics, and all five nonroot normal families | +| Cartan/Weyl cross-check, `geometry_audit.py` | Reflection-generated roots and normal/plane orbits; exact agreement on the complete deletion profiles; Fourier identity and full-E8 caps, including a direct dimension-eight check | +| Full root remainders | All 120 directions; 56 lines each; minimum nonzero character support 24 | +| Coefficient checker, `algebra_check.py` | 13 actual spaces over Q(i), 42 reconstructed swap witnesses, and a sharp cost-seven example | +| Exceptional supports | All 32,130 binary-dependent quartets, including 9,450 overrank orthogonal quartets and 151,200 signed half-sums | +| Kernel sharpness | Seven explicit cost-72 bases of C_E plus one through seven frame units | +| Cost-seven extension, `extension_check.py` | Two models; all 56 connected critical deletions; complete threshold-27/Off-85 additions; private-frame bound four; literal dimension-one cost-seven and carrying dimension-two cost-eight boundaries; sharp F1 support-24 theorem and support-25 failure; all 57,120 frame-plane cases per model | +| Failure controls | Five geometric, ten algebraic, and three corrupted six-pair-certificate controls | +| Partial Lean core | Generating-family one-exception rank bound, low-overlap quartet/singleton argument and overlapping connected-cover obstruction; compiled separately | + +Both geometry implementations compute exact integer/rational ranks. They +share the mathematical reduction, `EXPECTED_PROFILES` and attribution to +the same author, and use different root coordinates, orbit generation and +plane enumeration. They provide an internal cross-check, not independent +review or certification of the complete written proof in Lean. Coefficient fixtures are controls, +not an exhaustive search over arbitrary scalar spaces. No predecessor's long +DP/LP/RRC census is imported or rerun; none is needed for this branch. + +The three Lean files use the repository's existing `formal/lean` environment +(Lean/mathlib v4.21.0, exact pins in SOURCES.json). With that environment +prepared, run from the repository root: + +```sh +cd formal/lean +lake env lean ../../research/e8-d0-root-swaps/formal/RootSwapOneExceptional.lean +lake env lean ../../research/e8-d0-root-swaps/formal/RootSwapQuartet.lean +lake env lean ../../research/e8-d0-root-swaps/formal/RootSwapConnectedCover.lean +``` + +All three passed without warnings and are byte-identical to the separately +audited candidate; those compilation results are reused for this revision. +Printed axioms are only `propext`, +`Classical.choice` and `Quot.sound`. Python replay binds their source bytes +but does **not** execute Lean. The E8 instantiation, geometric classification, +two-factor lemma and final C7 assembly remain outside this formalization; +see EXTENSION.md Section 7. No hosted CI or predecessor long suites were run. + +## Sources, overlap and credit + +The base is `997e6a9ca7b4f95d50e366f61412fd640d72a88a`, priority revision 6. +Exact file blobs, SHA256 hashes, PR heads and roles are in [SOURCES.json](SOURCES.json). +Its `files` inventory is authenticated against Git objects reachable from the +base. Its `related_work` pins the unmerged PR2985/PR3074/PR3154 documentary citations; +those hashes were checked locally and are not fetched or validated by generic +CI. The C1 applications retain the stated model premises as assumptions; +the broader pending reduction is not validated here. Replay executes only +this package's standard-library code. Frozen packages and the selected result +are untouched. + +DreamingOfClouds' [PR1590](https://github.com/CrocSwap/integer-mult-bounds/pull/1590) +provides the two-factor lemma; +[PR2816](https://github.com/CrocSwap/integer-mult-bounds/pull/2816) provides the +model, peeling framework and classical parabolic reduction; +[PR2862](https://github.com/CrocSwap/integer-mult-bounds/pull/2862) is the +kappa<=3 predecessor; +[PR2985](https://github.com/CrocSwap/integer-mult-bounds/pull/2985) supplies +full-E8 cap context; and +[PR3074](https://github.com/CrocSwap/integer-mult-bounds/pull/3074) states the +open kernel case and padding implication. CubeJerry's +[PR3095](https://github.com/CrocSwap/integer-mult-bounds/pull/3095) independently +certifies the exact support chart and clarifies the field/normalization scope. +Those results retain their credit. No predecessor implementation is copied. The Lean coefficient and covering cores +use the existing mathlib library, under its upstream license. +DreamingOfClouds' PR3154 and Discussion3156 supply the fresh C7 target and +remaining-conjecture map, rigid C1 shape and corrected-invoice identity. +Their broader claimed reduction is not validated by this package. +[PR3158](https://github.com/CrocSwap/integer-mult-bounds/pull/3158) (Nick Petalas) +and [PR3160](https://github.com/CrocSwap/integer-mult-bounds/pull/3160) address +adjacent C5 deletion-quantifier/common-cut questions. +[PR3161](https://github.com/CrocSwap/integer-mult-bounds/pull/3161) closes the +pinned TWOSIDE `(5,3)` beta residue; its follow-up +[PR3162](https://github.com/CrocSwap/integer-mult-bounds/pull/3162) proves a +ten-deletion bound and another `(5,4)` exclusion. +[PR3163](https://github.com/CrocSwap/integer-mult-bounds/pull/3163) certifies +a fixed-first-space rank-seven/common-deletion slice. These concern C5, +not the C7 or scoped C1 results here; none is an imported proof premise. +The reduction's author announced a +[PR3154 follow-up consolidating the C5 results](https://github.com/CrocSwap/integer-mult-bounds/discussions/3156#discussioncomment-18998364) +and subsequently claimed C6, explicitly leaving C1-C4 and C7 open. Any +publication should coordinate with that active thread. + +Overlap was checked against the open and closed PR corpus and paginated +Discussion comments, then against the named predecessor heads and target +comments. The bounded search coverage and timestamps are recorded in +[TASK.json](TASK.json); absence of a matching search result is not proof of +priority. No public claim or coordination update has been posted because the +donor requires local review before any upstream action. + +This is a **changed** scope from `complex-rank-shape-decoder`, selected after +the donor requested a deeper opportunity review. It closes a named decoder +proof obligation instead of constructing a larger-rank child. It is a scoped +lower-bound result, with no family-expansion or selected-frontier claim. + +Prepared by **conorholds** with substantial OpenAI Codex assistance, including +GPT-6.1 SOL agents at xHigh reasoning for independent geometry, algebra and +proof audits. No independent human review is claimed. Apache-2.0. + +## Open next questions + +1. **Remaining C1 profiles and pivot cases.** Start with PR3154 CONJG2 Section 2: separate + actual basis total from minimum correction cost, and retain the pivot + rebate and T_v coefficients. The cost-eight carrying boundary here + rules out a direct extrapolation of the root-only filter. +2. **Complete formalization.** Instantiate the checked coefficient cores for + E8 and binary labels, then formalize the remaining exceptional cases and + geometric/greedy bridge. The current Lean files establish partial cores. +3. **C6 (DEG2) and the remaining reduction.** PR3154 retains the one-sided + ledger row 579 conditional on DEG2. First inspect its coverable triples + and the unfinished orbit representative, then retain coefficients through + the fourth/fifth-flat extension with an independent check. The larger + reduction and its imported claims still need their own review. This + package supplies neither a C6 result nor a validation of that reduction. + +Structured relevance, first steps and blockers are in [TASK.json](TASK.json). diff --git a/research/e8-d0-root-swaps/RESULT.json b/research/e8-d0-root-swaps/RESULT.json new file mode 100644 index 0000000000..e1a89572dc --- /dev/null +++ b/research/e8-d0-root-swaps/RESULT.json @@ -0,0 +1,1437 @@ +{ + "algebra": { + "coefficient_field": "Q(i)", + "complex_two_total": { + "rank_sum": 12, + "shared": 6, + "size": 8 + }, + "cost_ge_8": "root rank at most eight; no counterexample asserted", + "eligible_witnesses": 42, + "exception_profiles": [ + [ + 3, + 3 + ], + [ + 3, + 3, + 1 + ], + [ + 4, + 3 + ] + ], + "fixtures": [ + { + "cost": 7, + "eligible": 7, + "name": "sharp-3-3-1", + "one_exception_outside_o": null, + "overrank_pieces": 0, + "root_rank": 7, + "weights": [ + 3, + 3, + 1 + ] + }, + { + "cost": 5, + "eligible": 5, + "name": "complex-two-total-sharp", + "one_exception_outside_o": null, + "overrank_pieces": 0, + "root_rank": 5, + "weights": [ + 3, + 2 + ] + }, + { + "cost": 6, + "eligible": 0, + "name": "two-overrank-3-3", + "one_exception_outside_o": null, + "overrank_pieces": 2, + "root_rank": 0, + "weights": [ + 3, + 3 + ] + }, + { + "cost": 6, + "eligible": 1, + "name": "two-overrank-3-3-positive", + "one_exception_outside_o": null, + "overrank_pieces": 2, + "root_rank": 1, + "weights": [ + 3, + 3 + ] + }, + { + "cost": 7, + "eligible": 0, + "name": "two-overrank-4-3", + "one_exception_outside_o": null, + "overrank_pieces": 2, + "root_rank": 0, + "weights": [ + 4, + 3 + ] + }, + { + "cost": 7, + "eligible": 1, + "name": "orthogonal-3-3-1-overlap-0", + "one_exception_outside_o": null, + "overrank_pieces": 2, + "root_rank": 1, + "weights": [ + 3, + 3, + 1 + ] + }, + { + "cost": 7, + "eligible": 1, + "name": "orthogonal-3-3-1-overlap-1", + "one_exception_outside_o": null, + "overrank_pieces": 2, + "root_rank": 1, + "weights": [ + 3, + 3, + 1 + ] + }, + { + "cost": 7, + "eligible": 1, + "name": "orthogonal-3-3-1-overlap-2", + "one_exception_outside_o": null, + "overrank_pieces": 2, + "root_rank": 1, + "weights": [ + 3, + 3, + 1 + ] + }, + { + "cost": 7, + "eligible": 1, + "name": "orthogonal-3-3-1-overlap-4", + "one_exception_outside_o": null, + "overrank_pieces": 2, + "root_rank": 1, + "weights": [ + 3, + 3, + 1 + ] + }, + { + "cost": 6, + "eligible": 4, + "name": "one-exception-actual-space", + "one_exception_outside_o": 1, + "overrank_pieces": 1, + "root_rank": 4, + "weights": [ + 3, + 1, + 1, + 1 + ] + }, + { + "cost": 7, + "eligible": 7, + "name": "sharp-seven-units", + "one_exception_outside_o": null, + "overrank_pieces": 0, + "root_rank": 7, + "weights": [ + 1, + 1, + 1, + 1, + 1, + 1, + 1 + ] + }, + { + "cost": 8, + "eligible": 8, + "name": "cost-eight-ambient-bound", + "one_exception_outside_o": null, + "overrank_pieces": 0, + "root_rank": 8, + "weights": [ + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1 + ] + }, + { + "cost": 6, + "eligible": 6, + "name": "old-carrier-full-rank-control", + "one_exception_outside_o": null, + "overrank_pieces": 0, + "root_rank": 6, + "weights": [ + 5, + 1 + ] + } + ], + "kernel_sharpness": [ + { + "basis_cost": 72, + "frame_units": 1, + "full_dimension": 9, + "kernel_dimension": 1, + "restricted_dimension": 8 + }, + { + "basis_cost": 72, + "frame_units": 2, + "full_dimension": 10, + "kernel_dimension": 2, + "restricted_dimension": 8 + }, + { + "basis_cost": 72, + "frame_units": 3, + "full_dimension": 11, + "kernel_dimension": 3, + "restricted_dimension": 8 + }, + { + "basis_cost": 72, + "frame_units": 4, + "full_dimension": 12, + "kernel_dimension": 4, + "restricted_dimension": 8 + }, + { + "basis_cost": 72, + "frame_units": 5, + "full_dimension": 13, + "kernel_dimension": 5, + "restricted_dimension": 8 + }, + { + "basis_cost": 72, + "frame_units": 6, + "full_dimension": 14, + "kernel_dimension": 6, + "restricted_dimension": 8 + }, + { + "basis_cost": 72, + "frame_units": 7, + "full_dimension": 15, + "kernel_dimension": 7, + "restricted_dimension": 8 + } + ], + "old_carrier_cost": 5, + "old_carrier_count": 6, + "quartets": { + "dependent_quartets": 32130, + "overrank_orthogonal_quartets": 9450, + "signed_half_sums": 151200 + }, + "rejected_controls": 10, + "roots": 120, + "scope": "finite-independent-algebra-controls-not-an-exhaustion-of-L" + }, + "cost_seven_extension": { + "checks": { + "common_xor_pairs_per_deletion": 6, + "connected_rank7_deletions": 56, + "dimension_one_fixture": { + "corrected_weight": 8, + "eligible_root_count": 0, + "essential_coordinates": 12, + "h_doubled": [ + 2, + 2, + 2, + 2, + 0, + 0, + 0, + 0 + ], + "hyperplane_basis_doubled": [ + [ + 0, + 0, + 0, + 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, + 2 + ], + [ + 0, + 0, + 2, + 0, + -2, + 0, + 0, + 0 + ], + [ + 0, + 2, + 0, + 0, + -2, + 0, + 0, + 0 + ], + [ + 1, + -1, + -1, + -1, + -1, + -1, + -1, + 1 + ] + ], + "hyperplane_carries_frame": false, + "tau_entries": [ + [ + [ + 0, + 2, + 0, + 2, + 0, + 0, + 0, + 0 + ], + -2 + ], + [ + [ + 0, + 2, + 2, + 0, + 0, + 0, + 0, + 0 + ], + -2 + ], + [ + [ + 1, + 1, + 1, + 1, + -1, + -1, + -1, + -1 + ], + -2 + ], + [ + [ + 1, + 1, + 1, + 1, + -1, + -1, + 1, + 1 + ], + -2 + ], + [ + [ + 1, + 1, + 1, + 1, + -1, + 1, + -1, + 1 + ], + -2 + ], + [ + [ + 1, + 1, + 1, + 1, + -1, + 1, + 1, + -1 + ], + -2 + ], + [ + [ + 1, + 1, + 1, + 1, + 1, + -1, + -1, + 1 + ], + -2 + ], + [ + [ + 1, + 1, + 1, + 1, + 1, + -1, + 1, + -1 + ], + -2 + ], + [ + [ + 1, + 1, + 1, + 1, + 1, + 1, + -1, + -1 + ], + -2 + ], + [ + [ + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1 + ], + -2 + ], + [ + [ + 2, + 0, + 0, + 2, + 0, + 0, + 0, + 0 + ], + -2 + ], + [ + [ + 2, + 0, + 2, + 0, + 0, + 0, + 0, + 0 + ], + -2 + ] + ], + "tau_support": 12, + "tau_weight": 7 + }, + "dimension_two_cost_eight_fixture": { + "basis_weights": [ + 7, + 1 + ], + "carried_frame_indices": [ + 1, + 2, + 5, + 6 + ], + "corrected_support": 60, + "corrected_weight": 8, + "dimension": 2, + "exact_cost": 8, + "h_doubled": [ + 2, + 2, + 2, + 0, + 2, + 0, + 0, + 0 + ], + "q0_alone_corrected_weight": 9, + "q0_entries": [ + [ + [ + 0, + 2, + 0, + 0, + 2, + 0, + 0, + 0 + ], + -2 + ], + [ + [ + 0, + 2, + 2, + 0, + 0, + 0, + 0, + 0 + ], + -2 + ], + [ + [ + 1, + 1, + 1, + -1, + 1, + -1, + -1, + -1 + ], + -2 + ], + [ + [ + 1, + 1, + 1, + -1, + 1, + -1, + 1, + 1 + ], + -2 + ], + [ + [ + 1, + 1, + 1, + -1, + 1, + 1, + -1, + 1 + ], + -2 + ], + [ + [ + 1, + 1, + 1, + -1, + 1, + 1, + 1, + -1 + ], + -2 + ], + [ + [ + 1, + 1, + 1, + 1, + 1, + -1, + -1, + 1 + ], + -2 + ], + [ + [ + 1, + 1, + 1, + 1, + 1, + -1, + 1, + -1 + ], + -2 + ], + [ + [ + 1, + 1, + 1, + 1, + 1, + 1, + -1, + -1 + ], + -2 + ], + [ + [ + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1 + ], + -2 + ], + [ + [ + 2, + 0, + 0, + 0, + 2, + 0, + 0, + 0 + ], + -2 + ], + [ + [ + 2, + 0, + 2, + 0, + 0, + 0, + 0, + 0 + ], + -2 + ] + ], + "scope": "correction-space boundary only", + "tau_support": 13, + "tau_unit_coefficient": -2, + "union_label_rank": 8, + "unit_root_doubled": [ + 0, + 0, + 2, + 0, + 2, + 0, + 0, + 0 + ] + }, + "four_circuits_per_deletion": 15, + "frame_support_blocks": 14, + "large_proper_types": [ + [ + 6, + 30 + ], + [ + 6, + 36 + ], + [ + 7, + 28 + ], + [ + 7, + 37 + ], + [ + 7, + 42 + ], + [ + 7, + 63 + ] + ], + "maximum_private_choices": { + "4": 4, + "5": 1, + "6": 0 + }, + "negative_controls_rejected": 3, + "norm4_small_deletions": [ + [ + 12, + 7, + 56 + ], + [ + 13, + 8, + 896 + ], + [ + 14, + 8, + 128 + ] + ], + "norm8_off85": [ + 85, + 25, + 3584 + ], + "orthogonal_plane_off85": [ + 85, + 25, + 448 + ], + "parabolic_threshold": 27 + }, + "coordinate_models": 2, + "f1": { + "a2_plane_minimum_code_support": 78, + "large_proper_types": [ + [ + 6, + 36 + ], + [ + 7, + 37 + ], + [ + 7, + 42 + ], + [ + 7, + 63 + ] + ], + "maximum_guaranteed_correction_support": 24, + "norm4_minimum_required": 30, + "norm6_deletion_profile": [ + [ + 25, + 2688 + ], + [ + 26, + 5376 + ], + [ + 39, + 10752 + ], + [ + 40, + 64512 + ], + [ + 41, + 99456 + ], + [ + 42, + 26880 + ], + [ + 43, + 32256 + ], + [ + 44, + 43008 + ], + [ + 45, + 16128 + ] + ], + "norm6_minimum_code_support": 77, + "norm6_relevant_objects": 2688, + "other_root_minimum_required": 26, + "parabolic_threshold": 36, + "sharp_support25_fixture": { + "corrected_support": 52, + "corrected_weight": 8, + "dimension_two_space": { + "basis_weights": [ + 7, + 1 + ], + "cost_at_most7_dimension_two_union_cap": 21, + "dimension": 2, + "exact_cost": 8, + "fixed_nonunit_support_rank": 7, + "scope": "F1 correction-space counterexample only", + "union_support": 25, + "unit_root_doubled": [ + 0, + 0, + 0, + 0, + 2, + 0, + 0, + -2 + ] + }, + "essential_coordinates": 25, + "h_doubled": [ + 0, + 0, + 0, + 2, + -4, + 0, + -2, + 0 + ], + "tau_entries": [ + [ + [ + 0, + 0, + 0, + 0, + 2, + 0, + 0, + -2 + ], + 2 + ], + [ + [ + 0, + 0, + 0, + 0, + 2, + 0, + 0, + 2 + ], + 2 + ], + [ + [ + 0, + 0, + 0, + 2, + 0, + 0, + -2, + 0 + ], + -2 + ], + [ + [ + 0, + 0, + 2, + 0, + -2, + 0, + 0, + 0 + ], + -2 + ], + [ + [ + 0, + 0, + 2, + 0, + 2, + 0, + 0, + 0 + ], + 2 + ], + [ + [ + 0, + 2, + 0, + 0, + -2, + 0, + 0, + 0 + ], + -2 + ], + [ + [ + 0, + 2, + 0, + 0, + 2, + 0, + 0, + 0 + ], + 2 + ], + [ + [ + 1, + -1, + -1, + -1, + 1, + -1, + 1, + 1 + ], + 2 + ], + [ + [ + 1, + -1, + -1, + -1, + 1, + 1, + 1, + -1 + ], + 2 + ], + [ + [ + 1, + -1, + -1, + 1, + -1, + -1, + -1, + -1 + ], + -2 + ], + [ + [ + 1, + -1, + -1, + 1, + -1, + 1, + -1, + 1 + ], + -2 + ], + [ + [ + 1, + -1, + 1, + -1, + 1, + -1, + 1, + -1 + ], + 2 + ], + [ + [ + 1, + -1, + 1, + -1, + 1, + 1, + 1, + 1 + ], + 2 + ], + [ + [ + 1, + -1, + 1, + 1, + -1, + -1, + -1, + 1 + ], + -2 + ], + [ + [ + 1, + -1, + 1, + 1, + -1, + 1, + -1, + -1 + ], + -2 + ], + [ + [ + 1, + 1, + -1, + -1, + 1, + -1, + 1, + -1 + ], + 2 + ], + [ + [ + 1, + 1, + -1, + -1, + 1, + 1, + 1, + 1 + ], + 2 + ], + [ + [ + 1, + 1, + -1, + 1, + -1, + -1, + -1, + 1 + ], + -2 + ], + [ + [ + 1, + 1, + -1, + 1, + -1, + 1, + -1, + -1 + ], + -2 + ], + [ + [ + 1, + 1, + 1, + -1, + 1, + -1, + 1, + 1 + ], + 2 + ], + [ + [ + 1, + 1, + 1, + -1, + 1, + 1, + 1, + -1 + ], + 2 + ], + [ + [ + 1, + 1, + 1, + 1, + -1, + -1, + -1, + -1 + ], + -2 + ], + [ + [ + 1, + 1, + 1, + 1, + -1, + 1, + -1, + 1 + ], + -2 + ], + [ + [ + 2, + 0, + 0, + 0, + -2, + 0, + 0, + 0 + ], + -2 + ], + [ + [ + 2, + 0, + 0, + 0, + 2, + 0, + 0, + 0 + ], + 2 + ] + ], + "tau_support": 25, + "tau_weight": 7, + "v_doubled": [ + 0, + 0, + 0, + 2, + 0, + 0, + 2, + 0 + ] + } + }, + "frame_planes": { + "carrying_hyperplanes_per_pair": 255, + "cases": 57120, + "direct_rank_deletion_profiles_cross_checked": 5, + "frame_minimum_deletions": 24, + "maximum_correction_incidences": 148, + "minimum_seven_frame_incidences": 168, + "nonroot_cases_without_coloops": 42840, + "ordered_frame_pairs": 56, + "profiles": [ + [ + "frame", + 7, + 7, + 14224 + ], + [ + "frame", + 8, + 8, + 56 + ], + [ + "generic", + 8, + 8, + 14280 + ], + [ + "minus", + 8, + 8, + 14280 + ], + [ + "plus", + 8, + 8, + 14280 + ] + ], + "strata": 4 + } + }, + "geometry": { + "full_cap_bounds": { + "1": 1, + "2": 2, + "3": 4, + "4": 8, + "5": 12, + "6": 20, + "7": 36, + "8": 64 + }, + "full_code": { + "hyperplanes_checked": 511, + "minimum_complement_real_rank": 8 + }, + "model": { + "frame_label_rank": 4, + "frame_lines": 8, + "quadratic_gauss_sum": 16, + "root_lines": 120 + }, + "normal_filter": { + "a1_squared_plane": { + "orbit_size": 3780, + "profiles": [ + [ + 82, + 26, + null, + 448 + ], + [ + 84, + 24, + null, + 2688 + ] + ] + }, + "a2_plane": { + "orbit_size": 1120, + "profiles": [ + [ + 78, + 26, + null, + 896 + ], + [ + 80, + 24, + null, + 224 + ] + ] + }, + "norm4": { + "orbit_size": 1080, + "profiles": [ + [ + 70, + 14, + 8, + 128 + ], + [ + 73, + 13, + 8, + 896 + ], + [ + 76, + 12, + 7, + 56 + ] + ] + }, + "norm6": { + "orbit_size": 3360, + "profiles": [ + [ + 77, + 25, + null, + 2688 + ], + [ + 79, + 24, + null, + 448 + ], + [ + 80, + 24, + null, + 224 + ] + ] + }, + "norm8": { + "orbit_size": 8640, + "profiles": [ + [ + 84, + 28, + null, + 1024 + ] + ] + } + }, + "parabolics": { + "large_proper_types": [ + [ + 6, + 30 + ], + [ + 6, + 36 + ], + [ + 7, + 28 + ], + [ + 7, + 37 + ], + [ + 7, + 42 + ], + [ + 7, + 63 + ] + ], + "subsets_checked": 256 + }, + "root_remainders": { + "directions_checked": 120, + "minimum_nonzero_deletion": 24, + "size": 56 + }, + "schema_version": 1 + }, + "independent_geometry_controls": 5, + "schema_version": 1, + "scientific_sha256": { + "EXTENSION.md": "47f86fca33843bb2bc2b5ddbc07b91d846fe04952b8c133ff02dcbb9637b6357", + "PROOF.md": "531b1dcb0de5f652fa2ca8dca97174c4973face53c877bd919cf584afa632953", + "algebra_check.py": "45dad6b59a4fad6d2ccf6c6d7f726e5f9813f03e9ff1f33e84107797ca7bc040", + "extension_check.py": "a246c10ab650b46c13ec86ddc814306338ac84c65a93e2c6cda45c2fcf8c5b70", + "formal/RootSwapConnectedCover.lean": "9205ffe7c3ee68e7ade608631378ebb9e8d8f3e28d6c873de9cbdd7b1becf9b2", + "formal/RootSwapOneExceptional.lean": "7c506e82ccef28ec502eb7bcf214450c23b9decbd38c94d9b5b1fe66b81834a9", + "formal/RootSwapQuartet.lean": "43edf0c90eba5ba805b691cd0b36b8b1e8abc5f80519a5ee1e5cc163bfd8a3e6", + "geometry_audit.py": "dc6c51d1a9376498d35dd35f8f24eb33c2c461656b249a76bf6c41ec3cac91ad", + "verify.py": "ff2e84dd385490434435b871216044700bc949d00c7ea351fe91af5b07bb0217" + } +} diff --git a/research/e8-d0-root-swaps/SOURCES.json b/research/e8-d0-root-swaps/SOURCES.json new file mode 100644 index 0000000000..ea708fffd5 --- /dev/null +++ b/research/e8-d0-root-swaps/SOURCES.json @@ -0,0 +1,178 @@ +{ + "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/root-unit-decoder-lemmas/README.md", + "usage": "provenance", + "pin": "head:08e134b4a0c7f04869dae703f2a2e688e53c44f0:research/root-unit-decoder-lemmas/README.md", + "git_blob": "de305484c78226a3f8da5f3277ced78974116fbb", + "sha256": "e3c856bc361a57cc2424c829001dba94e8f3a1bc8f6616f9c2f740e9665506a9", + "source": "https://github.com/CrocSwap/integer-mult-bounds/pull/1590", + "contributor": "DreamingOfClouds", + "role": "Two-factor fitting lemma A; finite-order field extension is proved here." + }, + { + "path": "research/one-sided-decoders-all-m/README.md", + "usage": "provenance", + "pin": "head:4c32ac3b88d63ad06d2b30e526aa07a12929db36:research/one-sided-decoders-all-m/README.md", + "git_blob": "614ff7397c3510ca740b09bf8846034fef16fa13", + "sha256": "7c22a8d73d8e2cf1ec9ce259035fe97be7261b0f71d5555ee50fc4b821872bf8", + "source": "https://github.com/CrocSwap/integer-mult-bounds/pull/2816", + "contributor": "DreamingOfClouds", + "role": "One-sided lift model, greedy peeling and classical parabolic intersection argument C3." + }, + { + "path": "research/one-sided-decoders-all-m/data/data.json", + "usage": "provenance", + "pin": "head:4c32ac3b88d63ad06d2b30e526aa07a12929db36:research/one-sided-decoders-all-m/data/data.json", + "git_blob": "2b799f9238d11018edb2aa6ac542024dfabcb1b3", + "sha256": "8e4b2a306dfe3499b9d2104753a4cb203e14fbfa94fda03f6a415da956ba642b", + "source": "https://github.com/CrocSwap/integer-mult-bounds/pull/2816", + "contributor": "DreamingOfClouds", + "role": "Literal frame/root chart; provenance only, no imported executable." + }, + { + "path": "research/one-sided-excess-three/README.md", + "usage": "provenance", + "pin": "head:18f7d4da808edb82d32e2081f869b8c993eca891:research/one-sided-excess-three/README.md", + "git_blob": "b8d8f987ca2235f6a8bc491441c689192f8a38ec", + "sha256": "3d53f0d808523baf07e1fefae5b15a2633d7662f864edbfea165f4b099316475", + "source": "https://github.com/CrocSwap/integer-mult-bounds/pull/2862", + "contributor": "DreamingOfClouds", + "role": "Restricted carrier predecessor through kappa<=3; comparison boundary." + }, + { + "path": "research/one-sided-padding-audit/PROOF.md", + "usage": "provenance", + "pin": "head:41826461eaceb25b77c026148b50b884e3c9780e:research/one-sided-padding-audit/PROOF.md", + "git_blob": "986e4b9464a5c2d0ec3455c45cd8e5551c5db43d", + "sha256": "5b8ef47091aaf09610b66194d834afa6724f0b8cadcf582a25705bc6933c35b7", + "source": "https://github.com/CrocSwap/integer-mult-bounds/pull/3095", + "contributor": "CubeJerry", + "role": "Exact full/P112 support chart and field/normalization boundary; no certificates imported." + }, + { + "path": "formal/lean/lean-toolchain", + "usage": "provenance", + "git_blob": "980709bbbae28702ec58c368b84fdf6638093c63", + "sha256": "d24fed434d3b13adfaab57724a0a7f270ea8bf1c818b5ae5cf25cbce24dd685c", + "role": "Pinned optional Lean verification environment; not a Python replay dependency." + }, + { + "path": "formal/lean/lakefile.toml", + "usage": "provenance", + "git_blob": "b6abf04c93acf5ec745aa06aa1b503575b454186", + "sha256": "e5b1a6ff207cdd5e64b04ebfd944274d0ccde896f415bb578deb6090b4175ed5", + "role": "Pinned optional Lean verification environment; not a Python replay dependency." + }, + { + "path": "formal/lean/lake-manifest.json", + "usage": "provenance", + "git_blob": "36433bd6697cc16c39ff03acf97431386cb0f2c2", + "sha256": "702bd5bcfbf4a4739bea2e1cba72b471e8f0680520c67547f5daf3d0f26b6ddf", + "role": "Pinned optional Lean verification environment; not a Python replay dependency." + } + ], + "source_binding": { + "model": "D8 plus half-integral E8, squared root norm 2; the full 120-root-line set and literal PR2816 ordered frame.", + "reuse": "All roots, labels, parabolics and normal profiles are regenerated; no predecessor census, PASS receipt or numerical linear-algebra result is a live input.", + "classical_facts": "Even unimodular E8 lattice of minimum norm 2; Weyl chamber/parabolic classification as stated and credited in PR2816 C3.", + "chart_check": "Exact rational comparison: all 120 E8 lines, all 112 nonframe lines and all 8 ordered frame representatives match the pinned PR2816 chart." + }, + "related_work": [ + { + "path": "research/one-sided-residue-closures/README.md", + "git_blob": "f59ffdc7189d4107483064d7644254efec45c67c", + "sha256": "a72e954568dcd4c95e486c478f7db97187385c0eb618dcfbc252ebb8c06326ed", + "source": "https://github.com/CrocSwap/integer-mult-bounds/pull/2985", + "contributor": "DreamingOfClouds", + "role": "Full-E8 residue and geometric-cap context; no ledger kills imported.", + "head": "b07b0e3226bcbe32a90c1b43ab225c339086f7b5", + "status": "Documentary citation only; unmerged head, not an imported theorem or executable input. Hash checked locally; generic replay does not fetch or validate this external head." + }, + { + "path": "research/one-sided-residue-closures/checks/gtab.py", + "git_blob": "104a4a872617615178112a5ebebdd8842e096701", + "sha256": "12e15b34873cd8ab8ef9ab6c7183711ade2e7fd3d0f2b10d7db8892d6db00393", + "source": "https://github.com/CrocSwap/integer-mult-bounds/pull/2985", + "contributor": "DreamingOfClouds", + "role": "Confirms that the predecessor cap domain is full E8; no code copied or executed.", + "head": "b07b0e3226bcbe32a90c1b43ab225c339086f7b5", + "status": "Documentary citation only; unmerged head, not an imported theorem or executable input. Hash checked locally; generic replay does not fetch or validate this external head." + }, + { + "path": "research/one-sided-padding-lemma/README.md", + "git_blob": "9fca2bc3897ab41120bcebf21aa5b963a55768ac", + "sha256": "b056475ca54f685a26ff1de6ad2986fd31c4d448e02bac428afd85b9cd2443d1", + "source": "https://github.com/CrocSwap/integer-mult-bounds/pull/3074", + "contributor": "DreamingOfClouds", + "role": "Exact open d=0 nonzero-kernel obligation and downstream padding boundary.", + "head": "3cc41f260c31052c933d0e75ea02f2b7677e780c", + "status": "Documentary citation only; unmerged head, not an imported theorem or executable input. Hash checked locally; generic replay does not fetch or validate this external head." + }, + { + "path": "research/p112-reduction-to-conjectures/CONJECTURES.md", + "git_blob": "4d41043842b30f4f741caf198f72d2920b70d382", + "sha256": "998a97f29bffbf4d2cfa8a0f36f4ce1e2759d992b1158b794cce58cabd796791", + "source": "https://github.com/CrocSwap/integer-mult-bounds/pull/3154", + "contributor": "DreamingOfClouds", + "role": "Fresh C7 statement and separation from C1-C6; other closure claims are unimported and unaudited.", + "head": "708f0ad8928c383de8294aea3c126e9461d2066d", + "status": "Documentary citation only; unmerged head, not an imported theorem or executable input. Hash checked locally; generic replay does not fetch or validate this external head." + }, + { + "path": "research/p112-reduction-to-conjectures/checks/L120D0/NOTES.md", + "git_blob": "5cb8ec47c8e86407cb012dd09d4e45c4f8b944b6", + "sha256": "fbd8caf1e697f2bd14f69f4a05b18be8c0113ffa97d8ac31a0d7c6bc23bcab20", + "source": "https://github.com/CrocSwap/integer-mult-bounds/pull/3154", + "contributor": "DreamingOfClouds", + "role": "C7 exact inherited model and nonzero-kernel case in Section 4; alternative-frame lead not used.", + "head": "708f0ad8928c383de8294aea3c126e9461d2066d", + "status": "Documentary citation only; unmerged head, not an imported theorem or executable input. Hash checked locally; generic replay does not fetch or validate this external head." + }, + { + "path": "research/p112-reduction-to-conjectures/checks/CONJG2/NOTES.md", + "git_blob": "6de90e8f0f0d80cad1c1228d8cd3f19d8f1569be", + "sha256": "0e2a78bd38f68fcfbf922c6eb6485b7f114c856a0db416d8f6823c5ebdc67740", + "source": "https://github.com/CrocSwap/integer-mult-bounds/pull/3154", + "contributor": "DreamingOfClouds", + "head": "708f0ad8928c383de8294aea3c126e9461d2066d", + "role": "Conditional C1 premises: d=0 rigid basis shape, N8 and weight-eight high directions; source of the Section 2(ii) obligation resolved at kappa<=7.", + "status": "Documentary citation only; unmerged head. Its model premises are assumed explicitly in EXTENSION.md; the broader reduction is not imported or independently validated." + }, + { + "path": "research/p112-reduction-to-conjectures/checks/CONJ-G/NOTES.md", + "git_blob": "fe45a56747f1bf91805e79283abe5c4279d9acae", + "sha256": "8609121fe3d6c0fbab5c2fbdfbd87fffb20a91452f1d3bcc3d0697a9b3dfabf8", + "source": "https://github.com/CrocSwap/integer-mult-bounds/pull/3154", + "contributor": "DreamingOfClouds", + "head": "708f0ad8928c383de8294aea3c126e9461d2066d", + "role": "Conditional C1 premises: corrected-row duality, corrected ledger, pivot rebate and F1 support identities.", + "status": "Documentary citation only; unmerged head. Its model premises are assumed explicitly in EXTENSION.md; the broader reduction is not imported or independently validated." + }, + { + "path": "research/p112-reduction-to-conjectures/checks/CONJ-G/f1.py", + "git_blob": "d4b294328062390b4fe3224040c57226746c8fc4", + "sha256": "4c995d4a58809f0c297c44809ec488b99e2bb11bb5a64c1818adcc2f58bde0e5", + "source": "https://github.com/CrocSwap/integer-mult-bounds/pull/3154", + "contributor": "DreamingOfClouds", + "head": "708f0ad8928c383de8294aea3c126e9461d2066d", + "role": "Documentary definition of O_v from the complement and cardinality assertions at lines 2 and 10-12; no executable imported.", + "status": "Documentary citation only; unmerged head, checked locally. The local replay constructs O_v afresh and does not execute this source checker or its imports." + } + ], + "provenance_boundary": "The registered validator authenticates files against reachable Git objects. related_work records exact documentary citations outside the base ancestry; these rows are not replay dependencies or a claim of CI source validation." +} diff --git a/research/e8-d0-root-swaps/TASK.json b/research/e8-d0-root-swaps/TASK.json new file mode 100644 index 0000000000..5692dd896c --- /dev/null +++ b/research/e8-d0-root-swaps/TASK.json @@ -0,0 +1,189 @@ +{ + "schema_version": 1, + "task_id": "complex-rank-shape-decoder", + "priority_revision": 6, + "base_commit": "997e6a9ca7b4f95d50e366f61412fd640d72a88a", + "original_card": { + "id": "complex-rank-shape-decoder", + "question": "Can a decoder deliver the local paid mass in fewer, larger-rank children (block frame climbs instead of rank-1 to rank-3 steps)?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/complex-local-word-ceiling/README.md", + "research/complex-decoder-field-extension-seed44/README.md", + "research/complex-frame-pair-decoders/README.md", + "research/selected-k8-unrestricted-ends/README.md", + "research/eisenstein-reduction-copy-floor/README.md" + ], + "methods": [ + "Find one exact small decoding identity whose frame path climbs in blocks, and price its complete per-call profile.", + "Bound the best effective child rank achievable for one fixed support alphabet, including copies, frames and restoration." + ], + "acceptance_gate": "A per-call local profile, with all copied information, frames and restoration counted, whose ceiling exceeds the selected word's by at least 5%; masked or overcomplete supports must change an assumption of the eight-term all-pairs bound. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "research/complex-local-word-ceiling/verify.py" + ], + "expected": "PASS_COMPLEX_LOCAL_WORD_CEILING", + "inspect": "Read the selected word's per-call local profile, its packing ceiling and the lever table; run levers.py for the ideal budget of the lever you target.", + "scope": "Positive control and planning budget only; this is not a new construction or full cold replay." + }, + "first_experiment": "Before any synthesis, write the candidate per-call local profile (and centre charge / unpaid coordinates if changed) and screen it with ceiling.ceiling(); reject it if even the ideal ceiling does not beat the selected word's by your stated margin. Ideal budget: rank-16 delivery is 2.31x (levers.py).", + "bottleneck_link": "Rank-1 children are about half of recursive cost; the selected word's effective child rank is about 3.9. Larger-rank delivery lowers recursive cost per unit of paid mass.", + "allowed_variations": [ + "One masked, overcomplete or block decoder family with exact labels and supports.", + "A scoped lower bound on effective rank for one alphabet.", + "If the coverage law, template or guard changes, derive an applicable fully charged replacement bound instead of applying the incumbent ceiling outside its scope." + ], + "scope_change_triggers": [ + "Repacking idle remainders of an unchanged word (covered by the packing ceiling).", + "Repeating the eight-term all-pairs search inside its proved scope.", + "Only changing helper terminal subspaces and monotone frames within the fixed scalar word, entrances and cleanup contract already covered by #1995/#2013.", + "Searching below C=40 in the #2017 Eisenstein binary scalar-rectangle or fixed-support block-linear additive pairing model; specify a changed premise instead. This bound does not cover every complex decoder.", + "Continuing a partial cost improvement while leaving the same unpriced consumer, restoration or central-readout obligation unresolved; refresh the family expansion decision first. Local product-retiming evidence has a narrow scope and is not a ban on changed graphs or contracts." + ], + "overlap_terms": [ + "rank shape", + "block climb", + "masked decoder", + "overcomplete", + "effective rank" + ] + }, + "scope_status": "changed", + "actual_scope": "Prove C7: the full-E8 d=0 nonzero-kernel cost floor. Strengthen the P112 root-only filter to dimension at least two and cost at most seven, resolving CONJG2 Section 2(ii) at kappa<=7. Under PR3154's inherited rigid-shape and ledger assumptions, close the C1 d=0 invoice cases with actual total seven, or total eight and minimum cost at most seven or minimum profile (7,1). Prove sharp F1 support bound 24, retain its support-25 counterexample, and discharge F1 for every surviving d=0 rigid candidate with corrected invoice at most 64.", + "scope_change_reason": "The donor selected this named proof obligation after a deeper read-only opportunity/overlap review. This is a scoped decoder lower-bound contribution, rather than a positive larger-rank child construction from the original card.", + "bottleneck_link": "Closes one identified assumption in the one-sided decoder-floor program. It constrains the named dense-pairing/Gram model; it does not construct a supplier or improve the selected multiplication exponent.", + "budget_minutes": 60, + "stop_rule": "Complete and independently audit these scoped C7/C1 proofs, exact geometric certificates and actual boundary examples; verify the partial Lean cores and final local submission bytes. Retain other C1 cases, C2-C6 and complete formalization as open.", + "outcome": "completed", + "evidence": "PROOF.md Theorems A/B; EXTENSION.md Theorems C/E/F and Corollary D. Two exact coordinate methods used as an internal cross-check, with direct dimension-eight cap-64 checks; 13 coefficient spaces and 42 swap witnesses; exhaustive quartets; seven sharp kernel bases; 56 connected-deletion certificates; sharp root-only and F1 boundaries; 57,120 frame-plane cases per model and the 168>148 incidence contradiction; three checked Lean cores. Registered replay recomputes RESULT.json.", + "author": "conorholds", + "ai_assistance": "Substantial OpenAI Codex assistance, including GPT-6.1 SOL agents at xHigh reasoning for independent geometry, exact algebra, proof audits and partial Lean formalization. No independent human review or complete formal-kernel certification is claimed.", + "open_questions": [ + { + "question": "Can the remaining C1 actual-total-eight profiles (6,2),(5,3),(4,4), other dimensions and smaller-total pivot cases be closed?", + "why_it_matters": "Under the inherited shape and ledger assumptions, the Sigma=7 branch, Sigma=8 with minimum cost<=7 or minimum profile(7,1), CONJG2 Section 2(ii) at kappa<=7, and residual d=0 low-invoice F1 are closed. Other C1 cases and the broader reduction remain open.", + "first_step": "For an actual-total-eight minimum profile other than (7,1), retain the distinct frame-dual rows and full shared correction space; identify its low-dimensional normal strata and charge simultaneous cancellations before attempting a complete decoder.", + "blocked_by": "A genuine nonroot carrying member already exists in a dimension-two cost-eight correction space; the complete decoder conditions still need analysis." + }, + { + "question": "Can the complete E8/Theorem A/C7 argument be formalized in the existing Lean project?", + "why_it_matters": "The three checked abstract coefficient/covering cores cover substantive cases but do not certify the complete theorem.", + "first_step": "Instantiate the root and label pairing hypotheses, then connect geometric support-rank classification to the checked one-exception bound.", + "blocked_by": "E8 instantiation, exceptional classification, two-factor and high-overlap cases, geometric bounds and final weighted-basis assembly remain outside Lean." + }, + { + "question": "Can C6 (DEG2), the remaining conditional one-sided row in PR3154, be resolved and its complete reduction independently audited?", + "why_it_matters": "PR3154 claims its other ledger rows closed and retains C6/C7 on the one-sided track. This package closes C7 and scoped C1 inputs, and validates none of the other claimed ledger closures.", + "first_step": "Read PR3154 CONJECTURES.md C6 and DEG2 notes; retain actual coefficients in the fourth/fifth-flat extension for the coverable triples and unfinished orbit representative, with a separate checker.", + "blocked_by": "The finite extension and independent C6 check are unfinished there, and the broader imported reduction needs its own audit." + } + ], + "coordination": { + "publication_status": "local-only; no public claim or Discussion update posted; explicit donor approval is required for every upstream action.", + "base_checked": "2026-10-17T13:13:42Z", + "overlap_snapshot": { + "open_prs_at": "2026-10-17T13:13:56.508883+00:00", + "open_pr_records": 283, + "discussions_at": "2026-10-17T13:14:26.599149+00:00", + "discussion_records": 1932, + "closed_prs_at": "2026-10-17T13:14:47.647315+00:00", + "closed_pr_records": 2556, + "pagination": "Complete for all three cached feeds. Searched titles/bodies and Discussion comments/replies; not every PR diff or arbitrary PR comment.", + "terms": [ + "L120", + "d=0", + "root swap", + "root-swap", + "nonzero kernel", + "cost seven", + "C7" + ], + "finding": "PR3154 and Discussion3156 retain C7 and broader C1. No matching completion of C7 or the exact scoped C1 results found. New PR3161/3162/3163 and active structured-support beta work concern C5. DreamingOfClouds announced a PR3154 follow-up consolidating C5 results and claimed C6, expressly leaving C1-C4 and C7 open." + }, + "targeted_checks": "PR3154 remains open at 708f0ad8928c383de8294aea3c126e9461d2066d. Read PR3161/3162/3163 bodies and every updated Discussion3156 comment/reply, including the consolidation reply and C6 claim. Rechecked pinned CONJG2 Section 2 and CONJ-G notes/checker for the new explicit Section 2(ii) consequence and O_v definition. A separate read-only GPT-6.1 SOL xHigh source/scope review confirmed those applications.", + "final_base": "Canonical origin/main fetched at 13:13 UTC and remains 997e6a9ca7b4f95d50e366f61412fd640d72a88a, priority revision 6.", + "canonical_handoff": "https://github.com/CrocSwap/integer-mult-bounds/discussions/3156", + "adjacent_work": [ + { + "pr": 3158, + "head": "8e2167bac550bd653bb74c50c1f7c3f14b6c1f70", + "contributor": "Nick Petalas", + "scope": "C5 separate-versus-common deletion quantifier fixture; does not close C7 or the Sigma=7 C1 subcase." + }, + { + "pr": 3160, + "head": "9ab8c4cc2aed4a87293d7d04b2abfdf854ae43e2", + "scope": "C5 sharp common-four-deletion span for two fixed spaces; separate from the coefficient-space theorem here." + }, + { + "pr": 3161, + "head": "a1aba8389b87412e6f72ccf4d11f31e0ea232327", + "scope": "C5: pinned TWOSIDE (5,3) beta residue; distinct from C7 and the scoped C1 claims." + }, + { + "pr": 3162, + "head": "ebd7fd275288e4a9f658e77fa77a0119a8322e74", + "scope": "C5: ten-deletion span bound and one further TWOSIDE (5,4) exclusion." + }, + { + "pr": 3163, + "head": "89419106cd86896c366e853795978f1bc85f9112", + "scope": "C5: complete fixed-first-space rank-seven common-four-deletion calibration slice." + } + ], + "active_consolidation": { + "url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/3156#discussioncomment-18998364", + "updated_at": "2026-10-17T12:31:37Z", + "scope": "DreamingOfClouds plans to fold the adjacent C5 results into a follow-up to PR3154. No C1 or C7 completion announced." + }, + "active_c6_claim": { + "url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/3156#discussioncomment-18998639", + "updated_at": "2026-10-17T12:57:25Z", + "scope": "DreamingOfClouds takes C6 and explicitly leaves C1-C4 and C7 open. Coordinate before duplicating C6." + }, + "coordination_required_before_publication": "A scoped pointer to the active Discussion3156 thread is still pending donor approval. No public post or claim has been made; publication and Discussion coordination require separate explicit authorization." + }, + "family_expansion_decision": "A named open proof obligation, with no new synthesis/search family, copied-profile saving, consumer assumption or frontier admission. No construction expansion is proposed.", + "validation": { + "registered_replay": { + "python": "CPython 3.12.11", + "elapsed_seconds": 8.397, + "status": "PASS" + }, + "optimized_export": "Audit-fixed read-only Git-free CPython 3.12.11 export passed with -I -O -B -Werror in 7.967 seconds.", + "additional_local_probes": "Original receipt/source/overwrite controls and five mathematical extension mutants are retained as earlier evidence for unchanged components. After the audit fixes, cap-65 source mutants in both coordinate methods were rejected by their dimension-eight mathematical guards under optimized Python, before any receipt/hash comparison. The updated registered replay and read-only Git-free optimized export passed. Independent Cartesian-shell F1 reconstruction and full nonframe delete-one plane checks remain earlier unchanged-source evidence.", + "not_run": [ + "Hosted CI", + "Complete E8/Theorem A/C7 proof-assistant checking", + "Predecessor long DP/LP/RRC/SAT suites" + ], + "partial_lean": { + "status": "PASS", + "lean": "4.21.0", + "mathlib_commit": "308445d7985027f538e281e18df29ca16ede2ba3", + "files": [ + "formal/RootSwapOneExceptional.lean", + "formal/RootSwapQuartet.lean", + "formal/RootSwapConnectedCover.lean" + ], + "axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "boundary": "Abstract coefficient and connected-cover cores only; explicit pairing/support/connectedness hypotheses, no E8 instantiation or complete C7 formalization. Exact compiled source bytes are bound by RESULT.json. Checked in a private toolchain with the repository mathlib pins, not the full repository Lean build. All three files remain byte-identical to the independently audited candidate; their successful compilation is reused, not rerun for the prose/cap-check fixes." + }, + "separate_ai_audit": "The donor supplied a read-only audit of cfd99f9b3cd5093fe142418f1ca1c1f20d4ce090. It reported independent reconstruction of all finite inputs without candidate-code imports, agreement on all theorem implications, and successful replay and Lean checks. Its two additional AI reviewers found no demonstrated error. This is separate AI evidence, not independent human review; the author's two-model implementations remain an internal cross-check." + }, + "budget_note": "The donor requested a full 60-minute round; a final profile exclusion discovered near the checkpoint was audited and verified to completion before stopping.", + "inherited_c1_premises": [ + "PR3154 normalized tight decoder, d=0 rigid basis shape and high-member duality; dim(T) in {2,3}.", + "Corrected ledger cost(D') = sum_j w(A_j) - n_c.", + "Pivot rebate epsilon_k in {0,1}.", + "N8: n_c<=8 and distinct corrected frame indices.", + "These are conditional model premises, not independently validated closures of PR3154's broader reduction. Minimum cost kappa remains distinct from actual low-basis total Sigma." + ] +} diff --git a/research/e8-d0-root-swaps/VERIFY.json b/research/e8-d0-root-swaps/VERIFY.json new file mode 100644 index 0000000000..1def30a7f7 --- /dev/null +++ b/research/e8-d0-root-swaps/VERIFY.json @@ -0,0 +1,19 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Recompute geometry by Euclidean and Cartan/Weyl methods; shared-coefficient swaps, sharp kernel bases and exceptional quartets; cost-seven connected deletions, sharp boundary fixtures, F1 threshold24 and exhaustive frame-plane no-coloop certificates; 18 rejection controls; source-hash comparison. Lean source bytes are bound but Lean is run separately." + } + ] +} diff --git a/research/e8-d0-root-swaps/algebra_check.py b/research/e8-d0-root-swaps/algebra_check.py new file mode 100644 index 0000000000..b108bbd226 --- /dev/null +++ b/research/e8-d0-root-swaps/algebra_check.py @@ -0,0 +1,664 @@ +#!/usr/bin/env python3 +"""Independent finite algebra checks for the weighted exact-root-swap theorem. + +Prepared by conorholds with substantial OpenAI Codex assistance. Apache-2.0. +Credits: DreamingOfClouds/#1590 (two-total lemma), #2816/#2862 (root-swap +and carrier framework), and the retained E8/root-code predecessor lineage. + +This file imports no primary checker or generated certificate. Its fixtures +corroborate the written theorem; they do not enumerate all coefficient spaces. +The theorem concerns exact swaps. Converting general weight-eight vectors to +swaps requires the package's separately stated geometric bridge hypotheses. +""" + +from __future__ import annotations + +from collections import defaultdict +from dataclasses import dataclass +from fractions import Fraction +from itertools import combinations, product +import json + + +class CheckError(ValueError): + """A mathematical or coverage condition failed.""" + + +def require(condition: bool, message: str) -> None: + if not condition: + raise CheckError(message) + + +@dataclass(frozen=True) +class Gaussian: + """An exact element of Q(i), also used for rational fixtures.""" + + real: Fraction = Fraction(0) + imag: Fraction = Fraction(0) + + def __post_init__(self) -> None: + object.__setattr__(self, "real", Fraction(self.real)) + object.__setattr__(self, "imag", Fraction(self.imag)) + + @staticmethod + def of(value: object) -> Gaussian: + if isinstance(value, Gaussian): + return value + return Gaussian(Fraction(value)) + + def __add__(self, other: object) -> Gaussian: + z = self.of(other) + return Gaussian(self.real + z.real, self.imag + z.imag) + + __radd__ = __add__ + + def __neg__(self) -> Gaussian: + return Gaussian(-self.real, -self.imag) + + def __sub__(self, other: object) -> Gaussian: + return self + (-self.of(other)) + + def __rsub__(self, other: object) -> Gaussian: + return self.of(other) - self + + def __mul__(self, other: object) -> Gaussian: + z = self.of(other) + return Gaussian( + self.real * z.real - self.imag * z.imag, + self.real * z.imag + self.imag * z.real, + ) + + __rmul__ = __mul__ + + def __truediv__(self, other: object) -> Gaussian: + z = self.of(other) + norm = z.real * z.real + z.imag * z.imag + if not norm: + raise ZeroDivisionError("division by zero in Q(i)") + return self * Gaussian(z.real / norm, -z.imag / norm) + + def __bool__(self) -> bool: + return bool(self.real or self.imag) + + +ZERO = Gaussian() +ONE = Gaussian(1) +I = Gaussian(0, 1) +Vector = tuple[Gaussian, ...] +Root = tuple[int, ...] # doubled ordinary Euclidean E8 coordinates + + +def solve_columns(columns: list[Vector], target: Vector) -> tuple[Gaussian, ...] | None: + """Solve the actual shared coefficient equations; free variables are zero.""" + require(all(len(c) == len(target) for c in columns), "column shape") + width = len(columns) + rows = [[c[r] for c in columns] + [target[r]] for r in range(len(target))] + pivot_rows: list[tuple[int, int]] = [] + row = 0 + for col in range(width): + pivot = next((r for r in range(row, len(rows)) if rows[r][col]), None) + if pivot is None: + continue + rows[row], rows[pivot] = rows[pivot], rows[row] + scale = rows[row][col] + rows[row] = [x / scale for x in rows[row]] + for r in range(len(rows)): + if r != row and rows[r][col]: + scale = rows[r][col] + rows[r] = [x - scale * y for x, y in zip(rows[r], rows[row])] + pivot_rows.append((row, col)) + row += 1 + if any(not any(r[:width]) and r[-1] for r in rows): + return None + answer = [ZERO] * width + for r, col in pivot_rows: + answer[col] = rows[r][-1] + require( + all(sum((answer[j] * columns[j][r] for j in range(width)), ZERO) == target[r] + for r in range(len(target))), + "coefficient reconstruction", + ) + return tuple(answer) + + +def rational_rank(rows: list[tuple[int, ...]] | list[list[Fraction]]) -> int: + if not rows: + return 0 + a = [[Fraction(x) for x in row] for row in rows] + pivot = 0 + for col in range(len(a[0])): + at = next((j for j in range(pivot, len(a)) if a[j][col]), None) + if at is None: + continue + a[pivot], a[at] = a[at], a[pivot] + scale = a[pivot][col] + a[pivot] = [x / scale for x in a[pivot]] + for j in range(pivot + 1, len(a)): + scale = a[j][col] + if scale: + a[j] = [x - scale * y for x, y in zip(a[j], a[pivot])] + pivot += 1 + if pivot == len(a): + break + return pivot + + +def f2_rank(values: list[int]) -> int: + pivots: dict[int, int] = {} + for value in values: + x = value + while x: + at = x.bit_length() - 1 + if at in pivots: + x ^= pivots[at] + else: + pivots[at] = x + break + return len(pivots) + + +def in_f2_span(values: list[int], value: int) -> bool: + return f2_rank(values + [value]) == f2_rank(values) + + +def determinant(matrix: list[list[int]]) -> int: + """Fraction-free Bareiss determinant, including singular controls.""" + a = [row[:] for row in matrix] + if not a: + return 1 + sign, previous = 1, 1 + for col in range(len(a) - 1): + at = next((j for j in range(col, len(a)) if a[j][col]), None) + if at is None: + return 0 + if at != col: + a[col], a[at] = a[at], a[col] + sign = -sign + pivot = a[col][col] + for r in range(col + 1, len(a)): + for c in range(col + 1, len(a)): + numerator = a[r][c] * pivot - a[r][col] * a[col][c] + require(numerator % previous == 0, "Bareiss exact division") + a[r][c] = numerator // previous + a[r][col] = 0 + previous = pivot + return sign * a[-1][-1] + + +def canonical(root: Root) -> Root: + return root if next(x for x in root if x) > 0 else tuple(-x for x in root) + + +def e8_lines() -> tuple[Root, ...]: + roots: set[Root] = set() + for a, b in combinations(range(8), 2): + for sign in (-1, 1): + row = [0] * 8 + row[a], row[b] = 2, 2 * sign + roots.add(tuple(row)) + for signs in product((-1, 1), repeat=8): + if sum(x < 0 for x in signs) % 2 == 0: + roots.add(canonical(signs)) + require(len(roots) == 120, "E8 line inventory") + return tuple(sorted(roots)) + + +def inner(left: Root, right: Root) -> int: + value = sum(x * y for x, y in zip(left, right)) + require(value % 4 == 0, "integral E8 inner product") + return value // 4 + + +def lattice_member(root: Root) -> bool: + if all(x % 2 == 0 for x in root): + return sum(root) % 4 == 0 + return all(x % 2 for x in root) and sum(root) % 4 == 0 + + +class Geometry: + def __init__(self) -> None: + self.roots = e8_lines() + self.index = {r: j for j, r in enumerate(self.roots)} + # An independent D7 + half-root basis. Its Gram determinant is one, + # so inner products with it identify E8/2E8 without a coordinate solve. + basis: list[Root] = [(1,) * 8] + for j in range(1, 7): + row = [0] * 8 + row[j], row[j + 1] = 2, -2 + basis.append(tuple(row)) + basis.append((0, 0, 0, 0, 0, 0, 2, 2)) + gram = [[inner(a, b) for b in basis] for a in basis] + require(determinant(gram) == 1, "unimodular independent label basis") + self.labels = tuple( + 1 | sum((inner(r, b) % 2) << (j + 1) for j, b in enumerate(basis)) + for r in self.roots + ) + require(len(set(self.labels)) == 120, "distinct root labels") + require(all(x & 1 for x in self.labels), "affine labels") + require(f2_rank(list(self.labels)) == 9, "full label rank") + self.gram = tuple(tuple(inner(a, b) for b in self.roots) for a in self.roots) + self.frames = tuple( + self.root_index(tuple(2 if i == 2 * j else 2 * sign if i == 2 * j + 1 else 0 + for i in range(8))) + for j in range(4) for sign in (-1, 1) + ) + require(all(self.gram[a][b] == 0 for a, b in combinations(self.frames, 2)), + "orthogonal frame") + + def root_index(self, root: Root) -> int: + return self.index[canonical(root)] + + def support(self, vector: Vector) -> set[int]: + require(len(vector) == 120, "root vector shape") + return {j for j, x in enumerate(vector) if x} + + def weight(self, vector: Vector) -> int: + return f2_rank([self.labels[j] for j in self.support(vector)]) + + def vector(self, entries: dict[int, object]) -> Vector: + return tuple(Gaussian.of(entries.get(j, 0)) for j in range(120)) + + def root_codeword(self, root: int) -> Vector: + return tuple(Gaussian(x) for x in self.gram[root]) + + +def combine(basis: list[Vector], coefficients: tuple[Gaussian, ...]) -> Vector: + require(len(basis) == len(coefficients), "coefficient count") + return tuple(sum((a * q[j] for a, q in zip(coefficients, basis)), ZERO) + for j in range(120)) + + +def validate_swap(g: Geometry, root: int, tau: Vector) -> None: + require(0 <= root < 120 and len(tau) == 120, "swap shape") + require(tau[root] == ONE, "swap pivot must equal one") + require(all(not tau[s] for s in range(120) if s != root and g.gram[root][s] == 0), + "swap has orthogonal leakage") + actual = tuple(x - 2 * y for x, y in zip(g.root_codeword(root), tau)) + require(g.weight(actual) <= 8, "literal corrected codeword is not weight eight") + + +def root_swap_witnesses( + g: Geometry, basis: list[Vector] +) -> dict[int, tuple[tuple[Gaussian, ...], Vector]]: + """Exact swaps for arbitrary supplied coefficient spaces, not support unions.""" + zero = (ZERO,) * 120 + for j, q in enumerate(basis): + require(len(q) == 120, "basis vector shape") + require(any(q), "zero basis vector") + require(solve_columns(basis[:j], q) is None, "dependent basis") + witnesses = {} + for t in range(120): + constrained = [t] + [s for s in range(120) if s != t and g.gram[t][s] == 0] + columns = [tuple(q[s] for s in constrained) for q in basis] + target = (ONE,) + (ZERO,) * (len(constrained) - 1) + coefficients = solve_columns(columns, target) + if coefficients is not None: + tau = combine(basis, coefficients) if basis else zero + validate_swap(g, t, tau) + witnesses[t] = (coefficients, tau) + return witnesses + + +def independent_roots(g: Geometry, candidates: list[int]) -> list[int]: + chosen: list[int] = [] + for t in candidates: + if rational_rank([g.roots[s] for s in chosen + [t]]) > len(chosen): + chosen.append(t) + return chosen + + +def binary_subrank(g: Geometry, rows: list[int], columns: list[int]) -> int: + return f2_rank([ + sum((int(s == t or g.gram[s][t] == 0)) << j for j, t in enumerate(columns)) + for s in rows + ]) + + +def audit_two_total_fitting( + pairing: list[list[int]], p: list[list[Gaussian]], q: list[list[Gaussian]], + ratio_order: list[Gaussian] | None = None, +) -> dict[str, int]: + """Check all intermediate Lemma A inequalities over Q(i), without ordering it.""" + size = len(pairing) + require(all(len(row) == size for row in pairing), "pairing shape") + require(all(x in (0, 1) for row in pairing for x in row) + and all(pairing[t][t] == 1 for t in range(size)), "binary unit-diagonal pairing") + require(len(p) == len(q) == size and all(len(x) == 2 for x in p + q), "two-total shape") + matrix = [[sum((p[t][j] * q[s][j] for j in range(2)), ZERO) + for s in range(size)] for t in range(size)] + require(all(matrix[t][t] for t in range(size)), "zero fitting diagonal") + require(all(not matrix[t][s] for t in range(size) for s in range(size) + if t != s and pairing[t][s]), "fitting incidence is nonzero") + rsets = [{t for t in range(size) if p[t][j]} for j in range(2)] + asets = [{t for t in range(size) if q[t][j]} for j in range(2)] + dsets = [rsets[j] & asets[j] for j in range(2)] + shared = dsets[0] & dsets[1] + require(dsets[0] | dsets[1] == set(range(size)), "uncovered diagonal") + + def subrank(rows: set[int], columns: set[int]) -> int: + cs = sorted(columns) + return f2_rank([sum(pairing[t][s] << j for j, s in enumerate(cs)) for t in sorted(rows)]) + + ranks = [subrank(rsets[j], asets[j]) for j in range(2)] + shared_rank = subrank(shared, shared) + for j in range(2): + require(ranks[j] >= len(dsets[j] - shared) + shared_rank, "private pivot inequality") + alpha = {t: p[t][0] / p[t][1] for t in shared} + beta = {t: -q[t][1] / q[t][0] for t in shared} + values = list(dict.fromkeys(list(alpha.values()) + list(beta.values()))) + order = values if ratio_order is None else ratio_order + require(len(order) == len(set(order)) and set(order) == set(values), "incomplete ratio order") + positions = {v: j for j, v in enumerate(order)} + less = {t for t in shared if positions[alpha[t]] < positions[beta[t]]} + greater = shared - less + require(all(alpha[t] != beta[t] for t in shared), "tied diagonal ratios") + for subset, key, increasing in [(less, alpha, False), (greater, beta, True)]: + for t in subset: + for s in subset: + if t != s and pairing[t][s]: + require((positions[key[s]] > positions[key[t]]) == increasing, + "finite-order triangular implication") + require(subrank(subset, subset) == len(subset), "triangular block rank") + require(shared_rank >= max(len(less), len(greater)), "shared rank inequality") + require(sum(ranks) >= size, "two-total lower bound") + return {"size": size, "shared": len(shared), "rank_sum": sum(ranks)} + + +def fitting_from_swaps( + g: Geometry, basis: list[Vector], witnesses: dict[int, tuple[tuple[Gaussian, ...], Vector]] +) -> dict[str, int]: + chosen = independent_roots(g, sorted(witnesses)) + require(len(basis) <= 2, "two-total fitting used outside scope") + p = [[basis[j][s] if j < len(basis) else ZERO for j in range(2)] for s in chosen] + q = [[witnesses[t][0][j] if j < len(basis) else ZERO for j in range(2)] for t in chosen] + pairing = [[int(s == t or g.gram[s][t] == 0) for t in chosen] for s in chosen] + result = audit_two_total_fitting(pairing, p, q) + ranks = [] + for j in range(len(basis)): + rows = [s for s in chosen if basis[j][s]] + columns = [t for t in chosen if witnesses[t][0][j]] + ranks.append(binary_subrank(g, rows, columns)) + require(ranks[-1] <= g.weight(basis[j]), "block exceeds actual basis weight") + require(len(chosen) <= sum(ranks), "fitting root-rank consequence") + return result + + +def low_partitions(total: int, maximum: int | None = None) -> list[tuple[int, ...]]: + if total == 0: + return [()] + maximum = min(total, total if maximum is None else maximum) + return [(head,) + tail for head in range(maximum, 0, -1) + for tail in low_partitions(total - head, head)] + + +def check_profile_coverage(profiles: set[tuple[int, ...]]) -> None: + needed = {p for cost in range(1, 8) for p in low_partitions(cost) + if sum(w >= 3 for w in p) >= 2} + require(needed == {(3, 3), (4, 3), (3, 3, 1)}, "low-cost partition derivation") + require(profiles == needed, "incomplete exceptional-profile coverage") + + +def audit_fixture(g: Geometry, name: str, basis: list[Vector], expected_weights: tuple[int, ...], + expected_rank: int | None = None) -> dict[str, object]: + weights = tuple(g.weight(q) for q in basis) + require(weights == expected_weights, f"{name}: incorrect charged weights") + witnesses = root_swap_witnesses(g, basis) + rank = rational_rank([g.roots[t] for t in witnesses]) + cost = sum(weights) + require(rank <= cost, f"{name}: weighted root-swap rank bound") + if expected_rank is not None: + require(rank == expected_rank, f"{name}: actual independent-root rank") + overrank = [j for j, q in enumerate(basis) + if rational_rank([g.roots[t] for t in g.support(q)]) > weights[j]] + outside_count = 0 + if len(overrank) <= 1: + ordinary = [t for j, q in enumerate(basis) if j not in overrank for t in g.support(q)] + o_rank = rational_rank([g.roots[t] for t in ordinary]) + outside = [t for t in witnesses + if rational_rank([g.roots[s] for s in ordinary] + [g.roots[t]]) > o_rank] + outside_count = len(outside) + if overrank: + exception = basis[overrank[0]] + require(all(t in g.support(exception) for t in outside), "outside-O support binding") + require(all(g.gram[s][t] != 0 for s, t in combinations(outside, 2)), + "outside-O roots not pairwise nonorthogonal") + require(f2_rank([g.labels[t] for t in outside]) == len(outside), + "outside-O orthonormal label independence") + require(len(outside) <= weights[overrank[0]], "one-exception rank allowance") + else: + require(not outside, "ordinary pieces generated an outside-O root") + if len(basis) <= 2: + fitting_from_swaps(g, basis, witnesses) + if cost <= 7 and len(overrank) >= 2: + require(tuple(sorted(weights, reverse=True)) in {(3, 3), (4, 3), (3, 3, 1)}, + "missing exceptional proof profile") + if len(basis) == 3: + a, b = (g.support(basis[j]) for j in overrank) + require(len(a) == len(b) == 4, "three-piece exceptional support size") + require(all(g.gram[s][t] == 0 for s, t in combinations(a, 2)), "first orthogonal quartet") + require(all(g.gram[s][t] == 0 for s, t in combinations(b, 2)), "second orthogonal quartet") + ordinary_j = next(j for j in range(3) if j not in overrank) + unit = g.support(basis[ordinary_j]) + require(len(unit) == 1, "ordinary piece is not a unit") + if len(a & b) <= 1: + require(set(witnesses) <= unit, "uncancelled orthogonal quartet coordinate") + else: + require(len(a | b | unit) <= 7, "quartet union exceeds allowance") + return {"name": name, "weights": list(weights), "cost": cost, + "eligible": len(witnesses), "root_rank": rank, "overrank_pieces": len(overrank), + "one_exception_outside_o": outside_count if len(overrank) == 1 else None} + + +def quartet_checks(g: Geometry) -> dict[str, int]: + pairs: dict[int, list[tuple[int, int]]] = defaultdict(list) + for a, b in combinations(range(120), 2): + pairs[g.labels[a] ^ g.labels[b]].append((a, b)) + quartets: set[tuple[int, ...]] = set() + for group in pairs.values(): + for left, right in combinations(group, 2): + if len(set(left + right)) == 4: + quartets.add(tuple(sorted(left + right))) + overrank, signed = 0, 0 + for ids in sorted(quartets): + require(f2_rank([g.labels[j] for j in ids]) == 3, "dependent affine quartet rank") + gram = [[g.gram[a][b] for b in ids] for a in ids] + if determinant(gram): + overrank += 1 + require(all(g.gram[a][b] == 0 for a, b in combinations(ids, 2)), + "overrank quartet is not orthogonal") + for signs in product((-1, 1), repeat=4): + summed = [sum(sign * g.roots[j][c] for sign, j in zip(signs, ids)) for c in range(8)] + require(all(x % 2 == 0 for x in summed), "half-sum integer doubled coordinates") + half = tuple(x // 2 for x in summed) + require(lattice_member(half) and inner(half, half) == 2, "signed E8 half-sum") + signed += 1 + require(overrank > 0 and len(quartets) > overrank, "quartet controls not exercised") + return {"dependent_quartets": len(quartets), "overrank_orthogonal_quartets": overrank, + "signed_half_sums": signed} + + +def kernel_sharpness_checks(g: Geometry) -> list[dict[str, int]]: + """Literal cost-72 bases of C_E plus one through seven frame units. + + Restriction has exactly the P112 root-code space and kernel the displayed + units. The assertion that that code has no weight-at-most-seven vector + uses the separately stated source/geometry theorem, not these fixtures. + """ + code = [g.root_codeword(t) for t in g.frames] + require(rational_rank([g.roots[t] for t in g.frames]) == 8, "frame code basis") + restricted = [t for t in range(120) if t not in g.frames] + reports = [] + for count in range(1, 8): + units = [g.vector({t: 1}) for t in g.frames[:count]] + changed = [tuple(x - 2 * y for x, y in zip(code[j], units[j])) + if j < count else code[j] for j in range(8)] + basis = units + changed + weights = [g.weight(q) for q in basis] + require(weights == [1] * count + [8] * count + [9] * (8 - count), + "literal kernel-sharpness profile") + require(sum(weights) == 72, "literal kernel-sharpness invoice") + require(all(not value.imag for q in basis for value in q), "rational sharpness basis") + full_rank = rational_rank([[x.real for x in q] for q in basis]) + restricted_rank = rational_rank([[q[t].real for t in restricted] for q in basis]) + require(full_rank == 8 + count and restricted_rank == 8, + "literal full/restricted basis dimensions") + for j in range(8): + recovered = tuple(x + 2 * y for x, y in zip(changed[j], units[j])) \ + if j < count else changed[j] + require(recovered == code[j], "literal code containment") + require(tuple(changed[j][t] for t in restricted) + == tuple(code[j][t] for t in restricted), "restriction is the root code") + require(all(not q[t] for q in units for t in restricted), "unit kernel support") + reports.append({"frame_units": count, "full_dimension": full_rank, + "restricted_dimension": restricted_rank, + "kernel_dimension": full_rank - restricted_rank, "basis_cost": sum(weights)}) + return reports + + +def run_checks() -> dict[str, object]: + g = Geometry() + require(I * I == Gaussian(-1), "Q(i) field control") + fixtures: list[dict[str, object]] = [] + rejected = 0 + + def reject(action, name: str) -> None: + nonlocal rejected + try: + action() + except CheckError: + rejected += 1 + else: + raise CheckError(f"negative control accepted: {name}") + + def root(a: int, b: int, sign: int = 1) -> int: + v = [0] * 8 + v[a], v[b] = 2, 2 * sign + return g.root_index(tuple(v)) + + def indicator(ids: list[int] | tuple[int, ...], values: list[object] | None = None) -> Vector: + return g.vector(dict(zip(ids, [1] * len(ids) if values is None else values))) + + first = [root(0, j) for j in (1, 2, 3)] + second = [root(4, j) for j in (5, 6, 7)] + unit = root(0, 4, -1) + fixtures.append(audit_fixture(g, "sharp-3-3-1", [indicator(first), indicator(second), indicator([unit])], + (3, 3, 1), 7)) + fixtures.append(audit_fixture(g, "complex-two-total-sharp", [indicator(first, [1, I, 1 + I]), + indicator(second[:2], [I, 2 - I])], + (3, 2), 5)) + fixtures.append(audit_fixture(g, "two-overrank-3-3", [indicator(g.frames[:4]), indicator(g.frames[4:])], + (3, 3), 0)) + fixtures.append(audit_fixture(g, "two-overrank-3-3-positive", + [indicator(g.frames[:4]), indicator(g.frames[:4], [1, 1, 1, 2])], + (3, 3), 1)) + # A full orthogonal frame has affine label rank four and real rank eight. + fixtures.append(audit_fixture(g, "two-overrank-4-3", [indicator(g.frames), indicator(g.frames[:4], [1, 2, 3, 4])], + (4, 3), 0)) + overlap_one = [ + root(0, 1, -1), root(4, 5, -1), + g.root_index((1, 1, 1, 1, 1, 1, 1, 1)), + g.root_index((1, 1, -1, -1, 1, 1, -1, -1)), + ] + quartet_pairs = { + 0: list(g.frames[4:]), + 1: overlap_one, + 2: list(g.frames[:2]) + list(g.frames[4:6]), + 4: list(g.frames[:4]), + } + for overlap, b in quartet_pairs.items(): + a = list(g.frames[:4]) + require(len(a) == len(b) == 4 and len(set(a) & set(b)) == overlap, "quartet fixture overlap") + fixtures.append(audit_fixture(g, f"orthogonal-3-3-1-overlap-{overlap}", + [indicator(a), indicator(b, [1, 2, 3, 4]), indicator([unit])], + (3, 3, 1))) + fixtures.append(audit_fixture(g, "one-exception-actual-space", + [indicator(g.frames[:4])] + [indicator([j]) for j in g.frames[:3]], + (3, 1, 1, 1), 4)) + independent = independent_roots(g, list(range(120))) + fixtures.append(audit_fixture(g, "sharp-seven-units", [indicator([j]) for j in independent[:7]], + (1,) * 7, 7)) + fixtures.append(audit_fixture(g, "cost-eight-ambient-bound", [indicator([j]) for j in g.frames], + (1,) * 8, 8)) + + old_roots = [ + (0, 0, 0, 0, 0, 2, -2, 0), (0, 0, 0, 0, 0, 2, 0, -2), + (0, 0, 0, 2, 0, -2, 0, 0), (1, -1, -1, -1, -1, 1, -1, -1), + (1, -1, 1, -1, 1, 1, -1, -1), + ] + old_ids = [g.root_index(r) for r in old_roots] + frame = g.root_index((2, 2, 0, 0, 0, 0, 0, 0)) + q5 = indicator(old_ids) + require(g.weight(q5) == 5 and rational_rank(old_roots) == 5, "old carrier actual cost/rank") + require(all(g.gram[a][b] != 0 for a, b in combinations(old_ids, 2)), "old carrier clique") + require(all(g.gram[t][frame] == 0 for t in old_ids), "old carrier frame orthogonality") + xor = 0 + for t in old_ids: + xor ^= g.labels[t] + require(xor == g.labels[frame], "old carrier frame-label relation") + restricted = [s for s in range(120) if s not in g.frames] + + def restricted_weight(v: Vector) -> int: + return f2_rank([g.labels[s] for s in restricted if v[s]]) + + restricted_vectors = [q5] + [tuple(x - 2 * y for x, y in zip(g.root_codeword(t), q5)) for t in old_ids] + carriers = 0 + for vector in restricted_vectors: + labels = [g.labels[s] for s in restricted if vector[s]] + carriers += any(in_f2_span(labels, g.labels[f]) for f in g.frames) + require([restricted_weight(v) for v in restricted_vectors] == [5] + [8] * 5, + "old carrier literal restricted vectors") + require(carriers == 6, "old carrier counterexample not reproduced") + reject(lambda: require(carriers <= 5, "false old carrier count"), "carrier count shortcut") + fixtures.append(audit_fixture(g, "old-carrier-full-rank-control", [q5, indicator([frame])], (5, 1), 6)) + + # Non-orderable coefficient-field test with both private and shared lines. + values = [ONE, I, 1 + I, 2 - I, -1 + I, 3 + 2 * I] + p = [[ONE, ZERO], [ZERO, ONE]] + [[v, ONE] for v in values] + q = [[ONE, ZERO], [ZERO, ONE]] + [[ONE, -values[(j + 1) % len(values)]] for j in range(len(values))] + matrix = [[sum((p[t][j] * q[s][j] for j in range(2)), ZERO) for s in range(8)] for t in range(8)] + pairing = [[int(t == s or not matrix[t][s]) for s in range(8)] for t in range(8)] + complex_lemma = audit_two_total_fitting(pairing, p, q) + audit_two_total_fitting(pairing, p, q, list(reversed(values))) + reject(lambda: audit_two_total_fitting(pairing, p, q, values[:-1]), "incomplete finite order") + wrong_pairing = [row[:] for row in pairing] + row, col = next((t, s) for t in range(8) for s in range(8) + if t != s and matrix[t][s]) + wrong_pairing[row][col] = 1 + reject(lambda: audit_two_total_fitting(wrong_pairing, p, q), "nonzero fitting incidence") + wrong_diagonal = [row[:] for row in pairing] + wrong_diagonal[0][0] = 0 + reject(lambda: audit_two_total_fitting(wrong_diagonal, p, q), "missing pairing diagonal") + + single_quad = [indicator(g.frames[:4])] + actual = root_swap_witnesses(g, single_quad) + require(not actual, "orthogonal support shortcut control") + reject(lambda: require(set(actual) == set(g.frames[:4]), "support is not a coefficient space"), + "support-only eligibility") + tau = indicator([first[0]]) + wrong = list(tau) + orthogonal = next(s for s in range(120) if g.gram[first[0]][s] == 0) + wrong[orthogonal] = ONE + reject(lambda: validate_swap(g, first[0], tuple(wrong)), "orthogonal leakage") + reject(lambda: validate_swap(g, first[0], (ZERO,) * 120), "missing swap pivot") + reject(lambda: root_swap_witnesses(g, [q5, q5]), "dependent purported basis") + reject(lambda: audit_fixture(g, "undercharge", [q5], (4,)), "undercharged basis weight") + profiles = {(3, 3), (4, 3), (3, 3, 1)} + check_profile_coverage(profiles) + reject(lambda: check_profile_coverage(profiles - {(3, 3, 1)}), "incomplete profile list") + quartets = quartet_checks(g) + sharpness = kernel_sharpness_checks(g) + return { + "scope": "finite-independent-algebra-controls-not-an-exhaustion-of-L", + "roots": 120, "coefficient_field": "Q(i)", "fixtures": fixtures, + "eligible_witnesses": sum(int(f["eligible"]) for f in fixtures), + "complex_two_total": complex_lemma, "old_carrier_count": carriers, + "old_carrier_cost": 5, "exception_profiles": [list(p) for p in sorted(profiles)], + "quartets": quartets, "rejected_controls": rejected, + "kernel_sharpness": sharpness, + "cost_ge_8": "root rank at most eight; no counterexample asserted", + } + + +if __name__ == "__main__": + print(json.dumps(run_checks(), sort_keys=True)) + print("PASS_E8_D0_INDEPENDENT_ALGEBRA") diff --git a/research/e8-d0-root-swaps/extension_check.py b/research/e8-d0-root-swaps/extension_check.py new file mode 100644 index 0000000000..659edb7f09 --- /dev/null +++ b/research/e8-d0-root-swaps/extension_check.py @@ -0,0 +1,493 @@ +#!/usr/bin/env python3 +"""Two-model checks for the cost-seven root-only extension and C1 subcase. + +Prepared by conorholds with substantial OpenAI Codex assistance. Apache-2.0. +The model and predecessor geometric reduction are credited in PROOF.md. +This module imports no primary verifier and does not rerun its C7 checks. +""" + +from collections import Counter +from fractions import Fraction +from itertools import combinations, product +import json + +import geometry_audit + + +class ExtensionError(ValueError): + """A mathematical assertion or coverage check failed.""" + + +def need(condition, message): + if not condition: + raise ExtensionError(message) + + +def dot(a, b): + return sum(x * y for x, y in zip(a, b)) + + +def canonical(vector): + return tuple(vector) if next(x for x in vector if x) > 0 else tuple(-x for x in vector) + + +def rank(values): + pivots = {} + for value in values: + while value: + pivot = value.bit_length() - 1 + if pivot in pivots: + value ^= pivots[pivot] + else: + pivots[pivot] = value + break + return len(pivots) + + +def compact_labels(values): + """Coordinates in a basis of the Gram-character image, without an E8 chart.""" + pivots = {} + for value in values: + while value: + pivot = value.bit_length() - 1 + if pivot in pivots: + value ^= pivots[pivot][0] + else: + pivots[pivot] = (value, 1 << len(pivots)) + break + need(len(pivots) == 9, 'Gram-character label image is not nine-dimensional') + result = [] + for value in values: + coordinate = 0 + while value: + basis, bit = pivots[value.bit_length() - 1] + value ^= basis + coordinate ^= bit + result.append(coordinate) + return result + + +def integral_lines(fours, twos): + result = set() + for large in combinations(range(8), fours): + for small in combinations([i for i in range(8) if i not in large], twos): + for signs in product((-1, 1), repeat=fours + twos): + vector = [0] * 8 + for i, sign in zip(large + small, signs): + vector[i] = sign * (4 if i in large else 2) + if sum(vector) % 4 == 0: + result.add(canonical(vector)) + return result + + +def half_lines(count=0, large=3): + result = set() + for positions in combinations(range(8), count): + for signs in product((-1, 1), repeat=8): + vector = tuple(sign * (large if i in positions else 1) for i, sign in enumerate(signs)) + if sum(vector) % 4 == 0: + result.add(canonical(vector)) + return result + + +def simple_supports(roots): + # Only parabolic membership uses this rational basis. Labels below use + # all 120 Gram characters, independently of simple-root coordinates. + 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)) + rows = [[Fraction(simple[j][i]) for j in range(8)] + + [Fraction(i == j) for j in range(8)] for i in range(8)] + for column in range(8): + pivot = next(i for i in range(column, 8) if rows[i][column]) + rows[column], rows[pivot] = rows[pivot], rows[column] + scale = rows[column][column] + rows[column] = [x / scale for x in rows[column]] + for i in range(8): + if i != column: + scale = rows[i][column] + rows[i] = [x - scale * y for x, y in zip(rows[i], rows[column])] + coordinates = [tuple(dot(row[8:], root) for row in rows) for root in roots] + need(all(x.denominator == 1 for row in coordinates for x in row), 'nonintegral root coordinates') + return [sum(1 << i for i, x in enumerate(row) if x) for row in coordinates] + + +def direct_model(): + roots = sorted(integral_lines(0, 2) | half_lines()) + raw = [1 | sum(((dot(root, other) // 4) % 2) << (i + 1) + for i, other in enumerate(roots)) for root in roots] + norm4 = integral_lines(1, 0) | integral_lines(0, 4) | half_lines(1) + norm8 = (integral_lines(2, 0) | integral_lines(1, 4) | integral_lines(0, 8) + | half_lines(3) | half_lines(1, 5)) - {tuple(2 * x for x in r) for r in roots} + return roots, compact_labels(raw), simple_supports(roots), sorted(norm4), sorted(norm8) + + +def cartan_model(): + model = geometry_audit.CartanModel() + pairs = sorted((canonical(model.to_doubled(root)), i) for i, root in enumerate(model.roots)) + roots = [root for root, _ in pairs] + labels = [model.labels[i] for _, i in pairs] + supports = [sum(1 << j for j, x in enumerate(model.roots[i]) if x) for _, i in pairs] + normals = [] + for norm, count in ((4, 1080), (8, 8640)): + seeds = [tuple(model.inverse[i][j] for i in range(8)) for j in range(8)] + seed = next(vector for vector in seeds if model.inner(vector, vector) == norm) + normals.append(sorted(canonical(model.to_doubled(vector)) + for vector in model.vector_orbit(seed, count))) + return roots, labels, supports, *normals + + +def pair_certificate(points, pairs, labels): + need(len(points) == 12 and len(pairs) == 6, 'six-pair certificate cardinality') + need(len({i for pair in pairs for i in pair}) == 12, 'six-pair disjoint cover') + need({i for pair in pairs for i in pair} == set(points), 'six-pair point inventory') + xors = {labels[a] ^ labels[b] for a, b in pairs} + need(len(xors) == 1 and 0 not in xors, 'six-pair common nonzero XOR') + need(rank(labels[i] for i in points) == 7, 'deletion rank seven') + for first, second in combinations(pairs, 2): + need(rank(labels[i] for i in first + second) == 3, 'pair-union four-element circuit') + + +def check_model(model): + roots, labels, supports, norm4, norm8 = model + need(len(roots) == len(set(roots)) == 120 and len(set(labels)) == 120, 'root/label inventory') + need(rank(labels) == 9 and len(norm4) == 1080 and len(norm8) == 8640, 'model dimensions') + need(all(dot(r, r) == 8 for r in roots) and all(dot(h, h) == 16 for h in norm4) + and all(dot(h, h) == 32 for h in norm8), 'root and normal norms') + frame = [] + for sign in (1, -1): + for pair in range(4): + root = [0] * 8 + root[2 * pair], root[2 * pair + 1] = 2, 2 * sign + frame.append(roots.index(tuple(root))) + p = [i for i in range(120) if i not in frame] + p_mask = sum(1 << i for i in p) + index = {root: i for i, root in enumerate(roots)} + cuts = [sum(1 << i for i in p if (normal & labels[i]).bit_count() % 2) + for normal in range(1, 512)] + def mask_points(mask): + while mask: + bit = mask & -mask + yield bit.bit_length() - 1 + mask ^= bit + def off(normal): + return sum(1 << i for i in p if dot(normal, roots[i])) + types = Counter((subset.bit_count(), sum(s & ~subset == 0 for s in supports)) + for subset in range(255)) + large = sorted(key for key in types if key[1] >= 27) + need(large == [(6, 30), (6, 36), (7, 28), (7, 37), (7, 42), (7, 63)] + and all(types[key] == 1 for key in large), 'threshold-27 proper parabolics') + profile = Counter() + critical = {} + fixture = None + for h in norm4: + source = off(h) + for cut in cuts: + deletion = source & cut + if deletion.bit_count() > 21: + continue + points = list(mask_points(deletion)) + r = rank(labels[i] for i in points) + profile[(len(points), r)] += 1 + if r != 7: + continue + need(h not in critical, 'multiple critical cuts for one normal') + need(set(points) == {i for i in p if abs(dot(h, roots[i])) == 8}, 'critical deletion coordinates') + pairs = set() + for i in points: + oriented = roots[i] if dot(h, roots[i]) > 0 else tuple(-x for x in roots[i]) + partner = canonical(tuple(x - y for x, y in zip(h, oriented))) + need(partner in index and index[partner] != i, 'root pair closure') + pairs.add(tuple(sorted((i, index[partner])))) + pairs = sorted(pairs) + pair_certificate(points, pairs, labels) + critical[h] = deletion + if h == (2, 2, 2, 2, 0, 0, 0, 0): + fixture = h, source, deletion, points, pairs + need(profile == Counter({(12, 7): 56, (13, 8): 896, (14, 8): 128}), 'norm-four small-deletion profile') + frame_pairs = {canonical(tuple(x + sign * y for x, y in zip(roots[a], roots[b]))) + for a, b in combinations(frame, 2) for sign in (-1, 1)} + need(set(critical) == frame_pairs and len(frame_pairs) == 56, 'critical normals exactly frame sums/differences') + norm8_extra = Counter() + for h in norm8: + source = off(h) + if source.bit_count() == 85: + norm8_extra[min((source & cut).bit_count() for cut in cuts)] += 1 + need(norm8_extra == Counter({25: 3584}), 'norm-eight Off85 extension') + root_off = [sum(1 << j for j, other in enumerate(roots) if dot(root, other)) for root in roots] + planes = {root_off[i] | root_off[j] for i, j in combinations(range(120), 2) + if not dot(roots[i], roots[j])} + need(len(planes) == 3780, 'orthogonal-root plane inventory') + plane_extra = Counter() + for source in planes: + source &= p_mask + if source.bit_count() == 85: + plane_extra[min((source & cut).bit_count() for cut in cuts)] += 1 + need(plane_extra == Counter({25: 448}), 'orthogonal-plane Off85 extension') + blocks = {frozenset(j for j, f in enumerate(frame) if dot(roots[i], roots[f])) for i in p} + need(len(blocks) == 14 and all(len(block) == 4 for block in blocks), 'nonframe four-incidence') + need(all(len(a & b) % 2 == 0 for a, b in combinations(blocks, 2)), 'even frame-support intersections') + private = {} + for count in (4, 5, 6): + available = [sum(any(block & set(chosen) == {j} for block in blocks) for j in chosen) + for chosen in combinations(range(8), count)] + private[count] = max(available) + need(private == {4: 4, 5: 1, 6: 0}, 'four-private sharp control / five-private exclusion') + need(fixture is not None, 'displayed dimension-one fixture was not checked') + h, source, deletion, points, pairs = fixture + corrected = source ^ deletion + need(dot(h, h) == 16 and rank(labels[i] for i in points) == 7, 'dimension-one cost-seven fixture') + need(all(any(h[i] * r[j] != h[j] * r[i] for i, j in combinations(range(8), 2)) for r in roots), + 'dimension-one direction must be nonroot') + tau = {i: -dot(h, roots[i]) // 4 for i in points} + coefficients = {i: dot(h, roots[i]) // 4 + tau.get(i, 0) for i in p} + need({i for i, value in coefficients.items() if value} == set(mask_points(corrected)), + 'literal correction coefficients') + need(rank(labels[i] for i in mask_points(corrected)) == 8, 'dimension-one corrected weight eight') + need(all(rank([labels[i] for i in mask_points(corrected)] + [labels[t]]) == 9 for t in points), + 'all twelve correction coordinates are essential') + eligible = [t for t in points if all(dot(roots[t], roots[s]) for s in points if s != t)] + need(not eligible, 'dimension-one fixture is not an exact-root-swap counterexample') + hyperplane_basis = [] + for i in mask_points(corrected): + if rank([labels[j] for j in hyperplane_basis] + [labels[i]]) > len(hyperplane_basis): + hyperplane_basis.append(i) + need(len(hyperplane_basis) == 8, 'fixture hyperplane basis') + need(all(rank([labels[i] for i in hyperplane_basis] + [labels[f]]) == 9 for f in frame), + 'fixture hyperplane excludes all frame labels') + # A real cost-eight boundary, not a decoder or a C1 counterexample. + h8 = (2, 2, 2, 0, 2, 0, 0, 0) + unit = index[(0, 0, 2, 0, 2, 0, 0, 0)] + d8 = [i for i in p if abs(dot(h8, roots[i])) == 8] + d0 = [i for i in d8 if i != unit] + need(h8 in norm4 and unit in d8 and len(d8) == 13 and len(d0) == 12, 'cost-eight boundary supports') + need(rank(labels[i] for i in d0) == 7 and rank(labels[i] for i in d8) == 8, + 'cost-eight basis and union lower bound') + q0 = {i: -dot(h8, roots[i]) // 4 for i in d0} + corrected8 = [i for i in p if dot(h8, roots[i]) // 4 + q0.get(i, 0) - 2 * (i == unit)] + alone8 = [i for i in p if dot(h8, roots[i]) // 4 + q0.get(i, 0)] + need(len(corrected8) == 60 and rank(labels[i] for i in corrected8) == 8 + and rank(labels[i] for i in alone8) == 9, 'cost-eight literal corrected weights') + need(set(corrected8) == {i for i in p if (dot(h8, roots[i]) // 4) % 2}, 'cost-eight hyperplane equation') + carrying = [j for j, f in enumerate(frame) if rank([labels[i] for i in corrected8] + [labels[f]]) == 8] + need(carrying == [1, 2, 5, 6] and all(dot(h8, roots[frame[j]]) for j in carrying), + 'cost-eight actual span carries four relevant frame labels') + need(all(any(h8[i] * r[j] != h8[j] * r[i] for i, j in combinations(range(8), 2)) for r in roots), + 'cost-eight boundary direction must be nonroot') + need(min((off(h8) & cut).bit_count() for cut in cuts) == 13, 'cost-eight necessary deletion control') + rejected = 0 + damaged = [pairs[:-1], pairs[:-1] + [pairs[0]], + [(pairs[0][0], pairs[1][0]), (pairs[0][1], pairs[1][1])] + pairs[2:]] + for wrong in damaged: + try: + pair_certificate(points, wrong, labels) + except ExtensionError: + rejected += 1 + need(rejected == 3, 'corrupt pair certificates were accepted') + return {'parabolic_threshold': 27, 'large_proper_types': [list(key) for key in large], + 'norm4_small_deletions': [list(key) + [value] for key, value in sorted(profile.items())], + 'connected_rank7_deletions': len(critical), 'common_xor_pairs_per_deletion': 6, + 'four_circuits_per_deletion': 15, 'norm8_off85': [85, 25, 3584], + 'orthogonal_plane_off85': [85, 25, 448], 'frame_support_blocks': len(blocks), + 'maximum_private_choices': {str(key): value for key, value in private.items()}, + 'dimension_one_fixture': {'h_doubled': list(h), 'tau_support': len(points), + 'tau_weight': 7, 'corrected_weight': 8, 'essential_coordinates': 12, + 'tau_entries': [[list(roots[i]), tau[i]] for i in points], + 'hyperplane_basis_doubled': [list(roots[i]) for i in hyperplane_basis], + 'hyperplane_carries_frame': False, + 'eligible_root_count': len(eligible)}, + 'dimension_two_cost_eight_fixture': { + 'scope': 'correction-space boundary only', 'h_doubled': list(h8), + 'basis_weights': [7, 1], 'dimension': 2, 'exact_cost': 8, 'union_label_rank': 8, + 'q0_entries': [[list(roots[i]), q0[i]] for i in d0], + 'unit_root_doubled': list(roots[unit]), 'tau_unit_coefficient': -2, + 'tau_support': len(d8), 'q0_alone_corrected_weight': 9, + 'corrected_support': 60, 'corrected_weight': 8, 'carried_frame_indices': carrying}, + 'negative_controls_rejected': rejected} + + +def f1_checks(model, use_cartan): + """Sharp support-cardinality boundary: F1 holds through24, fails at25.""" + roots, labels, supports, norm4, _ = model + frame = [] + for sign in (1, -1): + for j in range(4): + vector = [0] * 8 + vector[2 * j], vector[2 * j + 1] = 2, 2 * sign + frame.append(roots.index(tuple(vector))) + p = [i for i in range(120) if i not in frame] + p_mask = sum(1 << i for i in p) + root_off = [sum(1 << j for j, root in enumerate(roots) if dot(h, root)) for h in roots] + ov = {v: p_mask ^ ((root_off[v] & p_mask) ^ (1 << v)) for v in p} + need(all(mask.bit_count() == 60 for mask in ov.values()), 'F1 orthogonality-set definition') + types = sorted((subset.bit_count(), sum(s & ~subset == 0 for s in supports)) + for subset in range(255) if sum(s & ~subset == 0 for s in supports) >= 35) + need(types == [(6, 36), (7, 37), (7, 42), (7, 63)], 'F1 threshold-35/36 parabolics') + if use_cartan: + cartan = geometry_audit.CartanModel() + seed = next(tuple(cartan.inverse[i][j] for i in range(8)) for j in range(8) + if cartan.inverse[j][j] == 6) + norm6 = [canonical(cartan.to_doubled(h)) for h in cartan.vector_orbit(seed, 3360)] + else: + norm6 = integral_lines(1, 2) | integral_lines(0, 6) | half_lines(2) + need(len(norm6) == 3360 and all(dot(h, h) == 24 for h in norm6), 'F1 norm-six inventory') + minima = {} + relevant6 = 0 + histogram6 = Counter() + for family, normals in ((4, norm4), (6, norm6)): + minimum = 112 + minimum_off = 112 + for h in normals: + source = sum(1 << i for i in p if dot(h, roots[i])) + minimum_off = min(minimum_off, source.bit_count()) + if family == 6 and source.bit_count() > 77: + continue + relevant6 += family == 6 + for v in p: + size = (source & ov[v]).bit_count() + minimum = min(minimum, size) + if family == 6: + histogram6[size] += 1 + minima[family] = (minimum_off, minimum) + need(minima == {4: (70, 30), 6: (77, 25)} and relevant6 == 2688, 'F1 nonroot deletion minima') + planes = {root_off[i] | root_off[j] for i, j in combinations(range(120), 2) if dot(roots[i], roots[j])} + need(len(planes) == 1120 and min((mask & p_mask).bit_count() for mask in planes) == 78, + 'F1 A2-plane minimum support') + root_min = min((root_off[t] & ov[v]).bit_count() for v in p for t in range(120) if t != v) + need(root_min == 26, 'F1 other-root minimum') + h = (0, 0, 0, 2, -4, 0, -2, 0) + v = roots.index((0, 0, 0, 2, 0, 0, 2, 0)) + deletion = [i for i in p if ov[v] >> i & 1 and dot(h, roots[i])] + tau = {i: -dot(h, roots[i]) // 4 for i in deletion} + g = {i: dot(h, roots[i]) // 4 + tau.get(i, 0) for i in p} + actual = [i for i in p if g[i]] + need(h in norm6 and v in p and dot(h, h) == 24 and dot(h, roots[v]) == 0 and len(deletion) == 25, + 'F1 sharp nonroot direction and25-point boundary') + need(all(not g[i] for i in p if ov[v] >> i & 1) and len(actual) == 52 + and rank(labels[i] for i in actual) == 8, 'F1 sharp literal vanishing codeword') + need(rank(labels[i] for i in deletion) == 7 + and all(rank([labels[i] for i in actual] + [labels[t]]) == 9 for t in deletion), + 'F1 all25 boundary correction coordinates essential') + unit = deletion[0] + fixed_rank = rank(labels[i] for i in deletion if i != unit) + need(len(deletion) > 1 and fixed_rank == 7, 'F1 dimension-two independence and exact-cost lower bound') + # U= has basis weights(7,1). Every vector outside the + # unit line retains the24 fixed coordinates of rank7, so cost(U)=8. + # This disproves the unrestricted F1 component at(7,1), not a decoder. + return {'maximum_guaranteed_correction_support': 24, 'parabolic_threshold': 36, + 'large_proper_types': [list(key) for key in types], 'norm4_minimum_required': 30, + 'norm6_minimum_code_support': 77, 'norm6_relevant_objects': relevant6, + 'norm6_deletion_profile': [[size, count] for size, count in sorted(histogram6.items())], + 'a2_plane_minimum_code_support': 78, 'other_root_minimum_required': root_min, + 'sharp_support25_fixture': {'h_doubled': list(h), 'v_doubled': list(roots[v]), + 'tau_entries': [[list(roots[i]), tau[i]] for i in deletion], + 'tau_weight': 7, 'tau_support': 25, 'corrected_support': 52, + 'corrected_weight': 8, 'essential_coordinates': 25, + 'dimension_two_space': {'scope': 'F1 correction-space counterexample only', + 'unit_root_doubled': list(roots[unit]), 'basis_weights': [7, 1], + 'dimension': 2, 'exact_cost': 8, 'fixed_nonunit_support_rank': fixed_rank, + 'union_support': 25, 'cost_at_most7_dimension_two_union_cap': 21}}} + + +def cycle_union(values): + """Return rank and the union of supports of a binary cycle-space basis.""" + pivots, covered = {}, 0 + for i, value in enumerate(values): + dependency = 1 << i + while value: + bit = value.bit_length() - 1 + if bit in pivots: + previous, mask = pivots[bit] + value ^= previous + dependency ^= mask + else: + pivots[bit] = (value, dependency) + break + if not value: + covered |= dependency + return len(pivots), covered + + +def frame_plane_checks(model): + """Exclude non-axis private-frame directions for a(7,1) correction basis.""" + roots, labels, _, _, _ = model + frame = [] + for sign in (1, -1): + for j in range(4): + vector = [0] * 8 + vector[2 * j], vector[2 * j + 1] = 2, 2 * sign + frame.append(roots.index(tuple(vector))) + p = [i for i in range(120) if i not in frame] + cuts = [(normal, sum(1 << i for i in p if (normal & labels[i]).bit_count() % 2)) + for normal in range(1, 512)] + profile, checked = Counter(), set() + cross_checks, frame_minimum, nonroot_cases = 0, 112, 0 + need(cycle_union([1, 2, 3]) == (2, 7) and cycle_union([1, 2, 4]) == (3, 0), + 'cycle-space dependent and independent controls') + for j in range(8): + for k in range(8): + if j == k: + continue + a, b = roots[frame[j]], roots[frame[k]] + strata = {'frame': a, 'plus': tuple(x + y for x, y in zip(a, b)), + 'minus': tuple(x - y for x, y in zip(a, b)), + 'generic': tuple(x + 2 * y for x, y in zip(a, b))} + for name, h in strata.items(): + source = sum(1 << i for i in p if dot(h, roots[i])) + for normal, cut in cuts: + if (normal & labels[frame[j]]).bit_count() % 2: + continue + deletion = source & cut + values = [] + while deletion: + bit = deletion & -deletion + values.append(labels[bit.bit_length() - 1]) + deletion ^= bit + r, covered = cycle_union(values) + all_points = (1 << len(values)) - 1 + after = r if covered == all_points else r - 1 + key = (name, r, after) + profile[key] += 1 + if key not in checked: + direct = [rank(values[:i] + values[i + 1:]) for i in range(len(values))] + need(after == min(direct), 'cycle-union minimum deletion rank') + need(all(direct[i] == r - (not (covered >> i & 1)) for i in range(len(values))), + 'cycle-union pointwise coloop certificate') + checked.add(key) + cross_checks += len(values) + if name == 'frame': + frame_minimum = min(frame_minimum, len(values)) + else: + need(r == 8 and covered == all_points, 'nonroot frame-plane deletion has a coloop') + nonroot_cases += 1 + expected = Counter({('frame', 7, 7): 14224, ('frame', 8, 8): 56, + ('plus', 8, 8): 14280, ('minus', 8, 8): 14280, + ('generic', 8, 8): 14280}) + need(profile == expected and frame_minimum == 24, 'frame-plane exhaustive profile') + need(len(checked) == 5 and cross_checks >= 120, 'direct deletion-rank cross-check coverage') + need(all(sum(bool(dot(root, roots[f])) for f in frame) == 4 for root in (roots[i] for i in p)), + 'aggregate four-frame incidence bound') + need(7 * frame_minimum > 37 * 4, 'seven corrected frame members exceed correction incidences') + return {'ordered_frame_pairs': 56, 'carrying_hyperplanes_per_pair': 255, + 'strata': 4, 'cases': sum(profile.values()), 'nonroot_cases_without_coloops': nonroot_cases, + 'profiles': [list(key) + [count] for key, count in sorted(profile.items())], + 'direct_rank_deletion_profiles_cross_checked': len(checked), + 'frame_minimum_deletions': frame_minimum, 'minimum_seven_frame_incidences': 7 * frame_minimum, + 'maximum_correction_incidences': 37 * 4} + + +def run_checks(): + direct, cartan = direct_model(), cartan_model() + need(direct[0] == cartan[0] and direct[3:] == cartan[3:], 'independent root/normal inventories disagree') + first, second = check_model(direct), check_model(cartan) + need(first == second, 'independent geometry extension summaries disagree') + f1_direct, f1_cartan = f1_checks(direct, False), f1_checks(cartan, True) + need(f1_direct == f1_cartan, 'independent sharp-F1 summaries disagree') + planes_direct, planes_cartan = frame_plane_checks(direct), frame_plane_checks(cartan) + need(planes_direct == planes_cartan, 'independent frame-plane summaries disagree') + return {'coordinate_models': 2, 'checks': first, 'f1': f1_direct, 'frame_planes': planes_direct} + + +if __name__ == '__main__': + print(json.dumps(run_checks(), sort_keys=True, indent=2)) diff --git a/research/e8-d0-root-swaps/formal/RootSwapConnectedCover.lean b/research/e8-d0-root-swaps/formal/RootSwapConnectedCover.lean new file mode 100644 index 0000000000..4351c589ec --- /dev/null +++ b/research/e8-d0-root-swaps/formal/RootSwapConnectedCover.lean @@ -0,0 +1,122 @@ +/- +Copyright (c) 2026 conorholds. All rights reserved. +Released under Apache 2.0 license as described in the repository LICENSE. +Prepared with substantial OpenAI Codex assistance. +-/ +import Mathlib.LinearAlgebra.FiniteDimensional.Lemmas +import Lean.Elab.Tactic.Omega + +/-! +# Connected deletion sets cannot have a positive tight cover + +This formalizes the coefficient-independent covering step of EXTENSION.md, +Section 1. Supports may overlap arbitrarily. Their weights are actual label-span +ranks. The geometric connectedness inequality is an explicit premise; neither +its E8 certificate nor the root-only conclusion is asserted here. +-/ + +noncomputable section + +open scoped BigOperators +open Submodule + +namespace RootSwapConnectedCover + +variable {F E J W : Type*} [Field F] +variable [AddCommGroup W] [Module F W] [FiniteDimensional F W] + +/-- Rank of the labels on a finite coordinate set. -/ +def supportRank (label : E → W) (s : Finset E) : ℕ := + Module.finrank F (Submodule.span F (label '' (s : Set E))) + +variable (label : E → W) +local notation "rk" => supportRank (F := F) label + +private theorem rank_mono {A B : Finset E} (h : A ⊆ B) : rk A ≤ rk B := + Submodule.finrank_mono (Submodule.span_mono (Set.image_mono h)) + +private theorem rank_sup_le (s : Finset J) (P : J → Submodule F W) : + Module.finrank F (s.sup P : Submodule F W) ≤ ∑ j ∈ s, Module.finrank F (P j) := by + classical + induction s using Finset.induction_on with + | empty => simp + | @insert j s hj ih => + rw [Finset.sup_insert, Finset.sum_insert hj] + exact (Submodule.finrank_add_le_finrank_add_finrank _ _).trans + (Nat.add_le_add_left ih _) + +/-- Any finite cover bounds rank by the sum of support ranks, even with overlap. -/ +theorem cover_rank_le_sum (D : Finset E) (C : J → Finset E) (s : Finset J) + (cover : ∀ t ∈ D, ∃ j ∈ s, t ∈ C j) : rk D ≤ ∑ j ∈ s, rk (C j) := by + classical + let P : J → Submodule F W := fun j => Submodule.span F (label '' (C j : Set E)) + have hspan : Submodule.span F (label '' (D : Set E)) ≤ s.sup P := by + apply Submodule.span_le.mpr + rintro _ ⟨t, ht, rfl⟩ + obtain ⟨j, hj, htj⟩ := cover t ht + have hp : P j ≤ s.sup P := Finset.le_sup hj + exact hp (Submodule.subset_span ⟨t, htj, rfl⟩) + exact (Submodule.finrank_mono hspan).trans (rank_sup_le s P) + +variable [Fintype J] [DecidableEq E] + +/-- A connected rank-r set cannot be covered by two or more positive-weight +supports whose total weight is at most r. `i` and `j` exhibit distinct members. +This uses the given supports directly and never assumes disjointness. -/ +theorem connected_cover_impossible (D : Finset E) (C : J → Finset E) + (i j : J) (hji : j ≠ i) + (positive : ∀ k, 0 < rk (C k)) + (cover : ∀ t ∈ D, ∃ k, t ∈ C k) + (connected : ∀ A : Finset E, A ⊆ D → A.Nonempty → (D \ A).Nonempty → + rk D < rk A + rk (D \ A)) + (budget : (∑ k, rk (C k)) ≤ rk D) : False := by + classical + let A := D ∩ C i + let B := D \ C i + let w : J → ℕ := fun k => rk (C k) + have hrest : rk B ≤ ∑ k ∈ Finset.univ.erase i, w k := by + apply cover_rank_le_sum label B C (Finset.univ.erase i) + intro t ht + obtain ⟨k, hk⟩ := cover t (Finset.mem_sdiff.mp ht).1 + refine ⟨k, Finset.mem_erase.mpr ⟨?_, Finset.mem_univ k⟩, hk⟩ + intro hki + exact (Finset.mem_sdiff.mp ht).2 (hki ▸ hk) + have hsum : (∑ k ∈ Finset.univ.erase i, w k) + w i = ∑ k, w k := + Finset.sum_erase_add Finset.univ w (Finset.mem_univ i) + have hjmem : j ∈ Finset.univ.erase i := Finset.mem_erase.mpr ⟨hji, Finset.mem_univ j⟩ + have hjbound : w j ≤ ∑ k ∈ Finset.univ.erase i, w k := + Finset.single_le_sum (fun _ _ => Nat.zero_le _) hjmem + have hAi : rk A ≤ w i := rank_mono label Finset.inter_subset_right + have hi := positive i + have hj := positive j + change 0 < w i at hi + change 0 < w j at hj + change (∑ k, w k) ≤ rk D at budget + by_cases hA : A.Nonempty + · by_cases hB : B.Nonempty + · have hpart : D \ A = B := Finset.sdiff_inter_self_left D (C i) + have hc := connected A Finset.inter_subset_left hA (hpart.symm ▸ hB) + rw [hpart] at hc + omega + · have hBempty : B = ∅ := Finset.not_nonempty_iff_eq_empty.mp hB + have hDC : D ⊆ C i := Finset.sdiff_eq_empty_iff_subset.mp hBempty + have hd := rank_mono (F := F) label hDC + change rk D ≤ w i at hd + omega + · have hAempty : A = ∅ := Finset.not_nonempty_iff_eq_empty.mp hA + have hBD : B = D := by + ext t + constructor + · exact fun ht => (Finset.mem_sdiff.mp ht).1 + · intro ht + apply Finset.mem_sdiff.mpr + refine ⟨ht, ?_⟩ + intro hti + have hmem : t ∈ A := Finset.mem_inter.mpr ⟨ht, hti⟩ + simp [hAempty] at hmem + rw [hBD] at hrest + omega + +#print axioms connected_cover_impossible + +end RootSwapConnectedCover diff --git a/research/e8-d0-root-swaps/formal/RootSwapOneExceptional.lean b/research/e8-d0-root-swaps/formal/RootSwapOneExceptional.lean new file mode 100644 index 0000000000..2041473a46 --- /dev/null +++ b/research/e8-d0-root-swaps/formal/RootSwapOneExceptional.lean @@ -0,0 +1,282 @@ +/- +Copyright (c) 2026 conorholds. All rights reserved. +Released under Apache 2.0 license as described in the repository LICENSE. +Prepared with substantial OpenAI Codex assistance. +-/ +import Mathlib.LinearAlgebra.FiniteDimensional.Lemmas + +/-! +# The coefficient-preserving one-exception root-swap argument + +This file formalizes the first case of Section 3 of `e8-d0-root-swaps/PROOF.md`. +The finite family `q` generates the correction space by actual scalar linear +combinations; a witness cannot independently choose values on its union support. +The coefficient field `K` and label field `F` are independent. For E8, specialize +`F` to the binary field, `root` to the root representatives, and `pairing` to beta. + +The main result is `one_exception_weighted_bound`: when all members except a +distinguished one have root-support rank bounded by label-support rank, every +swap-eligible root together has rank at most the total label-support weight. +The intermediate `one_exception_rank_bound` isolates the regular-support span. +This proves the at-most-one-exception case of Theorem A. No E8 geometric input, +exceptional-support classification, two-factor lemma, or C7 weighted-basis +reduction is asserted here. +-/ + +noncomputable section + +open scoped BigOperators +open Submodule + +namespace RootSwapOneExceptional + +attribute [local instance] Classical.propDecidable + +variable {K F E J V W : Type*} +variable [Field K] [Field F] [Fintype J] +variable [AddCommGroup V] [Module K V] +variable [AddCommGroup W] [Module F W] + +/-- An actual vector in the scalar span of the specified coefficient family. -/ +def combination (q : J → E → K) (c : J → K) (t : E) : K := + ∑ j, c j * q j t + +/-- A swap witness has a nonzero own coordinate and vanishes at all other +orthogonal coordinates. The root itself is allowed in the support. -/ +def Eligible (orthogonal : E → E → Prop) (q : J → E → K) (t : E) : Prop := + ∃ c : J → K, combination q c t ≠ 0 ∧ + ∀ s, s ≠ t → orthogonal s t → combination q c s = 0 + +/-- The coefficient representation agrees exactly with the submodule span; +this is the bridge to a correction space presented by a basis or generating family. -/ +theorem combination_mem_span (q : J → E → K) (c : J → K) : + combination q c ∈ Submodule.span K (Set.range q) := by + apply (Submodule.mem_span_range_iff_exists_fun K).mpr + refine ⟨c, ?_⟩ + ext t + simp [combination, Finset.sum_apply, smul_eq_mul] + +/-- Eligibility is equivalent to an actual vector in the generated subspace, +with precisely the original own-coordinate and orthogonal-coordinate conditions. -/ +theorem eligible_iff_span_witness (orthogonal : E → E → Prop) + (q : J → E → K) (t : E) : + Eligible orthogonal q t ↔ + ∃ tau : E → K, tau ∈ Submodule.span K (Set.range q) ∧ tau t ≠ 0 ∧ + ∀ s, s ≠ t → orthogonal s t → tau s = 0 := by + constructor + · rintro ⟨c, hc, hz⟩ + exact ⟨combination q c, combination_mem_span q c, hc, hz⟩ + · rintro ⟨tau, htau, hown, hzero⟩ + obtain ⟨c, hc⟩ := (Submodule.mem_span_range_iff_exists_fun K).mp htau + have hcs : ∀ s, combination q c s = tau s := by + intro s + simpa [combination, Finset.sum_apply, smul_eq_mul] using congrFun hc s + refine ⟨c, ?_, ?_⟩ + · rwa [hcs] + · intro s hst horth + rw [hcs] + exact hzero s hst horth + +/-- Coordinates eligible for a swap whose root vector is outside `O`. -/ +def Outside (orthogonal : E → E → Prop) (q : J → E → K) + (root : E → V) (O : Submodule K V) : Set E := + {t | Eligible orthogonal q t ∧ root t ∉ O} + +/-- Binary label rank is the intended specialization of this support weight. -/ +def supportWeight (label : E → W) (q : E → K) : ℕ := + Module.finrank F (Submodule.span F (label '' {t | q t ≠ 0})) + +/-- Away from `O`, all actual witnesses retain the same distinguished member, +with their own single scalar coefficient. -/ +theorem combination_outside (q : J → E → K) (e : J) + (root : E → V) (O : Submodule K V) + (regular : ∀ j, j ≠ e → ∀ t, q j t ≠ 0 → root t ∈ O) + (c : J → K) (t : E) (ht : root t ∉ O) : + combination q c t = c e * q e t := by + classical + unfold combination + apply Finset.sum_eq_single e + · intro j _ hje + have hz : q j t = 0 := by + by_contra hn + exact ht (regular j hje t hn) + simp [hz] + · simp + +/-- Both the distinguished coefficient and its own-coordinate value are nonzero. -/ +theorem outside_witness_nonzero (q : J → E → K) (e : J) + (root : E → V) (O : Submodule K V) + (regular : ∀ j, j ≠ e → ∀ t, q j t ≠ 0 → root t ∈ O) + (c : J → K) (t : E) (ht : root t ∉ O) + (hc : combination q c t ≠ 0) : c e ≠ 0 ∧ q e t ≠ 0 := by + rw [combination_outside q e root O regular c t ht] at hc + exact mul_ne_zero_iff.mp hc + +/-- The shared-coefficient argument: eligible roots outside `O` cannot be +orthogonal to one another. This does not replace the space by union support. -/ +theorem outside_pairwise_nonorthogonal + (orthogonal : E → E → Prop) (q : J → E → K) (e : J) + (root : E → V) (O : Submodule K V) + (regular : ∀ j, j ≠ e → ∀ t, q j t ≠ 0 → root t ∈ O) + {s t : E} (hs : s ∈ Outside orthogonal q root O) + (ht : t ∈ Outside orthogonal q root O) (hst : s ≠ t) : + ¬ orthogonal s t := by + obtain ⟨cs, hcs, _⟩ := hs.1 + obtain ⟨ct, hct, hzero⟩ := ht.1 + have hsne := (outside_witness_nonzero q e root O regular cs s hs.2 hcs).2 + have htne := (outside_witness_nonzero q e root O regular ct t ht.2 hct).1 + intro horth + have hz := hzero s hst horth + rw [combination_outside q e root O regular ct s hs.2] at hz + exact (mul_ne_zero htne hsne) hz + +/-- A family with a diagonal-one/off-diagonal-zero pairing is independent; +positivity or an ordered field is not needed, so this applies in characteristic two. -/ +theorem independent_of_pairing {I : Type*} [Fintype I] + (v : I → W) (pairing : W →ₗ[F] W →ₗ[F] F) + (diagonal : ∀ i, pairing (v i) (v i) = 1) + (offDiagonal : ∀ i j, i ≠ j → pairing (v i) (v j) = 0) : + LinearIndependent F v := by + classical + apply Fintype.linearIndependent_iff.mpr + intro c hc i + have h := congrArg (pairing (v i)) hc + simp only [map_sum, map_smul, map_zero] at h + have hs : (∑ j, c j • pairing (v i) (v j)) = c i := by + calc + _ = c i • pairing (v i) (v i) := by + apply Finset.sum_eq_single i + · intro j _ hji + rw [offDiagonal i j (Ne.symm hji), smul_zero] + · simp + _ = c i := by rw [diagonal i, smul_eq_mul, mul_one] + exact hs.symm.trans h + +variable [Fintype E] [FiniteDimensional F W] + +/-- The outside eligible labels are independent and lie in the distinguished +support span, so their number is at most that member's support weight. -/ +theorem outside_card_le_supportWeight + (orthogonal : E → E → Prop) (q : J → E → K) (e : J) + (root : E → V) (O : Submodule K V) (label : E → W) + (pairing : W →ₗ[F] W →ₗ[F] F) + (diagonal : ∀ t, pairing (label t) (label t) = 1) + (nonorthogonal : ∀ s t, s ≠ t → ¬ orthogonal s t → + pairing (label s) (label t) = 0) + (regular : ∀ j, j ≠ e → ∀ t, q j t ≠ 0 → root t ∈ O) : + Fintype.card (Outside orthogonal q root O) ≤ supportWeight (F := F) label (q e) := by + classical + let A := Outside orthogonal q root O + have hlin : LinearIndependent F (fun t : A => label t) := by + apply independent_of_pairing _ pairing + · intro t + exact diagonal t + · intro s t hst + apply nonorthogonal s t + · exact fun h => hst (Subtype.ext h) + · exact outside_pairwise_nonorthogonal orthogonal q e root O regular + s.property t.property (fun h => hst (Subtype.ext h)) + let U := Submodule.span F (label '' {t | q e t ≠ 0}) + have hmem : ∀ t : A, label t ∈ U := by + intro t + obtain ⟨c, hc, _⟩ := t.property.1 + have hqt := (outside_witness_nonzero q e root O regular c t t.property.2 hc).2 + exact Submodule.subset_span ⟨t, hqt, rfl⟩ + let v : A → U := fun t => ⟨label t, hmem t⟩ + have hlinU : LinearIndependent F v := by + apply LinearIndependent.of_comp U.subtype + exact hlin + exact hlinU.fintype_card_le_finrank + +variable [FiniteDimensional K V] + +/-- The coefficient-preserving rank bound with one distinguished member. +The subspace `O` contains the root supports of every other family member. +Its dimension can therefore be bounded separately by their total weights. -/ +theorem one_exception_rank_bound + (orthogonal : E → E → Prop) (q : J → E → K) (e : J) + (root : E → V) (O : Submodule K V) (label : E → W) + (pairing : W →ₗ[F] W →ₗ[F] F) + (diagonal : ∀ t, pairing (label t) (label t) = 1) + (nonorthogonal : ∀ s t, s ≠ t → ¬ orthogonal s t → + pairing (label s) (label t) = 0) + (regular : ∀ j, j ≠ e → ∀ t, q j t ≠ 0 → root t ∈ O) : + Module.finrank K (Submodule.span K (root '' {t | Eligible orthogonal q t})) ≤ + Module.finrank K O + supportWeight (F := F) label (q e) := by + classical + let A := Outside orthogonal q root O + let R := Submodule.span K (Set.range (fun t : A => root t)) + have hspan : Submodule.span K (root '' {t | Eligible orthogonal q t}) ≤ O ⊔ R := by + apply Submodule.span_le.mpr + rintro _ ⟨t, ht, rfl⟩ + by_cases hO : root t ∈ O + · exact (show O ≤ O ⊔ R from le_sup_left) hO + · apply (show R ≤ O ⊔ R from le_sup_right) + exact Submodule.subset_span ⟨⟨t, ht, hO⟩, rfl⟩ + calc + _ ≤ Module.finrank K (O ⊔ R : Submodule K V) := Submodule.finrank_mono hspan + _ ≤ Module.finrank K O + Module.finrank K R := + Submodule.finrank_add_le_finrank_add_finrank O R + _ ≤ Module.finrank K O + Fintype.card A := + Nat.add_le_add_left (finrank_range_le_card (R := K) (fun t : A => root t)) _ + _ ≤ Module.finrank K O + supportWeight (F := F) label (q e) := + Nat.add_le_add_left + (outside_card_le_supportWeight orthogonal q e root O label pairing + diagonal nonorthogonal regular) _ + +omit [Fintype J] in +/-- Dimension is subadditive for the span of finitely many subspaces. -/ +theorem finrank_finset_sup_le (s : Finset J) (P : J → Submodule K V) : + Module.finrank K (s.sup P : Submodule K V) ≤ ∑ j ∈ s, Module.finrank K (P j) := by + classical + induction s using Finset.induction_on with + | empty => simp + | @insert j s hjs ih => + rw [Finset.sup_insert, Finset.sum_insert hjs] + exact (Submodule.finrank_add_le_finrank_add_finrank (P j) (s.sup P)).trans + (Nat.add_le_add_left ih _) + +/-- The complete at-most-one-exception case of Theorem A, expressed for a finite +scalar generating family. Each member other than `e` has root-support rank at +most its label-support rank. No such inequality is assumed for `e`. -/ +theorem one_exception_weighted_bound + (orthogonal : E → E → Prop) (q : J → E → K) (e : J) + (root : E → V) (label : E → W) + (pairing : W →ₗ[F] W →ₗ[F] F) + (diagonal : ∀ t, pairing (label t) (label t) = 1) + (nonorthogonal : ∀ s t, s ≠ t → ¬ orthogonal s t → + pairing (label s) (label t) = 0) + (regularRank : ∀ j, j ≠ e → + Module.finrank K (Submodule.span K (root '' {t | q j t ≠ 0})) ≤ + supportWeight (F := F) label (q j)) : + Module.finrank K (Submodule.span K (root '' {t | Eligible orthogonal q t})) ≤ + ∑ j, supportWeight (F := F) label (q j) := by + classical + let P : J → Submodule K V := fun j => + Submodule.span K (root '' {t | q j t ≠ 0}) + let s : Finset J := Finset.univ.erase e + let O : Submodule K V := s.sup P + have regular : ∀ j, j ≠ e → ∀ t, q j t ≠ 0 → root t ∈ O := by + intro j hje t hqt + have hj : j ∈ s := Finset.mem_erase.mpr ⟨hje, Finset.mem_univ j⟩ + have hp : P j ≤ O := Finset.le_sup hj + exact hp (Submodule.subset_span ⟨t, hqt, rfl⟩) + have hO : Module.finrank K O ≤ ∑ j ∈ s, supportWeight (F := F) label (q j) := by + apply (finrank_finset_sup_le s P).trans + apply Finset.sum_le_sum + intro j hj + exact regularRank j (Finset.mem_erase.mp hj).1 + calc + _ ≤ Module.finrank K O + supportWeight (F := F) label (q e) := + one_exception_rank_bound orthogonal q e root O label pairing + diagonal nonorthogonal regular + _ ≤ (∑ j ∈ s, supportWeight (F := F) label (q j)) + + supportWeight (F := F) label (q e) := Nat.add_le_add_right hO _ + _ = ∑ j, supportWeight (F := F) label (q j) := + Finset.sum_erase_add Finset.univ + (fun j => supportWeight (F := F) label (q j)) (Finset.mem_univ e) + +#print axioms one_exception_rank_bound +#print axioms one_exception_weighted_bound + +end RootSwapOneExceptional diff --git a/research/e8-d0-root-swaps/formal/RootSwapQuartet.lean b/research/e8-d0-root-swaps/formal/RootSwapQuartet.lean new file mode 100644 index 0000000000..d7aecfd2f3 --- /dev/null +++ b/research/e8-d0-root-swaps/formal/RootSwapQuartet.lean @@ -0,0 +1,110 @@ +/- +Copyright (c) 2026 conorholds. All rights reserved. +Released under Apache 2.0 license as described in the repository LICENSE. +Prepared with substantial OpenAI Codex assistance. +-/ +import Mathlib.LinearAlgebra.FiniteDimensional.Lemmas + +/-! +# Two quartet supports and one singleton + +This is the coefficient argument for the low-overlap `(3,3,1)` profile in +Section 3 of `e8-d0-root-swaps/PROOF.md`. The identification of exceptional +weight-three supports as orthogonal quartets is not formalized here. Given +that geometry, the theorem proves that only the singleton coordinate can +be swap-eligible. Witnesses retain their actual three scalar coefficients. +-/ + +noncomputable section + +namespace RootSwapQuartet + +attribute [local instance] Classical.propDecidable + +variable {K E : Type*} [Field K] [DecidableEq E] + +/-- Four points cannot all be covered by the own coordinate, the singleton, +and an intersection containing at most one point. -/ +theorem exists_private_coordinate (A B : Finset E) + (hA : 4 ≤ A.card) (hAB : (A ∩ B).card ≤ 1) (t u : E) : + ∃ s ∈ A, s ≠ t ∧ s ≠ u ∧ s ∉ B := by + by_contra h + have hsub : A ⊆ insert t (insert u (A ∩ B)) := by + intro s hs + by_cases hst : s = t + · exact Finset.mem_insert.mpr (Or.inl hst) + by_cases hsu : s = u + · exact Finset.mem_insert_of_mem (Finset.mem_insert.mpr (Or.inl hsu)) + have hsB : s ∈ B := by + by_contra hn + exact h ⟨s, hs, hst, hsu, hn⟩ + exact Finset.mem_insert_of_mem (Finset.mem_insert_of_mem (Finset.mem_inter.mpr ⟨hs, hsB⟩)) + have hbound : (insert t (insert u (A ∩ B))).card ≤ 3 := by + calc + _ ≤ (insert u (A ∩ B)).card + 1 := Finset.card_insert_le _ _ + _ ≤ ((A ∩ B).card + 1) + 1 := + Nat.add_le_add_right (Finset.card_insert_le _ _) _ + _ ≤ (1 + 1) + 1 := Nat.add_le_add_right (Nat.add_le_add_right hAB _) _ + _ = 3 := rfl + exact (by decide : ¬ 4 ≤ 3) (hA.trans ((Finset.card_le_card hsub).trans hbound)) + +/-- An actual member of the span of two words and one coordinate unit. -/ +def combination (qA qB : E → K) (u : E) (a b c : K) (s : E) : K := + a * qA s + b * qB s + if s = u then c else 0 + +/-- Swap eligibility in that actual three-generator scalar span. -/ +def Eligible (orthogonal : E → E → Prop) (qA qB : E → K) + (u t : E) : Prop := + ∃ a b c : K, combination qA qB u a b c t ≠ 0 ∧ + ∀ s, s ≠ t → orthogonal s t → combination qA qB u a b c s = 0 + +/-- With two orthogonal supports of size at least four, overlap at most one, +and one singleton, every swap-eligible coordinate is the singleton. +No support-union relaxation of the coefficient space is used. -/ +theorem eligible_eq_singleton + (orthogonal : E → E → Prop) (A B : Finset E) (qA qB : E → K) + (u : E) (hA : 4 ≤ A.card) (hB : 4 ≤ B.card) + (hAB : (A ∩ B).card ≤ 1) + (supportA : ∀ s, qA s ≠ 0 ↔ s ∈ A) + (supportB : ∀ s, qB s ≠ 0 ↔ s ∈ B) + (orthA : ∀ s ∈ A, ∀ t ∈ A, s ≠ t → orthogonal s t) + (orthB : ∀ s ∈ B, ∀ t ∈ B, s ≠ t → orthogonal s t) + (t : E) (ht : Eligible orthogonal qA qB u t) : t = u := by + by_contra htu + obtain ⟨a, b, c, hown, hzero⟩ := ht + have ha : a * qA t = 0 := by + by_cases htA : t ∈ A + · obtain ⟨s, hsA, hst, hsu, hsB⟩ := exists_private_coordinate A B hA hAB t u + have hsqa : qA s ≠ 0 := (supportA s).mpr hsA + have hsqb : qB s = 0 := by + by_contra hn + exact hsB ((supportB s).mp hn) + have hz : a * qA s = 0 := by + simpa [combination, hsqb, hsu] using hzero s hst (orthA s hsA t htA hst) + have hazero : a = 0 := (mul_eq_zero.mp hz).resolve_right hsqa + simp [hazero] + · have hqt : qA t = 0 := by + by_contra hn + exact htA ((supportA t).mp hn) + simp [hqt] + have hb : b * qB t = 0 := by + by_cases htB : t ∈ B + · have hBA : (B ∩ A).card ≤ 1 := by simpa [Finset.inter_comm] using hAB + obtain ⟨s, hsB, hst, hsu, hsA⟩ := exists_private_coordinate B A hB hBA t u + have hsqb : qB s ≠ 0 := (supportB s).mpr hsB + have hsqa : qA s = 0 := by + by_contra hn + exact hsA ((supportA s).mp hn) + have hz : b * qB s = 0 := by + simpa [combination, hsqa, hsu] using hzero s hst (orthB s hsB t htB hst) + have hbzero : b = 0 := (mul_eq_zero.mp hz).resolve_right hsqb + simp [hbzero] + · have hqt : qB t = 0 := by + by_contra hn + exact htB ((supportB t).mp hn) + simp [hqt] + exact hown (by simp [combination, ha, hb, htu]) + +#print axioms eligible_eq_singleton + +end RootSwapQuartet diff --git a/research/e8-d0-root-swaps/geometry_audit.py b/research/e8-d0-root-swaps/geometry_audit.py new file mode 100644 index 0000000000..3084be53d3 --- /dev/null +++ b/research/e8-d0-root-swaps/geometry_audit.py @@ -0,0 +1,493 @@ +#!/usr/bin/env python3 +"""Independent exact finite geometry audit for the E8 d=0 argument. + +Prepared by conorholds with substantial OpenAI Codex assistance; Apache-2.0. +The E8/2E8 and decoder setting follows DreamingOfClouds' PR2816, PR2826, +PR2862 and PR2985. This checker generates its own roots, normal orbits, +binary labels and rank calculations; it imports no predecessor or primary +verifier mathematics. The parabolic completeness implication is a written +root-system argument, not a claim that enumerating 256 subsets proves it. +""" + +from collections import Counter, deque +from fractions import Fraction +from itertools import combinations +from math import gcd +import json + + +class AuditFailure(RuntimeError): + """A failed mathematical or coverage check, including under python -O.""" + + +def check(condition, message): + if not condition: + raise AuditFailure(message) + + +def canonical(vector): + for value in vector: + if value: + return tuple(vector) if value > 0 else tuple(-x for x in vector) + raise AuditFailure("zero has no projective representative") + + +def integer_rank(rows): + """Fraction-free row elimination, reducing each new row by its gcd.""" + rows = [list(row) for row in rows if any(row)] + if not rows: + return 0 + width = len(rows[0]) + check(all(len(row) == width for row in rows), "ragged rank input") + rank = 0 + for column in range(width): + pivot = next((i for i in range(rank, len(rows)) if rows[i][column]), None) + if pivot is None: + continue + rows[rank], rows[pivot] = rows[pivot], rows[rank] + pivot_row = rows[rank] + for i in range(rank + 1, len(rows)): + coefficient = rows[i][column] + if not coefficient: + continue + row = [pivot_row[column] * x - coefficient * y + for x, y in zip(rows[i], pivot_row)] + divisor = 0 + for value in row: + divisor = gcd(divisor, value) + rows[i] = [value // divisor for value in row] if divisor else row + rank += 1 + if rank == width: + break + return rank + + +def binary_rank(vectors): + pivots = {} + for value in vectors: + while value: + pivot = value.bit_length() - 1 + if pivot not in pivots: + pivots[pivot] = value + break + value ^= pivots[pivot] + return len(pivots) + + +def inverse_integer_matrix(matrix): + n = len(matrix) + rows = [[Fraction(x) for x in row] + + [Fraction(i == j) for j in range(n)] + for i, row in enumerate(matrix)] + for column in range(n): + pivot = next((i for i in range(column, n) if rows[i][column]), None) + check(pivot is not None, "singular Cartan matrix") + rows[column], rows[pivot] = rows[pivot], rows[column] + scale = rows[column][column] + rows[column] = [x / scale for x in rows[column]] + for i in range(n): + if i != column and rows[i][column]: + scale = rows[i][column] + rows[i] = [x - scale * y for x, y in zip(rows[i], rows[column])] + result = [row[n:] for row in rows] + check(all(x.denominator == 1 for row in result for x in row), + "E8 Cartan inverse is not integral") + return [[int(x) for x in row] for row in result] + + +class CartanModel: + """Integral simple-root coordinates; only the frame uses a D8 bridge.""" + + edges = ((0, 2), (1, 3), (2, 3), (3, 4), (4, 5), (5, 6), (6, 7)) + simple_doubled = ( + (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 __init__(self): + self.cartan = [[2 * (i == j) for j in range(8)] for i in range(8)] + for i, j in self.edges: + self.cartan[i][j] = self.cartan[j][i] = -1 + bridge_gram = [[sum(x * y for x, y in zip(a, b)) + for b in self.simple_doubled] for a in self.simple_doubled] + check(bridge_gram == [[4 * x for x in row] for row in self.cartan], + "fixed coordinate bridge disagrees with Cartan matrix") + self.inverse = inverse_integer_matrix(self.cartan) + simple = [tuple(int(i == j) for i in range(8)) for j in range(8)] + roots = set(simple) + queue = deque(simple) + while queue: + root = queue.popleft() + for generator in range(8): + image = self.reflect(root, generator) + if image not in roots: + roots.add(image) + queue.append(image) + check(len(roots) == 240, "Cartan root orbit is incomplete") + check(all(self.inner(root, root) == 2 for root in roots), "non-root in orbit") + check(all(tuple(-x for x in root) in roots for root in roots), "missing negative root") + self.roots = sorted({canonical(root) for root in roots}) + check(len(self.roots) == 120, "incorrect root-line quotient") + check(all(all(x >= 0 for x in root) for root in self.roots), + "positive roots have unexpected simple coordinates") + self.index = {root: i for i, root in enumerate(self.roots)} + self.labels = [256 | sum((x % 2) << i for i, x in enumerate(root)) + for root in self.roots] + self.gram = [[self.inner(a, b) for b in self.roots] for a in self.roots] + self.full_mask = (1 << 120) - 1 + self.off_masks = [sum(1 << j for j, value in enumerate(row) if value) + for row in self.gram] + self.permutations = [] + for generator in range(8): + permutation = [self.index[canonical(self.reflect(root, generator))] + for root in self.roots] + check(len(set(permutation)) == 120, "reflection does not permute roots") + self.permutations.append(permutation) + + doubled_index = {canonical(self.to_doubled(root)): i + for i, root in enumerate(self.roots)} + frame = [] + # Source PR2816 order: all four plus roots, then all four minus roots. + for sign in (1, -1): + for pair in range(4): + vector = [0] * 8 + vector[2 * pair], vector[2 * pair + 1] = 2, 2 * sign + check(tuple(vector) in doubled_index, "canonical frame root missing") + frame.append(doubled_index[tuple(vector)]) + self.frame = frame + self.frame_mask = sum(1 << i for i in frame) + self.p112_mask = self.full_mask ^ self.frame_mask + self.hyperplane_outside = [sum(1 << i for i, label in enumerate(self.labels) + if (normal & label).bit_count() % 2) + for normal in range(1, 512)] + + def inner(self, a, b): + return sum(a[i] * sum(self.cartan[i][j] * b[j] for j in range(8)) + for i in range(8)) + + def reflect(self, vector, generator): + coefficient = sum(self.cartan[generator][j] * vector[j] for j in range(8)) + result = list(vector) + result[generator] -= coefficient + return tuple(result) + + def to_doubled(self, vector): + return tuple(sum(vector[i] * self.simple_doubled[i][j] for i in range(8)) + for j in range(8)) + + def mask_labels(self, mask): + result = [] + while mask: + bit = mask & -mask + result.append(self.labels[bit.bit_length() - 1]) + mask ^= bit + return result + + def vector_orbit(self, seed, expected_size): + seen = {canonical(seed)} + queue = deque(seen) + while queue: + vector = queue.popleft() + for generator in range(8): + image = canonical(self.reflect(vector, generator)) + if image not in seen: + seen.add(image) + queue.append(image) + check(len(seen) == expected_size, "fundamental-normal Weyl orbit is incomplete") + norm = self.inner(seed, seed) + check(all(self.inner(x, x) == norm for x in seen), "normal orbit changes norm") + check(all(gcd(*x) == 1 for x in seen), "normal orbit contains an imprimitive vector") + return sorted(seen) + + def plane_orbit(self, seed, expected_size): + seen = {tuple(sorted(seed))} + queue = deque(seen) + while queue: + plane = queue.popleft() + for permutation in self.permutations: + image = tuple(sorted(permutation[i] for i in plane)) + if image not in seen: + seen.add(image) + queue.append(image) + check(len(seen) == expected_size, "normal-plane Weyl orbit is incomplete") + check(all(len(plane) == len(seed) for plane in seen), "normal-plane size changes") + return sorted(seen) + + +def check_root_class_bijection(labels, quadratic_values): + check(len(labels) == 120 and len(set(labels)) == 120, + "root-class inventory is incomplete or repeated") + check(all(label & 256 and 0 <= label < 512 for label in labels), + "root labels have lost their affine coordinate") + classes = {label ^ 256 for label in labels} + check(classes == {i for i, value in enumerate(quadratic_values) if value}, + "roots are not exactly the nonsingular quadratic classes") + + +def quadratic_checks(model): + values = [] + for value in range(256): + vector = [(value >> i) & 1 for i in range(8)] + norm = model.inner(vector, vector) + check(norm % 2 == 0, "Cartan lattice is not even") + values.append((norm // 2) % 2) + check_root_class_bijection(model.labels, values) + check(sum(1 - 2 * x for x in values) == 16, "quadratic form is not plus type") + check(binary_rank(sum((model.cartan[i][j] % 2) << j for j in range(8)) + for i in range(8)) == 8, "quadratic polar form is degenerate") + for i, row in enumerate(model.gram): + for j, value in enumerate(row): + a, b = model.roots[i], model.roots[j] + polar = sum((a[k] % 2) * (model.cartan[k][l] % 2) * (b[l] % 2) + for k in range(8) for l in range(8)) % 2 + check((1 + value) % 2 == (1 + polar) % 2, + "label pairing does not match root orthogonality") + + # Walsh transform verifies the Fourier identity used for every affine flat. + transform = [1 - 2 * x for x in values] + stride = 1 + while stride < 256: + for start in range(0, 256, 2 * stride): + for offset in range(stride): + a, b = transform[start + offset], transform[start + offset + stride] + transform[start + offset] = a + b + transform[start + offset + stride] = a - b + stride *= 2 + for value in range(256): + normal = sum((sum(model.cartan[i][j] * ((value >> j) & 1) + for j in range(8)) % 2) << i for i in range(8)) + check(transform[normal] == 16 * (1 - 2 * values[value]), + "quadratic Fourier identity failed") + + # Restriction to a dual space of dimension 1, 2, 3 or 4 is a quadratic polynomial + # with zero constant. Enumerating these small polynomials is exhaustive; + # it is not an enumeration or sampling of ambient affine flats. + minima = {} + for dimension in (1, 2, 3, 4): + monomials = [1 << i for i in range(dimension)] + monomials += [(1 << i) | (1 << j) + for i, j in combinations(range(dimension), 2)] + sums = [] + for coefficients in range(1 << len(monomials)): + total = 0 + for point in range(1 << dimension): + q = sum(1 for i, support in enumerate(monomials) + if coefficients >> i & 1 and point & support == support) % 2 + total += 1 - 2 * q + sums.append(total) + minima[dimension] = min(sums) + check(minima == {1: 0, 2: -2, 3: -4, 4: -8}, "small quadratic Gauss lower bounds changed") + cap7 = (64 - (16 // 4) * minima[2]) // 2 + cap6 = (32 - (16 // 8) * minima[3]) // 2 + cap5 = (16 - (16 // 16) * minima[4]) // 2 + cap8 = max(120 - cut.bit_count() for cut in model.hyperplane_outside) + check(cap8 == (128 - 8 * minima[1]) // 2, + "dimension-eight hyperplane maximum disagrees with the Fourier bound") + caps = {"1": 1, "2": 2, "3": 4, "4": 8, "5": cap5, "6": cap6, "7": cap7, "8": cap8} + check(caps == {"1": 1, "2": 2, "3": 4, "4": 8, "5": 12, "6": 20, "7": 36, "8": 64}, + "full-E8 support-cap bound failed") + # Attainment controls use coordinate D4/D5 subsets, not norm enumeration. + for width, weight, count in ((4, 5, 12), (5, 6, 20)): + subset = [i for i, root in enumerate(model.roots) + if all(x == 0 for x in model.to_doubled(root)[width:])] + check(len(subset) == count, "D4/D5 cap witness has the wrong size") + check(binary_rank(model.labels[i] for i in subset) == weight, + "D4/D5 cap witness has the wrong label rank") + return caps + + +def parabolic_checks(model): + large = {} + counts_by_rank = {} + for subset in range(256): + selected = [root for root in model.roots + if all(not value or subset >> i & 1 + for i, value in enumerate(root))] + rank = subset.bit_count() + check(integer_rank(selected) == rank, "standard parabolic rank mismatch") + counts_by_rank.setdefault(rank, Counter())[len(selected)] += 1 + if rank <= 7 and len(selected) >= 28: + large[(rank, len(selected))] = subset + expected = {(6, 30), (6, 36), (7, 28), (7, 37), (7, 42), (7, 63)} + check(set(large) == expected and len(large) == 6, + "large proper parabolic inventory changed") + check(max(count for rank, counts in counts_by_rank.items() if rank <= 5 + for count in counts) == 20, "rank<=5 parabolic maximum is not 20") + for key in expected: + check(counts_by_rank[key[0]][key[1]] == 1, "large parabolic seed is not unique") + return large, {"subsets_checked": 256, + "large_proper_types": [list(key) for key in sorted(large)]} + + +EXPECTED_PROFILES = { + "norm4": [[70, 14, 8, 128], [73, 13, 8, 896], [76, 12, 7, 56]], + "norm6": [[77, 25, None, 2688], [79, 24, None, 448], [80, 24, None, 224]], + "norm8": [[84, 28, None, 1024]], + "a2_plane": [[78, 26, None, 896], [80, 24, None, 224]], + "a1_squared_plane": [[82, 26, None, 448], [84, 24, None, 2688]], +} + + +def validate_class_inventory(classes): + check(set(classes) == set(EXPECTED_PROFILES), "incomplete non-root normal-class inventory") + + +def normal_filter_checks(model, parabolics): + summary = {} + relaxed_pass = False + + def profile(class_name, masks, orbit_size): + nonlocal relaxed_pass + counts = Counter() + for off in masks: + size = off.bit_count() + if size > 84: + continue + deletions = [(off & outside) for outside in model.hyperplane_outside] + minimum = min(mask.bit_count() for mask in deletions) + small = [mask for mask in deletions if mask.bit_count() <= 20] + if small: + minimum_rank = min(binary_rank(model.mask_labels(mask)) for mask in small) + check(minimum_rank >= 7, "a non-root normal passes the kappa<=6 gate") + relaxed_pass |= minimum_rank == 7 + else: + minimum_rank = None + check(minimum > 20, "deletion cardinality gate is incomplete") + counts[(size, minimum, minimum_rank)] += 1 + profiles = [list(key) + [count] for key, count in sorted(counts.items())] + check(profiles == EXPECTED_PROFILES[class_name], + "normal deletion profile differs for " + class_name) + summary[class_name] = {"orbit_size": orbit_size, "profiles": profiles} + + for norm, root_count, orbit_size in ((2, 63, 120), (4, 42, 1080), + (6, 37, 3360), (8, 28, 8640)): + subset = parabolics[(7, root_count)] + omitted = next(i for i in range(8) if not subset >> i & 1) + seed = tuple(model.inverse[i][omitted] for i in range(8)) + check(model.inner(seed, seed) == norm, "fundamental normal has the wrong norm") + check(all(sum(model.cartan[i][j] * seed[j] for j in range(8)) == 0 + for i in range(8) if subset >> i & 1), "normal is not perpendicular") + orbit = model.vector_orbit(seed, orbit_size) + if norm == 2: + check(set(orbit) == set(model.roots), "E7 normals do not give all roots") + continue + masks = [] + for vector in orbit: + functional = [sum(model.cartan[i][j] * vector[j] for j in range(8)) + for i in range(8)] + off = sum(1 << i for i, root in enumerate(model.roots) + if sum(x * y for x, y in zip(functional, root))) + masks.append(off & model.p112_mask) + profile("norm" + str(norm), masks, orbit_size) + + for root_count, class_name, orbit_size, plane_size in ( + (36, "a2_plane", 1120, 3), (30, "a1_squared_plane", 3780, 2)): + subset = parabolics[(6, root_count)] + seed = [i for i, root in enumerate(model.roots) + if all(sum(model.cartan[k][j] * root[j] for j in range(8)) == 0 + for k in range(8) if subset >> k & 1)] + check(len(seed) == plane_size and integer_rank(model.roots[i] for i in seed) == 2, + "rank-six perpendicular plane has the wrong root system") + planes = model.plane_orbit(seed, orbit_size) + masks = [] + for plane in planes: + check(all((model.gram[a][b] != 0) == (plane_size == 3) + for a, b in combinations(plane, 2)), "normal-plane root type changed") + off = 0 + for root in plane: + off |= model.off_masks[root] + masks.append(off & model.p112_mask) + profile(class_name, masks, orbit_size) + validate_class_inventory(summary) + check(relaxed_pass, "relaxing the binary rank gate has no positive control") + return summary + + +def full_code_checks(model): + minimum = 8 + for outside in model.hyperplane_outside: + roots = [root for i, root in enumerate(model.roots) if outside >> i & 1] + rank = integer_rank(roots) + minimum = min(minimum, rank) + check(rank == 8, "a nonzero full codeword can lie in a binary hyperplane") + # The complement-rank test proves weight9 for every nonzero direction, + # including directions not represented by finite normal orbits. + for off in model.off_masks: + check(binary_rank(model.mask_labels(off)) == 9, "root codeword weight is not 9") + return {"hyperplanes_checked": 511, "minimum_complement_real_rank": minimum} + + +def remainder_checks(model): + expected = Counter({0: 1, 24: 126, 28: 256, 32: 126, 56: 2}) + for i, off in enumerate(model.off_masks): + remainder = off ^ (1 << i) + check(remainder.bit_count() == 56, "root remainder has the wrong size") + check(binary_rank(model.mask_labels(remainder)) == 8, "root remainder rank is not 8") + check(Counter((remainder & outside).bit_count() + for outside in model.hyperplane_outside) == expected, + "root-remainder cocircuit profile changed") + return {"directions_checked": 120, "size": 56, "minimum_nonzero_deletion": 24} + + +def rejection_controls(model): + rejected = 0 + + def expect_failure(operation): + nonlocal rejected + try: + operation() + except AuditFailure: + rejected += 1 + else: + raise AuditFailure("a deliberately invalid control was accepted") + + quadratic_values = [0] * 256 + for label in model.labels: + quadratic_values[label ^ 256] = 1 + expect_failure(lambda: check_root_class_bijection(model.labels[:-1], quadratic_values)) + expect_failure(lambda: check_root_class_bijection( + [label & 255 for label in model.labels], quadratic_values)) + expect_failure(lambda: validate_class_inventory(set(EXPECTED_PROFILES) - {"norm8"})) + expect_failure(lambda: check(binary_rank(model.mask_labels(model.off_masks[0])) <= 8, + "false full-code weight8 claim")) + frame_remainder = model.off_masks[model.frame[0]] ^ (1 << model.frame[0]) + minimum = min((frame_remainder & outside).bit_count() + for outside in model.hyperplane_outside if frame_remainder & outside) + expect_failure(lambda: check(minimum <= 23, "false remainder erasure threshold")) + return rejected + + +def run_audit(): + model = CartanModel() + check(len(set(model.frame)) == 8, "canonical frame repeats a line") + check(all(model.gram[a][b] == 0 for a, b in combinations(model.frame, 2)), + "canonical frame is not orthogonal") + check(binary_rank(model.labels[i] for i in model.frame) == 4, + "canonical frame label rank is not 4") + caps = quadratic_checks(model) + parabolics, parabolic_summary = parabolic_checks(model) + full_code = full_code_checks(model) + remainders = remainder_checks(model) + normal_filter = normal_filter_checks(model, parabolics) + return { + "schema_version": 1, + "model": {"root_lines": 120, "frame_lines": 8, "frame_label_rank": 4, + "quadratic_gauss_sum": 16}, + "full_cap_bounds": caps, + "full_code": full_code, + "root_remainders": remainders, + "parabolics": parabolic_summary, + "normal_filter": normal_filter, + "rejection_controls": rejection_controls(model), + } + + +if __name__ == "__main__": + print(json.dumps(run_audit(), sort_keys=True, indent=2)) + print("PASS_E8_D0_GEOMETRY_AUDIT") diff --git a/research/e8-d0-root-swaps/verify.py b/research/e8-d0-root-swaps/verify.py new file mode 100644 index 0000000000..7be154af0f --- /dev/null +++ b/research/e8-d0-root-swaps/verify.py @@ -0,0 +1,362 @@ +#!/usr/bin/env python3 +"""Exact coordinate replay of the E8 d=0 root-swap proof inputs. + +Prepared by conorholds with substantial OpenAI Codex assistance. Apache-2.0. +See PROOF.md and SOURCES.json for predecessor credit and exact scope. + +This implementation enumerates Euclidean coordinate patterns. The separate +geometry_audit.py uses Cartan coordinates, reflections and Weyl orbits instead. +Neither imports predecessor code or reads a predecessor PASS receipt. +""" + +from __future__ import annotations + +import argparse +from collections import Counter +from fractions import Fraction +from hashlib import sha256 +from itertools import combinations, product +import json +from pathlib import Path +import sys + + +PACKAGE = Path(__file__).resolve().parent +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), +) +EXPECTED_PROFILES = { + "norm4": [[70, 14, 8, 128], [73, 13, 8, 896], [76, 12, 7, 56]], + "norm6": [[77, 25, None, 2688], [79, 24, None, 448], [80, 24, None, 224]], + "norm8": [[84, 28, None, 1024]], + "a2_plane": [[78, 26, None, 896], [80, 24, None, 224]], + "a1_squared_plane": [[82, 26, None, 448], [84, 24, None, 2688]], +} + + +class VerificationError(ValueError): + """A mathematical or receipt condition failed.""" + + +def require(condition, message): + if not condition: + raise VerificationError(message) + + +def dot(a, b): + return sum(x * y for x, y in zip(a, b)) + + +def canonical(vector): + return vector if next(x for x in vector if x) > 0 else tuple(-x for x in vector) + + +def binary_rank(values): + pivots = {} + for value in values: + while value: + position = value.bit_length() - 1 + if position in pivots: + value ^= pivots[position] + else: + pivots[position] = value + break + return len(pivots) + + +def rational_rank(rows): + matrix = [[Fraction(x) for x in row] for row in rows] + if not matrix: + return 0 + rank = 0 + for column in range(len(matrix[0])): + pivot = next((i for i in range(rank, len(matrix)) if matrix[i][column]), None) + if pivot is None: + continue + matrix[rank], matrix[pivot] = matrix[pivot], matrix[rank] + scale = matrix[rank][column] + matrix[rank] = [x / scale for x in matrix[rank]] + for i in range(rank + 1, len(matrix)): + scale = matrix[i][column] + if scale: + matrix[i] = [x - scale * y for x, y in zip(matrix[i], matrix[rank])] + rank += 1 + if rank == len(matrix): + break + return rank + + +def inverse(matrix): + size = len(matrix) + rows = [[Fraction(x) for x in row] + [Fraction(i == j) for j in range(size)] + for i, row in enumerate(matrix)] + for column in range(size): + pivot = next((i for i in range(column, size) if rows[i][column]), None) + require(pivot is not None, "singular E8 coordinate basis") + rows[column], rows[pivot] = rows[pivot], rows[column] + scale = rows[column][column] + rows[column] = [x / scale for x in rows[column]] + for i in range(size): + if i != column and rows[i][column]: + scale = rows[i][column] + rows[i] = [x - scale * y for x, y in zip(rows[i], rows[column])] + return [row[size:] for row in rows] + + +def integer_lines(twos, ones): + """Doubled integral E8 vectors with twos entries +/-4 and ones +/-2.""" + result = set() + for larger in combinations(range(8), twos): + remaining = [i for i in range(8) if i not in larger] + for smaller in combinations(remaining, ones): + positions = larger + smaller + for signs in product((-1, 1), repeat=len(positions)): + vector = [0] * 8 + for i, sign in zip(positions, signs): + vector[i] = sign * (4 if i in larger else 2) + if sum(vector) % 4 == 0: + result.add(canonical(tuple(vector))) + return result + + +def half_lines(larger_count=0, larger=3): + result = set() + for positions in combinations(range(8), larger_count): + for signs in product((-1, 1), repeat=8): + vector = tuple(sign * (larger if i in positions else 1) + for i, sign in enumerate(signs)) + if sum(vector) % 4 == 0: + result.add(canonical(vector)) + return result + + +def frame_roots(): + result = [] + for sign in (1, -1): + for pair in range(4): + vector = [0] * 8 + vector[2 * pair], vector[2 * pair + 1] = 2, 2 * sign + result.append(tuple(vector)) + return result + + +def indices(mask): + while mask: + bit = mask & -mask + yield bit.bit_length() - 1 + mask ^= bit + + +def support_mask(normal, roots): + return sum(1 << i for i, root in enumerate(roots) if dot(normal, root)) + + +def partitions(total, minimum=1): + if total == 0: + yield () + for part in range(minimum, total + 1): + for rest in partitions(total - part, part): + yield (part,) + rest + + +def partition_checks(caps): + profiles = [p for total in range(1, 8) for p in partitions(total)] + require(len(profiles) == 44, "incomplete low-cost partition enumeration") + require(max(sum(caps[x] for x in p) for p in profiles if sum(p) <= 6) == 20, + "restricted union-support bound is not 20") + require(max(sum(caps[x] for x in p) for p in profiles if len(p) >= 2) == 21, + "full union-support bound is not 21") + require({p for p in profiles if sum(x >= 3 for x in p) >= 2} + == {(3, 3), (3, 4), (1, 3, 3)}, "missing exceptional basis profile") + + +def run_geometry(): + root_set = integer_lines(0, 2) | half_lines() + frame = frame_roots() + require(len(root_set) == 120 and set(frame) <= root_set, "E8 root/frame inventory") + roots = sorted(root_set - set(frame)) + frame + require(all(dot(x, x) == 8 for x in roots), "root norm is not two") + require(all(dot(a, b) == 0 for a, b in combinations(frame, 2)), "frame is not orthogonal") + basis_inverse = inverse(list(zip(*SIMPLE))) + coordinates = [tuple(dot(row, root) for row in basis_inverse) for root in roots] + require(all(x.denominator == 1 for row in coordinates for x in row), + "a root is outside the integral E8 lattice basis") + labels = [1 | sum((int(x) % 2) << (i + 1) for i, x in enumerate(row)) + for row in coordinates] + require(len(set(labels)) == 120 and binary_rank(labels) == 9, "root-class labels") + require(binary_rank(labels[-8:]) == 4, "frame label rank is not four") + gram = [[Fraction(dot(a, b), 4) for b in SIMPLE] for a in SIMPLE] + require(all(x.denominator == 1 for row in gram for x in row), "nonintegral lattice Gram form") + quadratic = [] + for value in range(256): + vector = [(value >> i) & 1 for i in range(8)] + norm = sum(vector[i] * gram[i][j] * vector[j] for i in range(8) for j in range(8)) + require(norm.denominator == 1 and norm % 2 == 0, "lattice is not even") + quadratic.append(int(norm // 2) % 2) + require({label >> 1 for label in labels} == {i for i, q in enumerate(quadratic) if q}, + "root classes are not exactly the nonsingular points") + require(sum(1 - 2 * q for q in quadratic) == 16, "quadratic Gauss sum is not 16") + require(binary_rank(sum((int(gram[i][j]) % 2) << j for j in range(8)) + for i in range(8)) == 8, "quadratic polar form is degenerate") + outside = [sum(1 << i for i, label in enumerate(labels) if (normal & label).bit_count() % 2) + for normal in range(1, 512)] + for cut in outside: + require(rational_rank(roots[i] for i in indices(cut)) == 8, + "a full codeword can have weight at most eight") + off_masks = [support_mask(root, roots) for root in roots] + remainder_profile = Counter({0: 1, 24: 126, 28: 256, 32: 126, 56: 2}) + for i, off in enumerate(off_masks): + remainder = off ^ (1 << i) + require(remainder.bit_count() == 56, "root remainder does not have 56 lines") + require(binary_rank(labels[j] for j in indices(remainder)) == 8, + "root remainder label rank is not eight") + require(Counter((remainder & cut).bit_count() for cut in outside) == remainder_profile, + "root-remainder deletion profile differs") + + large = {} + for subset in range(256): + selected = [i for i, row in enumerate(coordinates) + if all(not x or subset >> j & 1 for j, x in enumerate(row))] + rank = subset.bit_count() + require(rational_rank(roots[i] for i in selected) == rank, "parabolic root rank") + if rank <= 5: + require(len(selected) <= 20, "small parabolic has too many roots") + if rank <= 7 and len(selected) >= 28: + key = (rank, len(selected)) + require(key not in large, "repeated large parabolic seed") + large[key] = subset + require(set(large) == {(6, 30), (6, 36), (7, 28), (7, 37), (7, 42), (7, 63)}, + "large proper parabolic inventory differs") + for (rank, count), subset in large.items(): + if rank == 7: + omitted = next(i for i in range(8) if not subset >> i & 1) + normal = basis_inverse[omitted] + require(4 * dot(normal, normal) == {63: 2, 42: 4, 37: 6, 28: 8}[count], + "fundamental normal norm differs") + else: + perpendicular = [root for root in roots + if all(not subset >> i & 1 or dot(root, SIMPLE[i]) == 0 + for i in range(8))] + require(len(perpendicular) == {36: 3, 30: 2}[count] + and rational_rank(perpendicular) == 2, "normal-plane root system") + + normal_sets = { + "norm4": integer_lines(1, 0) | integer_lines(0, 4) | half_lines(1), + "norm6": integer_lines(1, 2) | integer_lines(0, 6) | half_lines(2), + "norm8": (integer_lines(2, 0) | integer_lines(1, 4) | integer_lines(0, 8) + | half_lines(3) | half_lines(1, 5)) - {tuple(2 * x for x in r) for r in roots}, + } + expected_sizes = {"norm4": 1080, "norm6": 3360, "norm8": 8640} + family_masks = {} + p112 = (1 << 112) - 1 + for name, normals in normal_sets.items(): + require(len(normals) == expected_sizes[name], "normal coordinate inventory: " + name) + require(all(dot(x, x) == 4 * int(name[4:]) for x in normals), "normal coordinate norm") + family_masks[name] = [support_mask(x, roots) & p112 for x in normals] + for name, nonorthogonal, expected in (("a2_plane", True, 1120), + ("a1_squared_plane", False, 3780)): + planes = {off_masks[i] | off_masks[j] for i, j in combinations(range(120), 2) + if bool(dot(roots[i], roots[j])) == nonorthogonal} + require(len(planes) == expected, "root-pair normal-plane inventory: " + name) + family_masks[name] = [off & p112 for off in planes] + normal_filter = {} + for name, masks in family_masks.items(): + counts = Counter() + for off in masks: + size = off.bit_count() + if size > 84: + continue + deletions = [off & cut for cut in outside] + minimum = min(mask.bit_count() for mask in deletions) + small = [mask for mask in deletions if mask.bit_count() <= 20] + minimum_rank = min((binary_rank(labels[i] for i in indices(mask)) for mask in small), + default=None) + if small: + require(minimum_rank >= 7, "non-root normal passes the binary-rank filter") + else: + require(minimum > 20, "non-root normal passes the support-size filter") + counts[(size, minimum, minimum_rank)] += 1 + profiles = [list(key) + [count] for key, count in sorted(counts.items())] + require(profiles == EXPECTED_PROFILES[name], "normal deletion profile differs: " + name) + normal_filter[name] = {"orbit_size": len(masks), "profiles": profiles} + cap8 = max(120 - cut.bit_count() for cut in outside) + require(cap8 == 64, "dimension-eight full-E8 cap is not 64") + caps = {1: 1, 2: 2, 3: 4, 4: 8, 5: 12, 6: 20, 7: 36, 8: cap8} + # PROOF.md gives the uniform Fourier bound; the Cartan checker independently + # checks that Fourier identity and exhausts the required small quadratics. + partition_checks(caps) + return { + "schema_version": 1, + "model": {"root_lines": 120, "frame_lines": 8, "frame_label_rank": 4, + "quadratic_gauss_sum": 16}, + "full_cap_bounds": {str(k): v for k, v in caps.items()}, + "full_code": {"hyperplanes_checked": 511, "minimum_complement_real_rank": 8}, + "root_remainders": {"directions_checked": 120, "size": 56, "minimum_nonzero_deletion": 24}, + "parabolics": {"subsets_checked": 256, + "large_proper_types": [list(key) for key in sorted(large)]}, + "normal_filter": normal_filter, + } + + +def compare_geometry(primary, independent): + for key, value in primary.items(): + require(independent.get(key) == value, "independent geometry mismatch: " + key) + + +def scientific_hashes(): + return {name: sha256((PACKAGE / name).read_bytes()).hexdigest() + for name in ("PROOF.md", "EXTENSION.md", "verify.py", "geometry_audit.py", + "algebra_check.py", "extension_check.py", + "formal/RootSwapOneExceptional.lean", "formal/RootSwapQuartet.lean", + "formal/RootSwapConnectedCover.lean")} + + +def run_all(): + primary = run_geometry() + # Explicitly select package-local source even for isolated (-I) execution. + sys.path.insert(0, str(PACKAGE)) + import geometry_audit + import algebra_check + import extension_check + + independent = geometry_audit.run_audit() + compare_geometry(primary, independent) + algebra = algebra_check.run_checks() + extension = extension_check.run_checks() + return {"schema_version": 1, "geometry": primary, + "independent_geometry_controls": independent["rejection_controls"], + "algebra": algebra, "cost_seven_extension": extension, + "scientific_sha256": scientific_hashes()} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--emit", type=Path, help="create a new receipt; refuse to overwrite") + args = parser.parse_args() + try: + result = run_all() + if args.emit: + with args.emit.open("x", encoding="utf-8") as stream: + json.dump(result, stream, indent=2, sort_keys=True) + stream.write("\n") + else: + expected = json.loads((PACKAGE / "RESULT.json").read_text(encoding="utf-8")) + require(result == expected, "recomputed mathematics or scientific source hashes differ from RESULT.json") + except (OSError, ValueError, KeyError, TypeError) as error: + print("FAIL_E8_D0_ROOT_SWAPS: " + str(error), file=sys.stderr) + return 1 + print("PASS_E8_D0_ROOT_SWAPS geometry=two-exact-methods normal_families=5 " + "root_remainders=120 parabolics=256 " + "extension_models=2 f1_support=24 frame_plane_cases=57120") + return 0 + + +if __name__ == "__main__": + raise SystemExit(main())