From 4fcd89fc1f6c7760349def38d81e9d4f307587d4 Mon Sep 17 00:00:00 2001 From: Ali Romman <226877337+aliromman@users.noreply.github.com> Date: Mon, 26 Oct 2026 00:07:11 -0500 Subject: [PATCH 1/4] Retain PR5673 proof for independent connector audit --- .../vendor/PR5673-PROOF.md | 231 ++++++++++++++++++ 1 file changed, 231 insertions(+) create mode 100644 research/one-sided-connector-audit/vendor/PR5673-PROOF.md diff --git a/research/one-sided-connector-audit/vendor/PR5673-PROOF.md b/research/one-sided-connector-audit/vendor/PR5673-PROOF.md new file mode 100644 index 0000000000..e3800fbcf1 --- /dev/null +++ b/research/one-sided-connector-audit/vendor/PR5673-PROOF.md @@ -0,0 +1,231 @@ +# A connector must distinguish leaves in both directions + +This is a theorem about finite matrices in characteristic two. It is not a +native multiplication theorem. No new kappa is established. + +## 1. Contract + +Let the main space be `W_0 + W_1 + ... + W_g`, with each block of dimension +`d > 0`. Block zero is the core. Stage j acts on the core and leaf j. On these +two blocks put + +```text +E_j = diag(I,I), T_j = [[I,I],[I,I]]. +``` + +Thus `T_j^2=0`. Stage j can have any finite number of full calls. Their +projectors `P_jh` form an orthogonal resolution of `E_j`, and commute with +`T_j`. Their query maps are `R_jh=P_jh T_j`. There is no bound on the number +of stages, the number of splits, the block dimension, or their call order. + +In the normalized ring `F[e,D_1,...,D_g]/(e^2)`, a full call is + +```text +(I+(D_j+1)P_jh)(I+e R_jh). +``` + +A thin call is `I+e Z`. The proof permits arbitrary matrices Z. In particular, +it does not impose a rank, a square-zero condition, or a count on thin calls. +The required word is `Q product_j (I+(D_j+1)E_j)`, where `Q=1+e`. +The main fields are independent. All D variables remain independent. + +This is the star stage contract from PR5631/5649, with arbitrary stage splits +and a much larger connector class. It excludes no general complex or dyadic +caller. It also excludes no caller with a different grouped stage map, a +nonfull stage, a different output, or paid idle multipliers. + +## 2. The one-sided theorem + +**Theorem.** A successful word cannot have three distinct leaves whose block +columns are identical in every thin matrix Z. It also cannot have three +leaves whose block rows are identical in every thin matrix Z. + +Only one of these two equalities is needed for exclusion. Thus changing the +forward split, adding more queries, increasing their rank, or adding more +stage splits cannot repair connectors which only see the sum of the leaves. + +### Local form and chronology + +Commutation with T and the local support give + +```text +P_jh = [[A_jh+B_jh, B_jh], [B_jh, A_jh+B_jh]], +R_jh = [[A_jh, A_jh], [A_jh, A_jh]]. +``` + +The A matrices form an orthogonal resolution of I. In particular, +`A_jh A_jk=0` for `h!=k`, `A_jh^2=A_jh`, and `sum_h A_jh=I`. +These statements do not require the A matrices of different stages to commute. +The orthogonal-resolution hypothesis also follows from full rank use: if the +projectors sum to E and their ranks sum to rank E, their images form a direct +sum. Each projector is then the corresponding coordinate projection on that +sum. Stages with a rank deficit are a different contract. + +Set all D variables to one. The coefficient of e requires `sum R=I`, including +thin queries. The mixed coefficient of `e(D_j+1)` then requires + +```text +sum_(full call i in stage j) [P_i, sum_(calls l later than i) R_l] = 0. (1) +``` + +This necessary condition follows by expanding the literal ordered word. +No full-word converse is used. + +For distinct selected stages j,k define + +```text +S_jk = sum_(call (j,h) before call (k,l)) A_jh A_kl. (2) +``` + +In (1), add block rows zero and j, and read block column k. The contribution +of good calls is S_jk. The contribution of a later thin map Z is +`A_jh (Z_0k+Z_jk)`. If the three selected leaf columns of every Z are equal, +this thin contribution is the same for the two choices of k other than j. +Consequently + +```text +S_jk = S_jl for each permutation (j,k,l) of the three stages. (3) +``` + +Other good stages do not contribute to these blocks. Thus the argument +restricts to any three selected leaves in a larger star. + +### The prefix determinant argument + +Read just the calls of the three selected stages in their original order. +Before a call with projection A from stage j, let P_k be the sum of the A +projections already read from stage k. Left multiplication of (2) by A and +orthogonality within stage j give + +```text +A S_jk = A(I+P_k). +``` + +Equation (3) gives `A P_k=A P_l`. Also `A P_j=0`. Therefore, for the total +prefix `S=P_0+P_1+P_2`, every update satisfies + +```text +A S=0. (4) +``` + +Introduce an independent central variable x. Equation (4) implies + +```text +(I+xA)(I+xS) = I+x(S+A). +``` + +Starting at S=0, the product of all these factors is `I+xS_final`. +At the end, `S_final=I+I+I=I`. On the other hand, an idempotent of rank r +has determinant `det(I+xA)=(1+x)^r`. Each stage is a resolution of I, +so its ranks sum to d. Taking determinants now gives + +```text +(1+x)^(3d) = det(product(I+xA)) = det((1+x)I) = (1+x)^d. +``` + +This is impossible for positive d. This proves the column statement for +all finite dimensions and all finite split counts. It uses no list of orders. +Transpose all matrices and reverse the order to obtain the row statement. + +## 3. A paid-rank and finite-field cut + +Assume g is at least three. The sum of the good queries is +`sum T_j`. Hence the thin sum must be + +```text +K = I+sum T_j = epsilon E_core + F+G, +epsilon = (g+1) mod 2, +F: each leaf -> core by I, G: core -> each leaf by I. +``` + +The rank of K is `2d`. Its column space is the core plus the diagonal leaf +space, and its row space is the core plus the leaf-sum space. + +Let U be the span of all thin images, and V the span of all thin row spaces. +Write `dim U=2d+a`, `dim V=2d+b`, and let R be the sum of thin ranks. +Factor each thin map at its actual rank, then concatenate those factors. +Sylvester's rank inequality gives + +```text +R >= dim U + dim V - rank K = 2d+a+b. (5) +``` + +Both a and b must be positive. Otherwise one side of the one-sided theorem +applies to all leaves. In particular **R >= 2d+2**, over any field of +characteristic two. + +For a finite field of size s, choose b additional row basis vectors beyond +the row space of K. Their restriction to one leaf is a `b by d` matrix. +There are at most `s^(bd)` such signatures. Equal signatures imply equal +leaf columns for every thin map. Each signature can occur at most twice. +The column-space argument is the same. Therefore + +```text +g <= 2 s^(bd), g <= 2 s^(ad), +R >= 2d + 2 h, h = min {z >= 0 : g <= 2 s^(dz)}. (6) +``` + +This is a necessary condition, not a construction or a sufficient test. +It concerns a common field and a fixed block basis. For one-port binary +copies, d=2. It gives R>=6 for g=3..8, R>=8 for g=9..32, and R>=10 for +g=33..128. For coupled ports, use the actual larger d. Do not apply the +one-port bound per port after ports have been coupled. + +At g=31, five rank-one connectors fail this cut. Five rank-two connectors +with d=4 meet it exactly: `2d+2=10`. Thus coupled pairs of ports are a precise +remaining target. The cut does not prove that such a word exists. + +## 4. Constructive escape and its price + +`ESCAPE-WORD.json` contains a complete eight-field binary word. It has three +paired stages, six full calls with rank-one queries, and eight rank-one thin calls. +Every local projector, query rank and compatibility relation is checked. +The verifier retains every exponent of each independent D variable and +checks every coefficient of the full word. It also checks that the thin +maps distinguish all three leaves in both directions. + +Thus the changed connector contract has a real positive operator. It does +not give a profitable supplier. At the pinned PR5599 tariff, 104 copies have +complete optimistic moment coefficients + +```text +208 H25 + 624 H9 + 6 helpers - 6 paid - 832 H1. +``` + +Its linear margin is -336. After common ranks are cancelled, all positive +terms have rank at least eight and all negative terms have rank at most +seven. For every `0<=t<=1`, the margin is at most `8^(t-1)*(-336)<0`. +Additional physical adapters cannot repair that price. + +The new cut still leaves a useful target. At g=127, ten thin queries are +allowed by (6) for one-port binary copies. The optimistic PR5599 profile +has a positive exact margin at saving `7/2000=.0035`, and its numerical +crossing is about .00364156. **No 127-leaf word is supplied.** This screen +also does not establish a characteristic-zero lift, native frame adapters, +compiler admission, an outer transfer, or a new kappa. + +A smaller coupled target is g=31 with five rank-two connectors per two-port +block. Its optimistic bill, scaled to 104 ports, also has positive exact +margin at .0035. It needs only 62 full calls. No such word is supplied either. +Coupling physical ports can require new frame maps; their costs must be +charged before this screen can become a supplier claim. + +## 5. Evidence and limits + +The main result is a written finite-dimensional matrix proof. The checker +also verifies fifteen exact free-algebra certificates for the paired-stage +case, without a solver or the discovery implementation. Matrix and formal +polynomial controls test the chronology extraction, restriction to three +leaves, prefix factorization and determinant formula. They support the +proof; finite tests alone do not prove its unbounded statements. + +The discovery archive retains changed C,D splits, arbitrary aggregate maps, +extra thin queries, a different cycle frame, and three-/four-way splits. +Timeouts remain unknown. Passing first mixed coefficients is not passing the +full word. No proof assistant or independent human acceptance is claimed. + +Credit Cinna Davis's controller and simplex work; PR5617/5631/5649 for the +query-frame and fixed-star line; and the complete P104/native/helper/compiler +lineage for the tariff. This proof, cut, search and escape word were prepared +for Ali Romman with substantial OpenAI Codex assistance. No subagents. +New work is Apache-2.0. From 0f4becae8ec75c58afae1bda9dde8736ab9f3bcd Mon Sep 17 00:00:00 2001 From: Ali Romman <226877337+aliromman@users.noreply.github.com> Date: Mon, 26 Oct 2026 00:12:18 -0500 Subject: [PATCH 2/4] Audit the connector obstruction and attain its static rank bound --- research/one-sided-connector-audit/PROOF.md | 169 ++++++++++ research/one-sided-connector-audit/README.md | 61 ++++ .../one-sided-connector-audit/RESULT.json | 99 ++++++ .../one-sided-connector-audit/SOURCES.json | 34 ++ research/one-sided-connector-audit/TASK.json | 69 ++++ .../one-sided-connector-audit/VALIDATION.md | 9 + .../one-sided-connector-audit/VERIFY.json | 20 ++ research/one-sided-connector-audit/verify.py | 315 ++++++++++++++++++ 8 files changed, 776 insertions(+) create mode 100644 research/one-sided-connector-audit/PROOF.md create mode 100644 research/one-sided-connector-audit/README.md create mode 100644 research/one-sided-connector-audit/RESULT.json create mode 100644 research/one-sided-connector-audit/SOURCES.json create mode 100644 research/one-sided-connector-audit/TASK.json create mode 100644 research/one-sided-connector-audit/VALIDATION.md create mode 100644 research/one-sided-connector-audit/VERIFY.json create mode 100644 research/one-sided-connector-audit/verify.py diff --git a/research/one-sided-connector-audit/PROOF.md b/research/one-sided-connector-audit/PROOF.md new file mode 100644 index 0000000000..e3be1bb272 --- /dev/null +++ b/research/one-sided-connector-audit/PROOF.md @@ -0,0 +1,169 @@ +# The static connector rank cut is sharp + +This package checks the proof in the retained PR5673 source. It also gives +new static witnesses at its rank lower bound. A static witness gives the +thin query maps, their sum, ranks and leaf signatures. It does not give a +chronological word. No new kappa follows. + +## 1. Audit of the source implication + +Use the source contract, over a field of characteristic two. Each stage j +has full projectors P_jh supported on the core and leaf j. They give an +orthogonal resolution of that support. They commute with the local query +T_j, whose four blocks are I. Their queries are R_jh=P_jh T_j. +A thin map Z has no stage variable. All stage variables are independent. +The target is the stated product of full stages, times the scalar 1+e, +where e squared is zero. These hypotheses are required. + +Put x_j=D_j+1. Work first in the quotient which also sets x_j squared to +zero and every other x to zero. This quotient supplies necessary conditions +only. Read the literal calls in application order. If R_< and R_> are the +sums before and after a full call (P,R), the coefficient of e x_j contributed +by that call is + +```text +P R_< + R_> P + P R. +``` + +The coefficient of e first gives sum R=I. Since P R=R, the expression becomes +`P + P R_> + R_> P`. Summing the stage projectors gives E_j. The target has +e x_j coefficient E_j. Thus its defect is exactly the sum of commutators +`P R_> + R_> P`. No pure higher coefficient or endpoint converse is assumed. + +Commutation with T gives P=[[A+B,B],[B,A+B]]. The idempotent and orthogonality +relations imply that the A matrices in each stage are orthogonal idempotents +with sum I. Add block rows core and j, then take leaf column k, where k!=j. +The right product R_> P has no such column. A later stage k contributes +A_jh A_kl. Other full stages contribute zero. A thin map contributes +`A_jh (Z_0k+Z_jk)`. This proves the source restriction even when there are +other leaves, noncommuting stage flags and arbitrary blocks outside the +chosen three columns. + +If three leaf columns of every thin map agree, the thin contribution does +not depend on which of the other two leaves is k. Therefore S_jk=S_jl, +where S_jk is the sum of A_jh A_kl for jh before kl. For a given call A_jh, +orthogonality within j gives `A_jh S_jk=A_jh(I+P_k)`, with P_k the earlier +prefix of stage k. Thus A_jh P_k=A_jh P_l. Its own earlier prefix is +annihilated. The total prefix S obeys A_jh S=0. + +For a formal central variable x, this gives +`(I+xA)(I+xS)=I+x(A+S)` at every step. The product of factors is therefore +`(1+x)I`, since the three final stage prefixes each equal I. Each idempotent +of rank r has determinant (1+x)^r: its image and kernel give a direct sum +basis. Each stage contributes total rank d. The same determinant would have +to be both (1+x)^(3d) and (1+x)^d. These polynomials have different degrees +for d>0. This is a contradiction over every field of characteristic two. +Transpose and reverse the whole word for the row version. The target is +preserved by this operation because its full stage supports commute. + +No mathematical gap was found in this implication under these hypotheses. +The source does not exclude a different stage support, an incomplete stage, +a different target or a characteristic-zero caller. This audit does not +supply human review or a proof-assistant theorem. + +## 2. Rank cut and its exact static realization + +Let F have q elements, where q is a power of two. Let d,h be positive +integers. Put + +```text +g = 2 q^(d h) - 1, W = F^d + (F^d)^g. +``` + +Index the leaves by all h-by-d matrices M over F: use the zero matrix once +and every nonzero matrix twice. On W, define F_i to send coordinate i of +every leaf to core coordinate i. Define G_i to send core coordinate i to +coordinate i of every leaf. Both have rank one and square zero. Put + +```text +K = sum_i (F_i+G_i). +``` + +This is the required thin sum for odd g. It has rank 2d. Its image consists +of the core and the diagonal leaf space. Its row space consists of the core +and the leaf-sum space. + +For 1<=a<=h, let u_a have zero core and leaf block equal to row a of M, +viewed as a column. Let v_a have zero core and the same leaf entries as a +row. Put E_a=u_a v_a. Each E_a has rank one. Every nonzero signature occurs +twice, so + +```text +sum_leaf u_a = 0, sum_leaf v_a = 0, v_a u_b = 0 +``` + +for all a,b. Consequently E_a E_b=0; F_i E_a=E_a F_i=0; and +G_i E_a=E_a G_i=0. In particular all these maps have square zero. +Take the following thin maps, with both copies of each E_a charged: + +```text +F_0,...,F_(d-1), G_0,...,G_(d-1), E_1,E_1,...,E_h,E_h. +``` + +Their sum is K and their total rank is exactly 2d+2h. Their image span and +row span each have dimension 2d+h. To see independence of the extra h +vectors modulo the diagonal space, first inspect the zero-signature leaf. +It forces any diagonal component to vanish. Then inspect signatures with +one nonzero matrix entry; these force each coefficient of u_a to vanish. +The row proof is the same. + +Two leaves have the same block columns in all thin maps exactly when their +matrices M agree. Indeed the F/G columns are constant across leaves, and +E_a recovers row a of M because u_a is nonzero. The row statement uses v_a. +Thus there are exactly q^(dh) signatures; each occurs once or twice. +No forbidden triple occurs. + +The source Sylvester bound is R>=2d+a+b, with extra image and row dimensions +a,b. Both equal h here, so equality holds. The source signature bound asks +for the least z such that g<=2q^(dz). For this g, that least z is h. +Thus **both bounds are attained together by square-zero maps**, for every +q,d,h above. This proves sharpness of these static bounds at an unbounded +family of sizes. It does not prove sharpness for complete chronological +words. + +## 3. Five rank-two maps for the 31-leaf target + +When h=1 and d>=2, write E=E_1 and group the charged rank-one maps as + +```text +Z_0 = F_0 + E, +Z_1 = G_1 + E, +Z_(i+1) = F_i + G_((i+1) mod d), 1<=i=2, they group into d+1 rank-two +square-zero queries. This supplies static maps for both source targets: + +- F2, d=4: 31 leaves and five rank-two queries. +- F2, d=2, h=3: 127 leaves and ten rank-one queries. + +[PROOF.md](PROOF.md) gives the formulas and the audited implication. +[RESULT.json](RESULT.json) gives the exact finite checks. +[SOURCES.json](SOURCES.json) pins the retained source proof. The static maps +are not chronological words. Their purpose is to settle the proposed static +rank cut and give precise matrices for the next full-word search. A stronger +exclusion needs another condition. Native frames, ownership, tape costs and +the complete supplier remain open; the selected kappa is unchanged. + +## Reproduce + +Python 3.12 and its standard library suffice. From the repository root: + +```sh +python3.12 -B scripts/research_package.py --package research/one-sided-connector-audit +python3.12 -I -O -B research/one-sided-connector-audit/verify.py +``` + +Expect `PASS_ONE_SIDED_AUDIT_AND_STATIC_SHARPNESS` and the registered package +pass. The separate implementation imports no predecessor checker or finite +certificate. It checks 19,440 flag/order pairs, 72 literal words, 432 extracted +blocks, formal polynomial determinants and six full static matrices. The +matrices include the two proposed targets and F4. Twelve damaged constructions +are rejected. [VALIDATION.md](VALIDATION.md) records the executed export and +source corruption checks and the omitted checks. + +## Open next questions + +Choose a chronological split and order for the explicit 31-leaf maps, or +change these maps. Check every independent stage polynomial coefficient. +The static bounds give no guarantee that this is possible. Even a successful +binary word needs a native lift and a complete paid invoice before it can +change the multiplication bound. Do not run another rank-only search of +these exact targets as a substitute for that missing step. + +## Credit and scope + +Source: Ali Romman's PR5673 at c10f75f09e41803ae8efe478331a7509b7379b2f, +with substantial OpenAI Codex assistance. It supplies the one-sided proof, +Sylvester/signature cuts and the two search targets. Its retained proof credits +Cinna Davis, the PR5617/5631/5649 interface line and all P104/native/helper +contributors. This package adds the static sharpness theorem and a separate +implementation; it does not claim independent human or model-family review. +Prepared by Ali Romman with substantial OpenAI Codex assistance. No subagents. +Apache-2.0. Base main df0137efd35e11b4445734bf612bdd4c7ebc330c, priority7. +Coordination is in [Discussion5593](https://github.com/CrocSwap/integer-mult-bounds/discussions/5593#discussioncomment-19188781). diff --git a/research/one-sided-connector-audit/RESULT.json b/research/one-sided-connector-audit/RESULT.json new file mode 100644 index 0000000000..a6e86d06e9 --- /dev/null +++ b/research/one-sided-connector-audit/RESULT.json @@ -0,0 +1,99 @@ +{ + "limits": [ + "Written universal proof; no proof-assistant or human acceptance", + "Static witnesses are not chronological words", + "No native lift, complete physical invoice or new kappa" + ], + "mixed_coefficient_audit": { + "literal_words": 72, + "noncommuting_flags": 55, + "off_support_extractions": 432, + "words_with_external_stages": 48 + }, + "prefix_audit": { + "formal_polynomial_products": 36, + "nonzero_prefix_defects": 173, + "projection_determinants": 324 + }, + "split_census": { + "digest": "dca72cf055129c18dc3cc767c5977a5339aec70cb7d38850d21a54e99c7a54b8", + "first_failure_histogram": [ + 0, + 10368, + 9072, + 0, + 0, + 0 + ], + "ordered_flag_words": 19440 + }, + "static_witnesses": [ + { + "d": 2, + "field_dimension": 16, + "field_size": 2, + "h": 1, + "leaves": 7, + "rank_one_queries": 6, + "rank_two_queries": 3, + "rejected_controls": 2, + "thin_rank": 6 + }, + { + "d": 3, + "field_dimension": 48, + "field_size": 2, + "h": 1, + "leaves": 15, + "rank_one_queries": 8, + "rank_two_queries": 4, + "rejected_controls": 2, + "thin_rank": 8 + }, + { + "d": 4, + "field_dimension": 128, + "field_size": 2, + "h": 1, + "leaves": 31, + "rank_one_queries": 10, + "rank_two_queries": 5, + "rejected_controls": 2, + "thin_rank": 10 + }, + { + "d": 2, + "field_dimension": 64, + "field_size": 2, + "h": 2, + "leaves": 31, + "rank_one_queries": 8, + "rank_two_queries": null, + "rejected_controls": 2, + "thin_rank": 8 + }, + { + "d": 2, + "field_dimension": 256, + "field_size": 2, + "h": 3, + "leaves": 127, + "rank_one_queries": 10, + "rank_two_queries": null, + "rejected_controls": 2, + "thin_rank": 10 + }, + { + "d": 2, + "field_dimension": 64, + "field_size": 4, + "h": 1, + "leaves": 31, + "rank_one_queries": 6, + "rank_two_queries": 3, + "rejected_controls": 2, + "thin_rank": 6 + } + ], + "status": "PASS_ONE_SIDED_AUDIT_AND_STATIC_SHARPNESS" +} diff --git a/research/one-sided-connector-audit/SOURCES.json b/research/one-sided-connector-audit/SOURCES.json new file mode 100644 index 0000000000..9a52740e72 --- /dev/null +++ b/research/one-sided-connector-audit/SOURCES.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "base_commit": "df0137efd35e11b4445734bf612bdd4c7ebc330c", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8", + "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "research/one-sided-connector-audit/vendor/PR5673-PROOF.md", + "usage": "input", + "git_blob": "e3800fbcf1c5f5633e14d9856ca1400985292a0d", + "sha256": "e086b3376173f6b790e05ef09f23b4d5970c8ac5145ab2970e084743f782190b", + "pin": "head:4fcd89fc1f6c7760349def38d81e9d4f307587d4:research/one-sided-connector-audit/vendor/PR5673-PROOF.md" + } + ], + "external_inputs": [ + { + "local_path": "vendor/PR5673-PROOF.md", + "source_repository": "aliromman/integer-mult-bounds", + "source_commit": "c10f75f09e41803ae8efe478331a7509b7379b2f", + "source_path": "research/crossed-connector-caller/PROOF.md", + "sha256": "e086b3376173f6b790e05ef09f23b4d5970c8ac5145ab2970e084743f782190b" + } + ] +} diff --git a/research/one-sided-connector-audit/TASK.json b/research/one-sided-connector-audit/TASK.json new file mode 100644 index 0000000000..b45667621c --- /dev/null +++ b/research/one-sided-connector-audit/TASK.json @@ -0,0 +1,69 @@ +{ + "schema_version": 1, + "task_id": "connector-alphabet-change", + "priority_revision": 7, + "base_commit": "df0137efd35e11b4445734bf612bdd4c7ebc330c", + "original_card": { + "id": "connector-alphabet-change", + "question": "Does one explicit extension of the connector alphabet offer a favorable completed budget?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/universal-connector-boundary/README.md", + "certificates/selected-result.json" + ], + "methods": [ + "Construct and charge a legal extra operation on a minimal instance.", + "Prove a target-specific bound after adding one specified operation family." + ], + "acceptance_gate": "State which fixed-alphabet premise changes and charge its implementation; do not declare it free. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "research/universal-connector-boundary/verify.py" + ], + "expected": "PASS_UNIVERSAL_CONNECTOR_BOUNDARY", + "inspect": "Reproduce the 945-pairing control, then read Exact interface to list the allowed calls.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Add exactly one legally priced operation and test a tiny dirty-input instance before enumerating larger cases.", + "bottleneck_link": "A new legal connector operation could change recursive interface cost; a larger census in the same alphabet is a separate side result.", + "allowed_variations": [ + "Choose one additional operation and a small source count for its first counterexample." + ], + "scope_change_triggers": [ + "Keeping the alphabet and only increasing the source count; record this as a changed assignment.", + "Extending a source-count census without naming a supplier/interface decision it could change; audit #2973 pruning concerns before relying on the affected predecessor exclusions." + ], + "overlap_terms": [ + "universal connector", + "source-toggle", + "connector alphabet" + ] + }, + "scope_status": "changed", + "actual_scope": "Independent proof audit of PR5673, and exact sharpness of its static rank/signature cut with legal square-zero maps.", + "scope_change_reason": "Released independent review handoff in Discussion1166; original recursive-interface card remains in this file.", + "bottleneck_link": "Check the exclusion used to select long P104 callers. Explicit rank-minimum maps prove that static rank/signature tests cannot reject the remaining targets.", + "budget_minutes": 90, + "stop_rule": "Finish the proof audit and static sharpness construction. Do not claim a complete star word or a native supplier.", + "outcome": "scoped theorem and independent audit", + "evidence": "PROOF.md and RESULT.json; separate literal coefficient, matrix and enumeration checks.", + "author": "Ali Romman with substantial OpenAI Codex assistance", + "ai_assistance": "OpenAI Codex; no subagents. This is a separate implementation, not independent human review.", + "open_questions": [ + { + "question": "Does the 31-leaf, five rank-two static witness admit any full star word?", + "why_it_matters": "The source optimistic P104 price passes, but a word is absent.", + "first_step": "Use or change the explicit maps, solve complete chronological polynomial equations, and check every coefficient.", + "blocked_by": "Native adapters and the full physical bill remain after a binary word." + } + ], + "coordination": { + "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/5593#discussioncomment-19188781", + "source_pr": "https://github.com/CrocSwap/integer-mult-bounds/pull/5673", + "source_head": "c10f75f09e41803ae8efe478331a7509b7379b2f", + "picker_nonce": "056e2c1a811710ff064606e5d5e318a9", + "main": "df0137efd35e11b4445734bf612bdd4c7ebc330c" + } +} diff --git a/research/one-sided-connector-audit/VALIDATION.md b/research/one-sided-connector-audit/VALIDATION.md new file mode 100644 index 0000000000..e64cefa048 --- /dev/null +++ b/research/one-sided-connector-audit/VALIDATION.md @@ -0,0 +1,9 @@ +# Verification record + +The normal and optimized registered runs check the same saved RESULT.json. +The source proof is retained byte-for-byte and is checked by SHA-256 before +science checks. The checker uses Python 3.12 and the standard library. + +Publication checks, export evidence and scope limits are recorded below after +execution. No formal-kernel proof, independent human review, complete caller, +native supplier, selected cold replay or hosted CI acceptance is claimed. diff --git a/research/one-sided-connector-audit/VERIFY.json b/research/one-sided-connector-audit/VERIFY.json new file mode 100644 index 0000000000..251e534ed6 --- /dev/null +++ b/research/one-sided-connector-audit/VERIFY.json @@ -0,0 +1,20 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/one-sided-connector-audit/vendor/PR5673-PROOF.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Independent proof identities, full split census, static square-zero constructions and rejection controls." + } + ] +} diff --git a/research/one-sided-connector-audit/verify.py b/research/one-sided-connector-audit/verify.py new file mode 100644 index 0000000000..24ad8cd34c --- /dev/null +++ b/research/one-sided-connector-audit/verify.py @@ -0,0 +1,315 @@ +#!/usr/bin/env python3 +"""Check the connector proof identities and sharp static constructions. + +Ali Romman with substantial OpenAI Codex assistance. Apache-2.0. +""" +import hashlib +import itertools +import json +from pathlib import Path +import random + +ROOT = Path(__file__).resolve().parent + +def require(ok, message): + if not ok: + raise ValueError(message) + +def eye(n): + return tuple(1 << i for i in range(n)) + +def zero(n): + return (0,) * n + +def add(a, b): + return tuple(x ^ y for x, y in zip(a, b)) + +def mul(a, b): + out = [] + for row in a: + v = 0 + while row: + low = row & -row + v ^= b[low.bit_length()-1] + row ^= low + out.append(v) + return tuple(out) + +def rank(rows): + basis = {} + for v in rows: + while v: + k = v.bit_length()-1 + if k not in basis: + basis[k] = v + break + v ^= basis[k] + return len(basis) + +def transpose(a): + n = len(a) + return tuple(sum(((a[j] >> i) & 1) << j for j in range(n)) for i in range(n)) + +def inverse(a): + n = len(a) + rows = [a[i] | (1 << (n+i)) for i in range(n)] + for j in range(n): + k = next(i for i in range(j, n) if rows[i] >> j & 1) + rows[k], rows[j] = rows[j], rows[k] + for i in range(n): + if i != j and rows[i] >> j & 1: + rows[i] ^= rows[j] + return tuple(r >> n for r in rows) + +def random_gl(n, rng): + a = list(eye(n)) + for _ in range(5*n): + i,j = rng.sample(range(n),2) + a[i] ^= a[j] + return tuple(a) + +def outer(u,v,n): + return tuple(v if u >> i & 1 else 0 for i in range(n)) + +def local(a,b,j,g,d): + n=(g+1)*d + out=[0]*n + for i in range(d): + out[i]=(a[i]^b[i]) | b[i] << (j*d) + out[j*d+i]=b[i] | (a[i]^b[i]) << (j*d) + return tuple(out) + +def block(a,r,c,d): + return tuple((a[r*d+i] >> (c*d)) & ((1<> (chosen[0]*d)) & mask + for leaf in chosen[1:]: + z[i]=(z[i] & ~(mask << (leaf*d))) | value << (leaf*d) + z=tuple(z) + calls.append((0,zero(n),z,zero(d))) + rng.shuffle(calls) + repair=add(eye(n),sum_mats((r for _,_,r,_ in calls),n)) + calls.insert(rng.randrange(len(calls)+1),(0,zero(n),repair,zero(d))) + for _,_,zz,_ in (c for c in calls if c[0]==0): + require(all(block(zz,r,chosen[0],d)==block(zz,r,k,d) for r in range(g+1) for k in chosen),'equal columns') + for j in chosen: + # Direct literal multiplication in F2[e,x]/(e^2,x^2). + ce=zero(n);cx=zero(n);cex=zero(n) + for stage,p,r,a in calls: + px=p if stage==j else zero(n) + cex=add(add(add(cex,mul(r,cx)),mul(px,ce)),mul(px,r)) + ce=add(ce,r);cx=add(cx,px) + require(ce==eye(n),'query sum') + later=zero(n);comm=zero(n) + for stage,p,r,a in reversed(calls): + if stage==j:comm=add(comm,add(mul(p,later),mul(later,p))) + later=add(later,r) + require(add(cex,cx)==comm,'literal mixed coefficient') + other=[k for k in chosen if k!=j] + s={k:zero(d) for k in other};thin={k:zero(d) for k in other} + for i,(stage,p,r,a) in enumerate(calls): + if stage!=j:continue + for st2,p2,r2,a2 in calls[i+1:]: + for k in other: + if st2==k:s[k]=add(s[k],mul(a,a2)) + if st2==0:thin[k]=add(thin[k],mul(a,add(block(r2,0,k,d),block(r2,j,k,d)))) + for k in other: + got=add(block(comm,0,k,d),block(comm,j,k,d)) + require(got==add(s[k],thin[k]),'three-leaf extraction') + extractions+=1 + require(thin[other[0]]==thin[other[1]],'common thin term') + if g>3:distinct_external+=1 + cases+=1 + require(noncommuting>0 and distinct_external>0,'control coverage') + return {'literal_words':cases,'off_support_extractions':extractions,'noncommuting_flags':noncommuting,'words_with_external_stages':distinct_external} + +def poly_mul(a,b): + out=0 + while b: + if b&1:out^=a + a<<=1;b>>=1 + return out + +def poly_det(a): + n=len(a);out=0 + for order in itertools.permutations(range(n)): + term=1 + for i,j in enumerate(order):term=poly_mul(term,a[i][j]) + out^=term + return out + +def prefix_audit(): + rng=random.Random(51973);factors=0;products=0;defects=0 + for d in (2,3,4): + for trial in range(12): + calls=[] + for j in range(3): + h=random_gl(d,rng);hi=inverse(h) + for i in range(d): + a=mul(mul(h,tuple(1<>j)&1)<<1) for j in range(d)] for i in range(d)] + require(poly_det(factor)==3,'rank-one determinant') + next_product=[[0]*d for _ in range(d)] + for i in range(d): + for j in range(d): + for k in range(d):next_product[i][j]^=poly_mul(factor[i][k],product[k][j]) + product=next_product + if mul(a,prefix)!=zero(d):defects+=1 + prefix=add(prefix,a);factors+=1 + require(prefix==eye(d),'final prefix') + expected=1 + for _ in range(3*d):expected=poly_mul(expected,3) + require(poly_det(product)==expected,'product determinant') + target=1 + for _ in range(d):target=poly_mul(target,3) + require(expected!=target,'determinant contradiction') + products+=1 + return {'formal_polynomial_products':products,'projection_determinants':factors,'nonzero_prefix_defects':defects} + +def static_witness(d,h,field_bits=1): + # Multiplication matrices embed F4 in Mat_2(F2), when field_bits is two. + require(field_bits in (1,2),'field') + q=1<>1)<<1),(a>>1)|(((a&1)^(a>>1))<<1)) + def fmap(axis,forward): + m=[0]*n + for leaf in range(1,g+1): + for bit in range(field_bits): + r,c=(axis*field_bits+bit,leaf*D+axis*field_bits+bit) + if not forward:r,c=c,r + m[r]|=1<>k&1:uv^=u<> (leaf*D)) & ((1<=2: + paired=[add(fs[0],es[0]),add(gs[1],es[0])] + paired += [add(fs[i],gs[(i+1)%d]) for i in range(1,d)] + check_queries(paired,2*d+2) + require(all(rank(z)==2*field_bits for z in paired),'rank-two pairing') + # The static conditions must reject actual damage. + controls=0 + for broken in (queries[:-1], [add(queries[0],eye(n))]+queries[1:]): + try:check_queries(broken,2*d+2*h) + except ValueError:controls+=1 + else:raise ValueError('damaged witness accepted') + return {'field_size':q,'d':d,'h':h,'leaves':g,'field_dimension':n//field_bits,'thin_rank':2*d+2*h,'rank_one_queries':len(queries),'rank_two_queries':None if paired is None else len(paired),'rejected_controls':controls} + +def main(): + source=ROOT/'vendor/PR5673-PROOF.md' + manifest=json.loads((ROOT/'SOURCES.json').read_text()) + pin=next(x for x in manifest['files'] if x['path'].endswith('vendor/PR5673-PROOF.md')) + require(hashlib.sha256(source.read_bytes()).hexdigest()==pin['sha256'],'source hash') + result={'status':'PASS_ONE_SIDED_AUDIT_AND_STATIC_SHARPNESS','split_census':split_census(),'prefix_audit':prefix_audit(),'mixed_coefficient_audit':coefficient_audit(),'static_witnesses':[static_witness(*args) for args in [(2,1),(3,1),(4,1),(2,2),(2,3),(2,1,2)]],'limits':['Written universal proof; no proof-assistant or human acceptance','Static witnesses are not chronological words','No native lift, complete physical invoice or new kappa']} + saved=ROOT/'RESULT.json' + if saved.exists():require(json.loads(saved.read_text())==result,'saved result mismatch') + print(json.dumps(result,indent=2,sort_keys=True)) + +if __name__=='__main__':main() From 3924192ea418c1c891b808ba2c4cb95cdfbca6fa Mon Sep 17 00:00:00 2001 From: Ali Romman <226877337+aliromman@users.noreply.github.com> Date: Mon, 26 Oct 2026 00:13:21 -0500 Subject: [PATCH 3/4] Mark the completed audit with the package outcome contract --- research/one-sided-connector-audit/TASK.json | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/research/one-sided-connector-audit/TASK.json b/research/one-sided-connector-audit/TASK.json index b45667621c..38e5a8f411 100644 --- a/research/one-sided-connector-audit/TASK.json +++ b/research/one-sided-connector-audit/TASK.json @@ -47,7 +47,7 @@ "bottleneck_link": "Check the exclusion used to select long P104 callers. Explicit rank-minimum maps prove that static rank/signature tests cannot reject the remaining targets.", "budget_minutes": 90, "stop_rule": "Finish the proof audit and static sharpness construction. Do not claim a complete star word or a native supplier.", - "outcome": "scoped theorem and independent audit", + "outcome": "completed", "evidence": "PROOF.md and RESULT.json; separate literal coefficient, matrix and enumeration checks.", "author": "Ali Romman with substantial OpenAI Codex assistance", "ai_assistance": "OpenAI Codex; no subagents. This is a separate implementation, not independent human review.", From 67f07448eec5ad8d84bdf96b46981ac0b893592f Mon Sep 17 00:00:00 2001 From: Ali Romman <226877337+aliromman@users.noreply.github.com> Date: Mon, 26 Oct 2026 00:14:13 -0500 Subject: [PATCH 4/4] Record independent replay and source corruption evidence --- .../one-sided-connector-audit/VALIDATION.md | 31 +++++++++++++++---- 1 file changed, 25 insertions(+), 6 deletions(-) diff --git a/research/one-sided-connector-audit/VALIDATION.md b/research/one-sided-connector-audit/VALIDATION.md index e64cefa048..2204e4fe45 100644 --- a/research/one-sided-connector-audit/VALIDATION.md +++ b/research/one-sided-connector-audit/VALIDATION.md @@ -1,9 +1,28 @@ # Verification record -The normal and optimized registered runs check the same saved RESULT.json. -The source proof is retained byte-for-byte and is checked by SHA-256 before -science checks. The checker uses Python 3.12 and the standard library. +The final normal and optimized registered runs passed with CPython3.12.14. +Both runs reproduce RESULT.json exactly. The science export at +3924192ea418c1c891b808ba2c4cb95cdfbca6fa passed the nine-file committed-byte +and archive checks. A read-only export passed optimized, isolated execution +with empty PATH and no Git directory. All ten exported files, including the +manifest, retained their hashes. An appended line in the retained source +proof caused rejection before the science checks. -Publication checks, export evidence and scope limits are recorded below after -execution. No formal-kernel proof, independent human review, complete caller, -native supplier, selected cold replay or hosted CI acceptance is claimed. +The separate checker imports no source code. The full matrix checks include +both proposed search targets, F4 and twelve damaged constructions. The +coefficient and determinant tests support the written proof. They do not +establish all-size correctness by enumeration. No mathematical gap was found +in the audited source implication under its stated hypotheses. + +The final documentation commit does not change these science bytes. A final +committed-byte check and export also pass. The canonical main was refreshed +before publication. The live overlap report covers all7676 tracked notes and +fully paginated remote records; unpublished work and arbitrary diffs remain +outside that check. The published source proof is retained exactly from +PR5673 head c10f75f09e41803ae8efe478331a7509b7379b2f. + +A full-history preflight was not run in this shallow checkout. The immediate +base and retained-source ancestry and exact bytes are checked. No formal +kernel, human review, complete chronological caller, native supplier, selected +cold replay, new tariff calculation or hosted-CI acceptance is claimed. +Prepared by Ali Romman with substantial OpenAI Codex assistance. Apache-2.0.