Mister-Meeseeks · Oct 23, 2026 · Oct 23, 2026
diff --git a/research/coded-compiler-closure/PROOF.md b/research/coded-compiler-closure/PROOF.md
@@ -0,0 +1,167 @@
+# A compiler instance conditional on the coded p19 inventory
+
+Apache-2.0. Cinna Davis with substantial OpenAI Codex assistance.
+
+## 1. Exact premise and conclusion
+
+Assume an all-column native program realizes **the independent Gaussian jobs**
+and paid calls specified in Section 2, with the actual physical contracts needed
+by the chronological product and finite integer compiler. This is a premise:
+PR #4940's common-code model has no complete source-bound p19 physical replay.
+Its physical code/frame mixing and odd-denominator implementation are separate
+active investigations in Discussion #4930, comments 19139519 and 19139521.
+
+Under that premise, the credited higher-moment completion/splitting theorem
+and logarithmic compiler give a strict uniform moment at complex saving
+`0.0034 - 1/700000000`. The existing strict outer ledger accepts the planning
+endpoint `0.00339999`, using the inherited admitted BIT saving 0.0034.
+This proves a conditional compiler-arithmetic implication. It does not prove
+the premise, admit a supplier, improve the selected K, or prove multiplication
+faster. Fixed nonrecursive operations must still have the required physical,
+precision and tape implementations. No unknown module is priced at zero.
+
+The source results used here are PR #4940's declared rank model; Dugongue's
+PR #4929 native paid profile; the PR #4470 inventory/outer framework; and zxv's
+PR #4433 higher-moment and logarithmic-majorant theorem. Their exact current
+paths and immutable hashes are recorded in SOURCES.json. The core conditional
+compiler argument is Sections 2--4 of
+`research/higher-moment-strictification/README.md`; the selected p16 application
+is Sections 5--6 of `research/joint-helper-lattice/PROOF.md`.
+
+## 2. Reconstructing every declared job
+
+There are 19 odd FULL stages 1,3,...,37 and 20 thin query stages 0,2,...,38.
+Every FULL retains 408 independent helper jobs with profile
+`H={4:28,7:7,8:47,9:326}` and pays the complete coded-native profile
+`P0={1:2201,2:412,3:510,4:127,5:40}`. Both native orientation receipts agree
+with P0; this check authenticates their recorded inventory and is not a fresh
+632-column native replay.
+
+The full main pair has 224 owners of rank 153. The nine initial and nine terminal
+pairs have 224 owners per pair. Each retained thick-stage count 1,...,9 occurs
+twice, giving 448 main targets at each rank 9,17,...,73. The matched initial and
+terminal IDLEs pay 448 calls at each rank 8,16,...,72. Middle IDLEs use even
+stages and have zero retained rank. Every thin query pays 112 rank-one calls.
+Thus
+
+```
+T = 224 H153 + 448 sum_{j=1}^9 H(1+8j) + 19 H,
+P = 448 sum_{j=1}^9 H(8j) + 19 P0 + 2240 H1.
+```
+
+This totals 12008 productive fields and 68782 paid calls. Their rank masses
+are 265533 and 263517, with surplus 2016. The verifier independently reconstructs
+the interval census and compares every histogram entry against the exact
+`invoice` function of PR #4940, extracted without running its experiments.
+Deleting the 2240 thin-query children fails that equality. No coded owner is
+silently recounted as a Gaussian job: that identification is the explicit
+unproved premise in Section 1.
+
+## 3. Paid completion and splitting
+
+Take `C=17/5000`, `t=1-C`, `u=1/5`, cutoff 20, productive floor 21 and
+tensor power `v=128`. Let `T_s=sum_r T_r r^s`, and similarly P_s. The
+source higher-moment construction charges both padding short productive jobs
+and splitting large paid jobs. Its ratios are
+
+```
+alpha = P_t/T_t,
+gamma = P_(t+u)/(20^u T_t),
+delta = 21 (# productive fields)/(20^C T_t).
+```
+
+Two separate exact rational interval evaluations certify
+
+```
+alpha < 249/250,
+gamma < 97/100,
+delta < 97/100.
+```
+
+The first is the credited 192-bit outward grid engine. The second uses the
+separate positive logarithm/exponential series engine, with outward decimal
+rounding at 10^-40 and range reduction before exponentiation. Their unrounded
+intervals intersect, and each independently proves the strict inequalities.
+No floating arithmetic is used for acceptance.
+
+The exact block inequality `(97/100)^128 < 1/16` and Bernoulli give the
+fully charged normalized paid bound
+
+```
+alpha^128 + 2 gamma^128 + 2 delta^128
+ < 1/(1+128/250) + 4 (97/100)^128
+ < 125/189 + 1/4 = 689/756 < 1.
+```
+
+The actual rational bound is about 0.742442264862. Every small target is
+completed on its own existing arbitrary input; the new axes create no new
+productive owner. Every oversized paid child is split with its rounding
+surcharge. The strict integer inequality `20^64 < 21^63` separates the
+resulting paid and target ranks. The 128-fold chronological product has ambient
+`153^128`, paid rank at most `20^128` and target rank at least `21^128`.
+No product word is materialized. The same conservative bound exceeds one
+at 64 copies; this is a control, not a minimality claim for tensor power 128.
+
+## 4. Logarithmic compiler capacity and effective rank
+
+Apply the retained finite integer compiler and its normalized leaf-count
+majorant with `theta_bar=63/64` and logarithm power 140. The exact conditions are
+
+```
+2 (20^128)^64 <= (153^128)^63,
+eta = (1-C) 153^(-128 C) > (63/64)^140,
+153^(128 C) < 2^140.
+```
+
+Both interval engines certify eta in
+`(0.111620296585564378680783225123,
+  0.111620296585564378680783225124)`.
+At these fixed theta and tensor power, 139 fails the eta condition and 140
+passes. This is not a global optimum over compiler parameters.
+
+The logarithmic-majorant theorem yields
+`L(n) <= n^t (1+log2 n)^140` for integer n>=1 under its stated compiler
+premises. This is a normalized recursive leaf-count bound, not a full running
+time or precision/storage bound. The source induction uses no unknown
+multiplicative constant in this particular majorant.
+
+The desired uniform saving is `C-d`, with `d=1/700000000`. On the grid
+`H=700000000 j`, the sufficient integer-height comparison is
+
+```
+(700000000 j + 1)^140 < 2^j.
+```
+
+The first successful positive integer is j=5867, giving H=4106900000000;
+j=5866 fails. Exact integer arithmetic establishes both comparisons. The
+function `j ln(2) - 140 ln(700000000 j+1)` is strictly convex, initially
+decreasing, and eventually increasing, so it has a single positive crossing.
+The encoded uniform ambient rank is `N=2^H`; the word is algorithmically
+specified under the compiler premises and is not emitted.
+
+This also reproduces the missing-budget warning: at `v=1024` and logarithm
+power 1000, `(1-C)153^(-1024 C) < (63/64)^1000`. Reusing those constants fails
+the capacity test. The changed 128/140 instance clears it.
+
+## 5. Strict outer arithmetic and remaining obligations
+
+Set planning `k=0.00339999`, `d=1/700000000`, tested complex saving `k+7d=C`,
+uniform complex saving `k+6d`, `b=k+5d`, `a=k+4d`, `q=k+3d`,
+`epsilon=1-d`, `beta=1-3d`, `r0=d/10`, and `stop=layout=d`.
+Retain the admitted BIT saving 17/5000 and its atom exponent 1/250.
+Every one of the 54 named strict predicates and 4 functional guards is positive,
+including all nine outer cost rows. The fourth guard records the actual
+source BIT atom in addition to the three historical ledger guards.
+
+The exact BIT-cap endpoint 0.0034 fails strict BIT headroom. The old BIT
+admission, a closed uniform exponent gap and epsilon=1 each fail their named
+guards. These controls prevent replacing strict inequalities with limits.
+
+The unresolved obligations remain substantive: a correct all-width p19 coded
+caller with independent Gaussian endpoints; its actual signed port charts and
+raw dual; denominator 13 rounding and error propagation; independent helper
+returns and owned temporary cleanup; full scalar/address routing, physical
+storage and precision costs; the ordinary BIT premises; and retained compiler,
+analytic, prime-avoidance and exact-recovery contracts. This arithmetic package
+does not fill any of those gaps. Passing it determines that the stated
+compiler arithmetic need not be the limiting obstruction if they are closed.
diff --git a/research/coded-compiler-closure/README.md b/research/coded-compiler-closure/README.md
@@ -0,0 +1,87 @@
+# Compiler reserve for the declared coded p19 inventory
+
+**Exact conditional arithmetic; no new admitted K.** PR #4940 leaves its changed
+inventory's finite compiler constants unverified. This package supplies one
+strict instance: 128 chronological copies, logarithm power 140, and the complete
+54+4 outer predicates at the planning endpoint 0.00339999. The physical p19 coded
+caller, its Gaussian target identification and its nonrecursive implementation
+remain prerequisites.
+
+The result resolves only PR #4940's third open question at the level of its
+declared rank model. Its first two questions, physical frame/code binding and
+denominator 13 arithmetic, are under separate active claims in
+[Discussion #4930](https://github.com/CrocSwap/integer-mult-bounds/discussions/4930).
+No native replay, p19 operator synthesis, supplier admission, selected-frontier
+change or multiplication theorem is claimed.
+
+| Certified quantity | Value |
+| --- | --- |
+| Raw declared ambient rank | 153 |
+| Thick calls / paid thin queries | 19 / 20 |
+| Independent targets / paid calls | 12008 / 68782 |
+| Tested complex saving | 17/5000 = 0.0034 |
+| Completion/splitting tensor power | 128 |
+| Maximum paid / minimum target rank | 20^128 / 21^128 |
+| Normalized paid upper bound | less than 0.742442264862 |
+| Logarithm power / theta bound | 140 / 63/64 |
+| Uniform complex saving | 0.0034 minus 1/700000000 |
+| Sufficient compiler rank encoding | 2^4106900000000 |
+| Strict outer planning endpoint | 0.00339999 |
+
+[PROOF.md](PROOF.md) derives the entire conditional implication and the
+inventory. [RESULT.json](RESULT.json) contains the exact source-bound receipt,
+two separate rational interval evaluations, all outer predicates and failed
+semantic controls. The inherited 1024/1000 capacity test fails; 140 is the least
+passing logarithm power at the stated 128 copies and theta 63/64. No global
+parameter optimum, practical template size or full runtime bound is asserted.
+
+From the repository root, with Python 3.12 and no extra dependencies:
+
+```sh
+python3.12 -B scripts/research_package.py --package research/coded-compiler-closure
+python3.12 -I -O -B research/coded-compiler-closure/verify.py
+```
+
+Direct replay authenticates all live inputs and is read-only. The optional
+`--write` switch regenerates the arithmetic receipt. All live dependencies
+are declared in VERIFY.json; the official exporter can create a self-contained
+Git-free replay. No Lean, Docker, full selected replay or historical test suite
+is required by this package.
+
+The investigation started at canonical main `f259dabc7d70e0db8d6d36bfda888f008bbfecc1`,
+priority revision 7, selected conditional K 0.00302015. The canonical scoped claim
+is [Discussion #4930 comment 19139629](https://github.com/CrocSwap/integer-mult-bounds/discussions/4930#discussioncomment-19139629).
+Entry overlap covered 305 open PRs, 4126 Discussion records and all 6710 tracked
+local research notes. This bounded search excludes arbitrary diffs and
+unpublished work. Exact source hashes and historical selection/catalogue
+provenance are in SOURCES.json; the changed scope is recorded in TASK.json.
+
+## Open next questions
+
+- Can the actual signed p19 physical caller realize every independent Gaussian
+  target in this invoice? Start with the already claimed source-bound local
+  backward/thin pair at comment 19139519 before extending a complete word.
+  The formal scalar-code conjugation does not prove that physical binding.
+- Can its inverse recoding and full nonrecursive operations meet the retained
+  precision, storage and tape ABI? Bind the denominator 13 kernel claimed at
+  comment 19139521 to an actual recoding and its source-ordered error maps.
+  Local exact rational arithmetic is insufficient for rounded recursive work.
+
+TASK.json records the relevance, first step and blockers for each question.
+Further compiler parameter scans do not resolve these physical obligations.
+
+## Credit
+
+SethBurkart123 supplies PR #4940's coded-reverse controller model and the open
+compiler question. Dugongue/mdumitrean supplies PR #4929's center-free native
+profile. Dillon's PR #4933 supplies the physical coded interface and explicit
+unresolved target obligations. Cinna Davis's PR #4440/4470 supplies the retained
+query-thinned construction, and Cao Yifan/intqwq supplies the PR #4610 native
+word. The higher-moment and logarithmic-majorant theorem and first interval
+engine are zxv's PR #4433; the second interval engine retains zxv's source
+credit. Integer mixed flow is Jacob Alan Sussman's; the outer framework
+retains all its original contributors. Source archives remain unchanged.
+
+New work prepared by Cinna Davis with substantial OpenAI Codex assistance in
+derivation, verification and writing. Apache-2.0. No subagents, independent
+human review or proof-kernel acceptance were used or claimed.