From e0e612423820b8a46025deb3eb776729d9e6d940 Mon Sep 17 00:00:00 2001 From: Cursor Agent Date: Thu, 22 Oct 2026 13:33:39 +0000 Subject: [PATCH] Show the short-field movement does not tighten the Strassen boundary row. Substitute the proved layout count into #4100's written boundary density. At tau=45/16 the movement saving exceeds the boundary saving by 13/32, and the charge is absorbed without setting the exposed length equal to W or B. Co-authored-by: unpaidmoon --- research/pr4100-row-field-ledger/PROOF.md | 127 ++++++++++++++ research/pr4100-row-field-ledger/README.md | 95 ++++++++++ research/pr4100-row-field-ledger/SOURCES.json | 54 ++++++ research/pr4100-row-field-ledger/TASK.json | 80 +++++++++ research/pr4100-row-field-ledger/VERIFY.json | 25 +++ research/pr4100-row-field-ledger/verify.py | 163 ++++++++++++++++++ 6 files changed, 544 insertions(+) create mode 100644 research/pr4100-row-field-ledger/PROOF.md create mode 100644 research/pr4100-row-field-ledger/README.md create mode 100644 research/pr4100-row-field-ledger/SOURCES.json create mode 100644 research/pr4100-row-field-ledger/TASK.json create mode 100644 research/pr4100-row-field-ledger/VERIFY.json create mode 100644 research/pr4100-row-field-ledger/verify.py diff --git a/research/pr4100-row-field-ledger/PROOF.md b/research/pr4100-row-field-ledger/PROOF.md new file mode 100644 index 0000000000..a91c302f3a --- /dev/null +++ b/research/pr4100-row-field-ledger/PROOF.md @@ -0,0 +1,127 @@ +# Short-field movement sits above the Strassen boundary row + +Scoped substitution for one open question of +`research/pr4100-row-field-movement`. No new κ. #4100 is not accepted. +The selected record is unchanged. + +## What is substituted + +Lemma 3 of that package says that exposing one field of length `a ≥ 1` +and real volume `V` moves strictly fewer than + +```text +8 · max(1, ceil(log2 a)) · V +``` + +records on the forward-plus-undo schedule. The #4100 boundary sentence +already charges + +```text +O(V d W^(tau-1)/B polylog(p)), tau = 45/16, +``` + +and the same paragraph's union movement is + +```text +O(V d W/B polylog(p)). +``` + +PHASE-LAYOUT charges the layout itself as `O(log p)` times the boundary +volume, not a transpose of the long spectator field. The open question +was whether that count becomes the Strassen sentence only after the +exposed length is set equal to the carving parameters `W` and `B`. + +## Pinned lengths + +Two lengths are named. Neither is the equality `a = W` or `a = B`. + +- FINE-PRIME.md and GAUSSIAN.md set `W = O(sqrt(p) polylog p)`. The + boundary-row field in PHASE-LAYOUT is that polynomial-width row, so + this reading has `a = O(p^{1/2} polylog p)`. +- If the exposed field is instead the whole carved line, CAPPED-SIGNOFF + gives `|E_i| = O(L W/B polylog p + W polylog p)`, and GAUSSIAN.md sets + `L = 2^{ceil(400 log2 p)}`. Then `a` is still `p^{O(1)}`. + +In both readings `ceil(log2 a) = O(log p)`. Lemma 3 therefore multiplies +the volume it actually exposes by a polylogarithmic factor. It does not +change a `W` power. + +The volume it exposes is the boundary volume. GAUSSIAN.md gives that set +density `O(W/B polylog(p))`, and FINE-PRIME.md §6 keeps the cost power +`epsilon - xi + (tau-1)/2` because the density is still `W/B`. UNION-SCHEDULE +records the same density as `mu = O((W/B) polylog p)`. + +## Exponent comparison + +FINE-PRIME.md §6–§7 uses one dictionary. A term + +```text +O(V (d/B) W^alpha polylog p) +``` + +has cost power `epsilon - xi + alpha/2` and saving +`1 - epsilon + xi - alpha/2`, because the worst-case bandwidth in that +section satisfies `log_p W = 1/2`. That is why the printed union row +(`alpha = 1`) has saving `xi + 1/2 - epsilon`, and the printed Strassen +row (`alpha = tau - 1`) has saving `c + xi - epsilon` with +`c = (3 - tau)/2`. + +Lemma 3, on the boundary volume, is the `alpha = 1` shape: the extra +`ceil(log2 a)` factor is inside the polylog already written on the union +sentence `O(V d W/B polylog(p))`. Its saving exceeds the Strassen saving by + +```text +(xi + 1/2 - epsilon) - (c + xi - epsilon) = 1/2 - c = (tau - 2)/2. +``` + +The difference does not depend on `epsilon` or `xi`. For the stated +`tau = 45/16`, one has `c = 3/32` and + +```text +1/2 - 3/32 = 13/32. +``` + +`W = O(sqrt(p) polylog p)` contributes `o(1)` beyond the printed `1/2`, +because `(log p)^k = p^{o(1)}`. A constant gap of `13/32` stays positive +for all large `p`. This note does not compute that finite threshold; an +explicit density constant would be needed for one. A separate movement +row would still save `13/32 - o(1)` more than the Strassen boundary row, +so it does not become the minimum. At the explicit §7 balance +(`s = 10^{-64}`, boundary saving `= epsilon q + s`), the printed-power +movement saving is that boundary saving plus `13/32`. + +The same arithmetic gives the monomial comparison used by the big-O. +For every integer `W ≥ 1`, + +```text +W^{29} ≥ W^{16}, +``` + +so `W^{29/16} ≥ W`, and `W^{tau-1} ≥ W` at `tau = 45/16`. A movement of +shape `K V (d/B) W (log p)^k` is at most `K (log p)^k` times the monomial +inside `O(V d W^{tau-1}/B polylog p)`. The layout factor is absorbed by +the polylog of the boundary sentence. It is not necessary to set `a` +equal to `W` or to `B`. + +For the other printed exponent `tau_eff = 2 + 10^{-64}`, the same +difference is `(tau_eff - 2)/2 = 5 · 10^{-65} > 0`, and `W^{tau_eff-1} ≥ W` +for every integer `W ≥ 1`. Absorption holds for that exponent too. Which +of the two exponents the ledger should state is a separate question. + +## The density is necessary + +If Lemma 3 were charged on the full tensor volume instead of the boundary +volume, the `W/B` factor would drop out and the saving would fall to +`1 - epsilon`. At the §7 parameters `epsilon = 9999999/10000000`, that +saving is strictly smaller than the headline `epsilon q`. The boundary +density is what keeps the movement off the binding row. The proof does +not rerun the carving program that produces the density; it uses the +density #4100 already writes. + +## Not proved + +This note does not prove the Strassen count, the seven-product circuit, +conditioning, the row gap, or the choice between `tau = 45/16` and +`tau_eff`. It does not replay the dyadic carving. It does not accept +#4100 or change the selected exponent. The `O` constants inside the +written density are not replaced by explicit integers. diff --git a/research/pr4100-row-field-ledger/README.md b/research/pr4100-row-field-ledger/README.md new file mode 100644 index 0000000000..5f1fe4d4fb --- /dev/null +++ b/research/pr4100-row-field-ledger/README.md @@ -0,0 +1,95 @@ +# Short-field movement does not tighten the Strassen boundary row + +**Scoped exponent comparison. No new κ.** #4100 is not accepted, and the +selected conditional result stays `0.00302015`. + +## Scope and evidence + +Card `uniform-transfer-audit`, scope **refined** to one substitution left +open by the boundary-arithmetic layout lemma. That lemma bounds one exposed +field by `8 max(1, ceil(log2 a))` times its real volume. #4100 already +writes the Strassen boundary cost + +```text +O(V d W^(tau-1)/B polylog(p)), tau = 45/16, +``` + +and the union movement `O(V d W/B polylog(p))`. This package compares those +two shapes after the layout factor is included. It does not replay the +carving program. + +[PROOF.md](PROOF.md) records the argument. In the exponent dictionary of +FINE-PRIME.md §6–§7, a term `O(V (d/B) W^alpha polylog p)` has saving +`1 - epsilon + xi - alpha/2`. The layout movement is the `alpha = 1` shape, +because `ceil(log2 a) = O(log p)` for both named lengths: the +polynomial-width boundary row, using `W = O(sqrt(p) polylog p)`, and the +carved line `|E_i| = O(L W/B polylog p + W polylog p)` with +`L = 2^{ceil(400 log2 p)}`. Its saving exceeds the Strassen saving by + +```text +1/2 - (3 - tau)/2 = 13/32 +``` + +at `tau = 45/16`. The difference does not depend on `epsilon` or `xi`. +The printed `1/2` is the worst-case `log_p W`; a polylogarithmic factor +in `W` adds only `o(1)`, which does not close `13/32` for large `p`. +For every integer `W ≥ 1`, `W^{29} ≥ W^{16}`, so +`W^{tau-1} ≥ W` and the movement monomial is absorbed by the boundary +big-O. The exposed length is not set equal to `W` or to `B`. + +The same gap is `5 · 10^{-65}` at the other printed exponent +`tau_eff = 2 + 10^{-64}`. Both exponents absorb the movement. Choosing +which exponent the ledger states is left open. + +Charging the same logarithm on the full tensor volume, dropping the +written density `O(W/B polylog p)`, would leave saving `1 - epsilon`. +At the §7 parameters that quantity is strictly below the headline +`epsilon q`. The density is what keeps this charge off the binding row. + +`verify.py` recomputes the rational identities, the integer bandwidth +comparison for `W = 1..256` and two larger widths, the named core-length +logarithm, and the two rejecting controls (`tau = 2` is not strict; +`tau = 7/4` makes movement the heavier row; the full-volume charge +undercuts the headline). + +## Reproduce + +From the repository root, on CPython 3.12: + +```sh +python3.12 -B scripts/research_package.py --package research/pr4100-row-field-ledger --check-only +python3.12 -B scripts/research_package.py --package research/pr4100-row-field-ledger +``` + +The registered command is `verify.py`. It uses the standard library and +reads the pinned prose inputs. Expected first line: + +```text +PASS_ROW_FIELD_LEDGER tau=45/16 c=3/32 movement_minus_boundary_saving=13/32 gap_independent_of_epsilon_and_xi=true integer_bandwidth_absorbed=true tau_eff_gap=5e-65 full_volume_charge_binds=true boundary_volume_charge_binds=false exposed_length_equals_W_or_B=false selected_decimal=0.00302015 no_new_kappa=true +``` + +## Open next questions + +1. **Choose the boundary exponent.** GAUSSIAN.md uses `tau = 45/16` for the + seven-product paragraph, while UNION-SCHEDULE §4 uses + `tau_eff = 2 + 10^{-64}`. Both absorb this movement. The ledger row + still has to name one of them before the layout lemma is copied in as + a numeric coefficient. First compare those two sentences with the + generated ledger at head `337d04939571a637aeab54a0f58f54fde811663a`. + Blocked here because that ledger is a different program. +2. **Extract the density constant.** The `O(W/B polylog p)` factor is used + as written. An explicit `C` such that `mu ≤ C (W/B) (log p)^k` would + turn the `13/32` gap into a finite-`p` inequality. First pin `C` and + `k` from the carving proof, not from another asymptotic sentence. + +## Credit + +The boundary and union sentences are Cinna Davis's #4100. The layout lemma +is `research/pr4100-row-field-movement` (unpaidmoon). The exponent table is +FINE-PRIME.md §6–§7, and the carved-line bound is CAPPED-SIGNOFF.md. The +coverage map that listed the row-field movement as unaudited is PR #4311 +(Ryanson Jonathan). PR #4376 proved the layout count and left this +substitution open. + +Prepared by unpaidmoon with substantial Cursor Grok assistance. Apache-2.0. +No independent human review and no formal-kernel acceptance are claimed. diff --git a/research/pr4100-row-field-ledger/SOURCES.json b/research/pr4100-row-field-ledger/SOURCES.json new file mode 100644 index 0000000000..a292dd1b04 --- /dev/null +++ b/research/pr4100-row-field-ledger/SOURCES.json @@ -0,0 +1,54 @@ +{ + "schema_version": 1, + "base_commit": "fbc9ea0249746acca4f504d4fda2b84e0e36cf0d", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395", + "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "research/capped-phase-fusion/CAPPED-SIGNOFF.md", + "usage": "input", + "git_blob": "fc3456387b9399c8108db75b46088f85c5c26f82", + "sha256": "70e9175ebde200f8b016236adc88c4a1c4858945e7c3e5c453a8b6a5f79a263a" + }, + { + "path": "research/capped-phase-fusion/PHASE-LAYOUT-AUDIT.md", + "usage": "input", + "git_blob": "bbeeee7431720817f031360f67b2186abac5cd23", + "sha256": "54aafc7afd09fe1a5312e69fad09c87422690543ab75c6ae35f6cbcc26b3eb8a" + }, + { + "path": "research/pr4100-row-field-movement/PROOF.md", + "usage": "input", + "git_blob": "8cb9097d216677e218c5e59d9d6e7e77801e8727", + "sha256": "9b20f66269383535d20f1f0a762710a393ea036471a9383b7dafc07db341d02b" + }, + { + "path": "research/unconditional-batched-crt/GAUSSIAN.md", + "usage": "input", + "git_blob": "adfb28c93e6b06178c901caaac39ede41a9e541b", + "sha256": "2f63c91c58f2d1cf31294812c75970ea390c61866a8da7ed700d4316a033a242" + }, + { + "path": "research/unconditional-batched-crt/vendor/FINE-PRIME.md", + "usage": "input", + "git_blob": "bf9899ee21be4058e4aac0b64bfa67d01ee8ddd3", + "sha256": "47d1b1b4df28aadda3cd6bdeb1fbc47290595e9208cd09c1a1f338520d33fdce" + }, + { + "path": "research/unconditional-batched-crt/vendor/UNION-SCHEDULE.md", + "usage": "input", + "git_blob": "b5eb03e6745804f465a536fc9ffa87c2515d1bfa", + "sha256": "aabb28c343bcb9697a4cac7058060132617073df17ee18e591d2bf4defe9e921" + } + ] +} diff --git a/research/pr4100-row-field-ledger/TASK.json b/research/pr4100-row-field-ledger/TASK.json new file mode 100644 index 0000000000..97cee0d797 --- /dev/null +++ b/research/pr4100-row-field-ledger/TASK.json @@ -0,0 +1,80 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 7, + "base_commit": "fbc9ea0249746acca4f504d4fda2b84e0e36cf0d", + "original_card": { + "id": "uniform-transfer-audit", + "question": "Does one quantified step of the proposed #4100 all-size construction hold at its actual caller?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/unconditional-batched-crt/README.md" + ], + "methods": [ + "Prove one missing implication with explicit quantified hypotheses.", + "Find an exact counterexample at the claimed interface boundary." + ], + "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_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read PROOF.md and AUDIT.md in #4100. Select one distinct obligation: CRT total repair, native/free-algebra lifting, precision/conditioning, or complete fixed-tape cost. This is an author-submitted proof, not an accepted unconditional theorem.", + "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately." + }, + "first_experiment": "Check live handoffs; name one proposition, its caller, quantified domain and dependency closure. Independently prove the implication or exhibit a precise gap/counterexample. Prioritize CRT.md total repair or COMPLEX.md free-algebra lift only if unclaimed. Stop at the chosen obligation; do not substitute finite samples or root arithmetic for an all-size proof, or launch the complete package by default.", + "bottleneck_link": "Finite supplier improvements are useful only under the retained transfer obligations.", + "allowed_variations": [ + "One CRT repair, native lift, precision/conditioning or tape-cost proposition, with its exact caller." + ], + "scope_change_triggers": [ + "Replacing a quantified obligation with another finite smoke test.", + "Treating archive intake, an author PASS receipt or a finite composed fixture as discharge of the universal hypotheses." + ], + "overlap_terms": [ + "uniform transfer", + "all-size", + "precision", + "4100", + "unconditional-batched-crt" + ], + "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_status": "refined", + "actual_scope": "Substitute the proved short-field move count into #4100's Strassen boundary cost O(V d W^(tau-1)/B polylog p) at tau=45/16, using the written boundary density, and decide whether that charge tightens the boundary row.", + "scope_change_reason": "PR #4376 proved the layout count and left the ledger substitution open. The coverage map listed the row-field movement as unaudited obligation 3; this package answers that obligation's first remaining question and does not reopen the move-count proof.", + "bottleneck_link": "Side result for the #4100 admission audit: the layout movement does not undercut the Strassen boundary row, so it is not a new obstruction to the proposed exponent. It does not move the selected frontier.", + "budget_minutes": 60, + "stop_rule": "Stop after the exponent comparison and the integer absorption check. Do not choose between tau=45/16 and tau_eff, and do not replay the carving program.", + "outcome": "completed", + "evidence": "PROOF.md derives the 13/32 saving gap. verify.py checks the rational identities, the integer bandwidth comparison, the source sentences, and the full-volume rejecting control.", + "author": "unpaidmoon", + "ai_assistance": "Prepared by unpaidmoon with substantial Cursor Grok assistance.", + "open_questions": [ + { + "question": "Which printed boundary exponent, tau=45/16 or tau_eff=2+10^{-64}, does the #4100 ledger use when the layout lemma is copied in?", + "why_it_matters": "Both absorb this movement, but the numeric boundary row still has to name one exponent.", + "first_step": "Compare GAUSSIAN.md's seven-product sentence with UNION-SCHEDULE section 4 against the generated ledger at head 337d04939571a637aeab54a0f58f54fde811663a.", + "blocked_by": "The generated ledger is a different program and is not replayed here." + }, + { + "question": "What explicit C and k satisfy mu <= C (W/B) (log p)^k in the carving proof?", + "why_it_matters": "An explicit constant would turn the 13/32 exponent gap into a finite-p inequality.", + "first_step": "Pin C and k from the carving argument rather than from another asymptotic sentence.", + "blocked_by": "The carving program is not replayed here; the written O bound is the input." + } + ] +} diff --git a/research/pr4100-row-field-ledger/VERIFY.json b/research/pr4100-row-field-ledger/VERIFY.json new file mode 100644 index 0000000000..88245f2baf --- /dev/null +++ b/research/pr4100-row-field-ledger/VERIFY.json @@ -0,0 +1,25 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/capped-phase-fusion/CAPPED-SIGNOFF.md", + "research/capped-phase-fusion/PHASE-LAYOUT-AUDIT.md", + "research/pr4100-row-field-movement/PROOF.md", + "research/unconditional-batched-crt/GAUSSIAN.md", + "research/unconditional-batched-crt/vendor/FINE-PRIME.md", + "research/unconditional-batched-crt/vendor/UNION-SCHEDULE.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Exact 13/32 saving gap at tau=45/16; integer check W^(tau-1) >= W; tau_eff gap; full-volume charge undercuts the headline; source-sentence binding; rejection controls for tau=2 and tau=7/4." + } + ] +} diff --git a/research/pr4100-row-field-ledger/verify.py b/research/pr4100-row-field-ledger/verify.py new file mode 100644 index 0000000000..0803154047 --- /dev/null +++ b/research/pr4100-row-field-ledger/verify.py @@ -0,0 +1,163 @@ +#!/usr/bin/env python3 +"""Check the short-field movement against #4100's Strassen boundary row. + +The all-size comparison is the exponent identity in PROOF.md. This program +recomputes that identity in exact rationals, checks the integer form of +W^(tau-1) >= W, and rejects the two mis-charges named in the proof. +""" + +from __future__ import annotations + +import json +import re +from fractions import Fraction +from pathlib import Path + + +ROOT = Path(__file__).resolve().parents[2] + + +def require(condition: bool, message: str) -> None: + if not condition: + raise AssertionError(message) + + +def text(path: str) -> str: + return (ROOT / path).read_text(encoding="utf-8") + + +def require_phrase(document: str, phrase: str, source: str) -> None: + require(phrase in document, f"{source} no longer contains {phrase!r}") + + +def ceil_log2(value: int) -> int: + require(value >= 1, "log argument must be positive") + exponent = 0 + power = 1 + while power < value: + power *= 2 + exponent += 1 + return exponent + + +def saving_gap(tau: Fraction) -> Fraction: + """Movement saving minus Strassen saving, in the FINE-PRIME dictionary.""" + return (tau - 2) / 2 + + +def monomial_absorbs(width: int, tau: Fraction) -> bool: + """True when W^(tau-1) >= W for this integer width.""" + require(width >= 1, "bandwidth must be a positive integer") + if tau == Fraction(45, 16): + return width**29 >= width**16 + if tau == Fraction(7, 4): + # W^{3/4} >= W if and only if W <= 1. + return width**3 >= width**4 + if tau >= 2: + return True + return False + + +def main() -> None: + gaussian = text("research/unconditional-batched-crt/GAUSSIAN.md") + fine = text("research/unconditional-batched-crt/vendor/FINE-PRIME.md") + union = text("research/unconditional-batched-crt/vendor/UNION-SCHEDULE.md") + signoff = text("research/capped-phase-fusion/CAPPED-SIGNOFF.md") + phase = text("research/capped-phase-fusion/PHASE-LAYOUT-AUDIT.md") + lemma = text("research/pr4100-row-field-movement/PROOF.md") + selected = json.loads(text("certificates/selected-result.json")) + + require_phrase(gaussian, "7^16<2^45 gives exponent tau=45/16", "GAUSSIAN.md") + require_phrase(gaussian, "O(V d W^(tau-1)/B polylog(p)).", "GAUSSIAN.md") + require_phrase(gaussian, "O(V d W/B polylog(p)).", "GAUSSIAN.md") + require_phrase(gaussian, "L=2^ceil(400log2 p)", "GAUSSIAN.md") + require_phrase(gaussian, "W=O(sqrt(p)polylog(p)) headline, "boundary-volume movement undercut the headline") + + # The named core length is polynomial: L = 2^{ceil(400 log2 p)} <= (2p)^400. + for prime_power in (2, 3, 10, 100, 1000, 10**6): + length = 1 << ceil_log2(prime_power) + require(length <= 2 * prime_power, "next power of two exceeded 2p") + core = 1 << (400 * ceil_log2(prime_power)) + exposed = core * prime_power + require( + ceil_log2(exposed) <= 401 * ceil_log2(prime_power), + "exposed-line logarithm was not O(log p)", + ) + + decimal = selected["decimal"] + require(decimal == "0.00302015", "pinned selected decimal changed; re-read the record before quoting it") + print( + "PASS_ROW_FIELD_LEDGER " + "tau=45/16 " + "c=3/32 " + "movement_minus_boundary_saving=13/32 " + "gap_independent_of_epsilon_and_xi=true " + "integer_bandwidth_absorbed=true " + "tau_eff_gap=5e-65 " + "full_volume_charge_binds=true " + "boundary_volume_charge_binds=false " + "exposed_length_equals_W_or_B=false " + f"selected_decimal={decimal} " + "no_new_kappa=true" + ) + + +if __name__ == "__main__": + main()