Close fixed-source BIT price gates and a permutation rank floor

research/bit-fixed-source-price-gates/PROOF.md

@@ -0,0 +1,180 @@
+# Two fixed-source BIT price gates
+
+These are two separate applications of complete paid and target accounting.
+Neither gives a new supplier or a multiplication kappa value.
+
+## 1. Fresh commuting axes on the fixed PR589 word
+
+Fix the original scalar events, native frame paths, and owned operations.
+All free maps act as the identity on the added axes. The main boundaries and
+all target credits outside the selected helper set stay unchanged. A field
+state can carry any subset of the new commuting axes. Scalar contacts must
+have the same subset. A native MOVE with original rank r and a change of s
+new axes has rank r+s; this direct-sum charge is part of the lift contract.
+
+Choose a nonempty set of helpers and add k>0 fresh commuting axes to each
+chosen final helper job. The physical k is an integer. The original helper
+job has rank eight. Each chosen helper starts with no new axis and ends with
+k new axes. Along its own register path, let s_j count the changed new axes
+at MOVE j. Every final axis must change at least once, so sum_j s_j>=k.
+Scalar events cannot make this change. An owned COPY does not change its
+persistent source register.
+
+The exact source census shows that every helper has a paid MOVE and that
+every such MOVE has original rank r_j<=7. Different persistent helper paths
+use distinct MOVE events. For f(r)=r^(1-C), 0<C<1, define
+
+    g(s)=f(7+s)-f(7).
+
+The function g is increasing and concave, with g(0)=0. It is subadditive:
+g(a)+g(b)>=g(a+b). This follows by writing each increment as an integral of
+the decreasing derivative of f. Hence the paid increment on one helper path
+is at least
+
+    sum_j [f(r_j+s_j)-f(r_j)]
+      >= sum_j g(s_j)
+      >= g(sum_j s_j)
+      >= g(k)
+      > f(8+k)-f(8).
+
+The final strict inequality follows from strict concavity and 7<8. This is
+larger than the new helper target credit. Distinct helper paths give distinct
+charges. Further copied fields and boundary work have nonnegative cost.
+Every nonempty choice loses. The same proof permits different positive k
+values on different chosen helpers.
+
+Reversing the source leaves each helper's own MOVE ranks unchanged. The BIT
+rank-eight helper job is an involution, so the same target rank and argument
+apply in the reverse direction. The verifier checks the two rank censuses;
+it does not claim a new native reverse-word replay.
+
+This proof fixes the original word and its contact rules. It does not cover
+new scalar operations, status-changing free maps, different output jobs,
+preloaded added-axis status, shared persistent ownership, or a different
+native operation. No mincut computation is needed for the theorem.
+
+## 2. The retained paired-k3 p12 source
+
+Fix the paired-triple geometry parameter at 12. The retained generator and
+frozen matching give h=24, v=1760, R=19788 and centre debt c=528. Let L_r be
+the complete local paid histogram, including both main boundary legs. Let
+H=R H24 be the complete local helper target list. The source compiler gives
+
+    sum_r r L_r - 24 R = 2 v (24-1) + 528.
+
+The verifier reconstructs L from the unchanged generator, checks the scalar
+decoder, and includes its target-side main legs and source-side main legs.
+Each main side has rank mass v(24-1). No productive helper is made free or
+credited twice. The retained compiler's modular-rank argument and native
+invoice convention are inherited; this is not a new native admission proof.
+The predecessor's standalone independent `check_paired_cube_bit.py` is not
+rerun. The tariff conclusion applies to the reconstructed generator invoice.
+
+Let p>=1 now denote the balanced controller parameter, not the geometry
+parameter. Put d=23 and let a=floor((p-1)/2), b=p-1-a. Its paid list is
+
+    (p+2)L + v(p-1)H1
+    + 2v sum_(s in {a,b}) sum_(j=1)^s H_(d(j+1)).
+
+Its target list is
+
+    (p+2)R H24 + 2v H_(1+d(p+2))
+    + 2v sum_(s in {a,b}) sum_(j=1)^s H_(1+d(j+1)).
+
+The exact target rank minus paid rank is 1232p+704. This positive rank
+surplus is not enough to obtain a useful exponent.
+
+Set C=1/500 and t=1-C. Let delta be the local paid moment minus local helper
+moment, and let M(p) be the complete target moment minus paid moment. Each
+side pair contributes at most one unit before multiplication by 2v:
+
+    (x+1)^t-x^t <= 1.
+
+There are p-1 such pairs. Subtracting the thin calls gives
+
+    M(p) <= U(p)
+    U(p) = -(p+2)delta + v(p-1) + 2v(1+d(p+2))^t.
+
+The verifier uses exact rational enclosures from the retained positive-series
+engine. It proves M(p)<0 for p=1,...,64. It also proves U(64)<0 and U'(64)<0,
+using a lower enclosure for delta and upper enclosures for the positive
+endpoint terms. Since U''(p)<0, the derivative decreases. Therefore U(p)<0
+and M(p)<0 for every real p>=64. These checks cover every positive integer
+controller parameter.
+
+To interpret this as a raw-saving bound, normalize M by 24^t. Every local
+paid rank is less than 24, which the verifier checks. The normalized negative
+local term decreases with C. The normalized thin debit also decreases. The
+endpoint rank exceeds 24, so its normalized credit decreases with C. Every
+side pair has x>=46>24. The function
+
+    ((x+1)/24)^t-(x/24)^t
+
+increases with t>0: the derivative of y^t log y in y is positive for y>1.
+Hence each normalized side credit decreases with C. Thus M/24^t is strictly
+decreasing for 0<C<1. Since M(0)=1232p+704>0 and M(1/500)<0, the raw crossing
+for each p is strictly below 1/500.
+
+The retained p=11 crossing lies in
+
+    (0.00164539220, 0.00164539221).
+
+It is a positive sign-change control. This package does not claim that p=11
+is the global optimum. It performs no floating root search, matching search,
+or scan over other source geometries.
+
+This second gate fixes the p12 module, decoder, matching, full unnormalized
+invoice, and balanced caller. It does not cover a changed local recipe,
+partial-gauge optimization, another geometry parameter, or another caller.
+Its raw crossing is not the complete multiplication exponent.
+
+## Source-rank appendix: permutation-only completion
+
+This appendix bounds binary correction rank, not native factorization cost.
+Let J be the 111-by-111 noCOPY matrix in the pinned PR589-H-NATIVE source.
+The source factors A=J+I as U V, with rank nine. Thus U and V both have rank
+nine, and A and U have the same column code. The 511 nonzero words in this
+code all have weight at least 48. The verifier checks this exact
+code and its full weight distribution.
+
+Suppose a permutation matrix P had rank(J+P)<=8. Then
+
+    rank(P+I) <= rank(J+P)+rank(J+I) <= 17.
+
+A nontrivial permutation cycle of length l moves l rows and contributes
+l-1 to rank(P+I). Since l<=2(l-1) for l>=2, P can move at most 34 rows.
+Delete these moved rows from A. The remaining rows still have rank nine:
+a nonzero vector in the column code of U cannot be supported on only 34 rows,
+because its minimum weight is 48. On every remaining row P equals I, so J+P
+agrees with A there. Hence rank(J+P)>=9, a contradiction.
+
+The identity permutation attains rank nine. Thus
+
+    min_(P a permutation matrix) rank(J+P) = 9.
+
+The retained arbitrary-invertible completion changes three rows and yields
+an invertible output code. Its target code need not be a permutation. That
+rank-three construction does not contradict this permutation-only theorem.
+Conversely, this theorem gives no lower bound on the native cost of a new
+factorization, a general invertible output code, or a multi-call controller.
+The direct-sum plane price screen is not part of this appendix.
+
+## Exact evidence and controls
+
+RESULT.json contains outward rational enclosures, rounded by integer floor
+and ceiling to a denominator of 10^12. The verifier checks the unrounded
+exact signs first and checks that every displayed enclosure contains them.
+No floating-point value enters either gate.
+
+Ten live input files are pinned before external source code is loaded. The
+verifier executes those source bytes directly and does not use an inherited
+bytecode cache. Changed bytes in every source are rejected. It also rejects
+an own helper MOVE of rank eight, a helper without a paid path, a missing
+paid rank-one job, an unearned helper credit, and omission of the local gap
+from the analytic tail. The appendix rejects a changed decoder row and a
+zero-rank defect.
+
+These checks verify the stated source census, declared complete invoice, and
+price implications. They do not verify a common-cover supplier, full native
+payload, ordinary movement and precision budget, uniform compiler, or outer
+multiplication theorem.

