P104: prove owned-block cost floors and public delivery obstructions (no kappa)

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.

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<t<=1. Recipient148's
+own route is2->{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.

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 0<t<=1 (in the source, t=1-kappa). A public MOVE ascends to a
+containing frame and a private owned MOVE descends to a contained frame. A MOVE
+of positive dimension difference d is charged H_d. Rational ADD, SCALE and COPY
+must act at the same current frame. A new owned field starts at zero. CLEAR may
+erase an owned field, under the source's inherited owned-erasure assumptions.
+
+A fixed-delivery replacement for one block has exactly the same public roles,
+entry and exit frames, and public scalar map. It may use arbitrarily many new
+zero-initialized private fields and arbitrary rational linear operations. It
+may change its internal contacts, order and factorization. It leaves all
+private fields zero or cleared at its exit. It cannot read or modify external
+public roles, carry workspace across the boundary, change productive targets,
+or claim new productive credit. These are substantial restrictions; the result
+does not rule out a better complete word or cross-block sharing.
+
+Theorem (uniform delivery star)
+-------------------------------
+Suppose the public boundary has independent coordinates v,x_1,...,x_m. The
+source v starts and ends at dimension a. Each x_j starts at dimension zero and
+ends at one common dimension b frame, where a>b>=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 0<t<=1, within the stated boundary model. Separate local
+replacements cannot improve their combined 28H1+7H7. This combined statement
+does not allow any private work to cross the fixed boundaries.
+
+The theorem does NOT give the observed cost for738. Its recipient entry/exit
+dimensions are 7->7,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.

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.