From 8f8f518bd1a40baa30434ab18e86fd851d122b28 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Thu, 22 Oct 2026 23:24:10 +0100 Subject: [PATCH] feat(research): bound all-depth QQ16 parked volume --- research/qq16-parking-power-law/README.md | 260 +++++++++++++++++++ research/qq16-parking-power-law/SOURCES.json | 30 +++ research/qq16-parking-power-law/TASK.json | 96 +++++++ research/qq16-parking-power-law/VERIFY.json | 37 +++ research/qq16-parking-power-law/verify.py | 246 ++++++++++++++++++ 5 files changed, 669 insertions(+) create mode 100644 research/qq16-parking-power-law/README.md create mode 100644 research/qq16-parking-power-law/SOURCES.json create mode 100644 research/qq16-parking-power-law/TASK.json create mode 100644 research/qq16-parking-power-law/VERIFY.json create mode 100644 research/qq16-parking-power-law/verify.py diff --git a/research/qq16-parking-power-law/README.md b/research/qq16-parking-power-law/README.md new file mode 100644 index 0000000000..e9eff8b9d0 --- /dev/null +++ b/research/qq16-parking-power-law/README.md @@ -0,0 +1,260 @@ +# A critical-exponent law for QQ16's parked current-bank volume + +This contribution is produced by Nick Petalas. Apache-2.0. + +**Claim type: scoped recurrence proof with exact finite corroboration.** +For the original selected-C child backend retained inside the QQ16 caller, +assume the published tree and volume premises of Brian's +[PR #4753](https://github.com/CrocSwap/integer-mult-bounds/pull/4753), head +`44e2c79344e0090d4e829e0dde4f533d8d0273ec`. The volume-weighted current-bank +parking subtrace has a two-sided power law at its exact critical exponent. +The bounds below hold for every integer width `w >= 356` in the stated +recurrence, with no extra logarithmic factor: + +```text + ((w + 3456/25) / (355 + 3456/25))^s - 1 +H(w) >= ------------------------------------------------, + 248163/7168 + + (w/4)^s - 1 +H(w) <= ----------------, + 248163/7168 + +0.9983245373 < s < 0.9983245374. +``` + +Thus `H(w) = Theta(w^s)` for this fixed-cutoff recurrence, and no smaller +power gives an asymptotic upper bound. The exponent is the root of the +**already existing supplier moment**. More digits of that root are not the +new result. The new result is the quantified two-sided parked-volume bound, +including its endpoint exponent, floor correction and finite cutoff. +No literature-priority claim is made for the weighted-tree argument. + +## Premises and the exact quantity being bounded + +The live input is the published, hash-bound `RESULT.json` from #4753. Its +histogram, global cutoff and physical interpretation are cited premises. +This package does not rerun its census or audit its sources. The proof also +uses #4753's written fresh-row/full-spectator-volume argument. + +In the historical descriptor family `p=2^8500`, the unchanged global height +makes a call terminal exactly when its integer width is below 356. At every +nonterminal selected-C node, with `q=floor(w/73)`, the selected children have +width `r q`, multiplicity `n_r Gamma`, and full physical bank volume +`v/(14336 Gamma)` when the parent's bank volume is `v`. The inherited list is: + +```text +r 1 2 3 4 5 7 8 48 +n_r 349604 60192 62585 20448 11808 7 1152 4866 +``` + +The source tests its global cutoff before removing the remainder and does +not test again after stripping it. In particular a fresh width-356 call runs +its selected program at width 292. Its selected child parking is still paid. +Remainder leaves, native/Ordinary internals, other parked roles and restore +work are outside the subtrace considered here. + +Put `N=sum n_r=510662`, `c_r=n_r/14336` and `C=sum c_r=255331/7168`. +The normalized internal-node mass is the unique terminating recurrence + +```text +H(w) = 0, 0 <= w < 356, +H(w) = 1 + sum_r c_r H(r floor(w/73)), w >= 356. +``` + +For one complete original C8 call of width `w` and input-bank bit length `v`, +let `P(w,v)` sum the current-bank bit length once per selected-child parking +pair, across the complete selected-C descendant tree. Then exactly + +```text +P(w,v) = N Gamma v H(w). +``` + +To prove this identity, group internal nodes by rank path. At depth `j` their +multiplicity contains `Gamma^j`, and each current bank has volume +`v/(14336 Gamma)^j`. These factors of Gamma cancel. Each such node parks its +whole current bank once for each of its `N Gamma` selected children. +The normalized path weight is consequently `prod(n_r/14336)`. +Counting calls without dividing descendant volume gives a different quantity. + +For the sixteen equal-volume removed C8 calls per outer cover in #4753, +this extends its once-generation term to + +```text +P_removed = 16 N Gamma^2 v H(8 lambda). +``` + +Under the same source assumptions, #4753's literal park-loop lower bound +therefore gives removed reads, writes and unit moves at least +`(2,5,5) P_removed`. This remains one removed expense. It does not determine +the sign of `T_D-T_B`, `T_D-T_B*` or an implemented `D*` comparison. + +The abstract recurrence permits arbitrary widths. A physical application +additionally requires an admitted root, sufficient fresh-row stock for its +whole reached tree, and the inherited source, layout, precision, restoration +and native contracts. In particular the fixed physical descriptor has finite +root width. The statement `Theta(w^s)` concerns the recurrence as `w` tends +to infinity, not an assertion of unbounded admissible widths for that one +fixed RootPlan. No smaller root stock is installed. + +## Proof of the critical-exponent envelope + +Define + +```text +M(t) = sum_r c_r (r/73)^t. +``` + +Every `r/73` lies strictly between zero and one. Therefore M is continuous +and strictly decreasing. The exact inequalities + +```text +M(0) = 255331/7168 > 1, +M(1) = 1041408/1046528 < 1 +``` + +give a unique `s` in `(0,1)` with `M(s)=1`. The rational interval calculation +in the verifier encloses this root as displayed above. This is a convenient +certified coordinate for the proof, not a changed supplier saving or kappa. + +Expand the grouped rank tree to its terminal leaves. A rank-r edge has weight +`c_r`, and a vertex has the product of its edge weights. Let I be the sum of +internal vertex weights, including the root, and L the sum of terminal leaf +weights. Every child has width at most `48w/73`, so the tree is finite. +Each internal vertex replaces its own frontier weight by C times that weight. +Telescoping the resulting increments gives the exact identity + +```text +I = H(w), L = 1 + (C-1) H(w). +``` + +For `phi(x)=x^s`, writing `w=73q+delta` gives + +```text +sum_r c_r phi(r q) = (73q)^s <= w^s. +``` + +Apply this inequality at every internal vertex. The weighted terminal sum +of `phi` is at most `w^s`. Every terminal descendant of a nonterminal root +has width at least `floor(356/73)=4`, and at most 355. Consequently +`4^s L <= w^s`, which proves the upper bound after substituting for L. + +For the reverse inequality take `b=3456/25` and `psi(x)=(x+b)^s`. For every +rank in the list and every `delta` in `{0,...,72}`, + +```text +b >= r delta/(73-r), +r q + b >= (r/73)(w+b). +``` + +The largest allowance is exactly `48*72/(73-48)=3456/25`. +It is sharp for a uniform shift that must satisfy these individual affine +inequalities. It is not claimed to optimize every possible potential or the +constants in the final envelope. Since `s>0` and `M(s)=1`, + +```text +sum_r c_r psi(r q) >= (w+b)^s. +``` + +The weighted terminal sum of psi is therefore at least `(w+b)^s` and at most +`(355+b)^s L`. Substituting the exact identity for L proves the lower bound. +Both bounding expressions grow as positive constants times `w^s`, completing +the two-sided asymptotic statement. Every step uses a finite tree; no exchange +of an infinite sum with a limit is needed. + +## Exact verification and reproduction + +From the repository root, use the interpreter available in this workspace: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/qq16-parking-power-law +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/qq16-parking-power-law/verify.py +``` + +For another checkout, replace that absolute interpreter path with CPython +3.12. The registered normal and optimized commands each run the standalone +standard-library verifier. It writes no files. Its JSON output is a generated +receipt containing hashes of the package files. + +The verifier checks all 8,193 widths from 0 through 8,192 for the weighted +leaf identity. An independently arranged integer path census checks eleven +widths from 356 through 1,048,576, retaining level-by-level active and terminal +path multiplicities and their denominators. It compares the two methods +where their domains meet and checks both envelopes with outward rational +bounds. For example `H(584)=9601/7168`, the first extra-generation value. +These are finite corroboration of the written proof, not physical execution. + +The root enclosure uses log range reduction to `[1,2]`, 48 terms of the +atanh series with its positive geometric tail, and outward rounding to +40 decimal places. It evaluates `x^s` as `x exp((1-s) log(1/x))` for `x<=1` +and by the corresponding reciprocal formula for `x>=1`. The positive exp +series through degree 12 has tail at most its first omitted term divided +by `1-y/14`. All acceptance comparisons use rational arithmetic. +Eight controls distinguish two incorrect exponent brackets, reversed +endpoints, a repeated cutoff, terminal equality, missing fresh-row volume, +ceiling instead of floor, and an insufficient affine shift. +These compare specific incorrect predictions at named boundary witnesses. + +The source-binding positive control for the current selected record passed. +The card's historical `scripts/research_baseline.py` raises `KeyError: +bit_lower` against that changed record. It is not treated as scientific +verification. The current selected record remains unchanged. + +## Scope, resources and remaining obligations + +This is an ordinary written proof with an exact host certificate. Independent +human and formal proof-kernel review are unclaimed. No production C8 payload, +full RootLayer, native execution, complete cost comparison, supplier admission, +new kappa or selected-frontier change is established. No predecessor result +is independently validated by this package. + +Power of Ten rule 3 deviation: CPython's Fraction, Counter and JSON operations +allocate dynamically. This verifier is a finite exact certificate, not a +steady-state service. The DP arrays contain 8,193 entries each; the integer +census accepts widths at most `2^20`, at most 4,096 simultaneous distinct +widths and at most 64 levels. Child widths decrease by a factor at most +48/73. Series have 48 and 12 fixed terms, arguments have explicit bounds, +and the two authenticated premise files are each capped at 1 MiB. The +finite integers and rational denominators have bounds derived from these +limits. These bounds, ordinary failure exits and warning-as-error runs are +the compensating controls. Reassess capacities and arithmetic size before +raising any limit. There are no recursive calls or proof-relevant child +processes. Functions stay below 60 lines. Static parsing and normal/optimized +warning-as-error execution are the available Python diagnostics; no new +repository-wide lint configuration is introduced. + +## Open next questions + +1. Bound the complete unmatched candidate nonchild and shell work at one + admitted nonterminal geometry. The present removed-expense bound alone + cannot settle affordability. Start by supplying an upper bound for the + corresponding candidate terms while retaining every later root call. + This is blocked by the existing unpriced physical operations and control. +2. Determine the necessary stock and descriptor range when applying this + envelope to a growing family of admitted roots rather than a fixed-cutoff + recurrence. Start with the actual RootPlan height/cutoff relation and + source row divisions. Root admission and full physical contracts remain + separate premises; no construction expansion is justified by this bound. + +## Predecessor credit and coordination + +Brian / JoyboyBrian's #4753 supplies the histogram, cutoff, full-volume +fresh-row relation, original-child-backend boundary and park-loop floor. +Chris R / Clear1nsight's #4166, #4167, #4172 and #4177 supply the installed +caller, protected returns, context cancellation and terminal-band comparison. +Jose Manuel supplies the physical C/Ordinary/Compact machinery. Preserve +ywz65, Sagar Thakrar, Tekalign, Ali Romman, Arham Tahir and the full source +lineage credited in those packages. Their census and physical claims are +premises here. #4790 composes protected returns in the installed outer caller; +it does not replace the original descendant backend bounded here. + +Base main is `624de9dc66858af0945e5f8a0942488d62280d43`, priority revision 7. +This refines the joint-query-controller card to a scoped analytic cost +obligation rather than another decoder or construction round. Entry overlap +covered 379 open PRs and 3,853 Discussion records with complete pagination. +The sparse local scan covered 115 of 6,319 tracked note paths; separate Git +searches covered distinctive terms across main READMEs/proofs. Closed-code +and unpublished-work coverage is incomplete. These searches are not a +novelty certificate. + +[Advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19133725). diff --git a/research/qq16-parking-power-law/SOURCES.json b/research/qq16-parking-power-law/SOURCES.json new file mode 100644 index 0000000000..e2e23e52fd --- /dev/null +++ b/research/qq16-parking-power-law/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "624de9dc66858af0945e5f8a0942488d62280d43", + "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/qq16-nonterminal-c8-tree/README.md", + "usage": "input", + "git_blob": "55bd5ce66846b5ddf124c655c617a8b47b52d9b7", + "sha256": "e57f9c84275c5cf0baf914322392a8ba0b39e014490c396ed1da85fb005337a2" + }, + { + "path": "research/qq16-nonterminal-c8-tree/RESULT.json", + "usage": "input", + "git_blob": "8c11adabc19648de3ebcfb20cbad1cd47ee63e5d", + "sha256": "0e3fbddf58103dd04c2bdf2912b30c218e3e68a974aac868bd07b2cc1280230b" + } + ] +} diff --git a/research/qq16-parking-power-law/TASK.json b/research/qq16-parking-power-law/TASK.json new file mode 100644 index 0000000000..6b357b60d3 --- /dev/null +++ b/research/qq16-parking-power-law/TASK.json @@ -0,0 +1,96 @@ +{ + "schema_version": 1, + "task_id": "joint-query-controller", + "priority_revision": 7, + "base_commit": "624de9dc66858af0945e5f8a0942488d62280d43", + "original_card": { + "id": "joint-query-controller", + "question": "Can the installed QQ16 caller win a complete matched protocol bill, or can a changed demand eliminate actual paid work?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/qq16-caller-install/README.md" + ], + "methods": [ + "Derive the matched whole-caller physical bill for installed and baseline protocols.", + "Change the actual demanded observations and prove a cheaper legal producer/consumer contract." + ], + "acceptance_gate": "Name the changed premise of the fixed F0/B1 observation obstruction. Show exactly which query is recovered, legal native reads and restoration, and a full favorable budget including cover maps, helpers and endpoints. Local inverse identities alone do not close the global controller. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read #4166 COST.md and ADMISSION.json. An actual caller connection is now proposed. Its native-component profile loses; parent park/restore versus external-call costs remain unresolved. Retain the producer and recovery lineage rather than rebuild it.", + "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately." + }, + "first_experiment": "At the actual installed cut, compare matched complete parent park/restore and external input/return protocols at the same bank/packet geometry, including every later root call and service cost. Alternatively pin both bridge observations and derive a genuinely smaller source-compatible demand. Stop if the complete necessary inequality fails or an essential cost is unknown; no larger decoder scan from a local tape-action saving.", + "bottleneck_link": "The native local words exist; retained query information and its physical access are the missing link to a composed recursive interface.", + "allowed_variations": [ + "One paid query, one changed first pair, or one precisely specified affine helper state.", + "A counterexample or lower bound for that exact proposed repair.", + "One unresolved obligation of a newer local decoder, with exact source heads and a distinct claim/domain." + ], + "scope_change_triggers": [ + "Retaining the fixed first pair and ordinary schedule while allowing only homogeneous selected-only control, already excluded by the witness.", + "Treating cover-map counts as zero-cost physical address operations.", + "Recreating the pending complete local decoder or early-record/output-bank coalescing already under investigation without a distinct audit or changed premise.", + "Treating a completed-output defect inequality as a producer-interior, dirty-range or physical-cost certificate.", + "Recreating completed-output recovery or caller wiring already supplied by #4166 without new independent coverage.", + "Dropping retained later root calls or claiming native-profile dominance from the isolated publication saving." + ], + "overlap_terms": [ + "QQ16", + "joint-query", + "changing-chart controller", + "selected observation", + "1969", + "2540", + "early record", + "output-bank retention", + "complete native decoder", + "2965", + "producer defect", + "dirty-helper range", + "F17 consumer", + "4166", + "qq16-caller-install" + ], + "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_status": "refined", + "actual_scope": "Two-sided critical-exponent envelope for the all-depth current-bank parked-volume recurrence of the unchanged QQ16 child backend.", + "scope_change_reason": "Take PR4753's deeper-generation handoff as a scoped analytic cost bound; its histogram and volume relation are premises, not an audit deliverable.", + "bottleneck_link": "Prices one removed expense at nonterminal C8 widths, without inferring the complete QQ16 cost sign or expanding construction.", + "budget_minutes": 60, + "stop_rule": "Stop at the first proved explicit all-depth envelope and its exact bounded certificate.", + "outcome": "completed", + "evidence": "README.md quantified proof; verify.py exact root enclosure, leaf identity, independent integer path census and rejection controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Bound the complete unmatched candidate nonchild and shell work at an admitted nonterminal geometry.", + "why_it_matters": "A removed expense cannot determine the full signed comparison.", + "first_step": "Upper-bound the candidate terms at one identical complete geometry, retaining the later suffix.", + "blocked_by": "Unpriced physical operations and control." + }, + { + "question": "Relate the envelope to a growing family of admitted physical roots.", + "why_it_matters": "A fixed-cutoff recurrence is not an unbounded physical RootPlan family.", + "first_step": "Bind the RootPlan height/cutoff relation and row-stock divisions.", + "blocked_by": "Full descriptor admission and physical source contracts." + } + ] +} diff --git a/research/qq16-parking-power-law/VERIFY.json b/research/qq16-parking-power-law/VERIFY.json new file mode 100644 index 0000000000..5800fab6c6 --- /dev/null +++ b/research/qq16-parking-power-law/VERIFY.json @@ -0,0 +1,37 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/qq16-nonterminal-c8-tree/README.md", + "research/qq16-nonterminal-c8-tree/RESULT.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "critical-exponent-envelope-path-census-controls" + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "critical-exponent-envelope-path-census-controls-optimized" + } + ] +} diff --git a/research/qq16-parking-power-law/verify.py b/research/qq16-parking-power-law/verify.py new file mode 100644 index 0000000000..e8f6ca56b3 --- /dev/null +++ b/research/qq16-parking-power-law/verify.py @@ -0,0 +1,246 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Exact certificate for the stated parked-volume recurrence. + +Produced by Nick Petalas. The histogram and source-tree premises are Brian's +PR4753, with the physical/QQ16 predecessor attribution retained in README.md. +""" + +from collections import Counter +from fractions import Fraction as Q +from hashlib import sha256 +import json +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +DENOMINATOR = 14336 +DIMENSION = 73 +THRESHOLD = 356 +SHIFT = Q(3456, 25) +EXPONENT_LO = Q(9983245373, 10**10) +EXPONENT_HI = Q(9983245374, 10**10) +DP_LIMIT = 8192 +TREE_LIMIT = 2**20 + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def read_bounded(path, limit): + with path.open("rb") as stream: + raw = stream.read(limit + 1) + need(len(raw) <= limit, "bounded file input: " + str(path)) + return raw + + +def load_premises(): + manifest = json.loads(read_bounded(HERE / "SOURCES.json", 2**16)) + need(len(manifest["files"]) <= 16, "source row bound") + authenticated = {} + for row in manifest["files"]: + if row["usage"] == "input": + raw = read_bounded(ROOT / row["path"], 2**20) + need(sha256(raw).hexdigest() == row["sha256"], "premise digest") + authenticated[row["path"]] = raw + published = json.loads(authenticated["research/qq16-nonterminal-c8-tree/RESULT.json"]) + counts = {int(r): n for r, n in published["rank_histogram"].items()} + need(len(counts) == 8, "eight inherited rank classes") + need(all(1 <= r <= 48 and type(n) is int and n > 0 + for r, n in counts.items()), "positive inherited multiplicities") + need(published["first_nonterminal_width"] == THRESHOLD, "inherited cutoff") + return tuple(sorted(counts.items())) + + +def log_interval(value): + """Enclose log(value), value >= 1, by 48 atanh terms and their tail.""" + need(1 <= value <= 2**24, "log argument bound") + reduced, shifts = Q(value), 0 + for _ in range(25): + if reduced < 2: + break + reduced /= 2 + shifts += 1 + need(1 <= reduced < 2, "bounded log range reduction") + intervals = [] + for argument in (reduced, Q(2)): + z = (argument - 1) / (argument + 1) + partial = sum((2 * z**(2*j+1) / (2*j+1) for j in range(48)), Q(0)) + tail = 2 * z**97 / (97 * (1 - z*z)) + intervals.append((partial, partial + tail)) + lower = intervals[0][0] + shifts * intervals[1][0] + upper = intervals[0][1] + shifts * intervals[1][1] + scale = 10**40 + # Round outward to keep subsequent rational powers small. + return Q(lower * scale // 1, scale), Q(-(-upper * scale // 1), scale) + + +def exp_interval(value): + """Positive Taylor series through degree 12, with geometric tail.""" + need(0 <= value < 1, "exp argument bound") + term, partial = Q(1), Q(1) + for j in range(1, 13): + term *= value / j + partial += term + first_omitted = term * value / 13 + return partial, partial + first_omitted / (1 - value / 14) + + +def power_interval(base, exponent): + """Enclose base**exponent near exponent one using rational arithmetic.""" + need(Q(1, 73) <= base <= 2**24, "power argument bound") + need(Q(99, 100) <= exponent <= 1, "power exponent bound") + inverse = base < 1 + argument = 1 / base if inverse else base + log_lo, log_hi = log_interval(argument) + lower = exp_interval((1 - exponent) * log_lo)[0] + upper = exp_interval((1 - exponent) * log_hi)[1] + return (base * lower, base * upper) if inverse else (base / upper, base / lower) + + +def moment_interval(counts, exponent): + intervals = [(Q(n, DENOMINATOR), power_interval(Q(r, DIMENSION), exponent)) + for r, n in counts] + return tuple(sum((c * bounds[i] for c, bounds in intervals), Q(0)) + for i in range(2)) + + +def exponent_certificate(counts, lower, upper): + need(0 < lower < upper < 1, "ordered interior exponent bracket") + left, right = moment_interval(counts, lower), moment_interval(counts, upper) + need(left[0] > 1 and right[1] < 1, "opposite strict moment signs") + return left, right + + +def bottom_up(counts): + """Two independent recurrences: internal node mass and leaf mass.""" + tolls = [Q(0)] * (DP_LIMIT + 1) + leaves = [Q(1)] * (DP_LIMIT + 1) + for width in range(THRESHOLD, DP_LIMIT + 1): + q = width // DIMENSION + need(max(r*q for r, _ in counts) < width, "strict child descent") + tolls[width] = 1 + sum((Q(n, DENOMINATOR) * tolls[r*q] + for r, n in counts), Q(0)) + leaves[width] = sum((Q(n, DENOMINATOR) * leaves[r*q] + for r, n in counts), Q(0)) + return tolls, leaves + + +def level_census(counts, width): + """Count paths by depth with integer n_r, leaving Gamma symbolic.""" + need(type(width) is int and 0 <= width <= TREE_LIMIT, "tree width bound") + frontier, rows = Counter({width: 1}), [] + for depth in range(64): + if not frontier: + return rows + need(len(frontier) <= 4096, "frontier capacity") + active = {w: n for w, n in frontier.items() if w >= THRESHOLD} + rows.append((depth, sum(active.values()), + sum(n for w, n in frontier.items() if w < THRESHOLD))) + children = Counter() + for w, paths in active.items(): + for rank, multiplicity in counts: + child = rank * (w // DIMENSION) + need(child < w, "census child descent") + if child not in children: + need(len(children) < 4096, "successor frontier capacity") + children[child] += paths * multiplicity + frontier = children + raise ValueError("64-level capacity exhausted") + + +def census_masses(rows): + internal = sum((Q(active, DENOMINATOR**depth) + for depth, active, _ in rows), Q(0)) + leaf = sum((Q(terminal, DENOMINATOR**depth) + for depth, _, terminal in rows), Q(0)) + return internal, leaf + + +def check_envelope(width, mass, a): + lower_base = (Q(width) + SHIFT) / (THRESHOLD - 1 + SHIFT) + upper_base = Q(width, THRESHOLD // DIMENSION) + # Use the harder endpoints: these imply the claimed bounds for the root s. + lower_power = power_interval(lower_base, EXPONENT_HI)[1] + upper_power = power_interval(upper_base, EXPONENT_LO)[0] + need(a * (lower_power - 1) <= mass <= a * (upper_power - 1), + "two-sided finite envelope") + + +def rejection_controls(counts, tolls): + rejected = [] + for name, lo, hi in ( + ("root bracket above the root", Q(999, 1000), Q(9991, 10000)), + ("root bracket below the root", Q(997, 1000), Q(998, 1000)), + ("reversed bracket", EXPONENT_HI, EXPONENT_LO), + ): + try: + exponent_certificate(counts, lo, hi) + except ValueError: + rejected.append(name) + else: + raise ValueError("mutant bracket accepted") + # Each alternative makes a mathematically different, incorrect prediction. + alternatives = { + "cutoff repeated after remainder": tolls[DIMENSION * (356 // DIMENSION)], + "threshold equality called terminal": Q(0), + "fresh-row divisor omitted after cover cancellation": Q(1 + dict(counts)[48]), + "round width upward": tolls[584], + } + expected = {name: tolls[356] for name in alternatives} + expected["fresh-row divisor omitted after cover cancellation"] = tolls[584] + expected["round width upward"] = tolls[583] + for name, result in alternatives.items(): + need(result != expected[name], "incorrect recurrence not distinguished") + rejected.append(name) + too_small = SHIFT - Q(1, 25) + need(48 * 72 > too_small * 25, "smaller uniform shift is invalid") + rejected.append("shift below sharp residue allowance") + return rejected + + +def main(): + counts = load_premises() + total = sum(n for _, n in counts) + c = Q(total, DENOMINATOR) + a = 1 / (c - 1) + need(c > 1 and sum(Q(n*r, DENOMINATOR*DIMENSION) for r, n in counts) < 1, + "unique critical root between zero and one") + signs = exponent_certificate(counts, EXPONENT_LO, EXPONENT_HI) + shifts = [Q(r*delta, DIMENSION-r) for r, _ in counts for delta in range(73)] + need(max(shifts) == SHIFT, "sharp affine floor allowance") + tolls, leaves = bottom_up(counts) + for width in range(DP_LIMIT + 1): + need(leaves[width] == 1 + (c-1) * tolls[width], "weighted leaf identity") + need(tolls[355] == 0 and tolls[356] == tolls[583] == 1, "strict cutoff") + need(tolls[584] == Q(9601, 7168), "first extra generation value") + samples = (356, 360, 583, 584, 948, 949, 3284, 3285, 8192, 65536, TREE_LIMIT) + rows = [] + for width in samples: + census = level_census(counts, width) + mass, leaf = census_masses(census) + need(leaf == 1 + (c-1)*mass, "independent census leaf identity") + if width <= DP_LIMIT: + need(mass == tolls[width], "integer path census matches rational DP") + check_envelope(width, mass, a) + rows.append({"width": width, "mass": str(mass), "depth_rows": census}) + controls = rejection_controls(counts, tolls) + receipt = { + "status": "PASS_QQ16_PARKING_POWER_LAW", + "claim_type": "scoped proof with exact finite corroboration", + "exponent_open_interval": [str(EXPONENT_LO), str(EXPONENT_HI)], + "moment_sign_intervals": [[str(x) for x in pair] for pair in signs], + "C": str(c), "a": str(a), "shift": str(SHIFT), + "DP_widths": DP_LIMIT + 1, "path_censuses": rows, "controls": controls, + "source_sha256": {name: sha256(read_bounded(HERE / name, 2**20)).hexdigest() + for name in ("README.md", "SOURCES.json", "TASK.json", + "VERIFY.json", "verify.py")}, + "full_cost_sign": "unresolved", "new_kappa": False, + } + print(json.dumps(receipt, sort_keys=True, indent=2)) + + +if __name__ == "__main__": + main()