Skip to content

Review the staged544 fixed-frame new-gap reduction. - #4134

Merged
Mister-Meeseeks merged 1 commit into
CrocSwap:mainfrom
unpaidmoon:cursor/two-add-gap-review-337a
Oct 20, 2026
Merged

Mister-Meeseeks merged 1 commit into
CrocSwap:mainfrom
unpaidmoon:cursor/two-add-gap-review-337a

Conversation

@unpaidmoon

@unpaidmoon unpaidmoon commented Oct 20, 2026 •

Copy link
Copy Markdown
Contributor

Change and mathematical scope

Audit of the fixed-frame new-gap reduction in PR #3942. No new κ and no selected-frontier change. Selected κ stays 0.001672660197076918.

On both pinned PR #3734 providers, every scalar-legal third ADD at the swapped interior cut of a fixed-frame adjacent pair either matches a separately coded bridge formula or equals the original-word price at the cut named in that package's PROOF.md §3. The only nonzero bridge rows are the four published restore rows, and each passes the nonnegative curvature certificate. Every radius-one first-move interval has quotient rank at most 3, and an independent one-vector walk matches the Gaussian subspace counts.

This is not a replay of the 11.9-million-row variable-frame census and not a two-ADD impossibility theorem.

Task and overlap

Validation

CPython 3.12.3. Registered replay:

python3.12 -B scripts/research_package.py --package research/staged544-two-add-reduction-review

Passed locally as PASS_REGISTERED_RESEARCH_PACKAGE research/staged544-two-add-reduction-review outcome=negative-result.

verify.py also passed under python3 -I -B. Both providers report 4709 fixed pairs, 14966 bridge gates, 14693 bridge dimensions, quotient maximum 3, and the same four nonzero rows. A fast corridor test was checked against the explicit crossing walk on every restore pair and on the first 40 fixed pairs (166,691 comparisons). One published nonzero row matches apply_move plus a fresh trace.

Not run: the predecessor variable-frame census, Lean, Docker, and the selected cold replay.

Credit

Chris R / Clear1nsight for PR #3942 and the released review request. dataisfire for the PR #3734 providers. The PR #3886 single-move rules and the retiming line credited in that package are reused as the authenticated trace oracle, not re-authored. Prepared by unpaidmoon with substantial Cursor Grok assistance. No independent human or formal-kernel review is claimed. Apache-2.0.

Open next questions

  1. Does every disjoint-register second ADD have raw-moment delta equal to its original single-move delta? The crossing algebra is checked here; the summed histograms are not. Start from one changed-frame first word. Blocked by the size of the 11.9-million-row census.
  2. Does choosing the same ADD twice undo every radius-one first move? A failed undo would be a word the reduction never prices. Needs the variable first-move list.

Workflow feedback (optional)

The explicit numbered index in #1166 is smaller than the set of still-open prose handoffs. Keeping those handoffs in chronological order, and dropping a request only when its next task already has an open PR or a later DONE that answers that task, made the fourth remaining item the #3942 review rather than another retiming search. A machine-readable open-handoff list with that filter would let parallel sessions share one ordering.

Independently check PR CrocSwap#3942's interior-price localisation and
radius-one frame coverage on both pinned providers. No omitted
legal price, and the only nonzero bridge rows are the four published
losing restore rows. No new kappa.

Co-authored-by: unpaidmoon <unpaidmoon@users.noreply.github.com>
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.

3 participants