Certify the native/thin path-family ceiling C < 0.003022 and price H repair headroom

research/controller-stage-ceiling/PROOF.md

@@ -0,0 +1,126 @@
+# Complete stage-family ceiling and a native repair target
+
+Prepared by Cinna Davis with substantial OpenAI Codex assistance. Apache-2.0.
+
+## Family and scope
+
+Fix one of the three source-bound local invoices: selected PR4470, PR4610,
+or PR4626. There are v=112 ports and transverse rank b=8. For each
+1 <= p <= 64, take any split a in {0,...,p-1} of the minimal-cut paired
+path controller, and **any** subset S of its 2p+1 native stage positions.
+Stages outside S become fully paid query shears, lose all helper credit,
+and lose their stage multiplier in both main targets and idle jobs.
+This is the specialization operation of PR4440, not deletion of a bill.
+
+The family is deliberately an invoice relaxation: all these substitutions
+are priced even if a particular new physical contact has not been admitted.
+Rejecting this stronger relaxation is safe; positive scores alone would not
+admit a word. No other idle masks, words, native suppliers, typed outputs,
+or p>64 are excluded. The selected record is unchanged.
+
+## Complete surplus
+
+Let n=|S|, t=1-C, and let H_t and P_t be the local helper and paid moments.
+Write V=112 and B=8. The complete surplus is
+
+    F(C) = n(H_t-P_t+V) - V(2p+1) + 2V(1+Bn)^t
+           + sum_arm 2V[(1+B(k+e))^t - (Bk)^t - e B^t].
+
+There are a left arm of length a and a right arm of length p-1-a. At
+an arm step j, k is the number of selected bits in the first 2j positions
+of that arm and e is the next, even-position bit. The right arm is read
+in reverse stage order. Rank-zero idle terms mean zero cost, including
+in the limit t -> 0. The central odd-position bit contributes only to n.
+
+The first term includes all n independent helper inventories and all n
+native paid inventories. The V correction replaces the otherwise paid
+query at each native stage. The second term charges every query position.
+The third term is the two copies of the long main target. Each arm term
+includes its shorter main target, initial/terminal idle, and the separate
+middle idle of rank B when e=1. Thus no middle idle is silently erased
+when its stage remains native. `literal_control` independently counts every
+LOCAL, QUERY_SHEAR, IDLE and diagonal target of the retained p16 word.
+
+## Dynamic program, with outward rounding
+
+An arm's score depends on a prefix only through its selected-bit count.
+For a nonempty arm its first two bits have no separate charge and therefore
+only their count 0,1,2 matters. An empty arm has one bit. At each subsequent
+step choose e, add its displayed complete arm contribution, then choose the
+following odd bit unless this is the last step. Keep the largest score
+for each count. This is exhaustive induction on the bit prefix, not a
+local hill climb. It is the recurrence of the credited historical floating
+DP, now evaluated with exact, outward integer bounds.
+
+The retained rational interval engine encloses each r^t. Scale by 2^64,
+round positive occurrences up and negative occurrences down. Every DP
+score is consequently an upper bound on its real surplus. Maxima preserve
+upper bounds. Combine both arms, every split and the middle bit, then
+maximize over every p=1,...,64. The three native profiles share that
+combinatorial envelope. Their local replacement terms are added separately.
+
+At C=0.003022, every final upper bound is strictly negative. `RESULT.json`
+records the exact rational upper bounds, integer scale and witness parameters.
+The covered count is sum(p*2^(2p+1), p=1,...,64) per native invoice. It
+counts split/support pairs; it is not a claim that all invoices are distinct.
+
+Acceptance also exhausts every arm bit pattern through length four and
+all complete stage supports/splits through p=3; checks the actual p16
+invoice for each local substitution; and recomputes a witness moment with
+the independent full-invoice path of the rational engine. Omitting the
+real middle-idle charge or duplicating independent helper credit changes
+the rejection into an apparent positive result. These are rejected models.
+
+## Why one test excludes every larger saving in this family
+
+For each fixed support, divide the surplus by 8^t. Its normalized local
+replacement is
+
+    L(C) = (H_t - P_t + V)/8^t.
+
+All paid ranks are at most 8. For t in (0,1], its derivative with respect
+to C has upper bound
+
+    L'(C) <= -((P_1-V)/8)*log(8)
+              + sum_(r<8) H_r log(8/r) < 0.
+
+Indeed, retain only the negative rank-one paid contribution; its magnitude
+is at least (P_1-V)log(8)/8. Bound each possible positive helper contribution
+by H_r log(8/r), and drop the other negative contributions. The final strict
+inequality is enclosed rationally for each frozen invoice.
+
+For an arm step with k>=1, the derivative of
+
+    (k+e+1/8)^t - k^t - e
+
+is negative, since x^t log(x) is increasing for x>=1. If k=0,e=1,
+its derivative is again negative. The only positive case k=e=0 contributes
+at most (1/8)^t log(8) before the multiplicity 2V. There are at most p-1
+such arm steps. The normalized negative query term contributes
+-V(2p+1)(1/8)^t log(8), more than cancelling all of them. If n>=1,
+the normalized long main target has negative derivative. If n=0, its
+positive derivative leaves the total derivative exactly
+-V(1/8)^t log(8). Thus F(C)/8^(1-C) is strictly decreasing throughout
+0<=C<1 for every support in the family.
+
+The negative bound at .003022 therefore excludes **all C>=.003022,
+C<1**, not merely that one numerical point. This is a conditional invoice
+ceiling, not a universal limit on integer multiplication.
+
+## Changed model: the H repair budget
+
+The old H112 reconstruction changes a local rank-eight correction bill
+8 H8 to 8 H1, saving 56 units of rank per full call. Applying that
+56-unit change to PR4610's stronger native invoice is an **optimistic
+unrealized combination**. It is not a source-compatible H word: changed
+warp contacts, cross-port response, head/hole normalizers, absolute phases
+and arbitrary-input helper restoration all still need proof.
+
+For that explicitly hypothetical invoice, the same complete DP gives
+exact upper repair budgets at .004, .006 and .01. A full-invoice lower
+bound at each saved witness confirms the scale of the positive budgets.
+A rank-one repair request costs exactly one unit at every C; a rank-r
+request costs r^(1-C). Storage, scalar work and all other requests also
+need their actual ledger. These numbers are spending limits, not free
+allowances or proposed K values. In particular the .01 screen fails even
+before a repair in this bounded family. No conclusion for p>64 follows.

