diff --git a/research/shifted-persistence-threshold/PROOF.md b/research/shifted-persistence-threshold/PROOF.md new file mode 100644 index 0000000000..f91657a594 --- /dev/null +++ b/research/shifted-persistence-threshold/PROOF.md @@ -0,0 +1,166 @@ +# A shifted sufficient threshold for the one-step comparison + +This scoped proof was produced by Nick Petalas. Apache-2.0. + +## Statement + +Let `d0,a,b` be positive integers, and put `D=d0*b`. Define + +```text +T(a,D) = 1 if a>D, + max(2, ceil((3D-a)/(2a))) if a<=D. +``` + +For every integer `m>=T(a,D)`, + +```text +(m+1)^D < 2^a m^D. (1) +``` + +Moreover, `T(a,D)<=ceil(27D/(17a))` for every positive integer `a,D`. +At `(d0,a,b)=(1,1,5)` the new sufficient threshold is the exact minimum +`7`, whereas the cited #7450 sufficient threshold is `8`. At `(1,2,5)` +both sufficient thresholds are the exact minimum `4`. + +This is a new application of a classical elementary analytic inequality. +No novelty is claimed for that inequality or for logarithmic differentiation. +The general sufficient threshold is not claimed to be an exact minimum. + +## The shifted power inequality + +For real `x>0`, put `F(x)=(2x+1) log(1+1/x)`, using natural logarithms. +Differentiation gives + +```text +F'(x) = 2 log(1+1/x) - (2x+1)/(x(x+1)). +``` + +The function `t -> 1/t` is strictly convex on the positive real axis. +On `[x,x+1]` its graph is strictly below the secant except at the endpoints. +Integration therefore gives + +```text +log(1+1/x) = integral_x^(x+1) dt/t + < (1/2)(1/x + 1/(x+1)). +``` + +Consequently `F'(x)<0`. Since `F(1)=3 log 2`, every real `x>1` satisfies +`F(x)<3 log 2`. Exponentiating, for every integer `m>=2`, + +```text +((m+1)/m)^(2m+1) < 8. (2) +``` + +At `m=1` there is equality, not strict inequality. This endpoint is why +the definition of `T` separates `a>D` and requires `m>=2` otherwise. + +## Deriving the threshold + +Suppose `m>=2` and `a(2m+1)>=3D`. Raise (2) to the positive integer power +`D` and use that exponent inequality: + +```text +((m+1)/m)^(D(2m+1)) < 2^(3D) <= 2^(a(2m+1)). +``` + +Taking a positive `(2m+1)`-st root proves (1). Its hypothesis holds when +`m>=ceil((3D-a)/(2a))`. Thus the stated `T` works when `a<=D`. + +If `a>D`, then for every integer `m>=1`, `(m+1)/m<=2`, so +`((m+1)/m)^D<=2^D<2^a`. Therefore `T=1` works in this case. + +All inequalities are strict where required. In particular, equality in +`a(2m+1)>=3D` is allowed because (2) is strict for `m>=2`. + +## Comparison with the cited bound + +The predecessor #7450 supplies `ceil(27D/(17a))` as a sufficient threshold +through a uniform binomial bound and the pair `3^17<2^27`. That predecessor +result is a cited premise, not a replay target. The following comparison is +also an elementary comparison of the two displayed formulas. + +When `a>D`, the old ceiling is at least one, so it is at least `T=1`. +When `a<=D`, put `R=D/a>=1`. The old ceiling is at least two, and + +```text +27R/17 - (3R-1)/2 = 3R/34 + 1/2 > 0. +``` + +Ceiling monotonicity then gives + +```text +max(2, ceil((3R-1)/2)) <= ceil(27R/17). +``` + +Hence the new sufficient threshold never worsens that cited threshold. + +## The two sharp examples + +For `D=5,a=1`, the new value is `ceil(14/2)=7`. At its predecessor, + +```text +7^5 = 16807 > 15552 = 2*6^5. +``` + +Thus (1) fails at `m=6`. The theorem proves (1) for every `m>=7`; +directly, `8^5=32768<33614=2*7^5`. This makes seven the least integer +threshold valid for all subsequent integers at this triple. + +For `D=5,a=2`, the new value is `ceil(13/4)=4`. At its predecessor, + +```text +4^5 = 1024 > 972 = 4*3^5. +``` + +The theorem proves (1) for every `m>=4`; directly, +`5^5=3125<4096=4*4^5`. Thus four remains the exact threshold. + +These examples do not make the general formula an exact minimum. For +`D=10,a=1`, it gives fifteen, but (1) already holds at fourteen because +`15^10=576650390625<578509309952=2*14^10`. + +## Persistence at the retained comparison + +Section 6 of the #7000 application review considers a fixed constant +`C>=1`, an integer degree `d0` and positive rational slack `delta=a/b`. +For positive `d0`, raising its comparison to the power `b` gives + +```text +P(j): C^b (j+1)^D <= 2^(aj), D=d0*b. +``` + +If `P(j)` holds and `j+1>=T(a,D)`, apply (1) at `m=j+1`: + +```text +C^b (j+2)^D < 2^a C^b (j+1)^D <= 2^(a(j+1)). +``` + +Thus `P(j+1)` holds, and induction proves `P(k)` for every integer `k>=j`. +When `d0=0`, this persistence is immediate without a threshold lemma. +This establishes a smaller sufficient one-step region. It does not supply +an initial `j` satisfying `P(j)`, compute any complete selected cutoff, +or replace the other conditions in the review. + +## Evidence and limits + +The universal claims above follow from the written argument. The verifier +corroborates (2) for `m=2..256`, and decreasing `F` at consecutive integers +for `m=1..255` by exact cross-multiplication. It checks both threshold +formulas for every `a,D=1..96`, and checks (1) at each new threshold and +the next two integers. These are bounded finite checks of this new result. +They do not replay a predecessor verifier or establish the analytic proof +by enumeration. All arithmetic in the verifier is exact integer arithmetic. + +The comparison is an auxiliary threshold lemma, not a physical supplier, +a new kappa, or a complete multiplication theorem. All five selected +framework assumptions remain. Independent human and formal proof-kernel +review are unclaimed. + +## Open next questions + +Can an elementary rational correction to the shifted bound remove the +remaining sufficient-versus-necessary gap, such as fifteen versus fourteen +at `D=10,a=1`? A first step is an explicit upper bound for +`log(1+1/m)` with one more rational term and a proof that the resulting +integer test is no worse. This may reduce the auxiliary persistence region; +it does not determine the initial selected cutoff or settle physical costs. diff --git a/research/shifted-persistence-threshold/README.md b/research/shifted-persistence-threshold/README.md new file mode 100644 index 0000000000..3c353a825b --- /dev/null +++ b/research/shifted-persistence-threshold/README.md @@ -0,0 +1,119 @@ +# A shifted persistence threshold that includes the missing seven-step case + +This contribution was produced by Nick Petalas. Apache-2.0. + +Claim type: scoped written proof with exact finite corroboration. For +positive integers `d0,a,b`, set `D=d0*b` and + +```text +T = 1 if a>D, + max(2,ceil((3D-a)/(2a))) otherwise. +``` + +For every integer `m>=T`, `(m+1)^D < 2^a m^D`. The new `T` is never larger +than `ceil(27D/(17a))`, the sufficient threshold in unpaidmoon's +[PR #7450](https://github.com/CrocSwap/integer-mult-bounds/pull/7450). +At `(d0,a,b)=(1,1,5)` it lowers eight to the sharp seven. At `(1,2,5)` +the sharp four is preserved. The proof uses the classical decreasing +function `(2x+1) log(1+1/x)`. The threshold application is the new result. + +[PROOF.md](PROOF.md) gives the complete argument, the exact endpoint +exception at `m=1`, and the persistence implication. The general sufficient +threshold is not an exact minimum. For example it gives fifteen at +`D=10,a=1`, where fourteen already works. + +## Source and scope + +This answers Open next question 1 of unpaidmoon #7450 at +`f9b9057f9befe744df7f6b58b61b53e77001af1f` using an `m`-dependent inequality, +instead of refining another pair `3^p<2^q` under its uniform bound. Its +power-pair census and persistence construction are cited, not audited or +replayed. The question is the source; the classical convexity argument is +self-contained. No predecessor code or data is needed to run this verifier. + +The retained comparison is section 6 of +[the #7000 application review](../../docs/research/pr-intake-evidence/pr7000-application/PROOF-REVIEW.md). +[SOURCES.json](SOURCES.json) pins that historical context, the selected +record and the originating card at canonical base +`e54523517d0f03e58352e647c403a5af3e525a57`. These are provenance, not live +mathematical inputs. The source PR is external context with its exact head +and URL recorded in [TASK.json](TASK.json). + +Card `uniform-transfer-audit` has changed scope to this auxiliary lemma. +It reduces a sufficient persistence region relevant to the effective +cutoff discussion. It neither constructs the initial successful index nor +discharges `precision_tape` or another framework assumption. Selected +`kappa=363005817/100000000000` is unchanged. + +## Reproduce + +Use CPython 3.12 and the standard library, from the repository root: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/shifted-persistence-threshold/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -O -W error -B research/shifted-persistence-threshold/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/shifted-persistence-threshold +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/shifted-persistence-threshold --check-source-history +``` + +On another machine, substitute its CPython 3.12 executable. The direct +verifier emits `PASS_SHIFTED_PERSISTENCE_THRESHOLD` in a JSON receipt +containing all six package-file SHA256 hashes and the exact enumerated +counts. Redirect it outside the checkout to retain a generated receipt. +No handwritten receipt or generated replay output is committed. + +The bounded checks cover 255 shifted-power cases, 255 consecutive decreases, +9,216 parameter pairs and 27,648 one-step evaluations. In that parameter +rectangle, 4,753 threshold pairs strictly improve. Nine semantic controls +cover both sharp examples, strict equality, the `m=1` branch, a +sufficient-versus-necessary distinction and an overstrong slope. Eight +invalid parameter pairs must fail with the exact declared reason. Optimized +execution keeps every check active because checks do not rely on `assert`. + +No selected cold replay, predecessor scientific suite, Lean or Docker run +is needed for this local theorem. No hosted CI success is claimed here. + +## Verification design + +`verify.py` has a fixed finite workload, no recursion, subprocesses, +network calls, file writes or dynamic dispatch. All functions are shorter +than sixty lines. Positive-integer arguments are validated at the threshold +boundary; all result checks raise explicit errors even under `-O`. + +Power of Ten rule 3 has a managed-runtime deviation in `verify.py`: CPython +allocates arbitrary-precision integers during execution. The finite ranges +bound each power-product operand below `2^10240`, and the verifier retains +only one case at a time plus six source hashes. The registered commands +exercise that complete bounded workload. If these ranges become configurable, +the change must introduce explicit input and memory caps. Python has no +compiler warning mode; both registered commands use `-W error`. The package +does not alter shared diagnostics or repository CI configuration. Ruff and +Mypy are unavailable on the local PATH; in-memory compilation and the +warning-strict registered replays are the available Python diagnostics. + +## Related open work + +- [#7450](https://github.com/CrocSwap/integer-mult-bounds/pull/7450), unpaidmoon, + supplies the `27/17` bound and explicitly asks about the missing `m=7` + case. This proof includes that case and retains the same sharp four. +- [#7286](https://github.com/CrocSwap/integer-mult-bounds/pull/7286), unpaidmoon, + tightens a monomial record count used elsewhere in the same review. + Its count and elimination model are independent of this one-step inequality. + +## Open next questions + +The final section of [PROOF.md](PROOF.md) asks for a sharper elementary +correction where this sufficient bound exceeds the true threshold. Its +first example is `D=10,a=1`; no external blocker is required to begin. +Physical implementation, complete cutoffs, supplier admission and all five +framework assumptions remain separate obligations. + +## Credit + +Credit unpaidmoon #7450 for the source question, the prior `27/17` threshold +and its retained persistence-note lineage at +`8e0124415604b89a1cfc842cb6dc6da96ea87ac5`. Credit Douglas Colkitt's retained +#7000 application review for the effective-cutoff comparison. The convexity, +logarithm and induction arguments are classical. The shifted +threshold, its application and its exact verifier were produced by Nick +Petalas. Independent human and formal proof-kernel review are unclaimed. diff --git a/research/shifted-persistence-threshold/SOURCES.json b/research/shifted-persistence-threshold/SOURCES.json new file mode 100644 index 0000000000..cfcfe0ca38 --- /dev/null +++ b/research/shifted-persistence-threshold/SOURCES.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "75d77b328ea02ded535e7f23aee5b1e55d0bb1a8", + "sha256": "154c3d30455d778fd3343b6b4851f0fa4665f0f7625b0adb3675e2bafbbf6bf1" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "docs/research/pr-intake-evidence/pr7000-application/PROOF-REVIEW.md", + "usage": "provenance", + "git_blob": "3dd1af2285e597676725e85ad4f65e7ad326d695", + "sha256": "4501502c2ceb9759b20372435fe4beb51082c5a5e2910c1fd5dbe6edca415055" + } + ] +} diff --git a/research/shifted-persistence-threshold/TASK.json b/research/shifted-persistence-threshold/TASK.json new file mode 100644 index 0000000000..c5fadef43c --- /dev/null +++ b/research/shifted-persistence-threshold/TASK.json @@ -0,0 +1,111 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 8, + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "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": "A self-contained shifted sufficient threshold for (m+1)^(d0*b) < 2^a m^(d0*b), with exact sharp seven and four examples.", + "scope_change_reason": "Answer Open next question 1 of unpaidmoon PR7450 rather than audit a predecessor or discharge a complete selected assumption.", + "bottleneck_link": "Auxiliary effective-cutoff persistence comparison in section 6 of the selected #7000 application review. This changes a sufficient one-step region only.", + "budget_minutes": 60, + "stop_rule": "Stop after the first proved threshold improvement and its bounded exact verifier.", + "outcome": "completed", + "evidence": "PROOF.md is the scoped universal argument; verify.py corroborates shifted powers, 9216 parameter pairs, 27648 steps and boundary/failure controls. It emits generated six-file hash-bound JSON receipts.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can a further rational correction reduce the gap between the shifted sufficient threshold and the exact minimum, first at D=10,a=1?", + "why_it_matters": "A smaller sufficient region can reduce an auxiliary effective-cutoff requirement without changing the supplier.", + "first_step": "Bound log(1+1/m) with one more rational term and derive a sufficient integer inequality that is no worse.", + "blocked_by": "No external blocker; initial successful cutoff and physical costs remain separate." + } + ], + "claim_type": "scoped proof with exact finite corroboration", + "source_question": { + "pr": 7450, + "author": "unpaidmoon", + "head": "f9b9057f9befe744df7f6b58b61b53e77001af1f", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/7450", + "location": "research/threshold-ratio-sharper-pair/README.md, Open next questions 1", + "usage": "external context; no predecessor computation is replayed" + }, + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19572802", + "environment": { + "interpreter": "/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12", + "dependencies": "standard library only", + "python_version": "3.12.15" + }, + "overlap": { + "checked_at": "2026-11-12T19:17:00Z", + "open_prs": 768, + "discussion_records": 7356, + "own_recent_prs_in_source_check": 106, + "own_recent_source_matches": 0, + "note": "Full remote pagination; sparse local scan supplemented by origin/main README Git searches. Keyword checks are leads, not a novelty certificate.", + "precommit_refresh": { + "canonical_main": "e54523517d0f03e58352e647c403a5af3e525a57", + "no_new_overlapping_claim_found": true, + "merged_search": "Exact one-step, threshold-ratio, shifted threshold and general polynomial/exponential context; #6109 is a different source-specific compiler-grid binding." + } + } +} diff --git a/research/shifted-persistence-threshold/VERIFY.json b/research/shifted-persistence-threshold/VERIFY.json new file mode 100644 index 0000000000..966a1c15c2 --- /dev/null +++ b/research/shifted-persistence-threshold/VERIFY.json @@ -0,0 +1,32 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Exact shifted-power and monotonicity comparisons, all a,D=1..96 threshold pairs and three steps each, sharp/boundary/overstrong controls, invalid inputs; generated package hashes. Checks remain active under optimization." + }, + { + "argv": [ + "{python}", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Exact shifted-power and monotonicity comparisons, all a,D=1..96 threshold pairs and three steps each, sharp/boundary/overstrong controls, invalid inputs; generated package hashes. Checks remain active under optimization." + } + ] +} diff --git a/research/shifted-persistence-threshold/verify.py b/research/shifted-persistence-threshold/verify.py new file mode 100644 index 0000000000..045d0cc376 --- /dev/null +++ b/research/shifted-persistence-threshold/verify.py @@ -0,0 +1,120 @@ +#!/usr/bin/env python3 +"""Exact finite corroboration of the shifted persistence threshold. + +Produced by Nick Petalas. Apache-2.0. +The universal argument is in PROOF.md; this program uses integers only. +""" + +import hashlib +import json +import platform +import sys +from pathlib import Path + + +def require(condition: bool, message: str) -> None: + if not condition: + raise ValueError(message) + + +def threshold(a: int, degree: int) -> int: + """Return the new sufficient threshold, with D named degree.""" + if type(a) is not int or type(degree) is not int: + raise ValueError("a and D must be positive integers") + if a < 1 or degree < 1: + raise ValueError("a and D must be positive integers") + if a > degree: + return 1 + return max(2, (3 * degree - a + 2 * a - 1) // (2 * a)) + + +def step(a: int, degree: int, m: int) -> bool: + return (m + 1) ** degree < (1 << a) * m ** degree + + +def check_shifted_power() -> dict[str, int]: + powers = 0 + decreases = 0 + for m in range(2, 257): + require((m + 1) ** (2 * m + 1) < 8 * m ** (2 * m + 1), + f"shifted power failed at {m}") + powers += 1 + for m in range(1, 256): + # Cross-multiply F(m)>F(m+1), without logarithms or floats. + left = (m + 1) ** (4 * m + 4) + right = m ** (2 * m + 1) * (m + 2) ** (2 * m + 3) + require(left > right, f"shifted decrease failed at {m}") + decreases += 1 + return {"shifted_power_cases": powers, "decrease_cases": decreases} + + +def check_thresholds() -> dict[str, int]: + parameters = 0 + steps = 0 + drops = 0 + for a in range(1, 97): + for degree in range(1, 97): + new = threshold(a, degree) + old = (27 * degree + 17 * a - 1) // (17 * a) + require(new <= old, f"threshold worsened at {a},{degree}") + if a <= degree: + require(a * (2 * new + 1) >= 3 * degree, + "shifted exponent hypothesis missing") + for m in range(new, new + 3): + require(step(a, degree, m), f"step failed at {a},{degree},{m}") + steps += 1 + drops += int(new < old) + parameters += 1 + return {"parameter_pairs": parameters, "step_cases": steps, + "strict_threshold_drops": drops} + + +def check_controls() -> dict[str, int]: + controls = ( + (threshold(1, 5) == 7, "new first working example missing"), + (step(1, 5, 7) and not step(1, 5, 6), "seven not sharp"), + (threshold(2, 5) == 4, "second example changed"), + (step(2, 5, 4) and not step(2, 5, 3), "four not sharp"), + (not step(1, 1, 1), "strict equality was accepted"), + (threshold(1, 1) == 2, "m=1 equality exception missing"), + (threshold(2, 1) == 1 and step(2, 1, 1), "m=1 success missing"), + (threshold(1, 10) == 15 and step(1, 10, 14), "threshold not necessary"), + # A smaller, unproved 7/5 slope would propose m=8 at D=6,a=1. + (not step(1, 6, 8), "overstrong slope control did not reject"), + ) + for condition, message in controls: + require(condition, message) + invalid = ((0, 1), (1, 0), (-1, 1), (1, -1), + (True, 1), (1, False), (1.0, 1), (1, "1")) + rejected = 0 + for a, degree in invalid: + try: + threshold(a, degree) + except ValueError as error: + require(str(error) == "a and D must be positive integers", + "wrong rejection reason") + rejected += 1 + else: + raise ValueError("invalid input accepted") + return {"semantic_controls": len(controls), "invalid_input_controls": rejected} + + +def main() -> None: + require(len(sys.argv) == 1, "usage: verify.py") + counts = {} + counts.update(check_shifted_power()) + counts.update(check_thresholds()) + counts.update(check_controls()) + package = Path(__file__).resolve().parent + names = ("README.md", "PROOF.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_SHIFTED_PERSISTENCE_THRESHOLD", + "claim_type": "scoped proof with finite corroboration", + "counts": counts, "python": platform.python_version(), + "package_sha256": hashes}, sort_keys=True)) + + +if __name__ == "__main__": + main()