From 774e7890e9e1379d084e711c53937cc30c8bc434 Mon Sep 17 00:00:00 2001 From: Jerry Jiaheng Chen <80299683+CubeJerry@users.noreply.github.com> Date: Wed, 11 Nov 2026 00:11:30 +0800 Subject: [PATCH] Bound retained complex and BIT backing across stratified bootstrap calls and complete stock histories --- research/stratified-owned-reserves/OVERLAP.md | 48 +++ .../PR-DESCRIPTION.md | 79 ++++ .../stratified-owned-reserves/PR-TITLE.txt | 1 + research/stratified-owned-reserves/PROOF.md | 362 ++++++++++++++++++ research/stratified-owned-reserves/README.md | 104 +++++ .../stratified-owned-reserves/RESULT.json | 79 ++++ .../stratified-owned-reserves/SOURCES.json | 84 ++++ research/stratified-owned-reserves/TASK.json | 89 +++++ .../stratified-owned-reserves/VALIDATION.md | 84 ++++ .../stratified-owned-reserves/VERIFY.json | 70 ++++ .../independent-review/RESULT.json | 101 +++++ .../independent-review/REVIEW.md | 145 +++++++ .../independent-review/independent.py | 190 +++++++++ .../stratified-owned-reserves/stack_model.py | 136 +++++++ .../test_boundaries.py | 82 ++++ research/stratified-owned-reserves/verify.py | 275 +++++++++++++ 16 files changed, 1929 insertions(+) create mode 100644 research/stratified-owned-reserves/OVERLAP.md create mode 100644 research/stratified-owned-reserves/PR-DESCRIPTION.md create mode 100644 research/stratified-owned-reserves/PR-TITLE.txt create mode 100644 research/stratified-owned-reserves/PROOF.md create mode 100644 research/stratified-owned-reserves/README.md create mode 100644 research/stratified-owned-reserves/RESULT.json create mode 100644 research/stratified-owned-reserves/SOURCES.json create mode 100644 research/stratified-owned-reserves/TASK.json create mode 100644 research/stratified-owned-reserves/VALIDATION.md create mode 100644 research/stratified-owned-reserves/VERIFY.json create mode 100644 research/stratified-owned-reserves/independent-review/RESULT.json create mode 100644 research/stratified-owned-reserves/independent-review/REVIEW.md create mode 100644 research/stratified-owned-reserves/independent-review/independent.py create mode 100644 research/stratified-owned-reserves/stack_model.py create mode 100644 research/stratified-owned-reserves/test_boundaries.py create mode 100644 research/stratified-owned-reserves/verify.py diff --git a/research/stratified-owned-reserves/OVERLAP.md b/research/stratified-owned-reserves/OVERLAP.md new file mode 100644 index 0000000000..3eaccbf2aa --- /dev/null +++ b/research/stratified-owned-reserves/OVERLAP.md @@ -0,0 +1,48 @@ +# Scope and bounded overlap review + +Scientific source: canonical `e54523517d0f03e58352e647c403a5af3e525a57`. +This is the track-60/53 ownership/recursive-interface assignment, refined +from `uniform-transfer-audit`. The other current worker studies finite +control and source-bound contexts; this package studies physical capacity, +backend stratification and simultaneous stock only. + +## Predecessor distinctions + +| Prior contribution | Reused or excluded result | New residual treated here | +|---|---|---| +| #5814 | Single-provider geometric owned-segment implication and physical bridge construction | Noncontracting cross-backend edges in a finite ordered dependency graph | +| #5829 | Whole-high child volume V/L and complete high-field retention | Composition with ordinary wrappers and the complex caller | +| #5404 | Coordinatewise historical backing, including rotating tape roles | Finite multibackend per-tape potential at reusable origins | +| #6719, reviewed in #6737–#6740 | Two-site physical shape recursion and root A/R/H generation | No new shape dispatcher; its local facts remain source inputs | +| #6879 | Old ordinary helper's reusable-origin space theorem | Exact selected .0034 backend still requires its own contract | +| #6903 | Chronological high fields and separately quantified producer absorption | No new producer; mixed backend/stock accounting remains separate | +| #6896 | Recursive physical capacity for the dim64 continuation inventory | Six-stage current selected dependency, rather than another bank census | +| #2343 | Post-borrow body-dependent stock, fit cutoff and failed equality iteration | Uniform envelope over smaller sibling widths for the current stopped stock formula | +| #4432 | #4100 stock/depth/recurrence audit | Its D is a body-depth argument; this package does not reuse its historical child-volume wording or claim a current stock discontinuity from it | +| #4957 | Conditional completed ordinary backend API edge | Per-tape historical allocation after the API's local space data are supplied | +| #4338 | Optional B2 arithmetic and frozen source-relative coupling | No new backend saving, factory or moment proof | +| #7000/#7001 application | Frozen backend DAG, rho=1/250, ambient cap134, complete current inventory and simultaneous-reservation product | An explicit substitution lemma for its Sections 3 and 6, not complete dispatcher admission | + +The generic ownership/geometric theorem, raw lifetime counts and continuation +bank high-water formula were deliberately excluded after source inspection. +The new claim is the single combination in PROOF.md: a source-refined stage +graph whose complete history and fresh stock are both billed consistently. + +## Live search coverage + +On 2026-11-10 the coordinator supplied the current PR and account snapshots, +read the canonical discussion/claim guidance, and checked active scope. +The worker also read the named predecessor bodies and used bounded all-state +GitHub PR searches (six-result cap for each query): + +* `"stratified"`: #3998 and #5249, unrelated algebraic stratifications. +* `"same-volume" "space"`: #3724, an arithmetic ordinary-rate audit. +* `"stock" "monotone"`: #6488, #5881, #2353, #4432, #2343 and #6788. +* `"backend" "historical"`: #4338, #4957, #5848, #4167, #4172 and #1075. + +The material stock/API matches are distinguished above. #4167/#4172 concern +QQ16 physical-context/action coupling, not this selected backend-space +certificate. Search result caps and indexing can omit work. No matching +stratified-stack theorem was found in the inspected scope; that is a bounded +overlap finding, not proof of global novelty. The coordinator's live sprint +updates and final upstream refresh remain the publication checkpoint. diff --git a/research/stratified-owned-reserves/PR-DESCRIPTION.md b/research/stratified-owned-reserves/PR-DESCRIPTION.md new file mode 100644 index 0000000000..5ebc544b5e --- /dev/null +++ b/research/stratified-owned-reserves/PR-DESCRIPTION.md @@ -0,0 +1,79 @@ +## Change and mathematical scope + +The selected #7000/#7001 application freezes `.0034 -> .0038507 -> .00385248` +ordinary backends and retains suspended complex/BIT parents. Backend entry +can preserve or enlarge complete bit volume, so the one-provider geometric +space argument needs an explicit composition step. + +This package proves that step as a per-tape finite-stage allocation lemma. +The least certificate is `M_i=max(c_i/(1-rho_i), c_i+a_ij M_j)` over lower +backends. It gives a complete-history bound `sum K_t+V_root sum M_root,t` +under stated local physical contracts and reusable-origin discipline. The +source-refined six-stage graph retains ordinary padding, radix embedding, +all external payload factors, parent copies, private banks and erased tails. +Sequential siblings do not add a historical-count factor; the time bill +still sums every actual occurrence. + +A monotone envelope retains the full input-dependent stopped stock and the +product of simultaneous complex/BIT reservations. An exact stock-formula +counterexample at N=2, rho=1/250 shows why endpoint-only stock is unsafe as a +generic argument: from `3215^250` to `3215^250+1` the new factor drops by +`1/(L q^1244)`. This is symbolic for eligible fixed primes. q=3 is only an +algebraic control; no selected producer or actual selected-N discontinuity +is claimed. + +**No new κ.** The selected conditional κ=.00363005817 is unchanged. This is +an enabling allocation/accounting implication for application Sections 3 +and 6, not complete dispatcher admission or discharge of owned_erasure. +All five foundational assumptions remain. + +## Novelty, exact sources and reproduction + +Base: `e54523517d0f03e58352e647c403a5af3e525a57`. SOURCES.json binds eleven +live inputs by Git blob and SHA256 and retains historical selected/card +provenance. The package extends #5814's one-provider ownership theorem, +#5829's whole-high V/L geometry and #5404's historical-tape accounting. +#6719/#6737–#6740, #6879, #6903 and #6896 retain their distinct physical +shape, helper, chronological-field and capacity results; none is republished +as a new theorem. The related stock/API questions in #2343/#4432/#4957 +are explicitly distinguished in OVERLAP.md. + +```sh +python3 -B scripts/research_package.py --package research/stratified-owned-reserves +``` + +Expected: `PASS_STRATIFIED_OWNED_RESERVES` twice, +`PASS_STRATIFIED_BOUNDARIES`, `PASS_INDEPENDENT_STRATIFIED_SPACE` twice, +and `PASS_REGISTERED_RESEARCH_PACKAGE`. +CPython 3.12, standard library only. + +The exact finite evidence covers 512 stage graphs, 12,384 independently +enumerated bounded paths, a 31-node restored-origin history, 60,600 +smaller-width stock comparisons and 118 complete product coordinates. +Separate subprocess controls reject source drift, typed receipt corruption +and omitted radix inflation, including under optimization. The written +induction supplies the universal lemma; finite checks corroborate it. +Executed checks and scope are recorded in VALIDATION.md and RESULT.json. + +A separate research worker independently reviewed the mathematical/source +interfaces and supplied a different exact checker: complete descending paths +with geometric terminal rewards and finite dual witnesses. Normal and +optimized checks pass 1,068 coordinate certificates, 4,920 descending paths +and four controls. The source/stock/history review and reviewed core hashes +are included under independent-review; this is AI-assisted review, not human +or formal-kernel acceptance. + +## Remaining obligations and credit + +The exact `.0034` all-history space contract, actual local coefficients, +emitted numerical dispatcher, source width maxima, root stock fit and +common physical precision layout remain to be supplied. No actual cell +tariff, complete runtime, unconditional multiplication theorem, independent +human acceptance or formal-kernel proof is asserted. + +Prepared for **@CubeJerry** with substantial OpenAI Codex assistance in +derivation, source audit, implementation and checking. Credit the cited +predecessors, Jose Manuel/jmbarrancoml's ordinary and stock interfaces, and +the native, delayed-cover, compiler, frame and precision lineage retained +by the selected application. New work is Apache-2.0; predecessor files and +the selected certificate remain unchanged. diff --git a/research/stratified-owned-reserves/PR-TITLE.txt b/research/stratified-owned-reserves/PR-TITLE.txt new file mode 100644 index 0000000000..77665582c5 --- /dev/null +++ b/research/stratified-owned-reserves/PR-TITLE.txt @@ -0,0 +1 @@ +Bound retained backing across the selected complex and BIT backend stack with history-safe stock reserves diff --git a/research/stratified-owned-reserves/PROOF.md b/research/stratified-owned-reserves/PROOF.md new file mode 100644 index 0000000000..73a21eceeb --- /dev/null +++ b/research/stratified-owned-reserves/PROOF.md @@ -0,0 +1,362 @@ +# Retained backing and fresh stock across the selected backend stack + +Prepared for **@CubeJerry**, with substantial OpenAI Codex assistance. +All source statements below are frozen at canonical commit +`e54523517d0f03e58352e647c403a5af3e525a57`; `SOURCES.json` records their +Git blobs and SHA256 hashes. This is a source-bound conditional allocation +lemma, not a completed dispatcher or a new multiplication exponent. + +## 1. The remaining composition question + +The selected #7000/#7001 application uses the complex core, ordinary BIT +backends frozen in the order `.0034 -> .0038507 -> .00385248`, and the latter +backends' covered kernels. Section 3 of the application explicitly makes the +ordinary dependency acyclic and retains `rho=1/250`. Section 6 requires the +product of simultaneous BIT and complex reservations and retention of +suspended parents. Neither a count of two bootstrap improvements nor the +raw peak of 43 native private lifetimes is a recursive storage bound. + +#5814 already proves a single-provider geometric ownership implication. +#5829 supplies the whole-high `V/L` child geometry; its divisor is the +fixed low-type factor **L**, not the variable row factor `W(w)=L H(w)`. +#5404 already counts coordinatewise historical backing of the continuation. +#6719 proves a literal two-site shape recursion and its own geometric bill. +#6879 supplies a source-faithful reusable-origin space construction for the +old ordinary helper. #6903 supplies the chronological field producer and its +separately quantified volume-absorption conditions. None of those results is +claimed anew. In particular, #6879 does not by itself prove a space contract +for the selected `.0034` backend. + +The new obligation treated here is composing **different simultaneously +active providers**. An ordinary map can receive the same complete bit volume +as its complex parent. A radix/row wrapper may enlarge that volume by a +fixed factor. During its execution the parent copy, private banks and return +state remain allocated. A one-provider geometric series cannot simply +replace these noncontracting edges by recursive `V/L` edges. + +We give an exact finite certificate for that stack and an explicit safe +reservation for all smaller sibling widths. The latter needs an envelope: +the raw stopped-stock formula is not generally monotone in ordinary width. +These close an accounting implication under the listed physical and source +interfaces. Local machine realization, complete generated dispatch, +precision, actual stock fit and the base backend remain separate premises. + +## 2. Model and its physical boundary + +Fix a finite set of backend stages before input size varies, ordered +`0,...,s`. Fix a finite physical tape inventory. At a stage-i invocation +of **complete encoded bit volume** V, let `c[i,t] V` bound the new relative +extent needed on tape t. It includes all public and owned copies, erased +interiors, coded blanks, delimiters, descriptors, setup and local output +staging. The same local bound must hold at every prefix, before allocation; +a bound conditional on passing the same capacity guard would be circular. + +The volume includes all external complex spectators and every component +bit. A bare number of records U must be replaced by `r(p) U`, where r(p) +is the actual encoded record width. The selected common-grid route retains +the same global p through a complex recursion; an unbounded r(p) is never +part of a fixed c. Different local encodings and markers can be accounted +by explicit fixed coefficients and interface inflation factors. + +There are two types of active-child edge: + +* Same stage i: `V_child <= rho[i] V`, where `0 <= rho[i] < 1`. +* Strictly lower stage j j ). (1) +``` + +An empty lower-edge maximum leaves only the first term. All values are +finite rationals when c,rho,a are rational; they are computable without +executing an input-dependent call tree. + +**Theorem 1.** Every finite properly nested execution satisfying Section 2 +has + +``` +retained_total <= sum_t K[t] + V_root * sum_t M[root,t]. (2) +``` + +The bound holds over the complete history, not just at the point of maximum +live content, and is independent of the number of completed siblings. For +successive root calls at the same origins it holds with the maximum root +volume (or the maximum of the corresponding per-tape root bounds) and K +measured once at sequence entry. + +**Proof.** From (1), `c[i,t]+rho[i] M[i,t] <= M[i,t]` and +`c[i,t]+a[i,j] M[j,t] <= M[i,t]`. Strong induction on the length of any +finite active call path therefore bounds its sum of local tape extents by +`M[i,t] V`. Equivalently, telescope the remaining potential along that path. +This is a proof for arbitrary permitted edge choices, including every +finite termination pattern; it does not assume termination of the actual +numerical program. + +At a push, the absolute child origin is the parent's origin plus its actual +parked local extent and delimiter. That extent is no larger than the local +coefficient already counted. At any write, its coordinate is consequently +bounded by the path sum to the current invocation. Pop and erasure stay +inside previously bounded extents. A later sibling restores the earlier +origin and uses that same bounded interval; it does not append at the +historical high-water mark. A nonsegmented bridge has its fixed origin and +is bounded by the local term of the node using it. Thus every address ever +visited on tape t lies in a fixed interval bounded by the right side of (2). +Take the union over time **on each tape first**, then sum. Extents attained +on different sibling paths remain counted. This proves the theorem. The +same interval argument with a history-wide maximum proves the last claim. + +**Sharpness of the relaxation.** Formula (1) is the least nonnegative +coordinatewise solution of its Bellman inequalities. A same-stage path +of arbitrarily many edges approaches `c/(1-rho)`. Taking an immediately +descending edge and an arbitrarily near-extremal lower path approaches +`c+a M_lower`. Induction on stages proves minimality. This is sharpness +for the abstract real-volume path relaxation, not a claim that an actual +integer-sized supplier attains every local bound or that (2) is optimal +physical storage. Fixed finite integer histories still obey (2). + +The exact fraction calculation in `stack_model.py` is a certificate +constructor. Written induction supplies the universal statement. Independent +finite path enumeration and interval histories only corroborate it. + +## 4. Actual selected source graph and complete local costs + +Use the following six stages. `B0` is the selected completed `.0034` +interface. `Oi` is the ordinary wrapper at the ith new bootstrap stage; +`Ki` is its covered weighted kernel. `C` is the complex uniform core. +The source context fixes `O1=.0038507`, `O2=.00385248`, and the same weaker +`.00376669` BIT premise in the complex outer ledger. No saving is changed. + +| Stage | Lower calls | Same-stage contraction | Source and qualification | +|---|---|---|---| +| B0 | Internal implementation kept in its own contract | Absorbed into B0 coefficient | Application Section 3; a relative linear-space certificate for this exact interface remains a premise. The old helper in #6879 is narrower. | +| K1 | B0, factor at most 4 for a radix atom's binary embedding | `1/L1 <= 1/2` | Delayed-cover whole-high theorem and stopped-product paid atom interface; the complete target/spectator fibre remains present. | +| O1 | K1 and B0, factors at most `P1=2q1^2` | No self edge | One binary-to-radix enlargement below q1² and one row padding below two; the two completed body calls are sequential. Residual/high-part/finite-cutoff predecessor calls are included. | +| K2 | O1, factor at most 4 | `1/L2 <= 1/2` | The frozen `.0038507` predecessor is used for ordinary maps and atoms; a same-stage ordinary recursive call is not silently substituted. | +| O2 | K2 and O1, factors at most `P2=2q2^2` | No self edge | The same ordinary wrapper at the second frozen bootstrap. | +| C | O2, factor at most 1 at its binary entry | `1/W_C <= 1/2` | Complete complex fields passed to ordinary chunk interchange in compact movement; internal O2 padding is already its own edge. | + +L1,L2 are the final compiled low-type/role divisors, not 134 and not +`W(w)=L q^(N^2(w-1))`. W_C is the final complex productive width, not the +raw 23,392. The new current BIT ambient cap **134** is a source pin; it +does not determine any of these final compiler widths or tape coefficients. +The conservative 1/2 contractions require only their retained lower bound +two. The larger exact divisors can be used in (1) when actually supplied. + +The complete encoded volume at a lower entry contains every upper spectator +and record bit. The upper suspended copy and its private pools remain in +`c[parent,t] V`; the child's copy, output staging and scratch are charged +again in its own local coefficient. Equal mathematical values are not +merged physical storage. Thus the graph does not hide payload duplication. + +The factors in the table are sufficient geometric bounds, not new finite +runtime tariffs. An implementation using larger extra encoding factors +must put them in a or in its local c before applying the theorem. The +factors 4 and 2q² come from the retained source interfaces; no assertion +that q=3 is a sufficient source cover prime is made by small controls. + +For example, if every local coefficient on one tape is one, and the +conservative contractions are 1/2, (1) gives + +``` +M[B0]=1, M[K1]=5, +M[O1]=1+5P1, M[K2]=5+20P1, +M[O2]=1+5P2+20P1P2, M[C]=2+5P2+20P1P2. (3) +``` + +These are a transparent symbolic unit-coefficient example, **not** the +selected program's numerical cell bound. At q1=q2=3 the example is 6572. +Actual source constants, record encodings, private inventories, descriptor +bounds and the B0 certificate must replace those ones. The source's +`51J+U+O_aux`, `237J_B+U_B+O_B,aux`, and all compiler and primitive +workspace belong in those coefficients. Raw `10^9` is not reused. + +The extra administrative **time** is the occurrence sum +`sum_actual_invocations c_time[type] V_invocation`. All same-level paid +call multiplicities and lower-backend call counts remain in that sum. +At most twelve ordinary swaps in a compact-control macro do not mean twelve +simultaneously active lower stacks, but they are twelve time occurrences. +The existing source recurrence must fund this sum. A root-space bound is +not a proof of root-linear running time or a new κ. + +## 5. A history-safe stock envelope + +For one frozen ordinary backend, write + +``` +w(e) = ceil(e^rho), 0 < rho < 1, +H(w) = q^(N^2(w-1)), W(w) = L H(w), L=B |GL_N(F_q)|, +D(e) = 2 + ceil(log_N(max(1,ceil(e/w(e))))), +S(e) = W(w(e))^D(e) * S_old(e). (4) +``` + +The selected new stages use rho=1/250. The compiler constants N>=2, +B>=1 and the eligible prime q are fixed before e varies. `S_old(e)` is +the predecessor's own complete reserve and is not silently set to one. +Equation (4) is the application Section 3 / delayed-cover source stock +prescription, with the generous depth offset used by the current review. + +Suppose every invocation of that backend in one enclosing call has `e<=E`. +Supply a justified bound `S_old(e)<=S_old_bar(E)` over the same domain. +Define + +``` +w_bar(E)=ceil(E^rho), +D_bar(E)=2+ceil(log_N(max(1,E))), +S_bar(E)=[L q^(N^2(w_bar(E)-1))]^D_bar(E) * S_old_bar(E). (5) +``` + +**Theorem 2.** `S(e)<=S_bar(E)` for every positive integer e<=E. If the +predecessor envelope is nondecreasing, (5) is nondecreasing. For fixed +template constants its additional logarithmic size is +`O(E^rho log(2E))`; in particular it is o(E). This is a sufficient envelope, +not a sharp maximum of (4). + +**Proof.** Atom width is nondecreasing. Also `ceil(e/w(e))<=e<=E`, so +`D(e)<=D_bar(E)`. Both the base and the exponent in the new stock factor +are bounded by (5), and their bases are at least one. Multiply the inherited +predecessor inequality. The logarithmic statement follows by taking logs +and using `w_bar(E)<=E^rho+1`. These inequalities do not assume monotonicity +of the raw quotient `ceil(e/w(e))`, the raw depth, or their product. ∎ + +The actual source width bound E must be supplied by the caller; neither a +largest observed test width nor the number of bootstrap levels supplies it. +If different stages have different maxima E_i, use a separate envelope for +each. The asymptotic statement permits enlargement of a fixed threshold +when the enclosing source has the requisite strict stock-fit margins. It +does not prove those margins, choose their constants, or establish actual +input-dependent root generation. + +### Why replacing the envelope by the endpoint is not automatic + +Keep rho=1/250 and set the **stock-formula dimension** N=2. Put +`k=3215`, `e0=k^250`, `e1=e0+1`. Exact integer inequalities give + +``` +w(e0)=3215, w(e1)=3216, +2^2901 < ceil(e0/3215) <= 2^2902, +2^2900 < ceil(e1/3216) <= 2^2901, +D(e0)=2904, D(e1)=2903. +``` + +For the new stock factor alone (or constant S_old), + +``` +S(e1)/S(e0) = L^(-1) q^(4*(2904-3215)) + = 1/(L q^1244) < 1. (6) +``` + +This calculation holds for **every** fixed eligible q and positive L of +the stated form; it does not rely on an inadequately small cover prime. +Taking B=2,q=3 gives L=96 only as a finite algebraic control. We do not +claim that these parameters meet a supplier's moment, prime-avoidance or +admission conditions, or that the actual selected enormous N has this +discontinuity. Equation (6) refutes a blanket monotonicity justification +based solely on the displayed stock formula. For the selected N, (5) +remains valid whether or not any discontinuity occurs. + +## 6. Simultaneous reservations and source-preserving reuse + +Let S_C be a complete reserve for the current complex recursion, and let +the simultaneously callable ordinary stages have bounds `S_bar_i(E_i)`. +These are numerical row cardinalities, including their internal fresh +depth stock. A safe independent reserve is + +``` +S_total = S_C * product_i S_bar_i(E_i). (7) +``` + +One may avoid duplicating a predecessor factor already included in an +enclosing S_bar only after proving which exact coordinates it supplies. +Equation (7) intentionally allows overcounting; it never removes an +unidentified factor because a similarly named predecessor appears twice. +The `.0034` backend's internal reserve remains explicitly present. + +For Q>=S_total, pad once to `P=S_total ceil(Q/S_total)<2Q`. Euclidean +division identifies `[P]` with a slab factor and the Cartesian product of +all reservation coordinates. Assign each stage its own coordinate factor. +A stage's fresh fields consume only its own remaining stock; all upper and +other-stage factors are external spectators. On invoking a lower stage, +the complete upper factor is retained in the lower physical field and is +never relabelled as a free fresh lower digit. The #5829 whole-high map +moves that stage's exposed high coordinate into its body while fixing the +other factors; it is a bijection and changes no other reservation. + +Assuming each completed call restores its full assigned row endpoint, +sequential sibling calls reuse the same coordinates. They do not require +a product over historical invocations. Concurrent ancestor stages still +require their full product. This is the exact distinction needed by the +application's simultaneous-reservations clause. A maximum of two nontrivial +cardinalities has too few points for their independent Cartesian product. + +This argument concerns row allocation and complete-fibre preservation. +It does not identify that row range inside an already materialized physical +input, prove it fits the compact-control/precision parameters, synthesize +the chosen prime, or justify deleting padded rows at intermediate cuts. +Only a completed row-restoring endpoint permits restriction to the genuine +input range. Those source obligations stay explicit. + +## 7. Necessary failure controls + +1. If a same-stage edge has factor one and positive local extent, a chain + of h nodes keeps h copies of that extent. There is no uniform bound + proportional to root volume independent of h. A cycle of stage-changing + edges with product at least one has the same obstruction. The actual + frozen bootstrap DAG excludes such a cycle; completed backend names + alone do not establish this. +2. If a shrinking child drops an external factor before defining its local + V, the same source packet can have an arbitrarily large ratio of encoded + bits to the falsely quoted V. The Bellman certificate then prices a + different interface. +3. If siblings append after high-water backing instead of restoring the + segment origin, h equal children retain h blocks despite unit path depth. +4. On distinct tapes, historical maxima can be reached on different + siblings. `max_time(sum live)` is insufficient; (2) sums per-tape + historical bounds. K at entry cannot be discarded after erasure. +5. Equation (6) rejects endpoint-only stock reuse. Replacing actual + `D(e)` by the two frozen bootstrap improvements also fails as e grows. + +These are scoped countermodels to missing hypotheses, not observed failures +of the admitted #7000 construction and not multiplication lower bounds. + +## 8. Consequence and remaining work + +The current six-stage dependency pattern has a finite exact stack +certificate once its local relative-space interfaces are supplied. Every +complete upper payload copy, padding factor, private bank, suspended frame, +fresh stock coordinate and retained historical tail has a place in one +common bill. No extra logarithm of execution depth or count of completed +siblings is required for backing. The source-compatible envelope (5) +avoids an unjustified endpoint-monotonicity step in supplying that bill. + +The next concrete task is to instantiate c[i,t], E_i, the `.0034` backend +history contract and the common root row/precision layout for an emitted +selected dispatcher. #6719 and #6903 supply partial implementation pieces, +not that complete caller. No numerical upper tariff, complete runtime, +global `owned_erasure` discharge, new κ, independent human acceptance or +formal-kernel proof is claimed. All five selected assumptions remain. diff --git a/research/stratified-owned-reserves/README.md b/research/stratified-owned-reserves/README.md new file mode 100644 index 0000000000..cfacccf792 --- /dev/null +++ b/research/stratified-owned-reserves/README.md @@ -0,0 +1,104 @@ +# Bound backing and stock across the selected backend stack + +**Conditional allocation lemma and scoped counterexample; no new κ.** +The complete selected bound remains conditional at κ=.00363005817, with all +five foundational assumptions retained. This package supplies an accounting +implication needed to compose the source's owned streams; it does not emit +the complete selected numerical dispatcher. + +## Result and relevance + +The #7000/#7001 application freezes the ordinary dependency chain +`.0034 -> .0038507 -> .00385248`, while its complex caller keeps suspended +parent fields. Crossing to a lower backend need not reduce complete bit +volume: binary/radix wrappers can enlarge it. The geometric single-provider +argument therefore requires a separate composition step. + +[PROOF.md](PROOF.md) gives a per-tape certificate for that step. If local +relative extents are `c[i,t] V`, same-stage children shrink by `rho[i]<1`, +and a lower-stage edge has volume factor `a[i,j]`, the least certificate is + +``` +M[i,t] = max(c[i,t]/(1-rho[i]), c[i,t]+a[i,j]M[j,t] for lower j). +``` + +At reusable origins the complete history has retained backing at most +`sum K[t] + V_root sum M[root,t]`, including parents, duplicate payloads, +private pools and erased tails. Completed sibling count creates no extra +factor. The application refines to six stages, with ordinary wrapper +inflation at most `2q_i²`, atom embedding at most four, and conservative +same-stage contraction one half. Local coefficients and the exact `.0034` +backend's all-history contract remain explicit premises. + +For fresh stock, the package supplies a monotone envelope for every smaller +width, retaining the predecessor reserve and the product of simultaneous +complex/BIT reservations. A symbolic counterexample at stock-formula +dimension N=2 and rho=1/250 proves why the raw endpoint stock alone cannot +justify reuse: between `3215^250` and `3215^250+1`, its new factor drops by +`1/(L q^1244)`. This holds symbolically for every eligible fixed prime; the +small q=3 control is not an admitted producer. No discontinuity is claimed +at the actual selected enormous dimension. + +This extends #5814's single-provider allocation, #5829's whole-high `V/L` +geometry, #5404's historical-tape accounting, #6719's physical shape +recursion, #6879's old-helper space contract and #6903's chronological +fields. It does not reprove those results. [OVERLAP.md](OVERLAP.md) records +the boundary with #6896 and other stock/backend work. + +## Evidence and reproduction + +Scientific base: `e54523517d0f03e58352e647c403a5af3e525a57`. +[SOURCES.json](SOURCES.json) pins eleven live sources by Git blob and SHA256, +plus the historical task catalogue and selected record. Later priority +changes do not alter this frozen scope. From repository root, on CPython +3.12 using only the standard library: + +```sh +python3 -B scripts/research_package.py --package research/stratified-owned-reserves --check-only +python3 -B scripts/research_package.py --package research/stratified-owned-reserves +``` + +Expected markers: `PASS_STRATIFIED_OWNED_RESERVES` twice, +`PASS_STRATIFIED_BOUNDARIES`, `PASS_INDEPENDENT_STRATIFIED_SPACE` twice, +and `PASS_REGISTERED_RESEARCH_PACKAGE`. +The verifier independently enumerates 12,384 bounded paths in 512 stage +graphs, checks exact history coordinates, 60,600 smaller-width stock cases, +the symbolic discontinuity and 118 complete product coordinates. Separate +subprocess controls corrupt a real source, a typed receipt and a backend +inflation edge and require rejection. Ordinary and optimized Git-free +replays run from disposable copies of the declared source closure. + +Finite checks corroborate the written universal induction; they do not +prove source admission or global stock fit. The verifier is read-only by +default. `--emit` prints a proposed receipt without installing it. +[RESULT.json](RESULT.json) and [VALIDATION.md](VALIDATION.md) record the +exact finite outcomes and executed commands. + +A separate research worker independently reviewed the source application and +proof. Its [review](independent-review/REVIEW.md) and independently written +checker use complete descending paths with exact geometric terminal rewards, +rather than the author's bounded-depth enumeration. Both modes pass 1,068 +coordinate certificates, 4,920 descending paths and four controls, binding +the reviewed proof/model hashes. This is separate AI-assisted review, not +independent human or formal-kernel acceptance. + +## Open next questions + +The structured questions in [TASK.json](TASK.json) target two residuals. +First, instantiate every local per-tape coefficient and the `.0034` +relative-history contract for an emitted selected dispatcher, using #6719 +and #6903 only at their actual interfaces. Second, supply the actual width +maxima and common root row/precision layout, then prove the simultaneous +stock product fits. This package provides the composition rule once those +data are supplied; it proves neither input-dependent generation nor a new +complete runtime. The time bill remains the sum over all actual occurrences. + +## Credit + +Prepared for **@CubeJerry** with substantial OpenAI Codex assistance in +source study, mathematical derivation, implementation and checking. Credit +the cited predecessor packages, the retained Jose Manuel/jmbarrancoml +ordinary/stock interfaces, and the native, delayed-cover, compiler, frame +and precision authors credited in the frozen application review. No +predecessor evidence is modified or copied. New work is Apache-2.0; +independent human or formal-kernel acceptance is not claimed. diff --git a/research/stratified-owned-reserves/RESULT.json b/research/stratified-owned-reserves/RESULT.json new file mode 100644 index 0000000000..ff58801bc2 --- /dev/null +++ b/research/stratified-owned-reserves/RESULT.json @@ -0,0 +1,79 @@ +{ + "history": { + "controls": [ + "append-only sibling", + "entry backing omitted", + "external factor omitted", + "aggregate-live maximum substituted" + ], + "false_max_live": 80, + "historical_extents": [ + 126, + 251, + 373 + ], + "path_extents": [ + 124, + 248, + 372 + ], + "reference_nodes": 31, + "role_rotating_history": 160 + }, + "reservations": { + "complete_product_coordinates": 118, + "controls": [ + "max stock substituted for product", + "external stage coordinate dropped" + ] + }, + "schema": 1, + "scope": "conditional allocation accounting; no new kappa", + "source": { + "backend_savings": [ + ".0034", + ".0038507", + ".00385248" + ], + "live_pins": 11, + "raw_bit_ambient_cap": 134, + "source_application_sha256": "4501502c2ceb9759b20372435fe4beb51082c5a5e2910c1fd5dbe6edca415055", + "source_rho": "1/250" + }, + "stack": { + "bounded_path_comparisons": 12384, + "controls": [ + "same-stage noncontraction", + "upward edge / cycle", + "seven same-volume frames exceed 2V" + ], + "graphs": 512, + "selected_bounded_paths": 351, + "unit_example": { + "B0": 1, + "C": 6572, + "K1": 5, + "K2": 365, + "O1": 91, + "O2": 6571 + } + }, + "stock": { + "controls": [ + "raw endpoint stock substituted", + "bootstrap count substituted for depth" + ], + "counterexample_scope": "stock formula at N=2; no selected-instance or prime admission claim", + "depths": [ + 2904, + 2903 + ], + "discontinuity_k": 3215, + "e0_description": "3215^250", + "e1_description": "3215^250+1", + "monotonicity_checks": 1188, + "ratio": "L^-1*q^-1244", + "rho": "1/250", + "smaller_width_checks": 60600 + } +} diff --git a/research/stratified-owned-reserves/SOURCES.json b/research/stratified-owned-reserves/SOURCES.json new file mode 100644 index 0000000000..e068d0fd71 --- /dev/null +++ b/research/stratified-owned-reserves/SOURCES.json @@ -0,0 +1,84 @@ +{ + "schema_version": 1, + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "75d77b328ea02ded535e7f23aee5b1e55d0bb1a8", + "sha256": "154c3d30455d778fd3343b6b4851f0fa4665f0f7625b0adb3675e2bafbbf6bf1" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "docs/research/pr-intake-evidence/pr7000-application/PROOF-REVIEW.md", + "usage": "input", + "git_blob": "3dd1af2285e597676725e85ad4f65e7ad326d695", + "sha256": "4501502c2ceb9759b20372435fe4beb51082c5a5e2910c1fd5dbe6edca415055" + }, + { + "path": "notes/compact-control-movement.tex", + "usage": "input", + "git_blob": "06b6a9ef24245ac7b724c53a204635415b402357", + "sha256": "b963c3d2f4e1b7059aa289bb4b4ac89b688920bcf42f5b20d7698cdef0132cc6" + }, + { + "path": "notes/stopped-product-interface.tex", + "usage": "input", + "git_blob": "20c44ce4866fa972ce64365dcf365b1659a83050", + "sha256": "454a8f3924afc26e575b2a8cec6d0860397cb7f2dc431f3ba63fb8a7142cc96b" + }, + { + "path": "research/continuation-retained-backing/PROOF.md", + "usage": "input", + "git_blob": "179f4726a8bad426d2f691490b2c47dda3aebd81", + "sha256": "00995d2b056eaa943fa0ced9bdfdc030a7c5e93bb1b499e53d4083d99b84cc25" + }, + { + "path": "research/delayed-cover-batch-allocation/PROOF.md", + "usage": "input", + "git_blob": "32303307679612e33f8f6a3416b2b48c0cb5c53e", + "sha256": "adab55de97f1336a58922b2fc92782af335a94a36cbaae34d6d3314d18a882ea" + }, + { + "path": "research/delayed-cover-chronological-fields/PROOF.md", + "usage": "input", + "git_blob": "a564a45ff35314cc2fe23e43274036d84e771d43", + "sha256": "9571ecdf53f30bafb96d6acfdad2add756f0f900c6d6634fbd0a7f3dceaffd0e" + }, + { + "path": "research/delayed-cover-physical-batch-routing/recursion/core/PROOF.md", + "usage": "input", + "git_blob": "d18ec7c03fadc752dbf4f5636ec777680ad07323", + "sha256": "09e3fcc919afc65fc47a9f1dbe3597320c1a2ff1408e2c1170913ea3a4d72dda" + }, + { + "path": "research/kappa-rebuild/bit/DELAYED-COVER-BRIDGE.md", + "usage": "input", + "git_blob": "a58774e237c9362869a60a22bda35be09fb85872", + "sha256": "9731b93026717f5fa15851e3633cbb4bdc76eba2bffb9d6b4a3b69f7dd502443" + }, + { + "path": "research/ordinary-bit-retained-space/PROOF.md", + "usage": "input", + "git_blob": "d8fdae6afe4c84863730bf1be79015861bbb885d", + "sha256": "72f317eacb9db5667941ceda6557bb2b8efde19f451c69d197c736f03f405897" + }, + { + "path": "research/selected-owned-dispatch/ALLOCATION-THEOREM.md", + "usage": "input", + "git_blob": "b026ff11ceb626ff1dda30cb517eb63c0e47baa0", + "sha256": "49053c4c3568a20ffa075a6e6c3cc960eac954709072864f4ab39ac09be84897" + }, + { + "path": "research/selected-owned-dispatch/BINDING-STATUS.md", + "usage": "input", + "git_blob": "64806e5add98faa1ee36082c0e8ca93e5ac2d399", + "sha256": "ff2c3e7397f738f6d46a3a47820e94d04d1ad616b72ec14f5c81aec823dd3854" + } + ] +} diff --git a/research/stratified-owned-reserves/TASK.json b/research/stratified-owned-reserves/TASK.json new file mode 100644 index 0000000000..4d5085e801 --- /dev/null +++ b/research/stratified-owned-reserves/TASK.json @@ -0,0 +1,89 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 8, + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "original_card": { + "id": "uniform-transfer-audit", + "question": "Can one of the selected record's five inherited assumptions be proved at its actual caller?", + "starting_points": [ + "docs/research/current-priorities.md", + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md" + ], + "methods": [ + "Construct and independently check one source-bound instance of the stated first experiment.", + "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change." + ], + "acceptance_gate": "Identify the proposition and what would change downstream; do not equate a finite replay with a universal proof.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.", + "scope": "Source-bound orientation only, not a supplier replay or theorem proof." + }, + "first_experiment": "Choose one assumption ID (native_all_columns, owned_erasure, compiler, precision_tape, analytic_recovery), one quantified implication and exact dependency closure. Check current handoffs, including #5625 row reentry and #5707 root-prefix lowering, without treating their partial scope as the whole theorem. Prove or falsify that implication with a caller-bound argument; stop at the chosen obligation. Finite tests or root digits do not discharge an all-size statement.", + "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.", + "allowed_variations": [ + "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes." + ], + "scope_change_triggers": [ + "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.", + "Treating an archived proposal or local numerical pass as complete supplier admission." + ], + "overlap_terms": [ + "native_all_columns", + "owned_erasure", + "compiler", + "precision_tape", + "analytic_recovery" + ], + "existing_checks": [ + { + "scope": "PR #4100: proposed unconditional construction and finite checks, without independent acceptance.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Independent proof audit of one caller-bound all-size implication; all other premises remain explicit.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.", + "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.", + "status": "reviewed", + "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137", + "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + } + ] + }, + "scope_status": "refined", + "actual_scope": "Prove a per-tape complete-history allocation certificate for the current selected complex / ordinary-wrapper / covered-kernel backend DAG, with a safe stock envelope over all smaller sibling widths.", + "scope_change_reason": "The original uniform-transfer card is narrowed to the mixed-provider owned_erasure and precision_tape accounting implication at application Sections 3 and 6. Already proved generic ownership, whole-high geometry and raw bank counts are excluded.", + "bottleneck_link": "Same-volume or padded cross-backend calls preserve suspended parent copies. Their physical backing and fresh stock must compose before local space interfaces can discharge an actual selected dispatcher obligation.", + "budget_minutes": 140, + "stop_rule": "Stop after proving and independently corroborating the finite-stage history certificate and stock envelope, binding the actual six-stage source graph, and recording unresolved local coefficients/base-backend/stock-fit premises. Do not widen into dispatcher implementation or a new kappa claim.", + "outcome": "partial", + "evidence": "PROOF.md gives two universal conditional lemmas and a symbolic stock-formula counterexample. RESULT.json records independent bounded path, interval-history, smaller-width and Cartesian-stock checks. test_boundaries.py executes corrupt-input rejection controls.", + "author": "Prepared for @CubeJerry", + "ai_assistance": "Substantial OpenAI Codex assistance in source inspection, derivation, code, exact checks and packaging; parent orchestration supplies separate review/publication. No independent human or proof-kernel acceptance claimed.", + "open_questions": [ + { + "question": "Can the actual selected six-stage dispatcher supply every local per-tape coefficient and the exact .0034 backend relative-history space contract?", + "why_it_matters": "These are the explicit unresolved premises before the new Bellman certificate can become an actual selected owned-erasure space bound.", + "first_step": "Bind one .0034 entry and its real numerical continuation to reusable physical origins, retaining full spectators, primitive scratch and all historical backing; then inventory c[i,t] at emitted source cuts.", + "blocked_by": "No complete current numerical dispatcher or exact .0034 all-history space certificate is supplied by this package; #6879 proves a narrower old-helper contract." + }, + { + "question": "What actual per-stage width maxima and common root layout make the simultaneous monotone stock product fit?", + "why_it_matters": "The envelope removes an endpoint-monotonicity shortcut, but a physical caller still needs enough borrowed rows and a compatible common precision format.", + "first_step": "Trace e_i from the current compact-control and radix entries, set a justified E_i, then substitute S_bar_i(E_i) in the source stock-fit and root producer inequalities.", + "blocked_by": "Actual emitted producer/caller mapping and source-specific stock-fit margins remain separate premises." + } + ] +} diff --git a/research/stratified-owned-reserves/VALIDATION.md b/research/stratified-owned-reserves/VALIDATION.md new file mode 100644 index 0000000000..88c5fe5f54 --- /dev/null +++ b/research/stratified-owned-reserves/VALIDATION.md @@ -0,0 +1,84 @@ +# Validation and evidence boundary + +Executed on Linux x86_64, CPython 3.12.14, standard library only, +2026-11-10. Scientific base: +`e54523517d0f03e58352e647c403a5af3e525a57`. + +## Registered checks + +From repository root: + +```sh +python3 -B scripts/research_package.py --package research/stratified-owned-reserves --check-only +python3 -B scripts/research_package.py --package research/stratified-owned-reserves +``` + +The metadata and eleven live byte/Git-blob pins passed. The full registered +replay passed both ordinary and optimized exact checks and the separate +subprocess boundary suite. The deterministic mathematical receipt digest +in both modes was +`8127af69796828d95423a5ecdbc1e282a06b9e82784e30122d02e89d5606ac17`. +The final marker was +`PASS_REGISTERED_RESEARCH_PACKAGE research/stratified-owned-reserves outcome=partial`. + +The exact finite counts are in RESULT.json: + +* 512 finite stage graphs, 12,384 independently enumerated paths, plus 351 + bounded source-refined six-stage paths and a separate three-tape weighting. +* A 31-node complete sibling history with restored origins and separately + retained maxima; controls show why entry backing, external factors and + coordinatewise historical maxima cannot be omitted. +* 60,600 smaller-width stock checks, 1,188 envelope monotonicity checks and + the exact symbolic N=2/rho=1/250 discontinuity with depths 2904 and 2903. +* 118 complete Cartesian reservation coordinates, with inverse maps, + stage-local changes/restoration and one-time row padding. + +The independent bounded path checker does not use Bellman updates to expand +routes. The written induction proves arbitrary finite histories. Small graph +and stock checks are corroboration rather than a universal proof by search. +The q=3 unit-coefficient and GL2 examples are algebraic controls only. + +## Rejection and isolation + +`test_boundaries.py` creates a disposable mirror containing the package and +exactly its eleven declared source inputs. It executes successful normal +and optimized Git-free replays, then independently corrupts three real +inputs and requires the appropriate failing subprocess result: + +1. The receipt schema integer `1` is changed to Boolean `true`; Python's + untyped equality would identify them, but complete typed canonical JSON + equality rejects, also with `-O`. +2. A source byte suffix is appended; its SHA256 gate rejects. +3. A radix embedding factor four is replaced by one; the source-refined + graph certificate comparison rejects with `-O`. + +The original bytes are restored between controls and a final good replay +passes. The package's normal verification is read-only. It compiles its own +model directly from source bytes rather than loading an existing bytecode +cache; the generic registered runner also supplies its isolated cache. + +## Unrun and unresolved + +No full selected supplier replay, emitted numerical dispatcher, huge final +compiler instance, hosted CI, Lean/kernel proof or independent human review +was executed or claimed. The exact .0034 base space contract, actual local +coefficients, width maxima, source root generation, common format and stock +fit remain premises as stated in PROOF.md. No physical tape tariff, complete +running-time improvement or changed κ is inferred from these checks. + +## Separate review + +The analytic research worker independently reviewed the proof and selected +source boundaries, then implemented a descending-path/geometric-tail checker +without the author's bounded-depth enumeration. Its portable review, exact +receipt and code are included in independent-review. The receipt binds +PROOF.md and stack_model.py by SHA256, eleven live scientific source inputs, +1,068 coordinate certificates, 4,920 descending paths and four controls. +Normal and optimized replays pass. Historical catalogue/selected provenance +remains bound by the generic metadata validator, rather than requiring those +working files never to change after this frozen scientific base. + +The author checkpoint efb348fbb7cd39b5c8e9b41043774e7f468502bb passed the +committed-byte/mode preflight for all 24 then-existing package/live-input +files. The integrated review receives fresh registered and committed-byte +checks before publication; remote publication is a separate coordinator gate. diff --git a/research/stratified-owned-reserves/VERIFY.json b/research/stratified-owned-reserves/VERIFY.json new file mode 100644 index 0000000000..c2e0838175 --- /dev/null +++ b/research/stratified-owned-reserves/VERIFY.json @@ -0,0 +1,70 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "docs/research/pr-intake-evidence/pr7000-application/PROOF-REVIEW.md", + "notes/compact-control-movement.tex", + "notes/stopped-product-interface.tex", + "research/continuation-retained-backing/PROOF.md", + "research/delayed-cover-batch-allocation/PROOF.md", + "research/delayed-cover-chronological-fields/PROOF.md", + "research/delayed-cover-physical-batch-routing/recursion/core/PROOF.md", + "research/kappa-rebuild/bit/DELAYED-COVER-BRIDGE.md", + "research/ordinary-bit-retained-space/PROOF.md", + "research/selected-owned-dispatch/ALLOCATION-THEOREM.md", + "research/selected-owned-dispatch/BINDING-STATUS.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Exact pinned-source/backend graph, independent bounded paths, history coordinates, stock envelope and symbolic discontinuity, complete reservation product; typed RESULT equality." + }, + { + "argv": [ + "{python}", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Identical source and mathematical checks with assertions disabled; no assertion-dependent gate." + }, + { + "argv": [ + "{python}", + "-B", + "{package}/test_boundaries.py" + ], + "timeout_seconds": 60, + "checks": "Normal and optimized Git-free source mirror; real subprocess rejection of source, typed-receipt and edge-inflation corruption." + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/independent-review/independent.py" + ], + "timeout_seconds": 60, + "checks": "Separate reviewer exact descending-path/geometric-tail certificate, history model and stock calculation; reviewed core hashes and eleven live source pins." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/independent-review/independent.py" + ], + "timeout_seconds": 60, + "checks": "Separate reviewer exact descending-path/geometric-tail certificate, history model and stock calculation; reviewed core hashes and eleven live source pins." + } + ] +} diff --git a/research/stratified-owned-reserves/independent-review/RESULT.json b/research/stratified-owned-reserves/independent-review/RESULT.json new file mode 100644 index 0000000000..9859534130 --- /dev/null +++ b/research/stratified-owned-reserves/independent-review/RESULT.json @@ -0,0 +1,101 @@ +{ + "status": "PASS_INDEPENDENT_STRATIFIED_SPACE", + "seed": 20261110, + "coordinate_certificates": 1068, + "descending_paths_checked": 4920, + "selected_graphs": [ + { + "q1": 3, + "q2": 3, + "root": [ + [ + 8075, + 1 + ], + [ + 14647, + 2 + ], + [ + 7073, + 1 + ] + ] + }, + { + "q1": 5, + "q2": 7, + "root": [ + [ + 119179, + 1 + ], + [ + 217671, + 2 + ], + [ + 316163, + 3 + ] + ] + }, + { + "q1": 101, + "q2": 103, + "root": [ + [ + 10389690763, + 1 + ], + [ + 19047589575, + 2 + ], + [ + 27705488387, + 3 + ] + ] + } + ], + "unit_root": 6572, + "history": { + "entry": [ + 7, + 11 + ], + "retained": [ + 20, + 27 + ], + "live_peak": 37 + }, + "stock_counterexample": { + "k": 3215, + "rho": [ + 1, + 250 + ], + "N": 2, + "depths": [ + 2904, + 2903 + ], + "ratio_L_exponent": -1, + "ratio_q_exponent": -1244 + }, + "negative_controls": [ + "one_less_than_least_root", + "live_peak_as_backing", + "endpoint_stock_monotonicity", + "omitted_radix_atom_expansion" + ], + "source_pins": 11, + "reviewed_files": { + "PROOF.md": "7eecdb15b5ee78517461a03629f1421c1c8edf1c17d7e15d5363bbcc685e5860", + "stack_model.py": "9191ce603eceeee0d46d233fbb2abca6aa1e7f4bfcdc982397f28654a1b54b1c" + }, + "author_suite_rerun": false, + "full_dispatcher_admission": false +} diff --git a/research/stratified-owned-reserves/independent-review/REVIEW.md b/research/stratified-owned-reserves/independent-review/REVIEW.md new file mode 100644 index 0000000000..830827389a --- /dev/null +++ b/research/stratified-owned-reserves/independent-review/REVIEW.md @@ -0,0 +1,145 @@ +# Independent review of stratified owned reserves + +Reviewer: analytic research worker, separate from the ownership author. +Prepared for Jerry Chen / @CubeJerry with substantial OpenAI assistance. +Canonical source base: `e54523517d0f03e58352e647c403a5af3e525a57`. +This is model-assisted mathematical/source review, not human acceptance or +proof-kernel verification. The reviewed core hashes are in RESULT.json. + +## Outcome + +**Pass for the declared conditional accounting lemma.** I found no defect +in the Bellman certificate, complete-history conclusion, source-stratified +volume factors, monotone envelope or precisely scoped formula counterexample. +The local relative-space contracts, reusable-origin physical implementation, +complete `.0034` backend, stock-fit margins and selected emitted dispatcher +remain premises. No complete owned-erasure discharge, new runtime tariff, +unconditional multiplication theorem or new kappa follows. + +I read PROOF.md and stack_model.py; selected #7000/#7001 application Section 3; +the stopped-product paid atom and ordinary wrapper sections; the delayed-cover +stock prescription and whole-high batch allocation proof; and the existing +single-stage allocation and continuation-retained-backing contracts. The +script separately authenticates all 11 declared scientific input pins. +The two historical catalogue/selected provenance rows remain bound by the +package metadata; they are not treated as current scientific input bytes. +I did not rerun the +author's full verifier or copy its bounded-path enumeration. + +## Least certificate, including mixed self/lower paths + +The possible concern is a long self-chain followed by an expanding lower +edge. It does not create an omitted term. At one stage, let c be its local +cost, rho its self-contraction and y=c+a M_j the cost of exiting immediately +to lower stage j. After m self-edges and then that exit, the supremal path +cost is + + c(1-rho^m)/(1-rho) + rho^m y + = (1-rho^m) c/(1-rho) + rho^m y. + +It is a convex combination of the pure self-chain limit and immediate-exit +cost. Thus some endpoint is at least as large. Applying this elimination +successively leaves a strictly descending path whose final vertex carries +its full geometric self-chain reward. There are only finitely many such +descending paths in the fixed stage graph. Their maximum equals the stated +Bellman formula. + +This also gives a lower certificate. For any maximizing descending path, +replace the terminal infinite chain by m terms. Its value increases to the +claimed certificate, with exact missing tail + + product(lower-edge factors) * c_terminal * rho_terminal^m/(1-rho_terminal). + +Therefore no smaller coefficient bounds every finite abstract path. This is +sharpness for the stated real-volume relaxation, not an assertion that a +particular integer-sized supplier attains the bound. Nonnegative local terms, +strictly descending nonself edges, and rho<1 are essential. + +The independent script enumerates complete **descending paths with exact +terminal geometric rewards**, rather than bounded-depth active paths. It +checks 1,068 coordinate certificates over 48 seven-stage rational graphs, +three source-shaped six-stage examples and the unit example. It evaluates +4,920 descending paths, gives an exact finite dual witness plus its remainder +for each certificate, and checks every Bellman inequality and tightness. +The source unit example is exactly 6,572. A one-unit reduction fails the +root's lower-exit inequality. + +## Complete history and the actual source graph + +The source application freezes `.0034 -> .0038507 -> .00385248` and states +that each new backend uses its completed predecessor for ordinary maps and +high-part exchanges. Its two bootstrap stages are not recursion depth. The +stopped-product source gives the atom's below-four binary embedding and the +binary-to-radix below-q-squared enlargement; the delayed-cover source adds +one below-two row padding and two sequential completed body calls. Hence +the graph's conservative factors 4 and 2q^2 have the stated source meaning. +They do not certify the local workspace constants or numerical admission +of small test primes. + +The whole-high allocation source explicitly retains all H ancestor high +values. A recursive batch therefore has volume V/L, not V/(L H), and all +external body/spectator ranges remain present. The proof uses final fixed +template divisors, not the current 134-axis cap or a raw native role count. +The complex ordinary call consumes its complete encoded field; parent +suspension and private copies stay in the parent local envelope. + +On each tape, restored sibling origins bound every future written address +by one path interval. Erasure cannot reduce the already allocated backing. +Taking the union over time separately for each tape and then summing is +necessary. The separate literal history uses initial backing (7,11), parent +extents (2,3), and alternating child extents (11,1) and (1,13). Seventeen +repetitions retain capacities (20,27), total47, while the maximum live total +including initial backing is37. Initial dirty prefixes and suspended parent +contents remain unchanged. A live-peak substitute fails the control. + +The proof correctly retains this physical origin discipline as a premise. +Algebraic endpoint restoration alone would not supply it. It also keeps the +administrative time as a sum over all call occurrences; the space certificate +does not erase sequential multiplicity from time. + +## Stock envelope and counterexample scope + +For e<=E, both w(e)<=ceil(E^rho) and ceil(e/w(e))<=E hold. Hence the actual +depth is at most 2+ceil(log_N E). Increasing both the stock base and exponent, +and multiplying a justified predecessor envelope, proves the proposed bound. +If the predecessor envelope is nondecreasing, every factor is nondecreasing. +The logarithm of the newly added factor is O(E^rho log(2E))=o(E) for fixed +template parameters. This does not bound the inherited reserve for free or +establish the caller's actual maximal width E. + +I checked the nonmonotonicity example without calling the author's root or +log routines. For k=3215, exact integer power inequalities determine widths +k and k+1 at k^250 and k^250+1. Bit lengths of the two exact ceiling quotients +give depths 2904 and2903. Subtracting stock exponents gives L exponent -1 +and q exponent -1244. Thus the new-factor ratio is 1/(L q^1244)<1 for every +q>1 and L>=1 in that stock-formula dimension N=2. The finite q=3,L=96 check +is an algebraic control only. The proof does not falsely attribute this +discontinuity to the selected enormous compiler dimension or nonconstant +old reserve. + +Finally, independent simultaneous coordinate factors require a product of +reservations. Completed sibling endpoints allow reuse of the same product; +suspension does not turn an ancestor coordinate into unused fresh child +stock. The proof explicitly overcounts repeated inherited factors until a +source-preserving identification is proved, and assumes Q>=S_total before +using one less-than-two outer padding. These are correctly scoped conditions. + +## Reproduction and remaining gates + +When copied under the reviewed package as `independent-review`, run: + +```sh +python3 -I -B research/stratified-owned-reserves/independent-review/independent.py +python3 -I -O -B research/stratified-owned-reserves/independent-review/independent.py +``` + +The separate working copy accepts `--package-root PATH`. The default is +read-only and checks a frozen typed receipt; `--write-result` is explicit. +Expected marker: `PASS_INDEPENDENT_STRATIFIED_SPACE 1068 4920 4`. + +Normal and optimized independent replays both passed. Four controls reject +a smaller-than-least root certificate, live-peak backing, endpoint stock +monotonicity and omission of the source atom expansion factor. The finite +domains corroborate the quantified arguments above. The author's complete +registered replay, final commit and publication integrity checks remain the +author/orchestrator's gates, not tests silently performed by this review. diff --git a/research/stratified-owned-reserves/independent-review/independent.py b/research/stratified-owned-reserves/independent-review/independent.py new file mode 100644 index 0000000000..b796c3534d --- /dev/null +++ b/research/stratified-owned-reserves/independent-review/independent.py @@ -0,0 +1,190 @@ +"""Separate stratified-space review: descending paths and exact dual witnesses. + +Prepared for CubeJerry with substantial OpenAI assistance. Standard library. +This does not rerun the author's verifier or execute a multiplication caller. +""" +import argparse +from fractions import Fraction as F +from hashlib import sha1, sha256 +from pathlib import Path +from types import ModuleType +import json +import random + +parser = argparse.ArgumentParser() +parser.add_argument('--package-root', type=Path) +parser.add_argument('--write-result', action='store_true') +args = parser.parse_args() +OUT = Path(__file__).resolve().parent +P = (args.package_root or OUT.parent).resolve() +ROOT = P.parents[1] + + +def need(condition, label): + if not condition: + raise ValueError(label) + + +def load(path): + module = ModuleType(path.stem) + module.__file__ = str(path) + import sys + sys.modules[path.stem] = module + exec(compile(path.read_bytes(), str(path), 'exec'), module.__dict__) + return module + + +model = load(P / 'stack_model.py') +pins = [pin for pin in json.loads((P / 'SOURCES.json').read_text())['files'] + if pin['usage'] == 'input'] +for pin in pins: + raw = (ROOT / pin['path']).read_bytes() + need(sha256(raw).hexdigest() == pin['sha256'], 'source SHA256: ' + pin['path']) + need(sha1(b'blob ' + str(len(raw)).encode() + b'\0' + raw).hexdigest() + == pin['git_blob'], 'source Git blob: ' + pin['path']) + + +def descending_paths(name, graph): + # A path terminates in a full geometric self-chain, never in a guessed depth. + yield ((name, F(1)),) + for lower, factor in graph[name].lower: + for tail in descending_paths(lower, graph): + yield ((name, F(1)), (tail[0][0], F(factor)), *tail[1:]) + + +def path_value(path, graph, tape, terminal_terms=None): + prefix, scale = F(0), F(1) + for index, (name, factor) in enumerate(path): + scale *= factor + stage = graph[name] + if index + 1 < len(path): + prefix += scale * stage.local[tape] + else: + if terminal_terms is None: + tail = stage.local[tape] / (1-stage.contraction) + else: + tail = stage.local[tape] * sum((stage.contraction**j for j in range(terminal_terms)), F(0)) + return prefix + scale * tail, scale, stage + raise ValueError('empty descending path') + + +coordinate_checks = 0 +path_checks = 0 +def check_graph(stages): + global coordinate_checks, path_checks + graph = {s.name: s for s in stages} + certificate = model.potentials(stages) + for stage in stages: + paths = tuple(descending_paths(stage.name, graph)) + for tape in range(len(stage.local)): + scored = [(path_value(path, graph, tape)[0], path) for path in paths] + exact, path = max(scored, key=lambda x: x[0]) + got = certificate[stage.name][tape] + need(exact == got, 'all descending-path supremum') + finite, scale, terminal = path_value(path, graph, tape, 32) + tail = scale * terminal.local[tape] * terminal.contraction**32 / (1-terminal.contraction) + need(finite + tail == got and finite <= got, 'exact finite-path dual witness') + c, rho = stage.local[tape], stage.contraction + slacks = [got-c-rho*got] + slacks += [got-c-a*certificate[n][tape] for n, a in stage.lower] + need(min(slacks) == 0, 'tight feasible Bellman inequality') + need(all(x >= 0 for x in slacks), 'all Bellman inequalities') + coordinate_checks += 1 + path_checks += len(paths) + return certificate + + +rng = random.Random(20261110) +for case in range(48): + stages = [] + for i in range(7): + rho = rng.choice((F(0), F(1, 7), F(1, 2), F(4, 5))) + local = tuple(F(rng.randrange(10), rng.choice((1, 2, 3))) for _ in range(3)) + edges = tuple((str(j), rng.choice((F(1, 3), F(1), F(4), F(18)))) + for j in range(i) if rng.randrange(2)) + stages.append(model.Stage(str(i), rho, local, edges)) + check_graph(stages) +selected = [] +for q1, q2 in ((3, 3), (5, 7), (101, 103)): + local = tuple(tuple(F(1+i+t, 1+t) for t in range(3)) for i in range(6)) + certificate = check_graph(model.selected_relaxation(q1, q2, local)) + selected.append({'q1': q1, 'q2': q2, + 'root': [[x.numerator, x.denominator] for x in certificate['C']]}) +unit = check_graph(model.selected_relaxation(3, 3)) +need(unit['C'] == (F(6572),), 'source-graph unit example') + +# A literal two-tape history, with unchanged dirty entry prefixes and retained tails. +initial = (7, 11) +local = (2, 3) +tapes = [bytearray([9])*n for n in initial] +def write_block(tape, start, extent, symbol): + for position in range(start, start+extent): + if position == len(tape): + tape.append(0) + need(position < len(tape), 'no remote capacity jump') + tape[position] = symbol + +for tape, origin, width in zip(tapes, initial, local): + write_block(tape, origin, width, 7) +live_peak = 0 +for child in ((11, 1), (1, 13))*17: + live_peak = max(live_peak, sum(initial)+sum(local)+sum(child)) + for tape, origin, parked, width in zip(tapes, initial, local, child): + write_block(tape, origin+parked, width, 5) + need(tape[:origin] == bytearray([9])*origin, 'dirty entry prefix preserved') + need(tape[origin:origin+parked] == bytearray([7])*parked, 'parent preserved') + write_block(tape, origin+parked, width, 0) +history = {'entry': list(initial), 'retained': [len(t) for t in tapes], 'live_peak': live_peak} +need(history['retained'] == [20, 27] and live_peak == 37, 'crossed tape maxima') +need(sum(history['retained']) == sum(initial) + 13 + 16, 'coordinatewise certificate') +need(sum(history['retained']) > live_peak, 'live peak is not retained backing') + +# Counterexample checked using power inequalities and bit lengths, without atom_width/ceil_log. +k = 3215 +e0 = k**250 +e1 = e0 + 1 +need((k-1)**250 < e0 <= k**250 < e1 <= (k+1)**250, 'exact width straddling') +quotient0 = k**249 +quotient1 = (e1+k)//(k+1) +need(2**2901 < quotient0 <= 2**2902, 'first depth interval') +need(2**2900 < quotient1 <= 2**2901, 'second depth interval') +depth0, depth1 = 2+(quotient0-1).bit_length(), 2+(quotient1-1).bit_length() +delta_l = depth1-depth0 +delta_q = 4*(k*depth1-(k-1)*depth0) +need((depth0, depth1, delta_l, delta_q) == (2904, 2903, -1, -1244), + 'formula-only stock decrease for every q>1 and L>=1') +counter = {'k': k, 'rho': [1, 250], 'N': 2, 'depths': [depth0, depth1], + 'ratio_L_exponent': delta_l, 'ratio_q_exponent': delta_q} + +controls = [] +def rejects(label, function): + try: + function() + except ValueError: + controls.append(label) + else: + raise ValueError('surviving negative control: '+label) + +rejects('one_less_than_least_root', lambda: need(F(6571) >= 1+unit['O2'][0], 'lower exit')) +rejects('live_peak_as_backing', lambda: need(live_peak >= sum(history['retained']), 'history')) +rejects('endpoint_stock_monotonicity', lambda: need(F(1, 96*3**1244) >= 1, 'stock formula')) +wrong = list(model.selected_relaxation(3, 3)) +for index in (1, 3): + s = wrong[index] + wrong[index] = model.Stage(s.name, s.contraction, s.local, tuple((n, F(1)) for n, _ in s.lower)) +wrong_root = model.potentials(wrong)['C'][0] +rejects('omitted_radix_atom_expansion', lambda: need(wrong_root >= unit['C'][0], 'actual lower volumes')) + +receipt = {'status': 'PASS_INDEPENDENT_STRATIFIED_SPACE', 'seed': 20261110, + 'coordinate_certificates': coordinate_checks, 'descending_paths_checked': path_checks, + 'selected_graphs': selected, 'unit_root': 6572, 'history': history, + 'stock_counterexample': counter, 'negative_controls': controls, + 'source_pins': len(pins), + 'reviewed_files': {n: sha256((P/n).read_bytes()).hexdigest() + for n in ('PROOF.md', 'stack_model.py')}, + 'author_suite_rerun': False, 'full_dispatcher_admission': False} +if args.write_result: + (OUT/'RESULT.json').write_text(json.dumps(receipt, indent=2)+'\n') +else: + need(receipt == json.loads((OUT/'RESULT.json').read_text()), 'frozen independent receipt') +print(receipt['status'], coordinate_checks, path_checks, len(controls)) diff --git a/research/stratified-owned-reserves/stack_model.py b/research/stratified-owned-reserves/stack_model.py new file mode 100644 index 0000000000..235b0c86d1 --- /dev/null +++ b/research/stratified-owned-reserves/stack_model.py @@ -0,0 +1,136 @@ +"""Exact reference accounting; this is not an executed supplier dispatcher. + +Prepared for CubeJerry with substantial OpenAI Codex assistance. Apache-2.0. +""" +from dataclasses import dataclass +from fractions import Fraction +from typing import Sequence + + +@dataclass(frozen=True) +class Stage: + name: str + contraction: Fraction + local: tuple[Fraction, ...] + lower: tuple[tuple[str, Fraction], ...] = () + + +def potentials(stages: Sequence[Stage]) -> dict[str, tuple[Fraction, ...]]: + """Least coordinatewise certificate for the stated stratified relaxation.""" + if not stages: + raise ValueError("empty stage list") + tapes = len(stages[0].local) + if not tapes: + raise ValueError("no tape coordinates") + answer = {} + for stage in stages: + rho = Fraction(stage.contraction) + local = tuple(Fraction(c) for c in stage.local) + lower = tuple((name, Fraction(a)) for name, a in stage.lower) + if stage.name in answer or not 0 <= rho < 1: + raise ValueError("duplicate stage or noncontracting same-stage edge") + if len(local) != tapes or any(c < 0 for c in local): + raise ValueError("invalid local tape envelope") + if any(name not in answer or a <= 0 for name, a in lower): + raise ValueError("a lower edge must descend to a preceding stage") + answer[stage.name] = tuple( + max([c / (1 - rho)] + + [c + a * answer[name][t] + for name, a in lower]) + for t, c in enumerate(local) + ) + return answer + + +def selected_relaxation(q1: int, q2: int, + local: Sequence[Sequence[int | Fraction]] | None = None + ) -> tuple[Stage, ...]: + """The six source application stages, with conservative factors only. + + q values here are geometric parameters, not admission certificates. + B0 abbreviates a separate complete relative-space contract. + """ + if q1 < 3 or q2 < 3: + raise ValueError("q must be at least three") + rows = local if local is not None else [(1,)] * 6 + if len(rows) != 6: + raise ValueError("six local envelopes required") + a = [tuple(Fraction(x) for x in row) for row in rows] + p1, p2 = Fraction(2 * q1 * q1), Fraction(2 * q2 * q2) + return ( + Stage("B0", Fraction(0), a[0]), + Stage("K1", Fraction(1, 2), a[1], (("B0", Fraction(4)),)), + Stage("O1", Fraction(0), a[2], (("K1", p1), ("B0", p1))), + Stage("K2", Fraction(1, 2), a[3], (("O1", Fraction(4)),)), + Stage("O2", Fraction(0), a[4], (("K2", p2), ("O1", p2))), + Stage("C", Fraction(1, 2), a[5], (("O2", Fraction(1)),)), + ) + + +def ceil_div(a: int, b: int) -> int: + if a < 0 or b <= 0: + raise ValueError("ceil_div domain") + return (a + b - 1) // b + + +def ceil_log(n: int, base: int) -> int: + if n < 1 or base < 2: + raise ValueError("ceil_log domain") + power, depth = 1, 0 + while power < n: + power *= base + depth += 1 + return depth + + +def atom_width(e: int, numerator: int = 1, denominator: int = 250) -> int: + """Smallest positive w satisfying w**denominator >= e**numerator.""" + if e < 1 or not 0 < numerator < denominator: + raise ValueError("atom-width domain") + target = e ** numerator + lo, hi = 1, e + while lo < hi: + mid = (lo + hi) // 2 + if mid ** denominator < target: + lo = mid + 1 + else: + hi = mid + return lo + + +def stock_exponents(e: int, n: int, numerator: int = 1, + denominator: int = 250) -> tuple[int, int, int]: + """w, exponent of L, exponent of q in W(w)**D; old stock is separate.""" + w = atom_width(e, numerator, denominator) + d = 2 + ceil_log(max(1, ceil_div(e, w)), n) + return w, d, n * n * (w - 1) * d + + +def reserve_envelope(e_max: int, n: int, numerator: int = 1, + denominator: int = 250) -> tuple[int, int, int]: + w = atom_width(e_max, numerator, denominator) + d = 2 + ceil_log(max(1, e_max), n) + return w, d, n * n * (w - 1) * d + + +def mixed_rank(coordinates: Sequence[int], radices: Sequence[int]) -> int: + if len(coordinates) != len(radices) or any(r < 1 for r in radices): + raise ValueError("bad mixed-radix shape") + out = 0 + for digit, radix in zip(coordinates, radices, strict=True): + if not 0 <= digit < radix: + raise ValueError("digit outside its own reservation") + out = out * radix + digit + return out + + +def mixed_unrank(value: int, radices: Sequence[int]) -> tuple[int, ...]: + if value < 0 or any(r < 1 for r in radices): + raise ValueError("bad mixed-radix rank") + result = [] + for radix in reversed(radices): + value, digit = divmod(value, radix) + result.append(digit) + if value: + raise ValueError("rank outside complete reservation") + return tuple(reversed(result)) diff --git a/research/stratified-owned-reserves/test_boundaries.py b/research/stratified-owned-reserves/test_boundaries.py new file mode 100644 index 0000000000..154deafd50 --- /dev/null +++ b/research/stratified-owned-reserves/test_boundaries.py @@ -0,0 +1,82 @@ +#!/usr/bin/env python3 +"""Corrupt real replay inputs in disposable source mirrors and require rejection. + +Prepared for CubeJerry with substantial OpenAI Codex assistance. Apache-2.0. +""" +import json +from pathlib import Path +import shutil +import subprocess +import sys +import tempfile + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parents[1] +RELATIVE = PACKAGE.relative_to(ROOT) + + +def need(condition, label): + if not condition: + raise SystemExit("FAIL_STRATIFIED_BOUNDARIES: " + label) + + +def run(root, optimized=False): + command = [sys.executable, "-I", "-B"] + if optimized: + command.append("-O") + command.append(str(root / RELATIVE / "verify.py")) + return subprocess.run(command, cwd=root, text=True, capture_output=True, + timeout=30, check=False) + + +def main(): + inputs = json.loads((PACKAGE / "VERIFY.json").read_text())["inputs"] + with tempfile.TemporaryDirectory(prefix="stratified-owned-reserves-") as temp: + mirror = Path(temp) + package = mirror / RELATIVE + shutil.copytree(PACKAGE, package) + for name in inputs: + target = mirror / name + target.parent.mkdir(parents=True, exist_ok=True) + shutil.copy2(ROOT / name, target) + for optimized in (False, True): + good = run(mirror, optimized) + need(good.returncode == 0 and "PASS_STRATIFIED_OWNED_RESERVES" in good.stdout, + "clean Git-free replay in both interpreter modes") + + expected_path = package / "RESULT.json" + original = expected_path.read_bytes() + receipt = json.loads(original) + # Python's untyped object equality identifies True and 1. This + # mutation specifically checks the typed canonical-JSON comparison. + receipt["schema"] = True + expected_path.write_text(json.dumps(receipt)) + bad = run(mirror, True) + need(bad.returncode != 0 and "complete typed result equality" in bad.stderr, + "typed receipt corruption rejects under optimization") + expected_path.write_bytes(original) + + source_path = mirror / inputs[0] + source = source_path.read_bytes() + source_path.write_bytes(source + b"\nsource drift control\n") + bad = run(mirror) + need(bad.returncode != 0 and "SHA " in bad.stderr, "source drift rejects") + source_path.write_bytes(source) + + model_path = package / "stack_model.py" + model = model_path.read_text() + mutation = model.replace('(("B0", Fraction(4)),)', '(("B0", Fraction(1)),)', 1) + need(mutation != model, "edge mutation applied") + model_path.write_text(mutation) + bad = run(mirror, True) + need(bad.returncode != 0 and "selected graph symbolic unit example" in bad.stderr, + "dropped radix-embedding inflation rejects under optimization") + model_path.write_text(model) + + last = run(mirror) + need(last.returncode == 0, "restoration after all mutations") + print("PASS_STRATIFIED_BOUNDARIES clean_modes=2 rejecting_controls=3") + + +if __name__ == "__main__": + main() diff --git a/research/stratified-owned-reserves/verify.py b/research/stratified-owned-reserves/verify.py new file mode 100644 index 0000000000..1930744231 --- /dev/null +++ b/research/stratified-owned-reserves/verify.py @@ -0,0 +1,275 @@ +#!/usr/bin/env python3 +"""Exact bounded corroboration, not an executed supplier dispatcher. + +Prepared for CubeJerry with substantial OpenAI Codex assistance. Apache-2.0. +""" +from fractions import Fraction +from hashlib import sha256, sha1 +from itertools import product +import json +from pathlib import Path +import re +import sys + +sys.dont_write_bytecode = True +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parents[1] + + +def load_source(path): + import types + module = types.ModuleType("stack_model_source") + module.__file__ = str(path) + old = sys.modules.get(module.__name__) + sys.modules[module.__name__] = module + try: + exec(compile(path.read_bytes(), str(path), "exec"), module.__dict__) + finally: + if old is None: + sys.modules.pop(module.__name__, None) + else: + sys.modules[module.__name__] = old + return module + + +M = load_source(PACKAGE / "stack_model.py") + + +def need(condition, label): + if not condition: + raise SystemExit("FAIL_STRATIFIED_OWNED_RESERVES: " + label) + + +def rejects(function, label): + try: + function() + except (ValueError, SystemExit): + return label + raise SystemExit("negative control unexpectedly accepted: " + label) + + +def source_bindings(): + source = json.loads((PACKAGE / "SOURCES.json").read_text()) + live = [row for row in source["files"] if row["usage"] == "input"] + for row in live: + raw = (ROOT / row["path"]).read_bytes() + need(sha256(raw).hexdigest() == row["sha256"], "SHA " + row["path"]) + blob = sha1(b"blob " + str(len(raw)).encode() + b"\0" + raw).hexdigest() + need(blob == row["git_blob"], "Git blob " + row["path"]) + app = (ROOT / "docs/research/pr-intake-evidence/pr7000-application/PROOF-REVIEW.md").read_text() + pattern = r"\.0034\s*->\s*\.0038507\s*->\s*\.00385248" + need(re.search(pattern, app) is not None, "actual frozen backend chain") + for token in ["ρ=1/250", "**134**", "W(w)^D_stock(e) S_old", "107,352", + "117,612", "product of simultaneous BIT and complex reservations", + "ordinary maps/high-part exchanges", "with atom exponent"]: + need(token in app, "source application token " + token) + geometry = (ROOT / "research/delayed-cover-batch-allocation/PROOF.md").read_text() + need("V/L" in geometry, "whole-high contraction") + atom = (ROOT / "notes/stopped-product-interface.tex").read_text() + need("volume factor below four" in atom and "below $q^2$" in atom, + "retained embedding factors") + need(re.search(pattern, app.replace(".0038507", ".0034", 1)) is None, + "wrong middle backend rejects") + return {"live_pins": len(live), "backend_savings": [".0034", ".0038507", ".00385248"], + "source_rho": "1/250", "raw_bit_ambient_cap": 134, + "source_application_sha256": sha256(app.encode()).hexdigest()} + + +def enumerate_paths(stages, start, depth): + """Independent bounded route expansion, without Bellman updates.""" + by_name = {s.name: s for s in stages} + stack = [(start, Fraction(1), (Fraction(0),) * len(stages[0].local), 0)] + while stack: + name, volume, totals, used = stack.pop() + s = by_name[name] + now = tuple(x + volume * c for x, c in zip(totals, s.local, strict=True)) + yield now + if used == depth: + continue + if s.contraction: + stack.append((name, volume * s.contraction, now, used + 1)) + for other, inflation in s.lower: + stack.append((other, volume * inflation, now, used + 1)) + + +def stack_certificates(): + comparisons = 0 + graphs = 0 + for costs in product((1, 2), repeat=3): + for rhos in product((Fraction(0), Fraction(1, 2)), repeat=3): + for mask in range(8): + edges = [[], [], []] + for bit, (i, j) in enumerate(((1, 0), (2, 0), (2, 1))): + if mask & (1 << bit): + edges[i].append((str(j), Fraction(2 if bit % 2 else 1))) + stages = tuple(M.Stage(str(i), rhos[i], (Fraction(costs[i]),), tuple(edges[i])) + for i in range(3)) + bound = M.potentials(stages) + graphs += 1 + for path in enumerate_paths(stages, "2", 8): + comparisons += 1 + need(path[0] <= bound["2"][0], "bounded independent path") + for s in stages: + b = bound[s.name][0] + need(b >= s.local[0] + s.contraction * b, "self inequality") + for j, a in s.lower: + need(b >= s.local[0] + a * bound[j][0], "descending inequality") + chosen = M.selected_relaxation(3, 3) + bound = M.potentials(chosen) + expected = {"B0": 1, "K1": 5, "O1": 91, "K2": 365, "O2": 6571, "C": 6572} + need({key: int(value[0]) for key, value in bound.items()} == expected, + "selected graph symbolic unit example") + selected_paths = list(enumerate_paths(chosen, "C", 10)) + need(max(p[0] for p in selected_paths) == bound["C"][0], "attaining finite path") + rows = [(i + 1, 2 * i + 1, 1) for i in range(6)] + typed = M.selected_relaxation(3, 5, rows) + typed_bound = M.potentials(typed) + for path in enumerate_paths(typed, "C", 9): + need(all(x <= y for x, y in zip(path, typed_bound["C"], strict=True)), + "per-tape weighted path") + controls = [ + rejects(lambda: M.potentials([M.Stage("x", Fraction(1), (Fraction(1),))]), + "same-stage noncontraction"), + rejects(lambda: M.potentials([M.Stage("low", Fraction(0), (Fraction(1),), + (("high", Fraction(1)),)), + M.Stage("high", Fraction(0), (Fraction(1),))]), + "upward edge / cycle"), + ] + need(sum([1] * 7) > 2, "same-volume chain exceeds one-provider geometric two") + controls.append("seven same-volume frames exceed 2V") + return {"graphs": graphs, "bounded_path_comparisons": comparisons, + "selected_bounded_paths": len(selected_paths), "unit_example": expected, + "controls": controls} + + +def history_controls(): + tapes = 3 + initial = [11, 19, 7] + origin = [2, 3, 1] + historical = initial.copy() + all_paths = [] + node_count = 0 + + def visit(vol, level, path): + nonlocal node_count + node_count += 1 + local = [c * vol for c in (1, 2, 3)] + for t in range(tapes): + historical[t] = max(historical[t], origin[t] + local[t]) + new_path = [p + x for p, x in zip(path, local, strict=True)] + all_paths.append(tuple(new_path)) + if level: + saved = origin.copy() + for t in range(tapes): + origin[t] += local[t] + visit(vol // 2, level - 1, new_path) + after_first = origin.copy() + visit(vol // 2, level - 1, new_path) + need(origin == after_first, "sibling returns to same origin") + origin[:] = saved + + visit(64, 4, [0, 0, 0]) + per_tape = [max(p[t] for p in all_paths) for t in range(tapes)] + need(all(h <= k + b for h, k, b in zip(historical, initial, per_tape, strict=True)), + "historical coordinate envelope") + need(origin == [2, 3, 1], "root origins restored") + peaks = [(80, 0), (0, 80)] + history = sum(max(row[t] for row in peaks) for t in range(2)) + live_max = max(map(sum, peaks)) + need(history == 160 and live_max == 80, "sum of maxima differs from maximum sum") + need(7 * 80 > 80, "append-only sibling history violates restored-origin bound") + need(1000 + 80 > 80, "warm erased entry backing must be included") + need(23 * 64 > 64, "dropping external factor undercounts physical field") + return {"reference_nodes": node_count, "historical_extents": historical, + "path_extents": per_tape, "role_rotating_history": history, + "false_max_live": live_max, + "controls": ["append-only sibling", "entry backing omitted", "external factor omitted", + "aggregate-live maximum substituted"]} + + +def stock_checks(): + cases = 0 + monotone = 0 + for n in (2, 3, 5): + for numerator, denominator in ((1, 2), (1, 3), (2, 3), (1, 250)): + previous = None + for e_max in range(1, 101): + bar = M.reserve_envelope(e_max, n, numerator, denominator) + if previous: + need(all(a <= b for a, b in zip(previous, bar, strict=True)), + "safe envelope monotone") + monotone += 1 + previous = bar + for e in range(1, e_max + 1): + actual = M.stock_exponents(e, n, numerator, denominator) + need(all(a <= b for a, b in zip(actual, bar, strict=True)), + "every smaller width in reserve envelope") + cases += 1 + k = 3215 + e0, e1 = k ** 250, k ** 250 + 1 + need((k - 1) ** 250 < e0 <= k ** 250 < e1 <= (k + 1) ** 250, + "exact selected-rho atom widths") + n0, n1 = M.ceil_div(e0, k), M.ceil_div(e1, k + 1) + need(2 ** 2901 < n0 <= 2 ** 2902, "first depth interval") + need(2 ** 2900 < n1 <= 2 ** 2901, "second depth interval") + d0, d1 = 2 + M.ceil_log(n0, 2), 2 + M.ceil_log(n1, 2) + exponent_delta = 4 * (k * d1 - (k - 1) * d0) + need((d0, d1, d1 - d0, exponent_delta) == (2904, 2903, -1, -1244), + "symbolic stock decrease") + need(2 * (3 * 3 - 1) * (3 * 3 - 3) == 96, "GL2 algebraic control") + need(M.stock_exponents(2 ** 100, 2, 1, 250)[1] > 2, + "bootstrap count is not depth stock") + return {"smaller_width_checks": cases, "monotonicity_checks": monotone, + "rho": "1/250", "discontinuity_k": k, + "e0_description": "3215^250", "e1_description": "3215^250+1", + "depths": [d0, d1], "ratio": "L^-1*q^-1244", + "counterexample_scope": "stock formula at N=2; no selected-instance or prime admission claim", + "controls": ["raw endpoint stock substituted", "bootstrap count substituted for depth"]} + + +def product_reservations(): + count = 0 + for radices in ((2, 3), (2, 3, 5), (3, 4, 2, 3), (1, 2, 1, 5)): + total = 1 + for radix in radices: + total *= radix + seen = set() + for coordinates in product(*(range(r) for r in radices)): + rank = M.mixed_rank(coordinates, radices) + need(rank not in seen, "independent reservation injective") + seen.add(rank) + need(M.mixed_unrank(rank, radices) == coordinates, "reservation inverse") + for i, r in enumerate(radices): + changed = list(coordinates) + changed[i] = (changed[i] + 1) % r + returned = list(M.mixed_unrank(M.mixed_rank(changed, radices), radices)) + returned[i] = (returned[i] - 1) % r + need(tuple(returned) == coordinates, "other stage factors and returned row survive") + count += 1 + need(seen == set(range(total)), "complete simultaneous stock") + for q in range(total, 2 * total + 1): + padded = total * M.ceil_div(q, total) + need(q <= padded < 2 * q, "single complete-row padding") + need(max(2, 3, 5) < 2 * 3 * 5, "max is not product") + return {"complete_product_coordinates": count, + "controls": ["max stock substituted for product", "external stage coordinate dropped"]} + + +def main(): + need(sys.argv[1:] in ([], ["--emit"]), "command-line arguments") + result = {"schema": 1, "scope": "conditional allocation accounting; no new kappa", + "source": source_bindings(), "stack": stack_certificates(), + "history": history_controls(), "stock": stock_checks(), + "reservations": product_reservations()} + canonical = json.dumps(result, sort_keys=True, separators=(",", ":")) + if sys.argv[1:] == ["--emit"]: + print(json.dumps(result, sort_keys=True, indent=2)) + else: + frozen = json.loads((PACKAGE / "RESULT.json").read_text()) + need(canonical == json.dumps(frozen, sort_keys=True, separators=(",", ":")), + "complete typed result equality") + print("PASS_STRATIFIED_OWNED_RESERVES", sha256(canonical.encode()).hexdigest()) + + +if __name__ == "__main__": + main()