diff --git a/research/complex-e8-pair-block-climb/README.md b/research/complex-e8-pair-block-climb/README.md new file mode 100644 index 0000000000..b2f86d26aa --- /dev/null +++ b/research/complex-e8-pair-block-climb/README.md @@ -0,0 +1,186 @@ +# An exact complex decoder climbs from two E8 roots to rank 16 + +**Scoped partial result.** The exact tensor decoder and support/COPY ledger are +verified. Its copy-only profile clears the selected model's five-percent +ceiling screen, while one explicit frame-slot tariff sensitivity falls below +the selected endpoint. No physical tariff, selected supplier, new κ, or +frontier change is established. + +## Question and result + +Can a small complex decoder start from actual E8 roots, climb through block +ranks 2, 4, 8 and 16, and fit the selected call's full copy/frame ledger? + +The exact identity exists, and its support-pairing matrix has full rank at each +level. The rank-16 block has 16 full-support terms of copy rank 16, so its COPY +mass is 256. The selected model has 896 live families over nine stages. The +rank-16 construction therefore uses 56 blocks per nine-stage replica, or an +average `56/9` blocks per call. Keeping the selected eight rank-8 local terms, +the per-call profile is `{16:896/9, 8:8}` with local COPY mass `14912/9`. + +Under the pinned parent relaxation, that copy-only profile has ceiling bracket +`[1942057021/250000000000, 1553645617/200000000000]`, whose upper endpoint is +about `0.007768228085`. This exceeds the five-percent target +`0.00177455681454345`. The result is only an ideal profile screen: product +levels 2–4 use a new label form, and the frame ledger has no established tariff +in the parent model. Charging one rank-1 unit for each listed per-block frame, +embedding, restoration-read and scalar-add slot gives `12824/3` extra units per +call and a sensitivity ceiling near `0.001658774411`, below the selected +`0.001690054109089` endpoint. The physical tariff and a selected-code embedding +remain open. + +## Exact decoder identity + +Take the two E8 roots + +```text +r0 = (1,1,0,0,0,0,0,0) +r1 = (1,0,1,0,0,0,0,0) +``` + +Both have norm squared 2 and dot product 1, so their Gram matrix is + +```text +G0 = [[2,1], [1,2]]. +``` + +Over `Q(i)`, with **ordinary transpose**, set + +```text +D0 = [[1, 1], [1, i]] +T0 = [[3-i, 1+i], [3+i, -1-i]]. +``` + +Direct multiplication gives `D0 T0^T = [[4,2],[2,4]] = 2 G0`. Every entry of +both frames is nonzero. The two E8 support labels pair by +`( + 1) mod 2`, giving `B0 = I2`; each of the two terms therefore has +support-pairing rank 2 and the base copy mass is 4. Using conjugate transpose +does not give this identity (checked as a negative control). + +For `s=1,2,3,4`, let `n=2^s`, `Rs=R0^tensor_s`, +`Gs=G0^tensor_s`, `Ds=2^(1-s) D0^tensor_s`, and `Ts=T0^tensor_s`. Then + +```text +Ds Ts^T = 2 Gs = 2 Rs Rs^T. +``` + +The verifier checks every matrix entry. The block-climbing frame itinerary is +the repeated tensor step `s -> s+1`: the product-root frame has `n` rows in +ambient dimension `8^s`; the decoder and reader frames have shape `n x n`; +their ranks are `n`; and their exact inverses are checked. The product-root +embedding has `n²` nonzero coefficients. The left inverse `Ls=L0^tensor_s`, +where `L0` selects coordinates 2 and 3 of each base root, satisfies +`Ls Rs^T=I_n`; it uses `n` coordinate reads and restores every coefficient +vector in the product-root span. This does not restore arbitrary ambient state +outside that span. + +The binary support pairing at level `s` is `Bs=(Gs + J_n) mod 2`, where `J_n` +is the all-ones matrix. Modulo 2, `G0=[[0,1],[1,0]]`, so `Gs` is a permutation +matrix `Ps`. Since `n` is even, `Bs=Ps(I+J_n)` is nonsingular: over F2, +`det(I+J_n)=1+n=1`. The verifier independently computes all four ranks. For +`s>=2`, these are product roots in `R^(8^s)` and a new `n`-bit label form +`Bs`; they are not the selected 9-bit E8 port code. + +## Full block and per-call ledger + +| Tensor factors | Product lines | Terms | COPY rank per term | COPY mass | Forward D/T frame coefficients | Root embedding coefficients | Root-span restoration reads | +|---:|---:|---:|---:|---:|---:|---:|---:| +| 1 | 2 | 2 | 2 | 4 | 8 | 4 | 2 | +| 2 | 4 | 4 | 4 | 16 | 32 | 16 | 4 | +| 3 | 8 | 8 | 8 | 64 | 128 | 64 | 8 | +| 4 | 16 | 16 | 16 | 256 | 512 | 256 | 16 | + +At level 4, both forward `16 x 16` frames are dense. Their four-stage `2 x 2` +tensor application takes 272 constant-multiplication slots (including the +`1/8` normalization on D) and 128 additions for the two input frames. If a +consumer needs vector outputs returned to the original coefficient frames, +the two inverse frames are also dense, another 512 coefficient slots per +block. The scalar bilinear decoder returns a scalar and does not itself need +that output-vector restoration. Each block also uses 16 rank-16 bilinear child +products and 15 scalar accumulation additions. + +| Per-call quantity | Candidate profile | Selected model | +|---|---:|---:| +| Live families | `896/9` | `896/9` | +| Average rank-16 blocks / children | `56/9` / `896/9` | — | +| Retained rank-8 local terms | 8 | 8 | +| Decoder COPY mass | `14336/9` | — | +| Total local profile mass including retained rank-8 terms | `14912/9` | 5,586 | +| Full local-plus-centre coverage mass available | — | 7,232 | + +The ratio of candidate to selected local mass is `7456/25137`. The 7,232 +coverage allowance follows the pinned model's `72*(896/9)+64` identity; its +separate centre charge is retained. Under the parent ideal relaxation the +candidate profile's ceiling is above the five-percent target. The ceiling +assumes fractional idle counts and unconstrained repacking; it does not prove a +physically realizable supplier. + +The level-4 per-call frame ledger over the average `56/9` blocks is: + +| Item | Slots or coefficients per call | +|---|---:| +| Forward D/T dense coefficients | `28672/9` | +| Inverse D/T coefficients if vector outputs are required | `28672/9` | +| Staged D/T constant multiplications | `15232/9` | +| Staged D/T additions | `7168/9` | +| Product-root embedding coefficients | `14336/9` | +| Root-span restoration reads | `896/9` | +| Scalar output accumulation additions | `280/3` | + +For a tariff sensitivity only, charge one rank-1 unit per staged multiply, +addition, embedding coefficient, restoration read and scalar accumulation +addition. This is `687` units per block and `12824/3` units per call. The parent +profile can absorb at most 3,919 extra integer rank-1 units while clearing the +five-percent target; 3,920 fails. The sensitivity ceiling is therefore below +the selected endpoint. This unit tariff is not asserted to be the physical +cost, and the dense inverse is excluded unless vector restoration is needed. + +## Relation to retained work and credit + +The selected baseline is pinned through `certificates/selected-result.json`, +its manifest `research/community-frontier1094-audit/SELECTED-SOURCE.json`, its +assembly `research/community-frontier1094-audit/ASSEMBLY.json`, and the exact +review `docs/research/community-batch1099-review.md`. The selected assembly +SHA256 is `1122cb3a575f8c788345fc1bf4c108ac7c3250fb81a5988671f5eb04b3ab3045`. +The selected conditional κ is `0.001672660197076918`; the selected local-word +ceiling is `0.001690054109089`. The first-step rank-16 ideal is a 2.31x +relaxation and omits realization costs. + +Overlap checked live Start-here discussion #1163, handoff #1166, and relevant +PRs. PR #3039 has a charged-group block-climb obstruction, while #3066 corrects +its mixed-profile inference. PR #1633 bounds excess rank for all-pairs E8 +decoders and gives a ten-term normal form; #3566 binds a different masked P112 +tetrad decoder to selected ports. PRs #3701, #3805, #3811 and #3874 remain +rank-cap and ideal-budget screens. This package contributes the explicit +complex factorization on an actual E8 root pair, its four-level tensor +support/COPY ledger, and an exact frame-slot tariff sensitivity. It does not +duplicate the fixed-alphabet effective-rank result assigned to macbook-05 or +claim the product roots embed in the selected ports. Credit prior proofs and +source authors listed in `docs/research/complex-decoder-scope-map.md`, +including PR717, PR968 and PR1077. + +## Reproduce + +From the repository root, Python 3.12 and the standard library: + +```sh +python3 -I -B research/complex-e8-pair-block-climb/verify.py +python3 scripts/research_package.py --package research/complex-e8-pair-block-climb +``` + +Expected direct replay: +`PASS_COMPLEX_E8_PAIR_BLOCK_CLIMB levels=4 rank16_block_copy_mass=256 average_profile_mass=14912/9 ideal_a=0.007768228085 frame_proxy_a=0.001658774411`. +The package replay checks the source pins and runs the explicit verifier command +recorded in `VERIFY.json`. + +## Open next questions + +After the companion fixed-alphabet effective-rank result is available, does +its surviving support class embed this factorization into the selected 9-bit, +112-port pairing code, and what established physical tariff applies to the +complete frame ledger? Until then, stop; a copy-only ceiling pass does not +justify another construction round under the family-level expansion gate. + +Prepared with substantial OpenAI Codex assistance by homelab-05. No independent +human review or formal proof-assistant verification is claimed. New material +is Apache-2.0. diff --git a/research/complex-e8-pair-block-climb/RESULT.json b/research/complex-e8-pair-block-climb/RESULT.json new file mode 100644 index 0000000000..7ef607815d --- /dev/null +++ b/research/complex-e8-pair-block-climb/RESULT.json @@ -0,0 +1,652 @@ +{ + "base_D": [ + [ + "1", + "1" + ], + [ + "1", + "1*i" + ] + ], + "base_D_times_T_transpose": [ + [ + 4, + 2 + ], + [ + 2, + 4 + ] + ], + "base_T": [ + [ + "3-1*i", + "1+1*i" + ], + [ + "3+1*i", + "-1-1*i" + ] + ], + "base_gram": [ + [ + 2, + 1 + ], + [ + 1, + 2 + ] + ], + "base_roots": [ + [ + 1, + 1, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + 1, + 0, + 1, + 0, + 0, + 0, + 0, + 0 + ] + ], + "coefficient_field": "Q(i), ordinary transpose", + "controls": [ + "ordinary-transpose base identity", + "all four tensor-level identities entrywise", + "all four support-pairing matrices have exact full F2 rank", + "D and T frames and inverses are dense and mutually invertible", + "root-span embedding and exact left-inverse restoration at every level", + "per-call scaling uses 56 blocks over nine stages, not all 56 blocks in one call", + "selected centre profile is retained explicitly as eight rank-8 terms", + "COPY-only ceiling and one-rank1-unit-per-frame-slot sensitivity", + "exact integer allowance for additional rank-1 units at the five-percent target" + ], + "levels": [ + { + "D_frame_shape": [ + 2, + 2 + ], + "T_frame_shape": [ + 2, + 2 + ], + "ambient_dimension": 8, + "binary_pairing_matrix": [ + [ + 1, + 0 + ], + [ + 0, + 1 + ] + ], + "child_rank_per_term": 2, + "copied_information_per_term": 2, + "copy_mass_per_block": 4, + "forward_frame_nonzero_coefficients": 8, + "full_support_size_per_term_each_side": 2, + "inverse_frame_nonzero_coefficients_if_vector_restoration_is_needed": 8, + "line_count": 2, + "root_embedding_nonzero_coefficients": 4, + "root_span_extraction_reads": 2, + "scalar_accumulation_additions": 1, + "staged_forward_additions_for_D_and_T": 4, + "staged_forward_constant_multiplication_slots_for_D_and_T": 8, + "support_pairing_rank": 2, + "tensor_factors": 1, + "term_count": 2, + "term_matrix_rank_over_Q_i": 1, + "term_products_for_scalar_bilinear_form": 2 + }, + { + "D_frame_shape": [ + 4, + 4 + ], + "T_frame_shape": [ + 4, + 4 + ], + "ambient_dimension": 64, + "binary_pairing_matrix": [ + [ + 1, + 1, + 1, + 0 + ], + [ + 1, + 1, + 0, + 1 + ], + [ + 1, + 0, + 1, + 1 + ], + [ + 0, + 1, + 1, + 1 + ] + ], + "child_rank_per_term": 4, + "copied_information_per_term": 4, + "copy_mass_per_block": 16, + "forward_frame_nonzero_coefficients": 32, + "full_support_size_per_term_each_side": 4, + "inverse_frame_nonzero_coefficients_if_vector_restoration_is_needed": 32, + "line_count": 4, + "root_embedding_nonzero_coefficients": 16, + "root_span_extraction_reads": 4, + "scalar_accumulation_additions": 3, + "staged_forward_additions_for_D_and_T": 16, + "staged_forward_constant_multiplication_slots_for_D_and_T": 36, + "support_pairing_rank": 4, + "tensor_factors": 2, + "term_count": 4, + "term_matrix_rank_over_Q_i": 1, + "term_products_for_scalar_bilinear_form": 4 + }, + { + "D_frame_shape": [ + 8, + 8 + ], + "T_frame_shape": [ + 8, + 8 + ], + "ambient_dimension": 512, + "binary_pairing_matrix": [ + [ + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 0 + ], + [ + 1, + 1, + 1, + 1, + 1, + 1, + 0, + 1 + ], + [ + 1, + 1, + 1, + 1, + 1, + 0, + 1, + 1 + ], + [ + 1, + 1, + 1, + 1, + 0, + 1, + 1, + 1 + ], + [ + 1, + 1, + 1, + 0, + 1, + 1, + 1, + 1 + ], + [ + 1, + 1, + 0, + 1, + 1, + 1, + 1, + 1 + ], + [ + 1, + 0, + 1, + 1, + 1, + 1, + 1, + 1 + ], + [ + 0, + 1, + 1, + 1, + 1, + 1, + 1, + 1 + ] + ], + "child_rank_per_term": 8, + "copied_information_per_term": 8, + "copy_mass_per_block": 64, + "forward_frame_nonzero_coefficients": 128, + "full_support_size_per_term_each_side": 8, + "inverse_frame_nonzero_coefficients_if_vector_restoration_is_needed": 128, + "line_count": 8, + "root_embedding_nonzero_coefficients": 64, + "root_span_extraction_reads": 8, + "scalar_accumulation_additions": 7, + "staged_forward_additions_for_D_and_T": 48, + "staged_forward_constant_multiplication_slots_for_D_and_T": 104, + "support_pairing_rank": 8, + "tensor_factors": 3, + "term_count": 8, + "term_matrix_rank_over_Q_i": 1, + "term_products_for_scalar_bilinear_form": 8 + }, + { + "D_frame_shape": [ + 16, + 16 + ], + "T_frame_shape": [ + 16, + 16 + ], + "ambient_dimension": 4096, + "binary_pairing_matrix": [ + [ + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 0 + ], + [ + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 0, + 1 + ], + [ + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 0, + 1, + 1 + ], + [ + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 0, + 1, + 1, + 1 + ], + [ + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 0, + 1, + 1, + 1, + 1 + ], + [ + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 0, + 1, + 1, + 1, + 1, + 1 + ], + [ + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 0, + 1, + 1, + 1, + 1, + 1, + 1 + ], + [ + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 0, + 1, + 1, + 1, + 1, + 1, + 1, + 1 + ], + [ + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 0, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1 + ], + [ + 1, + 1, + 1, + 1, + 1, + 1, + 0, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1 + ], + [ + 1, + 1, + 1, + 1, + 1, + 0, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1 + ], + [ + 1, + 1, + 1, + 1, + 0, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1 + ], + [ + 1, + 1, + 1, + 0, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1 + ], + [ + 1, + 1, + 0, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1 + ], + [ + 1, + 0, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1 + ], + [ + 0, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1 + ] + ], + "child_rank_per_term": 16, + "copied_information_per_term": 16, + "copy_mass_per_block": 256, + "forward_frame_nonzero_coefficients": 512, + "full_support_size_per_term_each_side": 16, + "inverse_frame_nonzero_coefficients_if_vector_restoration_is_needed": 512, + "line_count": 16, + "root_embedding_nonzero_coefficients": 256, + "root_span_extraction_reads": 16, + "scalar_accumulation_additions": 15, + "staged_forward_additions_for_D_and_T": 128, + "staged_forward_constant_multiplication_slots_for_D_and_T": 272, + "support_pairing_rank": 16, + "tensor_factors": 4, + "term_count": 16, + "term_matrix_rank_over_Q_i": 1, + "term_products_for_scalar_bilinear_form": 16 + } + ], + "scope": { + "exact": "a two-root E8 subalphabet at level 1 and its tensor-product root frames at levels 2 through 4", + "label_pairing": "B_s=(G_0^tensor_s + all_ones) mod 2; represented by a new nondegenerate 2^s-bit form for s>=2", + "not_established": [ + "embedding the product labels in the selected 9-bit, 112-port E8 alphabet", + "an owner/dirty-state chronology or a selected-word consumer", + "a selected supplier, a kappa improvement, or an all-size theorem" + ] + }, + "selected_per_call_comparison": { + "COPY_plus_centre_a_ceiling_interval": [ + "1942057021/250000000000", + "1553645617/200000000000" + ], + "COPY_plus_centre_clears_five_percent": true, + "average_blocks_per_call": "56/9", + "candidate_decoder_copy_mass_per_call": "14336/9", + "candidate_local_copy_mass_per_call": "14912/9", + "candidate_rank16_child_count_per_call": "896/9", + "candidate_to_selected_local_mass_ratio": "7456/25137", + "direct_sum_blocks_per_nine_stage_replica": 56, + "extra_rank1_allowance_at_five_percent_target": { + "largest_integer_pass": 3919, + "next_integer_fails": 3920 + }, + "five_percent_target_a": "35491136290869/20000000000000000", + "forward_D_T_frame_nonzero_coefficients_per_call": "28672/9", + "frame_slot_proxy_clears_selected_endpoint": false, + "frame_slot_rank1_proxy_a_ceiling_interval": [ + "165877441/100000000000", + "1658774411/1000000000000" + ], + "frame_slot_rank1_proxy_units_per_call": "12824/3", + "idle_mass_per_call_under_parent_coverage": "50176/9", + "inverse_D_T_frame_coefficients_per_call_if_vector_output": "28672/9", + "live_families_per_nine_stage_replica": 896, + "local_profile_by_rank_per_call": { + "16": "896/9", + "8": 8 + }, + "parent_full_local_plus_centre_coverage_mass": "7232", + "retained_selected_centre_profile": { + "8": 8 + }, + "root_embedding_coefficients_per_call": "14336/9", + "root_span_restoration_reads_per_call": "896/9", + "scalar_accumulation_additions_per_call": "280/3", + "selected_local_copy_mass_allowance": 5586, + "staged_D_T_additions_per_call": "7168/9", + "staged_D_T_constant_multiplications_per_call": "15232/9", + "unchanged_selected_centre_charge_if_granted": 64, + "unpriced_physical_contract": "linear frame slots are listed exactly but the parent ceiling has no tariff converting them to copy rank; owner chronology, dirty-state consumer and outer hosting remain open" + }, + "status": "PASS_COMPLEX_E8_PAIR_BLOCK_CLIMB" +} diff --git a/research/complex-e8-pair-block-climb/SOURCES.json b/research/complex-e8-pair-block-climb/SOURCES.json new file mode 100644 index 0000000000..ca8280ee79 --- /dev/null +++ b/research/complex-e8-pair-block-climb/SOURCES.json @@ -0,0 +1,54 @@ +{ + "schema_version": 1, + "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "input", + "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81", + "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "67f085acd86acd7d4e03922d9cf4b26bca66fed5", + "sha256": "47b42433f5a85809a3aadd29c2c339da2c6ed728e4f7762df6b88bccb7874cf0" + }, + { + "path": "docs/research/community-batch1099-review.md", + "usage": "provenance", + "git_blob": "6cb6ec061a071a06a2d18cd4dc3e9a2b05d28099", + "sha256": "7e76d2c38e5fce30587835b7251df1430488ae4dd372611ef69a3f03f476b6cb" + }, + { + "path": "docs/research/complex-decoder-scope-map.md", + "usage": "input", + "git_blob": "727a8e0bd89da47e4842b02648c93466f42ff27f", + "sha256": "f22492089b77631cab712183beea11a8ed1ff0493d895a07f0022600d7af656c" + }, + { + "path": "research/community-frontier1094-audit/ASSEMBLY.json", + "usage": "provenance", + "git_blob": "5fd676df060f3b450782fdf5ff5f6beb63a5eeb0", + "sha256": "1122cb3a575f8c788345fc1bf4c108ac7c3250fb81a5988671f5eb04b3ab3045" + }, + { + "path": "research/community-frontier1094-audit/SELECTED-SOURCE.json", + "usage": "provenance", + "git_blob": "6a75493790b4eff9c4a98051ef8b01d6aad0d5a8", + "sha256": "79b3de5db3dbcb9829789ba58e9e45758926031e2a7d80667a08429d369be53b" + }, + { + "path": "research/complex-local-word-ceiling/RESULT.json", + "usage": "input", + "git_blob": "77f55043a679dd722330f1e2499863e36376d9f9", + "sha256": "d91d6c46509875abf1f61de67c2609656d3dc685451299f83caa6f922493692d" + }, + { + "path": "research/complex-local-word-ceiling/ceiling.py", + "usage": "input", + "git_blob": "6c0f54527d879396f689523bfde19928a9b6157c", + "sha256": "86a1432870b3b21d8454106ec9162fddc0471472d9214c590a1420f2426cedfc" + } + ] +} diff --git a/research/complex-e8-pair-block-climb/TASK.json b/research/complex-e8-pair-block-climb/TASK.json new file mode 100644 index 0000000000..005f5da272 --- /dev/null +++ b/research/complex-e8-pair-block-climb/TASK.json @@ -0,0 +1,72 @@ +{ + "schema_version": 1, + "task_id": "complex-rank-shape-decoder", + "priority_revision": 6, + "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "original_card": { + "id": "complex-rank-shape-decoder", + "question": "Can a decoder deliver the local paid mass in fewer, larger-rank children (block frame climbs instead of rank-1 to rank-3 steps)?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/complex-local-word-ceiling/README.md", + "research/complex-decoder-field-extension-seed44/README.md", + "research/complex-frame-pair-decoders/README.md", + "research/selected-k8-unrestricted-ends/README.md", + "research/eisenstein-reduction-copy-floor/README.md" + ], + "methods": [ + "Find one exact small decoding identity whose frame path climbs in blocks, and price its complete per-call profile.", + "Bound the best effective child rank achievable for one fixed support alphabet, including copies, frames and restoration." + ], + "acceptance_gate": "A per-call local profile, with all copied information, frames and restoration counted, whose ceiling exceeds the selected word's by at least 5%; masked or overcomplete supports must change an assumption of the eight-term all-pairs bound. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "research/complex-local-word-ceiling/verify.py" + ], + "expected": "PASS_COMPLEX_LOCAL_WORD_CEILING", + "inspect": "Read the selected word's per-call local profile, its packing ceiling and the lever table; run levers.py for the ideal budget of the lever you target.", + "scope": "Positive control and planning budget only; this is not a new construction or full cold replay." + }, + "first_experiment": "Before any synthesis, write the candidate per-call local profile (and centre charge / unpaid coordinates if changed) and screen it with ceiling.ceiling(); reject it if even the ideal ceiling does not beat the selected word's by your stated margin. Ideal budget: rank-16 delivery is 2.31x (levers.py).", + "bottleneck_link": "Rank-1 children are about half of recursive cost; the selected word's effective child rank is about 3.9. Larger-rank delivery lowers recursive cost per unit of paid mass.", + "allowed_variations": [ + "One masked, overcomplete or block decoder family with exact labels and supports.", + "A scoped lower bound on effective rank for one alphabet.", + "If the coverage law, template or guard changes, derive an applicable fully charged replacement bound instead of applying the incumbent ceiling outside its scope." + ], + "scope_change_triggers": [ + "Repacking idle remainders of an unchanged word (covered by the packing ceiling).", + "Repeating the eight-term all-pairs search inside its proved scope.", + "Only changing helper terminal subspaces and monotone frames within the fixed scalar word, entrances and cleanup contract already covered by #1995/#2013.", + "Searching below C=40 in the #2017 Eisenstein binary scalar-rectangle or fixed-support block-linear additive pairing model; specify a changed premise instead. This bound does not cover every complex decoder.", + "Continuing a partial cost improvement while leaving the same unpriced consumer, restoration or central-readout obligation unresolved; refresh the family expansion decision first. Local product-retiming evidence has a narrow scope and is not a ban on changed graphs or contracts." + ], + "overlap_terms": [ + "rank shape", + "block climb", + "masked decoder", + "overcomplete", + "effective rank" + ] + }, + "scope_status": "refined", + "actual_scope": "Construct the smallest explicit dense complex decoder on an actual E8 root pair, tensor-lift it through ranks 2, 4, 8 and 16, and account its support-pairing COPY/frame ledger in a nine-stage average profile with an explicit tariff sensitivity.", + "scope_change_reason": "The same broad card already has PR #3039's exact charged-block obstruction, PR #3066's mixed-profile correction, PR #1633's all-pairs overcomplete E8 rank form, and newer rank-cap/lever screens (#3811 and #3874); those do not exhibit this concrete product-root frame itinerary. This pass narrows to one two-root E8 identity and its four-level product lift, specifically measuring whether the full-support binary COPY rank and frame transforms fit the selected call. The product levels change the alphabet and are not represented as a selected E8 supplier.", + "bottleneck_link": "The selected local word pays rank mass 5586 per call across 896 live families. A rank-16 block can reduce the number of recursive children only if its exact support pairing, frame transforms and restoration fit inside the coverage mass; this identity measures that cost on the smallest explicit product alphabet.", + "budget_minutes": 60, + "stop_rule": "Stop after entrywise identities, support-pairing ranks, frame inverses/restoration, the correctly averaged 56-block/nine-stage profile, the COPY-plus-centre ceiling and the one-unit-per-frame-slot sensitivity. Do not search another product alphabet without an actual selected-port embedding and consumer tariff.", + "outcome": "partial", + "evidence": "python3 -I -B research/complex-e8-pair-block-climb/verify.py -> PASS_COMPLEX_E8_PAIR_BLOCK_CLIMB levels=4 rank16_block_copy_mass=256 average_profile_mass=14912/9 ideal_a=0.007768228085 frame_proxy_a=0.001658774411. The nine-stage average profile is {16:896/9, 8:8}; COPY-plus-centre ceiling is above the five-percent target. Exact linear frame/restoration counts are reported; the one-rank1-unit-per-slot sensitivity misses the selected endpoint, so the physical tariff and selected-code embedding remain unresolved.", + "author": "OpenAI Codex (homelab-05)", + "ai_assistance": "Substantial OpenAI Codex assistance (GPT-6 Luna xhigh): derivation, exact verifier, source review and package writing.", + "open_questions": [ + { + "question": "Can the exact 16-line block be embedded in the selected 9-bit, 112-port code and can its frame/consumer invoice fit the remaining five-percent allowance?", + "why_it_matters": "The COPY-plus-centre relaxation clears the target, but the product label form changes with rank and the parent model has no tariff for the dense frame maps. The exact one-rank1-unit-per-slot proxy exceeds the allowance by 356 units per average call.", + "first_step": "After the same-round fixed-alphabet bound is available, test its surviving supports against the 16-line identity, then trace one actual caller through D/T transforms and root-span restoration to derive a source-backed tariff.", + "blocked_by": "The concurrent macbook-05 assignment owns the fixed-support effective-rank bound; do not duplicate it. The selected-code consumer and owner chronology are absent, so no supplier admission follows from the ideal ceiling." + } + ] +} diff --git a/research/complex-e8-pair-block-climb/VERIFY.json b/research/complex-e8-pair-block-climb/VERIFY.json new file mode 100644 index 0000000000..e34140c61b --- /dev/null +++ b/research/complex-e8-pair-block-climb/VERIFY.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "certificates/selected-result.json", + "docs/research/complex-decoder-scope-map.md", + "research/complex-local-word-ceiling/RESULT.json", + "research/complex-local-word-ceiling/ceiling.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Entrywise Q(i) identities through rank 16; exact F2 support ranks; dense forward/inverse frame checks; product-root embedding and left-inverse restoration; nine-stage average COPY-plus-centre ceiling; exact rank-1 frame-slot allowance sensitivity." + } + ] +} diff --git a/research/complex-e8-pair-block-climb/verify.py b/research/complex-e8-pair-block-climb/verify.py new file mode 100644 index 0000000000..cc09e6edf7 --- /dev/null +++ b/research/complex-e8-pair-block-climb/verify.py @@ -0,0 +1,402 @@ +#!/usr/bin/env python3 +"""Exact Q(i) root-pair decoder and four-level tensor block climb. + +The checker uses only the Python standard library. It verifies every matrix +entry, every binary support-pairing rank, both frame inverses, the nine-stage +average copy profile, and a rank-1 frame-slot tariff sensitivity. +""" + +from __future__ import annotations + +import json +import sys +from fractions import Fraction as Q +from pathlib import Path + + +ROOT = Path(__file__).resolve().parent +REPO = ROOT.parents[1] +ZERO = (Q(0), Q(0)) +ONE = (Q(1), Q(0)) + + +def c(real=0, imag=0): + return (Q(real), Q(imag)) + + +def add(x, y): + return (x[0] + y[0], x[1] + y[1]) + + +def neg(x): + return (-x[0], -x[1]) + + +def sub(x, y): + return add(x, neg(y)) + + +def mul(x, y): + return (x[0] * y[0] - x[1] * y[1], x[0] * y[1] + x[1] * y[0]) + + +def inv(x): + den = x[0] * x[0] + x[1] * x[1] + if den == 0: + raise ZeroDivisionError("zero Gaussian rational") + return (x[0] / den, -x[1] / den) + + +def div(x, y): + return mul(x, inv(y)) + + +def conjugate(x): + return (x[0], -x[1]) + + +def scale(a, M): + q = c(a) + return [[mul(q, x) for x in row] for row in M] + + +def transpose(M): + return [list(row) for row in zip(*M)] + + +def matmul(A, B): + if not A or not B or len(A[0]) != len(B): + raise ValueError("matrix dimensions") + BT = transpose(B) + return [[sumq(mul(x, y) for x, y in zip(row, col)) for col in BT] for row in A] + + +def sumq(values): + out = ZERO + for value in values: + out = add(out, value) + return out + + +def kron(A, B): + return [[mul(A[i][j], B[r][k]) + for j in range(len(A[0])) for k in range(len(B[0]))] + for i in range(len(A)) for r in range(len(B))] + + +def kron_int(A, B): + return [[A[i][j] * B[r][k] + for j in range(len(A[0])) for k in range(len(B[0]))] + for i in range(len(A)) for r in range(len(B))] + + +def power_kron(A, exponent, integer=False): + out = A + op = kron_int if integer else kron + for _ in range(exponent - 1): + out = op(out, A) + return out + + +def inverse_matrix(A): + n = len(A) + if any(len(row) != n for row in A): + raise ValueError("inverse requires square matrix") + aug = [row[:] + [ONE if i == j else ZERO for j in range(n)] + for i, row in enumerate(A)] + for col in range(n): + pivot = next((r for r in range(col, n) if aug[r][col] != ZERO), None) + if pivot is None: + raise ValueError("singular frame") + aug[col], aug[pivot] = aug[pivot], aug[col] + p = inv(aug[col][col]) + aug[col] = [mul(p, x) for x in aug[col]] + for row in range(n): + if row == col or aug[row][col] == ZERO: + continue + q = aug[row][col] + aug[row] = [sub(x, mul(q, y)) for x, y in zip(aug[row], aug[col])] + return [row[n:] for row in aug] + + +def rank_f2(M): + A = [[int(x) & 1 for x in row] for row in M] + rows, cols = len(A), len(A[0]) if A else 0 + pivot_row = 0 + for col in range(cols): + pivot = next((r for r in range(pivot_row, rows) if A[r][col]), None) + if pivot is None: + continue + A[pivot_row], A[pivot] = A[pivot], A[pivot_row] + for r in range(rows): + if r != pivot_row and A[r][col]: + A[r] = [x ^ y for x, y in zip(A[r], A[pivot_row])] + pivot_row += 1 + if pivot_row == rows: + break + return pivot_row + + +def eq(A, B): + return len(A) == len(B) and all(len(a) == len(b) and a == b for a, b in zip(A, B)) + + +def nnz(A): + return sum(x != ZERO for row in A for x in row) + + +def fmt(x): + a, b = x + if b == 0: + return str(a) + if a == 0: + return f"{b}*i" + return f"{a}{'+' if b > 0 else ''}{b}*i" + + +def require(ok, why): + if not ok: + raise AssertionError(why) + + +def build_result(): + # Two actual E8 roots. Their Gram matrix is [[2,1],[1,2]]. + roots = [ + [1, 1, 0, 0, 0, 0, 0, 0], + [1, 0, 1, 0, 0, 0, 0, 0], + ] + R0 = [[c(x) for x in row] for row in roots] + G0_int = [[2, 1], [1, 2]] + G0 = [[c(x) for x in row] for row in G0_int] + require([sum(x * x for x in row) for row in roots] == [2, 2], "root norms") + require(sum(x * y for x, y in zip(*roots)) == 1, "root-pair dot product") + require(eq(matmul(R0, transpose(R0)), G0), "root Gram reconstruction") + + # A dense complex two-term factorization over Q(i), using ordinary transpose. + D0 = [[c(1), c(1)], [c(1), c(0, 1)]] + T0 = [[c(3, -1), c(1, 1)], [c(3, 1), c(-1, -1)]] + require(eq(matmul(D0, transpose(T0)), scale(2, G0)), "base decoder identity") + require(nnz(D0) == 4 and nnz(T0) == 4, "base frames must have full support") + T0_conj_transpose = transpose([[conjugate(x) for x in row] for row in T0]) + require(not eq(matmul(D0, T0_conj_transpose), scale(2, G0)), + "conjugate transpose must be rejected as a negative control") + + B0 = [[(G0_int[i][j] + 1) & 1 for j in range(2)] for i in range(2)] + require(B0 == [[1, 0], [0, 1]] and rank_f2(B0) == 2, "base support pairing") + + levels = [] + for s in range(1, 5): + n = 2 ** s + Rs = power_kron(R0, s) + Gs = power_kron(G0, s) + Ds = scale(Q(1, 2 ** (s - 1)), power_kron(D0, s)) + Ts = power_kron(T0, s) + require(eq(matmul(Ds, transpose(Ts)), scale(2, Gs)), f"level {s} decoder identity") + require(nnz(Ds) == n * n and nnz(Ts) == n * n, f"level {s} dense term supports") + + Gs_int = power_kron(G0_int, s, integer=True) + require(all(Gs[i][j][1] == 0 and Gs[i][j][0].denominator == 1 + and Gs_int[i][j] == Gs[i][j][0].numerator + for i in range(n) for j in range(n)), f"level {s} Gram consistency") + Bs = [[(Gs_int[i][j] + 1) & 1 for j in range(n)] for i in range(n)] + rank = rank_f2(Bs) + require(rank == n, f"level {s} binary support pairing rank") + require(all(Bs[i][j] == Bs[j][i] for i in range(n) for j in range(n)), + f"level {s} symmetric label form") + require(all(Bs[i][i] == 1 for i in range(n)), f"level {s} self-label pairing") + + Di = inverse_matrix(Ds) + Ti = inverse_matrix(Ts) + require(eq(matmul(Ds, Di), [[ONE if i == j else ZERO for j in range(n)] for i in range(n)]), + f"level {s} decoder-frame inverse") + require(eq(matmul(Ts, Ti), [[ONE if i == j else ZERO for j in range(n)] for i in range(n)]), + f"level {s} reader-frame inverse") + require(nnz(Di) == n * n and nnz(Ti) == n * n, f"level {s} inverse frame density") + + # Exact root-span embedding and left inverse: L_s R_s^T = I. + L0 = [[c(0), c(1), c(0), c(0), c(0), c(0), c(0), c(0)], + [c(0), c(0), c(1), c(0), c(0), c(0), c(0), c(0)]] + Ls = power_kron(L0, s) + require(eq(matmul(Ls, transpose(Rs)), + [[ONE if i == j else ZERO for j in range(n)] for i in range(n)]), + f"level {s} root-span restoration") + require(nnz(transpose(Rs)) == n * n and nnz(Ls) == n, + f"level {s} embedding/extraction counts") + + # For each of the two dense tensor frames, s stages apply 2x2 maps to + # n/2 pairs. D has an additional nontrivial global scale for s > 1. + staged_const_mults = 4 * n * s + (n if s > 1 else 0) + staged_adds = 2 * n * s + levels.append({ + "tensor_factors": s, + "ambient_dimension": 8 ** s, + "line_count": n, + "term_count": n, + "child_rank_per_term": rank, + "term_matrix_rank_over_Q_i": 1, + "copied_information_per_term": rank, + "copy_mass_per_block": n * rank, + "support_pairing_rank": rank, + "full_support_size_per_term_each_side": n, + "D_frame_shape": [n, n], + "T_frame_shape": [n, n], + "forward_frame_nonzero_coefficients": nnz(Ds) + nnz(Ts), + "inverse_frame_nonzero_coefficients_if_vector_restoration_is_needed": nnz(Di) + nnz(Ti), + "root_embedding_nonzero_coefficients": nnz(transpose(Rs)), + "root_span_extraction_reads": nnz(Ls), + "staged_forward_constant_multiplication_slots_for_D_and_T": staged_const_mults, + "staged_forward_additions_for_D_and_T": staged_adds, + "term_products_for_scalar_bilinear_form": n, + "scalar_accumulation_additions": n - 1, + "binary_pairing_matrix": Bs, + }) + + # A nine-stage replica has 896 live families, so 56 rank-16 blocks cover + # it. Report the exact per-call average rather than charging the entire + # replica to one call. + blocks_per_replica = 896 // 16 + require(blocks_per_replica == 56, "selected live-family count must partition into 16-line blocks") + blocks_per_call = Q(blocks_per_replica, 9) + # Retain the selected centre path explicitly: eight rank-8 centre terms + # cost 64. This is the same centre operation represented by the parent's + # coverage identity parameter, matching the selected profile. + local_profile = {16: Q(896, 9), 8: 8} + local_mass = sum(r * count for r, count in local_profile.items()) + decoder_copy_mass = Q(14336, 9) + require(local_mass == Q(14912, 9), "per-call COPY mass including the retained centre") + selected = json.loads((REPO / "certificates/selected-result.json").read_text()) + parent = json.loads((REPO / "research/complex-local-word-ceiling/RESULT.json").read_text()) + selected_local_mass = int(parent["selected"]["local_mass_per_call"]) + require(selected["decimal"] == "0.001672660197076918", "selected-result pin/value") + require(selected_local_mass == 5586, "selected local mass") + require(parent["model"]["live_families_per_call"] == "896/9", "selected coverage families") + require(parent["model"]["centre_per_call"] == 64, "selected centre charge") + + # The parent's coverage law has (73-1)*(896/9)+64 = 7232 total + # local+centre rank mass per call. First screen exact decoder COPY rank + # alone, then expose the unpriced linear frame/restoration bill separately. + coverage_total = Q(72 * 896, 9) + 64 + require(coverage_total == 7232 and local_mass < coverage_total, "coverage profile fits") + sys.path.insert(0, str(REPO / "research/complex-local-word-ceiling")) + import ceiling # noqa: E402 + local_model = ceiling.model(local_profile, 73, 896, 9, 64) + ideal_ceiling = ceiling.ceiling(local_profile, 73, 896, 9, 64, grid=Q(1, 10 ** 12)) + selected_a = Q(parent["ceiling"]["a_ceiling"]) + five_percent_target = selected_a * Q(21, 20) + require(ideal_ceiling[0] > five_percent_target, "COPY-only profile clears the five-percent screen") + + # Explicit tariff sensitivity: charge one rank-1 unit for each counted + # forward-frame multiply/add, embedding coefficient, restoration read and + # output accumulation add. This is a screen, not an asserted physical tariff. + rank1_proxy_per_block = 272 + 128 + 256 + 16 + 15 + rank1_proxy_per_call = Q(rank1_proxy_per_block * blocks_per_replica, 9) + proxy_profile = {16: Q(896, 9), 8: 8, 1: rank1_proxy_per_call} + proxy_ceiling = ceiling.ceiling(proxy_profile, 73, 896, 9, 64, grid=Q(1, 10 ** 12)) + require(proxy_ceiling[1] < selected_a, "one-unit-per-frame-slot proxy misses the selected endpoint") + + # Find the greatest integer number of additional rank-1 units per average + # call that still clears the +5% target under the pinned parent relaxation. + lo, hi = 0, 5639 + while hi - lo > 1: + mid = (lo + hi) // 2 + v = ceiling.relax({16: Q(896, 9), 8: 8, 1: Q(mid)}, 73, 896, 9, 64, + five_percent_target) + if v[1] < 1: + lo = mid + elif v[0] > 1: + hi = mid + else: + raise AssertionError("exact threshold bracket did not separate an integer grid point") + require(ceiling.relax({16: Q(896, 9), 8: 8, 1: Q(lo)}, 73, 896, 9, 64, + five_percent_target)[1] < 1, "rank-1 allowance lower endpoint") + require(ceiling.relax({16: Q(896, 9), 8: 8, 1: Q(hi)}, 73, 896, 9, 64, + five_percent_target)[0] > 1, "rank-1 allowance upper endpoint") + + return { + "status": "PASS_COMPLEX_E8_PAIR_BLOCK_CLIMB", + "coefficient_field": "Q(i), ordinary transpose", + "base_roots": roots, + "base_gram": G0_int, + "base_D": [[fmt(x) for x in row] for row in D0], + "base_T": [[fmt(x) for x in row] for row in T0], + "base_D_times_T_transpose": [[4, 2], [2, 4]], + "levels": levels, + "selected_per_call_comparison": { + "direct_sum_blocks_per_nine_stage_replica": blocks_per_replica, + "average_blocks_per_call": str(blocks_per_call), + "live_families_per_nine_stage_replica": 896, + "local_profile_by_rank_per_call": {"8": 8, "16": str(local_profile[16])}, + "candidate_rank16_child_count_per_call": str(local_profile[16]), + "candidate_decoder_copy_mass_per_call": str(decoder_copy_mass), + "retained_selected_centre_profile": {"8": 8}, + "candidate_local_copy_mass_per_call": str(local_mass), + "idle_mass_per_call_under_parent_coverage": str(local_model["idle_mass"]), + "selected_local_copy_mass_allowance": selected_local_mass, + "candidate_to_selected_local_mass_ratio": str(Q(local_mass, selected_local_mass)), + "parent_full_local_plus_centre_coverage_mass": str(coverage_total), + "unchanged_selected_centre_charge_if_granted": 64, + "forward_D_T_frame_nonzero_coefficients_per_call": str(Q(512 * blocks_per_replica, 9)), + "inverse_D_T_frame_coefficients_per_call_if_vector_output": str(Q(512 * blocks_per_replica, 9)), + "staged_D_T_constant_multiplications_per_call": str(Q(272 * blocks_per_replica, 9)), + "staged_D_T_additions_per_call": str(Q(128 * blocks_per_replica, 9)), + "root_embedding_coefficients_per_call": str(Q(256 * blocks_per_replica, 9)), + "root_span_restoration_reads_per_call": str(Q(16 * blocks_per_replica, 9)), + "scalar_accumulation_additions_per_call": str(Q(15 * blocks_per_replica, 9)), + "COPY_plus_centre_a_ceiling_interval": [str(ideal_ceiling[0]), str(ideal_ceiling[1])], + "five_percent_target_a": str(five_percent_target), + "COPY_plus_centre_clears_five_percent": True, + "frame_slot_rank1_proxy_units_per_call": str(rank1_proxy_per_call), + "frame_slot_rank1_proxy_a_ceiling_interval": [str(proxy_ceiling[0]), str(proxy_ceiling[1])], + "frame_slot_proxy_clears_selected_endpoint": False, + "extra_rank1_allowance_at_five_percent_target": { + "largest_integer_pass": lo, + "next_integer_fails": hi, + }, + "unpriced_physical_contract": "linear frame slots are listed exactly but the parent ceiling has no tariff converting them to copy rank; owner chronology, dirty-state consumer and outer hosting remain open", + }, + "scope": { + "exact": "a two-root E8 subalphabet at level 1 and its tensor-product root frames at levels 2 through 4", + "label_pairing": "B_s=(G_0^tensor_s + all_ones) mod 2; represented by a new nondegenerate 2^s-bit form for s>=2", + "not_established": [ + "embedding the product labels in the selected 9-bit, 112-port E8 alphabet", + "an owner/dirty-state chronology or a selected-word consumer", + "a selected supplier, a kappa improvement, or an all-size theorem", + ], + }, + "controls": [ + "ordinary-transpose base identity", + "all four tensor-level identities entrywise", + "all four support-pairing matrices have exact full F2 rank", + "D and T frames and inverses are dense and mutually invertible", + "root-span embedding and exact left-inverse restoration at every level", + "per-call scaling uses 56 blocks over nine stages, not all 56 blocks in one call", + "selected centre profile is retained explicitly as eight rank-8 terms", + "COPY-only ceiling and one-rank1-unit-per-frame-slot sensitivity", + "exact integer allowance for additional rank-1 units at the five-percent target", + ], + } + + +def main(): + import argparse + + parser = argparse.ArgumentParser() + parser.add_argument("--write", action="store_true", help="write deterministic RESULT.json") + args = parser.parse_args() + result = build_result() + payload = json.dumps(result, indent=2, sort_keys=True) + "\n" + path = ROOT / "RESULT.json" + if args.write: + path.write_text(payload) + elif not path.exists() or path.read_text() != payload: + raise SystemExit("RESULT.json differs from the exact replay; use --write deliberately") + screen = result["selected_per_call_comparison"] + ideal_a = Q(screen["COPY_plus_centre_a_ceiling_interval"][1]) + proxy_a = Q(screen["frame_slot_rank1_proxy_a_ceiling_interval"][1]) + print(f"{result['status']} levels=4 rank16_block_copy_mass=256 " + f"average_profile_mass={screen['candidate_local_copy_mass_per_call']} " + f"ideal_a={float(ideal_a):.12f} frame_proxy_a={float(proxy_a):.12f}") + + +if __name__ == "__main__": + main()