Skip to content

Prove weighted E8 query limits and low-redundancy obstructions - #4967

Merged
Mister-Meeseeks merged 1 commit into
CrocSwap:mainfrom
aliromman:codex/publish-fixed-e8-query-limits
Oct 23, 2026
Merged

Mister-Meeseeks merged 1 commit into
CrocSwap:mainfrom
aliromman:codex/publish-fixed-e8-query-limits

Conversation

@aliromman

Copy link
Copy Markdown
Contributor

This adds three scoped limits for scalar queries on fixed E8 matrices. They give a full weighted private-query optimum, a coefficient classification for nine specified totals, and a pairing-rank floor through eleven binary terms. These results rule out specific proposed cost reductions. They give no new supplier and no change to the complete kappa calculation.

The fields and charges differ:

Fixed input and model Proved result Proof
The retained 112-port Gram matrix over Q, R or C; any finite factorization; each query has a private binary source frame of rank 1 <= r_j <= 9 For every real 0 <= b <= 1, the minimum of sum_j r_j^(1-b) is 8*8^(1-b). Eight rank-eight coordinate gathers attain it. Full concave range
The canonical 120-port rational E8 scatter; nine totals assigned to its nine binary coordinate hyperplanes Each total is a nonzero scalar multiple of its canonical total a_i-t. Each has 64 nonzero coefficients, whose source labels span its full rank-eight hyperplane. All nine totals may change at once. Coordinate rigidity
The 120-line binary matrix K(q,r)=1+(q dot r)/2 mod 2; any outer-product factorization with at most eleven terms The sum of the rational ranks of the source-reader inner-product submatrices is at least 72. The binary factors may lie outside the rank-nine code. Ten terms, eleven terms

The private-cost review, E8 review, private source manifest, and E8 source pins give the dependency and verification boundaries. The three bounds are not a combined price.

The private-query result extends the historical weighted range 0 < b <= 1/32 to the whole concave range. Its new scalar step proves 7*9^a+2-8*8^a > 2/27 for 0 <= a <= 1, using five integer comparisons and a derivative argument. The submission includes the six required historical premises: code rank and support, permitted frame ranks, frame capacities, total private rank at least 64, exclusion of a rank-nine frame at total 64, and coordinate attainment. Redundant queries are allowed. At b=1, cost is the nonzero query count; at b>1, permitted enlargement to rank-nine frames gives a smaller bill. This is a cost-law boundary, not a physical construction.

The coordinate result prevents a frame reduction within the nine specified hyperplanes, even if every coefficient vector is redesigned. It does not classify other frame choices. The binary result extends the minimal nine-term obstruction to ten and eleven terms. Its algebraic pairing-rank objective becomes a physical drop-cost bound only under the separate copy-tree hypotheses of PR #446, Theorem C at its pinned source. Shared charges, dynamic delivery, changed fitting matrices, and twelve or more binary terms remain outside that result. No access, restoration, hosting, tape, or recursive-child invoice is supplied.

A small annex gives an alternative proof of the existing E8 hyperplane-complement floor. It supplies eight explicit thirteen-root certificates and a Schur-complement proof, with a standard-library replay that needs no SAT solver. This is not a new floor: it is the equal-normal case of PR #3045, Theorem 6 at its exact pin. The annex review checks all eight cases, 62,208 binary Schur assignments, eight positive controls and three rejection controls. The written chamber argument covers every real hyperplane; the fitting field is F2. No comparison of verification speed is claimed.

From the repository root, use Python 3.10 or later and the standard library. The two output directories must not exist:

python3 -B research/private-query-concave-range/verify.py --build /tmp/private-query-concave-replay
python3 -B research/e8-small-redundancy/verify.py
python3 -B research/e8-hyperplane-minrank/verify.py --build /tmp/e8-hyperplane-minrank-replay

The respective final lines are:

PASS_PRIVATE_QUERY_CONCAVE_RANGE_INPUTS 2/27 1735600
PASS_E8_SMALL_REDUNDANCY coordinate_rigidity=9 binary_terms<=11 pairing_floor=72 no_new_kappa
PASS_E8_HYPERPLANE_MINRANK 240 8 13

Fresh sequential runs passed under Python 3.14.7. The private replay receipt records all 43,435 rank-seven frames, 1,735,600 profiles of total rank at most 63, and 195,666 partitions of total 64; all 79,403 partitions containing a rank-nine frame are rejected. Separate review checked the two final profile contradictions and ran seven rejection controls, including false scalar comparisons in normal and optimized Python, source drift, altered roots, and duplicate labels. The historical sign and premise-omission controls also passed.

The E8 final replay reproduces all 511 nonzero binary codewords, eight E8 and seven E7 deletion cases, the exact coordinate-model map, and all 14,400 rational scatter entries. A separate 72-variable calculation reproduces ranks 71,72,72,72,72 over F107. Its independent controls reject five mutations, including a changed port order and coherently rehashed false evidence. The optimized-environment checks confirm that inherited Python flags cannot disable assertions in the child checkers. The deletion cases support a written Weyl-chamber coverage proof; finite replay alone does not prove that reduction. No Lean check, complete supplier replay, repository-wide build, or hosted CI pass is claimed.

The publication base is cef4b52f2a59009865bf8eabde1be3f159063703. Jacob Sussman's E8 certificate and framework supply the rational source model. The 112-port data came through @icekylinx's PR #531; the retained prototype is byte-identical to that pin. Rohan Arun's historical PR #462 supplies the bit-word root input; only its root lines are used. The copied notices retain the underlying contributor and AI credits.

The unweighted private floor is not claimed as new: @DreamingOfClouds' all-m decoder theorem already supplies an unweighted floor in its stated model. PR #620 and the tensor E8 floor provide earlier minimal-term results. The later one-coset theorem uses a scalar field of characteristic different from two and binary support prices. It subsumes an older numerical obstruction omitted here; it does not supply the binary-factor theorem or the stated coefficient classification.

Ali Romman directed this work. OpenAI Codex and separate research agents supplied substantial proof, implementation, audit, and packaging assistance. The independent reviews are agent reviews, not human reviews. New work is under Apache-2.0; inherited notices remain intact. The README files state the remaining questions and the precise interfaces that would need a different construction.

@Mister-Meeseeks
Mister-Meeseeks merged commit 9f789e8 into CrocSwap:main Oct 23, 2026
2 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants