diff --git a/research/query-tree-topology-optimum/CERTIFICATE.json b/research/query-tree-topology-optimum/CERTIFICATE.json new file mode 100644 index 0000000000..2e613395a8 --- /dev/null +++ b/research/query-tree-topology-optimum/CERTIFICATE.json @@ -0,0 +1,337 @@ +{ + "schema": "query-tree-hinge-upper/1", + "leaves": 19, + "roots": 3, + "hinges": [ + { + "threshold": 3, + "upper": [ + 0, + 1, + 1, + 2, + 2, + 3, + 3, + 4, + 4, + 5, + 5, + 6, + 6, + 7, + 7, + 8, + 8 + ] + }, + { + "threshold": 4, + "upper": [ + 0, + 2, + 3, + 4, + 5, + 6, + 7, + 8, + 9, + 10, + 11, + 12, + 13, + 14, + 15, + 16, + 17 + ] + }, + { + "threshold": 5, + "upper": [ + 0, + 3, + 5, + 7, + 8, + 10, + 12, + 14, + 15, + 17, + 19, + 21, + 22, + 24, + 26, + 28, + 29 + ] + }, + { + "threshold": 6, + "upper": [ + 0, + 4, + 7, + 10, + 12, + 14, + 17, + 20, + 22, + 24, + 27, + 30, + 32, + 34, + 37, + 40, + 42 + ] + }, + { + "threshold": 7, + "upper": [ + 0, + 5, + 9, + 13, + 16, + 19, + 22, + 26, + 29, + 32, + 35, + 39, + 42, + 45, + 48, + 52, + 55 + ] + }, + { + "threshold": 8, + "upper": [ + 0, + 6, + 11, + 16, + 20, + 24, + 28, + 32, + 36, + 40, + 44, + 48, + 52, + 56, + 60, + 64, + 68 + ] + }, + { + "threshold": 9, + "upper": [ + 0, + 7, + 13, + 19, + 24, + 29, + 34, + 39, + 43, + 48, + 53, + 58, + 63, + 68, + 73, + 78, + 82 + ] + }, + { + "threshold": 10, + "upper": [ + 0, + 8, + 15, + 22, + 28, + 34, + 40, + 46, + 51, + 56, + 62, + 68, + 74, + 80, + 86, + 92, + 97 + ] + }, + { + "threshold": 11, + "upper": [ + 0, + 9, + 17, + 25, + 32, + 39, + 46, + 53, + 59, + 65, + 71, + 78, + 85, + 92, + 99, + 106, + 112 + ] + }, + { + "threshold": 12, + "upper": [ + 0, + 10, + 19, + 28, + 36, + 44, + 52, + 60, + 67, + 74, + 81, + 88, + 96, + 104, + 112, + 120, + 127 + ] + }, + { + "threshold": 13, + "upper": [ + 0, + 11, + 21, + 31, + 40, + 49, + 58, + 67, + 75, + 83, + 91, + 99, + 107, + 116, + 125, + 134, + 142 + ] + }, + { + "threshold": 14, + "upper": [ + 0, + 12, + 23, + 34, + 44, + 54, + 64, + 74, + 83, + 92, + 101, + 110, + 119, + 128, + 138, + 148, + 157 + ] + }, + { + "threshold": 15, + "upper": [ + 0, + 13, + 25, + 37, + 48, + 59, + 70, + 81, + 91, + 101, + 111, + 121, + 131, + 141, + 151, + 162, + 172 + ] + }, + { + "threshold": 16, + "upper": [ + 0, + 14, + 27, + 40, + 52, + 64, + 76, + 88, + 99, + 110, + 121, + 132, + 143, + 154, + 165, + 176, + 187 + ] + }, + { + "threshold": 17, + "upper": [ + 0, + 15, + 29, + 43, + 56, + 69, + 82, + 95, + 107, + 119, + 131, + 143, + 155, + 167, + 179, + 191, + 202 + ] + } + ] +} diff --git a/research/query-tree-topology-optimum/README.md b/research/query-tree-topology-optimum/README.md new file mode 100644 index 0000000000..a032e4fc58 --- /dev/null +++ b/research/query-tree-topology-optimum/README.md @@ -0,0 +1,188 @@ +# Exact topology optimum for the nineteen-leaf query caller + +This contribution was produced by Nick Petalas. Claim type: a scoped +mathematical proof with a finite integer certificate. + +For the four-field merge and three-query root of Ali Romman's +[PR6348](https://github.com/CrocSwap/integer-mult-bounds/pull/6348), no +binary topology on nineteen native leaves improves the complete recursive +target-minus-paid power sum at any exponent `0 < s < 1`. The published +forest with root sizes `4,7,8` attains the optimum. Its internal-node size +histogram is the unique optimal histogram for each such exponent: + +```text +size 2 3 4 7 8 +multiplicity 9 1 4 1 1 +``` + +The result covers every positive three-part root partition, unbalanced +trees, arbitrary leaf labels and either order of the two children. It is +new finite-class optimality coverage. The predecessor supplies the module +and one attaining construction, without claiming a topology optimum. Its +merge identity and native realization are premises here, not review targets. + +This rules out a better recursive invoice through topology alone at this +leaf count. A changed merge, a changed leaf count or a changed native local +profile is a different question. There is no new kappa or selected-frontier +change, supplier admission, physical implementation or complete multiplication +theorem. + +## Reduction to a tree reward + +Write `P` for the number of ports and `d` for the fresh rank of each native +stage. In the actual source, `P=104` and `d=8`. An internal node on `n` +leaves supplies two independent rank-`dn+1` main targets per port, pays two +rank-`dn` whole idle calls per port, and pays one thin rank-one query per +port. All local helper/paid profiles of the nineteen native leaves stay +fixed, as does the rank-153 root target pair. No helper or idle is free. + +Thus, with target-minus-paid sign convention, the full recursive margin is + +```text +K(H) + 2P sum_v w(n_v), w(n) = H(dn+1) - H(dn), +K(H) = 19 L(H) + 2P H(19d+1) - 16P H(1). +``` + +Here `L(H)` is the fixed local helper credit minus local paid bill per +native call. Every three-root forest has sixteen binary internal nodes. +The sum runs over precisely these nodes, including each nontrivial subtree +root and excluding the final three-query root. This accounts for all +topology-dependent recursive targets and paid jobs in the retained contract. +Ordinary scalar work, routing, ownership and compiler realization retain +their separate obligations; this theorem does not optimize those costs. + +## A finite certificate for all decreasing convex rewards + +Let `F` be any full binary forest with three nonempty trees and nineteen +leaves. Each subtree has at most seventeen leaves. For each integer +`k=3,...,17`, define `h_k(n)=max(k-n,0)`. The certificate proves + +```text +sum_{v in F} h_k(n_v) <= B_k, +``` + +where the attaining histogram above gives, in increasing order of `k`, + +```text +9, 19, 33, 47, 61, 76, 92, 108, 124, 140, 156, 172, 188, 204, 220. +``` + +[CERTIFICATE.json](CERTIFICATE.json) contains seventeen integer upper bounds +`U_k(n)`, for `1 <= n <= 17`, for each hinge. The checker requires + +```text +U_k(1) = 0, +U_k(n) >= h_k(n) + U_k(a) + U_k(n-a) for every 1 <= a < n, +U_k(a) + U_k(b) + U_k(c) <= B_k whenever a+b+c=19 and a,b,c>=1. +``` + +Induction on the number of leaves proves the tree upper bound. The last +inequality then proves the forest upper bound. These are exhaustive finite +inequality checks, not samples of trees or real exponents. The verifier +checks 2,040 binary split inequalities and 2,295 ordered root inequalities. +It constructs the attaining forest separately and counts its actual nodes. +The optimizer is used only to generate a witness. It is not trusted by the +upper-bound checker. + +For a nonincreasing convex sequence `w(2),...,w(17)`, put + +```text +alpha = w(16)-w(17) >= 0, +delta_k = w(k-1)-2w(k)+w(k+1) >= 0, 3 <= k <= 16. +``` + +Successive finite differences give the exact identity + +```text +w(n) = w(17) + alpha h_17(n) + sum_{k=3}^{16} delta_k h_k(n). +``` + +Every forest has sixteen internal nodes, so its constant term is the +same. Multiplying the certified hinge bounds by these nonnegative +coefficients proves that the named forest maximizes every such reward. +This is an optimality result over a continuum of rewards, obtained from +fifteen exact integer certificates. + +For the power tariff, more generally take any real `d,b>0` and let +`w(x)=(dx+b)^s-(dx)^s`. When `0 0. +``` + +Consequently every coefficient in the hinge decomposition is strictly +positive. Equality of the reward forces equality of all fifteen hinge +scores. If `c_n` is the number of nodes of size `n` and +`A_k=sum_n c_n h_k(n)`, then `c_2=A_3`, +`c_n=A_{n+1}-2A_n+A_{n-1}` for `3<=n<=16`, and +`c_17=16-sum_{n=2}^{16} c_n`, with `A_2=0`. +Thus those scores and the fixed node count determine the histogram +uniquely. This proves the strict histogram assertion. The real-parameter +extension is a formal reward statement, not a construction of new native +operators. The invoice application uses `d=8,b=1`. + +## Reproduce + +Use CPython 3.12 and its standard library, from the repository root: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/query-tree-topology-optimum/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -O -B research/query-tree-topology-optimum/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/query-tree-topology-optimum +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/query-tree-topology-optimum --check-source-history +``` + +Expected marker: `PASS_QUERY_TREE_TOPOLOGY_OPTIMUM`, followed by the +registered runner's `PASS_REGISTERED_RESEARCH_PACKAGE` where applicable. +The direct commands emit generated receipts containing source and package +hashes. `--receipt PATH` additionally creates a new receipt at that path. +Normal and optimized registered commands are read-only. To regenerate the +integer certificate, run `generate.py` with the same interpreter and `-B`; +it writes JSON to stdout and checks equality with the retained certificate. + +The verifier checks exact rational hinge identities and rejects a lowered +split bound, an inflated unattainable root bound, an omitted hinge, a +Boolean substituted for an integer, a wrong leaf count and a worse +histogram. It authenticates both predecessor text inputs before checking. +No floating-point power evaluation or predecessor scientific replay is +needed. The written derivative, induction and equality arguments remain +outside a formal proof kernel. Independent human and formal proof-kernel +review are unclaimed. + +## Scope, credit and code constraints + +Credit Ali Romman for PR6348's four-field extension, paid complement, +binary-tree caller, nineteen-leaf construction and complete invoice; +Cinna Davis for the retained thin-query interface and query-thinned path; +DreamingOfClouds for the preceding native-word work; and the retained +P104/helper/native/compiler/outer lineage. Discrete finite differences and +dynamic programming are classical. The new contribution is the simultaneous +hinge optimum and its fixed-caller consequence. All predecessor files and +credit lines retain their bytes. Apache-2.0. + +The five inherited framework assumptions retain their status. Native +all-column implementation, owned erasure, compiler closure, precision/tape +and analytic recovery are not discharged. The source full replay, selected +cold replay, physical caller execution, Lean and Docker were not run. + +The new scripts use structured bounded loops, direct calls and checked +contracts. Their functions fit within sixty lines. Rule 3 of Power of Ten +has a managed-runtime deviation in these two Python scripts: Python and +JSON parsing allocate dynamically. The certificate input is capped at +64 KiB, with fifteen rows of seventeen bounded integers; all mathematical +work uses the fixed nineteen-leaf domain. There is no steady service or +unbounded work queue. Warning-strict normal and optimized execution check +the bounded paths and failure controls. A future variable-size solver +would need new resource limits before extending this scope. + +## Open next questions + +1. Can a changed leaf count improve the complete supplier invoice? This + theorem fixes nineteen. First form the corresponding complete local, + thin, whole-idle and root profiles, then retain compiler and outer + charges. The finite nineteen-leaf certificate does not settle that task. +2. Can a different merge or root contract improve the price beyond this + topology optimum? First state independent arbitrary inputs and every + paid complement. A favorable formal reward alone does not establish + native realization, restoration or supplier admission. diff --git a/research/query-tree-topology-optimum/SOURCES.json b/research/query-tree-topology-optimum/SOURCES.json new file mode 100644 index 0000000000..a2c45c1dc5 --- /dev/null +++ b/research/query-tree-topology-optimum/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a", + "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/balanced-query-tree/PROOF.md", + "usage": "input", + "git_blob": "08dd3e35b0bdd5a6e39f88183b2793c6bb5af6ca", + "sha256": "1fab54bc665bf6882f0bbd772af15fbf69a92eac040951ccd19a5accf02f328e" + }, + { + "path": "research/balanced-query-tree/README.md", + "usage": "input", + "git_blob": "0002a8f3f3f7aa4d6bb502f3c433d28532b61c8c", + "sha256": "c2fc24ddc0e68e59702afea581043f1a4dc7c553d46a7bd4da3ed339ba1675d3" + } + ] +} diff --git a/research/query-tree-topology-optimum/TASK.json b/research/query-tree-topology-optimum/TASK.json new file mode 100644 index 0000000000..47a50d762e --- /dev/null +++ b/research/query-tree-topology-optimum/TASK.json @@ -0,0 +1,90 @@ +{ + "schema_version": 1, + "task_id": "joint-query-controller", + "priority_revision": 8, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "original_card": { + "id": "joint-query-controller", + "question": "Can a changed query demand or caller remove real work while satisfying native chronology and restoration?", + "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": "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": "Choose an exact caller and a new demand/interface hypothesis. Read the scoped #5617/#5631/#5649/#5747 and #5720/#5745 objections before rebuilding an excluded schedule. Compare the complete matched source/consumer protocols including all retained helper outputs. For an active-mode injection, first check #5745: its canonical delivery claim repays the eight removed centre jobs. Audit that exact claim or change its channel/feedback hypothesis; do not repeat the same free-injection search. Stop if the full favorable budget fails or the required restored output is unobservable.", + "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": [ + "query demand", + "active mode", + "5720", + "5745", + "5747", + "caller" + ], + "existing_checks": [ + { + "scope": "PR #4166: author-checked installed producer/service/return/bridge connection; native-component comparison loses.", + "evidence": "research/qq16-caller-install/README.md", + "remaining": "Complete matched physical protocol bill, or changed source-compatible demand/circuit; no affordable supplier yet.", + "status": "author-checked", + "source_commit": "0b082d22a0e9a442d264ab0633e35ef26c790630", + "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": "Prove the exact nineteen-leaf three-root binary topology optimum for the retained four-field query merge, simultaneously for every decreasing convex node reward and every power tariff with exponent strictly between zero and one.", + "scope_change_reason": "The chosen caller is PR6348. Instead of constructing a new interface or auditing its proof, settle whether topology alone can improve its complete recursive moment at fixed leaf count.", + "bottleneck_link": "The selected complex supplier binds. Newer proposals retain this binary caller; a complete finite topology obstruction tells the next contributor to change the merge, native profile or leaf count rather than re-enumerate nineteen-leaf trees.", + "budget_minutes": 60, + "stop_rule": "Ship the first verified original finite-class obstruction; do not search larger leaf counts or changed modules.", + "outcome": "completed", + "evidence": "README.md proof, CERTIFICATE.json integer upper witnesses, independently checked by verify.py. No predecessor scientific replay is the deliverable.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can a changed leaf count improve the complete invoice?", + "why_it_matters": "The fixed nineteen-leaf optimum does not bound other leaf counts.", + "first_step": "Form every local, thin-query, whole-idle and root profile for one different leaf count.", + "blocked_by": "Complete compiler, native caller and outer charges must still be supplied." + }, + { + "question": "Can a changed merge or root contract beat the fixed-topology optimum?", + "why_it_matters": "The result fixes the four-field module and three-query root.", + "first_step": "State arbitrary independent inputs and all paid complements before optimizing.", + "blocked_by": "Native realization, dirty restoration and a favorable complete bill." + } + ] +} diff --git a/research/query-tree-topology-optimum/VERIFY.json b/research/query-tree-topology-optimum/VERIFY.json new file mode 100644 index 0000000000..664d270e91 --- /dev/null +++ b/research/query-tree-topology-optimum/VERIFY.json @@ -0,0 +1,46 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/balanced-query-tree/PROOF.md", + "research/balanced-query-tree/README.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 30, + "checks": "All fifteen integer hinge certificates, attaining forest, rational basis identities, six rejection controls and exact predecessor text bindings." + }, + { + "argv": [ + "{python}", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 30, + "checks": "All fifteen integer hinge certificates, attaining forest, rational basis identities, six rejection controls and exact predecessor text bindings." + }, + { + "argv": [ + "{python}", + "-W", + "error", + "-B", + "{package}/generate.py" + ], + "timeout_seconds": 30, + "checks": "Deterministic regeneration of the full integer certificate, compared byte-for-byte with CERTIFICATE.json." + } + ] +} diff --git a/research/query-tree-topology-optimum/generate.py b/research/query-tree-topology-optimum/generate.py new file mode 100644 index 0000000000..d5bf4feb2a --- /dev/null +++ b/research/query-tree-topology-optimum/generate.py @@ -0,0 +1,25 @@ +#!/usr/bin/env python3 +"""Generate the finite integer upper certificate; output only to stdout.""" + +import json +from pathlib import Path + + +def main(): + rows = [] + for threshold in range(3, 18): + optimum = [0] * 18 + for leaves in range(2, 18): + child_best = max(optimum[left] + optimum[leaves - left] for left in range(1, leaves)) + optimum[leaves] = max(threshold - leaves, 0) + child_best + rows.append({"threshold": threshold, "upper": optimum[1:]}) + certificate = {"schema": "query-tree-hinge-upper/1", "leaves": 19, "roots": 3, "hinges": rows} + payload = json.dumps(certificate, indent=2) + "\n" + existing = Path(__file__).with_name("CERTIFICATE.json") + if existing.exists() and existing.read_text(encoding="utf-8") != payload: + raise ValueError("generated certificate differs from committed certificate") + print(payload, end="") + + +if __name__ == "__main__": + main() diff --git a/research/query-tree-topology-optimum/verify.py b/research/query-tree-topology-optimum/verify.py new file mode 100644 index 0000000000..9a8cc2cf5b --- /dev/null +++ b/research/query-tree-topology-optimum/verify.py @@ -0,0 +1,191 @@ +#!/usr/bin/env python3 +"""Check finite upper certificates, without running a tree optimizer.""" + +import argparse +import copy +import hashlib +import json +from fractions import Fraction +from pathlib import Path + + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parents[1] +SIZES = tuple(range(2, 18)) +HISTOGRAM = {2: 9, 3: 1, 4: 4, 7: 1, 8: 1} + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def load_json(path): + require(path.stat().st_size <= 65536, "JSON exceeds 64 KiB") + return json.loads(path.read_text(encoding="utf-8")) + + +def authenticate_sources(): + manifest = load_json(PACKAGE / "SOURCES.json") + rows = [row for row in manifest["files"] if row["usage"] == "input"] + expected = { + "research/balanced-query-tree/PROOF.md", + "research/balanced-query-tree/README.md", + } + require(len(rows) == 2 and {row["path"] for row in rows} == expected, "source inventory") + for row in rows: + payload = (ROOT / row["path"]).read_bytes() + require(hashlib.sha256(payload).hexdigest() == row["sha256"], "source SHA256") + header = f"blob {len(payload)}\0".encode() + require(hashlib.sha1(header + payload).hexdigest() == row["git_blob"], "source blob") + return {row["path"]: row["sha256"] for row in rows} + + +def check_certificate(certificate, histogram): + require(set(certificate) == {"schema", "leaves", "roots", "hinges"}, "certificate fields") + require(certificate["schema"] == "query-tree-hinge-upper/1", "schema") + require(type(certificate["leaves"]) is int and certificate["leaves"] == 19, "leaves") + require(type(certificate["roots"]) is int and certificate["roots"] == 3, "roots") + require(all(type(n) is int and n in SIZES for n in histogram), "node sizes") + require(all(type(c) is int and 0 < c <= 16 for c in histogram.values()), "multiplicities") + require(sum(histogram.values()) == 16, "sixteen binary nodes") + rows = certificate["hinges"] + require(isinstance(rows, list) and len(rows) == 15, "hinge inventory") + split_checks = root_checks = 0 + scores = [] + for threshold, row in zip(range(3, 18), rows, strict=True): + require(set(row) == {"threshold", "upper"}, "hinge fields") + require(type(row["threshold"]) is int and row["threshold"] == threshold, "threshold") + upper = row["upper"] + require(isinstance(upper, list) and len(upper) == 17, "upper dimensions") + require(all(type(v) is int and 0 <= v <= 256 for v in upper), "upper range") + require(upper[0] == 0, "leaf has no reward") + for size in SIZES: + toll = max(threshold - size, 0) + for left in range(1, size): + bound = toll + upper[left - 1] + upper[size - left - 1] + require(upper[size - 1] >= bound, "binary split upper bound") + split_checks += 1 + score = sum(count * max(threshold - size, 0) for size, count in histogram.items()) + for first in range(1, 18): + for second in range(1, 19 - first): + third = 19 - first - second + bound = upper[first - 1] + upper[second - 1] + upper[third - 1] + require(bound <= score, "root upper bound exceeds attaining histogram") + root_checks += 1 + scores.append(score) + return scores, split_checks, root_checks + + +def construct_attainer(): + # Reconstruct the named forest independently from the stored histogram. + nodes = [(1, 1), (1, 2), (2, 2), (3, 4), (4, 4)] + trees = {1: ()} + for left, right in nodes: + trees[left + right] = (trees[left], trees[right]) + pending = [trees[4], trees[7], trees[8]] + histogram = {} + leaves = [] + # A forest with 19 leaves has 16 internal nodes and 35 nodes in total. + for _ in range(35): + require(bool(pending), "attainer traversal ended early") + tree = pending.pop() + if not tree: + leaves.append(1) + else: + frontier = [tree] + size = 0 + for _ in range(15): + if not frontier: + break + item = frontier.pop() + if item: + frontier.extend(item) + else: + size += 1 + require(not frontier, "subtree traversal bound") + histogram[size] = histogram.get(size, 0) + 1 + pending.extend(tree) + require(not pending and len(leaves) == 19, "attainer leaf count") + require(histogram == HISTOGRAM, "attainer histogram") + return histogram + + +def check_hinge_decomposition(): + # Exact rational checks of the basis identity in the written proof. + fixtures = [tuple(Fraction(1, n**power) for n in SIZES) for power in (1, 2, 3)] + fixtures += [tuple(Fraction(max(k - n, 0)) for n in SIZES) for k in range(3, 18)] + fixtures += [tuple(Fraction(7) for _ in SIZES), tuple(Fraction(31 - n) for n in SIZES)] + for values in fixtures: + slope = values[-2] - values[-1] + second = {k: values[k - 3] - 2 * values[k - 2] + values[k - 1] for k in range(3, 17)} + require(slope >= 0 and all(v >= 0 for v in second.values()), "convex fixture") + for n, value in zip(SIZES, values, strict=True): + reconstructed = values[-1] + slope * (17 - n) + reconstructed += sum(delta * max(k - n, 0) for k, delta in second.items()) + require(reconstructed == value, "hinge decomposition") + return len(fixtures) * len(SIZES) + + +def rejection_controls(certificate, histogram): + controls = [] + bad = copy.deepcopy(certificate) + bad["hinges"][0]["upper"][1] -= 1 + controls.append((bad, histogram)) + bad = copy.deepcopy(certificate) + bad["hinges"][-1]["upper"][7] += 1 + controls.append((bad, histogram)) + bad = copy.deepcopy(certificate) + bad["hinges"].pop() + controls.append((bad, histogram)) + bad = copy.deepcopy(certificate) + bad["hinges"][0]["upper"][0] = False + controls.append((bad, histogram)) + bad = copy.deepcopy(certificate) + bad["leaves"] = 18 + controls.append((bad, histogram)) + wrong_histogram = dict(histogram) + wrong_histogram[2] -= 1 + wrong_histogram[3] += 1 + controls.append((certificate, wrong_histogram)) + for candidate, counts in controls: + try: + check_certificate(candidate, counts) + except ValueError: + continue + raise ValueError("semantic control accepted") + return len(controls) + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--receipt", type=Path) + args = parser.parse_args() + sources = authenticate_sources() + certificate = load_json(PACKAGE / "CERTIFICATE.json") + histogram = construct_attainer() + scores, splits, roots = check_certificate(certificate, histogram) + receipt = { + "marker": "PASS_QUERY_TREE_TOPOLOGY_OPTIMUM", + "claim_type": "scoped proof with finite integer certificate", + "hinge_scores": scores, + "split_inequalities": splits, + "root_inequalities": roots, + "basis_identity_checks": check_hinge_decomposition(), + "rejection_controls": rejection_controls(certificate, histogram), + "source_sha256": sources, + "package_sha256": { + name: hashlib.sha256((PACKAGE / name).read_bytes()).hexdigest() + for name in ("CERTIFICATE.json", "verify.py", "generate.py", "README.md", "SOURCES.json") + }, + } + payload = json.dumps(receipt, indent=2, sort_keys=True) + "\n" + if args.receipt is not None: + with args.receipt.open("x", encoding="utf-8") as stream: + written = stream.write(payload) + require(written == len(payload), "short receipt write") + print(payload, end="") + + +if __name__ == "__main__": + main()