Sharpen adaptive compiler width with multiplicative shell counts (no new kappa)

research/adaptive-shell-width/PROOF.md

@@ -0,0 +1,182 @@
+# Fixed-ratio semigroup shells and adaptive chronological width
+
+## 1. New shell lemma
+
+Fix a finite set A of positive integers and an integer M >= 2. Let Gamma be
+the multiplicative semigroup generated by A union {M}, including 1. Let Pi
+be its finite prime support, V the rational span of the prime-valuation
+vectors of the generators, and r=dim V. Since M is a generator, r>=1.
+For every integer ell>=0 there is an effective constant K, depending only
+on A and M, such that
+
+    |Gamma intersect [M^ell, M^(ell+1))| <= K (ell+1)^(r-1).       (1)
+
+This also holds for all positive integers supported on Pi whose valuation
+vectors belong to V, a possibly larger set than Gamma. No freeness or unique
+factorization into the given generators is assumed; ordinary prime
+factorization is used.
+
+Here is an explicit constant. Write m_i=v_(p_i)(M), choose p_0 dividing M,
+and put q=m_0>0 and h=ceil(log_2 M). For each i != 0 define the integer form
+
+    F_i(x) = q*x_i - m_i*x_0.
+
+The common kernel of all these forms in Q^Pi is exactly Q*m, where m is the
+valuation vector of M. Since m belongs to V, their restriction to V has
+rank r-1. Choose a subset I of r-1 forms independent on V. The restricted
+map F_I has kernel exactly Q*m: its kernel has dimension one and contains m.
+The empty set I is allowed when r=1. Set
+
+    K = q * product_(i in I) (h*(q+m_i)+1).                    (2)
+
+For a product u in the shell, its nonnegative integer valuation coordinates
+obey x_i <= h*(ell+1). Thus the integer F_i(x) lies in the inclusive interval
+[-m_i*h*(ell+1), q*h*(ell+1)]. There are at most
+(h*(q+m_i)+1)*(ell+1) possibilities for this coordinate. The number of
+possible F_I values is at most the product of these r-1 bounds.
+
+Fix one such value. For any two vectors x,y in its fiber, x-y=t*m for a
+rational t. Their associated positive integers u,v satisfy u/v=M^t, since
+prime factorization gives this equality over the positive reals. Both lie
+in the half-open interval [M^ell,M^(ell+1)), so -1<t<1. More precisely the
+whole fiber's x_0 coordinates lie in one half-open real interval of length
+q: log_M(u) is an affine function of x_0 with slope 1/q. Consequently this
+fiber contains at most q distinct integer x_0 values. Each such value
+determines x uniquely because the remaining difference t*m has t*q=0.
+Multiplying by the number of F_I values proves (1)-(2).
+
+The q factor cannot generally be dropped: with A={2}, M=4, r=1, both 1
+and 2 are in the first shell, and every shell contains exactly two powers
+of 2. Adjoining M before computing r is essential: A={6}, M=2 gives an
+augmented rank of two, not one. The shell then contains
+2^ell and 6*2^(ell-2) for ell>=2, with further distinct powers of 6 as ell
+grows. A fixed bound obtained by omitting the M direction is false.
+
+## 2. Exact compiler hypotheses and source boundary
+
+Apply the lemma to the **unchanged** adaptive chronological compiler of
+codyw912's PR4638, `research/adaptive-chronological-batching/batching.py`,
+`compile_widths`, and its `WIDTH.md` sections 1-4. The following are retained
+hypotheses/results of that package, not independently reproved here.
+
+* Fixed positive integer target multiplicities W_k and paid multiplicities
+  P_j, with 2<=k0=min(k)<=k<=m=max(k), 1<=j<=jmax<m, and a paid rank-one
+  position. Put W=sum W_k and P=sum P_j.
+* Fixed integers M>=2, g>=1 and ordinary cutoff n0>=m. The named executable
+  adaptive interface uses g=a+b with positive a,b, hence g>=2, and fixes
+  n0=m. The cases g=1 and arbitrary n0>=m belong to the inherited written
+  theorem, not this executable mode. Widths below n0 equal one.
+* At n>=n0, C_n=floor(n/m), ell(n)=floor(log_M C_n), G_n=g*ell(n).
+  All chronological classes are retained, including descendants of empty
+  parent classes. Sources are nonempty. Every upfront complementary batch
+  and every separate exit cut is retained; repeated cuts cannot pool counts.
+* With source count S_n and those batches (j,b), the actual recurrence is
+  a_n=lcm_(j,b)(B_j/gcd(B_j,b)) and B_n=S_n*a_n. Children strictly decrease.
+  Their integer decrement is at least min(C_n,k0^(G_n+1)).
+
+Let Gamma be generated by all target ranks, all paid ranks and M. Source
+counts are constant on its multiplicative plateaus; only their locations
+are counted by (1). Their prime factors need not be in Pi and are never
+discarded. At level ell, 1<=S(gamma)<=W*(W+P)^(g*ell).
+
+For N>=n0 let Lambda=floor(log_M floor(N/m)), and set
+
+    lo_ell = max(n0, m*M^ell)
+    hi_ell = min(N, m*M^(ell+1)-1)
+    delta_ell = min(M^ell, k0^(g*ell+1))
+    t_ell = 0                                      if hi_ell < lo_ell,
+            1+floor((hi_ell-lo_ell)/delta_ell)       otherwise.
+
+The inherited all-prime divisor is
+
+    B_n divides Q_N=product_(ell=0..Lambda) L_ell^t_ell,  0<=n<=N, (3)
+
+where L_ell is the LCM of all S(gamma) with M^ell<=gamma<M^(ell+1) and
+gamma<=floor(N/m). It arises by bounding, separately for every prime, the
+sum of source valuations along a decreasing child chain. Different primes
+may choose different chains. No common maximizing chain is required.
+
+The new result changes only the bound on the number J_ell of these plateau
+starts, replacing the predecessor's full prime box by
+
+    J_ell <= K*(ell+1)^(r-1).
+
+Here r is the augmented valuation rank from section 1. This directly
+answers Nick Petalas's PR5962 Open next question 1, which left the adaptive
+shell count and this level-LCM use open.
+
+## 3. Effective bit envelope and growth
+
+Let w=ceil(log_2 W) and v=ceil(log_2(W+P)). Equations (1)-(3) give the exact
+integer envelope
+
+    log_2 B_n <= K*sum_(ell=0..Lambda)
+                    t_ell*(ell+1)^(r-1)*(w+g*ell*v),  n<=N.     (4)
+
+Indeed log_2 L_ell is at most the sum of the logarithms of the source counts
+at its J_ell starts. This is a statement about the same B_n; no batching,
+source count, leaf count, selected frontier or compiler program is changed.
+
+Put z=max(0,1-g*log_M k0). If k0^g>=M, delta_ell=M^ell and
+ t_ell<=m*(M-1). Each summand in (4) is O((ell+1)^r), so
+
+    log B_N = O((1+log N)^(r+1))                    when z=0.    (5)
+
+If k0^g<M, set rho=M/k0^g>1, so z=log_M rho belongs to (0,1).
+The inherited integer level bound gives t_ell<=A+B*rho^ell for fixed A,B.
+Since rho^ell>=1, this is at most (A+B)*rho^ell. Thus, for fixed r>=1,
+
+    sum_(ell=0..Lambda) rho^ell*(ell+1)^r
+       <= (Lambda+1)^r * rho^(Lambda+1)/(rho-1).
+
+As rho^Lambda<=N^z and Lambda=O(log N), equation (4) yields
+
+    log B_N = O(N^z*(1+log N)^r)                    when z>0.    (6)
+
+All constants depend only on the fixed rule and height parameters. These
+statements are not uniform in varying M, g or rank alphabets. At z=0 the
+geometric estimate cannot be used with rho=1; retaining (5) avoids a false
+extra logarithmic saving at that boundary. The bounds need not be tight and
+the conservative K can be numerically large.
+
+## 4. Source-bound p16 consequence
+
+The immutable `rank-convergence/BENCHMARKS.json` p16 entry supplies M=1024,
+g=a+b=2 and names `compact-joint-compiler/arithmetic/RESULT.json`. Its exact
+histograms have m=145, k0=4, W=10928, P=64620 and paid rank one. The
+augmented prime support is {2,3,5,7,11,13,17,19,29,41,73}; its rational
+valuation rank is r=11 (the checker independently verifies a full-rank
+minor). Since 1024^2=4^(5*2), z=3/5 exactly.
+
+Consequently, under PR4638's retained recurrence hypotheses, this **named
+p16 adaptive compiler width** has the improved upper bound
+
+    log B_N = O(N^(3/5)*(1+log N)^11),
+
+in place of PR4638's O(N^(3/5)*(1+log N)^12). This is a bound on the same
+width sequence, not evidence of a smaller actual width or runtime. The
+scientific benchmark is historical and is not the selected PR6030 default
+strictified compiler. No new exponent of multiplication, native theorem,
+physical-memory claim or selected compiler-assumption discharge follows.
+
+## 5. Evidence and remaining assumptions
+
+The written argument proves the quantified shell lemma. Finite independent
+semigroup enumerations, exact fiber counts, independent rank checks and
+bounded applications of the actual `compile_widths` corroborate its bindings.
+They do not prove the inherited all-size native, ownership or compiler
+correctness assumptions. Both PR4638 and PR5962 were archived as partially
+reviewed; their publication is not independent scientific acceptance.
+
+Native arbitrary-input semantics, whole-job adapters, chronological flow
+correctness, owned erasure, physical allocation/routing/precision/tape costs,
+outer transfer and exact integer recovery remain outside this result. No
+full selected/historical replay or proof assistant is used.
+
+Prepared by JoyboyBrian with substantial OpenAI Codex assistance. Credit
+codyw912 for PR4638's adaptive cuts and divisor; Nick Petalas for PR5962's
+multiplicative-rank refinement and explicit question; Mihir Srivastava for
+PR4507/4586 batching and width work; zxv for PR4436/4483 flow and adaptive
+height; Jacob Alan Sussman for the integer compiler; Ryanson Jonathan,
+Cinna Davis and all retained native/compiler predecessors. Elementary prime
+factorization and rational linear algebra are not claimed as new.

