diff --git a/research/p104-owned-cleanup-obstruction/LITERATURE.md b/research/p104-owned-cleanup-obstruction/LITERATURE.md new file mode 100644 index 0000000000..b5bfc23ce5 --- /dev/null +++ b/research/p104-owned-cleanup-obstruction/LITERATURE.md @@ -0,0 +1,31 @@ +# Primary literature consulted + +These sources informed questions and proof organization. None certifies the +P104 ownership, native operations or recursive tariff used here. + +- Bostan, Lecerf and Schost, *Tellegen's Principle into Practice*, ISSAC 2003 + ([author-hosted paper](https://mathexp.eu/bostan/publications/BoLeSc03.pdf)). + Linear-program transposition helps inspect how local errors reach outputs. + The repository already has an owned transpose construction; generic + transposition is not claimed as new here. +- Schaeffer and Perkowski, *A Cost Minimization Approach to Synthesis of Linear + Reversible Circuits* ([primary preprint](https://arxiv.org/abs/1407.0070)). + Bidirectional synthesis motivates considering both prefix and suffix maps. + Our condition `S(R-T)P=0` and its full-rank consequence are elementary linear + algebra, independently proved here; no P104 cost theorem comes from the paper. +- Paradis, Bichsel and Vechev, *Reqomp: Space-constrained Uncomputation for Quantum + Circuits*, Quantum 8, 1258 (2024) + ([primary preprint](https://arxiv.org/abs/2212.10395)). Value-version scheduling + motivates earlier equivalent producers or changed lifetimes. The loss-space + invariant tests unchanged scalar values. P104's inherited owned CLEAR can + erase a nonzero field, so quantum uncomputation costs cannot replace this + source's ownership contract. + +A genuinely different next test is coupled synthesis of a larger public+owned +window containing the public contact that causes a conflict and at least two +lifetimes. Allow intermediate public bases and payloads to change while +requiring the exact external map, then price the complete signed recursive +invoice. This is our proposed application of literature ideas, not a published +P104 result. Reject a candidate before full pricing if its altered dependency +cannot preserve external reads. None of these references establishes that +such a candidate exists or improves the bound. diff --git a/research/p104-owned-cleanup-obstruction/PROOF-738.md b/research/p104-owned-cleanup-obstruction/PROOF-738.md new file mode 100644 index 0000000000..37738e87fa --- /dev/null +++ b/research/p104-owned-cleanup-obstruction/PROOF-738.md @@ -0,0 +1,135 @@ +# The exceptional owned lifetime cannot lose a delivery stop in this model + +This concerns owned role738 in the pinned PR5569 word. Unlike the other seven +owned lifetimes, its descending route has several recipient contacts. We ask +whether one stop can be removed by relocating these five delivery ADDs within +their recipient idle windows, or by replacing a delivery with an arbitrary +linear combination of public registers at one common chart. All surrounding +scalar events, dependencies and contact charts remain fixed. This is a broader +test than the original owned-holder scan, but still a local model. + +## Delivery-frame intervals + +Role738 is initialized at frame591 of dimension8, copies public role133 and +scales it by -1/2, then is cleared at frame597 of dimension1. Let its copied +value be D. Its five deliveries are: + +| Recipient | Source event | Coefficient of D | Allowed contact dimension | +|---|---:|---:|---:| +|159|13412|-1|7| +|203|13414|2|6| +|148|13417|2|3 or4| +|710|13420|1|1| +|734|13422|1|1| + +The intervals are derived, not assumed. Remove the nominated delivery from +its recipient's scalar chronology. Let A and B be the preceding and following +remaining scalar-contact charts. A public recipient at a new contact F needs +A subseteq F subseteq B. The descending owned route from591 to597 needs +597 subseteq F subseteq591. Therefore + +``` +span(A + 597) subseteq F subseteq B intersect 591. +``` + +Exact binary spans yield the table. For recipient148 the lower endpoint has +dimension3 and the upper endpoint dimension4; the other intervals are single +subspaces. Reordering cannot evade the resulting strict descending dimension +order. Every route still includes + +``` +8 -> 7 -> 6 -> {3 or4} -> 1. +``` + +For either choice the direct route through the mandatory stops has paid +rank histogram 2H1+H2+H3. Here H_d(t)=d^t for 0{3 or4}->5, with histogramH1+H2 in either case. Additional stops +cannot lower an increasing concave tariff; they split a rank into smaller +positive pieces. No paid stop disappears in this changed-contact family. + +The feasibility and costs of other scalar events have not been weakened. The +table is already enough to rule out a gain from rearranging these deliveries. + +## Why multiple public partners do not bypass one nominated delivery + +The normalized public transfer matrix is invertible at every source cut. This +is certified structurally, without a large numerical rank calculation: + +1. Public ADD and nonzero SCALE are elementary invertible row operations. +2. Each source owned lifetime copies one public producer and only scales that + copy. The producer remains unchanged throughout the owned lifetime. +3. An ADD from that owned copy to a *different* public destination is therefore + an elementary public shear by the still-present producer row. +4. INIT, CLEAR and MOVE do not change the normalized public rows. + +The checker verifies all these conditions on the complete source program: +20,947 effective public ADDs, including33 owned-sourced shears, and707 nonzero +public SCALEs. Thus the735 current public rows form a basis at every cut. + +For each cut, D consequently has a unique coordinate vector c in that current +public basis. Its initial vector is derived by exact symbolic replay to the +owned COPY. Thereafter coordinates can be transported exactly through each +elementary operation. For `row_r += q row_s`, the fixed functional's coordinates +change by `c_s -= q c_r`; for `row_r *= q`, they change by `c_r /= q`. +The checker confirms that c is exactly `-1/2` on role133 and zero elsewhere +both after the producer's final contributing event13376 and at the owned +copy/scale boundary13410. Earlier cuts are included through the same exact +coordinate propagation. + +Any public-only linear combination equal to D must use every public row in +the nonzero support of c. Extra public partners cannot cancel this requirement, +because the entire public row family is a basis. At a single common contact, +all these necessary rows and the recipient must share a feasible chart. + +The checker examines every boundary in each recipient's idle window after +removing its nominated delivery: + +| Recipient | Inclusive preceding-contact boundary | Exclusive next contact | Cuts checked | +|---|---:|---:|---:| +|159|13363|15575|2212| +|203|13245|14027|782| +|148|13233|14018|785| +|710|817|13524|12707| +|734|804|14006|13202| + +At all29,688 recipient/cut pairs, the necessary public support and recipient +contain a pair of incompatible scalar windows: some vector in one lower +boundary chart is absent from another upper boundary chart. This rules out +every common chart, not just the original delivery chart or listed frames. +The recipient's own coordinate in c is zero throughout each tested window, +so there is no omitted self-SCALE alternative. + +Removing the nominated ADD is compatible with using the original donor rows. +Before that ADD nothing differs. Afterward and before the recipient's next +scalar contact, only its own row differs, by a multiple of D. The checked zero +recipient coordinate means the same coordinates on all other public rows still +represent D; those donors and their windows are unchanged. This is a test for +one nominated public replacement with its surrounding contacts fixed, not a +simultaneous synthesis theorem for multiple changed public dependencies. + +These are necessary geometric tests over arbitrary rational coefficients. +They therefore rule out the narrower dyadic legal scalar model without a +separate dyadic synthesis search. The result is a source-derived obstruction, +not a failed search over possible partner counts or coefficients. + +## Scope and controls + +This does not exclude new owned copies, multiple-chart delivery networks, +changed surrounding scalar dependencies, changed source/terminal boundaries, +or a different target functional. In particular, public-basis uniqueness does +not make owned copies useless: a copy can carry the same value on a descending +chart precisely where its original public producer cannot go. + +Four semantic controls reject changing a copied producer while its owned copy +is live, a zero public SCALE, an altered target functional, and a false zero +separating vector. A two-register positive control checks the direction of the +inverse covector update. The root package authenticates source bytes and checks +the entire original arbitrary-input map independently of this local gate. + +No new kappa, global optimum, or general barrier to owned-temporary cleanup is +claimed. The useful conclusion is that a successor mechanism must change a +specific dependency or boundary rather than further optimize these five +fixed-neighbor delivery windows. + +Source and contributor attribution are the same as README.md and inputs/README.md. Prepared with +substantial OpenAI Codex assistance; Apache-2.0. diff --git a/research/p104-owned-cleanup-obstruction/PROOF-blocks.md b/research/p104-owned-cleanup-obstruction/PROOF-blocks.md new file mode 100644 index 0000000000..c5e26e1a94 --- /dev/null +++ b/research/p104-owned-cleanup-obstruction/PROOF-blocks.md @@ -0,0 +1,141 @@ +FIXED-DELIVERY OWNED BLOCKS: A SCOPED RECURSIVE-MOMENT FLOOR + +Status: source-bound proof with exact finite checks. No new kappa is claimed. + +Source and reproducibility +-------------------------- +The source is PR5569 head af9f091ac6f30c6eaacb9c27777bfbe2d0e5ffdf, +research/p104-priced-handoff/WORD.json.gz. Its compressed SHA256 is +12224e9a13a49c830b304338a8d31610fb43da15d1a650537733c27f7864310f. +The registered verify.py calls check_lifetimes.py using Python's standard +library. It imports no predecessor verifier and compares a committed receipt. This audit checks exact rational +scalar rows, frame nesting, local rank tariffs and two-sided boundaries. It is +not a substitute for the source's native character and complete funding replay. + +Definitions and permitted replacements +-------------------------------------- +Let H_d(t)=d^t for 0b>=1. The required map is + + v -> v, x_j -> x_j+c_j v, c_j != 0. + +Under the permitted replacement model, every replacement pays at least + + m H_b(t) + H_(a-b)(t). + +This theorem is useful when a literal implementation attains the floor. It +does not assert that arbitrary given frames admit such an implementation. + +Proof. Each physical public recipient has to ascend from dimension0 to b. +If its ascents have ranks d_1,...,d_k, their sum is b; because +sum_i d_i^t >= (sum_i d_i)^t, its paid moment is at least H_b(t). Summing these +disjoint public moves gives m H_b(t). + +At least one final recipient contains a nonzero v coefficient. Expand its +coefficient through the chronological linear circuit. There is a nonzero +dependency path from the source entry to that recipient exit: zero INIT and +CLEAR cannot create the v coefficient, and cancellation of several paths +cannot leave a nonzero coefficient when there were no contributing paths. +Along this path scalar operations preserve frame dimension; public MOVEs have +nonnegative dimension change and owned MOVEs have nonpositive dimension +change. The path starts at dimension a and ends at dimension b. Its total +owned descent rank is therefore at least a-b. If these descents have ranks +r_1,...,r_l, their tariff is at least + + sum_i r_i^t >= (sum_i r_i)^t >= (a-b)^t. + +These owned moves are disjoint from the public moves charged above. All other +paid events have nonnegative tariff, proving the bound. Auxiliary dimension, +number of fields, rational coefficients, internal cancellation and uncompute +strategy do not change this argument. END PROOF. + +Application to the eight literal lifetimes +------------------------------------------ +Intervals below are zero-based and half open. All seven uniform stars have +a=8,b=1, source unchanged, owned exit zero, and independent actual prefix rows. + +owned interval source recipients coefficient tariff +735 [13377,13388) 173 704,705,706 +1/2 3H1+H7 +736 [13388,13399) 151 707,708,733 +1/2 3H1+H7 +737 [13399,13408) 146 709,732 -1/2 2H1+H7 +738 [13408,13424) 133 159,203,148,710,734 varied 5H1+H2+H3 +739 [13424,13439) 256 712,713,714,715,716 +1/4 5H1+H7 +740 [13439,13454) 92 717,718,719,720,721 +1/4 5H1+H7 +741 [13454,13469) 9 722,723,724,725,726 +1/4 5H1+H7 +742 [13469,13484) 240 727,728,729,730,731 -1/4 5H1+H7 + +For each of the seven stars, the literal cost attains the theorem. Therefore +even a changed internal scalar word cannot lower that block's raw recursive +paid moment, at any 07,6->6,2->3,0->1,0->1. Its public tariff is3H1 and its owned +tariff is2H1+H2+H3, delivering at levels7,6,3,1,1. The elementary dimension-path +argument only gives3H1+H7. No tight arbitrary-replacement bound for738 is claimed. +For example, attempting to deliver148 at its entry frame467 and then continue +down to frame597 fails because frame597=[82] is not contained in +frame467=[45,194]. This rejects that one template only. + +Why the local target map is forced by these two-sided cuts +--------------------------------------------------------- +For a block let P be the matrix of its public entry rows on independent +original scalar symbols, and S the fixed suffix map from its public exit +coordinates to all final public coordinates. Let T be the literal local map +and R a proposed local map. When the replacement cannot access external +coordinates and leaves those coordinates unchanged, full-word equality is + + S (R-T) P = 0. + +The checker verifies that P has full row rank and S has full column rank for +all eight blocks. The ranks are4,4,3,6,6,6,6,6, respectively. Thus a right inverse +of P and a left inverse of S imply R=T. This is an elementary finite-dimensional +linear algebra fact; it is not attributed as a new external theorem. + +The checker also verifies that retired owned coordinates have no subsequent +public effect, but their required zero exit is an independent condition. The +absence of public suffix influence does not authorize leaving private garbage. +Each block has an omitted-delivery negative control that demonstrably changes +at least one final public scalar output. + +Important independence caveat +----------------------------- +In the actual source, register173 is a helper, not a live main register. +Its prefix row has118 nonzero original coefficients and its information also +occurs in external registers. The verified row rank says the listed local +coordinates are linearly independent; it does not say their information exists +nowhere else. This is why outside side-information reuse is explicitly outside +the fixed-delivery theorem. In particular, this theorem does not prove that +the literal COPY producer is globally optimal. + +Scope of the result +------------------- +The seven tight floors concern raw recursive paid moments for fixed local +public boundaries and unchanged productive targets. They do not establish a +new complete bound, exclude lower ordinary scalar compilation costs, certify +new credits, or rule out shared multi-block construction or changing the +global public schedule. The eighth lifetime is deliberately left unresolved +by the stronger changed-internal-word claim. See PROOF-loss-space.md for a +separate global but non-additive preparation bound. + +Prepared for flyingviper with substantial OpenAI Codex assistance and +independent agent checks. Apache-2.0. diff --git a/research/p104-owned-cleanup-obstruction/PROOF-joint-cut.md b/research/p104-owned-cleanup-obstruction/PROOF-joint-cut.md new file mode 100644 index 0000000000..905c7d5881 --- /dev/null +++ b/research/p104-owned-cleanup-obstruction/PROOF-joint-cut.md @@ -0,0 +1,54 @@ +# A joint cut counts crossings, not their ranks + +The eight unchanged producer values are required as observations at their +retained one-dimensional delivery frames. They may be produced at different +times and erased afterward. All original public inputs remain independent; +owned INIT supplies zero and CLEAR deletes a row. Scalar contacts use one +common frame; public transport ascends and owned transport descends in frame +inclusion. This is the same literal row/frame model as PROOF-loss-space.md. + +Let W be the span of the eight delivery lines. The source-bound certificate +gives dim W=8. Partition original input symbols into those whose entry frames +are contained in W, and the outside symbols whose entry frames are not. +Project every scalar row onto the latter coordinates. + +Consider the span K of the projected rows that have ever appeared in registers +whose current frames are contained in W. Retain observations in K after their +physical registers are cleared or moved out. Initially K=0: each inside +register contains its own independent input, whose entry frame is inside W. +Common-frame scalar operations inside W only take linear combinations of +already available rows. Outside operations remain outside, and public ascent +cannot move an outside frame into W. INIT contributes zero and CLEAR cannot +increase K. An owned descent from outside W to inside W introduces one scalar +row and can increase dim K by at most one. Owned descents staying on the same +side contribute nothing new to this count. + +If the demanded observations have outside-coordinate matrix R, then + + number of owned descents crossing into W >= rank(R). + +The argument permits sequential outputs and arbitrary storage reuse: K is a +mathematical record of information ever available inside W, not an additional +physical register or an assumption that all outputs coexist. Any public +upward transport carrying an observed row out of W leaves that row in K; its +later return cannot invalidate the lower bound. + +`verify_joint_cut(word, producer_receipt)` reconstructs R from the exact +initial-input covectors and actual delivery scale factors. There are 112 +outside input roles and rank R=8. The receipt contains eight witness input +columns, the full rational 8-by-8 minor and its nonzero determinant. The source +has exactly eight crossing MOVE events, one for each owned role735--742, so it +attains this crossing-count floor. + +Two controls show the scope: duplicating one observation lowers the rank to7; +using the whole ambient space as W leaves no outside inputs and gives rank0. + +This does not prove a cost of8H7. Each crossing has its own rank, and the cut +only counts scalar rows that cross. Sharing cannot reduce the crossing count +below8 for these unchanged eight observations, but might still reduce their +ranks or other paid work. Removing a demanded intermediate value, changing its +payload or delivery frame, or changing the row/frame operation model is outside +the statement. No improved bound or whole-word tariff optimum is claimed. + +Prepared with OpenAI Codex assistance; no proof-kernel or independent human +acceptance is claimed. diff --git a/research/p104-owned-cleanup-obstruction/PROOF-loss-space.md b/research/p104-owned-cleanup-obstruction/PROOF-loss-space.md new file mode 100644 index 0000000000..40ba46bd42 --- /dev/null +++ b/research/p104-owned-cleanup-obstruction/PROOF-loss-space.md @@ -0,0 +1,84 @@ +# Global loss-space bound for an unchanged owned producer + +Let the ambient binary label space be E. Every original independent public +input x_i has entry frame A_i <= E. At any scalar-program instant, a live +register r has current frame F_r and row sum_i m_ri x_i. Define its source +support space L_r = sum_{i:m_ri != 0} A_i. Coefficients may be arbitrary elements +of a characteristic-zero field; cancellation can remove support but cannot +introduce a new input symbol. + +The model allows common-frame linear ADD/COPY/SCALE, public inclusion-ascent, +zero owned INIT, owned erasure, and owned inclusion-descent. It excludes hidden +nonascending public transports or native actions that change the literal row +semantics. Every owned descent of rank r is charged by r^t, 0 B with B <= A, choose any vector-space complement W +such that A=B direct-sum W. Replace V by V+W. For the moved field, + + L_r <= A+V = B+W+V. + +Other fields' bounds only become weaker. Since dim W = dim A-dim B, after all +owned descents to a chosen cut, + + dim V <= sum_j r_j, + +where r_j are their paid ranks. V may be shared by every register and persists +after owned erasures; erasing a register does not erase the global accounting. + +If a required output row v appears at frame F, with initial support space L, +then L<=F+V. Projecting to E/F gives + + sum_j r_j >= dim V >= dim(L+F)-dim F. + +Thus the total owned-transport moment up to that cut obeys + + sum_j r_j^t >= (sum_j r_j)^t >= [dim(L+F)-dim F]^t, + +using subadditivity of x^t for 0593 of +rank7, so it attains the owned-transport floor H7. The total owned-preparation moment for this retained value cannot fall below +H7 by moving COPY earlier, by arbitrary changed ascending public scalar +preparation, or by adding any number of owned preparations/erasures that still +deliver the same value at frame593 and have no offsetting new productive credit. + +All eight values individually have the same rank-mass lower bound7 at their +retained final one-dimensional delivery frames. This does not permit summing +the eight separate bounds: V is global, so a redesigned shared protocol could +amortize paid descents across different values. Owned738's source already splits +its rank7 descent to serve intermediate reads, so the scalar H7 floor is not a +claim of optimality for that complete multi-read itinerary. + +## Scope + +This is a floor for delivering one unchanged scalar value at one fixed frame, +not a bound on the final multiplication exponent. It does not exclude eliminating +that intermediate value, changing its payload, changing delivery frames, reusing +a descent paid for another target, adding productive credits, or a native-bearing +protocol outside the stated row/frame model. The theorem needs no search cutoff +and no fixed original scalar-contact windows. + +Prepared with OpenAI Codex assistance; no proof-kernel or independent human +acceptance is claimed. diff --git a/research/p104-owned-cleanup-obstruction/PROOF-windows.md b/research/p104-owned-cleanup-obstruction/PROOF-windows.md new file mode 100644 index 0000000000..8a3f8a50d8 --- /dev/null +++ b/research/p104-owned-cleanup-obstruction/PROOF-windows.md @@ -0,0 +1,149 @@ +# No common-chart hand-off in the omitted owned-holder states + +This is a source-bound obstruction to one successor hand-off template. It is +not an impossibility theorem for owned temporary registers or early cleanup. +No improved multiplication bound is claimed. Submission refresh found that +Ali Romman had independently published this same source domain and public-pair +mechanism in PR5579. This reconstruction corroborates that result; it is not +the novel claim of this package. See README.md for the distinct cost and +exceptional-delivery results. + +## Source and exact scope + +The input is PR5569's `research/p104-priced-handoff/WORD.json.gz` at commit +`af9f091ac6f30c6eaacb9c27777bfbe2d0e5ffdf`. Its compressed SHA-256 is +`12224e9a13a49c830b304338a8d31610fb43da15d1a650537733c27f7864310f`. +It has 735 arbitrary public inputs, 743 physical role IDs, 25,140 events, +104 live main ports and 527 productive helpers. Eight owned lifetimes use +roles 735 through 742, with peak live owned storage one. + +The omitted predecessor domain comprises states in which an owned register +contains a nonzero coefficient of a productive helper's original input. +The existing screen skipped 2,832 distinct helper/holder/window geometries. +Our checker replays *every* source event boundary, including MOVE boundaries, +and imposes no touched-symbol or first/last-use restriction. It finds 5,252 +helper/boundary pairs, 2,832 distinct full-holder geometries, and 2,340 distinct +public-holder geometries. + +We retain the chronological scalar events, their operand roles and contact +charts, including COPY and the boundaries of owned lifetimes. MOVE events may +be relocated, added, deleted or replaced within the resulting scalar-contact +windows, provided public transports remain ascending. At a cut we ask whether +one common chart can accommodate the nominated helper and every public role +that currently contains its original input symbol. All restrictions on owned +register charts are dropped in this test. We also allow every binary subspace +as a putative contact chart, not merely a listed source frame. + +The theorem excludes this single-common-chart successor hand-off at every +state in the omitted domain. It does not exclude earlier synthesis, changed +scalar contacts, multiple-chart cleanup networks, or different boundary maps. + +## The window lemma + +Fix a boundary immediately after a source event. For a public role `r`, let +`A_r` be its preceding scalar-contact chart, or initial chart if there is no +preceding contact. Let `B_r` be its following scalar-contact chart, or final +chart if there is no following contact. A contact introduced at a chart `F` +within this window must satisfy + +``` +A_r subseteq F subseteq B_r. +``` + +This follows from ascending public transports and unchanged scalar-contact +boundaries. It does not depend on how many transports are inserted or where +they occur in the window. + +Consequently, if required roles `a,b` have a binary vector `v` with + +``` +v in A_a, v not in B_b, +``` + +there is no common chart for those two roles, and therefore none for the +entire required set. Indeed, a common chart would imply +`A_a subseteq F subseteq B_b`, contradicting this vector. + +This elementary pair obstruction is stronger than the failure of a search +over a chosen frame list: it rules out every possible common subspace `F`. + +## Exact source certificate + +The checker interprets every source scalar operation over the rational numbers +on formal independent public-input symbols. INIT zeros the owned row; COPY +copies into an empty owned row; CLEAR erases it under the source ownership +contract. MOVEs preserve these normalized symbolic rows. Source transports, +ownership and common scalar charts are checked along the way. At the end all +743 output rows must equal the declared public map or the cleared owned row. +No public input is set to zero. + +After every event, for every productive helper symbol present in an active +owned row, the checker reconstructs all public holders. The nominated helper +role is also included whether or not its current coefficient is nonzero. +The preceding and following scalar contacts supply each holder's window. +For every one of the 5,252 helper/boundary pairs, a pair of public holders and +a separating binary vector satisfy the window lemma. Thus the obstruction +persists even if the owned holders may be moved at zero cost to arbitrary +charts or ignored altogether. + +Boundaries between consecutive events have constant symbolic rows and the same +adjacent scalar contacts; MOVE-only changes do not introduce an unexamined +window. Hence the event-boundary enumeration covers all temporal cuts in this +fixed-contact domain. The initial and final states have no active owned field. + +The receipt records the counts, per-owned-role census, sample witnesses and a +SHA-256 of the deterministically reconstructed complete witness list. The +optional `--witnesses PATH` flag emits every witness. Each witness contains the +two public role IDs, their relevant boundary frames, and the missing vector. +Verifying it needs only binary span membership and the reconstructed source +windows; no optimization solver or floating-point comparison is used. + +## Positive and negative controls + +On the pinned PR5561 predecessor, after event 15443 the known helper706/173 +cleanup has + +``` +row706 = input706 + (1/2) row173. +``` + +Both scalar windows contain frame559 of dimension8, strictly between +helper706's initial and final dimensions0 and9. The same window checker accepts +that common chart. This is the published positive example behind PR5569, +not a new contribution. + +Four corruption controls reject changed source bytes, the zero vector in +place of a separating vector, substitution of an owned role for a required +public holder, and a reversed public transport window. These run under normal +and optimized Python, without relying on `assert` statements. + +Source role173 is a productive helper because61 is absent from the live-port +list. PR5569's prose calls it a main Y register; our computation uses the actual +source role classification. This descriptive discrepancy does not invalidate +its cleanup identity or the positive control. + +## What this result changes + +Simply extending the predecessor's common-chart scan to its omitted owned +holder states cannot produce an improvement while those scalar contacts remain +fixed. The next useful test must change a hypothesis: synthesize a copy before +an incompatible public contact, change a scalar dependency, or design and fully +price a cleanup network with several contact charts. Additional coefficient +search at the obstructed common chart cannot help. + +The result has no tariff or global optimality claim. It does not assert that +the inherited conditional P104 construction is admitted, that arbitrary owned +erasure is free outside that contract, or that every productive-helper design +has the same obstruction. + +## Attribution + +PR5569: GamingPuzzled, successor hand-off and omitted-domain identification. +PR5561: DreamingOfClouds, free helper endpoints and source word. +PR5551: thu-nmrc, coupled contacts. PR5544/5545: Ali Romman, P104 caller and +local verifier. Retain the native, Clifford, compiler, geometry, precision and +analytic predecessor credits in those packages. The window lemma is elementary; +the contribution is its exact application to the formerly omitted source domain. + +Prepared for flyingviper with substantial OpenAI Codex assistance and independent +agent checks. Apache-2.0. No proof-kernel or independent human acceptance is claimed. diff --git a/research/p104-owned-cleanup-obstruction/README.md b/research/p104-owned-cleanup-obstruction/README.md new file mode 100644 index 0000000000..30fc5fedb0 --- /dev/null +++ b/research/p104-owned-cleanup-obstruction/README.md @@ -0,0 +1,136 @@ +# P104 owned-cleanup obstructions + +**Scoped negative result; no new kappa, construction, productive credit or +selected-frontier change.** This proves seven fixed-boundary owned-block cost floors, a joint crossing-count +floor, and a public multi-partner obstruction for the exceptional eighth block. +The results exclude concrete ways to save transport cost on PR5569's frozen +word, not owned temporaries in general. + +Submission refresh found concurrent [PR5579](https://github.com/CrocSwap/integer-mult-bounds/pull/5579), +which already publishes the same 5,252-case public-window obstruction. Our +independent reconstruction is retained as corroborating source validation, not +claimed as novel. The cost floors, joint cut and 29,688-case exceptional-block +test below are the additional results. [Discussion5575](https://github.com/CrocSwap/integer-mult-bounds/discussions/5575) +now investigates compensated source substitution; that changed-dependency +scope is distinct and remains open. [PR5580](https://github.com/CrocSwap/integer-mult-bounds/pull/5580) +reports a gain by changing another scalar contact. We do not claim our frozen +PR5569 checks automatically apply to that changed word. + +## Results + +| Question | Checked result | Essential restriction | +| --- | --- | --- | +| Independent check of PR5579: can omitted owned-holder states support one common-chart cleanup? | All **5,252 helper/boundary pairs**, representing **2,832 full-holder geometries** and **2,340 public geometries**, have a two-public-role obstruction. | Unchanged scalar contacts; the nominated helper and all its public input-symbol holders meet at one chart. | +| Can a different internal word improve an owned delivery star? | **Seven of eight blocks attain a proved raw paid-moment floor** for every `07->6->{3 or 4}->1`, with the same minimal route + histogram. For **29,688 recipient/cut pairs**, no public linear combination + can replace one nominated delivery at one common frame. The public rows + form a basis, so the copied value has unique necessary support. This is not + a limit on partner count or a coefficient-grid search. + +Here `H_d(t)=d^t`, with `t=1-kappa`. Fewer ADDs alone do not improve the recursive +invoice. The tight star tariffs are `3H1+H7`, `3H1+H7`, `2H1+H7`, and four copies +of `5H1+H7`. Their combined `28H1+7H7` is a floor only for **separate** replacements +respecting all seven boundaries. Owned738's observed tariff is `5H1+H2+H3`; +the star theorem does not prove it optimal under arbitrary replacement. + +The [window proof](PROOF-windows.md) excludes every binary contact subspace, +not just listed source frames. The [block proof](PROOF-blocks.md) allows arbitrary +rational internal words and private zero auxiliaries inside its fixed boundary. +The [loss-space proof](PROOF-loss-space.md) allows changed preparation and erased +fields, but accounts globally for their descents. This global accounting is why +the per-value floors are not additive. + +## Source and independent checks + +Source: [PR5569](https://github.com/CrocSwap/integer-mult-bounds/pull/5569), +head `af9f091ac6f30c6eaacb9c27777bfbe2d0e5ffdf`. The two unchanged compressed +inputs and credits are retained [here](inputs/README.md). [SOURCES.json](SOURCES.json) +pins use a retention commit in this PR's own history; a clean replay needs no +cached, unmerged predecessor objects. Base main was +`5e0052ca0aa3036a3afa8b0438927377c8d97d53`. + +The new replay checks all **743 final scalar rows**, preserving all 735 arbitrary +public inputs and clearing eight owned fields. It checks common scalar charts, +transport nesting and lifetimes. Each block's actual prefix and public suffix +have full ranks `4,4,3,6,6,6,6,6`; an unobservable local-map change cannot evade +the fixed-boundary result. Omitting a delivery changes final public outputs. + +An independent agent implemented the complete window census before reading the +candidate code, reproducing all three counts and public-only obstructions. +Other agents derived boundary and support checks, reviewed proofs and searched +primary literature. These are author checks, not independent human acceptance. + +The original PR5569 full verifier was run unchanged before this analysis and +returned `PASS P104_PRICED_HANDOFF`, including native/transposed replay, physical +caller, both moment engines, 54 strict plus four functional outer checks and +root interval `(0.00308181851522, 0.00308181851523)`. This is conditional, +unselected **predecessor baseline evidence**, not a new result. The small +registered replay here does not repeat that complete native/funding suite. + +## Reproduce + +Python 3.12, standard library only. Direct scientific replay needs no solver, +network, shell tools or Git. From the repository root: + +```sh +python3.12 -I -B research/p104-owned-cleanup-obstruction/verify.py +python3.12 -I -O -B research/p104-owned-cleanup-obstruction/verify.py +python3.12 -B scripts/research_package.py --package research/p104-owned-cleanup-obstruction +``` + +The verifier compares its fresh exact result with [RESULT.json](RESULT.json). +Normal runs do not write files. `--witnesses PATH` optionally exports all window +witnesses; `--write` explicitly authors a receipt. Known successful cleanup706/173 +is a positive control. Semantic controls reject changed source bytes, invalid +witnesses, reversed transports, changed payloads, incorrect delivery signs/frames +and a zeroed producer. Widening a delivery frame correctly weakens the producer +floor. Scientific checks do not depend on Python assertions. + +The registered runner also checks metadata and Git provenance and needs full +history. Exported source runs the direct verifier without Git. This publication +also checks committed bytes, source ancestry and a Git-free exported replay. + +## Literature and interpretation + +The [literature note](LITERATURE.md) separates useful linear-circuit ideas from +what is proved for this tariff. The two-sided boundary identity `S(R-T)P=0` and +full-rank implication `R=T` are elementary linear algebra, proved explicitly. +No paper is treated as evidence of a legal or cheaper P104 construction. + +The result corroborates PR5579's common-chart obstruction and establishes +additional fixed-boundary optima and delivery obstructions. Further coefficient search in those domains cannot help; +the dependency or boundary model must change. The whole productive-helper +programme is not ruled out. + +## Open next questions + +- Can a changed public dependency or cleanup using several contact charts lower + the complete paid-minus-productive profile? First specify one replacement map + and its entry/exit frames, then derive its histogram. +- Can a joint construction share preparation across owned lifetimes? Identify + a specific transport serving two demanded values and check its exact map; + adding the individual H7 bounds is invalid. Include all restorations, helpers, + ordinary passes and ownership obligations before claiming a gain. + +See [TASK.json](TASK.json) for the task refinement, expansion gate and stop rule. + +## Credit + +Prepared for flyingviper with substantial OpenAI Codex assistance and independent +agents; Apache-2.0. Ali Romman independently published the overlapping +window obstruction in PR5579 before our submission. Retain Joel Pulikkan (GamingPuzzled)'s PR5569 mechanism and +open question; DreamingOfClouds's PR5561/5553 endpoints and word; thu-nmrc's PR5551 +contacts; Ali Romman's PR5544/5545 verifier and caller; and the full predecessor +lineage in [inputs/README.md](inputs/README.md). No source construction is newly +attributed to this package. No proof-kernel acceptance is claimed. diff --git a/research/p104-owned-cleanup-obstruction/RESULT.json b/research/p104-owned-cleanup-obstruction/RESULT.json new file mode 100644 index 0000000000..ed8b2b2055 --- /dev/null +++ b/research/p104-owned-cleanup-obstruction/RESULT.json @@ -0,0 +1,5509 @@ +{ + "joint_cut": { + "delivery_space_basis": [ + 394, + 128, + 75, + 42, + 25, + 8, + 7, + 1 + ], + "delivery_space_dimension": 8, + "eight_H7_tariff_claimed": false, + "new_bound": false, + "observation_rank": 8, + "outside_input_count": 112, + "required_owned_crossing_count": 8, + "scope_controls": { + "duplicated_output_rank": 7, + "whole_space_rank": 0 + }, + "source_crossings": [ + { + "event": 13381, + "from": 559, + "owned": 735, + "paid_rank": 7, + "to": 593 + }, + { + "event": 13392, + "from": 543, + "owned": 736, + "paid_rank": 7, + "to": 594 + }, + { + "event": 13403, + "from": 531, + "owned": 737, + "paid_rank": 7, + "to": 595 + }, + { + "event": 13416, + "from": 564, + "owned": 738, + "paid_rank": 3, + "to": 596 + }, + { + "event": 13428, + "from": 518, + "owned": 739, + "paid_rank": 7, + "to": 598 + }, + { + "event": 13443, + "from": 267, + "owned": 740, + "paid_rank": 7, + "to": 599 + }, + { + "event": 13458, + "from": 517, + "owned": 741, + "paid_rank": 7, + "to": 600 + }, + { + "event": 13473, + "from": 477, + "owned": 742, + "paid_rank": 7, + "to": 601 + } + ], + "status": "PASS_JOINT_OWNED_CROSSING_COUNT_FLOOR", + "witness_determinant": "-1/32768", + "witness_input_columns": [ + 0, + 1, + 4, + 6, + 12, + 13, + 15, + 27 + ], + "witness_minor": [ + [ + "0", + "1/4", + "1/4", + "0", + "-1/4", + "-1/4", + "0", + "0" + ], + [ + "0", + "0", + "-1/4", + "1/4", + "0", + "1/4", + "1/4", + "-1/4" + ], + [ + "1/4", + "0", + "0", + "0", + "0", + "0", + "1/4", + "0" + ], + [ + "0", + "0", + "0", + "0", + "1/4", + "0", + "1/4", + "0" + ], + [ + "0", + "-1/4", + "-1/4", + "1/4", + "0", + "1/4", + "0", + "0" + ], + [ + "1/4", + "0", + "0", + "0", + "1/4", + "0", + "0", + "1/4" + ], + [ + "0", + "0", + "0", + "0", + "1/4", + "1/4", + "0", + "0" + ], + [ + "0", + "0", + "1/4", + "0", + "0", + "0", + "-1/4", + "0" + ] + ] + }, + "lifetime_controls": [ + { + "mutation": "wrong_delivery_sign", + "reason": "fixed local transfer coefficient", + "rejected": true + }, + { + "mutation": "zeroed_owned_producer", + "reason": "exact local delivery form", + "rejected": true + }, + { + "mutation": "wrong_delivery_frame", + "reason": "ADD/COPY common frame", + "rejected": true + } + ], + "lifetimes": { + "global_claim_excluded": "Per-row owned-preparation floors cannot be added when private work or lost subspaces are shared.", + "lifetimes": [ + { + "actual_prefix_rank": 4, + "corruption_changed_public_outputs": [ + 119, + 121, + 169, + 191, + 193, + 204, + 206, + 706 + ], + "entry_dimensions": { + "173": 8, + "704": 0, + "705": 0, + "706": 0 + }, + "entry_frames": { + "173": 559, + "704": 3, + "705": 3, + "706": 3 + }, + "events_half_open": [ + 13377, + 13388 + ], + "exit_dimensions": { + "173": 8, + "704": 1, + "705": 1, + "706": 1 + }, + "exit_frames": { + "173": 559, + "704": 593, + "705": 593, + "706": 593 + }, + "local_matrix": [ + { + "0": "1" + }, + { + "0": "1/2", + "1": "1" + }, + { + "0": "1/2", + "2": "1" + }, + { + "0": "1/2", + "3": "1" + }, + {} + ], + "local_paid_histogram": { + "1": 3, + "7": 1 + }, + "no_gain_scope": "Exact local public boundary charts and map; arbitrary private zero auxiliaries; no outside side information, changed productive targets or credits.", + "omitted_delivery_event": 13386, + "owned": 735, + "owned_exit_zero": true, + "owned_paid_histogram": { + "7": 1 + }, + "owned_public_suffix_column_zero": true, + "public_paid_histogram": { + "1": 3 + }, + "public_suffix_rank": 4, + "recipients": [ + 704, + 705, + 706 + ], + "source": 173, + "source_entry_support_span_dimension": 8, + "source_prefix_nonzeros": 118, + "source_role": "helper", + "support_to_recipient_exit_dimension_gaps": { + "704": 7, + "705": 7, + "706": 7 + }, + "tight_fixed_boundary_star_theorem_applies": true, + "transfers_from_source": { + "704": "1/2", + "705": "1/2", + "706": "1/2" + } + }, + { + "actual_prefix_rank": 4, + "corruption_changed_public_outputs": [ + 113, + 118, + 140, + 141, + 142, + 170, + 171, + 172, + 185, + 186, + 187, + 194, + 195, + 196, + 198, + 214, + 733 + ], + "entry_dimensions": { + "151": 8, + "707": 0, + "708": 0, + "733": 0 + }, + "entry_frames": { + "151": 543, + "707": 3, + "708": 3, + "733": 3 + }, + "events_half_open": [ + 13388, + 13399 + ], + "exit_dimensions": { + "151": 8, + "707": 1, + "708": 1, + "733": 1 + }, + "exit_frames": { + "151": 543, + "707": 594, + "708": 594, + "733": 594 + }, + "local_matrix": [ + { + "0": "1" + }, + { + "0": "1/2", + "1": "1" + }, + { + "0": "1/2", + "2": "1" + }, + { + "0": "1/2", + "3": "1" + }, + {} + ], + "local_paid_histogram": { + "1": 3, + "7": 1 + }, + "no_gain_scope": "Exact local public boundary charts and map; arbitrary private zero auxiliaries; no outside side information, changed productive targets or credits.", + "omitted_delivery_event": 13397, + "owned": 736, + "owned_exit_zero": true, + "owned_paid_histogram": { + "7": 1 + }, + "owned_public_suffix_column_zero": true, + "public_paid_histogram": { + "1": 3 + }, + "public_suffix_rank": 4, + "recipients": [ + 707, + 708, + 733 + ], + "source": 151, + "source_entry_support_span_dimension": 8, + "source_prefix_nonzeros": 113, + "source_role": "helper", + "support_to_recipient_exit_dimension_gaps": { + "707": 7, + "708": 7, + "733": 7 + }, + "tight_fixed_boundary_star_theorem_applies": true, + "transfers_from_source": { + "707": "1/2", + "708": "1/2", + "733": "1/2" + } + }, + { + "actual_prefix_rank": 3, + "corruption_changed_public_outputs": [ + 116, + 117, + 120, + 134, + 135, + 136, + 138, + 144, + 145, + 147, + 157, + 160, + 161, + 162, + 176, + 177, + 178, + 179, + 180, + 181, + 192, + 197, + 200, + 207, + 208, + 209, + 210, + 219, + 220, + 221, + 732 + ], + "entry_dimensions": { + "146": 8, + "709": 0, + "732": 0 + }, + "entry_frames": { + "146": 531, + "709": 3, + "732": 3 + }, + "events_half_open": [ + 13399, + 13408 + ], + "exit_dimensions": { + "146": 8, + "709": 1, + "732": 1 + }, + "exit_frames": { + "146": 531, + "709": 595, + "732": 595 + }, + "local_matrix": [ + { + "0": "1" + }, + { + "0": "-1/2", + "1": "1" + }, + { + "0": "-1/2", + "2": "1" + }, + {} + ], + "local_paid_histogram": { + "1": 2, + "7": 1 + }, + "no_gain_scope": "Exact local public boundary charts and map; arbitrary private zero auxiliaries; no outside side information, changed productive targets or credits.", + "omitted_delivery_event": 13406, + "owned": 737, + "owned_exit_zero": true, + "owned_paid_histogram": { + "7": 1 + }, + "owned_public_suffix_column_zero": true, + "public_paid_histogram": { + "1": 2 + }, + "public_suffix_rank": 3, + "recipients": [ + 709, + 732 + ], + "source": 146, + "source_entry_support_span_dimension": 8, + "source_prefix_nonzeros": 120, + "source_role": "helper", + "support_to_recipient_exit_dimension_gaps": { + "709": 7, + "732": 7 + }, + "tight_fixed_boundary_star_theorem_applies": true, + "transfers_from_source": { + "709": "-1/2", + "732": "-1/2" + } + }, + { + "actual_prefix_rank": 6, + "corruption_changed_public_outputs": [ + 127, + 132, + 136, + 140, + 144, + 147, + 153, + 157, + 158, + 160, + 165, + 170, + 183, + 187, + 194, + 197, + 202, + 210, + 218, + 219, + 734 + ], + "entry_dimensions": { + "133": 8, + "148": 2, + "159": 7, + "203": 6, + "710": 0, + "734": 0 + }, + "entry_frames": { + "133": 591, + "148": 467, + "159": 565, + "203": 564, + "710": 3, + "734": 3 + }, + "events_half_open": [ + 13408, + 13424 + ], + "exit_dimensions": { + "133": 8, + "148": 3, + "159": 7, + "203": 6, + "710": 1, + "734": 1 + }, + "exit_frames": { + "133": 591, + "148": 596, + "159": 565, + "203": 564, + "710": 597, + "734": 597 + }, + "local_matrix": [ + { + "0": "1" + }, + { + "0": "1/2", + "1": "1" + }, + { + "0": "-1", + "2": "1" + }, + { + "0": "-1", + "3": "1" + }, + { + "0": "-1/2", + "4": "1" + }, + { + "0": "-1/2", + "5": "1" + }, + {} + ], + "local_paid_histogram": { + "1": 5, + "2": 1, + "3": 1 + }, + "no_gain_scope": "No tight local cost floor claimed: delivery charts have several levels.", + "omitted_delivery_event": 13422, + "owned": 738, + "owned_exit_zero": true, + "owned_paid_histogram": { + "1": 2, + "2": 1, + "3": 1 + }, + "owned_public_suffix_column_zero": true, + "public_paid_histogram": { + "1": 3 + }, + "public_suffix_rank": 6, + "recipients": [ + 159, + 203, + 148, + 710, + 734 + ], + "source": 133, + "source_entry_support_span_dimension": 8, + "source_prefix_nonzeros": 110, + "source_role": "helper", + "support_to_recipient_exit_dimension_gaps": { + "148": 5, + "159": 1, + "203": 2, + "710": 7, + "734": 7 + }, + "tight_fixed_boundary_star_theorem_applies": false, + "transfers_from_source": { + "148": "-1", + "159": "1/2", + "203": "-1", + "710": "-1/2", + "734": "-1/2" + } + }, + { + "actual_prefix_rank": 6, + "corruption_changed_public_outputs": [ + 121, + 137, + 184, + 206, + 716 + ], + "entry_dimensions": { + "256": 8, + "712": 0, + "713": 0, + "714": 0, + "715": 0, + "716": 0 + }, + "entry_frames": { + "256": 518, + "712": 3, + "713": 3, + "714": 3, + "715": 3, + "716": 3 + }, + "events_half_open": [ + 13424, + 13439 + ], + "exit_dimensions": { + "256": 8, + "712": 1, + "713": 1, + "714": 1, + "715": 1, + "716": 1 + }, + "exit_frames": { + "256": 518, + "712": 598, + "713": 598, + "714": 598, + "715": 598, + "716": 598 + }, + "local_matrix": [ + { + "0": "1" + }, + { + "0": "1/4", + "1": "1" + }, + { + "0": "1/4", + "2": "1" + }, + { + "0": "1/4", + "3": "1" + }, + { + "0": "1/4", + "4": "1" + }, + { + "0": "1/4", + "5": "1" + }, + {} + ], + "local_paid_histogram": { + "1": 5, + "7": 1 + }, + "no_gain_scope": "Exact local public boundary charts and map; arbitrary private zero auxiliaries; no outside side information, changed productive targets or credits.", + "omitted_delivery_event": 13437, + "owned": 739, + "owned_exit_zero": true, + "owned_paid_histogram": { + "7": 1 + }, + "owned_public_suffix_column_zero": true, + "public_paid_histogram": { + "1": 5 + }, + "public_suffix_rank": 6, + "recipients": [ + 712, + 713, + 714, + 715, + 716 + ], + "source": 256, + "source_entry_support_span_dimension": 8, + "source_prefix_nonzeros": 106, + "source_role": "helper", + "support_to_recipient_exit_dimension_gaps": { + "712": 7, + "713": 7, + "714": 7, + "715": 7, + "716": 7 + }, + "tight_fixed_boundary_star_theorem_applies": true, + "transfers_from_source": { + "712": "1/4", + "713": "1/4", + "714": "1/4", + "715": "1/4", + "716": "1/4" + } + }, + { + "actual_prefix_rank": 6, + "corruption_changed_public_outputs": [ + 120, + 138, + 176, + 177, + 178, + 207, + 208, + 209, + 721 + ], + "entry_dimensions": { + "717": 0, + "718": 0, + "719": 0, + "720": 0, + "721": 0, + "92": 8 + }, + "entry_frames": { + "717": 3, + "718": 3, + "719": 3, + "720": 3, + "721": 3, + "92": 267 + }, + "events_half_open": [ + 13439, + 13454 + ], + "exit_dimensions": { + "717": 1, + "718": 1, + "719": 1, + "720": 1, + "721": 1, + "92": 8 + }, + "exit_frames": { + "717": 599, + "718": 599, + "719": 599, + "720": 599, + "721": 599, + "92": 267 + }, + "local_matrix": [ + { + "0": "1" + }, + { + "0": "1/4", + "1": "1" + }, + { + "0": "1/4", + "2": "1" + }, + { + "0": "1/4", + "3": "1" + }, + { + "0": "1/4", + "4": "1" + }, + { + "0": "1/4", + "5": "1" + }, + {} + ], + "local_paid_histogram": { + "1": 5, + "7": 1 + }, + "no_gain_scope": "Exact local public boundary charts and map; arbitrary private zero auxiliaries; no outside side information, changed productive targets or credits.", + "omitted_delivery_event": 13452, + "owned": 740, + "owned_exit_zero": true, + "owned_paid_histogram": { + "7": 1 + }, + "owned_public_suffix_column_zero": true, + "public_paid_histogram": { + "1": 5 + }, + "public_suffix_rank": 6, + "recipients": [ + 717, + 718, + 719, + 720, + 721 + ], + "source": 92, + "source_entry_support_span_dimension": 8, + "source_prefix_nonzeros": 111, + "source_role": "live", + "support_to_recipient_exit_dimension_gaps": { + "717": 7, + "718": 7, + "719": 7, + "720": 7, + "721": 7 + }, + "tight_fixed_boundary_star_theorem_applies": true, + "transfers_from_source": { + "717": "1/4", + "718": "1/4", + "719": "1/4", + "720": "1/4", + "721": "1/4" + } + }, + { + "actual_prefix_rank": 6, + "corruption_changed_public_outputs": [ + 144, + 153, + 154, + 157, + 164, + 165, + 197, + 219, + 726 + ], + "entry_dimensions": { + "722": 0, + "723": 0, + "724": 0, + "725": 0, + "726": 0, + "9": 8 + }, + "entry_frames": { + "722": 3, + "723": 3, + "724": 3, + "725": 3, + "726": 3, + "9": 517 + }, + "events_half_open": [ + 13454, + 13469 + ], + "exit_dimensions": { + "722": 1, + "723": 1, + "724": 1, + "725": 1, + "726": 1, + "9": 8 + }, + "exit_frames": { + "722": 600, + "723": 600, + "724": 600, + "725": 600, + "726": 600, + "9": 517 + }, + "local_matrix": [ + { + "0": "1" + }, + { + "0": "1/4", + "1": "1" + }, + { + "0": "1/4", + "2": "1" + }, + { + "0": "1/4", + "3": "1" + }, + { + "0": "1/4", + "4": "1" + }, + { + "0": "1/4", + "5": "1" + }, + {} + ], + "local_paid_histogram": { + "1": 5, + "7": 1 + }, + "no_gain_scope": "Exact local public boundary charts and map; arbitrary private zero auxiliaries; no outside side information, changed productive targets or credits.", + "omitted_delivery_event": 13467, + "owned": 741, + "owned_exit_zero": true, + "owned_paid_histogram": { + "7": 1 + }, + "owned_public_suffix_column_zero": true, + "public_paid_histogram": { + "1": 5 + }, + "public_suffix_rank": 6, + "recipients": [ + 722, + 723, + 724, + 725, + 726 + ], + "source": 9, + "source_entry_support_span_dimension": 8, + "source_prefix_nonzeros": 103, + "source_role": "live", + "support_to_recipient_exit_dimension_gaps": { + "722": 7, + "723": 7, + "724": 7, + "725": 7, + "726": 7 + }, + "tight_fixed_boundary_star_theorem_applies": true, + "transfers_from_source": { + "722": "1/4", + "723": "1/4", + "724": "1/4", + "725": "1/4", + "726": "1/4" + } + }, + { + "actual_prefix_rank": 6, + "corruption_changed_public_outputs": [ + 116, + 134, + 145, + 162, + 176, + 181, + 208, + 220, + 731 + ], + "entry_dimensions": { + "240": 8, + "727": 0, + "728": 0, + "729": 0, + "730": 0, + "731": 0 + }, + "entry_frames": { + "240": 477, + "727": 3, + "728": 3, + "729": 3, + "730": 3, + "731": 3 + }, + "events_half_open": [ + 13469, + 13484 + ], + "exit_dimensions": { + "240": 8, + "727": 1, + "728": 1, + "729": 1, + "730": 1, + "731": 1 + }, + "exit_frames": { + "240": 477, + "727": 601, + "728": 601, + "729": 601, + "730": 601, + "731": 601 + }, + "local_matrix": [ + { + "0": "1" + }, + { + "0": "-1/4", + "1": "1" + }, + { + "0": "-1/4", + "2": "1" + }, + { + "0": "-1/4", + "3": "1" + }, + { + "0": "-1/4", + "4": "1" + }, + { + "0": "-1/4", + "5": "1" + }, + {} + ], + "local_paid_histogram": { + "1": 5, + "7": 1 + }, + "no_gain_scope": "Exact local public boundary charts and map; arbitrary private zero auxiliaries; no outside side information, changed productive targets or credits.", + "omitted_delivery_event": 13482, + "owned": 742, + "owned_exit_zero": true, + "owned_paid_histogram": { + "7": 1 + }, + "owned_public_suffix_column_zero": true, + "public_paid_histogram": { + "1": 5 + }, + "public_suffix_rank": 6, + "recipients": [ + 727, + 728, + 729, + 730, + 731 + ], + "source": 240, + "source_entry_support_span_dimension": 8, + "source_prefix_nonzeros": 105, + "source_role": "helper", + "support_to_recipient_exit_dimension_gaps": { + "727": 7, + "728": 7, + "729": 7, + "730": 7, + "731": 7 + }, + "tight_fixed_boundary_star_theorem_applies": true, + "transfers_from_source": { + "727": "-1/4", + "728": "-1/4", + "729": "-1/4", + "730": "-1/4", + "731": "-1/4" + } + } + ], + "new_kappa": false, + "status": "PASS_EIGHT_OWNED_BOUNDARIES_SEVEN_TIGHT_STARS" + }, + "new_bound": false, + "owned738": { + "all_public_replacement_boundaries": 29688, + "corruption_controls": { + "altered_target_functional": true, + "copied_public_producer_changed": true, + "singular_public_scale": true, + "zero_separating_vector": true + }, + "covector_positive_control": "D=x0 before x0+=2*x1 becomes x0-2*x1 afterward", + "delivery_windows": [ + { + "event": 13412, + "lower_frame": 565, + "maximum_dimension": 7, + "minimum_dimension": 7, + "next_contact": 15575, + "previous_contact": 13363, + "recipient": 159, + "upper_frame": 565 + }, + { + "event": 13414, + "lower_frame": 564, + "maximum_dimension": 6, + "minimum_dimension": 6, + "next_contact": 14027, + "previous_contact": 13245, + "recipient": 203, + "upper_frame": 633 + }, + { + "event": 13417, + "lower_frame": 467, + "maximum_dimension": 4, + "minimum_dimension": 3, + "next_contact": 14018, + "previous_contact": 13233, + "recipient": 148, + "upper_frame": 655 + }, + { + "event": 13420, + "lower_frame": 3, + "maximum_dimension": 1, + "minimum_dimension": 1, + "next_contact": 13524, + "previous_contact": 817, + "recipient": 710, + "upper_frame": 597 + }, + { + "event": 13422, + "lower_frame": 3, + "maximum_dimension": 1, + "minimum_dimension": 1, + "next_contact": 14006, + "previous_contact": 804, + "recipient": 734, + "upper_frame": 597 + } + ], + "effective_public_operations": { + "ADD": 20947, + "SCALE": 707, + "owned_to_public_shear": 33 + }, + "initial_value_support": 110, + "new_bound": false, + "owned_paid_histogram_both_alternatives": { + "1": 2, + "2": 1, + "3": 1 + }, + "pair_examples": { + "148": { + "boundary": 13233, + "bounds": [ + [ + 25, + 292, + 292 + ], + [ + 31, + 307, + 570 + ], + [ + 32, + 348, + 572 + ], + [ + 33, + 365, + 573 + ], + [ + 36, + 499, + 562 + ], + [ + 69, + 442, + 577 + ], + [ + 74, + 401, + 575 + ], + [ + 75, + 386, + 574 + ], + [ + 88, + 421, + 576 + ], + [ + 91, + 268, + 561 + ], + [ + 99, + 481, + 481 + ], + [ + 102, + 330, + 571 + ], + [ + 133, + 459, + 564 + ], + [ + 148, + 467, + 655 + ], + [ + 159, + 3, + 489 + ], + [ + 191, + 3, + 292 + ], + [ + 203, + 278, + 563 + ], + [ + 269, + 297, + 297 + ], + [ + 287, + 317, + 570 + ], + [ + 301, + 336, + 571 + ], + [ + 317, + 356, + 572 + ], + [ + 335, + 373, + 573 + ], + [ + 349, + 392, + 574 + ], + [ + 367, + 411, + 575 + ], + [ + 383, + 429, + 576 + ], + [ + 397, + 450, + 577 + ], + [ + 415, + 467, + 562 + ], + [ + 429, + 489, + 489 + ], + [ + 445, + 507, + 507 + ], + [ + 483, + 3, + 3 + ], + [ + 494, + 3, + 3 + ], + [ + 519, + 3, + 3 + ], + [ + 530, + 3, + 3 + ], + [ + 697, + 1031, + 1041 + ], + [ + 698, + 1031, + 1042 + ], + [ + 701, + 1031, + 1043 + ], + [ + 702, + 1031, + 1044 + ] + ], + "pair": [ + 148, + 31, + 467, + 570, + 45 + ], + "support_size": 36 + }, + "159": { + "boundary": 13363, + "bounds": [ + [ + 133, + 565, + 591 + ], + [ + 159, + 565, + 565 + ], + [ + 697, + 1041, + 1045 + ], + [ + 698, + 1042, + 1046 + ], + [ + 701, + 1043, + 1046 + ], + [ + 702, + 1044, + 1045 + ] + ], + "pair": [ + 159, + 697, + 565, + 1045, + 2 + ], + "support_size": 5 + }, + "203": { + "boundary": 13245, + "bounds": [ + [ + 25, + 292, + 292 + ], + [ + 31, + 307, + 570 + ], + [ + 32, + 348, + 572 + ], + [ + 33, + 365, + 573 + ], + [ + 69, + 442, + 577 + ], + [ + 74, + 401, + 575 + ], + [ + 75, + 386, + 574 + ], + [ + 88, + 421, + 576 + ], + [ + 91, + 561, + 565 + ], + [ + 99, + 481, + 481 + ], + [ + 102, + 330, + 571 + ], + [ + 133, + 564, + 565 + ], + [ + 159, + 3, + 489 + ], + [ + 191, + 3, + 292 + ], + [ + 203, + 564, + 633 + ], + [ + 269, + 297, + 297 + ], + [ + 287, + 317, + 570 + ], + [ + 301, + 336, + 571 + ], + [ + 317, + 356, + 572 + ], + [ + 335, + 373, + 573 + ], + [ + 349, + 392, + 574 + ], + [ + 367, + 411, + 575 + ], + [ + 383, + 429, + 576 + ], + [ + 397, + 450, + 577 + ], + [ + 429, + 489, + 489 + ], + [ + 445, + 507, + 507 + ], + [ + 483, + 3, + 3 + ], + [ + 494, + 3, + 3 + ], + [ + 519, + 3, + 3 + ], + [ + 530, + 3, + 3 + ], + [ + 697, + 1031, + 1041 + ], + [ + 698, + 1031, + 1042 + ], + [ + 701, + 1031, + 1043 + ], + [ + 702, + 1031, + 1044 + ] + ], + "pair": [ + 203, + 25, + 564, + 292, + 2 + ], + "support_size": 33 + }, + "710": { + "boundary": 817, + "bounds": [ + [ + 2, + 2, + 2 + ], + [ + 5, + 5, + 5 + ], + [ + 8, + 8, + 8 + ], + [ + 11, + 11, + 11 + ], + [ + 12, + 12, + 12 + ], + [ + 15, + 14, + 14 + ], + [ + 16, + 15, + 15 + ], + [ + 19, + 18, + 18 + ], + [ + 20, + 19, + 19 + ], + [ + 23, + 21, + 21 + ], + [ + 24, + 22, + 22 + ], + [ + 25, + 23, + 23 + ], + [ + 26, + 24, + 24 + ], + [ + 28, + 26, + 26 + ], + [ + 29, + 27, + 27 + ], + [ + 31, + 29, + 29 + ], + [ + 32, + 30, + 30 + ], + [ + 33, + 31, + 31 + ], + [ + 36, + 33, + 33 + ], + [ + 40, + 36, + 36 + ], + [ + 41, + 37, + 37 + ], + [ + 44, + 40, + 40 + ], + [ + 46, + 42, + 42 + ], + [ + 48, + 44, + 44 + ], + [ + 49, + 45, + 45 + ], + [ + 53, + 49, + 49 + ], + [ + 54, + 50, + 50 + ], + [ + 58, + 54, + 54 + ], + [ + 59, + 55, + 55 + ], + [ + 63, + 58, + 58 + ], + [ + 64, + 59, + 59 + ], + [ + 69, + 64, + 64 + ], + [ + 70, + 65, + 65 + ], + [ + 74, + 69, + 69 + ], + [ + 75, + 70, + 70 + ], + [ + 77, + 71, + 71 + ], + [ + 78, + 72, + 72 + ], + [ + 79, + 73, + 73 + ], + [ + 80, + 74, + 74 + ], + [ + 82, + 76, + 76 + ], + [ + 83, + 77, + 77 + ], + [ + 88, + 82, + 82 + ], + [ + 91, + 85, + 85 + ], + [ + 94, + 87, + 87 + ], + [ + 97, + 90, + 90 + ], + [ + 99, + 92, + 92 + ], + [ + 102, + 95, + 95 + ], + [ + 103, + 96, + 96 + ], + [ + 106, + 99, + 99 + ], + [ + 107, + 100, + 100 + ], + [ + 108, + 101, + 101 + ], + [ + 111, + 104, + 104 + ], + [ + 133, + 3, + 3 + ], + [ + 240, + 3, + 3 + ], + [ + 243, + 3, + 3 + ], + [ + 246, + 3, + 3 + ], + [ + 249, + 3, + 3 + ], + [ + 250, + 3, + 3 + ], + [ + 251, + 3, + 3 + ], + [ + 255, + 3, + 3 + ], + [ + 257, + 3, + 3 + ], + [ + 258, + 3, + 3 + ], + [ + 259, + 3, + 3 + ], + [ + 261, + 3, + 3 + ], + [ + 267, + 3, + 3 + ], + [ + 269, + 3, + 3 + ], + [ + 270, + 3, + 3 + ], + [ + 271, + 3, + 3 + ], + [ + 287, + 3, + 3 + ], + [ + 288, + 3, + 3 + ], + [ + 292, + 3, + 3 + ], + [ + 296, + 3, + 3 + ], + [ + 302, + 3, + 3 + ], + [ + 304, + 3, + 3 + ], + [ + 308, + 3, + 3 + ], + [ + 312, + 3, + 3 + ], + [ + 318, + 3, + 3 + ], + [ + 335, + 3, + 3 + ], + [ + 336, + 3, + 3 + ], + [ + 340, + 3, + 3 + ], + [ + 350, + 3, + 3 + ], + [ + 351, + 3, + 3 + ], + [ + 367, + 3, + 3 + ], + [ + 383, + 3, + 3 + ], + [ + 384, + 3, + 3 + ], + [ + 388, + 3, + 3 + ], + [ + 398, + 3, + 3 + ], + [ + 399, + 3, + 3 + ], + [ + 400, + 3, + 3 + ], + [ + 402, + 3, + 3 + ], + [ + 403, + 3, + 3 + ], + [ + 406, + 3, + 3 + ], + [ + 409, + 3, + 3 + ], + [ + 410, + 3, + 3 + ], + [ + 411, + 3, + 3 + ], + [ + 415, + 3, + 3 + ], + [ + 417, + 3, + 3 + ], + [ + 419, + 3, + 3 + ], + [ + 421, + 3, + 3 + ], + [ + 427, + 3, + 3 + ], + [ + 429, + 3, + 3 + ], + [ + 430, + 3, + 3 + ], + [ + 431, + 3, + 3 + ], + [ + 432, + 3, + 3 + ], + [ + 433, + 3, + 3 + ], + [ + 435, + 3, + 3 + ], + [ + 438, + 3, + 3 + ], + [ + 442, + 3, + 3 + ], + [ + 443, + 3, + 3 + ], + [ + 445, + 3, + 3 + ], + [ + 710, + 3, + 597 + ] + ], + "pair": [ + 2, + 710, + 2, + 597, + 35 + ], + "support_size": 110 + }, + "734": { + "boundary": 804, + "bounds": [ + [ + 2, + 2, + 2 + ], + [ + 5, + 5, + 5 + ], + [ + 8, + 8, + 8 + ], + [ + 11, + 11, + 11 + ], + [ + 12, + 12, + 12 + ], + [ + 15, + 14, + 14 + ], + [ + 16, + 15, + 15 + ], + [ + 19, + 18, + 18 + ], + [ + 20, + 19, + 19 + ], + [ + 23, + 21, + 21 + ], + [ + 24, + 22, + 22 + ], + [ + 25, + 23, + 23 + ], + [ + 26, + 24, + 24 + ], + [ + 28, + 26, + 26 + ], + [ + 29, + 27, + 27 + ], + [ + 31, + 29, + 29 + ], + [ + 32, + 30, + 30 + ], + [ + 33, + 31, + 31 + ], + [ + 36, + 33, + 33 + ], + [ + 40, + 36, + 36 + ], + [ + 41, + 37, + 37 + ], + [ + 44, + 40, + 40 + ], + [ + 46, + 42, + 42 + ], + [ + 48, + 44, + 44 + ], + [ + 49, + 45, + 45 + ], + [ + 53, + 49, + 49 + ], + [ + 54, + 50, + 50 + ], + [ + 58, + 54, + 54 + ], + [ + 59, + 55, + 55 + ], + [ + 63, + 58, + 58 + ], + [ + 64, + 59, + 59 + ], + [ + 69, + 64, + 64 + ], + [ + 70, + 65, + 65 + ], + [ + 74, + 69, + 69 + ], + [ + 75, + 70, + 70 + ], + [ + 77, + 71, + 71 + ], + [ + 78, + 72, + 72 + ], + [ + 79, + 73, + 73 + ], + [ + 80, + 74, + 74 + ], + [ + 82, + 76, + 76 + ], + [ + 83, + 77, + 77 + ], + [ + 88, + 82, + 82 + ], + [ + 91, + 85, + 85 + ], + [ + 94, + 87, + 87 + ], + [ + 97, + 90, + 90 + ], + [ + 99, + 92, + 92 + ], + [ + 102, + 95, + 95 + ], + [ + 103, + 96, + 96 + ], + [ + 106, + 99, + 99 + ], + [ + 107, + 100, + 100 + ], + [ + 108, + 101, + 101 + ], + [ + 111, + 104, + 104 + ], + [ + 133, + 3, + 3 + ], + [ + 240, + 3, + 3 + ], + [ + 243, + 3, + 3 + ], + [ + 246, + 3, + 3 + ], + [ + 249, + 3, + 3 + ], + [ + 250, + 3, + 3 + ], + [ + 251, + 3, + 3 + ], + [ + 255, + 3, + 3 + ], + [ + 257, + 3, + 3 + ], + [ + 258, + 3, + 3 + ], + [ + 259, + 3, + 3 + ], + [ + 261, + 3, + 3 + ], + [ + 267, + 3, + 3 + ], + [ + 269, + 3, + 3 + ], + [ + 270, + 3, + 3 + ], + [ + 271, + 3, + 3 + ], + [ + 287, + 3, + 3 + ], + [ + 288, + 3, + 3 + ], + [ + 292, + 3, + 3 + ], + [ + 296, + 3, + 3 + ], + [ + 302, + 3, + 3 + ], + [ + 304, + 3, + 3 + ], + [ + 308, + 3, + 3 + ], + [ + 312, + 3, + 3 + ], + [ + 318, + 3, + 3 + ], + [ + 335, + 3, + 3 + ], + [ + 336, + 3, + 3 + ], + [ + 340, + 3, + 3 + ], + [ + 350, + 3, + 3 + ], + [ + 351, + 3, + 3 + ], + [ + 367, + 3, + 3 + ], + [ + 383, + 3, + 3 + ], + [ + 384, + 3, + 3 + ], + [ + 388, + 3, + 3 + ], + [ + 398, + 3, + 3 + ], + [ + 399, + 3, + 3 + ], + [ + 400, + 3, + 3 + ], + [ + 402, + 3, + 3 + ], + [ + 403, + 3, + 3 + ], + [ + 406, + 3, + 3 + ], + [ + 409, + 3, + 3 + ], + [ + 410, + 3, + 3 + ], + [ + 411, + 3, + 3 + ], + [ + 415, + 3, + 3 + ], + [ + 417, + 3, + 3 + ], + [ + 419, + 3, + 3 + ], + [ + 421, + 3, + 3 + ], + [ + 427, + 3, + 3 + ], + [ + 429, + 3, + 3 + ], + [ + 430, + 3, + 3 + ], + [ + 431, + 3, + 3 + ], + [ + 432, + 3, + 3 + ], + [ + 433, + 3, + 3 + ], + [ + 435, + 3, + 3 + ], + [ + 438, + 3, + 3 + ], + [ + 442, + 3, + 3 + ], + [ + 443, + 3, + 3 + ], + [ + 445, + 3, + 3 + ], + [ + 734, + 3, + 597 + ] + ], + "pair": [ + 2, + 734, + 2, + 597, + 35 + ], + "support_size": 110 + } + }, + "public148_paid_histogram_both_alternatives": { + "1": 1, + "2": 1 + }, + "public_replacement_boundaries": { + "148": 785, + "159": 2212, + "203": 782, + "710": 12707, + "734": 13202 + }, + "status": "PASS_OWNED738_DELIVERY_OBSTRUCTION", + "witnesses_sha256": "1b311a567e6e4f8225b702828ad8d224d9054eb697338a8d9ba71fee8f7cfe55" + }, + "producer_controls": { + "individual_floors_not_additive": true, + "rejected_corruptions": [ + "entry_support_outside_producer_frame", + "wrong_producer_value", + "unaccounted_descent_in_public_prefix", + "changed_owned_payload_before_delivery" + ], + "widened_delivery_loss_floor": 6, + "widened_delivery_rank": 2 + }, + "producers": { + "first_owned_init": 13377, + "new_bound": false, + "results": [ + { + "clear_frame": 593, + "copy_event": 13378, + "copy_frame": 559, + "delivery_factor": "1/2", + "independent_witnesses": [ + { + "coefficient": "1/2", + "initial_vector": 19, + "input": 1 + }, + { + "coefficient": "1/2", + "initial_vector": 131, + "input": 4 + }, + { + "coefficient": "1/2", + "initial_vector": 259, + "input": 5 + }, + { + "coefficient": "-1/2", + "initial_vector": 21, + "input": 7 + }, + { + "coefficient": "-1/2", + "initial_vector": 41, + "input": 12 + }, + { + "coefficient": "-1/2", + "initial_vector": 73, + "input": 13 + }, + { + "coefficient": "-1/2", + "initial_vector": 145, + "input": 18 + }, + { + "coefficient": "1/2", + "initial_vector": 22, + "input": 26 + } + ], + "initial_covector": { + "1": "1/2", + "10": "-1/2", + "101": "-1/2", + "102": "-1/2", + "103": "-1/2", + "104": "1/2", + "108": "-1/2", + "109": "-1/2", + "11": "-1/2", + "110": "1/2", + "111": "1/2", + "12": "-1/2", + "13": "-1/2", + "173": "1", + "18": "-1/2", + "19": "-1/2", + "224": "1/2", + "225": "-1/2", + "226": "1/2", + "227": "-1/2", + "233": "-1/2", + "235": "-1/2", + "237": "-1/2", + "239": "-1/2", + "24": "-1/2", + "241": "-1/2", + "243": "-1/2", + "249": "-1/2", + "251": "-1/2", + "253": "-1/2", + "255": "-1/2", + "256": "-1/2", + "257": "-1/2", + "259": "-1", + "26": "1/2", + "262": "1/2", + "265": "-1", + "266": "-1/2", + "269": "-1/2", + "276": "-1/2", + "283": "-1/2", + "286": "-1/2", + "287": "1", + "29": "1/2", + "292": "-1/2", + "299": "-1/2", + "30": "1/2", + "302": "-1/2", + "303": "1", + "308": "-1/2", + "315": "-1/2", + "318": "-1/2", + "319": "1", + "32": "-1/2", + "324": "-1/2", + "331": "-1/2", + "334": "-1/2", + "335": "1", + "336": "1/2", + "347": "1/2", + "351": "1/2", + "352": "1/2", + "36": "-1/2", + "363": "1/2", + "367": "1/2", + "368": "1/2", + "37": "-1/2", + "379": "1/2", + "38": "-1/2", + "383": "1/2", + "384": "1/2", + "395": "1/2", + "399": "1/2", + "4": "1/2", + "416": "-1/2", + "418": "1/2", + "419": "-1/2", + "422": "1/2", + "425": "-1/2", + "426": "-1/2", + "427": "1/2", + "43": "-1/2", + "431": "1/2", + "432": "-1/2", + "434": "1/2", + "435": "-1/2", + "438": "1/2", + "441": "-1/2", + "442": "-1/2", + "443": "1/2", + "447": "1/2", + "45": "-1/2", + "49": "-1/2", + "5": "1/2", + "50": "-1/2", + "51": "1/2", + "56": "-1/2", + "57": "-1/2", + "58": "1/2", + "62": "-1/2", + "63": "-1/2", + "64": "1/2", + "65": "1/2", + "67": "1/2", + "7": "-1/2", + "72": "-1/2", + "73": "1/2", + "74": "1/2", + "79": "-1/2", + "81": "-1/2", + "82": "1/2", + "86": "1/2", + "88": "1/2", + "89": "1/2", + "92": "-1/2", + "94": "-1/2", + "95": "1/2", + "98": "-1/2" + }, + "initial_span_rank": 8, + "nonzero_chart_inputs": 52, + "owned": 735, + "owned_move_ranks": [ + 7 + ], + "required_global_owned_descent_rank_mass": 7, + "source_role": 173, + "support_count": 118 + }, + { + "clear_frame": 594, + "copy_event": 13389, + "copy_frame": 543, + "delivery_factor": "1/2", + "independent_witnesses": [ + { + "coefficient": "-1/2", + "initial_vector": 35, + "input": 2 + }, + { + "coefficient": "-1/2", + "initial_vector": 131, + "input": 4 + }, + { + "coefficient": "1/2", + "initial_vector": 13, + "input": 6 + }, + { + "coefficient": "-1/2", + "initial_vector": 21, + "input": 7 + }, + { + "coefficient": "-1/2", + "initial_vector": 69, + "input": 9 + }, + { + "coefficient": "-1/2", + "initial_vector": 261, + "input": 11 + }, + { + "coefficient": "1/2", + "initial_vector": 73, + "input": 13 + }, + { + "coefficient": "-1/2", + "initial_vector": 38, + "input": 27 + } + ], + "initial_covector": { + "101": "1/2", + "103": "-1/2", + "105": "1/2", + "107": "-1/2", + "109": "-1/2", + "11": "-1/2", + "110": "-1/2", + "13": "1/2", + "15": "1/2", + "151": "1", + "17": "-1/2", + "19": "-1/2", + "2": "-1/2", + "20": "-1/2", + "224": "1/2", + "225": "-1/2", + "229": "-1/2", + "23": "-1/2", + "230": "-1/2", + "234": "1/2", + "235": "-1/2", + "237": "-1/2", + "238": "-1/2", + "242": "-1/2", + "243": "-1/2", + "246": "-1/2", + "250": "1/2", + "251": "-1", + "255": "-1/2", + "258": "-1/2", + "259": "-1/2", + "262": "-1/2", + "266": "1/2", + "267": "-1", + "27": "-1/2", + "271": "-1/2", + "283": "-1", + "29": "-1/2", + "299": "-1", + "303": "-1", + "304": "-1/2", + "312": "1/2", + "315": "-1/2", + "324": "-1/2", + "33": "-1/2", + "331": "-1/2", + "334": "-1/2", + "340": "1/2", + "347": "-1/2", + "35": "-1/2", + "350": "1/2", + "351": "-1", + "352": "1/2", + "36": "1/2", + "363": "-1/2", + "367": "-1/2", + "38": "-1/2", + "399": "-1", + "4": "-1/2", + "40": "-1/2", + "400": "1/2", + "401": "1/2", + "402": "-1/2", + "403": "1/2", + "405": "1/2", + "409": "1/2", + "41": "1/2", + "413": "1/2", + "414": "1/2", + "415": "-1/2", + "416": "1/2", + "417": "1/2", + "418": "-1/2", + "419": "1/2", + "421": "1/2", + "425": "1/2", + "429": "1/2", + "43": "1/2", + "430": "1/2", + "431": "-1/2", + "432": "1/2", + "437": "1/2", + "44": "1/2", + "443": "-1/2", + "446": "1/2", + "447": "-1", + "47": "1/2", + "48": "-1/2", + "50": "-1/2", + "52": "1/2", + "55": "-1/2", + "58": "-1/2", + "6": "1/2", + "60": "-1/2", + "62": "-1/2", + "65": "-1/2", + "68": "1/2", + "7": "-1/2", + "71": "-1/2", + "73": "1/2", + "75": "1/2", + "77": "-1/2", + "81": "-1/2", + "83": "1/2", + "85": "-1/2", + "86": "-1/2", + "87": "-1/2", + "89": "-1/2", + "9": "-1/2", + "91": "-1/2", + "94": "-1/2", + "96": "1/2", + "99": "1/2" + }, + "initial_span_rank": 8, + "nonzero_chart_inputs": 52, + "owned": 736, + "owned_move_ranks": [ + 7 + ], + "required_global_owned_descent_rank_mass": 7, + "source_role": 151, + "support_count": 113 + }, + { + "clear_frame": 595, + "copy_event": 13400, + "copy_frame": 531, + "delivery_factor": "-1/2", + "independent_witnesses": [ + { + "coefficient": "-1/2", + "initial_vector": 11, + "input": 0 + }, + { + "coefficient": "-1/2", + "initial_vector": 259, + "input": 5 + }, + { + "coefficient": "-1/2", + "initial_vector": 21, + "input": 7 + }, + { + "coefficient": "1/2", + "initial_vector": 37, + "input": 8 + }, + { + "coefficient": "-1/2", + "initial_vector": 69, + "input": 9 + }, + { + "coefficient": "-1/2", + "initial_vector": 133, + "input": 10 + }, + { + "coefficient": "-1/2", + "initial_vector": 265, + "input": 15 + }, + { + "coefficient": "-1/2", + "initial_vector": 14, + "input": 25 + } + ], + "initial_covector": { + "0": "-1/2", + "10": "-1/2", + "100": "-1/2", + "101": "-1/2", + "106": "1/2", + "109": "1/2", + "111": "-1/2", + "146": "1", + "15": "-1/2", + "16": "1/2", + "17": "-1/2", + "18": "-1/2", + "20": "1/2", + "22": "-1/2", + "225": "-1/2", + "226": "1/2", + "227": "-1/2", + "229": "-1/2", + "233": "-1/2", + "237": "-1/2", + "238": "-1/2", + "239": "1/2", + "240": "-1/2", + "241": "-1/2", + "243": "-1/2", + "245": "-1/2", + "249": "-1/2", + "25": "-1/2", + "253": "-1/2", + "254": "-1/2", + "255": "1/2", + "257": "-1/2", + "261": "-1/2", + "262": "-1/2", + "266": "1/2", + "267": "-1/2", + "269": "-1/2", + "270": "-1/2", + "272": "-1/2", + "280": "1/2", + "283": "-1/2", + "288": "-1/2", + "296": "1/2", + "299": "-1/2", + "30": "-1/2", + "303": "1", + "304": "-1/2", + "308": "-1/2", + "31": "-1/2", + "312": "1/2", + "318": "-1/2", + "319": "1", + "32": "-1/2", + "320": "-1", + "33": "-1/2", + "352": "-1/2", + "356": "1/2", + "366": "1/2", + "367": "-1/2", + "368": "-1/2", + "37": "1/2", + "379": "1/2", + "383": "-1/2", + "384": "-1/2", + "395": "1/2", + "399": "1/2", + "40": "-1/2", + "400": "-1/2", + "405": "-1/2", + "411": "1/2", + "414": "-1/2", + "415": "1", + "418": "-1/2", + "419": "1/2", + "42": "1/2", + "421": "-1/2", + "422": "-1/2", + "425": "1/2", + "426": "1/2", + "43": "1/2", + "430": "-1/2", + "431": "1/2", + "434": "-1/2", + "435": "1/2", + "437": "-1/2", + "438": "-1/2", + "441": "1/2", + "442": "1/2", + "446": "-1/2", + "447": "1/2", + "47": "-1/2", + "48": "-1/2", + "49": "-1/2", + "5": "-1/2", + "51": "-1/2", + "52": "-1/2", + "54": "-1/2", + "60": "1/2", + "63": "-1/2", + "65": "1/2", + "66": "1/2", + "67": "-1/2", + "68": "-1/2", + "7": "-1/2", + "70": "-1/2", + "73": "-1/2", + "77": "-1/2", + "79": "-1/2", + "8": "1/2", + "84": "1/2", + "85": "-1/2", + "87": "-1/2", + "88": "-1/2", + "89": "-1/2", + "9": "-1/2", + "90": "-1/2", + "92": "-1/2", + "97": "1/2", + "98": "-1/2", + "99": "-1/2" + }, + "initial_span_rank": 8, + "nonzero_chart_inputs": 52, + "owned": 737, + "owned_move_ranks": [ + 7 + ], + "required_global_owned_descent_rank_mass": 7, + "source_role": 146, + "support_count": 120 + }, + { + "clear_frame": 597, + "copy_event": 13409, + "copy_frame": 591, + "delivery_factor": "-1/2", + "independent_witnesses": [ + { + "coefficient": "-1/2", + "initial_vector": 35, + "input": 2 + }, + { + "coefficient": "-1/2", + "initial_vector": 259, + "input": 5 + }, + { + "coefficient": "-1/2", + "initial_vector": 37, + "input": 8 + }, + { + "coefficient": "-1/2", + "initial_vector": 41, + "input": 12 + }, + { + "coefficient": "-1/2", + "initial_vector": 49, + "input": 16 + }, + { + "coefficient": "-1/2", + "initial_vector": 161, + "input": 20 + }, + { + "coefficient": "1/2", + "initial_vector": 321, + "input": 23 + }, + { + "coefficient": "1/2", + "initial_vector": 14, + "input": 25 + } + ], + "initial_covector": { + "102": "1/2", + "103": "-1/2", + "106": "1/2", + "107": "-1/2", + "108": "-1/2", + "11": "1/2", + "111": "-1/2", + "12": "-1/2", + "133": "1", + "15": "-1/2", + "16": "-1/2", + "19": "1/2", + "2": "-1/2", + "20": "-1/2", + "23": "1/2", + "24": "1/2", + "240": "-1/2", + "243": "-1/2", + "246": "1/2", + "249": "-1/2", + "25": "1/2", + "250": "-1/2", + "251": "1/2", + "255": "1/2", + "257": "1/2", + "258": "-1/2", + "259": "-1/2", + "26": "1/2", + "261": "1/2", + "267": "-1/2", + "269": "1/2", + "270": "1/2", + "271": "-1/2", + "28": "1/2", + "287": "1", + "288": "-1/2", + "29": "1/2", + "292": "1/2", + "296": "1/2", + "302": "1/2", + "304": "-1/2", + "308": "1/2", + "31": "1/2", + "312": "1/2", + "318": "1/2", + "32": "1/2", + "33": "1/2", + "335": "1", + "336": "-1/2", + "340": "1/2", + "350": "1/2", + "351": "-1/2", + "36": "-1/2", + "367": "1", + "383": "1", + "384": "-1/2", + "388": "1/2", + "398": "1/2", + "399": "-1/2", + "40": "-1/2", + "400": "-1/2", + "402": "1/2", + "403": "-1/2", + "406": "1/2", + "409": "-1/2", + "41": "-1/2", + "410": "-1/2", + "411": "1/2", + "415": "1/2", + "417": "1/2", + "419": "-1/2", + "421": "1/2", + "427": "-1/2", + "429": "1/2", + "430": "1/2", + "431": "-1/2", + "432": "-1", + "433": "1/2", + "435": "-1", + "438": "-1/2", + "44": "1/2", + "442": "1/2", + "443": "-1", + "445": "1/2", + "46": "1/2", + "48": "-1/2", + "49": "-1/2", + "5": "-1/2", + "53": "1/2", + "54": "-1/2", + "58": "-1/2", + "59": "-1/2", + "63": "-1/2", + "64": "-1/2", + "69": "1/2", + "70": "-1/2", + "74": "1/2", + "75": "1/2", + "77": "1/2", + "78": "-1/2", + "79": "1/2", + "8": "-1/2", + "80": "-1/2", + "82": "-1/2", + "83": "-1/2", + "88": "1/2", + "91": "1/2", + "94": "-1/2", + "97": "1/2", + "99": "1/2" + }, + "initial_span_rank": 8, + "nonzero_chart_inputs": 52, + "owned": 738, + "owned_move_ranks": [ + 1, + 1, + 3, + 2 + ], + "required_global_owned_descent_rank_mass": 7, + "source_role": 133, + "support_count": 110 + }, + { + "clear_frame": 598, + "copy_event": 13425, + "copy_frame": 518, + "delivery_factor": "1/4", + "independent_witnesses": [ + { + "coefficient": "-1", + "initial_vector": 19, + "input": 1 + }, + { + "coefficient": "-1", + "initial_vector": 35, + "input": 2 + }, + { + "coefficient": "-1", + "initial_vector": 131, + "input": 4 + }, + { + "coefficient": "-1", + "initial_vector": 259, + "input": 5 + }, + { + "coefficient": "1", + "initial_vector": 13, + "input": 6 + }, + { + "coefficient": "-1", + "initial_vector": 69, + "input": 9 + }, + { + "coefficient": "1", + "initial_vector": 73, + "input": 13 + }, + { + "coefficient": "1", + "initial_vector": 14, + "input": 25 + } + ], + "initial_covector": { + "1": "-1", + "101": "1", + "102": "1", + "104": "-1", + "107": "-1", + "110": "-1", + "111": "-1", + "13": "1", + "16": "-1", + "18": "1", + "19": "1", + "2": "-1", + "20": "-1", + "21": "-1", + "24": "1", + "25": "1", + "256": "1", + "257": "1", + "258": "-1", + "261": "1", + "262": "-1", + "265": "1", + "266": "1", + "267": "-2", + "269": "1", + "270": "1", + "271": "-2", + "28": "1", + "288": "-1", + "292": "1", + "296": "1", + "302": "1", + "303": "-2", + "304": "-1", + "308": "1", + "312": "1", + "318": "1", + "319": "-2", + "32": "1", + "336": "-1", + "340": "1", + "35": "-1", + "350": "1", + "351": "-3", + "36": "1", + "37": "1", + "384": "-1", + "388": "1", + "39": "-1", + "398": "1", + "399": "-3", + "4": "-1", + "40": "-1", + "416": "1", + "417": "1", + "418": "-1", + "421": "1", + "422": "-1", + "425": "1", + "426": "1", + "427": "-2", + "429": "1", + "43": "1", + "430": "1", + "431": "-2", + "433": "1", + "434": "-1", + "437": "1", + "438": "-1", + "44": "1", + "441": "1", + "442": "1", + "443": "-2", + "445": "1", + "446": "1", + "447": "-2", + "45": "1", + "46": "1", + "47": "1", + "48": "-1", + "5": "-1", + "51": "-1", + "54": "-1", + "55": "-1", + "58": "-1", + "6": "1", + "61": "1", + "64": "-1", + "65": "-1", + "68": "1", + "69": "1", + "72": "1", + "75": "1", + "78": "-1", + "79": "1", + "82": "-1", + "85": "-1", + "86": "-1", + "89": "-1", + "9": "-1", + "93": "1", + "94": "-1", + "96": "1", + "97": "1", + "98": "1", + "99": "1" + }, + "initial_span_rank": 8, + "nonzero_chart_inputs": 52, + "owned": 739, + "owned_move_ranks": [ + 7 + ], + "required_global_owned_descent_rank_mass": 7, + "source_role": 256, + "support_count": 106 + }, + { + "clear_frame": 599, + "copy_event": 13440, + "copy_frame": 267, + "delivery_factor": "1/4", + "independent_witnesses": [ + { + "coefficient": "1", + "initial_vector": 11, + "input": 0 + }, + { + "coefficient": "1", + "initial_vector": 35, + "input": 2 + }, + { + "coefficient": "1", + "initial_vector": 21, + "input": 7 + }, + { + "coefficient": "1", + "initial_vector": 69, + "input": 9 + }, + { + "coefficient": "1", + "initial_vector": 133, + "input": 10 + }, + { + "coefficient": "1", + "initial_vector": 261, + "input": 11 + }, + { + "coefficient": "1", + "initial_vector": 41, + "input": 12 + }, + { + "coefficient": "1", + "initial_vector": 14, + "input": 25 + } + ], + "initial_covector": { + "0": "1", + "10": "1", + "100": "1", + "101": "1", + "102": "1", + "103": "1", + "107": "1", + "108": "1", + "109": "1", + "11": "1", + "12": "1", + "17": "1", + "18": "1", + "19": "1", + "2": "1", + "22": "1", + "225": "1", + "226": "-1", + "227": "2", + "229": "1", + "23": "1", + "230": "1", + "233": "1", + "234": "-1", + "235": "2", + "237": "1", + "238": "1", + "24": "1", + "240": "1", + "241": "1", + "242": "1", + "243": "2", + "245": "1", + "246": "1", + "249": "1", + "25": "1", + "250": "-1", + "251": "2", + "253": "1", + "254": "1", + "256": "1", + "257": "1", + "258": "1", + "259": "2", + "261": "1", + "262": "1", + "265": "1", + "266": "-1", + "267": "2", + "269": "1", + "27": "1", + "270": "1", + "272": "1", + "276": "1", + "280": "-1", + "283": "2", + "286": "1", + "287": "-2", + "288": "1", + "292": "1", + "296": "-1", + "299": "2", + "302": "1", + "303": "-2", + "304": "1", + "308": "1", + "31": "1", + "312": "-1", + "315": "2", + "318": "1", + "319": "-2", + "32": "1", + "320": "1", + "324": "1", + "33": "1", + "331": "2", + "334": "1", + "335": "-1", + "34": "1", + "35": "1", + "38": "1", + "39": "1", + "40": "1", + "45": "1", + "48": "1", + "49": "1", + "50": "1", + "54": "1", + "55": "1", + "56": "1", + "57": "1", + "61": "1", + "62": "1", + "63": "1", + "7": "1", + "70": "1", + "71": "1", + "72": "1", + "76": "1", + "77": "1", + "79": "1", + "81": "1", + "85": "1", + "87": "1", + "89": "1", + "9": "1", + "90": "1", + "91": "1", + "92": "1", + "94": "1", + "98": "1" + }, + "initial_span_rank": 8, + "nonzero_chart_inputs": 52, + "owned": 740, + "owned_move_ranks": [ + 7 + ], + "required_global_owned_descent_rank_mass": 7, + "source_role": 92, + "support_count": 111 + }, + { + "clear_frame": 600, + "copy_event": 13455, + "copy_frame": 517, + "delivery_factor": "1/4", + "independent_witnesses": [ + { + "coefficient": "1", + "initial_vector": 35, + "input": 2 + }, + { + "coefficient": "1", + "initial_vector": 37, + "input": 8 + }, + { + "coefficient": "-1", + "initial_vector": 69, + "input": 9 + }, + { + "coefficient": "1", + "initial_vector": 41, + "input": 12 + }, + { + "coefficient": "1", + "initial_vector": 49, + "input": 16 + }, + { + "coefficient": "1", + "initial_vector": 161, + "input": 20 + }, + { + "coefficient": "-1", + "initial_vector": 321, + "input": 23 + }, + { + "coefficient": "-1", + "initial_vector": 14, + "input": 25 + } + ], + "initial_covector": { + "100": "-1", + "103": "1", + "104": "-1", + "108": "1", + "109": "1", + "110": "-1", + "111": "-1", + "12": "1", + "13": "1", + "16": "1", + "17": "-1", + "2": "1", + "20": "1", + "21": "1", + "22": "-1", + "23": "-1", + "25": "-1", + "256": "1", + "257": "-1", + "258": "1", + "259": "2", + "26": "-1", + "261": "-1", + "262": "-1", + "265": "1", + "266": "1", + "269": "-1", + "270": "-1", + "272": "-1", + "276": "1", + "280": "1", + "286": "1", + "287": "-2", + "29": "-1", + "3": "1", + "30": "-1", + "31": "-1", + "320": "-1", + "324": "1", + "33": "-1", + "334": "1", + "335": "-3", + "34": "-1", + "352": "-1", + "356": "1", + "36": "1", + "366": "1", + "367": "-3", + "368": "-1", + "37": "1", + "372": "1", + "38": "1", + "382": "1", + "383": "-3", + "416": "1", + "417": "-1", + "418": "-1", + "419": "2", + "421": "-1", + "422": "-1", + "425": "1", + "426": "1", + "429": "-1", + "43": "1", + "430": "-1", + "432": "2", + "433": "-1", + "434": "-1", + "435": "2", + "437": "-1", + "438": "-1", + "44": "-1", + "441": "1", + "442": "1", + "445": "-1", + "446": "-1", + "46": "-1", + "47": "-1", + "49": "1", + "50": "1", + "51": "-1", + "56": "1", + "59": "1", + "60": "1", + "61": "1", + "66": "1", + "67": "-1", + "72": "1", + "73": "-1", + "74": "-1", + "77": "-1", + "78": "1", + "79": "-1", + "8": "1", + "80": "1", + "83": "1", + "84": "1", + "88": "-1", + "89": "-1", + "9": "-1", + "94": "1", + "95": "-1", + "99": "-1" + }, + "initial_span_rank": 8, + "nonzero_chart_inputs": 52, + "owned": 741, + "owned_move_ranks": [ + 7 + ], + "required_global_owned_descent_rank_mass": 7, + "source_role": 9, + "support_count": 103 + }, + { + "clear_frame": 601, + "copy_event": 13470, + "copy_frame": 477, + "delivery_factor": "-1/4", + "independent_witnesses": [ + { + "coefficient": "-1", + "initial_vector": 131, + "input": 4 + }, + { + "coefficient": "1", + "initial_vector": 259, + "input": 5 + }, + { + "coefficient": "1", + "initial_vector": 133, + "input": 10 + }, + { + "coefficient": "1", + "initial_vector": 265, + "input": 15 + }, + { + "coefficient": "1", + "initial_vector": 145, + "input": 18 + }, + { + "coefficient": "-1", + "initial_vector": 161, + "input": 20 + }, + { + "coefficient": "1", + "initial_vector": 193, + "input": 22 + }, + { + "coefficient": "-1", + "initial_vector": 134, + "input": 29 + } + ], + "initial_covector": { + "10": "1", + "101": "1", + "102": "-1", + "105": "1", + "106": "-1", + "108": "1", + "109": "-1", + "11": "-1", + "110": "-1", + "111": "1", + "14": "-1", + "15": "1", + "18": "1", + "19": "-1", + "20": "-1", + "21": "1", + "22": "1", + "23": "-1", + "240": "1", + "241": "1", + "242": "-1", + "245": "1", + "246": "-1", + "249": "1", + "250": "1", + "251": "-2", + "253": "1", + "254": "1", + "255": "-2", + "288": "1", + "29": "-1", + "292": "-1", + "296": "-1", + "30": "1", + "302": "-1", + "303": "-2", + "320": "1", + "324": "-1", + "33": "-1", + "334": "-1", + "335": "-1", + "34": "1", + "352": "1", + "356": "-1", + "36": "1", + "366": "-1", + "367": "-1", + "37": "-1", + "384": "1", + "388": "-1", + "39": "-1", + "398": "-1", + "399": "-1", + "4": "-1", + "40": "1", + "400": "1", + "401": "1", + "402": "-1", + "405": "1", + "406": "-1", + "409": "1", + "41": "1", + "410": "1", + "411": "-2", + "413": "1", + "414": "1", + "415": "-2", + "42": "-1", + "432": "2", + "433": "-1", + "434": "1", + "437": "1", + "438": "1", + "441": "-1", + "442": "-1", + "445": "-1", + "446": "1", + "447": "-2", + "46": "-1", + "47": "1", + "49": "1", + "5": "1", + "50": "-1", + "52": "1", + "53": "-1", + "54": "1", + "55": "-1", + "59": "1", + "60": "-1", + "62": "-1", + "63": "1", + "64": "1", + "65": "-1", + "68": "1", + "69": "-1", + "70": "1", + "71": "-1", + "73": "1", + "74": "-1", + "83": "1", + "84": "-1", + "90": "1", + "91": "-1", + "96": "1", + "97": "-1" + }, + "initial_span_rank": 8, + "nonzero_chart_inputs": 52, + "owned": 742, + "owned_move_ranks": [ + 7 + ], + "required_global_owned_descent_rank_mass": 7, + "source_role": 240, + "support_count": 105 + } + ], + "scope": "One unchanged scalar target at its retained delivery frame; owned descent cost can be shared across targets, so individual bounds must not be summed.", + "status": "PASS_RANK_EIGHT_PRODUCER_AND_LOSS_SPACE_BINDING" + }, + "status": "PASS_P104_OWNED_CLEANUP_OBSTRUCTIONS", + "windows": { + "all_source_endpoint_rows": 743, + "corruption_controls": { + "changed_source_bytes": true, + "owned_role_used_as_public_witness": true, + "reversed_public_window": true, + "zero_separating_vector": true + }, + "distinct_full_holder_geometries": 2832, + "distinct_public_holder_geometries": 2340, + "event_boundaries_with_helper_owned_pairs": 5252, + "new_bound": false, + "owned_holder_pairs_by_register": { + "735": 594, + "736": 549, + "737": 476, + "738": 812, + "739": 702, + "740": 767, + "741": 663, + "742": 689 + }, + "positive_control": { + "boundary": 15443, + "common_dimension": 8, + "common_frame": 559, + "helper": 706, + "partner": 173, + "source": "PR5561 headline word" + }, + "public_only_witnesses": true, + "source_role_173": "productive helper; port61 is not live", + "status": "PASS_PUBLIC_WINDOW_OBSTRUCTION", + "witness_examples": [ + { + "boundary": 13378, + "helper": 173, + "public_bounds": [ + [ + 112, + 3, + 593 + ], + [ + 115, + 3, + 430 + ], + [ + 117, + 3, + 439 + ], + [ + 118, + 3, + 3 + ], + [ + 120, + 3, + 430 + ], + [ + 121, + 549, + 549 + ], + [ + 142, + 3, + 411 + ], + [ + 169, + 553, + 553 + ], + [ + 170, + 3, + 3 + ], + [ + 171, + 3, + 412 + ], + [ + 173, + 559, + 559 + ], + [ + 174, + 3, + 593 + ], + [ + 176, + 3, + 449 + ], + [ + 179, + 3, + 421 + ], + [ + 180, + 3, + 3 + ], + [ + 182, + 3, + 593 + ], + [ + 184, + 3, + 593 + ], + [ + 185, + 3, + 401 + ], + [ + 188, + 3, + 249 + ], + [ + 192, + 3, + 3 + ], + [ + 194, + 3, + 383 + ], + [ + 195, + 3, + 3 + ], + [ + 198, + 3, + 597 + ], + [ + 199, + 3, + 258 + ], + [ + 205, + 3, + 3 + ], + [ + 206, + 278, + 1047 + ], + [ + 207, + 3, + 3 + ], + [ + 208, + 3, + 450 + ] + ], + "witness": [ + 121, + 112, + 549, + 593, + 2 + ] + }, + { + "boundary": 13378, + "helper": 224, + "public_bounds": [ + [ + 57, + 127, + 127 + ], + [ + 81, + 127, + 127 + ], + [ + 112, + 3, + 593 + ], + [ + 118, + 3, + 3 + ], + [ + 119, + 3, + 594 + ], + [ + 120, + 3, + 430 + ], + [ + 121, + 549, + 549 + ], + [ + 125, + 3, + 594 + ], + [ + 127, + 3, + 602 + ], + [ + 128, + 3, + 594 + ], + [ + 129, + 317, + 1055 + ], + [ + 130, + 541, + 144 + ], + [ + 139, + 3, + 594 + ], + [ + 151, + 543, + 543 + ], + [ + 152, + 3, + 17 + ], + [ + 154, + 3, + 602 + ], + [ + 169, + 553, + 553 + ], + [ + 173, + 559, + 559 + ], + [ + 174, + 3, + 593 + ], + [ + 176, + 3, + 449 + ], + [ + 182, + 3, + 593 + ], + [ + 184, + 3, + 593 + ], + [ + 185, + 3, + 401 + ], + [ + 194, + 3, + 383 + ], + [ + 195, + 3, + 3 + ], + [ + 206, + 278, + 1047 + ], + [ + 207, + 3, + 3 + ], + [ + 208, + 3, + 450 + ], + [ + 215, + 318, + 901 + ], + [ + 224, + 127, + 127 + ], + [ + 225, + 267, + 127 + ], + [ + 226, + 260, + 260 + ], + [ + 227, + 267, + 127 + ], + [ + 234, + 267, + 127 + ], + [ + 238, + 266, + 266 + ] + ], + "witness": [ + 57, + 112, + 127, + 593, + 1 + ] + }, + { + "boundary": 13378, + "helper": 225, + "public_bounds": [ + [ + 7, + 264, + 264 + ], + [ + 57, + 127, + 127 + ], + [ + 81, + 127, + 127 + ], + [ + 92, + 267, + 267 + ], + [ + 118, + 3, + 3 + ], + [ + 119, + 3, + 594 + ], + [ + 120, + 3, + 430 + ], + [ + 121, + 549, + 549 + ], + [ + 128, + 3, + 594 + ], + [ + 129, + 317, + 1055 + ], + [ + 130, + 541, + 144 + ], + [ + 146, + 531, + 531 + ], + [ + 151, + 543, + 543 + ], + [ + 152, + 3, + 17 + ], + [ + 154, + 3, + 602 + ], + [ + 162, + 529, + 529 + ], + [ + 169, + 553, + 553 + ], + [ + 173, + 559, + 559 + ], + [ + 174, + 3, + 593 + ], + [ + 176, + 3, + 449 + ], + [ + 185, + 3, + 401 + ], + [ + 194, + 3, + 383 + ], + [ + 195, + 3, + 3 + ], + [ + 206, + 278, + 1047 + ], + [ + 207, + 3, + 3 + ], + [ + 208, + 3, + 450 + ], + [ + 215, + 318, + 901 + ], + [ + 224, + 127, + 127 + ], + [ + 225, + 267, + 127 + ], + [ + 228, + 529, + 127 + ], + [ + 234, + 267, + 127 + ], + [ + 451, + 262, + 737 + ], + [ + 497, + 520, + 520 + ] + ], + "witness": [ + 7, + 118, + 264, + 3, + 11 + ] + }, + { + "boundary": 13378, + "helper": 226, + "public_bounds": [ + [ + 57, + 127, + 127 + ], + [ + 81, + 127, + 127 + ], + [ + 92, + 267, + 267 + ], + [ + 121, + 549, + 549 + ], + [ + 124, + 3, + 3 + ], + [ + 125, + 3, + 594 + ], + [ + 127, + 3, + 602 + ], + [ + 139, + 3, + 594 + ], + [ + 142, + 3, + 411 + ], + [ + 146, + 531, + 531 + ], + [ + 160, + 345, + 1059 + ], + [ + 161, + 3, + 46 + ], + [ + 162, + 529, + 529 + ], + [ + 166, + 3, + 327 + ], + [ + 169, + 553, + 553 + ], + [ + 170, + 3, + 3 + ], + [ + 171, + 3, + 412 + ], + [ + 173, + 559, + 559 + ], + [ + 174, + 3, + 593 + ], + [ + 205, + 3, + 3 + ], + [ + 206, + 278, + 1047 + ], + [ + 210, + 348, + 910 + ], + [ + 212, + 3, + 307 + ], + [ + 213, + 3, + 594 + ], + [ + 224, + 127, + 127 + ], + [ + 226, + 260, + 260 + ], + [ + 229, + 267, + 127 + ], + [ + 236, + 265, + 265 + ] + ], + "witness": [ + 57, + 92, + 127, + 267, + 2 + ] + }, + { + "boundary": 13378, + "helper": 227, + "public_bounds": [ + [ + 7, + 264, + 264 + ], + [ + 81, + 127, + 127 + ], + [ + 92, + 267, + 267 + ], + [ + 112, + 3, + 593 + ], + [ + 119, + 3, + 594 + ], + [ + 121, + 549, + 549 + ], + [ + 124, + 3, + 3 + ], + [ + 125, + 3, + 594 + ], + [ + 127, + 3, + 602 + ], + [ + 128, + 3, + 594 + ], + [ + 139, + 3, + 594 + ], + [ + 142, + 3, + 411 + ], + [ + 146, + 531, + 531 + ], + [ + 154, + 3, + 602 + ], + [ + 160, + 345, + 1059 + ], + [ + 161, + 3, + 46 + ], + [ + 162, + 529, + 529 + ], + [ + 166, + 3, + 327 + ], + [ + 169, + 553, + 553 + ], + [ + 170, + 3, + 3 + ], + [ + 171, + 3, + 412 + ], + [ + 173, + 559, + 559 + ], + [ + 174, + 3, + 593 + ], + [ + 182, + 3, + 593 + ], + [ + 184, + 3, + 593 + ], + [ + 205, + 3, + 3 + ], + [ + 206, + 278, + 1047 + ], + [ + 210, + 348, + 910 + ], + [ + 212, + 3, + 307 + ], + [ + 213, + 3, + 594 + ], + [ + 227, + 267, + 127 + ], + [ + 229, + 267, + 127 + ], + [ + 230, + 261, + 261 + ] + ], + "witness": [ + 7, + 112, + 264, + 593, + 11 + ] + }, + { + "boundary": 13378, + "helper": 233, + "public_bounds": [ + [ + 57, + 127, + 127 + ], + [ + 81, + 127, + 127 + ], + [ + 92, + 267, + 267 + ], + [ + 121, + 549, + 549 + ], + [ + 125, + 3, + 594 + ], + [ + 127, + 3, + 602 + ], + [ + 139, + 3, + 594 + ], + [ + 142, + 3, + 411 + ], + [ + 146, + 531, + 531 + ], + [ + 160, + 345, + 1059 + ], + [ + 161, + 3, + 46 + ], + [ + 162, + 529, + 529 + ], + [ + 169, + 553, + 553 + ], + [ + 170, + 3, + 3 + ], + [ + 171, + 3, + 412 + ], + [ + 173, + 559, + 559 + ], + [ + 174, + 3, + 593 + ], + [ + 205, + 3, + 3 + ], + [ + 206, + 278, + 1047 + ], + [ + 210, + 348, + 910 + ], + [ + 224, + 127, + 127 + ], + [ + 226, + 260, + 260 + ], + [ + 229, + 267, + 127 + ], + [ + 233, + 550, + 678 + ], + [ + 236, + 265, + 265 + ] + ], + "witness": [ + 57, + 92, + 127, + 267, + 2 + ] + }, + { + "boundary": 13378, + "helper": 235, + "public_bounds": [ + [ + 92, + 267, + 267 + ], + [ + 112, + 3, + 593 + ], + [ + 119, + 3, + 594 + ], + [ + 120, + 3, + 430 + ], + [ + 121, + 549, + 549 + ], + [ + 125, + 3, + 594 + ], + [ + 127, + 3, + 602 + ], + [ + 128, + 3, + 594 + ], + [ + 129, + 317, + 1055 + ], + [ + 130, + 541, + 144 + ], + [ + 134, + 3, + 595 + ], + [ + 139, + 3, + 594 + ], + [ + 151, + 543, + 543 + ], + [ + 152, + 3, + 17 + ], + [ + 154, + 3, + 602 + ], + [ + 157, + 3, + 3 + ], + [ + 169, + 553, + 553 + ], + [ + 173, + 559, + 559 + ], + [ + 174, + 3, + 593 + ], + [ + 176, + 3, + 449 + ], + [ + 182, + 3, + 593 + ], + [ + 184, + 3, + 593 + ], + [ + 206, + 278, + 1047 + ], + [ + 207, + 3, + 3 + ], + [ + 208, + 3, + 450 + ], + [ + 215, + 318, + 901 + ], + [ + 219, + 3, + 3 + ], + [ + 220, + 3, + 374 + ], + [ + 224, + 127, + 127 + ], + [ + 225, + 267, + 127 + ], + [ + 226, + 260, + 260 + ], + [ + 227, + 267, + 127 + ], + [ + 234, + 267, + 127 + ], + [ + 235, + 549, + 127 + ], + [ + 238, + 266, + 266 + ] + ], + "witness": [ + 92, + 112, + 267, + 593, + 1 + ] + }, + { + "boundary": 13378, + "helper": 237, + "public_bounds": [ + [ + 7, + 264, + 264 + ], + [ + 57, + 127, + 127 + ], + [ + 81, + 127, + 127 + ], + [ + 92, + 267, + 267 + ], + [ + 119, + 3, + 594 + ], + [ + 120, + 3, + 430 + ], + [ + 121, + 549, + 549 + ], + [ + 128, + 3, + 594 + ], + [ + 129, + 317, + 1055 + ], + [ + 130, + 541, + 144 + ], + [ + 146, + 531, + 531 + ], + [ + 151, + 543, + 543 + ], + [ + 152, + 3, + 17 + ], + [ + 154, + 3, + 602 + ], + [ + 162, + 529, + 529 + ], + [ + 169, + 553, + 553 + ], + [ + 173, + 559, + 559 + ], + [ + 174, + 3, + 593 + ], + [ + 176, + 3, + 449 + ], + [ + 206, + 278, + 1047 + ], + [ + 207, + 3, + 3 + ], + [ + 208, + 3, + 450 + ], + [ + 215, + 318, + 901 + ], + [ + 224, + 127, + 127 + ], + [ + 228, + 529, + 127 + ], + [ + 234, + 267, + 127 + ], + [ + 237, + 258, + 258 + ], + [ + 451, + 262, + 737 + ], + [ + 497, + 520, + 520 + ] + ], + "witness": [ + 7, + 119, + 264, + 594, + 11 + ] + } + ], + "witnesses_sha256": "46b34eea4ede33fb71a3e45b0ace22dbd36dddff5002aca3e8d6c172230c206c" + } +} diff --git a/research/p104-owned-cleanup-obstruction/SOURCES.json b/research/p104-owned-cleanup-obstruction/SOURCES.json new file mode 100644 index 0000000000..9fa46dac00 --- /dev/null +++ b/research/p104-owned-cleanup-obstruction/SOURCES.json @@ -0,0 +1,41 @@ +{ + "schema_version": 1, + "base_commit": "5e0052ca0aa3036a3afa8b0438927377c8d97d53", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "fc3d4ba105e1f097d0d7d051a308281e86ab1446", + "sha256": "66974efdced4083c00025f97d95d83909a226cdf801edb9301c195c6641f6903" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "research/p104-owned-cleanup-obstruction/inputs/pr5569-WORD.json.gz", + "usage": "input", + "git_blob": "3f4eb4be87a2f7a96391c39d960eedeb7bef5d1c", + "sha256": "12224e9a13a49c830b304338a8d31610fb43da15d1a650537733c27f7864310f", + "pin": "head:6784bc3d6e38d2092f4b43da5c1d2dabbd763092:research/p104-owned-cleanup-obstruction/inputs/pr5569-WORD.json.gz" + }, + { + "path": "research/p104-owned-cleanup-obstruction/inputs/pr5561-WORD.json.gz", + "usage": "input", + "git_blob": "c367d865a154ffd2ae0b6f6053469580a139f487", + "sha256": "b3701d78bee3661382ebe5414e678dfc9ee292e254cb9dc56339c2d2f45fdf44", + "pin": "head:6784bc3d6e38d2092f4b43da5c1d2dabbd763092:research/p104-owned-cleanup-obstruction/inputs/pr5561-WORD.json.gz" + } + ], + "retained_origin": { + "pr_url": "https://github.com/CrocSwap/integer-mult-bounds/pull/5569", + "head": "af9f091ac6f30c6eaacb9c27777bfbe2d0e5ffdf", + "original_paths": [ + "research/p104-priced-handoff/WORD.json.gz", + "research/p104-priced-handoff/inputs/pr5561-WORD.json.gz" + ], + "scope": "Byte-identical files retained with attribution in this publication history. Original foreign commit is not required by registered replay." + } +} diff --git a/research/p104-owned-cleanup-obstruction/TASK.json b/research/p104-owned-cleanup-obstruction/TASK.json new file mode 100644 index 0000000000..77b8673b97 --- /dev/null +++ b/research/p104-owned-cleanup-obstruction/TASK.json @@ -0,0 +1,130 @@ +{ + "schema_version": 1, + "task_id": "scalar-to-moment", + "priority_revision": 7, + "base_commit": "5e0052ca0aa3036a3afa8b0438927377c8d97d53", + "original_card": { + "id": "scalar-to-moment", + "question": "Can a changed frame itinerary remove a paid transition beyond the already covered scalar A2 contractions?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/staged544-a2-graph-rewrite/README.md", + "research/staged544-separated-a2/README.md", + "research/staged544-a2-composition-audit/README.md", + "research/staged544-a1858-contraction-audit/README.md" + ], + "methods": [ + "Derive the changed legal frame itinerary and exact child histogram.", + "Prove a scoped obstruction showing why that scalar gain cannot change the paid contract." + ], + "acceptance_gate": "An unchanged histogram is not a kappa gain; record any separate runtime or proof benefit explicitly.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read the A2 and separated-A2 constructions and their composition/contraction audits. Scalar contractions can preserve the complete recursive histogram; fewer ADDs alone do not justify further scans.", + "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately." + }, + "first_experiment": "Identify an actual paid transition to remove and construct a legal replacement frame itinerary, charging restoration, source windows and changed helpers. Compare complete before/after histograms. Stop if only scalar count changes; report that benefit honestly, without expanding the same scalar-only census.", + "bottleneck_link": "A legal change to the histogram, not addition count alone, is the bridge to an exponent gain.", + "allowed_variations": [ + "One existing scalar simplification and one proposed frame-path change." + ], + "scope_change_triggers": [ + "Submitting only another scalar count as completion of a paid-profile task." + ], + "overlap_terms": [ + "scalar simplification", + "paid profile", + "R439", + "3998", + "4019", + "4112", + "4152", + "staged544-a2-graph-rewrite", + "staged544-separated-a2", + "staged544-a2-composition-audit", + "staged544-a1858-contraction-audit" + ], + "existing_checks": [ + { + "scope": "PR #3998: consecutive A2 scalar contraction", + "evidence": "research/staged544-a2-graph-rewrite/README.md", + "remaining": "A genuinely changed paid itinerary or a distinct independent audit; no default scalar-only expansion.", + "status": "author-checked", + "source_commit": "389268a6b5e0373a3125d5c6fcd6995f4ea324f5", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4019: separated A2 sites with unchanged recursive histogram", + "evidence": "research/staged544-separated-a2/README.md", + "remaining": "A genuinely changed paid itinerary or a distinct independent audit; no default scalar-only expansion.", + "status": "author-checked", + "source_commit": "f408e09df300b575235f7f77f81948071397e16d", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4112: composition audit", + "evidence": "research/staged544-a2-composition-audit/README.md", + "remaining": "A genuinely changed paid itinerary or a distinct independent audit; no default scalar-only expansion.", + "status": "author-checked", + "source_commit": "205b7380656ba4b6316a8a493b1a3c679b8f7a0e", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4152: A1858 contraction audit", + "evidence": "research/staged544-a1858-contraction-audit/README.md", + "remaining": "A genuinely changed paid itinerary or a distinct independent audit; no default scalar-only expansion.", + "status": "author-checked", + "source_commit": "caaa14cde5962adc372fdca71f63d0f29e73c8b2", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "refined", + "actual_scope": "Can the owned-holder states omitted by PR5569 support a cheaper early cleanup, or can exact frame and boundary obstructions close specific mechanisms?", + "scope_change_reason": "The donor explicitly assigned P104 early cleanup with owned temporaries. PR5569 identifies 2832 skipped owned-holder geometries. We test that gap and the literal owned delivery blocks, rather than rerunning the older A2 census.", + "bottleneck_link": "The candidate mechanism must reduce a paid recursive transport moment after all public restorations and owned transports are charged. The result rules out specified routes to such savings; it supplies no new kappa or productive credit.", + "budget_minutes": 180, + "stop_rule": "Stop each template when an exact obstruction covers its declared domain. Do not expand a coefficient or frame grid after a source-window proof excludes every common subspace. Publish checked scope limits and the next changed-model question.", + "outcome": "negative-result", + "evidence": "Seven fixed-boundary star floors, nonadditive loss-space bound, joint eight-crossing count floor, and 29688-case public multi-partner obstruction for owned738. PROOF-*.md and verify.py provide exact source checks and semantic controls. The 5252-case window census independently corroborates concurrent PR5579 and is not claimed as novel.", + "author": "flyingviper, with substantial OpenAI Codex assistance and independent agents", + "ai_assistance": "Substantial OpenAI Codex assistance for analysis, Python, prose and publication; independent agents implemented a separate window census, audited source supports and boundaries, and searched primary literature. No independent human or proof-kernel acceptance is claimed.", + "open_questions": [ + { + "question": "Can a changed public dependency or a cleanup network using multiple contact charts lower the complete paid-minus-productive profile?", + "why_it_matters": "The all-holder window obstruction rules out a single common chart with unchanged scalar contacts, not multi-stage scalar redesign.", + "first_step": "Choose one required delivery, specify a changed dependency and all entry/exit rows and frames, then derive its exact replacement histogram before optimizing coefficients.", + "blocked_by": "Needs a new legal scalar/frame itinerary and complete native, ownership, ordinary-cost and funding replay; current results provide no candidate." + }, + { + "question": "Can work shared across owned lifetimes beat the separate fixed-boundary star floors?", + "why_it_matters": "The seven local optima do not apply when outside side information or private work crosses their boundaries; the global loss-space bounds are not additive.", + "first_step": "Write a joint public boundary and identify one specific transport whose information could serve two required values; verify the exact transfer map and account for new helpers.", + "blocked_by": "A feasible shared construction or a joint information-flow lower bound is missing; adding separate H7 bounds is invalid." + } + ], + "source_baseline": { + "pr": 5569, + "head": "af9f091ac6f30c6eaacb9c27777bfbe2d0e5ffdf", + "status": "Full original verifier passed locally before these checks; conditional and unselected." + }, + "expansion_gate": { + "ownership_contract": "735 arbitrary public inputs; zero-initialized owned fields may descend and be erased under the inherited source contract; public fields ascend.", + "proved_cost": "Seven separate fixed-delivery blocks attain their raw recursive paid moment floor for every 0= public and role not in owned, 'fresh private lifetime') + owned[role] = None + elif op == 'COPY': + need(role >= public and role in owned and owned[role] is None and event[2] < public, + 'COPY of one public producer') + coefficient = Q(event[-2]) + need(coefficient != 0, 'nonzero private COPY') + owned[role] = (event[2], coefficient) + elif op == 'CLEAR': + need(role in owned, 'active private CLEAR') + del owned[role] + elif op == 'SCALE' and role >= public: + need(role in owned and owned[role] is not None, 'scaled private copy') + source, coefficient = owned[role] + need(Q(event[-2]) != 0, 'nonzero private SCALE') + owned[role] = source, coefficient * Q(event[-2]) + elif op in ('ADD', 'SCALE'): + need(role < public, 'only scaled-copy private template') + need(all(value is None or value[0] != role for value in owned.values()), + 'copied producer remains unchanged throughout owned lifetime') + if op == 'SCALE': + need(Q(event[-2]) != 0, 'invertible public SCALE') + lowered = ('SCALE', role, Q(event[-2])) + else: + source, coefficient = event[2], Q(event[-2]) + if source >= public: + need(source in owned and owned[source] is not None, 'live private source') + source, factor = owned[source] + coefficient *= factor + census['owned_to_public_shear'] += 1 + need(source != role and coefficient != 0, 'invertible public ADD') + lowered = ('ADD', role, source, coefficient) + census[op] += 1 + else: + need(op == 'MOVE', 'known event type') + effective.append(lowered) + need(not owned, 'all owned lifetimes closed') + return effective, dict(census) + + +def _windows(word): + public = word['public'] + count = public + 8 + index = [[] for _ in range(count)] + windows = [[] for _ in range(count)] + chain = [[f] for f in word['initial']] + [[None] for _ in range(8)] + for i, event in enumerate(word['program']): + op, role = event[:2] + if op == 'MOVE': + need(chain[role][-1] == event[2], 'window source frame') + chain[role].append(event[3]) + continue + roles = (role,) if op in ('INIT', 'CLEAR', 'SCALE') else (role, event[2]) + for r in roles: + index[r].append(i) + windows[r].append(chain[r]) + chain[r] = [None if op == 'CLEAR' else event[-1]] + for r in range(count): + windows[r].append(chain[r]) + return index, windows + + +def _add(row, source, coefficient): + for key, value in source.items(): + result = row.get(key, Q(0)) + coefficient * value + if result: + row[key] = result + else: + row.pop(key, None) + + +def _initial_value(effective, public): + rows = [{r: Q(1)} for r in range(public)] + for operation in effective[:13411]: + if operation is None: + continue + if operation[0] == 'SCALE': + rows[operation[1]] = {k: operation[2] * x for k, x in rows[operation[1]].items()} + else: + _, role, source, coefficient = operation + _add(rows[role], rows[source], coefficient) + return {key: -value / 2 for key, value in rows[133].items()} + + +def _covector_step(value, operation): + """If x' = E x, fixed value c*x has coordinates c*E^-1 in x'.""" + if operation is None: + return + role = operation[1] + if operation[0] == 'SCALE': + if role in value: + value[role] /= operation[2] + elif value.get(role): + source, coefficient = operation[2:] + updated = value.get(source, Q(0)) - coefficient * value[role] + if updated: + value[source] = updated + else: + value.pop(source, None) + + +def _pair_witness(bounds, masks): + upper = (1 << 512) - 1 + for _, high in bounds.values(): + upper &= masks[high] + for role, (low, _) in bounds.items(): + missing = masks[low] & ~upper + if missing: + vector = (missing & -missing).bit_length() - 1 + other, high = next((r, high) for r, (_, high) in bounds.items() + if not (masks[high] >> vector & 1)) + return [role, other, low, high, vector] + return None + + +def _check_pair(pair, bounds, masks): + left, right, low, high, vector = pair + need(left in bounds and right in bounds, 'pair roles are necessary support or recipient') + need(bounds[left][0] == low and bounds[right][1] == high, 'pair binds actual windows') + need(masks[low] >> vector & 1 and not (masks[high] >> vector & 1), 'separating pair vector') + + +def _compute(word): + P = word['program'] + need(word['public'] == 735 and len(P) == 25140, 'pinned word shape') + need(P[13408] == ['INIT', 738, 591] and P[13409] == ['COPY', 738, 133, '1', 591] + and P[13410] == ['SCALE', 738, '-1/2', 591] + and P[13423] == ['CLEAR', 738, 597], 'owned738 source binding') + target_events = [(13412, 159, '-1'), (13414, 203, '2'), (13417, 148, '2'), + (13420, 710, '1'), (13422, 734, '1')] + effective, census = _ops(word) + index, windows = _windows(word) + masks = [_span(frame) for frame in word['frames']] + frames = word['frames'] + deliveries = [] + for event, role, coefficient in target_events: + need(P[event][:4] == ['ADD', role, 738, coefficient], 'actual delivery binding') + slot = index[role].index(event) + low, high = windows[role][slot][0], windows[role][slot + 1][-1] + previous = index[role][slot - 1] if slot else -1 + following = index[role][slot + 1] if slot + 1 < len(index[role]) else len(P) + # Sum of lower recipient and mandatory owned terminal span. + joined = {0} + for vector in frames[low] + frames[597]: + joined |= {x ^ vector for x in joined} + ceiling = masks[high] & masks[591] + need(all(ceiling >> vector & 1 for vector in joined), 'source delivery route feasible') + deliveries.append({'recipient': role, 'event': event, 'previous_contact': previous, + 'next_contact': following, 'lower_frame': low, 'upper_frame': high, + 'minimum_dimension': len(joined).bit_length() - 1, + 'maximum_dimension': ceiling.bit_count().bit_length() - 1}) + need([(x['minimum_dimension'], x['maximum_dimension']) for x in deliveries] + == [(7, 7), (6, 6), (3, 4), (1, 1), (1, 1)], 'complete delivery dimension alternatives') + owned_profiles = [] + for middle in (3, 4): + dims = [8, 7, 6, middle, 1] + owned_profiles.append(Counter(a - b for a, b in zip(dims, dims[1:]))) + need(owned_profiles == [Counter({1: 2, 2: 1, 3: 1})] * 2, 'both owned alternatives have identical invoice') + middle_delivery = deliveries[2] + lower_dim = len(frames[middle_delivery['lower_frame']]) + upper_dim = len(frames[middle_delivery['upper_frame']]) + need((lower_dim, upper_dim) == (2, 5), 'recipient148 neighboring dimensions') + need(Counter([3-lower_dim, upper_dim-3]) == Counter([4-lower_dim, upper_dim-4]), + 'recipient148 alternate invoice is equal') + initial = _initial_value(effective, word['public']) + value = dict(initial) + counts = {x['recipient']: 0 for x in deliveries} + examples, witnesses = {}, [] + for boundary, operation in enumerate(effective[:max(x['next_contact'] for x in deliveries)]): + _covector_step(value, operation) + if boundary in (13376, 13410): + need(value == {133: Q(-1, 2)}, 'unique value coordinates at producer birth and private COPY') + for d in deliveries: + role = d['recipient'] + if not d['previous_contact'] <= boundary < d['next_contact']: + continue + need(value.get(role, Q(0)) == 0, 'recipient is not needed to represent copied value') + bounds = {role: (d['lower_frame'], d['upper_frame'])} + for donor in sorted(value): + chain = windows[donor][bisect_right(index[donor], boundary)] + bounds[donor] = chain[0], chain[-1] + pair = _pair_witness(bounds, masks) + need(pair is not None, 'every public multipartner replacement lacks a common chart') + _check_pair(pair, bounds, masks) + counts[role] += 1 + witnesses.append([boundary, role, pair]) + if role not in examples: + examples[role] = {'boundary': boundary, 'pair': pair, 'support_size': len(value), + 'bounds': [[r, a, b] for r, (a, b) in sorted(bounds.items())]} + result = {'status': 'PASS_OWNED738_DELIVERY_OBSTRUCTION', + 'effective_public_operations': census, + 'delivery_windows': deliveries, + 'owned_paid_histogram_both_alternatives': {'1': 2, '2': 1, '3': 1}, + 'public148_paid_histogram_both_alternatives': {'1': 1, '2': 1}, + 'public_replacement_boundaries': {str(r): n for r, n in counts.items()}, + 'all_public_replacement_boundaries': len(witnesses), + 'witnesses_sha256': sha256(json.dumps(witnesses, separators=(',', ':')).encode()).hexdigest(), + 'initial_value_support': len(initial), + 'pair_examples': {str(r): value for r, value in examples.items()}, + 'new_bound': False} + return result, effective, initial, masks + + +def _rejected(fn): + try: + fn() + except ValueError: + return True + return False + + +def verify(word): + """Authenticate the scientific input externally, then recompute this gate.""" + result, effective, initial, masks = _compute(word) + changed_producer = json.loads(json.dumps(word)) + changed_producer['program'][13412][1] = 133 + zero_scale = json.loads(json.dumps(word)) + scale_event = next(e for e in zero_scale['program'] if e[0] == 'SCALE' and e[1] < word['public']) + scale_event[-2] = '0' + example = next(iter(result['pair_examples'].values())) + bounds = {r: (a, b) for r, a, b in example['bounds']} + bad_pair = example['pair'][:-1] + [0] + def altered_functional(): + value = dict(initial) + value[0] = value.get(0, Q(0)) + 1 + for operation in effective[:13411]: + _covector_step(value, operation) + need(value == {133: Q(-1, 2)}, 'target functional matches private copy') + controls = { + 'copied_public_producer_changed': _rejected(lambda: _ops(changed_producer)), + 'singular_public_scale': _rejected(lambda: _ops(zero_scale)), + 'altered_target_functional': _rejected(altered_functional), + 'zero_separating_vector': _rejected(lambda: _check_pair(bad_pair, bounds, masks)), + } + need(all(controls.values()), 'owned738 semantic mutation controls') + # Minimal algebraic positive control for the covector direction. + value = {0: Q(1)} + _covector_step(value, ('ADD', 0, 1, Q(2))) + need(value == {0: Q(1), 1: Q(-2)}, 'inverse elementary-row covector control') + result['corruption_controls'] = controls + result['covector_positive_control'] = 'D=x0 before x0+=2*x1 becomes x0-2*x1 afterward' + return result diff --git a/research/p104-owned-cleanup-obstruction/check_lifetimes.py b/research/p104-owned-cleanup-obstruction/check_lifetimes.py new file mode 100644 index 0000000000..c4a7c518ba --- /dev/null +++ b/research/p104-owned-cleanup-obstruction/check_lifetimes.py @@ -0,0 +1,259 @@ +"""Portable independent rational boundary checker for the eight owned blocks. + +Only stdlib imports; no side effects on import. The caller supplies the decoded +word and owns source pinning. This is not a complete native/funding verifier. +""" +from fractions import Fraction as Q +import copy + +# Literal public boundary specification, independently transcribed from the +# frozen source. Source byte/hash provenance belongs to the caller. +SPECS = { + 735: (173, [704,705,706], ['1/2']*3), + 736: (151, [707,708,733], ['1/2']*3), + 737: (146, [709,732], ['-1/2']*2), + 738: (133, [159,203,148,710,734], ['1/2','-1','-1','-1/2','-1/2']), + 739: (256, [712,713,714,715,716], ['1/4']*5), + 740: (92, [717,718,719,720,721], ['1/4']*5), + 741: (9, [722,723,724,725,726], ['1/4']*5), + 742: (240, [727,728,729,730,731], ['-1/4']*5), +} + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def add(row, source, coefficient): + out = dict(row) + for k, x in source.items(): + value = out.get(k, Q(0)) + coefficient*x + if value: + out[k] = value + else: + out.pop(k, None) + return out + + +def apply(rows, event): + op, dst = event[:2] + if op == 'MOVE': + return + if op in ('INIT', 'CLEAR'): + rows[dst] = {} + elif op == 'SCALE': + rows[dst] = {k: Q(event[2])*x for k, x in rows[dst].items()} + elif op == 'COPY': + rows[dst] = {k: Q(event[3])*x for k, x in rows[event[2]].items()} + elif op == 'ADD': + rows[dst] = add(rows[dst], rows[event[2]], Q(event[3])) + else: + raise ValueError('unknown scalar event') + + +def rational_rank(rows): + pivots = {} + for row in rows: + row = dict(row) + while row: + p = min(row) + if p not in pivots: + divisor = row[p] + pivots[p] = {k: x/divisor for k, x in row.items()} + break + row = add(row, pivots[p], -row[p]) + return len(pivots) + + +def binary_rank(vectors): + pivots = {} + for x in vectors: + while x: + p = x.bit_length()-1 + if p in pivots: + x ^= pivots[p] + else: + pivots[p] = x + break + return len(pivots) + + +def jsonrow(row): + return {str(k): str(x) for k, x in sorted(row.items())} + + +def add_hist(hist, degree): + hist[degree] = hist.get(degree, 0)+1 + + +def verify(w): + """Check the eight fixed public boundary blocks; return a JSON-safe receipt. + + The input is a decoded WORD object. No input mutation or filesystem access + occurs. This is not a complete native character or funding verifier. + """ + events, frames, public = w['program'], w['frames'], w['public'] + n = public+8 + need(public == 735, 'frozen role count') + intervals = {} + for owned in range(public, n): + starts_found = [i for i, e in enumerate(events) if e[:2] == ['INIT', owned]] + stops_found = [i+1 for i, e in enumerate(events) if e[:2] == ['CLEAR', owned]] + need(len(starts_found) == len(stops_found) == 1, 'one INIT/CLEAR per owned lifetime') + start, stop = starts_found[0], stops_found[0] + need(start < stop, 'INIT before CLEAR') + intervals[owned] = (start, stop) + need(all(intervals[r][1] == intervals[r+1][0] for r in range(735, 742)), 'consecutive blocks') + + rows = [{i: Q(1)} for i in range(public)]+[{} for _ in range(8)] + chart = list(w['initial'])+[None for _ in range(8)] + snapshots = {} + starts = {x[0]: r for r, x in intervals.items()} + ends = {x[1]: r for r, x in intervals.items()} + for i, e in enumerate(events): + if i in starts: + snapshots[(starts[i], 'before')] = ([dict(row) for row in rows], list(chart)) + op, dst = e[:2] + if op == 'INIT': + need(dst >= public and chart[dst] is None, 'INIT requires inactive private field') + chart[dst] = e[2] + elif op == 'MOVE': + need(chart[dst] is not None and chart[dst] == e[2], 'declared old frame matches active frame') + need(e[4] == (dst >= public), 'MOVE ownership flag matches role') + a, b = frames[e[2]], frames[e[3]] + need(binary_rank(a+b) == max(len(a),len(b)), 'MOVE charts nested') + need((len(a) >= len(b)) if e[4] else (len(a) <= len(b)), 'MOVE follows ownership direction') + chart[dst] = e[3] + elif op == 'CLEAR': + need(dst >= public and chart[dst] is not None and chart[dst] == e[2], 'CLEAR active private frame') + chart[dst] = None + elif op == 'SCALE': + need(chart[dst] is not None and chart[dst] == e[3], 'SCALE common frame') + elif op in ('ADD','COPY'): + need(chart[dst] is not None and chart[e[2]] is not None and chart[dst] == chart[e[2]] == e[4], 'ADD/COPY common frame') + if op == 'COPY': + need(dst >= public and rows[dst] == {}, 'COPY requires zero private destination') + else: + raise ValueError('unknown opcode') + apply(rows, e) + if i+1 in ends: + snapshots[(ends[i+1], 'after')] = ([dict(row) for row in rows], list(chart)) + + results = [] + for owned, (start, stop) in intervals.items(): + block = events[start:stop] + copies = [e for e in block if e[0] == 'COPY'] + need(len(copies) == 1 and copies[0][1] == owned, 'single source copy') + source = copies[0][2] + expected_source, expected_recipients, expected_coefficients = SPECS[owned] + need(source == expected_source, 'fixed local source role') + recipients = [e[1] for e in block if e[0] == 'ADD'] + need(recipients == expected_recipients, 'fixed local recipient roles') + need(len(set(recipients)) == len(recipients), 'one delivery per recipient') + need(all(e[2] == owned for e in block if e[0] == 'ADD'), 'owned source at deliveries') + roles = [source]+recipients + controls = roles+[owned] + before, entry = snapshots[(owned, 'before')] + after, exit_frames = snapshots[(owned, 'after')] + prefix_rank = rational_rank([before[r] for r in roles]) + need(prefix_rank == len(roles), 'public local prefix coordinates independent') + need(after[source] == before[source], 'source unchanged') + need(after[owned] == {}, 'owned exit zero') + need(all(before[r] == after[r] for r in range(public) if r not in recipients), + 'no outside public scalar row changed') + local = [{} for _ in range(n)] + for j, r in enumerate(controls): + local[r] = {j: Q(1)} + for e in block: + apply(local, e) + transfers = {} + for j, r in enumerate(recipients, 1): + need(set(local[r]) == {0, j} and local[r][j] == 1, 'exact local delivery form') + transfers[r] = local[r][0] + need(transfers[r] == Q(expected_coefficients[j-1]), 'fixed local transfer coefficient') + need(after[r] == add(before[r], before[source], transfers[r]), 'actual prefix delivery') + need(local[source] == {0: Q(1)} and local[owned] == {}, 'local source and zero exit') + suffix = [{} for _ in range(n)] + for j, r in enumerate(controls): + suffix[r] = {j: Q(1)} + for e in events[stop:]: + apply(suffix, e) + suffix_rank = rational_rank(suffix[:public]) + need(suffix_rank == len(roles), 'fixed suffix observes every public local coordinate') + need(all(len(roles) not in row for row in suffix[:public]), 'retired owned has no public suffix influence') + last_add = max(i for i in range(start, stop) if events[i][0] == 'ADD') + healthy = [{} for _ in range(n)] + damaged = [{} for _ in range(n)] + for j, r in enumerate(controls): + healthy[r] = damaged[r] = {j: Q(1)} + for i in range(start, len(events)): + apply(healthy, events[i]) + if i != last_add: + apply(damaged, events[i]) + different = [r for r in range(public) if healthy[r] != damaged[r]] + need(bool(different), 'omitted delivery negative control observed') + paid, private_paid, public_paid = {}, {}, {} + for e in block: + if e[0] == 'MOVE': + a, b = frames[e[2]], frames[e[3]] + need(binary_rank(a+b) == max(len(a), len(b)), 'source move charts nested') + degree = abs(len(a)-len(b)) + add_hist(paid, degree) + add_hist(private_paid if e[4] else public_paid, degree) + support = before[source] + entry_vectors = [v for r in support for v in frames[w['initial'][r]]] + star = all(len(frames[entry[r]]) == 0 and len(frames[exit_frames[r]]) == 1 for r in recipients) + if star: + need(private_paid == {7: 1} and public_paid == {1: len(recipients)}, 'tight uniform star tariff') + need(all(before[r] == {r: Q(1)} for r in recipients), 'star recipients independent original symbols') + need(len(frames[entry[source]]) == 8, 'star source dimension eight') + result = { + 'owned': owned, 'events_half_open': [start, stop], 'source': source, + 'source_role': 'live' if source in w['live'] else 'helper', + 'recipients': recipients, 'transfers_from_source': {str(r): str(c) for r, c in transfers.items()}, + 'entry_frames': {str(r): entry[r] for r in roles}, + 'exit_frames': {str(r): exit_frames[r] for r in roles}, + 'entry_dimensions': {str(r): len(frames[entry[r]]) for r in roles}, + 'exit_dimensions': {str(r): len(frames[exit_frames[r]]) for r in roles}, + 'local_matrix': [jsonrow(local[r]) for r in controls], + 'actual_prefix_rank': prefix_rank, 'public_suffix_rank': suffix_rank, + 'owned_exit_zero': True, 'owned_public_suffix_column_zero': True, + 'source_prefix_nonzeros': len(support), 'source_entry_support_span_dimension': binary_rank(entry_vectors), + 'support_to_recipient_exit_dimension_gaps': {str(r): binary_rank(entry_vectors+frames[exit_frames[r]])-len(frames[exit_frames[r]]) for r in recipients}, + 'local_paid_histogram': paid, 'public_paid_histogram': public_paid, + 'owned_paid_histogram': private_paid, 'omitted_delivery_event': last_add, + 'corruption_changed_public_outputs': different, + 'tight_fixed_boundary_star_theorem_applies': star, + 'no_gain_scope': ('Exact local public boundary charts and map; arbitrary private zero auxiliaries; no outside side information, changed productive targets or credits.' if star else 'No tight local cost floor claimed: delivery charts have several levels.')} + results.append(result) + need(sum(r['tight_fixed_boundary_star_theorem_applies'] for r in results) == 7, 'seven tight star blocks') + result = {'status': 'PASS_EIGHT_OWNED_BOUNDARIES_SEVEN_TIGHT_STARS', + 'lifetimes': results, 'new_kappa': False, + 'global_claim_excluded': 'Per-row owned-preparation floors cannot be added when private work or lost subspaces are shared.'} + return result + + +def mutation_controls(word): + """Require rejection of three local semantic corruptions of a passing word.""" + verify(word) + cases = [] + for name in ('wrong_delivery_sign', 'zeroed_owned_producer', 'wrong_delivery_frame'): + damaged = copy.deepcopy(word) + events = damaged['program'] + if name == 'zeroed_owned_producer': + event = next(e for e in events if e[:2] == ['COPY',735]) + event[3] = '0' + else: + event = next(e for e in events if e[:3] == ['ADD',704,735]) + if name == 'wrong_delivery_sign': + event[3] = '-1' + else: + event[4] = 559 + try: + verify(damaged) + except ValueError as error: + cases.append({'mutation': name, 'rejected': True, 'reason': str(error)}) + else: + raise AssertionError('semantic corruption escaped: '+name) + return cases diff --git a/research/p104-owned-cleanup-obstruction/check_producers.py b/research/p104-owned-cleanup-obstruction/check_producers.py new file mode 100644 index 0000000000..05ee08dce0 --- /dev/null +++ b/research/p104-owned-cleanup-obstruction/check_producers.py @@ -0,0 +1,253 @@ +"""Reusable exact producer-support and loss-space source certificate. + +The caller supplies the authenticated decoded PR5569 word. No filesystem, +network, optimizer or predecessor verifier is used here. +""" +from copy import deepcopy +from fractions import Fraction as Q + + +def need(condition, reason): + if not condition: + raise ValueError(reason) + + +def basis_reduce(vectors): + basis = [] + for original in vectors: + v = original + for row in basis: + v = min(v, v ^ row) + if v: + basis.append(v) + basis.sort(reverse=True) + return basis + + +def span(basis): + out = {0} + for v in basis: + out |= {x ^ v for x in tuple(out)} + return out + + +def loss_floor(support_basis, delivery_basis): + """dim((support+delivery)/delivery), the global descent rank-mass floor.""" + return len(basis_reduce(list(support_basis)+list(delivery_basis))) - len(basis_reduce(delivery_basis)) + + +def verify(word): + program = word['program'] + frames = word['frames'] + need(word['public'] == 735, 'public role inventory') + first_init = next((i for i,e in enumerate(program) if e[0] == 'INIT'), None) + need(first_init == 13377, 'first owned INIT source binding') + targets = [(i,e[1],e[2],e[-1]) for i,e in enumerate(program) if e[0] == 'COPY'] + need([(o,r) for i,o,r,f in targets] == [(735,173),(736,151),(737,146),(738,133), + (739,256),(740,92),(741,9),(742,240)], + 'exact eight owned producer bindings') + coefficients = [{role:Q(1)} for _,_,role,_ in targets] + for event, owned, role, frame in targets: + need(Q(program[event][-2]) != 0, 'nonzero COPY factor') + need(not any(e[1] == role and e[0] != 'MOVE' for e in program[first_init:event]), + 'producer row unchanged between public prefix and COPY') + # Unique pullback through the purely public invertible prefix. + for event in reversed(program[:first_init]): + op, dst = event[:2] + if op == 'MOVE': + need(not event[-1], 'no owned descent in public prefix') + need(span(frames[event[2]]) < span(frames[event[3]]), 'ascending public prefix MOVE') + continue + need(op in ('ADD','SCALE'), 'invertible public prefix operation') + q = Q(event[-2]) + need(q != 0, 'nonzero scalar coefficient') + for covector in coefficients: + if dst not in covector: + continue + if op == 'SCALE': + covector[dst] *= q + else: + src = event[2] + value = covector.get(src,Q(0)) + q * covector[dst] + if value: + covector[src] = value + else: + covector.pop(src,None) + results = [] + for target,covector in zip(targets,coefficients): + event,owned,role,frame = target + vectors = [v for r in covector for v in frames[word['initial'][r]]] + basis = basis_reduce(vectors) + need(len(basis) == 8 and span(basis) == span(frames[frame]), + 'rank-eight entry support equals producer frame') + end = next((j for j in range(event+1,len(program)) if program[j][0] == 'CLEAR' and program[j][1] == owned), None) + need(end is not None, 'owned delivery lifetime closes') + final_frame = program[end][-1] + current = frame + multiplier = Q(program[event][-2]) + paid_ranks = [] + final_reads = 0 + for e in program[event+1:end]: + if e[0] in ('ADD','COPY') and e[2] == owned and e[-1] == final_frame: + final_reads += 1 + if e[1] != owned: + continue + if e[0] == 'SCALE': + need(e[-1] == current and Q(e[-2]) != 0, 'owned scalar preserves producer support') + multiplier *= Q(e[-2]) + elif e[0] == 'MOVE': + need(e[2] == current and e[-1] is True, 'owned paid descent binding') + need(span(frames[e[3]]) < span(frames[current]), 'strict owned descent') + paid_ranks.append(len(frames[current])-len(frames[e[3]])) + current = e[3] + else: + raise ValueError('owned producer payload changed before delivery') + need(current == final_frame and final_reads > 0, 'actual retained delivery frame and read') + lower = loss_floor(basis,frames[final_frame]) + need(lower == 7 and sum(paid_ranks) == 7 and len(frames[final_frame]) == 1, + 'rank-seven loss-space lower bound and source rank mass') + witnesses = [] + independent = [] + for r in sorted(covector): + for v in frames[word['initial'][r]]: + if len(basis_reduce(independent+[v])) > len(independent): + independent.append(v) + witnesses.append({'input':r,'coefficient':str(covector[r]),'initial_vector':v}) + results.append({'owned':owned,'copy_event':event,'source_role':role,'copy_frame':frame, + 'support_count':len(covector),'initial_span_rank':8, + 'nonzero_chart_inputs':sum(bool(frames[word['initial'][r]]) for r in covector), + 'independent_witnesses':witnesses,'clear_frame':final_frame, + 'delivery_factor':str(multiplier),'owned_move_ranks':paid_ranks, + 'required_global_owned_descent_rank_mass':lower, + 'initial_covector':{str(k):str(v) for k,v in sorted(covector.items())}}) + return {'status':'PASS_RANK_EIGHT_PRODUCER_AND_LOSS_SPACE_BINDING','first_owned_init':first_init, + 'results':results,'new_bound':False, + 'scope':'One unchanged scalar target at its retained delivery frame; owned descent cost can be shared across targets, so individual bounds must not be summed.'} + + +def controls(word): + wrong_entry_support = deepcopy(word) + original_support = span(word['frames'][559]) + outside = next(v for v in range(1,512) if v not in original_support) + wrong_entry_support['frames'].append([outside]) + wrong_entry_support['initial'][111] = len(wrong_entry_support['frames'])-1 + wrong_producer = deepcopy(word) + wrong_producer['program'][13378][2] = 704 + unaccounted_descent = deepcopy(word) + move = next(e for e in unaccounted_descent['program'][:13377] if e[0] == 'MOVE') + move[-1] = True + changed_payload = deepcopy(word) + changed_payload['program'][13379] = ['ADD',735,111,'1',559] + rejected = [] + for name,mutant in [('entry_support_outside_producer_frame',wrong_entry_support), + ('wrong_producer_value',wrong_producer), + ('unaccounted_descent_in_public_prefix',unaccounted_descent), + ('changed_owned_payload_before_delivery',changed_payload)]: + try: + verify(mutant) + except ValueError: + rejected.append(name) + else: + raise ValueError('corruption control accepted: '+name) + # A widened delivery interface genuinely weakens the floor: no universal H7 claim. + support = word['frames'][559] + delivery = list(word['frames'][593]) + extra = next(v for v in support if v not in span(delivery)) + widened = delivery+[extra] + need(loss_floor(support,widened) == 6, 'widened-delivery scope control') + return {'rejected_corruptions':rejected,'widened_delivery_rank':2, + 'widened_delivery_loss_floor':6,'individual_floors_not_additive':True} + + +def rational_rank(rows): + """Exact row reduction, returning independent column indices as a witness.""" + rows = [[Q(x) for x in row] for row in rows] + if not rows: + return 0, [] + width = len(rows[0]) + need(all(len(row) == width for row in rows), 'rectangular rational matrix') + pivots = [] + for column in range(width): + at = len(pivots) + pivot = next((j for j in range(at,len(rows)) if rows[j][column]), None) + if pivot is None: + continue + rows[at], rows[pivot] = rows[pivot], rows[at] + q = rows[at][column] + rows[at] = [x/q for x in rows[at]] + for j in range(at+1,len(rows)): + q = rows[j][column] + if q: + rows[j] = [x-q*y for x,y in zip(rows[j],rows[at])] + pivots.append(column) + if len(pivots) == len(rows): + break + return len(pivots), pivots + + +def determinant(matrix): + matrix = [[Q(x) for x in row] for row in matrix] + n = len(matrix) + need(all(len(row) == n for row in matrix), 'square minor') + result = Q(1) + for column in range(n): + pivot = next((j for j in range(column,n) if matrix[j][column]), None) + if pivot is None: + return Q(0) + if pivot != column: + matrix[column],matrix[pivot] = matrix[pivot],matrix[column] + result = -result + q = matrix[column][column] + result *= q + for j in range(column+1,n): + factor = matrix[j][column]/q + for k in range(column+1,n): + matrix[j][k] -= factor*matrix[column][k] + return result + + +def verify_joint_cut(word, producer_receipt): + """Count shared owned crossings; this does NOT prove an eight-H7 tariff.""" + producers = producer_receipt['results'] + need([r['owned'] for r in producers] == list(range(735,743)), 'joint producer order') + delivery_frames = [word['frames'][r['clear_frame']] for r in producers] + need(all(len(frame) == 1 for frame in delivery_frames), 'eight fixed delivery lines') + W_basis = basis_reduce([v for frame in delivery_frames for v in frame]) + need(len(W_basis) == 8, 'joint delivery subspace rank') + W = span(W_basis) + outside = [i for i,f in enumerate(word['initial']) if not span(word['frames'][f]) <= W] + matrix = [[Q(r['delivery_factor'])*Q(r['initial_covector'].get(str(i),0)) for i in outside] + for r in producers] + rank, pivots = rational_rank(matrix) + need(rank == 8, 'eight independent outside-input observations') + minor = [[row[k] for k in pivots] for row in matrix] + det = determinant(minor) + need(det != 0, 'independent exact minor determinant') + crossings = [] + for i,e in enumerate(word['program']): + if e[0] != 'MOVE': + continue + before, after = span(word['frames'][e[2]]), span(word['frames'][e[3]]) + if not before <= W and after <= W: + need(e[-1] is True and after < before, 'every into-W crossing is a paid owned descent') + crossings.append({'event':i,'owned':e[1],'from':e[2],'to':e[3], + 'paid_rank':len(word['frames'][e[2]])-len(word['frames'][e[3]])}) + need(len(crossings) == 8 and sorted(r['owned'] for r in crossings) == list(range(735,743)), + 'source attains eight crossing events') + duplicated = matrix[:-1]+[list(matrix[0])] + duplicated_rank = rational_rank(duplicated)[0] + need(duplicated_rank == 7, 'duplicate-observation scope control') + whole = span([1<= public and role not in active, 'fresh owned lifetime') + rows[role] = {} + current[role] = event[2] + active.add(role) + elif op == 'CLEAR': + need(role in active and current[role] == event[2], 'owned erasure boundary') + rows[role] = {} + current[role] = None + active.remove(role) + else: + factor, frame = Q(event[-2]), event[-1] + need(factor and current[role] == frame, 'scalar destination') + if op == 'SCALE': + rows[role] = {symbol: factor * value for symbol, value in rows[role].items()} + else: + source = event[2] + need(source != role and current[source] == frame, 'common source chart') + if op == 'COPY': + need(role in active and not rows[role], 'COPY into empty owned field') + rows[role] = {symbol: factor * value for symbol, value in rows[source].items()} + else: + need(op == 'ADD', 'known scalar opcode') + target = dict(rows[role]) + for symbol, value in rows[source].items(): + coefficient = target.get(symbol, Q(0)) + factor * value + if coefficient: + target[symbol] = coefficient + else: + target.pop(symbol, None) + rows[role] = target + + +def analyze(word): + public = word['public'] + need(public == 735 and len(word['program']) == 25140, 'source dimensions') + indices, windows, spans = chronology(word) + mains = set(word['live']) | {r + 112 for r in word['live']} + rows = [{r: Q(1)} for r in range(public + 8)] + current = list(word['initial']) + [None] * 8 + active = set() + complete_states, public_states = set(), set() + witnesses, examples = [], [] + by_owned, peak = Counter(), 0 + for boundary, event in enumerate(word['program']): + apply(event, rows, current, active, spans, public) + peak = max(peak, len(active)) + # This is deliberately every event boundary, including MOVE boundaries, + # without the predecessor's touched-symbol or first/last-use filters. + helpers = {h for owned in active for h in rows[owned] if h < public and h not in mains} + for helper in sorted(helpers): + holders = [r for r, row in enumerate(rows) if helper in row] + required = sorted(set(holders) | {helper}) + all_bounds = [(r, window(indices, windows, r, boundary)[0], + window(indices, windows, r, boundary)[-1]) for r in required] + bounds = [(r, left, right) for r, left, right in all_bounds if r < public] + witness = obstruction(bounds, word['frames'], spans) + need(witness is not None, 'public-only obstruction at every owned-holder state') + check_witness(witness, bounds, spans) + complete_states.add((helper, tuple(all_bounds))) + public_states.add((helper, tuple(bounds))) + owned_holders = [r for r in holders if r >= public] + by_owned[','.join(map(str, owned_holders))] += 1 + witnesses.append([boundary, helper, witness]) + if len(examples) < 8: + examples.append({'boundary': boundary, 'helper': helper, + 'public_bounds': [list(bound) for bound in bounds], 'witness': witness}) + need(not active and peak == 1 and current[:public] == word['final'], 'complete source boundaries') + for role, row in enumerate(rows): + target = {role: Q(1)} if role < public else {} + if role - 112 in word['live']: + target[role - 112] = Q(1) + need(row == target, 'full arbitrary-input source transfer') + return { + 'status': 'PASS_PUBLIC_WINDOW_OBSTRUCTION', + 'event_boundaries_with_helper_owned_pairs': len(witnesses), + 'distinct_full_holder_geometries': len(complete_states), + 'distinct_public_holder_geometries': len(public_states), + 'owned_holder_pairs_by_register': dict(sorted(by_owned.items())), + 'all_source_endpoint_rows': len(rows), + 'public_only_witnesses': True, + 'witnesses_sha256': sha256(canonical(witnesses)).hexdigest(), + 'witness_examples': examples, + 'source_role_173': 'productive helper; port61 is not live', + 'new_bound': False, + }, witnesses + + +def positive_control(word): + indices, windows, spans = chronology(word) + public = word['public'] + rows = [{r: Q(1)} for r in range(public + 8)] + current = list(word['initial']) + [None] * 8 + active = set() + for event in word['program'][:15444]: + apply(event, rows, current, active, spans, public) + need(rows[706] == {706: Q(1), **{k: value / 2 for k, value in rows[173].items()}}, + 'positive control cleanup identity') + bounds = [(r, window(indices, windows, r, 15443)[0], + window(indices, windows, r, 15443)[-1]) for r in (706, 173)] + need(all(spans[left] <= spans[559] <= spans[right] for _, left, right in bounds), + 'published positive control has a common chart') + need(obstruction(bounds, word['frames'], spans) is None, 'positive control not falsely rejected') + need(len(word['frames'][word['initial'][706]]) < 8 < len(word['frames'][word['final'][706]]), + 'positive control is a strict interior helper split') + return {'source': 'PR5561 headline word', 'boundary': 15443, 'helper': 706, + 'partner': 173, 'common_frame': 559, 'common_dimension': 8} + + +def rejection(action): + try: + action() + except ValueError: + return True + return False + + +def run(source_raw, control_raw): + word = decode(source_raw, SOURCE_SHA256) + control = decode(control_raw, CONTROL_SHA256) + result, witnesses = analyze(word) + result['positive_control'] = positive_control(control) + spans = list(map(binary_span, word['frames'])) + example = result['witness_examples'][0] + bad_vector = example['witness'][:-1] + [0] + missing_role = example['witness'][:] + missing_role[0] = word['public'] + _, windows, _ = chronology(word) + chain = next(ch for role in windows[:word['public']] for ch in role if len(ch) > 1) + controls = { + 'changed_source_bytes': rejection(lambda: decode(source_raw + b' ', SOURCE_SHA256)), + 'zero_separating_vector': rejection(lambda: check_witness(bad_vector, example['public_bounds'], spans)), + 'owned_role_used_as_public_witness': rejection(lambda: check_witness(missing_role, example['public_bounds'], spans)), + 'reversed_public_window': rejection(lambda: public_window(list(reversed(chain)), spans)), + } + need(all(controls.values()), 'all semantic corruption controls rejected') + result['corruption_controls'] = controls + return result, witnesses diff --git a/research/p104-owned-cleanup-obstruction/inputs/README.md b/research/p104-owned-cleanup-obstruction/inputs/README.md new file mode 100644 index 0000000000..c556a33681 --- /dev/null +++ b/research/p104-owned-cleanup-obstruction/inputs/README.md @@ -0,0 +1,26 @@ +# Retained predecessor inputs + +These two gzip files are unchanged predecessor data, not new constructions. +They are retained so the new obstruction checker has a small, self-contained +source closure. Both compressed byte hashes are enforced before decoding. + +Source: [PR5569](https://github.com/CrocSwap/integer-mult-bounds/pull/5569), +head `af9f091ac6f30c6eaacb9c27777bfbe2d0e5ffdf`: + +| Retained file | Original repository path | Compressed SHA256 | +| --- | --- | --- | +| `pr5569-WORD.json.gz` | `research/p104-priced-handoff/WORD.json.gz` | `12224e9a13a49c830b304338a8d31610fb43da15d1a650537733c27f7864310f` | +| `pr5561-WORD.json.gz` | `research/p104-priced-handoff/inputs/pr5561-WORD.json.gz` | `b3701d78bee3661382ebe5414e678dfc9ee292e254cb9dc56339c2d2f45fdf44` | + +The second file is the PR5561 headline word retained by PR5569. It supplies the +known 706/173 successful cleanup as a positive control; it is not our baseline. +The package's standard provenance pins refer to the retention commit in its own +published history. Original source paths and head are attribution and audit +information, not a claim that a foreign PR commit is an ancestor of this PR. + +Credit: Joel Pulikkan (GamingPuzzled), with Claude Opus 5.5 assistance, for +PR5569; DreamingOfClouds for PR5561 and PR5553; thu-nmrc for PR5551; +aliromman for PR5544/5545; David Arias, Cinna Davis and Gareth Davidson for the +retained local verifier lineage; zxv for the productive-helper paradigm and +PR5554; Cao Yifan for PR4610 native semantics; GamingPuzzled for PR5472. +The source credits PR2305/2152/2219 as earlier lineage. Apache-2.0. diff --git a/research/p104-owned-cleanup-obstruction/inputs/pr5561-WORD.json.gz b/research/p104-owned-cleanup-obstruction/inputs/pr5561-WORD.json.gz new file mode 100644 index 0000000000..c367d865a1 Binary files /dev/null and b/research/p104-owned-cleanup-obstruction/inputs/pr5561-WORD.json.gz differ diff --git a/research/p104-owned-cleanup-obstruction/inputs/pr5569-WORD.json.gz b/research/p104-owned-cleanup-obstruction/inputs/pr5569-WORD.json.gz new file mode 100644 index 0000000000..3f4eb4be87 Binary files /dev/null and b/research/p104-owned-cleanup-obstruction/inputs/pr5569-WORD.json.gz differ diff --git a/research/p104-owned-cleanup-obstruction/verify.py b/research/p104-owned-cleanup-obstruction/verify.py new file mode 100644 index 0000000000..05a364e692 --- /dev/null +++ b/research/p104-owned-cleanup-obstruction/verify.py @@ -0,0 +1,58 @@ +"""Replay the source-bound owned-cleanup obstructions; no network or Git needed.""" +from pathlib import Path +import argparse +import importlib.util +import json + + +HERE = Path(__file__).resolve().parent + + +def module(name): + spec = importlib.util.spec_from_file_location(name, HERE / (name + '.py')) + loaded = importlib.util.module_from_spec(spec) + spec.loader.exec_module(loaded) + return loaded + + +def run(): + windows = module('check_windows') + producers = module('check_producers') + lifetimes = module('check_lifetimes') + exceptional = module('check_738') + source = (HERE / 'inputs/pr5569-WORD.json.gz').read_bytes() + control = (HERE / 'inputs/pr5561-WORD.json.gz').read_bytes() + word = windows.decode(source, windows.SOURCE_SHA256) + window_result, witnesses = windows.run(source, control) + producer_receipt = producers.verify(word) + result = { + 'status': 'PASS_P104_OWNED_CLEANUP_OBSTRUCTIONS', + 'new_bound': False, + 'windows': window_result, + 'producers': producer_receipt, + 'joint_cut': producers.verify_joint_cut(word, producer_receipt), + 'owned738': exceptional.verify(word), + 'producer_controls': producers.controls(word), + 'lifetimes': lifetimes.verify(word), + 'lifetime_controls': lifetimes.mutation_controls(word), + } + return result, witnesses + + +if __name__ == '__main__': + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--write', action='store_true', help='author the receipt') + parser.add_argument('--witnesses', type=Path, help='export all window witnesses') + args = parser.parse_args() + result, witnesses = run() + encoded = json.dumps(result, indent=2, sort_keys=True) + '\n' + if args.write: + (HERE / 'RESULT.json').write_text(encoded, encoding='utf-8', newline='\n') + elif encoded != (HERE / 'RESULT.json').read_text(encoding='utf-8'): + raise ValueError('fresh exact result differs from committed receipt') + if args.witnesses: + args.witnesses.write_text(json.dumps(witnesses, separators=(',', ':')) + '\n', + encoding='utf-8', newline='\n') + print(json.dumps({'status': result['status'], 'new_bound': False, + 'window_cases': result['windows']['event_boundaries_with_helper_owned_pairs'], + 'tight_local_stars': 7, 'source_rows': 743}))