From f8cee42b6aa2d650de8b359061a2660031506fe8 Mon Sep 17 00:00:00 2001 From: Ali Romman <226877337+aliromman@users.noreply.github.com> Date: Fri, 23 Oct 2026 13:06:10 -0500 Subject: [PATCH] Classify all first nonadditive P112 rank-59 diagonal completions --- research/p112-rank59-equality/README.md | 52 +++++++++ research/p112-rank59-equality/SOURCES.json | 18 +++ research/p112-rank59-equality/TASK.json | 78 +++++++++++++ research/p112-rank59-equality/VERIFY.json | 34 ++++++ research/p112-rank59-equality/verify.py | 123 +++++++++++++++++++++ 5 files changed, 305 insertions(+) create mode 100644 research/p112-rank59-equality/README.md create mode 100644 research/p112-rank59-equality/SOURCES.json create mode 100644 research/p112-rank59-equality/TASK.json create mode 100644 research/p112-rank59-equality/VERIFY.json create mode 100644 research/p112-rank59-equality/verify.py diff --git a/research/p112-rank59-equality/README.md b/research/p112-rank59-equality/README.md new file mode 100644 index 0000000000..0a981142cb --- /dev/null +++ b/research/p112-rank59-equality/README.md @@ -0,0 +1,52 @@ +# Classify all first nonadditive P112 rank-59 diagonal completions + +This result classifies every first nonadditive rank-59 complex diagonal completion of the doubled P112 Gram matrix. It answers Open next question 1 of the cited boundary proof and the released [Discussion #5336](https://github.com/CrocSwap/integer-mult-bounds/discussions/5336). There are exactly 112 supports, in one orbit under the specified frame-preserving E8 symmetry group. Each support has a complete coefficient equation. This is an algebraic diagonal-mask result; the complete kappa calculation is unchanged. + +**Model and retained premises.** Let X have the 112 doubled root-line representatives specified by the source, with squared row norm eight. Remove the eight lines 2e_(2j)+/-2e_(2j+1), j=0,1,2,3, from the 120 E8 root lines. Put G=XX^T. Corrections Delta are arbitrary complex diagonal matrices, with nonzero support S. All transposes are ordinary, not conjugate transposes. We retain the source's proved rank stratification and its explicitly inherited root-code distance and root-spanned-hyperplane premises. In particular, writing r=rank X_(S-complement), r=8 gives rank(G+Delta)=8+|S|; r=7 gives rank at least |S|+6 and |S|>=53; r<=6 gives rank at least62. The geometric premises are not independently accepted by this package. + +**Complete equality class.** Every rank-59 completion is one of the following: + +1. The additive case: |S|=51. Every nonzero choice of the 51 diagonal entries has rank59. +2. The nonadditive case: choose a live root line alpha in P112, set c=X alpha and S={i:c_i!=0}. Then |S|=53, and the nonzero complex coefficients must satisfy + + 1 + sum_(i in S) c_i^2/(8 delta_i) = 0. (1) + +There are no other cases. Choose the doubled representative alpha so alpha^T alpha=8. If i_alpha is its own row, then c_(i_alpha)^2=64 and the other52 nonzero squares are16. Thus (1) is equivalently + + 8/delta_(i_alpha) + 2 sum_(i in S, i!=i_alpha) 1/delta_i = -1. (2) + +This gives a parameterization by nonzero complex t_i with sum t_i=-1: set delta_i=c_i^2/(8t_i). In particular it includes nonreal coefficients. The common value -112 is the predecessor witness, not a new witness claim. For the G/2 convention, divide every delta_i by two. + +**Proof of support completeness.** The retained stratification forces r=7 and |S|=53 in the nonadditive case. Thus the 59 unchanged rows span a real root-spanned hyperplane. The inherited classification says that a root-spanned hyperplane with more than42 E8 root lines is E7, with63 lines and a root normal alpha. An excluded root normal is orthogonal to seven of the eight removed lines: six from the other three coordinate pairs and its partner in the same pair. A live two-coordinate root uses two distinct pairs and is orthogonal to the four removed lines on the other two pairs. A half-integral root in doubled coordinates has all coordinates +/-1; in each pair it is orthogonal to exactly one removed line, again four in total. Hence an excluded normal leaves56 live zero rows, whereas each live normal leaves59. Only the112 live normals give the required support. + +Each of these59-row zero sets has rank seven. This follows from the source's rank-six bound42, or from the independent eight-column elimination in the checker. Distinct root normals therefore give distinct supports. No minimum-codeword support is omitted: every eligible59-row set equals all live root lines of its E7 hyperplane. + +**Proof of the coefficient equation.** Pivot on seven independent unchanged rows. Projection off their real span leaves the line of alpha, so the Schur block on S is + + diag(delta_i) + c_S c_S^T/8. + +The diagonal is invertible. A rank-one update of an invertible |S|-square matrix has nullity at most one. It has nullity one exactly when (1) holds, by direct multiplication of the candidate kernel vector diag(delta)^-1 c_S, or by the determinant lemma. Thus rank59 is equivalent to (1); otherwise the rank is60. This argument is valid for all nonzero complex coefficients and does not replace squares by absolute squares. + +**The stated symmetry and its equivalence relation.** The group here consists of orthogonal E8 root-set symmetries that preserve the removed eight-line frame as a set. It is not an unspecified larger equivalence on matrices. Write the removed doubled roots as a_0,...,a_7 in pair order, plus then minus, and use coordinates y_j=(v dot a_j)/4. The removed roots become the lines of 2e_j. Each live root has four entries +/-1, and its support is an affine plane in F2^3 when j is labelled by its three binary digits. There are14 such planes and eight sign choices modulo overall sign on each plane, giving112 live lines. In the original coordinates the plane list consists of six unions of two coordinate pairs and eight choices of one coordinate from each pair with even parity. These are exactly the14 affine planes. + +Every independent coordinate sign change preserves this root set. Every affine permutation j -> Aj+b, A in GL3(F2), also preserves it. Conversely a frame-preserving orthogonal map is a signed permutation, and its permutation must preserve these planes. After a translation fixes zero, preservation of {0,a,b,a+b} forces additivity; hence it is in GL3(F2). The group is therefore the signed permutation group 2^8 semidirect AGL3(2), of order344064. Its central overall sign acts trivially on root lines. + +AGL3(2) is transitive on affine planes, and coordinate signs are transitive on the eight root lines on each plane. All112 normal lines and all112 supports are consequently in one orbit. To compare two coefficient choices, apply the induced permutation of live root lines to their supports and diagonal values. They are equivalent under this group exactly when one of these finitely many actions matches every coefficient. After fixing one normal alpha, take the quotient of (1) by its line stabilizer. This is a complete parameter space with an explicit finite equivalence test; no canonical ordering of arbitrary complex numbers or computation of an invariant ring is asserted. Row sign changes from the choice of root representatives leave diagonal values unchanged. + +**Evidence and limits.** The checker independently generates all120 root normals, finds112 distinct equality supports and checks all their unchanged-row ranks. It verifies the affine-plane model, all1344 affine permutations and18816 plane actions, plus eight independent sign generators. Literal rational elimination of two112-row matrices distinguishes the predecessor nonadditive witness from an additive51-support rank59 completion. Six literal53-row Gaussian-rational Schur eliminations check three coefficient solutions, including a nonreal solution, and their three one-entry failures. These checks corroborate the written classification; they do not audit the inherited global root-flat premises. No physical decoder, diagonal repair bill, COPY optimum, odd-only-mask claim or supplier admission follows. + +Credit Nick Petalas's [PR #5249](https://github.com/CrocSwap/integer-mult-bounds/pull/5249) supplies the exact model, rank stratification, rank-59 witness and equality question in its [pinned proof](https://github.com/CrocSwap/integer-mult-bounds/blob/1c8bf3f3dadd1f6fd14892630eb76e984a74738a/research/p112-diagonal-rank-boundary/README.md). It retains Arham-Tahir64's [PR #1313](https://github.com/CrocSwap/integer-mult-bounds/pull/1313) diagonal-mask question and pivot method, woklerx's [PR #1447](https://github.com/CrocSwap/integer-mult-bounds/pull/1447) code-distance premise, and themilkman216's [PR #968](https://github.com/CrocSwap/integer-mult-bounds/pull/968) root-flat classification. DreamingOfClouds and the retained E8/Hamming lineage keep their geometric credit. Rank-one determinant identities and the affine-plane model are classical. The new result is the complete first nonadditive coefficient/support class and its specified symmetry quotient. + +Prepared by Ali Romman with substantial OpenAI Codex assistance; Apache-2.0. + +## Reproduce + +```sh +python3 -B scripts/research_package.py --package research/p112-rank59-equality +``` + +Use Python 3.12 with the standard library. The normal and optimized commands must print `PASS_P112_RANK59_CLASSIFICATION`. The launcher must print `PASS_REGISTERED_RESEARCH_PACKAGE`. The checker has no external runtime inputs. + +## Open next questions + +Test a specified diagonal-repair consumer and charge its full decoder bill before using this algebraic rank reduction. The source binding and physical cost model are not supplied by this package. See `TASK.json` for the structured scope. diff --git a/research/p112-rank59-equality/SOURCES.json b/research/p112-rank59-equality/SOURCES.json new file mode 100644 index 0000000000..277ad46954 --- /dev/null +++ b/research/p112-rank59-equality/SOURCES.json @@ -0,0 +1,18 @@ +{ + "schema_version": 1, + "base_commit": "ff3cc58e370d0f678e529246f8c73e8094e18fcf", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395", + "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + } + ] +} diff --git a/research/p112-rank59-equality/TASK.json b/research/p112-rank59-equality/TASK.json new file mode 100644 index 0000000000..2fd11fd564 --- /dev/null +++ b/research/p112-rank59-equality/TASK.json @@ -0,0 +1,78 @@ +{ + "schema_version": 1, + "task_id": "complex-rank-shape-decoder", + "priority_revision": 7, + "base_commit": "ff3cc58e370d0f678e529246f8c73e8094e18fcf", + "original_card": { + "id": "complex-rank-shape-decoder", + "question": "Can a decoder deliver the local paid mass in fewer, larger-rank children (block frame climbs instead of rank-1 to rank-3 steps)?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/complex-local-word-ceiling/README.md", + "research/complex-decoder-field-extension-seed44/README.md", + "research/complex-frame-pair-decoders/README.md", + "research/selected-k8-unrestricted-ends/README.md", + "research/eisenstein-reduction-copy-floor/README.md" + ], + "methods": [ + "Find one exact small decoding identity whose frame path climbs in blocks, and price its complete per-call profile.", + "Bound the best effective child rank achievable for one fixed support alphabet, including copies, frames and restoration." + ], + "acceptance_gate": "A per-call local profile, with all copied information, frames and restoration counted, whose ceiling exceeds the selected word's by at least 5%; masked or overcomplete supports must change an assumption of the eight-term all-pairs bound. 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/complex-local-word-ceiling/verify.py" + ], + "expected": "PASS_COMPLEX_LOCAL_WORD_CEILING", + "inspect": "Read the selected word's per-call local profile, its packing ceiling and the lever table; run levers.py for the ideal budget of the lever you target.", + "scope": "Positive control and planning budget only; this is not a new construction or full cold replay." + }, + "first_experiment": "Before any synthesis, write the candidate per-call local profile (and centre charge / unpaid coordinates if changed) and screen it with ceiling.ceiling(); reject it if even the ideal ceiling does not beat the selected word's by your stated margin. Ideal budget: rank-16 delivery is 2.31x (levers.py).", + "bottleneck_link": "Rank-1 children are about half of recursive cost; the selected word's effective child rank is about 3.9. Larger-rank delivery lowers recursive cost per unit of paid mass.", + "allowed_variations": [ + "One masked, overcomplete or block decoder family with exact labels and supports.", + "A scoped lower bound on effective rank for one alphabet.", + "If the coverage law, template or guard changes, derive an applicable fully charged replacement bound instead of applying the incumbent ceiling outside its scope." + ], + "scope_change_triggers": [ + "Repacking idle remainders of an unchanged word (covered by the packing ceiling).", + "Repeating the eight-term all-pairs search inside its proved scope.", + "Only changing helper terminal subspaces and monotone frames within the fixed scalar word, entrances and cleanup contract already covered by #1995/#2013.", + "Searching below C=40 in the #2017 Eisenstein binary scalar-rectangle or fixed-support block-linear additive pairing model; specify a changed premise instead. This bound does not cover every complex decoder.", + "Continuing a partial cost improvement while leaving the same unpriced consumer, restoration or central-readout obligation unresolved; refresh the family expansion decision first. Local product-retiming evidence has a narrow scope and is not a ban on changed graphs or contracts." + ], + "overlap_terms": [ + "rank shape", + "block climb", + "masked decoder", + "overcomplete", + "effective rank" + ] + }, + "scope_status": "changed", + "actual_scope": "This scoped classification gives every nonadditive rank-59 complex diagonal completion of the doubled P112 Gram matrix. Exactly 112 supports form one orbit under the stated frame-preserving E8 group; one explicit reciprocal-coefficient equation is necessary and sufficient on each support. The inherited root-flat premises remain explicit.", + "scope_change_reason": "This is a scoped interface theorem. It does not complete the original supplier or uniform-transfer task.", + "bottleneck_link": "Test a specified diagonal-repair consumer and charge its full decoder bill before using this algebraic rank reduction.", + "budget_minutes": 60, + "stop_rule": "Stop after the scoped proof, exact controls and bounded registered replay; do not expand to physical lowering.", + "outcome": "completed", + "evidence": "120 root normals, 112 equality supports, 1,344 affine maps, 18,816 plane actions, two literal 112-row ranks and six 53-row Gaussian-rational rank checks", + "author": "Ali Romman", + "ai_assistance": "Substantial OpenAI Codex assistance; no independent human or proof-kernel acceptance is claimed.", + "open_questions": [ + { + "question": "Test a specified diagonal-repair consumer and charge its full decoder bill before using this algebraic rank reduction.", + "why_it_matters": "The abstract result needs an actual caller and a complete cost model.", + "first_step": "Test a specified diagonal-repair consumer and charge its full decoder bill before using this algebraic rank reduction.", + "blocked_by": "No production caller or physical cost model is supplied." + } + ], + "upstream_checkpoint": { + "commit": "ff3cc58e370d0f678e529246f8c73e8094e18fcf", + "priority_revision": 7, + "checked_at": "2026-10-23T18:06:00.792346+00:00" + }, + "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19151619" +} diff --git a/research/p112-rank59-equality/VERIFY.json b/research/p112-rank59-equality/VERIFY.json new file mode 100644 index 0000000000..7531483b55 --- /dev/null +++ b/research/p112-rank59-equality/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "120 root normals, 112 equality supports, 1,344 affine maps, 18,816 plane actions, two literal 112-row ranks and six 53-row Gaussian-rational rank checks" + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "120 root normals, 112 equality supports, 1,344 affine maps, 18,816 plane actions, two literal 112-row ranks and six 53-row Gaussian-rational rank checks" + } + ] +} diff --git a/research/p112-rank59-equality/verify.py b/research/p112-rank59-equality/verify.py new file mode 100644 index 0000000000..c39e92ddad --- /dev/null +++ b/research/p112-rank59-equality/verify.py @@ -0,0 +1,123 @@ +"""Exact P112 support, symmetry and coefficient classification checks. + +Prepared by Ali Romman with substantial OpenAI Codex assistance. Apache-2.0. +""" +from fractions import Fraction as F +from itertools import combinations, product + + +def need(ok,message): + if not ok:raise ValueError(message) + + +def canon(v): + v=tuple(v) + return v if next(x for x in v if x)>0 else tuple(-x for x in v) + + +def dot(a,b):return sum(x*y for x,y in zip(a,b)) + + +def rank(a): + a=[[F(x) for x in r] for r in a]; k=0 + for j in range(len(a[0]) if a else 0): + pivot=next((i for i in range(k,len(a)) if a[i][j]),None) + if pivot is None:continue + a[k],a[pivot]=a[pivot],a[k];t=a[k][j] + a[k]=[x/t for x in a[k]] + for i in range(k+1,len(a)): + if a[i][j]: + t=a[i][j];a[i]=[x-t*y for x,y in zip(a[i],a[k])] + k+=1 + return k + + +def roots(): + rows=set() + for i,j in combinations(range(8),2): + for s in (-1,1): + v=[0]*8;v[i]=2;v[j]=2*s;rows.add(tuple(v)) + for v in product((-1,1),repeat=8): + if sum(x<0 for x in v)%2==0:rows.add(canon(v)) + removed=[] + for j in range(4): + for sign in (1,-1): + v=[0]*8;v[2*j]=2;v[2*j+1]=2*sign;removed.append(tuple(v)) + return sorted(rows),removed,sorted(rows-set(removed)) + + +def plus(a,b):return (a[0]+b[0],a[1]+b[1]) +def times(a,b):return (a[0]*b[0]-a[1]*b[1],a[0]*b[1]+a[1]*b[0]) +def inv(a): + d=a[0]**2+a[1]**2;need(d!=0,'nonzero coefficient');return (a[0]/d,-a[1]/d) +def neg(a):return (-a[0],-a[1]) +def cplx(x):return (F(x),F(0)) + + +def crank(a): + a=[r[:] for r in a];k=0;zero=cplx(0) + for j in range(len(a[0])): + pivot=next((i for i in range(k,len(a)) if a[i][j]!=zero),None) + if pivot is None:continue + a[k],a[pivot]=a[pivot],a[k];t=inv(a[k][j]);a[k]=[times(x,t) for x in a[k]] + for i in range(k+1,len(a)): + if a[i][j]!=zero: + t=a[i][j];a[i]=[plus(x,neg(times(t,y))) for x,y in zip(a[i],a[k])] + k+=1 + return k + + +def main(): + allrows,removed,x=roots();need((len(allrows),len(removed),len(x))==(120,8,112),'root inventory') + need(all(dot(a,a)==8 for a in allrows),'doubled norm') + supports={};normal_counts={} + for alpha in allrows: + c=[dot(v,alpha) for v in x];s=tuple(i for i,a in enumerate(c) if a) + normal_counts[len(s)]=normal_counts.get(len(s),0)+1 + if len(s)==53: + need(alpha in x and rank([x[i] for i in range(112) if i not in s])==7,'all equality supports') + need(s not in supports,'distinct supports') + need(sorted(c[i]**2 for i in s)==[16]*52+[64],'coefficient weights') + supports[s]=alpha + need(normal_counts=={53:112,56:8},'all root normals') + y={canon(tuple(dot(v,a)//4 for a in removed)) for v in x} + need(all(all(dot(v,a)%4==0 for a in removed) for v in x),'frame coordinates integral') + planes={frozenset(i for i,z in enumerate(v) if z) for v in y} + expected={frozenset(s) for s in combinations(range(8),4) if s[0]^s[1]^s[2]^s[3]==0} + need(planes==expected and len(planes)==14,'affine plane supports') + aff=[] + for a,b,c in product(range(1,8),repeat=3): + vals=[(a if j&1 else 0)^(b if j&2 else 0)^(c if j&4 else 0) for j in range(8)] + if len(set(vals))==8: + for shift in range(8):aff.append(tuple(v^shift for v in vals)) + need(len(set(aff))==1344,'full affine group') + first=next(iter(planes));orbit={frozenset(p[i] for i in first) for p in aff} + need(orbit==planes,'support transitivity') + actions=0 + for p in aff: + for plane in planes: + need(frozenset(p[i] for i in plane) in planes,'plane action');actions+=1 + # Every independent frame sign flip preserves the literal root lines. + for i in range(8): + need({canon(tuple(-z if j==i else z for j,z in enumerate(v))) for v in y}==y,'sign symmetry') + # Independent literal full-matrix check of the predecessor witness. + alpha=(1,)*8;c=[dot(v,alpha) for v in x];s=[i for i,a in enumerate(c) if a] + g=[[dot(a,b) for b in x] for a in x] + witness=[[g[i][j]-(112 if i==j and i in s else 0) for j in range(112)] for i in range(112)] + need(rank(witness)==59,'literal 112-row rank') + need(rank([[g[i][j]-(112 if i==j and i in s[:51] else 0) for j in range(112)] for i in range(112)])==59,'additive rank59 is separate') + cv=[c[i] for i in s];weights=[F(z*z,8) for z in cv] + cases=0 + for eps in (cplx(0),(F(1,7),F(0)),(F(0),F(1,7))): + terms=[cplx(-a/112) for a in weights] + terms[0]=plus(terms[0],eps);terms[1]=plus(terms[1],neg(eps)) + delta=[times(cplx(a),inv(t)) for a,t in zip(weights,terms)] + mat=[[plus(cplx(F(a*b,8)),delta[i] if i==j else cplx(0)) for j,b in enumerate(cv)] for i,a in enumerate(cv)] + need(crank(mat)==52,'arbitrary coefficient equality rank') + mat[0][0]=plus(mat[0][0],cplx(1)) + need(crank(mat)==53,'wrong coefficient restores full Schur rank') + cases+=1 + need(len(s)==53 and len(s[:51])==51,'support distinction') + print('PASS_P112_RANK59_CLASSIFICATION',dict(root_normals=120,equality_supports=112,affine_maps=1344,plane_actions=actions,literal_full_ranks=2,coefficient_pairs=cases,sign_generators=8,controls=5)) + +if __name__=='__main__':main()