research/controller-stage-ceiling/README.md

@@ -0,0 +1,63 @@
+# Exact ceiling for native/thin path-controller changes
+
+**No higher K or new supplier is claimed.** For the source-pinned PR4470,
+PR4610 and PR4626 invoices, every minimal-cut path controller with 1..64
+pairs, every split, and every native/thin stage subset fails at
+C=0.003022. A normalized-moment monotonicity proof excludes all larger
+C<1 in this family. This turns the earlier floating stage search into an
+exact certificate and identifies a model change required for a substantial
+increase. The selected conditional K remains 0.00302015 at the base commit.
+
+[PROOF.md](PROOF.md) derives the complete invoice, the exhaustive max-plus
+recurrence, outward integer bounds and the monotone rank-eight separator.
+[RESULT.json](RESULT.json) contains the exact receipt. This does not exclude
+new words, native interfaces, idle masks, coded corrections, or p>64.
+
+The changed-model calculation also prices an optimistic combination of
+PR4610 with H112's 56-rank-unit local saving. Its repair budgets at .004,
+.006 and .01 are included, with the unproved native/caller compatibility
+explicitly retained. A budget or positive invoice is not an implementation.
+
+| Candidate C | Maximum optimistic rank-one repair budget |
+| --- | ---: |
+| .004 | 2641.1932795534 (p=64) |
+| .006 | 342.1085144324 (p=37) |
+| .01 | Already negative: -93.1789150428 |
+
+These are bounded-family upper limits; source compatibility is unproved.
+
+Reproduce from the repository root:
+
+```sh
+python3.12 -B scripts/research_package.py --package research/controller-stage-ceiling
+```
+
+The verifier uses the standard library and the pinned rational interval
+engine. It does not require a solver. Controls compare small complete
+censuses and literal p16 event bills, and show why dropping middle idles
+or duplicating independent helper credit would give false apparent gains.
+The external PR inputs are exact unmodified Git blobs, not newly admitted
+native words; their provenance and heads are in SOURCES.json.
+
+## Open next questions
+
+1. Construct a physical H caller with a complete correction invoice below
+   the recorded repair budget. Start with one actual head/hole boundary and
+   check all columns, source/complement ownership and absolute phases. The
+   old local H invoice and its scalar involution do not close that caller.
+2. Change the native word, interface or controller topology. A further
+   native/thin subset scan inside the certified family cannot reach .004.
+   A new candidate must provide an exact endpoint and a complete paid bill.
+
+## Attribution and status
+
+Prepared by Cinna Davis with substantial OpenAI Codex assistance, Apache-2.0.
+The branch recurrence is credited to the pre-existing
+`research/kappa-hybrid-controller/search/direct_stage_dp.py` authors and
+Cinna Davis's PR4440/PR4470 controller lineage. Cao Yifan's PR4610 supplies
+the changed warp invoice; hexapode's PR4626 supplies the helper621 invoice.
+Retain zxv's exact interval/native/strictification contributions and Jacob
+Alan Sussman's mixed-job/compiler work. The new contribution is the exact
+integer bound, the monotonicity proof and the current source-bound repair
+budget. It does not assert independent human review, a formal proof-kernel
+check, or a new multiplication theorem.

