Prove sharp multiplicative-shell growth for every rank alphabet (no κ)

research/multiplicative-shell-sharpness/PROOF.md

@@ -0,0 +1,118 @@
+# The shell exponent is sharp for every finite alphabet
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+## Statement
+
+Let A be a finite set of positive integers, let M >= 2 be an integer,
+and let Gamma be the multiplicative monoid generated by A union {M},
+including 1. Write v(g) for the vector of prime valuations of g, using
+the finite prime support of A union {M}. Put
+
+    r = dim_Q span{v(g): g in A union {M}},
+    J_l = |Gamma intersect [M^l, M^(l+1))|,  l = 0,1,2,... .
+
+Choose g_1,...,g_d from A such that v(M),v(g_1),...,v(g_d)
+are independent and span that space, where d=r-1. Such a selection exists
+because v(M) is nonzero and the original generators span the space.
+When d>0 put H=max_i ceil(log_M g_i); when d=0 put H=1.
+Every selected g_i is greater than one, so H>=1. Then
+
+    J_l >= binom(floor(l/H)+d, d)                    (1)
+
+for every l>=0. Together with JoyboyBrian's cited upper theorem in
+PR6086, J_l <= K(l+1)^d, this proves
+
+    J_l = Theta((l+1)^(r-1))                       (2)
+
+for every fixed A and M, including dependent alphabets and rank one.
+Constants may depend on A and M. This is a scoped counting theorem,
+not a lower bound on compiler widths.
+
+## Constructive lower bound
+
+For each tuple b=(b_1,...,b_d) of nonnegative integers with
+sum_i b_i <= floor(l/H), put G_b=product_i g_i^b_i. Since
+g_i <= M^H, we have 1<=G_b<=M^l. Let a_b be the least nonnegative
+integer with M^a_b G_b >= M^l. It exists with a_b<=l. Minimality gives
+
+    M^l <= M^a_b G_b < M^(l+1).
+
+For a_b=0 the upper inequality follows from G_b<=M^l<M^(l+1).
+For a_b>0 it follows by multiplying the preceding strict inequality
+M^(a_b-1)G_b<M^l by M. Thus each tuple gives a member of the required
+half-open shell, using only the original generators.
+
+If two images agree, unique prime factorization gives
+
+    (a_b-a_c)v(M) + sum_i (b_i-c_i)v(g_i) = 0.
+
+Independence forces b=c and a_b=a_c. The map is injective, even when
+other generators of A satisfy multiplicative relations. Stars and bars
+counts its domain as binom(floor(l/H)+d,d), proving (1).
+For d=0 this is the single witness M^l and binom(l,0)=1.
+
+For d>=1 and l>=H, floor(l/H)>=l/(2H), and
+binom(n+d,d)>=n^d/d!. This supplies an explicit positive multiple of
+l^d. The finitely many earlier levels contain M^l. The cited upper
+theorem now gives (2). In particular, for every epsilon>0 there is no
+bound J_l=O((l+1)^(r-1-epsilon)) for any one such fixed alphabet.
+
+## Exact formula in the independent case
+
+The same injection has an exact boundary. If Gamma is generated
+by precisely M,g_1,...,g_d and those valuation vectors are independent,
+then
+
+    J_l = #{b in Z_>=0^d: product_i g_i^b_i < M^(l+1)}.       (3)
+
+For any tuple counted on the right, choose the least nonnegative power
+of M taking its product into the shell, allowing a=0 when the product
+is already there. The argument above proves membership and injection.
+Conversely every shell member has a unique expression M^a product g_i^b_i.
+For that b there is exactly one allowable a because adjacent powers
+differ by the shell ratio M and the upper endpoint is excluded. This
+proves surjectivity and (3). Formula (3) counts finite exponent tuples;
+it is not asserted for arbitrary dependent alphabets.
+
+## Consequence and limit for adaptive widths
+
+PR6086 bounds the number of possible multiplicative plateau starts in
+each level of codyw912's PR4638 adaptive compiler. Its reported historical
+p16 alphabet has augmented valuation rank eleven. Using that reported
+rank as a premise, the present theorem gives J_l=Theta((l+1)^10) for
+that monoid. No predecessor rank computation or scientific replay is
+claimed here.
+
+Therefore replacing PR6086's shell estimate by a smaller polynomial
+degree for the same monoid cannot improve its width estimate. Actual
+plateau availability, source-count valuations, LCM cancellation and
+chronological reuse remain possible routes. There is no implication
+that the product upper bound for the LCM is attained. Nick Petalas's
+PR6612 already demonstrates the separate role of cancellation in a
+homogeneous model; its result is cited, not extended or rechecked here.
+
+No conclusion follows about a changed height base depending on l,
+an alphabet changing with l, a restricted reachable subset, a monoid
+that does not contain M, physical memory or runtime, native suppliers,
+any selected framework assumption, or a multiplication exponent.
+No selected construction or frontier is changed.
+
+## Evidence and credit
+
+The universal result is the written injection proof. The exact checker
+enumerates its own small finite monoids, independently constructs their
+membership by integer divisibility, checks all displayed lower witnesses,
+and tests (3) on independent alphabets. It does not import or execute
+any predecessor verifier. Positive finite cases corroborate the proof;
+they do not exhaust all alphabets or levels.
+
+Credit JoyboyBrian for PR6086's upper shell theorem, its actual adaptive
+application and open finite-bound question; codyw912 for PR4638's
+level-LCM recurrence; Nick Petalas for PR5962's multiplicative-rank
+refinement; Mihir Srivastava, zxv, Jacob Alan Sussman, Ryanson Jonathan,
+Cinna Davis and their retained compiler/native lineage. Prime valuation
+independence, unique factorization and stars and bars are classical.
+The new repository step is the effective matching lower theorem and
+its consequence for the shell-count route. General literature priority
+is unclaimed. Independent human and formal proof-kernel review are unclaimed.

