diff --git a/docs/ci-verification.md b/docs/ci-verification.md index 582e416aaf..50e8120dc0 100644 --- a/docs/ci-verification.md +++ b/docs/ci-verification.md @@ -2,6 +2,18 @@ ## Current selected-family replay +Resolve the [selected record](../certificates/selected-result.json) before +running a historical checkpoint. The current cold replay is +`make frontier4359-verify`, using the +[proof review](research/pr-intake-evidence/pr4359/PROOF-REVIEW.md), +[validation](research/pr-intake-evidence/pr4359/VALIDATION.json) and +[source manifest](../certificates/frontier4359-source.json). +The [frontier4359 workflow](../.github/workflows/frontier4359.yml) provides +hosted replay evidence. Metadata and source-pin checks are separate from +operator replay and do not discharge the inherited theorem assumptions. + +## Historical frontier1094 replay + Start with the [selected record](../certificates/selected-result.json). Its `reproduce`, `review`, `source_manifest` and `validation` fields identify the replay command, scoped assessment, source bindings and integration evidence. diff --git a/docs/research/current-status.md b/docs/research/current-status.md index 62a8cbb097..532af84312 100644 --- a/docs/research/current-status.md +++ b/docs/research/current-status.md @@ -1,12 +1,14 @@ # Current reviewed status -Selected conditional κ: **0.0023 = 23/10000**, zxv’s #4359 productive-helper construction, using Jacob Alan Sussman’s mixed-target recursion and the credited cumulative native/outer lineage. +Selected conditional κ: **0.0023** (= 23/10000), zxv’s #4359 productive-helper construction, using Jacob Alan Sussman’s mixed-target recursion and the credited cumulative native/outer lineage. [Selected record](../../certificates/selected-result.json) · [Proof review](pr-intake-evidence/pr4359/PROOF-REVIEW.md) · [Integration receipt](pr-intake-evidence/pr4359/INTEGRATION.json) · [Contributors](community-productive4359-contributors.md). Cold replay: `make frontier4359-verify`. The fresh 23-stage replay and 59 normalized artifacts pass; the changed interfaces have an AI-assisted proof review under retained analytic/native/fixed-tape hypotheses. Winning uniform templates are not materialized. This is not a complete formal or independent human verification. #4404 independently checks a narrower arithmetic/flow scope. -## Historical selected status through #1094 +All sections below are a historical snapshot; the selected-result.json record above is authoritative. + +## Historical checkpoint through #1094 Historical selected conditional κ: **0.001672660197076918**, Rohan Arun's #1094 on Jeremy Kothe's #1087 packing and the cumulative k8/slot/T16 construction. The bit supplier remains #589 on #555. diff --git a/research/d8-mixed-target-seeda97c8e/SOURCES.json b/research/d8-mixed-target-seeda97c8e/SOURCES.json index 9384463ff4..5dcfa9dd60 100644 --- a/research/d8-mixed-target-seeda97c8e/SOURCES.json +++ b/research/d8-mixed-target-seeda97c8e/SOURCES.json @@ -4,25 +4,25 @@ "files": [ { "path": "autoresearch.md", - "usage": "input", + "usage": "provenance", "git_blob": "8d5403e0f10f68a61d0cb9294fa2e83e872d1d82", "sha256": "215b3222f6a943edc69422a28ac21ea1f397ddf54770f1d87ac4195385d73699" }, { "path": "certificates/selected-result.json", - "usage": "input", + "usage": "provenance", "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" }, { "path": "docs/research/agent-task-catalog.json", - "usage": "input", + "usage": "provenance", "git_blob": "06c96f5579bb67ed1b86d334e78fbed7da6945f1", "sha256": "6686ad58f1fbdbc87134a78901b60fd53a20d3984355e91defbbebc9e9fa8075" }, { "path": "docs/research/current-status.md", - "usage": "input", + "usage": "provenance", "git_blob": "d73b4ff9da41f044e793422db4318be17e234a6c", "sha256": "adb54af005eb11edaf84d782fe729338680ff908f6d4fbf39ba1062d2e7d8a77" }, diff --git a/research/d8-mixed-target-seeda97c8e/VERIFY.json b/research/d8-mixed-target-seeda97c8e/VERIFY.json index caff4adf82..2726200ed3 100644 --- a/research/d8-mixed-target-seeda97c8e/VERIFY.json +++ b/research/d8-mixed-target-seeda97c8e/VERIFY.json @@ -4,10 +4,6 @@ "python": "3.12", "requirements": [], "inputs": [ - "autoresearch.md", - "certificates/selected-result.json", - "docs/research/agent-task-catalog.json", - "docs/research/current-status.md", "research/bit-three-register-lower-bound/README.md", "research/d8-mixed-target-seeda97c8e/verify.py" ], diff --git a/research/fresh-helper-boundary/ARITHMETIC-RESULT.json b/research/fresh-helper-boundary/ARITHMETIC-RESULT.json new file mode 100644 index 0000000000..686c36fb19 --- /dev/null +++ b/research/fresh-helper-boundary/ARITHMETIC-RESULT.json @@ -0,0 +1,219 @@ +{ + "BIT": { + "admitted": "273/100000", + "gap": "118653797/10000000000000", + "inherited_unrelaxed_saving": "27418653797/10000000000000" + }, + "compiler": { + "H": 349300000000, + "N": "2^349300000000", + "eta": { + "lower": "0.140815224484524968848722108625", + "upper": "0.140815224484524968848722108626" + }, + "gap": "1/700000000", + "integer_test_exponent": 499, + "logarithm_power": 13, + "theta_upper": "6/7", + "uniform_saving": "952437/350000000", + "word_materialized": false + }, + "fixed_profile_ceiling": { + "decreasing_C_interval": [ + "0", + "1/20" + ], + "negative_derivative_upper": { + "lower": "-178315.972608883259749333049784629374", + "upper": "-178315.972608883259749333049784629373" + }, + "negative_moment_upper": { + "lower": "-8137.901782546330185425252976230749", + "upper": "-8137.901782546330185425252976230748" + }, + "remaining_C_interval": [ + "1/20", + "1" + ] + }, + "gain_over_PR4416": "3477/100000000", + "headroom_from_declared_to_root": [ + "8051/400000000000", + "50319/2500000000000" + ], + "kappa": "68031/25000000", + "negative_controls": { + "closed_epsilon": [ + "epsilon_below_one", + "global_gamma_power_slack", + "actual_logarithmic_gamma_guard", + "source_axis_superpolynomial", + "gaussian_above_main", + "new_semantic_guard_with_C1_one" + ], + "closed_uniform_gap": [ + "new_complex_uniform_saving_above_b" + ], + "old_BIT_relaxation": [ + "actual_bit_above_effective" + ], + "unfunded_outer": [ + "main_transform_above_kappa", + "global_coordinate_router_above_kappa", + "fused_gaussian_above_kappa", + "group_bit_router_above_kappa", + "boundary_algebraic_matrix_above_kappa" + ] + }, + "outer": { + "functional_checks": { + "fixed_halo_explicit_metadata_branch": "13475000001/175000000", + "new_BIT_row_stock_sublinear_in_active_group": "697899997009/700000000000", + "new_semantic_group_guard": "3/700000000" + }, + "margins": { + "boundary_algebraic_matrix": "1333410398095129/490000000000000000", + "fused_gaussian": "1333410394285387/490000000000000000", + "global_coordinate_router": "238109/87500000", + "group_bit_router": "166676386785673/61250000000000000", + "group_scans": "349999999/350000000", + "main_transform": "1333409698095129/490000000000000000", + "microbox_face_corrections": "13475000001/175000000", + "polynomial_products": "699999999/700000000", + "sparse_union_movement": "200395910398095129/490000000000000000" + }, + "parameters": { + "a": "238109/87500000", + "b": "1904873/700000000", + "beta": "699999997/700000000", + "bit_saving": "273/100000", + "cap_xi": "445395909698095129/490000000000000000", + "complex_uniform_saving": "952437/350000000", + "d": "1/700000000", + "epsilon": "699999999/700000000", + "kappa": "68031/25000000", + "lambda_": "199455751/200000000", + "lambda_prime": "698095129/700000000", + "layout": "1/700000000", + "q": "1904871/700000000", + "r0": "1/7000000000", + "stop": "1/700000000", + "tested_saving": "2177/800000" + }, + "strict_checks": { + "actual_bit_above_effective": "383/43750000", + "actual_logarithmic_gamma_guard": "1/700000000", + "actual_logarithmic_group_guard": "44604091351904871/245000000000000000", + "alpha_logarithm_absorption": "1/7000000000", + "boundary_algebraic_matrix_above_kappa": "2798095129/490000000000000000", + "cap_above_band": "200395909698095129/490000000000000000", + "cap_below_cell": "44604089601904871/490000000000000000", + "cap_below_phase_cell_power": "534604090301904871/490000000000000000", + "complex_above_effective": "1/700000000", + "complex_below_one_over_32": "19970127/700000000", + "complex_endpoint": "1/350000000", + "epsilon_below_one": "1/700000000", + "epsilon_positive": "699999999/700000000", + "fine_prime_halo_umbrella": "7/2", + "fused_gaussian_above_kappa": "2794285387/490000000000000000", + "gaussian_above_main": "348095129/245000000000000000", + "global_coordinate_router_above_kappa": "1/175000000", + "global_gamma_power_slack": "9/7000000000", + "group_below_dimension": "1/350000000", + "group_bit_router_above_kappa": "436785673/61250000000000000", + "group_gauge_power_slack": "44604091316904871/245000000000000000", + "group_key_fits_record": "1/350000000", + "group_positive": "699999997/700000000", + "group_scans_above_kappa": "69809513/70000000", + "halo_covers_generic_inverse_radius": "5", + "improvement_over_user_baseline": "495134790400418148631/500000000000000000000000", + "lambda_above_internal": "1/1400000000", + "lambda_above_sigma": "3/1400000000", + "lambda_above_tau": "1/1400000000", + "lambda_prime_above_lambda": "1/1400000000", + "lambda_prime_above_leaf": "1398095127/490000000000000000", + "leaf_saving_above_effective": "698095127/490000000000000000", + "main_transform_above_kappa": "2098095129/490000000000000000", + "membership_arithmetic_fits_record": "1/700000000", + "microbox_face_corrections_above_kappa": "1684315473/21875000", + "microbox_halo_volume": "55300000003/700000000", + "new_complex_uniform_saving_above_b": "1/700000000", + "new_semantic_guard_with_C1_one": "1/700000000", + "polynomial_products_above_kappa": "698095131/700000000", + "positive_layout_slack": "1/700000000", + "q_below_effective": "1/700000000", + "q_below_internal": "1/700000000", + "q_below_leaf": "1398095127/490000000000000000", + "q_positive": "1904871/700000000", + "short_record_fallback": "698095127/700000000", + "source_axis_superpolynomial": "1/700000000", + "sparse_union_movement_above_kappa": "199062502798095129/490000000000000000", + "stop_below_one": "699999999/700000000", + "stop_positive": "1/700000000", + "strassen_integer_power_gap": "1951441519231", + "support_router_span": "3/700000000", + "theta_positive_polynomial_power": "2", + "union_header_fits_record": "3/700000000", + "union_tag_work_per_visit_fits_record": "3/700000000" + } + }, + "paid": { + "1": 33795, + "16": 448, + "2": 7725, + "3": 6675, + "32": 448, + "4": 1530, + "48": 448, + "5": 600, + "8": 1464 + }, + "paid_calls": 53133, + "productive_fields": 7688, + "relative_gain_over_PR4416": "1159/89549", + "root_bracket": [ + "1088504051/400000000000", + "6803150319/2500000000000" + ], + "status": "PASS_CHANGED_NATIVE_PROFILE_STRICTIFICATION_AND_COMPLETE_OUTER", + "strictification": { + "alpha": { + "lower": "0.999999983026163231936831206184", + "upper": "0.999999983026163231936831206185" + }, + "cutoff_base": 10, + "delta": { + "lower": "0.864870069524004068270352709182", + "upper": "0.864870069524004068270352709183" + }, + "gamma": { + "lower": "0.910935673068185945998089027910", + "upper": "0.910935673068185945998089027911" + }, + "gap": { + "lower": "0.000000705775426641554341705594", + "upper": "0.000000705775426641554341705595" + }, + "normalized_paid_upper": "312500529444649842944287051245464084985300648225953097729364854469515503029278664568874151635979493066877292627151728507225829268936433948299379518726558518343844530884174444838473561069623983608689185814338090148572417036912296673977860237369051387753314848294993638501683424262073636500572764166420861283708720335677094583332070847074689861555558356543552667138912721443073650953550760942655945597474686732201711464952735742366374988690440592748048891939/312500750000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + "rational_upper_limits": [ + "62499999/62500000", + "911/1000", + "173/200" + ], + "tail_offset": "3/10", + "target_floor_base": 15, + "tensor_power": 150 + }, + "targets": { + "121": 224, + "25": 448, + "4": 390, + "41": 448, + "5": 30, + "57": 448, + "7": 435, + "8": 630, + "9": 4635 + }, + "tested_saving": "2177/800000" +} diff --git a/research/fresh-helper-boundary/ATTEMPTS.md b/research/fresh-helper-boundary/ATTEMPTS.md new file mode 100644 index 0000000000..61dd1812f5 --- /dev/null +++ b/research/fresh-helper-boundary/ATTEMPTS.md @@ -0,0 +1,44 @@ +# Scope of discovery + +The new contribution changes helper entrances and exits jointly with scalar +contact frames. The old choice was optimized for a hosted owner fill. Once +all helper fields are fresh independent inputs, that objective is different: +price the paid moment minus the actual productive helper moment. + +Exploratory checks before this pivot (compiled C++ discovery, not registered +proofs or global optimality certificates): + +- All 262,144 paired p7 masks: 256 modular candidates; none passes the numerical test C=.00268649. + The old rank profile and root were reproduced. +- All 2,097,152 paired p8 masks: 576 modular candidates; none passes C=.00268649. +- 2,391,496 masks within six individual-bank toggles of the selected p7 mask: + 6,278 modular candidates; none passes the numerical test C=.00268649. +- No untouched consecutive native transports fuse. Single common-frame + components, and alpha expansions over the 1,159 existing frame spaces with + all boundaries fixed, gave no improvement at C=.003. + +The rank-sum modular test is a discovery filter. If a polynomial matrix A has +invertible A(1), a constant-basis diagonal monomial factorization implies that +the sum of ranks of its nonzero coefficient matrices equals the dimension. +A necessary mod-2 screen is particularly cheap here because A(1) stays +invertible mod 2. Scientific acceptance of the selected word uses rational +Laurent replay and full native replay, not this filter. + +Allowing helper boundary frames changes the result. A binary alpha-expansion +cut changes a selected set of scalar contacts to one frame, while hard +constraints preserve every nested chronological path and every warp contact. +The energy is the complete paid moment minus productive helper moment. Entry +and exit moves are optimized separately because their joint concave reward +is not a submodular binary cost. The submitted finite choices are recorded +explicitly in CHANGES.json; replay needs no optimizer or C++ compiler. + +The optimizer is a discovery aid. Passing every tested label does not prove +global optimality. In particular, simultaneous different-label moves, changed +scalar order, new operators, center sharing and new geometry remain open. + +A subsequent scan added all binary lines, all hyperplanes and all coordinate +subspaces of F2^9: 1,264 new distinct labels, for 2,423 tested spaces. Separate +entry and exit alpha-expansion sweeps from the submitted profile found no +negative move at C=.003. The registered proof uses only the final finite +choices and exact native/moment replay; no claim of global optimality or +exact mathematical acceptance is drawn from floating discovery costs. diff --git a/research/fresh-helper-boundary/CHANGES.json b/research/fresh-helper-boundary/CHANGES.json new file mode 100644 index 0000000000..45744fedd0 --- /dev/null +++ b/research/fresh-helper-boundary/CHANGES.json @@ -0,0 +1,562 @@ +{ + "entrances": [ + [448, 114, 0], + [449, 114, 0], + [450, 115, 0], + [451, 115, 0], + [452, 115, 0], + [453, 115, 0], + [454, 114, 0], + [455, 114, 0], + [457, 116, 0], + [458, 116, 0], + [460, 117, 0], + [462, 117, 0], + [473, 114, 0], + [474, 118, 0], + [475, 118, 0], + [476, 119, 0], + [477, 119, 0], + [478, 120, 0], + [480, 120, 0], + [482, 114, 0], + [483, 114, 0], + [484, 121, 0], + [485, 121, 0], + [486, 122, 0], + [487, 122, 0], + [492, 115, 0], + [493, 115, 0], + [502, 115, 0], + [503, 115, 0], + [504, 115, 0], + [513, 115, 0], + [514, 115, 0], + [515, 115, 0], + [516, 123, 0], + [517, 123, 0], + [518, 124, 0], + [519, 124, 0], + [520, 125, 0], + [521, 125, 0], + [522, 126, 0], + [523, 126, 0], + [524, 115, 0], + [525, 115, 0], + [526, 115, 0], + [527, 115, 0], + [528, 127, 0], + [529, 127, 0], + [530, 128, 0], + [531, 128, 0], + [532, 129, 0], + [533, 129, 0], + [534, 130, 0], + [535, 130, 0], + [536, 115, 0], + [537, 115, 0], + [538, 131, 114], + [539, 114, 0], + [544, 132, 0], + [545, 132, 0], + [546, 133, 0], + [547, 133, 0], + [548, 114, 0], + [549, 114, 0], + [550, 114, 0], + [551, 114, 0], + [553, 134, 0], + [555, 134, 0], + [556, 135, 0], + [557, 135, 0], + [558, 136, 0], + [559, 136, 0], + [563, 134, 0], + [565, 134, 0], + [570, 134, 0], + [571, 134, 0], + [572, 134, 0], + [573, 134, 0], + [578, 114, 0], + [579, 114, 0], + [580, 115, 0], + [581, 115, 0], + [582, 115, 0], + [583, 115, 0], + [585, 114, 0], + [586, 137, 0], + [587, 137, 0], + [588, 137, 0], + [589, 137, 0], + [590, 138, 0], + [591, 137, 0], + [592, 137, 0], + [593, 137, 0], + [596, 137, 0], + [597, 137, 0], + [598, 114, 0], + [599, 114, 0], + [600, 114, 0], + [601, 114, 0], + [606, 115, 0], + [607, 115, 0], + [608, 115, 0], + [609, 115, 0], + [610, 115, 0], + [611, 115, 0], + [612, 115, 0], + [614, 115, 0], + [615, 115, 0], + [616, 115, 0], + [617, 115, 0], + [618, 115, 0], + [619, 115, 0], + [620, 115, 0], + [621, 140, 0], + [622, 114, 0], + [623, 114, 0], + [624, 114, 0], + [625, 114, 0] + ], + "exits": [ + [277, 256, 299], + [282, 257, 299], + [293, 258, 301], + [298, 258, 301], + [307, 261, 303], + [309, 261, 303], + [311, 262, 1], + [314, 263, 303], + [323, 265, 304], + [325, 266, 304], + [327, 267, 1], + [330, 268, 304], + [337, 270, 305], + [339, 270, 305], + [341, 271, 305], + [346, 271, 305], + [353, 272, 307], + [355, 272, 307], + [357, 273, 307], + [362, 273, 307], + [369, 275, 308], + [371, 275, 308], + [373, 275, 308], + [378, 276, 308], + [385, 277, 309], + [387, 277, 309], + [389, 278, 309], + [394, 278, 309], + [494, 262, 1], + [495, 262, 1], + [505, 267, 1], + [506, 267, 1], + [548, 285, 1], + [560, 285, 1], + [566, 286, 279], + [567, 286, 279], + [568, 287, 280], + [569, 287, 280], + [574, 288, 279], + [575, 288, 279], + [576, 289, 281], + [577, 289, 281] + ], + "gates": [ + ["A", 626, 115, 0], + ["A", 627, 115, 0], + ["A", 628, 115, 0], + ["A", 629, 114, 0], + ["A", 630, 114, 0], + ["A", 631, 114, 0], + ["A", 632, 114, 0], + ["A", 633, 114, 0], + ["A", 1762, 134, 0], + ["A", 1763, 134, 0], + ["A", 1764, 134, 0], + ["A", 1765, 134, 0], + ["A", 1766, 134, 0], + ["A", 1767, 134, 0], + ["A", 1768, 134, 0], + ["A", 1769, 134, 0], + ["A", 1770, 134, 0], + ["A", 1771, 134, 0], + ["A", 1772, 134, 0], + ["A", 1773, 134, 0], + ["A", 1774, 134, 0], + ["A", 1775, 134, 0], + ["A", 1776, 134, 0], + ["A", 1777, 134, 0], + ["A", 1778, 134, 0], + ["A", 1779, 134, 0], + ["A", 1780, 134, 0], + ["A", 1781, 134, 0], + ["A", 1782, 134, 0], + ["A", 1783, 134, 0], + ["A", 1784, 134, 0], + ["A", 1785, 134, 0], + ["A", 1786, 134, 0], + ["A", 1787, 116, 0], + ["A", 1788, 119, 0], + ["A", 1789, 119, 0], + ["A", 1790, 119, 0], + ["A", 1791, 119, 0], + ["A", 1792, 117, 0], + ["A", 1793, 124, 0], + ["A", 1794, 124, 0], + ["A", 1795, 120, 0], + ["A", 1796, 124, 0], + ["A", 1797, 124, 0], + ["A", 1798, 125, 0], + ["A", 1799, 125, 0], + ["A", 1800, 125, 0], + ["A", 1801, 125, 0], + ["A", 1802, 135, 0], + ["A", 1803, 135, 0], + ["A", 1804, 117, 0], + ["A", 1805, 128, 0], + ["A", 1806, 128, 0], + ["A", 1807, 128, 0], + ["A", 1808, 128, 0], + ["A", 1809, 120, 0], + ["A", 1810, 130, 0], + ["A", 1811, 130, 0], + ["A", 1812, 130, 0], + ["A", 1813, 130, 0], + ["A", 1814, 133, 0], + ["A", 1815, 133, 0], + ["A", 1816, 116, 0], + ["A", 1817, 122, 0], + ["A", 1818, 122, 0], + ["A", 1819, 122, 0], + ["A", 1820, 122, 0], + ["A", 1821, 129, 0], + ["A", 1822, 129, 0], + ["A", 1823, 129, 0], + ["A", 1824, 129, 0], + ["A", 1825, 132, 0], + ["A", 1826, 132, 0], + ["A", 1827, 126, 0], + ["A", 1828, 126, 0], + ["A", 1829, 126, 0], + ["A", 1830, 126, 0], + ["A", 1831, 136, 0], + ["A", 1832, 136, 0], + ["A", 1833, 118, 0], + ["A", 1834, 118, 0], + ["A", 1835, 118, 0], + ["A", 1836, 118, 0], + ["A", 1837, 127, 0], + ["A", 1838, 127, 0], + ["A", 1839, 127, 0], + ["A", 1840, 127, 0], + ["A", 1841, 123, 0], + ["A", 1842, 123, 0], + ["A", 1843, 123, 0], + ["A", 1844, 123, 0], + ["A", 1845, 121, 0], + ["A", 1846, 121, 0], + ["A", 1847, 121, 0], + ["A", 1848, 121, 0], + ["A", 4031, 620, 621], + ["A", 4037, 622, 280], + ["B", 0, 115, 0], + ["B", 1, 115, 0], + ["B", 2, 115, 0], + ["B", 3, 115, 0], + ["B", 4, 115, 0], + ["B", 5, 115, 0], + ["B", 6, 115, 0], + ["B", 7, 115, 0], + ["B", 8, 114, 0], + ["B", 9, 114, 0], + ["B", 10, 114, 0], + ["B", 15, 114, 0], + ["B", 16, 114, 0], + ["B", 17, 114, 0], + ["B", 18, 114, 0], + ["B", 19, 115, 0], + ["B", 20, 115, 0], + ["B", 21, 115, 0], + ["B", 22, 115, 0], + ["B", 23, 115, 0], + ["B", 24, 115, 0], + ["B", 25, 115, 0], + ["B", 26, 115, 0], + ["B", 27, 114, 0], + ["B", 28, 114, 0], + ["B", 29, 114, 0], + ["B", 30, 114, 0], + ["B", 32, 114, 0], + ["B", 33, 114, 0], + ["B", 34, 114, 0], + ["B", 35, 115, 0], + ["B", 36, 115, 0], + ["B", 37, 115, 0], + ["B", 38, 115, 0], + ["B", 39, 115, 0], + ["B", 40, 115, 0], + ["B", 41, 115, 0], + ["B", 42, 115, 0], + ["B", 43, 114, 0], + ["B", 44, 114, 0], + ["B", 45, 114, 0], + ["B", 46, 114, 0], + ["B", 47, 114, 0], + ["B", 48, 114, 0], + ["B", 49, 115, 0], + ["B", 50, 115, 0], + ["B", 51, 115, 0], + ["B", 52, 115, 0], + ["B", 53, 115, 0], + ["B", 54, 115, 0], + ["B", 55, 115, 0], + ["B", 56, 115, 0], + ["B", 57, 114, 0], + ["B", 60, 114, 0], + ["B", 61, 137, 0], + ["B", 62, 137, 0], + ["B", 63, 137, 0], + ["B", 64, 137, 0], + ["B", 65, 137, 0], + ["B", 66, 137, 0], + ["B", 67, 137, 0], + ["B", 68, 137, 0], + ["B", 69, 137, 0], + ["B", 70, 137, 0], + ["B", 71, 137, 0], + ["B", 72, 137, 0], + ["B", 73, 137, 0], + ["B", 74, 137, 0], + ["B", 75, 137, 0], + ["B", 76, 137, 0], + ["B", 77, 137, 0], + ["B", 78, 137, 0], + ["B", 79, 137, 0], + ["B", 80, 137, 0], + ["B", 81, 137, 0], + ["B", 82, 137, 0], + ["B", 83, 137, 0], + ["B", 84, 137, 0], + ["B", 85, 137, 0], + ["B", 86, 137, 0], + ["B", 87, 137, 0], + ["B", 88, 137, 0], + ["B", 89, 137, 0], + ["B", 90, 137, 0], + ["B", 91, 137, 0], + ["B", 92, 137, 0], + ["B", 93, 137, 0], + ["B", 94, 137, 0], + ["B", 95, 137, 0], + ["B", 96, 137, 0], + ["B", 97, 114, 0], + ["B", 98, 114, 0], + ["B", 99, 114, 0], + ["B", 100, 114, 0], + ["B", 101, 114, 0], + ["B", 102, 114, 0], + ["B", 103, 114, 0], + ["B", 104, 114, 0], + ["B", 105, 114, 0], + ["B", 106, 114, 0], + ["B", 107, 114, 0], + ["B", 108, 114, 0], + ["B", 109, 114, 0], + ["B", 110, 114, 0], + ["B", 111, 114, 0], + ["B", 112, 114, 0], + ["B", 113, 114, 0], + ["B", 114, 114, 0], + ["B", 135, 115, 0], + ["B", 136, 115, 0], + ["B", 137, 115, 0], + ["B", 138, 115, 0], + ["B", 139, 115, 0], + ["B", 140, 115, 0], + ["B", 141, 115, 0], + ["B", 142, 115, 0], + ["B", 143, 115, 0], + ["B", 144, 115, 0], + ["B", 145, 115, 0], + ["B", 146, 115, 0], + ["B", 147, 115, 0], + ["B", 148, 115, 0], + ["B", 149, 115, 0], + ["B", 150, 115, 0], + ["B", 151, 115, 0], + ["B", 152, 115, 0], + ["B", 153, 115, 0], + ["B", 154, 115, 0], + ["B", 155, 115, 0], + ["B", 156, 115, 0], + ["B", 157, 115, 0], + ["B", 158, 115, 0], + ["B", 159, 115, 0], + ["B", 160, 115, 0], + ["B", 161, 115, 0], + ["B", 162, 115, 0], + ["B", 163, 115, 0], + ["B", 164, 115, 0], + ["B", 165, 115, 0], + ["B", 166, 115, 0], + ["B", 167, 115, 0], + ["B", 168, 115, 0], + ["B", 169, 115, 0], + ["B", 170, 115, 0], + ["B", 171, 115, 0], + ["B", 172, 115, 0], + ["B", 173, 115, 0], + ["B", 174, 115, 0], + ["B", 175, 115, 0], + ["B", 176, 115, 0], + ["B", 177, 115, 0], + ["B", 178, 115, 0], + ["B", 179, 115, 0], + ["B", 180, 115, 0], + ["B", 181, 115, 0], + ["B", 182, 115, 0], + ["B", 183, 115, 0], + ["B", 184, 115, 0], + ["B", 185, 115, 0], + ["B", 186, 115, 0], + ["B", 187, 115, 0], + ["B", 188, 115, 0], + ["B", 189, 115, 0], + ["B", 190, 115, 0], + ["B", 191, 115, 0], + ["B", 192, 115, 0], + ["B", 193, 115, 0], + ["B", 194, 115, 0], + ["B", 195, 115, 0], + ["B", 196, 115, 0], + ["B", 197, 115, 0], + ["B", 198, 115, 0], + ["B", 199, 114, 0], + ["B", 200, 114, 0], + ["B", 201, 114, 0], + ["B", 202, 114, 0], + ["B", 203, 114, 0], + ["B", 204, 114, 0], + ["B", 205, 114, 0], + ["B", 206, 114, 0], + ["B", 207, 114, 0], + ["B", 208, 114, 0], + ["B", 209, 114, 0], + ["B", 210, 114, 0], + ["B", 211, 114, 0], + ["B", 212, 114, 0], + ["B", 213, 114, 0], + ["B", 214, 114, 0], + ["B", 234, 114, 0], + ["B", 235, 114, 0], + ["B", 236, 114, 0], + ["B", 237, 114, 0], + ["B", 474, 138, 0], + ["B", 475, 731, 360], + ["B", 503, 743, 371], + ["B", 504, 744, 372], + ["B", 505, 745, 373], + ["B", 506, 746, 374], + ["B", 507, 747, 375], + ["B", 508, 748, 376], + ["B", 509, 749, 377], + ["B", 510, 750, 378], + ["B", 511, 751, 391], + ["B", 512, 752, 392], + ["B", 513, 753, 393], + ["B", 514, 754, 394], + ["B", 515, 755, 395], + ["B", 516, 756, 396], + ["B", 517, 757, 397], + ["B", 518, 758, 398], + ["B", 521, 256, 299], + ["B", 526, 257, 299], + ["B", 533, 765, 411], + ["B", 534, 766, 412], + ["B", 535, 767, 413], + ["B", 536, 768, 414], + ["B", 537, 769, 415], + ["B", 538, 770, 416], + ["B", 539, 771, 417], + ["B", 540, 772, 418], + ["B", 559, 779, 431], + ["B", 560, 780, 432], + ["B", 561, 781, 433], + ["B", 562, 782, 434], + ["B", 563, 783, 435], + ["B", 564, 784, 436], + ["B", 565, 785, 437], + ["B", 566, 786, 438], + ["B", 571, 261, 303], + ["B", 575, 263, 303], + ["B", 576, 263, 303], + ["B", 601, 268, 304], + ["B", 602, 268, 304], + ["B", 622, 271, 305], + ["B", 624, 270, 305], + ["B", 627, 271, 305], + ["B", 629, 270, 305], + ["B", 630, 140, 0], + ["B", 635, 801, 491], + ["B", 636, 802, 492], + ["B", 637, 803, 493], + ["B", 638, 804, 494], + ["B", 639, 805, 495], + ["B", 640, 806, 496], + ["B", 641, 807, 497], + ["B", 642, 808, 498], + ["B", 661, 813, 511], + ["B", 662, 814, 512], + ["B", 663, 815, 513], + ["B", 664, 816, 514], + ["B", 665, 817, 515], + ["B", 666, 818, 516], + ["B", 667, 819, 517], + ["B", 668, 820, 518], + ["B", 673, 275, 308], + ["B", 678, 276, 308], + ["B", 684, 131, 114], + ["cleanup_tail", 0, 286, 279], + ["cleanup_tail", 1, 286, 279], + ["cleanup_tail", 2, 286, 279], + ["cleanup_tail", 3, 287, 280], + ["cleanup_tail", 4, 287, 280], + ["cleanup_tail", 5, 287, 280], + ["cleanup_tail", 6, 288, 279], + ["cleanup_tail", 7, 288, 279], + ["cleanup_tail", 8, 288, 279], + ["cleanup_tail", 9, 289, 281], + ["cleanup_tail", 10, 289, 281], + ["cleanup_tail", 11, 289, 281], + ["cleanup_tail", 12, 262, 1], + ["cleanup_tail", 13, 262, 1], + ["cleanup_tail", 14, 262, 1], + ["cleanup_tail", 15, 267, 1], + ["cleanup_tail", 16, 267, 1], + ["cleanup_tail", 17, 267, 1], + ["cleanup_tail", 18, 267, 1], + ["cleanup_tail", 19, 267, 1], + ["cleanup_tail", 40, 262, 1], + ["cleanup_tail", 41, 262, 1], + ["cleanup_tail", 42, 262, 1], + ["cleanup_tail", 43, 262, 1], + ["cleanup_tail", 44, 262, 1], + ["cleanup_tail", 45, 262, 1], + ["cleanup_tail", 46, 262, 1], + ["cleanup_tail", 53, 267, 1], + ["cleanup_tail", 54, 267, 1], + ["cleanup_tail", 67, 285, 1], + ["cleanup_tail", 68, 285, 1], + ["cleanup_tail", 69, 285, 1], + ["cleanup_tail", 77, 285, 1], + ["cleanup_tail", 78, 285, 1], + ["cleanup_tail", 112, 267, 1], + ["cleanup_tail", 113, 267, 1], + ["cleanup_tail", 114, 267, 1], + ["cleanup_tail", 115, 267, 1], + ["cleanup_tail", 118, 262, 1], + ["cleanup_tail", 119, 262, 1], + ["cleanup_tail", 120, 262, 1] + ] +} diff --git a/research/fresh-helper-boundary/FRONTIER-CHECKS.json b/research/fresh-helper-boundary/FRONTIER-CHECKS.json new file mode 100644 index 0000000000..df86354352 --- /dev/null +++ b/research/fresh-helper-boundary/FRONTIER-CHECKS.json @@ -0,0 +1,21 @@ +{ + "schema": "frontier-watch/1", + "started_utc": "2026-10-21T19:32:20Z", + "interval_minutes": 20, + "checks": [ + { + "utc": "2026-10-21T19:52:05Z", + "latest_pr": 4437, + "highest_conditional_claim_pr": 4416, + "kappa": "0.00268647", + "action": "No stronger new claim found. Continue from p7 and PR4433 tail theorem." + }, + { + "utc": "2026-10-21T20:12:23Z", + "latest_pr": 4442, + "highest_conditional_claim_pr": 4440, + "kappa": "0.00296", + "action": "Audited exact head 40e22a83; registered replay passed. Switched to the stronger query-thinned construction and combined the verified helper retiming. New result is in research/fresh-helper-thinned." + } + ] +} diff --git a/research/fresh-helper-boundary/NATIVE-RESULT.json.gz b/research/fresh-helper-boundary/NATIVE-RESULT.json.gz new file mode 100644 index 0000000000..e6fdb31624 Binary files /dev/null and b/research/fresh-helper-boundary/NATIVE-RESULT.json.gz differ diff --git a/research/fresh-helper-boundary/PROOF.md b/research/fresh-helper-boundary/PROOF.md new file mode 100644 index 0000000000..4fe9fa7eec --- /dev/null +++ b/research/fresh-helper-boundary/PROOF.md @@ -0,0 +1,224 @@ +# Proof and conditional transfer + +## 1. Boundary contract + +Use the source full-identity native unit with 632 independent persistent +fields: 224 main fields and 408 helpers. Its two orientations give the source +main shears, while every helper is autonomous in its own logical reference. +The separately owned C0 field is cleared before each use and at return. No +arbitrary persistent input is overwritten or cleared. + +A field at frame f has physical value `C_f z`, where z denotes its logical +value and `C_f` is the source canonical Fourier frame. At entry this means +`z=C_start^-1 x` for an arbitrary physical input x. It does **not** require +precomputing a Fourier transform of x for free. The helper's actual final +operator is `C_end C_start^-1`, not merely `C_end`. + +For nested frame spaces S0` and `F(.0027212601276)<0`. To establish a fixed-profile +ceiling, arithmetic.py encloses `sum (T_r-P_r) r^(1-C) log r` on each of 16 +closed intervals covering `[0,1/20]`, and proves a strictly positive lower +bound throughout. Thus F is strictly decreasing there. On 128 further closed +intervals covering `[1/20,1]`, it bounds F directly strictly below zero. These +are interval implications for every real C in the covered intervals, not +extrapolation from point samples. The positive rank-one surplus at C=0 then +gives the unique relevant crossing and excludes any later positive region. + +A chronological tensor power multiplies both moments. Paid completion of a +rank-K target by D axes changes its moment by `(K+D)^t-K^t <= D^t`, which is +at most the added paid charge. Splitting a paid job on disjoint axes increases +or preserves its t-charge. Hence tensoring, this paid completion and paid +splitting cannot pass the raw fixed-profile ceiling. This is not a ceiling +on different native profiles or other algorithms. + +## 5. Pay both strictification tails + +Let `C=.00272125`, `t=1-C`, `u=3/10`, `v=150`, `J=10^v` and `L=15^v`. +Use the chronological native product of PR4416 and PR4433, restoring every +whole-job matcher and center before resuming a suspended caller. The product +has target and paid moments `T_t^v` and `P_t^v`, respectively; it is a +substitution of whole array programs, not the tensor power of a sum. + +Canonicalize each complete raw job with both recorded monomial factors; these +need not be an inverse pair. Subsequent placement on specified disjoint axes +is coordinate conjugation. No raw Clifford endpoint is assumed conjugate to +a canonical Fourier transform merely because its rank agrees. + +After the product finishes, complete every productive rank KJ, its split charge is at most +`2 R J^-C <= 2 R^(t+u) J^-u`, since `t+u>=1`. A completion has charge below +`2 L J^-C`. Therefore the complete normalized paid moment is bounded by + +``` +alpha^v + 2 gamma^v + 2 delta^v, +alpha=P_t/T_t, +gamma=P_(t+u)/(10^u T_t), +delta=7688*15/(10^C T_t). +``` + +The interval engine certifies `alpha<1-16/10^9`, `gamma<911/1000` and +`delta<173/200`. Bernoulli's inequality and an exact rational power test give + +``` +1/(1+150*16/10^9) + 2*(911/1000)^150 + 2*(173/200)^150 < 1. +``` + +Both original tails and every completion are paid. The product ambient rank +is `m=121^150`, with no need to materialize its immense word. + +## 6. Uniform compiler, BIT and outer bill + +Use the inherited finite integer mixed-target compiler only after strict +separation. Its fields, source complements, owned centers, integral batching, +matcher restoration and final exits are those of the specified new unit. +The new logarithmic majorant of PR4433 applies with `theta=6/7` and power 13: +`10^7<15^6`, `2*(10^150)^7 <= (121^150)^6`, and +`eta=t*121^(-150*C) > theta^13`. Its base-range condition is checked as well. +For declared `kappa=.00272124`, put `d=(C-kappa)/7=1/700000000` and uniform +saving `C-d`. The explicit integer comparison at `H=349300000000` is + +``` +(H+1)^13 < 2^499, d*H=499. +``` + +It specifies a finite uniform supplier at `N=2^H` with the required strict +saving. The instruction list and integer width B_N are generated by the +source finite algorithm rather than emitted here. + +The source BIT all-size parameter proof gives, before its last relaxation, +`(1-.003)*.00275 + .003*.0000384599 = .0027418653797`. Admit this unchanged +supplier at `.00273`; both the atom/adapter and borrowed-stock inequalities +remain strict. No BIT native word, cover or precision premise is weakened. +The old `.0027` relaxation fails the new outer bill and is a rejection control. + +Set `b=kappa+5d`, `a=kappa+4d`, `q=kappa+3d`, `epsilon=1-d`, `beta=1-3d`, +`r0=d/10`, `stop=d` and `layout=d`. The complete retained ledger recomputes all +nine cost rows, 54 current strict predicates and three functional guards. +Every one is strictly positive at this point. Closed uniform/epsilon gaps, +the insufficient old BIT relaxation and the unfunded tested endpoint fail. + +## 7. Costs and the precise conditional boundary + +Replace the old finite-unit constants by counts of the actual new word: +3363 paid local calls, the complete unchanged scalar lists and coefficients, +new serialized monomial/phase generators, 632 persistent fields and one owned +C0, all 408 helper normalizers, the unchanged p7 bridges and whole idles, the +150-fold chronological substitution, every completion and split, and finally +every integer-compiler unit, route, owned bank and rank-one leaf. A literal +finite recursive enumeration defines their counts and coefficient heights; +no p3 raw count is substituted for the compiled word. The new transport and +helper recipes are available explicitly in NATIVE-RESULT.json.gz. Internal +normalizers are restored before resuming a caller. + +Apply the source finite-template precision and stock argument with these new +constants. The native fixed coefficients and generators are finite, semantic +prefix bounds are rechecked, and all changed movement/scalar/normalizer work +enters the finite constants. The positive outer spare powers absorb those +constants after an effective threshold, under the inherited semantic, +all-column, physical primitive and fixed-tape hypotheses. This is the same +conditional transfer mechanism used by PR4416/4433, not a proof that local +savings are automatically a multiplication theorem. + +Analytic decomposition, permitted physical movement and whole-job frame +realization, source all-column correctness, finite-template closure, fine-prime +padding, fixed-tape execution and exact recovery remain stated source premises. +There is no formal verification or independent human mathematical review of +the complete theorem, no practical implementation claim, and no selected-result +change. Source files and contributor attribution are retained. diff --git a/research/fresh-helper-boundary/README.md b/research/fresh-helper-boundary/README.md new file mode 100644 index 0000000000..cbcfab9ccd --- /dev/null +++ b/research/fresh-helper-boundary/README.md @@ -0,0 +1,155 @@ +# Conditional κ = 0.00272124 from fresh-helper boundary retiming + +This changes the complete native p7 paid profile and proposes + +``` +T(n) = O(n (log n)^(1 - 0.00272124)). +``` + +The conditional saving exceeds [PR4416](https://github.com/CrocSwap/integer-mult-bounds/pull/4416)'s +`0.00268647` by **0.00003477 (about 1.2943%)**, and the pinned selected +`0.0023` by **18.31%**. This is a conditional construction submitted for review; +it does not change the selected record or establish an unconditional theorem. + +The new lever is to optimize helper entrances and exits for **fresh independent +helper inputs**, rather than retain frames selected for a hosted owner fill. +Changing those boundaries together with scalar contact frames saves recursive +calls without changing the scalar order, coefficients, main operator, warp +contacts or owned center program. The exact finite patch changes **117 helper +entrances, 42 helper exits and 395 scalar contact frames**. + +| Complete raw p7 invoice | PR4416 | This construction | +| --- | ---: | ---: | +| Independent productive fields | 7,688 | 7,688 | +| Paid calls | 55,998 | **53,133** | +| Productive rank mass | 131,723 | 133,718 | +| Paid rank mass | 131,115 | 133,110 | +| Rank-one surplus | 608 | 608 | +| Proposed conditional κ | 0.00268647 | **0.00272124** | + +The call reduction is **2,865 (about 5.12%)**. These are finite instruction +counts, not measured runtime speedups. The changed masses illustrate why +counting calls or rank-one mass alone does not establish the saving: the exact +concave moment and complete consumer are checked separately. + +## Native unit and exact evidence + +For each forward or backward local invocation, the new productive helper +profile and complete paid profile are + +``` +H = {4:26, 5:2, 7:29, 8:42, 9:309}, +P = {1:2253, 2:515, 3:445, 4:102, 5:40, 8:8}. +``` + +Every one of the 408 helpers has an independent arbitrary input. The center +remains separately owned, explicitly cleared, reused and uncredited. The +source p7 controller is unchanged: `pairs=7, keep_idle_mask=232127`. Its full +rational Laurent word is replayed; all 2,688 main idle calls are retained. +The complete new raw profiles are + +``` +T = {4:390, 5:30, 7:435, 8:630, 9:4635, + 25:448, 41:448, 57:448, 121:224}, +P = {1:33795, 2:7725, 3:6675, 4:1530, 5:600, + 8:1464, 16:448, 32:448, 48:448}. +``` + +[PROOF.md](PROOF.md) proves the retiming equivalence and explains the complete +transfer. [CHANGES.json](CHANGES.json) is the explicit circuit patch; +`native.py` resynthesizes every transport and replays both orientations on all +632 arbitrary inputs using two retained literal interpreters. All new transport +edges and every distinct helper boundary are independently lowered and decoded +as exact Clifford operations, including their absolute phase. Unchanged +transport phase evidence and the original all-column/native model remain +inherited source premises. + +`arithmetic.py` uses the unchanged interval engine of +[PR4433](https://github.com/CrocSwap/integer-mult-bounds/pull/4433). It certifies + +``` +0.0027212601275 < fixed-profile mixed root < 0.0027212601276. +``` + +An interval argument covers all real `0 0 and margin(ROOT_HIGH)[1] < 0, 'Certified changed-profile root bracket') + need(KAPPA < TESTED < ROOT_LOW, 'Strict supplier and outer headroom') + # An interval proof over real C, rather than signs only at a finite mesh. + signed = {r: targets[r]-paid[r] for r in targets.keys() | paid.keys()} + derivative_lower = None + for i in range(16): + left, right = Q(i, 320), Q(i+1, 320) + lower = Q(0) + for r, count in signed.items(): + power = E.power(r, 1-right if count > 0 else 1-left) + term = E.mul(power, E.log_bounds(r)) + lower += count*term[0 if count > 0 else 1] + derivative_lower = lower if derivative_lower is None else min(derivative_lower, lower) + need(derivative_lower > 0, 'Moment is strictly decreasing on [0,1/20]') + negative_upper = None + for i in range(128): + left, right = Q(1,20)+Q(19*i,2560), Q(1,20)+Q(19*(i+1),2560) + upper = sum(count*E.power(r, 1-left if count > 0 else 1-right)[1 if count > 0 else 0] + for r, count in signed.items()) + negative_upper = upper if negative_upper is None else max(negative_upper, upper) + need(negative_upper < 0, 'Every C in [1/20,1] has negative moment') + t, v, c, b, u = 1-TESTED, 150, 10, 15, Q(3,10) + target = E.moment(targets, t) + alpha = E.divide(E.moment(paid,t), target) + gamma = E.divide(E.moment(paid,t+u), E.mul(E.power(c,u),target)) + delta = E.divide((Q(sum(targets.values())*b),)*2, E.mul(E.power(c,TESTED),target)) + limits = (1-Q(16,10**9), Q(911,1000), Q(173,200)) + for bounds, limit in zip((alpha,gamma,delta),limits): + need(0 < bounds[0] <= bounds[1] < limit < 1, 'Certified complete tail limit') + a, g, d = limits + normalized_upper = 1/(1+v*(1-a))+2*g**v+2*d**v + need(normalized_upper < 1, 'All product, original paid tail and padding charges fit') + need(1 < c < b < 121 and t+u >= 1, 'Strictification hypotheses') + # PR4433's logarithmic majorant, rebound to this changed complete invoice. + theta, power = Q(6,7), 13 + eta = E.scale(E.exp_interval(E.scale(E.log_bounds(121),-v*TESTED)),t) + need(10**7 < 15**6 and 2*(10**v)**7 <= (121**v)**6, 'Actual exit cutoff and shifted logarithm') + need(eta[0] > theta**power, 'Strict exit versus complement contraction') + need(E.exp_interval(E.scale(E.log_bounds(121),v*TESTED))[1] < 2**power, 'Full initial rank range') + gap = (TESTED-KAPPA)/7 + need(gap.numerator == 1, 'Explicit integer grid for the uniform rank') + step = gap.denominator + def wins(j): + return (step*j+1)**power < 2**j + lo, hi = 1, 2 + while not wins(hi): + lo, hi = hi, 2*hi + while hi-lo > 1: + mid = (hi+lo)//2 + if wins(mid): hi = mid + else: lo = mid + H = step*hi + need(H > 7*v and wins(hi) and not wins(hi-1), 'Strict finite uniform-rank integer test') + # The original BIT proof already supplies the stronger, unrelaxed value. + bit = native.read(ROOT/'research/kappa-rebuild/bit/BIT-ALLSIZE-PARAMETERS.json') + bit_raw = (1-Q(bit['atom_power']))*Q(bit['C1_after_cover'])+Q(bit['atom_power'])*Q(bit['old_ordinary_saving']) + bit_admitted = Q('.00273') + need(bit_raw == Q(bit['ordinary_saving_before_final_relaxation']) > bit_admitted > KAPPA, 'Retain the existing stronger BIT conversion') + need(Q(bit['atom_power']) > bit_raw and 1-bit_raw-Q(bit['atom_power']) > 0, 'Both BIT adapter/stock gaps') + O = native.load(ROOT/'research/pr4359-p7-padding/dependencies/compiler-refill/endpoint.py', 'fresh_boundary_outer') + params = {'kappa': KAPPA, 'tested_saving': TESTED, + 'complex_uniform_saving': KAPPA+6*gap, 'b': KAPPA+5*gap, + 'a': KAPPA+4*gap, 'q': KAPPA+3*gap, 'bit_saving': bit_admitted, + 'epsilon': 1-gap, 'beta': 1-3*gap, 'r0': gap/10, + 'stop': gap, 'layout': gap, 'd': gap} + outer = O.ledger(params) + need(len(outer['strict_checks']) == 54 and len(outer['functional_checks']) == 3, 'Complete consumer predicate inventory') + need(all(value > 0 for group in ('strict_checks','functional_checks') for value in outer[group].values()), 'Every inherited consumer predicate') + controls = {} + for label, patch in [('old_BIT_relaxation', {'bit_saving': Q('.0027')}), + ('closed_uniform_gap', {'complex_uniform_saving': params['b']}), + ('closed_epsilon', {'epsilon': Q(1)}), + ('unfunded_outer', {'kappa': TESTED})]: + bad = O.ledger(dict(params,**patch)) + failed = [key for key,value in bad['strict_checks'].items() if value <= 0] + need(failed, 'Reject '+label); controls[label] = failed + return encode({'status':'PASS_CHANGED_NATIVE_PROFILE_STRICTIFICATION_AND_COMPLETE_OUTER', + 'kappa':KAPPA, 'tested_saving':TESTED, 'gain_over_PR4416':KAPPA-PREVIOUS, + 'relative_gain_over_PR4416':(KAPPA-PREVIOUS)/PREVIOUS, + 'targets':dict(sorted(targets.items())), 'paid':dict(sorted(paid.items())), + 'productive_fields':sum(targets.values()), 'paid_calls':sum(paid.values()), + 'root_bracket':[ROOT_LOW,ROOT_HIGH], 'headroom_from_declared_to_root':[ROOT_LOW-KAPPA,ROOT_HIGH-KAPPA], + 'fixed_profile_ceiling':{'decreasing_C_interval':['0','1/20'], + 'negative_derivative_upper':E.display((-derivative_lower,)*2), + 'remaining_C_interval':['1/20','1'], 'negative_moment_upper':E.display((negative_upper,)*2)}, + 'strictification':{'tensor_power':v,'cutoff_base':c,'target_floor_base':b,'tail_offset':u, + 'alpha':E.display(alpha),'gamma':E.display(gamma),'delta':E.display(delta), + 'rational_upper_limits':limits, 'normalized_paid_upper':normalized_upper, + 'gap':E.display((1-normalized_upper,)*2)}, + 'compiler':{'theta_upper':theta,'logarithm_power':power,'eta':E.display(eta), + 'uniform_saving':params['complex_uniform_saving'],'gap':gap,'H':H, + 'N':'2^'+str(H), 'integer_test_exponent':hi, 'word_materialized':False}, + 'BIT':{'inherited_unrelaxed_saving':bit_raw,'admitted':bit_admitted,'gap':bit_raw-bit_admitted}, + 'outer':outer, 'negative_controls':controls}) + +if __name__ == '__main__': + result = run(native.read(HERE/'NATIVE-RESULT.json.gz')) + (HERE/'ARITHMETIC-RESULT.json').write_text(json.dumps(result,indent=2,sort_keys=True)+'\n') + print(json.dumps({k:result[k] for k in ('status','kappa','gain_over_PR4416','root_bracket','compiler')},sort_keys=True)) diff --git a/research/fresh-helper-boundary/discover-cut.cpp b/research/fresh-helper-boundary/discover-cut.cpp new file mode 100644 index 0000000000..5caa077ea0 --- /dev/null +++ b/research/fresh-helper-boundary/discover-cut.cpp @@ -0,0 +1,35 @@ +// Optional floating-point discovery, never a proof checker. Apache-2.0. +// Prepared with substantial OpenAI Codex assistance. +#include +#include +#include +#include +#include +#include +#include +#include +using namespace std; +struct Arc{int v,rev;double cap;}; +struct Flow{vector> a;vector level,ptr;Flow(int n):a(n),level(n),ptr(n){};void edge(int u,int v,double c){Arc x{v,int(a[v].size()),c},y{u,int(a[u].size()),0};a[u].push_back(x);a[v].push_back(y);}double send(int u,int t,double f){if(u==t)return f;for(int&i=ptr[u];i1e-8&&level[e.v]==level[u]+1){double z=send(e.v,t,min(f,e.cap));if(z>1e-8){e.cap-=z;a[e.v][e.rev].cap+=z;return z;}}}return 0;}vectorcut(int s,int t){while(true){fill(level.begin(),level.end(),-1);queueq;level[s]=0;q.push(s);while(!q.empty()){int u=q.front();q.pop();for(auto e:a[u])if(e.cap>1e-8&&level[e.v]<0){level[e.v]=level[u]+1;q.push(e.v);}}if(level[t]<0){vectorv(level.size());for(int i=0;i=0;return v;}fill(ptr.begin(),ptr.end(),0);while(send(s,t,1e15)>1e-8){}}}}; +struct Node{bool mut;int oldf,newf;}; +int main(int argc,char**argv){if(argc!=3){cerr<<"usage: discover-cut entry|exit output-file"<>F>>N>>E;vectordim(F);vector>space(F);for(int f=0;f>dim[f];for(auto&x:space[f])cin>>x;}vector>sub(F,vector(F,true));for(int i=0;inodes(N);vectoridx(N,-1),rev;for(int i=0;i>m>>nodes[i].oldf>>nodes[i].newf;nodes[i].mut=m;if(m){idx[i]=rev.size();rev.push_back(i);}}vector>edges(E);for(auto&[a,b]:edges)cin>>a>>b; + int H;cin>>H;vector>helpers(H);for(auto&[i,f]:helpers)cin>>i>>f; + vectorcandidates;for(int f=0;funary(V,0);int s=V,t=V+1; + for(auto[a,b]:edges){int fa=nodes[a].newf,fb=nodes[b].oldf;double e0=powers[dim[fb]-dim[fa]];int i=idx[a],j=idx[b]; + double e10=sub[g][fb]?powers[dim[fb]-dim[g]]:INF;double e01=sub[fa][g]?powers[dim[g]-dim[fa]]:INF; + if(i>=0&&j>=0){double w=e10+e01-e0;if(w<-1e-7){cerr<<"nonsubmodular"<=0)unary[i]+=e10-e0;else if(j>=0)unary[j]+=e01-e0; + } + for(auto[i,f]:helpers){int old=nodes[i].newf;double delta=(entry?(sub[g][f] && dim[g]dim[f]))?(entry?powers[dim[f]-dim[old]]-powers[dim[f]-dim[g]]:powers[dim[old]-dim[f]]-powers[dim[g]-dim[f]]):INF;unary[idx[i]]+=delta;} + for(int i=0;i=0&&reach[idx[a]]?g:fa,gb=idx[b]>=0&&reach[idx[b]]?g:fb;if(!sub[ga][gb]){legal=false;break;}delta+=powers[dim[gb]-dim[ga]]-powers[dim[fb]-dim[fa]];} + for(auto[i,f]:helpers)if(reach[idx[i]]){int old=nodes[i].newf;if(entry?(!sub[g][f]||dim[g]>=dim[f]):(!sub[f][g]||dim[g]<=dim[f])){legal=false;break;}delta+=entry?powers[dim[f]-dim[old]]-powers[dim[f]-dim[g]]:powers[dim[old]-dim[f]]-powers[dim[g]-dim[f]];} + if(legal&&delta < -1e-8){int count=0;for(int i=0;i=-1e-8){cerr<<"NO_GAIN round "<= 224: + continue + out.append(e) + for r, f in enumerate(c['final']): + climb(r, f) + return out + +def run(changes=None, phase_check=True): + c = read(BASE/'THREE-base-FULL-IDENTITY-CANONICAL.json.gz') + original = read(BASE/'THREE-base-FULL-IDENTITY-NATIVE.json.gz') + changes = read(HERE/'CHANGES.json') if changes is None else changes + for key, frame_key in (('entrances', 'start'), ('exits', 'final')): + seen = set() + for role, old, new in changes[key]: + need(role not in seen and 224 <= role < 632 and c[frame_key][role] == old, 'Bound unique helper boundary') + seen.add(role); c[frame_key][role] = new + maps = {d: gates(p) for d, p in original.items()} + need(set(maps['forward']) == set(maps['backward']), 'Both scalar orientations have the same contact inventory') + for key in maps['forward']: + f = original['forward'][maps['forward'][key]] + b = original['backward'][maps['backward'][key]] + need(b[1] == dual(f[1]) and b[2] == f[2], 'Actual inverse-transpose scalar correspondence') + changed = deepcopy(original) + seen = set() + for phase, ordinal, old, new in changes['gates']: + key = (phase, ordinal) + need(key not in seen and key in maps['forward'], 'Bound unique retimed scalar contact') + seen.add(key) + for d in changed: + e = changed[d][maps[d][key]] + need(e[2] == old, 'Original scalar frame pin') + e[2] = new + programs = {d: synthesize(c, p) for d, p in changed.items()} + V = load(ROOT/'research/kappa-causal-continuation/buffer-borrowing/verify_buffers.py', 'fresh_boundary_rows') + X = load(ROOT/'research/kappa-rebuild/complex/native_extensions.py', 'fresh_boundary_literal') + checks = {} + profiles = {} + for d, p in programs.items(): + rows, receipt = X.literal_replay(V, c, p, d == 'backward') + for r in range(632): + need(rows['L', r] == V.expected(('L', r), [], d == 'backward', False), 'Every actual arbitrary-input endpoint, role '+str(r)) + profiles[d] = Counter({int(k): v for k, v in receipt['paid_profile'].items()}) + rebound = deepcopy(c) + rebound['local_profile'] = dict(profiles[d]) + receipt['second_literal'] = V.replay(p, rebound, [], d == 'backward', False) + checks[d] = receipt + need(profiles['forward'] == profiles['backward'], 'Same complete native tariff in both orientations') + H = Counter() + for r in range(224, 632): + a, b = c['start'][r], c['final'][r] + need(span(c['frames'][a]) <= span(c['frames'][b]), 'Nested productive helper boundary') + width = len(c['frames'][b])-len(c['frames'][a]) + need(width > 0, 'Every declared helper is independently productive') + H[width] += 1 + physical = [] + if phase_check: + ce = load(ROOT/'research/t74-native-fast/vendor/native/new/code/borrow/vendor/clifford/clifford_exact.py', 'fresh_boundary_clifford') + P = load(ROOT/'research/kappa-function-composition/complex/prune_native.py', 'fresh_boundary_lowering') + N = X.N + old_edges = {(e[3], e[4]) for e in original['forward'] if e[0] == 'climb'} + new_edges = {(e[3], e[4]) for e in programs['forward'] if e[0] == 'climb'} + helper_edges = {(c['start'][r], c['final'][r]) for r in range(224, 632)} + for a, b in sorted((new_edges-old_edges) | helper_edges): + op = ce.canonical_frame(9, c['frames'][a]).adjoint().then(ce.canonical_frame(9, c['frames'][b])) + want = len(c['frames'][b])-len(c['frames'][a]) + directions = {} + for d in ('forward', 'backward'): + actual = P.conjugate(ce, op) if d == 'backward' else op + rec = N.lower_exact(P, ce, actual) + need(rec['rank'] == want, 'New physical Fourier rank including phase') + directions[d] = rec + physical.append({'old': a, 'new': b, 'rank': want, 'recipes': directions}) + return {'status': 'PASS_RETIMED_BOTH_ORIENTATIONS_ALL_632_COLUMNS', + 'helpers': dict(sorted(H.items())), 'paid': dict(sorted(profiles['forward'].items())), + 'changed_entrances': len(changes['entrances']), 'changed_exits': len(changes['exits']), + 'changed_scalar_frames': len(changes['gates']), 'native': checks, + 'new_physical_edges_and_boundaries': physical}, c, programs + +if __name__ == '__main__': + import argparse + p = argparse.ArgumentParser(); p.add_argument('--skip-phase', action='store_true'); p.add_argument('--write-result', action='store_true'); args = p.parse_args() + result, _, _ = run(phase_check=not args.skip_phase) + if args.write_result: + need(not args.skip_phase, 'Do not replace a complete phase receipt with a diagnostic') + (HERE/'NATIVE-RESULT.json.gz').write_bytes(gzip.compress((json.dumps(result, indent=2, sort_keys=True)+'\n').encode(),mtime=0)) + print(json.dumps({k: v for k, v in result.items() if k not in ('native', 'new_physical_edges_and_boundaries')}, sort_keys=True)) diff --git a/research/fresh-helper-boundary/verify.py b/research/fresh-helper-boundary/verify.py new file mode 100644 index 0000000000..e434dbf7c6 --- /dev/null +++ b/research/fresh-helper-boundary/verify.py @@ -0,0 +1,99 @@ +"""Replay the changed native unit and its conditional multiplication endpoint. + +Standard library only. Apache-2.0; substantial OpenAI Codex assistance. +""" +import argparse +import gzip +from copy import deepcopy +from hashlib import sha256, sha1 +import json +from pathlib import Path +import native +import arithmetic + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] + +def need(ok, why): + if not ok: + raise ValueError(why) + +def authenticate(): + manifest = native.read(HERE/'SOURCES.json') + seen = set() + for row in manifest['files']: + if row['usage'] != 'input': + continue + path = Path(row['path']) + need(not path.is_absolute() and '..' not in path.parts and str(path) not in seen, 'Canonical unique input') + seen.add(str(path)) + actual = ROOT + for part in path.parts: + actual /= part + need(not actual.is_symlink(), 'No source alias') + data = actual.read_bytes() + need(sha256(data).hexdigest() == row['sha256'], 'Changed source: '+str(path)) + need(sha1(b'blob '+str(len(data)).encode()+b'\0'+data).hexdigest() == row['git_blob'], 'Changed source Git blob') + return len(seen) + +def controls(result, c, programs): + # This is a literal original-word control, not a second mathematical review. + baseline, _, _ = native.run({'entrances':[], 'exits':[], 'gates':[]}, phase_check=False) + need(baseline['helpers'] == {5:28,6:18,7:56,8:93,9:213}, 'Recover the actual predecessor helper profile') + need(baseline['paid'] == {1:2487,2:713,3:224,4:102,5:20,8:8}, 'Recover the actual predecessor paid profile') + V = native.load(ROOT/'research/kappa-causal-continuation/buffer-borrowing/verify_buffers.py','boundary_control_rows') + rebound = deepcopy(c); rebound['local_profile'] = result['paid'] + bad = deepcopy(programs['forward']) + bad.pop(next(i for i, e in enumerate(bad) if e[0] == 'center')) + rejected = False + try: + V.replay(bad, rebound, [], False, False) + except (ValueError, AssertionError): + rejected = True + need(rejected, 'A missing paid center is rejected at the actual frame contact') + # A pure global-phase corruption has an unchanged Pauli tableau. + ce = native.load(ROOT/'research/t74-native-fast/vendor/native/new/code/borrow/vendor/clifford/clifford_exact.py','boundary_control_phase') + P = native.load(ROOT/'research/kappa-function-composition/complex/prune_native.py','boundary_control_decode') + row = result['new_physical_edges_and_boundaries'][0] + rec = deepcopy(row['recipes']['forward']) + def decode(r): + left = P.monomial(ce, r['left'],9) + if r['rank']: + return P.monomial(ce,r['right'],9).then(ce.fourier(9,range(r['rank']))).then(left) + return left + original = decode(rec) + rec['left']['phase'] = (rec['left']['phase']+1)%4 + changed = decode(rec) + need(changed.tab == original.tab and changed.zero_state() != original.zero_state(), 'Absolute phase corruption is detected beyond tableau equality') + return {'predecessor_recovered':True,'omitted_center_rejected':True,'global_phase_only_corruption_rejected':True} + +def verify(write=False): + count = authenticate() + result, c, programs = native.run() + math = arithmetic.run(result) + checks = controls(result,c,programs) + artifacts = {'NATIVE-RESULT.json.gz': result, 'ARITHMETIC-RESULT.json': math} + for name, value in artifacts.items(): + normalized = json.loads(json.dumps(value)) + if write: + data = (json.dumps(normalized,indent=2,sort_keys=True)+'\n').encode() + (HERE/name).write_bytes(gzip.compress(data,mtime=0) if name.endswith('.gz') else data) + else: + need(normalized == native.read(HERE/name), 'Exact receipt replay: '+name) + receipt = {'status':'PASS_FRESH_HELPER_BOUNDARY_CONDITIONAL_KAPPA', + 'kappa_decimal':'0.00272124', 'source_inputs':count, + 'physical_edges_and_boundaries':len(result['new_physical_edges_and_boundaries']), + 'changed_entrances':result['changed_entrances'], 'changed_exits':result['changed_exits'], + 'changed_scalar_frames':result['changed_scalar_frames'], + 'controls':checks, 'scientific_receipts':{name:sha256(gzip.decompress((HERE/name).read_bytes()) if name.endswith('.gz') else (HERE/name).read_bytes()).hexdigest() for name in artifacts}} + if write: + (HERE/'RESULT.json').write_text(json.dumps(receipt,indent=2,sort_keys=True)+'\n') + else: + need(receipt == native.read(HERE/'RESULT.json'), 'Final checked receipt') + return receipt + +if __name__ == '__main__': + parser = argparse.ArgumentParser() + parser.add_argument('--write-receipts', action='store_true', help='Author receipts explicitly; ordinary replay does not write.') + args = parser.parse_args() + print(json.dumps(verify(args.write_receipts),sort_keys=True)) diff --git a/research/fresh-helper-thinned/AUDIT-4440.md b/research/fresh-helper-thinned/AUDIT-4440.md new file mode 100644 index 0000000000..64c4a98675 --- /dev/null +++ b/research/fresh-helper-thinned/AUDIT-4440.md @@ -0,0 +1,44 @@ +# Audit of PR4440 at 40e22a83ed660d3d6074c4f2dbf14bfb621eee51 + +The 20:12 UTC frontier check found PR4440's conditional 0.00296 above the first +helper-retiming result. Work switched to that source. Its complete registered +Python 3.12.15 replay passed before this combination was developed. Normal +combined replay repeats its full verifier and compares its saved receipt. + +No blocking defect was found **under its stated native, arbitrary-column, +owned-erasure and transfer contracts**. This is an AI-assisted source/proof +and finite-replay audit, not independent human or formal theorem acceptance. + +- **Paid query primitive.** Clear an owned stream, copy the donor, pay one + rank-one Q or Q^-1 job, add/subtract into the target, and erase only the owned + stream. The donor is retained; copied data create no productive input. + The inverse complex Gaussian is normalized with its actual Pauli translation, + not an order-two assumption. Literal arbitrary X/Y/Z columns reject omitted + clear/erase steps. Arbitrary-column physical lowering and owned erasure remain + explicit retained contracts rather than consequences of the finite test. +- **Actual controller.** Rational Laurent and binary coefficient checks replay + every emitted LOCAL, QUERY_SHEAR, IDLE, bridge and boundary program. Replacing + even stages also removes exactly those stage factors from idle operators and + target monomials. Lost helper inventories are charged. A wrong query direction + or altered coefficient changes the checked operator. +- **Native geometry.** Complex forward/inverse contact phases use the same + old-nine/fresh-eight chart on all 112 ports; the central q is fixed. Removing + inactive spectator blocks does not remove an active transform. BIT separately + checks all 111 rational charts and the original native child/copy bills. +- **Chronology and owners.** Full calls return their center before the next + query call. The one sequential owned stream can be reused at raw level; + nested products allocate the distinct centers required by suspended callers. + All full-call helpers are fresh independent fields. No copy, center or inactive + stage receives productive credit. +- **Complete costs.** The literal and closed-form invoices agree. Paid products, + completion and splitting charge both tails; the strict compiler is used only + after separation. The stronger BIT conversion pays its delayed cover fallback + and changes its atom power to 0.004; retaining 0.003 fails the adapter comparison. + Nine outer rows, 54 predicates and four guards are recomputed, with controls. +- **Limits.** The huge winning words and widths are finite algorithmic + specifications. Source all-column, owned-erasure, legal matcher, tape, + precision, analytic and recovery obligations remain conditional. + +The combination below makes no edit to PR4440. Its full and query main operators +stay fixed. It replaces only each full unit by an all-input-equivalent native +unit, then independently rebuilds the complete paid/productive invoice. diff --git a/research/fresh-helper-thinned/PROOF.md b/research/fresh-helper-thinned/PROOF.md new file mode 100644 index 0000000000..bf68dc2b98 --- /dev/null +++ b/research/fresh-helper-thinned/PROOF.md @@ -0,0 +1,132 @@ +# Conditional combination proof + +## 1. Exact unit substitution + +Use the source full-identity main shears and autonomous helpers in both +orientations. The retiming lemma of `fresh-helper-boundary/PROOF.md` changes +helper entrance/exit gauges and scalar contact frames while preserving every +logical row, main boundary, warp contact, scalar order/coefficient and owned +center. Both actual native words are replayed on all 632 arbitrary input +columns; 320 distinct new transport edges/helper boundaries are lowered and +decoded with absolute phase. Every helper boundary is normalized with its +recorded input and output monomials around the complete local job. These +factors need not be an inverse pair. + +Consequently a full LOCAL call in PR4440's complex word can be replaced by +this unit without changing its physical main operator. Allocate its 408 fresh +helper fields on the same distinct owner slots. Their new target profile is +`{4:26,5:2,7:29,8:42,9:309}` and paid profile is +`{1:2253,2:515,3:445,4:102,5:40,8:8}`. Each center remains owned and uncredited. +The same formal gauge equivalence applies under the retained all-column block +lifts; no sum of operators is tensor-powered. + +The source p17 controller has 19 full calls and 16 copied query shears. Every +thin query, full-call phase contact, main boundary and whole idle is unchanged. +The copied-query primitive and its zero/erase and physical Q contracts are +those audited in AUDIT-4440.md. Substitution therefore preserves the entire +main word. The normal verifier freshly executes both source verifiers before +using this implication. + +## 2. Entire changed invoice + +Count the actual emitted source events. Each LOCAL contributes one new H and +P; each QUERY_SHEAR contributes 112 paid rank-one jobs and no productive field; +each nonzero IDLE contributes 224 jobs of rank eight times its listed active +stage count. Each actual main diagonal monomial contributes 112 independent +rank `1+8*number_of_active_stages` fields. This gives + +``` +T={4:494,5:38,7:551,8:798,9:5871,17:448,25:448,33:448, + 41:448,49:448,57:448,65:448,73:448,153:224}, +P={1:44599,2:9785,3:8455,4:1938,5:760,8:152,16:448, + 24:448,32:448,40:448,48:448,56:448,64:448,72:448}. +``` + +There are 11,560 independent productive fields, 69,273 paid calls and rank +masses 260,798 and 259,998. Surplus 800 is preserved. An independent subtraction +of nineteen old helper/paid inventories and addition of nineteen new ones to +the source invoice must agree exactly with these event counts. + +At C=.003001052 the strict raw moment is checked by two rational interval +engines. Root signs at .0030010541830 and .0030010541834 enclose the new root. +As in the source helper package, interval derivatives prove strict decrease +on [0,1/20], and 128 closed interval enclosures exclude any positive moment on +[1/20,1]. This is a fixed-profile ceiling, not a global optimum. Chronological +products multiply the moments; paid completion loses moment by concavity and +splitting increases paid charge. Those operations cannot beat this raw ceiling. + +## 3. Pay both tails and specify a finite uniform rank + +Use t=1-C, u=1/5, v=1024, cutoff J=20^v and floor L=21^v. Apply the source +chronological product and whole-job completion/splitting algorithm, preserving +all spectators, restored matchers, distinct productive fields and owned banks. +Exactly the same charged theorem bounds the normalized paid moment by + +``` +alpha^v + 2 gamma^v + 2 delta^v, +alpha=P_t/T_t, +gamma=P_(t+u)/(20^u*T_t), +delta=11560*21/(20^C*T_t). +``` + +The new exact limits are `alpha<1-10^-9`, `gamma<97/100`, `delta<19/20`. +The old gamma limit 31/32 fails on this changed invoice and is explicitly +rejected. Both new tail limits to power 128 are strictly below 1/16. Hence +both tails at v=1024 are below 2^-32, and the exact rational inequality is + +``` +1/(1+1024/10^9) + 4/2^32 < 1. +``` + +Every completion and original paid tail is included. Final paid ranks are +at most 20^v and every productive target is at least 21^v. The maximum target +and ambient rank is m=153^v. + +Use PR4433's general logarithmic majorant, not an uncharged direct compiler. +Put theta=63/64 and p=1000. Check `20^64<21^63`, +`2*(20^v)^64 <= (153^v)^63`, and `eta=t*153^(-v*C)>theta^1000`. +The complete base range satisfies `153^(v*C)<2^1000` as well. These are precisely +the shifted exit, complement and base-range hypotheses of that majorant. + +For declared kappa=.00300105, set d=(C-kappa)/7=1/3500000000 and uniform +saving C-d. Let H be the reported multiple of 3500000000 satisfying +`(H+1)^1000 < 2^(d*H)`, and reject the previous grid point. RESULT.json +records the exact integers, giving the explicit sufficient rank N=2^H. +The source integer mixed flow supplies its integral widths, complements, owned +centers and exit jobs. The massive word is algorithmically specified, not emitted. + +## 4. Nonrecursive work, BIT and outer bill + +The complete local scalar lists retain the checked maximum allowance 158,168. +Bound each paid-job and helper monomial pair by 1000 elementary fixed +nine-coordinate records: Gaussian elimination, swaps, quadratic/linear phases, +offsets and global phase fit this conservative bound. The resulting local +scalar plus route allowance is below 10^7. The remaining 240 fixed warp +events and 448 main boundary adapters contribute fewer than 688,000 further +elementary records, also within that 10^7 local budget. Nineteen such units, all source query +records, bridges, boundary words and fixed chart records fit the retained raw +10^9 record bound; the verifier checks that larger substituted allowance. + +Update every product/compiler count from this actual word. The source finite +record bound and precision/stock prescription include the new normalizers, +every paid query and copied stream, all completions/splits, source complements, +owned banks, routes and rank-one leaves. No small predecessor constant is +substituted for the final compiled word. Fixed constants are absorbed only +through the positive spare powers of the inherited conditional transfer. + +Retain PR4440's entire BIT construction: pre-cover saving .003459, covered +saving .00345 and atom power .004. Its ordinary saving is .0034363538396, +admitted at .0034, strictly above the new complex endpoint. Its adapter, stock, +cover, owned queries and effective compiler remain unchanged. Normal replay +freshly checks that complete source construction. + +Set b=kappa+5d, a=kappa+4d, q=kappa+3d, epsilon=1-d, beta=1-3d, +r0=d/10 and stop=layout=d. Recompute all nine outer rows, 54 strict predicates +and four functional guards, including the actual new BIT atom. Every check +passes. Old BIT admission, a closed uniform/epsilon gap and the unfunded tested +endpoint are rejected. + +The source arbitrary-column native, owned-erasure, permitted physical matching, +finite-template precision, analytic decomposition, fixed-tape, prime and exact +recovery contracts remain conditional premises. These finite exact checks are +not formal verification or independent human acceptance of the complete theorem. diff --git a/research/fresh-helper-thinned/README.md b/research/fresh-helper-thinned/README.md new file mode 100644 index 0000000000..344616d665 --- /dev/null +++ b/research/fresh-helper-thinned/README.md @@ -0,0 +1,92 @@ +# Conditional κ = 0.00300105: fresh helper retiming on query-thinned controllers + +This builds on the stronger [PR4440](https://github.com/CrocSwap/integer-mult-bounds/pull/4440) +found during the requested 20-minute frontier check. After auditing its exact +head, replace all 19 full complex native calls by the verified fresh-helper +unit of `research/fresh-helper-boundary`. The main controller, 16 paid query +shears and stronger ordinary BIT supplier stay those of PR4440. The proposed +conditional bound is + +``` +T(n) = O(n (log n)^(1 - 0.00300105)). +``` + +The gain is **0.00004105 (about 1.39%) over PR4440's 0.00296**, +**about 11.71% over PR4416's 0.00268647**, and **30.48% over the pinned +selected 0.0023**. The new result is author-checked and awaits review; it +retains the conditional source implementation and transfer contracts. + +| Complete complex raw invoice | PR4440 | Combined construction | +| --- | ---: | ---: | +| Full native calls / paid query shears | 19 / 16 | 19 / 16 | +| Independent productive fields | 11,560 | 11,560 | +| Paid calls | 72,902 | **69,273** | +| Productive / paid rank mass | 258,271 / 257,471 | 260,798 / 259,998 | +| Rank-one surplus | 800 | 800 | +| Proposed conditional κ | 0.00296 | **0.00300105** | + +The native retiming removes **3,629 paid calls**. It changes 117 helper +entrances, 42 exits and 395 scalar frames in each full invocation, with exactly +the same main operator and complete owned-center program. Thus substitution +is a native operator equivalence, not merely replacement of a histogram. +Every helper is still a distinct arbitrary original input; query copies and +centers receive no productive credit. [PROOF.md](PROOF.md) gives the join. + +The exact changed-profile root is enclosed by + +``` +0.0030010541830 < root < 0.0030010541834. +``` + +An interval proof covers every real `0 2^26*N^5 avoiding all fixed denominators and rank witnesses" + }, + "outer": { + "functional_checks": { + "actual_new_BIT_stock_sublinear": "871499999253/875000000000", + "fixed_halo_explicit_metadata_branch": "67375000001/875000000", + "new_BIT_row_stock_sublinear_in_active_group": "3489499997009/3500000000000", + "new_semantic_group_guard": "3/3500000000" + }, + "margins": { + "boundary_algebraic_matrix": "18381438244748161/6125000000000000000", + "fused_gaussian": "18381438234244483/6125000000000000000", + "global_coordinate_router": "10503679/3500000000", + "group_bit_router": "36762879968488963/12250000000000000000", + "group_scans": "1749999999/1750000000", + "main_transform": "18381436494748161/6125000000000000000", + "microbox_face_corrections": "67375000001/875000000", + "polynomial_products": "3499999999/3500000000", + "sparse_union_movement": "2506662688244748161/6125000000000000000" + }, + "parameters": { + "a": "10503679/3500000000", + "b": "8206/2734375", + "beta": "3499999997/3500000000", + "bit_saving": "17/5000", + "cap_xi": "5569162686494748161/6125000000000000000", + "complex_uniform_saving": "10503681/3500000000", + "d": "1/3500000000", + "epsilon": "3499999999/3500000000", + "kappa": "60021/20000000", + "lambda_": "996998949/1000000000", + "lambda_prime": "1744748161/1750000000", + "layout": "1/3500000000", + "q": "5251839/1750000000", + "r0": "1/35000000000", + "stop": "1/3500000000", + "tested_saving": "750263/250000000" + }, + "strict_checks": { + "actual_bit_above_effective": "1396321/3500000000", + "actual_logarithmic_gamma_guard": "1/3500000000", + "actual_logarithmic_group_guard": "555837316130251839/3062500000000000000", + "alpha_logarithm_absorption": "1/35000000000", + "boundary_algebraic_matrix_above_kappa": "6994748161/6125000000000000000", + "cap_above_band": "2506662686494748161/6125000000000000000", + "cap_below_cell": "555837311755251839/6125000000000000000", + "cap_below_phase_cell_power": "6680837313505251839/6125000000000000000", + "complex_above_effective": "1/3500000000", + "complex_below_one_over_32": "2471783/87500000", + "complex_endpoint": "1/1750000000", + "epsilon_below_one": "1/3500000000", + "epsilon_positive": "3499999999/3500000000", + "fine_prime_halo_umbrella": "7/2", + "fused_gaussian_above_kappa": "6984244483/6125000000000000000", + "gaussian_above_main": "869748161/3062500000000000000", + "global_coordinate_router_above_kappa": "1/875000000", + "global_gamma_power_slack": "9/35000000000", + "group_below_dimension": "1/1750000000", + "group_bit_router_above_kappa": "17468488963/12250000000000000000", + "group_gauge_power_slack": "555837316042751839/3062500000000000000", + "group_key_fits_record": "1/1750000000", + "group_positive": "3499999997/3500000000", + "group_scans_above_kappa": "3489496323/3500000000", + "halo_covers_generic_inverse_radius": "5", + "improvement_over_user_baseline": "635039790400418148631/500000000000000000000000", + "lambda_above_internal": "1/7000000000", + "lambda_above_sigma": "3/7000000000", + "lambda_above_tau": "1/7000000000", + "lambda_prime_above_lambda": "1/7000000000", + "lambda_prime_above_leaf": "85321/149536132812500", + "leaf_saving_above_effective": "2726169/9570312500000000", + "main_transform_above_kappa": "5244748161/6125000000000000000", + "membership_arithmetic_fits_record": "1/3500000000", + "microbox_face_corrections_above_kappa": "269489496329/3500000000", + "microbox_halo_volume": "276500000003/3500000000", + "new_complex_uniform_saving_above_b": "1/3500000000", + "new_semantic_guard_with_C1_one": "1/3500000000", + "polynomial_products_above_kappa": "872374081/875000000", + "positive_layout_slack": "1/3500000000", + "q_below_effective": "1/3500000000", + "q_below_internal": "1/3500000000", + "q_below_leaf": "85321/149536132812500", + "q_positive": "5251839/1750000000", + "short_record_fallback": "2726169/2734375", + "source_axis_superpolynomial": "1/3500000000", + "sparse_union_movement_above_kappa": "2488281256994748161/6125000000000000000", + "stop_below_one": "3499999999/3500000000", + "stop_positive": "1/3500000000", + "strassen_integer_power_gap": "1951441519231", + "support_router_span": "3/3500000000", + "theta_positive_polynomial_power": "2", + "union_header_fits_record": "3/3500000000", + "union_tag_work_per_visit_fits_record": "3/3500000000" + } + }, + "paid": { + "1": 44599, + "16": 448, + "2": 9785, + "24": 448, + "3": 8455, + "32": 448, + "4": 1938, + "40": 448, + "48": 448, + "5": 760, + "56": 448, + "64": 448, + "72": 448, + "8": 152 + }, + "paid_calls": 69273, + "productive_fields": 11560, + "query_shears": 16, + "scope": "Author-checked conditional construction; retained native/all-column, owned-erasure, whole-job, analytic, precision, tape, prime and recovery contracts. No selected promotion or formal/human acceptance.", + "source_heads": { + "PR4440": "40e22a83ed660d3d6074c4f2dbf14bfb621eee51", + "helper_retiming": "ccdae89b2ab9ced24ee3e7adfdb670ef80d223d9" + }, + "source_inputs": 41, + "status": "PASS_CONDITIONAL_FRESH_HELPER_QUERY_THINNED_KAPPA", + "strictification": { + "alpha": { + "lower": "0.999999997758999184602267590366", + "upper": "0.999999997758999184602267590367" + }, + "cutoff": 20, + "delta": { + "lower": "0.932537400874663431699700098660", + "upper": "0.932537400874663431699700098661" + }, + "floor": 21, + "gamma": { + "lower": "0.969126930833863729265427869330", + "upper": "0.969126930833863729265427869331" + }, + "limits": [ + "999999999/1000000000", + "97/100", + "19/20" + ], + "normalized_paid_upper": "2097152001953127/2097154147483648", + "power": 1024, + "tail_offset": "1/5", + "tested": "750263/250000000" + }, + "targets": { + "153": 224, + "17": 448, + "25": 448, + "33": 448, + "4": 494, + "41": 448, + "49": 448, + "5": 38, + "57": 448, + "65": 448, + "7": 551, + "73": 448, + "8": 798, + "9": 5871 + } +} diff --git a/research/fresh-helper-thinned/SOURCES.json b/research/fresh-helper-thinned/SOURCES.json new file mode 100644 index 0000000000..4089ad3711 --- /dev/null +++ b/research/fresh-helper-thinned/SOURCES.json @@ -0,0 +1,278 @@ +{ + "schema_version": 1, + "base_commit": "3a23e9d9d2e67833515d1c60a17e966bcdcab43c", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ed33caef5c5827693e9572d252a66f99cbb73d40", + "sha256": "5732707cc1e460b090b53f2463162749ad860de878a18f7408938671d295a9d9" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "64bfc5af6709ed9811171e0a2108f05e1219cb65", + "sha256": "352a6184713b8843d96fd2c2071eb7aeaa655906b7c51d45ad444912666c8a96" + }, + { + "path": "research/fresh-helper-boundary/ARITHMETIC-RESULT.json", + "usage": "input", + "git_blob": "686c36fb19680db327f797ebdfe612487d8c53f8", + "sha256": "5d25fec9ac4b036c93846a50dccfa4af030e2982f5cec02e28702193bf157cf7", + "pin": "head:ccdae89b2ab9ced24ee3e7adfdb670ef80d223d9:research/fresh-helper-boundary/ARITHMETIC-RESULT.json" + }, + { + "path": "research/fresh-helper-boundary/CHANGES.json", + "usage": "input", + "git_blob": "45744fedd0e28967aa72586048b8bc0c72f419a9", + "sha256": "cde73b8ff5b3c0d06e69e2293b991b24fd14a16dd4ccab7ff6b3439074a94624", + "pin": "head:ccdae89b2ab9ced24ee3e7adfdb670ef80d223d9:research/fresh-helper-boundary/CHANGES.json" + }, + { + "path": "research/fresh-helper-boundary/NATIVE-RESULT.json.gz", + "usage": "input", + "git_blob": "e6fdb31624e4eb8c7c770bb4422cd07ea99ab152", + "sha256": "37d0848458b289eb50271c47adef6e74014ae30be6363d09394b2337b566b839", + "pin": "head:ccdae89b2ab9ced24ee3e7adfdb670ef80d223d9:research/fresh-helper-boundary/NATIVE-RESULT.json.gz" + }, + { + "path": "research/fresh-helper-boundary/RESULT.json", + "usage": "input", + "git_blob": "e26608e20be115d28f8853a8c1a12bebfc8e8ec3", + "sha256": "34163eeeef1cd712de457d7fd3b0435f98a12ac456b82256b078f33225456fbd", + "pin": "head:ccdae89b2ab9ced24ee3e7adfdb670ef80d223d9:research/fresh-helper-boundary/RESULT.json" + }, + { + "path": "research/fresh-helper-boundary/SOURCES.json", + "usage": "input", + "git_blob": "0b40275502f4263a19905f4fb50e346a3629c712", + "sha256": "01998e9b86222d10811fc0114dcd5c946ff9e95025a7cacd00e67a3eefe543d0", + "pin": "head:ccdae89b2ab9ced24ee3e7adfdb670ef80d223d9:research/fresh-helper-boundary/SOURCES.json" + }, + { + "path": "research/fresh-helper-boundary/arithmetic.py", + "usage": "input", + "git_blob": "4822f04ae09d84a16e8fa8656a533e23fd4068f0", + "sha256": "212bae96d0ddcbc25076afe2589a47736c66b77420057f28c44c937ad087fc07", + "pin": "head:ccdae89b2ab9ced24ee3e7adfdb670ef80d223d9:research/fresh-helper-boundary/arithmetic.py" + }, + { + "path": "research/fresh-helper-boundary/native.py", + "usage": "input", + "git_blob": "1b36f6cb5f205c33bf48811e0b1b3621c55e8154", + "sha256": "9b55a2d3c3972148fae9d112e745d9244968166bd89bd900c938f429fc76ab29", + "pin": "head:ccdae89b2ab9ced24ee3e7adfdb670ef80d223d9:research/fresh-helper-boundary/native.py" + }, + { + "path": "research/fresh-helper-boundary/verify.py", + "usage": "input", + "git_blob": "e434dbf7c68afa0390a307fd15f32348b0e87207", + "sha256": "4c18851214400cf955e10565d89357029d9e765140233831472ce23f0c3ee7bf", + "pin": "head:ccdae89b2ab9ced24ee3e7adfdb670ef80d223d9:research/fresh-helper-boundary/verify.py" + }, + { + "path": "research/higher-moment-strictification/README.md", + "usage": "input", + "git_blob": "0a736ca89e1eafb73a30e1f2589cc45e6b5f76c3", + "sha256": "ebe80b68ff026ce90f71f274c31744f4c0b36132d15ebb7e39cf2d5df4df270d" + }, + { + "path": "research/higher-moment-strictification/verify.py", + "usage": "input", + "git_blob": "4b24a5096154736ce060474eb8c72dc64c303699", + "sha256": "0ce7e7137422d5ffeda22085c81fa88471bbe963100fdad62e659f1e3bf89326" + }, + { + "path": "research/kappa-0023-productive-jobs/dependencies/kappa-next-regime/bit-compression/carrier-reuse/reference/joint_pair_dag.py", + "usage": "input", + "git_blob": "8b40135a84e7f0f0cd44bed69655801310b916a7", + "sha256": "8a0de761642d21919e969475c3f13e5d01a4bae7343c1e1f37c586d94b676a85" + }, + { + "path": "research/kappa-0023-productive-jobs/dependencies/kappa-next-regime/direct-decoder/sources/DATA-PHASES.json", + "usage": "input", + "git_blob": "d9a4f84211182ca200c081ea061d724c8a2cfb70", + "sha256": "c5916ff312678f12aba403847643fbbc29f643acec60bdf836fa56cd3e8251fa" + }, + { + "path": "research/kappa-causal-continuation/buffer-borrowing/verify_buffers.py", + "usage": "input", + "git_blob": "5a55034ec9e6185d981e16c28e1e2e455069e2cb", + "sha256": "106b4d5e052427230df452f0c901d5390a0583782960b80a8af94d9a984022c7" + }, + { + "path": "research/kappa-function-composition/complex/prune_native.py", + "usage": "input", + "git_blob": "8c3e11b2408fa96eefa3ebe7952d1b11b90b772b", + "sha256": "f2b37c183a10922eabc8e0436b426a08866430e96bd0adc7e178951c7fbb5257" + }, + { + "path": "research/kappa-rebuild/architecture/mixed_target_probe.py", + "usage": "input", + "git_blob": "4fc05ab08138218ba9f09e5c89b649afae7c914e", + "sha256": "011c3c9d0cf81103dc84d709a0e36793eb7c5ae3f23c85eac27650ef13afa04a" + }, + { + "path": "research/kappa-rebuild/bit/BIT-ALLSIZE-PARAMETERS.json", + "usage": "input", + "git_blob": "fbe6da7241357d89cf5c55b2e7ce2d0d046be32a", + "sha256": "edb273f59a27356ad89f38791590c3c806b228c3510eb508e01e89f2caba95ef" + }, + { + "path": "research/kappa-rebuild/bit/BIT-P3-NATIVE-BINDING.json", + "usage": "input", + "git_blob": "e8c5e4f077fea0bef355e6c3013c7f252d3606cf", + "sha256": "9ece46fdfda6182e757e9a3b1f513fb3d029d730f3bafdcd6ed59180a14175b0" + }, + { + "path": "research/kappa-rebuild/bit/DELAYED-COVER-BRIDGE.md", + "usage": "input", + "git_blob": "a58774e237c9362869a60a22bda35be09fb85872", + "sha256": "9731b93026717f5fa15851e3633cbb4bdc76eba2bffb9d6b4a3b69f7dd502443" + }, + { + "path": "research/kappa-rebuild/bit/MIXED-PRODUCTIVE-BIT.json", + "usage": "input", + "git_blob": "6a139eedbc1015c13df6f2a4333e1a89b5edd18d", + "sha256": "2f69a19f417c0e0d141c180f9b2fae3d358391b9a230f5848ee07c45450e70bf" + }, + { + "path": "research/kappa-rebuild/bit/bit_native_binding.py", + "usage": "input", + "git_blob": "f4c4082d89969ea311219d9af8013082d599f6f1", + "sha256": "bf6374225f388e7531fa6475cc255bd430100ff62c38d582c41601f0739de7b7" + }, + { + "path": "research/kappa-rebuild/bit/complex_controller_factor.py", + "usage": "input", + "git_blob": "cb0cff7c8be5f38f2ee52201d9d0907f9dfd7947", + "sha256": "1de9aaf918e6a4f2f5448754c1f3c3da3b85e6257849ebd097af09859c4e5497" + }, + { + "path": "research/kappa-rebuild/bit/mixed_productive_bit.py", + "usage": "input", + "git_blob": "9c7a8bd5d3ae4c19952648c815031858d6627b96", + "sha256": "b32291b0db7fc0d332ec444c70746ab0fb03351d2e50546f8bcb64060e3ff95e" + }, + { + "path": "research/kappa-rebuild/complex/FULL-IDENTITY.md", + "usage": "input", + "git_blob": "f97a23d7d21bd7f79c9d0cb14d8c6b44fddd3f23", + "sha256": "c4aa88c4943ef041e9542c519b7600ecf26ed6caff92558fdb07ac88ace64c17" + }, + { + "path": "research/kappa-rebuild/complex/full-identity-certificates/RESULT.json", + "usage": "input", + "git_blob": "c6edcbdc43bf36bb11201235027d0ec170d07fc8", + "sha256": "943d5fad2fc529f470df05a35446e07ecaef7344abfce450d2c2eb2c9b3798f6" + }, + { + "path": "research/kappa-rebuild/complex/full-identity-certificates/THREE-base-FULL-IDENTITY-CANONICAL.json.gz", + "usage": "input", + "git_blob": "4a8c4ed26e53a72362d571c972e65aff546be784", + "sha256": "6418ec3da24d548a57f5c3fe5b9062c26c9478e638504a61c387f5cfb5f4ed61" + }, + { + "path": "research/kappa-rebuild/complex/full-identity-certificates/THREE-base-FULL-IDENTITY-NATIVE.json.gz", + "usage": "input", + "git_blob": "b46d44c6ee624968dd57be928b0c15d9d45f3b2c", + "sha256": "c54b0a3e129d28e6dbf74fa731fc3bb70fe3c6705f07256750fbecddcc842d39" + }, + { + "path": "research/kappa-rebuild/complex/native_extensions.py", + "usage": "input", + "git_blob": "7f84894efc309546a903d314c7ac1473e7f594a8", + "sha256": "50ad007d9c386393657e86c99a96ae0a63a8fbc52872579b185002cc626e88e3" + }, + { + "path": "research/kappa-rebuild/complex/power_two_balance.py", + "usage": "input", + "git_blob": "a55ae0ce78a1861965f899a82604b276260f636c", + "sha256": "76929bb3887911ccf100c4593574b8a1c82ee64e96f939a8aca196869438b424" + }, + { + "path": "research/kappa-rebuild/complex/rebuild_native.py", + "usage": "input", + "git_blob": "78a7b1b0e6e43a1347fb361f45c6e0eaff8dd27b", + "sha256": "f94c527cc02215de49350d477618188c4c0da48bc8fb05b4e37b24c482cad7d5" + }, + { + "path": "research/kappa-rebuild/transfer-audit/p3_native_audit.py", + "usage": "input", + "git_blob": "0f3a4067a4b4e20d0e6ca0f84f41851c5168f76d", + "sha256": "5504a55a50546418d10c522984438cdeedb44993f7c1dab7bd4aa1ae0515d902" + }, + { + "path": "research/pr4359-p7-padding/P7-FACTOR.json", + "usage": "input", + "git_blob": "04c7ef620e760cc8f1764bbf0ccd7f32c6a5bd86", + "sha256": "6f96f6be5d8441f71cbe6ebb1657c69b543eb085b848b92b591b7ac01d6e6598" + }, + { + "path": "research/pr4359-p7-padding/TENSOR.md", + "usage": "input", + "git_blob": "8ecfd3e4d0bcb449ecb1e150c4f1f4fbb39ca656", + "sha256": "b2eba86cb979b4dc2a045f2e74bbd29e4d9e5ec87d6a2bc23ba7b54f1f58e3e3" + }, + { + "path": "research/pr4359-p7-padding/dependencies/compiler-refill/endpoint.py", + "usage": "input", + "git_blob": "340e1f0ffb8a1a9c38fbbd9119580b6d23e01b59", + "sha256": "d097e55f06c3f244f2074ffd7c1a0a5f3c4b4b6a6accf9619d1dde5c0ae85e15" + }, + { + "path": "research/pr4359-p7-padding/native_inventory.py", + "usage": "input", + "git_blob": "8d2d96e3998254c2333c43fe47cdfd074cbd811e", + "sha256": "65539acaf45bdfe8c5aee6830f9c9b3d1107c442a60842ef803fdd7688de8f32" + }, + { + "path": "research/query-thinned-controllers/BIT-CONTROLLER.json", + "usage": "input", + "git_blob": "89c400d5970024b3debe870c36ce43889beed001", + "sha256": "39ac84fb848b908f7ba051fae4556d507900c421dc5d23501a9c0cb1d61fd08d", + "pin": "head:40e22a83ed660d3d6074c4f2dbf14bfb621eee51:research/query-thinned-controllers/BIT-CONTROLLER.json" + }, + { + "path": "research/query-thinned-controllers/COMPLEX-CONTROLLER.json", + "usage": "input", + "git_blob": "39318f6ad9baf0838a274ca1042b1e3ba0e74bf9", + "sha256": "bf1143325d8380fab40cd5a85449f9a5412f0340deba7f4693714c92ae320088", + "pin": "head:40e22a83ed660d3d6074c4f2dbf14bfb621eee51:research/query-thinned-controllers/COMPLEX-CONTROLLER.json" + }, + { + "path": "research/query-thinned-controllers/RESULT.json", + "usage": "input", + "git_blob": "e0695152c98d727edfd0d2034b58a1c7e8682c0c", + "sha256": "6ebfc8c0f09166f4834e9d7427410cb31aefff2cd4d4ce588c8e52c9c70e9a0f", + "pin": "head:40e22a83ed660d3d6074c4f2dbf14bfb621eee51:research/query-thinned-controllers/RESULT.json" + }, + { + "path": "research/query-thinned-controllers/SOURCES.json", + "usage": "input", + "git_blob": "0f061c87ff87c43ff1ea0fc418582e9ccea3bc1d", + "sha256": "74b73563d9f78a4562d376b6f33528d652e41097f65747667f112a3e1fa81d29", + "pin": "head:40e22a83ed660d3d6074c4f2dbf14bfb621eee51:research/query-thinned-controllers/SOURCES.json" + }, + { + "path": "research/query-thinned-controllers/controller.py", + "usage": "input", + "git_blob": "d4557e08cfb9fe57cc1ae4024705a72dc95f3583", + "sha256": "8b462d660487b1be4940357c4c7522967b1bfaede3c02b1c66109b85acae0fd2", + "pin": "head:40e22a83ed660d3d6074c4f2dbf14bfb621eee51:research/query-thinned-controllers/controller.py" + }, + { + "path": "research/query-thinned-controllers/verify.py", + "usage": "input", + "git_blob": "f1114036fff66f57014e5c1256141fb78ff4c4a9", + "sha256": "07dea601d6bbaa4d90e576f20c8607c37fb01e8778c798d919fa9df435049950", + "pin": "head:40e22a83ed660d3d6074c4f2dbf14bfb621eee51:research/query-thinned-controllers/verify.py" + }, + { + "path": "research/t74-native-fast/vendor/native/new/code/borrow/vendor/clifford/clifford_exact.py", + "usage": "input", + "git_blob": "166841a037f069249f6f7f6dedb89248812f59e2", + "sha256": "2982ead07721e83358dc67c6f49c2b4c16a236a6bebdfd72f58221be1f5d0962" + } + ] +} diff --git a/research/fresh-helper-thinned/TASK.json b/research/fresh-helper-thinned/TASK.json new file mode 100644 index 0000000000..ee8b8e27d1 --- /dev/null +++ b/research/fresh-helper-thinned/TASK.json @@ -0,0 +1,96 @@ +{ + "schema_version": 1, + "task_id": "supplier-boundary-audit", + "priority_revision": 7, + "base_commit": "3a23e9d9d2e67833515d1c60a17e966bcdcab43c", + "original_card": { + "id": "supplier-boundary-audit", + "question": "Can the #4088 four-provider dispatch satisfy the complete ordinary/outer admission contract?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/staged544-mixed-fourth-entry/README.md", + "research/scatter-boundary-decision/README.md" + ], + "methods": [ + "Trace one hypothesis through the source, checker and complete caller.", + "Construct one semantically invalid but superficially well-formed fixture and test rejection." + ], + "acceptance_gate": "Pin the current sources and one obligation; the historical owner audit is an example, not evidence of a current bug.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read #4088 Scope and Open next questions: local words, native receipts and literal fill do not include a rerun of the mixed four-provider ordinary/outer engine. #3801 is the newer scatter-boundary decision; do not restart #2977 as if untouched.", + "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately." + }, + "first_experiment": "Pin the provider registry, four native source closures and dispatch. Make a bounded acceptance coverage map or one registry adapter preserving every inherited admission predicate and rejection control (including an omitted fourth provider). Record remaining ordinary/outer obligations and a resource estimate before heavy execution. Stop at unresolved source/caller dependencies; no selected-result promotion from a local pass.", + "bottleneck_link": "Closing a current acceptance gap or proof obligation strengthens reliability even without changing kappa.", + "allowed_variations": [ + "One provider-registry, dispatch, native-closure or admission-predicate obligation; separate branches must name distinct coverage." + ], + "scope_change_triggers": [ + "Reporting the historical timing-only diagnostic as a new current acceptance bug.", + "Calling a malformed mutant a failure of the selected construction, or importing an opt-in repair without testing the exporter boundary.", + "Running another root enclosure instead of validating dispatch or weakening an inherited predicate to make mixed admission pass." + ], + "overlap_terms": [ + "owner boundary", + "bridge omission", + "hosting", + "2977", + "scatter export", + "duplicate index", + "parity semantics", + "4088", + "3801", + "staged544-mixed-fourth-entry", + "scatter-boundary-decision" + ], + "existing_checks": [ + { + "scope": "PR #4088: author-checked local words, native receipts, owner/phase fill and exact moment.", + "evidence": "research/staged544-mixed-fourth-entry/README.md", + "remaining": "Rebind and validate ordinary/outer admission with all four providers; full mixed release not established.", + "status": "author-checked", + "source_commit": "72d7efc181edb21806a878f174847c96dd410ab0", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #3801: successor scatter-boundary decision package.", + "evidence": "research/scatter-boundary-decision/README.md", + "remaining": "Consult its exact acceptance scope before any new exporter audit; not proof of a selected failure.", + "status": "author-checked", + "source_commit": "911f8800ba7a4b03603ef62c5ffc6240e53cb5fd", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Combine the exact-head PR4440 query-thinned complex controller and stronger BIT supplier with the verified helper boundary retiming; certify a new complete conditional kappa beyond both predecessors.", + "scope_change_reason": "The explicit user task is to beat the strongest current kappa and switch to any stronger PR found in 20-minute checks. PR4440 at head 40e22a83 appeared during this run; its query-thinned native construction supersedes the first p7 result. This package audits and builds on that exact head, combining it with the independently replayed fresh helper retiming.", + "bottleneck_link": "Changing the complete nineteen-call native paid/productive profile improves the binding complex moment while retaining all copied-query charges and the stronger BIT consumer.", + "budget_minutes": 60, + "stop_rule": "Do not continue a superseded lesser kappa. Audit the stronger exact source, check actual unit substitution and the entire outer bill; no root digit-only or selected-frontier promotion.", + "outcome": "completed", + "evidence": "README.md; PROOF.md; AUDIT-4440.md; RESULT.json; SOURCES.json; VALIDATION.md", + "author": "1337isnot1337 with substantial OpenAI Codex assistance", + "ai_assistance": "Substantial OpenAI Codex assistance. No subagents or independent human mathematical review.", + "open_questions": [ + { + "question": "Can another simultaneous multi-frame or query/native topology change beat the new fixed-profile root?", + "why_it_matters": "Only about 4.18e-9 headroom remains in this invoice; another substantial improvement requires a changed profile.", + "first_step": "Start from the two pinned native units and emit a literal changed chronological word with all helper, owned-query and idle charges before a new root claim.", + "blocked_by": "No global optimum or complete multi-frame search is supplied." + }, + { + "question": "Can the owned-query and helper-retiming interfaces be independently proved at arbitrary column multiplicity?", + "why_it_matters": "The finite replays inherit source native, owned-erasure and whole-job contracts.", + "first_step": "Audit AUDIT-4440.md and the block-lift/whole-job clauses of both pinned source proofs.", + "blocked_by": "Finite phase/operator evidence is not formal or human acceptance of the entire source stack." + } + ] +} diff --git a/research/fresh-helper-thinned/VALIDATION.md b/research/fresh-helper-thinned/VALIDATION.md new file mode 100644 index 0000000000..ed9998e51a --- /dev/null +++ b/research/fresh-helper-thinned/VALIDATION.md @@ -0,0 +1,26 @@ +# Validation and limits + +- Source PR4440 head 40e22a83ed660d3d6074c4f2dbf14bfb621eee51: the unchanged + registered CPython 3.12.15 replay passed during the frontier audit. +- Helper retiming head ccdae89b2ab9ced24ee3e7adfdb670ef80d223d9: complete + CPython 3.12.15 registered replay, 320 phase/boundary checks, all 632 arbitrary + columns in both native orientations, negative controls and separate Git-free + replay passed before composition. Its published optimizer reproduces its patch. +- New arithmetic authoring freshly authenticates all pinned inputs, counts the + actual combined event word, and checks the full changed moment, root ceiling, + both tail bounds, logarithmic rank, enlarged scalar/route budget and outer bill. + The authoring path uses previously checked source receipts. Normal registered + replay freshly executes both full source verifiers and compares the combined + receipt. That normal registered CPython 3.12.15 replay passed, freshly + executing both complete source verifiers before the new arithmetic checks. + +No source package was edited. Both exact predecessor commits are retained in +publication ancestry. The selected record is unchanged. No Lean, Docker, +all-history suite, formal theorem acceptance or independent human review is +claimed. Native all-column, owned-erasure, whole-job, physical/tape, analytic, +precision, prime and exact-recovery premises remain conditional. + +The first hosted plan run at predecessor ccdae89 failed four pre-existing +selected-status navigation tests before reaching research replay. The submission +repairs only the two navigation documents, retaining selected kappa 0.0023 and +all historical content. The six targeted navigation/locale tests pass. diff --git a/research/fresh-helper-thinned/VERIFY.json b/research/fresh-helper-thinned/VERIFY.json new file mode 100644 index 0000000000..5af213891f --- /dev/null +++ b/research/fresh-helper-thinned/VERIFY.json @@ -0,0 +1,60 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/fresh-helper-boundary/ARITHMETIC-RESULT.json", + "research/fresh-helper-boundary/CHANGES.json", + "research/fresh-helper-boundary/NATIVE-RESULT.json.gz", + "research/fresh-helper-boundary/RESULT.json", + "research/fresh-helper-boundary/SOURCES.json", + "research/fresh-helper-boundary/arithmetic.py", + "research/fresh-helper-boundary/native.py", + "research/fresh-helper-boundary/verify.py", + "research/higher-moment-strictification/README.md", + "research/higher-moment-strictification/verify.py", + "research/kappa-0023-productive-jobs/dependencies/kappa-next-regime/bit-compression/carrier-reuse/reference/joint_pair_dag.py", + "research/kappa-0023-productive-jobs/dependencies/kappa-next-regime/direct-decoder/sources/DATA-PHASES.json", + "research/kappa-causal-continuation/buffer-borrowing/verify_buffers.py", + "research/kappa-function-composition/complex/prune_native.py", + "research/kappa-rebuild/architecture/mixed_target_probe.py", + "research/kappa-rebuild/bit/BIT-ALLSIZE-PARAMETERS.json", + "research/kappa-rebuild/bit/BIT-P3-NATIVE-BINDING.json", + "research/kappa-rebuild/bit/DELAYED-COVER-BRIDGE.md", + "research/kappa-rebuild/bit/MIXED-PRODUCTIVE-BIT.json", + "research/kappa-rebuild/bit/bit_native_binding.py", + "research/kappa-rebuild/bit/complex_controller_factor.py", + "research/kappa-rebuild/bit/mixed_productive_bit.py", + "research/kappa-rebuild/complex/FULL-IDENTITY.md", + "research/kappa-rebuild/complex/full-identity-certificates/RESULT.json", + "research/kappa-rebuild/complex/full-identity-certificates/THREE-base-FULL-IDENTITY-CANONICAL.json.gz", + "research/kappa-rebuild/complex/full-identity-certificates/THREE-base-FULL-IDENTITY-NATIVE.json.gz", + "research/kappa-rebuild/complex/native_extensions.py", + "research/kappa-rebuild/complex/power_two_balance.py", + "research/kappa-rebuild/complex/rebuild_native.py", + "research/kappa-rebuild/transfer-audit/p3_native_audit.py", + "research/pr4359-p7-padding/P7-FACTOR.json", + "research/pr4359-p7-padding/TENSOR.md", + "research/pr4359-p7-padding/dependencies/compiler-refill/endpoint.py", + "research/pr4359-p7-padding/native_inventory.py", + "research/query-thinned-controllers/BIT-CONTROLLER.json", + "research/query-thinned-controllers/COMPLEX-CONTROLLER.json", + "research/query-thinned-controllers/RESULT.json", + "research/query-thinned-controllers/SOURCES.json", + "research/query-thinned-controllers/controller.py", + "research/query-thinned-controllers/verify.py", + "research/t74-native-fast/vendor/native/new/code/borrow/vendor/clifford/clifford_exact.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 600, + "checks": "Freshly replay both exact-head source constructions; independently count the combined native/query/idle invoice; certify changed root and all-C fixed-profile ceiling, both charged tails with repaired gamma limit, logarithmic compiler rank, complete stronger BIT and all 54 outer predicates plus four guards." + } + ] +} diff --git a/research/fresh-helper-thinned/verify.py b/research/fresh-helper-thinned/verify.py new file mode 100644 index 0000000000..9ba85a59aa --- /dev/null +++ b/research/fresh-helper-thinned/verify.py @@ -0,0 +1,180 @@ +"""Combine the exact helper retiming with audited PR4440 query thinning. + +Apache-2.0; substantial OpenAI Codex assistance. Source notices retained. +Normal replay freshly executes both source verifiers, then this new ledger. +""" +from collections import Counter +from fractions import Fraction as Q +from hashlib import sha1, sha256 +import argparse +import gzip +import importlib.util +import json +from pathlib import Path +import sys + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +KAPPA, TESTED = Q('.00300105'), Q('.003001052') +ROOT_LOW, ROOT_HIGH = Q('.0030010541830'), Q('.0030010541834') + +def need(ok, why): + if not ok: raise ValueError(why) + +def read(path): + data = path.read_bytes() + return json.loads(gzip.decompress(data) if path.suffix == '.gz' else data) + +def load(path,name): + spec = importlib.util.spec_from_file_location(name,path) + module = importlib.util.module_from_spec(spec) + sys.modules[name]=module;spec.loader.exec_module(module) + return module + +def encode(x): + if isinstance(x,Q): return str(x) + if isinstance(x,dict): return {str(k):encode(v) for k,v in x.items()} + if isinstance(x,(list,tuple)): return [encode(v) for v in x] + return x + +def authenticate(): + seen=set() + for row in read(HERE/'SOURCES.json')['files']: + if row['usage']!='input': continue + p=Path(row['path']);need(not p.is_absolute() and '..' not in p.parts and str(p) not in seen,'Canonical input') + seen.add(str(p));actual=ROOT + for part in p.parts: + actual/=part;need(not actual.is_symlink(),'No source aliases') + b=actual.read_bytes() + need(sha256(b).hexdigest()==row['sha256'],'Changed source: '+str(p)) + need(sha1(b'blob '+str(len(b)).encode()+b'\0'+b).hexdigest()==row['git_blob'],'Changed Git source blob') + return len(seen) + +def ceiling(E,T,P): + signed={r:T[r]-P[r] for r in T.keys()|P.keys()} + def margin(c): + a,b=E.moment(T,1-c),E.moment(P,1-c) + return a[0]-b[1],a[1]-b[0] + need(margin(ROOT_LOW)[0]>0 and margin(ROOT_HIGH)[1]<0,'New complete profile root bracket') + derivative=None + for i in range(16): + l,r=Q(i,320),Q(i+1,320);low=Q(0) + for rank,n in signed.items(): + term=E.mul(E.power(rank,1-r if n>0 else 1-l),E.log_bounds(rank)) + low+=n*term[0 if n>0 else 1] + derivative=low if derivative is None else min(derivative,low) + upper=None + for i in range(128): + l,r=Q(1,20)+Q(19*i,2560),Q(1,20)+Q(19*(i+1),2560) + hi=sum(n*E.power(rank,1-l if n>0 else 1-r)[1 if n>0 else 0] for rank,n in signed.items()) + upper=hi if upper is None else max(hi,upper) + need(derivative>0 and upper<0,'Fixed-profile ceiling for every real 00,'No nonzero charge for erased idle stage') + P[rank]+=224;idle+=224 + for term in word['diagonal']: + need(term[0] in (-1,1) and all(x in (0,1) for x in term[1:]),'Actual normalized main target') + T[1+8*sum(term[1:])]+=112 + need((full,thin,idle)==(19,16,3584),'Every full, copied-query and whole-idle event') + need(sum(T.values())==11560 and sum(P.values())==69273,'Complete new productive/call counts') + need((sum(r*n for r,n in T.items()),sum(r*n for r,n in P.items()))==(260798,259998),'Preserve the exact surplus 800') + # Independent substitution into the source invoice must give the same ledger. + oldH={5:28,6:18,7:56,8:93,9:213};oldP={1:2487,2:713,3:224,4:102,5:20,8:8} + ref=source_query['complex_invoice'] + for key,new,old_unit,new_unit in [('targets',T,oldH,H),('paid',P,oldP,N)]: + check=Counter({int(k):v for k,v in ref[key].items()}) + check.subtract({k:19*v for k,v in old_unit.items()});check.update({k:19*v for k,v in new_unit.items()}) + need(+check==new,'Literal event count equals whole-call substitution: '+key) + E=S.C.load(ROOT/'research/higher-moment-strictification/verify.py','combined_exact_intervals') + root=ceiling(E,T,P) + t,u,v,c,b=1-TESTED,Q(1,5),1024,20,21 + target=E.moment(T,t);alpha=E.divide(E.moment(P,t),target) + other=S.C.load(ROOT/'research/kappa-rebuild/architecture/mixed_target_probe.py','combined_separate_intervals') + tl,th=other.moment(T,TESTED);pl,ph=other.moment(P,TESTED) + need(tl>ph and max(tl,target[0])<=min(th,target[1]),'Independent exact raw-moment engine') + gamma=E.divide(E.moment(P,t+u),E.mul(E.power(c,u),target)) + delta=E.divide((Q(sum(T.values())*b),)*2,E.mul(E.power(c,TESTED),target)) + alpha_gap=Q(1,1000000000);g,d=Q(97,100),Q(19,20) + need(alpha[1]<1-alpha_gap and gamma[1]Q(31,32),'The previous gamma limit fails and is explicitly replaced') + # Apply PR4433's general logarithmic majorant at the actual new ambient rank. + theta,power=Q(63,64),1000 + eta=E.scale(E.power(153,-v*TESTED),t) + need(2*(20**v)**64<=(153**v)**63 and eta[0]>theta**power,'Shifted exit and complement capacity') + need(E.power(153,v*TESTED)[1]<2**power,'Initial compiler range') + gap=(TESTED-KAPPA)/7;need(gap.numerator==1,'Integer compiler grid') + step=gap.denominator + def passes(j):return (step*j+1)**power<2**j + lo,hi=1,2 + while not passes(hi):lo,hi=hi,2*hi + while hi-lo>1: + mid=(lo+hi)//2 + if passes(mid):hi=mid + else:lo=mid + height=step*hi + need(height>8*v and passes(hi) and not passes(hi-1),'Effective uniform rank integer inequality') + # The changed local list is charged under an explicit larger fixed bound. + local_scalar=max(x['real_scalar_allowance'] for x in local['native'].values()) + local_routes=(sum(N.values())+2*408)*1000 + need(local_scalar+local_routes<10**7,'Every new local scalar and monomial route fits') + scalar_upper=19*10**7+16*1792+32*112*(len(word['physical_events'])+sum(len(word['boundaries'][k+'_program']) for k in ('left','right'))) + need(scalar_upper<10**9,'Retain the complete raw nonrecursive bound') + bit=source_query['ordinary_BIT'];atom=Q(bit['atom']);ordinary=(1-atom)*Q(bit['after_cover'])+atom*Q('.0000384599') + admitted=Q(bit['admitted']);need(atom==Q('.004') and atom>ordinary>admitted>TESTED and atom<1-ordinary,'Complete stronger source BIT admission') + L=S.C.load(ROOT/'research/pr4359-p7-padding/dependencies/compiler-refill/endpoint.py','combined_outer_ledger') + params={'kappa':KAPPA,'tested_saving':TESTED,'complex_uniform_saving':KAPPA+6*gap, + 'b':KAPPA+5*gap,'a':KAPPA+4*gap,'q':KAPPA+3*gap,'bit_saving':admitted, + 'epsilon':1-gap,'beta':1-3*gap,'r0':gap/10,'stop':gap,'layout':gap,'d':gap} + outer=L.ledger(params);outer['functional_checks']['actual_new_BIT_stock_sublinear']=params['beta']*(1-atom) + need(len(outer['strict_checks'])==54 and len(outer['functional_checks'])==4,'Complete outer predicate inventory') + need(all(x>0 for key in ('strict_checks','functional_checks') for x in outer[key].values()),'Every complete outer inequality') + controls={} + for name,patch in [('old_BIT',{'bit_saving':Q('.0027')}),('closed_uniform',{'complex_uniform_saving':params['b']}),('unfunded_endpoint',{'kappa':TESTED}),('closed_epsilon',{'epsilon':Q(1)})]: + bad=L.ledger(dict(params,**patch));failed=[k for k,x in bad['strict_checks'].items() if x<=0] + need(failed,'Reject '+name);controls[name]=failed + return encode({'status':'PASS_CONDITIONAL_FRESH_HELPER_QUERY_THINNED_KAPPA', 'kappa':KAPPA,'kappa_decimal':'0.00300105', + 'source_inputs':count,'source_heads':{'PR4440':'40e22a83ed660d3d6074c4f2dbf14bfb621eee51','helper_retiming':'ccdae89b2ab9ced24ee3e7adfdb670ef80d223d9'}, + 'gain_over_PR4440':KAPPA-Q('.00296'),'gain_over_PR4416':KAPPA-Q('.00268647'), + 'targets':dict(sorted(T.items())),'paid':dict(sorted(P.items())),'full_calls':full,'query_shears':thin, + 'paid_calls':sum(P.values()),'productive_fields':sum(T.values()),'fixed_profile_ceiling':root, + 'strictification':{'tested':TESTED,'power':v,'cutoff':c,'floor':b,'tail_offset':u, + 'alpha':E.display(alpha),'gamma':E.display(gamma),'delta':E.display(delta), + 'limits':[1-alpha_gap,g,d],'normalized_paid_upper':bound}, + 'compiler':{'theta':theta,'logarithm_power':power,'eta':E.display(eta),'uniform_saving':params['complex_uniform_saving'], + 'gap':gap,'H':height,'N':'2^'+str(height),'integer_test_exponent':hi,'word_materialized':False}, + 'nonrecursive':{'local_scalar_allowance':local_scalar,'local_route_bound':local_routes,'raw_upper':scalar_upper,'raw_budget':10**9}, + 'ordinary_BIT':bit,'outer':outer,'negative_controls':controls, + 'scope':'Author-checked conditional construction; retained native/all-column, owned-erasure, whole-job, analytic, precision, tape, prime and recovery contracts. No selected promotion or formal/human acceptance.'}) + +if __name__=='__main__': + parser=argparse.ArgumentParser() + parser.add_argument('--write',action='store_true',help='Author the new arithmetic receipt from already-audited dependency receipts; normal replay freshly reruns both dependencies.') + args=parser.parse_args();result=run(execute_sources=not args.write) + if args.write:(HERE/'RESULT.json').write_text(json.dumps(result,indent=2,sort_keys=True)+'\n') + else:need(result==read(HERE/'RESULT.json'),'Exact combined receipt replay') + print(json.dumps({k:result[k] for k in ('status','kappa_decimal','gain_over_PR4440','compiler')},sort_keys=True)) diff --git a/research/historical-1042-link/RESULT.json b/research/historical-1042-link/RESULT.json index a9d58d2881..30ec98c793 100644 --- a/research/historical-1042-link/RESULT.json +++ b/research/historical-1042-link/RESULT.json @@ -2,8 +2,9 @@ "historical_href": "../../certificates/selected-result.json", "checkpoint": "certificates/checkpoints/frontier1042.json", "historical_kappa": "1672188119205421/1000000000000000000", - "live_kappa": "836330098538459/500000000000000000", + "live_kappa": "23/10000", "same_href": true, "kappas_differ": true, - "no_new_kappa": true + "no_new_kappa": true, + "intermediate_checkpoint": "certificates/checkpoints/frontier1094.json" } diff --git a/research/historical-1042-link/SOURCES.json b/research/historical-1042-link/SOURCES.json index c6119ca5a8..746e91383f 100644 --- a/research/historical-1042-link/SOURCES.json +++ b/research/historical-1042-link/SOURCES.json @@ -11,20 +11,29 @@ { "path": "docs/research/current-status.md", "usage": "input", - "git_blob": "4e0a8b7cdacc1d9680f7f81d03624118bb20416d", - "sha256": "00a08925c51b26d168b8099ddeed659ac4381f7e04f3c7fd0e9de8e71f206823" + "git_blob": "532af84312cbfeb39a1e4659d8398deb560f1e4a", + "sha256": "54c843968d0b178369a7e56161be44c4692935c3f46ce261678aeedadb309891", + "pin": "head:5f9d871c6bd1b9e34db5a7ea5ef08a908e94db39:docs/research/current-status.md" }, { "path": "certificates/selected-result.json", "usage": "input", - "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81", - "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + "git_blob": "ed33caef5c5827693e9572d252a66f99cbb73d40", + "sha256": "5732707cc1e460b090b53f2463162749ad860de878a18f7408938671d295a9d9", + "pin": "head:5f9d871c6bd1b9e34db5a7ea5ef08a908e94db39:certificates/selected-result.json" }, { "path": "certificates/checkpoints/frontier1042.json", "usage": "input", "git_blob": "f451ced6626a1f03aba6915ce23a136b01ebe51d", "sha256": "207d1f49f113c585024b9d3c17eadbb8b1be17c1321e3d190aabe2f18ce1c5b7" + }, + { + "path": "certificates/checkpoints/frontier1094.json", + "usage": "input", + "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81", + "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129", + "pin": "head:5f9d871c6bd1b9e34db5a7ea5ef08a908e94db39:certificates/checkpoints/frontier1094.json" } ] } diff --git a/research/historical-1042-link/VERIFY.json b/research/historical-1042-link/VERIFY.json index 5cff7b26c9..5138c1b017 100644 --- a/research/historical-1042-link/VERIFY.json +++ b/research/historical-1042-link/VERIFY.json @@ -6,16 +6,25 @@ "inputs": [ "docs/research/current-status.md", "certificates/selected-result.json", - "certificates/checkpoints/frontier1042.json" + "certificates/checkpoints/frontier1042.json", + "certificates/checkpoints/frontier1094.json" ], "commands": [ { - "argv": ["{python}", "-B", "{package}/verify.py"], + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], "timeout_seconds": 30, "checks": "Compare the #1042 status link with the live record and the frontier1042 checkpoint." }, { - "argv": ["{python}", "-B", "{package}/test_verify.py"], + "argv": [ + "{python}", + "-B", + "{package}/test_verify.py" + ], "timeout_seconds": 30, "checks": "Check the printed decimal and the historical section cut." } diff --git a/research/historical-1042-link/verify.py b/research/historical-1042-link/verify.py index 12170922e5..2ffd4a8ce4 100644 --- a/research/historical-1042-link/verify.py +++ b/research/historical-1042-link/verify.py @@ -2,7 +2,8 @@ """Separate the #1042 status link from the live selected record. The historical section states the #1042 kappa and links to the live record. -The matching checkpoint is the selected record's previous_record field. +The matching checkpoint is reached through the selected record's historical +previous_record chain (currently via frontier1094). """ import hashlib @@ -16,6 +17,7 @@ MARKER = "PASS_HISTORICAL_1042_LINK kappas_differ=true no_new_kappa" HREF = "../../certificates/selected-result.json" CHECKPOINT = "certificates/checkpoints/frontier1042.json" +INTERMEDIATE = "certificates/checkpoints/frontier1094.json" SHOWN = "0.001672188119205421" @@ -43,6 +45,7 @@ def authenticate(): "docs/research/current-status.md", "certificates/selected-result.json", "certificates/checkpoints/frontier1042.json", + "certificates/checkpoints/frontier1094.json", } require(set(pinned) == expected, "input inventory changed") for path, row in pinned.items(): @@ -64,12 +67,15 @@ def evaluate(): require(HREF in section, "the historical section lost the live-record link") require(SHOWN in section, "the historical kappa sentence moved") require(Fraction(SHOWN) == Fraction(old["kappa"]), "the checkpoint kappa left the printed decimal") - require(live["previous_record"] == CHECKPOINT, "the previous-record pointer moved") + require(live["previous_record"] == INTERMEDIATE, "the live previous-record pointer moved") + intermediate = json.loads((ROOT / INTERMEDIATE).read_text(encoding="utf-8")) + require(intermediate["previous_record"] == CHECKPOINT, "the checkpoint ancestry link moved") require(Fraction(live["kappa"]) != Fraction(old["kappa"]), "the live and historical kappas agree") require(text.index(HREF) < text.index("# Historical status through #1042"), "the live section lost its record link") return { "historical_href": HREF, "checkpoint": CHECKPOINT, + "intermediate_checkpoint": INTERMEDIATE, "historical_kappa": old["kappa"], "live_kappa": live["kappa"], "same_href": True, diff --git a/research/query-thinned-controllers/BIT-CONTROLLER.json b/research/query-thinned-controllers/BIT-CONTROLLER.json new file mode 100644 index 0000000000..89c400d597 --- /dev/null +++ b/research/query-thinned-controllers/BIT-CONTROLLER.json @@ -0,0 +1,2175 @@ +{ + "ambient_rank": 127, + "boundaries": { + "boundary_unit_ADDs_per_port": 160, + "coefficient_projectors": { + "12884901889": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1073741824, + 2147483648 + ], + "1367": [ + 1280, + 0, + 1280, + 0, + 1280, + 0, + 1280, + 0, + 1280, + 682, + 0, + 682, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "13958643713": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 268435456, + 536870912, + 0, + 0 + ], + "14227079169": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 67108864, + 134217728, + 0, + 0, + 0, + 0 + ], + "14294188033": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 16777216, + 33554432, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "14310965249": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 4194304, + 8388608, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "14315159553": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1048576, + 2097152, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "14316208129": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 262144, + 524288, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "14316470273": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 65536, + 131072, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "14316557655": [ + 16384, + 0, + 16384, + 0, + 16384, + 0, + 16384, + 0, + 16384, + 0, + 16384, + 0, + 16384, + 0, + 16384, + 43690, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "21847": [ + 20480, + 0, + 20480, + 0, + 20480, + 0, + 20480, + 0, + 20480, + 0, + 20480, + 0, + 20480, + 10922, + 0, + 10922, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "23": [ + 20, + 0, + 20, + 10, + 0, + 10, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "343": [ + 320, + 0, + 320, + 0, + 320, + 0, + 320, + 170, + 0, + 170, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "5463": [ + 5120, + 0, + 5120, + 0, + 5120, + 0, + 5120, + 0, + 5120, + 0, + 5120, + 2730, + 0, + 2730, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "7": [ + 5, + 2, + 0, + 2, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "87": [ + 80, + 0, + 80, + 0, + 80, + 42, + 0, + 42, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ] + }, + "diagonal_monomials": [ + 7, + 7, + 23, + 23, + 87, + 87, + 343, + 343, + 1367, + 1367, + 5463, + 5463, + 21847, + 21847, + 12884901889, + 12884901889, + 13958643713, + 13958643713, + 14227079169, + 14227079169, + 14294188033, + 14294188033, + 14310965249, + 14310965249, + 14315159553, + 14315159553, + 14316208129, + 14316208129, + 14316470273, + 14316470273, + 14316557655, + 14316557655 + ], + "full_coefficient_endpoint_sha256": "0164c424ad261c955e105330fcec5942d9a863d1b6030f70e786f5cdafb2acef", + "left_program": [ + [ + "SWAP", + 30, + 31 + ], + [ + "SWAP", + 21, + 25 + ], + [ + "SWAP", + 20, + 24 + ], + [ + "SWAP", + 19, + 27 + ], + [ + "SWAP", + 18, + 26 + ], + [ + "SWAP", + 17, + 29 + ], + [ + "SWAP", + 16, + 28 + ], + [ + "SWAP", + 15, + 30 + ], + [ + "ADD", + 12, + 14 + ], + [ + "ADD", + 10, + 14 + ], + [ + "ADD", + 8, + 14 + ], + [ + "ADD", + 6, + 14 + ], + [ + "ADD", + 4, + 14 + ], + [ + "ADD", + 2, + 14 + ], + [ + "ADD", + 0, + 14 + ], + [ + "SWAP", + 14, + 31 + ], + [ + "ADD", + 30, + 13 + ], + [ + "ADD", + 10, + 12 + ], + [ + "ADD", + 8, + 12 + ], + [ + "ADD", + 6, + 12 + ], + [ + "ADD", + 4, + 12 + ], + [ + "ADD", + 2, + 12 + ], + [ + "ADD", + 0, + 12 + ], + [ + "SWAP", + 12, + 13 + ], + [ + "ADD", + 30, + 11 + ], + [ + "ADD", + 12, + 11 + ], + [ + "ADD", + 8, + 10 + ], + [ + "ADD", + 6, + 10 + ], + [ + "ADD", + 4, + 10 + ], + [ + "ADD", + 2, + 10 + ], + [ + "ADD", + 0, + 10 + ], + [ + "SWAP", + 10, + 11 + ], + [ + "ADD", + 30, + 9 + ], + [ + "ADD", + 12, + 9 + ], + [ + "ADD", + 10, + 9 + ], + [ + "ADD", + 6, + 8 + ], + [ + "ADD", + 4, + 8 + ], + [ + "ADD", + 2, + 8 + ], + [ + "ADD", + 0, + 8 + ], + [ + "SWAP", + 8, + 9 + ], + [ + "ADD", + 30, + 7 + ], + [ + "ADD", + 12, + 7 + ], + [ + "ADD", + 10, + 7 + ], + [ + "ADD", + 8, + 7 + ], + [ + "ADD", + 4, + 6 + ], + [ + "ADD", + 2, + 6 + ], + [ + "ADD", + 0, + 6 + ], + [ + "SWAP", + 6, + 7 + ], + [ + "ADD", + 30, + 5 + ], + [ + "ADD", + 12, + 5 + ], + [ + "ADD", + 10, + 5 + ], + [ + "ADD", + 8, + 5 + ], + [ + "ADD", + 6, + 5 + ], + [ + "ADD", + 2, + 4 + ], + [ + "ADD", + 0, + 4 + ], + [ + "SWAP", + 4, + 5 + ], + [ + "ADD", + 30, + 3 + ], + [ + "ADD", + 12, + 3 + ], + [ + "ADD", + 10, + 3 + ], + [ + "ADD", + 8, + 3 + ], + [ + "ADD", + 6, + 3 + ], + [ + "ADD", + 4, + 3 + ], + [ + "ADD", + 0, + 2 + ], + [ + "SWAP", + 2, + 3 + ], + [ + "ADD", + 30, + 1 + ], + [ + "ADD", + 12, + 1 + ], + [ + "ADD", + 10, + 1 + ], + [ + "ADD", + 8, + 1 + ], + [ + "ADD", + 6, + 1 + ], + [ + "ADD", + 4, + 1 + ], + [ + "ADD", + 2, + 1 + ] + ], + "left_rows": [ + 5, + 2, + 10, + 20, + 42, + 80, + 170, + 320, + 682, + 1280, + 2730, + 5120, + 10922, + 20480, + 1073741824, + 2147483648, + 268435456, + 536870912, + 67108864, + 134217728, + 16777216, + 33554432, + 4194304, + 8388608, + 1048576, + 2097152, + 262144, + 524288, + 65536, + 131072, + 43690, + 16384 + ], + "right_program": [ + [ + "ADD", + 13, + 31 + ], + [ + "SWAP", + 30, + 31 + ], + [ + "SWAP", + 21, + 25 + ], + [ + "SWAP", + 20, + 24 + ], + [ + "SWAP", + 19, + 27 + ], + [ + "SWAP", + 18, + 26 + ], + [ + "SWAP", + 17, + 29 + ], + [ + "SWAP", + 16, + 28 + ], + [ + "SWAP", + 15, + 31 + ], + [ + "SWAP", + 14, + 30 + ], + [ + "ADD", + 11, + 13 + ], + [ + "ADD", + 15, + 12 + ], + [ + "SWAP", + 12, + 13 + ], + [ + "ADD", + 9, + 11 + ], + [ + "ADD", + 13, + 10 + ], + [ + "SWAP", + 10, + 11 + ], + [ + "ADD", + 7, + 9 + ], + [ + "ADD", + 11, + 8 + ], + [ + "SWAP", + 8, + 9 + ], + [ + "ADD", + 5, + 7 + ], + [ + "ADD", + 9, + 6 + ], + [ + "SWAP", + 6, + 7 + ], + [ + "ADD", + 3, + 5 + ], + [ + "ADD", + 7, + 4 + ], + [ + "SWAP", + 4, + 5 + ], + [ + "ADD", + 0, + 3 + ], + [ + "ADD", + 5, + 2 + ], + [ + "SWAP", + 2, + 3 + ], + [ + "ADD", + 3, + 1 + ] + ], + "right_rows": [ + 2147494569, + 2, + 2147494568, + 6, + 2147494560, + 20, + 2147494528, + 80, + 2147494400, + 320, + 2147493888, + 1280, + 2147491840, + 5120, + 2147483648, + 1073745920, + 268435456, + 536870912, + 67108864, + 134217728, + 16777216, + 33554432, + 4194304, + 8388608, + 1048576, + 2097152, + 262144, + 524288, + 65536, + 131072, + 16384, + 32768 + ] + }, + "diagonal": [ + 7, + 7, + 23, + 23, + 87, + 87, + 343, + 343, + 1367, + 1367, + 5463, + 5463, + 21847, + 21847, + 12884901889, + 12884901889, + 13958643713, + 13958643713, + 14227079169, + 14227079169, + 14294188033, + 14294188033, + 14310965249, + 14310965249, + 14315159553, + 14315159553, + 14316208129, + 14316208129, + 14316470273, + 14316470273, + 14316557655, + 14316557655 + ], + "invoice": { + "main": { + "15": 444, + "22": 444, + "29": 444, + "36": 444, + "43": 444, + "50": 444, + "57": 444, + "64": 222, + "127": 222 + }, + "owned_streams_reused_sequentially": 1, + "paid": { + "1": 25479, + "2": 24156, + "3": 1422, + "4": 792, + "5": 1836, + "6": 198, + "7": 342, + "14": 444, + "21": 444, + "28": 444, + "35": 444, + "42": 444, + "49": 444, + "56": 444, + "63": 222 + }, + "paid_calls": 57555, + "productive_fields": 11454, + "rank_surplus": 753, + "raw_scalar_record_bound": 1000000000, + "targets": { + "8": 7902, + "15": 444, + "22": 444, + "29": 444, + "36": 444, + "43": 444, + "50": 444, + "57": 444, + "64": 222, + "127": 222 + }, + "thick_calls": 18, + "thick_stages": [ + 0, + 1, + 3, + 5, + 7, + 9, + 11, + 13, + 15, + 17, + 19, + 21, + 23, + 25, + 27, + 29, + 31, + 32 + ], + "thin_queries": 1665, + "whole_idle": { + "14": 444, + "21": 444, + "28": 444, + "35": 444, + "42": 444, + "49": 444, + "56": 444, + "63": 222 + } + }, + "keep_mask": 35047648968703, + "kind": "bit", + "pairs": 16, + "physical_events": [ + [ + "LOCAL", + 0, + 0, + false + ], + [ + "LOCAL", + 1, + 0, + true + ], + [ + "IDLE", + 1, + [ + 0, + 1 + ] + ], + [ + "ADD", + 0, + 2 + ], + [ + "ADD", + 3, + 1 + ], + [ + "QUERY_SHEAR", + 2, + 0, + false + ], + [ + "ADD", + 0, + 2 + ], + [ + "ADD", + 3, + 1 + ], + [ + "LOCAL", + 3, + 1, + true + ], + [ + "IDLE", + 2, + [ + 0, + 1, + 3 + ] + ], + [ + "ADD", + 2, + 4 + ], + [ + "ADD", + 5, + 3 + ], + [ + "QUERY_SHEAR", + 4, + 1, + false + ], + [ + "ADD", + 2, + 4 + ], + [ + "ADD", + 5, + 3 + ], + [ + "LOCAL", + 5, + 2, + true + ], + [ + "IDLE", + 3, + [ + 0, + 1, + 3, + 5 + ] + ], + [ + "ADD", + 4, + 6 + ], + [ + "ADD", + 7, + 5 + ], + [ + "QUERY_SHEAR", + 6, + 2, + false + ], + [ + "ADD", + 4, + 6 + ], + [ + "ADD", + 7, + 5 + ], + [ + "LOCAL", + 7, + 3, + true + ], + [ + "IDLE", + 4, + [ + 0, + 1, + 3, + 5, + 7 + ] + ], + [ + "ADD", + 6, + 8 + ], + [ + "ADD", + 9, + 7 + ], + [ + "QUERY_SHEAR", + 8, + 3, + false + ], + [ + "ADD", + 6, + 8 + ], + [ + "ADD", + 9, + 7 + ], + [ + "LOCAL", + 9, + 4, + true + ], + [ + "IDLE", + 5, + [ + 0, + 1, + 3, + 5, + 7, + 9 + ] + ], + [ + "ADD", + 8, + 10 + ], + [ + "ADD", + 11, + 9 + ], + [ + "QUERY_SHEAR", + 10, + 4, + false + ], + [ + "ADD", + 8, + 10 + ], + [ + "ADD", + 11, + 9 + ], + [ + "LOCAL", + 11, + 5, + true + ], + [ + "IDLE", + 6, + [ + 0, + 1, + 3, + 5, + 7, + 9, + 11 + ] + ], + [ + "ADD", + 10, + 12 + ], + [ + "ADD", + 13, + 11 + ], + [ + "QUERY_SHEAR", + 12, + 5, + false + ], + [ + "ADD", + 10, + 12 + ], + [ + "ADD", + 13, + 11 + ], + [ + "LOCAL", + 13, + 6, + true + ], + [ + "IDLE", + 7, + [ + 0, + 1, + 3, + 5, + 7, + 9, + 11, + 13 + ] + ], + [ + "ADD", + 12, + 14 + ], + [ + "ADD", + 15, + 13 + ], + [ + "QUERY_SHEAR", + 14, + 6, + false + ], + [ + "ADD", + 12, + 14 + ], + [ + "ADD", + 15, + 13 + ], + [ + "LOCAL", + 15, + 7, + true + ], + [ + "ADD", + 14, + 16 + ], + [ + "ADD", + 17, + 15 + ], + [ + "QUERY_SHEAR", + 16, + 7, + false + ], + [ + "ADD", + 14, + 16 + ], + [ + "ADD", + 17, + 15 + ], + [ + "LOCAL", + 17, + 8, + true + ], + [ + "ADD", + 16, + 18 + ], + [ + "ADD", + 19, + 17 + ], + [ + "QUERY_SHEAR", + 18, + 8, + false + ], + [ + "ADD", + 16, + 18 + ], + [ + "ADD", + 19, + 17 + ], + [ + "LOCAL", + 19, + 9, + true + ], + [ + "ADD", + 18, + 20 + ], + [ + "ADD", + 21, + 19 + ], + [ + "QUERY_SHEAR", + 20, + 9, + false + ], + [ + "ADD", + 18, + 20 + ], + [ + "ADD", + 21, + 19 + ], + [ + "LOCAL", + 21, + 10, + true + ], + [ + "ADD", + 20, + 22 + ], + [ + "ADD", + 23, + 21 + ], + [ + "QUERY_SHEAR", + 22, + 10, + false + ], + [ + "ADD", + 20, + 22 + ], + [ + "ADD", + 23, + 21 + ], + [ + "LOCAL", + 23, + 11, + true + ], + [ + "ADD", + 22, + 24 + ], + [ + "ADD", + 25, + 23 + ], + [ + "QUERY_SHEAR", + 24, + 11, + false + ], + [ + "ADD", + 22, + 24 + ], + [ + "ADD", + 25, + 23 + ], + [ + "LOCAL", + 25, + 12, + true + ], + [ + "ADD", + 24, + 26 + ], + [ + "ADD", + 27, + 25 + ], + [ + "QUERY_SHEAR", + 26, + 12, + false + ], + [ + "ADD", + 24, + 26 + ], + [ + "ADD", + 27, + 25 + ], + [ + "LOCAL", + 27, + 13, + true + ], + [ + "ADD", + 26, + 28 + ], + [ + "ADD", + 29, + 27 + ], + [ + "QUERY_SHEAR", + 28, + 13, + false + ], + [ + "ADD", + 26, + 28 + ], + [ + "ADD", + 29, + 27 + ], + [ + "LOCAL", + 29, + 14, + true + ], + [ + "ADD", + 28, + 30 + ], + [ + "ADD", + 31, + 29 + ], + [ + "QUERY_SHEAR", + 30, + 14, + false + ], + [ + "ADD", + 28, + 30 + ], + [ + "ADD", + 31, + 29 + ], + [ + "LOCAL", + 31, + 15, + true + ], + [ + "LOCAL", + 32, + 15, + false + ], + [ + "IDLE", + 7, + [ + 17, + 19, + 21, + 23, + 25, + 27, + 29, + 31, + 32 + ] + ], + [ + "IDLE", + 8, + [ + 19, + 21, + 23, + 25, + 27, + 29, + 31, + 32 + ] + ], + [ + "IDLE", + 9, + [ + 21, + 23, + 25, + 27, + 29, + 31, + 32 + ] + ], + [ + "IDLE", + 10, + [ + 23, + 25, + 27, + 29, + 31, + 32 + ] + ], + [ + "IDLE", + 11, + [ + 25, + 27, + 29, + 31, + 32 + ] + ], + [ + "IDLE", + 12, + [ + 27, + 29, + 31, + 32 + ] + ], + [ + "IDLE", + 13, + [ + 29, + 31, + 32 + ] + ], + [ + "IDLE", + 14, + [ + 31, + 32 + ] + ], + [ + "ADD", + 30, + 28 + ], + [ + "ADD", + 29, + 31 + ], + [ + "ADD", + 28, + 26 + ], + [ + "ADD", + 27, + 29 + ], + [ + "ADD", + 26, + 24 + ], + [ + "ADD", + 25, + 27 + ], + [ + "ADD", + 24, + 22 + ], + [ + "ADD", + 23, + 25 + ], + [ + "ADD", + 22, + 20 + ], + [ + "ADD", + 21, + 23 + ], + [ + "ADD", + 20, + 18 + ], + [ + "ADD", + 19, + 21 + ], + [ + "ADD", + 18, + 16 + ], + [ + "ADD", + 17, + 19 + ], + [ + "ADD", + 16, + 14 + ], + [ + "ADD", + 15, + 17 + ], + [ + "ADD", + 14, + 12 + ], + [ + "ADD", + 13, + 15 + ], + [ + "ADD", + 12, + 10 + ], + [ + "ADD", + 11, + 13 + ], + [ + "ADD", + 10, + 8 + ], + [ + "ADD", + 9, + 11 + ], + [ + "ADD", + 8, + 6 + ], + [ + "ADD", + 7, + 9 + ], + [ + "ADD", + 6, + 4 + ], + [ + "ADD", + 5, + 7 + ], + [ + "ADD", + 4, + 2 + ], + [ + "ADD", + 3, + 5 + ], + [ + "ADD", + 2, + 0 + ], + [ + "ADD", + 1, + 3 + ], + [ + "SWAP", + 0, + 1 + ], + [ + "SWAP", + 2, + 3 + ], + [ + "SWAP", + 4, + 5 + ], + [ + "SWAP", + 6, + 7 + ], + [ + "SWAP", + 8, + 9 + ], + [ + "SWAP", + 10, + 11 + ], + [ + "SWAP", + 12, + 13 + ], + [ + "SWAP", + 14, + 15 + ], + [ + "SWAP", + 16, + 17 + ], + [ + "SWAP", + 18, + 19 + ], + [ + "SWAP", + 20, + 21 + ], + [ + "SWAP", + 22, + 23 + ], + [ + "SWAP", + 24, + 25 + ], + [ + "SWAP", + 26, + 27 + ], + [ + "SWAP", + 28, + 29 + ], + [ + "SWAP", + 30, + 31 + ] + ], + "prefix_pairs": 7 +} diff --git a/research/query-thinned-controllers/COMPLEX-CONTROLLER.json b/research/query-thinned-controllers/COMPLEX-CONTROLLER.json new file mode 100644 index 0000000000..39318f6ad9 --- /dev/null +++ b/research/query-thinned-controllers/COMPLEX-CONTROLLER.json @@ -0,0 +1,5801 @@ +{ + "ambient_rank": 153, + "boundaries": { + "left": [ + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "1", + "0", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "1", + "0", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "1", + "0", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "1", + "0", + "-1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "1", + "0", + "-1", + "0", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "1", + "0", + "-1", + "0", + "1", + "0", + "-1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "1", + "0", + "-1", + "0", + "1", + "0", + "-1", + "0", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "1", + "0", + "-1", + "0", + "1", + "0", + "-1", + "0", + "1", + "0", + "-1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "1", + "0", + "-1", + "0", + "1", + "0", + "-1", + "0", + "1", + "0", + "-1", + "0", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "1", + "0", + "-1", + "0", + "1", + "0", + "-1", + "0", + "1", + "0", + "-1", + "0", + "1", + "0", + "-1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "1", + "0", + "-1", + "0", + "1", + "0", + "-1", + "0", + "1", + "0", + "-1", + "0", + "1", + "0", + "-1", + "0", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ] + ], + "left_program": [ + [ + "SWAP", + 29, + 31 + ], + [ + "SWAP", + 28, + 29 + ], + [ + "SWAP", + 27, + 30 + ], + [ + "SWAP", + 25, + 27 + ], + [ + "SWAP", + 24, + 31 + ], + [ + "SWAP", + 23, + 27 + ], + [ + "SWAP", + 22, + 27 + ], + [ + "SWAP", + 21, + 23 + ], + [ + "SWAP", + 20, + 30 + ], + [ + "SWAP", + 19, + 24 + ], + [ + "SWAP", + 18, + 28 + ], + [ + "SWAP", + 17, + 33 + ], + [ + "ADD", + 14, + 16, + "1" + ], + [ + "ADD", + 12, + 16, + "-1" + ], + [ + "ADD", + 10, + 16, + "1" + ], + [ + "ADD", + 8, + 16, + "-1" + ], + [ + "ADD", + 6, + 16, + "1" + ], + [ + "ADD", + 4, + 16, + "-1" + ], + [ + "ADD", + 2, + 16, + "1" + ], + [ + "ADD", + 0, + 16, + "-1" + ], + [ + "ADD", + 33, + 15, + "-1" + ], + [ + "SCALE", + 15, + "-1" + ], + [ + "SWAP", + 15, + 32 + ], + [ + "ADD", + 12, + 14, + "1" + ], + [ + "ADD", + 10, + 14, + "-1" + ], + [ + "ADD", + 8, + 14, + "1" + ], + [ + "ADD", + 6, + 14, + "-1" + ], + [ + "ADD", + 4, + 14, + "1" + ], + [ + "ADD", + 2, + 14, + "-1" + ], + [ + "ADD", + 0, + 14, + "1" + ], + [ + "SWAP", + 14, + 15 + ], + [ + "ADD", + 33, + 13, + "1" + ], + [ + "ADD", + 32, + 13, + "1" + ], + [ + "SWAP", + 13, + 31 + ], + [ + "ADD", + 10, + 12, + "1" + ], + [ + "ADD", + 8, + 12, + "-1" + ], + [ + "ADD", + 6, + 12, + "1" + ], + [ + "ADD", + 4, + 12, + "-1" + ], + [ + "ADD", + 2, + 12, + "1" + ], + [ + "ADD", + 0, + 12, + "-1" + ], + [ + "SWAP", + 12, + 14 + ], + [ + "ADD", + 33, + 11, + "-1" + ], + [ + "ADD", + 32, + 11, + "-1" + ], + [ + "ADD", + 31, + 11, + "-1" + ], + [ + "SCALE", + 11, + "-1" + ], + [ + "SWAP", + 11, + 30 + ], + [ + "ADD", + 8, + 10, + "1" + ], + [ + "ADD", + 6, + 10, + "-1" + ], + [ + "ADD", + 4, + 10, + "1" + ], + [ + "ADD", + 2, + 10, + "-1" + ], + [ + "ADD", + 0, + 10, + "1" + ], + [ + "SWAP", + 10, + 13 + ], + [ + "ADD", + 33, + 9, + "1" + ], + [ + "ADD", + 32, + 9, + "1" + ], + [ + "ADD", + 31, + 9, + "1" + ], + [ + "ADD", + 30, + 9, + "1" + ], + [ + "SWAP", + 9, + 29 + ], + [ + "ADD", + 6, + 8, + "1" + ], + [ + "ADD", + 4, + 8, + "-1" + ], + [ + "ADD", + 2, + 8, + "1" + ], + [ + "ADD", + 0, + 8, + "-1" + ], + [ + "SWAP", + 8, + 12 + ], + [ + "ADD", + 33, + 7, + "-1" + ], + [ + "ADD", + 32, + 7, + "-1" + ], + [ + "ADD", + 31, + 7, + "-1" + ], + [ + "ADD", + 30, + 7, + "-1" + ], + [ + "ADD", + 29, + 7, + "-1" + ], + [ + "SCALE", + 7, + "-1" + ], + [ + "SWAP", + 7, + 28 + ], + [ + "ADD", + 4, + 6, + "1" + ], + [ + "ADD", + 2, + 6, + "-1" + ], + [ + "ADD", + 0, + 6, + "1" + ], + [ + "SWAP", + 6, + 11 + ], + [ + "ADD", + 33, + 5, + "1" + ], + [ + "ADD", + 32, + 5, + "1" + ], + [ + "ADD", + 31, + 5, + "1" + ], + [ + "ADD", + 30, + 5, + "1" + ], + [ + "ADD", + 29, + 5, + "1" + ], + [ + "ADD", + 28, + 5, + "1" + ], + [ + "SWAP", + 5, + 27 + ], + [ + "ADD", + 2, + 4, + "1" + ], + [ + "ADD", + 0, + 4, + "-1" + ], + [ + "SWAP", + 4, + 10 + ], + [ + "ADD", + 33, + 3, + "-1" + ], + [ + "ADD", + 32, + 3, + "-1" + ], + [ + "ADD", + 31, + 3, + "-1" + ], + [ + "ADD", + 30, + 3, + "-1" + ], + [ + "ADD", + 29, + 3, + "-1" + ], + [ + "ADD", + 28, + 3, + "-1" + ], + [ + "ADD", + 27, + 3, + "-1" + ], + [ + "SCALE", + 3, + "-1" + ], + [ + "SWAP", + 3, + 26 + ], + [ + "ADD", + 0, + 2, + "1" + ], + [ + "SWAP", + 2, + 9 + ], + [ + "ADD", + 33, + 1, + "1" + ], + [ + "ADD", + 32, + 1, + "1" + ], + [ + "ADD", + 31, + 1, + "1" + ], + [ + "ADD", + 30, + 1, + "1" + ], + [ + "ADD", + 29, + 1, + "1" + ], + [ + "ADD", + 28, + 1, + "1" + ], + [ + "ADD", + 27, + 1, + "1" + ], + [ + "ADD", + 26, + 1, + "1" + ], + [ + "SWAP", + 1, + 25 + ], + [ + "SWAP", + 0, + 8 + ] + ], + "right": [ + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "-1", + "1", + "-1", + "1", + "-1", + "1", + "-1", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "-1", + "1", + "-1", + "1", + "-1", + "1", + "-1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "-1", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "-1", + "1", + "-1", + "1", + "-1", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "-1", + "1", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "-1", + "1", + "-1", + "1", + "-1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "-1", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "-1", + "1", + "-1", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "-1", + "1", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "-1", + "1", + "-1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "-1", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "-1", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "-1", + "1", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "-1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "-1", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "-1", + "1" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ] + ], + "right_program": [ + [ + "ADD", + 33, + 32, + "-1" + ], + [ + "SCALE", + 32, + "-1" + ], + [ + "ADD", + 32, + 31, + "1" + ], + [ + "ADD", + 30, + 31, + "-1" + ], + [ + "ADD", + 29, + 31, + "-1" + ], + [ + "ADD", + 28, + 31, + "-1" + ], + [ + "SCALE", + 31, + "-1" + ], + [ + "ADD", + 31, + 30, + "-1" + ], + [ + "ADD", + 29, + 30, + "-1" + ], + [ + "ADD", + 28, + 30, + "-1" + ], + [ + "SCALE", + 30, + "-1" + ], + [ + "ADD", + 31, + 29, + "-1" + ], + [ + "ADD", + 28, + 29, + "-1" + ], + [ + "SWAP", + 29, + 30 + ], + [ + "ADD", + 31, + 28, + "-1" + ], + [ + "SCALE", + 28, + "-1" + ], + [ + "ADD", + 31, + 27, + "1" + ], + [ + "ADD", + 26, + 27, + "-1" + ], + [ + "ADD", + 25, + 27, + "-1" + ], + [ + "SWAP", + 27, + 30 + ], + [ + "ADD", + 30, + 26, + "1" + ], + [ + "ADD", + 25, + 26, + "-1" + ], + [ + "SCALE", + 26, + "-1" + ], + [ + "ADD", + 30, + 25, + "1" + ], + [ + "SWAP", + 25, + 26 + ], + [ + "SWAP", + 24, + 29 + ], + [ + "SWAP", + 23, + 25 + ], + [ + "SWAP", + 22, + 23 + ], + [ + "SWAP", + 21, + 25 + ], + [ + "SWAP", + 20, + 27 + ], + [ + "SWAP", + 19, + 29 + ], + [ + "SWAP", + 18, + 31 + ], + [ + "SWAP", + 17, + 33 + ], + [ + "ADD", + 15, + 16, + "-1" + ], + [ + "ADD", + 14, + 15, + "-1" + ], + [ + "SWAP", + 15, + 32 + ], + [ + "ADD", + 13, + 14, + "-1" + ], + [ + "SWAP", + 14, + 32 + ], + [ + "ADD", + 12, + 13, + "-1" + ], + [ + "SWAP", + 13, + 24 + ], + [ + "ADD", + 11, + 12, + "-1" + ], + [ + "SWAP", + 12, + 32 + ], + [ + "ADD", + 10, + 11, + "-1" + ], + [ + "SWAP", + 11, + 20 + ], + [ + "ADD", + 9, + 10, + "-1" + ], + [ + "SWAP", + 10, + 24 + ], + [ + "ADD", + 8, + 9, + "-1" + ], + [ + "SWAP", + 9, + 28 + ], + [ + "SWAP", + 8, + 32 + ], + [ + "SWAP", + 7, + 18 + ], + [ + "SWAP", + 6, + 20 + ], + [ + "SWAP", + 5, + 22 + ], + [ + "SWAP", + 4, + 24 + ], + [ + "SWAP", + 3, + 26 + ], + [ + "SWAP", + 2, + 28 + ], + [ + "SWAP", + 1, + 30 + ], + [ + "SWAP", + 0, + 32 + ] + ] + }, + "diagonal": [ + [ + -1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 1 + ], + [ + -1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 0, + 1, + 1 + ], + [ + -1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 0, + 1, + 0, + 1, + 1 + ], + [ + -1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 1 + ], + [ + -1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 1 + ], + [ + -1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 1 + ], + [ + -1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 1 + ], + [ + -1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 1 + ], + [ + -1, + 1, + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + -1, + 1, + 1, + 0, + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + -1, + 1, + 1, + 0, + 1, + 0, + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + -1, + 1, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + -1, + 1, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + -1, + 1, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + -1, + 1, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + -1, + 1, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + -1, + 1, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 1 + ], + [ + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 1 + ], + [ + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 0, + 1, + 1 + ], + [ + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 0, + 1, + 0, + 1, + 1 + ], + [ + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 1 + ], + [ + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 1 + ], + [ + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 1 + ], + [ + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 1 + ], + [ + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 1 + ], + [ + 1, + 1, + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + 1, + 1, + 1, + 0, + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + 1, + 1, + 1, + 0, + 1, + 0, + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + 1, + 1, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + 1, + 1, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + 1, + 1, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + 1, + 1, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + 1, + 1, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + 1, + 1, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 1 + ] + ], + "invoice": { + "main": { + "17": 448, + "25": 448, + "33": 448, + "41": 448, + "49": 448, + "57": 448, + "65": 448, + "73": 448, + "153": 224 + }, + "owned_streams_reused_sequentially": 1, + "paid": { + "1": 49045, + "2": 13547, + "3": 4256, + "4": 1938, + "5": 380, + "8": 152, + "16": 448, + "24": 448, + "32": 448, + "40": 448, + "48": 448, + "56": 448, + "64": 448, + "72": 448 + }, + "paid_calls": 72902, + "productive_fields": 11560, + "rank_surplus": 800, + "raw_scalar_record_bound": 1000000000, + "targets": { + "5": 532, + "6": 342, + "7": 1064, + "8": 1767, + "9": 4047, + "17": 448, + "25": 448, + "33": 448, + "41": 448, + "49": 448, + "57": 448, + "65": 448, + "73": 448, + "153": 224 + }, + "thick_calls": 19, + "thick_stages": [ + 0, + 1, + 3, + 5, + 7, + 9, + 11, + 13, + 15, + 17, + 19, + 21, + 23, + 25, + 27, + 29, + 31, + 33, + 34 + ], + "thin_queries": 1792, + "whole_idle": { + "16": 448, + "24": 448, + "32": 448, + "40": 448, + "48": 448, + "56": 448, + "64": 448, + "72": 448 + } + }, + "keep_mask": 280378328416255, + "kind": "complex", + "pairs": 17, + "physical_events": [ + [ + "LOCAL", + 0, + 0, + false + ], + [ + "LOCAL", + 1, + 0, + true + ], + [ + "IDLE", + 1, + [ + 0, + 1 + ] + ], + [ + "ADD", + 0, + 2, + 1 + ], + [ + "ADD", + 3, + 1, + -1 + ], + [ + "QUERY_SHEAR", + 2, + 0, + false + ], + [ + "ADD", + 0, + 2, + -1 + ], + [ + "ADD", + 3, + 1, + 1 + ], + [ + "LOCAL", + 3, + 1, + true + ], + [ + "IDLE", + 2, + [ + 0, + 1, + 3 + ] + ], + [ + "ADD", + 2, + 4, + 1 + ], + [ + "ADD", + 5, + 3, + -1 + ], + [ + "QUERY_SHEAR", + 4, + 1, + false + ], + [ + "ADD", + 2, + 4, + -1 + ], + [ + "ADD", + 5, + 3, + 1 + ], + [ + "LOCAL", + 5, + 2, + true + ], + [ + "IDLE", + 3, + [ + 0, + 1, + 3, + 5 + ] + ], + [ + "ADD", + 4, + 6, + 1 + ], + [ + "ADD", + 7, + 5, + -1 + ], + [ + "QUERY_SHEAR", + 6, + 2, + false + ], + [ + "ADD", + 4, + 6, + -1 + ], + [ + "ADD", + 7, + 5, + 1 + ], + [ + "LOCAL", + 7, + 3, + true + ], + [ + "IDLE", + 4, + [ + 0, + 1, + 3, + 5, + 7 + ] + ], + [ + "ADD", + 6, + 8, + 1 + ], + [ + "ADD", + 9, + 7, + -1 + ], + [ + "QUERY_SHEAR", + 8, + 3, + false + ], + [ + "ADD", + 6, + 8, + -1 + ], + [ + "ADD", + 9, + 7, + 1 + ], + [ + "LOCAL", + 9, + 4, + true + ], + [ + "IDLE", + 5, + [ + 0, + 1, + 3, + 5, + 7, + 9 + ] + ], + [ + "ADD", + 8, + 10, + 1 + ], + [ + "ADD", + 11, + 9, + -1 + ], + [ + "QUERY_SHEAR", + 10, + 4, + false + ], + [ + "ADD", + 8, + 10, + -1 + ], + [ + "ADD", + 11, + 9, + 1 + ], + [ + "LOCAL", + 11, + 5, + true + ], + [ + "IDLE", + 6, + [ + 0, + 1, + 3, + 5, + 7, + 9, + 11 + ] + ], + [ + "ADD", + 10, + 12, + 1 + ], + [ + "ADD", + 13, + 11, + -1 + ], + [ + "QUERY_SHEAR", + 12, + 5, + false + ], + [ + "ADD", + 10, + 12, + -1 + ], + [ + "ADD", + 13, + 11, + 1 + ], + [ + "LOCAL", + 13, + 6, + true + ], + [ + "IDLE", + 7, + [ + 0, + 1, + 3, + 5, + 7, + 9, + 11, + 13 + ] + ], + [ + "ADD", + 12, + 14, + 1 + ], + [ + "ADD", + 15, + 13, + -1 + ], + [ + "QUERY_SHEAR", + 14, + 6, + false + ], + [ + "ADD", + 12, + 14, + -1 + ], + [ + "ADD", + 15, + 13, + 1 + ], + [ + "LOCAL", + 15, + 7, + true + ], + [ + "IDLE", + 8, + [ + 0, + 1, + 3, + 5, + 7, + 9, + 11, + 13, + 15 + ] + ], + [ + "ADD", + 14, + 16, + 1 + ], + [ + "ADD", + 17, + 15, + -1 + ], + [ + "QUERY_SHEAR", + 16, + 7, + false + ], + [ + "ADD", + 14, + 16, + -1 + ], + [ + "ADD", + 17, + 15, + 1 + ], + [ + "LOCAL", + 17, + 8, + true + ], + [ + "ADD", + 16, + 18, + 1 + ], + [ + "ADD", + 19, + 17, + -1 + ], + [ + "QUERY_SHEAR", + 18, + 8, + false + ], + [ + "ADD", + 16, + 18, + -1 + ], + [ + "ADD", + 19, + 17, + 1 + ], + [ + "LOCAL", + 19, + 9, + true + ], + [ + "ADD", + 18, + 20, + 1 + ], + [ + "ADD", + 21, + 19, + -1 + ], + [ + "QUERY_SHEAR", + 20, + 9, + false + ], + [ + "ADD", + 18, + 20, + -1 + ], + [ + "ADD", + 21, + 19, + 1 + ], + [ + "LOCAL", + 21, + 10, + true + ], + [ + "ADD", + 20, + 22, + 1 + ], + [ + "ADD", + 23, + 21, + -1 + ], + [ + "QUERY_SHEAR", + 22, + 10, + false + ], + [ + "ADD", + 20, + 22, + -1 + ], + [ + "ADD", + 23, + 21, + 1 + ], + [ + "LOCAL", + 23, + 11, + true + ], + [ + "ADD", + 22, + 24, + 1 + ], + [ + "ADD", + 25, + 23, + -1 + ], + [ + "QUERY_SHEAR", + 24, + 11, + false + ], + [ + "ADD", + 22, + 24, + -1 + ], + [ + "ADD", + 25, + 23, + 1 + ], + [ + "LOCAL", + 25, + 12, + true + ], + [ + "ADD", + 24, + 26, + 1 + ], + [ + "ADD", + 27, + 25, + -1 + ], + [ + "QUERY_SHEAR", + 26, + 12, + false + ], + [ + "ADD", + 24, + 26, + -1 + ], + [ + "ADD", + 27, + 25, + 1 + ], + [ + "LOCAL", + 27, + 13, + true + ], + [ + "ADD", + 26, + 28, + 1 + ], + [ + "ADD", + 29, + 27, + -1 + ], + [ + "QUERY_SHEAR", + 28, + 13, + false + ], + [ + "ADD", + 26, + 28, + -1 + ], + [ + "ADD", + 29, + 27, + 1 + ], + [ + "LOCAL", + 29, + 14, + true + ], + [ + "ADD", + 28, + 30, + 1 + ], + [ + "ADD", + 31, + 29, + -1 + ], + [ + "QUERY_SHEAR", + 30, + 14, + false + ], + [ + "ADD", + 28, + 30, + -1 + ], + [ + "ADD", + 31, + 29, + 1 + ], + [ + "LOCAL", + 31, + 15, + true + ], + [ + "ADD", + 30, + 32, + 1 + ], + [ + "ADD", + 33, + 31, + -1 + ], + [ + "QUERY_SHEAR", + 32, + 15, + false + ], + [ + "ADD", + 30, + 32, + -1 + ], + [ + "ADD", + 33, + 31, + 1 + ], + [ + "LOCAL", + 33, + 16, + true + ], + [ + "LOCAL", + 34, + 16, + false + ], + [ + "IDLE", + 8, + [ + 19, + 21, + 23, + 25, + 27, + 29, + 31, + 33, + 34 + ] + ], + [ + "IDLE", + 9, + [ + 21, + 23, + 25, + 27, + 29, + 31, + 33, + 34 + ] + ], + [ + "IDLE", + 10, + [ + 23, + 25, + 27, + 29, + 31, + 33, + 34 + ] + ], + [ + "IDLE", + 11, + [ + 25, + 27, + 29, + 31, + 33, + 34 + ] + ], + [ + "IDLE", + 12, + [ + 27, + 29, + 31, + 33, + 34 + ] + ], + [ + "IDLE", + 13, + [ + 29, + 31, + 33, + 34 + ] + ], + [ + "IDLE", + 14, + [ + 31, + 33, + 34 + ] + ], + [ + "IDLE", + 15, + [ + 33, + 34 + ] + ], + [ + "ADD", + 32, + 30, + 1 + ], + [ + "ADD", + 31, + 33, + -1 + ], + [ + "ADD", + 30, + 28, + 1 + ], + [ + "ADD", + 29, + 31, + -1 + ], + [ + "ADD", + 28, + 26, + 1 + ], + [ + "ADD", + 27, + 29, + -1 + ], + [ + "ADD", + 26, + 24, + 1 + ], + [ + "ADD", + 25, + 27, + -1 + ], + [ + "ADD", + 24, + 22, + 1 + ], + [ + "ADD", + 23, + 25, + -1 + ], + [ + "ADD", + 22, + 20, + 1 + ], + [ + "ADD", + 21, + 23, + -1 + ], + [ + "ADD", + 20, + 18, + 1 + ], + [ + "ADD", + 19, + 21, + -1 + ], + [ + "ADD", + 18, + 16, + 1 + ], + [ + "ADD", + 17, + 19, + -1 + ], + [ + "ADD", + 16, + 14, + 1 + ], + [ + "ADD", + 15, + 17, + -1 + ], + [ + "ADD", + 14, + 12, + 1 + ], + [ + "ADD", + 13, + 15, + -1 + ], + [ + "ADD", + 12, + 10, + 1 + ], + [ + "ADD", + 11, + 13, + -1 + ], + [ + "ADD", + 10, + 8, + 1 + ], + [ + "ADD", + 9, + 11, + -1 + ], + [ + "ADD", + 8, + 6, + 1 + ], + [ + "ADD", + 7, + 9, + -1 + ], + [ + "ADD", + 6, + 4, + 1 + ], + [ + "ADD", + 5, + 7, + -1 + ], + [ + "ADD", + 4, + 2, + 1 + ], + [ + "ADD", + 3, + 5, + -1 + ], + [ + "ADD", + 2, + 0, + 1 + ], + [ + "ADD", + 1, + 3, + -1 + ], + [ + "SIGNED_SWAP", + 0, + 1 + ], + [ + "SIGNED_SWAP", + 2, + 3 + ], + [ + "SIGNED_SWAP", + 4, + 5 + ], + [ + "SIGNED_SWAP", + 6, + 7 + ], + [ + "SIGNED_SWAP", + 8, + 9 + ], + [ + "SIGNED_SWAP", + 10, + 11 + ], + [ + "SIGNED_SWAP", + 12, + 13 + ], + [ + "SIGNED_SWAP", + 14, + 15 + ], + [ + "SIGNED_SWAP", + 16, + 17 + ], + [ + "SIGNED_SWAP", + 18, + 19 + ], + [ + "SIGNED_SWAP", + 20, + 21 + ], + [ + "SIGNED_SWAP", + 22, + 23 + ], + [ + "SIGNED_SWAP", + 24, + 25 + ], + [ + "SIGNED_SWAP", + 26, + 27 + ], + [ + "SIGNED_SWAP", + 28, + 29 + ], + [ + "SIGNED_SWAP", + 30, + 31 + ], + [ + "SIGNED_SWAP", + 32, + 33 + ] + ], + "prefix_pairs": 8 +} diff --git a/research/query-thinned-controllers/PROOF.md b/research/query-thinned-controllers/PROOF.md new file mode 100644 index 0000000000..9068f42989 --- /dev/null +++ b/research/query-thinned-controllers/PROOF.md @@ -0,0 +1,278 @@ +# Query-thinned productive controllers + +## Conditional result + +Under the retained native, whole-job matching, owned-erasure, tape, analytic, +precision and exact-recovery contracts of #4359/#4416, the construction below +gives + + T(n) = O(n (log n)^(1 - kappa)), kappa = 37/12500 = 0.00296. + +This is a new author-checked conditional construction. It is not an +unconditional theorem, a formal-kernel proof, a practical implementation or a +change to the selected record. It improves #4416/#4433's conditional 0.00268647 +by about 10.1818%, and the selected 0.0023 checkpoint by about 28.6957%. +Those percentages compare exponent savings, not running times. + +The new mechanism replaces selected full native invocations by copied +rank-one query shears. Losing their productive helpers is charged. Removing +their stage multipliers also removes the corresponding parts of every idle +transform and main target. These coupled changes improve the complete moment; +merely deleting a local bill would not. + +## 1. Exact local interfaces + +Retain the source local word's all-column interpretation. For complex data, +on each of 112 ports write Q for its central rank-one Gaussian and D_s for +the commuting fresh eight-axis multiplier at stage s. Stage zero instead +uses the source nine-axis multiplier times Q^-1. The forward and backward +physical local maps are + + D_s S_y(Q^-1), D_s S_x(-Q). + +The complete THREE-base supplier has independent helper targets + + {5:28, 6:18, 7:56, 8:93, 9:213} + +and unsplit paid profile + + {1:2487, 2:713, 3:224, 4:102, 5:20, 8:8}. + +Its 408 helpers are arbitrary original fields. The one sequentially reused +owned center receives no productive credit. These source words and their +all-column/phase evidence are retained unchanged; this contribution does not +repeat their full historical physical replay. + +For BIT, retain the PR589 local word on 111 ports and 439 arbitrary helpers. +Each helper target has rank 8, D_s has rank 7, Q is the port's rank-one +projector involution, and the paid profile is + + {1:1323, 2:1342, 3:79, 4:44, 5:102, 6:11, 7:19}. + +Its nine copied-center episodes remain in that profile. Its rational charts +and common-weight delayed-cover interpretation remain explicit premises. + +### The new query-only call + +To implement S_y(Q^-1) on arbitrary X,Y, clear one owned stream Z, copy X +into Z, perform Q^-1 on Z, add Z to Y, and erase Z. Return X unchanged and +Z zero. Backward uses Q and subtracts from X. Each port costs exactly one +paid rank-one job, plus the copy/add/erase and fixed matching/routing work. +There is no independent input or output credit for Z. + +For complex data Q^-1 is one positive Gaussian followed by its physical +Pauli translation: the Z4 phases -q and q+2q agree. It is not replaced by Q +using an order-two assumption. For BIT Q^-1=Q. The same construction at +column multiplicity f makes a rank-f request; this cost is never treated as +a scalar operation. Erasure is the inherited owned-stream erasure operation, +not a claim about reversible or dirty-borrowed erasure. + +## 2. The two actual finite controller words + +Start with the credited paired path controller, keeping all middle idle +windows and splitting the initial/terminal windows at a. Let p be the pair +count, with 2p+1 local stages. Keep the full native call at stages + + S = {0, 2p} union {1,3,...,2p-1}. + +Replace each other local call by its query-only shear. In every idle word, +remove those same stage multipliers. Every scalar bridge and signed exchange +remains in its original chronological place. Thus there are p+2 full native +calls and p-1 query shears. Thin stages have no fresh axes or helpers. + +`controller.py` constructs the words and constant scalar boundaries. The +verifier replays the emitted LOCAL, QUERY_SHEAR, IDLE, ADD and exchange events +directly, compares with the original polynomial specialized by D_s=1 on thin +stages, and checks every coefficient of L A R against the advertised diagonal. +The complex check is over rational Laurent polynomials, with all Q signs +retained. BIT has a separate exact binary group-ring factorization. + +Only two finite words are needed: + +| Family | p | a | Full native calls | Query shears | Active ambient rank | +|---|---:|---:|---:|---:|---:| +| Complex | 17 | 8 | 19 | 16 | 153 | +| BIT | 16 | 7 | 18 | 15 | 127 | + +Unused fresh blocks can be removed by an injective relabeling. All noninitial +complex native contacts occur on the same old-nine plus fresh-eight space; +other blocks are fixed spectators. Exact forward/inverse phase checks on +all 112 ports establish this contact independently of the number of stages. +The initial native call is unchanged. The binary rational 15-dimensional +charts are likewise checked on all 111 ports. Tensoring these identities with +I_f preserves them for each positive column multiplicity under the inherited +all-column implementation contract. + +For block rank d and port count v, the main targets are two v-field copies +of rank 1+d(p+2), and two v-field copies of rank 1+d(j+1) for j=1..a and +j=1..p-1-a. The corresponding whole idle ranks are d(j+1), each with 2v +calls. The old one-stage middle idles have become identities. In addition, +there are (p+2) fresh helper inventories, (p+2) native paid inventories, and +v(p-1) paid rank-one queries. Literal and formula-derived ledgers agree. + +All helper identities are allocated freshly per full invocation. The main +fields, helpers and suspended centers have distinct physical slots. Scalar +boundary changes are invertible, so independent arbitrary main inputs remain +independent. Thin copies introduce no new sources. Center/query ownership is +retained until the relevant call returns, and every matcher is undone. + +The exact invoices are in RESULT.json. Their basic resource counts are: + +| Family | Productive fields | Paid jobs | Productive rank mass | Paid rank mass | Surplus | +|---|---:|---:|---:|---:|---:| +| Complex | 11,560 | 72,902 | 258,271 | 257,471 | 800 | +| BIT | 11,454 | 57,555 | 217,506 | 216,753 | 753 | + +Both paid and target ranks overlap. They are not directly admitted to the +strict compiler. Raw numerical roots near 0.002960345565 and 0.003464248972 +were discovery aids; the argument uses the exact strict tests below. + +## 3. Charged tensor completion and splitting + +Apply #4416's chronological product construction and #4433's higher-moment +tail theorem to each new native unit. This is composition of actual programs: +copies are paused at the same paid position, a complete child unit runs on +distinct current owners, and it returns before any parent resumes. Correlated +values in distinct slots are allowed. No product of sums of operator matrices +is substituted for this schedule. + +Write T_t,P_t for the raw moments, B for the productive field count, +t=1-C, and choose cutoff c, target floor b, u>=C and integer power v. +After the product finishes, complete every rank K2^26*N^5, also avoiding the finite denominators and +rank witnesses, exceeds 256/(C0-C1)*N^5 and pays the complete fallback. + +Change the atom power to delta=0.004. With retained old ordinary saving +a_old=0.0000384599, the ordinary saving is exactly + + (1-delta)*C1+delta*a_old = 0.0034363538396 > 0.0034. + +Admit 0.0034. The linear adapter has saving delta>0.0034363538396; stock +is sublinear because delta<1-0.0034363538396. The old delta=0.003 fails +this adapter comparison and is explicitly rejected. All compiled dimensions, +role counts, routes, centers and leaf counts replace the old p3 constants in +the delayed-cover stock formulas. For fixed compiled N,B,P, the borrowed +digits remain O(w log e)=o(e), with w=ceil(e^0.004). + +Put kappa=0.00296, C=0.00296030, d=(C-kappa)/7, and + + complex_uniform = kappa+6d, b=kappa+5d, + a=kappa+4d, q=kappa+3d, + epsilon=1-d, beta=1-3d, r0=d/10, stop=layout=d. + +Use the admitted BIT saving 0.0034 in the unchanged nine-row outer ledger. +All 54 named strict predicates and the three retained functional predicates +pass. An additional functional predicate binds the new BIT atom explicitly, +beta*(1-0.004)>0. The smallest outer saving exceeds kappa by +629378373/4900000000000000. Old BIT admission, zero layout, closed epsilon, +closed complex slack and an unfunded endpoint each fail their intended checks. + +## 5. Finite constants, precision and scope + +No new operation is declared free. Raw scalar programs, signed swaps, copy/ +erase records, affine port charts and inverse routes are finite emitted lists. +The conservative raw scalar record bound is 10^9, above the checked local, +query and boundary bills. Every query adds its own paid job and its own +fixed routing records. Initial/end charts and target normalizers are retained. + +For a raw unit with productive count B, paid count P and scalar bound L0, +a v-fold chronological product has at most +L0*v*(B+P)^v nonrecursive records before final completion. Its old paid rank +mass is P1^v, and added completion rank is at most B^v*b^v. Bound all new +completion/splitting records by their integer rank masses, then multiply by +10*m^(2v)+10 to cover whole-job normalizers and inverse routes. This is a +constructive finite overestimate, not a claim that those movements vanish. +Allocate a distinct center to each simultaneously suspended instance; a +bound by the total expanded record count suffices. The integer compiler adds +only finitely many effective classes and clears their batch denominators. + +Apply the retained semantic-precision and stock prescriptions to these new +finite lists, coefficient heights, prefix row norms, owned centers and +matchers. They are fixed constants before the asymptotic input size varies. +All raw complex boundary coefficients are unit signed scalars; native dyadic +coefficients and BIT rational cover entries retain their pinned bounds. A +brute-force product of per-record row-mass bounds supplies an effective +prefix bound if a sharper bound is unnecessary. Increase the fixed precision +constant and fixed stock coefficient accordingly. The outer slack conditions +are strict, so absorbing these fixed constants does not change their powers. +This inherits the same all-column, physical tape, native movement/repair, +precision, analytic and recovery contracts as the reviewed source; it does +not independently prove that historical implementation stack. + +## 6. Sources, attribution, validation and next questions + +Canonical baseline: 3a23e9d9d2e67833515d1c60a17e966bcdcab43c, priority +revision 7. Refreshed main and PR checks are recorded in TASK.json. Live +overlap covered all open PR bodies and Discussion pages; sparse local README +coverage and closed-PR-body coverage are incomplete. No novelty theorem is +claimed. #4194's coded/clean local hybrid addresses a different interface; +this construction uses complete native calls and copied rank-one shears. + +Credit: zxv for the retained controller/native construction and higher-moment +tail proof (#4359/#4433); Jacob Alan Sussman for mixed-target integer flow +(#4268); Cinna Davis for the p7 paid-completion/native construction (#4416); +DreamingOfClouds, eumemic and their retained PR589/PR555 BIT lineage; +David Ganz, Jeremy Kothe, Rohan Arun, Marius-Paul Dumitrean, Erwan Secousses +and the native/outer contributors named in the unchanged source notices and +the selected contributor map. New query-thinning construction, proofs and +checks were prepared for Cinna Davis with substantial OpenAI Codex assistance. +Apache-2.0. No subagents were used. + +Reproduce with the registered command in README.md. Finite source, physical +operator, phase, interval, invoice and outer checks support this written +conditional proof; they do not constitute formal verification. Full old native +word replays, Lean and Docker were not rerun for this contribution. + +Open next questions, with first steps and blockers, are in TASK.json. The +next useful audit is the whole-job/owned-query lowering at arbitrary column +multiplicity. The next improvement question is a changed local query/native +alphabet or controller topology. A larger path census alone gives no global +optimality or assurance of a stronger complete construction. diff --git a/research/query-thinned-controllers/README.md b/research/query-thinned-controllers/README.md new file mode 100644 index 0000000000..6d1099e9a5 --- /dev/null +++ b/research/query-thinned-controllers/README.md @@ -0,0 +1,39 @@ +# Conditional κ = 0.00296 through query-thinned productive controllers + +The new construction replaces selected full native calls by paid rank-one +query shears, charging the lost productive helpers and removing the same +stage multipliers from the idle and main transforms. It gives an author-checked +conditional multiplication saving **κ = 37/12500 = 0.00296**, approximately +**10.18% above #4416/#4433's 0.00268647**. + +The complex controller uses 17 pairs, 19 full native calls and 16 query shears. +The accompanying BIT controller uses 16 pairs, 18 full calls and 15 query +shears, supporting a stronger ordinary BIT saving of 0.0034 after all cover +and atom-conversion charges. The complete outer ledger passes at κ=0.00296. + +[PROOF.md](PROOF.md) gives the native query implementation, chronological +product and paid completion, effective compiler ranks, changed BIT stock +parameters, full cost/precision obligations, attribution and conditional scope. +[RESULT.json](RESULT.json) records the exact arithmetic and rejection controls. +The two controller JSON files contain their actual emitted event lists and +constant scalar boundary programs. `controller.py` regenerates them; normal +verification directly replays them without repeating factor discovery. + +```sh +python3.12 -B scripts/research_package.py --package research/query-thinned-controllers +python3.12 -O -B research/query-thinned-controllers/verify.py +``` + +See VALIDATION.md for the exact executed environments and commands. + +This retains the reviewed source's all-column native, owned-erasure, +whole-job matching, fixed-tape, precision, analytic, prime and recovery +premises. It claims no unconditional theorem, formal verification, practical +speedup, global controller optimum or selected-frontier change. + +## Open next questions + +Open next questions are recorded in [TASK.json](TASK.json), with relevance, +first steps and blockers. Prepared for Cinna Davis with substantial OpenAI +Codex assistance; no subagents. Apache-2.0. Source attribution is in PROOF.md +and the unchanged pinned predecessor notices. diff --git a/research/query-thinned-controllers/RESULT.json b/research/query-thinned-controllers/RESULT.json new file mode 100644 index 0000000000..e0695152c9 --- /dev/null +++ b/research/query-thinned-controllers/RESULT.json @@ -0,0 +1,356 @@ +{ + "bit_invoice": { + "main": { + "127": 222, + "15": 444, + "22": 444, + "29": 444, + "36": 444, + "43": 444, + "50": 444, + "57": 444, + "64": 222 + }, + "owned_streams_reused_sequentially": 1, + "paid": { + "1": 25479, + "14": 444, + "2": 24156, + "21": 444, + "28": 444, + "3": 1422, + "35": 444, + "4": 792, + "42": 444, + "49": 444, + "5": 1836, + "56": 444, + "6": 198, + "63": 222, + "7": 342 + }, + "paid_calls": 57555, + "productive_fields": 11454, + "rank_surplus": 753, + "raw_scalar_record_bound": 1000000000, + "targets": { + "127": 222, + "15": 444, + "22": 444, + "29": 444, + "36": 444, + "43": 444, + "50": 444, + "57": 444, + "64": 222, + "8": 7902 + }, + "thick_calls": 18, + "thick_stages": [ + 0, + 1, + 3, + 5, + 7, + 9, + 11, + 13, + 15, + 17, + 19, + 21, + 23, + 25, + 27, + 29, + 31, + 32 + ], + "thin_queries": 1665, + "whole_idle": { + "14": 444, + "21": 444, + "28": 444, + "35": 444, + "42": 444, + "49": 444, + "56": 444, + "63": 222 + } + }, + "bit_strictification": { + "alpha": { + "lower": "0.999995735238059506641600561767", + "upper": "0.999995735238059506641600561768" + }, + "compiler_H0": 3755884544, + "cutoff_base": 17, + "delta": { + "lower": "0.949707924144871179442776557218", + "upper": "0.949707924144871179442776557219" + }, + "gamma": { + "lower": "0.957429821066420278606254392110", + "upper": "0.957429821066420278606254392111" + }, + "normalized_surplus_lower": "68719461047/16845935476736", + "tail_exponent": "1/5", + "target_floor_base": 18, + "tensor_power": 1024, + "tested_saving": "173/50000", + "uniform_H1": 25986965159937, + "uniform_N": "2^25986965159937", + "uniform_saving": "3459/1000000", + "winning_word_materialized": false + }, + "complex_invoice": { + "main": { + "153": 224, + "17": 448, + "25": 448, + "33": 448, + "41": 448, + "49": 448, + "57": 448, + "65": 448, + "73": 448 + }, + "owned_streams_reused_sequentially": 1, + "paid": { + "1": 49045, + "16": 448, + "2": 13547, + "24": 448, + "3": 4256, + "32": 448, + "4": 1938, + "40": 448, + "48": 448, + "5": 380, + "56": 448, + "64": 448, + "72": 448, + "8": 152 + }, + "paid_calls": 72902, + "productive_fields": 11560, + "rank_surplus": 800, + "raw_scalar_record_bound": 1000000000, + "targets": { + "153": 224, + "17": 448, + "25": 448, + "33": 448, + "41": 448, + "49": 448, + "5": 532, + "57": 448, + "6": 342, + "65": 448, + "7": 1064, + "73": 448, + "8": 1767, + "9": 4047 + }, + "thick_calls": 19, + "thick_stages": [ + 0, + 1, + 3, + 5, + 7, + 9, + 11, + 13, + 15, + 17, + 19, + 21, + 23, + 25, + 27, + 29, + 31, + 33, + 34 + ], + "thin_queries": 1792, + "whole_idle": { + "16": 448, + "24": 448, + "32": 448, + "40": 448, + "48": 448, + "56": 448, + "64": 448, + "72": 448 + } + }, + "complex_strictification": { + "alpha": { + "lower": "0.999999952117240859760145478345", + "upper": "0.999999952117240859760145478346" + }, + "compiler_H0": 75415467350, + "cutoff_base": 20, + "delta": { + "lower": "0.941649713484853845388929204840", + "upper": "0.941649713484853845388929204841" + }, + "gamma": { + "lower": "0.967466409565147920980822933859", + "upper": "0.967466409565147920980822933860" + }, + "normalized_surplus_lower": "8589700209/251666829934592", + "tail_exponent": "1/5", + "target_floor_base": 21, + "tensor_power": 1024, + "tested_saving": "29603/10000000", + "uniform_H1": 10418370291022217, + "uniform_N": "2^10418370291022217", + "uniform_saving": "103609/35000000", + "winning_word_materialized": false + }, + "kappa": "37/12500", + "minimum_outer_margin_minus_kappa": "629378373/4900000000000000", + "native": { + "binary_charts": 111, + "complex_contacts_and_inverses": 896, + "owned_stream_restored_zero": true, + "thin_paid_rank_per_port": 1, + "thin_productive_credit": 0 + }, + "negative_controls": { + "closed_epsilon": [ + "epsilon_below_one", + "global_gamma_power_slack", + "actual_logarithmic_gamma_guard", + "source_axis_superpolynomial", + "gaussian_above_main", + "new_semantic_guard_with_C1_one" + ], + "closed_uniform_gap": [ + "new_complex_uniform_saving_above_b" + ], + "missing_layout": [ + "positive_layout_slack" + ], + "old_BIT_cap": [ + "actual_bit_above_effective" + ], + "unfunded_kappa": [ + "main_transform_above_kappa", + "global_coordinate_router_above_kappa", + "fused_gaussian_above_kappa", + "group_bit_router_above_kappa", + "boundary_algebraic_matrix_above_kappa" + ] + }, + "old_atom_rejected": true, + "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": "17429997759/17500000000", + "fixed_halo_explicit_metadata_branch": "1347500003/17500000", + "new_BIT_row_stock_sublinear_in_active_group": "69789991027/70000000000", + "new_semantic_group_guard": "9/70000000" + }, + "margins": { + "boundary_algebraic_matrix": "14504839378373/4900000000000000", + "fused_gaussian": "14504838135119/4900000000000000", + "global_coordinate_router": "51803/17500000", + "group_bit_router": "3626262033773/1225000000000000", + "group_scans": "34999997/35000000", + "main_transform": "14504629378373/4900000000000000", + "microbox_face_corrections": "1347500003/17500000", + "polynomial_products": "69999997/70000000", + "sparse_union_movement": "2005129839378373/4900000000000000" + }, + "parameters": { + "a": "51803/17500000", + "b": "41443/14000000", + "beta": "69999991/70000000", + "bit_saving": "17/5000", + "cap_xi": "4455129629378373/4900000000000000", + "complex_uniform_saving": "103609/35000000", + "d": "3/70000000", + "epsilon": "69999997/70000000", + "kappa": "37/12500", + "lambda_": "19940797/20000000", + "lambda_prime": "69792791/70000000", + "layout": "3/70000000", + "q": "207209/70000000", + "r0": "3/700000000", + "stop": "3/70000000", + "tested_saving": "29603/10000000" + }, + "strict_checks": { + "actual_bit_above_effective": "7697/17500000", + "actual_logarithmic_gamma_guard": "3/70000000", + "actual_logarithmic_group_guard": "444870685621627/2450000000000000", + "alpha_logarithm_absorption": "3/700000000", + "boundary_algebraic_matrix_above_kappa": "839378373/4900000000000000", + "cap_above_band": "2005129629378373/4900000000000000", + "cap_below_cell": "444870160621627/4900000000000000", + "cap_below_phase_cell_power": "5344870370621627/4900000000000000", + "complex_above_effective": "3/70000000", + "complex_below_one_over_32": "396057/14000000", + "complex_endpoint": "3/35000000", + "epsilon_below_one": "3/70000000", + "epsilon_positive": "69999997/70000000", + "fine_prime_halo_umbrella": "7/2", + "fused_gaussian_above_kappa": "838135119/4900000000000000", + "gaussian_above_main": "104378373/2450000000000000", + "global_coordinate_router_above_kappa": "3/17500000", + "global_gamma_power_slack": "27/700000000", + "group_below_dimension": "3/35000000", + "group_bit_router_above_kappa": "262033773/1225000000000000", + "group_gauge_power_slack": "444870675121627/2450000000000000", + "group_key_fits_record": "3/35000000", + "group_positive": "69999991/70000000", + "group_scans_above_kappa": "34896397/35000000", + "halo_covers_generic_inverse_radius": "5", + "improvement_over_user_baseline": "614514790400418148631/500000000000000000000000", + "lambda_above_internal": "3/140000000", + "lambda_above_sigma": "9/140000000", + "lambda_above_tau": "3/140000000", + "lambda_prime_above_lambda": "3/140000000", + "lambda_prime_above_leaf": "83875671/980000000000000", + "leaf_saving_above_effective": "41875671/980000000000000", + "main_transform_above_kappa": "629378373/4900000000000000", + "membership_arithmetic_fits_record": "3/70000000", + "microbox_face_corrections_above_kappa": "1347448203/17500000", + "microbox_halo_volume": "5530000009/70000000", + "new_complex_uniform_saving_above_b": "3/70000000", + "new_semantic_guard_with_C1_one": "3/70000000", + "polynomial_products_above_kappa": "69792797/70000000", + "positive_layout_slack": "3/70000000", + "q_below_effective": "3/70000000", + "q_below_internal": "3/70000000", + "q_below_leaf": "83875671/980000000000000", + "q_positive": "207209/70000000", + "short_record_fallback": "13958557/14000000", + "source_axis_superpolynomial": "3/70000000", + "sparse_union_movement_above_kappa": "1990625839378373/4900000000000000", + "stop_below_one": "69999997/70000000", + "stop_positive": "3/70000000", + "strassen_integer_power_gap": "1951441519231", + "support_router_span": "9/70000000", + "theta_positive_polynomial_power": "2", + "union_header_fits_record": "9/70000000", + "union_tag_work_per_visit_fits_record": "9/70000000" + } + }, + "relative_gain_over_p7": "27353/268647", + "schema": "query-thinned-productive-controllers/1", + "scope": "Conditional native construction; all-column, erasure, whole-job matching, fixed-tape, precision, analytic, prime and exact-recovery premises retained. No unconditional theorem or selected promotion.", + "source_inputs_authenticated": 17, + "status": "PASS_CONDITIONAL_QUERY_THINNED_KAPPA_00296" +} diff --git a/research/query-thinned-controllers/SOURCES.json b/research/query-thinned-controllers/SOURCES.json new file mode 100644 index 0000000000..0f061c87ff --- /dev/null +++ b/research/query-thinned-controllers/SOURCES.json @@ -0,0 +1,120 @@ +{ + "schema_version": 1, + "base_commit": "3a23e9d9d2e67833515d1c60a17e966bcdcab43c", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ed33caef5c5827693e9572d252a66f99cbb73d40", + "sha256": "5732707cc1e460b090b53f2463162749ad860de878a18f7408938671d295a9d9" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "64bfc5af6709ed9811171e0a2108f05e1219cb65", + "sha256": "352a6184713b8843d96fd2c2071eb7aeaa655906b7c51d45ad444912666c8a96" + }, + { + "path": "research/higher-moment-strictification/README.md", + "usage": "input", + "git_blob": "0a736ca89e1eafb73a30e1f2589cc45e6b5f76c3", + "sha256": "ebe80b68ff026ce90f71f274c31744f4c0b36132d15ebb7e39cf2d5df4df270d" + }, + { + "path": "research/higher-moment-strictification/verify.py", + "usage": "input", + "git_blob": "4b24a5096154736ce060474eb8c72dc64c303699", + "sha256": "0ce7e7137422d5ffeda22085c81fa88471bbe963100fdad62e659f1e3bf89326" + }, + { + "path": "research/kappa-0023-productive-jobs/dependencies/kappa-next-regime/bit-compression/carrier-reuse/reference/joint_pair_dag.py", + "usage": "input", + "git_blob": "8b40135a84e7f0f0cd44bed69655801310b916a7", + "sha256": "8a0de761642d21919e969475c3f13e5d01a4bae7343c1e1f37c586d94b676a85" + }, + { + "path": "research/kappa-0023-productive-jobs/dependencies/kappa-next-regime/direct-decoder/sources/DATA-PHASES.json", + "usage": "input", + "git_blob": "d9a4f84211182ca200c081ea061d724c8a2cfb70", + "sha256": "c5916ff312678f12aba403847643fbbc29f643acec60bdf836fa56cd3e8251fa" + }, + { + "path": "research/kappa-rebuild/bit/BIT-ALLSIZE-PARAMETERS.json", + "usage": "input", + "git_blob": "fbe6da7241357d89cf5c55b2e7ce2d0d046be32a", + "sha256": "edb273f59a27356ad89f38791590c3c806b228c3510eb508e01e89f2caba95ef" + }, + { + "path": "research/kappa-rebuild/bit/BIT-P3-NATIVE-BINDING.json", + "usage": "input", + "git_blob": "e8c5e4f077fea0bef355e6c3013c7f252d3606cf", + "sha256": "9ece46fdfda6182e757e9a3b1f513fb3d029d730f3bafdcd6ed59180a14175b0" + }, + { + "path": "research/kappa-rebuild/bit/DELAYED-COVER-BRIDGE.md", + "usage": "input", + "git_blob": "a58774e237c9362869a60a22bda35be09fb85872", + "sha256": "9731b93026717f5fa15851e3633cbb4bdc76eba2bffb9d6b4a3b69f7dd502443" + }, + { + "path": "research/kappa-rebuild/bit/MIXED-PRODUCTIVE-BIT.json", + "usage": "input", + "git_blob": "6a139eedbc1015c13df6f2a4333e1a89b5edd18d", + "sha256": "2f69a19f417c0e0d141c180f9b2fae3d358391b9a230f5848ee07c45450e70bf" + }, + { + "path": "research/kappa-rebuild/bit/bit_native_binding.py", + "usage": "input", + "git_blob": "f4c4082d89969ea311219d9af8013082d599f6f1", + "sha256": "bf6374225f388e7531fa6475cc255bd430100ff62c38d582c41601f0739de7b7" + }, + { + "path": "research/kappa-rebuild/bit/complex_controller_factor.py", + "usage": "input", + "git_blob": "cb0cff7c8be5f38f2ee52201d9d0907f9dfd7947", + "sha256": "1de9aaf918e6a4f2f5448754c1f3c3da3b85e6257849ebd097af09859c4e5497" + }, + { + "path": "research/kappa-rebuild/bit/mixed_productive_bit.py", + "usage": "input", + "git_blob": "9c7a8bd5d3ae4c19952648c815031858d6627b96", + "sha256": "b32291b0db7fc0d332ec444c70746ab0fb03351d2e50546f8bcb64060e3ff95e" + }, + { + "path": "research/kappa-rebuild/complex/FULL-IDENTITY.md", + "usage": "input", + "git_blob": "f97a23d7d21bd7f79c9d0cb14d8c6b44fddd3f23", + "sha256": "c4aa88c4943ef041e9542c519b7600ecf26ed6caff92558fdb07ac88ace64c17" + }, + { + "path": "research/kappa-rebuild/complex/full-identity-certificates/RESULT.json", + "usage": "input", + "git_blob": "c6edcbdc43bf36bb11201235027d0ec170d07fc8", + "sha256": "943d5fad2fc529f470df05a35446e07ecaef7344abfce450d2c2eb2c9b3798f6" + }, + { + "path": "research/pr4359-p7-padding/TENSOR.md", + "usage": "input", + "git_blob": "8ecfd3e4d0bcb449ecb1e150c4f1f4fbb39ca656", + "sha256": "b2eba86cb979b4dc2a045f2e74bbd29e4d9e5ec87d6a2bc23ba7b54f1f58e3e3" + }, + { + "path": "research/pr4359-p7-padding/dependencies/compiler-refill/endpoint.py", + "usage": "input", + "git_blob": "340e1f0ffb8a1a9c38fbbd9119580b6d23e01b59", + "sha256": "d097e55f06c3f244f2074ffd7c1a0a5f3c4b4b6a6accf9619d1dde5c0ae85e15" + }, + { + "path": "research/pr4359-p7-padding/native_inventory.py", + "usage": "input", + "git_blob": "8d2d96e3998254c2333c43fe47cdfd074cbd811e", + "sha256": "65539acaf45bdfe8c5aee6830f9c9b3d1107c442a60842ef803fdd7688de8f32" + }, + { + "path": "research/kappa-rebuild/architecture/mixed_target_probe.py", + "usage": "input", + "git_blob": "4fc05ab08138218ba9f09e5c89b649afae7c914e", + "sha256": "011c3c9d0cf81103dc84d709a0e36793eb7c5ae3f23c85eac27650ef13afa04a" + } + ] +} diff --git a/research/query-thinned-controllers/TASK.json b/research/query-thinned-controllers/TASK.json new file mode 100644 index 0000000000..ebba49a09c --- /dev/null +++ b/research/query-thinned-controllers/TASK.json @@ -0,0 +1,86 @@ +{ + "schema_version": 1, + "task_id": "complex-new-helper-inventory", + "priority_revision": 7, + "base_commit": "3a23e9d9d2e67833515d1c60a17e966bcdcab43c", + "original_card": { + "id": "complex-new-helper-inventory", + "question": "Can a new local cost interface change the deficit-to-recursive-cost ratio beyond current packing?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/complex-local-word-ceiling/README.md", + "research/heterogeneous-owner-assembly/README.md", + "certificates/selected-result.json", + "research/selected-k8-unrestricted-ends/README.md" + ], + "methods": [ + "Propose a changed helper inventory and derive an optimistic exact moment.", + "Design a small completed instance and independently verify its endpoint and rank bill." + ], + "acceptance_gate": "A new physically realizable contract outside the frozen catalogue whose per-call profile, screened with ceiling.ceiling(), beats the selected word's packing ceiling; a lower cap does not establish identical circuitry or order attainable optima, and is insufficient to pass the stronger-budget target under this model. 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.", + "bottleneck_link": "Packing of the selected word is capped at +0.87% (ceiling model); only a lower local excess spend or a changed coverage law raises the cap.", + "allowed_variations": [ + "Narrow to one changed boundary or helper type with explicit counts.", + "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": [ + "Mixing only providers already inside the pinned catalogue.", + "Only changing helper terminal subspaces and monotone frames within the fixed scalar word, entrances and cleanup contract already covered by #1995/#2013.", + "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": [ + "helper inventory", + "heterogeneous-owner", + "mutable leaver" + ] + }, + "scope_status": "changed", + "actual_scope": "Construct query-thinned complex and BIT productive controllers and carry their exact physical words, paid tails, ordinary BIT conversion and complete outer costs to conditional kappa 0.00296.", + "scope_change_reason": "Explicit user assignment to improve kappa using the new productive-helper mechanism. The current card predates the selected changed interface; this replaces its frozen local-packing question with a complete global native/query construction.", + "bottleneck_link": "Selected full-native path calls impose stage and idle transforms even where a paid rank-one shear suffices. Removing them changes the full target/paid moment; a stronger BIT admission is needed above the prior cap.", + "budget_minutes": 60, + "stop_rule": "Finish the two actual finite native/query words and all caller costs; reject the endpoint if physical query ownership, full invoice, paid completion, BIT cover/stock or any outer predicate fails.", + "outcome": "completed", + "evidence": "PROOF.md, RESULT.json, COMPLEX-CONTROLLER.json, BIT-CONTROLLER.json, VALIDATION.md", + "author": "Cinna Davis / 1337isnot1337, with substantial OpenAI Codex assistance", + "ai_assistance": "Substantial OpenAI Codex assistance in derivation, implementation, audit and writing; no subagents.", + "open_questions": [ + { + "question": "Can the arbitrary-column owned-query lowering receive an independent native/tape audit?", + "why_it_matters": "It is the new primitive interface connecting the physical word to the changed exponent.", + "first_step": "Replay one complex inverse query and one binary cover query at two column multiplicities, charging copy, matching, read and erasure.", + "blocked_by": "Independent native/tape review of the retained all-column contracts." + }, + { + "question": "Can a changed local query/native alphabet or branching controller exceed this complete moment?", + "why_it_matters": "The old all-native p7 screen does not constrain this changed alphabet.", + "first_step": "Define a different complete finite physical word and screen its full invoice before larger native reconstruction.", + "blocked_by": "No stronger complete native/query construction has been established." + } + ], + "upstream_checkpoint": { + "main": "2a13eb1827784206202db90e5dc8327cf8a250db", + "checked_at_utc": "2026-10-21T20:06:00Z", + "priority_revision": 7, + "selected_kappa": "0.0023", + "stronger_reviewed_conditional_kappa": "0.00268647" + }, + "overlap_coverage": { + "open_prs": "296 bodies, complete pagination, 2026-10-21T19:50:54Z", + "discussions": "3284 records, complete pagination, 2026-10-21T19:51:43Z", + "local_readmes": "sparse; incomplete", + "closed_pr_bodies": "not exhaustively searched", + "additional_checks": "PR4194 coded/clean hybrid differs; PR4433 higher-moment theorem adopted. Frontier rechecked at 19:33, 19:51 and 20:06 UTC, through #4439; no higher kappa found." + } +} diff --git a/research/query-thinned-controllers/VALIDATION.md b/research/query-thinned-controllers/VALIDATION.md new file mode 100644 index 0000000000..8e9598ece7 --- /dev/null +++ b/research/query-thinned-controllers/VALIDATION.md @@ -0,0 +1,44 @@ +# Validation and limits + +Environment: Linux x86_64, CPython **3.12.14** (bundled runtime). Initial +factor discovery also ran on CPython 3.14.8. Standard library only. No +subagents, Lean build, Docker run or full historical suite. + +Completed on 2026-10-21: + +- `python3.12 -B scripts/research_package.py --package research/query-thinned-controllers --check-only` + passes metadata and all 17 input pins. +- `python3.12 -B scripts/research_package.py --package research/query-thinned-controllers` + passes the complete registered replay. +- `python3.12 -O -B research/query-thinned-controllers/verify.py` passes + from a separate **Git-free export** containing this package and exactly the + declared input files. Its RESULT.json agrees with the normal replay. +- The two external rejection controls also run in that Git-free export under + optimized Python. Appending a comment to the pinned interval source rejects + with `Changed source`. Changing an emitted QUERY_SHEAR to LOCAL rejects the + physical-event equality check. Both altered export files were restored; + no canonical predecessor file was changed. +- Internal controls execute omitted-clear and omitted-erase query words, + reverse a query's actual orientation, change a Laurent coefficient, retain + the old BIT cap or atom, close the complex/epsilon gap, omit layout, and + request the unfunded outer endpoint. Their intended gates reject. + +The exact native contacts include 896 complex forward/inverse checks and +111 rational binary charts. Both complete physical event lists are replayed. +Two rational interval implementations agree on the strict native moments. +The complete charged tensor tails, effective compiler ranks, ordinary BIT +cover/conversion and nine-row outer ledger pass. All 54 strict outer +predicates, three inherited functional predicates and the added stock guard +are retained. + +The actual local full-native words and their all-column implementation are +reused from the pinned reviewed lineage. Their entire historical physical +stack was not rerun. New winning tensor/uniform words are specified by +finite algorithms; their enormous instruction lists have not been emitted. +No finite pass establishes an unconditional theorem or formal verification. + +The committed-byte preflight and source-history check both pass after +committing the package, with all 28 package/input files matching and the pinned +canonical base in publication ancestry. Hosted CI is reported separately. +All reports retain the inherited native, whole-job, owned-erasure, fixed-tape, +precision, analytic, prime-supply and exact-recovery proof boundaries. diff --git a/research/query-thinned-controllers/VERIFY.json b/research/query-thinned-controllers/VERIFY.json new file mode 100644 index 0000000000..768aad6d68 --- /dev/null +++ b/research/query-thinned-controllers/VERIFY.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/higher-moment-strictification/README.md", + "research/higher-moment-strictification/verify.py", + "research/kappa-0023-productive-jobs/dependencies/kappa-next-regime/bit-compression/carrier-reuse/reference/joint_pair_dag.py", + "research/kappa-0023-productive-jobs/dependencies/kappa-next-regime/direct-decoder/sources/DATA-PHASES.json", + "research/kappa-rebuild/architecture/mixed_target_probe.py", + "research/kappa-rebuild/bit/BIT-ALLSIZE-PARAMETERS.json", + "research/kappa-rebuild/bit/BIT-P3-NATIVE-BINDING.json", + "research/kappa-rebuild/bit/DELAYED-COVER-BRIDGE.md", + "research/kappa-rebuild/bit/MIXED-PRODUCTIVE-BIT.json", + "research/kappa-rebuild/bit/bit_native_binding.py", + "research/kappa-rebuild/bit/complex_controller_factor.py", + "research/kappa-rebuild/bit/mixed_productive_bit.py", + "research/kappa-rebuild/complex/FULL-IDENTITY.md", + "research/kappa-rebuild/complex/full-identity-certificates/RESULT.json", + "research/pr4359-p7-padding/TENSOR.md", + "research/pr4359-p7-padding/dependencies/compiler-refill/endpoint.py", + "research/pr4359-p7-padding/native_inventory.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 600, + "checks": "Authenticate source blobs; replay both emitted physical controller words and exact boundary programs; native phase and rational chart checks; full query, completion, compiler, BIT cover and outer costs with negative controls." + } + ] +} diff --git a/research/query-thinned-controllers/controller.py b/research/query-thinned-controllers/controller.py new file mode 100644 index 0000000000..d4557e08cf --- /dev/null +++ b/research/query-thinned-controllers/controller.py @@ -0,0 +1,208 @@ +#!/usr/bin/env python3 +"""Exact native/query controller construction. Apache-2.0; Codex assistance.""" +from collections import Counter +from fractions import Fraction as Q +from hashlib import sha256 +import importlib.util +import json +from pathlib import Path +import sys + +sys.dont_write_bytecode = True +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def load(path, name): + spec = importlib.util.spec_from_file_location(name, path) + module = importlib.util.module_from_spec(spec) + sys.modules[name] = module + spec.loader.exec_module(module) + return module + + +def engines(): + reference = ROOT/'research/kappa-0023-productive-jobs/dependencies/kappa-next-regime/bit-compression/carrier-reuse/reference/joint_pair_dag.py' + load(reference, 'joint_pair_dag') + base = ROOT/'research/kappa-rebuild/bit' + bit = load(base/'mixed_productive_bit.py', 'mixed_productive_bit') + complex_ = load(base/'complex_controller_factor.py', 'query_complex_factor') + return bit, complex_ + + +def keep_mask(p, a): + b = p-1-a + return sum(1 << i for i in list(range(1, 2*p-2, 2))+ + list(range(0, 2*a, 2))+list(range(3*(p-1)-b, 3*(p-1)))) + + +def thick_stages(p): + return {0, 2*p, *range(1, 2*p, 2)} + + +def specialize_complex(coefficients, thick): + result = {} + for term, matrix in coefficients.items(): + key = (term[0],)+tuple(x if s in thick else 0 for s, x in enumerate(term[1:])) + out = result.setdefault(key, [[Q(0)]*len(matrix) for _ in matrix]) + for i, row in enumerate(matrix): + for j, value in enumerate(row): + out[i][j] += value + return {k: m for k, m in result.items() if any(any(row) for row in m)} + + +def specialize_bit(coefficients, thick): + keep = 1+sum(1 << (s+1) for s in thick) + out = {} + for term, matrix in coefficients.items(): + key = term & keep + old = out.setdefault(key, [0]*len(matrix)) + for i, row in enumerate(matrix): + old[i] ^= row + return {k: m for k, m in out.items() if any(m)} + + +def replay_events(events, p, kind): + """Literal second replay of the emitted word, including query-only gates.""" + _, engine = engines() + size, stages = 2*p, 2*p+1 + zero = (0,)*(stages+1) + matrix = [[{zero: Q(i == j)} if i == j else {} for j in range(size)] for i in range(size)] + for event in events: + op = event[0] + if op in ('LOCAL', 'QUERY_SHEAR'): + _, stage, pair, backward = event + x, y = 2*pair, 2*pair+1 + if backward: x, y = y, x + term = (1 if backward else -1,)+(0,)*stages + matrix[y] = [engine.plus(a, engine.monomial_times(b, term, -1 if backward else 1)) for a, b in zip(matrix[y], matrix[x])] + if op == 'LOCAL': + term = (0,)+tuple(int(s == stage) for s in range(stages)) + for role in (x, y): matrix[role] = [engine.monomial_times(a, term) for a in matrix[role]] + elif op == 'IDLE': + _, pair, selected = event + term = (0,)+tuple(int(s in selected) for s in range(stages)) + for role in (2*pair, 2*pair+1): matrix[role] = [engine.monomial_times(a, term) for a in matrix[role]] + elif op == 'ADD': + _, dst, src, *coefficient = event + c = coefficient[0] if coefficient else 1 + matrix[dst] = [engine.plus(a, b, c) for a, b in zip(matrix[dst], matrix[src])] + elif op in ('SWAP', 'SIGNED_SWAP'): + _, x, y = event + matrix[x], matrix[y] = matrix[y], [engine.monomial_times(a, zero, -1 if op == 'SIGNED_SWAP' else 1) for a in matrix[x]] + else: + raise ValueError('Unknown emitted event: '+op) + result = {} + for i, row in enumerate(matrix): + for j, poly in enumerate(row): + for key, value in poly.items(): + if kind == 'complex': + result.setdefault(key, [[Q(0)]*size for _ in range(size)])[i][j] += value + elif value.numerator % 2: + need(value.denominator == 1, 'Integral binary replay coefficient') + term = (key[0] % 2)+sum((exponent % 2) << (s+1) for s, exponent in enumerate(key[1:])) + result.setdefault(term, [0]*size)[i] ^= 1 << j + return {k: m for k, m in result.items() if any(any(r) for r in m)} if kind == 'complex' else {k: m for k, m in result.items() if any(m)} + + +def inventories(kind, p, a, diagonal, idles): + thick = thick_stages(p) + ports, block = (112, 8) if kind == 'complex' else (111, 7) + if kind == 'complex': + local = json.loads((ROOT/'research/kappa-rebuild/complex/full-identity-certificates/RESULT.json').read_text())['providers']['THREE-base'] + helpers = {int(k): v for k, v in local['helper_boundary']['widths'].items()} + children = {int(k): v for k, v in local['unsplit_replays']['forward']['paid_profile'].items()} + selected = [[s for s, x in enumerate(term[1:]) if x] for term in diagonal] + need(all(term[0] in (-1, 1) for term in diagonal), 'Only legal central Gaussian normalizers') + else: + helpers = {8: 439} + children = {1: 1323, 2: 1342, 3: 79, 4: 44, 5: 102, 6: 11, 7: 19} + selected = [[s for s in range(2*p+1) if term >> (s+1) & 1] for term in diagonal] + need(all(term & 1 for term in diagonal), 'Every binary main output retains its central rank-one factor') + targets = Counter({r: len(thick)*n for r, n in helpers.items()}) + paid = Counter({r: len(thick)*n for r, n in children.items()}) + thin_calls = ports*(2*p+1-len(thick)) + paid[1] += thin_calls + main = Counter() + for stages in selected: + need(set(stages) <= thick, 'No removed stage receives output credit') + main[1+block*len(stages)] += ports + targets.update(main) + idle = Counter() + for row in idles: + if row['retained']: + rank = block*len(thick.intersection(row['stages'])) + if rank: + idle[rank] += 2*ports + paid.update(idle) + # A second derivation uses only the declared prefix/suffix intervals. + expected_main = Counter({1+block*(p+2): 2*ports}) + expected_idle = Counter() + for length in (a, p-1-a): + for j in range(1, length+1): + expected_main[1+block*(j+1)] += 2*ports + expected_idle[block*(j+1)] += 2*ports + need(main == expected_main and idle == expected_idle, 'Literal and interval-derived complete invoices agree') + surplus = sum(r*n for r, n in targets.items())-sum(r*n for r, n in paid.items()) + need(surplus == (48*len(thick)-112 if kind == 'complex' else 48*len(thick)-111), 'Rank mass includes every query and lost helper') + return {'targets': dict(sorted(targets.items())), 'paid': dict(sorted(paid.items())), + 'main': dict(sorted(main.items())), 'whole_idle': dict(sorted(idle.items())), + 'productive_fields': sum(targets.values()), 'paid_calls': sum(paid.values()), + 'rank_surplus': surplus, 'thin_queries': thin_calls, + 'thick_calls': len(thick), 'thick_stages': sorted(thick), + 'raw_scalar_record_bound': 10**9, 'owned_streams_reused_sequentially': 1} + + +def run(kind, p, a): + bit, complex_ = engines() + mask = keep_mask(p, a) + thick = thick_stages(p) + if kind == 'complex': + coefficients, events, idles = complex_.controller(p, mask) + coefficients = specialize_complex(coefficients, thick) + factor = complex_.factor(coefficients) + need(factor is not None, 'Exact rational Laurent simultaneous factorization') + diagonal = factor['diagonal'] + boundaries = {'left': complex_.serialize_matrix(factor['left']), + 'right': complex_.serialize_matrix(factor['right']), + 'left_program': factor['left_program'], 'right_program': factor['right_program']} + need(all(Q(row[-1]) in (1, -1) for program in (factor['left_program'], factor['right_program']) + for row in program if row[0] in ('ADD', 'SCALE')), 'Unit scalar boundary coefficients') + else: + coefficients, events, idles = bit.physical_controller(p, mask) + coefficients = specialize_bit(coefficients, thick) + factor = bit.simultaneous_monomial_factor(coefficients) + need(factor is not None, 'Exact binary group-ring simultaneous factorization') + diagonal = factor['diagonal_monomials'] + boundaries = factor + invoice = inventories(kind, p, a, diagonal, idles) + new_events = [] + for row in events: + if row[0] == 'LOCAL' and row[1] not in thick: + new_events.append(['QUERY_SHEAR', *row[1:]]) + elif row[0] == 'IDLE': + selected = ([s for s in row[2] if s in thick] if kind == 'complex' else + [s for s in range(2*p+1) if row[2] >> (s+1) & 1 and s in thick]) + if selected: + new_events.append(['IDLE', row[1], selected]) + else: + new_events.append(row) + need(sum(row[0] == 'LOCAL' for row in new_events) == p+2, 'Exactly p+2 full native calls') + need(sum(row[0] == 'QUERY_SHEAR' for row in new_events) == p-1, 'Exactly p-1 copied-query shears') + return {'kind': kind, 'pairs': p, 'prefix_pairs': a, 'keep_mask': mask, + 'ambient_rank': 1+(8 if kind == 'complex' else 7)*(p+2), + 'diagonal': diagonal, 'boundaries': boundaries, + 'physical_events': new_events, 'invoice': invoice} + + +if __name__ == '__main__': + for kind, p, a in [('complex', 17, 8), ('bit', 16, 7)]: + row = run(kind, p, a) + path = HERE/(kind.upper()+'-CONTROLLER.json') + path.write_text(json.dumps(row, indent=2, sort_keys=True)+'\n') + print(kind, row['invoice'], flush=True) diff --git a/research/query-thinned-controllers/verify.py b/research/query-thinned-controllers/verify.py new file mode 100644 index 0000000000..f1114036ff --- /dev/null +++ b/research/query-thinned-controllers/verify.py @@ -0,0 +1,202 @@ +#!/usr/bin/env python3 +"""Exact finite replay for the conditional query-thinned construction. + +Apache-2.0. Prepared for Cinna Davis with substantial OpenAI Codex assistance. +Retains zxv's native/factor/tail work and Jacob Alan Sussman's integer flow. +""" +from fractions import Fraction as Q +from hashlib import sha1, sha256 +import argparse +import json +import sys +sys.dont_write_bytecode = True +import controller as C +HERE, ROOT, need = C.HERE, C.ROOT, C.need + + +def encode(x): + if isinstance(x, Q): return str(x) + if isinstance(x, dict): return {str(k): encode(v) for k, v in x.items()} + if isinstance(x, (list, tuple)): return [encode(v) for v in x] + return x + + +def authenticate(): + count = 0 + for row in json.loads((HERE/'SOURCES.json').read_text())['files']: + if row['usage'] != 'input': continue + path = ROOT/row['path']; raw = path.read_bytes() + need(not path.is_symlink(), 'No source alias') + need(sha256(raw).hexdigest() == row['sha256'], 'Changed source: '+row['path']) + need(sha1(b'blob '+str(len(raw)).encode()+b'\0'+raw).hexdigest() == row['git_blob'], 'Changed Git blob') + count += 1 + return count + + +def controllers(): + B, E = C.engines(); result = {} + for kind, p, a in [('complex', 17, 8), ('bit', 16, 7)]: + row = json.loads((HERE/(kind.upper()+'-CONTROLLER.json')).read_text()) + thick, mask = C.thick_stages(p), C.keep_mask(p, a) + if kind == 'complex': + coefficients, events, idles = E.controller(p, mask) + coefficients = C.specialize_complex(coefficients, thick) + left = [[Q(x) for x in r] for r in row['boundaries']['left']] + right = [[Q(x) for x in r] for r in row['boundaries']['right']] + diagonal = [tuple(term) for term in row['diagonal']] + transformed = {k: B.matrix_multiply(B.matrix_multiply(left, m), right) for k, m in coefficients.items()} + expected = {k: [[Q(i == j and diagonal[i] == k) for j in range(2*p)] for i in range(2*p)] for k in set(diagonal)} + need(transformed == expected, 'All exact rational Laurent coefficients, including signs and Q powers') + for name, matrix in [('left', left), ('right', right)]: + need(E.scalar_program(matrix) == row['boundaries'][name+'_program'], 'Literal unit scalar boundary program') + changed = dict(coefficients) + k = next(iter(changed)); changed[k] = [r[:] for r in changed[k]]; changed[k][0][0] += 1 + need(B.matrix_multiply(B.matrix_multiply(left, changed[k]), right) != expected.get(k), 'A changed physical coefficient is rejected') + else: + coefficients, events, idles = B.physical_controller(p, mask) + coefficients = C.specialize_bit(coefficients, thick) + fresh = B.simultaneous_monomial_factor(coefficients) + need(fresh == row['boundaries'], 'Exact binary physical operator and scalar boundaries') + diagonal = fresh['diagonal_monomials'] + need(C.replay_events(row['physical_events'], p, kind) == coefficients, + 'Emitted native/query/idle word equals the specialized physical source') + mutant = json.loads(json.dumps(row['physical_events'])) + # Every removed stage is forward; changing its direction must change + # the actual operator rather than merely a tariff field. + next(ev for ev in mutant if ev[0] == 'QUERY_SHEAR')[3] = True + need(C.replay_events(mutant, p, kind) != coefficients, 'Wrong query orientation rejected') + invoice = C.inventories(kind, p, a, diagonal, idles) + ports = 112 if kind == 'complex' else 111 + boundary_records = (sum(len(row['boundaries'][name+'_program']) for name in ('left', 'right')) + if kind == 'complex' else row['boundaries']['boundary_unit_ADDs_per_port']) + scalar_upper = (p+2)*10**6+16*invoice['thin_queries']+32*ports*(len(row['physical_events'])+boundary_records) + need(scalar_upper < invoice['raw_scalar_record_bound'], 'Conservative complete scalar/route count fits') + need(encode(invoice) == row['invoice'], 'Literal and closed-form complete '+kind+' invoice') + result[kind] = invoice + return result + + +def native_contacts(): + n = C.load(ROOT/'research/pr4359-p7-padding/native_inventory.py', 'thinned_native_phases') + phases = json.loads((ROOT/'research/kappa-0023-productive-jobs/dependencies/kappa-next-regime/direct-decoder/sources/DATA-PHASES.json').read_text()) + axes = tuple(1 << i for i in range(17)); old = [(a, 1) for a in axes[:9]]; fresh = [(a, 1) for a in axes[9:]] + checks = 0 + for recipe in phases['recipes']: + q = recipe['q']; basis = recipe['idle_children'][0]['orthogonal_axes'][:8] + need(all((b&q).bit_count() % 2 == 0 for b in basis), 'Old eight-space perpendicular to q') + swaps = [b ^ axes[9+i] for i, b in enumerate(basis)] + route = tuple(e ^ n.act(swaps, sum(((e&v).bit_count() % 2) << i for i, v in enumerate(swaps))) for e in axes) + need(all(n.act(route, route[i]) == axes[i] for i in range(17)), 'Exact physical route inverse') + need(all((a&b).bit_count() % 2 == int(i == j) for i, a in enumerate(route) for j, b in enumerate(route)), 'Orthogonal physical route') + need(n.act(route, q) == q, 'Central query direction fixed') + need(n.polynomial(n.norm([(q, -1)]), 17) == n.polynomial(n.norm([(q, 1), (q, 2)]), 17), + 'Inverse thin Gaussian is one positive query and a physical translation') + for sign in (-1, 1): + raw = (n.norm(old), n.norm(old+[(q, -1)])) + entry = (n.norm(fresh+[(q, sign)]), n.norm(fresh)) + out0 = n.norm(fresh+[(a, sign) for a in axes[:9]]) + local_out = (out0, n.norm(list(out0)+[(q, -sign)])) + out = (n.norm(old+fresh), n.norm(old+fresh+[(q, -1)])) + for x, y in list(zip(raw, entry))+list(zip(local_out, out)): + n.contact(x, y, route, 17); checks += 1 + for x, y in zip(raw, out): + need(n.polynomial(n.norm(list(y)+[(a, -c) for a, c in x]), 17) == n.polynomial(n.norm(fresh), 17), 'Exactly the fresh eight-axis multiplier') + bit = C.load(ROOT/'research/kappa-rebuild/bit/bit_native_binding.py', 'thinned_binary_charts') + ports = json.loads((ROOT/'research/kappa-rebuild/bit/BIT-P3-NATIVE-BINDING.json').read_text())['ports'] + local = json.loads((ROOT/'research/kappa-rebuild/bit/MIXED-PRODUCTIVE-BIT.json').read_text())['local'] + for direction in local['signed_directions']: + need({int(k): v for k, v in direction['profile'].items()} == C.engines()[0].LOCAL, + 'Every actual binary local child remains charged') + need(direction['unit_ADDs'] < 10**6 and direction['owned_COPY_episodes'] == 9, + 'Native binary scalar and owned-center bills retained') + for row in ports: + p = [[Q(x) for x in r] for r in row['central_projector']]; rho = [[Q(x) for x in r] for r in row['chart_15']] + active = [[p[i][j] if i < 8 and j < 8 else Q(i == j and i >= 8) for j in range(15)] for i in range(15)] + full = [[Q(i == j and i < 8) for j in range(15)] for i in range(15)] + need(bit.multiply(rho, rho) == bit.ident(15) and bit.multiply(bit.multiply(rho, active), rho) == full, 'BIT exact arbitrary-column chart') + need(bit.multiply(p, p) == p and sum(p[i][i] for i in range(8)) == 1, 'BIT query rank one') + # Formal independent X,Y,Z columns. Mutants execute the same word with + # an actual omitted operation; they are not merely different receipts. + for e in (-1, 1): + def execute(clear=True, erase=True): + x, y, z = {('X', 0): 1}, {('Y', 0): 1}, {('Z', 0): 1} + if clear: z = {} + for key, value in x.items(): z[key] = z.get(key, 0)+value + z = {(name, power+e): value for (name, power), value in z.items()} + for key, value in z.items(): y[key] = y.get(key, 0)+(-1 if e == 1 else 1)*value + if erase: z = {} + return x, y, z + expected = ({('X', 0): 1}, {('Y', 0): 1, ('X', e): -1 if e == 1 else 1}, {}) + need(execute() == expected, 'Completed arbitrary-input owned-query shear') + need(execute(clear=False) != expected and execute(erase=False) != expected, 'Clear/erase omission controls rejected') + return {'complex_contacts_and_inverses': checks, 'binary_charts': len(ports), + 'thin_paid_rank_per_port': 1, 'thin_productive_credit': 0, 'owned_stream_restored_zero': True} + + +def tail(E, invoice, tested, uniform, cutoff, floor, alpha_gap): + T, P = invoice['targets'], invoice['paid']; t, u, v = 1-tested, Q(1, 5), 1024 + target, paid = E.moment(T, t), E.moment(P, t) + alpha = E.divide(paid, target) + other = C.load(ROOT/'research/kappa-rebuild/architecture/mixed_target_probe.py', 'separate_rational_moment_engine') + tl, th = other.moment(T, tested); pl, ph = other.moment(P, tested) + need(tl > ph and max(target[0], tl) <= min(target[1], th) + and max(paid[0], pl) <= min(paid[1], ph), 'Separate rational interval engine agrees') + gamma = E.divide(E.moment(P, t+u), E.mul(E.power(cutoff, u), target)) + delta = E.divide((Q(sum(T.values())*floor),)*2, E.mul(E.power(cutoff, tested), target)) + need(alpha[1] < 1-alpha_gap and gamma[1] < Q(31, 32) and delta[1] < Q(19, 20), 'Three completely charged tail ratios') + need(Q(31, 32)**128 < Q(1, 16) and Q(19, 20)**128 < Q(1, 16), 'Exact decay blocks') + surplus = 1-Q(1)/(1+v*alpha_gap)-Q(4, 2**32) + need(surplus > 0, 'Original and completion tails both fit') + need(cutoff**64 < floor**63 and max(T) < 256, 'Strict ranks after completion and splitting') + h = Q(1, 64); z, z0 = 1-uniform, (t+1-uniform)/2; gap = z0-t + B, debt = (5+8*h)*v, 1+8*v*(1-z0) + x = (gap*B+debt)/(h*gap); H0 = -((-x.numerator)//x.denominator) + x = H0*(1-z0)/(z-z0); H1 = x.numerator//x.denominator+1 + need(H0 >= 8*v and H0*h*gap >= gap*B+debt and H1*(z-z0) > H0*(1-z0), 'Effective integer compiler bound') + return {'tested_saving': tested, 'uniform_saving': uniform, 'alpha': E.display(alpha), + 'gamma': E.display(gamma), 'delta': E.display(delta), 'tensor_power': v, + 'cutoff_base': cutoff, 'target_floor_base': floor, 'tail_exponent': u, + 'normalized_surplus_lower': surplus, 'compiler_H0': H0, 'uniform_H1': H1, + 'uniform_N': '2^'+str(H1), 'winning_word_materialized': False} + + +def run(): + count = authenticate(); rows = controllers(); native = native_contacts() + E = C.load(ROOT/'research/higher-moment-strictification/verify.py', 'credited_exact_intervals') + kappa, tested = Q('.00296'), Q('.00296030'); d = (tested-kappa)/7 + complex_ = tail(E, rows['complex'], tested, kappa+6*d, 20, 21, Q(1, 30000000)) + bit = tail(E, rows['bit'], Q('.00346'), Q('.003459'), 17, 18, Q(1, 250000)) + before, after, atom, old = Q('.003459'), Q('.00345'), Q('.004'), Q('.0000384599') + ordinary, admitted = (1-atom)*after+atom*old, Q('.0034') + need(before > after and atom > ordinary > admitted and atom < 1-ordinary, 'Complete ordinary BIT conversion') + need(Q('.003') < ordinary and 2**26 > 256/(before-after), 'Old atom rejected and finite prime bound') + L = C.load(ROOT/'research/pr4359-p7-padding/dependencies/compiler-refill/endpoint.py', 'complete_outer_ledger') + params = {'kappa': kappa, 'tested_saving': tested, 'complex_uniform_saving': kappa+6*d, + 'b': kappa+5*d, 'a': kappa+4*d, 'q': kappa+3*d, 'bit_saving': admitted, + 'epsilon': 1-d, 'beta': 1-3*d, 'r0': d/10, 'stop': d, 'layout': d, 'd': d} + outer = L.ledger(params) + outer['functional_checks']['actual_new_BIT_stock_sublinear'] = params['beta']*(1-atom) + need(len(outer['strict_checks']) == 54 and len(outer['functional_checks']) == 4, 'Complete predicate inventory') + need(all(x > 0 for group in ('strict_checks', 'functional_checks') for x in outer[group].values()), 'All outer predicates') + controls = {} + for label, changes in [('old_BIT_cap', {'bit_saving': Q('.0027')}), ('closed_uniform_gap', {'complex_uniform_saving': params['b']}), + ('unfunded_kappa', {'kappa': tested}), ('closed_epsilon', {'epsilon': Q(1)}), ('missing_layout', {'layout': Q(0)})]: + bad = L.ledger(dict(params, **changes)); failed = [k for k, v in bad['strict_checks'].items() if v <= 0] + need(failed, 'Reject '+label); controls[label] = failed + return encode({'schema': 'query-thinned-productive-controllers/1', 'status': 'PASS_CONDITIONAL_QUERY_THINNED_KAPPA_00296', + 'kappa': kappa, 'relative_gain_over_p7': kappa/Q('.00268647')-1, + 'source_inputs_authenticated': count, 'native': native, 'complex_invoice': rows['complex'], 'bit_invoice': rows['bit'], + 'complex_strictification': complex_, 'bit_strictification': bit, + 'ordinary_BIT': {'before_cover': before, 'after_cover': after, 'atom': atom, 'ordinary_saving': ordinary, + 'admitted': admitted, 'prime_rule': 'odd q > 2^26*N^5 avoiding all fixed denominators and rank witnesses'}, + 'outer': outer, 'minimum_outer_margin_minus_kappa': min(outer['margins'].values())-kappa, + 'negative_controls': controls, 'old_atom_rejected': True, + 'scope': 'Conditional native construction; all-column, erasure, whole-job matching, fixed-tape, precision, analytic, prime and exact-recovery premises retained. No unconditional theorem or selected promotion.'}) + + +if __name__ == '__main__': + parser = argparse.ArgumentParser(description=__doc__); parser.add_argument('--write', action='store_true'); args = parser.parse_args() + result = run(); output = HERE/'RESULT.json' + if args.write: output.write_text(json.dumps(result, indent=2, sort_keys=True)+'\n') + else: need(result == json.loads(output.read_text()), 'Complete receipt matches exact replay') + print(json.dumps({k: result[k] for k in ('status', 'kappa', 'source_inputs_authenticated', 'minimum_outer_margin_minus_kappa')}, sort_keys=True)) diff --git a/research/test-suite-locale-reads/SOURCES.json b/research/test-suite-locale-reads/SOURCES.json index be5f08378a..e3424afdb7 100644 --- a/research/test-suite-locale-reads/SOURCES.json +++ b/research/test-suite-locale-reads/SOURCES.json @@ -17,8 +17,9 @@ { "path": "docs/research/current-status.md", "usage": "input", - "git_blob": "d73b4ff9da41f044e793422db4318be17e234a6c", - "sha256": "adb54af005eb11edaf84d782fe729338680ff908f6d4fbf39ba1062d2e7d8a77" + "git_blob": "532af84312cbfeb39a1e4659d8398deb560f1e4a", + "sha256": "54c843968d0b178369a7e56161be44c4692935c3f46ce261678aeedadb309891", + "pin": "head:5f9d871c6bd1b9e34db5a7ea5ef08a908e94db39:docs/research/current-status.md" }, { "path": "tests/test_research_current_status.py",