diff --git a/research/rank-sensitive-mirror/PROOF.md b/research/rank-sensitive-mirror/PROOF.md new file mode 100644 index 0000000000..31bf8ec277 --- /dev/null +++ b/research/rank-sensitive-mirror/PROOF.md @@ -0,0 +1,285 @@ +# Rank-sensitive complement capacity for the capped mirror flow + +This contribution is produced by Nick Petalas. Apache-2.0. + +Claim type: scoped written mathematical proof with exact finite corroboration. +The capped-flow and normalized recurrence contracts are cited premises. No +native unit realizing the example, physical supplier, new kappa, or complete +multiplication theorem is supplied. + +## 1. Premises and the new source charge + +Use zxv's arbitrary-height capped flow from PR4436/4483 and Ryanson Jonathan's +corrected PR4459 mirror identity. Dillon Amburgey's PR4532 supplies the +critical-root tail construction and shifted-logarithmic majorant. These results +are used as premises, without auditing or replaying their examples. + +The nonempty integer histograms have target ranks `2 <= k <= m=max(k)` and +paid ranks `1 <= r < m`, with multiplicities `W_k` and `P_r`. Let + +```text +T(t) = sum_k W_k k^t, P(t) = sum_r P_r r^t, +0 < t < 1, C = floor(n/m). +``` + +Fix a real ambient scale `Lambda>m`. Restrict to integers `n` for which +`n<=Lambda C`. It suffices that `C >= (m-1)/(Lambda-m)`, since +`n<=mC+m-1`. This is a finite base-range restriction, not a substitution +of `n/m` for the integer cutoff. + +The cited mirror identity expresses every inner source through a pair `k>r` +and an integer base product `z`, in the window + +```text +C/k < z <= C/r, source rank s=rkz. +``` + +Consequently `s>rC>=rn/Lambda`. For the pure power, concavity gives + +```text +n^t-(n-s)^t >= t n^(t-1) s >= eta_r(t) s^t, +eta_r(t) := t (r/Lambda)^(1-t). (1) +``` + +The inequality includes `s=n`. Every source rank is at most `n`, by the +inherited flow contract. The usual uniform charge uses only `eta_1`; (1) +retains the paid letter `r` attached to that particular source window. + +The same charge works for the shifted-logarithmic function + +```text +f(0)=0, f(x)=A x^theta (c+log x)^p for x>=1, +tau(x)=theta+p/(c+log x), 0=p/(1-theta). +``` + +Indeed `f` is increasing and concave on `[1,infinity)`, `tau<=1`, and +`f'(x)=tau(x)f(x)/x`. For integer `1<=s=tau(n)f(n)s/n`. For `s=n`, use `f(0)=0` and `tau(n)<=1`. +Thus, at `t=tau(n)`, + +```text +[f(n)-f(n-s)]/f(n) >= eta_r(t) (s/n)^t. (2) +``` + +This is the new replacement for the uniform source-capacity step. It does +not alter the flow, its paid positions, or the productive boundary. + +## 2. Weighted mirror inequality and complete leaf funding + +Partition the `y=z/C` axis at the endpoints `1/k,1/r`, using the inherited +half-open windows. Write + +```text +E_J(t) = sum_(r>k, J subset (1/r,1/k]) P_r W_k (rk)^t, +S_(J,r)(t) = sum_(k>r, J subset (1/k,1/r]) P_r W_k (rk)^t, +D_J(t) = sum_r eta_r(t) S_(J,r)(t). +``` + +Suppose a constant `0<=b<1` satisfies + +```text +E_J(t) <= b D_J(t) for every elementary cell J. (3) +``` + +A zero `D_J` must have zero `E_J`. Let `K_t` be the sum of `eta_r(t)s^t` +over all actual inner sources, with their multiplicities, and let `I_t` +be their ordinary `t`-potential. Integrating (3) against the exact +nonnegative capped base measure gives + +```text +B_t <= b K_t, K_t >= eta I_t, +eta := eta_1(t) in (0,1). (4) +``` + +Here `B_t` is boundary-exit potential. There is no assumed density, +equidistribution, or limit measure. The actual nonlinear complement capacity +dominates `K_t` after the common normalization in (2). + +Let `F_t` be leaf-exit potential and `A_t` the net occupation surplus after +root sources. The cited exact cancellation is + +```text +I_t = B_t + F_t + A_t. +``` + +The new sufficient funding implication is + +```text +A_t >= 0 and (1-b) eta A_t >= (1-eta) F_t + imply B_t+F_t <= K_t. (5) +``` + +To prove it, suppose `K_t=eta I_t>eta(K_t+A_t)`, hence +`(1-eta)K_t>eta A_t`. Also (4) gives +`F_t>K_t-B_t>=(1-b)K_t`. Multiplying these inequalities contradicts +the hypothesis of (5). This proof uses no division by `F_t` and covers +zero leaf or boundary mass. With (2), exit charge is therefore funded by +the actual inner-source complement capacity. Root complement capacities +are nonnegative and remain available. + +In particular, the inherited bounds + +```text +F_t <= P(t)^(G+1), A_t >= Q_ell(t) P(t)^(G+1) +``` + +are sufficient whenever + +```text +Q_ell(t) >= (1-eta)/((1-b)eta). (6) +``` + +Leaves have not been dropped. Condition (6) replaces the uniform mirror +threshold; it does not assert that a favorable mirror test alone funds a flow. + +Allowing `Lambda>m` to be chosen makes this a weaker sufficient mirror test. +Indeed, if the old uniform ratio is `beta=1`, +`D_J>=eta_1 S_J`, so (3) holds with `b=beta/eta_1<1`. The example below +proves that the converse fails. No inclusion is asserted for an arbitrary +fixed, excessively large value of `Lambda`. + +## 3. Critical-root corollary + +Assume the same finite-flow and normalized recurrence contracts as PR4532. +Suppose, for some `theta in (0,1)`, + +```text +T(theta)=P(theta), +mu_T(theta)>mu_P(theta), +E_J(theta)<=b_* D_J(theta) for every J, with b_*<1. (7) +``` + +Then there exist positive `A,c,p` and an integer base cutoff `n0` such that +the conditional normalized leaf recurrence has + +```text +L(0)=0, L(n)<=A n^theta(c+log n)^p for all n>=1. (8) +``` + +The following specifies exactly which predecessor steps are used and which +capacity step changes. The moment crossing and positive mean gap give positive +integers `a,b_h`, an integer height base `M>1`, and positive rational tail +parameters `s_0,lambda` as in PR4532 section 2.1--2.2. The mixed and root +tail factors are strictly below one, and forward ratio ordering holds. +This tail argument uses the mean gap, not mirror capacity. + +Every nonzero `D_J(t)` is positive and continuous near `theta`; identically +zero source cells have no exit under (7). Choose `b_bar` strictly between +`b_*` and one. On a sufficiently short right interval at `theta`, (3) +holds with `b_bar`, both tails are bounded by constants `U,V<1`, and +`d(log(T/P))/dt>=d>0`. Also + +```text +eta_1'(t) = Lambda^(t-1)(1+t log Lambda)>0, +eta_1(t)>=eta_*:=eta_1(theta)>0. +``` + +The inherited shifted-logarithmic occupation estimate is + +```text +Q_ell(tau(n)) >= +(1-U^ell)(exp(K_ell)-1)-Q M^lambda V^ell, +K_ell = d p(a ell+1)/(c+log m+(ell+1)log M+log 2), +``` + +where `Q` is a finite upper bound for `T/P` on that interval. This is the +same occupation/root-tail estimate, not a new invoice or tail inequality. +Its right side increases to `exp(dpa/log M)-1` as `ell` increases. Choose +`p` so that this limit exceeds + +```text +(1-eta_*)/((1-b_bar)eta_*). +``` + +Choose `c>=p/(1-theta)`, then a sufficiently large integer `ell0` so that +the occupation estimate exceeds this threshold, `tau(n)` lies in the +certified right interval, and `n<=Lambda floor(n/m)` above the base cutoff. +All these demands are finite. Increasing `ell0` preserves them. Put +`n0=m M^ell0` and use elementary evaluation through `n0`. + +For `n>n0`, set `ell=floor(log_M floor(n/m))`, so `ell>=ell0`. +The occupation estimate, monotonicity of `eta_1`, and (6) fund all exits +by the source capacities (2). The inherited exit comparison +`f(e)/f(n)<=(e/n)^tau(n)` applies unchanged. Choosing +`A=n0^(1-theta)/(c+log n0)^p` funds the elementary base range since `f/x` +is decreasing. Every recursive rank is strictly below `n`, so induction +proves (8). No predecessor native premise has been discharged. + +The mean gap is an explicit hypothesis in this corollary. The weighted +condition is not used to infer it. This avoids transferring PR4532's +unweighted integral argument to a different mirror inequality. + +## 4. Exact integer-histogram separation + +Take the abstract histograms + +```text +W_16=1, W_64=2; P_1=2, P_4=6, P_36=1; +theta=1/2, m=64, Lambda=289/4, sqrt(Lambda)=17/2. +``` + +Both moments at `theta` are exactly 20. Their tilted-log mean difference is + +```text +mu_T-mu_P = (19 log 2-3 log 3)/5 > 0, +``` + +since `2^19>3^3`. The only cell with exits is `(1/36,1/16]`. On it, + +```text +E=24, S_(J,1)=32, S_(J,4)=192, +E/S = 24/224 = 3/28 > 1/16. +``` + +Thus PR4532's uniform mirror hypothesis fails, even with its more favorable +ambient constant `m=64`. For the new charge, + +```text +eta_1=1/17, eta_4=2/17, +D_J=32/17+384/17=416/17, +E/D_J=51/52<1. +``` + +All other cells have zero exit coefficient. The floor guard holds uniformly +for `C>=8`, since `64C+63 <= (289/4)C`. In particular `n>=512` suffices. +The local mirror calculation uses exactly the cap and costs declared in +sections 1--2. + +There is also an exact two-tail positive control. Choose `a=b_h=1`, +`M=1024`, `s_0=lambda=1/2`. Then + +```text +T(1)=144, P(1)=62, T(0)=3, +u=1024^(-1/2)(144/20)(62/20)=279/400<1, +v=1024^(1/2)(3/20)^2=18/25<1, +144/20 > 62/20. +``` + +The corollary therefore applies to this abstract recurrence at exponent +`1/2`. This is not a native supplier with saving `1/2`. No native word +realizing these histograms has been given. + +At the exact exponent, (6)'s threshold is 832. The algebraic values +`B=51,F=1,A=832,I=884,K=52` attain every constraint in (4)--(6) and give +`K=B+F`. The shifted-log proof uses a strictly larger bound on a right +interval. The number 832 is not a claimed sufficient compiler height. + +## 5. Verification boundary + +The standalone verifier computes only this new toy profile and the new +capacity/funding implications. It uses exact rational and integer arithmetic. +It enumerates the toy's capped base measures in two ways and checks actual +nonlinear square-root complement capacities at 49 finite rank/height fixtures. +Those checks corroborate (1)--(6); (8) rests on the written argument and cited +flow/tail premises. No p7/p16 or selected native replay is performed. + +The contribution only replaces a sufficient complement-capacity test. It +does not solve the full distribution-dependent mirror question in PR4532, +prove an actual profile's physical costs, or discharge any of the selected +record's five inherited assumptions. Arbitrary-input native correctness, +ownership/restoration, chronological batch widths, adapters, movement, +precision, stock, tape execution, analytic transfer and exact recovery remain +separate obligations. Independent human and formal proof-kernel review are +unclaimed. diff --git a/research/rank-sensitive-mirror/README.md b/research/rank-sensitive-mirror/README.md new file mode 100644 index 0000000000..f13f5453be --- /dev/null +++ b/research/rank-sensitive-mirror/README.md @@ -0,0 +1,140 @@ +# Rank-sensitive mirror capacity admits a previously excluded profile + +This contribution is 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. +Keeping each inner source's paid rank, with a freely chosen ambient scale, +gives a strictly weaker sufficient +complement-capacity test for the conditional capped-flow compiler. The new +lemma includes leaf funding and a critical-root shifted-logarithmic corollary. +No native supplier or new kappa is claimed. + +## Result + +For target/paid ranks `k>r`, the exact source window has rank +`s=rkz>r floor(n/m)`. With `Lambda>m` and +`n<=Lambda floor(n/m)`, charge that source by + +```text +eta_r(t) s^t, eta_r(t)=t(r/Lambda)^(1-t). +``` + +The actual nonlinear complement capacity dominates this charge. Retain the +per-paid-rank mirror coefficients `S_(J,r)`, and replace the uniform mirror +comparison by + +```text +E_J(t) <= b sum_r eta_r(t) S_(J,r)(t), b<1. +``` + +If the occupation surplus and leaves also satisfy +`(1-b)eta_1 A_t >= (1-eta_1)F_t`, every exit is funded. A moment crossing, +an explicit positive tilted-mean gap, and this strict weighted mirror +condition imply the same conditional critical-exponent polylogarithmic +leaf bound as the predecessor. [PROOF.md](PROOF.md) gives the hypotheses +and argument, including integer floors and zero-leaf cases. + +The abstract integer histograms + +```text +targets: W_16=1, W_64=2 +paid: P_1=2, P_4=6, P_36=1 +theta=1/2, Lambda=289/4 +``` + +have equal moments of 20 and positive tilted-mean gap. The only exit cell +has coefficients `E=24`, `S_1=32`, `S_4=192`. The old uniform mirror +test fails because `3/28>1/16`. The new weighted ratio is `51/52<1`. +The floor guard holds for every `n>=512`. Exact tail factors `279/400` +and `18/25` give a separate positive control. This exhibits a strict +extension of a sufficient test, not a native saving of one half. + +## Reproduce + +From the repository root, using CPython 3.12 and only its standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/rank-sensitive-mirror/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/rank-sensitive-mirror/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/rank-sensitive-mirror +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/rank-sensitive-mirror --check-source-history +``` + +Replace the interpreter path with another CPython 3.12 installation as needed. +The direct verifier is read-only and Git-free. Its generated stdout receipt +binds all six package files by SHA256. Expected scientific marker: +`PASS_RANK_SENSITIVE_MIRROR`. + +The finite replay covers all mirror cells of this new toy, 49 capped-flow +fixtures at heights 1 through 7 and ranks `24^2,25^2,32^2,33^2,48^2,64^2,65^2`, +369 source-term checks across those fixtures, and 1,220 funding cases. +Two enumeration methods agree on the toy base measures. All nonlinear +square-root capacity comparisons are exact squared rational comparisons. +The nine semantic controls include a changed paid-rank distribution, +the strict-mirror equality boundary, the two sides of the cutoff guard, +four malformed profiles, and an uncovered source window. A separate +underfunding control retains the leaf charge. These finite checks corroborate +the written proof. They do not prove its universal conclusion by enumeration. + +## Scope and credit + +The question comes from Dillon Amburgey's +[PR4532](https://github.com/CrocSwap/integer-mult-bounds/pull/4532), Open next +question 1. The new step retains source rank inside complement capacity; +the full distribution-dependent measure question remains open. Cite zxv's +[PR4436](https://github.com/CrocSwap/integer-mult-bounds/pull/4436) and +[PR4483](https://github.com/CrocSwap/integer-mult-bounds/pull/4483) for the capped +flow and occupation estimates, Ryanson Jonathan's corrected +[PR4459](https://github.com/CrocSwap/integer-mult-bounds/pull/4459) for the mirror +identity, and Jacob Alan Sussman for the integer compiler. Dillon's +critical-root tail construction and shifted-logarithmic argument are cited +premises. Their retained native, geometry, helper, Cinna Davis and outer +contributors keep their credit. Concavity and weighted summation are classical. +No predecessor code, examples, counts or credit lines are modified or audited. + +The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19358858) +specifies the scope. Canonical base is +`7c49fe32c55de02c2c873655c804b16e4c3fef0a`, priority revision 8. +[TASK.json](TASK.json) declares the change from selected-assumption work to a +compiler side lemma; [SOURCES.json](SOURCES.json) pins historical provenance. +The verifier has no live predecessor input or executable dependency. + +The histograms are abstract. No native realizing word, chronological batch +width, physical caller, restoration, precision/tape/stock budget, supplier +admission or analytic recovery is supplied. The five selected framework +assumptions remain. The selected cold replay, native suites, Lean and Docker +are unrun. The corollary is conditional on the cited compiler/recurrence +contracts. It supplies no explicit useful base cutoff or physical cost bound. + +## Verifier bounds + +The verifier has no recursion, subprocess, network, external input, or +mutable global state. Functions stay below 60 physical lines. Every scientific +check uses an explicit exception and remains enabled under optimization. +The fixed workload has seven heights, seven ranks and six source-pair types. +The literal base enumerator has at most +`sum_(d=0)^6 3^d 2^(6-d)=2059` words at the largest height. +The receipt reads six regular files capped at 256 KiB each. + +Power-of-ten rule 3 has a managed-runtime deviation in `verify.py`: Python +allocates integers, fractions and collections during checking. The fixed +height/alphabet bounds limit live state; only one capped fixture is live at +a time. The largest product-law support has at most `3^7=2187` entries, +and the literal enumeration streams its words. Normal/optimized replay and +an AST/function-size inspection check this bounded design. Fixed storage +would require replacing Python's arithmetic/runtime, beyond this isolated +proof package. Reassess the bound before exposing configurable workloads. +Warning-strict execution is the available diagnostic; no separate Python +type checker or whole-repository static analysis is claimed. + +## Open next questions + +1. Can an actual native profile pass this test while failing the old one, + with a complete paid/target and physical bill? Start with its exact + per-paid-rank source cells and mean gap. A native realization and full + implementation budget are missing here. +2. Can the actual capped base measure weaken the new pointwise test further? + Start with a failing weighted cell and prove a uniform mass bound. + Finite sampled caps are insufficient. This is the remaining part of + PR4532's broader question. Structured questions are in TASK.json. diff --git a/research/rank-sensitive-mirror/SOURCES.json b/research/rank-sensitive-mirror/SOURCES.json new file mode 100644 index 0000000000..21191e17ab --- /dev/null +++ b/research/rank-sensitive-mirror/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a", + "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/adaptive-gate-existence/README.md", + "usage": "provenance", + "git_blob": "955d60830dc7d95316e2fd9c0ca5df1fbd1738ed", + "sha256": "02170ceba88fafac5a3f49f766b86c32972be71e071cad8be3ac1d9f17228b13" + }, + { + "path": "research/adaptive-gate-existence/PROOF.md", + "usage": "provenance", + "git_blob": "bdf142f26d8b01164c9db1c021f7385a9f11a7d6", + "sha256": "340d637feef40f44a808c718207c0fede12cc483e2c979b86c56bb736b9c1ef5" + }, + { + "path": "research/rank-convergence/PROOF.md", + "usage": "provenance", + "git_blob": "75f451837204bd141f357e7f5e5d6c6f42e1423e", + "sha256": "3c971c5670669cb36312815b111e64c83e1490a10ee82f5412bd9aee01e9c376" + } + ] +} diff --git a/research/rank-sensitive-mirror/TASK.json b/research/rank-sensitive-mirror/TASK.json new file mode 100644 index 0000000000..3b7f78dd9f --- /dev/null +++ b/research/rank-sensitive-mirror/TASK.json @@ -0,0 +1,101 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 8, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "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 a rank-sensitive capped-flow complement-capacity criterion and its complete leaf-funding implication; give an abstract integer-histogram separation from PR4532's uniform mirror criterion.", + "scope_change_reason": "This is a new compiler side lemma answering a direction in PR4532 Open next question 1. It does not discharge the selected compiler assumption at an actual native caller. The drawn BIT-helper card was not retained because its immediately available handoffs were audits or recent-account continuations.", + "bottleneck_link": "Retaining each source's paid rank weakens one sufficient compiler-admission condition without changing the native profile or deleting leaf costs. The missing native realizer prevents a supplier or kappa claim.", + "budget_minutes": 60, + "stop_rule": "Stop after the first exact separation and capacity/funding proof; package it without searching native profiles or optimizing constants.", + "outcome": "completed", + "evidence": "PROOF.md; generated hash-bound stdout receipt; exact 3/28 versus 1/16 and 51/52 witness; 49 new toy capped-flow fixtures, 369 source terms, 1220 funding cases and nine semantic controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Does an actual native target/paid profile fail uniform mirror capacity but pass the rank-sensitive condition with complete costs?", + "why_it_matters": "This would turn the new sufficient compiler lemma into a source-bound admission improvement.", + "first_step": "Bind one independent native word's exact histograms, compute its per-paid-rank source cells, and certify the new ratios and mean gap.", + "blocked_by": "No native realization or physical budget is supplied for the abstract example." + }, + { + "question": "Can integration against the actual capped base measure improve the rank-sensitive pointwise condition?", + "why_it_matters": "This retains the unresolved distribution-dependent part of PR4532's question.", + "first_step": "Retain the measure on a cell that fails the weighted condition and prove a uniform bound for its contribution.", + "blocked_by": "A uniform measure estimate, rather than sampled cap values, is needed." + } + ], + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19358858", + "claim_type": "scoped written mathematical proof with exact finite corroboration", + "question_source": { + "pull_request": 4532, + "author": "dillona", + "question": "Can a weaker bound against the actual capped measure replace strict pointwise mirror slack?", + "relationship": "A rank-sensitive sufficient source-capacity step; the full distribution-dependent question remains open." + }, + "environment": { + "python": "CPython 3.12.15", + "dependencies": "standard library only" + } +} diff --git a/research/rank-sensitive-mirror/VERIFY.json b/research/rank-sensitive-mirror/VERIFY.json new file mode 100644 index 0000000000..fbf53bd692 --- /dev/null +++ b/research/rank-sensitive-mirror/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": 60, + "checks": "Exact new toy histogram separation, cap/source capacity, full leaf funding and semantic controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Same complete finite scope with optimization; checks use explicit exceptions." + } + ] +} diff --git a/research/rank-sensitive-mirror/verify.py b/research/rank-sensitive-mirror/verify.py new file mode 100644 index 0000000000..3d41b5b0fa --- /dev/null +++ b/research/rank-sensitive-mirror/verify.py @@ -0,0 +1,230 @@ +#!/usr/bin/env python3 +"""Exact corroboration of the new rank-sensitive mirror lemma and toy profile. + +Produced by Nick Petalas. Apache-2.0. +The all-rank conclusion is the written proof, not this finite enumeration. +""" + +from collections import Counter +from fractions import Fraction as F +from hashlib import sha256 +from itertools import product +import json +from math import isqrt, prod +from pathlib import Path +import sys + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def root(rank): + require(type(rank) is int and 1 <= rank <= 4096, "rank outside finite domain") + value = isqrt(rank) + require(value * value == rank, "finite oracle requires square ranks") + return value + + +def validate(target, paid): + for histogram in (target, paid): + require(1 <= len(histogram) <= 8, "histogram size outside finite domain") + for rank, count in histogram.items(): + root(rank) + require(type(count) is int and 1 <= count <= 4096, "invalid count") + m = max(target) + require(min(target) >= 2 and max(paid) < m, "invalid target/paid ranks") + + +def mirror_cells(target, paid): + validate(target, paid) + endpoints = sorted({F(1, rank) for rank in (*target, *paid)}) + cells = [] + for lo, hi in zip(endpoints, endpoints[1:]): + point = (lo + hi) / 2 + exit_weight = 0 + sources = Counter() + for r, k in product(paid, target): + weight = paid[r] * target[k] * root(r) * root(k) + if r > k and F(1, r) < point <= F(1, k): + exit_weight += weight + if k > r and F(1, k) < point <= F(1, r): + sources[r] += weight + cells.append((lo, hi, exit_weight, dict(sources))) + return cells + + +def weighted_ratio(cells, sqrt_ambient): + require(sqrt_ambient > 0, "nonpositive ambient scale") + ratios = [] + for _, _, exit_weight, sources in cells: + capacity = sum((F(weight * root(r), 2) / sqrt_ambient + for r, weight in sources.items()), F(0)) + require(capacity > 0 or exit_weight == 0, "uncovered exit cell") + ratios.append(F(exit_weight) / capacity if capacity else F(0)) + return max(ratios) + + +def profile_fixture(): + target, paid = {16: 1, 64: 2}, {1: 2, 4: 6, 36: 1} + cells = mirror_cells(target, paid) + require(sum(c * root(k) for k, c in target.items()) == 20, "target moment") + require(sum(c * root(r) for r, c in paid.items()) == 20, "paid moment") + active = [row for row in cells if row[2]] + require(active == [(F(1, 36), F(1, 16), 24, {1: 32, 4: 192})], + "literal offending cell") + old_ratio = max(F(e, sum(s.values())) for _, _, e, s in cells) + require(old_ratio == F(3, 28) > F(1, 16), "old uniform mirror rejection") + require(weighted_ratio(cells, F(17, 2)) == F(51, 52), "new strict mirror") + require(2 ** 19 > 3 ** 3, "positive exact tilted-mean gap") + target_one = sum(k * c for k, c in target.items()) + paid_one = sum(r * c for r, c in paid.items()) + require((target_one, paid_one) == (144, 62), "shifted moments") + require(F(target_one * paid_one, 20 ** 2 * 32) == F(279, 400) < 1, + "mixed tail at a=b=1, M=1024, s=1/2") + require(32 * F(sum(target.values()), 20) ** 2 == F(18, 25) < 1, + "root tail at lambda=1/2") + require(F(target_one, 20) > F(paid_one, 20), "forward ratio ordering") + return target, paid, cells + + +def product_law(histogram, degree): + require(0 <= degree <= 7, "degree outside finite domain") + law = {1: 1} + for _ in range(degree): + next_law = Counter() + for value, rank in product(law, histogram): + next_law[value * rank] += law[value] * histogram[rank] + law = dict(next_law) + return law + + +def base_measure(target, paid, height): + require(1 <= height <= 7, "height outside finite domain") + measure = Counter() + for depth in range(height): + left = product_law(paid, depth) + right = product_law(target, height - depth - 1) + for a, b in product(left, right): + measure[a * b] += left[a] * right[b] + return dict(measure) + + +def literal_base(target, paid, height): + require(1 <= height <= 7, "height outside literal domain") + measure = Counter() + for depth in range(height): + for left in product(tuple(paid), repeat=depth): + for right in product(tuple(target), repeat=height - depth - 1): + weight = prod(paid[r] for r in left) * prod(target[k] for k in right) + measure[prod(left) * prod(right)] += weight + return dict(measure) + + +def integer_root(value): + require(type(value) is int and value >= 0, "invalid square argument") + result = isqrt(value) + require(result * result == value, "expected a literal square product") + return result + + +def capped_fixture(target, paid, height, sqrt_n): + n, m = sqrt_n ** 2, max(target) + cutoff = n // m + require(n <= F(289, 4) * cutoff, "ambient cutoff guard") + measure = base_measure(target, paid, height) + require(measure == literal_base(target, paid, height), "independent base enumeration") + inner, boundary, capacity, terms = 0, 0, F(0), 0 + for z, r, k in product(measure, paid, target): + weight = measure[z] * paid[r] * target[k] + rank = r * k * z + if k * z <= cutoff < r * z: + boundary += weight * integer_root(rank) + if r * z <= cutoff < k * z: + require(r * cutoff < rank <= n, "literal inner-source rank") + lower = F(root(r) * integer_root(rank), 17) + require(sqrt_n >= lower and (sqrt_n - lower) ** 2 >= n - rank, + "exact nonlinear complement dominates rank-sensitive charge") + capacity += weight * lower + inner += weight * integer_root(rank) + terms += 1 + require(boundary <= F(51, 52) * capacity, "weighted mirror integrated at cap") + require(capacity >= F(inner, 17), "minimum source capacity") + roots = 20 * sum(c * integer_root(z) for z, c in product_law(target, height).items() + if z <= cutoff) + leaves = 20 * sum(c * integer_root(z) for z, c in product_law(paid, height).items() + if z <= cutoff) + require(inner + roots == boundary + leaves, "new toy flow cancellation") + return terms + + +def funding_fixtures(): + eta, beta = F(1, 17), F(51, 52) + threshold = (1 - eta) / ((1 - beta) * eta) + require(threshold == 832, "complete leaf-funding threshold") + count = 0 + for leaf, surplus_extra, boundary in product(range(5), range(4), range(61)): + surplus = threshold * leaf + surplus_extra + capacity = max(eta * (boundary + leaf + surplus), F(boundary) / beta) + require(capacity >= boundary + leaf, "new funding implication") + count += 1 + require(eta * (51 + 1 + 832) == 52 and beta * 52 == 51, + "all-constraint equality fixture") + underfunded = eta * 832 / (1 - eta * beta) + require((1 - beta) * underfunded < 1, "one-unit underfunding control") + return count + + +def rejecting_controls(cells): + bad_cells = mirror_cells({16: 1, 64: 2}, {1: 4, 4: 5, 36: 1}) + require(weighted_ratio(bad_cells, F(17, 2)) > 1, "paid-rank distribution control") + require(weighted_ratio(cells, F(26, 3)) == 1, "strict mirror boundary control") + require(64 * 7 + 63 > F(289, 4) * 7, "insufficient cutoff control") + require(64 * 8 + 63 <= F(289, 4) * 8, "first uniform cutoff control") + rejected = 0 + for target, paid in (({1: 1}, {1: 1}), ({16: 1}, {36: 1}), + ({16: 0, 64: 2}, {1: 1}), ({17: 1, 64: 2}, {1: 1})): + try: + mirror_cells(target, paid) + except ValueError: + rejected += 1 + require(rejected == 4, "invalid input controls") + uncovered = mirror_cells({4: 1, 64: 2}, {16: 1}) + try: + weighted_ratio(uncovered, F(17, 2)) + except ValueError: + return 9 + raise ValueError("uncovered source window accepted") + + +def receipt(results): + directory = Path(__file__).resolve().parent + names = ("PROOF.md", "README.md", "SOURCES.json", "TASK.json", "VERIFY.json", "verify.py") + hashes = {} + for name in names: + path = directory / name + require(path.is_file() and not path.is_symlink(), "missing regular package file") + require(path.stat().st_size <= 262144, "package file exceeds receipt bound") + hashes[name] = sha256(path.read_bytes()).hexdigest() + return {"schema": "rank-sensitive-mirror-receipt/v1", "results": results, + "python": sys.version.split()[0], "files_sha256": hashes} + + +def main(): + target, paid, cells = profile_fixture() + terms = 0 + sizes = (24, 25, 32, 33, 48, 64, 65) + for height, sqrt_n in product(range(1, 8), sizes): + terms += capped_fixture(target, paid, height, sqrt_n) + results = {"old_mirror_ratio": "3/28", "old_uniform_capacity": "1/16", + "new_weighted_ratio": "51/52", "ambient_scale": "289/4", + "crossing_moment": 20, "mixed_tail": "279/400", "root_tail": "18/25", + "capped_flows": 49, "source_terms": terms, + "funding_cases": funding_fixtures(), "controls": rejecting_controls(cells)} + print(json.dumps(receipt(results), sort_keys=True)) + print("PASS_RANK_SENSITIVE_MIRROR " + json.dumps(results, sort_keys=True)) + + +if __name__ == "__main__": + main()