Skip to content

Record separate c=5 weight-2-family and all-ones-window centre counterexamples - #7058

Open
unpaidmoon wants to merge 2 commits into
CrocSwap:mainfrom
unpaidmoon:cursor/c5-mask-centre-nondetermination-704a
Open

unpaidmoon wants to merge 2 commits into
CrocSwap:mainfrom
unpaidmoon:cursor/c5-mask-centre-nondetermination-704a

Conversation

@unpaidmoon

@unpaidmoon unpaidmoon commented Nov 10, 2026 •

Copy link
Copy Markdown
Contributor

Change and mathematical scope

Two separate counterexamples. Not a depth-two exclusion and not a κ change. In the unchanged unsigned dirty connector:

  1. No individual all-ones window forces a legal centre. Every one of the 4095 admissible all-ones windows has a length-30 floor word with that window and an illegal S(16) = q_16 + q_17. 1731 of them also have a word with a legal centre. None forces a legal centre. Of the 2364 windows that force an illegal centre, 1573 do so because q_16 cannot contain a coordinate 0 (human classes 845 + 721 + 7). The other 791 admit a zero, but no feasible vector is a legal centre; that comparison is an exhaustive census.
  2. The fifteen weight-2 masks admit both polarities. The sorted floor word realizes all fifteen with illegal S(16). The word 001211112322203343354444555500 realizes all fifteen with legal S(16). Neither word realizes the weight-6 mask.

These two statements do not imply a statement about their conjunction. No conclusion is established about a floor word that realizes all fifteen weight-2 masks and the weight-6 mask together, including in the case where such a word exists. This package does not show that the conjunction forces a legal centre, and it does not show that the conjunction admits an illegal centre.

The weight identity is rechecked and is not that conjunction claim: no allowed 6-tuple of sum 33 has weight 2 or 6, so one pair with s + t = 33 cannot carry a weight-2 mask or the weight-6 mask.

Merged PR #6216 asserts that no floor word realizes all sixteen masks. This package does not replay that certificate and does not use the asserted empty fibre as a centre conclusion. Open PR #7038 still needs a legal centre that a word actually reaches before the centre-freeze can empty hypothesis (H). This note does not supply that derivation.

The selected conditional κ stays 781451/250000000. No selected-frontier file changes.

Evidence class: exhaustive finite census. The completeness argument is in the package README. This is not a SAT proof and not a heuristic search. The census counts are unchanged.

Task and overlap

Base: CrocSwap/integer-mult-bounds 17469fff78c22941280f04d39dc5a1faee09c840. This draft uses cursor/upstream-main-17469fff-b813 as its base because that branch is exactly that commit. The fork's main is an older snapshot, so it is not the review base.

Task card: connector-alphabet-change (priority revision 8). Scope status: changed. The card asks for one new connector operation. This package keeps the alphabet fixed and records two separate counterexamples toward open question 1 of PR #7038. It does not decide whether the sixteen masks together determine the sum-33 centre. A new operation is not the missing step.

Package: research/c5-mask-centre-nondetermination.

Overlap: scripts/find_overlap.py --offline at the base commit searched the local note inventory (10180 records, complete head inventory). It hits research/connector-six-source-small-char, which is the solver exclusion this note does not rerun. A GitHub search of open PRs hits PR #7038, whose centre-freeze theorem is the predecessor and is not re-proved. The adjacent-centre question, the c=6 and c=7 remainders, and the merged DRAT certificate in PR #6216 are different questions. Remote discussion and open-PR snapshots were not refreshed through find_overlap.py; the offline report says so.

Validation

Python 3.12, standard library only, from the repository root. Author-checked on 2026-11-10 after the scope-text correction:

python3.12 -I -W error -B research/c5-mask-centre-nondetermination/verify.py
python3.12 -I -O -W error -B research/c5-mask-centre-nondetermination/verify.py
python3.12 -B scripts/research_package.py --package research/c5-mask-centre-nondetermination --check-only
python3.12 -B scripts/research_package.py --package research/c5-mask-centre-nondetermination

Marker: PASS_C5_MASK_CENTRE_NONDETERMINATION assignments=4095 illegal_only=2364 both=1731 legal_only=0 no_zero=1573 zero_but_illegal=791 classes=845+721+7 constructed=5826 midpoint_q16=21 weight2_polarities=2 weight6_forces_legal=0 joint_weight2=13 joint_missing=2 controls=9

The marker token is the package id. legal_only=0 and weight6_forces_legal=0 are Result 1. weight2_polarities=2 is Result 2. joint_weight2=13 counts masks on one six-D window example and is not a conjunction-16 result.

The registered package replay passed in both command modes. scripts/check_research_commit.py --check-source-history was not run: this checkout is shallow (the preflight requires full history). The metadata pin check passed against the base-commit blobs that are present. No Lean, Docker, or historical suite was run.

Two witness words were first found by a local CaDiCaL search. The replay checks those literal words and does not call a solver.

Credit

The depth-two interface and the weight identity are Nick Petalas's (PR #4231, PR #4248, PR #6107), with the Ross Richardson PR #934 / PR #943 lineage. JosieElliston's PR #6141 is the solver exclusion. queelius's merged PR #6216 is the characteristic-5 DRAT certificate and is not replayed. The centre-freeze and hypothesis (H) are open PR #7038. The sorted word is the weight-two control of research/connector-six-source-small-char.

Prepared by unpaidmoon with substantial Cursor Grok assistance. Apache-2.0.

Open next questions

  1. For a floor word that realizes all fifteen weight-2 masks and the weight-6 mask together, what is the status of S(16)? Result 1 and Result 2 do not apply to that word. This package does not take the next step of treating that conjunction as its own hypothesis. No joint word is constructed or excluded here, and the PR Certify PR6141 characteristic-five connector exclusion (independent verification; no κ) #6216 empty-fibre assertion is not an input to this census.

Workflow feedback (optional)

The one-window census and the weight-2 family are separate checks. They do not decide a word that realizes both. Link once: #1200

cursoragent and others added 2 commits November 10, 2026 10:20
Every admissible all-ones window has a floor word with an illegal sum-33 centre, and the fifteen weight-2 masks occur at both centre polarities. The joint sixteen-mask fibre stays open. No kappa change.

Co-authored-by: unpaidmoon <unpaidmoon@users.noreply.github.com>
No individual all-ones window forces a legal centre, and the fifteen weight-2 masks admit both polarities. Those facts do not decide a word that realizes both together. Census counts are unchanged. No kappa change.

Co-authored-by: unpaidmoon <unpaidmoon@users.noreply.github.com>
@unpaidmoon unpaidmoon changed the title Cursor/c5 mask centre nondetermination 704a Record separate c=5 weight-2-family and all-ones-window centre counterexamples Nov 10, 2026
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