diff --git a/research/integer-fanout-shortening-gap/PROOF.md b/research/integer-fanout-shortening-gap/PROOF.md new file mode 100644 index 0000000000..ac24465c45 --- /dev/null +++ b/research/integer-fanout-shortening-gap/PROOF.md @@ -0,0 +1,120 @@ +# An integer shortening obstruction + +## Contract and theorem + +Let `a,b,p` be arbitrary elements of `Z^w`, where `w>=1`. The source p is +preserved. Exactly two dirty working rows A and B start at a and b. Allowed +gates have arbitrary integer coefficients and are only + +```text +P0(t): A += t p P1(t): B += t p price mu each +E0(t): A += t B E1(t): B += t A price c each. +``` + +Prices mu and c are positive, stationary and coefficient-independent. All +gates, including inverses, are paid. There are no extra rows, free scales, +free swaps, observers, branching or free basis changes. A word is finite +and independent of its input values. Its endpoint must be + +```text +A = a + 5p, B = b + 12p, with p unchanged. +``` + +**Theorem.** The exact minimum price over all such words is +`min(2 mu, mu+6c)`. In particular it is 16 when mu=10 and c=1. + +This is a scoped algebraic tariff. The assumption of coefficient-independent +prices is a declared interface, not a claim about actual fixed-tape costs. + +## Lower bound + +With no source insertion, both source coefficients stay zero, so the word +cannot attain the endpoint. A word with at least two insertions costs at least +2 mu. This bound does not limit their placement or their coefficients. + +Consider a word with exactly one insertion `Pi(beta)`. Let L be the 2-by-2 +integer matrix of all row additions before it and C the matrix of all row +additions after it, in their chronological action order. Dirt restoration +requires `CL=I`. The source column is `beta C e_i = (5,12)^T`. + +Every elementary row-addition matrix has determinant one. Each column of +C is therefore primitive. Equivalently, its coordinates have gcd one, +because the corresponding row of C inverse is an integral Bezout witness. +The source equation gives `|beta|=gcd(5,12)=1`. Thus +`C e_i` is either `(5,12)^T` or `(-5,-12)^T`. + +Neither signed column can be obtained from either coordinate vector with +at most two integer row additions. Consecutive additions in one direction +combine into one. Of the two alternating orders, one has an initially +inactive first gate. The only remaining possibilities, including shorter +words, are + +```text +from e0: (1,t) or (1+s t,t), +from e1: (t,1) or (t,1+s t), s,t in Z. +``` + +For e0, the latter form would require t=12 or t=-12. Its first coordinate +is 1 modulo 12, whereas 5 and -5 are not. The former form has first +coordinate one. For e1 the latter form would require t=5 or t=-5. Its +second coordinate is 1 modulo 5, whereas 12 and -12 are not. The former +form has second coordinate one. All possibilities fail. + +Consequently every suffix C uses at least three row additions. Every +prefix L uses at least three as well. Otherwise reversing its at-most-two +gates and negating their coefficients would express `L^-1=C` with at most +two gates, contradicting the same column obstruction. Exactly one insertion +therefore costs at least `mu+6c`. Together with the insertion-count split +this proves the lower envelope. Arbitrarily large integer coefficients and +arbitrarily long interleavings have not been bounded or omitted. + +## Attainment + +Let C be the following three row additions in chronological order + +```text +E1(2), E0(2), E1(2). +``` + +Their matrix is `[[5,2],[12,5]]`, with determinant one and first column +(5,12). Perform C inverse, then `P0(1)`, then C. In literal order this is + +```text +E1(-2), E0(-2), E1(-2), P0(1), E1(2), E0(2), E1(2). +``` + +Every dirt column returns and the source contribution is exactly (5,12). +The price is `mu+6c`. Direct insertions `P0(5),P1(12)` cost 2 mu. These +two words attain both branches of the envelope, including their tie at +mu=6c. Since equality of the full integer coefficient matrices implies +equality on each coordinate, both constructions work for every w>=1. + +## Why finiteness matters + +Ali Romman's PR5312 extends lee-phys's finite-commutative formula to finite +associative rings. Its shortening step is expressly finite; this package +does not dispute that theorem. Formally applying its five-term formula over +Z to demand (5,12), with equal directional prices, would give +`min(2mu,mu+4c)`: the demand ideal is principal and neither demand divides +the other. At mu=10,c=1 this is 14, strictly below the proved optimum 16. + +Thus principality alone does not justify that finite-length tariff over +integer coefficients. This example does admit one insertion; its extra +restoration cost, rather than infeasibility, is the obstruction. The result +does not exclude a different integer formula, extra dirty rows, rational or +dyadic coefficients, coefficient-dependent pricing or a different caller. + +## Finite evidence + +The new verifier checks the complete 3-by-3 operators, literal dirty inputs, +both attaining costs and semantic mutations. It also enumerates every +column reachable in at most two shears over Z/60Z, with all sixty residue +coefficients in each direction. Both signed target columns are absent from +both origins. A separate direct normal-form set gives the identical result. +Every integer two-shear word maps into this finite quotient, so this is +also an independently rerunnable finite certificate of that local step. +It does not replace the written insertion-count and restoration argument. + +Elementary matrices, primitivity and Bezout identities are classical. The +new repository result is this exact integer tariff and its finite-ring +extension discriminator; global literature priority is unclaimed. diff --git a/research/integer-fanout-shortening-gap/README.md b/research/integer-fanout-shortening-gap/README.md new file mode 100644 index 0000000000..132cf4e8ea --- /dev/null +++ b/research/integer-fanout-shortening-gap/README.md @@ -0,0 +1,132 @@ +# An exact integer dirty-fanout tariff beyond finite-ring shortening + +This contribution was produced by Nick Petalas. Apache-2.0. +Independent human and formal proof-kernel review are unclaimed. + +**Claim type: scoped proof with exact finite corroboration.** For two arbitrary +dirty integer rows a,b and one preserved source p, require +`A=a+5p, B=b+12p`. Permit only integer source insertions and integer scaled +row additions, at uniform positive prices mu and c respectively. All dirt +must return, with no extra row, free scale or free basis change. The exact +minimum over arbitrary finite input-independent words is + +```text +OPT = min(2 mu, mu + 6 c). +``` + +At mu=10,c=1 the optimum is 16. Formally extending the five-term finite-ring +formula would give 14. This is a sharp obstruction to that extension; the +predecessor's finite-ring theorem remains outside the claim being proved. + +[PROOF.md](PROOF.md) proves the unrestricted coefficient and word-length +statement. With one insertion, the suffix must have primitive column +plus or minus (5,12). Every two-shear integer column has a coordinate one +or has one coordinate congruent to one modulo the other. Neither target +sign passes. Dirt restoration requires the inverse prefix, giving at least +six paid row additions. The following chronological word attains that bound + +```text +B -= 2A; A -= 2B; B -= 2A; A += p; B += 2A; A += 2B; B += 2A. +``` + +Two direct insertions attain the other branch. The proof applies to every +positive row width by exact equality of the full coefficient operators. + +## Evidence and reproduction + +From the repository root with CPython 3.12 and the standard library + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/integer-fanout-shortening-gap/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/integer-fanout-shortening-gap/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/integer-fanout-shortening-gap +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/integer-fanout-shortening-gap --check-source-history +``` + +On another host substitute its CPython 3.12 executable. The direct verifier +prints `PASS_INTEGER_FANOUT_SHORTENING_GAP` inside a generated JSON receipt +bound to all six package files. It writes no files. The registered runner +prints `PASS_REGISTERED_RESEARCH_PACKAGE`. No receipt is handwritten. + +The verifier checks both complete 3-by-3 dirty/source operators and the +attaining inverse, literal integer input fixtures, rational price fixtures +and semantic mutations. A complete modulo-60 column census includes every +residue coefficient in both directions through two shears. A separate +normal-form calculation produces the same reachable sets. Both signed +columns are absent from both origins. Reduction maps every integer word +into that quotient, making this a finite certificate of the local lower-bound +step. The universal tariff still uses the written insertion-count proof. +The generated receipt supplies the exact enumerated counts. + +The local replay enumerates 1,458 dirty-input executions, 729 rational +price pairs, 1,617 reachable quotient columns per origin and 14,400 +quotient transitions across both searches. All sixteen semantic rejection +controls pass. Normal and optimized receipts agree exactly. + +## Source, credit and overlap + +Credit Ali Romman's [PR5312](https://github.com/CrocSwap/integer-mult-bounds/pull/5312) +for the finite-ring five-term tariff and its explicit infinite-ring boundary, +lee-phys's PR5139 for the finite-commutative formula, Krzysztof Wojt's PR5045 +for the insertion/return classification, Ross Richardson's PR3121 for the +dirty-fanout lineage, Nick Petalas's PR4916 for the older unit-demand ring +contract, and Ali Romman's PR5310 for finite-module shortening. Their +predecessor credits remain intact. No predecessor executable or scientific +census is replayed as this contribution. Elementary matrices, Euclidean +arithmetic and Bezout identities are classical; global literature priority +is unclaimed. + +Base canonical main is `2485805a6d47f36ea83ddde6327d453ac82d44dc`, priority +revision 8. [Advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19294861). +[SOURCES.json](SOURCES.json) pins the finite-ring README as context, not as +a mathematical dependency for the integer proof. The source PR head is +`5cbdbc8e3858e67c8bfbd160f742ef1e9ced9d38`. TASK.json explicitly changes the +connector-alphabet card to this scoped interface side result. Its first +945-pairing control and the selected source-binding orientation passed. + +Live handoffs, active Discussions, current open PRs, recent account work, +local reservations and distinctive main/merged searches were checked. +No same-demand integer shortening result was found in that coverage. +Recent three-row Boolean and directed-cycle tariff results have different +row/topology contracts. Sparse local notes, arbitrary historical diffs and +unpublished work remain coverage limits. No novelty guarantee follows. + +## Limits and implementation bounds + +This proves an abstract exact tariff under the stated arithmetic and price +contract. It supplies no physical caller, rounded implementation, recursive +invoice gain, new kappa or complete multiplication theorem. The selected +frontier and five framework assumptions retain their status. No selected +cold replay, native suite, Lean or Docker build was run. + +The checker has fixed domains: 3-by-3 matrices, words of at most eight gates, +coefficients of magnitude at most twelve, 9^3 input triples, at most 40^2 +price fixtures, and two depth-two searches in a 60^2-state quotient. These +are checker capacities, not bounds on the theorem. The proof covers arbitrary +integer coefficients and word lengths. There is no recursion, subprocess, +network access, dynamic code or writable output. Every function fits below +sixty lines. Explicit guards remain enabled under optimized Python. + +Power of Ten rule 3 has a managed-runtime deviation: CPython allocates +integers, fractions and bounded collections. At most 3600 quotient states +and six one-MiB file reads constrain live data. No allocation-free runtime +claim is made. A fixed-buffer port would be needed if that becomes a host +requirement. Warning-strict normal/optimized runs and available static +analysis provide the interpreted-code diagnostics. +No separate Python linter is installed; source compilation and a static +function-length inspection also pass, with a largest function of sixteen +lines. + +## Open next questions + +- Can one-insertion restoration require arbitrarily many row additions for + primitive integer demands? This determines whether a finite shortening + allowance needs an unbounded replacement. Start with signed Euclidean + paths and include their inverse-prefix costs. A general shortest-column + classification is not supplied here. +- Does a real helper caller enforce integer coefficients and supply complete + coefficient-independent prices? Pin its arithmetic, source access, frames, + precision and tape contract before using this tariff. No such caller or + favorable complete invoice is supplied here. + +These questions are recorded in TASK.json. Stop at this first exact result. diff --git a/research/integer-fanout-shortening-gap/SOURCES.json b/research/integer-fanout-shortening-gap/SOURCES.json new file mode 100644 index 0000000000..8cfb860c99 --- /dev/null +++ b/research/integer-fanout-shortening-gap/SOURCES.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "base_commit": "2485805a6d47f36ea83ddde6327d453ac82d44dc", + "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/noncommutative-two-row-tariff/README.md", + "usage": "input", + "git_blob": "e10c6ed3e334833381a5fdd6194f5997b748588a", + "sha256": "4493ad8069af23eec19c8bccc685a41444d712167a1e7b3e6cd5121a7d1ba130" + } + ] +} diff --git a/research/integer-fanout-shortening-gap/TASK.json b/research/integer-fanout-shortening-gap/TASK.json new file mode 100644 index 0000000000..f5b240d312 --- /dev/null +++ b/research/integer-fanout-shortening-gap/TASK.json @@ -0,0 +1,75 @@ +{ + "schema_version": 1, + "task_id": "connector-alphabet-change", + "priority_revision": 8, + "base_commit": "2485805a6d47f36ea83ddde6327d453ac82d44dc", + "original_card": { + "id": "connector-alphabet-change", + "question": "Does one explicit extension of the connector alphabet offer a favorable completed budget?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/universal-connector-boundary/README.md", + "certificates/selected-result.json" + ], + "methods": [ + "Construct and charge a legal extra operation on a minimal instance.", + "Prove a target-specific bound after adding one specified operation family." + ], + "acceptance_gate": "State which fixed-alphabet premise changes and charge its implementation; do not declare it free. 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", + "research/universal-connector-boundary/verify.py" + ], + "expected": "PASS_UNIVERSAL_CONNECTOR_BOUNDARY", + "inspect": "Reproduce the 945-pairing control, then read Exact interface to list the allowed calls.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Add exactly one legally priced operation and test a tiny dirty-input instance before enumerating larger cases.", + "bottleneck_link": "A new legal connector operation could change recursive interface cost; a larger census in the same alphabet is a separate side result.", + "allowed_variations": [ + "Choose one additional operation and a small source count for its first counterexample." + ], + "scope_change_triggers": [ + "Keeping the alphabet and only increasing the source count; record this as a changed assignment.", + "Extending a source-count census without naming a supplier/interface decision it could change; audit #2973 pruning concerns before relying on the affected predecessor exclusions." + ], + "overlap_terms": [ + "universal connector", + "source-toggle", + "connector alphabet" + ] + }, + "scope_status": "changed", + "actual_scope": "Exact unrestricted integer-coefficient tariff for demand (5,12) on two dirty rows and one preserved source, at equal positive source and row-ADD prices.", + "scope_change_reason": "The connector card is changed to a scoped infinite-coefficient interface obstruction. The source finite-ring shortening theorem explicitly excludes infinite rings; this is a new tariff result, not a predecessor audit or a new operation supplied to the selected caller.", + "bottleneck_link": "Side result: prevents importing a finite-ring helper-delivery price into an integral dirty-restoration contract without an additional shortening proof. It does not improve the selected invoice.", + "budget_minutes": 60, + "stop_rule": "Ship the first exact tariff and its attaining word; no general Euclidean-length classification or physical implementation expansion.", + "outcome": "completed", + "evidence": "PROOF.md and standalone verify.py; full dirty/source operators, complete two-shear quotient obstruction, literal input executions, tariff fixtures and semantic rejection controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Which primitive integer demands require arbitrarily many paid row additions with exactly one source insertion?", + "why_it_matters": "A uniform finite-ring shortening allowance might need an unbounded integer replacement.", + "first_step": "Relate the shortest attainable primitive-column path to a signed Euclidean algorithm, preserving the inverse-prefix cost.", + "blocked_by": "No general integer shortest-column classification is proved here." + }, + { + "question": "Does an actual helper caller enforce integer coefficients and provide coefficient-independent complete prices?", + "why_it_matters": "The scoped tariff has no supplier consequence without a matching arithmetic and physical contract.", + "first_step": "Pin one caller, its allowed coefficient domain and its complete source/ADD tariff before applying the example.", + "blocked_by": "No selected caller or rounded/tape realization is supplied." + } + ], + "source_question": { + "source": "PR #5312", + "author": "aliromman", + "head": "5cbdbc8e3858e67c8bfbd160f742ef1e9ced9d38", + "question": "Originally posed exact integer tariff at the source theorem's explicit infinite-ring scope boundary; not a claimed question from its physical-realization handoff." + }, + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19294861" +} diff --git a/research/integer-fanout-shortening-gap/VERIFY.json b/research/integer-fanout-shortening-gap/VERIFY.json new file mode 100644 index 0000000000..1f18e1c0e2 --- /dev/null +++ b/research/integer-fanout-shortening-gap/VERIFY.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/noncommutative-two-row-tariff/README.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Exact full dirty/source operators, complete modulo-60 short-column certificate, prices and semantic rejection controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Identical fixed-domain theorem corroboration with optimized Python; guards remain enabled." + } + ] +} diff --git a/research/integer-fanout-shortening-gap/verify.py b/research/integer-fanout-shortening-gap/verify.py new file mode 100644 index 0000000000..69ca0734e6 --- /dev/null +++ b/research/integer-fanout-shortening-gap/verify.py @@ -0,0 +1,169 @@ +"""Exact fixed-domain corroboration of the integer fanout tariff theorem.""" + +import hashlib +import itertools +import json +import platform +import sys +from fractions import Fraction +from pathlib import Path + + +PACKAGE = Path(__file__).resolve().parent +FILES = ("README.md", "PROOF.md", "TASK.json", "SOURCES.json", "VERIFY.json", "verify.py") +IDENTITY = ((1, 0, 0), (0, 1, 0), (0, 0, 1)) +DEMAND = ((1, 0, 5), (0, 1, 12), (0, 0, 1)) +FORWARD = ((1, 0, 2), (0, 1, 2), (1, 0, 2)) +INVERSE = tuple((i, j, -a) for i, j, a in reversed(FORWARD)) +CONJUGATION = INVERSE + ((0, 2, 1),) + FORWARD +DIRECT = ((0, 2, 5), (1, 2, 12)) + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def read_bytes(path): + require(path.is_file() and not path.is_symlink(), "missing regular input") + require(path.stat().st_size <= 1024 * 1024, "input exceeds one MiB") + return path.read_bytes() + + +def authenticate(): + source = json.loads(read_bytes(PACKAGE / "SOURCES.json")) + live = [row for row in source["files"] if row["usage"] == "input"] + require(len(live) == 1, "exactly one context input required") + row = live[0] + require(row["path"] == "research/noncommutative-two-row-tariff/README.md", "source path") + payload = read_bytes(PACKAGE.parent.parent / row["path"]) + require(hashlib.sha256(payload).hexdigest() == row["sha256"], "source hash mismatch") + return {name: hashlib.sha256(read_bytes(PACKAGE / name)).hexdigest() for name in FILES} + + +def operator(word): + require(len(word) <= 8, "fixed checker word capacity") + matrix = [list(row) for row in IDENTITY] + for i, j, coefficient in word: + require(type(i) is int and type(j) is int, "integer role indices") + require(i in (0, 1) and j in (0, 1, 2) and i != j, "gate roles") + require(type(coefficient) is int and abs(coefficient) <= 12, "checker coefficient capacity") + matrix[i] = [x + coefficient * y for x, y in zip(matrix[i], matrix[j], strict=True)] + return tuple(tuple(row) for row in matrix) + + +def multiply(left, right): + return tuple(tuple(sum(left[i][k] * right[k][j] for k in range(3)) + for j in range(3)) for i in range(3)) + + +def execute(word, values): + state = list(values) + for i, j, coefficient in word: + state[i] += coefficient * state[j] + return tuple(state) + + +def check_attainers(): + forward, inverse = operator(FORWARD), operator(INVERSE) + require(forward == ((5, 2, 0), (12, 5, 0), (0, 0, 1)), "attaining column") + require(multiply(forward, inverse) == IDENTITY, "right inverse") + require(multiply(inverse, forward) == IDENTITY, "left inverse") + for word in (CONJUGATION, DIRECT): + require(operator(word) == DEMAND, "full dirt/source endpoint") + cases = 0 + for values in itertools.product(range(-4, 5), repeat=3): + a, b, p = values + for word in (CONJUGATION, DIRECT): + require(execute(word, values) == (a + 5 * p, b + 12 * p, p), "literal dirty input") + cases += 1 + return cases + + +def short_columns(origin): + reached = {origin} + frontier = {origin} + layers = [1] + edges = 0 + for _depth in range(2): + following = set() + for x, y in frontier: + for a in range(60): + following.add(((x + a * y) % 60, y)) + following.add((x, (y + a * x) % 60)) + edges += 2 + frontier = following - reached + reached.update(following) + layers.append(len(frontier)) + return reached, layers, edges + + +def check_short_obstruction(): + rows = [] + for axis, origin in enumerate(((1, 0), (0, 1))): + reached, layers, edges = short_columns(origin) + expected = set() + for s, t in itertools.product(range(60), repeat=2): + if axis == 0: + expected.update(((1, t), ((1 + s * t) % 60, t))) + else: + expected.update(((t, 1), (t, (1 + s * t) % 60))) + require(reached == expected, "independent two-shear normal form") + for sign in (-1, 1): + require((sign * 5 % 60, sign * 12 % 60) not in reached, "short integer column excluded") + rows.append({"origin": list(origin), "new_states_by_depth": layers, "edges": edges}) + require(5 * 5 - 12 * 2 == 1, "primitive demand Bezout witness") + return rows + + +def bill(word, mu, c): + return sum((mu if j == 2 else c) for _i, j, _a in word) + + +def check_prices(): + prices = sorted({Fraction(n, d) for n in range(1, 11) for d in range(1, 5)}) + cases = 0 + for mu, c in itertools.product(prices, repeat=2): + witness = min(bill(DIRECT, mu, c), bill(CONJUGATION, mu, c)) + require(witness == min(2 * mu, mu + 6 * c), "attained envelope") + cases += 1 + require(bill(CONJUGATION, 10, 1) == 16, "integer discriminator") + require(min(2 * 10, 10 + 4 * 1) == 14, "excluded finite-formula extension") + require(bill(CONJUGATION, 6, 1) == bill(DIRECT, 6, 1), "tariff transition") + return cases + + +def check_controls(): + controls = 0 + for k in range(len(CONJUGATION)): + deleted = CONJUGATION[:k] + CONJUGATION[k + 1:] + require(operator(deleted) != DEMAND, "deleted gate accepted") + i, j, a = CONJUGATION[k] + wrong_sign = CONJUGATION[:k] + ((i, j, -a),) + CONJUGATION[k + 1:] + require(operator(wrong_sign) != DEMAND, "wrong sign accepted") + controls += 2 + require(operator(((0, 2, 5),)) != DEMAND, "missing second output accepted") + require(operator(((1, 0, 2), (0, 2, 5), (1, 0, -2))) != DEMAND, "wrong ratio accepted") + return controls + 2 + + +def main(): + require(len(sys.argv) == 1, "this fixed verifier takes no arguments") + hashes = authenticate() + receipt = { + "status": "PASS_INTEGER_FANOUT_SHORTENING_GAP", + "claim_type": "scoped proof with exact finite corroboration", + "demand": [5, 12], + "tariff": "min(2*mu,mu+6*c), mu>0,c>0", + "literal_dirty_executions": check_attainers(), + "modulus_60_short_column_census": check_short_obstruction(), + "rational_price_fixtures": check_prices(), + "semantic_rejection_controls": check_controls(), + "package_sha256": hashes, + "python": platform.python_version(), + } + print(json.dumps(receipt, sort_keys=True, indent=2)) + + +if __name__ == "__main__": + main()