From 50a0edd82520770b6eefc76e32163746fc6330cb Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Tue, 27 Oct 2026 10:13:37 +0000 Subject: [PATCH] feat(research): tighten joint interval amplification bounds --- .../PROOF.md | 132 +++++++++++ .../README.md | 110 +++++++++ .../SOURCES.json | 42 ++++ .../TASK.json | 101 ++++++++ .../VERIFY.json | 36 +++ .../verify.py | 218 ++++++++++++++++++ 6 files changed, 639 insertions(+) create mode 100644 research/protected-boundary-interval-bound/PROOF.md create mode 100644 research/protected-boundary-interval-bound/README.md create mode 100644 research/protected-boundary-interval-bound/SOURCES.json create mode 100644 research/protected-boundary-interval-bound/TASK.json create mode 100644 research/protected-boundary-interval-bound/VERIFY.json create mode 100644 research/protected-boundary-interval-bound/verify.py diff --git a/research/protected-boundary-interval-bound/PROOF.md b/research/protected-boundary-interval-bound/PROOF.md new file mode 100644 index 0000000000..e479ec1418 --- /dev/null +++ b/research/protected-boundary-interval-bound/PROOF.md @@ -0,0 +1,132 @@ +# A smaller joint interval envelope from protected boundaries + +This contribution was produced by Nick Petalas. Apache-2.0. + +Claim type: scoped written proof. The proof uses the cited prefix-entry and +squarefree-interval lemmas as premises. It does not audit those predecessors. + +## Contract and theorem + +Use Chafik Boukhalfa's PR628 balanced dirty word on n>=1 factors, a protected +source x, an unread target y and h=ceil(log2 n) arbitrary dirty scratch registers. +The scratch register for each depth is reused by sibling calls. All cuts are +complete ideal-leaf boundaries. Let P_t be any prefix of either word orientation. +The full state has the maximum of the individual register norms. + +Put + +```text +K(0)=2, +K(h)=h^2+2h+3 for h>=1. +``` + +For every ordered pair of cuts s,t, the free noncommutative coefficient +absolute row sum of P_t P_s^-1 is at most K(h). Consequently: + +1. For arbitrary contractive operator factors, without commutation, + ||P_t P_s^-1|| <= K(h). +2. If the factors commute and every subset product, including the empty one, + has norm at most G>=1, then ||P_t P_s^-1|| <= K(h) G. + +For h>=1 the coefficient envelope improves the squared-prefix bound by +exactly (h+2)^2-K(h)=2h+1. It is not claimed sharp. Arham Tahir's PR1374 +lower bound floor(h^2/2)+h+2 remains compatible with it. This does not change +the exact destination-only result of philippeVV's PR2177. + +## Predecessor inputs + +Hanson Sun's PR1085 proves that every entry of P_t and P_s^-1 is zero or +one signed monomial, and that the source row and target column are identity. +Its retained text is at +`research/single-register-interval-transport/vendor/PR1085-PROOF.md`. +We consume those assertions without replaying or re-proving them. + +Charles Bethin's PR1278 proves that every surviving interval monomial uses +each factor at most once, including both cut orders, both orientations and +shared deeper scratch. This is needed only for conclusion 2. Its retained +text is `research/commuting-interval-audit/PROOF.md`. + +## New block inequality + +Order registers as source, the h scratch registers, target. The protected +source and unread target force the following shape for P=P_t and Q=P_s^-1: + +```text +P = [ 1 0 0 ] Q = [ 1 0 0 ] + [ a B 0 ] [ c D 0 ] + [ b e 1 ] [ d f 1 ]. + +P Q = [ 1 0 0 ] + [ a+B c B D 0 ] + [ b+e c+d e D+f 1 ]. +``` + +Here a,c are h-by-1, B,D are h-by-h, e,f are 1-by-h, and b,d are scalars +in the free algebra. Every displayed entry of P and Q has coefficient mass +at most one. Coefficient mass is subadditive and submultiplicative because +concatenation multiplies words and cancellation can only reduce mass. + +A scratch row of Q has at most h+1 occupied entries, since its target entry +vanishes. Its source row has mass one. Therefore any scratch row of P Q has +mass at most + +```text +1 + h(h+1) = h^2+h+1. +``` + +The target row of Q has mass at most h+2. The target row of P Q is the sum +of b times Q's source row, h terms e_j times Q's scratch rows, and Q's target +row. Its mass is at most + +```text +1 + h(h+1) + (h+2) = h^2+2h+3. +``` + +The protected source row still has mass one. Taking the largest row gives +the theorem for h>=1. This argument uses both boundary restrictions; it +does not multiply the global row bound h+2 by itself. It does not assume +fresh scratch, commuting coefficients, or an ordering of s and t. + +When h=0, n=1 and there is one leaf. Every interval is identity or that +leaf shear in either sign. Its coefficient row sum is at most two, proving +the separate K(0)=2 case. + +For conclusion 1, every formal word evaluates to an operator of norm at +most one, by submultiplicativity of the contractive factor norms. Summing +the row coefficient masses gives K(h). For conclusion 2, use PR1278's +squarefree conclusion before substitution. Commutation turns each surviving +word into a subset product with norm at most G. The same coefficient bound +gives K(h)G. Individual factor bounds by G alone would not justify this step. + +## What the computation checks + +The verifier multiplies generic protected-boundary matrices with independent +formal entries. It obtains the exact abstract row counts above for h=1..8. +These matrices are not asserted to be prefixes of a common word, so equality +in that calculation is not a sharpness claim for actual dirty intervals. +The strict-gain identity is checked with exact integers at h=1..10000. + +A separately written iterative emitter expands the balanced word for six +factor counts, with both signs and the same physical scratch at each depth. +It propagates every nonempty interval directly over the free noncommutative +algebra and checks the new inequality. It also checks the full arbitrary-dirty +endpoint and literal inverse order. It imports no predecessor implementation. +No predecessor extremal census or scalar sign witness is a deliverable here. + +Abstract controls remove each protected boundary or the entry-size premise +and require failure of the new bound. Invalid argument controls check the +finite executable capacities. These are not claimed to be realizable dirty +word counterexamples. A separate check keeps the bound labelled nonsharp. + +## Limits and next implication + +The all-size statement rests on the written block proof and the cited +lemmas. Computation only corroborates its fixed finite fixtures. No formal +proof-kernel or independent human review is claimed. Internal rounded leaf +operations, nonlinear errors, negative-leaf preimages, preparation, physical +movement, stock, precision and a complete caller invoice are not supplied. +The five selected framework assumptions remain. No new kappa follows. + +The original sharp-constant question remains open between the cited lower +family and this smaller upper bound. A further improvement must exploit +relations between the two actual prefixes, beyond these protected boundaries. diff --git a/research/protected-boundary-interval-bound/README.md b/research/protected-boundary-interval-bound/README.md new file mode 100644 index 0000000000..755591e2da --- /dev/null +++ b/research/protected-boundary-interval-bound/README.md @@ -0,0 +1,110 @@ +# A smaller joint interval bound from protected boundaries + +This contribution was produced by Nick Petalas. Apache-2.0. + +Claim type: scoped written proof with exact finite corroboration. No new kappa. + +For the unchanged balanced PR628 dirty word, put h=ceil(log2 n). The protected +source and unread target improve the general joint-error coefficient envelope: + +```text +previous: (h+2)^2 +new: h^2+2h+3, for h>=1 +gain: 2h+1 +``` + +The one-factor case has the separate bound two. Every ordered pair of complete +leaf cuts and both word orientations are covered, with the same dirty scratch +register reused at each depth. For arbitrary contractive factors the new norm +bound is h^2+2h+3, without commutation. For commuting factors whose every subset +product has norm at most G, it is (h^2+2h+3)G. + +For example, height four improves the upper bound from 36 to 27. This is an +upper-bound improvement, not a sharpness theorem. Arham Tahir's #1374 gives the +compatible lower family floor(h^2/2)+h+2 and explicitly leaves the sharp upper +constant open. [PROOF.md](PROOF.md) supplies the new block inequality. The +prefix-entry invariant and squarefree-interval theorem are cited dependencies, +not verification deliverables. No predecessor executable is imported or run. + +## Evidence and reproduction + +The standalone verifier checks eight generic formal block products and 10,000 +strict-gain identities. Its own iterative word emitter checks 23,736 nonempty +free noncommutative intervals at n=1,2,3,5,8,11 in both directions, full arbitrary +dirty endpoints and literal inverse order. Fourteen controls cover invalid +arguments, removed source/target restrictions, an oversized entry and the +distinction between an upper bound and a sharp value. A generated receipt on +stdout binds all six package files by SHA256; no receipt is hand-written. + +From the repository root with the Python 3.12 standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B -W error -X dev research/protected-boundary-interval-bound/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B -W error -X dev -O research/protected-boundary-interval-bound/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/protected-boundary-interval-bound +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/protected-boundary-interval-bound --check-source-history +``` + +Any CPython 3.12 installation can replace the local interpreter path. Expected +markers are `PASS_PROTECTED_BOUNDARY_INTERVAL_BOUND`, +`PASS_REGISTERED_RESEARCH_PACKAGE` and `PASS_RESEARCH_COMMIT_BYTES`. +The last command requires the publication commit and full source history. +Both registered commands have 120-second timeouts. Direct verification also +works in a Git-free export containing these six files. + +## Scope and implementation limits + +The all-size theorem rests on the written block proof and cited lemmas. +The finite verifier does not prove those premises. Its generic matrices have +independent formal entries and need not be prefixes of a common word; their +exact row counts do not prove sharpness for actual words. + +The finite emitter accepts at most sixteen factors and height four. Generic +matrix checks use at most ten rows. Polynomial operations enforce at most +64 terms and word length 32. All loops have finite fixture or capacity bounds, +the emitter uses a bounded explicit stack, and no function exceeds sixty lines. +Python allocation is a managed-runtime deviation from fixed allocation; the +matrix and polynomial capacities bound live objects. The only indirect calls +are three fixed invalid-argument control variants. There is no recursion, +subprocess, network access, solver, dynamic code generation or external +dependency in the verifier. Diagnostics use warning-strict normal and optimized +execution. + +Rounded-leaf execution, negative-leaf preimages, internal magnitude and +coefficient preparation, precision/tape integration, native realization, stock, +ownership and a complete supplier invoice remain unrun or unproved here. +The selected result and its five framework assumptions are unchanged. +Independent human and formal proof-kernel review are unclaimed. + +## Open next questions + +- Is floor(h^2/2)+h+2 the sharp universal joint interval envelope? Use actual + chronological relations between the two prefixes in the six phase-pair + formulas. Cancellation and shared scratch across unequal child sizes are + the remaining obstacles. +- Can one exact rounded caller use the smaller envelope in a complete + sufficient-precision and physical-cost substitution? First retain its + destination support, negative-leaf preimages, preparation and internal + magnitudes. No such caller or complete invoice is supplied here. + +These questions and their first steps are also recorded in [TASK.json](TASK.json). +The scope is frozen after this first local improvement. + +## Credit and provenance + +Chafik Boukhalfa supplies the PR628/905 word and retained lineage. Hanson Sun +supplies PR1085's prefix-entry invariant. Charles Bethin supplies PR1278's +squarefree-interval theorem and PR1416's distinction between a column and a +joint-state bound. Arham Tahir supplies PR1374's quadratic lower family and +explicit open upper-bound question. Philippe Van Velzen's PR2177 settles the +different completed-leaf destination problem. Philipp/mightyOil, Gareth +Davidson and 0xkilgore retain the precision, perturbation and restoration +lineage credited in those sources. + +[SOURCES.json](SOURCES.json) pins exact main-tree proof and context blobs at +`de5ec2e7a6074068452f45b1a191b5c72832df4a`. They are historical proof premises, +not runtime imports. The current `uniform-transfer-audit` card is explicitly +changed to this original algebraic side result. Current selected-metadata +orientation passed; no selected scientific replay is claimed. + +[Advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19214460). diff --git a/research/protected-boundary-interval-bound/SOURCES.json b/research/protected-boundary-interval-bound/SOURCES.json new file mode 100644 index 0000000000..4787faa2ca --- /dev/null +++ b/research/protected-boundary-interval-bound/SOURCES.json @@ -0,0 +1,42 @@ +{ + "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" + }, + { + "path": "research/single-register-interval-transport/vendor/PR1085-PROOF.md", + "usage": "provenance", + "git_blob": "b794f4253b30f9af1d29c875097d04349715582b", + "sha256": "b21febd8202b433f3f7c046e2c62e29c5772c8bee79327c51729d500c024a8b2" + }, + { + "path": "research/commuting-interval-audit/PROOF.md", + "usage": "provenance", + "git_blob": "de9c8fca358c225e2ef30180c553717208015252", + "sha256": "17d346b53eb71780410e1ec5e87d56bc444215a540e98c84283f12553c0c81e9" + }, + { + "path": "research/dirty-interval-coefficient-boundary/README.md", + "usage": "provenance", + "git_blob": "59cb826f1378d1311fa1994c872e3bf20703f669", + "sha256": "41c69924abe9881d4b68549879dd248adccfd379899281ad6b9289b814429604" + }, + { + "path": "research/leaf-destination-transport-bound/README.md", + "usage": "provenance", + "git_blob": "b8d857e408f4e0bbdff33d33a134a6d8e8f4649c", + "sha256": "01a2c4d599fd6e071c613026627fdf980b45f9cfaadb9cbb0c96d9ab5591ebd9" + } + ] +} diff --git a/research/protected-boundary-interval-bound/TASK.json b/research/protected-boundary-interval-bound/TASK.json new file mode 100644 index 0000000000..0d574fb0d9 --- /dev/null +++ b/research/protected-boundary-interval-bound/TASK.json @@ -0,0 +1,101 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 8, + "base_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a", + "original_card": { + "id": "uniform-transfer-audit", + "question": "Can one of the selected record's five inherited assumptions be proved at its actual caller?", + "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": "Identify the proposition and what would change downstream; do not equate a finite replay with a universal proof.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_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 one assumption ID (native_all_columns, owned_erasure, compiler, precision_tape, analytic_recovery), one quantified implication and exact dependency closure. Check current handoffs, including #5625 row reentry and #5707 root-prefix lowering, without treating their partial scope as the whole theorem. Prove or falsify that implication with a caller-bound argument; stop at the chosen obligation. Finite tests or root digits do not discharge an all-size statement.", + "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": [ + "native_all_columns", + "owned_erasure", + "compiler", + "precision_tape", + "analytic_recovery" + ], + "existing_checks": [ + { + "scope": "PR #4100: proposed unconditional construction and finite checks, without independent acceptance.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Independent proof audit of one caller-bound all-size implication; all other premises remain explicit.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "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": "Original protected-boundary block inequality improving the PR628 joint interval coefficient envelope from (h+2)^2 to h^2+2h+3 for every h>=1, with the separate h=0 bound two.", + "scope_change_reason": "The assignment requests original mathematics rather than an audit. This is a scoped precision-interface side result taking Open next question 2 of Arham Tahir PR1374. It does not discharge a selected framework assumption.", + "bottleneck_link": "A smaller all-size joint error-transport constant can reduce a sufficient precision allowance when a rounded caller satisfies the exact word contract. A complete precision and physical cost substitution remains separate.", + "budget_minutes": 60, + "stop_rule": "Freeze at the first verified uniform upper-bound improvement; leave sharpness and rounded caller integration open.", + "outcome": "completed", + "evidence": "PROOF.md; verify.py checks generic formal block products, strict-gain identities, 23736 exact nonempty intervals and 14 controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Is floor(h^2/2)+h+2 the sharp universal joint interval coefficient envelope?", + "why_it_matters": "The cited lower family and this improved upper bound still differ in the leading quadratic coefficient.", + "first_step": "Use the actual chronological relation between the two prefixes, beyond the protected boundary pattern, in the six phase-pair formulas.", + "blocked_by": "Cancellation and scratch reuse across unequal child sizes are not controlled sharply by the block count." + }, + { + "question": "Can a rounded caller use the new interval envelope to lower its complete sufficient precision?", + "why_it_matters": "A norm lemma alone does not reduce a paid physical bill.", + "first_step": "Choose an exact caller with this balanced word and retain destination support, negative-leaf preimages, coefficient preparation and all internal magnitude charges.", + "blocked_by": "No actual rounded caller, complete invoice or physical implementation is supplied here." + } + ], + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19214460", + "environment": { + "interpreter": "CPython 3.12.15", + "platform": "macOS arm64", + "dependencies": "Python standard library only" + }, + "expansion_decision": "Stop after the local norm improvement. No supplier construction campaign is expanded; rounded delivery and physical costs remain unknown.", + "overlap": { + "canonical_main": "de5ec2e7a6074068452f45b1a191b5c72832df4a", + "priority_revision": 8, + "scope": "Live open/account PRs and handoffs; cached complete PR/discussion pagination; distinctive all-main README and merged searches. Sparse local notes and code diffs are incomplete. PR2177 settled the discarded destination-only candidate." + } +} diff --git a/research/protected-boundary-interval-bound/VERIFY.json b/research/protected-boundary-interval-bound/VERIFY.json new file mode 100644 index 0000000000..7d9e32ae46 --- /dev/null +++ b/research/protected-boundary-interval-bound/VERIFY.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "-W", + "error", + "-X", + "dev", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact generic block counts, strict gain, full formal dirty endpoints, both literal inverse orders, all intervals of six fixed words, boundary and capacity controls; generated six-file SHA256 receipt." + }, + { + "argv": [ + "{python}", + "-B", + "-W", + "error", + "-X", + "dev", + "-O", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact generic block counts, strict gain, full formal dirty endpoints, both literal inverse orders, all intervals of six fixed words, boundary and capacity controls; generated six-file SHA256 receipt." + } + ] +} diff --git a/research/protected-boundary-interval-bound/verify.py b/research/protected-boundary-interval-bound/verify.py new file mode 100644 index 0000000000..45862c8d1c --- /dev/null +++ b/research/protected-boundary-interval-bound/verify.py @@ -0,0 +1,218 @@ +#!/usr/bin/env python3 +"""Exact checks of the protected-boundary interval inequality. Apache-2.0.""" + +import hashlib +import json +from pathlib import Path + + +MAX_FACTORS = 16 +MAX_HEIGHT = 4 +MAX_TERMS = 64 +MAX_WORD = 32 +FILES = ("README.md", "PROOF.md", "TASK.json", "SOURCES.json", "VERIFY.json", "verify.py") + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def envelope(height): + require(type(height) is int and 0 <= height <= 10000, "invalid height") + return 2 if height == 0 else height * height + 2 * height + 3 + + +def identity(size): + require(type(size) is int and 1 <= size <= 12, "invalid matrix size") + return [[{(): 1} if i == j else {} for j in range(size)] for i in range(size)] + + +def add(left, right, sign=1): + result = dict(left) + for word, coefficient in right.items(): + value = result.get(word, 0) + sign * coefficient + if value: + result[word] = value + else: + result.pop(word, None) + require(len(result) <= MAX_TERMS, "polynomial capacity") + require(all(len(word) <= MAX_WORD for word in result), "word capacity") + return result + + +def multiply(left, right): + result = {} + for first, a in left.items(): + for second, b in right.items(): + word = first + second + result[word] = result.get(word, 0) + a * b + require(len(result) <= MAX_TERMS, "product capacity") + require(all(len(word) <= MAX_WORD for word in result), "word capacity") + return {word: coefficient for word, coefficient in result.items() if coefficient} + + +def product(left, right): + size = len(left) + require(len(right) == size, "matrix size mismatch") + result = [[{} for _ in range(size)] for _ in range(size)] + for i in range(size): + for j in range(size): + for k in range(size): + result[i][j] = add(result[i][j], multiply(left[i][k], right[k][j])) + return result + + +def row_mass(row): + return sum(abs(value) for entry in row for value in entry.values()) + + +def matrix_mass(matrix): + return max(row_mass(row) for row in matrix) + + +def generic_template(height, label): + """Independent formal entries, with source first and target last.""" + size = height + 2 + result = identity(size) + for i in range(1, size): + for j in range(size - 1): + result[i][j] = {((label, i, j),): 1} + return result + + +def check_block_counts(): + cases = 0 + for height in range(1, 9): + left = generic_template(height, "p") + right = generic_template(height, "q") + combined = product(left, right) + require(row_mass(combined[0]) == 1, "protected source count") + require(row_mass(combined[-1]) == envelope(height), "target block count") + for row in combined[1:-1]: + require(row_mass(row) == height * height + height + 1, "scratch block count") + cases += 1 + for height in range(1, 10001): + require((height + 2) ** 2 - envelope(height) == 2 * height + 1, "strict gain") + return cases + + +def leaf_word(factors, sign): + require(type(factors) is int and 1 <= factors <= MAX_FACTORS, "invalid factor count") + require(type(sign) is int and sign in (-1, 1), "invalid sign") + height = (factors - 1).bit_length() + require(height <= MAX_HEIGHT, "height capacity") + stack = [(0, factors, 0, 1, 0, sign)] + result = [] + for _ in range((4 ** (height + 1) - 1) // 3): + if not stack: + break + start, count, source, target, depth, direction = stack.pop() + if count == 1: + result.append((start, source, target, direction)) + continue + left = count // 2 + connector = depth + 2 + u = (start, left, source, connector, depth + 1) + v = (start + left, count - left, connector, target, depth + 1) + children = (u + (1,), v + (1,), u + (-1,), v + (-1,)) + if direction == -1: + children = (v + (1,), u + (1,), v + (-1,), u + (-1,)) + stack.extend(reversed(children)) + require(not stack, "node budget exhausted") + q = 1 << (factors.bit_length() - 1) + require(len(result) == 3 * q * factors - 2 * q * q, "word extent") + return result, height + 2 + + +def apply_leaf(matrix, event): + factor, source, target, sign = event + require(source != target, "aliased leaf") + row = [] + for entry in matrix[source]: + row.append({(factor,) + word: value for word, value in entry.items()}) + matrix[target] = [add(old, new, sign) for old, new in zip(matrix[target], row, strict=True)] + + +def check_word(factors, sign): + events, size = leaf_word(factors, sign) + height = size - 2 + intervals = 0 + for start in range(len(events)): + matrix = identity(size) + for end in range(start, len(events)): + apply_leaf(matrix, events[end]) + require(matrix_mass(matrix) <= envelope(height), "new interval envelope") + require(matrix[0] == identity(size)[0], "source changed") + require(all(matrix[i][1] == ({(): 1} if i == 1 else {}) + for i in range(size)), "target was read") + intervals += 1 + complete = identity(size) + for event in events: + apply_leaf(complete, event) + expected = identity(size) + expected[1][0] = {tuple(range(factors - 1, -1, -1)): sign} + require(complete == expected, "full arbitrary-dirty endpoint") + return intervals + + +def must_reject(function, argument): + try: + function(argument) + except ValueError: + return + raise ValueError("invalid argument accepted") + + +def check_controls(): + controls = 0 + for value in (True, -1, 10001, 1.0): + must_reject(envelope, value) + controls += 1 + for value in (True, 0, 17): + must_reject(lambda count: leaf_word(count, 1), value) + controls += 1 + for value in (True, 0, 2): + must_reject(lambda sign: leaf_word(2, sign), value) + controls += 1 + # These abstract controls deliberately remove one premise at a time. + size = 3 + dense = [[{(("d", i, j),): 1} for j in range(size)] for i in range(size)] + source_only = [[dict(entry) for entry in row] for row in dense] + source_only[0] = identity(size)[0] + target_only = [[dict(entry) for entry in row] for row in dense] + for i in range(size): + target_only[i][-1] = {(): 1} if i == size - 1 else {} + require(matrix_mass(product(source_only, source_only)) > envelope(1), "unread-target control") + require(matrix_mass(product(target_only, target_only)) > envelope(1), "protected-source control") + scaled = generic_template(1, "s") + scaled[-1][0] = {(("s", 2, 0),): 10} + require(matrix_mass(product(scaled, scaled)) > envelope(1), "entry-size control") + controls += 3 + require(envelope(1) > 3, "must not label the upper envelope sharp") + controls += 1 + return controls + + +def main(): + block_cases = check_block_counts() + controls = check_controls() + intervals = 0 + fixtures = (1, 2, 3, 5, 8, 11) + for factors in fixtures: + positive, _ = leaf_word(factors, 1) + negative, _ = leaf_word(factors, -1) + require(negative == [(a, b, c, -d) for a, b, c, d in reversed(positive)], "literal inverse") + for sign in (-1, 1): + intervals += check_word(factors, sign) + package = Path(__file__).resolve().parent + hashes = {name: hashlib.sha256((package / name).read_bytes()).hexdigest() for name in FILES} + receipt = {"status": "PASS_PROTECTED_BOUNDARY_INTERVAL_BOUND", "claim_type": "scoped proof", + "generic_block_cases": block_cases, "strict_gain_heights": 10000, + "word_factor_counts": list(fixtures), "word_orientations": 12, + "nonempty_intervals": intervals, "controls": controls, "sha256": hashes} + print(json.dumps(receipt, sort_keys=True, indent=2)) + + +if __name__ == "__main__": + main()