research/controller-stage-ceiling/RESULT.json

@@ -0,0 +1,82 @@
+{
+  "all_native_stage_subsets": true,
+  "all_splits": true,
+  "ceiling": "1511/500000",
+  "controls": [
+    "all_5_small_arm_censuses",
+    "all_complete_patterns_p1_to_p3",
+    "all_3_literal_p16_invoices",
+    "missing_middle_idle_changes_sign",
+    "duplicate_helper_credit_changes_sign"
+  ],
+  "fixed_point_scale": "18446744073709551616",
+  "new_kappa": null,
+  "optimistic_H_repair_budgets": {
+    "1/100": {
+      "best_surplus_upper": "-53713987464422013341/576460752303423488",
+      "status": "OPTIMISTIC_INVOICE_ONLY_NO_H_NATIVE_ADMISSION",
+      "witness_parameters": [
+        1,
+        0,
+        6
+      ],
+      "witness_surplus_lower": "-292446764658482249839017434957133446527108325308117437477329/3138550867693340381917894711603833208051177722232017256448"
+    },
+    "1/250": {
+      "best_surplus_upper": "24360708238561784637317/9223372036854775808",
+      "status": "OPTIMISTIC_INVOICE_ONLY_NO_H_NATIVE_ADMISSION",
+      "witness_parameters": [
+        64,
+        31,
+        680564733840226340207702041255296892927
+      ],
+      "witness_surplus_lower": "2072379864822052426775990683944584074709758170880344027228125/784637716923335095479473677900958302012794430558004314112"
+    },
+    "3/500": {
+      "best_surplus_upper": "3155394105585959091153/9223372036854775808",
+      "status": "OPTIMISTIC_INVOICE_ONLY_NO_H_NATIVE_ADMISSION",
+      "witness_parameters": [
+        37,
+        18,
+        31482443219130968091307
+      ],
+      "witness_surplus_lower": "2147449949634335534650179046572602361862313365888596319687777/6277101735386680763835789423207666416102355444464034512896"
+    }
+  },
+  "pair_counts": [
+    1,
+    64
+  ],
+  "patterns_per_profile": "57772384072799330241337377795082425233864",
+  "profiles": {
+    "PR4470": {
+      "separator_derivative_lower": "834868369783004008952768229585313202122157833070803325402459/1569275433846670190958947355801916604025588861116008628224",
+      "surplus_upper": "-4184234018831163103/9223372036854775808",
+      "witness_parameters": [
+        16,
+        7,
+        7158278827
+      ]
+    },
+    "PR4610": {
+      "separator_derivative_lower": "410091947704675574684453227077902260907026584522260683631425/784637716923335095479473677900958302012794430558004314112",
+      "surplus_upper": "-1014518977939581775/9223372036854775808",
+      "witness_parameters": [
+        16,
+        7,
+        7158278827
+      ]
+    },
+    "PR4626": {
+      "separator_derivative_lower": "1640764499882385906456930065487073635005120770603694469307877/3138550867693340381917894711603833208051177722232017256448",
+      "surplus_upper": "-977466852836146591/9223372036854775808",
+      "witness_parameters": [
+        16,
+        7,
+        7158278827
+      ]
+    }
+  },
+  "scope": "Frozen native invoices and minimal-cut path family, p<=64. No global operator/controller ceiling or new supplier.",
+  "status": "PASS_EXACT_STAGE_FAMILY_CEILING"
+}

