diff --git a/research/boolean-directed-cycle-tariff/README.md b/research/boolean-directed-cycle-tariff/README.md new file mode 100644 index 0000000000..cd87a4441c --- /dev/null +++ b/research/boolean-directed-cycle-tariff/README.md @@ -0,0 +1,221 @@ +# Exact Boolean triple tariff on a directed cycle + +This contribution was produced by Nick Petalas. Apache-2.0. + +**Claim type: scoped written proof with exact finite corroboration.** +For the Boolean demand `(110,101,011)`, the exact complete abstract tariff is + +```text +OPT = min(mu_0, mu_1, mu_2) + 8c +``` + +when the three ADD edges `0 -> 1 -> 2 -> 0` cost `c>0`, every source +insertion price `mu_i` is at least `8c`, and every reverse ADD edge price +is at least `8c`. Coefficients do not affect prices. The cone need not be +maximal. With insertion and reverse-edge prices 100 and cycle-edge price 1, +the optimum is **108**, attained by one insertion and eight cycle ADDs. +Three direct insertions cost 300. + +This answers one price family of Open next question 1 in lee-phys's +[PR5304](https://github.com/CrocSwap/integer-mult-bounds/pull/5304). +That predecessor proves destination-row tariffs and leaves independently +directed prices open. The new step is the exact cycle column distance, +its conversion to a dirty-restored lower bound, and the attaining word. +It is a local arithmetic result. No new kappa or physical supplier is claimed. + +## Contract + +Let `R=F2^3`, represented by masks 0 through 7 with XOR addition, AND +multiplication and identity 7. Three arbitrary independent dirty rows +`A_0,A_1,A_2 in R^w`, `w>=1`, and a disjoint preserved source `p in R^w` +are available. A fixed finite word must implement + +```text +A_i <- a_i + lambda_i p, lambda=(3,5,6). +P_i(beta): A_i <- A_i + beta p, price mu_i +E_ij(alpha): A_i <- A_i + alpha A_j, price c_ij, i != j. +``` + +Every coefficient is allowed; zero gates can be deleted. All original dirt +columns must return exactly. There are no extra rows, CLEARs, observations, +free basis changes or adaptive choices. Prices are positive, stationary, +coefficient-independent abstract complete gate prices. An application must +supply such prices including its required access, routing and restoration. +Separate inverse execution must be paid separately. + +The three cycle edges have equal price `c`. The other three edge prices +may differ. Put `m=min_i mu_i`. The theorem assumes `m>=8c` and +`min_reverse c_ij>=8c`. + +## Four ADDs are necessary and sufficient to split one inserted column + +Consider an ADD-only word C taking `7 e_i` to lambda. First let `i=0`. +Every destination must change: rows 1 and 2 start zero but have nonzero +targets, and row 0 starts 7 but must end at 3. With at most three cycle ADDs, +each destination must therefore receive exactly one gate. To change row 2, +its only parent row 1 must first have changed. To change row 0, its only +parent row 2 must first have changed. The only possible order is + +```text +E_10(alpha), E_21(beta), E_02(gamma). +``` + +Row 1 is then already at its final value 5 when row 2 changes. Consequently +row 2's final value is `beta AND 5`, which cannot equal 6. This excludes +every word with at most three cycle ADDs, including arbitrary coefficients. +For the other roots, cyclic row relabeling gives the same argument: each +required target is incomparable with its parent's mask under support +inclusion. Thus the column distance is at least four for every root. + +Here is an attaining suffix for any root i. Put `j=i+1 mod 3`, +`k=i+2 mod 3`, and `h_i=7 XOR lambda_i`. Execute + +```text +C_i = E_ji(lambda_k), E_kj(7), E_ji(lambda_i), E_ik(h_i). +``` + +The source column changes through + +```text +7 e_i -> (7, lambda_k, 0) -> (7, lambda_k, lambda_k) + -> (7, lambda_j, lambda_k) -> (lambda_i, lambda_j, lambda_k), +``` + +where the entries are ordered as i,j,k. The final step uses +`h_i AND lambda_k=h_i`; all displayed coefficients are nonzero. Hence the +distance is exactly four. The written argument applies to every finite +ADD-only word; no search cutoff is used in the theorem. + +## Restoration doubles the column distance + +Suppose a correct word has exactly one insertion `P_i(beta)`. Write M +for the dirt matrix of its ADD-only prefix and L for that of its suffix. +Every ADD is invertible, and restoration forces `LM=I`, so `L=M^-1`. +The source column is `L(beta e_i)=lambda`. + +Every one of the three bit coordinates occurs in lambda. If the +corresponding bit of beta were zero, that whole coordinate of the source +column would remain zero under L. Thus beta must be 7. + +The suffix is therefore an ADD word taking `7 e_i` to lambda. Reversing +the prefix gives another word for L, because every Boolean ADD is its own +inverse. If only cycle edges are used, each of these two words has at +least four ADDs. Any one-insertion cycle word needs at least eight ADDs. + +The chronological word `C_i^-1, P_i(7), C_i` attains this lower bound and +returns every dirt column. For root zero it is + +```text +E_02(4), E_10(3), E_21(7), E_10(6), P_0(7), +E_10(6), E_21(7), E_10(3), E_02(4). +``` + +For example the suffix sends its source column through +`(7,0,0),(7,6,0),(7,6,6),(7,5,6),(3,5,6)`. +The first four gates prepare dirt, and the last four restore it while +delivering the inserted source. Omitting that preparation is invalid. + +## Complete tariff lower bound + +A correct word needs at least one insertion. The following cases exhaust +all finite words under the stated prices. + +- At least two insertions cost at least `2m>=m+8c`. +- A reverse ADD and at least one insertion cost at least `m+8c`. +- Exactly one insertion and only cycle ADDs cost at least `m+8c`, by the + preceding restoration argument. + +Choose a minimum-price insertion root and use its nine-gate word. Its cost +is exactly `m+8c`, proving the theorem, including the boundary equalities. +This settles the complete program optimum within the displayed cone, +rather than only the one-insertion branch. All-width correctness follows +coordinatewise from the same ring-linear identity. + +## Exact verification + +Use CPython 3.12 and the standard library, from the repository root: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/boolean-directed-cycle-tariff/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/boolean-directed-cycle-tariff +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/boolean-directed-cycle-tariff --check-source-history +``` + +Another CPython 3.12 path may replace the local interpreter path. Normal +and optimized warning-strict direct commands are registered in VERIFY.json. +Each writes only stdout, including a generated receipt bound to all five +package file hashes. The expected scientific status is +`PASS_BOOLEAN_DIRECTED_CYCLE_TARIFF`. + +The packed source-column graph has exactly `7^3=343` vertices. In each +bit coordinate the nonzero three-entry column stays nonzero under invertible +ADDs. The verifier visits every state for each root, checks every directed +distance inequality and finds target distance four. Its layer sizes are +`1,7,19,74,176,66`. A separately arranged bit-coordinate implementation +enumerates all columns reachable through length three and excludes the +target. These two programs use different state orientations. + +A separate literal bit-list interpreter checks all 4,096 assignments of +the three dirty scalars and source for each root, both forward and inverse: +12,288 input cases in total. Formal basis-column checks establish each +linear endpoint. Twelve exact rational price fixtures include nonuniform +insertion prices and cone boundaries. Twenty-five controls reject nine +deleted gates, nine changed nonzero coefficients, three omitted-preparation +words and four invalid price/arity boundaries. Counts are enumerated by +the verifier. No predecessor executable or reported numerical census is +used as an oracle. + +## Scope and resources + +Independent human and formal proof-kernel review are unclaimed. The proof +covers the specified Boolean triple, three rows and the displayed price cone. +It does not settle arbitrary directed tariffs, extra workspace, non-Boolean +rings, native operators, precision/tape costs, stock, supplier admission or +a complete multiplication theorem. The selected frontier is unchanged. + +The current selected-record positive control passed. That command checks +metadata bindings and is not scientific evidence for this local theorem. + +The verifier has no recursion, subprocesses or runtime source imports. +All search loops have fixed finite domains: three roots, 343 column states, +21 cycle gates, three short-word layers, and 4,096 scalar assignments per +root. Short-word frontiers have at most 343 entries. Literal states have +four rows of three bits and words have at most nine gates. Functions stay +under 60 lines. Guards raise exceptions under normal and optimized Python. +Power of Ten rule 3 deviation: CPython collections, fractions and hashing +allocate dynamically; the finite domains and five 128 KiB file limits bound +the owned input and state. Standard-library dispatch is fixed by the code. +Warning-strict execution and AST compilation are the available diagnostics; +no repository-wide configuration change is introduced. + +## Open next questions + +What is the exact tariff outside this cone, with all six ADD prices +independent? The 343-state graph solves the single-insertion column problem, +but multiple insertions need a dirt-aware lower bound. Start by deriving +that bound before extending the tariff search. The present proof gives +no physical gate prices or complete supplier invoice for such an expansion. + +## Credit and coordination + +lee-phys's PR5304 supplies the Boolean triple, arbitrary-dirty restoration +contract, destination-price comparison and explicit directed-price question. +Credit lee-phys PR5259, Ali Romman Discussion5266/5300, Krzysztof Wojt +PR5045, Ross Richardson PR3063/3121, Nick Petalas PR4916/5208, and the +earlier fanout lineage retained there. Their results are credited premises, +not audit deliverables. No literature-priority claim is made for elementary +matrix conjugation or shortest-path search. + +The base is canonical main `7c49fe32c55de02c2c873655c804b16e4c3fef0a`, +priority revision 8. SOURCES.json retains the card, selected-record and +PR5304 README provenance at that ancestor. These are provenance records, +not executable dependencies. The proof and verifier are self-contained. +The changed `bit-helper-contract` scope concerns the cost of a local dirty +interface, rather than an audit or a changed G20 word. + +[Advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19377650). +Overlap checks covered live PRs and claims, the cached complete corpus and +distinctive main/merged searches. They do not certify novelty against +unpublished work or every historical diff. PR5933's Z/4 nonunit cycle and +PR5948's orthogonal Boolean demand are different instances; neither proves +this tariff. Their original credit and source packages remain unchanged. diff --git a/research/boolean-directed-cycle-tariff/SOURCES.json b/research/boolean-directed-cycle-tariff/SOURCES.json new file mode 100644 index 0000000000..79116ac952 --- /dev/null +++ b/research/boolean-directed-cycle-tariff/SOURCES.json @@ -0,0 +1,24 @@ +{ + "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/boolean-triple-fanout/README.md", + "usage": "provenance", + "git_blob": "efa6fe83c9081f2895fae16718c44f3c5dad7bde", + "sha256": "8ccfe785fe04f982ab6ee05ac23727f0905cf198d5113d46ca70f553c753fd75" + } + ] +} diff --git a/research/boolean-directed-cycle-tariff/TASK.json b/research/boolean-directed-cycle-tariff/TASK.json new file mode 100644 index 0000000000..7383bfb0bf --- /dev/null +++ b/research/boolean-directed-cycle-tariff/TASK.json @@ -0,0 +1,82 @@ +{ + "schema_version": 1, + "task_id": "bit-helper-contract", + "priority_revision": 8, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "original_card": { + "id": "bit-helper-contract", + "question": "Can a changed G20 helper path or independent-target split improve the complete BIT moment without losing its physical endpoint?", + "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", + "research/g20-helper-split/README.md", + "research/g20-conjugation-admission/README.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 full boundary contract and paid profile; unchanged scalar counts alone are insufficient. 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_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": "First read #5679/#5708 and their audits as pending component proposals. Choose one uncovered helper group/cut on an exact word; compare arbitrary-input native action, targets, owned storage, both orientations and full signed bill. Stop if the gain is only a scalar count or repaid by lost targets. Do not rerun the frozen #5609 common-frame domain without changing its hypothesis.", + "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": [ + "G20", + "helper split", + "5679", + "5708", + "independent target" + ], + "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": "Exact complete tariff for the Boolean demand (3,5,6) over F2^3 when three directed-cycle ADDs have common price c and every insertion and reverse ADD costs at least 8c.", + "scope_change_reason": "Refine the BIT helper boundary to the independently directed-price question explicitly left open in lee-phys PR5304. This is a local arithmetic side result, not a supplier audit or a source-word change.", + "bottleneck_link": "Dirty restoration and directed routing can consume sharing gains. An exact cycle tariff prices one source-preserving local boundary; physical use needs actual complete gate prices and a complete signed invoice.", + "budget_minutes": 60, + "stop_rule": "Stop at the first exact new cycle tariff and matching literal word; leave arbitrary directed prices to Open next questions.", + "outcome": "completed", + "evidence": "Written arbitrary-word lower bound and nine-gate attaining word. Complete 343-state source-column graph for each root; separate scalar-column search through three ADDs; 12,288 literal forward/inverse input cases; 12 rational price fixtures; 25 rejecting controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "What is the exact tariff outside the displayed price cone for the same Boolean triple with all six directed ADD prices independent?", + "why_it_matters": "Two insertions or a reverse edge can then compete, and source-column optimality alone no longer settles the full dirty-restored word.", + "first_step": "Use the 343-state column graph for the one-insertion branch, then derive a multi-insertion lower bound retaining all original dirt columns.", + "blocked_by": "No directed-edge all-word classification is supplied outside this cone." + } + ], + "coordination": { + "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19377650", + "question_source": "lee-phys PR5304, Open next question 1", + "overlap": "Live open PRs, latest handoff comments and active Discussions, cached complete overlap covering 613 open PRs and 6706 Discussion records, and main README/merged-PR searches were inspected. Historical diffs and unpublished work are not completely covered." + } +} diff --git a/research/boolean-directed-cycle-tariff/VERIFY.json b/research/boolean-directed-cycle-tariff/VERIFY.json new file mode 100644 index 0000000000..7d3d9a5cb6 --- /dev/null +++ b/research/boolean-directed-cycle-tariff/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Complete column distances, independent short-word exclusion, all scalar dirty inputs and inverses, exact price fixtures and semantic rejection controls; prints a generated file-hash receipt." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Complete column distances, independent short-word exclusion, all scalar dirty inputs and inverses, exact price fixtures and semantic rejection controls; prints a generated file-hash receipt." + } + ] +} diff --git a/research/boolean-directed-cycle-tariff/verify.py b/research/boolean-directed-cycle-tariff/verify.py new file mode 100644 index 0000000000..ba962ae170 --- /dev/null +++ b/research/boolean-directed-cycle-tariff/verify.py @@ -0,0 +1,198 @@ +#!/usr/bin/env python3 +"""Exact Boolean triple cycle tariff. Produced by Nick Petalas. Apache-2.0.""" + +from collections import Counter, deque +from fractions import Fraction +from hashlib import sha256 +from itertools import product +import json +from pathlib import Path + + +TARGET = (3, 5, 6) +CYCLE = ((1, 0), (2, 1), (0, 2)) +FILES = ("README.md", "SOURCES.json", "TASK.json", "VERIFY.json", "verify.py") + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def column_step(state, gate): + i, j, coefficient = gate + need(0 <= i < 3 and 0 <= j < 3 and i != j, "invalid directed edge") + need(1 <= coefficient <= 7, "invalid nonzero Boolean coefficient") + result = list(state) + result[i] ^= coefficient & state[j] + return tuple(result) + + +def column_graph(root): + start = tuple(7 if i == root else 0 for i in range(3)) + distance = {start: 0} + queue = deque([start]) + gates = tuple((i, j, a) for i, j in CYCLE for a in range(1, 8)) + for _ in range(343): + if not queue: + break + state = queue.popleft() + for gate in gates: + result = column_step(state, gate) + if result not in distance: + need(len(distance) < 343, "column-state capacity exceeded") + distance[result] = distance[state] + 1 + queue.append(result) + need(not queue and len(distance) == 343, "incomplete nonzero-column graph") + for state in distance: + for gate in gates: + result = column_step(state, gate) + need(abs(distance[result] - distance[state]) <= 1, "distance edge") + need(distance[TARGET] == 4, "cycle column distance is not four") + return dict(sorted(Counter(distance.values()).items())) + + +def scalar_column_obstruction(root): + """Enumerate the columns reachable by every word of length <=3.""" + start = tuple(1 << root for _ in range(3)) + goal = (3, 5, 6) # Each bit-coordinate column, encoded by destination bits. + frontier = {start} + counts = [1] + for _ in range(3): + next_frontier = set() + for columns in frontier: + for destination, source in CYCLE: + for chosen in range(1, 8): + changed = [] + for coordinate, column in enumerate(columns): + active = (chosen >> coordinate) & (column >> source) & 1 + changed.append(column ^ (active << destination)) + next_frontier.add(tuple(changed)) + need(goal not in next_frontier, "a three-step column word exists") + frontier = next_frontier + counts.append(len(frontier)) + return counts + + +def suffix(root): + following, last = (root + 1) % 3, (root + 2) % 3 + return ((following, root, TARGET[last]), (last, following, 7), + (following, root, TARGET[root]), (root, last, 7 ^ TARGET[root])) + + +def program(root): + tail = suffix(root) + return tuple(reversed(tail)) + ((root, 3, 7),) + tail + + +def literal(state, word): + """Bit-list arithmetic, separate from the packed column transition.""" + rows = [[(value >> bit) & 1 for bit in range(3)] for value in state] + for destination, source, coefficient in word: + need(0 <= destination < 3 and 0 <= source < 4, "invalid row") + need(destination != source and 1 <= coefficient <= 7, "invalid gate") + for bit in range(3): + if (coefficient >> bit) & 1: + rows[destination][bit] = (rows[destination][bit] + rows[source][bit]) % 2 + return tuple(sum(value << bit for bit, value in enumerate(row)) for row in rows) + + +def expected(state): + return tuple(state[i] ^ (TARGET[i] & state[3]) for i in range(3)) + (state[3],) + + +def endpoint(word): + for column in range(4): + for bit in range(3): + state = tuple(1 << bit if i == column else 0 for i in range(4)) + if literal(state, word) != expected(state): + return False + return True + + +def check_words(): + scalar_cases = 0 + for root in range(3): + word = program(root) + need(len(word) == 9 and endpoint(word), "formal arbitrary-dirt endpoint") + need(sum(j == 3 for _, j, _ in word) == 1, "insertion count") + need(all(j == 3 or (i, j) in CYCLE for i, j, _ in word), "off-cycle gate") + for state in product(range(8), repeat=4): + result = literal(state, word) + need(result == expected(state), "literal scalar endpoint") + need(literal(result, tuple(reversed(word))) == state, "literal inverse") + scalar_cases += 1 + return scalar_cases + + +def tariff(insertion_prices, cycle_price, reverse_prices): + need(len(insertion_prices) == 3 and len(reverse_prices) == 3, "three prices required") + need(cycle_price > 0, "cycle price must be positive") + need(min(insertion_prices) >= 8 * cycle_price, "insertion prices outside cone") + need(min(reverse_prices) >= 8 * cycle_price, "reverse prices outside cone") + return min(insertion_prices) + 8 * cycle_price + + +def check_prices(): + cases = 0 + for denominator in (1, 3, 7): + c = Fraction(1, denominator) + for mu in ((8, 8, 8), (100, 100, 100), (9, 20, 30), (31, 8, 19)): + prices = tuple(x * c for x in mu) + reverse = (8 * c, 100 * c, 12 * c) + optimum = tariff(prices, c, reverse) + root = min(range(3), key=lambda i: prices[i]) + bill = sum(prices[i] if j == 3 else c for i, j, _ in program(root)) + need(bill == optimum, "attaining word tariff") + need(2 * min(prices) >= optimum, "multi-insertion bound") + need(min(prices) + min(reverse) >= optimum, "reverse-edge bound") + cases += 1 + need(tariff((100, 100, 100), 1, (100, 100, 100)) == 108, "concrete tariff") + return cases + + +def check_controls(): + word = program(0) + for index in range(9): + need(not endpoint(word[:index] + word[index + 1:]), "omitted-gate mutant") + for index, (i, j, a) in enumerate(word): + mutant = word[:index] + ((i, j, a ^ 1),) + word[index + 1:] + if a ^ 1: + need(not endpoint(mutant), "coefficient mutant") + for root in range(3): + need(not endpoint(((root, 3, 7),) + suffix(root)), "missing dirt preparation") + invalid = (((7, 8, 8), 1, (8, 8, 8)), ((8, 8, 8), 1, (8, 7, 8)), + ((8, 8, 8), 0, (8, 8, 8)), ((8, 8), 1, (8, 8, 8))) + for prices, c, reverse in invalid: + try: + tariff(prices, c, reverse) + except ValueError: + continue + raise ValueError("invalid tariff boundary accepted") + return 9 + sum((a ^ 1) != 0 for _, _, a in word) + 3 + len(invalid) + + +def main(): + layers = [column_graph(root) for root in range(3)] + short = [scalar_column_obstruction(root) for root in range(3)] + cases = check_words() + prices = check_prices() + controls = check_controls() + folder = Path(__file__).resolve().parent + hashes = {} + for name in FILES: + content = (folder / name).read_bytes() + need(len(content) <= 131072, "package file capacity exceeded") + hashes[name] = sha256(content).hexdigest() + print(json.dumps({"status": "PASS_BOOLEAN_DIRECTED_CYCLE_TARIFF", + "claim_type": "scoped proof with exact finite corroboration", + "column_states_per_root": 343, "minimum_suffix_adds": [4] * 3, + "distance_layers": layers, "short_word_frontiers": short, + "literal_forward_inverse_inputs": cases, + "price_fixtures": prices, "rejection_controls": controls, + "concrete_optimum": 108, "direct_insertion_bill": 300, + "word_root_zero": program(0), "sha256": hashes}, sort_keys=True)) + + +if __name__ == "__main__": + main()