Prove exact polynomial widths from chronological gcd cancellation (no κ)

research/homogeneous-gcd-width/PROOF.md

@@ -0,0 +1,172 @@
+# Exact cancellation in a homogeneous chronological compiler
+
+This scoped written proof was produced by Nick Petalas. It specializes
+codyw912's PR4638 arbitrary-height forest and Mihir Srivastava's PR4507
+chronological batching policy. Their validity and native contracts are cited
+premises. No predecessor result is re-audited here.
+
+## Hypotheses
+
+Fix integers m>=2 and W,P>=1. A raw unit has W distinguishable productive
+positions, all of rank m, and P distinguishable chronological paid positions,
+all of rank 1. Use precisely the arbitrary-height forest in PR4638. At
+ambient integer rank n>=m its cutoff is C=floor(n/m), and its height G(n)
+is any specified nonnegative finite integer. Different ranks may have
+different heights. Set B_j=1 for 0<=j<m.
+
+The W targets are separate arbitrary inputs. No productive role is silently
+identified with another. Separate paid paths and positions retain separate
+chronological cuts. The interpretation as a physical supplier requires the
+predecessor's native, whole-job, ownership and closure hypotheses. This proof
+does not construct a native unit with this symbolic inventory.
+
+For every n>=m define
+
+```text
+H(n) = floor(log_m n),
+k(n) = min(G(n)+1,H(n)),
+d(n) = G(n)+1-k(n),
+s(n) = m^k(n),
+S(n) = P^d(n) W^k(n).
+```
+
+All logarithms here define integer floors by power comparison. Since
+floor(log_m floor(n/m))=H(n)-1, the first present depth of the forest is
+d(n). In particular 1<=k(n)<=H(n), m<=s(n)<=n, and n-s(n)<n.
+
+## Lemma 1. The complete source and cut lists
+
+At depth d a class is indexed by a distinguishable paid path of length d.
+There are P^d such classes. A unit is indexed by an ordered target word of
+length G-d. All these words have column m^(G-d), independently of their
+letters. Consequently either the entire class is present or it is empty.
+It is present exactly when m^(G-d)<=C, which is equivalent to d>=d(n).
+
+For a nonleaf present parent, its W^(G-d) paid outputs at one position
+match the child's target demands bijectively. Split a parent word into its
+first letter and remaining word. Both have the same column/rank contract,
+and the child is present whenever its parent is. Thus no present class has
+an unmatched nonleaf exit. This is matching within one actual paid cut,
+with no pooling between paths or positions.
+
+If d(n)=0, the root demands W^(G+1) source jobs of rank m^(G+1).
+If d(n)>0, the classes through depth d(n)-1 are empty. At the first present
+depth d(n), each of the P^d(n) classes demands W^(G-d(n)+1) fresh source
+jobs, all of rank m^(G-d(n)+1). No later class needs a fresh source because
+its present parent supplies it. These two cases give the same source list
+
+```text
+one rank s(n), with total multiplicity S(n).
+```
+
+Every depth-G class contains the single empty target word. Each of its P
+paid positions therefore exits with one rank-one job. The complete exit
+list has P^(G+1) separate cuts, each (rank 1, multiplicity 1). Its length
+is an algebraic count; a general-height forest is not emitted by this proof.
+There are no boundary exits. This also proves nonemptiness, including when
+the root class is empty.
+
+As a consistency identity, its unit-column mass V is
+
+```text
+V = sum_(d=d(n)..G) P^d (Wm)^(G-d),
+S(n) s(n) - P^(G+1) = (Wm-P) V.
+```
+
+This is a telescoping finite geometric sum, valid also at Wm=P. No positive
+surplus or favorable moment is assumed merely to count the forest.
+
+## Theorem 2. Exact least-LCM width at every height
+
+The source complement is one upfront batch
+(n-s(n),S(n)). All the separate exits use B_1=1 and impose no replication
+constraint. Applying the cited local batching lemma gives
+
+```text
+a_n = B_(n-s(n)) / gcd(B_(n-s(n)),S(n)),
+B_n = S(n) a_n = lcm(S(n),B_(n-s(n))).                 (1)
+```
+
+This is the recursively least library under that fixed common-replication
+policy. Local minimality is inherited from PR4507; no optimality over other
+policies or physical programs is claimed.
+
+Starting at n_0=n, set n_(i+1)=n_i-s(n_i) until n_t<m. Each step decreases
+the rank by at least m, so t<=floor(n/m). Repeated application of (1) gives
+the exact closed expression
+
+```text
+B_n = lcm_(0<=i<t) [P^d(n_i) W^k(n_i)].              (2)
+```
+
+The empty LCM is 1. This expression retains the actual gcd cancellations;
+replacing the LCM by multiplication or by numerical maximum is invalid.
+
+## Corollary 3. Exact default width
+
+For the default height G(n)=floor(log_m floor(n/m))=H(n)-1,
+one has d(n)=0, s(n)=m^H(n), S(n)=W^H(n). Along the decreasing chain every
+later H is at most the initial H. Every later source total therefore divides
+the first. Equation (2) proves, for all n>=m,
+
+```text
+B_n = W^floor(log_m n).                              (3)
+```
+
+At n=m^h, this is exactly W^h, so its polynomial order cannot be reduced
+when W>1. P affects exits and cost, but not this default productive width.
+
+For comparison define the specific gcd-free recurrence
+U_j=1 for j<m and U_n=S(n) U_(n-s(n)). Writing n=sum a_j m^j in base m
+gives U_n=W^(sum_(j>=1) j a_j), because each subtraction removes one largest
+power. At n=m^(h+1)-1 its exponent is (m-1)h(h+1)/2. Hence retaining gcd
+cancellation changes this particular upper construction from worst-shell
+exp(Theta((log n)^2)) to polynomial width when W>1. This comparator is
+defined here; it is not alleged to be a predecessor's optimal width.
+
+## Corollary 4. Polynomial adaptive widths, including empty roots
+
+Put G_*(N)=max_(m<=j<=N) G(j), with N>=m. Every source in the chain for
+any n<=N divides W^H(N) P^G_*(N), since k(j)<=H(N) and d(j)<=G(j).
+This remains true when W and P have shared prime factors. Thus
+
+```text
+B_n divides W^H(N) P^G_*(N),  m<=n<=N.               (4)
+```
+
+In particular, fix M>=2 and integer g>=1 and use the predecessor's height
+G(n)=g floor(log_M floor(n/m)). This is monotone, so (4) at N=n gives
+
+```text
+B_n divides W^floor(log_m n) P^(g floor(log_M floor(n/m))),
+B_n <= n^(log_m W + g log_M P).                     (5)
+```
+
+This proves polynomial width even when m^g<M, where the general adaptive
+envelope in PR4638 has a subexponential factor. Equation (5) need not be
+sharp. No lower bound or universal polynomial width theorem for mixed rank
+alphabets follows. The hypothesis that every paid rank is one is essential
+to the cut reduction used above.
+
+## Scope and attribution
+
+The new results are the exact homogeneous source/cut reduction, chain-LCM
+solution, default closed form and polynomial adaptive divisor. The question
+comes from PR4638's request to retain actual gcd savings. PR5962's independent
+prime-coordinate projection and PR6086's shell counting retain a different
+mechanism and are not audited or extended here. This proof does not tighten
+their generic semigroup estimates.
+
+Credit Jacob Alan Sussman's integer compiler; zxv's PR4436/4483 chronological
+forest; Mihir Srivastava's PR4507 local gcd/LCM policy; codyw912's PR4638
+arbitrary-height transfer and width question; and Cinna Davis and Ryanson
+Jonathan for the retained native/flow lineage. LCM arithmetic, positional
+notation and finite geometric sums are classical. No literature-wide
+priority is claimed for those tools.
+
+This is a conditional mathematical specialization. It supplies no physical
+native inventory, storage/tape cost, numerical precision, stock constant,
+outer consumer, new kappa or complete multiplication theorem. In particular,
+polynomial productive width does not bound the cost of generating every
+smaller program. The five selected framework assumptions remain.
+Independent human and formal proof-kernel review are unclaimed.

