From f0d9e8d112359c17c66b84bcc4786fb65f1516af Mon Sep 17 00:00:00 2001 From: JoyboyBrian <122925040+JoyboyBrian@users.noreply.github.com> Date: Tue, 27 Oct 2026 22:10:37 -0700 Subject: [PATCH] Prove adaptive compiler shell bound and bind p16 width envelope --- research/adaptive-shell-width/PROOF.md | 182 ++++++++++++ research/adaptive-shell-width/README.md | 128 ++++++++ research/adaptive-shell-width/SOURCES.json | 54 ++++ research/adaptive-shell-width/TASK.json | 102 +++++++ research/adaptive-shell-width/VERIFY.json | 39 +++ research/adaptive-shell-width/verify.py | 327 +++++++++++++++++++++ 6 files changed, 832 insertions(+) create mode 100644 research/adaptive-shell-width/PROOF.md create mode 100644 research/adaptive-shell-width/README.md create mode 100644 research/adaptive-shell-width/SOURCES.json create mode 100644 research/adaptive-shell-width/TASK.json create mode 100644 research/adaptive-shell-width/VERIFY.json create mode 100644 research/adaptive-shell-width/verify.py diff --git a/research/adaptive-shell-width/PROOF.md b/research/adaptive-shell-width/PROOF.md new file mode 100644 index 0000000000..39f9caa6bf --- /dev/null +++ b/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=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=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, 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^g1, 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. diff --git a/research/adaptive-shell-width/README.md b/research/adaptive-shell-width/README.md new file mode 100644 index 0000000000..deab225e95 --- /dev/null +++ b/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. diff --git a/research/adaptive-shell-width/SOURCES.json b/research/adaptive-shell-width/SOURCES.json new file mode 100644 index 0000000000..f7d3d1576d --- /dev/null +++ b/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" + } + ] +} diff --git a/research/adaptive-shell-width/TASK.json b/research/adaptive-shell-width/TASK.json new file mode 100644 index 0000000000..f49cab354f --- /dev/null +++ b/research/adaptive-shell-width/TASK.json @@ -0,0 +1,102 @@ +{ + "schema_version": 1, + "task_id": "formal-interface-lemma", + "priority_revision": 8, + "base_commit": "721c03822c421b7f7fcbb2598993b947c4d88419", + "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 an effective multiplicative-shell lemma and apply it to the unchanged adaptive chronological compiler level-LCM divisor, answering PR5962 Open next question 1.", + "scope_change_reason": "The formal-interface card is narrowed to a written compiler-size lemma with exact caller and source binding, not a proof-assistant arithmetic formalization. The actual caller is PR4638 adaptive compile_widths, not selected6030 default strictification.", + "bottleneck_link": "A missing compiler-size implication: fixed-ratio shell counts reduce the proven upper envelope for one existing adaptive compiler, without changing its program or admitting physical costs.", + "budget_minutes": 60, + "stop_rule": "Stop at the first rigorous shell bound and its actual caller consequence; no parameter scan or selected compiler substitution.", + "outcome": "completed", + "evidence": "PROOF.md: quotient kernel and half-open fiber proof. verify.py: independent semigroup/minor oracles, 372 shell fixtures, 257 actual compiled ranks, source-bound p16 and ten rejecting controls.", + "author": "JoyboyBrian", + "ai_assistance": "Substantial OpenAI Codex assistance, including separate read-only AI proof review. No independent human or formal-kernel acceptance claimed.", + "open_questions": [ + { + "question": "Can a smaller shell constant or actual source-valuation information improve a named finite adaptive-width bound?", + "why_it_matters": "The effective constant K is conservative; an asymptotic degree improvement need not improve practical finite estimates.", + "first_step": "Retain the exact per-level source LCM and compare a justified tighter quotient box against it for the pinned p16 profile.", + "blocked_by": "The large winning template is not materialized, and no matching actual-width lower bound is known here." + }, + { + "question": "Can the improved adaptive width envelope replace a physical resource bound at an admitted caller?", + "why_it_matters": "Compiler width alone does not price routing, temporary storage or precision.", + "first_step": "Bind one emitted adaptive program to native bank allocations and complete movement/scratch charges.", + "blocked_by": "Native execution, whole-job adapters, owned erasure and fixed-tape/precision contracts remain inherited." + } + ], + "canonical_discussion": "https://github.com/CrocSwap/integer-mult-bounds/discussions/6076" +} diff --git a/research/adaptive-shell-width/VERIFY.json b/research/adaptive-shell-width/VERIFY.json new file mode 100644 index 0000000000..1092b6183b --- /dev/null +++ b/research/adaptive-shell-width/VERIFY.json @@ -0,0 +1,39 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/adaptive-chronological-batching/batching.py", + "research/compact-joint-compiler/arithmetic/RESULT.json", + "research/rank-convergence/BENCHMARKS.json", + "research/adaptive-chronological-batching/WIDTH.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 30, + "checks": "Exact shell/fiber inequalities, independent semigroup and minor oracles, source-bound p16 profile, unchanged adaptive compiler fixtures and semantic controls" + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 30, + "checks": "Same mathematical checks under optimized Python; no assertions carry validation" + } + ] +} diff --git a/research/adaptive-shell-width/verify.py b/research/adaptive-shell-width/verify.py new file mode 100644 index 0000000000..454bb25e57 --- /dev/null +++ b/research/adaptive-shell-width/verify.py @@ -0,0 +1,327 @@ +#!/usr/bin/env python3 +"""Exact bounded shell/caller checks. JoyboyBrian, Codex assistance; Apache-2.0.""" +from collections import defaultdict +from fractions import Fraction +from hashlib import sha256 +from itertools import combinations, permutations +import json +from math import lcm, prod +from pathlib import Path +from types import ModuleType + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parents[1] + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def factors(n): + need(type(n) is int and n >= 1, 'positive integer generator') + result = {} + p = 2 + while p*p <= n: + while n % p == 0: + result[p] = result.get(p, 0)+1 + n //= p + p += 1 + if n > 1: + result[n] = result.get(n, 0)+1 + return result + + +def pivots(matrix): + """Rational elimination; returns independent column indices.""" + rows = [list(map(Fraction, row)) for row in matrix] + if not rows: + return [] + out = [] + for j in range(len(rows[0])): + pivot = next((i for i in range(len(out), len(rows)) if rows[i][j]), None) + if pivot is None: + continue + k = len(out) + rows[k], rows[pivot] = rows[pivot], rows[k] + a = rows[k][j] + rows[k] = [x/a for x in rows[k]] + for i in range(k+1, len(rows)): + a = rows[i][j] + rows[i] = [x-a*y for x, y in zip(rows[i], rows[k])] + out.append(j) + return out + + +def rank(matrix): + return len(pivots(matrix)) + + +def determinant(matrix): + """Independent integer Bareiss determinant for the full-rank p16 minor.""" + a = [list(row) for row in matrix] + sign, previous = 1, 1 + for k in range(len(a)-1): + j = next((j for j in range(k, len(a)) if a[j][k]), None) + if j is None: + return 0 + if j != k: + a[k], a[j] = a[j], a[k] + sign = -sign + pivot = a[k][k] + for i in range(k+1, len(a)): + for j in range(k+1, len(a)): + value = a[i][j]*pivot-a[i][k]*a[k][j] + need(value % previous == 0, 'Bareiss exact division') + a[i][j] = value//previous + a[i][k] = 0 + previous = pivot + return sign*a[-1][-1] if a else 1 + + +def minor_rank(matrix): + """Independent Leibniz minors for small test matrices.""" + def det(a): + total = 0 + for order in permutations(range(len(a))): + sign = (-1)**sum(order[i] > order[j] + for i in range(len(a)) for j in range(i+1, len(a))) + total += sign*prod(a[i][order[i]] for i in range(len(a))) + return total + for size in range(min(len(matrix), len(matrix[0])), 0, -1): + for rs in combinations(range(len(matrix)), size): + for cs in combinations(range(len(matrix[0])), size): + if det([[matrix[i][j] for j in cs] for i in rs]): + return size + return 0 + + +def descriptor(alphabet, M): + need(type(M) is int and M >= 2, 'fixed height base at least two') + need(bool(alphabet), 'nonempty alphabet') + generators = sorted(set(alphabet) | {M}) + valuations = [factors(a) for a in generators] + primes = sorted(set().union(*(v.keys() for v in valuations))) + matrix = [[v.get(p, 0) for v in valuations] for p in primes] + m = [factors(M).get(p, 0) for p in primes] + pivot = min((i for i in range(len(m)) if m[i]), key=lambda i: m[i]) + q = m[pivot] + quotient = [[q*x-m[i]*y for x, y in zip(matrix[i], matrix[pivot])] + for i in range(len(primes))] + chosen = [] + for i, row in enumerate(quotient): + if rank([quotient[j] for j in chosen]+[row]) > len(chosen): + chosen.append(i) + r = rank(matrix) + need(len(chosen) == r-1, 'quotient rank r minus one') + h = (M-1).bit_length() + K = q*prod(h*(q+m[i])+1 for i in chosen) + return {'generators': generators, 'primes': primes, 'matrix': matrix, + 'm': m, 'pivot': pivot, 'q': q, 'chosen': chosen, 'r': r, + 'h': h, 'K': K} + + +def products(generators, cap): + seen, todo = {1}, [1] + while todo: + a = todo.pop() + for g in generators: + b = a*g + if b <= cap and b not in seen: + seen.add(b) + todo.append(b) + return seen + + +def divisibility_oracle(generators, cap): + reached = {1} + for n in range(2, cap+1): + if any(g > 1 and n % g == 0 and n//g in reached for g in generators): + reached.add(n) + return reached + + +def floor_log(n, M): + ell = 0 + while n >= M: + n //= M + ell += 1 + return ell + + +def shell_fixture(alphabet, M, cap): + d = descriptor(alphabet, M) + members = products(d['generators'], cap) + need(members == divisibility_oracle(d['generators'], cap), 'independent semigroup') + if len(d['matrix']) <= 4 and len(d['generators']) <= 4: + need(d['r'] == minor_rank(d['matrix']), 'independent rank minors') + shells = defaultdict(list) + for value in members: + shells[floor_log(value, M)].append(value) + fiber_cases = 0 + for ell, values in shells.items(): + groups = defaultdict(list) + for value in values: + v = factors(value) + x = [v.get(p, 0) for p in d['primes']] + F = tuple(d['q']*x[i]-d['m'][i]*x[d['pivot']] for i in d['chosen']) + need(all(-d['m'][i]*d['h']*(ell+1) <= f <= d['q']*d['h']*(ell+1) + for i, f in zip(d['chosen'], F)), 'integer quotient box') + groups[F].append(x) + need(len(values) <= d['K']*(ell+1)**(d['r']-1), 'shell envelope') + for xs in groups.values(): + need(len(xs) <= d['q'], 'half-open shell fiber') + need(len({x[d['pivot']] for x in xs}) == len(xs), 'fiber pivot injectivity') + first = xs[0] + for x in xs: + need(all(d['q']*(x[i]-first[i]) == + d['m'][i]*(x[d['pivot']]-first[d['pivot']]) + for i in range(len(x))), 'quotient kernel') + fiber_cases += 1 + return len(members), len(shells), fiber_cases + + +def authenticate(data, digest): + need(sha256(data).hexdigest() == digest, 'source hash mismatch') + return data + + +def inputs(): + sources = json.loads((PACKAGE/'SOURCES.json').read_text()) + return {row['path']: authenticate((ROOT/row['path']).read_bytes(), row['sha256']) + for row in sources['files'] if row['usage'] == 'input'} + + +def source_profile(source): + benchmark = json.loads(source['research/rank-convergence/BENCHMARKS.json']) + case = next(c for c in benchmark['cases'] if c['name'] == 'p16') + need(case['source'] == 'research/compact-joint-compiler/arithmetic/RESULT.json' + and case['profile_key'] is None, 'exact p16 profile path') + raw = json.loads(source[case['source']]) + targets = {int(k): v for k, v in raw['targets'].items()} + paid = {int(k): v for k, v in raw['paid'].items()} + witness = case['witness'] + M, g = witness['height_base'], witness['a']+witness['b'] + need((max(targets), min(targets), M, g, sum(targets.values()), sum(paid.values())) + == (145, 4, 1024, 2, 10928, 64620), 'exact p16 geometry') + need(paid.get(1, 0) > 0 and max(paid) < max(targets), 'nonempty decreasing rule') + d = descriptor(set(targets) | set(paid), M) + need(d['primes'] == [2, 3, 5, 7, 11, 13, 17, 19, 29, 41, 73] + and d['r'] == 11, 'p16 augmented rank') + cols = pivots(d['matrix']) + det = determinant([[row[j] for j in cols] for row in d['matrix']]) + need(det != 0, 'independent full-rank p16 minor') + need(M**2 == min(targets)**(5*g) and min(targets)**g < M, 'exact z equals three fifths') + return {'name': 'p16', 'r': d['r'], 'prime_count': len(d['primes']), + 'minor': det, 'z': '3/5', 'old_log_degree': 12, 'new_log_degree': 11, + 'shell_K': d['K'], 'changed_compiler': False} + + +def caller_cases(source): + module = ModuleType('retained_adaptive_batching') + path = 'research/adaptive-chronological-batching/batching.py' + exec(compile(source[path], path, 'exec'), module.__dict__) + cases = [({2: 1, 5: 1}, {1: 2, 4: 1}, 2, 2, 100), + ({2: 1, 5: 1}, {1: 2, 4: 1}, 16, 2, 100), + ({6: 1, 36: 1}, {1: 1, 6: 1}, 36, 2, 100)] + checked, cut_count = 0, 0 + regimes = set() + for targets, paid, M, g, N in cases: + m, k0 = max(targets), min(targets) + need(paid.get(1, 0) > 0, 'paid rank one') + d = descriptor(set(targets) | set(paid), M) + result = module.compile_widths(targets, paid, N, ('adaptive', M, 1, g-1)) + cap = N//m + starts = products(d['generators'], cap) + level_sources = defaultdict(list) + for gamma in starts: + ell = floor_log(gamma, M) + flow = module.census(targets, paid, gamma, g*ell) + S = sum(flow['sources'].values()) + need(0 < S <= sum(targets.values())*(sum(targets.values())+sum(paid.values()))**(g*ell), + 'retained source bound') + level_sources[ell].append(S) + Q, bit_bound = 1, 0 + w = (sum(targets.values())-1).bit_length() + v = (sum(targets.values())+sum(paid.values())-1).bit_length() + for ell in range(floor_log(cap, M)+1): + lo, hi = m*M**ell, min(N, m*M**(ell+1)-1) + delta = min(M**ell, k0**(g*ell+1)) + visits = 0 if hi < lo else 1+(hi-lo)//delta + level_lcm = lcm(*level_sources[ell]) + Q *= level_lcm**visits + bit_bound += d['K']*visits*(ell+1)**(d['r']-1)*(w+g*ell*v) + need((Q-1).bit_length() <= bit_bound, 'explicit symbolic shell bit envelope') + for n, B in enumerate(result['widths']): + need(Q % B == 0, 'actual compiler all-prime divisor') + need((B-1).bit_length() <= bit_bound, 'actual compiler width envelope') + if n < m: + continue + flow = result['flows'][(n//m, module.height(('adaptive', M, 1, g-1), targets, n))] + representative = max(gamma for gamma in starts if gamma <= n//m) + S = sum(module.census(targets, paid, representative, + g*floor_log(representative, M))['sources'].values()) + need(S == sum(flow['sources'].values()), 'source plateau binding') + delta = min(n//m, k0**(flow['height']+1)) + for child, count in module.batch_rows(flow, n): + need(0 <= child < n and n-child >= delta and count > 0, 'actual child decrement') + cut_count += 1 + checked += 1 + regimes.add('z=0' if k0**g >= M else 'z>0') + need(regimes == {'z=0', 'z>0'}, 'both growth regimes') + return {'fixtures': len(cases), 'compiled_ranks': checked, 'batch_rows': cut_count} + + +def controls(source): + rejected = 0 + def reject(f): + nonlocal rejected + try: + f() + except ValueError: + rejected += 1 + else: + raise ValueError('negative control accepted') + reject(lambda: descriptor([2], 1)) + reject(lambda: descriptor([0], 4)) + reject(lambda: descriptor([], 4)) + reject(lambda: authenticate(b'changed', sha256(b'original').hexdigest())) + d = descriptor([2], 4) + reject(lambda: need(len(products(d['generators'], 3)) <= 1, 'omit fiber multiplicity')) + d = descriptor([6], 2) + reject(lambda: need(d['r'] == rank([[1], [1]]), 'omit height-base direction')) + d = descriptor([2, 3], 4) + reject(lambda: need(len([]) == d['r']-1, 'omit quotient coordinate')) + reject(lambda: need(len({1, 4}) <= 1, 'close both ends of rank-one shell')) + reject(lambda: need(4**2 < 16, 'apply geometric sum at z zero')) + d = descriptor([2, 5, 3], 4) + reject(lambda: need(d['r'] == descriptor([2, 5], 4)['r'], 'omit paid generator')) + return rejected + + +def main(): + source = inputs() + members = shells = fibers = fixtures = 0 + for size in (1, 2, 3): + for alphabet in combinations(range(2, 10), size): + for M in (2, 3, 4, 6): + a, b, c = shell_fixture(alphabet, M, 4096) + members += a + shells += b + fibers += c + fixtures += 1 + for alphabet, M in [([6], 36), ([6, 36], 36), ([4, 8], 16), ([6, 10], 12)]: + a, b, c = shell_fixture(alphabet, M, 65536) + members += a + shells += b + fibers += c + fixtures += 1 + report = {'status': 'PASS_ADAPTIVE_SHELL_WIDTH', 'shell_fixtures': fixtures, + 'member_occurrences': members, 'shells': shells, 'fibers': fibers, + 'caller': caller_cases(source), 'p16': source_profile(source), + 'controls_rejected': controls(source)} + print(json.dumps(report, sort_keys=True, indent=2)) + + +if __name__ == '__main__': + main()