Sharpen chronological width by multiplicative rank (no new κ)

research/semigroup-rank-width/PROOF.md

@@ -0,0 +1,119 @@
+# A multiplicative-rank refinement of chronological width
+
+## Statement
+
+Use exactly the fixed default-height rule, chronological batches and integer
+width recurrence of codyw912's [PR #4638](https://github.com/CrocSwap/integer-mult-bounds/pull/4638),
+`research/chronological-width-bound`, sections 1-4. In particular the target
+ranks have positive integer multiplicities W_k, paid ranks have positive
+integer multiplicities P_j, and
+
+```
+2 <= k_min <= k <= m = max(target ranks),
+1 <= j <= j_max < m,
+W = sum W_k, P = sum P_j.
+```
+
+Base widths below m are one. At rank n >= m the cap is floor(n/m) and
+the height is floor(log_(k_min)(floor(n/m))). Let A be the set of all target
+and paid ranks. Rank one is permitted and contributes a zero valuation vector.
+Let Pi be the prime support of A and d its size. Form the integer matrix
+
+```
+V = (v_p(a)) with rows p in Pi and columns a in A,
+r = rank_Q(V).
+```
+
+Then 1 <= r <= d, and the same width sequence satisfies
+
+\[
+\log B_N=O((\log N)^{r+1}).
+\]
+
+The constant depends on the fixed rule. This replaces d+1 in #4638 by r+1.
+The degree strictly decreases when the valuation vectors span a proper
+subspace of Q^d. It is an upper bound and does not assert a matching lower
+bound for the actual widths.
+
+## The new counting lemma
+
+Let Gamma be the multiplicative semigroup generated by A, including one.
+Choose a set I of r prime coordinates whose r rows of V are independent.
+Such rows exist by the definition of rank. Projection to those coordinates
+is injective on the column space U of V. Indeed its restriction has rank r,
+equal to dim U, so its kernel is zero.
+
+For x in Gamma, the complete valuation vector v(x) belongs to U. If two
+products x,y have the same valuations at the primes in I, injectivity gives
+v(x)=v(y) at every prime in Pi. Unique prime factorization gives x=y.
+This argument does not require a unique expression as a product of generators.
+
+For 1 <= x <= X, each selected coordinate is an integer in
+[0,floor(log_p X)]. Therefore
+
+\[
+|\Gamma\cap[1,X]|
+\le\prod_{p\in I}(1+\lfloor\log_p X\rfloor)
+\le(1+\lfloor\log_2 X\rfloor)^r.                 \tag{1}
+\]
+
+The selected-prime box can contain vectors outside the projected semigroup.
+Surjectivity is unnecessary. Selecting arbitrary r primes is insufficient;
+their rows must be independent on U. For example projecting the semigroup
+generated by 6 and 10 only to the 3-adic coordinate identifies 1 and 10.
+
+## Application to the inherited width divisor
+
+The following facts are cited from #4638, sections 2-4, rather than
+re-established by a source replay here. Source counts S(gamma) are constant
+on Gamma plateaus. At cap C their bound is
+
+\[
+1\le S(\gamma)\le W(W+P)^G,
+\qquad G=\lfloor\log_{k_{\min}} C\rfloor.
+\]
+
+Every recursive child has rank at most alpha=(m-1)/m times its parent rank.
+With tau=m ceil(log_2 k_min), every descending rank chain visits each plateau
+at most tau times. For every N >= m, this yields the all-prime divisor
+
+\[
+B_n\mid Q_N=
+\prod_{\substack{\gamma\in\Gamma\\\gamma\le C}} S(\gamma)^\tau,
+\qquad C=\lfloor N/m\rfloor,\quad 0\le n\le N.       \tag{2}
+\]
+
+The prime factors of S(gamma) need not belong to Pi. Equation (2) retains
+all of them. The new projection is used only to count plateau locations;
+it does not discard any source-count or width prime.
+
+Combining (1) and (2) gives the explicit new estimate
+
+\[
+\log_2 B_n\le
+\tau\prod_{p\in I}(1+\lfloor\log_p C\rfloor)
+\bigl(\log_2 W+G\log_2(W+P)\bigr),\quad n\le N.     \tag{3}
+\]
+
+There are O((log N)^r) box points, and the final factor is O(log N).
+This proves the stated all-rank bound. Replacing the two logarithms in the
+last factor by their integer ceilings gives a computable integer exponent
+b_N with B_n <= 2^b_N. All width and chronological correctness premises
+are unchanged. No assumption that gcd cancellation is small or absent is used.
+
+## A strict degree improvement
+
+Take target multiplicities W_6=W_36=1 and paid multiplicities P_1=P_6=1.
+This is an admissible rank pattern for the integer recurrence, since 6<36.
+No physical native rule realizing it is asserted. Its prime support is {2,3},
+but its valuation columns are (1,1), (2,2) and (0,0), of rational rank one.
+The old width theorem gives log B_N=O((log N)^3); (3) gives
+log B_N=O((log N)^2) for this same recurrence.
+
+The semigroup is exactly {6^j:j>=0}, so its exact plateau count is
+1+floor(log_6 C). This example witnesses a strict decrease of the proved
+upper-bound degree, not a measured asymptotic separation between two
+width sequences. This contribution changes no sequence.
+
+The first proved refinement is the finish line. Adaptive heights, optimal
+coordinate choices and sharper actual-width growth are left open.