research/adaptive-shell-width/README.md

@@ -0,0 +1,128 @@
+# Adaptive compiler width from multiplicative shells
+
+For a fixed target/paid rank alphabet, adjoin its height base M and let r
+be the rational rank of the prime-valuation vectors. This package proves
+an effective bound of K(ell+1)^(r-1) on the number of semigroup products in
+[M^ell,M^(ell+1)). It answers Open next question 1 of Nick Petalas's
+[PR5962](https://github.com/CrocSwap/integer-mult-bounds/pull/5962).
+
+Applied to the unchanged level-LCM divisor of codyw912's
+[PR4638](https://github.com/CrocSwap/integer-mult-bounds/pull/4638), it gives
+
+| Fixed adaptive regime | New upper bound for log B_N |
+| --- | --- |
+| z=max(0,1-g log_M k0)>0 | O(N^z (1+log N)^r) |
+| z=0 | O((1+log N)^(r+1)) |
+
+The historical p16 source has r=11 and z=3/5. Its bound improves from
+O(N^(3/5)(1+log N)^12) to O(N^(3/5)(1+log N)^11). **The compiler and its
+actual widths are unchanged.** This is a conditional compiler-size result,
+not a new multiplication exponent or a physical memory/runtime reduction.
+The effective constant can be large; it is an upper bound, not an optimum.
+
+[PROOF.md](PROOF.md) proves the shell lemma, states every inherited compiler
+hypothesis, derives an explicit integer bit envelope and separates z=0.
+The new shell argument uses r-1 integer forms whose common kernel is the
+height-base direction. Each fiber contributes at most v_p(M) points to a
+half-open shell. Ordinary prime factorization and linear algebra are not
+claimed as new; the source-bound shell and compiler application are the
+contribution.
+
+## Exact caller and predecessor scope
+
+The caller is `research/adaptive-chronological-batching/batching.py`:
+`compile_widths`, `batch_rows` and `multiplier`. The consumed theorem is
+that package's `WIDTH.md` sections 1-4. Its executable uses cutoff n0=m and
+positive a,b, hence g=a+b>=2. The general written theorem also permits
+n0>=m and g>=1; the executable fixtures do not claim those extra modes.
+The proof retains paid rank one, nonempty sources, every chronological cut,
+all source-count primes and the inherited child-decrement bound.
+
+The p16 binding reads the exact `rank-convergence/BENCHMARKS.json` entry
+and its named `compact-joint-compiler/arithmetic/RESULT.json`: m=145,
+k0=4, M=1024, g=2, W=10928, P=64620. An independent integer determinant
+of a full 11-by-11 valuation minor is -1. The relation
+1024^2=4^(5*2) verifies z=3/5 without floating point. The conservative shell
+constant used here is 1104622125411204510010.
+
+PR4638 head `385a4436a47ea8e80cc1503948fe7a36e1b1c5af` supplies the
+adaptive compiler and level-LCM theorem. PR5962 head
+`6f87acd840f31a092238ecf7e5c455289430878a` supplies the default-height
+multiplicative-rank result and this open question. Both are archived,
+partially reviewed sources; their scientific assumptions are used explicitly.
+Their original files are unchanged. SOURCES.json pins the retained bytes at
+base `721c03822c421b7f7fcbb2598993b947c4d88419`.
+
+## Bounded verification
+
+From the repository root with Python 3.12 and its standard library:
+
+```sh
+python3.12 -B scripts/research_package.py --package research/adaptive-shell-width
+python3.12 -I -W error -B research/adaptive-shell-width/verify.py
+python3.12 -I -O -W error -B research/adaptive-shell-width/verify.py
+```
+
+The direct checker is read-only and works in the official Git-free export.
+It authenticates all live inputs, then executes the authenticated standalone
+predecessor `batching.py` as the object under test. No predecessor scientific
+verifier or pricing engine is imported. The semigroup and rank oracles are
+independent of that source implementation.
+
+The first Python 3.12 run takes under one second and reports:
+
+- 372 generator/base fixtures, 21,754 member occurrences in 3,054 shells,
+  with 20,547 quotient fibers. Multiplicative closure agrees with an
+  independent integer-by-integer divisibility oracle. Small valuation ranks
+  agree with independent Leibniz minors.
+- Three unchanged executable compiler fixtures across both z regimes:
+  257 compiled ranks and 1,856 batch rows, including the height boundary at
+  cap 16. The all-prime level-LCM divisor divides every actual width, and
+  the new exact bit envelope bounds that divisor. Source plateau and child
+  decrement checks retain the actual caller boundary.
+- Ten rejecting source/domain/semantic controls: invalid bases/generators,
+  bad source bytes, missing fiber multiplicity, missing M direction or
+  quotient coordinate, closed shell endpoint, z=0 misuse and omitted paid
+  generator.
+
+Finite checks corroborate the written theorem and source bindings; they are
+not an all-size compiler or native proof. The caller fixtures are small
+abstract rules, while the p16 check binds the actual historical profile;
+no full p16 compiler is materialized. Validation contains no Python asserts.
+
+## Limits and next questions
+
+This is the alternative adaptive compiler, **not selected PR6030's default
+strictified compiler**. The selected result remains conditional kappa
+0.003125804 under all five assumptions. Native/all-column semantics,
+whole-job adapters, owned erasure, chronological correctness, physical
+allocation, routing, precision, tape costs, outer transfer and exact recovery
+are not discharged. No Lean, Docker or full selected/historical replay is run.
+Independent human and formal-kernel review are unclaimed.
+
+### Open next questions
+
+1. Can exact source valuations or a tighter shell constant improve a named
+   finite bound? Retain the actual per-level LCM and compare a proved tighter
+   quotient box; the present asymptotic improvement alone does not establish
+   a practical finite saving or a lower bound.
+2. Which physical resource bound can use this envelope? Bind an emitted
+   adaptive program to actual banks, routes and scratch before claiming any
+   memory or runtime reduction. These native and physical contracts remain
+   the blocker. TASK.json records the precise first steps and limitations.
+
+## Coordination and attribution
+
+Canonical claim: [Discussion6076](https://github.com/CrocSwap/integer-mult-bounds/discussions/6076).
+Base main `721c03822c421b7f7fcbb2598993b947c4d88419`, priority8. Preclaim
+cached overlap covered 341 open PRs, 5,722 Discussion records and all 8,348
+tracked local README/TASK notes. Specific terms led to PR5962's open question;
+no competing shell result surfaced. This is bounded text coverage, not a
+novelty certificate or a search of arbitrary diffs/unpublished work.
+
+Prepared by JoyboyBrian with substantial OpenAI Codex assistance and a
+separate read-only AI proof review. Credit Nick Petalas for PR5962, codyw912
+for PR4638, Mihir Srivastava for PR4507/4586, zxv for PR4436/4483, Jacob Alan
+Sussman for the integer compiler, Ryanson Jonathan and Cinna Davis for the
+retained flow/native lineage, and all source-specific predecessors.
+New work is Apache-2.0; no third-party source is modified or vendored.

research/adaptive-shell-width/SOURCES.json

@@ -0,0 +1,54 @@
+{
+  "schema_version": 1,
+  "base_commit": "721c03822c421b7f7fcbb2598993b947c4d88419",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a",
+      "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    },
+    {
+      "path": "research/adaptive-chronological-batching/batching.py",
+      "usage": "input",
+      "git_blob": "0347e94fec541a373807d5536e164d8ba617be77",
+      "sha256": "e443972cc4b4a5247b90a6b042f61db8171080c7499b416fbaad56059ef3f369"
+    },
+    {
+      "path": "research/compact-joint-compiler/arithmetic/RESULT.json",
+      "usage": "input",
+      "git_blob": "514d12ce4d2d824a4e0a418022bba610c8aed8ff",
+      "sha256": "a6caaa2a6d6460a8c1ef7e48c4853bb27976be33a52b96a4216dfa90d96c9091"
+    },
+    {
+      "path": "research/rank-convergence/BENCHMARKS.json",
+      "usage": "input",
+      "git_blob": "bc58c96abda014c28de91eca3ff10a7d4ec30b32",
+      "sha256": "513efe2fe74af82891c1918e462ba8338b1bbd06403cbfcec284bcf3b4f8f850"
+    },
+    {
+      "path": "research/adaptive-chronological-batching/WIDTH.md",
+      "usage": "input",
+      "git_blob": "4c637ac8968ffd5268ef39bf136e140afec11f6e",
+      "sha256": "63ddab206587d72abb9e155fd2f3532ca6c1b3a822a5e426a829f31bcfa535f8"
+    },
+    {
+      "path": "research/semigroup-rank-width/README.md",
+      "usage": "provenance",
+      "git_blob": "22d11704e08fc2fb4840986e2ea7b56502b5b30d",
+      "sha256": "eac1a545d42c9defad93e793948dc8298f383991a0c7fa42117b4fb75ceb3d09"
+    },
+    {
+      "path": "research/semigroup-rank-width/PROOF.md",
+      "usage": "provenance",
+      "git_blob": "2bffda1cd5f25464e26fa6dae0999d5646d0bbf3",
+      "sha256": "a03cb3e4d6831b7ef7bba3a5af88f92603adc6719c65e9455afec5ab5e3e4710"
+    }
+  ]
+}