Skip to content

Attain the mixed-negative Q8 bound for t <= 2 - #3697

Merged
Mister-Meeseeks merged 1 commit into
CrocSwap:mainfrom
petalas:research/w4-b21-q8-tower-20261018
Oct 20, 2026
Merged

Mister-Meeseeks merged 1 commit into
CrocSwap:mainfrom
petalas:research/w4-b21-q8-tower-20261018

Conversation

@petalas

@petalas petalas commented Oct 18, 2026

Copy link
Copy Markdown
Contributor

Summary

Close PR3589's open sharpness question for mixed-negative Q8 endpoints, in the t <= 2 regime.

inherited PR3589 bound:   5n >= 11t,   inherited parity:  n = t mod 2

t = 1   (zi), (zj)        minimum 3    attained
t = 2   (zi,zi),(zi,zj),(zj,zj)   minimum 6    attained

The lower bound is inherited and role-free, so these minima are complete over all role counts and over any finite restored dirty workspace. The upper bound is an explicit word: a paid factor with u = v = e_a multiplies role a by its label g, and i^3 = zi, j^3 = zj, so three calls per target role realize the endpoint in 3t calls — which for t = 1, 2 lands exactly on the bound.

Two consequences, in the direction that narrows the question:

  • The uniform 11t/5 constant is attained at t = 1 and t = 2. No strictly stronger necessary function of t can hold at those points. This is PR3589's open question 2, answered affirmatively for t <= 2 only.
  • The bound is not attained by this witness family for t >= 3. t = 3 admits bound value 7 against a 9-call witness; balanced t = 4 admits 10 against 12. Those minima stay in {7,9} and {10,12} and are not decided here.

This is a mathematical side result for the nonabelian bit-register model. No new kappa, physical supplier, invoice, native conversion or selected-frontier change is claimed.

Evidence

  • Before: PR3589 gives a necessary region and explicitly states the factor 11/5 is not claimed sharp. After: the constant is shown attained at t = 1 and t = 2, so no improvement of n as a function of t is available there.
  • All 64 Q8 group products agree between a basis bit-arithmetic product and an independent signed-unit table, so the group law behind the witnesses is not assumed from the routine it tests. i^3 = zi, j^3 = zj, z^2 = 1 are checked directly.
  • Eight explicit witnesses are replayed to their exact diagonal endpoints; each witness's call count is compared against the independently computed parity-rounded bound.
  • Five complete breadth-first searches exhaust every legal word on 1 and 2 roles up to lengths 2 and 5 — 6 and 56,084 distinct states — and find none. These are a cross-check of the model and the witnesses; the theoretical bound is what supplies completeness at t <= 2.
  • Behavioural controls run under -O and must produce real rejections for a corrupted Q8 product law, a corrupted z involution, a bad paid label, a zero or out-of-range projector, even v^T u overlap, role capacity, an empty or unknown endpoint target, a truncated witness, a shrunk census limit, a corrupted parity bound, and a receipt round trip. No check uses assert.
  • Registered replay passes at the publication commit:
python3.12 -B scripts/research_package.py --package research/q8-min-length-census
python3.12 -B scripts/check_research_commit.py --package research/q8-min-length-census --check-source-history

giving PASS_REGISTERED_RESEARCH_PACKAGE and PASS_RESEARCH_COMMIT_BYTES (097d500ac). The package is standard-library only and replays without Git or network.

Search failure, recorded as such

A randomised hill-climbing search for a ten-call balanced four-target word was run over 4–6 roles (18 independent runs, best cost 6, no cost 0). A positive control at twelve calls reached only cost 8, so the search is known to be weak. Its failure is written into VALIDATION.md only to stop a later reader mistaking it for an exclusion. It excludes nothing.

Limits and unrun obligations

t >= 3 is not decided; complete enumeration at four or more roles exceeded this session's budget. Nothing here re-proves PR3589, and no physical scalar, routing, restoration, hosting, precision, recursive or supplier-admission cost is computed. Lean, Docker, the selected full cold replay, ruff (not installed in the authoring environment), independent human review and formal proof-kernel acceptance are unrun.

Credit

Nick Petalas/PR3589 for the mixed-negative boundary-rank bound and the parity, with PR3570 (mixed cubic identity), PR3578 (two-orientation boundary-rank method), PR3536 (sign-sensitive chronology) and PR3558 (cyclic subspace argument). Only the witnesses, the complete small-case census and the sharpness consequence are new here.

PR3589 proved the necessary bound 5n >= 11t for mixed-negative Q8
endpoints and left "is 11t/5 sharp?" open. This package closes that
question in the t <= 2 regime.

For every mixed-negative endpoint with t = 1 or t = 2 the minimum number
of paid rank-one calls is exactly the parity-rounded bound: 3 and 6. The
lower bound is inherited and role-free, so the minima are complete over
all role counts; the upper bound is an explicit word, because three calls
on one role multiply it by the cube of its label and i^3 = zi, j^3 = zj.

Consequences: the uniform constant is attained at t = 1 and t = 2, so no
strictly stronger necessary function of t can hold there. The bound is not
attained by this witness family for t >= 3: t = 3 stays in {7,9} and the
balanced t = 4 in {10,12}, both still undecided.

Evidence is five complete breadth-first receipts over 6 and 56084 distinct
states, eight witnesses replayed to their exact diagonal endpoints, the
Q8 product law checked against an independent signed-unit table, and
behavioural controls that must reject corrupted algebra, boundaries,
witnesses and limits. A randomised search for a ten-call balanced word is
recorded in VALIDATION.md as a search failure only; it excludes nothing.

No new kappa, physical supplier, invoice or frontier change is claimed.
@petalas
petalas force-pushed the research/w4-b21-q8-tower-20261018 branch from 097d500 to b5fa864 Compare October 18, 2026 17:33
@Mister-Meeseeks
Mister-Meeseeks merged commit eae5700 into CrocSwap:main Oct 20, 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