diff --git a/research/power-variation-outside-roots/README.md b/research/power-variation-outside-roots/README.md new file mode 100644 index 0000000000..6209df2d32 --- /dev/null +++ b/research/power-variation-outside-roots/README.md @@ -0,0 +1,157 @@ +# Outside-domain root witnesses for the power-variation certificate + +**Scoped proof and exact checker; no new κ.** The general-rank invoice +certificate from Ali Romman's PR5788 +([`recursive-power-variation.md`](../../docs/research/recursive-power-variation.md)) +bounds all real roots of `F(t) = Σ c_r r^t` by the number `V` of sign changes +in the rank-ordered coefficients. It spends that budget only on `t = 0`, `t = 1` +and brackets inside `(0,1)`. Roots at `t < 0` or `t > 1` leave the budget +unspent, so the report is `inconclusive`. That document's Open next question +asks for a proof that a root lies outside the domain. + +This package proves such roots from exact data and subtracts them before the +interior count. On a factored oracle census of 4,455 invoices, the predecessor +certifies 391. With this change, 2,987 are certified (2,596 newly settled). +There are no false certificates and no changed predecessor verdicts. + +For example, `4 - 8·2^t - 3^t + 2·6^t = 2(2^t - 1/2)(3^t - 4)` has `V = 2` and +equal endpoint values `-3`. The predecessor reports `inconclusive`. Here an +exact zero at `t = -1` and a sign change on `(1,2)` use both roots, so the +difference is **uniformly lower on all of `0 < t < 1`**. The fixture +`15 - 20·2^t - 3·3^t + 4·6^t` has an irrational root in `(-1,0)` and is settled +in the same way. + +## Statement + +Let `F(t) = Σ_i c_i r_i^t` with distinct positive integer ranks +`r_0 < … < r_n` and nonzero integer coefficients. Let `V` be the number of +sign changes in `c_0, …, c_n`, and let `e_0, e_1` be the exact endpoint +multiplicity lower bounds from PR5788. On the left, list +`-∞, -K, …, -1`, followed by `0` when `F(0) ≠ 0`. On the right, list `1` +when `F(1) ≠ 0`, followed by `2, …, K, +∞`. Give `-∞` the sign of `c_0` +and `+∞` the sign of `c_n`. Each finite point gets the sign of the exact +rational `F(k)`. Let `W` count the exact zeros at listed integers plus the +strict sign changes between adjacent strictly signed points, with an exact zero +breaking adjacency. Then `F` has at least `W` distinct real roots in +`(-∞,0) ∪ (1,∞)`, and + +`(roots in (0,1), with multiplicity) ≤ V - e_0 - e_1 - W`. + +If the interior brackets and exact interior zeros number exactly this +remainder, every interior root is simple and witnessed. With remainder zero +and one strict interior sample, the sign is uniform on `(0,1)`. These are +the same closure rules as PR5788, applied to a smaller budget. + +## Proof + +*Asymptotic signs.* `F(t) = r_0^t (c_0 + Σ_{i>0} c_i (r_i/r_0)^t)`. Every +ratio exceeds one, so the bracket tends to `c_0` as `t → -∞`. Hence `F` has +the sign of `c_0` on some ray `(-∞, T)`. Symmetrically, `F(t) = r_n^t (c_n + …)` +has the sign of `c_n` on some ray `(T', ∞)`. + +*Witnesses.* A strict sign change between adjacent finite listed points gives +a root in that open interval by continuity. Between `-∞` and the first finite +point `-K`, choose `T < -K` inside the asymptotic ray; the opposite signs at +`T` and `-K` give a root in `(T,-K)`. The `+∞` case is symmetric. An exact zero +at a listed integer is a root. The open intervals are pairwise disjoint. They +avoid every listed integer and neither contains `0` or `1`: the point `0` or +`1` is listed when `F` is nonzero there. When `F(0) = 0`, the last left point is +`-1` and no interval reaches `0`. So the `W` roots are distinct, lie outside +`[0,1]`, and are disjoint from the endpoint roots counted by `e_0, e_1`. + +*Budget.* PR5788 proves (generalized Descartes rule, Rolle induction) that `F` +has at most `V` real roots counted with multiplicity. Each outside witness has +multiplicity at least one. Subtracting `W` and the endpoint lower bounds leaves +the stated interior bound. The closure step is unchanged. Interior witnesses +lie in disjoint subintervals, so if they exhaust the remainder, each has +multiplicity exactly one and no other interior root exists. ∎ + +Outside witnesses only reduce an upper bound, so they cannot turn a valid +predecessor certificate into a different verdict. The census also checks this +on every fixture. + +## Evidence + +[`outside_roots.py`](outside_roots.py) imports the unchanged +`scripts/compare_power_variation.py` helpers (endpoint multiplicities, +directed interior enclosures). It adds `outside_witnesses` and the reduced +budget. Values at integer exponents are exact `Fraction`s. Reach `K` defaults +to 8 (at most 64). It accepts the same invoice pair as the shared tool: + +```sh +python3 -B research/power-variation-outside-roots/outside_roots.py OLD.json NEW.json +``` + +[`verify.py`](verify.py) checks the following (about 13 s on CPython 3.12): + +- The two fixtures above are `inconclusive` under PR5788 and become + `uniformly_lower` with the stated witnesses. +- **Factored oracle census.** Every product of one, two or three factors + `q·a^t − p` is checked. Bases are `a ∈ {2,3,5}`, three-factor products use + three distinct bases, and `p/q` ranges over 15 thresholds from `1/3` to `25`. + This gives 4,455 expanded invoices. Roots are `log(p/q)/log a` in closed form. + Interior membership (`1 < p/q < a`), integer roots and the sign at `t = 1/2` + are exact integer tests. Floats only order distinct non-integer roots, and a + near-coincidence would be excluded and counted (0 occurred). Every predecessor + and extended certificate is compared with the oracle: uniform sign, number of + interior roots, simplicity and bracket location. Result: predecessor 391 + certified, extension 2,987, newly settled 2,596. False certificates, + budget overruns and changed predecessor verdicts are all 0. 3,544 reports use + an outside witness. Both tools use a 32-cell interior grid in the census. +- **Failure controls.** Two deliberately wrong witness rules are rejected by the + same oracle. Swapping the two asymptotic signs gives 887 false certificates, + 2,026 budget overruns and 94 changed verdicts. Listing `0`/`1` as a witness + point even when `F` vanishes there double-counts endpoint roots: 463 false, + 491 overruns and 104 changed. + +Reproduce from the repository root (local run: CPython 3.12.14 at +`~/git/integer-mult-bounds/.venv/bin/python3.12`): + +```sh +python3.12 -B research/power-variation-outside-roots/verify.py +python3.12 -B scripts/research_package.py --package research/power-variation-outside-roots +python3.12 -B scripts/check_research_commit.py --package research/power-variation-outside-roots --check-source-history +``` + +Expected final line: `PASS_POWER_VARIATION_OUTSIDE_ROOTS`. The verifier +fails closed without `assert`, so an isolated optimized run +(`python3.12 -I -O -B research/power-variation-outside-roots/verify.py`) +checks the same conditions. + +## Scope and limits + +This is invoice arithmetic only. It is not a construction, source extraction, +native operator, compiler endpoint, supplier admission or new κ. The selected +result is unchanged. The census is a finite exact check of the implementation, +not a proof of completeness. Two roots in the same unit interval outside +`[0,1]` with equal signs at its ends are not witnessed; the report then stays +`inconclusive`, which remains sound. Touching interior roots (even +multiplicity) are still unresolved, as in PR5788. The shared +`scripts/compare_power_variation.py` is not modified. Merging this check into it +is a separate maintainer decision. + +## Open next questions + +Structured versions are in [TASK.json](TASK.json). + +- **Finer outside brackets.** Can rational points beyond the unit grid + (directed enclosures at `t < 0` and `t > 1`) separate two outside roots in one + unit interval? Start with `(2^t − 5/2)(3^t − 4)`, whose two roots + (about 1.32 and 1.26) both lie in `(1,2)`. The existing power engine accepts + only `0 < t < 1`, so this needs an exact `r^(k+s)` reduction. +- **Pinned source invoices.** Does any committed paid-minus-target invoice + that PR5788 leaves `inconclusive` become certified here? Run `outside_roots.py` + on the pinned P104 ledger exported by the selected-invoice tool (#5735) and + its declared edits. +- **Touching interior roots.** Even-multiplicity interior roots still block + closure. A Sturm-type argument for exponential sums with commensurable + exponents, or an exact derivative-sign witness, is needed. + +## Credit + +The root budget, endpoint multiplicities, interior brackets, invoice schema and +directed power engine are Ali Romman's PR5788/PR5746 work and their credited +predecessors (zxv's signed-invoice interface, woklerx's T16 unique-crossing +proof, mightyOil's moment-order audit). The generalized Descartes rule is +classical. New here: the outside-domain witness rule, its proof, the factored +oracle census and controls, produced by Nick Petalas. Apache-2.0. diff --git a/research/power-variation-outside-roots/SOURCES.json b/research/power-variation-outside-roots/SOURCES.json new file mode 100644 index 0000000000..50411215cc --- /dev/null +++ b/research/power-variation-outside-roots/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8", + "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "scripts/compare_power_variation.py", + "usage": "input", + "git_blob": "6a06c55174fb0f37d792ed7b84eaeae08da9c88a", + "sha256": "6650eebabaf65360b4efedb6074776b9a8966cb1bdf07650806e4361326ad590" + }, + { + "path": "scripts/compare_recursive_invoices.py", + "usage": "input", + "git_blob": "fda2a852e9937e42fe40df0707694465ca7c1b48", + "sha256": "3930c22c11da7bc6042cfeb6e459ecb06e4478430037bee3469d034353855fc6" + }, + { + "path": "scripts/evaluate_recursive_power.py", + "usage": "input", + "git_blob": "ca50f8021fc3238a58fd420383f4619a8d008ace", + "sha256": "52b20f41fd0bb55fa88dccd6015af2ce358917817b9506720f3e60ce681cc3ad" + } + ] +} diff --git a/research/power-variation-outside-roots/TASK.json b/research/power-variation-outside-roots/TASK.json new file mode 100644 index 0000000000..8a4a630fea --- /dev/null +++ b/research/power-variation-outside-roots/TASK.json @@ -0,0 +1,111 @@ +{ + "schema_version": 1, + "task_id": "independent-moment", + "priority_revision": 8, + "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "original_card": { + "id": "independent-moment", + "question": "Does a changed construction's serialized target/paid invoice independently support its claimed improvement?", + "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", + "docs/research/recursive-invoice-preflight.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": "Demonstrate independence, source binding, positive cases and semantic failure controls. Name the existing checks and the missing coverage. More digits or another equivalent evaluation of an unchanged root is not by itself new verification coverage.", + "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": "Independently recount one changed emitted word and its complete caller, importing no constructor or pricing engine. Include target losses, owned lifetimes, native orientation and extra charges. Check existing #5633/#5708/#5717/#5719 coverage to avoid duplicate audits and preserve its exact head. Stop after the chosen missing implication; a correct root alone is not supplier admission.", + "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": [ + "invoice", + "signed moment", + "productive target", + "independent recount" + ], + "existing_checks": [ + { + "scope": "PR #4088: mixed local/owner/phase ledger and moment reported.", + "evidence": "research/staged544-mixed-fourth-entry/README.md", + "remaining": "Independent binding of changed construction to paid histogram, distinct from full admission.", + "status": "author-checked", + "source_commit": "72d7efc181edb21806a878f174847c96dd410ab0", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4091: sharp pooled ceiling proposed for fixed THREE/FOUR words and inventory.", + "evidence": "research/staged-fourth-mixture-ceiling/README.md", + "remaining": "Validate dual, exhaustive pattern scope and exact source equivalence before applying to newer fills.", + "status": "author-checked", + "source_commit": "a29bdd8f56cd18b805917775cdec09ff935eddc4", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4067: paid (2,2) to (1,3) exchange and fixed OQ4 host reported.", + "evidence": "research/r437-two-window-carrier/README.md", + "remaining": "Independent full cost delta; remaining caller/precision/stock obligations are separate.", + "status": "author-checked", + "source_commit": "a95f11c52e3ca1e4c5171b3c20d8f4b0815aee2e", + "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": "Invoice-order certificate tooling: spend the generalized Descartes root budget of PR5788's general-rank power-variation comparator on exactly witnessed roots at t<0 and t>1, then close the interior count on the reduced budget.", + "scope_change_reason": "The card asks for an independent recount of a changed construction's invoice. This package instead answers the Open next question of docs/research/recursive-power-variation.md (PR5788): proving outside-domain roots so an unspent budget can be closed. It strengthens the certificate that such invoice comparisons use; it recounts no construction.", + "bottleneck_link": "Revision 8 asks contributors to compare complete paid and target power sums over the whole exponent interval; PR5788's certificate is the general-rank tool for that and returns inconclusive when roots lie outside 0 1 also consume that budget. This module certifies them with exact +rational values at integer exponents and the exact asymptotic signs + + sign F(t) = sign(c_min) as t -> -infinity, + sign F(t) = sign(c_max) as t -> +infinity, + +then runs the interior bracket count against the smaller remaining budget. +The shared script is imported unchanged. Proof: README.md. +""" +import argparse +from fractions import Fraction as Q +import json +from pathlib import Path +import sys + +sys.path.insert(0, str(Path(__file__).resolve().parents[2] / 'scripts')) +try: + import compare_power_variation as V + from compare_recursive_invoices import compare_invoices, load_invoice, require +finally: + sys.path.pop(0) + +MAX_REACH = 64 + + +def exact_value(delta, k): + """F(k) for an integer k, as an exact rational.""" + if k >= 0: + return Q(sum(n * r**k for r, n in delta.items())) + return sum((Q(n, r**-k) for r, n in delta.items()), Q(0)) + + +def outside_witnesses(delta, endpoints, reach): + """Disjoint certified roots in (-inf, 0) and (1, +inf). + + Each side is an ordered list of points with strict known signs: the + asymptotic sign, the integers out to `reach`, and the adjacent endpoint + when F is nonzero there. An exact zero at an integer point and each strict + sign change between adjacent points certify one root. The open intervals + and exact points are pairwise disjoint and avoid t = 0, 1. + """ + ranks = list(delta) + low, high = (1 if delta[ranks[0]] > 0 else -1), (1 if delta[ranks[-1]] > 0 else -1) + left = [('-inf', low)] + [(-k, exact_value(delta, -k)) for k in range(reach, 0, -1)] + right = [(k, exact_value(delta, k)) for k in range(2, reach + 1)] + [('+inf', high)] + if not endpoints['0']: + left.append((0, exact_value(delta, 0))) + if not endpoints['1']: + right.insert(0, (1, exact_value(delta, 1))) + found = [] + for side in (left, right): + previous = None + for t, value in side: + s = (value > 0) - (value < 0) + if s == 0: + found.append({'exact': str(t)}) + previous = None + continue + if previous is not None and previous[1] != s: + found.append({'left': str(previous[0]), 'right': str(t)}) + previous = (t, s) + return found + + +def classify(delta, bits=128, grid=64, reach=8): + require(type(reach) is int and 1 <= reach <= MAX_REACH, 'reach must be an integer in1..64') + require(type(bits) is int and 16 <= bits <= 256, 'bits must be an integer in16..256') + require(type(grid) is int and 2 <= grid <= 256, 'grid must be an integer in2..256') + delta = dict(sorted((int(r), n) for r, n in delta.items() if n)) + require(len(delta) <= 512, 'power comparison supports at most512 nonzero ranks') + if not delta: + return {'classification': 'equal', 'root_budget': 0, 'interior_roots': 0, + 'root_witnesses': [], 'outside_witnesses': []} + signs = [1 if n > 0 else -1 for n in delta.values()] + budget = sum(a != b for a, b in zip(signs, signs[1:])) + endpoints = {str(t): V.endpoint_multiplicity(delta, t) for t in (0, 1)} + outside = outside_witnesses(delta, endpoints, reach) + remaining = budget - sum(endpoints.values()) - len(outside) + require(remaining >= 0, 'outside and endpoint roots exceed the sign-variation budget') + points = [Q(1, 2)] if not remaining else [Q(i, grid) for i in range(grid + 1)] + values = [V.enclosure(delta, t, bits) for t in points] + point_signs = [V.sign(v) for v in values] + roots = [] + for i, t in enumerate(points): + if 0 < t < 1 and point_signs[i] == 0: + roots.append({'exact': V.witness(t, values[i])}) + if i and point_signs[i] in (-1, 1) and point_signs[i - 1] in (-1, 1): + if point_signs[i] != point_signs[i - 1]: + roots.append({'left': V.witness(points[i - 1], values[i - 1]), + 'right': V.witness(t, values[i])}) + require(len(roots) <= remaining, 'root witnesses exceed the sign-variation budget') + sample = next((V.witness(t, v) for t, v, s in zip(points, values, point_signs) + if 0 < t < 1 and s in (-1, 1)), None) + complete = len(roots) == remaining and sample is not None + classification = ('inconclusive' if not complete else 'crossing' if roots else + 'uniformly_higher' if Q(sample['lower']) > 0 else 'uniformly_lower') + return {'classification': classification, 'root_budget': budget, + 'endpoint_multiplicity_lower_bounds': endpoints, + 'outside_witnesses': outside, 'root_witnesses': roots, + 'interior_roots': len(roots) if complete else None, + 'interior_root_upper_bound': remaining, + 'all_interior_roots_simple': True if complete else None, + 'unspent_root_budget': remaining - len(roots), 'sample': sample, + 'grid': grid, 'bits': bits, 'reach': reach} + + +def compare(old, new, bits=128, grid=64, reach=8): + source = compare_invoices(old, new) + return {'schema': 'integer-mult-power-variation-outside/v1', 'contract': source['contract'], + 'quantity': source['quantity'], 'signed_net_delta': source['signed_net_delta'], + 'exponent_domain': '0 < t < 1', + **classify(source['signed_net_delta'], bits, grid, reach), + 'scope': 'Declared invoice arithmetic only. No source, native, compiler or kappa admission.'} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('old'); parser.add_argument('new') + parser.add_argument('--bits', type=int, default=128) + parser.add_argument('--grid', type=int, default=64) + parser.add_argument('--reach', type=int, default=8) + args = parser.parse_args() + try: + old, old_pin = load_invoice(args.old); new, new_pin = load_invoice(args.new) + report = compare(old, new, args.bits, args.grid, args.reach) + report['inputs'] = {'old': old_pin, 'new': new_pin} + except (OSError, ValueError, TypeError, RecursionError) as error: + print('Power variation comparison failed: ' + str(error), file=sys.stderr) + return 2 + print(json.dumps(report, indent=2, sort_keys=True)) + return 0 + + +if __name__ == '__main__': + raise SystemExit(main()) diff --git a/research/power-variation-outside-roots/verify.py b/research/power-variation-outside-roots/verify.py new file mode 100644 index 0000000000..f206934bdc --- /dev/null +++ b/research/power-variation-outside-roots/verify.py @@ -0,0 +1,193 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Check outside-domain root witnesses against an independent factored oracle. + +Every fixture is F(t) = prod_i (q_i a_i^t - p_i) with prime bases a_i and +positive rational thresholds p_i/q_i. Its real roots are known in closed form, +t_i = log(p_i/q_i)/log(a_i), so the oracle needs no root finding. The oracle +uses exact integer tests for interior membership, integer roots and the sign at +t = 1/2; floating logarithms only separate distinct non-integer roots, and any +near-coincidence between different exact keys is excluded and counted. +""" +from fractions import Fraction as Q +from itertools import combinations_with_replacement +import math +from pathlib import Path +import sys + +HERE = Path(__file__).resolve().parent +sys.path.insert(0, str(HERE)) +import outside_roots as O +sys.path.pop(0) +V = O.V + + +def check(condition, message): + """Fail closed under -O as well; assert statements would be stripped.""" + if not condition: + raise SystemExit('FAIL ' + repr(message)) + +BASES = (2, 3, 5) +THRESHOLDS = tuple(Q(x) for x in ('1/3', '1/2', '3/4', '1', '4/3', '3/2', '2', '5/2', + '3', '4', '9/2', '5', '7', '9', '25')) + + +def expand(factors): + poly = {1: 1} + for a, theta in factors: + p, q = theta.numerator, theta.denominator + out = {} + for r, n in poly.items(): + out[r * a] = out.get(r * a, 0) + n * q + out[r] = out.get(r, 0) - n * p + poly = {r: n for r, n in out.items() if n} + return poly + + +def integer_root(a, theta): + """Return m when theta = a^m exactly, else None.""" + for m in range(-8, 9): + if theta == Q(a)**m: + return m + return None + + +def truth(factors): + """Interior root keys with multiplicities, and the sign at t = 1/2.""" + roots, sign_half = {}, 1 + for a, theta in factors: + m = integer_root(a, theta) + key = ('int', m) if m is not None else ('log', a, theta) + roots[key] = roots.get(key, 0) + 1 + p, q = theta.numerator, theta.denominator + sign_half *= (q * q * a > p * p) - (q * q * a < p * p) + located = {k: (k[1] if k[0] == 'int' else math.log(k[2]) / math.log(k[1])) for k in roots} + keys = sorted(located, key=located.get) + ambiguous = any(abs(located[x] - located[y]) < 1e-9 for x, y in zip(keys, keys[1:])) + interior = {k: n for k, n in roots.items() if 0 < located[k] < 1 and + not (k[0] == 'int')} + # Interior membership is exact: 0 < log(theta)/log(a) < 1 iff 1 < theta < a. + for k in interior: + check(1 < k[2] < k[1], '1 < k[2] < k[1]') + return interior, located, sign_half, ambiguous + + +def consistent(report, factors): + """True when a certificate agrees with the oracle; inconclusive is always sound.""" + interior, located, sign_half, _ = truth(factors) + kind = report['classification'] + if kind == 'inconclusive': + return True + if any(n > 1 for n in interior.values()): + return False + if kind in ('uniformly_higher', 'uniformly_lower'): + return not interior and sign_half == (1 if kind == 'uniformly_higher' else -1) + if kind != 'crossing' or len(report['root_witnesses']) != len(interior): + return False + points = sorted(located[k] for k in interior) + for witness, point in zip(report['root_witnesses'], points): + if 'exact' in witness: + if abs(float(Q(witness['exact']['t'])) - point) > 1e-12: + return False + elif not float(Q(witness['left']['t'])) < point < float(Q(witness['right']['t'])): + return False + return True + + +def fixtures(): + factors = [(a, theta) for a in BASES for theta in THRESHOLDS] + for size in (1, 2, 3): + for combo in combinations_with_replacement(factors, size): + if size == 3 and len({a for a, _ in combo}) < 3: + continue + yield combo + + +def census(classify): + stats = {'cases': 0, 'ambiguous': 0, 'old_certified': 0, 'new_certified': 0, + 'newly_settled': 0, 'false': 0, 'budget_errors': 0, 'regressions': 0, + 'outside_used': 0} + for combo in fixtures(): + if truth(combo)[3]: + stats['ambiguous'] += 1 + continue + delta = expand(combo) + stats['cases'] += 1 + old = V.classify(delta, grid=32) + try: + new = classify(delta, grid=32) + except ValueError: + stats['budget_errors'] += 1 + continue + check(consistent(old, combo), ('predecessor certificate disagrees', combo)) + stats['false'] += not consistent(new, combo) + stats['old_certified'] += old['classification'] != 'inconclusive' + stats['new_certified'] += new['classification'] != 'inconclusive' + stats['outside_used'] += bool(new.get('outside_witnesses')) + stats['regressions'] += (old['classification'] != 'inconclusive' and + new['classification'] != old['classification']) + stats['newly_settled'] += (old['classification'] == 'inconclusive' and + new['classification'] != 'inconclusive') + return stats + + +def mutant(swap_asymptotes=False, keep_zero_endpoints=False): + """A deliberately wrong copy of outside_witnesses for failure controls.""" + def witnesses(delta, endpoints, reach): + ranks = list(delta) + low, high = (1 if delta[ranks[0]] > 0 else -1), (1 if delta[ranks[-1]] > 0 else -1) + if swap_asymptotes: + low, high = high, low + left = [('-inf', low)] + [(-k, O.exact_value(delta, -k)) for k in range(reach, 0, -1)] + right = [(k, O.exact_value(delta, k)) for k in range(2, reach + 1)] + [('+inf', high)] + if keep_zero_endpoints or not endpoints['0']: + left.append((0, O.exact_value(delta, 0))) + if keep_zero_endpoints or not endpoints['1']: + right.insert(0, (1, O.exact_value(delta, 1))) + found = [] + for side in (left, right): + previous = None + for t, value in side: + s = (value > 0) - (value < 0) + if s == 0: + found.append({'exact': str(t)}); previous = None; continue + if previous is not None and previous[1] != s: + found.append({'left': str(previous[0]), 'right': str(t)}) + previous = (t, s) + return found + return witnesses + + +def main(): + for delta, expected, outside in [ + ({1: 4, 2: -8, 3: -1, 6: 2}, 'uniformly_lower', [{'exact': '-1'}, {'left': '1', 'right': '2'}]), + ({1: 15, 2: -20, 3: -3, 6: 4}, 'uniformly_lower', + [{'left': '-1', 'right': '0'}, {'left': '1', 'right': '2'}])]: + check(V.classify(delta)['classification'] == 'inconclusive', "V.classify(delta)['classification'] == 'inconclusive'") + report = O.classify(delta) + check(report['classification'] == expected and report['outside_witnesses'] == outside, report) + check(report['unspent_root_budget'] == 0, "report['unspent_root_budget'] == 0") + print('PASS_MOTIVATING_FIXTURES 2 predecessor-inconclusive -> uniformly_lower') + + stats = census(O.classify) + print('census', stats) + check(stats['false'] == stats['budget_errors'] == stats['regressions'] == stats['ambiguous'] == 0, "stats['false'] == stats['budget_errors'] == stats['regressions'] == stats['ambiguous'] == 0") + check(stats['newly_settled'] > 0, "stats['newly_settled'] > 0") + print('PASS_FACTORED_ORACLE_CENSUS') + + original = O.outside_witnesses + try: + for name, options in (('swap_asymptotes', {'swap_asymptotes': True}), + ('count_zero_endpoints', {'keep_zero_endpoints': True})): + O.outside_witnesses = mutant(**options) + bad = census(O.classify) + failures = {k: bad[k] for k in ('false', 'budget_errors', 'regressions')} + check(sum(failures.values()) > 0, (name, bad)) + print('PASS_CONTROL_REJECTED', name, failures) + finally: + O.outside_witnesses = original + print('PASS_POWER_VARIATION_OUTSIDE_ROOTS') + + +if __name__ == '__main__': + main()