Prove three-term transport rigidity for an eight-call address-twist pattern

research/bit-three-term-twist-rigidity/PROOF.md

@@ -0,0 +1,125 @@
+# Three-contribution rigidity for two-sided address twists
+
+## Scoped result and inherited model
+
+Use the odd-denominator coefficient ring O=Z_(2), Gamma=M_m(O), m>=2,
+and R=F2[Gamma] from PR5003 (`bit-address-twist-second-order/PROOF.md`).
+There are exactly three arbitrary dirty registers. Paid calls are
+D_N(A)=I+([A]-1)N with rational rank-one A in Gamma, conjugated by an
+independent diagonal tuple tau_jr(B)=L_jr B R_jr, L_jr,R_jr in GL_m(O).
+The new **eight-call pattern** contains two independent J=uu^T calls,
+one P_s=u e_s^T for each s, and one D_s=e_s e_s^T for each s, u=(1,1,1)^T.
+All orders and all these twists/frames are allowed. No further mixing or
+registers are allowed. Twists are favorably free; this is not a native tariff.
+
+**Theorem.** If this word equals diag([C_0],[C_1],[C_2]) as an operator on
+(R/I^3)^3, where I is the augmentation ideal, then every C_s mod2 has matrix
+rank at most one. In particular it cannot realize three I_m targets, m>=2.
+The same conclusion holds if any listed frame is zero modulo two.
+
+This is a different first-order-feasible pattern from PR5003's one-J seven-call
+pattern. It is not a classification of arbitrary eight-call words, a universal
+nine-call bound, a supplier, a kappa improvement or independent formal acceptance.
+
+## 1. Rank distance of two-sided transports
+
+Let V=M_m(F2). For distinct linear maps U(B)=LBR and U'(B)=L'BR', with
+all four factors invertible, rank(U-U')>=m.
+
+Composing with U^-1 reduces the assertion to F(B)=B-XBY. If X is not scalar,
+there exists v such that v and Xv are independent. Indeed, if every nonzero
+vector were its own invariant line, over F2 invertibility would give Xv=v
+for every v. Choose a linear functional ell with ell(v)=1 and ell(Xv)=0.
+On the m-dimensional subspace B=v w^T, ell(F(B))=w^T, so F is injective
+there and rank(F)>=m. If X is scalar, it equals I; then F(B)=B(I-Y), whose
+rank as a map of matrix spaces is m rank(I-Y). Distinctness gives Y!=I,
+so this is at least m. This proof does not assume uniqueness of a factorization.
+
+## 2. Three-term quadratic rigidity
+
+Let a_1,a_2,a_3 in V, and let U_1,U_2,U_3 be two-sided invertible transports.
+Suppose
+
+    sum_i a_i=0,    sum_i a_i (U_i z)=0 in Sym^2(V), for all z in V.       (1)
+
+Polynomial squares are retained. Then the nonzero terms have a common U_i.
+Consequently, if b_i=U_i^-1 a_i, then sum_i b_i=0.
+
+If all a_i vanish the conclusion is immediate. Exactly one nonzero term is
+impossible. If exactly two are nonzero they coincide, and injectivity of
+multiplication by their nonzero linear polynomial forces their transports equal.
+If all three are nonzero, a_1 and a_2 are distinct, hence linearly independent
+over F2, and a_3=a_1+a_2. Equation (1) gives
+
+    a_1 ((U_1-U_3)z) + a_2 ((U_2-U_3)z)=0.                            (2)
+
+In the ordinary polynomial ring, the distinct linear factors a_1,a_2 are
+coprime. Thus the degree-one forms (U_1-U_3)z and (U_2-U_3)z are respectively
+lambda(z)a_2 and lambda(z)a_1. This holds also when either is zero; over F2
+the scalar lambda(z) is unique and linear in z. The two difference maps have
+rank at most one. Section1 and m>=2 force both differences to vanish.
+Then sum b_i=U_3^-1(sum a_i)=0. We use only homogeneous degree two, so the
+argument does not mistake the truncated algebra for an integral domain.
+
+The rank-distance premise matters: arbitrary invertible linear maps of V can
+differ by rank one. The verifier supplies an explicit such three-term solution
+with distinct maps. Therefore this lemma does not eliminate arbitrary linear
+address relabeling or four-or-more-term syzygies.
+
+## 3. Apply the lemma to the actual eight-call pattern
+
+The predecessor establishes R/I^3 = F2[t_1,...,t_(m^2)]/(degree>=3), with
+V=I/I^2 and degree2=Sym^2(V). This follows by reducing Gamma modulo4; odd
+denominators are invertible there. Its derivation and operator convention are
+retained, not replaced by Boolean or square-free polynomial semantics.
+
+For call j define a_jr=tau_jr(A_j) mod2 and let U_jrs be the induced map
+of tau_jr tau_js^-1 on V. Source compatibility gives
+
+    a_jr=U_jrs a_js.                                                 (3)
+
+A call increment raises augmentation degree at least one. For an off-diagonal
+block (r,s), constants give sum a_jr=0. Dirty degree-one input z gives
+sum a_jr(U_jrs z)=0 in degree2. Products of two increments have degree>=3
+on that input, so these necessary conditions are independent of chronology.
+In products, later calls act on the left. We do not discard cross terms on
+constant inputs; we simply do not need them for this necessary obstruction.
+
+Exactly three calls contribute to (r,s): J_1,J_2,P_s. Apply Section2 and (3):
+
+    a_J1,s+a_J2,s+a_Ps,s=0.                                          (4)
+
+The diagonal first-order equation is therefore c_s=a_Ds,s. Reduction mod2
+of a rank-one matrix over O has rank<=1, by vanishing of its 2x2 minors;
+invertible left/right twists preserve this. Hence rank(c_s)<=1 for each s.
+The proof includes all zero reductions and every call order. It does not need
+an exhaustive twist enumeration or an endpoint search.
+
+## 4. A genuinely new first-order-feasible fixture
+
+For m=3 take untwisted frames A_J1=E00 and A_J2=E01. For P_s use A=E00;
+choose its role-s transport to send E00 to d=(e0+e1)e1^T and its other two
+role transports to send E00 to b=e0(e0+e1)^T. Such maps are invertible
+left/right maps: at role s use L=I+E10 and R exchanging columns0,1; at
+other roles use L=I and R=I+E01. Take A_Ds=E22, untwisted. Then in every
+off-diagonal block E00+E01+b=0, while every diagonal increment is
+E00+E01+d+E22=I3. Every one of the eight frames is nonzero and rank one.
+This passes the constant-input first-order screen, yet the theorem excludes it.
+The two J terms have equal transport, while the P_s relative transport is
+different. For a basis z with z!=U_Ps,rs z the dirty residue is
+b(z+U_Ps,rs z), nonzero by polynomial injectivity. The independent sparse
+(Z/4) group-ring oracle checks this residue after the actual complete word.
+
+## Evidence and open boundary
+
+The quantified result is the written proof. The finite verifier checks all
+36 two-sided GL2(F2) maps, their pairwise rank distances, all nonzero
+three-form/transport solutions in a reduced complete local domain, the above
+m3 fixture, independent dirty group-ring calculations, and direct positive
+controls. It retains an arbitrary-GL(V) counterexample as a boundary control.
+No finite check substitutes for the all-m proof. Arbitrary other projectors,
+extra mixing/helpers, even denominators, and native pricing remain open.
+
+Credit PR5003 Krzysztof Wójt and PR4953 JoyboyBrian; Cinna Davis/PR2110
+and the Ali Romman, eumemic and huxint lineage. Prepared by JoyboyBrian with
+substantial OpenAI Codex assistance. Apache-2.0.

research/bit-three-term-twist-rigidity/README.md

@@ -0,0 +1,53 @@
+# Three-term rigidity closes a new eight-call twist pattern
+
+A new rank-distance/syzygy argument closes the first three-contribution
+escape named in [Discussion4999](https://github.com/CrocSwap/integer-mult-bounds/discussions/4999).
+Distinct PBQ transports on M_m(F2) differ in rank by at least m; three-term
+quadratic cancellation would force rank at most one. For m>=2 this makes
+all active relative transports equal. Source compatibility then excludes the
+specific eight-call pattern with two J calls, three P_s and three D_s under
+all orders and arbitrary odd-denominator rank-one frames and independent
+per-register PBQ conjugations. Every diagonal target has mod2 rank<=1.
+
+[PROOF.md](PROOF.md) is the quantified result. The package includes a genuinely
+first-order-feasible m3 eight-call fixture with all frames nonzero, a complete
+272,160-case normalized GL2 local check and 39 independent sparse finite
+group-ring word checks. Twelve representative orders corroborate the
+order-independent proof; they are not an exhaustive eight-call search.
+General GL(V) admits the explicit rank-one-difference control, so this is
+not a theorem for arbitrary linear twists, extra mixing, helpers or patterns.
+No native tariff, kappa improvement, supplier or full multiplication theorem.
+
+## Reproduce
+
+```sh
+python3.12 -I -W error -B research/bit-three-term-twist-rigidity/verify.py
+python3.12 -I -O -W error -B research/bit-three-term-twist-rigidity/verify.py
+python3.12 -B scripts/research_package.py --package research/bit-three-term-twist-rigidity
+```
+
+Expected `PASS_THREE_TERM_TWIST_RIGIDITY`; standard library only. The verifier
+imports no predecessor executable. Exact proof dependencies are in SOURCES.json
+and declared in VERIFY.json. Native/full-route/Lean checks are outside scope.
+The result is author-checked with AI assistance, not independent human or
+proof-kernel acceptance. See VALIDATION.md for performed checks.
+
+## Open next questions
+
+1. Find a different first-order-feasible pattern with at least four active
+   contributions and derive its dirty-input syzygies before attempting synthesis.
+   This result supplies no candidate or justification for an unchanged census.
+2. Price a legal native realization of the explicit general-GL(V) transvections
+   before treating their algebraic escape as a useful construction.
+
+Structured gates are in TASK.json. Original assignment and selected result
+are provenance only; selected frontier files are unchanged.
+
+## Credit
+
+JoyboyBrian, with substantial OpenAI Codex assistance; Apache-2.0. PR5003 by
+Krzysztof Wójt supplies the second-order quotient, source compatibility and
+seven-call obstruction; PR4953 supplies the two-sided model and first-order
+witness. Credit Cinna Davis/PR2110 and the Ali Romman, eumemic and huxint
+lineage. The new contribution is the uniform rank-distance/three-term lemma,
+its different eight-call pattern, and independent algebraic corroboration.

research/bit-three-term-twist-rigidity/SOURCES.json

@@ -0,0 +1,30 @@
+{
+  "schema_version": 1,
+  "base_commit": "32890bc5de034ab8fc93ac88ead7279a6a416d04",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "fc3d4ba105e1f097d0d7d051a308281e86ab1446",
+      "sha256": "66974efdced4083c00025f97d95d83909a226cdf801edb9301c195c6641f6903"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602",
+      "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72"
+    },
+    {
+      "path": "research/bit-address-twist-register-floor/PROOF.md",
+      "usage": "input",
+      "git_blob": "26cbb34d5a76866227b13dc0691a5e0bef169346",
+      "sha256": "c890d847b7dacc6c5434edfab30b2cf59dc69edf8830f75a6b30915ce4a2f003"
+    },
+    {
+      "path": "research/bit-address-twist-second-order/PROOF.md",
+      "usage": "input",
+      "git_blob": "e2d5cc54c28ac92a77a2fd8fb503e89cccccecaf",
+      "sha256": "d90ea3bbc06c95bfc5812306eb810b2e9d0682c05d576c8311797a8d0b614f43"
+    }
+  ]
+}

