research: trace V45 recovery and price the remaining margin

research/v45-recovery-transfer/PROOF.md

@@ -0,0 +1,168 @@
+# V45 access, consumed directions, and the remaining cost allowance
+
+## Exact model
+
+Let D = Z[1/2]. For each pinned provider let L be its 520 live non-target
+registers. The input cut is immediately after the 84-event prelude. Give every
+register in L an independent arbitrary entrance value in a D-module W. The
+middle M is the non-target part of A after the prelude, then B with its
+chronological formal warps, then restore. Formal warp generators act by
+arbitrary invertible D-linear maps on W. Target writes, compensation, inverse
+cleanup and native/physical realization are separate obligations.
+
+H consists of live helpers with index at least 224, excluding restored
+`helper_final` coordinates, `start_extra` coordinates and initial-correction
+sources. Its size changes with the construction. In particular P =
+{249,251,265,267} is eligible before the PR2942 extraction and protected afterward.
+A zero entrance frame does not mean a zero entrance value.
+
+Fix V45 = span_F2(256,128,64,35,16,11,5), and the twelve-register allowance
+U = {2,61,62,63,70,71,72,94,249,251,265,267}. Define R(V45) by replaying every
+literal frame incident and selecting all live non-target registers with terminal
+frame contained in V45. Protected/restored rows remain in R. This is not the
+historical solver-lowered support search: U is an explicit algebraic observation
+allowance, and its physical availability must be established separately.
+
+As in the pinned source, separate target-add records use the inherited center-cut
+convention. The frame replay checks the recorded center frames and the literal
+A/B/restore scalar incidents and warp resets. It does not reconstruct additional
+native moves for those separate target records.
+
+## What the exact comparison establishes
+
+Both providers give the same dimensions and supports below. The checker uses
+all coefficients of each observed free-operator row, rather than specializing
+warps to commuting or identity maps.
+
+| Construction | Size of H | Literal R(V45) | Scalar left/right/pairing dimensions on U |
+|---|---:|---|---|
+| PR2894 | 226 | empty | 4 / 4 / 4 |
+| PR2917 | 216 | empty | 4 / 4 / 4 |
+| PR2942 | 212 | empty | 0 / 0 / 0 |
+| PR2979 stage 1 | 212 | U | 0 / 0 / 0 |
+| PR2979 final | 207 | U minus {61,63} | 0 / 0 / 0 |
+
+The complete rows M[U,:] are equal between PR2894 and PR2917 (98 nonzero
+coefficients), and equal between PR2942, stage 1 and final (42 coefficients).
+The four-dimensional old pairing has determinant -128. Eight selected nuisance
+columns B0 have an eight-row minor of determinant -2, and the twelve-column
+completion [Y,B0] has determinant 256. All are dyadic units. Thus
+PR2917 did not create these four directions on U: they were already available
+algebraically in PR2894. Neither old shipped circuit makes U available at V45.
+The paid frame and boundary changes are essential to the implemented recovery.
+
+On every later word, M[U,H] is identically zero. This is stronger than a rank-zero
+pairing. Moreover the U nuisance rows admit a purely scalar square minor on
+protected columns with determinant 2, a unit of D. The final ten-row literal
+support has a protected scalar unit minor with determinant 1. If P is returned
+to the eligible set solely as a diagnostic, the left/right/pairing dimensions
+are again 4 / 4 / 4. The four rows indexed by P are their restored identity rows.
+This does not authorize treating those protected helpers as fresh resources.
+
+## The old quotient over every dyadic module
+
+The receipt records four covectors Alpha, four eligible quantities U0=Alpha M,
+four eligible columns V, and Y=M V, with Alpha B0=0. Set K=Alpha Y. Both
+K and C=[Y,B0] are invertible over D by their unit determinants. Every readout
+has unique coordinates Y a+B0 b, and Alpha reads K a. Consequently
+ker Alpha=im B0 on W^12 for every D-module W. Since all nuisance columns lie
+in ker Alpha and B0 consists of nuisance columns, im B=im B0.
+
+Two eligible states h,h' can yield a common U readout after choosing independent
+nuisance values exactly when U0(h-h')=0. Every exactly recoverable function of h
+therefore factors through the four displayed quantities U0 h. Conversely they
+are read directly by Alpha. This proves the quotient description over D-modules,
+not only a dimension statement over Q. For nonlinear H-only recoding S, replace
+U0 h by U0 S(h); no four-scalar information-capacity bound follows for unrestricted
+nonlinear encodings. The later zero-block obstruction below remains unchanged.
+
+## No fresh nonlinear recovery on the later words
+
+Write the entrance tuple as (h,z), with h on H and z on L minus H. For every
+later word the complete U observation is
+
+    y = M[U,H] h + M[U,L minus H] z = B z.
+
+Fix z and vary h arbitrarily. The observation remains identical. Any function
+of h exactly determined by this observation for every independent entrance tuple
+must therefore be constant. This argument also permits an arbitrary H-only
+entrance recoding S(h), because the coefficient of S(h) is still zero. No
+statistical distribution or information-theoretic entropy assumption is needed.
+Ancillas may be fixed or jointly independent of the entrance tuple; data-bearing
+side observations are outside the contract. The unit minors independently
+certify nuisance saturation but are not needed for the stronger zero-block step.
+
+The conclusion holds for every D-module and every allowed representation of the
+formal warps, since zero formal coefficients specialize to zero operators. It
+does not require freeness of the specialized native operators.
+
+A finite appended computation inherits this conclusion if every data and control
+dependency is explicit, frame inclusions are monotone, its output identities and
+frames are fixed, and it uses no new warp resets or additional source, target or
+earlier-snapshot reads. Every initial register in the causal cone of an output
+at V45 must have terminal frame contained in V45. Therefore that output depends
+only on R(V45), a subset of U, and independent ancillas. Arbitrary nonlinear
+local gates and additional intermediate buffers cannot supply missing h
+information. Pooling incomparable endpoints or changing the middle is not covered.
+
+## Paired rank is a separate condition
+
+For a fixed observation set, define the scalar left space by alpha M supported
+on H, and the scalar right space by M v supported on that set with v supported
+on H. Pair them using alpha M v. The reported dimensions are exact rational
+formal-space dimensions with explicit witnesses, not a universal native-cost
+claim. A zero pairing alone would not establish the nonlinear result above:
+for M(h,z)=(h,h+z), observing the first coordinate recovers h, although
+M^{-1} e_1=(1,-1) is not supported on H. Here the complete zero eligible block,
+not the absence of a normalized pair by itself, establishes the obstruction.
+
+## Complete-cost decision
+
+The four directions and their V45 endpoint saving already occur in PR2979.
+They cannot be counted again. The published frozen-owner audit PR3014 also
+shows that the local V45 saving can lose after idle capacity is charged; that
+existing result is credited, not presented as a new calculation here.
+
+The accompanying exact cost certificate derives a marginal screen in PR2979's
+fixed bin-capacity relaxation. At its rational complex parameter b0, use
+H_r(b0)=r(73/r)^b0. One freed width unit raises the optimal fractional idle bill
+per call by
+
+    D(b0) = (H_48(b0) - H_3(b0) - 5 H_5(b0))/20.
+
+The checker solves the retained basis with exact rationals, verifies nonnegative
+changed counts, and checks every feasible pattern against the dual with rigorous
+rational tariff intervals. Thus it proves the marginal at b0 for the specified
+single-helper inventory changes; it does not assert that the basis stays optimal
+for all parameters.
+
+For a hypothetical new 9-to-7 helper with local difference E - 2 H_1, the best
+fractional local-plus-idle difference is E - 2(H_1-D). This leaves approximately
+0.0246870954232 tariff units per call for E. The finite literal comparator has a
+small additional fractional slack, explicitly certified in the receipt. This is
+a necessary screen within the fixed-capacity model; it does not pay new private
+buffers, the actual paired residual T_out T_in^-1, physical access, precision,
+stock or a changed compiler interface. Those
+must be constructed and charged before any positive supplier claim.
+
+The bounded comparison finds no unused direction in U on PR2979. It therefore
+does not nominate a new extraction to send through owner/native/outer admission.
+A cheaper realization of the four existing directions is not excluded. The
+observed-row equality does not provide new compensation identities or a strict
+paid advantage for moving extraction earlier through other stages. PR2942
+already reports optimization of extraction order within its fixed gate-order,
+end-of-restore model; that historical result is not a global optimum for PR2979.
+
+The stopping decision is specific: adding a decoder or an H-only recoding on
+this frozen observation contract cannot produce a fresh V45 helper. Changes to
+the middle, cut or accessible coordinates remain possible, but require a new
+mathematical and cost argument. No improved kappa or global optimality follows.
+
+## Evidence boundary
+
+This is an exact finite comparison plus written proofs for all entrance values
+and allowed finite suffixes. Two separately implemented operator propagations
+check the observation claims. The cost arithmetic reuses the credited retained
+rational interval kernel. No formal proof assistant, independent human review,
+new native supplier, complete physical invoice or all-size multiplication theorem
+is claimed.

research/v45-recovery-transfer/README.md

@@ -0,0 +1,164 @@
+# V45 recovery was already present, and its four directions are already used
+
+The bounded comparison finds **no new fully costed improvement to PR2979**.
+It identifies exactly why the proposed information-recovery route stops:
+
+* The same four paired directions are already present on twelve named registers
+  of PR2894 and PR2917. Their complete readout maps are identical.
+* Those registers are not available at V45 in either shipped literal frame
+  schedule. The later paid frame and boundary changes supply access.
+* After the four PR2942 extractions, every coefficient from a fresh eligible
+  input vanishes from that twelve-register readout. PR2979 retains this exact
+  map. The four observable helper coordinates are already restored/protected.
+
+Thus the construction did not create four new algebraic information directions.
+It made existing ones usable and then consumed their eligibility. Nonlinear
+postprocessing or eligible-only entrance recoding cannot expose a fifth fresh
+helper through this fixed readout. Cheaper implementations of the existing four,
+changed middle circuits and other observation cuts remain open.
+
+This package adds the exact before/after transfer and its nonlinear consequence,
+plus a fixed-target fractional cost screen. It does not repeat the prior pairing
+census or claim the existing V45 construction as new.
+
+## Exact comparison
+
+For both base and extra providers, let
+
+```text
+V45 = span_F2(256,128,64,35,16,11,5)
+U12 = {2,61,62,63,70,71,72,94,249,251,265,267}
+P4  = {249,251,265,267}
+```
+
+H is the actual eligible-input set after the prelude, excluding restored,
+nonzero-frame entrance and initial-correction-source coordinates. U12 is a
+specified algebraic observation allowance; it is not asserted to be the complete
+set accessible under arbitrary frame refits. Literal supports include protected
+and restored registers as well as eligible ones.
+
+| Word | Eligible inputs | Literal V45 readout | Recoverable fresh directions on U12 |
+|---|---:|---:|---:|
+| PR2894 | 226 | 0 rows | 4 |
+| PR2917 | 216 | 0 rows | 4 |
+| PR2942 | 212 | 0 rows | 0 |
+| PR2979 stage 1 | 212 | all 12 rows | 0 |
+| PR2979 final | 207 | 10 rows, omitting 61 and 63 | 0 |
+
+All 98 scalar coefficients of the old U12 map agree between PR2894 and PR2917.
+All 42 coefficients of the later map agree across PR2942, stage 1 and final.
+The old four-dimensional pairing has determinant -128; eight nuisance directions
+and the four observable directions have a square completion of determinant 256.
+These dyadic units give the exact four-quantity observation quotient over every
+Z[1/2]-module, as detailed in [PROOF.md](PROOF.md).
+
+On each later word, the eligible block is exactly zero. The complete U12 nuisance
+minor has determinant 2; the final ten-row literal minor has determinant 1.
+Reclassifying P4 as eligible solely as a control recovers precisely their four
+identity coordinates. It does not make them new resources.
+
+The nonlinear obstruction also covers finite appended computations at V45 with
+fixed output identities and a fixed complete dependency graph, monotone frames,
+independent ancillas, and no new warp resets or source/target/earlier-snapshot
+reads. It does not cover combining incomparable endpoints. The input cut and
+inherited center-cut frame convention are explicit in the proof.
+
+## Cost and stopping decision
+
+The existing V45 local saving is already included in PR2979. [PR3014][3014]
+previously proved that retaining PR2942's owner assignment makes that local
+saving lose after idle children are charged. PR2979 uses a changed allocation;
+we do not transfer the frozen-owner negative to it.
+
+The new cost calculation binds PR2979's actual final inventory, complete profile,
+and fixed-bin relaxation. At its rational complex parameter
+`b0=0.001729033982646513517717`, write `H_r=r*(73/r)^b0`. An exact basis/dual
+calculation over all 2,551 patterns gives the optimal fractional idle charge per
+freed helper width:
+
+```text
+D = (H48 - H3 - 5 H5)/20
+```
+
+For one hypothetical fresh 9-to-7 extraction with actual local change
+`E - 2H1`, the best fractional local-plus-idle difference is
+`E - 2(H1-D)`. Only approximately **0.0246870954232** tariff units per call
+remain for E. The old literal allocation has an additional fractional slack of
+about **0.0000367672400** per call; the receipt gives rigorous rational intervals.
+The dual has 12 identically tight patterns and 2,539 strictly positive ones.
+
+This screen includes the optimal fractional idle adjustment in the stated bin
+model. It is not a completed physical invoice: new private buffers, chronological
+owners, native access, stock, precision and outer admission must still be paid.
+A favorable screen alone cannot certify a new supplier. Existing packing-only
+follow-ups already address the old cap gap.
+
+The comparison yields no unused direction in U12 on PR2979, so no new candidate
+reaches the allocation/native/admission stage. We stop this fresh-helper route.
+It does not establish global optimality of the existing four-direction circuit.
+
+## Reproduce and evidence
+
+Standard library, Python 3.12:
+
+```sh
+python3.12 scripts/research_package.py --package research/v45-recovery-transfer
+python3 scripts/check_research_commit.py --package research/v45-recovery-transfer
+```
+
+[EXPECTED.json](EXPECTED.json) records complete readout coefficients, eligibility,
+terminal frames, left/right bases, pairing matrices and dyadic-unit witnesses.
+[RESULT.json](RESULT.json) records the independent checker and exact cost screen.
+[VALIDATION.md](VALIDATION.md) states executed checks and review boundaries.
+
+The primary forward engine is the authenticated PR2918 implementation, credited
+and reused unchanged. A separately implemented backward-covector/inverse-column
+checker imports no predecessor Python and checks every readout coefficient and
+basis witness. Both use exact rational arithmetic. The cost basis/dual code is
+separate from the predecessor optimizer but uses its authenticated rational
+logarithm/exponential enclosure kernel. Neither implementation is a formal-kernel
+proof or independent human review.
+
+## Sources, overlap and credit
+
+Canonical base: `997e6a9ca7b4f95d50e366f61412fd640d72a88a`, priority revision 6.
+Scientific heads:
+
+| Source | Exact head |
+|---|---|
+| PR2894, Jeremy Kothe | `18d03c447886895ef9abf888398178e0428533ca` |
+| PR2917, Mason Hale | `224bd5e56041c40078ff6b5fa7393733a215de5c` |
+| PR2942, Marius-Paul Dumitrean | `a027b0f6fdb0ab2b42ba10fc31b53960166bf2bf` |
+| PR2979, Marius-Paul Dumitrean | `be191346391661f4d35fc0d1508d0a6029572576` |
+| PR3172, preceding obstruction | `0a632b00ef59a9f43b1f6c7965ff1ca7a3f188f3` |
+
+The mathematical methods retain Jeremy Diviney's PR2908 paired extraction,
+Jeremy Kothe's word/frame/cleanup construction, Mason Hale's extension,
+Marius-Paul Dumitrean's coordinated V45 construction and tariff kernel, and
+Ross Richardson's PR2918/3172 obstruction. The complete owner/native lineage
+retains Yiyang Lu, Tekalign, icekylinx, Dugongue, themilkman216 and the contributors
+credited by the frozen packages. Nick Petalas's V45 frame/native/invoice audits
+and jwr404's PR3112/3119/3126 audits delimit existing coverage.
+
+PR2979 already reports rank-four V45 pairing in a solver-lowered search model.
+Its exploratory script imports absent local `synth`/`lower` modules; we do not
+claim to replay that search. The independent literal-support calculation and
+fixed U12 map comparison here avoid that dependency. No frozen source is edited
+or re-vendored. PR3133/3148 and the separate active whole-word investigation are
+outside this bounded comparison.
+
+New work by Ross Richardson with substantial OpenAI Codex assistance, including
+separately assigned mathematical, source, cost and verifier reviewers. Apache-2.0.
+The underlying quotient and linear-programming principles are standard.
+
+## Open next questions
+
+A useful positive continuation must name a changed middle, observation cut or
+implementation of the four already-used directions. Its first step is an exact
+before/after program and full local histogram that passes the applicable cost
+screen while preserving compensation and restoration. The current zero block
+will not price or validate that changed program. Repeating nonlinear decoding
+on unchanged U12, or recounting the four existing helpers, cannot reopen this
+route. See [TASK.json](TASK.json) for the bounded handoff and blockers.
+
+[3014]: https://github.com/CrocSwap/integer-mult-bounds/pull/3014