Skip to content

Independent verification: R480 packing optimum uniformly through a=1/2 - #1914

Merged
Mister-Meeseeks merged 1 commit into
CrocSwap:mainfrom
bbMisk:codex/t16-pattern-dual
Oct 14, 2026
Merged

Mister-Meeseeks merged 1 commit into
CrocSwap:mainfrom
bbMisk:codex/t16-pattern-dual

Conversation

@bbMisk

@bbMisk bbMisk commented Oct 14, 2026

Copy link
Copy Markdown
Contributor

Ali Romman’s PR1129 already establishes the R480 packing optimum and an attaining T37 construction. This contribution adds an independent standard-library verifier bound to selected PR1094’s T16 inputs, checks PR1129’s fine root endpoints without importing its moment engines, and proves the same fractional optimum uniformly for every real 0 < a <= 1/2. The related U8 supporting audit covers a <= 1/3; the new continuum argument uses exact square-root signs and concavity.

The package checks all 1,163 feasible bin patterns. Nine rational primal patterns match all capacity/helper inventories, and a symbolic dual attains their cost. A separate rational-squaring oracle confirms all endpoint inequalities. The verifier reconciles the primal exactly to PR1129’s T37 table scaled by 16/37 and the dual to its signed prices, independently recounts 69,120 selected owner rows, and confirms the existing root bracket (0.001676905273619680861300, 0.001676905273619680861301).

Scope: fixed local paid profile, helper inventory, disjoint whole-helper reservations and child capacities. Pattern multiplicities, timing and family compatibility are relaxed. No new numerical optimum, kappa, physical owner construction, full cold replay or Lean theorem is claimed. The selected record and all frozen predecessors are unchanged.

Validation on CPython 3.12.13 / macOS arm64:

python3.12 -B scripts/research_package.py --package research/selected-t16-pattern-dual
python3.12 -I -O -B research/selected-t16-pattern-dual/verify.py
python3.12 -I -O -B research/selected-t16-pattern-dual/test_verify.py
git diff --cached --check

All pass: 11 semantic failure controls and nine test groups, including four predecessor-claim mutations and 64 exact integer-power comparisons. Discovery used SciPy; replay has no third-party dependency. Hosted CI is separate.

Started from current main 0b1cccf86e2f5132ed286a26ef0a681a495740ea. Task independent-moment, nonce 14c8429d797658917dfffd38f0db810d. Coordination and final scope. Final full overlap snapshot covered 554 open PRs and 535 discussion records; limits and historical follow-up are recorded in TASK.json.

Credit Ali Romman (PR1129), Chafik Boukhalfa (PR795/1131 and signed prices), woklerx’s U8 uniform audit, Rohan Arun, Jeremy Kothe, Hao Yan and the retained supplier lineage. Nearby PR1783/1847 screens and PR1685 have explicit scope comparisons. Substantial OpenAI Codex assistance; Apache-2.0. No independent human review is claimed.

@Mister-Meeseeks
Mister-Meeseeks merged commit ec94fd3 into CrocSwap:main Oct 14, 2026
4 of 61 checks passed
@Mister-Meeseeks

Copy link
Copy Markdown
Contributor

Batch review at 05c3b117e962e6a1ba8fa5c524cd4cfafb3e5c74.

Merged to main, preserving the original contributor commits and package attribution.

Reviewed scope: Exact1163-pattern dual and nine-pattern fractional attainment extend the credited1129 optimum uniformly to0<a<=1/2. Independent radical engines,11 controls and9 tests pass; T16 integer nonattainment is distinguished from T37 attainment and actual chronological packing. No new frontier.

The pinned scoped command passed; the batch ledger contains its command, input hashes, environment and log. This incorporates the research/tooling contribution and does not change the selected κ or discharge the inherited multiplication-theorem assumptions.

Batch review, attribution and evidence. Thank you for the contribution.

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