research/bit-three-term-twist-rigidity/TASK.json

@@ -0,0 +1,70 @@
+{
+  "schema_version": 1,
+  "task_id": "bit-new-register-model",
+  "priority_revision": 7,
+  "base_commit": "32890bc5de034ab8fc93ac88ead7279a6a416d04",
+  "original_card": {
+    "id": "bit-new-register-model",
+    "question": "Can an explicitly larger or nonabelian register model escape the scoped three-register obstruction?",
+    "starting_points": [
+      "docs/research/research-family-status.md",
+      "research/bit-three-register-lower-bound/README.md",
+      "certificates/selected-result.json",
+      "research/bit-gl3-mixed-targets-length10/README.md",
+      "docs/research/community-efficient1000-review.md"
+    ],
+    "methods": [
+      "Construct the smallest exact identity in a newly specified legal operation alphabet.",
+      "Derive a target-specific relaxation bound for that same explicit alphabet."
+    ],
+    "acceptance_gate": "Name the changed hypothesis, all counted roles and a uniform identity; finite column tests alone do not certify it. 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",
+        "scripts/research_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Read Model section 1 of the three-register bound and identify the exact excluded free operations.",
+      "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay."
+    },
+    "first_experiment": "First compare the alphabet, role count and length with the fully replayed #1974 census and #2027 mixed-root tariff. Identify a changed premise and a legal native implementation; then price one smallest completed instance before searching larger words.",
+    "bottleneck_link": "A small-width completed saving changes the bit primitive; a finite-address identity alone is insufficient.",
+    "allowed_variations": [
+      "Choose a fixed larger register count or a specified nonabelian operation family."
+    ],
+    "scope_change_triggers": [
+      "Remaining inside the already-excluded three-register abelian model.",
+      "Repeating the two-register GL3 census or a covered three-register length without changing a hypothesis; a formal group-algebra word without native conversion is a partial result."
+    ],
+    "overlap_terms": [
+      "three-register",
+      "nonabelian",
+      "group algebra"
+    ]
+  },
+  "scope_status": "refined",
+  "actual_scope": "Uniform three-contribution PBQ transport rigidity and the two-J/P_s/D_s eight-call pattern obstruction modulo I^3.",
+  "scope_change_reason": "Follow D4999 explicit three-contribution handoff using rank-distance and polynomial syzygies, not another fixed seven-call census.",
+  "bottleneck_link": "Scoped exclusion of a first-order-feasible two-sided-twist pattern; no native price or full register-model barrier.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop at rank-distance/source-compatibility failure; no unrestricted synthesis or large twist census.",
+  "outcome": "completed",
+  "evidence": "PROOF.md and verify.py: all-m proof; finite independent sparse group-ring corroboration.",
+  "author": "JoyboyBrian, with substantial OpenAI Codex assistance",
+  "ai_assistance": "OpenAI Codex assisted derivation, source analysis, implementation and writing.",
+  "open_questions": [
+    {
+      "question": "Can four or more off-diagonal contributions survive the dirty degree-one condition?",
+      "why_it_matters": "Three-contribution transport rigidity no longer directly applies to higher syzygies.",
+      "first_step": "Exhibit a different first-order-feasible projector pattern and compute its exact degree2 module syzygies before synthesis.",
+      "blocked_by": "No admissible pattern or native full-cost allowance supplied."
+    },
+    {
+      "question": "Which non-PBQ linear address actions admit a paid implementation?",
+      "why_it_matters": "The verifier gives a rank-one difference escape for general GL(V), outside this proof.",
+      "first_step": "Name one legal native map realizing the explicit transvections and price all movement, preparation and cleanup.",
+      "blocked_by": "Favorable free linear maps do not constitute native primitives."
+    }
+  ]
+}