research/semigroup-rank-width/README.md

@@ -0,0 +1,147 @@
+# Chronological width in the multiplicative rank
+
+For the fixed default-height chronological compiler of
+[codyw912's PR #4638](https://github.com/CrocSwap/integer-mult-bounds/pull/4638),
+let d count primes dividing target or paid ranks, and let r be the rational
+rank of their prime-valuation vectors. The same width sequence satisfies
+
+```
+Previous upper bound: log B_N = O((log N)^(d+1))
+New upper bound:      log B_N = O((log N)^(r+1)),  r <= d.
+```
+
+This answers the exponent-lattice refinement in #4638's first Open next
+question. A projection to r independent prime coordinates is injective on
+the rank semigroup. Its selected-prime exponent box therefore bounds the
+number of source-count plateaus. [PROOF.md](PROOF.md) gives the quantified
+argument and the resulting explicit integer bit envelope.
+
+This is a **scoped conditional all-rank proof**, with finite exact
+corroboration. It changes neither the compiler nor its width sequence.
+It gives a strictly smaller upper-bound degree when r<d; it does not prove
+that either bound is tight. No new leaf exponent or kappa is claimed.
+
+For the abstract target pattern {6:1,36:1} and paid pattern {1:1,6:1},
+d=2 and r=1. The proved logarithmic degree decreases from three to two.
+The semigroup is exactly {6^j:j>=0}. No physical native supplier for this
+pattern is asserted. The finite checker at cap 46656 finds its seven
+semigroup elements. The generic selected-prime box has 16 points, and the
+explicit conservative width exponent is 22464. These are different quantities.
+
+## Evidence and scope
+
+The independently written standard-library checker imports no predecessor
+program and replays no predecessor census. It checks:
+
+- Every one-, two- and three-element subset of {1,...,12}, at caps 1, 7, 64
+  and 257, plus four larger discriminating fixtures at cap 46656.
+- Exact semigroup equality between bounded generator multiplication and an
+  independent integer-by-integer divisibility oracle, projection injectivity,
+  the selected-prime box bound and the full-prime comparison.
+- Rational elimination ranks against independent nonzero-minor enumeration
+  using the Leibniz determinant formula, for every fixture.
+- Thirteen rejecting controls and two further semantic comparisons, including
+  a rank-deficient coordinate choice, omitting a paid-rank prime and an
+  actual collision under an insufficient projection.
+
+Executed output on CPython 3.12.15:
+
+```
+PASS_SEMIGROUP_RANK_WIDTH
+fixtures=1196 enumerated_members=7641 strict_rank_reductions=186 controls=15
+```
+
+The member count sums occurrences across fixtures; it is not a count of
+distinct integers across the whole run. The 186 counts fixtures with r<d.
+Normal and optimized modes run the same explicit checks without Python
+assertions. Finite checks corroborate the new counting lemma; the all-rank
+conclusion follows from the written proof and the cited #4638 premises.
+The predecessor's flow, batching policy, source bound and all-prime width
+divisor are used as published results and were not audited here. Both timed
+registered commands completed in about 0.13 seconds locally. Three disposable
+optimized-code mutations reject: an insufficient coordinate set, omitted
+semigroup products and an incorrect width charge.
+
+## Reproduce
+
+From the repository root, using CPython 3.12 and its standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/semigroup-rank-width
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/semigroup-rank-width/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/semigroup-rank-width/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/semigroup-rank-width --check-source-history
+```
+
+Substitute a local CPython 3.12 path on another machine. Each registered
+check has a 120-second timeout. The direct checker works without Git or
+network access and normally writes nothing. To create a new receipt, add
+`--record /absolute/scratch/path/receipt.json`. It refuses to overwrite an
+existing file and generates the results, interpreter version and SHA256
+hashes of all six package files. No receipt is hand-written.
+
+[SOURCES.json](SOURCES.json) pins historical source documents and task
+provenance. There are no external executable or data inputs. The source
+README is cited as provenance, not dynamically imported. Hosted CI and
+independent mathematical acceptance are separate from local checks.
+
+## Limitations and open obligations
+
+This is a compiler-size side result under the precise default-height
+recurrence. The selected baseline orientation passed; no selected supplier
+or historical scientific replay was run. No actual selected inventory is
+claimed to have r<d. Native semantics, physical allocation, dirty restoration,
+fixed-tape movement, precision, stock, all-size implementation and outer
+transfer remain inherited obligations. The five selected framework assumptions
+and selected frontier are unchanged. Independent human and formal proof-kernel
+review are unclaimed.
+
+The proof has no generator-size limit. The executable helper bounds its
+alphabet to 16 entries, each at most 1000000, and cap to 65536; the exhaustive
+minor oracle is used only for at most three distinct generators. Python
+allocates managed objects during execution; input capacities bound live
+collections. The fixed local control table uses thirteen bounded callbacks.
+No recursion or dynamic code generation is used. Warning-strict execution and
+in-memory Python compilation pass; no external Python linter was available.
+
+## Open next questions
+
+1. Does the same multiplicative-rank refinement sharpen #4638's adaptive
+   theorem after adjoining its height base M to the alphabet? First isolate
+   its level-LCM count and prove the required shell bound. The changed-height
+   decrement and nonemptiness hypotheses must be retained.
+2. Can source valuations or actual gcd cancellation reduce the remaining
+   logarithmic factor for a named default-height rule? First derive an exact
+   valuation recurrence for that rule. The semigroup count alone gives no
+   matching lower bound for its widths.
+
+Structured relevance, first steps and blockers are in [TASK.json](TASK.json).
+No further construction or search was undertaken after this refinement.
+
+## Credit and coordination
+
+This contribution was produced by Nick Petalas. The new step is the
+independent-coordinate counting lemma and its application to the inherited
+chronological width divisor. The projection argument uses elementary
+linear algebra and unique prime factorization; no historical priority for
+those tools is claimed. New work is Apache-2.0.
+
+codyw912 #4638 supplies the d+1 theorem, the bounded plateau visits and the
+explicit exponent-lattice question. Mihir Srivastava #4507 supplies least
+chronological batching, zxv #4436/#4483 and Jacob Alan Sussman supply the
+compiler and flow, and Ryanson Jonathan and Cinna Davis retain their
+credited flow/width and native-construction lineage. Mihir Srivastava #4586
+and Ryanson Jonathan #4588 supply earlier growth and finite-check context.
+Nick Petalas #4892 concerns global divisibility minimality for a fixed
+batch library, a distinct result with no new growth-degree bound.
+
+Base: canonical main 19fdb086ea96af9a9f87936a2b888e10af4ed810, priority
+revision 8. The formal-interface-lemma card is explicitly changed to this
+written compiler-size lemma, not a proof-assistant formalization. The
+[advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19221421)
+records the bounded target. Live open/account PRs, merged term searches,
+main's README text, active Discussions and the latest handoff comments were
+checked. The overlap cache searched 341 open PRs and 5519 Discussion records
+with reported complete pagination, but only 214 of 8136 local note records
+were materialized; separate Git searches covered omitted main README files.
+This is bounded overlap evidence, not a proof of novelty.

research/semigroup-rank-width/SOURCES.json

@@ -0,0 +1,24 @@
+{
+  "schema_version": 1,
+  "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8",
+      "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    },
+    {
+      "path": "research/chronological-width-bound/README.md",
+      "usage": "provenance",
+      "git_blob": "7548fd2060e41cf5b58485126d14b4dec936406a",
+      "sha256": "0a255788cd9b462c4cbef39721ce42d129878bf564fc08be33752ca84530e38d"
+    }
+  ]
+}

research/semigroup-rank-width/TASK.json

@@ -0,0 +1,101 @@
+{
+  "schema_version": 1,
+  "task_id": "formal-interface-lemma",
+  "priority_revision": 8,
+  "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810",
+  "original_card": {
+    "id": "formal-interface-lemma",
+    "question": "Can one uncovered interface implication be formalized with exact caller and certificate bindings?",
+    "starting_points": [
+      "docs/research/research-family-status.md",
+      "certificates/selected-result.json",
+      "research/gate-operand-parity-lean/README.md",
+      "research/staged544-certified-endpoint/README.md",
+      "research/unconditional-batched-crt/README.md"
+    ],
+    "methods": [
+      "Formalize a missing boundary lemma identified by the selected review.",
+      "Audit a formal theorem-to-certificate binding independently."
+    ],
+    "acceptance_gate": "State the exact formalized proposition and remaining assumptions; avoid duplicate arithmetic formalizations already present.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_selected_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Resolve the current selected review, separate complex/ordinary BIT/admitted BIT/outer budgets, and compare the card against live handoffs before starting. Historical ceilings require exact source/model equivalence.",
+      "scope": "Source-binding orientation only; not a scientific replay or all-size proof. Materialize selected inputs if this checkout is sparse."
+    },
+    "first_experiment": "Write one missing statement with quantified hypotheses, actual caller and existing coverage. A compact-switch lemma is a candidate only after its mathematical contract is reviewed. Establish a bounded proof plan before a separately budgeted proof-assistant build; do not rerun large Lean jobs as orientation.",
+    "bottleneck_link": "A missing interface proof can reduce the conditional gap even if it does not change kappa.",
+    "allowed_variations": [
+      "Narrow to one formal lemma or one theorem-to-certificate binding."
+    ],
+    "scope_change_triggers": [
+      "Formalizing already-covered arithmetic and claiming the full multiplication theorem."
+    ],
+    "overlap_terms": [
+      "hyperplane end",
+      "formal interface",
+      "Lean binding",
+      "3807",
+      "3857",
+      "4100",
+      "gate-operand-parity-lean",
+      "staged544-certified-endpoint",
+      "unconditional-batched-crt"
+    ],
+    "existing_checks": [
+      {
+        "scope": "PR #3807: scoped gate-operand parity formalization.",
+        "evidence": "research/gate-operand-parity-lean/README.md",
+        "remaining": "Exact theorem-to-caller binding and genuinely uncovered interface lemmas.",
+        "status": "author-checked",
+        "source_commit": "4c3530f42a6abcc48e7a6bcffd6c901911dc8269",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "scope": "PR #3857: certified real-power moment/endpoint arithmetic.",
+        "evidence": "research/staged544-certified-endpoint/README.md",
+        "remaining": "Uniform algorithmic implications, not another endpoint digit.",
+        "status": "author-checked",
+        "source_commit": "ef4315b8caa605e47a2515004845eb2d2ed71a86",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "scope": "PR #4100: compact-switch formalization proposed as future validation.",
+        "evidence": "research/unconditional-batched-crt/README.md",
+        "remaining": "Audit the statement and assumptions before a formal proof campaign.",
+        "status": "author-checked",
+        "source_commit": "337d04939571a637aeab54a0f58f54fde811663a",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      }
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "Prove a multiplicative-rank refinement of the default chronological compiler width, answering PR4638 Open next question 1.",
+  "scope_change_reason": "The user requests original work rather than an audit. This is a written compiler-size lemma, not a proof-assistant theorem-to-certificate binding.",
+  "bottleneck_link": "Compiler-size side result: dependencies in the rank alphabet reduce the proven width-growth degree. No supplier, physical caller or kappa improvement follows.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop at the first verified multiplicative-rank degree refinement; leave adaptive heights and sharper growth open.",
+  "outcome": "completed",
+  "evidence": "PROOF.md and verify.py: independent semigroup and minor oracles, explicit degree-reduction witness and semantic controls.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Extend the multiplicative-rank bound to fixed adaptive heights after adjoining M.",
+      "why_it_matters": "Rank dependencies may also improve the adaptive compiler-size bound.",
+      "first_step": "Prove a semigroup shell count compatible with the inherited level-LCM envelope.",
+      "blocked_by": "Changed-height decrements and nonemptiness must be retained; not proved here."
+    },
+    {
+      "question": "Reduce the remaining logarithmic factor for a named default-height rule.",
+      "why_it_matters": "The current source-count bound can still be loose.",
+      "first_step": "Derive an exact prime-valuation recurrence retaining batch gcd cancellation.",
+      "blocked_by": "A plateau count alone supplies no actual-width lower bound or sharper source valuations."
+    }
+  ]
+}