research/multiplicative-shell-sharpness/README.md

@@ -0,0 +1,130 @@
+# Multiplicative shell counts have the sharp valuation-rank exponent
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+Independent human and formal proof-kernel review are unclaimed.
+
+Claim type: scoped written mathematical proof with exact finite corroboration.
+For every fixed finite integer alphabet containing the height base M>=2,
+let r be its rational prime-valuation rank. Its multiplicative monoid has
+
+    J_l = Theta((l+1)^(r-1))
+
+elements in the half-open shell [M^l,M^(l+1)). The new step is an effective
+matching lower bound for JoyboyBrian's
+[PR6086](https://github.com/CrocSwap/integer-mult-bounds/pull/6086).
+The predecessor upper theorem is cited, not reverified.
+
+Choose generators g_1,...,g_d whose valuation vectors extend v(M) to a
+basis, with d=r-1, and put H=max_i ceil(log_M g_i), or H=1 if d=0.
+The lower bound is
+
+    J_l >= binom(floor(l/H)+d,d),   for every integer l>=0.
+
+Each bounded exponent tuple supplies one distinct shell element after
+multiplication by the least suitable power of M. The [proof](PROOF.md)
+also gives the exact shell-count formula for independent generators.
+Dependent alphabets and rank one are included in the lower theorem.
+
+Using PR6086's reported p16 rank eleven as a premise gives a matching
+shell degree ten for that historical alphabet. The full-monoid exponent
+cannot decrease. A better actual width bound must use further information,
+such as reachable plateau restrictions or LCM cancellation. This is not a
+lower bound on compiler widths, physical costs or multiplication complexity.
+No new kappa, supplier, selected-frontier update or framework-assumption
+discharge is claimed.
+
+## Scope and evidence
+
+The base is `e54523517d0f03e58352e647c403a5af3e525a57`, priority revision 8.
+The source-binding orientation check reports selected #7000 at conditional
+kappa 0.00363005817; the older strategic text predates that selection.
+[TASK.json](TASK.json) records the change from the caller-bound
+`uniform-transfer-audit` card to this adaptive-compiler counting side result.
+[SOURCES.json](SOURCES.json) pins the catalogue, selected record and cited
+predecessor documents as provenance. The checker has no external live inputs.
+
+The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19538428)
+reserves the lower-bound question. Live overlap checks covered open PR
+metadata, recent handoffs and active Discussions, this account's previous
+PRs, merged searches and all-main README searches for shell lower bounds,
+valuation rank and semigroups. These searches do not cover unpublished work
+or every historical source file. PR6086 proves the upper theorem. PR5962
+and PR6612 give different width upper bounds and cancellation results.
+
+The exact finite checker constructs 360 alphabet/base fixtures and checks
+1,800 shells, including 4,016 lower-witness occurrences. Multiplicative
+closure agrees with an independent integer-divisibility membership oracle
+in every fixture. Seven independent-generator models give 49 exact shell
+identities with 297 point occurrences. Nine controls cover invalid domains,
+dependent generators, the excluded upper endpoint, capacity exhaustion,
+the missing-base hypothesis and rank one. These counts describe the declared
+finite domains; the universal conclusion rests on the written proof.
+
+## Reproduce
+
+From the repository root, with standard-library CPython 3.12:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/multiplicative-shell-sharpness/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/multiplicative-shell-sharpness/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/multiplicative-shell-sharpness
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/multiplicative-shell-sharpness --check-source-history
+```
+
+Substitute any CPython 3.12 path on another machine. Run the last command
+after committing. Each direct run prints `PASS_MULTIPLICATIVE_SHELL_SHARPNESS`
+inside a generated JSON receipt with counts and SHA256 of all six package
+files. It writes no files. The registered runner executes both modes and
+checks metadata and Git pins. No receipt is handwritten.
+
+No predecessor scientific replay, actual p16 compiler, selected cold replay,
+Lean, Docker, physical caller or complete multiplier is run or certified.
+The constants are fixed-alphabet constants. Varying alphabets/bases,
+restricted reachable subsets and monoids without M are outside the theorem.
+
+## Open next questions
+
+1. Can one nonhomogeneous compiler use a smaller actual reachable set?
+   Derive its exact plateau language, retaining every chronological cut.
+   A proved reachability invariant and full LCM bound are missing.
+2. Can source-count prime valuations improve the level-LCM bound despite
+   the sharp shell exponent? Start with an all-prime cancellation bound
+   along actual decreasing child chains in one nonhomogeneous profile.
+   Counting shell elements alone does not control those valuations.
+
+## Credit
+
+JoyboyBrian supplies PR6086's upper shell theorem, adaptive application and
+open finite-bound question. Retain codyw912's PR4638 level-LCM recurrence,
+Nick Petalas's PR5962 refinement, Mihir Srivastava, zxv, Jacob Alan Sussman,
+Ryanson Jonathan, Cinna Davis and the predecessor compiler/native lineage.
+PR6612 is cited only to distinguish cancellation from counting. Unique
+factorization, valuation independence and stars and bars are classical;
+general literature priority is unclaimed. No predecessor files are changed.
+
+## Implementation constraints
+
+The checker has no recursion, subprocesses, network, dynamic evaluation or
+package writes. Every enumeration is finite. Its main fixture list has
+360 entries and five levels each; the exact free-model list has seven
+entries and seven levels each. Matrix work is bounded by eight rows and
+six columns. Constructor domains have at most three independent directions
+and levels at most sixteen. Closure has a one-million-integer ceiling;
+the separate literal oracle has an 8,000-integer ceiling. Runtime contracts
+raise explicit exceptions and remain active with Python optimization.
+All functions fit within 60 physical lines.
+
+Power of Ten rule 3 deviation, `verify.py`: Python sets, Fraction and integer
+operations allocate during verification. Fixed allocation conflicts with this
+standard-library reference's managed runtime. The finite capacities above
+bound live data; only one alphabet is processed at a time. Boundary rejection
+controls and both interpreter modes check those limits. Runtime-internal
+allocation was not instrumented. A fixed-allocation implementation is needed
+before making any native fixed-memory claim.
+
+Rule 9 deviation, `check_controls`: a fixed seven-case table dispatches to
+four named checker functions, with no user-selected target or lifecycle.
+All seven rejecting calls are executed. Replace this test-only dispatch if
+the checker is ported to a platform forbidding indirect calls. Rule 10 uses
+warning-strict normal/optimized execution and AST inspection. No separate
+project-wide type checker or linter is claimed.

research/multiplicative-shell-sharpness/SOURCES.json

@@ -0,0 +1,30 @@
+{
+  "schema_version": 1,
+  "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "75d77b328ea02ded535e7f23aee5b1e55d0bb1a8",
+      "sha256": "154c3d30455d778fd3343b6b4851f0fa4665f0f7625b0adb3675e2bafbbf6bf1"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    },
+    {
+      "path": "research/adaptive-shell-width/PROOF.md",
+      "usage": "provenance",
+      "git_blob": "39f9caa6bf921fd2a814c4774fc1a938c715426b",
+      "sha256": "b8639b44c33d14b8e4f51fdfebaeba5b6d47a98010fbcd4167444f076f7b140d"
+    },
+    {
+      "path": "research/adaptive-shell-width/README.md",
+      "usage": "provenance",
+      "git_blob": "deab225e955710ac7e144d82173c5a62108ac587",
+      "sha256": "04cd01a446384ac0d089cfa92b4bbb1dfb1299f1c8d8d9d41255b4cd71dfeb91"
+    }
+  ]
+}

research/multiplicative-shell-sharpness/TASK.json

@@ -0,0 +1,89 @@
+{
+  "schema_version": 1,
+  "task_id": "uniform-transfer-audit",
+  "priority_revision": 8,
+  "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57",
+  "original_card": {
+    "id": "uniform-transfer-audit",
+    "question": "Can one of the selected record's five inherited assumptions be proved at its actual caller?",
+    "starting_points": [
+      "docs/research/current-priorities.md",
+      "docs/research/research-family-status.md",
+      "certificates/selected-result.json",
+      "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md"
+    ],
+    "methods": [
+      "Construct and independently check one source-bound instance of the stated first experiment.",
+      "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change."
+    ],
+    "acceptance_gate": "Identify the proposition and what would change downstream; do not equate a finite replay with a universal proof.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_selected_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.",
+      "scope": "Source-bound orientation only, not a supplier replay or theorem proof."
+    },
+    "first_experiment": "Choose one assumption ID (native_all_columns, owned_erasure, compiler, precision_tape, analytic_recovery), one quantified implication and exact dependency closure. Check current handoffs, including #5625 row reentry and #5707 root-prefix lowering, without treating their partial scope as the whole theorem. Prove or falsify that implication with a caller-bound argument; stop at the chosen obligation. Finite tests or root digits do not discharge an all-size statement.",
+    "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.",
+    "allowed_variations": [
+      "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes."
+    ],
+    "scope_change_triggers": [
+      "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.",
+      "Treating an archived proposal or local numerical pass as complete supplier admission."
+    ],
+    "overlap_terms": [
+      "native_all_columns",
+      "owned_erasure",
+      "compiler",
+      "precision_tape",
+      "analytic_recovery"
+    ],
+    "existing_checks": [
+      {
+        "scope": "PR #4100: proposed unconditional construction and finite checks, without independent acceptance.",
+        "evidence": "research/unconditional-batched-crt/README.md",
+        "remaining": "Independent proof audit of one caller-bound all-size implication; all other premises remain explicit.",
+        "status": "author-checked",
+        "source_commit": "337d04939571a637aeab54a0f58f54fde811663a",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.",
+        "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md",
+        "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.",
+        "status": "reviewed",
+        "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137",
+        "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5"
+      }
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "Prove an effective matching lower bound for every fixed multiplicative-shell alphabet, settling sharpness of the r-1 exponent in PR6086.",
+  "scope_change_reason": "The selected card asks for a caller-bound framework implication. This side result instead settles a quantitative counting obstruction in the alternative adaptive compiler; it does not discharge a selected assumption or claim a width lower bound.",
+  "bottleneck_link": "The matching lower exponent rules out a smaller-degree shell-count estimate for the same monoid as a route to improving the adaptive width upper bound. Actual LCM cancellation or a restricted reachable set remains necessary for that route.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop at the first verified constructive lower theorem and package it; do not pursue an actual compiler or exponent improvement.",
+  "outcome": "negative-result",
+  "evidence": "PROOF.md gives the all-alphabet injection; verify.py checks independent finite monoid oracles, lower witnesses, the exact free-monoid identity and rejection controls.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Can a named adaptive compiler use a smaller reachable set than the full multiplicative monoid in its level-LCM bound?",
+      "why_it_matters": "The full-monoid shell exponent cannot decrease, but not every monoid element must be a distinct actual plateau start.",
+      "first_step": "Derive the exact reachable plateau language for one nonhomogeneous target/paid profile and retain every chronological cut.",
+      "blocked_by": "No such reachable-set invariant or resulting full LCM bound is established here."
+    },
+    {
+      "question": "Can actual source-count prime valuations improve the adaptive level-LCM estimate despite the sharp shell exponent?",
+      "why_it_matters": "A product bound need not be attained by the LCM.",
+      "first_step": "Choose one nonhomogeneous profile and prove an all-prime cancellation bound along the actual decreasing child chains.",
+      "blocked_by": "The shell theorem alone does not control source-count valuations or the full width recurrence."
+    }
+  ]
+}