research/bit-fixed-source-price-gates/README.md

@@ -0,0 +1,140 @@
+# Two complete fixed-source BIT price gates
+
+This package closes two price questions without another discovery search.
+For the fixed PR589 word, adding fresh commuting axes to any nonempty helper
+set loses for every positive axis count and every tariff r^(1-C), 0<C<1.
+For the retained paired-k3 p12 source in the balanced query-thinned caller,
+the raw saving is below 0.002 for every positive integer controller parameter.
+These are separate fixed-source scopes. Neither improves complete kappa.
+
+Read [the proofs](PROOF.md), [exact result](RESULT.json), and
+[source pins](SOURCES.json). The publication base is
+`32890bc5de034ab8fc93ac88ead7279a6a416d04`. All ten live inputs are pinned at
+that base. The original investigation used the same source bytes at
+`1ec1119972c9aefe42525172d07b332fcff81cb4`. The task catalogue and selected
+record are historical provenance; no frozen source or selected result changes.
+
+## Fixed helper-axis gate
+
+The actual PR589 source has 439 rank-eight helper jobs. Each helper has an
+own-register paid MOVE, and all such MOVEs have rank at most seven. A helper
+that acquires k fresh axes must change at least k axis statuses along its
+own paid path. Different helpers use distinct paths. Concavity and
+subadditivity of the rank increments make their paid cost larger than the
+rank-eight target increments they could fund. Partial axis sets are allowed. The result
+holds in either orientation of the fixed word.
+
+This fixes the source events, scalar contacts, free maps on the new axes,
+and all other target credits. It does not cover a changed source word,
+preloaded axes, another output contract, or a different native operation.
+The former mincut results are not needed and are not rerun.
+
+## Paired-triple gate
+
+The source geometry parameter stays at 12: h=24, v=1760, R=19788, and centre
+debt 528. The retained scalar decoder and rank compiler run on the frozen
+module and matching. Both main boundary legs and all productive helper
+credits are included. The caller parameter p is separate from this fixed
+geometry parameter.
+
+Exact rational calculations show negative complete margin at C=1/500 for
+p=1,...,64. A decreasing concave upper bound is already negative with
+negative derivative at 64, so it closes the entire remaining tail. A separate
+normalized-margin argument proves that each raw crossing is below 1/500.
+The retained p=11 bracket (0.00164539220,0.00164539221) is only a positive
+control; this package makes no global optimum claim.
+
+The rank compiler and its documented modular-rank argument are inherited.
+No new native lift, partial-gauge optimization, source-size search, caller
+construction, or ordinary supplier admission is supplied. The former floating
+root search is not rerun.
+
+## Separate source-rank appendix
+
+For the pinned PR589 noCOPY matrix J, the minimum of rank(J+P) over every
+permutation matrix P is exactly nine. The identity attains nine. The exact
+511-word defect code has minimum weight 48; a hypothetical rank-eight repair
+would let P move at most 34 rows, too few to remove a nonzero codeword.
+This is a binary correction-rank theorem. It is not a native-cost bound.
+
+The [retained arbitrary-invertible completion](https://github.com/CrocSwap/integer-mult-bounds/blob/32890bc5de034ab8fc93ac88ead7279a6a416d04/research/kappa-rebuild/bit/pr589_minimum_completion.py)
+uses a rank-three row repair and need not end in a permutation, so it is
+outside this appendix. [PR #673](https://github.com/CrocSwap/integer-mult-bounds/pull/673)
+prices dirty echo and restored role sharing, while
+[PR #1246](https://github.com/CrocSwap/integer-mult-bounds/pull/1246) implements
+paid nonzero reader-defect repair. Neither is the fixed J-to-permutation
+rank problem here. They are related contracts, not executable dependencies.
+
+## Reproduce
+
+Use Python 3.12 and the standard library. All executable source dependencies
+and their data files are declared in VERIFY.json.
+
+```sh
+python3 -B research/bit-fixed-source-price-gates/verify.py
+python3 -O -B research/bit-fixed-source-price-gates/verify.py
+python3 -B scripts/research_package.py --package research/bit-fixed-source-price-gates --check-only
+python3 -B scripts/research_package.py --package research/bit-fixed-source-price-gates
+```
+
+Expected direct output:
+
+```text
+PASS_BIT_FIXED_SOURCE_PRICE_GATES helper_axis=all_k_C paired_k3=all_controller_p source_controls=10 new_kappa=false
+```
+
+The direct verifier also works in the committed export without Git. It checks
+all ten source pins before it loads retained code. Normal and optimized runs
+must give identical exact reports. Five controls reject invalid source-rank,
+paid-path, target-credit, paid-charge and tail-gap assumptions. Mutating each
+live source is also rejected. Two appendix controls reject a changed
+decoder row and a zero-rank defect. No mincut, matching or root search runs.
+
+No native payload, complete cover, ordinary precision/movement budget,
+uniform compiler, or outer multiplication assembly is checked here. The
+predecessor's standalone independent `check_paired_cube_bit.py` is not rerun;
+the second gate prices the exact retained generator invoice.
+
+## Open next questions
+
+[TASK.json](TASK.json) records two distinct questions. A changed literal
+helper path could escape the first proof's fixed-word charge. A changed
+paired-cube recipe or caller could change the second complete invoice. In
+either case, first provide a concrete word and every target debit. Neither
+changed construction is supplied by this package.
+
+## Credit and nearby contracts
+
+The first source is the retained
+[PR #589](https://github.com/CrocSwap/integer-mult-bounds/pull/589) and
+[PR #555](https://github.com/CrocSwap/integer-mult-bounds/pull/555) word. Its
+[pinned source notice](https://github.com/CrocSwap/integer-mult-bounds/blob/32890bc5de034ab8fc93ac88ead7279a6a416d04/research/e8-bit-p111-tuned/NOTICE.md)
+credits eumemic with substantial Anthropic Claude assistance and lists its
+earlier contributors.
+
+The second source is the retained fast paired-cube generator. Its
+[SOURCE.json](https://github.com/CrocSwap/integer-mult-bounds/blob/32890bc5de034ab8fc93ac88ead7279a6a416d04/research/paired-cube-bit-fast/SOURCE.json)
+pins the [PR #168](https://github.com/CrocSwap/integer-mult-bounds/pull/168)
+lineage and frozen p12 data. Its frame and gauge ledger retains
+[PR #144](https://github.com/CrocSwap/integer-mult-bounds/pull/144) credit.
+The [exact series engine](https://github.com/CrocSwap/integer-mult-bounds/blob/32890bc5de034ab8fc93ac88ead7279a6a416d04/research/bit-compact-productive-controller/exact_series.py)
+comes from ai-nanachi's compact productive BIT package. Cinna Davis's query-thinned
+controller lineage is credited in that package's
+[README](https://github.com/CrocSwap/integer-mult-bounds/blob/32890bc5de034ab8fc93ac88ead7279a6a416d04/research/bit-compact-productive-controller/README.md).
+Concavity and the decreasing-derivative test are standard analysis; this
+contribution applies them to the complete pinned source invoices.
+
+Nearby work has different contracts.
+[PR #1931](https://github.com/CrocSwap/integer-mult-bounds/pull/1931) changes the
+source with an involutive E8 reflection and boundary repairs; it does not fix
+the source word and add commuting helper axes.
+[PR #1998](https://github.com/CrocSwap/integer-mult-bounds/pull/1998) decodes
+ordered paired dirty logs with specified intermediate observations; it is not
+the paired-triple geometry or its complete invoice.
+[PR #2376](https://github.com/CrocSwap/integer-mult-bounds/pull/2376) maps QQ16
+observation contracts and does not prove either price gate. These are scope
+comparisons, not executable dependencies.
+
+The source-bound proofs, checks, and packaging have substantial OpenAI Codex
+assistance. New files are Apache-2.0. Retained authors, notices and source files
+remain unchanged. This is author-side evidence, not independent human review.