Prove the 64-rank center floor under global monotone chart retiming (no new κ)

research/center-chart-bound/PROOF.md

@@ -0,0 +1,116 @@
+# Every retained center still costs rank eight
+
+Prepared by Cinna Davis with substantial OpenAI Codex assistance. Apache-2.0.
+
+## Exact model
+
+Work in the nine-dimensional binary chart space of Cao Yifan's PR4610 word.
+Keep the scalar order, coefficients, field references, logical warp maps,
+main endpoints and explicit adapter boundaries. Each scalar operation must
+still use a common chart on its operands. Persistent transports keep their
+original ascending orientation; zero-length positions may acquire an
+ascending transport. A logical warp G remains monomial and maps its entire
+new input space to its new output space. All helper boundaries are free.
+
+Keep the owned center protocol: clear/copy or gather, one complete Gaussian
+center call at the retained position, scatter or copy back, then erase.
+There is no added center transport between its scalar contacts. Thus its
+live chart between these contacts is common. Its zero reset has no chart
+constraint until its first nonzero use. Both center endpoint charts may
+change. No source center chart is fixed by hand.
+
+All charts can be arbitrary subspaces of F_2^9. They need not be one-axis
+edits, superspaces or subspaces of the submitted charts. This is not a
+search over 511 directions or a local optimum statement. Descending
+persistent moves, additional center calls, new scalar circuits, changed
+logical maps or boundary contracts, enlarged ambient spaces and maps
+between digit columns are outside the model.
+
+## Inclusion graph
+
+Give every chart boundary and scalar contact a node n with unknown
+subspace V_n. A main endpoint or explicit adapter has its original fixed
+space. Other nodes, including every helper endpoint and every center
+contact, are unconstrained initially.
+
+An ascending persistent transport from a to b imposes V_a subset V_b.
+The two endpoints of a center call are initially unrelated: the closure
+adds **no inclusion arc for that call**. This deliberately relaxes its
+implementation contract. A common scalar contact shares one node. Persistent arrival at that contact
+imposes inclusion, permitting a newly paid ascending step. Nonzero owned
+center state has no intervening transport, so its consecutive contact
+nodes are equal. A cleared zero state imposes no previous chart relation.
+
+A logical warp imposes G V_a = V_b. Encode this with both directed
+inclusions G V_a subset V_b and G^-1 V_b subset V_a. Warps are not frozen
+to their old charts. Every constraint is of the form
+
+    A V_a subset V_b,
+
+where A is an invertible binary map or the identity. The original word
+is checked as a feasible assignment of the whole graph, including all
+scalar contacts, all warp maps and both complete paid profiles.
+
+## Universal lower and upper spaces
+
+Initialize lower spaces L_n to {0}, except that a fixed node has its
+fixed space. For each arc A V_a subset V_b, repeatedly replace
+
+    L_b <- span(L_b union A L_a).
+
+For every feasible assignment, induction gives L_n subset V_n. Each
+replacement is a necessary consequence of one actual inclusion. The
+process terminates: every strict replacement raises one finite binary
+subspace dimension. At a fixed point the lower assignment itself obeys
+all graph inclusions and fixed spaces, so it is the least assignment.
+The verifier uses actual XOR span; set union alone would be incorrect.
+
+Initialize upper spaces U_n to F_2^9, except at fixed nodes. Repeatedly
+apply the reverse implication
+
+    U_a <- U_a intersection A^-1 U_b.
+
+For every feasible assignment V_n subset U_n, again by induction. Each
+strict update decreases dimension. Its fixed point is the greatest
+assignment. Neither calculation assumes that different chart choices are
+independent. Equalities, scalar sharing and warp maps propagate globally.
+Original feasibility guarantees that no propagated bound contradicts a
+fixed boundary. The implementation checks every final inclusion as well
+as containment of the submitted assignment inside the interval.
+
+## Result on the actual centers
+
+For both the forward and backward word, each of the eight center calls
+has its originally lower/higher endpoints lo,hi satisfying
+
+    U_lo = {0},       dim(L_hi) = 8.
+
+Thus **every** feasible reassignment has V_lo={0} and dim(V_hi)>=8.
+The nesting and direction for the center follow from the bound, although
+neither was imposed on its unknown endpoint spaces in the closure.
+Its Gaussian rank is at least eight, and the eight calls together retain
+at least 64 units of paid rank mass. For 0<t<=1 their paid moment is at
+least 8*8^t; at t=0 all eight positive calls remain paid. Any phase forms
+within a grammar where nested Fourier rank is at least the dimension
+difference cannot lower this bound.
+
+The verifier checks the original eight rank-eight calls, so the floor is
+attained in this model. This proves a center-bill floor, not optimality
+of the other paid calls or the full native word. A different paid shape
+with the same center bill could still improve K. The conclusion also does
+not price a redesigned center protocol with multiple calls or shared data.
+
+## Evidence boundary and credit
+
+The bound is a finite exact structural theorem about the source's binary
+chart model. It is not a new native construction or multiplication exponent.
+Native/absolute-phase, all-column, ownership, compiler, precision, tape and
+outer hypotheses are not re-proved. There is no Lean or independent human
+proof review. Both queue orders and a change of every frame basis produce
+the same center intervals; three actual source mutations are rejected.
+
+Credit Cao Yifan/PR4610 for the source word; Dugongue/PR4654 for the broader
+chart and phase question; Cinna Davis/PR4665 and PR4696 for phase barriers;
+Cinna Davis/PR4470, zxv, Jacob Alan Sussman and the retained native, helper
+and compiler contributors. The source blob is retained exactly with its
+original commit/path provenance. No predecessor package is copied.