research/homogeneous-gcd-width/README.md

@@ -0,0 +1,129 @@
+# Exact polynomial widths from chronological gcd cancellation
+
+This scoped written proof was produced by Nick Petalas. For a symbolic native
+rule with W distinguishable rank-m productive targets and P distinguishable
+rank-one paid positions, the least chronological compiler widths have the
+exact default-height formula
+
+```text
+B_n = W^floor(log_m n),  n>=m;       B_n=1, 0<=n<m.
+```
+
+At an arbitrary finite height G(n), put H=floor(log_m n), k=min(G(n)+1,H),
+s=m^k and S=P^(G(n)+1-k) W^k. The complete cut inventory gives
+
+```text
+B_n = lcm(S,B_(n-s)).
+```
+
+Thus B_n is exactly the LCM of source totals along one decreasing rank chain.
+At adaptive height G(n)=g floor(log_M floor(n/m)), for fixed M>=2 and g>=1,
+
+```text
+B_n divides W^floor(log_m n) P^(g floor(log_M floor(n/m))),
+B_n <= n^(log_m W + g log_M P).
+```
+
+This is a polynomial bound, including parameter ranges where PR4638's general
+adaptive envelope is subexponential. The new step retains actual gcd
+cancellation. It supplies a concrete positive answer to that package's
+gcd-savings opening, without improving its generic semigroup count.
+[PROOF.md](PROOF.md) gives all quantifiers, the complete specialized cuts and
+the comparison with a separately defined gcd-free recurrence.
+
+At m=2,W=2,P=3,n=1023, the least width is 512. Omitting gcd cancellation in
+that recurrence gives 2^45. At fixed height two, the actual rank-10 chain has
+source totals 8 and 18 and needs width 72; replacing LCM by maximum fails.
+These are compiler widths, not runtime measurements or a new kappa.
+
+## Evidence and reproduction
+
+The standalone checker imports no predecessor code and writes no files. It
+enumerates 2,052 forests, including 1,422 empty-root cases, and 139,536 literal
+leaf cuts. Distinguishable paid paths and ordered target words independently
+recover the claimed source/cut and unit-column formula. Exact rank invoices
+also agree. A separate literal-batch compiler checks 27 default width tables.
+The recurrence and chain formula agree at 121,440 coordinates in 480 tables
+across default, fixed and adaptive rules. Twelve domain rejections and seven
+semantic control groups retain explicit checks under optimization.
+Four capacity controls exercise the declared logarithm, closed-form, chain
+and width-table limits. Three disposable optimized-code mutations reject an
+omitted empty-root depth, omitted paid-path multiplicity and omitted gcd.
+
+The finite domains corroborate the written proof. They do not establish its
+unbounded quantifiers or certify a physical native supplier. The receipt is
+generated on stdout and binds all six package files by SHA256; no receipt is
+hand-written or committed.
+
+From the worktree root, with the local CPython 3.12 interpreter:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/homogeneous-gcd-width/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/homogeneous-gcd-width/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/homogeneous-gcd-width
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/homogeneous-gcd-width --check-source-history
+```
+
+Other machines may substitute their CPython 3.12 path. Only the standard
+library is required. Expected markers are PASS_HOMOGENEOUS_GCD_WIDTH,
+PASS_REGISTERED_RESEARCH_PACKAGE and PASS_RESEARCH_COMMIT_BYTES. Source pins
+are provenance only, so the standalone six-file replay also works without Git.
+
+## Scope, credit and overlap
+
+The source question is codyw912 / [PR4638](https://github.com/CrocSwap/integer-mult-bounds/pull/4638),
+Open next question 2 of research/adaptive-chronological-batching. Credit Mihir
+Srivastava / [PR4507](https://github.com/CrocSwap/integer-mult-bounds/pull/4507)
+for least chronological batching; zxv / PR4436 and PR4483 for the default and
+arbitrary-height forests; Jacob Alan Sussman for integer compilation; and
+Cinna Davis and Ryanson Jonathan for their retained native and flow lineage.
+LCM arithmetic and positional notation are classical. No literature-wide
+priority claim is made.
+
+Nick Petalas / PR5962 improves semigroup counting, and JoyboyBrian / PR6086
+improves adaptive shell counting. This proof uses a different mechanism,
+retaining exact cancellation in source multiplicities. The source results
+and their numbers are cited premises, not audit or replay deliverables.
+
+Canonical base is 7c49fe32c55de02c2c873655c804b16e4c3fef0a, priority revision 8,
+selected PR6030. The selected mixed-rank inventory is outside this theorem.
+Live open PRs, active Discussions, recent account work, local reservations and
+main/merged object and general-form searches were checked. Cached overlap
+reported complete pagination for 555 open PRs and 6,599 discussion records;
+sparse local notes, arbitrary historical diffs and unpublished work remain
+coverage limits. The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19373389)
+records the exact scope. Structured metadata is in [TASK.json](TASK.json).
+
+No physical realization of the homogeneous rule, finite generation-time bound,
+practical cutoff, storage extent, precision, stock, outer consumer, supplier
+admission or complete multiplication theorem is supplied. All-column native
+semantics, ownership/erasure, compiler realization, precision/tape and analytic
+recovery remain conditional obligations. Independent human and formal
+proof-kernel review are unclaimed. The selected cold replay, Lean and Docker
+were not run. New work is Apache-2.0; frozen predecessor files are unchanged.
+
+## Open next questions
+
+- Bind one physically realized native word to this inventory and price its
+  complete caller. A useful physical inventory is missing; polynomial width
+  alone does not improve the selected exponent.
+- Find a valuation invariant retaining gcd savings for one mixed-rank physical
+  profile. The one-complement and rank-one-exit reduction fails there, so this
+  proof supplies no mixed-rank polynomial width claim.
+
+## Verifier constraints
+
+All functions are at most 45 lines. Loops and iterator products have explicit
+finite domains; there is no recursion, subprocess, network, dynamic code
+execution, callback or output-file creation. Explicit guards remain active
+under optimized Python. Registered replay uses warnings as errors.
+
+Power-of-ten rule 3 deviation: CPython allocates managed integers, sets and
+containers during checking. The literal oracle bounds m<=6, W,P<=3, n<=512
+and height<=5. Each target-word set has at most 243 members and each paid-path
+iterator has at most 243 members; a leaf sweep has at most 729 cuts. Width
+tables have at most 1,025 entries. The closed formula caps height at 256 and
+rank at 2^256. Package reads are bounded by two MiB per file. These controls
+bound live memory in this one-shot verifier; they do not provide an
+allocation-free runtime. An embedded fixed-allocation port would need a
+separate implementation and capacity review.

research/homogeneous-gcd-width/SOURCES.json

@@ -0,0 +1,42 @@
+{
+  "schema_version": 1,
+  "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a",
+  "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/README.md",
+      "usage": "provenance",
+      "git_blob": "d8cb94c3f4e9210060da425d882fde9d2b03e6c1",
+      "sha256": "3943b7e0dabc0486d566f2070518a28f1429e9cce9b578dd4b3a2a00dc7f4cf4"
+    },
+    {
+      "path": "research/adaptive-chronological-batching/WIDTH.md",
+      "usage": "provenance",
+      "git_blob": "4c637ac8968ffd5268ef39bf136e140afec11f6e",
+      "sha256": "63ddab206587d72abb9e155fd2f3532ca6c1b3a822a5e426a829f31bcfa535f8"
+    },
+    {
+      "path": "research/adaptive-chronological-batching/batching.py",
+      "usage": "provenance",
+      "git_blob": "0347e94fec541a373807d5536e164d8ba617be77",
+      "sha256": "e443972cc4b4a5247b90a6b042f61db8171080c7499b416fbaad56059ef3f369"
+    },
+    {
+      "path": "research/chronological-batch-width/README.md",
+      "usage": "provenance",
+      "git_blob": "c85304a601f858774f425d5f3869ac0a6f85ec29",
+      "sha256": "0cf276c77016a98a0dabba822d27bb9cb94c0bf86ec353a16499fe85e6032c20"
+    }
+  ]
+}