diff --git a/research/p104-minimum-tail-block/ORIGINS.json b/research/p104-minimum-tail-block/ORIGINS.json new file mode 100644 index 0000000000..1c5470968e --- /dev/null +++ b/research/p104-minimum-tail-block/ORIGINS.json @@ -0,0 +1,29 @@ +{ + "repository": "CrocSwap/integer-mult-bounds", + "pull_request": 5775, + "head": "56dc0a9ec02020f5e035c7d83f078fb2b27ac76a", + "files": [ + { + "retained_path": "premises/RESULT.json", + "source_path": "research/p104-tail-feasible-envelope/RESULT.json", + "git_blob": "a30006be845abb830d4c9f953c828a4b2444fe0a", + "sha256": "bd8b2572ba9d64421dfef00440ae2f5e7f7d0c98875111e4d29ac4eb63e55531", + "url": "https://github.com/CrocSwap/integer-mult-bounds/blob/56dc0a9ec02020f5e035c7d83f078fb2b27ac76a/research/p104-tail-feasible-envelope/RESULT.json" + }, + { + "retained_path": "premises/PROOF.md", + "source_path": "research/p104-tail-feasible-envelope/PROOF.md", + "git_blob": "5611eb8f8611d9dd2c7748d163b0db540ebe2831", + "sha256": "39c32069071950dbbb65211c4b857291d92103d7801b70eec78667a0c8e397e7", + "url": "https://github.com/CrocSwap/integer-mult-bounds/blob/56dc0a9ec02020f5e035c7d83f078fb2b27ac76a/research/p104-tail-feasible-envelope/PROOF.md" + }, + { + "retained_path": "premises/INVOICE.json", + "source_path": "research/p104-tail-feasible-envelope/inputs/RESULT.json", + "git_blob": "9d47144bd99dc57d799345c940232eb26afdc33c", + "sha256": "062fb71b92ca620cbea4a4469458ede513e4dc1039bfa783e06ed11f51335a9e", + "url": "https://github.com/CrocSwap/integer-mult-bounds/blob/56dc0a9ec02020f5e035c7d83f078fb2b27ac76a/research/p104-tail-feasible-envelope/inputs/RESULT.json" + } + ], + "use": "Cited mathematical premises, retained verbatim; predecessor theorem not replayed." +} diff --git a/research/p104-minimum-tail-block/PROOF.md b/research/p104-minimum-tail-block/PROOF.md new file mode 100644 index 0000000000..b852d4945c --- /dev/null +++ b/research/p104-minimum-tail-block/PROOF.md @@ -0,0 +1,124 @@ +# A sharp minimum block exponent + +## Statement and inherited premises + +Fix the complete PR5756 paid and target histograms `P_r,T_r`, with +`C = 622627591/200000000000`, `t=1-C`, +`T = sum_r T_r r^t`, and `N = sum_r T_r = 13390`. Define + +```text +g(c,u) = sum_r P_r r^(t+u) / (c^u T), +d(c,b) = N b / (c^C T). +``` + +The declared gate family has integers `L>=3`, `c>=1`, `b>=1`, real `u>0`, +and rational `0=112`. At `L=112`, its unique integer +cutoff/floor pair is `(16,17)`. An explicit witness is + +```text +L=112, c=16, b=17, u=1/7, rho=1951/2000. +``` + +The theorem remains true if `L` must be even or if `u` must be rational. + +Ali Romman's [PR5775](https://github.com/CrocSwap/integer-mult-bounds/pull/5775), +head `56dc0a9ec02020f5e035c7d83f078fb2b27ac76a`, supplies these premises: + +| Quantity | Cited rational lower bound | +| --- | --- | +| `inf_{u>0} g(15,u)` | `983563652257169/1000000000000000` | +| `inf_{u>0} g(16,u)` | `a = 487740894096357/500000000000000` | +| `d(17,18)` | `999697814388247/1000000000000000` | +| `d(16,18)` | `999886507972867/1000000000000000` | + +Each cited lower bound is strict and exceeds `a`, except the row defining +`a` itself. The retained [result](premises/RESULT.json) and +[proof](premises/PROOF.md) specify their scope. PR5775 also retains PR5756's +[source invoice](premises/INVOICE.json), whose `strictification` records +upper bounds for `g(16,1/7)` and `d(16,17)`. Exact comparison gives + +```text +g(16,1/7) < 975485/1000000 < 1951/2000, +d(16,17) < 945/1000 < 1951/2000. +``` + +These are cited mathematical premises, not independently rederived results +of this package. `ORIGINS.json` binds the verbatim source bytes to their +repository, head, paths, Git blobs and SHA256 hashes. Authentication does not +prove the predecessor's mathematics. This contribution proves the new +block-exponent consequence of those premises. + +## Exclusion of every smaller block + +The capacity inequality implies `b>=c+1`. Indeed, `b<=c` would give +`b^(L-2)<=c^(L-2)<=c^L`, a contradiction. + +For fixed `u>0`, `g(c,u)` decreases with `c`. Thus every `c<=15` has +`g(c,u)>983563652257169/1000000000000000>a`. + +The function `d(c,b)` increases with `b`. On real `c>=1`, the derivative of +`(c+1)/c^C` has the sign of `(1-C)c-C`, which is positive since `0=17` and every capacity-compatible `b` has +`d(c,b)>=d(17,18)>a`. + +For `c=16`, every `b>=18` has `d(c,b)>=d(16,18)>a`. The only remaining +integer pair is `(16,17)`, and its paid tail is at least the cited infimum, +which exceeds `a`. Therefore every capacity-compatible pair and every +positive offset satisfy `max(g(c,u),d(c,b))>a`. + +The new exact integer comparison is + +```text +16 * 487740894096357^111 > 500000000000000^111. +``` + +It says `a^111>1/16`. Since `0=a^111>1/16`. Any passing tail choice requires `rho>a`, hence +`rho^L>1/16`. This contradicts the reserve gate. This argument covers all +cutoffs, floors, offsets and decays in the declared model. + +## A passing block and all larger blocks + +The cited upper bounds give both tail inequalities for the displayed +rational witness. The remaining new checks are integer comparisons: + +```text +16 * 1951^112 < 2000^112, +16^112 < 17^110. +``` + +These prove the strict reserve and capacity gates at length 112. For larger +`L`, the same witness still works. Its reserve `rho^L` decreases, and its +capacity ratio is `17^2*(16/17)^L`, which also decreases. The two tails are +independent of `L` in the declared family. This proves the exact feasibility +set, without an upper cutoff on `L`. + +At `L=112`, each of the other three cited lower bounds has its 112th power +strictly greater than `1/16`. The same case split therefore excludes every +integer cutoff/floor pair except `(16,17)` at the minimum. + +## Meaning and limits + +The new minimum is 16 below the predecessor's fixed length 128, a fractional +shortening of `1/8` within this gate family. This is a parameter-existence +result and a sharp obstruction below 112. It does not show that a complete +compiler can use 112, reduce carrier height, preserve another gate, or earn +a new exponent saving. Changing a block can change normalization, exit, +rounding and nonrecursive charges. Those changes require a separate complete +construction and bill. No source operator replay or predecessor audit is +part of this proof, and no physical supplier or complete multiplication theorem +follows. diff --git a/research/p104-minimum-tail-block/README.md b/research/p104-minimum-tail-block/README.md new file mode 100644 index 0000000000..4ab55a9fa2 --- /dev/null +++ b/research/p104-minimum-tail-block/README.md @@ -0,0 +1,89 @@ +# Minimum block length 112 for a fixed two-tail gate family + +The fixed PR5756 two-tail/capacity inequalities, with a variable integer block +exponent, are feasible exactly at lengths **112 and above**. At the minimum, +the unique integer cutoff/floor pair is `(16,17)`. A rational witness is +`offset=1/7`, `decay=1951/2000`. This shortens the predecessor's fixed block +length 128 by `1/8` within the stated inequality family. + +Claim type: a scoped written proof using explicitly cited scalar bounds from +Ali Romman's [PR5775](https://github.com/CrocSwap/integer-mult-bounds/pull/5775). +Those bounds are premises, not audited or independently replayed here. +[PROOF.md](PROOF.md) gives the complete model, case split and new exact integer +comparisons. The new result changes the block exponent, leaving the complete +paid/target bill and both charged tails explicit. + +A complete changed compiler, all other gates, physical realization and new +carrier-size or kappa claims remain open. The selected frontier is unchanged. +The theorem also applies when block lengths must be even or offsets rational. + +## Reproduce + +From the repository root, using standard-library CPython 3.12: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/p104-minimum-tail-block/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/p104-minimum-tail-block +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/p104-minimum-tail-block --check-source-history +``` + +Expected direct output: + +```text +PASS_MINIMUM_TAIL_BLOCK minimum=112 cutoff=16 floor=17 excluded_lengths=109 controls=10 +``` + +`VERIFY.json` registers warning-strict normal and isolated optimized commands. +The verifier uses exact rational arithmetic and integer powers. It enumerates +all 109 lengths from 3 through 111 as finite corroboration of the monotonicity +proof, checks the new witness and the unique minimal integer pair, and rejects +ten semantic or source-corruption controls. Controls distinguish the old decay, +old offset, larger completion floor, strict reserve/capacity equalities, and +unsupported lower bounds or thresholds. They do not audit the source theorem. + +The direct command is read-only and Git-free. Optional `--receipt /absolute/path` +writes a generated receipt outside this package, binding every package file to +its SHA256 and recording the actual interpreter version. No receipt is required +as an input and no handwritten receipt is supplied. `SOURCES.json` pins the +historical catalogue and selected record. `ORIGINS.json` authenticates three +verbatim predecessor files retained locally, so no unmerged Git object or +network fetch is needed to reproduce the new arithmetic. + +## Open next questions + +Can length 112 be realized by a complete charged compiler for this invoice? +First specify its changed block decomposition and rederive normalization, +exit, rounding and nonrecursive costs. Then check the remaining gates against +the exact source. The missing block rule and complete cost ledger prevent a +carrier-height or admission conclusion. [TASK.json](TASK.json) records this +question and the scope change from the independent-moment card. + +## Implementation limits + +The script has no recursion, network calls, solver, dynamic imports or local +source-module execution. File inputs have a 128 KiB cap and an exact three-file +allowlist. Its largest explicit loop has 109 iterations. Public arithmetic +checks cap finite test lengths and widths at 4096; the written theorem covers +unbounded lengths by monotonicity. Explicit exceptions remain active under +optimized Python. All functions are below 60 lines. + +Power of Ten rule 3 has a managed-runtime deviation in `verify.py`: Python's +exact integers, fractions and JSON parser allocate dynamically. The file cap, +fixed source inventory and bounded arithmetic inputs limit live data. There +are no persistent buffers or background processes. Normal and optimized runs +exercise these bounds and the invalid-input paths. A fixed-allocation port +would be needed if this offline checker were used in a real-time environment. +Python supplies no static pointer-dereference or compile-time allocation +checks; direct local values and explicit calls keep the equivalent paths +visible. The registered warning-strict replays provide recurring diagnostics. + +## Credit + +New block-threshold proof and checker produced by Nick Petalas. Credit +Ali Romman's PR5775 for the fixed-length envelope and cited scalar premises; +Joel Pulikkan / GamingPuzzled's PR5756 for the complete invoice; and the retained +Ali Romman PR5751, flyingviper PR5718, P104/native/controller and Jacob Alan +Sussman, zxv and Cao Yifan compiler lineage. The retained predecessor files +are unchanged. Elementary monotonicity and integer-power comparisons are +classical. Independent human and formal proof-kernel review are unclaimed. +Apache-2.0. diff --git a/research/p104-minimum-tail-block/SOURCES.json b/research/p104-minimum-tail-block/SOURCES.json new file mode 100644 index 0000000000..fdb80ada25 --- /dev/null +++ b/research/p104-minimum-tail-block/SOURCES.json @@ -0,0 +1,18 @@ +{ + "schema_version": 1, + "base_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8", + "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + } + ] +} diff --git a/research/p104-minimum-tail-block/TASK.json b/research/p104-minimum-tail-block/TASK.json new file mode 100644 index 0000000000..fca7a3c697 --- /dev/null +++ b/research/p104-minimum-tail-block/TASK.json @@ -0,0 +1,104 @@ +{ + "schema_version": 1, + "task_id": "independent-moment", + "priority_revision": 8, + "base_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a", + "original_card": { + "id": "independent-moment", + "question": "Does a changed construction's serialized target/paid invoice independently support its claimed improvement?", + "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", + "docs/research/recursive-invoice-preflight.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": "Demonstrate independence, source binding, positive cases and semantic failure controls. Name the existing checks and the missing coverage. More digits or another equivalent evaluation of an unchanged root is not by itself new verification coverage.", + "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": "Independently recount one changed emitted word and its complete caller, importing no constructor or pricing engine. Include target losses, owned lifetimes, native orientation and extra charges. Check existing #5633/#5708/#5717/#5719 coverage to avoid duplicate audits and preserve its exact head. Stop after the chosen missing implication; a correct root alone is not supplier admission.", + "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": [ + "invoice", + "signed moment", + "productive target", + "independent recount" + ], + "existing_checks": [ + { + "scope": "PR #4088: mixed local/owner/phase ledger and moment reported.", + "evidence": "research/staged544-mixed-fourth-entry/README.md", + "remaining": "Independent binding of changed construction to paid histogram, distinct from full admission.", + "status": "author-checked", + "source_commit": "72d7efc181edb21806a878f174847c96dd410ab0", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4091: sharp pooled ceiling proposed for fixed THREE/FOUR words and inventory.", + "evidence": "research/staged-fourth-mixture-ceiling/README.md", + "remaining": "Validate dual, exhaustive pattern scope and exact source equivalence before applying to newer fills.", + "status": "author-checked", + "source_commit": "a29bdd8f56cd18b805917775cdec09ff935eddc4", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4067: paid (2,2) to (1,3) exchange and fixed OQ4 host reported.", + "evidence": "research/r437-two-window-carrier/README.md", + "remaining": "Independent full cost delta; remaining caller/precision/stock obligations are separate.", + "status": "author-checked", + "source_commit": "a95f11c52e3ca1e4c5171b3c20d8f4b0815aee2e", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.", + "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.", + "status": "reviewed", + "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137", + "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Sharp minimum block exponent of the fixed PR5756 two-tail/capacity inequality family, using cited PR5775 scalar bounds.", + "scope_change_reason": "Original research rather than a repeated moment audit: change the fixed block exponent 128 to an arbitrary integer L>=3 and determine the exact feasibility threshold.", + "bottleneck_link": "A scoped compiler-parameter result. It identifies a shorter candidate block and a sharp obstruction below it; complete compiler costs and admission remain open.", + "budget_minutes": 60, + "stop_rule": "Ship the first exact threshold and rational witness; do not optimize other gates or the invoice.", + "outcome": "completed", + "evidence": "PROOF.md and verify.py: minimum L=112, explicit witness, 109 excluded lengths and strict-boundary controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Does block length 112 extend to a complete charged compiler for this invoice?", + "why_it_matters": "The gate theorem alone does not lower carrier height or establish a legal compiler.", + "first_step": "Write the changed block decomposition and rederive its normalization, exit, rounding and nonrecursive charges before testing other gates.", + "blocked_by": "No source-bound changed block rule or complete cost ledger is supplied." + } + ], + "claim_type": "Scoped proof conditional on explicitly cited predecessor scalar bounds.", + "predecessor_pr": 5775, + "predecessor_head": "56dc0a9ec02020f5e035c7d83f078fb2b27ac76a", + "upstream_checked_at": "2026-10-27T12:02:44.189218+00:00", + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19216140" +} diff --git a/research/p104-minimum-tail-block/VERIFY.json b/research/p104-minimum-tail-block/VERIFY.json new file mode 100644 index 0000000000..8ed788aea8 --- /dev/null +++ b/research/p104-minimum-tail-block/VERIFY.json @@ -0,0 +1,33 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact threshold separation, rational length-112 witness, unique minimal cutoff/floor and semantic controls; cited predecessor bounds are premises." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "The same new-result certificate with isolated optimized Python and active explicit contracts." + } + ] +} diff --git a/research/p104-minimum-tail-block/premises/INVOICE.json b/research/p104-minimum-tail-block/premises/INVOICE.json new file mode 100644 index 0000000000..9d47144bd9 --- /dev/null +++ b/research/p104-minimum-tail-block/premises/INVOICE.json @@ -0,0 +1,1400 @@ +{ + "changed_charts": [ + [ + 11545, + [ + "ADD", + 42, + 41, + "1" + ], + 477, + 1090 + ], + [ + 11546, + [ + "ADD", + 41, + 42, + "-1" + ], + 477, + 1090 + ], + [ + 11547, + [ + "ADD", + 42, + 41, + "1" + ], + 477, + 1090 + ], + [ + 11548, + [ + "SCALE", + 41, + "-1" + ], + 477, + 1090 + ], + [ + 11549, + [ + "SCALE", + 41, + "-2" + ], + 477, + 1090 + ], + [ + 11550, + [ + "ADD", + 400, + 41, + "-1" + ], + 477, + 1090 + ], + [ + 11551, + [ + "ADD", + 401, + 41, + "-1" + ], + 477, + 1090 + ], + [ + 11552, + [ + "SCALE", + 42, + "-2" + ], + 477, + 1090 + ], + [ + 11553, + [ + "ADD", + 106, + 42, + "1/2" + ], + 477, + 1090 + ], + [ + 11554, + [ + "ADD", + 403, + 42, + "-1" + ], + 477, + 1090 + ], + [ + 11555, + [ + "ADD", + 405, + 106, + "1" + ], + 477, + 1090 + ], + [ + 11556, + [ + "ADD", + 106, + 405, + "-1" + ], + 477, + 1090 + ], + [ + 11557, + [ + "ADD", + 405, + 106, + "1" + ], + 477, + 1090 + ], + [ + 11558, + [ + "SCALE", + 106, + "-1" + ], + 477, + 1090 + ], + [ + 11559, + [ + "ADD", + 41, + 405, + "-2" + ], + 477, + 1090 + ], + [ + 11560, + [ + "ADD", + 405, + 42, + "-1" + ], + 477, + 1090 + ], + [ + 11561, + [ + "ADD", + 405, + 403, + "-1/2" + ], + 477, + 1090 + ], + [ + 11562, + [ + "ADD", + 741, + 403, + "1/2" + ], + 477, + 1090 + ], + [ + 11563, + [ + "ADD", + 741, + 42, + "1" + ], + 477, + 1090 + ], + [ + 11564, + [ + "ADD", + 41, + 741, + "2" + ], + 477, + 1090 + ], + [ + 11565, + [ + "ADD", + 410, + 400, + "1" + ], + 477, + 1090 + ], + [ + 11566, + [ + "ADD", + 400, + 410, + "-1" + ], + 477, + 1090 + ], + [ + 11567, + [ + "ADD", + 410, + 400, + "1" + ], + 477, + 1090 + ], + [ + 11568, + [ + "SCALE", + 400, + "-1" + ], + 477, + 1090 + ], + [ + 11569, + [ + "SCALE", + 400, + "-2" + ], + 477, + 1090 + ], + [ + 11570, + [ + "ADD", + 403, + 401, + "1" + ], + 477, + 1090 + ], + [ + 11571, + [ + "ADD", + 401, + 403, + "-1" + ], + 477, + 1090 + ], + [ + 11572, + [ + "ADD", + 403, + 401, + "1" + ], + 477, + 1090 + ], + [ + 11573, + [ + "SCALE", + 401, + "-1" + ], + 477, + 1090 + ], + [ + 11574, + [ + "ADD", + 42, + 401, + "1" + ], + 477, + 1090 + ], + [ + 11575, + [ + "ADD", + 741, + 401, + "1/2" + ], + 477, + 1090 + ], + [ + 11576, + [ + "ADD", + 41, + 403, + "1" + ], + 477, + 1090 + ], + [ + 11577, + [ + "ADD", + 400, + 403, + "1" + ], + 477, + 1090 + ], + [ + 11578, + [ + "ADD", + 410, + 403, + "-2" + ], + 477, + 1090 + ], + [ + 11579, + [ + "ADD", + 410, + 741, + "1" + ], + 477, + 1090 + ], + [ + 11580, + [ + "ADD", + 741, + 410, + "-1" + ], + 477, + 1090 + ], + [ + 11581, + [ + "ADD", + 410, + 741, + "1" + ], + 477, + 1090 + ], + [ + 11582, + [ + "SCALE", + 741, + "-1" + ], + 477, + 1090 + ], + [ + 11583, + [ + "SCALE", + 741, + "-1/2" + ], + 477, + 1090 + ], + [ + 11584, + [ + "ADD", + 41, + 741, + "-1" + ], + 477, + 1090 + ], + [ + 11585, + [ + "ADD", + 400, + 741, + "-1" + ], + 477, + 1090 + ], + [ + 11586, + [ + "ADD", + 403, + 741, + "-1" + ], + 477, + 1090 + ], + [ + 11587, + [ + "ADD", + 42, + 410, + "-1" + ], + 477, + 1090 + ], + [ + 11588, + [ + "ADD", + 106, + 410, + "-1" + ], + 477, + 1090 + ], + [ + 11589, + [ + "ADD", + 401, + 410, + "-1" + ], + 477, + 1090 + ], + [ + 11590, + [ + "ADD", + 741, + 410, + "1" + ], + 477, + 1090 + ], + [ + 11591, + [ + "ADD", + 403, + 410, + "1" + ], + 477, + 1090 + ], + [ + 11592, + [ + "ADD", + 401, + 410, + "-1" + ], + 477, + 1090 + ], + [ + 11593, + [ + "SCALE", + 410, + "2" + ], + 477, + 1090 + ], + [ + 11594, + [ + "ADD", + 403, + 741, + "1" + ], + 477, + 1090 + ], + [ + 11595, + [ + "ADD", + 106, + 741, + "1" + ], + 477, + 1090 + ], + [ + 11596, + [ + "ADD", + 42, + 741, + "-1" + ], + 477, + 1090 + ], + [ + 11597, + [ + "ADD", + 410, + 741, + "1" + ], + 477, + 1090 + ], + [ + 11598, + [ + "ADD", + 741, + 410, + "-1" + ], + 477, + 1090 + ], + [ + 11599, + [ + "ADD", + 410, + 741, + "1" + ], + 477, + 1090 + ], + [ + 11600, + [ + "SCALE", + 741, + "-1" + ], + 477, + 1090 + ], + [ + 11601, + [ + "ADD", + 410, + 403, + "-1/2" + ], + 477, + 1090 + ], + [ + 11602, + [ + "ADD", + 741, + 403, + "-1" + ], + 477, + 1090 + ], + [ + 11603, + [ + "ADD", + 401, + 403, + "1" + ], + 477, + 1090 + ], + [ + 11604, + [ + "ADD", + 400, + 403, + "1/2" + ], + 477, + 1090 + ], + [ + 11605, + [ + "ADD", + 106, + 403, + "-1/2" + ], + 477, + 1090 + ], + [ + 11606, + [ + "ADD", + 42, + 403, + "1/2" + ], + 477, + 1090 + ], + [ + 11607, + [ + "ADD", + 41, + 403, + "-1/2" + ], + 477, + 1090 + ], + [ + 11608, + [ + "SCALE", + 403, + "-1/2" + ], + 477, + 1090 + ], + [ + 11609, + [ + "ADD", + 741, + 401, + "1" + ], + 477, + 1090 + ], + [ + 11610, + [ + "ADD", + 403, + 401, + "1/2" + ], + 477, + 1090 + ], + [ + 11611, + [ + "ADD", + 400, + 401, + "-1/2" + ], + 477, + 1090 + ], + [ + 11612, + [ + "ADD", + 106, + 401, + "1/2" + ], + 477, + 1090 + ], + [ + 11613, + [ + "ADD", + 42, + 401, + "1/2" + ], + 477, + 1090 + ], + [ + 11614, + [ + "ADD", + 41, + 401, + "1/2" + ], + 477, + 1090 + ], + [ + 11615, + [ + "SCALE", + 401, + "-2" + ], + 477, + 1090 + ], + [ + 11616, + [ + "ADD", + 106, + 400, + "1" + ], + 477, + 1090 + ], + [ + 11617, + [ + "ADD", + 42, + 400, + "1" + ], + 477, + 1090 + ], + [ + 11618, + [ + "ADD", + 41, + 400, + "-1" + ], + 477, + 1090 + ], + [ + 11619, + [ + "SCALE", + 400, + "2" + ], + 477, + 1090 + ], + [ + 11620, + [ + "ADD", + 401, + 400, + "1" + ], + 477, + 1090 + ], + [ + 11621, + [ + "ADD", + 400, + 401, + "-1" + ], + 477, + 1090 + ], + [ + 11622, + [ + "ADD", + 401, + 400, + "1" + ], + 477, + 1090 + ], + [ + 11623, + [ + "SCALE", + 400, + "-1" + ], + 477, + 1090 + ], + [ + 11624, + [ + "ADD", + 403, + 106, + "1/2" + ], + 477, + 127 + ], + [ + 11625, + [ + "ADD", + 401, + 106, + "-1" + ], + 477, + 127 + ], + [ + 11626, + [ + "ADD", + 41, + 106, + "1" + ], + 477, + 1090 + ], + [ + 11627, + [ + "SCALE", + 106, + "-2" + ], + 477, + 127 + ], + [ + 11628, + [ + "ADD", + 403, + 42, + "1/2" + ], + 477, + 1090 + ], + [ + 11629, + [ + "ADD", + 401, + 42, + "-1" + ], + 477, + 1090 + ], + [ + 11630, + [ + "ADD", + 41, + 42, + "1" + ], + 477, + 1090 + ], + [ + 11631, + [ + "SCALE", + 42, + "-2" + ], + 477, + 1090 + ], + [ + 11632, + [ + "ADD", + 400, + 42, + "1" + ], + 477, + 1090 + ], + [ + 11633, + [ + "ADD", + 42, + 400, + "-1" + ], + 477, + 1090 + ], + [ + 11634, + [ + "ADD", + 400, + 42, + "1" + ], + 477, + 1090 + ], + [ + 11635, + [ + "SCALE", + 42, + "-1" + ], + 477, + 127 + ], + [ + 11636, + [ + "ADD", + 403, + 41, + "-1/2" + ], + 477, + 127 + ], + [ + 11637, + [ + "ADD", + 401, + 41, + "1" + ], + 477, + 127 + ], + [ + 11638, + [ + "ADD", + 400, + 41, + "1" + ], + 477, + 1090 + ], + [ + 11639, + [ + "ADD", + 106, + 41, + "1" + ], + 477, + 127 + ], + [ + 11640, + [ + "ADD", + 42, + 41, + "1" + ], + 477, + 127 + ] + ], + "complete_cost": { + "compiler": { + "H": 80511200000000000, + "N": "2^80511200000000000", + "eta": { + "lower": "0.000000128387229643834457871291", + "upper": "0.000000128387229643834457871292" + }, + "gap": "1/1400000000000", + "integer_test_exponent": 57508, + "logarithm_power": 1024, + "theta": "63/64", + "uniform_saving": "272399571/87500000000", + "word_materialized": false + }, + "full_forward_calls": 18, + "gain": "2439/20000000000", + "kappa": "62262759/20000000000", + "kappa_decimal": "0.00311313795", + "margin_at_previous": { + "lower": "0.029578770580357904755090866637", + "upper": "0.029578770580357904755090866638" + }, + "negative_controls": { + "old_BIT": "Rejected by outer inequalities", + "old_cutoff": "Rejected by completion-tail ratio greater than one", + "source_completion": "Rejected at cutoff17, floor18 and decay39/40", + "source_offset": "Rejected at cutoff16 with tail offset1/5" + }, + "nonrecursive": { + "fixed_scalar_growth_bound": "At most 2^(16*26000) before native factors; a declared constant, not an attained norm.", + "local_paid_rank_mass": 5987, + "local_routes": 5240000, + "local_scalar": 224138, + "peak_owned_fields": 2, + "raw_budget": 1000000000, + "raw_scalar_upper": 184647552, + "tensor_native_growth_bound": "Each rank-r Gaussian has row l1 norm at most 2^(rf); use local_paid_rank_mass for the whole word." + }, + "ordinary_BIT": { + "admitted": "17/5000", + "after_cover": "69/20000", + "atom": "1/250", + "before_cover": "3459/1000000", + "ordinary_saving": "8590884599/2500000000000", + "prime_rule": "odd q > 2^26*N^5 avoiding all fixed denominators and rank witnesses" + }, + "outer": { + "functional_checks": { + "actual_new_BIT_stock_sublinear": "348599999999253/350000000000000", + "fixed_halo_explicit_metadata_branch": "26950000000001/350000000000", + "new_BIT_row_stock_sublinear_in_active_group": "1395799999997009/1400000000000000", + "new_semantic_group_guard": "3/1400000000000" + }, + "margins": { + "boundary_algebraic_matrix": "6101750387595641606867/1960000000000000000000000", + "fused_gaussian": "6101750387586924820601/1960000000000000000000000", + "global_coordinate_router": "2179196567/700000000000", + "group_bit_router": "3050875194493462410299/980000000000000000000000", + "group_scans": "699999999999/700000000000", + "main_transform": "6101750386195641606867/1960000000000000000000000", + "microbox_face_corrections": "26950000000001/350000000000", + "polynomial_products": "1399999999999/1400000000000", + "sparse_union_movement": "802351750387595641606867/1960000000000000000000000" + }, + "parameters": { + "a": "2179196567/700000000000", + "b": "871678627/280000000000", + "beta": "1399999999997/1400000000000", + "bit_saving": "17/5000", + "cap_xi": "1782351750386195641606867/1960000000000000000000000", + "complex_uniform_saving": "272399571/87500000000", + "d": "1/1400000000000", + "epsilon": "1399999999999/1400000000000", + "kappa": "62262759/20000000000", + "lambda_": "398754744819/400000000000", + "lambda_prime": "1395641606867/1400000000000", + "layout": "1/1400000000000", + "q": "4358393133/1400000000000", + "r0": "1/14000000000000", + "stop": "1/1400000000000", + "tested_saving": "622627591/200000000000" + }, + "strict_checks": { + "actual_bit_above_effective": "200803433/700000000000", + "actual_logarithmic_gamma_guard": "1/1400000000000", + "actual_logarithmic_group_guard": "177648249615904358393133/980000000000000000000000", + "alpha_logarithm_absorption": "1/14000000000000", + "boundary_algebraic_matrix_above_kappa": "5595641606867/1960000000000000000000000", + "cap_above_band": "802351750386195641606867/1960000000000000000000000", + "cap_below_cell": "177648249612404358393133/1960000000000000000000000", + "cap_below_phase_cell_power": "2137648249613804358393133/1960000000000000000000000", + "complex_above_effective": "1/1400000000000", + "complex_below_one_over_32": "7878321373/280000000000", + "complex_endpoint": "1/700000000000", + "epsilon_below_one": "1/1400000000000", + "epsilon_positive": "1399999999999/1400000000000", + "fine_prime_halo_umbrella": "7/2", + "fused_gaussian_above_kappa": "5586924820601/1960000000000000000000000", + "gaussian_above_main": "695641606867/980000000000000000000000", + "global_coordinate_router_above_kappa": "1/350000000000", + "global_gamma_power_slack": "9/14000000000000", + "group_below_dimension": "1/700000000000", + "group_bit_router_above_kappa": "3493462410299/980000000000000000000000", + "group_gauge_power_slack": "177648249615834358393133/980000000000000000000000", + "group_key_fits_record": "1/700000000000", + "group_positive": "1399999999997/1400000000000", + "group_scans_above_kappa": "348910401717/350000000000", + "halo_covers_generic_inverse_radius": "5", + "improvement_over_user_baseline": "691083765400418148631/500000000000000000000000", + "lambda_above_internal": "1/2800000000000", + "lambda_above_sigma": "3/2800000000000", + "lambda_above_tau": "1/2800000000000", + "lambda_prime_above_lambda": "1/2800000000000", + "lambda_prime_above_leaf": "559128321373/392000000000000000000000", + "leaf_saving_above_effective": "279128321373/392000000000000000000000", + "main_transform_above_kappa": "4195641606867/1960000000000000000000000", + "membership_arithmetic_fits_record": "1/1400000000000", + "microbox_face_corrections_above_kappa": "53897820803437/700000000000", + "microbox_halo_volume": "110600000000003/1400000000000", + "new_complex_uniform_saving_above_b": "1/1400000000000", + "new_semantic_guard_with_C1_one": "1/1400000000000", + "polynomial_products_above_kappa": "1395641606869/1400000000000", + "positive_layout_slack": "1/1400000000000", + "q_below_effective": "1/1400000000000", + "q_below_internal": "1/1400000000000", + "q_below_leaf": "559128321373/392000000000000000000000", + "q_positive": "4358393133/1400000000000", + "short_record_fallback": "279128321373/280000000000", + "source_axis_superpolynomial": "1/1400000000000", + "sparse_union_movement_above_kappa": "796250000005595641606867/1960000000000000000000000", + "stop_below_one": "1399999999999/1400000000000", + "stop_positive": "1/1400000000000", + "strassen_integer_power_gap": "1951441519231", + "support_router_span": "3/1400000000000", + "theta_positive_polynomial_power": "2", + "union_header_fits_record": "3/1400000000000", + "union_tag_work_per_visit_fits_record": "3/1400000000000" + } + }, + "paid": { + "1": 41520, + "16": 416, + "2": 8172, + "24": 416, + "3": 8856, + "32": 416, + "4": 1674, + "40": 416, + "48": 416, + "5": 3132, + "56": 416, + "6": 108, + "64": 416, + "7": 270, + "72": 208 + }, + "paid_calls": 66852, + "previous_pr5718": "389127/125000000", + "productive_fields": 13390, + "query_shears": 15, + "rank_mass_surplus": 760, + "raw_ceiling": { + "derivative_upper": "-738596154004511222636095493817850924833979710424488126325902089/3138550867693340381917894711603833208051177722232017256448", + "interval": [ + "0", + "17/5000" + ] + }, + "raw_headroom": [ + "73/3125000000000", + "2337/100000000000000" + ], + "raw_root_interval": [ + "38914224667/12500000000000", + "311313797337/100000000000000" + ], + "relative_gain_percent": "4065/1037672", + "strictification": { + "alpha": { + "lower": "0.999999999981368230437503066447", + "upper": "0.999999999981368230437503066448" + }, + "cutoff": 16, + "delta": { + "lower": "0.944337257529929949513398128117", + "upper": "0.944337257529929949513398128118" + }, + "floor": 17, + "gamma": { + "lower": "0.975484709128690914856977434634", + "upper": "0.975484709128690914856977434635" + }, + "normalized_paid_upper": "1048576000976562501/1048576001073741824", + "power": 1024, + "reserve": "1/1000000000000", + "tail_block": 128, + "tail_decay": "125/128", + "tail_offset": "1/7", + "tested": "622627591/200000000000" + }, + "targets": { + "1": 432, + "145": 208, + "17": 416, + "2": 90, + "25": 416, + "33": 416, + "4": 1656, + "41": 416, + "49": 416, + "5": 126, + "57": 416, + "65": 416, + "7": 108, + "73": 208, + "8": 666, + "9": 6984 + }, + "whole_idle_jobs": 3120 + }, + "controls": { + "block_op_on_old_chart": "Scalar destination and coefficient", + "extra_target_credit": "Every productive helper has a native target", + "missing_block_move": "Scalar destination and coefficient", + "old_helper_start": "Scalar destination and coefficient", + "read_after_write": "Dependent operations keep their order", + "unpaid_query": "Complete field and call counts" + }, + "global_paid_delta": { + "1": 18, + "4": 18, + "5": -18 + }, + "helper_credit_delta": { + "1": -1, + "4": 1, + "5": 1, + "8": -1 + }, + "helper_finals": { + "405": [ + 477, + 1090 + ] + }, + "helper_starts": { + "741": [ + 477, + 1090 + ] + }, + "local": { + "endpoint_coefficients": 602176, + "helpers": { + "1": 24, + "2": 5, + "4": 92, + "5": 7, + "7": 6, + "8": 37, + "9": 388 + }, + "owned_fields": 9, + "owned_lifetimes": 11, + "paid": { + "1": 2220, + "2": 454, + "3": 492, + "4": 93, + "5": 174, + "6": 6, + "7": 15 + }, + "paid_rank_mass": 5987, + "peak_owned_fields": 2, + "public_inputs": 767, + "real_scalar_allowance": 224138 + }, + "local_paid_delta": { + "1": 1, + "4": 1, + "5": -1 + }, + "native": { + "distinct_maps": 2927, + "helper_normalizers": 1118, + "helpers": { + "1": 24, + "2": 5, + "4": 92, + "5": 7, + "7": 6, + "8": 37, + "9": 388 + }, + "main_adapters": 208, + "proof": "Every signed Pauli image and exact global phase; frame induction at every positive tensor width", + "recipe_payload_sha256": "b566ac8ebfb9df3d4c8a7be449c749283ec70dedbdaad7f943c264c692da544a", + "wrong_phase_rejected": true + }, + "physical": { + "central_square_columns": 53248, + "full_calls": 18, + "main_targets": { + "145": 208, + "17": 416, + "25": 416, + "33": 416, + "41": 416, + "49": 416, + "57": 416, + "65": 416, + "73": 208 + }, + "new_paid_jobs": 0, + "physical_contacts": 7488, + "ports": 104, + "route_payload_sha256": "7f4f0ca768ffbc4f93dcff575592c4c67411f46b4289e45b73f715a2ad47b142", + "tensor_rule": "Factorwise native maps; scalar signs stay outside the tensor power.", + "whole_idle_jobs": { + "16": 416, + "24": 416, + "32": 416, + "40": 416, + "48": 416, + "56": 416, + "64": 416, + "72": 208 + }, + "wrapper_sites": [ + 1, + 3, + 5, + 7, + 9, + 11, + 13, + 15, + 17, + 19, + 21, + 23, + 25, + 27, + 29, + 31 + ] + }, + "source": { + "pr5751": "8483f9a679d06c1e270141dbc686a7e76e7a7522" + }, + "status": "PASS_P104_R22_REFRAME_KAPPA_00311313795", + "transpose": { + "arithmetic": "Dense integer rows with binary denominators; reverse chronology", + "coefficients": 602176, + "columns": 776 + } +} diff --git a/research/p104-minimum-tail-block/premises/PROOF.md b/research/p104-minimum-tail-block/premises/PROOF.md new file mode 100644 index 0000000000..5611eb8f86 --- /dev/null +++ b/research/p104-minimum-tail-block/premises/PROOF.md @@ -0,0 +1,81 @@ +# Fixed-contract feasibility proof + +Fix the retained PR5756 target and paid histograms `T_r,P_r`, saving +`C=622627591/200000000000` and `t=1-C`. Put `T=sum T_r r^t` and +`N=sum T_r=13390`. For integer cutoff `c>=1`, integer floor `b`, positive +real offset `u` and rational decay `rho`, the two source tail gates are + +``` +g(c,u) = sum P_r r^(t+u) / (c^u T) < rho, +d(c,b) = N b / (c^C T) < rho, +rho^128 < 1/16. +``` + +The capacity condition `c^64 < b^63` implies `b>=c+1`. Let +`R=2^(-1/32)`. A permitted rational rho exists if and only if both g and d +are strictly below R: rationals are dense in the open interval between their +maximum and R. Equality at R is excluded. This eliminates every decay choice, +not just a grid. We first use the weaker condition b>=c+1 to exclude parameters; +the sole remaining pair also passes the exact capacity condition. + +## Exclude all but one integer pair + +For positive u, g(c,u) decreases with c. For fixed c, g is a positive sum +of exponentials in u and is strictly convex, since a paid rank differs from c. +Its derivative is the same sum weighted by `log(r/c)`. A negative derivative +at l and positive derivative at h locate its unique global minimum in (l,h). +For x in this interval, convexity gives +`g(x)>=g(l)+g'(l)(x-l)>=g(l)+g'(l)(h-l)` when g'(l)<0. +The verifier uses a lower interval endpoint for both terms. The midpoint gives +an upper bound on the minimum. Strict convexity extends this statement to all +real u; no unsearched tail or sampled-grid premise remains. + +At c=15 the resulting lower bound is `0.983563652257169`, while +`R<0.978572062087701`. Thus every positive u fails for c<=15. + +For real c>=1, `(c+1)/c^C` has derivative with sign `(1-C)c-C`, which is +positive because `0R`. Thus every c>=17 and every permitted +b fails. At c=16,b=18, d exceeds `0.999886507972867>R`, which excludes all +larger floors. The only pair left is c=16,b=17. It passes `16^64<17^63`. + +## Full offset interval and optimum + +For c=16, g(0)>R, g(1/7)R. Strict convexity, together with the +unique derivative zero, gives exactly two positive roots of g(u)=R and a +single open feasible interval between them. The exact root brackets are in +RESULT.json. The completion tail is constant in u and is below +`0.944337257529930`. It is below even the global minimum of g, so it never +binds in this interval. Thus these two roots specify the complete tail set. + +The derivative has opposite signs at the endpoints of the reported best-offset +bracket. The convex minimum bound above gives the stated decay infimum. +The infimum is not attained by rho because g 0 and completion_upper > 0, 'tail domain') + need(paid_upper < decay, 'paid tail') + need(completion_upper < decay, 'completion tail') + need(decay ** length < RESERVE, 'reserve') + need(cutoff ** length < floor ** (length - 2), 'capacity') + + +def check_threshold(lower, length): + need(type(length) is int and 3 <= length <= 4096, 'threshold domain') + need(0 < lower < 1, 'lower domain') + need(lower ** (length - 1) > RESERVE, 'lower boundary') + + +def derive(bounds): + need(0 < bounds['a16'] < bounds['a15'] < bounds['d17'] < 1, 'lower ordering') + need(bounds['a15'] < bounds['d18'] < 1, 'floor ordering') + need(bounds['gamma'] < Q(975485, 1000000), 'displayed paid upper bound') + need(bounds['delta'] < Q(945, 1000), 'displayed completion upper bound') + length = 112 + check_threshold(bounds['a16'], length) + check_witness(length, 16, 17, DECAY, bounds['gamma'], bounds['delta']) + need(bounds['a15'] ** length > RESERVE, 'other cutoffs at minimum') + need(bounds['d17'] ** length > RESERVE, 'large cutoffs at minimum') + need(bounds['d18'] ** length > RESERVE, 'large floors at minimum') + excluded = 0 + for candidate in range(3, length): + need(bounds['a16'] ** candidate > RESERVE, 'finite length corroboration') + excluded += 1 + return { + 'claim_type': 'scoped proof using cited predecessor scalar premises', + 'minimum_block_length': length, + 'unique_cutoff_floor_at_minimum': [16, 17], + 'witness': {'offset': '1/7', 'decay': str(DECAY)}, + 'excluded_integer_lengths_enumerated': excluded, + 'new_reserve_slack': str(RESERVE - DECAY ** length), + 'shortening_from_128': str(Q(128 - length, 128)), + } + + +def controls(bounds, origins): + cases = ( + (111, 16, 17, DECAY, bounds['gamma'], bounds['delta'], 'reserve'), + (112, 16, 17, Q(125, 128), bounds['gamma'], bounds['delta'], 'reserve'), + (112, 16, 17, DECAY, bounds['bad_offset'], bounds['delta'], 'paid tail'), + (112, 16, 18, DECAY, bounds['gamma'], bounds['d18'], 'completion tail'), + (2, 16, 17, DECAY, bounds['gamma'], bounds['delta'], 'length domain'), + (4, 1, 2, Q(1, 2), Q(1, 3), Q(1, 3), 'reserve'), + (4, 1, 1, Q(1, 3), Q(1, 4), Q(1, 4), 'capacity'), + ) + rejected = 0 + for length, cutoff, floor, decay, paid, completion, reason in cases: + try: + check_witness(length, cutoff, floor, decay, paid, completion) + except ValueError as exc: + need(str(exc) == reason, 'wrong witness rejection') + rejected += 1 + else: + raise ValueError('accepted invalid witness') + for lower, length in ((Q(97, 100), 112), (bounds['a16'], 113)): + try: + check_threshold(lower, length) + except ValueError as exc: + need(str(exc) == 'lower boundary', 'wrong threshold rejection') + rejected += 1 + else: + raise ValueError('accepted unsupported threshold') + row = origins['files'][0] + try: + check_bytes(read_bytes(row['retained_path']) + b' ', row) + except ValueError as exc: + need(str(exc) == 'source hash', 'wrong corruption rejection') + rejected += 1 + else: + raise ValueError('accepted corrupt source') + need(rejected == 10, 'control coverage') + return rejected + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--receipt', type=Path, help='write a hash-bound receipt outside the package') + args = parser.parse_args() + bounds, origins = cited_premises() + result = derive(bounds) + result['controls'] = controls(bounds, origins) + if args.receipt is not None: + destination = args.receipt.resolve() + need(not destination.is_relative_to(PACKAGE), 'receipt must be outside the package') + receipt = { + 'result': result, + 'source_status': 'Cited bounds authenticated, not independently replayed.', + 'python': platform.python_version(), + 'files': {name: hashlib.sha256(read_bytes(name)).hexdigest() for name in FILES}, + } + destination.write_text(json.dumps(receipt, indent=2, sort_keys=True) + '\n') + print('PASS_MINIMUM_TAIL_BLOCK minimum=112 cutoff=16 floor=17' + f" excluded_lengths={result['excluded_integer_lengths_enumerated']}" + f" controls={result['controls']}") + + +if __name__ == '__main__': + main()