research/bit-three-term-twist-rigidity/VALIDATION.md

@@ -0,0 +1,24 @@
+# Validation and limits
+
+Author checks on macOS, CPython3.12, standard library only. No heavy solver,
+Lean, Docker, complete multiplication replay or predecessor suite was run.
+
+- Registered normal and optimized independent replay passed. The final verifier
+  includes 272,160 complete normalized nonzero GL2 local cases, 1,621 zero-case
+  controls, all1,296 GL2 transport-pair ranks, 36 dirty obstructions over12
+  sampled orders and3 exact nine-call positive controls.
+- A separate sparse group-ring implementation applies the entire word before
+  projecting modulo I^3. No predecessor executable or precomputed oracle is imported.
+- Source metadata, committed-byte/source-history and explicit-input-ref export
+  are checked at the final commit; a read-only Git-free extracted copy is replayed.
+  Export success is a packaging check, not mathematical acceptance.
+- The all-m, all-order and arbitrary PBQ statement rests on PROOF.md. Finite
+  GL2 checks and m3 word fixtures are corroboration only.
+
+Initial metadata used an invalid outcome label; the validator rejected it and
+it was corrected to `completed` before the final registered replay. The label
+means the scoped task is complete, not that the full register model is solved.
+
+Remaining obligations: arbitrary other patterns, four-term syzygies, additional
+mixing/registers, even denominators, and paid native implementation are unproved.
+No selected result or recursive invoice is changed.

research/bit-three-term-twist-rigidity/VERIFY.json

@@ -0,0 +1,37 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/bit-address-twist-register-floor/PROOF.md",
+    "research/bit-address-twist-second-order/PROOF.md"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 30,
+      "checks": "Rank-distance census, complete normalized three-term local domain, first-order-feasible eight-call fixture, independent full sparse group oracle, positive and failure controls."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-O",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 30,
+      "checks": "Same mathematical controls with assertions disabled."
+    }
+  ]
+}