diff --git a/research/unit-fee-target-threshold/PROOF.md b/research/unit-fee-target-threshold/PROOF.md new file mode 100644 index 0000000000..c0472e6830 --- /dev/null +++ b/research/unit-fee-target-threshold/PROOF.md @@ -0,0 +1,116 @@ +# The sharp unit-fee target-rank threshold + +This scoped proof is produced by Nick Petalas. New material is Apache-2.0. +The fee-charged partition contract comes from Ali Romman's PR #5769. Strict +concavity, Jensen's inequality and balancing are classical ingredients. + +## Contract and theorem + +Fix `p=99/100`. Replace one productive target of integer rank `R` by `k>=2` +independent productive targets with positive integer ranks `r_1,...,r_k`, whose +sum is `R`. Charge **one additional paid rank-one recursive child per piece**. +Keep every other paid child, productive target and fee fixed. Under the raw +power tariff, the improvement in paid cost minus productive credit is + +```text +G(R;r_1,...,r_k) = sum_i r_i^p - R^p - k. +``` + +A positive `G` means a strictly cheaper complete invoice. The `R^p` debit is +essential. The charge is `k`, including every resulting piece. This theorem +uses neither `k-1` fees nor a free distinguished piece. A scalar addition is +not assumed to cost a recursive rank-one child. + +**Theorem.** Such a strictly improving partition exists if and only if +`R>=288`. At the first rank, `(96,96,96)` has improvement strictly between +`6289/1000000` and `6290/1000000`. Every proper partition with `R<=287` loses. +In fact its improvement is less than `-4077/1000000`. + +This is an arithmetic screening result for the declared fee. It does not assert +that arbitrary target partitions are physically realizable or useful. + +## Rejecting every smaller rank + +For any fixed `R,k`, Jensen's inequality gives + +```text +sum_i r_i^p <= k(R/k)^p = R^p k^(1/100), +G <= J(R,k) = R^p (k^(1/100)-1) - k. +``` + +For every `k>=2`, `J(R,k)` strictly increases with positive real `R`. +Consequently, for `R<=287` and `2<=k<=R`, it suffices to bound `J(287,k)` for +the complete finite list `k=2,...,287`. No integer partitions are omitted by +this reduction; it even grants arbitrary positive real piece sizes at each k. + +The standalone checker supplies an exact dyadic certificate for each of those +286 inequalities. Let `D=2^128`. To bound a positive `n^(a/100)`, compute + +```text +L = floor_root_100(n^a D^100), +U = L if L^100=n^a D^100, else L+1. +``` + +The checker verifies `L^100 <= n^a D^100 < (L+1)^100` using integers. +Thus `L/D <= n^(a/100) <= U/D`. Use `a=99` for `287^p` and `a=1` for each +`k^(1/100)`. With their respective upper numerators `U_287,U_k`, + +```text +D^2 J(287,k) <= U_287 (U_k-D) - k D^2 < 0. +``` + +Every right-hand numerator is present in the generated receipt. The largest +Jensen upper bound occurs at `k=3` and is strictly negative. Monotonicity proves +the stated rejection for every smaller integer rank and every proper partition. + +The stronger integer margin uses balancing, proved below. The checker also +encloses the balanced integer partition's profit at rank 287 for every one of +the same 286 piece counts. The largest upper bound occurs at `k=3`, with parts +`(95,96,96)`, and is below `-4077/1000000`. Balanced profit strictly increases +with R at fixed k, as shown below, so this integer margin applies to every +proper partition at every smaller rank too. Jensen's real-size relaxation is +used only for the sign, not for this stronger integer margin. + +## Attainment and all larger ranks + +At `R=288`, take three rank-96 pieces. The exact root enclosures above, with +`a=99`, give + +```text +6289/1000000 < 3*96^p - 288^p - 3 < 6290/1000000. +``` + +All comparisons are integer cross-multiplications. This proves attainment at +288 independently of any floating-point approximation or source executable. + +For completeness, the witness extends to every larger rank. For fixed k, +strict concavity implies that a maximizing integer partition has parts differing +by at most one. Indeed, if `b>=a+2`, replace `(a,b)` by `(a+1,b-1)`. +The decreasing increments of `x^p` make the credit strictly larger. + +Write `B_k(R)` for the balanced partition's improvement. When `R` increases by +one, increase a smallest piece `q=floor(R/k)` by one. Then + +```text +B_k(R+1)-B_k(R) = ((q+1)^p-q^p) - ((R+1)^p-R^p) > 0, +``` + +since `q=288`. The positive rank-288 witness and this strict +monotonicity establish existence at every larger rank. No additional search or +new supplier premise is used. + +## What the executable proves + +The written argument reduces the infinite claim to 286 root-enclosed Jensen +inequalities and one positive witness. `verify.py` checks those inequalities +and rational margins with integer arithmetic. It also checks the balancing +lemma on every proper sorted integer partition of ranks 2 through 24, uses an +independently implemented bisection oracle for eleven decisive powers, and +rejects forged certificates and invalid partitions. These finite checks +corroborate the written proof; they are not proof-kernel verification. + +The receipt is generated on stdout and binds every package file by SHA256. +No receipt is hand-written or stored as an assumed mathematical input. Normal +and optimized modes must emit identical receipts. A supplied `--check-receipt` +file is checked against a fresh computation and fresh source hashes. diff --git a/research/unit-fee-target-threshold/README.md b/research/unit-fee-target-threshold/README.md new file mode 100644 index 0000000000..8f169dc0e5 --- /dev/null +++ b/research/unit-fee-target-threshold/README.md @@ -0,0 +1,92 @@ +# First profitable target rank with one paid unit per piece + +This contribution is produced by Nick Petalas. Claim type: **scoped proof with +exact finite corroboration**. It does not improve kappa or change the selected +frontier. New material is Apache-2.0. + +At power exponent `99/100`, replacing one rank-R productive target by a proper +positive integer partition, while adding one paid rank-one recursive child for +each resulting target, can improve the complete signed bill **exactly when +R>=288**. The first witness is `288=96+96+96`. + +```text +profit = sum_i r_i^(99/100) - R^(99/100) - number_of_pieces +R <= 287: every proper partition has profit < -0.004077 +R = 288: (96,96,96) has 0.006289 < profit < 0.006290 +``` + +[PROOF.md](PROOF.md) reduces the all-partition lower bound to 286 explicit +Jensen inequalities at rank 287. Integer-root enclosures certify each one and +the positive witness. Balancing and strictly decreasing power increments extend +the witness to all larger ranks. The proof has no piece-count or menu limit. + +This specializes Ali Romman's [PR #5769](https://github.com/CrocSwap/integer-mult-bounds/pull/5769) +complete fee-charged target-partition contract. That finite optimizer caps the +replaced rank at 256. The present unit-fee model has no profitable rank inside +that cap at this exponent; the first opportunity is 288. This is a new arithmetic +screen, rather than a replay or audit of the optimizer. The result tells a +contributor using this fee model to seek lower or shared fees before searching +small target partitions. It grants independent targets and adds no other fees, +so extra nonnegative costs can only strengthen the rejection below 288. + +## Reproduce + +From the repository root, using CPython 3.12 and the standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/unit-fee-target-threshold +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/unit-fee-target-threshold/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -O -B research/unit-fee-target-threshold/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/unit-fee-target-threshold --check-source-history +``` + +Another CPython 3.12 interpreter can replace the absolute path. Expected marker +in the JSON stdout receipt: `PASS_UNIT_FEE_TARGET_THRESHOLD`. The receipt +contains all 286 dyadic rejection bounds, the witness bounds, finite coverage +counts and SHA256 of every package file. Redirect stdout outside the checkout +if retaining it. `verify.py --check-receipt PATH` recomputes the result and checks +both the supplied receipt and the current source hashes. Replay writes no files. + +## Scope and limitations + +The exponent is fixed at 99/100, a one-percent raw power-saving screen. It is +not the selected supplier exponent or the nine-row outer budget. One recursive +rank-one child per resulting piece is an explicit additional-fee hypothesis; +ordinary scalar ADD charges and shared fees are different models. The result +does not exclude no-fee target refinements, including selected #5599, or any +construction with paid removals, other productive credits or changed boundaries. + +Independent useful targets, native/source maps, chronological delivery, dirty +restoration, owned lifetimes, complete compiler/precision/tape/outer admission +and the full multiplication theorem are unproved here. No predecessor verifier, +selected cold replay, Lean proof or physical supplier was run. Independent human +and formal proof-kernel review are unclaimed. The five selected framework +assumptions remain. + +## Open next questions + +- At the actual source-bound supplier exponent, what is the first profitable + rank under the same fee? Start with balanced partitions and certify the two + adjacent rank signs. This would tailor the screen to a real caller; the + correct tariff and exponent must first be pinned. +- Can a real helper split share one paid route across its targets, rather than + paying one child per piece? Start with one literal helper/cut and derive its + complete invoice. Independent target realization and dirty restoration are + the blockers; this arithmetic theorem supplies neither. + +## Credit and provenance + +Credit Ali Romman #5769, head `a869fed1b3ab00ffcddd3791c579c408594325f8`, +for the fee-charged partition definition, original-target debit and finite +optimizer. Credit classical concavity, Jensen and integer balancing, and the +signed-invoice framework, mightyOil's T16 audit and their retained predecessors. +[SOURCES.json](SOURCES.json) records exact reference-document bytes and the +base catalogue/selected-record pins. The source document is reference-only; +this self-contained theorem has no unmerged runtime or Git-object dependency. + +Related work includes Charan . #5702's thirteen fixed H9 helpers funding one +shared extra child, Arham Tahir #1605 and Aaron Wang #3110's paid-child reblocking +contracts, and Ali Romman #5341's paid-increment fragmentation. Those models and +quantities differ; their reported numbers are not replayed as this deliverable. +The account's #5901 concerns incomparable invoice pools, rather than existence +of an improving unit-fee partition. It supplies no premise used here. diff --git a/research/unit-fee-target-threshold/SOURCES.json b/research/unit-fee-target-threshold/SOURCES.json new file mode 100644 index 0000000000..834552f070 --- /dev/null +++ b/research/unit-fee-target-threshold/SOURCES.json @@ -0,0 +1,29 @@ +{ + "schema_version": 1, + "base_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a", + "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" + } + ], + "reference_only": [ + { + "pr": 5769, + "head": "a869fed1b3ab00ffcddd3791c579c408594325f8", + "path": "docs/research/target-partition-optimization.md", + "sha256": "3a8dc58083cb4d9d8b0f92764c93f2a8dfcd42b703565d944be63a48df8446a9", + "git_blob": "a1d612450907ec34bf99747929da04276aac2e80", + "url": "https://github.com/aliromman/integer-mult-bounds/blob/a869fed1b3ab00ffcddd3791c579c408594325f8/docs/research/target-partition-optimization.md", + "usage": "Definition/motivation citation only. No runtime or Git-object dependency." + } + ] +} diff --git a/research/unit-fee-target-threshold/TASK.json b/research/unit-fee-target-threshold/TASK.json new file mode 100644 index 0000000000..7fddf24dc7 --- /dev/null +++ b/research/unit-fee-target-threshold/TASK.json @@ -0,0 +1,123 @@ +{ + "schema_version": 1, + "task_id": "complex-rank-shape-decoder", + "priority_revision": 8, + "base_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a", + "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": "Sharp first profitable integer target rank at exponent 99/100 with one additional paid rank-one child per resulting piece, over every positive integer partition.", + "scope_change_reason": "Specialize the complete fee-charged target-partition contract of Ali Romman PR5769 to a uniform explicit fee. This arithmetic screen precedes, and does not supply, a physical decoder or supplier.", + "bottleneck_link": "A complete target refinement must beat all added recursive charges. This theorem identifies the first rank that can do so under the declared one-unit-per-piece fee; the exponent is a target one-percent raw screen, not selected supplier admission.", + "budget_minutes": 60, + "stop_rule": "Stop at the first exact threshold with a complete all-partition rejection below it and a positive witness at it. No wider exponent or mechanism search.", + "outcome": "completed", + "evidence": "PROOF.md all-rank proof; 286 exact Jensen and integer-balanced rejection bounds; positive rank-288 witness; 7313 complete small proper integer partitions; eleven independent bisection checks; eight forged certificates and five invalid partitions rejected. Warning-strict normal and optimized receipts agree.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "What is the first profitable rank at a pinned actual supplier exponent under the same fee?", + "why_it_matters": "This would specialize the arithmetic screen to a real complete caller bill.", + "first_step": "Use balanced fixed-count partitions and certify the two adjacent rank signs.", + "blocked_by": "The correct source tariff and supplier exponent must be pinned first." + }, + { + "question": "Can a literal helper split share paid routes across its independent targets?", + "why_it_matters": "Shared or lower fees change this scoped threshold.", + "first_step": "Choose one source helper and causal cut; derive all target credits and paid routes.", + "blocked_by": "Independent useful target delivery and dirty restoration are not realized here." + } + ], + "predecessor": { + "pr": 5769, + "head": "a869fed1b3ab00ffcddd3791c579c408594325f8", + "author": "Ali Romman", + "usage": "Reference-only fee-charged partition definition; no source executable or result is replayed." + }, + "scope_key": "target-partition/unit-per-piece-fee/exponent-99-100/all-positive-integer-ranks", + "coordination": { + "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19216793" + }, + "engineering": { + "playbook": "autonomous local run", + "principles": [ + "Build the Lever: standalone verifier emits a source-bound receipt.", + "Prove It Works: integer endpoint powers check every bound; normal and optimized replay.", + "Power of Ten: no recursion; fixed domains, bounded root iterations and enumeration; functions below 60 lines." + ], + "deviations": [ + "Python integer/JSON allocation is runtime-managed. Ranks are at most 288; root radicands are below 15000 bits, table size is 288 and small-partition depth is at most 24. No fixed-allocation runtime claim.", + "No Python static analyzer is configured for this package. Warning-strict normal and optimized execution plus AST and function-size inspection are used." + ] + }, + "environment": { + "python": "3.12.15", + "platform": "macOS-27.0.1-arm64-arm-64bit", + "dependencies": "standard library only" + }, + "overlap": { + "open_prs": { + "fetched_at": "2026-10-27T12:31:48.049401+00:00", + "complete_pagination": true, + "records": 459 + }, + "discussions": { + "fetched_at": "2026-10-27T12:32:49.937283+00:00", + "complete_pagination": true, + "records": 5400 + }, + "limits": "Sparse helper searched 184 local notes of 7845 HEAD note paths. Distinctive searches across all origin/main research README blobs and live merged PR searches supplemented that incomplete local corpus. No keyword search proves novelty. PR5769 reference and related PR5702/5341/3110/1605/1888 bodies read.", + "canonical_main": "de5ec2e7a6074068452f45b1a191b5c72832df4a", + "refreshed_before_publication": true + } +} diff --git a/research/unit-fee-target-threshold/VERIFY.json b/research/unit-fee-target-threshold/VERIFY.json new file mode 100644 index 0000000000..e97f69208a --- /dev/null +++ b/research/unit-fee-target-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": 180, + "checks": "286 exact Jensen rejections, positive witness and rational margins; every proper partition through rank 24, eleven bisection oracles, eight forged certificates and five invalid partitions; source-bound stdout receipt." + }, + { + "argv": [ + "{python}", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 180, + "checks": "The same complete bounded checks with Python assertions disabled." + } + ] +} diff --git a/research/unit-fee-target-threshold/verify.py b/research/unit-fee-target-threshold/verify.py new file mode 100644 index 0000000000..e8a53ea81d --- /dev/null +++ b/research/unit-fee-target-threshold/verify.py @@ -0,0 +1,218 @@ +#!/usr/bin/env python3 +"""Exact unit-fee target-partition threshold. Produced by Nick Petalas.""" +import argparse +import hashlib +import json +from pathlib import Path + +BITS = 128 +SCALE = 1 << BITS +ROOT = Path(__file__).resolve().parent + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def integer_root(value, degree): + """Return floor(value**(1/degree)), with integer endpoint certificates.""" + require(type(value) is int and 0 <= value < 1 << 15000, "radicand limit") + require(type(degree) is int and 1 <= degree <= 100, "degree limit") + if value == 0: + return 0 + estimate = 1 << ((value.bit_length() + degree - 1) // degree) + for _ in range(512): + next_estimate = ((degree - 1) * estimate + + value // estimate ** (degree - 1)) // degree + if next_estimate >= estimate: + require(estimate ** degree <= value < (estimate + 1) ** degree, + "root endpoint certificate") + return estimate + estimate = next_estimate + raise ValueError("root iteration limit") + + +def power_bounds(rank, numerator): + require(type(rank) is int and 1 <= rank <= 288, "rank limit") + require(numerator in (1, 99), "exponent limit") + radicand = rank ** numerator << (100 * BITS) + lower = integer_root(radicand, 100) + upper = lower if lower ** 100 == radicand else lower + 1 + return lower, upper + + +def balanced_parts(rank, count): + require(type(rank) is int and type(count) is int + and 2 <= count <= rank <= 288, "partition domain") + quotient, remainder = divmod(rank, count) + result = (quotient,) * (count - remainder) + (quotient + 1,) * remainder + require(sum(result) == rank and len(result) == count, "balanced mass") + return result + + +def profit_bounds(parts, table): + require(isinstance(parts, tuple) and 2 <= len(parts) <= 288, + "proper partition required") + require(all(type(r) is int and r >= 1 for r in parts), "positive ranks") + rank = sum(parts) + require(rank <= 288, "partition rank limit") + debit_lower, debit_upper = table[rank] + fee = len(parts) * SCALE + lower = sum(table[r][0] for r in parts) - debit_upper - fee + upper = sum(table[r][1] for r in parts) - debit_lower - fee + return lower, upper + + +def threshold_certificate(table): + """Jensen rejects all smaller ranks; a balanced partition attains 288.""" + debit_lower, debit_upper = table[287] + rows = [] + for count in range(2, 288): + root_lower, root_upper = power_bounds(count, 1) + lower = debit_lower * (root_lower - SCALE) - count * SCALE ** 2 + upper = debit_upper * (root_upper - SCALE) - count * SCALE ** 2 + require(upper < 0, "Jensen rejection failed") + balanced_lower, balanced_upper = profit_bounds(balanced_parts(287, count), table) + rows.append({"pieces": count, "lower": lower, "upper": upper, + "balanced_lower": balanced_lower, "balanced_upper": balanced_upper}) + best = max(rows, key=lambda row: row["upper"]) + require(best["pieces"] == 3, "critical rejected count") + integer_best = max(rows, key=lambda row: row["balanced_upper"]) + require(integer_best["pieces"] == 3, "critical integer count") + require(integer_best["balanced_upper"] * 1000000 < -4077 * SCALE, + "uniform integer negative margin") + parts = balanced_parts(288, 3) + lower, upper = profit_bounds(parts, table) + require(lower * 1000000 > 6289 * SCALE, "positive witness lower margin") + require(upper * 1000000 < 6290 * SCALE, "positive witness upper margin") + return {"exponent": "99/100", "fee_per_piece": 1, + "first_profitable_rank": 288, "rejected_rank": 287, + "jensen_denominator": SCALE ** 2, "jensen_rows": rows, + "critical_rejected_pieces": 3, "witness": list(parts), + "profit_denominator": SCALE, "profit_lower": lower, + "profit_upper": upper} + + +def binary_root_oracle(value, degree): + """Independent bisection, used only on the decisive endpoint powers.""" + low, high = 0, 1 << ((value.bit_length() + degree - 1) // degree) + for _ in range(high.bit_length() + 1): + if high - low <= 1: + require(low ** degree <= value < high ** degree, "oracle endpoints") + return low + middle = (low + high) // 2 + if middle ** degree <= value: + low = middle + else: + high = middle + raise ValueError("oracle iteration limit") + + +def check_power_oracle(table): + cases = [(rank, 99) for rank in (1, 2, 3, 4, 96, 287, 288)] + cases += [(rank, 1) for rank in (2, 3, 4, 287)] + for rank, numerator in cases: + radicand = rank ** numerator << (100 * BITS) + actual = table[rank][0] if numerator == 99 else power_bounds(rank, 1)[0] + require(actual == binary_root_oracle(radicand, 100), "oracle mismatch") + return len(cases) + + +def check_all_small_partitions(table): + """Enumerate each sorted partition once; test the fixed-count maximizer.""" + checked = 0 + for rank in range(2, 25): + stack = [(rank, 1, ())] + for _ in range(100000): + if not stack: + break + remaining, minimum, prefix = stack.pop() + if remaining == 0: + if len(prefix) < 2: + continue + lower, upper = profit_bounds(prefix, table) + require(upper < 0, "small partition passed") + balanced = balanced_parts(rank, len(prefix)) + if prefix != balanced: + balanced_lower, _ = profit_bounds(balanced, table) + require(upper < balanced_lower, "strict balancing failed") + require(lower <= upper, "reversed profit interval") + checked += 1 + continue + for part in range(minimum, remaining + 1): + stack.append((remaining - part, part, prefix + (part,))) + else: + raise ValueError("partition enumeration limit") + return checked + + +def verify_certificate(certificate, table): + require(type(certificate) is dict, "certificate object") + expected = threshold_certificate(table) + require(json.dumps(certificate, sort_keys=True) == json.dumps(expected, sort_keys=True), + "threshold certificate mismatch") + + +def check_controls(certificate, table): + controls = [] + for key, wrong in (("first_profitable_rank", 287), ("fee_per_piece", 0), + ("exponent", "1/2"), ("witness", [95, 96, 96]), + ("profit_lower", -1), ("critical_rejected_pieces", 2), + ("fee_per_piece", True)): + altered = dict(certificate) + altered[key] = wrong + controls.append(altered) + altered = json.loads(json.dumps(certificate)) + altered["jensen_rows"][0]["upper"] = 1 + controls.append(altered) + for altered in controls: + try: + verify_certificate(altered, table) + except ValueError: + continue + raise ValueError("forged certificate accepted") + return len(controls) + + +def check_domain_controls(table): + bad_parts = ((288,), (0, 288), (-1, 2), (True, 2), (144, 145)) + for parts in bad_parts: + try: + profit_bounds(parts, table) + except ValueError: + continue + raise ValueError("invalid partition accepted") + return len(bad_parts) + + +def source_hashes(): + names = ("README.md", "PROOF.md", "TASK.json", "SOURCES.json", "VERIFY.json", + "verify.py") + return {name: hashlib.sha256((ROOT / name).read_bytes()).hexdigest() + for name in names} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--check-receipt", type=Path) + args = parser.parse_args() + table = {rank: power_bounds(rank, 99) for rank in range(1, 289)} + certificate = threshold_certificate(table) + report = {"marker": "PASS_UNIT_FEE_TARGET_THRESHOLD", "certificate": certificate, + "small_partitions": check_all_small_partitions(table), + "independent_power_checks": check_power_oracle(table), + "forged_certificates_rejected": check_controls(certificate, table), + "invalid_partitions_rejected": check_domain_controls(table), + "source_sha256": source_hashes()} + if args.check_receipt: + require(args.check_receipt.stat().st_size <= 1000000, "receipt size limit") + supplied = json.loads(args.check_receipt.read_text(encoding="utf-8")) + require(type(supplied) is dict + and json.dumps(supplied, sort_keys=True) == json.dumps(report, sort_keys=True), + "receipt or source mismatch") + print(json.dumps(report, sort_keys=True, indent=2)) + + +if __name__ == "__main__": + main()