diff --git a/research/hardy-inverse-constant/PROOF.md b/research/hardy-inverse-constant/PROOF.md new file mode 100644 index 0000000000..46c4f2e160 --- /dev/null +++ b/research/hardy-inverse-constant/PROOF.md @@ -0,0 +1,149 @@ +# A sharper constant in the degree-controlled inverse envelope + +The claim is a scoped analytic proof. Let P be a nonzero complex polynomial +of degree n and suppose |P(z)| >= delta > 0 on the unit circle. Let m be +the number of roots strictly inside the circle, including multiplicity. +With normalized circle measure and the two-sided Fourier coefficient norm W, + +\[ + \|1/P\|_W\le\frac{(1+\pi m)(1+\pi n)}{\delta} + \le\frac{(1+22m/7)(1+22n/7)}{\delta}. \tag{1} +\] + +The second inequality is strict when n>0. For n=0 both expressions equal +1/delta. If U is an invertible bounded operator on a complex Banach space +with ||U^k|| <= 1 for every integer k, the same right side bounds +||P(U)^(-1)||. Thus the statement covers unit-phase cyclic shifts at +every length and integer stride, including zero and noncoprime strides. + +Rafael Guevara's PR803 proves the same assertions with 4 in place of pi. +Its proof at `a0f15ce84f0951f69b39795f229cb854307ca52b`, retained unchanged +on the package base, supplies the Hardy factorization, normalized rational +arc-length inequality, root reflection and operator substitution used below. +Those are cited premises. This contribution sharpens the coefficient +estimate in that chain; it does not audit the predecessor or claim a new +Hardy inequality. + +## 1. Evaluate the Schur integral instead of splitting it + +For j,k >= 0 put K_jk=1/(j+k+1), w_j=(j+1/2)^(-1/2), and a=j+1/2. +The positive function f_a(x)=1/((a+x)sqrt(x)) is convex on x>0, since + +\[ + f_a''(x)=\frac{3}{4x^{5/2}(a+x)} + +\frac{1}{x^{3/2}(a+x)^2} + +\frac{2}{x^{1/2}(a+x)^3}>0. +\] + +The midpoint bound, including the integrable interval starting at zero, +gives the same Schur row estimate as PR803 Section 1. Evaluate its integral +using x=a t^2: + +\[ + \sum_{k\ge0}K_{jk}w_k + \le\int_0^\infty\frac{dx}{(a+x)\sqrt{x}} + =\frac{2}{\sqrt a}\int_0^\infty\frac{dt}{1+t^2} + =\pi w_j. \tag{2} +\] + +PR803 instead bounds the two parts at x=a separately, obtaining 4w_j. +The weighted Cauchy-Schwarz argument applied to finite nonnegative +sequences s,t therefore gives + +\[ + \sum_{j,k}K_{jk}s_jt_k\le\pi\|s\|_2\|t\|_2. \tag{3} +\] + +For h analytic in a neighborhood of the closed disk, use the classical +Hardy factorization h=ab with ||a||_2 ||b||_2=||h||_1, as in PR803 +Section 1. Coefficient convolution, (3), and increasing finite truncations +give + +\[ + \sum_{l\ge0}\frac{|h_l|}{l+1}\le\pi\|h\|_1. \tag{4} +\] + +The predecessor's radial limit handles boundary zeros of h. The constant +change does not alter that limit or any analyticity hypothesis. + +## 2. Carry the constant through the inherited analytic chain + +For a rational R of degree at most d analytic near the closed disk, apply +(4) to h=R'. The normalized Dolzhenko-Spijker inequality, used in PR803 +Sections 2 and 3, is ||R'||_1 <= d||R||_infinity. Consequently + +\[ + \|R\|_W + \le |R(0)|+\pi\|R'\|_1 + \le(1+\pi d)\|R\|_\infty. \tag{5} +\] + +Use the exact factorization P=JQ from PR803 Section 4. Here J is the +finite Blaschke product of the m interior roots, has rational degree m +and unit circle magnitude one. The polynomial Q has degree at most n +and no roots in the closed disk, with |Q|=|P| on the circle. Hence J +and 1/Q are analytic near the closed disk. Applying (5) gives + +\[ + \|J\|_W\le1+\pi m,\qquad + \|1/Q\|_W\le(1+\pi n)/\delta. +\] + +On the circle, 1/P=conjugate(J)/Q. Absolute coefficient convolution gives +the first bound in (1). PR803 Section 5's absolutely convergent +two-sided operator substitution then gives the asserted operator bound. +This uses the full integer-power hypothesis; spectral location alone is +not a replacement. No roots need to be computed to apply the bound with m=n. + +## 3. A rational upper certificate and strict improvement + +The elementary polynomial identity + +\[ + x^4(1-x)^4=(1+x^2)(x^6-4x^5+5x^4-4x^2+4)-4 +\] + +integrates on [0,1] to + +\[ + 0<\int_0^1\frac{x^4(1-x)^4}{1+x^2}\,dx + =\frac{22}{7}-\pi. \tag{6} +\] + +The numerator is positive on (0,1), and the quotient polynomial has +integral 22/7. This proves the rational version of (1) without a decimal +approximation to pi. The integral certificate is classical; no historical +priority is asserted for it or for the Hardy constant pi. + +The exact difference between the old and new rational multipliers is + +\[ + (1+4m)(1+4n)-(1+22m/7)(1+22n/7) + =\frac67(m+n)+\frac{300}{49}mn. \tag{7} +\] + +It is positive for every n>0 and 0<=m<=n. At m=n the leading quadratic +coefficient decreases from 16 to 484/49, a ratio of 121/196. This is a +comparison of sufficient upper bounds. It is not a ratio of actual norms +or a lower bound on the improvement to a working implementation. + +## 4. Scope of the exact checks + +The verifier checks (6)'s polynomial identity and rational integral, (7) +on its declared finite calibration domain, exact binary ceiling brackets, +and new sufficient norm budgets for fourteen named prime-power radices. +The budget input from PR803 Section 5 is the cited circle certificate +delta^(-1)=2rn(2^r-1)^(n phi(r)-1), with n=r-1. We substitute the new +multiplier, not replay the source's circle theorem or numerical results. +Later #1025 improves that gap certificate in another regime; the theorem +here accepts any independently supplied positive delta, including that one. + +Finite checks do not prove the infinite Schur bound, classical arc-length +premise, or analytic limits. Those are the written argument and explicit +dependencies above. No optimal degree dependence, paid inverse routine, +rounded precision recurrence, complete supplier or multiplication theorem +is established. Independent human and formal proof-kernel review are unclaimed. + +This refinement was produced by Nick Petalas. Credit Rafael Guevara/PR803, +Ali Romman/PR621, and the classical Hardy, Hilbert, Blaschke, +Dolzhenko-Spijker and Baranov-Zarouf lineage retained in PR803. Apache-2.0. diff --git a/research/hardy-inverse-constant/README.md b/research/hardy-inverse-constant/README.md new file mode 100644 index 0000000000..cc14496429 --- /dev/null +++ b/research/hardy-inverse-constant/README.md @@ -0,0 +1,98 @@ +# A sharper degree-controlled cyclic inverse constant + +For a degree-n polynomial P with |P| >= delta > 0 on the unit circle, +and m interior roots counted with multiplicity, this scoped analytic proof gives + +\[ + \|1/P\|_W\le(1+\pi m)(1+\pi n)/\delta + \le(1+22m/7)(1+22n/7)/\delta. +\] + +The same envelope bounds ||P(U)^(-1)|| whenever U is an invertible bounded +operator with ||U^k|| <= 1 for every integer k. In particular it applies +to unit-phase cyclic shifts at every length and stride. + +Rafael Guevara's [PR803](https://github.com/CrocSwap/integer-mult-bounds/pull/803) +uses 4 instead of pi. The new step evaluates its positive Schur kernel +integral exactly, then carries the smaller constant through its cited +Hardy, rational arc-length and root-reflection chain. The rational envelope +is strictly smaller at every positive degree. The leading quadratic +coefficient at m=n changes from 16 to 484/49. + +The sufficient binary norm-bound ceilings decrease from 19 to 18 at radix 3, +441 to 440 at radix 9, 11,999 to 11,998 at radix 25, and 347,859 to 347,858 +at radix 71, using the same explicit PR621 circle certificate. These are +ceilings of upper bounds, not measured norms or working-precision savings. +Later PR1025's improved circle gap is a separate input and is compatible +with the general delta-parametric statement. + +[PROOF.md](PROOF.md) contains the written all-degree argument and identifies +the inherited analytic premises. The classical constant pi and the positive +integral proving pi<22/7 are not new mathematics. This contribution is the +strict refinement of the repository's explicit inverse envelope. No optimal +degree dependence, paid inverse algorithm, rounded implementation, complete +supplier or new kappa is claimed. + +## Reproduce + +Use CPython 3.12 and the standard library, from the worktree root: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/hardy-inverse-constant +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/hardy-inverse-constant/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/hardy-inverse-constant --check-source-history +``` + +Other machines can substitute their CPython 3.12 executable. The registered +commands run both normal and optimized Python. They print +`PASS_HARDY_INVERSE_CONSTANT` in a generated JSON receipt containing exact +results and SHA256 bindings to every package file and the consumed proof. +An optional `--emit /absolute/external/new-receipt.json` creates that receipt +outside the checkout and refuses overwrites. No receipt is hand-written. + +The checks cover the polynomial division and rational integral for pi<22/7, +8,385 degree pairs with 0<=m<=n<=128, 4,096 exact logarithm brackets, +fourteen named prime-power norm budgets, and seven rejection controls. +Finite checks corroborate the new rational arithmetic; they do not prove +the analytic limits or independently validate PR803. No predecessor verifier +is run. Source bindings are in [SOURCES.json](SOURCES.json); the catalogue +and selected record are historical provenance. The originating scope change +and next questions are explicit in [TASK.json](TASK.json). + +## Verification limits + +The analytic proof is conditional on the explicitly cited classical and +PR803 implications. Independent human and formal proof-kernel review are +unclaimed. Rounded scan errors, preparation, routing, restoration and full +supplier admission are unrun obligations. No selected frontier changes. + +The verifier has no recursion, subprocesses or network access. Its numerical +loops have fixed finite domains; the largest budget uses fewer than 350,000 +bits. Functions are shorter than 60 lines, and required invariants use +explicit exceptions under optimized Python. Python's managed allocation is +a documented deviation from fixed allocation: only fourteen bounded budget +rows are retained, each source file is capped at two MiB, and no steady +service loop or mutable shared state exists. The written theorem has no +finite-degree or radix ceiling; those limits apply only to calibration. + +## Open next questions + +- Integrate the smaller envelope into one actual PR628 or PR764 rounded + precision recurrence. Start with its explicitly consumed inverse norm, + retaining preparation, every error source and dirty restoration. No such + implementation or resource improvement is supplied here. +- Improve the quadratic degree dependence. Start with a direct two-sided + Wiener estimate that avoids separately multiplying the reflected factors. + Neither this proof nor PR803 establishes an optimal degree multiplier. + +## Credit + +This refinement was produced by Nick Petalas. Credit Rafael Guevara/PR803 +for the degree-controlled inverse argument; Ali Romman/PR621 for the +prime-power setting and circle certificate; Hardy, Hilbert, Blaschke, +Dolzhenko and Spijker for the classical analytic ingredients; and +Baranov-Zarouf for the normalized arc-length source retained by PR803. +Thiago Costa/PR832 supplies a distinct Sobolev estimate, William Lawyer/PR852 +treats weighted power caps, and Philipp/PR1025 improves the circle gap. +Their results are cited, not rechecked or incorporated as new work here. +Apache-2.0. diff --git a/research/hardy-inverse-constant/SOURCES.json b/research/hardy-inverse-constant/SOURCES.json new file mode 100644 index 0000000000..e56450097a --- /dev/null +++ b/research/hardy-inverse-constant/SOURCES.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "base_commit": "4c0a359d88f22f05189d51f48387750b801a45d4", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395", + "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "research/rational-circle-bound/PROOF.md", + "usage": "input", + "git_blob": "15d344789d1ae475790f5d6a45cd37ae27f05d1c", + "sha256": "6c28d93d9d1d37da0bbc3876070ef8c6f0f5dad8e186b31b31330028e5420c0e" + } + ] +} diff --git a/research/hardy-inverse-constant/TASK.json b/research/hardy-inverse-constant/TASK.json new file mode 100644 index 0000000000..beee7ba7e9 --- /dev/null +++ b/research/hardy-inverse-constant/TASK.json @@ -0,0 +1,92 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 7, + "base_commit": "4c0a359d88f22f05189d51f48387750b801a45d4", + "original_card": { + "id": "uniform-transfer-audit", + "question": "Does one quantified step of the proposed #4100 all-size construction hold at its actual caller?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/unconditional-batched-crt/README.md" + ], + "methods": [ + "Prove one missing implication with explicit quantified hypotheses.", + "Find an exact counterexample at the claimed interface boundary." + ], + "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_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read PROOF.md and AUDIT.md in #4100. Select one distinct obligation: CRT total repair, native/free-algebra lifting, precision/conditioning, or complete fixed-tape cost. This is an author-submitted proof, not an accepted unconditional theorem.", + "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately." + }, + "first_experiment": "Check live handoffs; name one proposition, its caller, quantified domain and dependency closure. Independently prove the implication or exhibit a precise gap/counterexample. Prioritize CRT.md total repair or COMPLEX.md free-algebra lift only if unclaimed. Stop at the chosen obligation; do not substitute finite samples or root arithmetic for an all-size proof, or launch the complete package by default.", + "bottleneck_link": "Finite supplier improvements are useful only under the retained transfer obligations.", + "allowed_variations": [ + "One CRT repair, native lift, precision/conditioning or tape-cost proposition, with its exact caller." + ], + "scope_change_triggers": [ + "Replacing a quantified obligation with another finite smoke test.", + "Treating archive intake, an author PASS receipt or a finite composed fixture as discharge of the universal hypotheses." + ], + "overlap_terms": [ + "uniform transfer", + "all-size", + "precision", + "4100", + "unconditional-batched-crt" + ], + "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_status": "changed", + "actual_scope": "Sharpen PR803's degree-controlled Wiener and cyclic inverse upper envelope by replacing its Hardy coefficient constant 4 with pi, with a fully rational 22/7 upper certificate.", + "scope_change_reason": "The original card asks to audit one all-size construction implication. This is an original analytic constant improvement to a separately scoped inverse estimate; no predecessor audit or full caller admission is attempted.", + "bottleneck_link": "A smaller analytic inverse envelope can reduce a sufficient normalization or precision budget for cyclic components. Incorporation into a rounded paid caller remains an open obligation; this is an analytic side result.", + "budget_minutes": 60, + "stop_rule": "Package the first proved strict constant improvement; do not optimize the degree factor or begin a rounded implementation.", + "outcome": "completed", + "evidence": "PROOF.md derives the pi Schur constant and its operator corollary. verify.py checks the polynomial integral certificate, 8385 degree pairs, 4096 exact binary ceiling brackets, fourteen radix budgets and seven rejection controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Does this smaller inverse envelope lower a concrete rounded cyclic caller's sufficient precision?", + "why_it_matters": "An analytic norm improvement changes execution resources only after every error source, preparation and restoration charge is included.", + "first_step": "Select one PR628 or PR764 rounded scan with an explicit consumed inverse norm, and substitute this envelope into that one recurrence.", + "blocked_by": "No rounded scan, factor preparation or dirty restoration implementation is supplied here." + }, + { + "question": "Can the quadratic degree multiplier be replaced by a smaller asymptotic degree dependence?", + "why_it_matters": "The present improvement only changes constants; the separate Blaschke and reflected reciprocal factors are still multiplied.", + "first_step": "Study a direct two-sided Wiener estimate for one rational function, retaining a uniform circle-gap premise.", + "blocked_by": "The inherited argument separately bounds the two analytic factors and gives no optimality theorem." + } + ], + "claim_type": "scoped proof", + "predecessors": [ + { + "pr": 803, + "author": "Rafael Guevara", + "proof_commit": "a0f15ce84f0951f69b39795f229cb854307ca52b" + }, + { + "pr": 621, + "author": "Ali Romman" + } + ] +} diff --git a/research/hardy-inverse-constant/VERIFY.json b/research/hardy-inverse-constant/VERIFY.json new file mode 100644 index 0000000000..7e2adbc216 --- /dev/null +++ b/research/hardy-inverse-constant/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/rational-circle-bound/PROOF.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Exact rational pi upper certificate, strict degree-envelope improvement, binary ceilings, fourteen radix budgets and seven semantic rejection controls." + }, + { + "argv": [ + "{python}", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Repeat the same exact checks with optimization enabled; executable invariants remain active." + } + ] +} diff --git a/research/hardy-inverse-constant/verify.py b/research/hardy-inverse-constant/verify.py new file mode 100644 index 0000000000..6f9e5dc39c --- /dev/null +++ b/research/hardy-inverse-constant/verify.py @@ -0,0 +1,184 @@ +#!/usr/bin/env python3 +"""Check the rational Hardy constant and derived norm budgets exactly.""" + +import argparse +from fractions import Fraction as F +import hashlib +import json +from pathlib import Path + + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parents[1] +LIMIT = 2 * 1024 * 1024 +RADICES = (3, 4, 5, 7, 8, 9, 11, 16, 25, 27, 32, 49, 64, 71) +CONSTANT = F(22, 7) + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def multiply(left, right): + result = [F(0)] * (len(left) + len(right) - 1) + for i, a in enumerate(left): + for j, b in enumerate(right): + result[i + j] += a * b + return tuple(result) + + +def integral(polynomial): + return sum((F(c, i + 1) for i, c in enumerate(polynomial)), F(0)) + + +def check_certificate(quotient, remainder): + # x^4(1-x)^4 = (1+x^2)Q(x) - 4. + numerator = (0, 0, 0, 0, 1, -4, 6, -4, 1) + product = list(multiply((1, 0, 1), quotient)) + product[0] += remainder + require(tuple(product) == numerator, "polynomial division certificate") + require(remainder == -4, "arctangent coefficient must give pi") + require(integral(quotient) == CONSTANT, "rational integral must be 22/7") + return { + "quotient": list(quotient), + "remainder": remainder, + "integral_quotient": str(integral(quotient)), + "integral_positive_numerator": str(integral(numerator)), + } + + +def envelope(n, m, delta, constant=CONSTANT): + require(type(n) is int and type(m) is int, "degrees must be exact integers") + require(0 <= m <= n <= 128, "finite calibration degree domain") + require(delta > 0 and constant > 0, "positive gap and coefficient constant") + return (1 + constant * m) * (1 + constant * n) / delta + + +def ceil_log2(value): + require(value > 0, "logarithm argument must be positive") + numerator, denominator = value.numerator, value.denominator + exponent = numerator.bit_length() - denominator.bit_length() + below = (numerator <= denominator << exponent) if exponent >= 0 else ( + numerator << -exponent <= denominator) + return exponent if below else exponent + 1 + + +def prime_power(r): + for p in range(2, r + 1): + if r % p == 0: + power, exponent = p, 1 + for _ in range(r.bit_length()): + if power >= r: + break + power *= p + exponent += 1 + require(power == r, "radix must be a prime power") + return p, exponent + raise ValueError("radix must exceed one") + + +def budget_rows(): + rows = [] + for r in RADICES: + p, exponent = prime_power(r) + n, degree, height = r - 1, r - r // p, 2 ** r - 1 + gap_inverse = 2 * r * n * height ** (n * degree - 1) + old = F(gap_inverse * (1 + 4 * n) ** 2) + new = gap_inverse * (1 + CONSTANT * n) ** 2 + require(new < old, "strict rational-envelope improvement") + old_bits, new_bits = ceil_log2(old), ceil_log2(new) + require(new_bits <= old_bits, "ceiling monotonicity") + rows.append({"radix": r, "prime": p, "prime_exponent": exponent, + "old_bound_bits": old_bits, "new_bound_bits": new_bits, + "saved_bound_bits": old_bits - new_bits}) + return rows + + +def rejection_controls(): + bad_arguments = ((-1, 0, F(1)), (1, 2, F(1)), (1, 0, F(0)), + (1, 0, F(-1)), (True, 0, F(1))) + rejected = 0 + for args in bad_arguments: + try: + envelope(*args) + except ValueError: + rejected += 1 + for quotient, remainder in (((4, 0, -4, 0, 5, -4, 2), -4), + ((4, 0, -4, 0, 5, -4, 1), 4)): + try: + check_certificate(quotient, remainder) + except ValueError: + rejected += 1 + require(rejected == 7, "all seven malformed controls must be rejected") + return rejected + + +def finite_checks(): + count = 0 + for n in range(129): + for m in range(n + 1): + old, new = envelope(n, m, F(1), F(4)), envelope(n, m, F(1)) + difference = F(6, 7) * (n + m) + F(300, 49) * n * m + require(old - new == difference, "symbolic improvement coefficients") + require((old > new) == (n > 0), "constant-polynomial boundary") + count += 1 + log_checks = 0 + for numerator in range(1, 65): + for denominator in range(1, 65): + value = F(numerator, denominator) + e = ceil_log2(value) + require(F(2) ** (e - 1) < value <= F(2) ** e, + "exact binary ceiling bracket") + log_checks += 1 + return {"degree_pairs": count, "logarithm_brackets": log_checks, + "rejected_controls": rejection_controls()} + + +def read_bounded(path): + require(path.is_file() and not path.is_symlink(), "regular source file required") + require(path.stat().st_size <= LIMIT, "source exceeds two MiB") + return path.read_bytes() + + +def digest(path): + return hashlib.sha256(read_bounded(path)).hexdigest() + + +def source_receipt(): + manifest = json.loads(read_bounded(PACKAGE / "SOURCES.json")) + live = [row for row in manifest["files"] if row["usage"] == "input"] + require(len(live) == 1, "exactly one inherited proof input") + row = live[0] + require(row["path"] == "research/rational-circle-bound/PROOF.md", "proof path") + actual = digest(ROOT / row["path"]) + require(actual == row["sha256"], "inherited proof source hash") + names = ("PROOF.md", "README.md", "SOURCES.json", "TASK.json", "VERIFY.json", + "verify.py") + return {"input": {row["path"]: actual}, + "package": {name: digest(PACKAGE / name) for name in names}} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--emit", type=Path, help="create a new external receipt") + args = parser.parse_args() + certificate = check_certificate((4, 0, -4, 0, 5, -4, 1), -4) + require(F(22, 7) < 4, "rational constant improves four") + require(CONSTANT ** 2 / 16 == F(121, 196), "quadratic coefficient ratio") + receipt = {"status": "PASS_HARDY_INVERSE_CONSTANT", "claim_type": "scoped proof", + "constant_upper_bound": str(CONSTANT), "certificate": certificate, + "finite_checks": finite_checks(), "budgets": budget_rows(), + "sha256": source_receipt()} + rendered = json.dumps(receipt, sort_keys=True, indent=2) + "\n" + if args.emit is not None: + output = args.emit.resolve() + require(not output.is_relative_to(ROOT), "receipt must be outside checkout") + with output.open("x", encoding="utf-8") as handle: + written = handle.write(rendered) + require(written == len(rendered), "complete receipt write") + print(rendered, end="") + + +if __name__ == "__main__": + main()