Attain the static connector rank bound and audit its obstruction

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<d.
+```
+
+Each has rank two. The two images and the two row directions are independent.
+All squares are zero. For the last group, the two indices differ, so both
+cross products vanish. The sum is still K. The union of images and row
+spaces still has dimension 2d+1: E is separate from the core/diagonal spaces,
+and each rank-two image and row space contains both rank-one directions.
+The first map detects the entire leaf column signature, and the second
+detects the entire row signature. Therefore all static bounds still pass.
+
+For F2,d=4,h=1 this gives **31 leaves and five rank-two maps**, with total
+thin rank ten. For F2,d=2,h=3, the ungrouped construction gives **127 leaves
+and ten rank-one maps**. These are exactly the two source search targets.
+Their static query maps now have an explicit formula. We do not replay or
+admit their source optimistic tariff, and we do not supply either word.
+A rejection of these targets must use an additional condition, such as the
+chronology equations or the complete polynomial endpoint.
+
+## 4. Verification boundary
+
+The separate checker imports no source code or certificates. It multiplies
+literal factors in the truncated polynomial ring and compares the extracted
+blocks in 72 words, with 55 noncommuting stage flags and 48 words that have
+external stages. It checks all 19,440 ordered three-stage rank-one flag words
+in dimension two over F2. Every word fails the prefix condition. A formal
+polynomial determinant computation is separate from that census.
+
+Six full static matrix fixtures include both target sizes and an F4 case.
+The F4 matrices use the exact regular representation from x^2+x+1; binary
+ranks are twice the stated F4 ranks. Each fixture checks every matrix entry,
+square, rank, sum and signature. Deleted queries and added identity maps are
+rejected. These finite checks support the written general proof; they do
+not replace it. No native lift, frame adapters, ownership/tape bill, complete
+caller or kappa improvement is established.
+
+Credit the retained PR5673 proof and its source lineage for the obstruction
+and rank bounds. The sharpness construction and separate audit code are new
+here. Ali Romman with substantial OpenAI Codex assistance. Apache-2.0.

research/one-sided-connector-audit/README.md

@@ -0,0 +1,61 @@
+# Sharp static connector bounds and an independent proof audit
+
+The one-sided obstruction in [PR5673](https://github.com/CrocSwap/integer-mult-bounds/pull/5673)
+passes a separate proof and coefficient audit under its stated full-stage,
+characteristic-two contract. The new construction proves that its rank and
+signature bounds are sharp at an unbounded family of sizes, even when every
+thin query has square zero. **No new kappa is claimed.**
+
+Over F_q, choose positive d,h and g=2q^(dh)-1 leaves. The explicit maps have
+required sum K, total thin rank 2d+2h, extra image/row dimensions h, and at
+most two leaves per signature. When h=1,d>=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).

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"
+}

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"
+    }
+  ]
+}