Repository navigation
Prove the 64-rank center floor under global monotone chart retiming (no new κ) - #4700
Conversation
|
Note: the centre cannot be shared across recursion levels either (nested-recursion check on #4470). We asked whether a child controller could live in the parent's F2^9 block (the child inherits the parent's 9 label axes instead of a fresh tensor factor), so that one rank-8 centre transport and one thin query shear per port serve two levels. Three independent obstructions, checked on the #4470 word in both orientations:
Scripts and receipts (nest_check.py, cone_check.py, nest_controller.py; standard library plus sympy for the controller replay) are available on request. No new kappa. |
|
Note on splitting the ports into two alternating phases (Mark / @Matarener, with Claude). Scoped screen, not a theorem; no new κ, no PR. Question: can the centre bill be avoided by serving the 112 ports in two alternating phases of 56, so that each full call only needs a centre for 56 ports? On the obvious halves the answer is no, and not by a small margin. 1. Threshold. For a unit of v ports with centre cost c per full call, the #4470 surplus identity reads S = (p+2)(v − c) − v, and G scales with v. Matching #4470 (S/v = 752/112 = 6.714 at p+2 = 18) needs c/v ≤ 0.5714. That means c ≤ 64 at v = 112 (today's tie), c ≤ 32 at v = 56 and c ≤ 13.7 at v = 24. 2. Centre floor for sub-sets of P112, in the model of
The control reproduces the package's 64. Every sub-set's floor is above the cost it would need, and the known decoders are higher still. 3. Alternation adds idle cost. In the #4440/#4470 family idle is the d = 8 price per thick stage for every field, including fields that are not served in that phase, and it is credited only in a field's own window. A sleeping half therefore pays idle without credit. An honest "two phases" reading becomes two independent small units, and those die on the centre floor in item 2. Limits. Only these five sub-sets were checked, not all 56-subsets, and term directions are limited to the {−2..2}^8 box. Terms are taken in the root code, as in the package. This is a screen, and it only shows that the natural halves are far from the needed price (42 against 32 at best). |
Every retained PR4610 center call still costs rank at least eight under arbitrary monotone chart retiming of the stated protocol. Exact global subspace closures force each originally low endpoint to zero and each high endpoint to contain an eight-dimensional space. The eight calls therefore retain at least 64 paid rank units. No higher K is claimed.
This is an all-assignment certificate for binary charts in F_2^9, rather than a failed local, one-axis or superspace search. All helper boundaries, both center endpoint charts and logical warp charts may change. The actual G maps, scalar graph/order/coefficients/references, main/adapter boundaries and monotone persistent direction remain fixed. The center keeps one call between its copy/gather and scatter/return; no added center transport occurs between its scalar contacts. New circuits, descending persistent steps, changed maps/contracts and maps between digit columns remain outside scope.
The proof deliberately imposes no relation between the two unknown endpoints of a center call. Its rank floor follows from the surrounding computation. Both complete orientations have 22,255 nodes, 38,280 directed inclusions and 761 fixed nodes. Least and greatest subspace assignments come from exact XOR spans, intersections and actual invertible warp maps. Their universal sandwich proof is in
research/center-chart-bound/PROOF.md; README.md defines the limitations and concrete next question. This bounds the center bill, not the other paid profile or the best K.Only
research/center-chart-bound/is added. Original PR4610 bytes, blob and commit/path provenance are retained exactly. The original paid profiles, scalar frames and warp geometry are checked. Opposite worklist orders and independent changes to every frame basis give the same center intervals; three actual source mutations and the set-union/span distinction are controlled.Validation: CPython 3.12 registered replay and isolated optimized replay pass; committed-byte/source-history preflight and official export integrity pass. The final exported verifier passes under -O with Git absent from PATH and leaves every exported file unchanged. No native all-column, selected cold replay, outer theorem or formal kernel run is claimed. Refreshed canonical main remains b58ad9e, selecting conditional K=.00302015. The 16:35 UTC overlap snapshot completely paginated 467 open PR bodies and 3,623 Discussion records; sparse local note coverage is incomplete. Historical #1517/#4585 local floors are credited and not used as premises.
Credit Cao Yifan/#4610, Dugongue/#4654, Cinna Davis/#4665 and #4696 for the phase questions, Cinna Davis/#4470, zxv, Jacob Alan Sussman and the retained native/helper/compiler lineage. Prepared by Cinna Davis with substantial OpenAI Codex assistance; Apache-2.0. No independent human review is claimed.