diff --git a/research/eisenstein-stage-tail/.gitattributes b/research/eisenstein-stage-tail/.gitattributes new file mode 100644 index 0000000000..fa1385d99a --- /dev/null +++ b/research/eisenstein-stage-tail/.gitattributes @@ -0,0 +1 @@ +* -text diff --git a/research/eisenstein-stage-tail/README.md b/research/eisenstein-stage-tail/README.md new file mode 100644 index 0000000000..2a0d438daf --- /dev/null +++ b/research/eisenstein-stage-tail/README.md @@ -0,0 +1,226 @@ +# A uniform tail bound for the Eisenstein stage census + +This scoped written proof was produced by Nick Petalas. Apache-2.0. + +In the historical `B_K` forced-slot model of Rohan Guliani / Rohansguliani's +[PR #801](https://github.com/CrocSwap/integer-mult-bounds/pull/801), put +`h/k=4` and `x/k>=25/40`. For **every odd stage count `s>=15`**, the +positive saving ceiling satisfies + +```text +X(s,4,25/40) < 9/1000. +``` + +This closes the tail in the cost-25 case of #801's first Open next question. +Together with its cited, unreplayed `s=3,5,...,13` enclosures, it gives +`X(s,4,25/40)<1/99` for every allowed stage count. Increasing the copy cost +can only lower this ceiling. Thus more stages cannot rescue the historical +cost-at-least-25 route at that target. This is a necessary bound under a +declared accounting model. It supplies no decoder or multiplication theorem. + +The new result is the infinite tail inequality and its short rational +certificate. The earlier finite census, geometry, copy-cost floors and +slot-domination theorem are cited premises, not new verification work. + +## Exact model + +Normalize `k=1`, so `h=4`, the active climb is `a=3`, and the copy charge +per port is `x=5/8`. Write `s=2K+1`, `K>=7`, and `m=6K+4`. +The pressure at saving `q>=0` is + +```text +F_K(q) = sum_slots mass * ((m/cap)^q - 1), +D_K = (6K-5)/8. +``` + +The ceiling `X` is the unique positive solution `F_K(X)=D_K`. +All masses are positive and every cap is strictly between zero and `m`, +so the pressure is strictly increasing from zero to infinity. + +There are two active wires at every stage, each with a rank-three climb. +The copy slot has cap four. The idle stretches are those of the retained +`B_K` schedule. Pair zero is active at stages `0,1,2`. Pair `p>=1` is +active at `2p+1,2p+2`; its initial idle stretch is cut by the bridge read +after `2p` stages. Both bank copies are charged. Grouping these slots gives + +| Cap | Total mass | +|---|---:| +| `3` | `12K+6` | +| `4` | `(58K-43)/8` | +| `6p`, for each `1<=p=1` and `q>=0`, + +```text +z^q - 1 >= q log(z), +log(z) >= 2(z-1)/(z+1). +``` + +The first inequality is `exp(t)>=1+t`. For the second, subtract its +right side from `log(z)`. The difference vanishes at one and has derivative +`(z-1)^2 / (z(z+1)^2)>=0`. + +Apply these inequalities separately to every slot. Let `L_K` be the sum +of `mass * 2(m-cap)/(m+cap)`. Then `F_K(q)>=q L_K`. +For the idle slots, the positive weights are `24p`, their sum is +`12K(K-1)`, and their weighted mean cap is + +```text +sum(24p * 6p) / sum(24p) = 4K-2. +``` + +The function `f(t)=2(m-t)/(m+t)` has second derivative +`8m/(m+t)^3>0` for `t>0`. Jensen's inequality therefore bounds the idle +part of `L_K` from below by + +```text +24K(K-1)(K+3)/(5K+1). +``` + +Keep the active and cap-four terms exactly. This proves `L_K>=J_K`, where + +```text +J_K = 12(2K+1)(6K+1)/(6K+7) + + 3K(58K-43)/(4(3K+4)) + + 24K(K-1)(K+3)/(5K+1). +``` + +The following exact identity finishes the proof: + +```text +9 J_K - 1000 D_K = P(K) / [4(3K+4)(5K+1)(6K+7)], + +P(7+t) = 15552 t^5 + 469044 t^4 + 5264496 t^3 + + 26053149 t^2 + 48011339 t + 476748. +``` + +Every coefficient is positive, so `P(K)>0` for every real `K>=7`. +The denominator is positive too. Consequently + +```text +F_K(9/1000) >= (9/1000) L_K >= (9/1000) J_K > D_K. +``` + +Strict monotonicity of `F_K` gives `X<9/1000`, as claimed. +For `x>=5/8`, the copy mass increases and the deficit decreases, so the +same exclusion holds whenever the positive root exists. If the deficit +is nonpositive, there is no positive saving in this model. + +At `K=7`, `J_K=2519527/4900` and `D_K=37/8`. These exact values are a +control on the new tail proof. The displayed polynomial is negative at +`K=6`; this proof intentionally starts at fifteen stages. It does not +replace the cited lower-stage census. + +## Reproduction and evidence + +From the worktree root, CPython 3.12 and the standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/eisenstein-stage-tail/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -O -B research/eisenstein-stage-tail/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/eisenstein-stage-tail +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/eisenstein-stage-tail --check-source-history +``` + +Any CPython 3.12 installation can replace that local interpreter path. +The last command needs the publication commit and full source history. +Expected markers are `PASS_EISENSTEIN_STAGE_TAIL`, +`PASS_REGISTERED_RESEARCH_PACKAGE` and `PASS_RESEARCH_COMMIT_BYTES`. + +`verify.py` expands the rational identity by integer polynomial arithmetic, +then translates its coefficients by seven using the binomial theorem. +`oracle.py` imports no grouped profile or polynomial. It walks each bank's +literal stage activity and bridge boundary to reconstruct every idle +stretch. A second lower bound integrates `1/t` with four exact midpoint +pieces per slot. The two implementations agree on all grouped slots at +`1<=K<=128`; both pressure lower bounds exceed the deficit for all 122 +tail cases. The rational identity is checked at all 128 values as a +finite control, in addition to its exact symbolic coefficient check. + +The verifier rejects malformed/beyond-budget inputs and six separately +altered polynomial coefficients. It distinguishes omitted bridge mass, +an unpaid bank copy and a missing active wire, and checks the `K=6` +scope boundary. Checks use explicit exceptions and remain enabled under +optimized Python. Its stdout is a generated receipt bound to SHA256 +hashes of all seven package files. No receipt is handwritten or stored. +Both registered commands have a 120-second limit and write no files. + +## Scope, sources and credit + +Scientific base is canonical main +`19fdb086ea96af9a9f87936a2b888e10af4ed810`, priority revision 8. +The selected binding-only positive control passed. The selected conditional +`kappa=0.00310045` is context, not an input to this inequality. +[SOURCES.json](SOURCES.json) pins the source question, model specification, +earlier finite evidence, original task card and selected context as +historical provenance. No predecessor executable is imported or replayed. + +The `complex-rank-shape-decoder` card is changed to this narrow accounting +side result. Its physical-construction acceptance gate is not claimed. +The [advance CLAIM](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19221564) +predicted an exclusion below `1/99`; the proved tail bound is below +`9/1000`. Entry overlap covered 341 open PRs and 5,521 Discussion records +with complete remote pagination. Local notes were sparse, with 225 of +8,136 tracked note paths searched. Targeted main and merged-PR searches +were also read. This coverage does not establish absence of unpublished work. + +Credit Rohansguliani / Rohan Guliani #801 for the finite label-field census +and tail question; DreamingOfClouds for `format-limits-corrected`, the +`B_K` forced-slot framework and its retained #446/#386 lineage; Jonathan +Lam #798 for the Eisenstein decoder setting; GamingPuzzled / Joel Pulikkan +#620 for the extension-ring geometry; and the Gaussian, Hurwitz and +pairing-rank predecessors credited in #801. Maximooch #1794 supplies a +different all-stage screen for complex windows `h>=7` at a historical +selected target. It is not the `h=4`, `1/99` result proved here. +The logarithm, Jensen and exponential inequalities are classical. + +Field-to-rational and residue-field realization, changed coverage laws, +physical delivery, native operators, ownership, restoration, compilation, +precision/tape, stock and outer admission remain outside this result. +The historical `a/(1+a)` conversion is not applied to today's assembly. +No supplier or selected-frontier change follows. Independent human and +formal proof-kernel review are unclaimed. Lean, Docker and selected-operator +replay were not run. + +## Open next questions + +The remaining part of #801's tail question covers its other copy costs +and label windows. A useful first step is a complete signed-slot formula +for one of those rows, followed by its own tail certificate. This matters +for a valid all-stage ceiling rather than a finite-stage extrapolation. +No further census or construction expansion is justified by this package. +An actual extension-field supplier still needs its physical and native +interface before any such ceiling has an algorithmic consequence. + +## Implementation bounds + +The exact polynomial certificate, literal schedule and separate integral +lower bound are retained in the two new Python files. There is no recursion +or generated code; functions are below +60 lines. The APIs enforce `K<=128`, polynomial degree at most five and +at most sixteen integration pieces. Every loop is bounded by these limits. +State is local apart from immutable constants. File reads use a fixed +seven-file inventory and propagate failures. CPython allocation is a +managed-runtime deviation from fixed allocation within these finite bounds. +Python iterator dispatch is a language-level deviation from a literal ban +on indirect calls. Rejection callbacks have four fixed targets and execute +once per control; there are no extensible callback or plugin targets. +Warning-strict normal/optimized runs provide diagnostics without changing +repository-wide configuration. + +Local CPython 3.12.15 normal and optimized registered commands passed in +0.259 seconds each. Metadata/pins and the registered package replay pass. +Three disposable source mutations reject an altered certificate coefficient, +an underpriced idle term and a shifted bridge boundary. Both direct modes +also pass in a read-only Git-free package copy with an empty `PATH`. +An unexpected CLI argument rejects. Hosted CI is separate from these local +checks. No external Python linter was available locally. diff --git a/research/eisenstein-stage-tail/SOURCES.json b/research/eisenstein-stage-tail/SOURCES.json new file mode 100644 index 0000000000..937e8273f2 --- /dev/null +++ b/research/eisenstein-stage-tail/SOURCES.json @@ -0,0 +1,48 @@ +{ + "schema_version": 1, + "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "files": [ + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8", + "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + }, + { + "path": "research/label-field-census/README.md", + "usage": "provenance", + "git_blob": "d6cd3ea75bb7a6a5f537c9fe11479afbe80ab89a", + "sha256": "bc3da10c6880d5532750ef54e4d28f078ee95a648203c05c1dc8c62339a2df43" + }, + { + "path": "research/label-field-census/RESULT.json", + "usage": "provenance", + "git_blob": "458dcbd7fe02e46bce652bd61aad653af4e98c04", + "sha256": "015c5f8886ff2958a7f074dc37b371a24eece87332061da466656a4f52c1e946" + }, + { + "path": "research/label-field-census/census.py", + "usage": "provenance", + "git_blob": "ac9cc0cfefa32312272455f2b07442634800150e", + "sha256": "9d211cc0c1b83c8752cf6f14ee0d6957f75a0f9f66dd80ad5b939ae566f1b1ea" + }, + { + "path": "research/format-limits-corrected/README.md", + "usage": "provenance", + "git_blob": "95c7ae59f24eeebba4baae992e70d11ff5d68459", + "sha256": "1bcd80c1cd61fddae9f3a7f00fc9d1c796410408251e576600e94c19b16b1e5e" + }, + { + "path": "research/format-limits-corrected/scripts/skel.py", + "usage": "provenance", + "git_blob": "e3c6c815b604dd41d3807c78917806ae4a5c08a7", + "sha256": "9cfbc1316389a46922765cdae85fdde2042f7681986d1c97a19174c4922ea29c" + } + ] +} diff --git a/research/eisenstein-stage-tail/TASK.json b/research/eisenstein-stage-tail/TASK.json new file mode 100644 index 0000000000..fc43e3af9c --- /dev/null +++ b/research/eisenstein-stage-tail/TASK.json @@ -0,0 +1,98 @@ +{ + "schema_version": 1, + "task_id": "complex-rank-shape-decoder", + "priority_revision": 8, + "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "original_card": { + "id": "complex-rank-shape-decoder", + "question": "Can a legal decoder or coframe change improve the full signed moment, including changed helper targets?", + "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": "A source-bound arbitrary-input identity and legal producer/consumer boundary with the complete paid and productive target invoice, including restoration, ownership, native alignment and extra charges. Price under the actual current model; historical ceiling.py assumptions must be established before use. A favorable optimistic relaxation keeps a route open but is not a completed supplier. A scoped local result remains useful; expansion requires the family-level budget gate.", + "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": "Price one complete changed itinerary with both paid and productive histograms. Check #5693/#5698 for overlap and their exact hypotheses before another coframe search. Use the signed invoice preflight where its boundary contract agrees; an inconclusive concave comparison is not a power crossing. Stop if an optimistic complete budget fails at the chosen target or native delivery remains unspecified.", + "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": [ + "coframe", + "signed moment", + "5693", + "5698" + ], + "existing_checks": [ + { + "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.", + "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.", + "status": "reviewed", + "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137", + "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Prove X(s,4,25/40)<9/1000 for every odd stage count s>=15 under the historical B_K slot accounting.", + "scope_change_reason": "PR801 explicitly leaves its stage-count tail open. This is an original infinite-tail bound, not a decoder construction or an audit of its finite census.", + "bottleneck_link": "A narrow historical extension-field accounting side result. More stages cannot evade the cost25 ceiling at 1/99 in this model; it does not improve the selected complex supplier.", + "budget_minutes": 60, + "stop_rule": "Stop at the first verified original uniform tail inequality and package it; do not extend to other costs.", + "outcome": "negative-result", + "evidence": "Written log/Jensen argument; exact positive-coefficient degree-five identity; literal schedule and independent rational midpoint lower-bound corroboration for K<=128; generated stdout receipts bound to package hashes.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "claim_type": "scoped written proof with exact finite corroboration", + "open_questions": [ + { + "question": "Can the other cost/window rows in PR801 receive all-stage ceilings?", + "why_it_matters": "Their finite-stage maxima do not exclude a larger-stage recovery.", + "first_step": "Derive the complete signed-slot formula for one other row and a uniform tail certificate.", + "blocked_by": "A separate parameter-specific inequality and the inherited physical/native realization obligations." + } + ], + "source_question": { + "pr": 801, + "author": "Rohansguliani", + "item": "Open next question 1 of research/label-field-census/README.md" + }, + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19221564", + "environment": { + "python": "CPython 3.12.15", + "platform": "macOS arm64", + "local_interpreter": "/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12" + }, + "unrun_obligations": [ + "Independent human and formal proof-kernel review", + "Field/rational realization", + "Physical supplier and complete caller", + "Selected operator replay, Lean and Docker" + ], + "upstream_checkpoint": { + "commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "priority_revision": 8, + "checked_at": "2026-10-27T16:04:59Z" + } +} diff --git a/research/eisenstein-stage-tail/VERIFY.json b/research/eisenstein-stage-tail/VERIFY.json new file mode 100644 index 0000000000..c4f7f30cf1 --- /dev/null +++ b/research/eisenstein-stage-tail/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": 120, + "checks": "Exact symbolic rational identity and coefficient positivity, 128 independent literal schedules, 122 tail lower bounds, scope and corruption controls; generated hash-bound stdout receipt." + }, + { + "argv": [ + "{python}", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact symbolic rational identity and coefficient positivity, 128 independent literal schedules, 122 tail lower bounds, scope and corruption controls; generated hash-bound stdout receipt." + } + ] +} diff --git a/research/eisenstein-stage-tail/oracle.py b/research/eisenstein-stage-tail/oracle.py new file mode 100644 index 0000000000..5c66f3e753 --- /dev/null +++ b/research/eisenstein-stage-tail/oracle.py @@ -0,0 +1,72 @@ +"""Literal B_K stage schedule and exact integral lower sums. + +Produced by Nick Petalas. Apache-2.0. +This module does not import the grouped profile or its polynomial proof. +""" + +from collections import Counter +from fractions import Fraction + +MAX_K = 128 + + +def checked_k(k): + if type(k) is not int or not 1 <= k <= MAX_K: + raise ValueError("K must be an integer in 1..128") + return k + + +def schedule(k): + """Each inactive run is cut at the named pre-bridge read boundary.""" + checked_k(k) + stages = 2 * k + 1 + slots = Counter() + for _stage in range(stages): + slots[3] += 6 # Two active bank wires each climb three. + slots[4] += Fraction(5, 8) + for pair in range(k): + active = {0, 1, 2} if pair == 0 else {2 * pair + 1, 2 * pair + 2} + run = 0 + for boundary in range(stages + 1): + split = pair > 0 and boundary == 2 * pair + stop = boundary == stages or boundary in active + if (split or stop) and run: + rank = 3 * run + slots[max(4, rank)] += 2 * rank + run = 0 + if boundary < stages and boundary not in active: + run += 1 + return dict(slots) + + +def midpoint_log_lower(ratio, pieces=4): + """Convexity of 1/t gives an exact lower Riemann sum for log.""" + ratio = Fraction(ratio) + if ratio < 1 or type(pieces) is not int or not 1 <= pieces <= 16: + raise ValueError("require ratio>=1 and 1..16 midpoint pieces") + width = (ratio - 1) / pieces + return sum(width / (1 + (Fraction(j) + Fraction(1, 2)) * width) + for j in range(pieces)) + + +def schedule_cost_lower(k): + checked_k(k) + width = 6 * k + 4 + return sum(mass * midpoint_log_lower(Fraction(width, cap)) + for cap, mass in schedule(k).items()) + + +def weighted_reciprocal_gap(k): + """Cauchy's inequality on the literal repeated idle lengths.""" + checked_k(k) + if k == 1: + return Fraction(0) + width = 6 * k + 4 + weights = [24 * p for p in range(1, k)] + lengths = [6 * p for p in range(1, k)] + total = sum(weights) + mean = Fraction(sum(w * r for w, r in zip(weights, lengths)), total) + literal = sum(Fraction(2 * w * (width - r), width + r) + for w, r in zip(weights, lengths)) + bound = 2 * total * (width - mean) / (width + mean) + return literal - bound diff --git a/research/eisenstein-stage-tail/verify.py b/research/eisenstein-stage-tail/verify.py new file mode 100644 index 0000000000..3958aa99e9 --- /dev/null +++ b/research/eisenstein-stage-tail/verify.py @@ -0,0 +1,178 @@ +#!/usr/bin/env python3 +"""Exact finite corroboration of the written infinite-stage tail proof. + +Produced by Nick Petalas. Apache-2.0. +""" + +from fractions import Fraction as Q +from hashlib import sha256 +import json +from math import comb +from pathlib import Path +import sys + +import oracle + +MAX_K = 128 +PACKAGE_FILES = (".gitattributes", "README.md", "SOURCES.json", "TASK.json", + "VERIFY.json", "oracle.py", "verify.py") +EXPECTED_NUMERATOR = (71728, 321557, 54309, -248256, -75276, 15552) +EXPECTED_SHIFT = (476748, 48011339, 26053149, 5264496, 469044, 15552) + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def validate_k(k): + if type(k) is not int or not 1 <= k <= MAX_K: + raise ValueError("K must be an integer in 1..128") + + +def grouped_slots(k): + validate_k(k) + slots = {3: Q(12 * k + 6), 4: Q(58 * k - 43, 8)} + for p in range(1, k): + slots[6 * p] = Q(24 * p) + return slots + + +def rational_cost(k): + validate_k(k) + width = 6 * k + 4 + return sum(2 * mass * Q(width - cap, width + cap) + for cap, mass in grouped_slots(k).items()) + + +def jensen_cost(k): + validate_k(k) + active = Q(12 * (2 * k + 1) * (6 * k + 1), 6 * k + 7) + bridge_copy = Q(3 * k * (58 * k - 43), 4 * (3 * k + 4)) + idle = Q(24 * k * (k - 1) * (k + 3), 5 * k + 1) + return active + bridge_copy + idle + + +def multiply(*factors): + require(len(factors) <= 5, "polynomial factor limit") + result = [1] + for factor in factors: + require(1 <= len(factor) <= 6, "polynomial degree limit") + require(len(result) + len(factor) <= 7, "product degree limit") + out = [0] * (len(result) + len(factor) - 1) + for i, left in enumerate(result): + for j, right in enumerate(factor): + out[i + j] += left * right + result = out + return result + + +def numerator(): + # Denominator is 4(3K+4)(5K+1)(6K+7). + active = multiply([432], [1, 2], [1, 6], [4, 3], [1, 5]) + bridge = multiply([27], [0, 1], [-43, 58], [1, 5], [7, 6]) + idle = multiply([864], [0, -1, 1], [3, 1], [4, 3], [7, 6]) + deficit = multiply([-500], [-5, 6], [4, 3], [1, 5], [7, 6]) + return tuple(sum(part[i] if i < len(part) else 0 + for part in (active, bridge, idle, deficit)) for i in range(6)) + + +def shifted(coefficients): + require(len(coefficients) == 6, "degree-five certificate required") + return tuple(sum(coefficients[j] * comb(j, i) * 7 ** (j - i) + for j in range(i, 6)) for i in range(6)) + + +def evaluate(coefficients, value): + require(len(coefficients) <= 6, "degree limit") + result = 0 + for coefficient in reversed(coefficients): + result = result * value + coefficient + return result + + +def proof_certificate(coefficients): + require(tuple(coefficients) == numerator(), "wrong cleared numerator") + shift = shifted(coefficients) + require(all(coefficient > 0 for coefficient in shift), "tail positivity failed") + return shift + + +def finite_checks(): + for k in range(1, MAX_K + 1): + require(grouped_slots(k) == oracle.schedule(k), "literal schedule differs") + width = 6 * k + 4 + require(all(0 < cap < width and mass > 0 + for cap, mass in grouped_slots(k).items()), "illegal slot") + require(rational_cost(k) >= jensen_cost(k), "Jensen bound failed") + require(oracle.weighted_reciprocal_gap(k) >= 0, "reciprocal bound failed") + denominator = 4 * (3 * k + 4) * (5 * k + 1) * (6 * k + 7) + deficit = Q(6 * k - 5, 8) + require(9 * jensen_cost(k) - 1000 * deficit + == Q(evaluate(numerator(), k), denominator), "rational identity failed") + if k >= 7: + require(Q(9, 1000) * jensen_cost(k) > deficit, "tail bound failed") + require(Q(9, 1000) * oracle.schedule_cost_lower(k) > deficit, + "independent integral lower bound failed") + return {"literal_schedule_cases": MAX_K, "tail_cases": MAX_K - 6, + "polynomial_identity_cases": MAX_K} + + +def reject(operation): + try: + operation() + except ValueError: + return + raise ValueError("rejection control was accepted") + + +def controls(): + count = 0 + for k in (0, -1, True, Q(7), MAX_K + 1): + reject(lambda: grouped_slots(k)) + reject(lambda: oracle.schedule(k)) + count += 2 + for index in range(6): + bad = list(EXPECTED_NUMERATOR) + bad[index] += 1 + reject(lambda: proof_certificate(bad)) + count += 1 + reject(lambda: oracle.midpoint_log_lower(Q(1, 2))) + reject(lambda: oracle.midpoint_log_lower(2, 0)) + count += 2 + k = 7 + literal = oracle.schedule(k) + missing_bridge = dict(literal) + missing_bridge[4] -= 6 * (k - 1) + missing_bank = dict(literal) + missing_bank[6] -= 12 + wrong_active = dict(literal) + wrong_active[3] -= 3 * (2 * k + 1) + for mutant in (missing_bridge, missing_bank, wrong_active): + require(mutant != grouped_slots(k), "schedule mutant survived") + count += 1 + require(evaluate(EXPECTED_NUMERATOR, 6) < 0, + "K=6 must not be certified by this polynomial") + return count + 1 + + +def main(): + require(len(sys.argv) == 1, "this verifier accepts no arguments") + coefficients = numerator() + require(coefficients == EXPECTED_NUMERATOR, "numerator coefficients differ") + require(proof_certificate(coefficients) == EXPECTED_SHIFT, "shift coefficients differ") + result = finite_checks() + result["rejection_and_scope_controls"] = controls() + result["cleared_numerator_ascending"] = coefficients + result["shift_at_seven_ascending"] = EXPECTED_SHIFT + result["tail_bound"] = "9/1000" + result["K7_lower_cost"] = str(jensen_cost(7)) + root = Path(__file__).resolve().parent + result["sha256"] = {name: sha256((root / name).read_bytes()).hexdigest() + for name in PACKAGE_FILES} + print(json.dumps(result, sort_keys=True)) + print("PASS_EISENSTEIN_STAGE_TAIL s>=15 X<9/1000 no_new_kappa") + + +if __name__ == "__main__": + main()