research/center-chart-bound/README.md

@@ -0,0 +1,77 @@
+# The retained center protocol cannot be made cheaper by chart retiming
+
+**Exact finite structural theorem; no higher K.** Every one of PR4610's
+eight retained center calls still has Gaussian rank at least eight under
+any feasible chart reassignment in the monotone nine-axis model below.
+The center bill is therefore at least **64 rank units**, and this floor
+is attained by the submitted word.
+
+This permits arbitrary binary subspaces at every nonfixed contact,
+including all helper boundaries and both endpoints of every center call.
+It is broader than one-contact moves, 511 one-axis tests, or a search
+through superspaces/subspaces of the original charts. Logical warp charts
+may change; the actual G maps remain fixed. The proof uses global lower
+and upper subspace closures, rather than a failed candidate search.
+
+For both complete emitted orientations, all eight originally low center
+endpoints have upper bound `{0}`, while every high endpoint has a forced
+eight-dimensional lower space. The calculation does not even impose a
+relation between the two endpoints of a center call. Its rank floor is
+forced by the surrounding computation.
+
+[PROOF.md](PROOF.md) defines the model and proves the universal interval
+argument. [RESULT.json](RESULT.json) records both exact source certificates:
+22,255 nodes, 38,280 directed inclusions and 761 fixed nodes per orientation.
+The scalar order, coefficients, references, main/adapter boundaries and
+logical maps stay fixed. Persistent transports remain ascending. The owned
+center keeps its clear/copy-or-gather, one call, scatter-or-copy-back and
+erase protocol, with no added center calls between contacts.
+
+New scalar circuits, descending persistent moves, inserted center calls,
+changed main contracts or warp maps, larger ambient spaces and maps between
+digit columns are outside scope. Other paid profile improvements with the
+same center bill remain possible. This is not a universal 64-unit lower
+bound on multiplication suppliers.
+
+Historical [fixed-interface floors](https://github.com/CrocSwap/integer-mult-bounds/pull/1517)
+and [receiver-window floors](https://github.com/CrocSwap/integer-mult-bounds/pull/4585)
+are related predecessors. Here the object is all eight centers of the
+complete PR4610 word, with all helper boundaries and logical warp charts
+free. These older local floors are not used as proof premises.
+
+## Reproduce
+
+```
+python3.12 -B scripts/research_package.py --package research/center-chart-bound
+```
+
+The standard-library verifier authenticates exact original PR4610 bytes,
+recounts both full paid profiles and propagates inclusions through actual
+invertible G maps. Least and greatest fixed points are computed with exact
+binary spans and intersections. Opposite worklist orders and a change of
+every frame basis preserve the center intervals. Three actual source
+mutations and the incorrect set-union interpretation of span are controlled.
+Direct exported replay is `python3.12 -I -B verify.py` from this directory.
+Checks remain enabled under `-O`.
+
+The source native/absolute-phase, all-column, owned-erasure, compiler,
+precision, tape and outer theorems are premises. No new supplier, selected
+cold replay, Lean run or independent human review is claimed. The selected
+conditional K at the pinned main is still .00302015.
+
+## Open next questions
+
+To reduce the center bill, change its actual computation. Start with one
+real source/call/scatter block and give a different arbitrary-input operator
+with its full correction and return bill, or identify a specific changed
+main/map/descending-transport premise. A new candidate must price all new
+calls and the helper inventory it changes. Chart reassignment alone in the
+stated model cannot supply the required center saving.
+Structured questions and the stopping rule are in [TASK.json](TASK.json).
+
+Prepared by Cinna Davis with substantial OpenAI Codex assistance; Apache-2.0.
+Credit Cao Yifan/PR4610; Dugongue/PR4654; Cinna Davis/PR4665 and
+[PR4696](https://github.com/CrocSwap/integer-mult-bounds/pull/4696) for the
+phase questions; Cinna Davis/PR4470, zxv, Jacob Alan Sussman and the retained
+native/helper/compiler lineage. Original source commit/path/blob and exact
+byte pins are in SOURCES.json. No predecessor package is copied.

research/center-chart-bound/RESULT.json

@@ -0,0 +1,164 @@
+{
+  "backward": {
+    "center_bounds_low_high": {
+      "lower": [
+        [
+          0,
+          8
+        ],
+        [
+          0,
+          8
+        ],
+        [
+          0,
+          8
+        ],
+        [
+          0,
+          8
+        ],
+        [
+          0,
+          8
+        ],
+        [
+          0,
+          8
+        ],
+        [
+          0,
+          8
+        ],
+        [
+          0,
+          8
+        ]
+      ],
+      "upper": [
+        [
+          0,
+          9
+        ],
+        [
+          0,
+          8
+        ],
+        [
+          0,
+          8
+        ],
+        [
+          0,
+          9
+        ],
+        [
+          0,
+          8
+        ],
+        [
+          0,
+          9
+        ],
+        [
+          0,
+          8
+        ],
+        [
+          0,
+          9
+        ]
+      ]
+    },
+    "fixed_nodes": 761,
+    "inclusion_arcs": 38280,
+    "nodes": 22255,
+    "unavoidable_center_rank_mass": 64
+  },
+  "controls": {
+    "all_frame_basis_changes": true,
+    "opposite_worklist_order": true,
+    "source_mutations_rejected": [
+      "center_width",
+      "warp_chart",
+      "dependent_frame_basis"
+    ],
+    "xor_span_join": true
+  },
+  "forward": {
+    "center_bounds_low_high": {
+      "lower": [
+        [
+          0,
+          8
+        ],
+        [
+          0,
+          8
+        ],
+        [
+          0,
+          8
+        ],
+        [
+          0,
+          8
+        ],
+        [
+          0,
+          8
+        ],
+        [
+          0,
+          8
+        ],
+        [
+          0,
+          8
+        ],
+        [
+          0,
+          8
+        ]
+      ],
+      "upper": [
+        [
+          0,
+          9
+        ],
+        [
+          0,
+          8
+        ],
+        [
+          0,
+          8
+        ],
+        [
+          0,
+          9
+        ],
+        [
+          0,
+          8
+        ],
+        [
+          0,
+          9
+        ],
+        [
+          0,
+          8
+        ],
+        [
+          0,
+          9
+        ]
+      ]
+    },
+    "fixed_nodes": 761,
+    "inclusion_arcs": 38280,
+    "nodes": 22255,
+    "unavoidable_center_rank_mass": 64
+  }
+}

research/center-chart-bound/SOURCES.json

@@ -0,0 +1,30 @@
+{
+  "schema_version": 1,
+  "base_commit": "b58ad9ef4d4e861b0eaa5dba41742bdc072dca51",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395",
+      "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602",
+      "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72"
+    },
+    {
+      "path": "research/center-chart-bound/inputs/round3-native.json.gz",
+      "usage": "input",
+      "git_blob": "46d929df83817b85a5387bcdb9745e0627d6366e",
+      "sha256": "7679daa4ec6a40f56fc7f0202379a6f454310e94945aba4f48beaaaafb838d05",
+      "pin": "head:96144824fafacf8e4d17b0caf201d74ae757f0d2:research/center-chart-bound/inputs/round3-native.json.gz",
+      "origin": {
+        "commit": "1eb8da6cfb35512c0cc2533413e5ca42f48e13c6",
+        "path": "research/kappa-round3-warp-20261022/ACTUAL-WORD.json.gz",
+        "git_blob": "46d929df83817b85a5387bcdb9745e0627d6366e"
+      }
+    }
+  ]
+}