research/controller-stage-ceiling/SOURCES.json

@@ -0,0 +1,70 @@
+{
+  "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/higher-moment-strictification/verify.py",
+      "usage": "input",
+      "git_blob": "4b24a5096154736ce060474eb8c72dc64c303699",
+      "sha256": "0ce7e7137422d5ffeda22085c81fa88471bbe963100fdad62e659f1e3bf89326"
+    },
+    {
+      "path": "research/joint-helper-lattice/NATIVE.json.gz",
+      "usage": "input",
+      "git_blob": "0910f74138decf498e7fc445cc2daff4390169d6",
+      "sha256": "74582cce642c80f0235be7fcbce3716174666326ac6a1d46d02a62a75d7be4c6"
+    },
+    {
+      "path": "research/kappa-hybrid-controller/search/direct_stage_dp.py",
+      "usage": "input",
+      "git_blob": "0717a3a577fd7a4e3eea9901bb266955bdb908de",
+      "sha256": "4a457525a8c041d3e0fd2671634627d831e3c0dc2970219b11b3b2692ba32125"
+    },
+    {
+      "path": "research/kappa-rebuild/bit/complex_controller_factor.py",
+      "usage": "input",
+      "git_blob": "cb0cff7c8be5f38f2ee52201d9d0907f9dfd7947",
+      "sha256": "1de9aaf918e6a4f2f5448754c1f3c3da3b85e6257849ebd097af09859c4e5497"
+    },
+    {
+      "path": "research/query-thinned-controllers/controller.py",
+      "usage": "input",
+      "git_blob": "d4557e08cfb9fe57cc1ae4024705a72dc95f3583",
+      "sha256": "8b462d660487b1be4940357c4c7522967b1bfaede3c02b1c66109b85acae0fd2"
+    },
+    {
+      "path": "research/controller-stage-ceiling/inputs/pr4610-native.json",
+      "usage": "input",
+      "git_blob": "88fa05cb3d0b7227f85ba0c42eb427184949447d",
+      "sha256": "c6f16840b3f7bed8686ad494b479df599b18b420c239dc6167c214130b78eb64",
+      "pin": "head:6ba2f0ad1809172be7ebf04ad750592f14475dab:research/controller-stage-ceiling/inputs/pr4610-native.json",
+      "original_source_pin": "head:1eb8da6cfb35512c0cc2533413e5ca42f48e13c6:research/warp-interface-20261022/NATIVE-VALIDATION.json"
+    },
+    {
+      "path": "research/controller-stage-ceiling/inputs/pr4626-arithmetic.json",
+      "usage": "input",
+      "git_blob": "bec84f7dc990a0a892fd77fd74665d49df66d4de",
+      "sha256": "5787bae88594f8d05e1a7bbecdc98c8635523c817093b717af621ac893277d28",
+      "pin": "head:6ba2f0ad1809172be7ebf04ad750592f14475dab:research/controller-stage-ceiling/inputs/pr4626-arithmetic.json",
+      "original_source_pin": "head:e4413c43eeaacdd20be123fdd7d7add53427f028:research/helper621-warp-combination/ARITHMETIC.json"
+    },
+    {
+      "path": "research/joint-helper-lattice/CONTROLLER.json",
+      "usage": "input",
+      "git_blob": "49a2f0675819f9deeea27ed77be2c2b6ff2e87e5",
+      "sha256": "1f5d6aa267e4e66048818714b5d3b5eae17a58abe91d15deeaa34574f7391a5f"
+    }
+  ]
+}