From 07d644c8c798e3d3fb676a1451b08b41afd54b02 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Tue, 27 Oct 2026 15:20:32 +0000 Subject: [PATCH] feat(research): exclude the nonlinear six-frame seed with two cuts --- research/six-frame-seed-cut/README.md | 188 +++++++++++++++++++++++ research/six-frame-seed-cut/SOURCES.json | 24 +++ research/six-frame-seed-cut/TASK.json | 90 +++++++++++ research/six-frame-seed-cut/VERIFY.json | 36 +++++ research/six-frame-seed-cut/verify.py | 174 +++++++++++++++++++++ 5 files changed, 512 insertions(+) create mode 100644 research/six-frame-seed-cut/README.md create mode 100644 research/six-frame-seed-cut/SOURCES.json create mode 100644 research/six-frame-seed-cut/TASK.json create mode 100644 research/six-frame-seed-cut/VERIFY.json create mode 100644 research/six-frame-seed-cut/verify.py diff --git a/research/six-frame-seed-cut/README.md b/research/six-frame-seed-cut/README.md new file mode 100644 index 0000000000..d198c33293 --- /dev/null +++ b/research/six-frame-seed-cut/README.md @@ -0,0 +1,188 @@ +# Two cuts exclude the proposed six-frame nonlinear seed + +This scoped mathematical proof establishes the sharp rank-mass bound `s >= 2W` +for the six rational frames + +```text +S = {0, I, J, J+I, B, B+I}, +J = [[0,1],[-1,0]], B = [[0,0],[-1,1]]. +``` + +Five roles therefore require cost at least ten. Searching for a cost-nine +nonlinear circuit inside this alphabet cannot answer the open construction +question in Jose Manuel / jmbarrancoml's +[PR #1757](https://github.com/CrocSwap/integer-mult-bounds/pull/1757). +That source proposes `J` and `B` as a possible seed because they have no common +flag. The new result shows that this seed, with its identity translates and +`0,I` endpoints, still has a sharp cut obstruction. Larger frame alphabets +and arbitrary rational combinations of the seed matrices remain outside scope. + +The new proof and checker were produced by Nick Petalas. Independent human and +formal proof-kernel review are unclaimed. No new kappa, supplier, selected-frontier +change or complete multiplication theorem is claimed. + +## Contract and theorem + +Use PR #1757's fixed finite acyclic pointwise circuit model. There are `W` +independent input symbols over one finite alphabet of size at least two. Every +required output is its prescribed input under one fixed role permutation `rho`, +on every assignment. Count all arbitrary dirty roles among these inputs. +Gates may be nonlinear and need only be deterministic. Each gate has one common +frame on all its ports; every source and sink also has a frame. All frames +belong to `S`. Charge every physical wire segment `e=(u,v)`, including terminal +and untouched wires, by + +```text +r_e = rank_Q(M_v - M_u), s = sum_e r_e. +``` + +For each demand `w`, require +`M_out(rho(w)) - M_in(w) = I`. There are no uncharged observations, +message-bearing side channels, postselection or input-dependent topologies. + +**Theorem.** Every such circuit satisfies `s >= 2W`. Equality is attainable +within this class. Thus the five-role minimum is ten when topology may vary. + +## Exact certificate and proof + +Assign each frame two Boolean labels: + +| Frame | First label | Second label | +|---|---:|---:| +| `0` | 0 | 0 | +| `I` | 1 | 1 | +| `J` | 0 | 0 | +| `J+I` | 1 | 1 | +| `B` | 0 | 1 | +| `B+I` | 1 | 0 | + +In this frame order the complete rank-distance matrix is + +```text + 0 I J J+I B B+I + 0 0 2 2 2 1 2 + I 2 0 2 2 1 1 + J 2 2 0 2 1 2 + J+I 2 2 2 0 1 1 + B 1 1 1 1 0 2 + B+I 2 1 2 1 2 0 +``` + +Write `d_H` for Hamming distance between the two-bit labels. Every entry obeys +`d_H(labels(A),labels(C)) <= rank_Q(C-A)`. A two-by-two difference has rank two +when its determinant is nonzero, rank one when it is nonzero with determinant +zero, and rank zero otherwise. These rules verify the table directly. + +The only ordered pairs in `S` with difference `I` are `(0,I)`, `(J,J+I)` and +`(B,B+I)`. All three have Hamming distance two. Each of the two labelings +therefore separates every prescribed source/sink demand. + +Apply PR #1757's weighted partition theorem to these two unit-weight labelings. +Its cut inequality charges at least `W` crossing edges for each labeling. +The Hamming inequality bounds the sum of the two crossing indicators on any +edge by its rank charge. Hence + +```text +s >= number of first-label crossing edges + + number of second-label crossing edges >= W + W = 2W. +``` + +This is a new finite frame certificate applied to the cited cut theorem. +The conclusion covers every topology and number of gates satisfying the +contract; it is not an inference from a failed circuit search. + +For sharpness, take `W` direct wires from source `w` to sink `rho(w)`, with +source frame `0` and sink frame `I`. Each wire costs two and copies its symbol. +For `W >= 3`, assign three source/sink pairs the three different identity-shift +types instead. This attains the same bound while using all six frames. +Sharpness is over this circuit class, not every fixed topology. + +For every `0 < alpha < 1`, the normalized optimistic rank invoice satisfies + +```text +(1/W) sum_e (r_e/2)^alpha >= (1/W) sum_e r_e/2 >= 1. +``` + +This alphabet therefore cannot give strict contraction under that invoice +before nonnegative implementation charges. This is a circuit-class +obstruction, not an integer-multiplication lower bound. + +## Why this goes beyond a common flag + +The commutator is `J B - B J = [[-1,1],[1,1]]`, of determinant `-2`. +A common invariant line over a characteristic-zero extension would let both +matrices be simultaneously upper triangular. Their commutator would then +have zero diagonal and determinant zero. They therefore have no such line. +A common affine frame offset does not help: differences from frame `0` would +still triangularize `J` and `B`. Thus the excluded alphabet has no common flag. +This certificate does not assert that all rank metrics admit these cuts. + +## Reproduce and evidence + +From the repository root, with CPython 3.12 and its standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/six-frame-seed-cut/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/six-frame-seed-cut/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/six-frame-seed-cut +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/six-frame-seed-cut --check-source-history +``` + +The verifier prints `PASS_SIX_FRAME_SEED_CUT` in a generated JSON receipt. +It checks all 36 ordered rank pairs by determinant and separate rational row +elimination, all three identity shifts, the explicit certificate, and all +4,096 assignments of two Boolean labels to six frames. Exactly sixteen +assignments obey the edge budgets and separate all identity demands in both +bits. Eleven controls reject malformed labels, changed edge budgets, changed +labels and incomplete/reordered endpoint lists. The commutator check confirms +the declared common-flag boundary. The receipt hashes all five package files +and the cited source bytes. Default replay writes no files, uses no Git or +external programs, and works in an export containing the declared input. + +The finite checks certify the matrix table and cuts. The all-circuit statement +is the written application of the predecessor's theorem. The original theorem, +its circuits and reported counts are cited, not audited. No Lean, native +supplier or selected cold replay is run. + +The checker uses fixed two-by-two matrices, six frames, at most 4,096 label +assignments and eleven controls. Every function is below sixty lines. Explicit +exceptions keep checks enabled under optimized Python. Python and `Fraction` +allocate dynamically; bounded finite data replace static allocation in this +offline checker. This managed-runtime deviation supplies no real-time or +physical-memory guarantee. Warning-strict runs are registered in +[VERIFY.json](VERIFY.json). + +## Scope and attribution + +[TASK.json](TASK.json) records the changed `bit-new-register-model` scope, +priority revision eight, the advance claim and stopping rule. The card's first +source-binding command passed. This side result addresses one nonlinear seed; +it does not implement the card's nonabelian native register program. Main was +pinned at `19fdb086ea96af9a9f87936a2b888e10af4ed810`. Exact predecessor and +historical card/selected-record pins are in [SOURCES.json](SOURCES.json). +Live open PRs, Discussions and cached overlap were checked; all main README +paths were additionally searched. Unpublished work and arbitrary code diffs +remain outside that coverage. + +Jose Manuel / jmbarrancoml supplies PR #1757's nonlinear cut theorem, weighted +partition criterion and seed question. Navinor supplies PR #825's earlier +common-flag XOR obstruction. The retained upstream finite shear contract and +routing/cleanup lineage retain the credit stated in those sources. +CubeJerry's PR #907 distinguishes arbitrary rank metrics from cut metrics; +its counterexamples and distortion results are cited, not replayed. Cut +counting and rational matrix rank are classical methods. The new contribution +is this six-frame certificate, its all-topology application and checker. +No general literature-priority claim is made. Apache-2.0. + +## Open next questions + +1. Which added rational frame defeats this certificate and still permits a + complete cost-nine five-role circuit? First include that frame and all new + identity shifts in the weighted cut feasibility problem. Failure of these + two cuts alone does not establish feasibility or exclude other cut bounds. +2. Can a complete nonlinear permutation circuit outside this alphabet achieve + `s < 2W`? Publish the DAG, complete scalar truth table and every charged + frame edge before claiming a gain. A physical implementation, complete + invoice, compiler and outer admission remain separate obligations. + +No follow-up is reserved. Structured first steps and blockers are in TASK.json. diff --git a/research/six-frame-seed-cut/SOURCES.json b/research/six-frame-seed-cut/SOURCES.json new file mode 100644 index 0000000000..557ca6201f --- /dev/null +++ b/research/six-frame-seed-cut/SOURCES.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "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/nonlinear-frame-cut-bound/README.md", + "usage": "input", + "git_blob": "1fae484c0dc371afb0ec0d0c9b1f781d78dbffbb", + "sha256": "411b78a56180e835bb97e59b9845968d84ad3fb8f5658acde684e4491b3b1c3e" + } + ] +} diff --git a/research/six-frame-seed-cut/TASK.json b/research/six-frame-seed-cut/TASK.json new file mode 100644 index 0000000000..4c48aeffcb --- /dev/null +++ b/research/six-frame-seed-cut/TASK.json @@ -0,0 +1,90 @@ +{ + "schema_version": 1, + "task_id": "bit-new-register-model", + "priority_revision": 8, + "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "original_card": { + "id": "bit-new-register-model", + "question": "Can an explicitly larger or nonabelian register model escape the scoped three-register obstruction?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/bit-three-register-lower-bound/README.md", + "certificates/selected-result.json", + "research/bit-gl3-mixed-targets-length10/README.md", + "docs/research/community-efficient1000-review.md" + ], + "methods": [ + "Construct the smallest exact identity in a newly specified legal operation alphabet.", + "Derive a target-specific relaxation bound for that same explicit alphabet." + ], + "acceptance_gate": "Name the changed hypothesis, all counted roles and a uniform identity; finite column tests alone do not certify it. 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": "Resolve the current selected review, separate complex/ordinary BIT/admitted BIT/outer budgets, and compare the card against live handoffs before starting. Historical ceilings require exact source/model equivalence.", + "scope": "Source-binding orientation only; not a scientific replay or all-size proof. Materialize selected inputs if this checkout is sparse." + }, + "first_experiment": "First compare the alphabet, role count and length with the fully replayed #1974 census and #2027 mixed-root tariff. Identify a changed premise and a legal native implementation; then price one smallest completed instance before searching larger words.", + "bottleneck_link": "A small-width completed saving changes the bit primitive; a finite-address identity alone is insufficient.", + "allowed_variations": [ + "Choose a fixed larger register count or a specified nonabelian operation family." + ], + "scope_change_triggers": [ + "Remaining inside the already-excluded three-register abelian model.", + "Repeating the two-register GL3 census or a covered three-register length without changing a hypothesis; a formal group-algebra word without native conversion is a partial result." + ], + "overlap_terms": [ + "three-register", + "nonabelian", + "group algebra" + ] + }, + "scope_status": "changed", + "actual_scope": "Prove a sharp rank-mass obstruction s >= 2W for arbitrary deterministic finite-alphabet permutation circuits whose rational two-dimensional frames lie in {0,I,J,J+I,B,B+I}, the seed proposed by PR1757 with its identity translates.", + "scope_change_reason": "The current card suggests a larger/nonabelian register alphabet. The live source question in PR1757 instead supplies a specific non-common-flag rational frame seed and asks for a five-role cost at most nine. This contribution changes to a source-specific alphabet obstruction using its cited weighted partition theorem, not another three-register census.", + "bottleneck_link": "Scoped side result for the search for a contracting nonlinear finite shear circuit. It rules out the proposed six-frame seed at every circuit size and therefore prevents further topology search inside this alphabet from beating its rank-mass bill. It supplies no BIT or complex supplier.", + "budget_minutes": 60, + "stop_rule": "Ship the first new exact cut certificate after a written proof and bounded local replay; do not enlarge the frame alphabet or seek a stronger theorem.", + "outcome": "completed", + "evidence": "README.md proves s >= 2W by applying PR1757 to the two explicitly certified binary partitions. verify.py checks 36 ordered exact ranks with two rank algorithms, all three identity shifts, all 4096 binary-pair label assignments, and 11 rejecting controls. Receipts are computed on stdout and bind all five package files and the predecessor bytes.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Which additional rational frame destroys the two-cut certificate while retaining an attainable five-role cost at most nine?", + "why_it_matters": "Non-common-flag geometry alone does not escape this new alphabet-specific obstruction. A changed frame alphabet is necessary before the source topology search can succeed.", + "first_step": "Add one proposed rational frame to the six-frame distance table, include every available identity-shift demand, and solve the weighted partition feasibility problem before searching circuit words.", + "blocked_by": "Failure of this particular two-cut certificate is not a construction or a proof that no other weighted cut certificate exists." + }, + { + "question": "Can a complete nonlinear permutation circuit outside this alphabet achieve s < 2W?", + "why_it_matters": "Such a witness would move beyond both the common-flag class and the newly excluded seed, and is a prerequisite for a favorable optimistic concave rank bill.", + "first_step": "Publish one finite DAG with full truth-table semantics, one common rational frame per gate, every physical edge and the exact source/sink identity shifts.", + "blocked_by": "The present result supplies no changed-alphabet circuit, physical supplier, compiler or complete invoice." + } + ], + "source_question": { + "pr": 1757, + "author": "jmbarrancoml", + "path": "research/nonlinear-frame-cut-bound/README.md", + "section": "Open next questions" + }, + "coordination": { + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19219986", + "upstream_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "priority_revision": 8, + "checked_at_utc": "2026-10-27T15:17:18.417247+00:00", + "coverage": "Live open PR bodies and discussions through the overlap cache; all main README paths additionally searched by git grep. Arbitrary code diffs and unpublished work are not covered." + }, + "environment": { + "python": "3.12.15", + "implementation": "CPython", + "system": "Darwin", + "machine": "arm64" + }, + "claim_type": "scoped mathematical proof with exact finite certificate" +} diff --git a/research/six-frame-seed-cut/VERIFY.json b/research/six-frame-seed-cut/VERIFY.json new file mode 100644 index 0000000000..91f1ebb6e8 --- /dev/null +++ b/research/six-frame-seed-cut/VERIFY.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/nonlinear-frame-cut-bound/README.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 30, + "checks": "Exact six-frame cut certificate, separate rational rank oracle, complete two-bit label enumeration, identity endpoints, no-common-flag witness and eleven rejection controls; stdout receipt binds package/source bytes." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 30, + "checks": "Same full finite certificate and rejecting controls with assertions disabled." + } + ] +} diff --git a/research/six-frame-seed-cut/verify.py b/research/six-frame-seed-cut/verify.py new file mode 100644 index 0000000000..b740ca6709 --- /dev/null +++ b/research/six-frame-seed-cut/verify.py @@ -0,0 +1,174 @@ +#!/usr/bin/env python3 +"""Check the new six-frame cut certificate; do not replay predecessor circuits.""" + +from fractions import Fraction +from hashlib import sha256 +from itertools import product +import json +from pathlib import Path +import sys + + +ZERO = (0, 0, 0, 0) +IDENTITY = (1, 0, 0, 1) +J = (0, 1, -1, 0) +B = (0, 0, -1, 1) +FRAMES = (ZERO, IDENTITY, J, (1, 1, -1, 1), B, (1, 0, -1, 2)) +LABELS = ((0, 0), (1, 1), (0, 0), (1, 1), (0, 1), (1, 0)) +FILES = ("README.md", "TASK.json", "SOURCES.json", "VERIFY.json", "verify.py") +SOURCE = "research/nonlinear-frame-cut-bound/README.md" +SOURCE_HASH = "411b78a56180e835bb97e59b9845968d84ad3fb8f5658acde684e4491b3b1c3e" + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def difference(left, right): + return tuple(left[i] - right[i] for i in range(4)) + + +def determinant(matrix): + return matrix[0] * matrix[3] - matrix[1] * matrix[2] + + +def rank(matrix): + return 2 if determinant(matrix) else int(any(matrix)) + + +def elimination_rank(matrix): + """A separate rational elimination oracle for the 2-by-2 differences.""" + rows = [[Fraction(matrix[2 * i + j]) for j in range(2)] for i in range(2)] + pivots = 0 + for column in range(2): + candidates = [i for i in range(pivots, 2) if rows[i][column]] + if not candidates: + continue + pivot = candidates[0] + rows[pivots], rows[pivot] = rows[pivot], rows[pivots] + scale = rows[pivots][column] + rows[pivots] = [entry / scale for entry in rows[pivots]] + for i in range(2): + if i != pivots: + scale = rows[i][column] + rows[i] = [rows[i][j] - scale * rows[pivots][j] for j in range(2)] + pivots += 1 + return pivots + + +def multiply(left, right): + return tuple(sum(left[2 * i + k] * right[2 * k + j] for k in range(2)) + for i in range(2) for j in range(2)) + + +def hamming(left, right): + return sum(left[i] != right[i] for i in range(2)) + + +def check_certificate(labels, ranks, demands): + require(len(labels) == 6, "six labels required") + require(all(len(label) == 2 for label in labels), "two bits per label required") + require(all(type(bit) is int and bit in (0, 1) for label in labels for bit in label), + "labels must contain integer bits") + require(len(ranks) == 6 and all(len(row) == 6 for row in ranks), "rank table shape") + require(all(type(ranks[i][j]) is int and 0 <= ranks[i][j] <= 2 + for i in range(6) for j in range(6)), "rank range") + for i in range(6): + for j in range(6): + require(hamming(labels[i], labels[j]) <= ranks[i][j], "edge budget") + require(tuple(demands) == ((0, 1), (2, 3), (4, 5)), "complete identity demands") + for i, j in demands: + require(hamming(labels[i], labels[j]) == 2, "endpoint separation") + + +def check_algebra(): + require(len(set(FRAMES)) == 6, "distinct frames") + for i in (0, 2, 4): + require(difference(FRAMES[i + 1], FRAMES[i]) == IDENTITY, "identity translate") + ranks = tuple(tuple(rank(difference(a, b)) for b in FRAMES) for a in FRAMES) + for i in range(6): + for j in range(6): + require(ranks[i][j] == elimination_rank(difference(FRAMES[i], FRAMES[j])), + "independent rank oracle") + demands = tuple((i, j) for i in range(6) for j in range(6) + if difference(FRAMES[j], FRAMES[i]) == IDENTITY) + commutator = difference(multiply(J, B), multiply(B, J)) + require(commutator == (-1, 1, 1, 1), "commutator entries") + require(determinant(commutator) == -2, "no common invariant line") + check_certificate(LABELS, ranks, demands) + return ranks, demands + + +def enumerate_labels(ranks, demands): + """Enumerate all 4^6 assignments, including translated/complemented cuts.""" + solutions = [] + bits = tuple(product((0, 1), repeat=2)) + checked = 0 + for labels in product(bits, repeat=6): + checked += 1 + if not all(hamming(labels[i], labels[j]) == 2 for i, j in demands): + continue + if all(hamming(labels[i], labels[j]) <= ranks[i][j] + for i in range(6) for j in range(6)): + solutions.append(labels) + require(checked == 4096, "complete finite label domain") + require(len(solutions) == 16 and LABELS in solutions, "attaining cut assignments") + return checked, len(solutions) + + +def rejection_controls(ranks, demands): + bad_labels = [LABELS[:5], ((0,),) + LABELS[1:], ((False, 0),) + LABELS[1:]] + bad_labels += [((2, 0),) + LABELS[1:]] + for i, j in ((1, 0), (4, 3), (5, 3)): + changed = list(LABELS) + changed[i] = ((j >> 1) & 1, j & 1) + bad_labels.append(tuple(changed)) + cases = [(labels, ranks, demands) for labels in bad_labels] + for i, j in ((0, 1), (0, 4)): + changed = [list(row) for row in ranks] + changed[i][j] -= 1 + cases.append((LABELS, changed, demands)) + cases += [(LABELS, ranks, demands[:2]), (LABELS, ranks, tuple(reversed(demands)))] + for labels, table, endpoints in cases: + try: + check_certificate(labels, table, endpoints) + except ValueError: + continue + raise ValueError("a corrupt certificate was accepted") + return len(cases) + + +def receipt(package, ranks, checked, solutions, controls): + source = package.parent.parent / SOURCE + require(sha256(source.read_bytes()).hexdigest() == SOURCE_HASH, "source bytes changed") + hashes = {name: sha256((package / name).read_bytes()).hexdigest() for name in FILES} + return { + "status": "PASS_SIX_FRAME_SEED_CUT", + "claim_type": "scoped mathematical proof with exact finite certificate", + "rank_table": ranks, + "labels": LABELS, + "ordered_rank_pairs": 36, + "identity_shift_demands": 3, + "label_assignments_enumerated": checked, + "valid_two_cut_assignments": solutions, + "rejection_controls": controls, + "five_role_lower_bound": 10, + "rank_mass_bound": "s >= 2W", + "commutator_determinant": -2, + "source_sha256": SOURCE_HASH, + "package_sha256": hashes, + } + + +def main(): + require(len(sys.argv) == 1, "no arguments are accepted") + ranks, demands = check_algebra() + checked, solutions = enumerate_labels(ranks, demands) + controls = rejection_controls(ranks, demands) + print(json.dumps(receipt(Path(__file__).resolve().parent, ranks, checked, + solutions, controls), indent=2, sort_keys=True)) + + +if __name__ == "__main__": + main()