Prove rank-eight owned high contacts after removing all native constraints

research/monotone-owned-centre-floor/PROOF.md

@@ -0,0 +1,116 @@
+# Sharp high-contact floor in the round-three word
+
+Prepared by Cinna Davis / 1337isnot1337 with substantial OpenAI Codex
+assistance; Apache-2.0. This is a written scoped proof with exact finite
+witnesses, not a proof-kernel check or a new multiplication theorem.
+
+## Statement
+
+Use the exact scalar opcode, coefficient, order and persistent-field incidence
+of Cao Yifan's round-three word in `SOURCES.json`, separately in either
+orientation. At every scalar event, all its persistent operands have one
+common binary frame subspace in F2^9. Between consecutive scalar contacts on
+a persistent field, with no intervening native warp, require containment in
+chronological order. The main entrance subspaces stay fixed. The helper
+entrances/exits, all scalar contact subspaces and all native warp boundaries
+may otherwise vary. In particular, do not impose a relation across any native
+warp and do not require final endpoints in this relaxation.
+
+Then each of the eight high owned contacts has dimension at least eight. The
+original word simultaneously attains eight at all of them, so these bounds are
+sharp. For a center job between that high contact and the zero subspace, its
+rank is therefore at least eight. Retaining all eight jobs gives paid rank
+mass at least 64 and, at every positive rank exponent t, center moment at
+least 8 times 8^t. This is a bound on the center contribution. It does not
+optimize the remaining paid/helper moment.
+
+In the forward orientation the contact is the persistent source of an owned
+COPY immediately before the descending center job. In the backward orientation
+it is the persistent destination of the owned output ADD immediately after
+the ascending job. `verify.py` checks these actual macro boundaries and the
+initial/final owned CLEARs adjacent to the high side.
+
+## Path lemma
+
+Matarener's PR5060 (`research/owned-centre-wire-floor/PROOF.md`, Lemma1)
+already uses forward joins and backward meets to force contact subspaces,
+and proves a complete nested owned-wire floor with fixed warps and helpers.
+The containment propagation below is the same elementary invariant. The new
+source-specific coverage removes all native relations and helper boundaries,
+retains only fixed main entrance seeds, and supplies explicit path witnesses
+for the newer round-three word. It proves the high-contact floor in that
+larger domain, not the predecessor's full owned-wire conclusion there.
+
+Associate a vertex with each main entrance and scalar contact. For each
+persistent field, draw an edge from its previous entrance/contact to the next
+scalar contact. A native warp terminates that chain: its output begins a new
+unconstrained chain, and no relation across the warp is retained. Identifying
+the two operands of a scalar ADD at one contact gives their common subspace.
+No edge for a productive helper target or final endpoint is needed.
+
+If v lies in a fixed main entrance space and a directed path leads from that
+entrance to contact q, then v lies in the space at q. This follows by induction
+on the path length, using the containment hypothesis on every edge. Thus k
+linearly independent fixed entrance vectors with paths to q force dimension
+at least k, regardless of all other contacts, helper choices and native maps.
+
+This argument uses the common physical frame of scalar operands, not their
+data coefficients or nonzero logical dependence. Data cancellation does not
+remove a required physical contact. Splitting operands into independent gauges
+requires a different paid scalar interface and falls outside this statement.
+
+## Source-bound witnesses
+
+The source has 632 persistent fields, of which 224 are main and 408 are
+independent arbitrary helpers. Raw event ordinals below omit `climb` events
+and start at zero. The graph contains 31,630 distinct monotone edges in each
+orientation. Every one of the 240 native events per orientation is cut.
+All owned scalar contacts, including the low scatter/gather side, are released
+while proving the high-side floor. Helper spaces do not supply witness seeds.
+
+| Persistent role | Forward high event | Backward high event | Original frame ID | Eight independent entrance vectors |
+| --- | ---: | ---: | ---: | --- |
+| 92 | 10344 | 10367 | 254 | 276, 351, 266, 74, 44, 193, 247, 14 |
+| 57 | 10370 | 10393 | 274 | 304, 379, 259, 67, 37, 131, 254, 14 |
+| 81 | 10396 | 10419 | 619 | 471, 386, 73, 506, 164, 194, 254, 388 |
+| 224 | 10422 | 10445 | 279 | 471, 386, 73, 506, 164, 194, 304, 74 |
+| 11 | 10448 | 10471 | 621 | 268, 274, 164, 194, 146, 289, 67, 388 |
+| 240 | 10474 | 10497 | 280 | 268, 274, 146, 289, 304, 379, 164, 247 |
+| 9 | 10500 | 10523 | 624 | 268, 274, 146, 289, 471, 386, 67, 14 |
+| 256 | 10526 | 10549 | 281 | 247, 145, 290, 196, 268, 274, 471, 304 |
+
+Each integer encodes a nine-bit binary vector. `WITNESSES.json` records the
+actual fixed entrance role and every graph vertex on each path. It contains
+128 paths and 2,204 links across both orientations. The verifier checks every
+seed, chronological link, target, binary rank and equality of the resulting
+eight-dimensional span with the original high contact. The path lemma proves
+the bound for arbitrary candidate subspaces, without enumerating them.
+
+The original full source has paid histogram
+`{1:2201, 2:412, 3:510, 4:127, 5:40, 8:8}` and productive-helper histogram
+`{4:28, 7:7, 8:47, 9:326}` in both directions. These are reconstructed as
+baseline controls, including every center. They are not a claimed new invoice.
+No solver, power approximation or floating tolerance enters the certificate.
+
+## Decision and limits
+
+The independent-contact/shared-native-map proposal in
+[the preceding claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/4611#discussioncomment-19139586)
+released the high COPY chart while keeping the opposite owned chart at zero.
+Its proposed center reduction is impossible under monotone persistent paths.
+The proof already holds in a relaxation that forgets every shared-map equation.
+No MILP is required to decide that center reduction.
+
+Other bridges or productive boundaries might still improve while all centers
+retain rank eight. This theorem proves no whole-profile optimum. Moving the
+low center side can also change the job rank, which is then a relative rank
+between two nonzero spaces rather than the dimension bounded here. Nonmonotone
+transitions, changed scalar chronology, split scalar contacts, phase/general
+gauges, changed main entrances and sharing different owned macros need separate
+analysis. In particular the previous common-kernel prototype allowed
+nonmonotone edges and is not excluded by this theorem.
+
+The source-specific finite statement is distinct from native all-column
+realization, precision, movement, owned erasure, compilation and the outer
+integer-recovery theorem. Those are not reverified or strengthened here. The
+selected conditional kappa remains 0.00302015.

research/monotone-owned-centre-floor/README.md

@@ -0,0 +1,79 @@
+# Monotone owned-center high-contact floor
+
+Each of the eight owned high contacts in the actual round-three word must
+have dimension at least eight under fixed main entrances, the fixed scalar
+word and monotone persistent-field contact subspaces. This remains true after
+discarding every native warp relation, freeing all helper boundaries and
+freeing the other scalar contacts. The source attains all eight bounds.
+
+Consequently, releasing only the high side of the centers while keeping the
+other side at zero cannot reduce their paid rank mass below 64. The proof
+does not give a global moment optimum or a higher kappa. The selected
+conditional result at the base commit is kappa 0.00302015.
+
+Read [PROOF.md](PROOF.md) for the mathematical argument, exact hypotheses,
+source-contact table and limits. [WITNESSES.json](WITNESSES.json) contains
+128 independent entrance-vector paths with 2,204 links, covering both actual
+orientations and all eight owned lifetimes separately. Only fixed main
+entrances supply seeds; no clean logical helper input is assumed.
+
+Reproduce with standard Python 3.12 or later:
+
+```sh
+python3 -B scripts/research_package.py --package research/monotone-owned-centre-floor
+python3 -I -B research/monotone-owned-centre-floor/verify.py
+python3 -I -O -B research/monotone-owned-centre-floor/verify.py
+```
+
+The registered commands include the normal and optimized exact checks, the
+complete source paid/helper baseline and 144 corruption, rank-seven-hyperplane
+and warp-cut controls. `verify.py --write` regenerates the deterministic
+witness artifact. Verification does not write it. This needs no solver,
+network, imported predecessor executable or optional package.
+
+Source: Cao Yifan / intqwq's round-three word, retained in
+`research/kappa-round3-warp-20261022/ACTUAL-WORD.json.gz`, with compressed and
+decompressed SHA256 bindings. The source manifest pins the base and exact live
+input; all frozen predecessor bytes remain unchanged. Retain Cinna Davis's
+native/controller/retiming lineage, Dugongue's transported-frame work, zxv,
+Jacob Alan Sussman and the source's complete predecessor attribution.
+
+This continues the owned-contact question from the
+[bounded common-kernel prototype](https://github.com/1337isnot1337/integer-mult-bounds/tree/8052b4818738986960c5b243097b3fffb6d21139/research/owned-centre-kernel-retiming)
+and [independent-contact claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/4611#discussioncomment-19139586).
+The former permits nonmonotone transitions and is not excluded by this proof.
+The pending nearest-Clifford/split-contact work in
+[discussion #5125](https://github.com/CrocSwap/integer-mult-bounds/discussions/5125)
+also has a different boundary. Canonical investigation update:
+[the scoped finding](https://github.com/CrocSwap/integer-mult-bounds/discussions/4611#discussioncomment-19143793).
+
+Matarener's [PR5060 owned-wire floor](https://github.com/CrocSwap/integer-mult-bounds/pull/5060)
+already proves a complete nested C-wire floor for the older #4470 word with
+fixed native warps and helper boundaries, including variable low contacts.
+Its interval-propagation/path argument is prior work. The present result
+extends the high-contact part to the actual round-three word with every warp
+relation removed and all helper boundaries free, using explicit paths seeded
+only by main entrances. It does not extend PR5060's complete C-wire floor to
+that larger domain. In particular, its open low-side/helper-boundary question
+must not be reported as solved here.
+
+Prepared by Cinna Davis / 1337isnot1337 with substantial OpenAI Codex
+assistance; no subagents. Apache-2.0. Evidence is author-checked, not independent
+human or proof-kernel acceptance. A package merge would not select a frontier.
+
+## Open next questions
+
+- Can changing both sides of an owned center job improve the complete moment?
+  The high-side floor does not settle its relative rank. First reconstruct
+  both owned macro itineraries with one variable low chart, charge all changed
+  persistent bridges and the full center rank power, and gate the complete
+  baseline before solving. Actual frame/phase, ownership, cleanup, precision
+  and compiler/outer charges remain obligations.
+- Can a changed scalar word or nonmonotone paid itinerary remove the forced
+  entrance paths at a favorable total cost? Name the exact edit or descending
+  bridge, emit both orientations, and reconstruct every paid/helper child.
+  The present proof and the old floating common-kernel failure do not decide
+  that question.
+
+The structured questions, stopping rule and scope change are in
+[TASK.json](TASK.json). No extra search is claimed by this package.

research/monotone-owned-centre-floor/SOURCES.json

@@ -0,0 +1,36 @@
+{
+  "schema_version": 1,
+  "base_commit": "20a1e31bc6009b9b3f4d084bbaadc6350e34fcba",
+  "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/kappa-round3-warp-20261022/ACTUAL-WORD.json.gz",
+      "usage": "input",
+      "git_blob": "46d929df83817b85a5387bcdb9745e0627d6366e",
+      "sha256": "7679daa4ec6a40f56fc7f0202379a6f454310e94945aba4f48beaaaafb838d05"
+    },
+    {
+      "path": "research/owned-centre-wire-floor/README.md",
+      "usage": "provenance",
+      "git_blob": "ffd10d3c4314d3bdc80aad56d606b73e1bb4d820",
+      "sha256": "f2fdd6c91d98b692dac91e7a6cd6c8f09094cd2259ed3737ec429b147499c0a3"
+    },
+    {
+      "path": "research/owned-centre-wire-floor/PROOF.md",
+      "usage": "provenance",
+      "git_blob": "e6033ac5ddedc4152c2553499021b262f81f75bd",
+      "sha256": "4fddcb9d3595870dd6ba9a0819e19ba50d9748b3cd643b978f43aef8750dcaf5"
+    }
+  ]
+}

research/monotone-owned-centre-floor/TASK.json

@@ -0,0 +1,75 @@
+{
+  "schema_version": 1,
+  "task_id": "centre-path-sharing",
+  "priority_revision": 7,
+  "base_commit": "20a1e31bc6009b9b3f4d084bbaadc6350e34fcba",
+  "original_card": {
+    "id": "centre-path-sharing",
+    "question": "Can the 64-per-call centre path (eight rank-8 COPY/ERASE totals through the private temporary) be shared across calls or shrunk?",
+    "starting_points": [
+      "docs/research/research-family-status.md",
+      "research/complex-local-word-ceiling/README.md",
+      "research/split-centres-global/proofs/PR386-BIT-GEOMETRY.txt",
+      "certificates/selected-result.json"
+    ],
+    "methods": [
+      "Derive a fully charged favorable relaxation for sharing one centre path across k calls, including restoration, hosting and precision.",
+      "Prove a lower bound on copied information per call for the selected decoder contract."
+    ],
+    "acceptance_gate": "Show the changed centre charge and copy profile per call with every added restoration or hosting cost charged, and its ceiling via ceiling.ceiling(centre=...). A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "research/complex-local-word-ceiling/verify.py"
+      ],
+      "expected": "PASS_COMPLEX_LOCAL_WORD_CEILING",
+      "inspect": "Read the selected word's per-call local profile, its packing ceiling and the lever table; run levers.py for the ideal budget of the lever you target.",
+      "scope": "Positive control and planning budget only; this is not a new construction or full cold replay."
+    },
+    "first_experiment": "Write the per-call centre charge and copy children for sharing across k = 2 calls, charge the sharing overhead, and screen it; stop this route if even the ideal sharing gains under 10%. Ideal budgets: free 2.80x, shared by two 1.90x (levers.py).",
+    "bottleneck_link": "The centre path consumes 64 of about 99.6 unpaid coordinates per call, i.e. about 64% of the raw deficit.",
+    "allowed_variations": [
+      "One sharing pattern across a fixed number of calls.",
+      "One reduced copied-total contract for the existing decoder.",
+      "If the coverage law, template or guard changes, derive an applicable fully charged replacement bound instead of applying the incumbent ceiling outside its scope."
+    ],
+    "scope_change_triggers": [
+      "Removing copies without a replacement contract for the decoder's copied totals.",
+      "Continuing a partial cost improvement while leaving the same unpriced consumer, restoration or central-readout obligation unresolved; refresh the family expansion decision first. Local product-retiming evidence has a narrow scope and is not a ban on changed graphs or contracts."
+    ],
+    "overlap_terms": [
+      "centre path",
+      "copied totals",
+      "private temporary",
+      "shared centre",
+      "batching"
+    ]
+  },
+  "scope_status": "refined",
+  "actual_scope": "Prove sharp rank-eight floors at every owned high contact of the actual round-three word, for arbitrary monotone contact subspaces and all native warp relations removed.",
+  "scope_change_reason": "Resumes the independent owned-COPY/shared-map handoff. Before solving, exact paths already exclude lowering the high side; the card historical sharing/ceiling experiment does not cover this changed-source invariant.",
+  "bottleneck_link": "Eight rank-eight owned center jobs remain a paid rank mass of at least64 when their opposite chart stays zero. This closes the high-contact-only monotone retiming route without a solver.",
+  "budget_minutes": 60,
+  "stop_rule": "Finish exact source-bound floor and explicit path witnesses; do not launch the precluded high-side-only MILP or infer a universal moment optimum.",
+  "outcome": "completed",
+  "evidence": "PROOF.md, WITNESSES.json; normal and optimized registered replay with source baseline and144 controls.",
+  "author": "Cinna Davis / 1337isnot1337, with substantial OpenAI Codex assistance",
+  "ai_assistance": "Substantial OpenAI Codex assistance in proof, implementation, experiments and writing. No subagents or human/kernel proof acceptance claimed.",
+  "open_questions": [
+    {
+      "question": "Can releasing the zero-side charts of a center macro lower the complete paid-minus-productive moment?",
+      "why_it_matters": "The high-side floor alone does not bound rank of a transition between two nonzero charts.",
+      "first_step": "Derive both orientation owned macro itineraries with a variable low chart, reprice all adjacent persistent transports and use full center rank powers.",
+      "blocked_by": "A common physical contact chart for every scatter/gather operation, owned restoration, native phases and full supplier/outer costs."
+    },
+    {
+      "question": "Can a changed scalar word or nonmonotone paid itinerary avoid the eight independent entrance paths?",
+      "why_it_matters": "Those are hypotheses of the floor; the previous common-kernel search permits nonmonotone edges and is not excluded by this theorem.",
+      "first_step": "Name the exact edited scalar event or descending bridge, emit both full literal words and reconstruct every paid/helper child before search.",
+      "blocked_by": "Exact endpoint, native absolute-phase and fully funded compiler/precision/outer obligations."
+    }
+  ],
+  "upstream_checked_commit": "20a1e31bc6009b9b3f4d084bbaadc6350e34fcba",
+  "canonical_thread": "https://github.com/CrocSwap/integer-mult-bounds/discussions/4611#discussioncomment-19143793"
+}

research/monotone-owned-centre-floor/VERIFY.json

@@ -0,0 +1,36 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/kappa-round3-warp-20261022/ACTUAL-WORD.json.gz"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 30,
+      "checks": "Exact source baseline,128 independent main entrance paths,2204 literal links,144 corruption/hyperplane/warp-cut controls."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-O",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 30,
+      "checks": "Same source-bound proof and controls with assertions disabled."
+    }
+  ]
+}