From 426d1f55263d91ccfedd85a80b059659a634091b Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Wed, 11 Nov 2026 09:03:41 +0000 Subject: [PATCH] docs(research): prove sharp multiplicative shell growth --- .../multiplicative-shell-sharpness/PROOF.md | 118 ++++++++++ .../multiplicative-shell-sharpness/README.md | 130 +++++++++++ .../SOURCES.json | 30 +++ .../multiplicative-shell-sharpness/TASK.json | 89 +++++++ .../VERIFY.json | 34 +++ .../multiplicative-shell-sharpness/verify.py | 221 ++++++++++++++++++ 6 files changed, 622 insertions(+) create mode 100644 research/multiplicative-shell-sharpness/PROOF.md create mode 100644 research/multiplicative-shell-sharpness/README.md create mode 100644 research/multiplicative-shell-sharpness/SOURCES.json create mode 100644 research/multiplicative-shell-sharpness/TASK.json create mode 100644 research/multiplicative-shell-sharpness/VERIFY.json create mode 100644 research/multiplicative-shell-sharpness/verify.py diff --git a/research/multiplicative-shell-sharpness/PROOF.md b/research/multiplicative-shell-sharpness/PROOF.md new file mode 100644 index 0000000000..e7a86617c1 --- /dev/null +++ b/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^l0 it follows by multiplying the preceding strict inequality +M^(a_b-1)G_b=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. diff --git a/research/multiplicative-shell-sharpness/README.md b/research/multiplicative-shell-sharpness/README.md new file mode 100644 index 0000000000..f3ec3367a8 --- /dev/null +++ b/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. diff --git a/research/multiplicative-shell-sharpness/SOURCES.json b/research/multiplicative-shell-sharpness/SOURCES.json new file mode 100644 index 0000000000..6ae45512f4 --- /dev/null +++ b/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" + } + ] +} diff --git a/research/multiplicative-shell-sharpness/TASK.json b/research/multiplicative-shell-sharpness/TASK.json new file mode 100644 index 0000000000..ece6a5cddd --- /dev/null +++ b/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." + } + ] +} diff --git a/research/multiplicative-shell-sharpness/VERIFY.json b/research/multiplicative-shell-sharpness/VERIFY.json new file mode 100644 index 0000000000..37632ed40c --- /dev/null +++ b/research/multiplicative-shell-sharpness/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact independent monoid counts, constructive shell injections, exact free-monoid formula and rejection controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "The same proof-relevant checks with Python assertions disabled." + } + ] +} diff --git a/research/multiplicative-shell-sharpness/verify.py b/research/multiplicative-shell-sharpness/verify.py new file mode 100644 index 0000000000..60311371b2 --- /dev/null +++ b/research/multiplicative-shell-sharpness/verify.py @@ -0,0 +1,221 @@ +"""Exact corroboration of the shell lower theorem; standard library, no writes.""" + +import hashlib +import itertools +import json +import math +from fractions import Fraction +from pathlib import Path + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def valuations(number): + require(type(number) is int and 1 <= number <= 128, "integer domain") + row = [] + for prime in (2, 3, 5, 7, 11, 13): + exponent = 0 + for _ in range(8): + if number % prime: + break + number //= prime + exponent += 1 + row.append(exponent) + require(number == 1, "unsupported prime") + return tuple(row) + + +def rank(rows): + require(len(rows) <= 8, "rank row limit") + require(all(len(row) == 6 for row in rows), "valuation row shape") + work = [[Fraction(x) for x in row] for row in rows] + pivot = 0 + for column in range(6): + candidates = [i for i in range(pivot, len(work)) if work[i][column]] + if not candidates: + continue + selected = candidates[0] + work[pivot], work[selected] = work[selected], work[pivot] + divisor = work[pivot][column] + work[pivot] = [x / divisor for x in work[pivot]] + for i in range(pivot + 1, len(work)): + factor = work[i][column] + work[i] = [x - factor * y for x, y in zip(work[i], work[pivot])] + pivot += 1 + return pivot + + +def independent_generators(base, alphabet): + require(type(base) is int and 2 <= base <= 16, "base domain") + require(len(alphabet) <= 6, "alphabet limit") + rows = [valuations(base)] + chosen = [] + for generator in alphabet: + row = valuations(generator) + if rank(rows + [row]) > len(rows): + rows.append(row) + chosen.append(generator) + require(rank(rows) == len(rows), "independent basis") + return tuple(chosen) + + +def ceil_log(base, value): + require(2 <= base <= 16 and 1 <= value <= 128, "logarithm domain") + power = 1 + for exponent in range(value.bit_length() + 1): + if power >= value: + return exponent + power *= base + raise ValueError("ceil logarithm bound") + + +def lift(base, level, raw): + require(2 <= base <= 16 and 0 <= level <= 16, "lift domain") + require(1 <= raw < base ** (level + 1), "strict upper endpoint") + result = raw + for _ in range(level + 1): + if result >= base ** level: + require(result < base ** (level + 1), "shell overshoot") + return result + result *= base + raise ValueError("lift iteration bound") + + +def lower_witnesses(base, level, chosen): + require(0 <= level <= 16 and len(chosen) <= 3, "witness domain") + rows = [valuations(x) for x in (base,) + chosen] + require(rank(rows) == len(rows), "dependent generators") + heights = tuple(ceil_log(base, x) for x in chosen) + height = max(heights, default=1) + radius = level // height + witnesses = [] + for exponents in itertools.product(range(radius + 1), repeat=len(chosen)): + if sum(exponents) <= radius: + raw = math.prod(g ** b for g, b in zip(chosen, exponents)) + witnesses.append(lift(base, level, raw)) + expected = math.comb(radius + len(chosen), len(chosen)) + require(len(witnesses) == expected, "stars and bars count") + require(len(set(witnesses)) == expected, "injective shell map") + return set(witnesses) + + +def closure(generators, upper): + require(1 < upper <= 1_000_000, "closure capacity") + require(len(generators) <= 7 and all(type(g) is int and 1 <= g <= 128 + for g in generators), "generator domain") + members = {1} + for generator in generators: + if generator == 1: + continue + previous = tuple(members) + for value in previous: + power = value + for _ in range(upper.bit_length()): + if power >= upper: + break + members.add(power) + power *= generator + return members + + +def literal_members(generators, upper): + require(1 < upper <= 8_000, "literal capacity") + require(len(generators) <= 7 and all(type(g) is int and 1 <= g <= 128 + for g in generators), "generator domain") + reachable = bytearray(upper) + reachable[1] = 1 + for value in range(2, upper): + reachable[value] = any( + g > 1 and value % g == 0 and reachable[value // g] + for g in generators + ) + return {value for value in range(1, upper) if reachable[value]} + + +def check_alphabets(): + counts = {"alphabets": 0, "shells": 0, "lower_witnesses": 0} + alphabets = [a for size in range(3) + for a in itertools.combinations(range(2, 13), size)] + alphabets += [(1, 2, 3), (2, 3, 5), (4, 6, 9), (6, 10, 15), (6, 35, 77)] + for base, alphabet in itertools.product(range(2, 7), alphabets): + generators = (base,) + alphabet + chosen = independent_generators(base, alphabet) + require(rank([valuations(g) for g in generators]) == len(chosen) + 1, + "basis spans alphabet") + upper = base ** 5 + members = closure(generators, upper) + require(members == literal_members(generators, upper), "monoid oracles") + previous_count = 0 + for level in range(5): + shell = {x for x in members if base ** level <= x < base ** (level + 1)} + witnesses = lower_witnesses(base, level, chosen) + require(witnesses <= shell, "new constructive lower bound") + require(len(shell) >= previous_count, "multiplication injection") + previous_count = len(shell) + counts["shells"] += 1 + counts["lower_witnesses"] += len(witnesses) + counts["alphabets"] += 1 + return counts + + +def check_free_shells(): + counts = {"free_shells": 0, "free_points": 0} + for base, chosen in ((2, (3,)), (4, (3,)), (6, (10,)), (2, (3, 5)), + (4, (6, 5)), (3, (2, 7)), (2, ())): + require(rank([valuations(x) for x in (base,) + chosen]) == len(chosen) + 1, + "free model independence") + for level in range(7): + upper = base ** (level + 1) + if upper > 1_000_000: + continue + raw_products = closure(chosen, upper) + images = {lift(base, level, raw) for raw in raw_products} + complete = closure((base,) + chosen, upper) + shell = {x for x in complete if base ** level <= x < upper} + require(images == shell and len(images) == len(raw_products), + "exact free-monoid shell formula") + counts["free_shells"] += 1 + counts["free_points"] += len(images) + return counts + + +def check_controls(): + cases = ((independent_generators, (1, (2,))), + (independent_generators, (2, (17,))), + (independent_generators, (2, (2,) * 7)), + (lower_witnesses, (2, 4, (4,))), + (lower_witnesses, (2, -1, (3,))), + (lift, (2, 4, 32)), (closure, ((2,), 1_000_001))) + for function, arguments in cases: + try: + function(*arguments) + except ValueError: + continue + raise ValueError("negative control accepted") + require(not {x for x in closure((3,), 8) if 4 <= x < 8}, + "omitting the base can leave an empty shell") + require(lower_witnesses(4, 3, ()) == {64}, "rank-one boundary") + return len(cases) + 2 + + +def main(): + counts = check_alphabets() + counts.update(check_free_shells()) + counts["controls"] = check_controls() + package = Path(__file__).resolve().parent + names = ("README.md", "PROOF.md", "SOURCES.json", "TASK.json", "VERIFY.json", "verify.py") + hashes = {} + for name in names: + path = package / name + require(not path.is_symlink() and path.stat().st_size <= 524_288, + "package source capacity") + hashes[name] = hashlib.sha256(path.read_bytes()).hexdigest() + print(json.dumps({"status": "PASS_MULTIPLICATIVE_SHELL_SHARPNESS", + "counts": counts, "sha256": hashes}, sort_keys=True)) + + +if __name__ == "__main__": + main()