diff --git a/research/p112-two-product-compensation/CERTIFICATE.json b/research/p112-two-product-compensation/CERTIFICATE.json new file mode 100644 index 0000000000..e71b87ae65 --- /dev/null +++ b/research/p112-two-product-compensation/CERTIFICATE.json @@ -0,0 +1,728 @@ +{ + "schema_version": 1, + "status": "scoped-copy-obstruction-no-new-kappa", + "base_commit": "cd91ac8e2652bfee6bf09da3b8724253bcf78f5f", + "geometry_source_sha256": "4f44af368e046002553d632ee90c6470990827cea3fae41f0f54018522d7a080", + "root_order": "lexicographic, first nonzero coordinate positive, twice-E8 roots", + "root_order_sha256": "e49bb0dba131174a4436e1a8c4ee5d6dd282664a25737699021c8417792cac45", + "finite": { + "coordinate_pair": [ + 4, + 6 + ], + "ports": 112, + "pairing_rank": 9, + "baseline_coordinate_ranks": [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8 + ], + "pairing_sha256": "438f0a93d8d15d54b9a13bdb03cc6685254af9b84eb430fc6a1a2ec606ff2ca7", + "strata": [ + { + "normal": [ + 1, + 0 + ], + "support_size": 56, + "span_dimension": 8, + "erasure_distance": 24, + "character_weight_histogram": { + "0": 1, + "24": 126, + "28": 256, + "32": 126, + "56": 2 + } + }, + { + "normal": [ + 0, + 1 + ], + "support_size": 56, + "span_dimension": 8, + "erasure_distance": 24, + "character_weight_histogram": { + "0": 1, + "24": 126, + "28": 256, + "32": 126, + "56": 2 + } + }, + { + "normal": [ + 1, + 1 + ], + "support_size": 76, + "span_dimension": 9, + "erasure_distance": 12, + "character_weight_histogram": { + "12": 1, + "32": 2, + "34": 152, + "36": 60, + "38": 80, + "40": 60, + "42": 152, + "44": 2, + "64": 1, + "76": 1 + } + }, + { + "normal": [ + 1, + -1 + ], + "support_size": 76, + "span_dimension": 9, + "erasure_distance": 12, + "character_weight_histogram": { + "12": 1, + "32": 2, + "34": 152, + "36": 60, + "38": 80, + "40": 60, + "42": 152, + "44": 2, + "64": 1, + "76": 1 + } + }, + { + "normal": [ + 1, + 2 + ], + "support_size": 88, + "span_dimension": 9, + "erasure_distance": 24, + "character_weight_histogram": { + "24": 1, + "32": 2, + "40": 188, + "44": 128, + "48": 188, + "56": 2, + "64": 1, + "88": 1 + } + } + ], + "character_evaluations": 2555, + "free_port_pairs": 5824, + "one_sided_records": 2800, + "one_sided_sha256": "189a1c4c6d5983a4b204ba680405b2f8632d6a43ca861e500085697633f1d744", + "two_sided_records": 145600, + "two_sided_sha256": "8c149e2d4ca08f8f84da0622794cede92923a91687e8aaad10ed750385f87141", + "pairs": [ + { + "left": 0, + "right": 0, + "original_rank": 8, + "one_sided_histogram": { + "7": 112 + }, + "one_sided_minimum": 7, + "one_sided_witness": 0, + "two_sided_histogram": { + "6": 1568, + "7": 4256 + }, + "two_sided_minimum": 6, + "two_sided_witness": [ + 0, + 1 + ] + }, + { + "left": 0, + "right": 1, + "original_rank": 8, + "one_sided_histogram": { + "7": 112 + }, + "one_sided_minimum": 7, + "one_sided_witness": 0, + "two_sided_histogram": { + "6": 1440, + "7": 4384 + }, + "two_sided_minimum": 6, + "two_sided_witness": [ + 0, + 1 + ] + }, + { + "left": 0, + "right": 2, + "original_rank": 8, + "one_sided_histogram": { + "7": 112 + }, + "one_sided_minimum": 7, + "one_sided_witness": 0, + "two_sided_histogram": { + "7": 5824 + }, + "two_sided_minimum": 7, + "two_sided_witness": [ + 0, + 1 + ] + }, + { + "left": 0, + "right": 3, + "original_rank": 8, + "one_sided_histogram": { + "7": 112 + }, + "one_sided_minimum": 7, + "one_sided_witness": 0, + "two_sided_histogram": { + "7": 5824 + }, + "two_sided_minimum": 7, + "two_sided_witness": [ + 0, + 1 + ] + }, + { + "left": 0, + "right": 4, + "original_rank": 8, + "one_sided_histogram": { + "7": 112 + }, + "one_sided_minimum": 7, + "one_sided_witness": 0, + "two_sided_histogram": { + "7": 5824 + }, + "two_sided_minimum": 7, + "two_sided_witness": [ + 0, + 1 + ] + }, + { + "left": 1, + "right": 0, + "original_rank": 8, + "one_sided_histogram": { + "7": 112 + }, + "one_sided_minimum": 7, + "one_sided_witness": 0, + "two_sided_histogram": { + "6": 1440, + "7": 4384 + }, + "two_sided_minimum": 6, + "two_sided_witness": [ + 0, + 1 + ] + }, + { + "left": 1, + "right": 1, + "original_rank": 8, + "one_sided_histogram": { + "7": 112 + }, + "one_sided_minimum": 7, + "one_sided_witness": 0, + "two_sided_histogram": { + "6": 1568, + "7": 4256 + }, + "two_sided_minimum": 6, + "two_sided_witness": [ + 0, + 1 + ] + }, + { + "left": 1, + "right": 2, + "original_rank": 8, + "one_sided_histogram": { + "7": 112 + }, + "one_sided_minimum": 7, + "one_sided_witness": 0, + "two_sided_histogram": { + "7": 5824 + }, + "two_sided_minimum": 7, + "two_sided_witness": [ + 0, + 1 + ] + }, + { + "left": 1, + "right": 3, + "original_rank": 8, + "one_sided_histogram": { + "7": 112 + }, + "one_sided_minimum": 7, + "one_sided_witness": 0, + "two_sided_histogram": { + "7": 5824 + }, + "two_sided_minimum": 7, + "two_sided_witness": [ + 0, + 1 + ] + }, + { + "left": 1, + "right": 4, + "original_rank": 8, + "one_sided_histogram": { + "7": 112 + }, + "one_sided_minimum": 7, + "one_sided_witness": 0, + "two_sided_histogram": { + "7": 5824 + }, + "two_sided_minimum": 7, + "two_sided_witness": [ + 0, + 1 + ] + }, + { + "left": 2, + "right": 0, + "original_rank": 8, + "one_sided_histogram": { + "7": 56, + "8": 56 + }, + "one_sided_minimum": 7, + "one_sided_witness": 10, + "two_sided_histogram": { + "7": 5824 + }, + "two_sided_minimum": 7, + "two_sided_witness": [ + 0, + 1 + ] + }, + { + "left": 2, + "right": 1, + "original_rank": 8, + "one_sided_histogram": { + "7": 56, + "8": 56 + }, + "one_sided_minimum": 7, + "one_sided_witness": 8, + "two_sided_histogram": { + "7": 5824 + }, + "two_sided_minimum": 7, + "two_sided_witness": [ + 0, + 1 + ] + }, + { + "left": 2, + "right": 2, + "original_rank": 9, + "one_sided_histogram": { + "8": 112 + }, + "one_sided_minimum": 8, + "one_sided_witness": 0, + "two_sided_histogram": { + "8": 5824 + }, + "two_sided_minimum": 8, + "two_sided_witness": [ + 0, + 1 + ] + }, + { + "left": 2, + "right": 3, + "original_rank": 9, + "one_sided_histogram": { + "8": 112 + }, + "one_sided_minimum": 8, + "one_sided_witness": 0, + "two_sided_histogram": { + "8": 5824 + }, + "two_sided_minimum": 8, + "two_sided_witness": [ + 0, + 1 + ] + }, + { + "left": 2, + "right": 4, + "original_rank": 9, + "one_sided_histogram": { + "8": 112 + }, + "one_sided_minimum": 8, + "one_sided_witness": 0, + "two_sided_histogram": { + "8": 5824 + }, + "two_sided_minimum": 8, + "two_sided_witness": [ + 0, + 1 + ] + }, + { + "left": 3, + "right": 0, + "original_rank": 8, + "one_sided_histogram": { + "7": 56, + "8": 56 + }, + "one_sided_minimum": 7, + "one_sided_witness": 10, + "two_sided_histogram": { + "7": 5824 + }, + "two_sided_minimum": 7, + "two_sided_witness": [ + 0, + 1 + ] + }, + { + "left": 3, + "right": 1, + "original_rank": 8, + "one_sided_histogram": { + "7": 56, + "8": 56 + }, + "one_sided_minimum": 7, + "one_sided_witness": 8, + "two_sided_histogram": { + "7": 5824 + }, + "two_sided_minimum": 7, + "two_sided_witness": [ + 0, + 1 + ] + }, + { + "left": 3, + "right": 2, + "original_rank": 9, + "one_sided_histogram": { + "8": 112 + }, + "one_sided_minimum": 8, + "one_sided_witness": 0, + "two_sided_histogram": { + "8": 5824 + }, + "two_sided_minimum": 8, + "two_sided_witness": [ + 0, + 1 + ] + }, + { + "left": 3, + "right": 3, + "original_rank": 9, + "one_sided_histogram": { + "8": 112 + }, + "one_sided_minimum": 8, + "one_sided_witness": 0, + "two_sided_histogram": { + "8": 5824 + }, + "two_sided_minimum": 8, + "two_sided_witness": [ + 0, + 1 + ] + }, + { + "left": 3, + "right": 4, + "original_rank": 9, + "one_sided_histogram": { + "8": 112 + }, + "one_sided_minimum": 8, + "one_sided_witness": 0, + "two_sided_histogram": { + "8": 5824 + }, + "two_sided_minimum": 8, + "two_sided_witness": [ + 0, + 1 + ] + }, + { + "left": 4, + "right": 0, + "original_rank": 8, + "one_sided_histogram": { + "7": 56, + "8": 56 + }, + "one_sided_minimum": 7, + "one_sided_witness": 10, + "two_sided_histogram": { + "7": 5824 + }, + "two_sided_minimum": 7, + "two_sided_witness": [ + 0, + 1 + ] + }, + { + "left": 4, + "right": 1, + "original_rank": 8, + "one_sided_histogram": { + "7": 56, + "8": 56 + }, + "one_sided_minimum": 7, + "one_sided_witness": 8, + "two_sided_histogram": { + "7": 5824 + }, + "two_sided_minimum": 7, + "two_sided_witness": [ + 0, + 1 + ] + }, + { + "left": 4, + "right": 2, + "original_rank": 9, + "one_sided_histogram": { + "8": 112 + }, + "one_sided_minimum": 8, + "one_sided_witness": 0, + "two_sided_histogram": { + "8": 5824 + }, + "two_sided_minimum": 8, + "two_sided_witness": [ + 0, + 1 + ] + }, + { + "left": 4, + "right": 3, + "original_rank": 9, + "one_sided_histogram": { + "8": 112 + }, + "one_sided_minimum": 8, + "one_sided_witness": 0, + "two_sided_histogram": { + "8": 5824 + }, + "two_sided_minimum": 8, + "two_sided_witness": [ + 0, + 1 + ] + }, + { + "left": 4, + "right": 4, + "original_rank": 9, + "one_sided_histogram": { + "8": 112 + }, + "one_sided_minimum": 8, + "one_sided_witness": 0, + "two_sided_histogram": { + "8": 5824 + }, + "two_sided_minimum": 8, + "two_sided_witness": [ + 0, + 1 + ] + } + ] + }, + "fixtures": { + "cases": [ + { + "name": "sharp-free-singleton", + "rectangle_size": [ + 1, + 1 + ], + "projected_products": 2, + "copy_ranks": [ + 8, + 8, + 0 + ], + "matrix_entries": 12544 + }, + { + "name": "dense-triangular", + "rectangle_size": [ + 1, + 1 + ], + "projected_products": 2, + "copy_ranks": [ + 9, + 9, + 1 + ], + "matrix_entries": 12544 + }, + { + "name": "large-rectangle", + "rectangle_size": [ + 24, + 1 + ], + "projected_products": 2, + "copy_ranks": [ + 7, + 8, + 7 + ], + "matrix_entries": 12544 + }, + { + "name": "compensation-is-required", + "rectangle_size": [ + 24, + 1 + ], + "projected_products": 2, + "copy_ranks": [ + 7, + 8, + 7 + ], + "matrix_entries": 12544 + }, + { + "name": "transpose-branch", + "rectangle_size": [ + 1, + 24 + ], + "projected_products": 2, + "copy_ranks": [ + 8, + 8, + 7 + ], + "matrix_entries": 12544 + }, + { + "name": "three-products", + "rectangle_size": [ + 1, + 1 + ], + "projected_products": 3, + "copy_ranks": [ + 8, + 8, + 9 + ], + "matrix_entries": 12544 + }, + { + "name": "nonreal-rescaling", + "rectangle_size": [ + 1, + 1 + ], + "projected_products": 2, + "copy_ranks": [ + 8, + 8, + 0 + ], + "matrix_entries": 12544 + } + ], + "entry_checks": 100352, + "zero_factor_boundary": { + "projected_products": 3, + "copy_ranks": [ + 8, + 8, + 0 + ] + }, + "omission_invoice": { + "six_unchanged": 48, + "falsely_omitting_compensation": 63, + "complete": 70 + }, + "concavity_combination": { + "weights": [ + "3/4", + "1/8", + "1/8" + ], + "result": [ + 7, + 7, + 2 + ] + }, + "negative_controls": [ + "nonfree-diagonal", + "zero-rectangle-factor", + "singular-factor-change", + "omitted-compensation-identity", + "omitted-compensation-invoice-63-versus-70", + "conjugate-instead-of-ordinary-transpose", + "three-products-without-nonzero-rectangle", + "power-exponent-outside-zero-one" + ] + } +} diff --git a/research/p112-two-product-compensation/PROOF.md b/research/p112-two-product-compensation/PROOF.md new file mode 100644 index 0000000000..dbeddc34ea --- /dev/null +++ b/research/p112-two-product-compensation/PROOF.md @@ -0,0 +1,196 @@ +# Compensation rank closes the two-product branch + +This is a scoped, computer-assisted algebraic proof. Its finite premises are +recomputed by two exact implementations; the quantified argument below is +written mathematics, not a proof-assistant formalization. + +## Statement and model + +Use PR717/PR845's P112 geometry, with its eight deleted orthogonal frame lines, +112 live root lines, coordinate matrix X, and symmetric binary matrix + + XX^T = 2G, X^T X = 56I, B_ij = (1 + G_ij) mod 2. + +Fix x = X[:,4] and y = X[:,6], using zero-based coordinate indices. For complex +column vectors a,b define the separate-total COPY charge + + beta(a,b) = rank_F2 B[supp(a), supp(b)]. + +Let u,v be nonzero complex vectors with U=supp(u), V=supp(v), and B[U,V]=0. +Thus uv^T is a free rectangular correction in this model: it vanishes on +every constrained entry and beta(u,v)=0. For any M in GL(3,C), set + + D = [x,y,u] M, S = [x,y,v] M^(-T). + +Transpose is ordinary, not conjugate. The other six coordinate terms stay +unchanged. Then DS^T = xx^T + yy^T + uv^T, so this is a valid masked identity. + +**Theorem.** If r_j = beta(D[:,j],S[:,j]), then + + r_1+r_2+r_3 >= 16, + r_1^t+r_2^t+r_3^t >= 2*8^t for every real 0=8. +4. Put E(a,j)={i in C(a): B_ij=1}. For all five-by-five support pairs and all + 112 ports j, rank B[E(a,j),C(b)]>=7: 2,800 ranks in total. +5. For all support pairs and all 5,824 ordered pairs (i,j) with B_ij=0, + rank B[E(a,j),E(b,i)] >= 4+nnz(a)+nnz(b)>=6. This is PR1373's credited + premise, replayed across all 145,600 records, including its exact minima. + +For item 2, the primary checker enumerates every nonzero word in the +nine-dimensional row space of B. Because B is symmetric, these are precisely +the values of all nonzero linear functionals on L, evaluated on its spanning +list of rows. The independent checker instead enumerates all 511 nine-bit +functionals on the source's dual labels. Both obtain identical histograms. +Zero restrictions on an eight-dimensional support are excluded only when +taking the *positive* minimum. + +Deleting at most three rows from any C(a) preserves its entire row span. +Otherwise some linear functional would vanish on the remaining rows but not +on the original span, giving a positive restricted weight at most three, +contrary to item 2. This also preserves every further column restriction of +that row span. The independent checker exhibits actual span loss at each of +the five stated erasure distances, so the distance calculation has a boundary +control as well as a lower-bound check. + +## Why only two branches exist + +Let q_j and p_j be the first two entries of columns j of M and M^(-T). +The top-left block of M(M^(-T))^T=I gives + + sum_j q_j p_j^T = I_2. + +At least two of these outer products are nonzero. Thus there are exactly two +or exactly three. Over C, a zero outer product means q_j=0 or p_j=0. + +In the two-product case, permute the three terms so that the zero product is +third. If necessary transpose the entire factorization, exchanging u and v +and replacing M by M^(-T), so that q_3=0. Symmetry of B preserves every charge. +Invertibility now gives the block form + + [ C 0 ] + M = [ d^T e ], C in GL(2,C), e != 0. + +With F=[x,y], put f_j=(FC)[:,j], g_j=(FC^(-T))[:,j], and w=FC^(-T)d. The three +terms, ignoring reciprocal nonzero column scalings, are + + (f_1+d_1*u) g_1^T, + (f_2+d_2*u) g_2^T, + u (v-w)^T. + +Each f_j and g_j is a nonzero two-coordinate normal. The last term is the +compensation term and must be included in the bill. + +## Compensation rank controls support size + +Suppose d!=0. Since F has column rank two, w!=0; put W=supp(w). On columns outside V, +v-w=-w; on columns inside V, every row indexed by U is zero in B. Therefore + + r_3 = rank B[U,supp(v-w)] = rank B[U,W]. (1) + +This is equality of column spans after ignoring zero columns, not an +assumption that supp(v-w)=supp(w). + +Let L_U be the span of the rows of B indexed by U, as a subspace of L. The +coordinate-restriction map pi:L -> F2^W has rank at least eight by +item 2 and symmetry of B, so its kernel has dimension at most one. Equation +(1) says dim pi(L_U)=r_3. Rank-nullity gives + + dim L_U <= r_3+1, |U| <= 2^(r_3+1)-1. (2) + +The second inequality uses the distinct, nonzero row property. In particular, +if r_3<=1, then |U|<=3. Removing U from C(f_j) therefore preserves its full +row span. Outside U, f_j+d_j*u=f_j, so monotonicity of rank and item 3 imply +r_1,r_2>=8. This proves both desired bills in this case. + +If r_3>=2, choose any port k in the nonempty V. Every row in U has B_ik=0, +so E(f_j,k) lies outside U and survives in supp(f_j+d_j*u). The right factor +is g_j without a rectangle correction. Item 4 gives r_1,r_2>=7. Thus the +rank vector dominates (7,7,2) componentwise, proving the sum bound. + +If d=0 instead, both original mixed terms are unchanged, item 3 gives +r_1,r_2>=8, and the third term is the free correction with rank zero. This +completes every two-product case, including the transposed branch. + +## The power bill + +For 0 z^t is increasing and concave on nonnegative reals. The +identity + + (7,7,2) = (3/4)(8,8,0) + (1/8)(8,0,8) + (1/8)(0,8,8) + +and coordinatewise concavity imply 2*7^t+2^t >= 2*8^t. This completes the +two-product power bound; the r_3<=1 and d=0 cases already have two ranks >=8. +The same assertion is false at t=2, as the checked control 102<128 shows. + +For three active products, choose any i in U and j in V. The uncorrected +left and right normals survive on E(q_k,j) and E(p_k,i), respectively, since +these sets are outside U and V. Item 5 gives all three ranks at least six, +as in PR1373. Hence + + (3*6^t)/(2*8^t) = (3/2)(3/4)^t >= 9/8 > 1. + +The total rank sum is at least 18 in that branch. Adding the six unchanged +rank-eight terms establishes the full theorem. At fixed width m, common +multiplicity and normalization, multiplication by m^(-t) preserves the power +comparison. Taking t=1-a yields the separate COPY moment screen for 0<=a<1. + +## Sharpness, failure controls, and limits + +At M=I the replacement ranks are (8,8,0), attaining the full cost 64 and +the full power baseline. The singleton free rectangle in the certificate +also gives a rank-nine masked completion: each singleton vector e_i is +outside col(X), since X^T X=56I and the squared norm of row i is four, so the +projection of e_i onto col(X) has i-th entry 4/56 != 1. Both [X,e_i] and +[X,e_j] have rank nine, and their product has rank nine. + +The literal cancellation fixture uses u=-x on the zero-pairing neighbors of +canonical port 46, v=e_46, C=I, d=(1,0), e=1. The ranks are (7,8,7). Omitting +the compensation term falsely reports 48+7+8=63; its complete bill is 70. +Deleting the term also fails the full matrix identity. Other controls check +nonfree and zero rectangles, singular factor changes, ordinary versus +conjugate transpose, and the required power range. + +All helper preparation, source access, factor mixing, frame changes, copies +other than these charged terms, restoration, hosting and child management +were optimistically assigned zero *additional* cost for this rejection +screen. A nonnegative added expense cannot improve this fixed separate-COPY +comparison. This does not bound a whole supplier with changed widths, +normalization, sharing rules or compensating savings elsewhere. + +The result covers this pair (4,6), nonzero rank-one free corrections, and +three-term invertible mixing, with six coordinate terms fixed. It does not +cover other coordinate pairs, three or more mixed coordinates, multiple free +rectangles, arbitrary nine-term factorizations, other punctures, shared-copy +accounting or zero-factor boundary families. No physical supplier, new kappa, +full compiler/hosting/precision/analytic result or formal multiplication +theorem follows. The algebraic objective is explicit; its physical +interpretation retains the separate-total, drop-free copy-tree assumptions. diff --git a/research/p112-two-product-compensation/README.md b/research/p112-two-product-compensation/README.md new file mode 100644 index 0000000000..dfdf3584c4 --- /dev/null +++ b/research/p112-two-product-compensation/README.md @@ -0,0 +1,130 @@ +# Sharp COPY64 floor for the P112 (4,6) rectangle family + +**Scoped negative result; no new kappa.** On the fixed P112 coordinate pair +(4,6), arbitrary GL(3,C) mixing of two coordinate terms and one nonzero free +rectangle cannot lower the complete separate COPY sum below **64**, or lower +its separate power bill at unchanged width and normalization. + +The new argument closes the **exactly-two projected-product branch** left +open by Cinna Davis's [PR1373](https://github.com/CrocSwap/integer-mult-bounds/pull/1373). +It uses the compensation term's COPY rank to bound its support. Rank at most +one permits at most three support rows; those deletions cannot reduce the +other terms' ranks. Larger compensation rank already pays for possible +losses. Omitting that term in an explicit fixture falsely reports **63**, +while the actual bill is **70**. + +The three-product argument belongs to PR1373. Both implementations here +recheck its finite premise before combining it with the new branch. The +result covers arbitrary nonzero free rectangles for this one coordinate +pair, including rank-nine masked completions. Identity mixing attains 64. +The exact statement, complete coefficient reduction and power inequality are +in [PROOF.md](PROOF.md); executed commands and validation limits are in +[VALIDATION.json](VALIDATION.json). + +## Reproduce + +From the repository root, using Python 3.12 and only its standard library: + +```sh +python3.12 -B scripts/research_package.py --package research/p112-two-product-compensation +``` + +Expected final line: + +```text +PASS_REGISTERED_RESEARCH_PACKAGE research/p112-two-product-compensation outcome=negative-result +``` + +The hook authenticates the base/source pins, runs both checkers and runs three +CLI corruption/export test groups. Direct +commands work with Python 3.10+ and preserve checks under optimized execution: + +```sh +python3 -I -O -B research/p112-two-product-compensation/verify.py +python3 -I -O -B research/p112-two-product-compensation/independent_check.py +``` + +Default replay is read-only. To create a fresh certificate without overwriting +an existing file, use `verify.py --write /tmp/p112-compensation-new.json`. +Use `--check PATH` to check a different certificate. All fields must match. + +## Evidence and boundaries + +[CERTIFICATE.json](CERTIFICATE.json) records all five complex support strata, +2,555 character evaluations, 2,800 one-sided survivor ranks, and 145,600 +credited three-product records. It includes eight exact Gaussian-rational +matrix fixtures covering 100,352 entries, eight semantic negative controls, +the complete compensation bill and a rational concavity witness. +The registered corruption controls also reject altered finite receipts, an +altered compensation invoice, modified source bytes and modified blob pins; +a minimal relocated export passes with assertions disabled. + +The primary checker constructs Euclidean E8 roots and uses 112-bit binary +rows. The separate checker uses the pinned nine-bit labels, a bilinear-image +calculation and a different elimination order. Their complete finite receipts +agree, including every histogram and ordered transcript hash. The separate +checker also verifies five sharp erasure boundaries and an affine-coordinate +omission control. Both implementations are from the same AI-assisted author; +this is code/method independence, not independent human review. + +This is finite exact evidence plus a written proof for all coefficients in +the stated family. It is not a finite search promoted to a universal decoder +theorem. Other pairs, three or more mixed coordinates, multiple rectangles, +arbitrary nine-term factorizations, zero-factor families, other geometries, +shared copies and changed normalization remain outside scope. + +All additional preparation, source access, mixing, frame changes, +restoration, hosting and recursive-child expenses are optimistically free +for the separate COPY rejection screen. No complete supplier or improved +recursive moment is constructed. Physical interpretation retains the +separate-total/drop-free copy-tree assumptions; the selected construction's +all-size/compiler, common-label/mutable-source, whole-call hosting, +precision/tape, analytic and bit H1-H5 obligations remain untouched. + +## Sources, overlap and credit + +Exact base: `cd91ac8e2652bfee6bf09da3b8724253bcf78f5f`. +The selected conditional result at that base is PR1094, +`kappa = 836330098538459/500000000000000000`, with PR589 on PR555 for bits. +Its actual construction and maintainer review were read; no selected cold +replay, native supplier admission or hosted CI is claimed for this package. + +[SOURCES.json](SOURCES.json) pins the live geometry and notices by Git blob +and SHA256, plus the originating catalogue and selected record as historical +provenance. [TASK.json](TASK.json) records the OS seed **46**, three candidate +tasks, local claim, bounded coverage and overlap distinctions. No pinned +sprint issue existed, so the claim was recorded locally. + +- **Cinna Davis, PR1373**, head `3eaef3e4427068b33847dc1147c8a2e5709a970e`: + same pair, three-active-product theorem, and explicit remaining two-product + question. The new branch is the contribution; neither the same seed nor + replaying the predecessor is claimed as novelty. +- **Arham Tahir, PR1331**, head `f08b698cc2bd74e2425486728a008e531fc35f0e`: + one-coordinate rectangle obstruction and survivor-containment method. +- **@commdata2338, PR1375**, head `4a533aff2a7a87c9b36e077a31774b332a7f64bd`: + all-pair small-rectangle result and erasure distances. This package handles + unbounded rectangle support on (4,6) through compensation accounting. +- **Hanson Sun / @bbMisk, concurrent [PR1432](https://github.com/CrocSwap/integer-mult-bounds/pull/1432)**, + head `4bcc49e3f4041018b0607da46a87d8928a6e0fd0`: fixed 24-row support on + (0,1), arbitrary amplitudes including zero factors. That result is not a + dependency. The reported (7,8,7) compensation pattern is independently + corroborated here on (4,6); this package removes the support-size cap for + nonzero rectangles on that pair through a different support-rank argument. +- **Mihir Srivastava, PR845**, and **DreamingOfClouds, PR717/446**: + exact geometry snapshot, binary labels, masked model and physical COPY + convention. **Joel Pulikkan / GamingPuzzled, PR620**: coordinate COPY64 + construction. The pinned PR845 and PR717 notices retain their wider + predecessor and AI-assistance attribution. + +Prepared for **Hanson Sun (@bbMisk)** with substantial **OpenAI Codex** +assistance in mathematics, implementation, checking and writing. New work is +Apache-2.0. + +## Open next questions + +Can three or more original coordinate terms mixed with one free rectangle +reduce the complete COPY power bill? This changes a remaining restriction of +the theorem. The first useful step is a minimal-active-product normal form +and a compensation-support bound before physical synthesis. New projective +support classes and simultaneous survivor-rank bounds are the blockers; +this package does not predict a gain. See the structured question in TASK.json. diff --git a/research/p112-two-product-compensation/SOURCES.json b/research/p112-two-product-compensation/SOURCES.json new file mode 100644 index 0000000000..cf3295e07c --- /dev/null +++ b/research/p112-two-product-compensation/SOURCES.json @@ -0,0 +1,70 @@ +{ + "schema_version": 1, + "base_commit": "cd91ac8e2652bfee6bf09da3b8724253bcf78f5f", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "c05fafaa25ba95b2d5af86b1800427198e3d20eb", + "sha256": "89b5928bc92c81e2647b6d702a7ad85a6795b8f44e2eb267b2ff3145d8f2b2ce" + }, + { + "path": "research/p112-single-lift/NOTICE.md", + "usage": "input", + "git_blob": "eb811ef7e601441f07c996fa3a265639b354eb8f", + "sha256": "54fcd00460fed3afecad295c0e8310cc1f44d00a21c9ac2872be8c4e3ca26dbe" + }, + { + "path": "research/p112-single-lift/SOURCES.json", + "usage": "input", + "git_blob": "a36ad2fa75d5f2bbce60997a4caa21b0f12786c3", + "sha256": "3895e1e5d97987d760fca7ef124cccabcfe5a675ce2928c1c9b2de1f48bb7667" + }, + { + "path": "research/p112-single-lift/reference-geometry.json", + "usage": "input", + "git_blob": "d862663d3c0ffe3c72df510e89997beb85cef640", + "sha256": "4f44af368e046002553d632ee90c6470990827cea3fae41f0f54018522d7a080" + }, + { + "path": "research/p112-single-lift/reference/PR717-NOTICE.md", + "usage": "input", + "git_blob": "481f6bf99bb19c7f2f73b0991a751b6b9187b16c", + "sha256": "7809c20cd037dcc29edb5207cbc333bed7b2bd1026cb4f1137f150de90d6866d" + } + ], + "citation_only_predecessors": [ + { + "pr": 1373, + "head": "3eaef3e4427068b33847dc1147c8a2e5709a970e", + "author": "Cinna Davis", + "path": "research/p112-gl3-survivors-seed46/PROOF.md", + "sha256": "06ee789e727d63b2bc4bd3daad6783488d7e0278fdb43139ed965e372b5411e9", + "role": "Credited three-product proof; its geometry premise is recomputed by both new checkers, with no predecessor code execution." + }, + { + "pr": 1331, + "head": "f08b698cc2bd74e2425486728a008e531fc35f0e", + "author": "Arham Tahir", + "role": "One-coordinate rectangle predecessor and survivor-containment method." + }, + { + "pr": 1375, + "head": "4a533aff2a7a87c9b36e077a31774b332a7f64bd", + "author": "commdata2338", + "role": "All-pair small-support result; same finite erasure distances, different support boundary." + }, + { + "pr": 1432, + "head": "4bcc49e3f4041018b0607da46a87d8928a6e0fd0", + "author": "Hanson Sun / bbMisk", + "role": "Concurrent fixed pair (0,1), fixed 24-row support, arbitrary-amplitude result; not a theorem/code dependency. Its reported (7,8,7) compensation pattern is independently corroborated on (4,6)." + } + ] +} diff --git a/research/p112-two-product-compensation/TASK.json b/research/p112-two-product-compensation/TASK.json new file mode 100644 index 0000000000..8d153c0ab0 --- /dev/null +++ b/research/p112-two-product-compensation/TASK.json @@ -0,0 +1,154 @@ +{ + "schema_version": 1, + "task_id": "complex-masked-decoder", + "priority_revision": 2, + "base_commit": "cd91ac8e2652bfee6bf09da3b8724253bcf78f5f", + "original_card": { + "id": "complex-masked-decoder", + "question": "Can one specified masked or overcomplete decoder improve the complete moment budget?", + "starting_points": [ + "research/complex-decoder-field-extension-seed44/README.md", + "research/complex-frame-pair-decoders/README.md" + ], + "methods": [ + "Synthesize a decoder with exact coefficients and fully priced helper endpoints.", + "Bound the best possible budget for a fixed support alphabet before synthesis." + ], + "acceptance_gate": "Change an assumption of the eight-term all-pairs bound and count all copied information, frames and restoration.", + "first_step": { + "command": [ + "python3", + "-B", + "research/complex-decoder-field-extension-seed44/verify.py" + ], + "expected": "PASS_COMPLEX_DECODER_FIELD_EXTENSION_S44", + "inspect": "Locate the excluded classes: masked identities, at least nine terms, and deeper punctures.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Choose one finite support alphabet and test exact decoding constraints before building a whole network.", + "bottleneck_link": "A cheaper fully realized decoder could increase deficit or lower recursive cost on the binding complex side.", + "allowed_variations": [ + "Select a specific masked or overcomplete family with exact labels and supports." + ], + "scope_change_triggers": [ + "Repeating the exact eight-term all-pairs search inside its proved scope." + ], + "overlap_terms": [ + "masked decoder", + "overcomplete", + "eight-term" + ] + }, + "scope_status": "refined", + "actual_scope": "P112 coordinate pair (4,6), nonzero arbitrary free rectangles B[U,V]=0, and every GL(3,C) factor change. New theorem handles exactly two active coordinate products; the three-product branch is credited to PR1373 and independently replayed.", + "scope_change_reason": "User seed46 assigns structural decoder research. The task is the exactly-two projected-product branch excluded by PR1373, using a new compensation-rank support bound, with a fixed-pair full-GL3 corollary after independently replaying its three-product premise.", + "bottleneck_link": "The complex supplier is binding at the selected record. This tests a masked rank-nine route to reduce its separate COPY power bill, with all added physical expenses optimistically free.", + "budget_minutes": 60, + "stop_rule": "Complete all five projective support strata, 2555 nonzero-character evaluations, 2800 one-sided survivor ranks, and the 145600 credited three-product premise records; then prove or reject the compensation-rank bound. No unbounded coefficient search. Reserve the final 15 of 60 minutes for verification and handoff.", + "outcome": "negative-result", + "evidence": "PROOF.md plus exact CERTIFICATE.json regenerated by verify.py and checked with the differently implemented independent_check.py.", + "author": "Hanson Sun (@bbMisk)", + "ai_assistance": "Substantial OpenAI Codex assistance in mathematics, implementation, verification and prose; both implementations are from the same AI-assisted contributor, not independent human review.", + "open_questions": [ + { + "question": "Can mixing three or more original coordinate terms with one free rectangle reduce the complete COPY power bill?", + "why_it_matters": "This is outside the two-coordinate theorem and may change the copied-information profile.", + "first_step": "Derive the minimal-active-product block-triangular normal form and test the same compensation-rank support bound before any physical synthesis.", + "blocked_by": "New support classes and simultaneous survivor rank bounds are required; this result gives no cost bound for that larger family." + } + ], + "assignment_seed": 46, + "user_track": "structural-decoder", + "claim": { + "track": "structural-decoder", + "assignment_seed": 46, + "base_commit": "cd91ac8e2652bfee6bf09da3b8724253bcf78f5f", + "started_utc": "2026-10-14T00:27:54.650447+00:00", + "expected_finish_utc": "2026-10-14T01:27:55Z", + "claim_location": "local: no pinned sprint coordination issue", + "scope": "P112 coordinates (4,6), arbitrary nonzero free rectangle, GL(3,C) changes with exactly two nonzero original-coordinate outer products; isolate the triangular normal form and bound all three COPY terms.", + "candidate_tasks": [ + { + "task": "rank-nine singleton masked completion", + "decision": "not chosen; Discussion1360 already claims every nine-term factorization" + }, + { + "task": "24-row free-compatible first span-loss witness", + "decision": "not chosen; Discussion1316 active bbMisk seed39 claim investigates this fixed witness" + }, + { + "task": "exactly-two projected-product branch with arbitrary free rectangles", + "decision": "chosen; complementary algebraic branch excluded by PR1373, broader supports than PR1375" + } + ], + "method": "triangular GL3 normal form, exhaustive projective two-coordinate support classes, exact binary survivor ranks, compensation-term accounting; one bounded pivot if this screen is inconclusive", + "domain": "fixed pair (4,6), all complex GL3 matrices with exactly two active projected outer products, all nonzero u,v satisfying B[supp u,supp v]=0", + "budget": "seek COPY sum below16 or smaller sum of r^(1-a) at unchanged width and normalization, granting all extra physical overhead zero", + "deliverable": "scoped proof or exact counterexample, standard-library checker, source pins, semantic negative controls; no new kappa claim", + "prior_work": { + "1331": "f08b698cc2bd74e2425486728a008e531fc35f0e", + "1373": "3eaef3e4427068b33847dc1147c8a2e5709a970e", + "1375": "4a533aff2a7a87c9b36e077a31774b332a7f64bd" + }, + "protected_invariant": "Every asserted COPY bill includes the compensation term and uses exact supports; finite strata support a stated algebraic proof, not a full multiplication theorem." + }, + "overlap_checks": [ + { + "searched_at": "2026-10-14T00:31:12.151135+00:00", + "terms": [ + "two projected", + "two-product", + "two active", + "GL(3", + "24-row" + ], + "coverage": { + "open_prs": { + "fetched_at": "2026-10-14T00:30:50.756376+00:00", + "complete_pagination": true, + "records": 794 + }, + "discussions": { + "fetched_at": "2026-10-14T00:31:12.101000+00:00", + "complete_pagination": true, + "records": 143 + } + }, + "warnings": [], + "limits": "Remote PR scope is open PRs including drafts. Closed work is searched through local READMEs, TASK metadata and ledger only. No code diffs or arbitrary package files are searched. Recheck relevant heads before submission." + }, + { + "searched_at": "2026-10-14T00:49:44.699073+00:00", + "terms": [ + "two-product", + "compensation rank", + "GL(3", + "two projected" + ], + "coverage": { + "open_prs": { + "fetched_at": "2026-10-14T00:49:27.043808+00:00", + "complete_pagination": true, + "records": 797 + }, + "discussions": { + "fetched_at": "2026-10-14T00:49:44.654164+00:00", + "complete_pagination": true, + "records": 149 + } + }, + "warnings": [], + "limits": "Remote PR scope is open PRs including drafts. Closed work is searched through local READMEs, TASK metadata and ledger only. No code diffs or arbitrary package files are searched. Recheck relevant heads before submission." + } + ], + "seed_diversification": "Decimal digits select zero-based coordinates (4,6), matching the open branch in PR1373; the fixture uses canonical port 46. The distinct contribution is compensation accounting, not the seed or pair choice.", + "current_upstream_check": { + "head": "410026dc5513b87db92ae98571d1d5984c69a983", + "result": "All live geometry/notice inputs, catalogue and selected record match the exact base; only unrelated reconciliation metadata changed." + }, + "nearest_concurrent_result": { + "pr": 1432, + "head": "4bcc49e3f4041018b0607da46a87d8928a6e0fd0", + "distinction": "Fixed 24-row support on pair (0,1), including zero factors, versus arbitrary nonzero rectangle supports on pair (4,6); compensation-rank support bound closes PR1373 two-product branch." + } +} diff --git a/research/p112-two-product-compensation/VALIDATION.json b/research/p112-two-product-compensation/VALIDATION.json new file mode 100644 index 0000000000..f2f01471e3 --- /dev/null +++ b/research/p112-two-product-compensation/VALIDATION.json @@ -0,0 +1,83 @@ +{ + "status": "local-scoped-verification-complete", + "base_commit": "cd91ac8e2652bfee6bf09da3b8724253bcf78f5f", + "checked_upstream_head": "410026dc5513b87db92ae98571d1d5984c69a983", + "environment": { + "platform": "macOS-27.0.1-arm64-arm-64bit-Mach-O", + "registered_python": "Python 3.12.13", + "optimized_python": "3.14.6", + "dependencies": "Python standard library only" + }, + "commands": [ + { + "argv": [ + "python3.12", + "-B", + "scripts/research_package.py", + "--package", + "research/p112-two-product-compensation" + ], + "result": "PASS_REGISTERED_RESEARCH_PACKAGE research/p112-two-product-compensation outcome=negative-result", + "coverage": "Both finite-premise implementations, exact fixtures, eight semantic controls, three CLI corruption/export test groups." + }, + { + "argv": [ + "python3", + "-I", + "-O", + "-B", + "research/p112-two-product-compensation/verify.py" + ], + "result": "PASS_P112_TWO_PRODUCT_COMPENSATION" + }, + { + "argv": [ + "python3", + "-I", + "-O", + "-B", + "research/p112-two-product-compensation/independent_check.py" + ], + "result": "PASS_P112_COMPENSATION_INDEPENDENT" + }, + { + "argv": [ + "python3.12", + "-B", + "-m", + "unittest", + "discover", + "-s", + "tests", + "-p", + "test_research_*.py", + "-v" + ], + "result": "20 tests passed" + }, + { + "argv": [ + "python3", + "-B", + "scripts/verify_selected_result.py" + ], + "result": "PASS selected record, exact kappa, original source inventory and proof supplement: 836330098538459/500000000000000000" + } + ], + "artifact_sha256": { + "CERTIFICATE.json": "8ee4249397f879fecfac63695fe547badddd8492533279689c71079ae943aa1b", + "PROOF.md": "23fd3a89b641a7f1265d267cf7ba129c8417b0cdfe1f5217b4a2e8f8ca71fb7f", + "verify.py": "181b78799b1464bf74e53e09f416c6e0540fdbf82c1fd1b4585054194c169650", + "independent_check.py": "29f6a9ae7028122d75695bc2766a5ef3866971687e7dbf87e23d40c50ae592e1", + "test_controls.py": "0bd07fdbf8023d49ca33ce24c109d72efbcc48aa92265e1e449113568e91af03" + }, + "comparison_scope": "Both engines agree on the entire finite receipt, including histogram entries and every ordered transcript digest. The separate checker does not independently replay the Gaussian-rational fixture implementation. All repeated runs followed source changes or new failure controls.", + "unrun": [ + "full selected-supplier cold replay", + "native compiler or physical supplier admission", + "hosted CI at the time of this local record", + "proof-assistant formalization", + "independent human review" + ], + "limitations": "Quantified coefficient coverage follows the written support-stratum and compensation-rank proof, not a numerical search. Only coordinate pair (4,6), nonzero rank-one free corrections, six unchanged coordinate terms and the separate-total COPY objective are covered." +} diff --git a/research/p112-two-product-compensation/VERIFY.json b/research/p112-two-product-compensation/VERIFY.json new file mode 100644 index 0000000000..9f29b7b9ef --- /dev/null +++ b/research/p112-two-product-compensation/VERIFY.json @@ -0,0 +1,44 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/p112-single-lift/NOTICE.md", + "research/p112-single-lift/SOURCES.json", + "research/p112-single-lift/reference-geometry.json", + "research/p112-single-lift/reference/PR717-NOTICE.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact P112 geometry and finite support premises; full factorization and compensation fixtures; semantic negative controls; deterministic certificate comparison" + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/independent_check.py" + ], + "timeout_seconds": 120, + "checks": "Independent nine-bit label and low-pivot rank replay of all finite support premises against the entire finite certificate" + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/test_controls.py" + ], + "timeout_seconds": 120, + "checks": "Relocated optimized export; CLI rejects altered finite and compensation receipts, changed source bytes and changed Git blob pins" + } + ] +} diff --git a/research/p112-two-product-compensation/independent_check.py b/research/p112-two-product-compensation/independent_check.py new file mode 100644 index 0000000000..f2cc6451e7 --- /dev/null +++ b/research/p112-two-product-compensation/independent_check.py @@ -0,0 +1,153 @@ +#!/usr/bin/env python3 +"""Independent nine-bit-label replay; imports no package/predecessor code. + +Hanson Sun (@bbMisk), substantial OpenAI Codex assistance. Apache-2.0. +Uses PR845's pinned PR717 labels, low-pivot elimination and bilinear images, +instead of the primary checker's Euclidean construction and 112-bit rows. +The shared input and same AI-assisted author limit the independence claim. +""" +from collections import Counter +import hashlib +import json +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +SOURCE = "research/p112-single-lift/reference-geometry.json" +NORMALS = [(1, 0), (0, 1), (1, 1), (1, -1), (1, 2)] + + +def check(ok, message): + if not ok: + raise ValueError(message) + + +def sha(value): + return hashlib.sha256(value).hexdigest() + + +def encoded(value): + return json.dumps(value, sort_keys=True, separators=(",", ":")).encode() + + +def parity(value): + return value.bit_count() % 2 + + +def spanning(rows): + pivots = {} + for value in rows: + while value: + bit = value & -value + if bit in pivots: + value ^= pivots[bit] + else: + pivots[bit] = value + break + return list(pivots.values()) + + +def image_rank(left, right): + images = [] + for r in right: + image = 0 + for i, l in enumerate(left): + image |= parity(l & r) << i + images.append(image) + return len(spanning(images)) + + +def canonical_root(row): + sign = 1 if next(t for t in row if t) > 0 else -1 + return tuple(sign * t for t in row) + + +def main(): + pins = json.loads((HERE / "SOURCES.json").read_text()) + for entry in pins["files"]: + if entry["usage"] == "input": + raw = (ROOT / entry["path"]).read_bytes() + check(sha(raw) == entry["sha256"], "source hash") + check(hashlib.sha1(b"blob " + str(len(raw)).encode() + b"\0" + raw).hexdigest() + == entry["git_blob"], "source blob") + raw = (ROOT / SOURCE).read_bytes() + source = json.loads(raw) + expected = json.loads((HERE / "CERTIFICATE.json").read_text()) + order = sorted(range(112), key=lambda i: canonical_root(source["roots"][i])) + x = [source["X"][i] for i in order] + check(all(sum(row[i] * row[j] for row in x) == 56 * (i == j) + for i in range(8) for j in range(8)), "coordinate independence") + labels = [source["labels"][i] for i in order] + duals = [source["duals"][i] for i in order] + check(len(set(labels)) == len(set(duals)) == 112 and all(labels) and all(duals), "distinct nonzero labels") + check(len(spanning(labels)) == len(spanning(duals)) == 9, "ambient dimensions") + b = [[parity(a & c) for c in labels] for a in duals] + for i in range(112): + for j in range(112): + rr, ss = source["roots"][order[i]], source["roots"][order[j]] + gram4 = sum(a * c for a, c in zip(rr, ss)) + check(gram4 % 4 == 0 and b[i][j] == (1 + gram4 // 4) % 2, "all-entry Gram/label binding") + check(b[i][j] == b[j][i], "symmetric pairing") + b_words = [sum(t << j for j, t in enumerate(row)) for row in b] + check(sha(raw) == expected["geometry_source_sha256"], "receipt source") + roots = [canonical_root(source["roots"][i]) for i in order] + check(sha(encoded(roots)) == expected["root_order_sha256"], "canonical root order") + supports = [[i for i, row in enumerate(x) if a * row[4] + c * row[6]] for a, c in NORMALS] + coordinate_ranks = [] + for k in range(8): + points = [i for i, row in enumerate(x) if row[k]] + coordinate_ranks.append(image_rank(spanning(duals[i] for i in points), spanning(labels[i] for i in points))) + check(coordinate_ranks == [8] * 8, "all eight coordinate charges") + strata, erasure_witnesses = [], [] + for normal, points in zip(NORMALS, supports): + weights = [sum(parity(t & duals[i]) for i in points) for t in range(1, 512)] + dimension = len(spanning(duals[i] for i in points)) + distance = min(w for w in weights if w) + check(dimension >= 8 and distance > 3, "span robustness") + histogram = dict(sorted(Counter(weights).items())) + strata.append({"normal": list(normal), "support_size": len(points), "span_dimension": dimension, + "erasure_distance": distance, "character_weight_histogram": histogram}) + witness = weights.index(distance) + 1 + survivors = [duals[i] for i in points if not parity(witness & duals[i])] + check(len(spanning(survivors)) < dimension, "sharp erasure boundary must lose span") + erasure_witnesses.append({"character": witness, "deleted": distance, + "remaining_dimension": len(spanning(survivors))}) + left_full = [spanning(duals[i] for i in points) for points in supports] + right_full = [spanning(labels[i] for i in points) for points in supports] + left_slices = [[spanning(duals[i] for i in points if b[i][j]) for j in range(112)] + for points in supports] + right_slices = [[spanning(labels[i] for i in points if b[i][j]) for j in range(112)] + for points in supports] + free = [(i, j) for i in range(112) for j in range(112) if b[i][j] == 0] + check(len(free) == 5824, "free-pair coverage") + pairs, one_trace, two_trace = [], bytearray(), bytearray() + for a in range(5): + for c in range(5): + original = image_rank(left_full[a], right_full[c]) + one = [image_rank(l, right_full[c]) for l in left_slices[a]] + two = [image_rank(left_slices[a][j], right_slices[c][i]) for i, j in free] + check(original >= 8 and min(one) >= 7 and min(two) >= 6, "survivor floors") + check(min(two) == 4 + sum(bool(t) for t in NORMALS[a]) + sum(bool(t) for t in NORMALS[c]), + "credited PR1373 refined floor") + one_trace.extend(one) + two_trace.extend(two) + pairs.append({"left": a, "right": c, "original_rank": original, + "one_sided_histogram": dict(sorted(Counter(one).items())), + "one_sided_minimum": min(one), "one_sided_witness": one.index(min(one)), + "two_sided_histogram": dict(sorted(Counter(two).items())), + "two_sided_minimum": min(two), "two_sided_witness": list(free[two.index(min(two))])}) + actual = {"coordinate_pair": [4, 6], "ports": 112, "pairing_rank": image_rank(spanning(duals), spanning(labels)), + "baseline_coordinate_ranks": coordinate_ranks, + "pairing_sha256": sha(encoded(b_words)), "strata": strata, "character_evaluations": 2555, + "free_port_pairs": len(free), "one_sided_records": len(one_trace), "one_sided_sha256": sha(one_trace), + "two_sided_records": len(two_trace), "two_sided_sha256": sha(two_trace), "pairs": pairs} + check(json.loads(json.dumps(actual)) == expected["finite"], "complete finite-premise receipt mismatch") + # A missing affine coordinate changes rank nine to rank eight. + unshifted = [sum((1 - t) << j for j, t in enumerate(row)) for row in b] + check(len(spanning(unshifted)) == 8, "affine omission boundary") + print("PASS_P112_COMPENSATION_INDEPENDENT characters=2555 one_sided=2800 " + "three_product_records=145600 sharp_erasure_controls=5 affine_control=1") + + +if __name__ == "__main__": + main() diff --git a/research/p112-two-product-compensation/test_controls.py b/research/p112-two-product-compensation/test_controls.py new file mode 100644 index 0000000000..39de2f73fc --- /dev/null +++ b/research/p112-two-product-compensation/test_controls.py @@ -0,0 +1,79 @@ +#!/usr/bin/env python3 +"""CLI corruption and relocated-export controls for the research evidence. + +Hanson Sun (@bbMisk), with substantial OpenAI Codex assistance. Apache-2.0. +""" +import copy +import json +from pathlib import Path +import shutil +import subprocess +import sys +import tempfile +import unittest + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +PACKAGE = HERE.relative_to(ROOT) + + +class EvidenceControls(unittest.TestCase): + def setUp(self): + self.tmp = tempfile.TemporaryDirectory(prefix="p112-compensation-") + self.addCleanup(self.tmp.cleanup) + self.root = Path(self.tmp.name) + self.package = self.root / PACKAGE + self.package.mkdir(parents=True) + for name in ("verify.py", "independent_check.py", "SOURCES.json", "CERTIFICATE.json"): + shutil.copyfile(HERE / name, self.package / name) + self.pins = json.loads((HERE / "SOURCES.json").read_text()) + for pin in self.pins["files"]: + if pin["usage"] == "input": + target = self.root / pin["path"] + target.parent.mkdir(parents=True, exist_ok=True) + shutil.copyfile(ROOT / pin["path"], target) + + def run_checker(self, name, expected_error=None, *extra): + result = subprocess.run([sys.executable, "-I", "-O", "-B", str(self.package / name), *extra], + cwd=self.root, capture_output=True, text=True, timeout=120) + if expected_error is None: + self.assertEqual(result.returncode, 0, result.stderr) + self.assertIn("PASS_P112", result.stdout) + else: + self.assertNotEqual(result.returncode, 0, result.stdout) + self.assertIn(expected_error, result.stderr) + + def test_relocated_optimized_export(self): + # No .git, imported predecessor code, third-party packages, or package directory on sys.path. + self.run_checker("verify.py") + self.run_checker("independent_check.py") + + def test_complete_receipt_binding(self): + path = self.package / "CERTIFICATE.json" + original = json.loads(path.read_text()) + changed = copy.deepcopy(original) + changed["finite"]["one_sided_records"] -= 1 + path.write_text(json.dumps(changed)) + self.run_checker("verify.py", "complete certificate mismatch") + self.run_checker("independent_check.py", "complete finite-premise receipt mismatch") + changed = copy.deepcopy(original) + changed["fixtures"]["omission_invoice"]["complete"] = 63 + path.write_text(json.dumps(changed)) + self.run_checker("verify.py", "complete certificate mismatch") + + def test_source_bytes_and_blob_binding(self): + pin = next(p for p in self.pins["files"] if p["path"].endswith("reference-geometry.json")) + path = self.root / pin["path"] + original = path.read_bytes() + path.write_bytes(original + b"\n") + self.run_checker("verify.py", "source SHA256 drift") + self.run_checker("independent_check.py", "source hash") + path.write_bytes(original) + pin["git_blob"] = "0" * 40 + (self.package / "SOURCES.json").write_text(json.dumps(self.pins)) + self.run_checker("verify.py", "source Git blob drift") + self.run_checker("independent_check.py", "source blob") + + +if __name__ == "__main__": + unittest.main(verbosity=2) diff --git a/research/p112-two-product-compensation/verify.py b/research/p112-two-product-compensation/verify.py new file mode 100644 index 0000000000..4f6595c60e --- /dev/null +++ b/research/p112-two-product-compensation/verify.py @@ -0,0 +1,379 @@ +#!/usr/bin/env python3 +"""Exact premises for the P112 two-product compensation proof. + +Hanson Sun (@bbMisk), with substantial OpenAI Codex assistance. Apache-2.0. +Geometry: DreamingOfClouds PR717; exact snapshot: Mihir Srivastava PR845. +The three-product survivor premise is credited to Cinna Davis PR1373. +No predecessor code is imported; no floating-point arithmetic is used. +""" +import argparse +from collections import Counter +from dataclasses import dataclass +from fractions import Fraction +import hashlib +from itertools import combinations, product +import json +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +SOURCE = "research/p112-single-lift/reference-geometry.json" +PAIR = (4, 6) +NORMALS = ((1, 0), (0, 1), (1, 1), (1, -1), (1, 2)) + + +def require(ok, message): + if not ok: + raise ValueError(message) + + +def digest(data): + return hashlib.sha256(data).hexdigest() + + +def canonical(data): + return json.dumps(data, sort_keys=True, separators=(",", ":")).encode() + + +def basis(rows): + pivots = {} + for row in rows: + while row: + p = row.bit_length() - 1 + if p in pivots: + row ^= pivots[p] + else: + pivots[p] = row + break + return [pivots[p] for p in sorted(pivots)] + + +def rank(rows): + return len(basis(rows)) + + +def indices(mask): + while mask: + bit = mask & -mask + yield bit.bit_length() - 1 + mask ^= bit + + +def support(values): + return sum(1 << i for i, value in enumerate(values) if value) + + +def dot(x, y): + return sum(a * b for a, b in zip(x, y)) + + +def root_key(row): + row = tuple(row) + return row if next(x for x in row if x) > 0 else tuple(-x for x in row) + + +def load_source(): + pins = json.loads((HERE / "SOURCES.json").read_text()) + for entry in pins["files"]: + if entry["usage"] != "input": + continue + raw = (ROOT / entry["path"]).read_bytes() + require(digest(raw) == entry["sha256"], "source SHA256 drift: " + entry["path"]) + blob = hashlib.sha1(b"blob " + str(len(raw)).encode() + b"\0" + raw).hexdigest() + require(blob == entry["git_blob"], "source Git blob drift: " + entry["path"]) + return json.loads((ROOT / SOURCE).read_text()) + + +def geometry(source): + roots = set() + for i, j in combinations(range(8), 2): + for sign in (-1, 1): + r = [0] * 8 + r[i], r[j] = 2, 2 * sign + roots.add(tuple(r)) + for tail in product((-1, 1), repeat=7): + r = (1, *tail) + if r.count(-1) % 2 == 0: + roots.add(r) + frame = [] + for i in range(0, 8, 2): + for sign in (1, -1): + r = [0] * 8 + r[i], r[i + 1] = 2, 2 * sign + frame.append(r) + require(len(roots) == 120, "E8 line coverage") + roots = sorted(roots - {tuple(r) for r in frame}) + require(frame == source["frame"], "frame order") + require(set(roots) == {root_key(r) for r in source["roots"]}, "root source binding") + require(len(roots) == 112, "P112 coverage") + require(all(dot(r, f) % 4 == 0 for r in roots for f in frame), "integral frame coordinates") + x = [[dot(r, f) // 4 for f in frame] for r in roots] + require(all(sum(row[i] * row[j] for row in x) == 56 * (i == j) + for i in range(8) for j in range(8)), "X^T X = 56I") + source_index = {root_key(r): i for i, r in enumerate(source["roots"])} + for r, row in zip(roots, x): + i = source_index[r] + sign = 1 if tuple(source["roots"][i]) == r else -1 + require(row == [sign * z for z in source["X"][i]], "X source binding") + require(set(row) <= {-1, 0, 1} and dot(row, row) == 4, "coordinate alphabet") + b = [] + for i, r in enumerate(roots): + row = 0 + for j, s in enumerate(roots): + require(dot(r, s) % 4 == 0, "integral Gram") + gram = dot(r, s) // 4 + require(dot(x[i], x[j]) == 2 * gram, "XX^T = 2G") + row |= ((1 + gram) % 2) << j + b.append(row) + require(rank(b) == 9 and len(set(b)) == 112 and all(b), "distinct nonzero rank-nine rows") + require(all(b[i] >> i & 1 for i in range(112)), "affine diagonal") + return roots, x, b + + +def finite_premises(x, b): + coordinate_masks = [support(row[j] for row in x) for j in range(8)] + coordinate_ranks = [rank(b[i] & mask for i in indices(mask)) for mask in coordinate_masks] + require(coordinate_ranks == [8] * 8, "all eight baseline coordinate charges") + masks = [support(a * row[PAIR[0]] + c * row[PAIR[1]] for row in x) + for a, c in NORMALS] + words = [0] + for row in basis(b): + words += [w ^ row for w in words] + require(len(set(words)) == 512, "complete binary character space") + strata = [] + for n, mask in zip(NORMALS, masks): + hist = Counter((word & mask).bit_count() for word in words if word) + distance = min(k for k in hist if k) + dimension = rank(b[i] for i in indices(mask)) + require(dimension >= 8 and distance > 3, "small-erasure premise") + strata.append({"normal": list(n), "support_size": mask.bit_count(), + "span_dimension": dimension, "erasure_distance": distance, + "character_weight_histogram": dict(sorted(hist.items()))}) + require([r["span_dimension"] for r in strata] == [8, 8, 9, 9, 9], "stratum dimensions") + require([r["erasure_distance"] for r in strata] == [24, 24, 12, 12, 24], "stratum distances") + slices = [[mask & b[j] for j in range(112)] for mask in masks] + free_pairs = [(i, j) for i in range(112) for j in range(112) if not (b[i] >> j & 1)] + require(len(free_pairs) == 5824, "all free port pairs") + records, one_trace, two_trace = [], bytearray(), bytearray() + for a, left in enumerate(masks): + for c, right in enumerate(masks): + original = rank(b[i] & right for i in indices(left)) + require(original >= 8, "unperturbed term floor") + one = [rank(b[i] & right for i in indices(slices[a][j])) for j in range(112)] + require(min(one) >= 7, "one-sided survivor floor") + # Projection of any row basis spans the restricted matrix. + row_bases = [basis(b[i] for i in indices(slices[a][j])) for j in range(112)] + two = [rank(row & slices[c][i] for row in row_bases[j]) for i, j in free_pairs] + expected = 4 + sum(t != 0 for t in NORMALS[a]) + sum(t != 0 for t in NORMALS[c]) + require(min(two) == expected, "PR1373 two-sided survivor premise") + one_trace.extend(one) + two_trace.extend(two) + records.append({"left": a, "right": c, "original_rank": original, + "one_sided_histogram": dict(sorted(Counter(one).items())), + "one_sided_minimum": min(one), "one_sided_witness": one.index(min(one)), + "two_sided_histogram": dict(sorted(Counter(two).items())), + "two_sided_minimum": min(two), + "two_sided_witness": list(free_pairs[two.index(min(two))])}) + require(len(one_trace) == 2800 and len(two_trace) == 145600, "full survivor coverage") + return {"coordinate_pair": list(PAIR), "ports": 112, "pairing_rank": rank(b), + "baseline_coordinate_ranks": coordinate_ranks, + "pairing_sha256": digest(canonical(b)), "strata": strata, + "character_evaluations": 2555, "free_port_pairs": len(free_pairs), + "one_sided_records": len(one_trace), "one_sided_sha256": digest(one_trace), + "two_sided_records": len(two_trace), "two_sided_sha256": digest(two_trace), + "pairs": records} + + +@dataclass(frozen=True) +class QI: + real: Fraction + imag: Fraction = Fraction(0) + + def __add__(self, other): + other = qi(other) + return QI(self.real + other.real, self.imag + other.imag) + + __radd__ = __add__ + + def __neg__(self): + return QI(-self.real, -self.imag) + + def __sub__(self, other): + return self + -qi(other) + + def __mul__(self, other): + other = qi(other) + return QI(self.real * other.real - self.imag * other.imag, + self.real * other.imag + self.imag * other.real) + + __rmul__ = __mul__ + + def __truediv__(self, other): + other = qi(other) + den = other.real * other.real + other.imag * other.imag + require(bool(den), "division by zero") + return self * QI(other.real / den, -other.imag / den) + + def __bool__(self): + return bool(self.real or self.imag) + + +def qi(value): + return value if isinstance(value, QI) else QI(Fraction(value)) + + +def inverse(matrix): + n = len(matrix) + rows = [[qi(t) for t in row] + [qi(i == j) for j in range(n)] for i, row in enumerate(matrix)] + for j in range(n): + pivot = next((i for i in range(j, n) if rows[i][j]), None) + require(pivot is not None, "singular matrix") + rows[j], rows[pivot] = rows[pivot], rows[j] + z = rows[j][j] + rows[j] = [t / z for t in rows[j]] + for i in range(n): + if i != j: + z = rows[i][j] + rows[i] = [a - z * c for a, c in zip(rows[i], rows[j])] + return [row[n:] for row in rows] + + +def transpose(matrix): + return list(map(list, zip(*matrix))) + + +def multiply(a, c): + return [[sum((qi(u) * v for u, v in zip(row, col)), qi(0)) for col in zip(*c)] for row in a] + + +def factors(x, u, v, matrix): + invt = transpose(inverse(matrix)) + left = multiply([[row[4], row[6], z] for row, z in zip(x, u)], matrix) + right = multiply([[row[4], row[6], z] for row, z in zip(x, v)], invt) + active = sum(any(matrix[i][j] for i in (0, 1)) and any(invt[i][j] for i in (0, 1)) + for j in range(3)) + require(active in (2, 3), "projected rank-two identity") + return left, right, active + + +def free_rectangle(u, v, b): + um, vm = support(u), support(v) + require(um and vm, "rectangle factors must be nonzero") + require(all(not (b[i] & vm) for i in indices(um)), "rectangle is not free") + + +def check_identity(left, right, x, u, v): + for i in range(112): + for j in range(112): + expected = qi(x[i][4] * x[j][4] + x[i][6] * x[j][6]) + qi(u[i]) * v[j] + actual = sum((a * c for a, c in zip(left[i], right[j])), qi(0)) + require(actual == expected, "ordinary-transpose factor identity") + + +def costs(left, right, b): + return [rank(b[i] & support(c) for i in indices(support(a))) + for a, c in zip(transpose(left), transpose(right))] + + +def reject(fn, message): + try: + fn() + except (ValueError, ZeroDivisionError): + return message + raise ValueError("negative control unexpectedly accepted: " + message) + + +def fixtures(x, b): + z, e = [0] * 112, [int(i == 46) for i in range(112)] + partner = next(i for i in range(112) if not (b[i] >> 46 & 1)) + u = [int(i == partner) for i in range(112)] + large = [-row[4] if not (b[i] >> 46 & 1) else 0 for i, row in enumerate(x)] + identity = [[1, 0, 0], [0, 1, 0], [0, 0, 1]] + imag = QI(Fraction(0), Fraction(1)) + cases = [ + ("sharp-free-singleton", u, e, identity), + ("dense-triangular", u, e, [[1, 1, 0], [1, -1, 0], [2, 3, 1]]), + ("large-rectangle", large, e, [[1, 1, 0], [0, 1, 0], [1, 2, 1]]), + ("compensation-is-required", large, e, [[1, 0, 0], [0, 1, 0], [1, 0, 1]]), + ("transpose-branch", e, large, [[1, 0, 1], [0, 1, -1], [0, 0, 1]]), + ("three-products", u, e, [[1, 0, 1], [0, 1, 1], [1, 1, 3]]), + ("nonreal-rescaling", u, e, [[imag, 0, 0], [0, 1, 0], [0, 0, 1]]), + ] + results, saved = [], {} + for name, a, c, matrix in cases: + free_rectangle(a, c, b) + left, right, active = factors(x, a, c, matrix) + check_identity(left, right, x, a, c) + ranks = costs(left, right, b) + require(sum(ranks) >= 16, "fixture COPY floor") + if active == 3: + require(min(ranks) >= 6, "three-product fixture floor") + results.append({"name": name, "rectangle_size": [support(a).bit_count(), support(c).bit_count()], + "projected_products": active, "copy_ranks": ranks, "matrix_entries": 12544}) + saved[name] = (left, right, a, c) + require(results[0]["copy_ranks"] == [8, 8, 0], "sharp attainment") + omission = next(r for r in results if r["name"] == "compensation-is-required") + require(omission["copy_ranks"] == [7, 8, 7], "compensation omission witness") + controls = [] + controls.append(reject(lambda: free_rectangle(e, e, b), "nonfree-diagonal")) + controls.append(reject(lambda: free_rectangle(z, e, b), "zero-rectangle-factor")) + controls.append(reject(lambda: inverse([[1, 0, 1], [0, 1, 0], [1, 0, 1]]), "singular-factor-change")) + left, right, a, c = saved["compensation-is-required"] + omitted = [[row[0], row[1], qi(0)] for row in left] + controls.append(reject(lambda: check_identity(omitted, right, x, a, c), "omitted-compensation-identity")) + controls.append(reject(lambda: require(48 + sum(omission["copy_ranks"]) == 63, "complete bill is 70"), + "omitted-compensation-invoice-63-versus-70")) + left, right, a, c = saved["nonreal-rescaling"] + conjugated = [[QI(t.real, -t.imag) for t in row] for row in right] + controls.append(reject(lambda: check_identity(left, conjugated, x, a, c), "conjugate-instead-of-ordinary-transpose")) + boundary_m = [[1, 0, 1], [0, 1, 1], [1, 0, 2]] + boundary_v = [row[4] for row in x] + left, right, active = factors(x, z, boundary_v, boundary_m) + check_identity(left, right, x, z, boundary_v) + boundary_costs = costs(left, right, b) + require(active == 3 and boundary_costs == [8, 8, 0], "zero-factor boundary") + controls.append(reject(lambda: require(min(boundary_costs) >= 6, "zero-factor boundary has rank zero"), + "three-products-without-nonzero-rectangle")) + require([Fraction(3, 4) * a + Fraction(1, 8) * c + Fraction(1, 8) * d + for a, c, d in zip((8, 8, 0), (8, 0, 8), (0, 8, 8))] == [7, 7, 2], + "concavity witness") + require(2 * 7 ** 2 + 2 ** 2 < 2 * 8 ** 2, "out-of-range power boundary") + controls.append(reject(lambda: require(2 * 7 ** 2 + 2 ** 2 >= 2 * 8 ** 2, "q=2 outside theorem"), + "power-exponent-outside-zero-one")) + return {"cases": results, "entry_checks": 8 * 12544, + "zero_factor_boundary": {"projected_products": active, "copy_ranks": boundary_costs}, + "omission_invoice": {"six_unchanged": 48, "falsely_omitting_compensation": 63, "complete": 70}, + "concavity_combination": {"weights": ["3/4", "1/8", "1/8"], "result": [7, 7, 2]}, + "negative_controls": controls} + + +def build(): + source = load_source() + roots, x, b = geometry(source) + result = {"schema_version": 1, "status": "scoped-copy-obstruction-no-new-kappa", + "base_commit": json.loads((HERE / "SOURCES.json").read_text())["base_commit"], + "geometry_source_sha256": digest((ROOT / SOURCE).read_bytes()), + "root_order": "lexicographic, first nonzero coordinate positive, twice-E8 roots", + "root_order_sha256": digest(canonical(roots)), + "finite": finite_premises(x, b), "fixtures": fixtures(x, b)} + return json.loads(json.dumps(result)) + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--write", type=Path, help="create a new certificate; refuse overwrites") + parser.add_argument("--check", type=Path, default=HERE / "CERTIFICATE.json") + args = parser.parse_args() + result = build() + if args.write: + with args.write.open("x") as output: + json.dump(result, output, indent=2) + output.write("\n") + else: + require(result == json.loads(args.check.read_text()), "complete certificate mismatch") + print("PASS_P112_TWO_PRODUCT_COMPENSATION strata=5 characters=2555 one_sided=2800 " + "three_product_records=145600 fixtures=8 controls=8 copy_floor=64 no_new_kappa") + + +if __name__ == "__main__": + main()