diff --git a/research/direct-flow-finite-tail/PROOF.md b/research/direct-flow-finite-tail/PROOF.md new file mode 100644 index 0000000000..3b6b4d4dd5 --- /dev/null +++ b/research/direct-flow-finite-tail/PROOF.md @@ -0,0 +1,148 @@ +# A finite-depth exponential envelope for the direct-flow leaf deficit + +This is a scoped written proof. The classical Berry–Esseen inequality is an +external theorem. The exact verifier checks the finite numerical hypotheses +and the rational constants below. It is not a formalization of this proof. + +## 1. Law and result + +Use Ryanson Jonathan / pinterbanget's PR #4467 paid law + +``` +P = {1:37305, 2:10695, 3:3360, 4:1530, 5:300, + 8:1464, 16:448, 32:448, 48:448} +W = {5:420, 6:270, 7:840, 8:1395, 9:3195, + 25:448, 41:448, 57:448, 121:224}. +``` + +Write Z(s)=sum_r P_r r^s and mu(s)=Z'(s)/Z(s). Let t be the invoice +root sum_k W_k k^t=Z(t) in [0.9973,0.9974], and let alpha be the unique +solution mu(alpha)=a=log(5). Put lambda=t-alpha. PR #6118 supplies the +qualitative saturation theorem, its sharper parameters and the exact +identification of the leaf measure. They are predecessor results. + +Let R_i be iid with p_t(r)=P_r r^t/Z(t), S_G=sum_i log(R_i), +B_G=G a+delta, and define the unconditioned difference Y_G=B_G-S_G. +Conditioning is written explicitly wherever it is used. + +**Theorem.** For every integer G>=11000, every delta in [0,log(5)], and +all real x>=0, + + Pr_t(Y_G>=x | S_G<=B_G) <= min(1, 5 exp(-lambda x)). + +Consequently, for all L>=0, + + E_t[(Y_G-L)_+ | S_G<=B_G] <= (5/lambda) exp(-lambda L), + E_t[Y_G 1_{Y_G>=L} | S_G<=B_G] + <= 5 (L+1/lambda) exp(-lambda L). + +These are finite-depth tail and truncation-error bounds, uniform across the +whole lockstep level. They are a partial answer to PR #4467 open question 2. +They establish neither the Bahadur–Rao asymptotic nor its error term, +and give no rate of convergence to Exp(lambda), no full-flow share or ceiling, +and no new kappa. The law is historical, rather than the selected P104 law. + +## 2. A quantitative tilted-normal lemma + +Let q(r)=P_r r^alpha/Z(alpha). Under q, X=log(R) has mean a, variance +sigma^2>0 and third absolute centered moment rho. Set b=(14/25) rho/sigma^3. +Berry–Esseen gives a Kolmogorov distance at most b/sqrt(G) between +Y=B_G-S_G and a normal variable Z with mean delta and variance G sigma^2. +The constant 14/25=0.56 is deliberately conservative. For example, +[Shevtsova, arXiv:1111.6554v1](https://arxiv.org/abs/1111.6554v1), abstract +and Corollary 1, proves an iid constant below 0.4756. Only the weaker 0.56 +bound is used here. No nonlattice local-limit or finite-depth asymptotic +expansion is needed for this lemma. + +If two distribution functions are within epsilon and f has finite total +variation and vanishes at both infinities, integration by parts bounds the +difference of their expectations by epsilon times the total variation of f. +For f_x(y)=exp(-lambda y) 1_{y>=x}, x>=0, that variation is +2 exp(-lambda x). The bound remains valid at atoms, by taking one-sided +limits of distribution functions against the continuous normal CDF. Thus, +with c=1/(sigma sqrt(2 pi)), + + sqrt(G) E_q[f_x(Y)] <= exp(-lambda x) (c/lambda+2b). (1) + +Indeed, the normal density is at most c/sqrt(G) everywhere. If + + sigma sqrt(G) >= a+1/lambda, + +then for every 0<=delta<=a and 0<=y<=1/lambda its normal density is at +least c exp(-1/2)/sqrt(G). Integration on that interval gives + + sqrt(G) E_q[f_0(Y)] + >= c exp(-1/2) (1-exp(-1))/lambda - 2b. (2) + +Whenever the right side is positive, division of (1) by (2) is legitimate. +For every ordered tuple, p_t(tuple)/q(tuple) is + + (Z(alpha)/Z(t))^G exp(lambda B_G) exp(-lambda Y). + +Its common factor cancels under conditioning. Therefore E_q[f_x]/E_q[f_0] +is exactly the desired conditional tail. This change of measure, including +its direction and normalization, holds at finite G. + +## 3. Explicit constants for this law + +The verifier establishes the following coarse intervals with exact rational +series. It does not reproduce PR #6118's high-precision parameter receipt. + + 0.9973 < t < 0.9974, + 0.9898 < alpha < 0.9899, + 7/1000 < lambda < 8/1000, + 7/5 < sigma < 3/2, + a < 2, + |log(r)-a| < 5/2 for every supported r. + +The last bound implies rho <= (5/2) sigma^2, hence b<=1. Also +5/2 < sqrt(2 pi) < 8/3 implies 1/43/5 and 1-exp(-1)>3/5. Consequently (2) exceeds + + (1/4)(3/5)(3/5)(1000/8)-2 = 37/4, + +whereas the coefficient in (1) is below + + (2/7)(1000/7)+2 = 2098/49 < 5(37/4). + +The normal-window premise follows for G>=11000 from + + ((2+1000/7)/(7/5))^2 = 25704900/2401 < 11000. + +This proves the tail inequality. The elementary pi bounds can be weakened +to 25/8=L}]=L Pr(Y>=L)+E[(Y-L)_+] proves the second bound, +including L=0 and distributions with atoms. A convenient mean bound is +E[Y] <= (1+log(5))/lambda, obtained by integrating min(1,5 exp(-lambda x)). + +For rank N, PR #6118 identifies G=floor(log_5(N/121)), +delta=log(N/121)-G log(5), and an independent terminal rank R with law p_t. +Its actual leaf depth is log(121)+Y_G-log(R). The terminal rank remains +unconditioned. For G>=11000, clipping Y_G at L changes the mean actual leaf depth +by at most (5/lambda) exp(-lambda L). This is a deterministic error bound +for that truncation, not a bound on distance to the limiting mean. + +## Credit and limits + +The finite-depth envelope, its explicit threshold and truncation constants +are produced by Nick Petalas. Ryanson Jonathan / pinterbanget supplied the +law, diagnostic and quantitative open question in PR #4467. DLamdata's +PR #6118 supplied the saturation proof and the precise leaf-measure statement. +zxv supplied the direct flow, Cinna Davis the refined induction, and Jacob +Alan Sussman the lockstep compiler. Berry–Esseen, change of measure and the +bounded-variation expectation estimate are classical ingredients. + +The result does not discharge any of the selected record's five assumptions. +No selected supplier, complete flow, physical word, native theorem, numerical +induction ceiling or complete multiplication theorem is checked here. +Independent human and formal proof-kernel review are unclaimed. Apache-2.0. diff --git a/research/direct-flow-finite-tail/README.md b/research/direct-flow-finite-tail/README.md new file mode 100644 index 0000000000..00426ed62c --- /dev/null +++ b/research/direct-flow-finite-tail/README.md @@ -0,0 +1,106 @@ +# A finite-depth tail bound for the direct-flow leaf walk + +This scoped proof gives the historical raw-p7 leaf law an explicit +finite-depth exponential envelope. For all G>=11000, +0<=delta<=log(5), and x>=0, + + Pr(Y_G>=x | S_G<=G log(5)+delta) <= min(1, 5 exp(-lambda x)). + +Here Y_G=G log(5)+delta-S_G and lambda=t-alpha is the tilt gap defined in +[PROOF.md](PROOF.md). The bound on clipping the deficit at L>=0 is + + E[(Y_G-L)_+ | survival] <= (5/lambda) exp(-lambda L). + +The same bound controls the resulting error in mean actual leaf depth, +including the independent unconditioned terminal rank. The proof also gives +E[Y_G 1_{Y_G>=L} | survival] <= 5(L+1/lambda) exp(-lambda L). + +This partially answers open question 2 of Ryanson Jonathan / pinterbanget's +[PR #4467](https://github.com/CrocSwap/integer-mult-bounds/pull/4467). +DLamdata's [PR #6118](https://github.com/CrocSwap/integer-mult-bounds/pull/6118), +head `6310550e932de70243fc2aaab6f4885688b6fe21`, supplies the qualitative +saturation theorem and exact leaf-measure identification. Those predecessor +results are cited, rather than audited or claimed here. The new step uses +Berry–Esseen and bounded-variation integration to replace an unspecified tail +constant and onset by explicit finite values. + +This does not establish a Bahadur–Rao asymptotic or its error term, a rate of +convergence to the exponential law, stable full-flow shares, a numerical +induction ceiling, supplier admission or a new kappa. The selected PR6030 +record and its five assumptions are unchanged. This is historical compiler +side work, not a selected-frontier improvement. + +## Reproduce + +Python 3.12, standard library only. From the repository root: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B research/direct-flow-finite-tail/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/direct-flow-finite-tail +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/direct-flow-finite-tail --check-source-history +``` + +Other reviewers can replace the interpreter path with their CPython 3.12. +The principal marker is `PASS_DIRECT_FLOW_FINITE_TAIL`. Each direct run prints +a generated JSON receipt binding all six package files by SHA256. It writes +nothing to the checkout. The registered normal and optimized commands repeat +the exact numerical gates and rejecting controls with no dependence on Python +assertions. Source laws are parsed as literals from the authenticated pinned +file; no predecessor code executes. + +The certificate encloses only the coarse hypotheses needed by the new bound, +not the predecessor's high-precision result. Logarithms use 48 terms of the +atanh series after power-of-two reduction. Exponentials use 32 terms after +scaling by 16, with geometric remainder bounds and four outward-rounded +squarings. All acceptance decisions use integers or rational intervals. +Finite Bernoulli fixtures separately check the tilt ratio and clipping +identity at atoms. The written proof and the external Berry–Esseen theorem +carry the universal probability claim; finite fixtures do not replace them. + +## Verification boundaries + +The exact source closure is in [SOURCES.json](SOURCES.json). The base is +`721c03822c421b7f7fcbb2598993b947c4d88419`, priority revision 8. +The source question and advisory claim are recorded in [TASK.json](TASK.json). +The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19241861) +precedes substantial work. PR6118's separate power-tariff follow-up concerns +asymptotic moments, while this result gives a finite-depth tail envelope. + +No selected cold replay, full historical flow replay, native or physical +program, Lean proof or complete multiplication theorem is run. The classical +Berry–Esseen inequality and elementary pi bounds are external mathematical +inputs. Independent human and formal proof-kernel review are unclaimed. + +The verifier uses bounded nonrecursive loops. It reads four fixed source +records, parses an authenticated source with at most 100 top-level statements, +and processes two supports of nine ranks no larger than 121. The finite-word +fixtures stop at depth eight, with at most 256 words in a fixture. Functions +stay below 60 lines. Every gate fails through an explicit exception, including +under optimized Python. The JSON serializer has one fixed callback target. + +Power-of-Ten rule 3 has a managed-runtime deviation in `verify.py`: Python +allocates Fraction integers and collections during execution. Fixed input +inventories, fixed series lengths, 128-bit outward rounding and the depth-eight +fixture cap bound the live workload. Source files are capped at one million +bytes. The registered normal and optimized checks exercise this bounded path. +A fixed-memory implementation would require a different arithmetic runtime; +no such implementation or physical resource claim is made. Diagnostics use +Python development mode and warnings as errors in local verification. + +## Open next questions + +Can an effective nonlattice interval local-limit bound give an explicit +*decreasing* error for the distribution or mean relative to its exponential +limit? This would quantify the onset of saturation. A first step is to pair +such a remainder with the finite tail envelope proved here. The missing input +is a quantitative local-limit estimate, not another tail-constant search. + +## Credit + +The finite-depth envelope and explicit truncation constants are produced by +Nick Petalas. Ryanson Jonathan / pinterbanget supplied the fixed law and the +explicit-constant question in PR4467. DLamdata supplied the saturation theorem +and exact leaf observable in PR6118. zxv supplied the direct flow, Cinna Davis +the refined induction, and Jacob Alan Sussman the lockstep compiler. The +Berry–Esseen inequality, change of measure and bounded-variation estimate are +classical. Predecessor files and credit lines remain unchanged. Apache-2.0. diff --git a/research/direct-flow-finite-tail/SOURCES.json b/research/direct-flow-finite-tail/SOURCES.json new file mode 100644 index 0000000000..408da6b263 --- /dev/null +++ b/research/direct-flow-finite-tail/SOURCES.json @@ -0,0 +1,30 @@ +{ + "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/direct-flow-leaf-walk/README.md", + "usage": "input", + "git_blob": "02ddde948f2e94874850eadd70d7d32559916848", + "sha256": "bf79c953cd02ad62ffd44c58ae4f5b78f2b3439574176140ba6eceb1b77430cc" + }, + { + "path": "research/direct-flow-leaf-walk/verify.py", + "usage": "input", + "git_blob": "42440e630a46c6e581797f52bfb4c0c87bbdac3a", + "sha256": "2030d79d7f136b39b4e2a3f5b033af4bba18ab87579ec352267dc1697e02157d" + } + ] +} diff --git a/research/direct-flow-finite-tail/TASK.json b/research/direct-flow-finite-tail/TASK.json new file mode 100644 index 0000000000..e9ab8bf7f3 --- /dev/null +++ b/research/direct-flow-finite-tail/TASK.json @@ -0,0 +1,95 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 8, + "base_commit": "721c03822c421b7f7fcbb2598993b947c4d88419", + "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 explicit finite-depth exponential tail and truncation-error envelope for the fixed PR4467 direct-flow leaf law.", + "scope_change_reason": "This takes PR4467 open question 2 as a scoped historical compiler side result, rather than claiming to discharge a selected P104 assumption. The source question is distinct from the concurrent PR6118 power-tariff phase-transition target.", + "bottleneck_link": "Quantitative control of conditioned leaf depth makes finite-depth truncation errors assessable. This historical raw-p7 lemma does not change the selected supplier, compiler or kappa.", + "budget_minutes": 60, + "stop_rule": "Stop at the first exact finite-depth tail envelope with a written proof and bounded certificate; leave convergence rates and full-flow shares open.", + "outcome": "completed", + "evidence": "PROOF.md and verify.py; runtime receipts bind all six package files by SHA256.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can one bound the finite-G distance from the exponential limit or the limiting mean with an explicit decreasing error?", + "why_it_matters": "The envelope bounds truncation error but does not locate the onset of saturation accurately.", + "first_step": "Combine an effective interval local-limit estimate with the existing finite tail envelope.", + "blocked_by": "No quantitative nonlattice local-limit remainder is supplied." + } + ], + "coordination": { + "source_question": "PR #4467 open question 2", + "source_author": "pinterbanget", + "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19241861", + "predecessor": "PR #6118 at 6310550e932de70243fc2aaab6f4885688b6fe21" + }, + "environment": { + "python": "CPython 3.12.15", + "platform": "macOS arm64", + "dependencies": "standard library only" + }, + "claim_type": "scoped written proof with finite exact numerical certificate" +} diff --git a/research/direct-flow-finite-tail/VERIFY.json b/research/direct-flow-finite-tail/VERIFY.json new file mode 100644 index 0000000000..41e4e96fcb --- /dev/null +++ b/research/direct-flow-finite-tail/VERIFY.json @@ -0,0 +1,31 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/direct-flow-leaf-walk/README.md", + "research/direct-flow-leaf-walk/verify.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact rational numerical hypotheses, tail constants, finite tilt/clipping fixtures and six rejecting certificate/source controls." + }, + { + "argv": [ + "{python}", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "The same proof gates and controls with assertions disabled." + } + ] +} diff --git a/research/direct-flow-finite-tail/verify.py b/research/direct-flow-finite-tail/verify.py new file mode 100644 index 0000000000..d96684d90c --- /dev/null +++ b/research/direct-flow-finite-tail/verify.py @@ -0,0 +1,255 @@ +#!/usr/bin/env python3 +"""Certify the numerical gates of PROOF.md, without replaying predecessors. + +Produced by Nick Petalas. Apache-2.0. +""" +import ast +import hashlib +import json +from fractions import Fraction as F +from itertools import product +from pathlib import Path + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parents[1] +GRID = 1 << 128 + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def rounded(lo, hi): + need(lo <= hi, 'reversed interval') + return (F(lo.numerator * GRID // lo.denominator, GRID), + F(-((-hi.numerator * GRID) // hi.denominator), GRID)) + + +def add(x, y): + return rounded(x[0] + y[0], x[1] + y[1]) + + +def mul(x, y): + bounds = [a * b for a in x for b in y] + return rounded(min(bounds), max(bounds)) + + +def div(x, y): + need(y[0] > 0, 'nonpositive denominator interval') + return mul(x, (1 / y[1], 1 / y[0])) + + +def point(x): + return (F(x), F(x)) + + +def log_unit(x): + need(F(1) <= x <= 2, 'log reduction domain') + z = (x - 1) / (x + 1) + total = sum((2 * z ** (2 * j + 1) / (2 * j + 1) + for j in range(48)), F(0)) + tail = 2 * z ** 97 / (97 * (1 - z * z)) + return rounded(total, total + tail) + + +def log_integer(n): + need(type(n) is int and 1 <= n <= 121, 'log integer domain') + k = n.bit_length() - 1 + return add(log_unit(F(n, 1 << k)), mul(point(k), log_unit(F(2)))) + + +def exp_scalar(x): + need(F(0) <= x <= 5, 'exp domain') + y = x / 16 + term = F(1) + total = F(1) + for j in range(1, 33): + term *= y / j + total += term + next_term = term * y / 33 + tail = next_term / (1 - y / 34) + result = rounded(total, total + tail) + for _ in range(4): + result = mul(result, result) + return result + + +def exp_interval(x): + return exp_scalar(x[0])[0], exp_scalar(x[1])[1] + + +def authenticate(data, record): + need(hashlib.sha256(data).hexdigest() == record['sha256'], + 'source hash mismatch: ' + record['path']) + + +def inputs(): + manifest = json.loads((PACKAGE / 'SOURCES.json').read_text()) + need(len(manifest['files']) == 4, 'source inventory') + payloads = {} + for entry in manifest['files']: + path = entry['path'] + need(path in {'certificates/selected-result.json', + 'docs/research/agent-task-catalog.json', + 'research/direct-flow-leaf-walk/README.md', + 'research/direct-flow-leaf-walk/verify.py'}, 'source path') + if entry['usage'] == 'provenance': + continue + data = (ROOT / path).read_bytes() + need(len(data) <= 1_000_000, 'source capacity') + authenticate(data, entry) + payloads[path] = data + tree = ast.parse(payloads['research/direct-flow-leaf-walk/verify.py']) + laws = {} + need(len(tree.body) <= 100, 'source AST capacity') + for node in tree.body: + if isinstance(node, ast.Assign) and len(node.targets) == 1: + target = node.targets[0] + if isinstance(target, ast.Name) and target.id in {'P', 'W'}: + laws[target.id] = ast.literal_eval(node.value) + need(set(laws) == {'P', 'W'}, 'missing law') + for law in laws.values(): + need(len(law) == 9, 'law support') + need(all(type(r) is int and 1 <= r <= 121 and type(c) is int + and 1 <= c <= 100000 for r, c in law.items()), 'law domain') + return laws, manifest + + +def moments(law, exponent, logs): + result = [point(0), point(0), point(0)] + for r, count in law.items(): + weight = mul(point(count), exp_interval(mul(exponent, logs[r]))) + result[0] = add(result[0], weight) + result[1] = add(result[1], mul(weight, logs[r])) + result[2] = add(result[2], mul(weight, mul(logs[r], logs[r]))) + return result + + +def minus(x, y): + return rounded(x[0] - y[1], x[1] - y[0]) + + +def numerical_gates(laws): + logs = {r: log_integer(r) for r in sorted(set(laws['P']) | set(laws['W']))} + t = F(9973, 10000), F(9974, 10000) + alpha = F(9898, 10000), F(9899, 10000) + a = logs[5] + signs = [] + for endpoint in t: + wm = moments(laws['W'], point(endpoint), logs) + pm = moments(laws['P'], point(endpoint), logs) + signs.append(minus(wm[0], pm[0])) + need(signs[0][1] < 0 < signs[1][0], 'invoice endpoint signs') + wm = moments(laws['W'], t, logs) + pm = moments(laws['P'], t, logs) + need(wm[1][0] > pm[1][1], 'invoice derivative') + means = [] + for endpoint in alpha: + z, first, _ = moments(laws['P'], point(endpoint), logs) + means.append(div(first, z)) + need(means[0][1] < a[0] and means[1][0] > a[1], 'tilt endpoint signs') + z, first, second = moments(laws['P'], alpha, logs) + mean = div(first, z) + variance = minus(div(second, z), mul(mean, mean)) + need(F(49, 25) < variance[0] and variance[1] < F(9, 4), 'variance gate') + lam = minus(t, alpha) + need(F(7, 1000) < lam[0] and lam[1] < F(8, 1000), 'lambda gate') + need(a[1] < 2, 'offset gate') + for r in laws['P']: + centered = minus(logs[r], a) + need(-F(5, 2) < centered[0] <= centered[1] < F(5, 2), 'support radius') + # e^(1/2)<5/3 and e>5/2 imply both elementary exponential gates. + need(exp_scalar(F(1, 2))[1] < F(5, 3), 'normal window density') + need(exp_scalar(F(1))[0] > F(5, 2), 'window integral') + return {'t': t, 'alpha': alpha, 'lambda': lam, 'variance': variance, + 'invoice_signs': signs, 'tilt_means': means} + + +def constants(depth=11000, factor=5, sigma_low=F(7, 5), be=F(14, 25)): + need(depth >= 0 and factor > 0 and sigma_low > 0 and be > 0, 'gate domain') + b_upper = be * F(5, 2) / sigma_low + lower = F(1, 4) * F(3, 5) ** 2 * F(1000, 8) - 2 * b_upper + upper = F(2, 7) * F(1000, 7) + 2 * b_upper + threshold = ((2 + F(1000, 7)) / sigma_low) ** 2 + need(F(depth) >= threshold, 'depth window') + need(lower > 0, 'positive denominator') + need(upper <= factor * lower, 'tail constant') + return {'depth': depth, 'factor': factor, 'b_upper': b_upper, + 'denominator_lower': lower, 'numerator_upper': upper, + 'threshold_upper': threshold, 'ratio_upper': upper / lower} + + +def finite_tilt_fixtures(): + count = 0 + # Integer-valued X with q=(1/2,1/2), p=(1/3,2/3), exp(lambda)=2. + # These exact fixtures check the finite ratio and clipping identities. + for g in range(1, 9): + sums = [sum(word) for word in product((0, 1), repeat=g)] + for barrier in range(g + 1): + chosen = [s for s in sums if s <= barrier] + pweights = [F(2 ** s, 3 ** g) for s in chosen] + qweights = [F(2 ** s, 2 ** (g + barrier)) for s in chosen] + for cut in range(barrier + 2): + direct = sum((w for s, w in zip(chosen, pweights) + if barrier - s >= cut), F(0)) / sum(pweights) + tilted = sum((w for s, w in zip(chosen, qweights) + if barrier - s >= cut), F(0)) / sum(qweights) + need(direct == tilted, 'finite tilt factorization') + clipped = sum((max(barrier - s - cut, 0) * w + for s, w in zip(chosen, pweights)), F(0)) + tail = sum(((barrier - s) * w + for s, w in zip(chosen, pweights) + if barrier - s >= cut), F(0)) + need(tail == cut * direct * sum(pweights) + clipped, + 'clipping identity at atoms') + count += 1 + return count + + +def controls(manifest): + failures = 0 + trials = ({'depth': 10000}, {'factor': 4}, {'sigma_low': F(1)}, + {'be': F(2)}, {'depth': -1}) + for trial in trials: + try: + constants(**trial) + except ValueError: + failures += 1 + else: + raise ValueError('invalid numerical certificate accepted') + entry = next(e for e in manifest['files'] if e['usage'] == 'input') + try: + authenticate(b'changed scientific input', entry) + except ValueError: + failures += 1 + else: + raise ValueError('changed source accepted') + need(failures == 6, 'control coverage') + return failures + + +def serialize(value): + if isinstance(value, F): + return str(value) + raise TypeError('unsupported receipt value') + + +def main(): + laws, manifest = inputs() + gates = numerical_gates(laws) + bound = constants() + fixtures = finite_tilt_fixtures() + rejected = controls(manifest) + names = ['PROOF.md', 'README.md', 'TASK.json', 'SOURCES.json', + 'VERIFY.json', 'verify.py'] + hashes = {name: hashlib.sha256((PACKAGE / name).read_bytes()).hexdigest() + for name in names} + print(json.dumps({'status': 'PASS_DIRECT_FLOW_FINITE_TAIL', + 'gates': gates, 'bound': bound, 'finite_fixtures': fixtures, + 'rejection_controls': rejected, 'package_sha256': hashes}, + default=serialize, sort_keys=True, indent=2)) + + +if __name__ == '__main__': + main()