diff --git a/research/bit-three-term-twist-rigidity/PROOF.md b/research/bit-three-term-twist-rigidity/PROOF.md new file mode 100644 index 0000000000..65120d64fb --- /dev/null +++ b/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. diff --git a/research/bit-three-term-twist-rigidity/README.md b/research/bit-three-term-twist-rigidity/README.md new file mode 100644 index 0000000000..65f924dda7 --- /dev/null +++ b/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. diff --git a/research/bit-three-term-twist-rigidity/SOURCES.json b/research/bit-three-term-twist-rigidity/SOURCES.json new file mode 100644 index 0000000000..b9f92b2231 --- /dev/null +++ b/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" + } + ] +} diff --git a/research/bit-three-term-twist-rigidity/TASK.json b/research/bit-three-term-twist-rigidity/TASK.json new file mode 100644 index 0000000000..488658fffa --- /dev/null +++ b/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." + } + ] +} diff --git a/research/bit-three-term-twist-rigidity/VALIDATION.md b/research/bit-three-term-twist-rigidity/VALIDATION.md new file mode 100644 index 0000000000..a761e61c97 --- /dev/null +++ b/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. diff --git a/research/bit-three-term-twist-rigidity/VERIFY.json b/research/bit-three-term-twist-rigidity/VERIFY.json new file mode 100644 index 0000000000..fbf34bdcbb --- /dev/null +++ b/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." + } + ] +} diff --git a/research/bit-three-term-twist-rigidity/verify.py b/research/bit-three-term-twist-rigidity/verify.py new file mode 100644 index 0000000000..0dfa71e8f9 --- /dev/null +++ b/research/bit-three-term-twist-rigidity/verify.py @@ -0,0 +1,271 @@ +#!/usr/bin/env python3 +"""Independent exact finite corroboration; no predecessor executable imports. +JoyboyBrian, substantial OpenAI Codex assistance; Apache-2.0. +""" +from itertools import product, combinations_with_replacement +import json +import random + + +def need(x, why): + if not x: + raise ValueError(why) + + +def bits(x): + while x: + t = x & -x + yield t.bit_length()-1 + x ^= t + + +def rank(cols): + pivots = {} + for x in cols: + while x: + k = x.bit_length()-1 + if k not in pivots: + pivots[k] = x + break + x ^= pivots[k] + return len(pivots) + + +def lin(cols, x): + y = 0 + for i in bits(x): + y ^= cols[i] + return y + + +def matmul(a, b, m, modulus=2): + return tuple(sum(a[r*m+k]*b[k*m+c] for k in range(m)) % modulus + for r in range(m) for c in range(m)) + + +def eye(m): + return tuple(int(r == c) for r in range(m) for c in range(m)) + + +def unit(d, k): + return tuple(int(i == k) for i in range(d)) + + +def inv(a, m): + rows = [list(a[r*m:(r+1)*m])+list(eye(m)[r*m:(r+1)*m]) for r in range(m)] + for c in range(m): + p = next((r for r in range(c, m) if rows[r][c] % 2), None) + need(p is not None, 'invertible mod4') + rows[c], rows[p] = rows[p], rows[c] + v = pow(rows[c][c], -1, 4) + rows[c] = [v*x % 4 for x in rows[c]] + for r in range(m): + if r != c: + v = rows[r][c] + rows[r] = [(x-v*y) % 4 for x,y in zip(rows[r], rows[c])] + return tuple(x for row in rows for x in row[m:]) + + +def transform(pair, a, m, modulus=4): + return matmul(matmul(pair[0], a, m, modulus), pair[1], m, modulus) + + +def maps(m): + gl = [a for a in product(range(2), repeat=m*m) + if rank([sum(a[r*m+c]<=2,'rank distance') + # Normalize U3 to identity by changing the input z. The class is a group. + solutions=checks=0 + for a,b in product(range(1,16),repeat=2): + if a==b:continue + forms=(a,b,a^b) + for u,v in product(us,repeat=2): + checks+=1 + if relation(forms,(u,v,ident),4): + solutions+=1 + need(u==v==ident,'three-term rigidity') + need(solutions==210,'all and only common transports') + zero_cases=0 + for a in range(1,16): + for u in us: + for zero_slot in range(3): + forms=[a,a,a];transports=[u,ident,ident] + forms[zero_slot]=0 + active=[i for i in range(3) if i!=zero_slot] + transports[active[0]]=u;transports[active[1]]=ident + need(relation(forms,transports,4)==(u==ident), 'two active terms') + zero_cases+=1 + need(relation((0,0,0),(us[0],us[1],us[2]),4), 'all zero reductions') + # The rank-distance hypothesis is essential: arbitrary GL(V) admits rank1 gaps. + u=list(ident);u[2]^=2 + v=list(ident);v[2]^=1 + need(rank(u)==rank(v)==4 and relation((1,2,3),(u,v,ident),4), 'general GL counterexample') + need(tuple(u)!=ident and rank([a^b for a,b in zip(u,ident)])==1,'rank1 escape') + specs=witness();expected=[[0]*3 for _ in range(3)] + for s in range(3):expected[s][s]=273 # E00+E11+E22 + need(first(specs,3)==expected,'eight nonzero calls pass first order') + rng=random.Random(19173175);orders=[list(range(8)),list(reversed(range(8)))] + for _ in range(10): + order=list(range(8));rng.shuffle(order);orders.append(order) + oracle_cases=0;obstructions=0 + for order in orders: + for source,k in [(0,0),(1,1),(2,3)]: + state=[set(),set(),set()];state[source]={unit(9,k),(0,)*9} + for j in order:state=call(state,specs[j],3) + got=[project_group(s,9) for s in state] + need(got==dirty_formula(specs,3,source,k),'sparse group vs independent dirty jet') + need(any(got[r] for r in range(3) if r!=source),'dirty obstruction') + obstructions+=1;oracle_cases+=1 + # Direct nine-call positive control, full sparse operator on independent dirty inputs. + standard=[(eye(3),eye(3))]*3 + direct=[(unit(3,s),unit(3,s),unit(9,4*k),standard) for s in range(3) for k in range(3)] + for source in range(3): + state=[set(),set(),set()];state[source]={unit(9,1),(0,)*9} + for spec in direct:state=call(state,spec,3) + target=tuple(eye(3));expected_state=[set(),set(),set()] + expected_state[source]={target,tuple((a+b)%4 for a,b in zip(target,unit(9,1)))} + need(state==expected_state,'nine-call exact positive');oracle_cases+=1 + # Squaring cannot be discarded; [2E]-1 projects to t_E^2. + square=project_group({(2,)+(0,)*8,(0,)*9},9) + need(square==1 << monomials(9).index((0,0)),'squares retained') + # Explicit falsification controls do not use assert (optimization safe). + controls=0 + for good,why in [(solutions==211,'wrong solution count'), + (first(specs,3)!=expected,'wrong first order'), + (square==0,'square-free quotient'), + (all(r>=3 for r in distances if r),'false rank3 floor')]: + try:need(good,why) + except ValueError:controls+=1 + else:raise ValueError('control did not reject: '+why) + need(controls==4,'controls complete') + return {'status':'PASS_THREE_TERM_TWIST_RIGIDITY','two_sided_maps_m2':36, + 'rank_distance_histogram':distances,'normalized_three_term_cases':checks, + 'normalized_solutions':solutions,'zero_reduction_cases':zero_cases+1,'full_sparse_oracle_cases':oracle_cases, + 'first_order_feasible_eight_call_obstructions':obstructions, + 'orders_sampled':len(orders),'rejection_controls':controls, + 'arbitrary_GL_counterexample':True,'quantified_result':'written proof; finite checks corroborate', + 'new_kappa':False} + +if __name__=='__main__': + print(json.dumps(main(),sort_keys=True,indent=2))