diff --git a/research/selected-quadratic-root-brackets/README.md b/research/selected-quadratic-root-brackets/README.md new file mode 100644 index 0000000000..9f6a80064d --- /dev/null +++ b/research/selected-quadratic-root-brackets/README.md @@ -0,0 +1,187 @@ +# Quadratic screening brackets for the selected supplier roots + +**Independent analytic screening, not endpoint-grid certification or a new κ.** +For the three frozen selected pricing ledgers, two rational surrogate curves +bracket the moment root more than **418×** more tightly than the gap left by +the linear `a < D/E` diagnostic. All modeled surcharges are retained as +exponential terms. No arbitrary fractional-power evaluation is used to obtain +the brackets, and no predecessor pricing function is imported. + +The selected endpoint signs already have several independent full replays. +This contribution instead supplies a sharper screening implication and a +source-bound check of that implication. It does not replace those replays. + +## Exact model and comparison theorem + +For the normalized bill, write + +```text +M(a) = sum_i c_i exp(lambda_i*a), c_i>0, lambda_i>=0, +D = 1-sum_i c_i > 0, +E = sum_i c_i lambda_i > 0, +F = sum_i c_i lambda_i^2, +L = max_i lambda_i. +``` + +An ordinary rank-r child contributes `c_i=n_r*r/(m*W)` and +`lambda_i=ln(m/r)`. The modeled bad-residue surcharge contributes +`rho*m^a`, with `rho=32*m*sum_r n_r/(10^16*W)`: its weight is rho and its +logarithmic rate is ln(m). It contributes to **D, E, F and L**, not just D. +The physical derivation of this inherited surcharge remains assumed. +With no surcharge, this normalized D/E equals the repository's raw +`(mW-sum n_r r)/(sum n_r r ln(m/r))` diagnostic. + +For `0<=t<3`, + +```text +1+t+t^2/2 <= exp(t) <= 1+t+t^2/[2(1-t/3)]. +``` + +The lower inequality follows from the nonnegative exponential series. For +the upper inequality, `n! >= 2*3^(n-2)` for every n>=2: equality at n=2,3, +and induction thereafter. Summing that geometric coefficient majorant gives +the rational upper expression. Applying it to every term, and using +`lambda_i<=L`, gives + +```text +E*a + F*a^2/2 <= M(a)-M(0) + <= E*a + F*a^2/[2(1-L*a/3)]. +``` + +For certified nonnegative log intervals, let `Elo<=E<=Ehi`, +`Flo<=F<=Fhi`, and `L<=Lhi`. Define + +```text +Q(a) = Elo*a + Flo*a^2/2, +U(a) = Ehi*a + Fhi*a^2/[2(1-Lhi*a/3)], +H = D/Elo, requiring Elo>0 and Lhi*H<3. +``` + +Both Q and U are strictly increasing on [0,H], start at zero and reach at +least D at H. Their roots at height D are therefore bracketed there. +The true moment is strictly increasing and unbounded because some positive +weight has positive rate, so it has exactly one positive root a* at height one. +The comparison proves + +```text +root(U=D) <= a* <= root(Q=D) <= H. +``` + +Exact rational bisection reports the **lower endpoint of the U-root bracket** +and the **upper endpoint of the Q-root bracket**. The inner endpoints would +not certify this implication. The implementation verifies the final signs +and rejects the pole/domain or an unbracketed surrogate. + +## Selected evidence + +Profiles are read from the selected assembly and bit `nine.profile`, not from +PR headlines. The complex profile, rank mass and deficit are cross-bound to +the retained independent owner receipt. The bit rank mass and endpoint are +also matched, and the selected surcharge flags checked. Exact live-input and +historical provenance pins are in [SOURCES.json](SOURCES.json). + +The following decimals are **outward rounded** displays of the exact rational +root brackets in [RESULT.json](RESULT.json). Narrowing is +`(linear_upper-published_endpoint)/(root_upper-root_lower)`; it measures a +diagnostic uncertainty gap, not a speedup or exponent improvement. + +| Model | Certified lower | Certified upper | D/E upper | Narrowing factor | +|---|---:|---:|---:|---:| +| Native complex, m=73, W=14336 | 0.00167546136793417 | 0.00167547358407120 | 0.00168059070975433 | >419 | +| Conservative complex, same profile + surcharge | 0.00167546136507270 | 0.00167547358120967 | 0.00168059070687533 | >419 | +| Bit, m=64, W=28416, surcharge | 0.00173342514312811 | 0.00173343740334675 | 0.00173855724840137 | >418 | + +Every interval contains the published endpoint and its next 10^-24 grid +point. **Containment does not reprove acceptance or rejection at those points.** +The approximately 1.2e-8 surrogate gap also cannot resolve the much smaller +native/conservative correction. Finer bisection alone will not remove this +analytic approximation gap. + +## Reproduce and controls + +Python 3.10+, standard library only, from the repository root: + +```sh +python3 -I -O -B research/selected-quadratic-root-brackets/verify.py +python3 -I -O -B research/selected-quadratic-root-brackets/test_verify.py +python3 scripts/research_package.py --package research/selected-quadratic-root-brackets --check-only +python3.12 -B scripts/research_package.py --package research/selected-quadratic-root-brackets +``` + +Expected verifier output: + +```text +PASS_SELECTED_QUADRATIC_ROOT_BRACKETS ledgers=3 controls=12 narrowing_gt_100x surcharge_included no_new_kappa +``` + +The independently written logarithm primitive uses binary reduction and +72 positive atanh terms, an explicit geometric tail, and outward 160-bit +dyadic rounding. On `[1,2]`, z=(x-1)/(x+1) lies in [0,1/3]. After 72 terms, +the remaining log series is at most `2*z^145/[145*(1-z^2)]`. +The log method itself is not claimed as new or distinct from every retained +log implementation: the **moment-root enclosure** is the rational surrogate +comparison rather than another full exponential-series endpoint replay. + +Twelve check groups cover log-one, a log-two decimal interval, a single +exponential root, an independent exact dyadic root, six invalid-domain or +unbracketed-root rejections, every surcharge D/E/F contribution and a fixture +where the surcharge strictly raises the maximum logarithmic rate. The +exact fixture `M(a)=2^(a-1)` has root 1; broad rational bounds +`2/30 and `Lhi*D/Elo<3`, then +comparing with its independent full replay. The blocker is that this package +covers only three frozen selected ledgers; pending-profile source binding, +complete invoice and actual timing benefit must be established separately. +Structured fields are in [TASK.json](TASK.json). + +## Credit and license + +Credit the selected construction and reviewed source lineage: Rohan Arun +(https://github.com/CrocSwap/integer-mult-bounds/pull/1094), Jeremy Kothe +(https://github.com/CrocSwap/integer-mult-bounds/pull/1087 and mutable-leaver +lineage), Hao Yan (https://github.com/CrocSwap/integer-mult-bounds/pull/858), +and DreamingOfClouds' retained bit supplier +(https://github.com/CrocSwap/integer-mult-bounds/pull/589), with eumemic and +the full predecessor credit in the selected review. Sources are untouched. +Aaron Wang / navinor's prior linear diagnostic +https://github.com/CrocSwap/integer-mult-bounds/pull/1293 motivates the +comparison; TennisBowling's https://github.com/CrocSwap/integer-mult-bounds/pull/1405 +is credited for the fail-closed log-contract audit. Neither numerical routine +is imported or reused. Existing complete endpoint replays retain their credit. + +Prepared by Aaron Wang / navinor, **with help from chatgpt**, including +separate read-only AI proof/code review. No independent human or +proof-assistant review is claimed. Apache-2.0. diff --git a/research/selected-quadratic-root-brackets/RESULT.json b/research/selected-quadratic-root-brackets/RESULT.json new file mode 100644 index 0000000000..2a319c6b48 --- /dev/null +++ b/research/selected-quadratic-root-brackets/RESULT.json @@ -0,0 +1,95 @@ +{ + "sources": { + "research/community-frontier1094-audit/ASSEMBLY.json": "1122cb3a575f8c788345fc1bf4c108ac7c3250fb81a5988671f5eb04b3ab3045", + "research/community-frontier1094-audit/INDEPENDENT1094.json": "301fb8a0e4ab7e3c383ff974c54c08178283b2a3453c5282757f692a3c7a4bfd", + "research/e8-bit-p111-tuned/tune/EXPECTED.json": "b9f0e5ca038abe837b0007c8fe006f366a6f02009244ac57705a8a200e2301f4" + }, + "ledgers": [ + { + "D": "5/1022", + "E": [ + "2226267329607014812531773732109440320235069757525462461/764751192756317584590932940306453117997241886167793664", + "4452534659214029625063547464218880640470139515055948977/1529502385512635169181865880612906235994483772335587328" + ], + "F": [ + "423642475897354140413299417883439912745134363922753651212945362074467456741824477438689136542666162239/39917325727289967619798165644896589917695342113801126964770313566981642235388610598829115480670732288", + "3389139807178833123306395343067519301961074911389585273831274365789791055719806875074238397406521732929/319338605818319740958385325159172719341562736910409015718162508535853137883108884790632923845365858304" + ], + "L_upper": "783814187267525543074368603512103785548504437263/182687704666362864775460604089535377456991567872", + "surcharge_coefficient": "0", + "linear_upper": "3741444191567111470601433171753684530319187310018560/2226267329607014812531773732109440320235069757525462461", + "root_lower": "3730024905450536003526167599368321493128347385856000/2226267329607014812531773732109440320235069757525462461", + "root_upper": "1243350700612425834451262209817631057636993489960960/742089109869004937510591244036480106745023252508487487", + "width": "27196386741499827619030084571679782633084026880/2226267329607014812531773732109440320235069757525462461", + "log_bits": 160, + "log_terms": 72, + "bisection_steps": 100, + "name": "native_complex", + "m": 73, + "W": 14336, + "surcharge": false, + "endpoint": "67018507072324140917/40000000000000000000000", + "rank_mass": 1041408, + "narrowing_factor": "456654888532557295881935749100389403969058823851099670637704755042383263/1087855469659993104761203382867191305323361075200000000000000000000000", + "narrowing_factor_floor": 419 + }, + { + "D": "114285714091334443/23360000000000000000", + "E": [ + "695708540510724158908723380275351679746858872586852300332113580615203/238984747736349245184666543845766599374138089427435520000000000000000", + "86963567563840519863590422534418959968357359073454663615734138153437/29873093467043655648083317980720824921767261178429440000000000000000" + ], + "F": [ + "3706871664155348937851154683532397509559433283033197998212737066209490423583928468326968318347378591103637959795768691/349276600113787216673233949392845161779834243495759860941740243711089369559650342739754760455868907520000000000000000", + "57919869752427327153924291930193711086866145047522850677383452094693433773943424726036159606085544544394630728072931/5457446876777925260519280459263205652809910054621247827214691307985771399369536605308668132122951680000000000000000" + ], + "L_upper": "783814187267525543074368603512103785548504437263/182687704666362864775460604089535377456991567872", + "surcharge_coefficient": "18639163/2240000000000000000", + "linear_upper": "1169201307876117125825584202814113553498009201483363467256005656576/695708540510724158908723380275351679746858872586852300332113580615203", + "root_lower": "1165632780976839579968930177935206036867808848298459602692958322688/695708540510724158908723380275351679746858872586852300332113580615203", + "root_upper": "1165641279847652929602261155879619754480749985731745786272635944960/695708540510724158908723380275351679746858872586852300332113580615203", + "width": "8498870813349633330977944413717612941137433286183579677622272/695708540510724158908723380275351679746858872586852300332113580615203", + "log_bits": 160, + "log_terms": 72, + "bisection_steps": 100, + "name": "conservative_complex", + "m": 73, + "W": 14336, + "surcharge": true, + "endpoint": "1675462673946628390003/1000000000000000000000000", + "rank_mass": 1041408, + "narrowing_factor": "3567616304512985759694051176976209232156984041838810332016144209905296166479833844984391/8498870813349633330977944413717612941137433286183579677622272000000000000000000000000", + "narrowing_factor_floor": 419 + }, + { + "D": "16326904278023/2890625000000000", + "E": [ + "857816062600787715311825029205937383584944311835989118313192937/264040823150602577995782904348156600230808125440000000000000000", + "13725057001612603444989200467294998137359108989389858028020965729/4224653170409641247932526469570505603692930007040000000000000000" + ], + "F": [ + "34178575185287116286055432031537844231841197666129604174357369819366745552809403008560658509722331673539651550591/3087168762854440353461554809698180790636721379968599706564083573805551947417332044955062391275520000000000000000", + "68357150370574232572110864063075688463682395332397527451134424773488254505732667886567689030007893245740993464383/6174337525708880706923109619396361581273442759937199413128167147611103894834664089910124782551040000000000000000" + ], + "L_upper": "3039107217898977213407095817540395654759610698101/730750818665451459101842416358141509827966271488", + "surcharge_coefficient": "4713/722656250000000", + "linear_upper": "1491362333429721118405064796109867521564479852090397481238528/857816062600787715311825029205937383584944311835989118313192937", + "root_lower": "1486959931091370769655699369190842305347682679541384406368256/857816062600787715311825029205937383584944311835989118313192937", + "root_upper": "135179131645803832552914005658087330608515987248426722000896/77983278418253428664711366291448853053176755621453556210290267", + "width": "10517012471388426354693048118331345993180191309535641600/857816062600787715311825029205937383584944311835989118313192937", + "log_bits": 160, + "log_terms": 72, + "bisection_steps": 100, + "name": "bit", + "m": 64, + "W": 28416, + "surcharge": true, + "endpoint": "1733427039589844234749/1000000000000000000000000", + "rank_mass": 1808352, + "narrowing_factor": "4400775523021170984351065424627457254861917496773458391989867891439947364443232187/10517012471388426354693048118331345993180191309535641600000000000000000000000000", + "narrowing_factor_floor": 418 + } + ], + "controls": 12, + "scope": "screening brackets only; no endpoint-grid certification, word replay or new kappa" +} diff --git a/research/selected-quadratic-root-brackets/SOURCES.json b/research/selected-quadratic-root-brackets/SOURCES.json new file mode 100644 index 0000000000..c29d1baed4 --- /dev/null +++ b/research/selected-quadratic-root-brackets/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "2de86c77b4127d2f01f504e0c7c5e4db737caa3c", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "06c96f5579bb67ed1b86d334e78fbed7da6945f1", + "sha256": "6686ad58f1fbdbc87134a78901b60fd53a20d3984355e91defbbebc9e9fa8075" + }, + { + "path": "research/community-frontier1094-audit/ASSEMBLY.json", + "usage": "input", + "git_blob": "5fd676df060f3b450782fdf5ff5f6beb63a5eeb0", + "sha256": "1122cb3a575f8c788345fc1bf4c108ac7c3250fb81a5988671f5eb04b3ab3045" + }, + { + "path": "research/community-frontier1094-audit/INDEPENDENT1094.json", + "usage": "input", + "git_blob": "009a385e26858058a18188364078d162aa6f9519", + "sha256": "301fb8a0e4ab7e3c383ff974c54c08178283b2a3453c5282757f692a3c7a4bfd" + }, + { + "path": "research/e8-bit-p111-tuned/tune/EXPECTED.json", + "usage": "input", + "git_blob": "e293ddc557742637f9f679f083a1a282d87b1b13", + "sha256": "b9f0e5ca038abe837b0007c8fe006f366a6f02009244ac57705a8a200e2301f4" + } + ] +} diff --git a/research/selected-quadratic-root-brackets/TASK.json b/research/selected-quadratic-root-brackets/TASK.json new file mode 100644 index 0000000000..dd05484e02 --- /dev/null +++ b/research/selected-quadratic-root-brackets/TASK.json @@ -0,0 +1,71 @@ +{ + "schema_version": 1, + "task_id": "independent-moment", + "priority_revision": 3, + "base_commit": "2de86c77b4127d2f01f504e0c7c5e4db737caa3c", + "original_card": { + "id": "independent-moment", + "question": "Can one selected pricing or assembly claim be checked by a genuinely independent exact implementation?", + "starting_points": [ + "certificates/selected-result.json" + ], + "methods": [ + "Reconstruct the rank ledger from original operations rather than trusting its aggregate.", + "Implement certified moment inequalities through a different exact enclosure method." + ], + "acceptance_gate": "Demonstrate independence, source binding, positive cases and semantic failure controls.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Record the selected certificate and complex_profile rather than taking a PR headline as input.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Recompute one small part of the ledger or one certified enclosure using an independent implementation.", + "bottleneck_link": "Independent pricing prevents unsupported frontier claims and can reveal genuine accounting slack.", + "allowed_variations": [ + "Reconstruct either a source ledger or a numeric enclosure with a different method." + ], + "scope_change_triggers": [ + "Importing the primary function and calling its output independent verification." + ], + "overlap_terms": [ + "independent moment", + "rank histogram", + "exact enclosure" + ] + }, + "scope_status": "refined", + "actual_scope": "Certified two-sided quadratic/rational-majorant brackets of the three selected finite moment roots: native complex m=73,W=14336; conservative complex with its modeled surcharge; bit m=64,W=28416 with surcharge. This is screening, not 1e-24 endpoint-grid certification.", + "scope_change_reason": "Selected endpoint signs already have several code-disjoint replays. Refine the card's independent-enclosure method to a rational quadratic diagnostic with a proved comparison theorem, avoiding another full-precision endpoint replay.", + "bottleneck_link": "This sharpens the repository's a0 and L*D/Elo<3, then compare the screening bounds with its independent full moment replay.", + "blocked_by": "This package covers only the three selected frozen ledgers. Profiling benefit, a pending profile's source binding and its complete invoice must be established separately." + } + ] +} diff --git a/research/selected-quadratic-root-brackets/VERIFY.json b/research/selected-quadratic-root-brackets/VERIFY.json new file mode 100644 index 0000000000..6fbf864e72 --- /dev/null +++ b/research/selected-quadratic-root-brackets/VERIFY.json @@ -0,0 +1,29 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/community-frontier1094-audit/ASSEMBLY.json", + "research/community-frontier1094-audit/INDEPENDENT1094.json", + "research/e8-bit-p111-tuned/tune/EXPECTED.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Three source-bound quadratic screening brackets; exact log enclosures, matched source profiles/mass/deficits, full modeled surcharges, twelve positive/domain/control groups; deterministic receipt comparison." + }, + { + "argv": ["{python}", "-I", "-O", "-B", "{package}/test_verify.py"], + "timeout_seconds": 120, + "checks": "Positive optimized CLI; false root, omitted surcharge and changed source-hash receipt rejected with explicit diagnostics." + } + ] +} diff --git a/research/selected-quadratic-root-brackets/test_verify.py b/research/selected-quadratic-root-brackets/test_verify.py new file mode 100644 index 0000000000..b82b47d795 --- /dev/null +++ b/research/selected-quadratic-root-brackets/test_verify.py @@ -0,0 +1,39 @@ +"""Positive replay and explicit rejection controls for the screening certificate.""" +import subprocess +import sys +import json +import tempfile +import unittest +from pathlib import Path + +HERE = Path(__file__).resolve().parent + +class ScreeningTests(unittest.TestCase): + def test_three_fully_charged_screening_brackets(self): + result = subprocess.run([sys.executable, '-I', '-O', '-B', str(HERE / 'verify.py')], + capture_output=True, text=True, encoding='utf-8', timeout=120) + self.assertEqual(result.returncode, 0, result.stdout + result.stderr) + self.assertIn('PASS_SELECTED_QUADRATIC_ROOT_BRACKETS ledgers=3', result.stdout) + + def test_false_root_missing_surcharge_and_changed_source_receipts_reject(self): + original = json.loads((HERE / 'RESULT.json').read_text(encoding='utf-8')) + mutations = [ + lambda d: d['ledgers'][0].update(root_lower='1/100'), + lambda d: d['ledgers'][2].update(surcharge_coefficient='0'), + lambda d: d['sources'].update({'research/community-frontier1094-audit/ASSEMBLY.json': '0'*64}), + ] + with tempfile.TemporaryDirectory(prefix='.controls-', dir=HERE) as temp: + for index, mutate in enumerate(mutations): + with self.subTest(index=index): + data = json.loads(json.dumps(original)) + mutate(data) + path = Path(temp) / f'bad-{index}.json' + path.write_text(json.dumps(data), encoding='utf-8') + result = subprocess.run([sys.executable, '-I', '-O', '-B', str(HERE/'verify.py'), '--result', str(path)], + capture_output=True, text=True, encoding='utf-8', timeout=120) + self.assertNotEqual(result.returncode, 0) + self.assertIn('result receipt mismatch', result.stdout + result.stderr) + self.assertNotIn('PASS_SELECTED_QUADRATIC_ROOT_BRACKETS', result.stdout) + +if __name__ == '__main__': + unittest.main() diff --git a/research/selected-quadratic-root-brackets/verify.py b/research/selected-quadratic-root-brackets/verify.py new file mode 100644 index 0000000000..6aa57c7501 --- /dev/null +++ b/research/selected-quadratic-root-brackets/verify.py @@ -0,0 +1,226 @@ +#!/usr/bin/env python3 +"""Two-sided rational screening of selected moment roots; not supplier adoption. + +Aaron Wang / navinor, with help from chatgpt. Apache-2.0. +No primary pricing implementation is imported. +""" +import argparse +from fractions import Fraction as Q +from functools import lru_cache +import hashlib +import json +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +SCALE = 1 << 160 +ASSEMBLY = 'research/community-frontier1094-audit/ASSEMBLY.json' +OWNER = 'research/community-frontier1094-audit/INDEPENDENT1094.json' +BIT = 'research/e8-bit-p111-tuned/tune/EXPECTED.json' + + +def require(ok, message): + if not ok: + raise ValueError(message) + + +def outward(lo, hi): + require(lo <= hi, 'reversed interval') + return (Q((lo*SCALE).__floor__(), SCALE), Q((hi*SCALE).__ceil__(), SCALE)) + + +def atanh_log(x): + z = (x-1)/(x+1) + require(0 <= z <= Q(1, 3), 'log reduction outside [1,2]') + power, total = z, Q(0) + for j in range(72): + total += 2*power/(2*j+1) + power *= z*z + tail = 2*power/(145*(1-z*z)) + return outward(total, total+tail) + + +@lru_cache(maxsize=None) +def logarithm(x): + x = Q(x) + require(x >= 1, 'log input below one') + k = 0 + while x >= 2: + x /= 2 + k += 1 + lo, hi = atanh_log(x) + two_lo, two_hi = atanh_log(Q(2)) + return outward(lo+k*two_lo, hi+k*two_hi) + + +def coefficients(profile, m, w, surcharge): + require(isinstance(m, int) and isinstance(w, int) and m > 1 and w > 0, + 'invalid width or normalization') + require(profile and all(isinstance(r, int) and isinstance(n, int) + and 0 < r < m and n > 0 for r, n in profile.items()), + 'invalid child profile') + terms = [(Q(n*r, m*w), logarithm(Q(m, r))) for r, n in sorted(profile.items())] + rho = Q(32*m*sum(profile.values()), 10**16*w) if surcharge else Q(0) + if surcharge: + terms.append((rho, logarithm(Q(m)))) + d = 1-sum(c for c, _ in terms) + e_lo = sum(c*lo for c, (lo, hi) in terms) + e_hi = sum(c*hi for c, (lo, hi) in terms) + f_lo = sum(c*lo*lo for c, (lo, hi) in terms) + f_hi = sum(c*hi*hi for c, (lo, hi) in terms) + l_hi = max(hi for c, (lo, hi) in terms) + require(d > 0 and e_lo > 0 and f_lo > 0, 'no positive saving domain') + return d, e_lo, e_hi, f_lo, f_hi, l_hi, rho + + +def gain(a, e, f, ell=None): + require(a >= 0 and e > 0 and f >= 0, 'invalid gain arguments') + denominator = 1 if ell is None else 1-ell*a/3 + require(denominator > 0, 'majorant pole/domain') + return e*a + f*a*a/(2*denominator) + + +def root_bracket(d, e, f, hi, ell=None): + require(d > 0 and hi > 0 and gain(hi, e, f, ell) >= d, + 'unbracketed surrogate root') + lo = Q(0) + for _ in range(100): + mid = (lo+hi)/2 + if gain(mid, e, f, ell) <= d: + lo = mid + else: + hi = mid + require(gain(lo, e, f, ell) <= d <= gain(hi, e, f, ell), + 'surrogate root sides') + return lo, hi + + +def screen(profile, m, w, surcharge): + d, e_lo, e_hi, f_lo, f_hi, l_hi, rho = coefficients(profile, m, w, surcharge) + linear = d/e_lo + require(l_hi*linear < 3, 'linear root ceiling crosses majorant pole') + lower = root_bracket(d, e_hi, f_hi, linear, l_hi)[0] + upper = root_bracket(d, e_lo, f_lo, linear)[1] + require(0 < lower < upper < linear, 'screening bounds not nested') + require(gain(lower, e_hi, f_hi, l_hi) < d, 'lower bound not strict') + require(gain(upper, e_lo, f_lo) > d, 'upper bound not strict') + return {'D': str(d), 'E': [str(e_lo), str(e_hi)], + 'F': [str(f_lo), str(f_hi)], 'L_upper': str(l_hi), + 'surcharge_coefficient': str(rho), 'linear_upper': str(linear), + 'root_lower': str(lower), 'root_upper': str(upper), + 'width': str(upper-lower), + 'log_bits': 160, 'log_terms': 72, 'bisection_steps': 100} + + +def reject(call, diagnostic): + try: + call() + except ValueError as error: + require(diagnostic in str(error), 'wrong rejection diagnostic') + else: + raise ValueError('negative control accepted') + + +def controls(): + require(logarithm(Q(1)) == (0, 0), 'log-one exact fixture') + lo, hi = logarithm(Q(2)) + require(Q(693147180559945309, 10**18) < lo < hi + < Q(693147180559945310, 10**18), 'log-two independent decimal fixture') + # Algebraic fixture: a single exp(a) curve, D=1/2. The true root ln(2) + # is bracketed by both rational surrogates with no selected-data dependency. + low = root_bracket(Q(1,2), Q(1,2), Q(1,2), Q(1), Q(1))[0] + high = root_bracket(Q(1,2), Q(1,2), Q(1,2), Q(1))[1] + require(low < lo < hi < high, 'single-exponential fixture') + # Independent exact root: M(a)=2^(a-1), a*=1. Use deliberately broad + # rational log bounds rather than the logarithm implementation above. + require(gain(Q(1), Q(1,3), Q(2,9)) == Q(4,9), 'dyadic lower fixture') + require(gain(Q(1), Q(7,20), Q(49,200), Q(7,10)) == Q(469,920), + 'dyadic upper fixture') + require(root_bracket(Q(1,2), Q(7,20), Q(49,200), Q(3,2), Q(7,10))[0] < 1 + < root_bracket(Q(1,2), Q(1,3), Q(2,9), Q(3,2))[1], + 'dyadic exact root outside surrogate bracket') + reject(lambda: logarithm(Q(0)), 'log input below one') + reject(lambda: gain(Q(3), Q(1), Q(1), Q(1)), 'majorant pole/domain') + reject(lambda: screen({1: 1}, 2, 0, False), 'invalid width or normalization') + reject(lambda: screen({2: 1}, 2, 2, False), 'invalid child profile') + reject(lambda: screen({1: 4}, 2, 2, False), 'no positive saving domain') + reject(lambda: root_bracket(Q(1), Q(1), Q(1), Q(1,10)), 'unbracketed surrogate root') + plain = coefficients({1: 1}, 2, 2, False) + charged = coefficients({1: 1}, 2, 2, True) + rho = Q(32*2, 10**16*2) + require(plain[0]-charged[0] == rho and charged[6] == rho + and charged[1]-plain[1] == rho*lo + and charged[2]-plain[2] == rho*hi + and charged[3]-plain[3] == rho*lo*lo + and charged[4]-plain[4] == rho*hi*hi, + 'surcharge exponential D/E/F contributions omitted') + require(coefficients({2: 1}, 4, 2, True)[5] + > coefficients({2: 1}, 4, 2, False)[5], + 'surcharge maximum logarithmic rate omitted') + return 12 + + +def evaluate(): + assembly = json.loads((ROOT / ASSEMBLY).read_text(encoding='utf-8')) + owner = json.loads((ROOT / OWNER).read_text(encoding='utf-8')) + bit = json.loads((ROOT / BIT).read_text(encoding='utf-8'))['nine'] + complex_profile = {int(r): n for r, n in assembly['complex_profile'].items()} + require(complex_profile == {int(r): n for r,n in owner['owner']['profile'].items()}, + 'independent owner/profile disagreement') + require(sum(r*n for r,n in complex_profile.items()) == owner['owner']['rank_mass'], + 'independent rank mass disagreement') + w = owner['price']['live'] + require(73*w-sum(r*n for r,n in complex_profile.items()) == owner['owner']['deficit'], + 'independent deficit disagreement') + bit_profile = {int(r): n for r,n in bit['profile'].items()} + require(sum(r*n for r,n in bit_profile.items()) == bit['bit']['rank_mass'], + 'bit rank mass disagreement') + require(Q(bit['bit_lower']) == Q(assembly['bit_lower']), 'selected bit endpoint disagreement') + require(assembly['surcharge_model'] == {'complex': False, 'bit': True} + and all(row['surcharge'] for row in assembly['conservative_moments']), + 'selected surcharge contract disagreement') + cases = [('native_complex', complex_profile, 73, w, False, assembly['complex_lower']), + ('conservative_complex', complex_profile, 73, w, True, assembly['conservative_complex_lower']), + ('bit', bit_profile, 64, bit['bit']['live'], True, assembly['bit_lower'])] + results = [] + for name, profile, m, live, bad, endpoint in cases: + result = screen(profile, m, live, bad) + lower, upper, linear = map(Q, [result['root_lower'], result['root_upper'], result['linear_upper']]) + alpha = Q(endpoint) + require(lower < alpha < alpha+Q(1,10**24) < upper, + 'published endpoint interval outside screening bracket') + improvement = (linear-alpha)/(upper-lower) + require(improvement > 100, 'quadratic screen did not materially narrow D/E') + result.update(name=name, m=m, W=live, surcharge=bad, endpoint=endpoint, + rank_mass=sum(r*n for r,n in profile.items()), + narrowing_factor=str(improvement), + narrowing_factor_floor=improvement.__floor__()) + results.append(result) + require(Q(results[1]['root_upper']) < Q(results[0]['linear_upper']), + 'conservative/native consistency') + return {'sources': {p: hashlib.sha256((ROOT/p).read_bytes()).hexdigest() + for p in (ASSEMBLY, OWNER, BIT)}, + 'ledgers': results, 'controls': controls(), + 'scope': 'screening brackets only; no endpoint-grid certification, word replay or new kappa'} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--write', action='store_true') + parser.add_argument('--result', type=Path, default=HERE / 'RESULT.json') + args = parser.parse_args() + result = evaluate() + path = args.result + if args.write: + path.write_text(json.dumps(result, indent=2)+'\n', encoding='utf-8') + else: + require(result == json.loads(path.read_text(encoding='utf-8')), 'result receipt mismatch') + print('PASS_SELECTED_QUADRATIC_ROOT_BRACKETS ledgers=3 controls=12 ' + 'narrowing_gt_100x surcharge_included no_new_kappa') + + +if __name__ == '__main__': + try: + main() + except (ValueError, KeyError) as error: + raise SystemExit('FAIL_SELECTED_QUADRATIC_ROOT_BRACKETS: '+str(error))