From 9df32e528da547a1c1cb51cbd480f88f8b7d197e Mon Sep 17 00:00:00 2001 From: Sricharan Vagvala Date: Wed, 14 Oct 2026 22:55:11 -0700 Subject: [PATCH 1/2] Prove the three-call P112 isometric-chart copy floor --- .../p112-three-call-isometric-floor/CLAIM.md | 10 + .../EXPECTED.json | 472 ++++++++++++++++++ .../p112-three-call-isometric-floor/PROOF.md | 187 +++++++ .../p112-three-call-isometric-floor/README.md | 186 +++++++ .../SOURCES.json | 48 ++ .../p112-three-call-isometric-floor/TASK.json | 167 +++++++ .../VERIFY.json | 35 ++ .../test_package.py | 98 ++++ .../p112-three-call-isometric-floor/verify.py | 412 +++++++++++++++ 9 files changed, 1615 insertions(+) create mode 100644 research/p112-three-call-isometric-floor/CLAIM.md create mode 100644 research/p112-three-call-isometric-floor/EXPECTED.json create mode 100644 research/p112-three-call-isometric-floor/PROOF.md create mode 100644 research/p112-three-call-isometric-floor/README.md create mode 100644 research/p112-three-call-isometric-floor/SOURCES.json create mode 100644 research/p112-three-call-isometric-floor/TASK.json create mode 100644 research/p112-three-call-isometric-floor/VERIFY.json create mode 100644 research/p112-three-call-isometric-floor/test_package.py create mode 100644 research/p112-three-call-isometric-floor/verify.py diff --git a/research/p112-three-call-isometric-floor/CLAIM.md b/research/p112-three-call-isometric-floor/CLAIM.md new file mode 100644 index 0000000000..268fc087f4 --- /dev/null +++ b/research/p112-three-call-isometric-floor/CLAIM.md @@ -0,0 +1,10 @@ +CLAIM — structural decoder research: three-call P112 batches with independent isometric charts + +- Track / OS-random assignment seed: 40–49 structural decoder research / **47** (`secrets.randbelow(100)`, 2026-10-15 05:35 UTC). +- Exact base: `0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2`; priority revision 4; selected conditional κ remains 0.001672660197076918. +- Object: three independent P112 all-pairs demands (`C=I_3`) in PR1714's root-code, separate-total union-price model, with a separate arbitrary b-isometric binary label chart on each call. Does the 192 copy floor, and its rank-power counterpart, survive? +- Changed premise / predecessor: PR2294 head `18d6ac4f864af2b71aa8cf5f4541fcfc4350e2f0` proves the two-call case and lists `k>=3` as open. This investigates exactly `k=3`, allowing any finite number of terms and arbitrary complex coefficients. No new supplier or κ claim. +- Method: a six-order block-triangular deletion argument for pure cross-call outer products, with exact enumeration of the 12 disjoint support patterns; independently reconstructed P112 finite premises and full all-pairs decoder fixtures. Free chart conversions are a favorable relaxation; all omitted physical costs are nonnegative. Include a four-call 2-by-2 support control that prevents overgeneralizing the argument. +- Expected deliverable: `research/p112-three-call-isometric-floor/`, a scoped proof or exact falsifier, standard-library verifier, source pins and meaningful negative controls, as one focused research-note PR. +- Overlap: complete entry refresh covers 546 open PR bodies and 1,049 Discussions, without warnings (2026-10-15 05:41 UTC). Nearby three-call finite-group and shared-product work changes other models; no matching three-call P112 isometric-chart result was identified in the searched coverage. No pinned sprint issue exists; this reply is the canonical public claim. +- Expected finish / expiry: **2026-10-15 06:35 UTC**; final 15 minutes reserved for verification and handoff. Author: Sricharan Vagvala (@theon199), with substantial OpenAI Codex assistance; author-checked, no independent human review. diff --git a/research/p112-three-call-isometric-floor/EXPECTED.json b/research/p112-three-call-isometric-floor/EXPECTED.json new file mode 100644 index 0000000000..0b6305e19f --- /dev/null +++ b/research/p112-three-call-isometric-floor/EXPECTED.json @@ -0,0 +1,472 @@ +{ + "chart_seed": 47, + "cross_pair_ranks": [ + [ + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7 + ], + [ + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7 + ], + [ + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7 + ], + [ + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7 + ], + [ + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7 + ], + [ + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7 + ], + [ + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7 + ], + [ + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7 + ] + ], + "fixtures": [ + { + "all_pairs_checked": 112896, + "cost": 192, + "lower_ranks_by_order": [ + 0, + 0, + 0, + 0, + 0, + 0 + ], + "name": "standard", + "non_pure": 24, + "price_histogram": { + "8": 24 + }, + "pure": 0, + "terms": 24, + "terms_sha256": "61130e987de2644a0bf22da9c6d14efba99be923da86010c0cfb359569068bad" + }, + { + "all_pairs_checked": 112896, + "cost": 199, + "lower_ranks_by_order": [ + 0, + 0, + 1, + 1, + 0, + 1 + ], + "name": "one_rank7_cross", + "non_pure": 24, + "price_histogram": { + "7": 1, + "8": 24 + }, + "pure": 1, + "terms": 25, + "terms_sha256": "39d14348e0d2fea4aaece4778aedce50e80480d4afcf5539524eb46c2a3daf65" + }, + { + "all_pairs_checked": 112896, + "cost": 200, + "lower_ranks_by_order": [ + 0, + 0, + 1, + 1, + 1, + 1 + ], + "name": "one_three_call_pure", + "non_pure": 24, + "price_histogram": { + "8": 25 + }, + "pure": 1, + "terms": 25, + "terms_sha256": "9d7bd76aea56cb7c50399a1d37c75ac27ca81cbe460c2f065396da70ab1efebd" + }, + { + "all_pairs_checked": 112896, + "cost": 201, + "lower_ranks_by_order": [ + 2, + 2, + 2, + 2, + 2, + 2 + ], + "name": "sharp_deletion_coupled", + "non_pure": 22, + "price_histogram": { + "8": 24, + "9": 1 + }, + "pure": 3, + "terms": 25, + "terms_sha256": "e4f981b0d4494698152bfa30153eb451af550cfef40763397ee1a4c4b8285edb" + } + ], + "geometry": { + "ambient_labels": 9, + "complement_ranks": { + "7": 8, + "8": 503 + }, + "deficient": [ + [ + 1, + 0 + ], + [ + 2, + 1 + ], + [ + 4, + 2 + ], + [ + 7, + 3 + ], + [ + 8, + 4 + ], + [ + 11, + 5 + ], + [ + 13, + 6 + ], + [ + 14, + 7 + ] + ], + "geometry_sha256": "231e3234c27df63ba2676e0c9925efeefe28b6310f343dcf9a14f822d0142f20", + "live_roots": 112, + "modular_prime": 65537, + "support_pair_ranks": [ + [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8 + ], + [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8 + ], + [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8 + ], + [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8 + ], + [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8 + ], + [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8 + ], + [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8 + ], + [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8 + ] + ] + }, + "negative_controls": [ + "invertible nonisometric chart rejected", + "false per-term rank-eight floor rejected", + "wrong cross cancellation sign rejected", + "missing coordinate term rejected", + "diagonal-only crosstalk rejected by all-pairs check", + "invalid four-call extension rejected", + "rank-one truncation assumption at four calls rejected" + ], + "ordering": { + "four_call_control": { + "orders": 24, + "rank_histogram": { + "0": 4, + "1": 16, + "2": 4 + }, + "rank_sum": 24 + }, + "three_call_order_checks": 72, + "three_call_patterns": [ + { + "reader_mask": 1, + "six_ranks": [ + 0, + 0, + 1, + 1, + 0, + 1 + ], + "source_mask": 2 + }, + { + "reader_mask": 1, + "six_ranks": [ + 0, + 0, + 0, + 1, + 1, + 1 + ], + "source_mask": 4 + }, + { + "reader_mask": 1, + "six_ranks": [ + 0, + 0, + 1, + 1, + 1, + 1 + ], + "source_mask": 6 + }, + { + "reader_mask": 2, + "six_ranks": [ + 1, + 1, + 0, + 0, + 1, + 0 + ], + "source_mask": 1 + }, + { + "reader_mask": 2, + "six_ranks": [ + 0, + 1, + 0, + 0, + 1, + 1 + ], + "source_mask": 4 + }, + { + "reader_mask": 2, + "six_ranks": [ + 1, + 1, + 0, + 0, + 1, + 1 + ], + "source_mask": 5 + }, + { + "reader_mask": 3, + "six_ranks": [ + 0, + 1, + 0, + 1, + 1, + 1 + ], + "source_mask": 4 + }, + { + "reader_mask": 4, + "six_ranks": [ + 1, + 1, + 1, + 0, + 0, + 0 + ], + "source_mask": 1 + }, + { + "reader_mask": 4, + "six_ranks": [ + 1, + 0, + 1, + 1, + 0, + 0 + ], + "source_mask": 2 + }, + { + "reader_mask": 4, + "six_ranks": [ + 1, + 1, + 1, + 1, + 0, + 0 + ], + "source_mask": 3 + }, + { + "reader_mask": 5, + "six_ranks": [ + 1, + 0, + 1, + 1, + 0, + 1 + ], + "source_mask": 2 + }, + { + "reader_mask": 6, + "six_ranks": [ + 1, + 1, + 1, + 0, + 1, + 0 + ], + "source_mask": 1 + } + ] + }, + "proof_status": "written quantified proof; finite evidence only, no formal theorem", + "schema_version": 1, + "sources": { + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "bound_files": 5 + }, + "transvection_vectors": [ + 367, + 47 + ] +} diff --git a/research/p112-three-call-isometric-floor/PROOF.md b/research/p112-three-call-isometric-floor/PROOF.md new file mode 100644 index 0000000000..188887e4aa --- /dev/null +++ b/research/p112-three-call-isometric-floor/PROOF.md @@ -0,0 +1,187 @@ +# Three independently recharted P112 calls still pay 192 + +This is a scoped written proof, with exact finite premises. It is not a +formal proof of integer multiplication or a lower bound for arbitrary circuits. +It extends the **two-call** isometric-chart result of Sagar Thakrar's pending +[PR2294](https://github.com/CrocSwap/integer-mult-bounds/pull/2294), head +`18d6ac4f864af2b71aa8cf5f4541fcfc4350e2f0`, to **three** independent calls. +The block-triangular averaging argument below is the new step. + +## 1. Exact model and inherited finite premises + +Use the model of alephnan's merged PR1714 +(`research/p112-batch-centre-floor/PROOF.md`, at the base in SOURCES.json). +Let X be the norm-four 112-by-8 P112 root matrix in frame-adapted Hamming +coordinates. Its eight coordinate directions have been punctured, and +`X^T X = 56 I_8`. + +The binary Gram matrix on the full 120 lines is + + B_ij = 1 + (x_i dot x_j)/2 (mod 2). + +It has rank nine. Write ell_i for its labels in a nine-dimensional space V +with nondegenerate symmetric bilinear form b, so `b(ell_i,ell_j)=B_ij`. +The chart of this form need not be the standard binary dot product. + +We inherit the following finite support classification from Mihir Srivastava +(PR845), Adam Gall (PR1098), and the PR1714 support/pair lemmas: + +* For nonzero `a in C^8`, the label span of `supp(Xa)` is V or one of eight + hyperplanes H_i, and hence has dimension at least eight. +* For any two nonzero `a,c in C^8`, b on their support spans has rank at + least eight. + +The verifier reconstructs the Hamming geometry and checks the finite premises: +among all 511 nonzero binary functionals, 503 complement root matrices have +rank eight and eight have rank seven, each with a distinct coordinate kernel; +all 64 ordered exceptional-support pairs have binary rank eight. A nonzero +minor over Q stays nonzero over C, while the exact coordinate kernel gives +the upper bound. Thus these premises include complex isotropic coefficients. +The deduction from this finite census to the quantified support lemma is +written out in PR1714 section 2; it is an inherited lemma, not a new claim here. + +There are three independent calls, indexed by 0,1,2. Call s uses an arbitrary +linear b-isometry phi_s of V, the same chart on its reader and source sides. +These charts can be chosen independently, and are granted **free**. + +Allow any finite number m of active root-code terms, with arbitrary complex +coefficient columns `a_j,c_j in C^24`, each split into three 8-blocks. Exactness +means + + sum_j a_j c_j^T = I_24. (1) + +Equivalently the live all-pairs endpoint is +`I_3 tensor (X X^T)`, because `I_3 tensor X` has a left inverse. Transpose is +ordinary, not conjugate transpose. Terms with a zero factor are discarded. +Coefficients of overcomplete factors must remain in the block-root code. + +Term j pays the F2 rank r_j of b between the two **unions** + + union_s phi_s ell(supp(X a_j^s)), + union_t phi_t ell(supp(X c_j^t)). + +The union forgets call identity and is charged only once. No preparation, +source access, conversion, routing, frame change, restoration or extra helper +cost is added to this favorable algebraic relaxation. A physical interpretation +requires the separate-total copy/delivery interface; this is not a universal +information lower bound for interacting circuits. + +## 2. Term prices + +Write S_j for the calls with `a_j^s != 0`, and T_j for those with +`c_j^t != 0`. They are nonempty. A term is **pure** if `S_j intersect T_j` +is empty; all other terms are **non-pure**. Let p and n count them. + +Every non-pure term contains a within-call support-pair block. The chart on +both sides of that block is the same isometry, so the pair lemma gives +`r_j >= 8`. + +Every pure term contains a block pairing two subspaces U,W of V of dimensions +at least eight. Nondegeneracy gives + + rank b|(U x W) = dim U - dim(U intersect W^perp) + >= dim U + dim W - 9 >= 7. (2) + +This uses dimensions, not the common-chart pair lemma. Rank-seven cross +terms really exist (PR2294); reasserting a per-term floor of eight would be +incorrect. Enlarging to the union cannot reduce a submatrix rank. + +## 3. A three-block triangular deletion lemma + +**Lemma.** Suppose the 24-by-24 identity is a sum of n non-pure and p pure +rank-one terms, classified by the three block supports above. Then + + n >= 24 - (2/3)p. (3) + +More precisely, if p_11 pure terms touch one reader and one source call, +and p_12 touch three calls, then +`n >= 24 - p_11/2 - 2 p_12/3`. + +*Proof.* Put `Q = sum_non-pure a_j c_j^T`. Every pure term P_j has zero +diagonal blocks, so (1) gives `Q = I_24 - sum_pure P_j`. + +For any of the six orders pi of the three calls, let L_pi keep only the +strictly lower **blocks** in that order. The matrix + + U_pi = Q - L_pi(Q) = Q + sum_pure L_pi(P_j) + +is block upper triangular with identity diagonal blocks. It is invertible, +with rank 24. Subadditivity of rank and `rank Q <= n` imply + + 24 <= n + sum_pure rank L_pi(P_j). (4) + +For a pure term, the disjoint nonempty sets S,T have either sizes (1,1), +(1,2) or (2,1). In each case one side occupies a single block. Consequently +L_pi(P_j) is zero or is still a single outer product: truncation only removes +whole blocks of the *other* factor. Its rank is one exactly when at least +one source call precedes a reader call. + +For sizes (1,1) this happens in three of the six orders. For (1,2), the +single reader is earliest among the three calls in two orders, and the +truncation is nonzero in the other four. For (2,1), the single source is +latest in two orders, again giving four nonzero truncations. These counts +do not depend on coefficients, block widths or the chosen charts. + +Average (4) over all six orders. This gives +`24 <= n + p_11/2 + 2 p_12/3 <= n + 2p/3`, proving (3). Equivalently, +some single order has at most `floor(2p/3)` nonzero pure truncations. QED. + +The coefficient 2/3 is sharp even for exact coefficient identities. On one +coordinate of each call, + + I_3 = 1 1^T - sum_(s=0..2) e_s (1-e_s)^T. + +Here 1 is the three-component all-ones vector: there is one non-pure term +and three pure terms, so `n + 2p/3 = 3`. Add the 21 untouched coordinate +terms to obtain an exact 24-dimensional root-code identity with n=22, p=3. +In every call order exactly two pure truncations are nonzero. The verifier's +`sharp_deletion_coupled` fixture checks this attained counting bound. Its +actual copy bill is 201 in the selected charts; it does not attain (5). + +## 4. Sharp copy and recursive-power floors + +**Theorem.** Under section 1's model, for every choice of the three isometric +charts and every exact root-code factorization, + + sum_j r_j >= 192 + (5/3)p >= 192. (5) + +The minimum is 192, and equality excludes pure terms. + +*Proof.* Sections 2 and 3 give +`sum r_j >= 8n + 7p >= 8(24 - 2p/3) + 7p = 192 + 5p/3`. +For attainment, use the 24 standard coordinate terms +`a=c=e_s tensor e_k`, for s=0,1,2 and k=0,...,7. Each has rank eight +by the within-call pair lemma and isometry, and their outer products sum to +I_24. If p>0, (5) is strict. QED. + +**Power-price corollary.** For every real `0 < q <= 1`, + + sum_j r_j^q >= 24 * 8^q + + p * (7^q - (2/3)8^q) >= 24 * 8^q. (6) + +The coefficient of p is positive because +`(7/8)^q >= 7/8 > 2/3`. Attainment is the same 24 coordinate terms. +Dividing by any fixed parent width M to the power q gives the same sharp +comparison for the separate-total child bill `sum_j (r_j/M)^q`. +In particular q=1-a is covered for the supplier regime `0 <= a < 1`. + +Thus three-call chart sharing in this relaxation cannot reduce either the +64-per-call centre rank or its separate-total recursive power bill. Adding +nonnegative helper, source-access, frame, routing or restoration charges +cannot improve this comparison. Changing the separate-total contract, the +parent width/volume or other local children needs a new accounting argument. +No changed kappa, supplier or physical construction follows from this note. + +## 5. Boundary of the proof + +For four calls a pure term can have two reader and two source calls. Lower +block truncation can then have rank two, although the untruncated term has +rank one. Averaging over all 24 orders gives mean rank one for the all-ones +2-by-2 support pattern, exceeding 2/3. The verifier records this as a scope +control. It neither supplies a four-call escape nor rules one out. + +Non-isometric own-call charts, different reader/source charts, nonidentity +call coupling, outside-code factors, temporal reuse and interacting copied +totals are also outside this theorem. Finite replay checks the geometry, +ordering counts and explicit examples; the quantified conclusion follows +from the written argument, not a finite search or a proof assistant. diff --git a/research/p112-three-call-isometric-floor/README.md b/research/p112-three-call-isometric-floor/README.md new file mode 100644 index 0000000000..230160d571 --- /dev/null +++ b/research/p112-three-call-isometric-floor/README.md @@ -0,0 +1,186 @@ +# Three independently recharted P112 calls still pay 192 + +**Scoped negative result / research note. No new supplier or kappa.** + +Three independent P112 all-pairs demands cannot share away their separate-total +copy bill by using different **isometric binary label charts**. For arbitrary +complex root-code factors, any finite number of terms, and free chart +conversions, the sharp total pairing-rank cost is **192 = 3 × 64**. +For every `0 < q <= 1`, the sharp separate-total power bill is `24 × 8^q`. +Thus this particular three-call sharing route also fails to reduce the +centre's recursive moment at fixed parent width and volume. + +This changes the two-call premise of Sagar Thakrar's pending [PR2294](https://github.com/CrocSwap/integer-mult-bounds/pull/2294), +which explicitly leaves `k >= 3` open. It does **not** repeat its chart sample +or claim the one-call support census as new. The new ingredient is the +six-order triangular deletion lemma in [PROOF.md](PROOF.md), section 3. + +## Statement and evidence + +Let p count active terms whose nonzero reader and source calls are disjoint +("pure" cross-call terms), and n count all other terms. Exactness of the +three independent endpoints forces + + n + (2/3)p >= 24. + +Within-call isometry gives each non-pure term price at least eight. A pure +term can cost seven, as the exact fixtures confirm. Therefore + + total rank >= 8n + 7p >= 192 + (5/3)p. + +For q in `(0,1]`, replace eight and seven by their q-th powers; the surplus +coefficient `7^q - (2/3)8^q` stays positive. Twenty-four independent coordinate +terms attain both floors. Equality excludes pure terms. + +The proof averages lower-block truncation over the six call orders. A pure +term occupies either one reader and one source call, or three calls with one +side occupying a single call. Its truncation remains rank zero or one, with +mean 1/2 or 2/3. +Triangularizing the non-pure sum leaves identity diagonal blocks and hence +rank 24. This argument applies to all complex coefficients and all three +isometric charts; it is **not** an inference from the finite examples. + +The new standard-library verifier imports no predecessor executable. Its +deterministic [EXPECTED.json](EXPECTED.json) records: + +- A reconstructed 120-line Hamming geometry, the 112 live lines and the + nondegenerate nine-dimensional binary form. +- All 511 binary hyperplane complements: 503 exact rank-eight cases and + eight rank-seven cases with the eight coordinate kernels. Modular lower + bounds and exact nullspaces certify rational/complex ranks; the eight + deficient cases are also checked by Fraction elimination. +- All 64 ordered within-call exceptional pairs (rank eight) and all 64 + pairs under a selected transvection (rank seven), with direct 56-by-56 + ranks checked against reduced-span pricing. +- All **12** disjoint three-call support patterns, each at all six orders + (**72** exact truncation-rank checks). +- Four exact decoder fixtures, each replayed on all **112,896** live + output/input pairs, including cross-call blocks. Their copy bills are + **192, 199, 200 and 201**. The cost-199 example contains a genuine + rank-seven pure term. The cost-200 example has the three-call support + pattern attaining the deletion argument's mean 2/3. The cost-201 example + has n=22, p=3 and attains `n + (2/3)p = 24` in every call order, proving + sharpness of the counting lemma on an exact root-code identity. +- Seven internal mathematical controls, plus the separate package tests + described below. + +## Reproduce + +Base commit: `0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2`. +Python 3.12 and Git with this base available suffice; no third-party dependencies. +From the repository root: + +```sh +python3.12 scripts/research_package.py --package research/p112-three-call-isometric-floor +``` + +Expected: the two registered checks end with +`PASS_P112_THREE_CALL_ISOMETRIC_FLOOR` and `PASS_THREE_CALL_PACKAGE_CONTROLS`, +then the runner prints `PASS_REGISTERED_RESEARCH_PACKAGE`. +Direct read-only replay is also available: + +```sh +python3.12 -I -O -B research/p112-three-call-isometric-floor/verify.py +``` + +The direct replay prints receipt SHA256 +`c1278f0b9154e144fe67e85652c0b98c4bfd98b9c481a2680037a2b8efe08f09` +and `PASS_P112_THREE_CALL_ISOMETRIC_FLOOR`. Only the explicit `--write` option +regenerates this package's own `EXPECTED.json`; normal replay writes nothing. +Checks remain active under `-O`. [VERIFY.json](VERIFY.json) declares all live +inputs; [SOURCES.json](SOURCES.json) binds their exact SHA256/Git blobs. + +Validation on macOS arm64 passed with CPython **3.12.13** (registered, optimized +and normal) and **3.14.5** (optimized). Direct outputs are byte-identical. The +registered check includes all five deliberate on-disk corruptions. No hosted +CI, proof-assistant run or independent human review is claimed. + +## Controls and scope limits + +Internal controls reject an invertible non-isometric chart, the false +common-chart per-term floor eight, an incorrect cancellation sign, an omitted +coordinate term, and cross-call crosstalk that passes diagonal-only endpoint +checks. Two controls prevent extending the three-call deletion lemma to four +calls: a pure 2-by-2 support pattern has truncation rank two in four orders +and mean rank **one** over 24 orders, exceeding 2/3. + +`test_package.py` checks relocation and read-only replay, plus on-disk +corruptions of the receipt, source digest, chart-dependent pricing and the +three-call ordering count. Every rejection must name the intended failure. + +The inherited model is PR1714's **separate-total union-price root-code** +objective. Both factors must stay in the respective block-root codes, and +each call uses the same isometry on its reader and source sides. The endpoint +is `C=I_3` on independent input blocks, with ordinary transpose. Charts are +granted free; no physical decoder is compiled or installed. Positive source +access, helper, frame-change, routing and restoration costs cannot reverse +this lower bound within that objective. A different cost/interface law needs +its own full invoice. + +This is a written proof after inherited, rechecked finite premises. It is +not Lean formalization, a universal circuit lower bound, or a complete +multiplication theorem. Compiler/all-size, physical common-label realization, +whole-call hosting, precision/tape, exact recovery, analytic transfer and +bit H1–H5 obligations remain untouched. The selected result and `upstream/` +are unchanged. No selected cold replay is required for this isolated note. + +## Sprint record and overlap + +OS-random assignment seed **47** chose structural decoder research. It also +selects the two distinct fixture transvections (vectors 367 and 47 in the +verifier's explicitly reconstructed chart); it is not offered as a novelty +claim. This is a proof and fixed finite replay, not a candidate search. +Coverage ends at the declared three-call model, all 511 functionals, all +12 support patterns, 64 ordered pairs in each named pairing, and four +explicit endpoint fixtures. No failed search is called an impossibility theorem. + +Three candidate tasks were considered: the P104 cut-2429 nested-frame contact price, +the noncommuting thirteen-call five-SWAP continuation of PR2317, and the +three-call chart question. The first had extensive live correction work; +the second lacked a promising completed budget in this session. The third +changes one explicit predecessor premise and admits a bounded proof check. + +Entry overlap covered 546 open PRs including drafts and 1,049 Discussions +with complete pagination, no warnings, and 1,536 local package/ledger records +(2026-10-15 05:41 UTC). No matching three-call P112 chart result was identified +in that coverage. Closed PRs are covered only through local notes and the +ledger; arbitrary diffs are not searched. The canonical claim is +[Discussion1166 comment 18941767](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-18941767). +The final refresh at 05:54 UTC covered **550 open PRs and 1,058 Discussions** +with complete pagination and no warnings. Main and PR2294's pinned head were +unchanged. Other three-mode matches concern coordinates within one call, +not three independent calls. No competing matching result was identified. +Full task, stopping rule, final freshness and verification evidence are in +[TASK.json](TASK.json). + +## Open next questions + +1. **Four independent calls with independent isometric charts.** The present + truncation argument loses its 2/3 coefficient on balanced 2-by-2 pure + supports. First classify the prices of those supports jointly with the + required cross-block cancellation, rather than assuming a sub-256 decoder + exists. This determines whether the next batch size offers a real escape. +2. **Beyond the root-code separate-total interface.** A saving construction + would need a different copied-total contract or outside-code factors. + First specify one exact all-pairs endpoint and fully price its preparation, + dirty restoration and recursive children. The blocker is an admitted + physical interface, not this note's ordering census. + +Structured relevance, first steps and blockers appear in TASK.json. + +## Credit and disclosure + +Sricharan Vagvala (@theon199), with **substantial OpenAI Codex assistance**: +the AI drafted the argument, implementation and documentation, followed by +author checks. No independent human review or proof-assistant check is claimed. +New material is Apache-2.0 under the repository license. + +Credit alephnan / PR1714 for the batch root-code model and original common-chart +floor; Sagar Thakrar (@thakrarsagar) / PR2294 for the two-call isometric result, +rank-seven cross-term mechanism and explicit `k>=3` question; Mihir Srivastava +/ PR845 and Adam Gall / PR1098 for the support classification; woklerx / +PR1077 and PR1180 and themilkman216 / PR968 for the decoder-floor lineage; +Douglas Colkitt / PR1240 for the centre-sharing motivation and package tools. +The retained selected construction remains Rohan Arun's PR1094 on Jeremy +Kothe's PR1087 and the cumulative k8/T16 lineage, with the DreamingOfClouds +PR589 / eumemic PR555 bit supplier. No predecessor code or data is vendored. diff --git a/research/p112-three-call-isometric-floor/SOURCES.json b/research/p112-three-call-isometric-floor/SOURCES.json new file mode 100644 index 0000000000..5bfd3149ce --- /dev/null +++ b/research/p112-three-call-isometric-floor/SOURCES.json @@ -0,0 +1,48 @@ +{ + "schema_version": 1, + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "e8870e5917057d59b730eb14721a778639eca050", + "sha256": "d46eb6d5b3e279428753d770653663fbdf1063e55c255ea073d768f344927ef7" + }, + { + "path": "research/complex-local-word-ceiling/README.md", + "usage": "input", + "git_blob": "f5f742f8196da29d2c3f4dffb3c27685ca9401f6", + "sha256": "b60be039cb0e03e064a27407d0bce9e58908d793da5ee405c876de5aebfa5f81" + }, + { + "path": "research/p112-batch-centre-floor/PROOF.md", + "usage": "input", + "git_blob": "1e43f0a92084d3c156712d40dd793540f8399030", + "sha256": "86533996351ec45afc1f0bab904a1ff0716c45c5c43c558ba61b267aea914d69" + }, + { + "path": "research/p112-batch-centre-floor/README.md", + "usage": "input", + "git_blob": "6a779efc838fe4a0628f3f99e7cdaaf00f8fe4e5", + "sha256": "3e9b69de6242e8429f92e5027570d65315fbbb82ae3afd0a043cc82aefdea307" + } + ], + "external_provenance": [ + { + "repository": "https://github.com/CrocSwap/integer-mult-bounds", + "pr": 2294, + "commit": "18d6ac4f864af2b71aa8cf5f4541fcfc4350e2f0", + "path": "research/p112-batch-chart-change/PROOF.md", + "sha256": "b0aef60119916aea6f768a92896be3b934a017a14e0ffdb17d66d6187ae3438b", + "git_blob": "177c27bd6c4f75a2524eb2e8ade74045b7abb060", + "url": "https://github.com/CrocSwap/integer-mult-bounds/blob/18d6ac4f864af2b71aa8cf5f4541fcfc4350e2f0/research/p112-batch-chart-change/PROOF.md", + "usage": "Read-only cited predecessor and open question, no executable/data dependency; its mathematical two-call result is not used as an oracle in the new proof." + } + ] +} diff --git a/research/p112-three-call-isometric-floor/TASK.json b/research/p112-three-call-isometric-floor/TASK.json new file mode 100644 index 0000000000..1524d86c7f --- /dev/null +++ b/research/p112-three-call-isometric-floor/TASK.json @@ -0,0 +1,167 @@ +{ + "schema_version": 1, + "task_id": "centre-path-sharing", + "priority_revision": 4, + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "original_card": { + "id": "centre-path-sharing", + "question": "Can the 64-per-call centre path (eight rank-8 COPY/ERASE totals through the private temporary) be shared across calls or shrunk?", + "starting_points": [ + "research/complex-local-word-ceiling/README.md", + "research/split-centres-global/proofs/PR386-BIT-GEOMETRY.txt", + "certificates/selected-result.json" + ], + "methods": [ + "Derive a fully charged favorable relaxation for sharing one centre path across k calls, including restoration, hosting and precision.", + "Prove a lower bound on copied information per call for the selected decoder contract." + ], + "acceptance_gate": "Show the changed centre charge and copy profile per call with every added restoration or hosting cost charged, and its ceiling via ceiling.ceiling(centre=...).", + "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": "Write the per-call centre charge and copy children for sharing across k = 2 calls, charge the sharing overhead, and screen it; stop this route if even the ideal sharing gains under 10%. Ideal budgets: free 2.80x, shared by two 1.90x (levers.py).", + "bottleneck_link": "The centre path consumes 64 of about 99.6 unpaid coordinates per call, i.e. about 64% of the raw deficit.", + "allowed_variations": [ + "One sharing pattern across a fixed number of calls.", + "One reduced copied-total contract for the existing decoder.", + "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": [ + "Removing copies without a replacement contract for the decoder's copied totals." + ], + "overlap_terms": [ + "centre path", + "copied totals", + "private temporary", + "shared centre", + "batching" + ] + }, + "scope_status": "refined", + "actual_scope": "Three independent P112 all-pairs demands (C=I_3), arbitrary finite root-code complex factors, one arbitrary b-isometric label chart per call, separate-total union pairing-rank and q-power price for 0=4.", + "outcome": "completed", + "evidence": "PROOF.md gives the quantified complex-coefficient proof: n+(2/3)p>=24, cost>=192+(5/3)p and the sharp q-power floor. EXPECTED.json records 511 functionals, 72 support/order checks, 64 within-chart and 64 cross-chart ranks, four full 336x336 endpoints, and seven internal controls. test_package.py adds relocation/no-write and five on-disk failure controls.", + "author": "Sricharan Vagvala (@theon199)", + "ai_assistance": "Substantial OpenAI Codex assistance drafted the proof, verifier, controls and documentation; author-checked. No delegated agents, independent human review or formal proof assistant used.", + "open_questions": [ + { + "question": "Does the 256 floor survive four independently isometrically recharted calls?", + "why_it_matters": "This is the next unresolved batch size for the same centre-sharing mechanism.", + "first_step": "Jointly classify price and cross-block cancellation for balanced 2-by-2 pure supports; the recorded 24-order control shows why the 2/3 deletion coefficient fails.", + "blocked_by": "The current termwise averaging bound is one, not 2/3, on those supports; no saving construction is known here." + }, + { + "question": "Can a legal interacting copied-total contract or outside-code factorization reduce the centre bill?", + "why_it_matters": "The theorem only blocks the root-code separate-total union-price relaxation; structural savings require a different expense or contract.", + "first_step": "Specify one exact all-pairs endpoint and a complete preparation, source-access, dirty-restoration and recursive-child invoice before optimizing it.", + "blocked_by": "No admitted physical replacement interface is supplied by this note." + } + ], + "assignment_seed": 47, + "assignment_rng": "OS randomness through Python secrets.randbelow(100), 2026-10-15T05:35:15Z", + "assigned_track": "40-49 structural decoder research (explicit donor allocation)", + "verification_reserved_minutes": 15, + "started_utc": "2026-10-15T05:35:15Z", + "expected_finish_utc": "2026-10-15T06:35:00Z", + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-18941767", + "candidate_tasks": [ + { + "object": "P104 cut-2429 strictly nested-frame contacts on the frozen PR1972 temporal network", + "decision": "Not selected: PR2172 already certifies C(F)=9*max(0,F-8), including cost 864 at F=104, under its stated contact model; repeating that price does not add a mechanism." + }, + { + "object": "Noncommuting rank-one projectors for the strictly alternating thirteen-call five-SWAP target, the case left open by PR2317", + "decision": "Not selected: no favorable completed budget available before a potentially large search." + }, + { + "object": "Three independently isometrically recharted P112 calls, PR2294 k>=3 question", + "decision": "Selected: new batch size and a coefficient-neutral six-order proof obligation." + } + ], + "experiment_domain": { + "kind": "written proof with fixed exhaustive finite premises and named examples, not a search for a stronger bound", + "charts_in_theorem": "all triples of b-isometries; not finitely enumerated", + "decoder_factors_in_theorem": "arbitrary finite exact complex root-code factors; not finitely enumerated", + "finite_coverage": { + "functionals": 511, + "disjoint_support_patterns": 12, + "call_orders_per_pattern": 6, + "within_call_pairs": 64, + "cross_call_pairs": 64, + "named_fixtures": 4, + "all_pairs_per_fixture": 112896 + }, + "fixture_selection": "random.Random(47).sample on the 16 explicitly computed target transvections, selecting vectors 367 and 47; no novelty claim from this seed" + }, + "entry_overlap": { + "open_prs": { + "fetched_at": "2026-10-15T05:39:25.208844+00:00", + "complete_pagination": true, + "records": 546 + }, + "discussions": { + "fetched_at": "2026-10-15T05:41:20.883124+00:00", + "complete_pagination": true, + "records": 1049 + } + }, + "overlap_limits": "Open PR bodies including drafts, Discussion bodies/comments/replies and local README/TASK/ledger records. Closed PRs only through local records; no arbitrary diffs. Absence of a match is not novelty proof.", + "validation": [ + { + "command": "python3.12 scripts/research_package.py --package research/p112-three-call-isometric-floor", + "environment": "macOS arm64, CPython 3.12.13, standard library + Git", + "result": "PASS_REGISTERED_RESEARCH_PACKAGE outcome=completed; two -I -O -B commands, seven mathematical controls, relocation/no-write and five on-disk corruption controls" + }, + { + "command": "python3.12 -I -B research/p112-three-call-isometric-floor/verify.py", + "result": "PASS; same exact receipt as optimized 3.12 and optimized 3.14" + }, + { + "command": "python3 -I -O -B research/p112-three-call-isometric-floor/verify.py", + "environment": "macOS-27.0.1-arm64-arm-64bit-Mach-O, CPython 3.14.5", + "result": "PASS; byte-identical output to normal Python 3.12.13" + }, + { + "command": "git diff --cached --check", + "result": "PASS; only nine new files in this package; upstream/, selected frontier, shared scripts and tests untouched" + } + ], + "verification_started_utc": "2026-10-15T05:51:17Z", + "receipt_sha256": "c1278f0b9154e144fe67e85652c0b98c4bfd98b9c481a2680037a2b8efe08f09", + "upstream_refresh": { + "canonical_main": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "pending_pr2294_head": "18d6ac4f864af2b71aa8cf5f4541fcfc4350e2f0", + "status": "canonical main and pending PR2294 head unchanged; final complete overlap refresh passed without warnings", + "checked_utc": "2026-10-15T05:52:15Z" + }, + "final_overlap": { + "searched_at": "2026-10-15T05:54:12.039387+00:00", + "coverage": { + "open_prs": { + "fetched_at": "2026-10-15T05:52:15.199164+00:00", + "complete_pagination": true, + "records": 550 + }, + "discussions": { + "fetched_at": "2026-10-15T05:54:11.934274+00:00", + "complete_pagination": true, + "records": 1058 + } + }, + "local_records": 1538, + "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.", + "assessment": "Only predecessor PR2294, its released claim, our own claim/package, and unrelated one-call three-coordinate-mode results match. No competing three-call P112 isometric-chart proof was identified in the searched coverage." + } +} diff --git a/research/p112-three-call-isometric-floor/VERIFY.json b/research/p112-three-call-isometric-floor/VERIFY.json new file mode 100644 index 0000000000..2dc2f8a19f --- /dev/null +++ b/research/p112-three-call-isometric-floor/VERIFY.json @@ -0,0 +1,35 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/complex-local-word-ceiling/README.md", + "research/p112-batch-centre-floor/PROOF.md", + "research/p112-batch-centre-floor/README.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact source pins, all 511 finite support premises, 64 within/cross pair ranks, 72 support/order ranks, four full all-pairs endpoints, seven mathematical controls and canonical receipt equality." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/test_package.py" + ], + "timeout_seconds": 120, + "checks": "Relocated read-only replay and five reason-specific on-disk corruptions: receipt, source digest, chart pricing, deletion count, duplicate JSON key." + } + ] +} diff --git a/research/p112-three-call-isometric-floor/test_package.py b/research/p112-three-call-isometric-floor/test_package.py new file mode 100644 index 0000000000..dbb20bf014 --- /dev/null +++ b/research/p112-three-call-isometric-floor/test_package.py @@ -0,0 +1,98 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Relocation, no-write replay and reason-specific mutation checks in scratch. + +Sricharan Vagvala (@theon199), with substantial OpenAI Codex assistance. +""" +import hashlib +import json +from pathlib import Path +import shutil +import subprocess +import sys +import tempfile + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def snapshot(root): + return {p.relative_to(root).as_posix(): hashlib.sha256(p.read_bytes()).hexdigest() + for p in root.rglob("*") if p.is_file()} + + +def main(): + manifest = json.loads((HERE / "SOURCES.json").read_text()) + with tempfile.TemporaryDirectory(prefix="p112-three-call-controls-") as directory: + scratch = Path(directory) + package = scratch / "research" / "renamed-package" + shutil.copytree(HERE, package) + # Git is used only to read historical provenance from the existing object store. + git_directory = subprocess.run(["git", "-C", str(ROOT), "rev-parse", "--absolute-git-dir"], + check=True, capture_output=True, text=True).stdout.strip() + (scratch / ".git").write_text("gitdir: " + git_directory + "\n") + for entry in manifest["files"]: + if entry["usage"] == "input": + destination = scratch / entry["path"] + destination.parent.mkdir(parents=True, exist_ok=True) + shutil.copyfile(ROOT / entry["path"], destination) + + def execute(): + return subprocess.run([sys.executable, "-I", "-O", "-B", str(package / "verify.py")], + cwd=scratch, capture_output=True, text=True, timeout=60) + + before = snapshot(scratch) + positive = execute() + require(positive.returncode == 0, "relocated positive failed: " + positive.stderr) + require("PASS_P112_THREE_CALL_ISOMETRIC_FLOOR" in positive.stdout, "missing positive marker") + require(snapshot(scratch) == before, "default replay wrote files") + + def mutation(name, filename, change, expected): + path = package / filename + original = path.read_text() + modified = change(original) + require(modified != original, "mutation did not change input: " + name) + try: + path.write_text(modified) + result = execute() + require(result.returncode != 0 and expected in result.stderr, + "wrong mutation result: " + name + "\n" + result.stderr) + finally: + path.write_text(original) + + def receipt_change(text): + data = json.loads(text) + data["fixtures"][0]["cost"] -= 1 + return json.dumps(data) + + def source_change(text): + data = json.loads(text) + next(x for x in data["files"] if x["usage"] == "input")["sha256"] = "0" * 64 + return json.dumps(data) + + def replace_once(text, old, new): + require(text.count(old) == 1, "mutation target is not unique") + return text.replace(old, new) + + mutation("false receipt", "EXPECTED.json", receipt_change, "receipt mismatch") + mutation("source digest", "SOURCES.json", source_change, "source sha256:") + mutation("ignored chart", "verify.py", + lambda s: replace_once(s, "charts[s][label]", "label"), + "attainment / rank-seven fixture") + mutation("false half-frequency", "verify.py", + lambda s: replace_once(s, "expected_sum = 3 if sum(a) == sum(c) == 1 else 4", + "expected_sum = 3"), + "three-call deletion counts") + mutation("duplicate receipt key", "EXPECTED.json", + lambda s: '{"schema_version": 1, ' + s[1:], "duplicate JSON key: schema_version") + require(snapshot(scratch) == before, "controls did not restore scratch inputs") + print("PASS_THREE_CALL_PACKAGE_CONTROLS relocated=1 read_only=1 mutations_rejected=5") + + +if __name__ == "__main__": + main() diff --git a/research/p112-three-call-isometric-floor/verify.py b/research/p112-three-call-isometric-floor/verify.py new file mode 100644 index 0000000000..3c4ed73cc4 --- /dev/null +++ b/research/p112-three-call-isometric-floor/verify.py @@ -0,0 +1,412 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Exact evidence for PROOF.md; stdlib, read-only default, checks active under -O. + +Sricharan Vagvala (@theon199), with substantial OpenAI Codex assistance. +No predecessor executable is imported. --write updates only EXPECTED.json. +""" +import argparse +from collections import Counter +from fractions import Fraction +import hashlib +from itertools import permutations, product +import json +from pathlib import Path +import random +import subprocess + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +BASE = "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2" + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def canonical(value): + return json.dumps(value, indent=2, sort_keys=True, ensure_ascii=True) + "\n" + + +def sha(value): + return hashlib.sha256(canonical(value).encode()).hexdigest() + + +def object_pairs(pairs): + result = {} + for key, value in pairs: + require(key not in result, "duplicate JSON key: " + key) + result[key] = value + return result + + +def read_json(path): + def invalid_constant(value): + raise ValueError("nonfinite JSON constant: " + value) + return json.loads(path.read_text(encoding="utf-8"), object_pairs_hook=object_pairs, + parse_constant=invalid_constant) + + +def source_pins(): + data = read_json(HERE / "SOURCES.json") + require(data["base_commit"] == BASE, "source base") + required = {"certificates/selected-result.json", "docs/research/agent-task-catalog.json", + "research/p112-batch-centre-floor/PROOF.md", + "research/p112-batch-centre-floor/README.md", + "research/complex-local-word-ceiling/README.md"} + require(len(data["files"]) == len(required) + and {x["path"] for x in data["files"]} == required, "source inventory") + for entry in data["files"]: + name = entry["path"] + if entry["usage"] == "provenance": + payload = subprocess.run(["git", "-C", str(ROOT), "show", BASE + ":" + name], + check=True, capture_output=True).stdout + else: + require(entry["usage"] == "input", "source usage") + payload = (ROOT / name).read_bytes() + require(hashlib.sha256(payload).hexdigest() == entry["sha256"], "source sha256: " + name) + blob = hashlib.sha1(b"blob " + str(len(payload)).encode() + b"\0" + payload).hexdigest() + require(blob == entry["git_blob"], "source Git blob: " + name) + return {"base_commit": BASE, "bound_files": len(required)} + + +def dot(a, b): + return sum(x * y for x, y in zip(a, b)) + + +def binary_basis(rows): + pivots, indices = {}, [] + for index, value in enumerate(rows): + while value: + bit = value.bit_length() - 1 + if bit in pivots: + value ^= pivots[bit] + else: + pivots[bit] = value + indices.append(index) + break + return indices + + +def binary_rank(rows): + return len(binary_basis(rows)) + + +def rational_rank(rows): + pivots = {} + for row in rows: + v = list(map(Fraction, row)) + for column, basis in sorted(pivots.items()): + coefficient = v[column] + if coefficient: + v = [x - coefficient * y for x, y in zip(v, basis)] + column = next((j for j, value in enumerate(v) if value), None) + if column is not None: + pivot = v[column] + pivots[column] = [x / pivot for x in v] + return len(pivots) + + +def modular_rank(rows, prime=65537): + """A nonzero mod-prime minor certifies a rational rank lower bound.""" + pivots = {} + for row in rows: + v = [x % prime for x in row] + for column, basis in sorted(pivots.items()): + coefficient = v[column] + if coefficient: + v = [(x - coefficient * y) % prime for x, y in zip(v, basis)] + column = next((j for j, value in enumerate(v) if value), None) + if column is not None: + inverse = pow(v[column], -1, prime) + pivots[column] = [(x * inverse) % prime for x in v] + return len(pivots) + + +def invert_binary(rows): + size = len(rows) + a = [row | (1 << (size + i)) for i, row in enumerate(rows)] + for column in range(size): + pivot = next((i for i in range(column, size) if (a[i] >> column) & 1), None) + require(pivot is not None, "singular binary form") + a[column], a[pivot] = a[pivot], a[column] + for i in range(size): + if i != column and ((a[i] >> column) & 1): + a[i] ^= a[column] + require([x & ((1 << size) - 1) for x in a] == [1 << i for i in range(size)], + "binary inverse identity") + return [x >> size for x in a] + + +def geometry(): + # Four-point affine planes of F2^3, with all sign lines; no imported data. + live = [] + for normal in range(1, 8): + for offset in (0, 1): + support = [x for x in range(8) if ((normal & x).bit_count() & 1) == offset] + require(len(support) == 4, "affine plane size") + for signs in product((-1, 1), repeat=3): + root = [0] * 8 + for coordinate, sign in zip(support, (1,) + signs): + root[coordinate] = sign + live.append(root) + axes = [[2 * (i == j) for i in range(8)] for j in range(8)] + roots = axes + live + require(len(live) == 112 and len({tuple(x) for x in roots}) == 120, "root count") + require(all(dot(x, x) == 4 for x in roots), "root norm") + require(all(dot(x, y) % 2 == 0 for x in roots for y in roots), "Gram integrality") + require(all(sum(x[i] * x[j] for x in live) == 56 * (i == j) + for i in range(8) for j in range(8)), "X transpose X") + gram = [sum(((1 + dot(x, y) // 2) & 1) << j for j, y in enumerate(roots)) for x in roots] + chosen = binary_basis(gram) + require(len(chosen) == 9, "Gram rank nine") + labels = [sum(((row >> index) & 1) << j for j, index in enumerate(chosen)) for row in gram] + form = invert_binary([labels[index] for index in chosen]) + + def pair(x, y): + return sum(((x >> i) & 1) * ((form[i] & y).bit_count() & 1) for i in range(9)) & 1 + + require(all(pair(labels[i], labels[j]) == ((gram[i] >> j) & 1) + for i in range(120) for j in range(120)), "label/form reconstruction") + require(binary_rank(labels[8:]) == 9, "live label rank") + live_labels = labels[8:] + census, deficient = Counter(), [] + for functional in range(1, 512): + complement = [root for root, label in zip(live, live_labels) + if (functional & label).bit_count() & 1] + rank = modular_rank(complement) + census[rank] += 1 + if rank != 8: + kernels = [j for j in range(8) if all(row[j] == 0 for row in complement)] + require(rank == 7 and len(kernels) == 1, "deficient complement kernel") + require(rational_rank(complement) == 7, "independent deficient rational rank") + deficient.append([functional, kernels[0]]) + require(census == {8: 503, 7: 8}, "support census") + require(sorted(j for _, j in deficient) == list(range(8)), "eight coordinate kernels") + exceptional = [[label for root, label in zip(live, live_labels) if root[j]] for j in range(8)] + require(all(len(s) == 56 and binary_rank(s) == 8 for s in exceptional), "exceptional dimensions") + pairs = [[binary_rank([sum(pair(x, y) << k for k, y in enumerate(w)) for x in u]) + for w in exceptional] for u in exceptional] + require(pairs == [[8] * 8 for _ in range(8)], "within-call pair lemma") + normals = [] + for support in exceptional: + candidates = [x for x in range(1, 512) if all(pair(x, y) == 0 for y in support)] + require(len(candidates) == 1, "exceptional hyperplane normal") + normals.append(candidates[0]) + receipt = {"live_roots": 112, "ambient_labels": 9, "modular_prime": 65537, + "complement_ranks": dict(sorted(census.items())), "deficient": deficient, + "support_pair_ranks": pairs, "geometry_sha256": sha([roots, labels, form])} + return live, live_labels, pair, exceptional, normals, receipt + + +def xor_sum(values): + result = 0 + for value in values: + result ^= value + return result + + +def check_chart(chart, pair): + require(len(chart) == 512 and set(chart) == set(range(512)), "chart bijection") + basis = [chart[1 << j] for j in range(9)] + require(all(chart[x] == xor_sum(basis[j] for j in range(9) if (x >> j) & 1) + for x in range(512)), "chart linearity") + require(all(pair(basis[i], basis[j]) == pair(1 << i, 1 << j) + for i in range(9) for j in range(9)), "chart isometry") + + +def rank_of_pairing(u, w, pair): + ub, wb = [u[i] for i in binary_basis(u)], [w[i] for i in binary_basis(w)] + return binary_rank([sum(pair(x, y) << k for k, y in enumerate(wb)) for x in ub]) + + +def lower_term(a, c, order, width): + position = {block: i for i, block in enumerate(order)} + return [[a[i] * c[j] if position[i // width] > position[j // width] else 0 + for j in range(len(c))] for i in range(len(a))] + + +def ordering_certificate(): + patterns = [] + for left in range(1, 8): + for right in range(1, 8): + if left & right: + continue + a, c = [[(mask >> i) & 1 for i in range(3)] for mask in (left, right)] + ranks = [rational_rank(lower_term(a, c, order, 1)) for order in permutations(range(3))] + expected_sum = 3 if sum(a) == sum(c) == 1 else 4 + require(set(ranks) <= {0, 1} and sum(ranks) == expected_sum, "three-call deletion counts") + patterns.append({"reader_mask": left, "source_mask": right, "six_ranks": ranks}) + require(len(patterns) == 12, "complete disjoint support domain") + a, c = [1, 0, 1, 0], [0, 1, 0, 1] + four_ranks = [rational_rank(lower_term(a, c, order, 1)) for order in permutations(range(4))] + require(max(four_ranks) == 2 and sum(four_ranks) == 24, "four-call scope control") + return {"three_call_patterns": patterns, "three_call_order_checks": 72, + "four_call_control": {"rank_histogram": dict(sorted(Counter(four_ranks).items())), + "rank_sum": sum(four_ranks), "orders": 24}} + + +def unit(index, size=24): + return [int(i == index) for i in range(size)] + + +def coefficient_endpoint(terms): + return [[sum(a[i] * c[j] for a, c in terms) for j in range(24)] for i in range(24)] + + +def check_endpoint(terms): + require(coefficient_endpoint(terms) == [[int(i == j) for j in range(24)] for i in range(24)], + "all-pairs coefficient endpoint") + + +def root_values(coefficient, live): + return [dot(root, coefficient[8 * s:8 * s + 8]) for s in range(3) for root in live] + + +def term_price(a, c, live, labels, charts, pair): + spans = [] + for coefficient in (a, c): + spans.append(sorted({charts[s][label] for s in range(3) + for root, label in zip(live, labels) + if dot(root, coefficient[8 * s:8 * s + 8])})) + return rank_of_pairing(*spans, pair) + + +def fixture(name, terms, live, labels, charts, pair): + check_endpoint(terms) + actual = [[0] * 336 for _ in range(336)] + prices, pure_terms = [], [] + for a, c in terms: + av, cv = root_values(a, live), root_values(c, live) + for i, value in enumerate(av): + if value: + for j, other in enumerate(cv): + if other: + actual[i][j] += value * other + reader = {s for s in range(3) if any(a[s * 8:(s + 1) * 8])} + source = {s for s in range(3) if any(c[s * 8:(s + 1) * 8])} + require(reader and source, "inactive fixture term") + pure = not reader.intersection(source) + rank = term_price(a, c, live, labels, charts, pair) + require(rank >= (7 if pure else 8), "term rank floor") + prices.append(rank) + if pure: + pure_terms.append((a, c)) + for i in range(336): + for j in range(336): + expected = dot(live[i % 112], live[j % 112]) if i // 112 == j // 112 else 0 + require(actual[i][j] == expected, "live all-pairs endpoint") + p, n = len(pure_terms), len(terms) - len(pure_terms) + require(3 * n + 2 * p >= 72, "averaged triangular count") + require(3 * sum(prices) >= 576 + 5 * p, "copy floor") + lower_ranks = [] + for order in permutations(range(3)): + ranks = [rational_rank(lower_term(a, c, order, 8)) for a, c in pure_terms] + require(24 <= n + sum(ranks), "triangular order rank inequality") + lower_ranks.append(sum(ranks)) + return {"name": name, "terms": len(terms), "pure": p, "non_pure": n, + "price_histogram": dict(sorted(Counter(prices).items())), "cost": sum(prices), + "lower_ranks_by_order": lower_ranks, "all_pairs_checked": 336 ** 2, + "terms_sha256": sha(terms)} + + +def rejected(action, diagnostic): + try: + action() + except ValueError as error: + require(diagnostic in str(error), "wrong control rejection: " + str(error)) + return + raise ValueError("control was accepted: " + diagnostic) + + +def run(): + sources = source_pins() + live, labels, pair, exceptional, normals, geom_receipt = geometry() + orders = ordering_certificate() + isotropic = [x for x in range(1, 512) if pair(x, x) == 0] + require(len(isotropic) == 255, "isotropic vector count") + targets = [u for u in isotropic if all(pair(v, u) for v in normals)] + require(len(targets) == 16, "targeted transvection count") + chosen = random.Random(47).sample(targets, 2) + charts = [list(range(512))] + [[x ^ (u if pair(x, u) else 0) for x in range(512)] for u in chosen] + for chart in charts: + check_chart(chart, pair) + cross_ranks = [[rank_of_pairing(exceptional[i], [charts[1][x] for x in exceptional[j]], pair) + for j in range(8)] for i in range(8)] + require(cross_ranks == [[7] * 8 for _ in range(8)], "real rank-seven cross terms") + for i in range(8): + for j in range(8): + direct = binary_rank([sum(pair(x, charts[1][y]) << k + for k, y in enumerate(exceptional[j])) for x in exceptional[i]]) + require(direct == cross_ranks[i][j], "direct cross-pair rank") + standard = [(unit(i), unit(i)) for i in range(24)] + one_cross = [(a[:], c[:]) for a, c in standard] + one_cross[0][1][8] = 1 + one_cross.append((unit(0), [-x for x in unit(8)])) + wide_cross = [(a[:], c[:]) for a, c in standard] + wide_cross[0][1][8] = wide_cross[0][1][16] = 1 + wide_cross.append((unit(0), [-int(i in (8, 16)) for i in range(24)])) + coupled = [(unit(i), unit(i)) for i in range(24) if i not in (0, 8, 16)] + common = [int(i in (0, 8, 16)) for i in range(24)] + coupled.append((common, common[:])) + for s in range(3): + correction = [-int(i in (0, 8, 16) and i != 8 * s) for i in range(24)] + coupled.append((unit(8 * s), correction)) + fixtures = [fixture(name, terms, live, labels, charts, pair) for name, terms in + (("standard", standard), ("one_rank7_cross", one_cross), + ("one_three_call_pure", wide_cross), ("sharp_deletion_coupled", coupled))] + require(fixtures[0]["cost"] == 192 and fixtures[1]["cost"] == 199, "attainment / rank-seven fixture") + require(fixtures[3]["non_pure"] == 22 and fixtures[3]["pure"] == 3 + and fixtures[3]["lower_ranks_by_order"] == [2] * 6, "sharp triangular count fixture") + controls = [] + shear = [x ^ (((x >> 1) & 1) << 0) for x in range(512)] + rejected(lambda: check_chart(shear, pair), "chart isometry") + controls.append("invertible nonisometric chart rejected") + rejected(lambda: require(min(map(min, cross_ranks)) >= 8, "false common-chart floor"), + "false common-chart floor") + controls.append("false per-term rank-eight floor rejected") + wrong_sign = [(a[:], c[:]) for a, c in one_cross] + wrong_sign[-1] = (unit(0), unit(8)) + rejected(lambda: check_endpoint(wrong_sign), "all-pairs coefficient endpoint") + controls.append("wrong cross cancellation sign rejected") + rejected(lambda: check_endpoint(standard[:-1]), "all-pairs coefficient endpoint") + controls.append("missing coordinate term rejected") + correlated = coupled[:22] + diagonal = coefficient_endpoint(correlated) + require(all(diagonal[i][j] == int(i == j) for i in range(24) for j in range(24) + if i // 8 == j // 8), "diagonal-only control positive side") + rejected(lambda: check_endpoint(correlated), "all-pairs coefficient endpoint") + controls.append("diagonal-only crosstalk rejected by all-pairs check") + four = orders["four_call_control"] + rejected(lambda: require(3 * four["rank_sum"] <= 2 * four["orders"], "four-call mean exceeds 2/3"), + "four-call mean exceeds 2/3") + controls.append("invalid four-call extension rejected") + rejected(lambda: require(max(four["rank_histogram"]) <= 1, "four-call truncation rank two"), + "four-call truncation rank two") + controls.append("rank-one truncation assumption at four calls rejected") + require(Fraction(7) > Fraction(4, 9) * 8 and Fraction(7, 8) > Fraction(2, 3), + "power-price positivity endpoints") + return {"schema_version": 1, "sources": sources, "geometry": geom_receipt, + "ordering": orders, "chart_seed": 47, "transvection_vectors": chosen, + "cross_pair_ranks": cross_ranks, "fixtures": fixtures, "negative_controls": controls, + "proof_status": "written quantified proof; finite evidence only, no formal theorem"} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--write", action="store_true", help="replace only this package's EXPECTED.json") + args = parser.parse_args() + result = run() + path = HERE / "EXPECTED.json" + if args.write: + path.write_text(canonical(result), encoding="utf-8") + else: + require(read_json(path) == json.loads(canonical(result)), "receipt mismatch") + print(canonical(result), end="") + print("receipt_sha256", sha(result)) + print("PASS_P112_THREE_CALL_ISOMETRIC_FLOOR") + + +if __name__ == "__main__": + main() From 25cd637a6f7bf92669bce28836e3015cbae87167 Mon Sep 17 00:00:00 2001 From: Sricharan Vagvala Date: Wed, 14 Oct 2026 22:58:45 -0700 Subject: [PATCH 2/2] Credit concurrent batch floor and frame this as an independent proof --- .../p112-three-call-isometric-floor/PROOF.md | 8 +++++++ .../p112-three-call-isometric-floor/README.md | 21 +++++++++++++++++-- .../SOURCES.json | 10 +++++++++ .../p112-three-call-isometric-floor/TASK.json | 12 +++++++++++ 4 files changed, 49 insertions(+), 2 deletions(-) diff --git a/research/p112-three-call-isometric-floor/PROOF.md b/research/p112-three-call-isometric-floor/PROOF.md index 188887e4aa..00e7039f85 100644 --- a/research/p112-three-call-isometric-floor/PROOF.md +++ b/research/p112-three-call-isometric-floor/PROOF.md @@ -7,6 +7,14 @@ It extends the **two-call** isometric-chart result of Sagar Thakrar's pending `18d6ac4f864af2b71aa8cf5f4541fcfc4350e2f0`, to **three** independent calls. The block-triangular averaging argument below is the new step. +Concurrent [PR2338](https://github.com/CrocSwap/integer-mult-bounds/pull/2338), +head `82700676e1d42acf98dc1921cb6ef82551620008`, section 3.4 states a broader +all-batch symmetric-chart result via normal classes and a frame lemma. It was +discovered during the final overlap check, after this core proof and verifier +were completed. This is an independent, narrower proof that does not use +that frame lemma or theorem; no first-closure claim is made. The attained +counting lemma below concerns all pure terms, not only rank-seven terms. + ## 1. Exact model and inherited finite premises Use the model of alephnan's merged PR1714 diff --git a/research/p112-three-call-isometric-floor/README.md b/research/p112-three-call-isometric-floor/README.md index 230160d571..e6132d3a34 100644 --- a/research/p112-three-call-isometric-floor/README.md +++ b/research/p112-three-call-isometric-floor/README.md @@ -1,6 +1,6 @@ # Three independently recharted P112 calls still pay 192 -**Scoped negative result / research note. No new supplier or kappa.** +**Independent proof / scoped negative result. No new supplier or kappa.** Three independent P112 all-pairs demands cannot share away their separate-total copy bill by using different **isometric binary label charts**. For arbitrary @@ -15,6 +15,18 @@ which explicitly leaves `k >= 3` open. It does **not** repeat its chart sample or claim the one-call support census as new. The new ingredient is the six-order triangular deletion lemma in [PROOF.md](PROOF.md), section 3. +**Concurrent overlap, discovered before submission:** DreamingOfClouds' +[PR2338](https://github.com/CrocSwap/integer-mult-bounds/pull/2338), head +`82700676e1d42acf98dc1921cb6ef82551620008`, states a broader all-batch theorem +for symmetric charts in section 3.4, using normal classes and an additional +frame lemma. The core proof and verifier here were completed before reading +that submission (retained in commit `9df32e528da547a1c1cb51cbd480f88f8b7d197e`). +This package supplies an **independent, frame-lemma-free proof for three +Gram-root-code calls**, an attained general counting bound, and direct +all-pairs/mutation evidence. Its scope and surplus bound are narrower than +the concurrent theorem's. No first-closure or stronger-floor claim is made; +the concurrent theorem and its full package have not been audited here. + ## Statement and evidence Let p count active terms whose nonzero reader and source calls are disjoint @@ -149,7 +161,9 @@ ledger; arbitrary diffs are not searched. The canonical claim is The final refresh at 05:54 UTC covered **550 open PRs and 1,058 Discussions** with complete pagination and no warnings. Main and PR2294's pinned head were unchanged. Other three-mode matches concern coordinates within one call, -not three independent calls. No competing matching result was identified. +not three independent calls. A subsequent newest-PR check at 05:56 UTC found +PR2338; its batching proof was read before submission, and the independent +contribution and narrower scope are stated above. Full task, stopping rule, final freshness and verification evidence are in [TASK.json](TASK.json). @@ -184,3 +198,6 @@ Douglas Colkitt / PR1240 for the centre-sharing motivation and package tools. The retained selected construction remains Rohan Arun's PR1094 on Jeremy Kothe's PR1087 and the cumulative k8/T16 lineage, with the DreamingOfClouds PR589 / eumemic PR555 bit supplier. No predecessor code or data is vendored. +DreamingOfClouds / concurrent PR2338 receives credit for the broader all-batch +symmetric-chart statement, independently developed using normal classes and +its frame lemma; the present argument does not use that result as a premise. diff --git a/research/p112-three-call-isometric-floor/SOURCES.json b/research/p112-three-call-isometric-floor/SOURCES.json index 5bfd3149ce..5cf2ef1b4a 100644 --- a/research/p112-three-call-isometric-floor/SOURCES.json +++ b/research/p112-three-call-isometric-floor/SOURCES.json @@ -43,6 +43,16 @@ "git_blob": "177c27bd6c4f75a2524eb2e8ade74045b7abb060", "url": "https://github.com/CrocSwap/integer-mult-bounds/blob/18d6ac4f864af2b71aa8cf5f4541fcfc4350e2f0/research/p112-batch-chart-change/PROOF.md", "usage": "Read-only cited predecessor and open question, no executable/data dependency; its mathematical two-call result is not used as an oracle in the new proof." + }, + { + "repository": "https://github.com/CrocSwap/integer-mult-bounds", + "pr": 2338, + "commit": "82700676e1d42acf98dc1921cb6ef82551620008", + "path": "research/decoder-floors-frontier-format/README.md", + "sha256": "0a941616cd2fac679182e5bb97e9a307bf22e42ac9541bbca3fadc81b1fda2b5", + "git_blob": "a1751a2a0b35d8607cf901da6fae6036cdb9e1bc", + "url": "https://github.com/CrocSwap/integer-mult-bounds/blob/82700676e1d42acf98dc1921cb6ef82551620008/research/decoder-floors-frontier-format/README.md", + "usage": "Concurrent overlap, read after the core proof/verifier were completed. Section 3.4 states a broader all-k symmetric-chart theorem via normal classes and a frame lemma. No mathematical or executable dependency here; not fully audited." } ] } diff --git a/research/p112-three-call-isometric-floor/TASK.json b/research/p112-three-call-isometric-floor/TASK.json index 1524d86c7f..976fffb812 100644 --- a/research/p112-three-call-isometric-floor/TASK.json +++ b/research/p112-three-call-isometric-floor/TASK.json @@ -163,5 +163,17 @@ "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.", "assessment": "Only predecessor PR2294, its released claim, our own claim/package, and unrelated one-call three-coordinate-mode results match. No competing three-call P112 isometric-chart proof was identified in the searched coverage." + }, + "contribution_status": "Independent proof / verification of a three-call floor also covered by concurrent PR2338; attained general triangular-count lemma; no first-closure claim.", + "late_overlap": { + "checked_utc": "2026-10-15T05:56:42Z", + "pr": 2338, + "head": "82700676e1d42acf98dc1921cb6ef82551620008", + "files_read": [ + "research/decoder-floors-frontier-format/README.md, especially section 3.4" + ], + "comparison": "PR2338 states a stronger all-k symmetric-chart result using hyperplane normal classes and an additional frame lemma. This package independently proves the k=3 Gram-root-code floor by a six-order triangular deletion argument, without that frame lemma, and certifies its sharp n+(2/3)p count, full all-pairs fixtures and failure controls. No audit of all PR2338 claims is made.", + "core_commit_before_reading": "9df32e528da547a1c1cb51cbd480f88f8b7d197e", + "decision": "Retain one focused contribution as a meaningfully different independent proof/certificate package; update framing and credit before submitting." } }