Screen recursive cost edits and certify centre-exchange headroom

CONTRIBUTING.md

@@ -63,6 +63,12 @@ For a parameter improvement, supply exact rational choices, the full dependency
 argument, and an updated patch against the pinned source. Explain whether the
 change stays within the parameter ceiling or changes one of its hypotheses.
 
+Before extending a recursive cost edit, compare its complete paid and target
+histograms with the [signed invoice preflight](docs/research/recursive-invoice-preflight.md).
+It can certify uniform concave-moment gains or losses without a root search.
+Its accounting contract is declared; source correctness and supplier admission
+still require their own evidence.
+
 Keep `upstream/`, frozen source archives and pinned evidence unchanged. When
 changing generated artifacts, edit their generators and include the regenerated
 certificates and patches in the same change. Run the checks affected by your

docs/research/recursive-invoice-preflight.md

@@ -0,0 +1,108 @@
+# Compare the complete recursive invoice before extending a construction
+
+The same local edit can save scalar instructions while worsening its recursive
+bill. Conversely, owning a helper can remove paid work while also surrendering
+a productive target. Compare **both** paid jobs and target credits first:
+
+```sh
+python3 -B scripts/compare_recursive_invoices.py OLD.json NEW.json
+```
+
+This standard-library tool uses integer arithmetic, without a root search or
+contribution replay. It reports an exact certificate for every increasing
+concave rank tariff with f(0)=0, including r^(1-C), 0<C<1. The method is classical
+concave order, already used by mightyOil's
+[T16 audit](../../research/t16-moment-order-audit/README.md) and its predecessors.
+The shared interface adds signed target accounting; it is not a new theorem.
+The concurrent [source-bound pricing oracle #5391](https://github.com/CrocSwap/integer-mult-bounds/pull/5391)
+checks compatibility of reviewed physical, invoice, closure and funding receipts.
+This comparator is an earlier arithmetic screen, not a replacement for that
+evidence join or its trusted policies.
+
+## Input and meaning
+
+Both files use this schema, with identical declared accounting contracts:
+
+```json
+{
+  "schema": "integer-mult-recursive-invoice/v1",
+  "contract": {
+    "model": "mixed-target-unnormalized-power-v1",
+    "rank_semantics": "H_r costs r^(1-C); debit surrendered productive fields",
+    "ambient_rank": 145,
+    "boundary": "complete unit before the same mixed-target compiler"
+  },
+  "paid": {"1": 1, "8": 1},
+  "targets": {"9": 1}
+}
+```
+
+Ranks are canonical positive integer strings; counts are nonnegative integers.
+The contract identifies the common pricing and consumer boundary. A change in
+ownership can change targets inside that boundary, but requires its own legal
+construction and complete debit. Different rank meanings, normalization rules
+or transfer contracts require a separately justified comparison. Matching text
+does not prove applicability.
+
+The tool hashes the exact input bytes. It does **not** derive the invoice from
+a circuit, detect an omitted target debit, or authenticate an author's source
+claim. Keep the source word, extraction command and exact head with the invoice.
+The [worked package](../../research/owned-relation-exhaustion/README.md)
+independently reconstructs its complete source invoice before comparing it.
+
+| Result | What it establishes | Next action |
+|---|---|---|
+| `uniformly_worse` | Larger paid-minus-target cost for every power 0<t<1. | Stop this raw-moment improvement claim; identify a changed charge or contract before expanding it. |
+| `equal` | Identical net raw moment at every rank tariff. | Report scalar/compiler/implementation gains separately. Same invoice can still improve a funded compiler endpoint. |
+| `uniformly_better` | Smaller paid-minus-target cost for every power 0<t<1. | Price the complete candidate and prove its source, ownership, phase and caller obligations. |
+| `inconclusive` | Concave order does not decide the comparison. | Use a scoped exact power-moment calculation; mixed signs alone establish no crossing or failure. |
+
+For general concave tariffs the order is weak: a linear tariff can give equality.
+The strict power conclusion requires a nonzero signed difference. These results
+do not imply circuit equivalence, an admitted supplier or a compiler endpoint.
+
+## Recent discriminating examples
+
+* [#5350](https://github.com/CrocSwap/integer-mult-bounds/pull/5350): the filtered
+  151-ADD compression preserves the recursive invoice. Its unfiltered variant
+  splits one H4 into two H2 jobs, a strict loss for every 0<t<1. Scalar event count
+  alone chooses the wrong variant.
+* [#5377](https://github.com/CrocSwap/integer-mult-bounds/pull/5377) and
+  [#5383](https://github.com/CrocSwap/integer-mult-bounds/pull/5383): removing H1+H8
+  and debiting H9 gives a strict gain, 1+8^t-9^t>0. Leaving the H9 target credited
+  produces a much larger, unsupported budget.
+* [#5387](https://github.com/CrocSwap/integer-mult-bounds/pull/5387) and
+  [#5390](https://github.com/CrocSwap/integer-mult-bounds/pull/5390): compiler
+  refinements retain the same recursive invoice. #5390 also reports a smaller
+  sufficient compiler at a matched exponent. `equal` is therefore not a reason
+  to dismiss a compiler or implementation contribution.
+
+Run the source-bound current examples:
+
+```sh
+python3 -B scripts/compare_recursive_invoices.py \
+  research/owned-relation-exhaustion/examples/source.json \
+  research/owned-relation-exhaustion/examples/exchange-128.json
+python3 -B scripts/compare_recursive_invoices.py \
+  research/owned-relation-exhaustion/examples/source.json \
+  research/owned-relation-exhaustion/examples/h4-split.json
+```
+
+The second is a declared single-H4 edit to the complete source invoice, illustrating
+the unfiltered retiming's algebra; it is not a newly emitted physical supplier.
+
+## Certificate and bounds
+
+Set d_r=Δpaid_r-Δtargets_r. The report gives K(k)=Σ d_r min(r,k) at every support
+breakpoint. Between breakpoints K is linear. If all K are nonnegative, every
+increasing concave cost change is nonnegative; reversing the signs gives the
+reverse order. The discrete-slope proof is in the script and the worked package.
+No equal-rank-mass assumption is required.
+
+Inputs are bounded to 1 MiB, 4,096 keys per histogram, ranks at most 10^9 and counts
+at most 10^60. The implementation sweeps sparse support; it does not allocate an
+array of ambient width. Duplicate keys, floats, booleans and differing contracts
+fail with a diagnostic and exit code 2. Valid comparisons, including inconclusive
+ones, exit 0: this is an arithmetic report, not an automatic acceptance gate.
+
+Prepared for zxv with substantial OpenAI Codex assistance. Apache-2.0.

research/owned-relation-exhaustion/.gitattributes

@@ -0,0 +1,4 @@
+# Preserve exact retained source exports, including original line endings.
+source/** -text
+WITNESS.json -text
+source/INVOICE.json whitespace=cr-at-eol

research/owned-relation-exhaustion/PROOF.md

@@ -0,0 +1,128 @@
+# Signed invoice order and the fixed centre-exchange ceiling
+
+## 1. The reusable order certificate
+
+Let d_r=(P'_r-P_r)-(T'_r-T_r), with finite positive integer rank support and signed
+integer coefficients. Put K(k)=Σ_r d_r min(r,k). For an increasing concave tariff
+f with f(0)=0 and largest rank R, write s_j=f(j)-f(j-1). Direct telescoping gives
+
+    Σ_r d_r f(r) = s_R K(R) + Σ_{k=1}^{R-1} (s_k-s_{k+1}) K(k).
+
+All coefficients are nonnegative. Thus nonnegative K means no improvement in
+paid-minus-target cost; nonpositive K means no worsening. Conversely, each
+min(r,k) is an allowed tariff, so these signs characterize the whole tariff
+class. K is linear between support breakpoints, including the segment from zero
+to the first breakpoint. Checking just the reported knots is sufficient.
+
+For f(r)=r^t, 0<t<1, s_R>0 and every curvature coefficient is positive. A nonzero
+one-sided K therefore gives a strict sign. If every K vanishes, d vanishes.
+Unequal rank mass is allowed; K(R) explicitly carries its linear contribution.
+This is classical concave order, not a new theorem. mightyOil's retained T16
+audit supplies the closely related equal-mass predecessor implementation.
+
+Two useful controls have equal rank mass but opposite strict signs:
+
+* H4→2H2 gives d_2=2,d_4=-1, K(2)=2,K(4)=0: uniformly worse.
+* Remove paid H1+H8 and target H9: d_1=d_8=-1,d_9=1, K(1)=K(8)=-1,K(9)=0:
+  uniformly better. For powers, the margin gain is g(C)=1+8^(1-C)-9^(1-C)>0.
+
+## 2. Exact current-source inventory and exchange family
+
+The retained final #4610 word has 3,298 paid events per orientation, including
+exactly eight H8 centre events and no other H8 paid events. The retained p16/a7
+controller has sixteen backward and two forward local invocations: 144 original
+centre slots. `source_invoice()` separately rebuilds the complete paid histogram
+and targets from this word and controller, including copied queries, whole idles,
+all helper endpoints and main diagonal outputs. It agrees exactly with the
+final source invoice. Its rank surplus is 752.
+
+Define the following restricted optimistic family, for integers 0≤k≤144:
+
+    P(k) = P(0) - k H1 - k H8
+    T(k) = T(0) - k H9.
+
+There is at most one exchange per original centre slot and **all other recursive
+charges and target credits remain fixed**. Giving every exchange free preparation,
+storage, copying and completion only favors it. A scalar basis choice or schedule
+cannot create a 145th original centre slot within this definition. No assumption
+is made that all 144 exchanges have a physical realization.
+
+The margin is M_k(C)=Σ_r(T_r(k)-P_r(k))r^(1-C). By strict concavity,
+M_k(C)=M_0(C)+k g(C), with g(C)>0 for 0<C<1. Therefore M_144 dominates this entire
+family. The raw-root brackets proved by directed rational intervals are:
+
+| Exchanges | Complete raw crossing |
+|---|---|
+| 0 | (.00302177587077, .00302177587078) |
+| 16, #5377 bill | (.00302238736347, .00302238736348) |
+| 128, #5383/#5387 bill | (.00302667476807, .00302667476808) |
+| 144, optimistic whole-family maximum | (.00302728824993, .00302728824994) |
+
+Consequently the remaining **raw** gain above the 128-exchange crossing is less
+than .00000061348187. Even the all-144 margin at C=.0034 is below -91.8985594569.
+The #5387 claimed endpoint .003026674765 is within .00000000000308 of the
+128-exchange raw upper bracket. These are ceilings on this recursive invoice,
+not supplier admissions or a claim that every compiler achieves its raw root.
+
+`budget.py` proves strict decrease on [0,.01] by bounding the derivative
+Σ_r(P_r-T_r)log(r)r^(1-C) throughout that interval, not just at sample points.
+Each root has strictly positive and negative directed margins at its bracket
+endpoints. A 1,024-cell directed interval cover proves M_144<0 on [.01,1]. For
+each cell [a,b], it bounds targets at a and paid terms at b, using monotonicity
+of every power term. The largest upper bound is below -1,134. Thus there is no
+later positive window; the brackets give global raw ceilings for 0<C<1 in the
+stated family. Other k are dominated by 144.
+
+Every endpoint is rational. Logarithms use range reduction to [1,2] and the
+positive atanh series with an explicit geometric tail; exponentials use Taylor
+series, a geometric tail and repeated squaring. Integer endpoints round
+outwards at scale 10^50. Exact integral and square-root cases calibrate the
+implementation. This is an independently written arithmetic engine, not reuse
+of the predecessor's pricing code. The classical interval formulas are shared.
+
+## 3. Independent fixed-eight formal-row census
+
+The eight entry relations and their first physical realization are Ali Romman's
+#5383. Exact rational row reduction gives pivots
+225,227,229,230,241,245,257,288. Substitution leaves the 224 main inputs and all
+nonpivot helper inputs independent. The census walks every source event in
+both orientations, checks its frame progression and paid rank, and follows
+the retained scalar-row convention: paid inclusion changes the frame, while
+native warp symbols act on the row and cancel only adjacent inverse pairs.
+
+At every boundary it records a nonzero row's exact physical frame identifier
+and rational projective normal form. Every historical row is retained without
+charging slots or enforcing liveness. This favors possible snapshot reuse.
+Before each paid job it checks whether the row is zero or proportional to any
+earlier row already in that job's output frame. Since the source event list is
+finite and every boundary is visited, the census is exhaustive in this grammar.
+
+| Orientation / entry contract | Paid jobs | Zero rows | Proportional single-snapshot matches |
+|---|---:|---:|---:|
+| Forward / original inputs | 3,298 | 0 | 0 |
+| Backward / exact eight relations | 3,298 | 8 | 8 |
+
+All eight nonzero matches are precisely the previously supplied centre
+witnesses, each unique with factor +1. All zero jobs are the supplied later
+climbs. Relations of the same span give the same quotient regardless of basis.
+Wrong relation sign, a dropped actual ADD and a wrong snapshot sign fail.
+
+This is a **formal-row** absence result, not a proof of physical operator
+inequality. Concrete native operators obey further identities; this traversal
+uses only the retained free reduction. It also excludes arbitrary linear
+combinations of saved rows, changed scalar programs, extra entry relations,
+new preparations, alternate frame equivalences and different caller boundaries.
+It does not itself verify the physical construction's phase or erasure ABI.
+
+## 4. Scope and reopening conditions
+
+The budget and census have different scopes. The exchange ceiling allows any
+basis or schedule that keeps exactly the declared complete invoice family; the
+census fixes the eight relations and unchanged source event history, regardless
+of whether a proposed edit has that invoice. Neither implies that all productive
+helper ideas are exhausted. Removing different ranks, surrendering different
+targets, using scalar combinations or native relations, changing contact heights,
+or changing the controller requires a fresh complete signed bill and proof.
+The selected construction and its five framework assumptions are unchanged.
+
+Prepared for zxv with substantial OpenAI Codex assistance. Apache-2.0.