Repository navigation
Static44 packing ceiling: less than 0.000399% kappa headroom - #549
Conversation
|
Thank you @chafreaky. This contribution at Dual lower bound for a relaxation of fixed local profile/inventory/stage and fallback model. Relaxation removes chronology/ownership/integrality; exact dual feasible inequalities imply exclusion. Not applicable after topology/frame inventory or surcharge changes. Preserved implementation and research: The family review and individual disposition record the scope, evidence and attribution. Parallel and intermediate contributions remain credited even where a later composition has a stronger bound. The published multiplication bound remains conditional on the documented compiler, realization, hosting and analytic assumptions; these finite checks are not a full Lean multiplication proof. |
Scoped negative result: no improved κ is claimed. For #544's fixed static44 complex word, nine-stage chain, eight replicas, helper widths and inherited bad-class charge, every whole-helper packing in the stated model has b < 0.001593251957517. Even an optimistic fractional pool that ignores chronology and ownership cannot reach that endpoint.
The retained balanced conversion then gives κ < 0.001590717543676681. Relative to #547's pinned
079c86cd4a0667506f4d75e0d2584a51a481a3bbcheckpoint, 0.001590711200057236, all remaining packing headroom is less than 6.344e-9, or 0.000399%. The subsequently updated #547 adopts a changed #548 complex word and is outside this fixed-word bound. This identifies a limit of further owner-map/schedule tuning for this fixed word; changed circuits, widths, chains, banks, bad-class charges and outer proofs remain outside the bound.The package derives idle stock and helper demand from pinned #544 artifacts, enumerates every relaxed pattern, and verifies a seven-weight rational dual. Two independent moment engines must each establish every pattern inequality and a strictly positive exclusion margin, including the retained per-child fallback charge. The already-admitted rate and an inflated dual weight must reject as negative controls. A floating LP only nominated the vector; the verifier imports no optimizer.
Standard library only; no network or solver. Complete macOS/Python 3.14.8 and Linux/Python 3.11.15 verification receipts are byte-identical. A dedicated 3.11/3.14 workflow is included; GitHub CI is separate and not claimed green. The proof, source Git-blob bindings, frozen certificate and platform receipts are self-contained.
This is not a universal lower bound, a new finite supplier, an enlarged theorem domain or a κ = 1 proof. The separate 1/33 and Gaussian 1/4 assembly-domain restrictions are already documented upstream and are credited as existing results.
Prepared for chafreaky with OpenAI Codex assistance. Credits: Dugongue #541 static44 construction; icekylinx #535/#531 and the attributed kernel/phase lineage; our #544 admission and owner allocation; Rohan Arun #547 comparison composition; eumemic #543 R420 supplier; the unchanged attributed moment engines. Original notices and licenses remain intact.