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/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/native-lattice-retiming/LITERATURE.md b/research/native-lattice-retiming/LITERATURE.md new file mode 100644 index 0000000000..2e3a5b7846 --- /dev/null +++ b/research/native-lattice-retiming/LITERATURE.md @@ -0,0 +1,46 @@ +# Literature evaluated during this continuation + +Research notes, 21 October 2026. This revisits my +[0.0023 literature list](../kappa-0023-productive-jobs/LITERATURE.md). +The sources motivate experiments; their theorems are not imported as native +instructions or as a proof of the new multiplication bound. + +| Paper | Applicable idea | Missing transfer / outcome here | +| --- | --- | --- | +| [Dumas–Grenet, In-place accumulation, §3 and Theorem 5](https://arxiv.org/html/2307.12712v3) | Prepare output registers by subtraction, accumulate once, then distribute by restoring the changed register. Inputs must be restored; the computed function cannot use its output as scratch. | Native Fourier frame contacts still need payment. Our exact commuting-ADD folding removes 108 scalar records in each orientation but leaves the recursive profile unchanged, even after retiming. This is not the κ improvement. A multi-target native interface remains a useful larger direction. | +| [Brislawn, Causal Complementation, §§2.2–2.4](https://arxiv.org/html/2408.07970v1) | Couple elimination to divisibility and causal availability rather than use an arbitrary inverse. | The paper works with causal polynomial filter matrices; our controller has several independent Laurent variables and restricted dyadic/native contacts. No direct factorization theorem applies. It suggested checking the actual subspace lattice instead of the old finite frame menu. The accepted three-dimensional contact is proved separately by native replay and Clifford decoding. | +| [Urschel, block unitriangular representations, Lemma 5](https://arxiv.org/html/2305.00485v2) | Short alternating block shears can represent a general special-linear operator. | Its construction uses inverses over a field. Neither dyadic coefficients nor cheap native block operators follow from the six-factor count. Deferred until an explicit small legal block factorization replaces paid work. | +| [Buhrman–Cleve–Koucký–Loff–Speelman, catalytic space](https://eccc.weizmann.ac.il/report/2014/053/) | Arbitrary initial workspace must return exactly. | Tested a joint-boundary move allowing helpers to become zero-width catalysts and removing their productive credit. No improving move was found in the declared single-label experiment. The accepted move keeps all helpers productive. No catalytic-space upper bound is transferred. | +| [Robere–Zuiddam, amortized/catalytic circuits](https://eccc.weizmann.ac.il/report/2021/035/) | Optimize the cost against the complete resource ledger. | Repeated copies of one function on one input do not supply independent productive fields. Retained as a discipline for the objective, not a source of output credit. | + +The useful change of direction was to leave the exhausted p7 idle-mask model, +read the newly published #4440/#4441 constructions, and search new subspaces +of their actual native word. This produces a changed paid profile. No claim +is made that any cited author supplied this contact or the new κ. + +## Bounded discovery and limitations + +Before the new upstream sources appeared, bidirectional coordinate retiming, +75 commuting-ADD combinations (108 removed records), and 1,320 paired +same/complement rank-one idle-projector experiments found no paid improvement. +Those are local-only exploratory results; they are not global barriers. + +Starting from #4441's exact native patch, the optional lattice optimizer tries +joining frames with each binary line and intersecting them with each binary +hyperplane, with paired helper-boundary decisions and exact nesting checks. +At the discovery exponent 1−0.00300106 it finds one move: intersect frame 732 +with the hyperplane orthogonal to binary vector 2, at phase B scalar 480. +Its floating objective is only a ranking aid. `verify.py` does not run a +solver or trust the objective; it executes the explicit PATCH.json. + +Subsequent exploratory expansion over 111,887 distinct old/new candidate +spaces, and the same expansion after scalar folding, found no additional +improving single-label move in that particular program. Simultaneous +multiple-label moves, changed scalar graphs and other providers remain open. +No global or exact search-optimality claim is made. + +Apache-2.0 for these notes. Papers retain their own copyrights and licenses. + +Submission refresh: concurrent [PR4447](https://github.com/CrocSwap/integer-mult-bounds/pull/4447) +reports the same contact and profile. This separate discovery and replay is +retained with the smaller charged templates; no novelty claim is made. diff --git a/research/native-lattice-retiming/NATIVE-RESULT.json b/research/native-lattice-retiming/NATIVE-RESULT.json new file mode 100644 index 0000000000..b5c0af78f1 --- /dev/null +++ b/research/native-lattice-retiming/NATIVE-RESULT.json @@ -0,0 +1,816 @@ +{ + "controls": { + "global_phase_only_corruption_rejected": true, + "wrong_scalar_frame_rejected": true + }, + "helpers": { + "4": 26, + "5": 2, + "7": 29, + "8": 42, + "9": 309 + }, + "native": { + "backward": { + "arbitrary_owned_C0_cleared": true, + "independent_interpreter": { + "all_scalar_frames_checked": true, + "clean_J": false, + "conservative_real_scalar_primitive_allowance": 158168, + "direction": "backward", + "dyadic_coefficients_and_unit_scales_checked": true, + "event_counts": { + "adapter": 448, + "center": 8, + "climb": 3355, + "phase": 10, + "scalar": 17453, + "warp": 240 + }, + "expected_restored_arbitrary_cleanup_buffers": 0, + "expected_restored_helpers": 408, + "explicitly_owned_C_fields_cleared": 1, + "free_warp_operator_endpoint_matches": true, + "independent_borrowed_input_fields": 632, + "mismatch_examples": [], + "negative_control_omitted_last_cleanup_scalar": false, + "original_data_fields": 224, + "paid_profile": { + "1": 2254, + "2": 514, + "3": 444, + "4": 103, + "5": 40, + "8": 8 + }, + "paid_rank_mass": 5290 + }, + "independent_owned_entry_columns": 1, + "independent_persistent_columns": 632, + "l1_witness": { + "event": 6396, + "role": [ + "L", + 225 + ] + }, + "max_denominator": 64, + "max_formal_prefix_l1": "169", + "paid_profile": { + "1": 2254, + "2": 514, + "3": 444, + "4": 103, + "5": 40, + "8": 8 + }, + "paid_rank_mass": 5290, + "real_scalar_allowance": 158168, + "scalar_frames_checked": true + }, + "forward": { + "arbitrary_owned_C0_cleared": true, + "independent_interpreter": { + "all_scalar_frames_checked": true, + "clean_J": false, + "conservative_real_scalar_primitive_allowance": 158120, + "direction": "forward", + "dyadic_coefficients_and_unit_scales_checked": true, + "event_counts": { + "adapter": 448, + "center": 8, + "climb": 3355, + "phase": 10, + "scalar": 17453, + "warp": 240 + }, + "expected_restored_arbitrary_cleanup_buffers": 0, + "expected_restored_helpers": 408, + "explicitly_owned_C_fields_cleared": 1, + "free_warp_operator_endpoint_matches": true, + "independent_borrowed_input_fields": 632, + "mismatch_examples": [], + "negative_control_omitted_last_cleanup_scalar": false, + "original_data_fields": 224, + "paid_profile": { + "1": 2254, + "2": 514, + "3": 444, + "4": 103, + "5": 40, + "8": 8 + }, + "paid_rank_mass": 5290 + }, + "independent_owned_entry_columns": 1, + "independent_persistent_columns": 632, + "l1_witness": { + "event": 19099, + "role": [ + "L", + 224 + ] + }, + "max_denominator": 32, + "max_formal_prefix_l1": "457", + "paid_profile": { + "1": 2254, + "2": 514, + "3": 444, + "4": 103, + "5": 40, + "8": 8 + }, + "paid_rank_mass": 5290, + "real_scalar_allowance": 158120, + "scalar_frames_checked": true + } + }, + "new_physical_edges": [ + { + "new_basis": [ + 45, + 133, + 336 + ], + "old_basis": [ + 133, + 45 + ], + "recipes": { + "backward": { + "left": { + "linear_Z4": [ + 2, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "matrix_rows": [ + 2, + 4, + 8, + 16, + 33, + 64, + 129, + 256, + 1 + ], + "offset": 0, + "phase": 0, + "quadratic_rows": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ] + }, + "rank": 1, + "right": { + "linear_Z4": [ + 0, + 0, + 0, + 0, + 1, + 0, + 1, + 0, + 2 + ], + "matrix_rows": [ + 336, + 1, + 2, + 4, + 8, + 272, + 32, + 320, + 128 + ], + "offset": 0, + "phase": 3, + "quadratic_rows": [ + 0, + 0, + 0, + 0, + 80, + 0, + 80, + 0, + 0 + ] + } + }, + "forward": { + "left": { + "linear_Z4": [ + 2, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "matrix_rows": [ + 2, + 4, + 8, + 16, + 33, + 64, + 129, + 256, + 1 + ], + "offset": 0, + "phase": 0, + "quadratic_rows": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ] + }, + "rank": 1, + "right": { + "linear_Z4": [ + 0, + 0, + 0, + 0, + 3, + 0, + 3, + 0, + 2 + ], + "matrix_rows": [ + 336, + 1, + 2, + 4, + 8, + 272, + 32, + 320, + 128 + ], + "offset": 1, + "phase": 1, + "quadratic_rows": [ + 0, + 0, + 0, + 0, + 80, + 0, + 80, + 0, + 0 + ] + } + } + } + }, + { + "new_basis": [ + 45, + 133, + 336 + ], + "old_basis": [ + 336, + 45 + ], + "recipes": { + "backward": { + "left": { + "linear_Z4": [ + 2, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "matrix_rows": [ + 3, + 4, + 9, + 16, + 32, + 64, + 128, + 1, + 256 + ], + "offset": 0, + "phase": 0, + "quadratic_rows": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ] + }, + "rank": 1, + "right": { + "linear_Z4": [ + 1, + 0, + 1, + 0, + 0, + 0, + 0, + 2, + 0 + ], + "matrix_rows": [ + 133, + 129, + 2, + 132, + 8, + 16, + 32, + 64, + 256 + ], + "offset": 0, + "phase": 3, + "quadratic_rows": [ + 5, + 0, + 5, + 0, + 0, + 0, + 0, + 0, + 0 + ] + } + }, + "forward": { + "left": { + "linear_Z4": [ + 2, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "matrix_rows": [ + 3, + 4, + 9, + 16, + 32, + 64, + 128, + 1, + 256 + ], + "offset": 0, + "phase": 0, + "quadratic_rows": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ] + }, + "rank": 1, + "right": { + "linear_Z4": [ + 3, + 0, + 3, + 0, + 0, + 0, + 0, + 2, + 0 + ], + "matrix_rows": [ + 133, + 129, + 2, + 132, + 8, + 16, + 32, + 64, + 256 + ], + "offset": 1, + "phase": 1, + "quadratic_rows": [ + 5, + 0, + 5, + 0, + 0, + 0, + 0, + 0, + 0 + ] + } + } + } + }, + { + "new_basis": [ + 258, + 128, + 64, + 33, + 18, + 9, + 5 + ], + "old_basis": [ + 45, + 133, + 336 + ], + "recipes": { + "backward": { + "left": { + "linear_Z4": [ + 2, + 3, + 2, + 2, + 0, + 0, + 0, + 0, + 0 + ], + "matrix_rows": [ + 16, + 40, + 69, + 129, + 258, + 4, + 8, + 5, + 10 + ], + "offset": 0, + "phase": 0, + "quadratic_rows": [ + 0, + 10, + 0, + 2, + 0, + 0, + 0, + 0, + 0 + ] + }, + "rank": 4, + "right": { + "linear_Z4": [ + 2, + 3, + 0, + 3, + 2, + 0, + 2, + 2, + 1 + ], + "matrix_rows": [ + 172, + 16, + 36, + 338, + 13, + 18, + 128, + 160, + 256 + ], + "offset": 438, + "phase": 2, + "quadratic_rows": [ + 12, + 322, + 1, + 9, + 64, + 0, + 274, + 0, + 322 + ] + } + }, + "forward": { + "left": { + "linear_Z4": [ + 2, + 3, + 2, + 2, + 0, + 0, + 0, + 0, + 0 + ], + "matrix_rows": [ + 16, + 40, + 69, + 129, + 258, + 4, + 8, + 5, + 10 + ], + "offset": 0, + "phase": 0, + "quadratic_rows": [ + 0, + 10, + 0, + 2, + 0, + 0, + 0, + 0, + 0 + ] + }, + "rank": 4, + "right": { + "linear_Z4": [ + 2, + 1, + 0, + 1, + 0, + 0, + 2, + 2, + 3 + ], + "matrix_rows": [ + 172, + 16, + 36, + 338, + 13, + 18, + 128, + 160, + 256 + ], + "offset": 443, + "phase": 3, + "quadratic_rows": [ + 12, + 322, + 1, + 9, + 64, + 0, + 274, + 0, + 322 + ] + } + } + } + }, + { + "new_basis": [ + 258, + 133, + 66, + 45, + 16 + ], + "old_basis": [ + 45, + 133, + 336 + ], + "recipes": { + "backward": { + "left": { + "linear_Z4": [ + 3, + 2, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "matrix_rows": [ + 4, + 10, + 16, + 32, + 66, + 128, + 1, + 256, + 3 + ], + "offset": 0, + "phase": 0, + "quadratic_rows": [ + 3, + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ] + }, + "rank": 2, + "right": { + "linear_Z4": [ + 0, + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 3 + ], + "matrix_rows": [ + 320, + 338, + 1, + 322, + 4, + 8, + 256, + 32, + 128 + ], + "offset": 64, + "phase": 3, + "quadratic_rows": [ + 0, + 18, + 0, + 0, + 66, + 0, + 272, + 0, + 320 + ] + } + }, + "forward": { + "left": { + "linear_Z4": [ + 3, + 2, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "matrix_rows": [ + 4, + 10, + 16, + 32, + 66, + 128, + 1, + 256, + 3 + ], + "offset": 0, + "phase": 0, + "quadratic_rows": [ + 3, + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ] + }, + "rank": 2, + "right": { + "linear_Z4": [ + 0, + 3, + 0, + 0, + 0, + 0, + 2, + 0, + 3 + ], + "matrix_rows": [ + 320, + 338, + 1, + 322, + 4, + 8, + 256, + 32, + 128 + ], + "offset": 66, + "phase": 0, + "quadratic_rows": [ + 0, + 18, + 0, + 0, + 66, + 0, + 272, + 0, + 320 + ] + } + } + } + } + ], + "paid": { + "1": 2254, + "2": 514, + "3": 444, + "4": 103, + "5": 40, + "8": 8 + }, + "status": "PASS_NEW_LATTICE_CONTACT_BOTH_ORIENTATIONS_ALL_COLUMNS" +} diff --git a/research/native-lattice-retiming/NOTICE.md b/research/native-lattice-retiming/NOTICE.md new file mode 100644 index 0000000000..e7add6c881 --- /dev/null +++ b/research/native-lattice-retiming/NOTICE.md @@ -0,0 +1,16 @@ +# Attribution + +New work prepared for zxv with substantial OpenAI Codex assistance; Apache-2.0. +No subagents were used. Source files remain unchanged in their existing paths. + +The native supplier, reconstruction, arbitrary-input interpreters, complex +controller, higher-moment strictification and logarithmic compiler retain zxv's +PR4359/PR4433 lineage. Fresh-helper boundary retiming is Cinna Davis's PR4441; +query thinning and the stronger BIT interface are Cinna Davis's PR4440. +Mixed-target integer flow is Jacob Alan Sussman's Theorem 1G. The retained +native/Clifford/BIT sources preserve their original contributor notices, +including DreamingOfClouds, eumemic and their predecessor contributions. + +The optional min-cut discovery code adapts PR4441's Apache-2.0 floating Dinic +implementation. Its new moves act on the subspace lattice. The mathematical +claim depends on the explicit exact contact, not the optimizer. diff --git a/research/native-lattice-retiming/PATCH.json b/research/native-lattice-retiming/PATCH.json new file mode 100644 index 0000000000..be818ab439 --- /dev/null +++ b/research/native-lattice-retiming/PATCH.json @@ -0,0 +1,8 @@ +{ + "phase": "B", + "scalar_ordinal": 480, + "old_frame": 732, + "old_basis": [258, 133, 82, 45], + "new_basis": [45, 133, 336], + "forward_gate": ["add", ["L", 90], ["L", 253], 1, 1] +} diff --git a/research/native-lattice-retiming/PROOF.md b/research/native-lattice-retiming/PROOF.md new file mode 100644 index 0000000000..5ed2cacea7 --- /dev/null +++ b/research/native-lattice-retiming/PROOF.md @@ -0,0 +1,96 @@ +# Native contact and conditional transfer + +## Scope and source boundary + +Source PR4441 is fixed at `5f9d871c6bd1b9e34db5a7ea5ef08a908e94db39`, +including PR4440 at `40e22a83ed660d3d6074c4f2dbf14bfb621eee51`. +Their conditional contracts are retained. No selected result, independent +scientific acceptance or universal implementation hypothesis is promoted. +The exact byte closure is SOURCES.json. The user authorized submission after review. + +## One legal contact outside the predecessor frame menu + +Use PR4441's chronological word and all its boundary changes. A field with +logical value z and frame S holds C_S z. A paid nested transport from S to T +implements C_T C_S^-1, retaining z. At a common frame T an ADD is +C_T z_i + a C_T z_j = C_T(z_i + a z_j). Thus changing common frames while +keeping every contact legal preserves the entire formal logical program. +This is an induction over the actual instruction sequence, not a tensor power +of an equality between sums of matrices. + +The source forward ADD at phase B, persistent ordinal 480, is +`L90 += L253`. Its old frame is span(258,133,82,45). Set +S=span(45,133,336), the intersection with the hyperplane perpendicular to 2. +The generator checks strict inclusion. Both previous contacts lie in S; +both following contacts contain S. Resynthesis therefore uses only ascending +nested transports. All warp and owned-center contacts keep their actual +original gauges. The backward ADD is matched to the literal source dual, +then receives the same common frame. + +Two source interpreters execute both new words on 632 arbitrary persistent +input columns, plus an arbitrary owned-center entry column. The main shears +and all autonomous helper rows match exactly; C0 is cleared only at its legal +owned operations. Main and helper boundaries are unchanged from PR4441. +Four newly used edge types receive complete forward and conjugate Clifford +recipes; serialized decoding checks tableau and exact zero-state phase. +The old edges and unchanged helper normalizers retain their pinned evidence. +Wrong-contact and phase-only corruptions are rejected. + +At every permitted positive column multiplicity the same formal gauge +induction applies to the allowed generator lifts. This uses the retained +all-column/native contract, including the new fixed Clifford monomial +recipes. The finite checks do not independently prove that universal +implementation or the physical tape model. + +## Why the invoice improves + +The complete local change is + + P_new = P_old + [1] + [4] - [2] - [3]. + +No target, field count, scalar coefficient/order, query or center is removed. +For 0theta^p and 153^(v*C)<2^p. These are the exit/contraction +and initial-range conditions of PR4433's generalized majorant. With +kappa=.00300120 and d=(C-kappa)/7=1/350000000, the verifier finds +H=2299850000000 with (H+1)^160<2^(d*H). The previous grid value fails. +The same construction at kappa=.00300105 gives H=249900000000. + +Every expanded program is finite. Its complete raw nonrecursive record bound +is below 10^9, and the source explicit product, adapter, precision and stock +prescriptions apply to these new finite ranks and lists. Suspended instances +retain distinct center storage; no materialized gigantic program is claimed. +The BIT supplier remains the source stronger ordinary admission .0034 with +atom .004. Exact outer arithmetic passes all nine rows, 54 current predicates, +four guards and 63 legacy predicates at the new point. The same-kappa rank +comparison separately checks the complete current outer ledger. + +The conclusion is conditional on the retained native/all-column, +whole-job/owned-erasure, finite-precision, analytic, physical tape, prime and +exact-recovery contracts: T(n)=O(n*(log n)^(1-.00300120)). It is not an +unconditional theorem, formal proof or practical runtime claim. diff --git a/research/native-lattice-retiming/README.md b/research/native-lattice-retiming/README.md new file mode 100644 index 0000000000..22cb2378ee --- /dev/null +++ b/research/native-lattice-retiming/README.md @@ -0,0 +1,137 @@ +# Conditional κ = 0.00300120 (71.9× smaller uniform-rank exponent) + +**Submission authorized by the user after review on 21 October 2026.** + +A changed native paid profile raises the conditional multiplication saving to +**κ = 0.00300120** and specifies sufficient uniform rank +**`2^2299850000000`**. The κ gain over +[PR4441](https://github.com/CrocSwap/integer-mult-bounds/pull/4441) is modest: +`0.00000015` (about 0.005%). The exponent of its sufficient uniform rank falls +by **71.88×**. At PR4441's unchanged κ=0.00300105, the rank can instead be +**`2^249900000000`**, a **661.53×** exponent reduction. +These are sufficient mathematical template sizes, not practical speedups. + +The submission refresh found concurrent [PR4447](https://github.com/CrocSwap/integer-mult-bounds/pull/4447), +which uses the same B/480 contact and paid profile and declares κ=0.00300123. +This contribution retains the reviewed κ=0.00300120 and supplies the smaller +paid-tail and uniform-template bounds above, with a separate discovery path. +No unique-discovery or strongest-κ claim is made. + +This builds on my selected [0.0023 construction](../kappa-0023-productive-jobs/README.md), +my [higher-moment/logarithmic compiler](../higher-moment-strictification/README.md), +and Cinna Davis's new query-thinning and fresh-helper constructions +([PR4440](https://github.com/CrocSwap/integer-mult-bounds/pull/4440), +[PR4441](https://github.com/CrocSwap/integer-mult-bounds/pull/4441)). +Both pending source heads are pinned; they are author-checked conditional +claims, not independently accepted frontier updates. The selected record stays +0.0023. The new work retains their native/all-column, owned-erasure, whole-job, +precision, analytic, fixed-tape, prime and exact-recovery premises. + +## The actual construction change + +At phase B, persistent scalar ordinal 480, the forward ADD is +`L90 += L253`. Its old common frame has basis `[258,133,82,45]`. +Replace it by the three-dimensional subspace with basis `[45,133,336]`. +It is the old space intersected with the hyperplane orthogonal to binary +vector 2. Apply the same frame change at the literal inverse-transpose ADD in +the backward word. Scalar order, coefficients, warp contacts, main boundaries, +helper boundaries and all eight complete centers remain those of PR4441. + +Direct ascending transports before and after the changed contact give: + +| Local resource | PR4441 | New word | +| --- | ---: | ---: | +| Paid rank 1 | 2253 | 2254 | +| Paid rank 2 | 515 | 514 | +| Paid rank 3 | 445 | 444 | +| Paid rank 4 | 102 | 103 | +| Paid rank 5 / rank 8 | 40 / 8 | 40 / 8 | +| Productive helper widths | 26×4, 2×5, 29×7, 42×8, 309×9 | same | + +Thus the net paid change is `H2+H3 → H1+H4`. For every real `0 2^26*N^5 avoiding all fixed denominators and rank witnesses" + }, + "outer": { + "functional_checks": { + "actual_new_BIT_stock_sublinear": "87149999253/87500000000", + "fixed_halo_explicit_metadata_branch": "6737500001/87500000", + "new_BIT_row_stock_sublinear_in_active_group": "348949997009/350000000000", + "new_semantic_group_guard": "3/350000000" + }, + "margins": { + "boundary_algebraic_matrix": "367648398949577/122500000000000000", + "fused_gaussian": "367648396848731/122500000000000000", + "global_coordinate_router": "131303/43750000", + "group_bit_router": "45956093356091/15312500000000000", + "group_scans": "174999999/175000000", + "main_transform": "367648048949577/122500000000000000", + "microbox_face_corrections": "6737500001/87500000", + "polynomial_products": "349999999/350000000", + "sparse_union_movement": "50133273398949577/122500000000000000" + }, + "parameters": { + "a": "131303/43750000", + "b": "42017/14000000", + "beta": "349999997/350000000", + "bit_saving": "17/5000", + "cap_xi": "111383273048949577/122500000000000000", + "complex_uniform_saving": "525213/175000000", + "d": "1/350000000", + "epsilon": "349999999/350000000", + "kappa": "7503/2500000", + "lambda_": "99699879/100000000", + "lambda_prime": "348949577/350000000", + "layout": "1/350000000", + "q": "1050423/350000000", + "r0": "1/3500000000", + "stop": "1/350000000", + "tested_saving": "150061/50000000" + }, + "strict_checks": { + "actual_bit_above_effective": "17447/43750000", + "actual_logarithmic_gamma_guard": "1/350000000", + "actual_logarithmic_group_guard": "11116727476050423/61250000000000000", + "alpha_logarithm_absorption": "1/3500000000", + "boundary_algebraic_matrix_above_kappa": "1398949577/122500000000000000", + "cap_above_band": "50133273048949577/122500000000000000", + "cap_below_cell": "11116726601050423/122500000000000000", + "cap_below_phase_cell_power": "133616726951050423/122500000000000000", + "complex_above_effective": "1/350000000", + "complex_below_one_over_32": "395483/14000000", + "complex_endpoint": "1/175000000", + "epsilon_below_one": "1/350000000", + "epsilon_positive": "349999999/350000000", + "fine_prime_halo_umbrella": "7/2", + "fused_gaussian_above_kappa": "1396848731/122500000000000000", + "gaussian_above_main": "173949577/61250000000000000", + "global_coordinate_router_above_kappa": "1/87500000", + "global_gamma_power_slack": "9/3500000000", + "group_below_dimension": "1/175000000", + "group_bit_router_above_kappa": "218356091/15312500000000000", + "group_gauge_power_slack": "11116727458550423/61250000000000000", + "group_key_fits_record": "1/175000000", + "group_positive": "349999997/350000000", + "group_scans_above_kappa": "174474789/175000000", + "halo_covers_generic_inverse_radius": "5", + "improvement_over_user_baseline": "635114790400418148631/500000000000000000000000", + "lambda_above_internal": "1/700000000", + "lambda_above_sigma": "3/700000000", + "lambda_above_tau": "1/700000000", + "lambda_prime_above_lambda": "1/700000000", + "lambda_prime_above_leaf": "27957983/4900000000000000", + "leaf_saving_above_effective": "13957983/4900000000000000", + "main_transform_above_kappa": "1048949577/122500000000000000", + "membership_arithmetic_fits_record": "1/350000000", + "microbox_face_corrections_above_kappa": "1684309349/21875000", + "microbox_halo_volume": "27650000003/350000000", + "new_complex_uniform_saving_above_b": "1/350000000", + "new_semantic_guard_with_C1_one": "1/350000000", + "polynomial_products_above_kappa": "348949579/350000000", + "positive_layout_slack": "1/350000000", + "q_below_effective": "1/350000000", + "q_below_internal": "1/350000000", + "q_below_leaf": "27957983/4900000000000000", + "q_positive": "1050423/350000000", + "short_record_fallback": "13957983/14000000", + "source_axis_superpolynomial": "1/350000000", + "sparse_union_movement_above_kappa": "49765626398949577/122500000000000000", + "stop_below_one": "349999999/350000000", + "stop_positive": "1/350000000", + "strassen_integer_power_gap": "1951441519231", + "support_router_span": "3/350000000", + "theta_positive_polynomial_power": "2", + "union_header_fits_record": "3/350000000", + "union_tag_work_per_visit_fits_record": "3/350000000" + } + }, + "paid": { + "1": 44618, + "16": 448, + "2": 9766, + "24": 448, + "3": 8436, + "32": 448, + "4": 1957, + "40": 448, + "48": 448, + "5": 760, + "56": 448, + "64": 448, + "72": 448, + "8": 152 + }, + "rank_exponent_reduction": "472330/6571", + "rank_surplus": 800, + "raw_moment_margin": { + "lower": "0.005035901012260126500228750242", + "upper": "0.005035901012260126500228750243" + }, + "raw_root": [ + "3001239017/1000000000000", + "30012390173/10000000000000" + ], + "raw_root_scope": "Unique crossing on [0,.01]; no universal or global mechanism ceiling.", + "same_kappa_rank_exponent_reduction": "236165/357", + "same_predecessor_kappa_compiler": { + "H": 249900000000, + "N": "2^249900000000", + "eta": { + "lower": "0.000037402048244786272108248731", + "upper": "0.000037402048244786272108248732" + }, + "gap": "17/700000000", + "integer_exponent": 6069, + "logarithm_power": 160, + "theta": "15/16", + "uniform_saving": "2100837/700000000", + "word_materialized": false + }, + "same_predecessor_kappa_outer": { + "functional_checks": { + "actual_new_BIT_stock_sublinear": "174299987301/175000000000", + "fixed_halo_explicit_metadata_branch": "13475000017/175000000", + "new_BIT_row_stock_sublinear_in_active_group": "697899949153/700000000000", + "new_semantic_group_guard": "51/700000000" + }, + "margins": { + "boundary_algebraic_matrix": "735281032143319/245000000000000000", + "fused_gaussian": "735280996429957/245000000000000000", + "global_coordinate_router": "2100803/700000000", + "group_bit_router": "1470573892859047/490000000000000000", + "group_scans": "349999983/350000000", + "main_transform": "735275082143319/245000000000000000", + "microbox_face_corrections": "13475000017/175000000", + "polynomial_products": "699999983/700000000", + "sparse_union_movement": "100266531032143319/245000000000000000" + }, + "parameters": { + "a": "2100803/700000000", + "b": "105041/35000000", + "beta": "699999949/700000000", + "bit_saving": "17/5000", + "cap_xi": "222766525082143319/245000000000000000", + "complex_uniform_saving": "2100837/700000000", + "d": "17/700000000", + "epsilon": "699999983/700000000", + "kappa": "60021/20000000", + "lambda_": "199399773/200000000", + "lambda_prime": "348949607/350000000", + "layout": "17/700000000", + "q": "1050393/350000000", + "r0": "17/7000000000", + "stop": "17/700000000", + "tested_saving": "150061/50000000" + }, + "strict_checks": { + "actual_bit_above_effective": "279197/700000000", + "actual_logarithmic_gamma_guard": "17/700000000", + "actual_logarithmic_group_guard": "22233483842856681/122500000000000000", + "alpha_logarithm_absorption": "17/7000000000", + "boundary_algebraic_matrix_above_kappa": "23782143319/245000000000000000", + "cap_above_band": "100266525082143319/245000000000000000", + "cap_below_cell": "22233468967856681/245000000000000000", + "cap_below_phase_cell_power": "267233474917856681/245000000000000000", + "complex_above_effective": "17/700000000", + "complex_below_one_over_32": "988709/35000000", + "complex_endpoint": "17/350000000", + "epsilon_below_one": "17/700000000", + "epsilon_positive": "699999983/700000000", + "fine_prime_halo_umbrella": "7/2", + "fused_gaussian_above_kappa": "23746429957/245000000000000000", + "gaussian_above_main": "2957143319/122500000000000000", + "global_coordinate_router_above_kappa": "17/175000000", + "global_gamma_power_slack": "153/7000000000", + "group_below_dimension": "17/350000000", + "group_bit_router_above_kappa": "59392859047/490000000000000000", + "group_gauge_power_slack": "22233483545356681/122500000000000000", + "group_key_fits_record": "17/350000000", + "group_positive": "699999949/700000000", + "group_scans_above_kappa": "697899231/700000000", + "halo_covers_generic_inverse_radius": "5", + "improvement_over_user_baseline": "635039790400418148631/500000000000000000000000", + "lambda_above_internal": "17/1400000000", + "lambda_above_sigma": "51/1400000000", + "lambda_above_tau": "17/1400000000", + "lambda_prime_above_lambda": "17/1400000000", + "lambda_prime_above_leaf": "1188214303/24500000000000000", + "leaf_saving_above_effective": "593214303/24500000000000000", + "main_transform_above_kappa": "17832143319/245000000000000000", + "membership_arithmetic_fits_record": "17/700000000", + "microbox_face_corrections_above_kappa": "53897899333/700000000", + "microbox_halo_volume": "55300000051/700000000", + "new_complex_uniform_saving_above_b": "17/700000000", + "new_semantic_guard_with_C1_one": "17/700000000", + "polynomial_products_above_kappa": "43618703/43750000", + "positive_layout_slack": "17/700000000", + "q_below_effective": "17/700000000", + "q_below_internal": "17/700000000", + "q_below_leaf": "1188214303/24500000000000000", + "q_positive": "1050393/350000000", + "short_record_fallback": "34894959/35000000", + "source_axis_superpolynomial": "17/700000000", + "sparse_union_movement_above_kappa": "99531273782143319/245000000000000000", + "stop_below_one": "699999983/700000000", + "stop_positive": "17/700000000", + "strassen_integer_power_gap": "1951441519231", + "support_router_span": "51/700000000", + "theta_positive_polynomial_power": "2", + "union_header_fits_record": "51/700000000", + "union_tag_work_per_visit_fits_record": "51/700000000" + } + }, + "status": "PASS_CONDITIONAL_NEW_NATIVE_PROFILE_KAPPA", + "strictification": { + "alpha": { + "lower": "0.999999980480394484617151340349", + "upper": "0.999999980480394484617151340350" + }, + "cutoff": 18, + "delta": { + "lower": "0.977253011855658562221385892786", + "upper": "0.977253011855658562221385892787" + }, + "floor": 22, + "gamma": { + "lower": "0.981971726999571315878434078558", + "upper": "0.981971726999571315878434078559" + }, + "limits": [ + "999999981/1000000000", + "491/500", + "391/400" + ], + "normalized_paid_upper": "3135316342855047938216186285366284791836015552731567401908176734930110521667998541808860782674464246329116429895882753096247698522148271859666641784228677573912605332725923383934714825294597676931624212032514027646967981541336965729076185554268027233444327337403745878243356820959932112007771549864881590155015123496432209395021364448015796884438028569244657405717369951884743365972882095120039957983925379611291360772632665217708326491914268771819562848029846703500646180491671401882021101698766069617361586201262698776684351995258277190425359783195465694122176833672706484066530574724789787037479061017911116773108073612235843989560762616998581715509178001466468362876164703345435291409263816689904692103757941883488341058980494142712686923568812288022949192890478433946276536436589153790091599648369106702773634555281575360964032314712840386529515907102227717937795524446796747828703981436724132739380841411013441416769926025052267538328282156106210906013225055943965375562532068983730967116286827198591247798727678176171320478590738500846420117865786648859883120410371898612074031256962522241496076154923725770848767431043120528509433496714324101025959590085951574021714319434271053115042416232189788263853499205089931368330261666401396910361932147924932944049888383159214229752743917428741596819317242725132712760528603789131532630741472925548561970849762668570817110437699349242714467130025311116618881358860815044369352216933087978747203390374142945600672289781753394274808328461504479642084553107824308868694078844054600750174201186469373656303128692027810576278159672148330996943494335356428296005636709069876376626933852810296702680886721507369314046399539101605976615201231427346183584818214127701391923728250913847612146632050052126755457091296857078080483746571485029373221974027408859524785238239130664547070069062887791736006969711830300497542975648628304802085160737580120878371177685768802133093055833042983690068619665100866536539147891836775462897136439867703923989275080988185809322290236782727815805504224638071293970925407386829055785555936017618119880456302458931410718717523322804435169311032474465174265268263099422925367321268723174472263506975656429644591851528543559670335484908199131423006788263629803652987/3135325528854913035113346724853144051552102259356465975465195756269284493200158883437639560729811317502778741665335773348010541036368854326255535712764450586037113873286263239677927235348235120600546751065096192000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + "power": 675, + "tested": "150061/50000000", + "u": "3/25" + }, + "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/native-lattice-retiming/SOURCES.json b/research/native-lattice-retiming/SOURCES.json new file mode 100644 index 0000000000..5dc627b3b2 --- /dev/null +++ b/research/native-lattice-retiming/SOURCES.json @@ -0,0 +1,282 @@ +{ + "base_commit": "5f9d871c6bd1b9e34db5a7ea5ef08a908e94db39", + "files": [ + { + "git_blob": "686c36fb19680db327f797ebdfe612487d8c53f8", + "path": "research/fresh-helper-boundary/ARITHMETIC-RESULT.json", + "sha256": "5d25fec9ac4b036c93846a50dccfa4af030e2982f5cec02e28702193bf157cf7", + "usage": "input" + }, + { + "git_blob": "45744fedd0e28967aa72586048b8bc0c72f419a9", + "path": "research/fresh-helper-boundary/CHANGES.json", + "sha256": "cde73b8ff5b3c0d06e69e2293b991b24fd14a16dd4ccab7ff6b3439074a94624", + "usage": "input" + }, + { + "git_blob": "e6fdb31624e4eb8c7c770bb4422cd07ea99ab152", + "path": "research/fresh-helper-boundary/NATIVE-RESULT.json.gz", + "sha256": "37d0848458b289eb50271c47adef6e74014ae30be6363d09394b2337b566b839", + "usage": "input" + }, + { + "git_blob": "e26608e20be115d28f8853a8c1a12bebfc8e8ec3", + "path": "research/fresh-helper-boundary/RESULT.json", + "sha256": "34163eeeef1cd712de457d7fd3b0435f98a12ac456b82256b078f33225456fbd", + "usage": "input" + }, + { + "git_blob": "0b40275502f4263a19905f4fb50e346a3629c712", + "path": "research/fresh-helper-boundary/SOURCES.json", + "sha256": "01998e9b86222d10811fc0114dcd5c946ff9e95025a7cacd00e67a3eefe543d0", + "usage": "input" + }, + { + "git_blob": "4822f04ae09d84a16e8fa8656a533e23fd4068f0", + "path": "research/fresh-helper-boundary/arithmetic.py", + "sha256": "212bae96d0ddcbc25076afe2589a47736c66b77420057f28c44c937ad087fc07", + "usage": "input" + }, + { + "git_blob": "1b36f6cb5f205c33bf48811e0b1b3621c55e8154", + "path": "research/fresh-helper-boundary/native.py", + "sha256": "9b55a2d3c3972148fae9d112e745d9244968166bd89bd900c938f429fc76ab29", + "usage": "input" + }, + { + "git_blob": "e434dbf7c68afa0390a307fd15f32348b0e87207", + "path": "research/fresh-helper-boundary/verify.py", + "sha256": "4c18851214400cf955e10565d89357029d9e765140233831472ce23f0c3ee7bf", + "usage": "input" + }, + { + "git_blob": "e223acd07a6b1f4f1c9f2778b8ea64d4b7a2be55", + "path": "research/fresh-helper-thinned/RESULT.json", + "sha256": "8e7db2fed5f4be6a7f944bc59e7942ccbcc3e6c36130b5671331540c183ada21", + "usage": "input" + }, + { + "git_blob": "0a736ca89e1eafb73a30e1f2589cc45e6b5f76c3", + "path": "research/higher-moment-strictification/README.md", + "sha256": "ebe80b68ff026ce90f71f274c31744f4c0b36132d15ebb7e39cf2d5df4df270d", + "usage": "input" + }, + { + "git_blob": "d3b6149c5c1cca84c7c305f6e2e32c814e30777e", + "path": "research/higher-moment-strictification/vendor/check_ledger.py", + "sha256": "1dd56009986eb14dd6603c9193c7ad71dd45c7d005bf71c9cd3f916e66f54d98", + "usage": "input" + }, + { + "git_blob": "4b24a5096154736ce060474eb8c72dc64c303699", + "path": "research/higher-moment-strictification/verify.py", + "sha256": "0ce7e7137422d5ffeda22085c81fa88471bbe963100fdad62e659f1e3bf89326", + "usage": "input" + }, + { + "git_blob": "8b40135a84e7f0f0cd44bed69655801310b916a7", + "path": "research/kappa-0023-productive-jobs/dependencies/kappa-next-regime/bit-compression/carrier-reuse/reference/joint_pair_dag.py", + "sha256": "8a0de761642d21919e969475c3f13e5d01a4bae7343c1e1f37c586d94b676a85", + "usage": "input" + }, + { + "git_blob": "d9a4f84211182ca200c081ea061d724c8a2cfb70", + "path": "research/kappa-0023-productive-jobs/dependencies/kappa-next-regime/direct-decoder/sources/DATA-PHASES.json", + "sha256": "c5916ff312678f12aba403847643fbbc29f643acec60bdf836fa56cd3e8251fa", + "usage": "input" + }, + { + "git_blob": "5a55034ec9e6185d981e16c28e1e2e455069e2cb", + "path": "research/kappa-causal-continuation/buffer-borrowing/verify_buffers.py", + "sha256": "106b4d5e052427230df452f0c901d5390a0583782960b80a8af94d9a984022c7", + "usage": "input" + }, + { + "git_blob": "8c3e11b2408fa96eefa3ebe7952d1b11b90b772b", + "path": "research/kappa-function-composition/complex/prune_native.py", + "sha256": "f2b37c183a10922eabc8e0436b426a08866430e96bd0adc7e178951c7fbb5257", + "usage": "input" + }, + { + "git_blob": "4fc05ab08138218ba9f09e5c89b649afae7c914e", + "path": "research/kappa-rebuild/architecture/mixed_target_probe.py", + "sha256": "011c3c9d0cf81103dc84d709a0e36793eb7c5ae3f23c85eac27650ef13afa04a", + "usage": "input" + }, + { + "git_blob": "fbe6da7241357d89cf5c55b2e7ce2d0d046be32a", + "path": "research/kappa-rebuild/bit/BIT-ALLSIZE-PARAMETERS.json", + "sha256": "edb273f59a27356ad89f38791590c3c806b228c3510eb508e01e89f2caba95ef", + "usage": "input" + }, + { + "git_blob": "e8c5e4f077fea0bef355e6c3013c7f252d3606cf", + "path": "research/kappa-rebuild/bit/BIT-P3-NATIVE-BINDING.json", + "sha256": "9ece46fdfda6182e757e9a3b1f513fb3d029d730f3bafdcd6ed59180a14175b0", + "usage": "input" + }, + { + "git_blob": "a58774e237c9362869a60a22bda35be09fb85872", + "path": "research/kappa-rebuild/bit/DELAYED-COVER-BRIDGE.md", + "sha256": "9731b93026717f5fa15851e3633cbb4bdc76eba2bffb9d6b4a3b69f7dd502443", + "usage": "input" + }, + { + "git_blob": "6a139eedbc1015c13df6f2a4333e1a89b5edd18d", + "path": "research/kappa-rebuild/bit/MIXED-PRODUCTIVE-BIT.json", + "sha256": "2f69a19f417c0e0d141c180f9b2fae3d358391b9a230f5848ee07c45450e70bf", + "usage": "input" + }, + { + "git_blob": "f4c4082d89969ea311219d9af8013082d599f6f1", + "path": "research/kappa-rebuild/bit/bit_native_binding.py", + "sha256": "bf6374225f388e7531fa6475cc255bd430100ff62c38d582c41601f0739de7b7", + "usage": "input" + }, + { + "git_blob": "cb0cff7c8be5f38f2ee52201d9d0907f9dfd7947", + "path": "research/kappa-rebuild/bit/complex_controller_factor.py", + "sha256": "1de9aaf918e6a4f2f5448754c1f3c3da3b85e6257849ebd097af09859c4e5497", + "usage": "input" + }, + { + "git_blob": "9c7a8bd5d3ae4c19952648c815031858d6627b96", + "path": "research/kappa-rebuild/bit/mixed_productive_bit.py", + "sha256": "b32291b0db7fc0d332ec444c70746ab0fb03351d2e50546f8bcb64060e3ff95e", + "usage": "input" + }, + { + "git_blob": "f97a23d7d21bd7f79c9d0cb14d8c6b44fddd3f23", + "path": "research/kappa-rebuild/complex/FULL-IDENTITY.md", + "sha256": "c4aa88c4943ef041e9542c519b7600ecf26ed6caff92558fdb07ac88ace64c17", + "usage": "input" + }, + { + "git_blob": "c6edcbdc43bf36bb11201235027d0ec170d07fc8", + "path": "research/kappa-rebuild/complex/full-identity-certificates/RESULT.json", + "sha256": "943d5fad2fc529f470df05a35446e07ecaef7344abfce450d2c2eb2c9b3798f6", + "usage": "input" + }, + { + "git_blob": "4a8c4ed26e53a72362d571c972e65aff546be784", + "path": "research/kappa-rebuild/complex/full-identity-certificates/THREE-base-FULL-IDENTITY-CANONICAL.json.gz", + "sha256": "6418ec3da24d548a57f5c3fe5b9062c26c9478e638504a61c387f5cfb5f4ed61", + "usage": "input" + }, + { + "git_blob": "b46d44c6ee624968dd57be928b0c15d9d45f3b2c", + "path": "research/kappa-rebuild/complex/full-identity-certificates/THREE-base-FULL-IDENTITY-NATIVE.json.gz", + "sha256": "c54b0a3e129d28e6dbf74fa731fc3bb70fe3c6705f07256750fbecddcc842d39", + "usage": "input" + }, + { + "git_blob": "7f84894efc309546a903d314c7ac1473e7f594a8", + "path": "research/kappa-rebuild/complex/native_extensions.py", + "sha256": "50ad007d9c386393657e86c99a96ae0a63a8fbc52872579b185002cc626e88e3", + "usage": "input" + }, + { + "git_blob": "a55ae0ce78a1861965f899a82604b276260f636c", + "path": "research/kappa-rebuild/complex/power_two_balance.py", + "sha256": "76929bb3887911ccf100c4593574b8a1c82ee64e96f939a8aca196869438b424", + "usage": "input" + }, + { + "git_blob": "78a7b1b0e6e43a1347fb361f45c6e0eaff8dd27b", + "path": "research/kappa-rebuild/complex/rebuild_native.py", + "sha256": "f94c527cc02215de49350d477618188c4c0da48bc8fb05b4e37b24c482cad7d5", + "usage": "input" + }, + { + "git_blob": "0f3a4067a4b4e20d0e6ca0f84f41851c5168f76d", + "path": "research/kappa-rebuild/transfer-audit/p3_native_audit.py", + "sha256": "5504a55a50546418d10c522984438cdeedb44993f7c1dab7bd4aa1ae0515d902", + "usage": "input" + }, + { + "git_blob": "04c7ef620e760cc8f1764bbf0ccd7f32c6a5bd86", + "path": "research/pr4359-p7-padding/P7-FACTOR.json", + "sha256": "6f96f6be5d8441f71cbe6ebb1657c69b543eb085b848b92b591b7ac01d6e6598", + "usage": "input" + }, + { + "git_blob": "8ecfd3e4d0bcb449ecb1e150c4f1f4fbb39ca656", + "path": "research/pr4359-p7-padding/TENSOR.md", + "sha256": "b2eba86cb979b4dc2a045f2e74bbd29e4d9e5ec87d6a2bc23ba7b54f1f58e3e3", + "usage": "input" + }, + { + "git_blob": "340e1f0ffb8a1a9c38fbbd9119580b6d23e01b59", + "path": "research/pr4359-p7-padding/dependencies/compiler-refill/endpoint.py", + "sha256": "d097e55f06c3f244f2074ffd7c1a0a5f3c4b4b6a6accf9619d1dde5c0ae85e15", + "usage": "input" + }, + { + "git_blob": "8d2d96e3998254c2333c43fe47cdfd074cbd811e", + "path": "research/pr4359-p7-padding/native_inventory.py", + "sha256": "65539acaf45bdfe8c5aee6830f9c9b3d1107c442a60842ef803fdd7688de8f32", + "usage": "input" + }, + { + "git_blob": "89c400d5970024b3debe870c36ce43889beed001", + "path": "research/query-thinned-controllers/BIT-CONTROLLER.json", + "sha256": "39ac84fb848b908f7ba051fae4556d507900c421dc5d23501a9c0cb1d61fd08d", + "usage": "input" + }, + { + "git_blob": "39318f6ad9baf0838a274ca1042b1e3ba0e74bf9", + "path": "research/query-thinned-controllers/COMPLEX-CONTROLLER.json", + "sha256": "bf1143325d8380fab40cd5a85449f9a5412f0340deba7f4693714c92ae320088", + "usage": "input" + }, + { + "git_blob": "e0695152c98d727edfd0d2034b58a1c7e8682c0c", + "path": "research/query-thinned-controllers/RESULT.json", + "sha256": "6ebfc8c0f09166f4834e9d7427410cb31aefff2cd4d4ce588c8e52c9c70e9a0f", + "usage": "input" + }, + { + "git_blob": "0f061c87ff87c43ff1ea0fc418582e9ccea3bc1d", + "path": "research/query-thinned-controllers/SOURCES.json", + "sha256": "74b73563d9f78a4562d376b6f33528d652e41097f65747667f112a3e1fa81d29", + "usage": "input" + }, + { + "git_blob": "d4557e08cfb9fe57cc1ae4024705a72dc95f3583", + "path": "research/query-thinned-controllers/controller.py", + "sha256": "8b462d660487b1be4940357c4c7522967b1bfaede3c02b1c66109b85acae0fd2", + "usage": "input" + }, + { + "git_blob": "f1114036fff66f57014e5c1256141fb78ff4c4a9", + "path": "research/query-thinned-controllers/verify.py", + "sha256": "07dea601d6bbaa4d90e576f20c8607c37fb01e8778c798d919fa9df435049950", + "usage": "input" + }, + { + "git_blob": "166841a037f069249f6f7f6dedb89248812f59e2", + "path": "research/t74-native-fast/vendor/native/new/code/borrow/vendor/clifford/clifford_exact.py", + "sha256": "2982ead07721e83358dc67c6f49c2b4c16a236a6bebdfd72f58221be1f5d0962", + "usage": "input" + }, + { + "git_blob": "64bfc5af6709ed9811171e0a2108f05e1219cb65", + "path": "docs/research/agent-task-catalog.json", + "sha256": "352a6184713b8843d96fd2c2071eb7aeaa655906b7c51d45ad444912666c8a96", + "usage": "provenance" + }, + { + "git_blob": "ed33caef5c5827693e9572d252a66f99cbb73d40", + "path": "certificates/selected-result.json", + "sha256": "5732707cc1e460b090b53f2463162749ad860de878a18f7408938671d295a9d9", + "usage": "provenance" + }, + { + "git_blob": "2fe84a7b30b1e26e60ce0ec4775894eb1831c5d6", + "path": "autoresearch.md", + "sha256": "d16f0d3bb4d4b213d06c128db6d6460b0fe9ec1ac5a6c1ea1febf1db40e7b60d", + "usage": "provenance" + } + ], + "schema_version": 1 +} diff --git a/research/native-lattice-retiming/TASK.json b/research/native-lattice-retiming/TASK.json new file mode 100644 index 0000000000..544002777e --- /dev/null +++ b/research/native-lattice-retiming/TASK.json @@ -0,0 +1,143 @@ +{ + "actual_scope": "Build a changed native frame contact beyond PR4441, then completely pay tensor completion, finite uniform compilation and the integer-multiplication consumer.", + "ai_assistance": "Substantial OpenAI Codex assistance; no subagents.", + "author": "zxv, with substantial OpenAI Codex assistance", + "base_commit": "5f9d871c6bd1b9e34db5a7ea5ef08a908e94db39", + "bottleneck_link": "New subspaces outside the predecessor frame menu can change the raw paid profile while exact native endpoints and all helper outputs stay fixed.", + "budget_minutes": 60, + "evidence": "Explicit one-contact native patch; two all-column replays in both orientations, new absolute-phase transports, complete changed invoice, two moment engines, both paid tails, finite ranks and all outer predicates.", + "open_questions": [ + { + "blocked_by": "No global optimization certificate; keep all fixed contacts and exact replay.", + "first_step": "Start from PATCH.json and test one fully charged coordinated new-label move.", + "question": "Can simultaneous moves to different frame labels improve the full invoice further?", + "why_it_matters": "A fixed-frame-menu optimum does not cover the subspace lattice." + }, + { + "blocked_by": "No complete restoration and frame-transfer invoice.", + "first_step": "Price the Dumas\u2013Grenet prepare/accumulate/distribute pattern through actual Fourier frames.", + "question": "Can a multi-target accumulating native interface share a paid query?", + "why_it_matters": "This could yield a larger change than local retiming." + }, + { + "blocked_by": "These universal contracts remain premises.", + "first_step": "Audit a named caller and retained hypothesis in PR4359/4440/4441.", + "question": "Do the inherited all-column, precision and tape contracts survive independent scientific review?", + "why_it_matters": "Exact finite arithmetic is not unconditional or formal acceptance." + } + ], + "original_card": { + "acceptance_gate": "Pin the current sources and one obligation; the historical owner audit is an example, not evidence of a current bug.", + "allowed_variations": [ + "One provider-registry, dispatch, native-closure or admission-predicate obligation; separate branches must name distinct coverage." + ], + "bottleneck_link": "Closing a current acceptance gap or proof obligation strengthens reliability even without changing kappa.", + "existing_checks": [ + { + "evidence": "research/staged544-mixed-fourth-entry/README.md", + "remaining": "Rebind and validate ordinary/outer admission with all four providers; full mixed release not established.", + "scope": "PR #4088: author-checked local words, native receipts, owner/phase fill and exact moment.", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129", + "source_commit": "72d7efc181edb21806a878f174847c96dd410ab0", + "status": "author-checked" + }, + { + "evidence": "research/scatter-boundary-decision/README.md", + "remaining": "Consult its exact acceptance scope before any new exporter audit; not proof of a selected failure.", + "scope": "PR #3801: successor scatter-boundary decision package.", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129", + "source_commit": "911f8800ba7a4b03603ef62c5ffc6240e53cb5fd", + "status": "author-checked" + } + ], + "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.", + "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." + }, + "id": "supplier-boundary-audit", + "methods": [ + "Trace one hypothesis through the source, checker and complete caller.", + "Construct one semantically invalid but superficially well-formed fixture and test rejection." + ], + "overlap_terms": [ + "owner boundary", + "bridge omission", + "hosting", + "2977", + "scatter export", + "duplicate index", + "parity semantics", + "4088", + "3801", + "staged544-mixed-fourth-entry", + "scatter-boundary-decision" + ], + "question": "Can the #4088 four-provider dispatch satisfy the complete ordinary/outer admission contract?", + "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." + ], + "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" + ] + }, + "outcome": "completed", + "overlap": { + "checked_at_utc": "2026-10-21T20:51:25Z", + "discussion_records": 3289, + "limits": "Sparse local coverage; no arbitrary diffs or closed remote PR-body coverage; no novelty certificate. No public participation authorized for this successor.", + "local_HEAD_notes": 5739, + "local_notes_searched": 23, + "open_pr_bodies": 301, + "remote_pagination_complete": true, + "submission_refresh": { + "canonical_main": "2a13eb1827784206202db90e5dc8327cf8a250db", + "checked_at_utc": "2026-10-21T21:36:00Z", + "concurrent_PR4447": "322e0ec764aa7ef7801383feb1f656e460dd8bed", + "finding": "Same B/480 contact and paid profile, declared kappa .00300123. This contribution retains .00300120 and gives substantially smaller sufficient templates. No novelty or strongest-endpoint claim." + } + }, + "priority_revision": 7, + "publication_policy": "User approved submission of this reviewed contribution on 2026-10-21. First-person prose refers to the author, zxv. No further Discussion participation is requested.", + "resource_budget": "Single-process bounded controller arithmetic, under a few minutes per screen; no Lean, Docker, concurrent artifact replay or native historical suites.", + "schema_version": 1, + "scope_change_reason": "The explicit user requested a changed native construction and literature evaluation when stuck, then approved submission after reviewing the local result. PR4440/4441 supplied the useful starting model.", + "scope_decision": "The new exact contact changes the paid profile and passes the fully charged conditional transfer. Publish the reviewed result and smaller finite ranks; acknowledge concurrent PR4447 without a novelty or strongest-kappa claim.", + "scope_status": "changed", + "stop_rule": "Publish the reviewed, strictly improving exact paid profile with all inherited native and consumer obligations retained; do not expand the mathematical scope during submission.", + "task_id": "supplier-boundary-audit", + "upstream_checkpoint": { + "checked_at_utc": "2026-10-21T21:36:00Z", + "commit": "2a13eb1827784206202db90e5dc8327cf8a250db", + "pending_sources": { + "PR4440": "40e22a83ed660d3d6074c4f2dbf14bfb621eee51", + "PR4441": "5f9d871c6bd1b9e34db5a7ea5ef08a908e94db39" + }, + "priority_revision": 7 + }, + "validation": { + "changed_receipt": "rejected", + "changed_source": "rejected", + "committed_bytes": "pass", + "export_integrity": "pass", + "git_free_optimized": "pass", + "metadata_pins": "pass", + "optional_discovery": "reproduces exact patch", + "platform": "macOS arm64", + "python": "3.12.8", + "registered_replay": "pass", + "source_history": "unavailable: shallow checkout", + "unpublished_at_initial_validation": true + } +} diff --git a/research/native-lattice-retiming/VALIDATION.md b/research/native-lattice-retiming/VALIDATION.md new file mode 100644 index 0000000000..d63d8cce0b --- /dev/null +++ b/research/native-lattice-retiming/VALIDATION.md @@ -0,0 +1,75 @@ +# Validation + +All scientific checks below pass on CPython 3.12.8, macOS arm64, 21 October +2026. Scientific code/receipts were committed at +`71c54ffcfee4c77d77164f9b02bdf763a8f267d0`; the final follow-up only records +validation and changes documentation/task status. + +| Check | Result | +| --- | --- | +| Metadata and all source pins | PASS_PACKAGE_METADATA_AND_PINS | +| Registered full replay | PASS_REGISTERED_RESEARCH_PACKAGE | +| Both native orientations, two interpreters, 632 arbitrary persistent columns, arbitrary owned-center entry then legal erasure | PASS | +| Four new edge types, forward/conjugate Clifford decoding, exact rank and absolute phase | PASS | +| Complete p17 physical/Laurent word, changed full paid/productive invoice | PASS | +| Two interval engines, new root bracket, both paid strictification tails, both finite uniform ranks | PASS | +| Nine outer rows, 54 current predicates, four guards and 63 legacy predicates | PASS | +| Wrong contact, global-phase-only, short-product-bound and outer negative controls | REJECTED as intended | +| Committed-byte preflight, 59 exported files | PASS_RESEARCH_COMMIT_BYTES | +| Deterministic committed export and independent integrity check | PASS_RESEARCH_EXPORT | +| Isolated Git-free optimized replay (`-I -O -B`, explicit package import path) | PASS_CONDITIONAL_NEW_NATIVE_PROFILE_KAPPA | +| Changed pinned source comment in the Git-free export | Rejected by source authentication | +| Changed saved κ receipt in the Git-free export, full optimized replay | Rejected at exact RESULT.json comparison | +| Optional C++20 discovery | Reproduces exactly phase B contact 480 and the new span | + +Commands: + +```sh +python3.12 -B scripts/research_package.py --package research/native-lattice-retiming --check-only +python3.12 -B scripts/research_package.py --package research/native-lattice-retiming +python3.12 -B scripts/check_research_commit.py --package research/native-lattice-retiming +python3.12 -B scripts/export_research_package.py export --package research/native-lattice-retiming --ref 71c54ffcfee4c77d77164f9b02bdf763a8f267d0 --output /tmp/native-lattice-71c54ff.tar +python3.12 -B scripts/export_research_package.py check /tmp/native-lattice-71c54ff.tar +python3.12 -B research/native-lattice-retiming/discover.py --output /tmp/native-lattice-discovery-replay +``` + +The checked export was extracted without Git, then `verify.py` ran through +`runpy.run_path` under `python3.12 -I -O -B` with only the explicit package +folder inserted into `sys.path`. Its normal 43-input authentication, complete +native and arithmetic checks and receipt comparisons all ran. The two external +mutation controls used that export and restored the exact original bytes. +The optional compiler was Apple clang 21.0.0 with `-O3 -std=c++20`. + +`--check-source-history` is **unavailable**: its explicit precondition rejects +this shallow checkout with “source-history check requires full Git history.” +No unshallow fetch was attempted. Exact pending heads and consumed bytes are +present, pinned and retained in local merge ancestry; the unavailable check +is not presented as scientific or provenance acceptance. + +Source ancestry includes PR4440 head +`40e22a83ed660d3d6074c4f2dbf14bfb621eee51` and PR4441 head +`5f9d871c6bd1b9e34db5a7ea5ef08a908e94db39`. SOURCES.json binds the 43 +consumed source files. The final upstream checkpoint at 20:56 UTC found +canonical main still `2a13eb1827784206202db90e5dc8327cf8a250db`, unchanged +priority guidance, unchanged pending heads and selected κ=.0023. + +No hosted CI, Lean, Docker, complete historical suite or independent +scientific review is claimed. Universal native/all-column, owned-query, +precision, physical tape, analytic and recovery contracts remain conditional +premises. At the initial validation checkpoint this package was unpublished. +The user subsequently approved submission after review. + +## Publication preparation + +The submission branch starts from public PR4441 head `5f9d871c` and carries +only this package beyond that dependency. The earlier unpublished p7 negative +screen remains on its local branch and is excluded. All 46 source/provenance +rows were checked byte-for-byte against this public base before updating the +base pin; no scientific program, patch or receipt changed. The original local +validation commit is retained locally, and its code/receipt bytes are identical +to this submission's scientific files. + +The 21:36 UTC refresh found unchanged canonical main and guidance, plus +concurrent PR4447 at `322e0ec764aa7ef7801383feb1f656e460dd8bed`. Its same +contact/profile and higher declared endpoint are acknowledged in README.md +and the PR description. No unique-discovery or strongest-kappa claim is made. diff --git a/research/native-lattice-retiming/VERIFY.json b/research/native-lattice-retiming/VERIFY.json new file mode 100644 index 0000000000..a0eb02eb26 --- /dev/null +++ b/research/native-lattice-retiming/VERIFY.json @@ -0,0 +1,69 @@ +{ + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "checks": "Authenticate exact source bytes; replay both orientations and 632 arbitrary inputs with two native interpreters; decode all new physical edges with absolute phase; rebuild the unchanged p17 Laurent controller and changed full invoice; certify two-engine moments, both paid tails, finite compiler ranks, stronger BIT and all 54+4 current and 63 legacy outer predicates, with mutation controls.", + "timeout_seconds": 600 + } + ], + "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/fresh-helper-thinned/RESULT.json", + "research/higher-moment-strictification/README.md", + "research/higher-moment-strictification/vendor/check_ledger.py", + "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/native-lattice-retiming/NATIVE-RESULT.json", + "research/native-lattice-retiming/PATCH.json", + "research/native-lattice-retiming/RESULT.json", + "research/native-lattice-retiming/SOURCES.json", + "research/native-lattice-retiming/arithmetic.py", + "research/native-lattice-retiming/native.py", + "research/native-lattice-retiming/verify.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" + ], + "python": "3.12", + "requirements": [], + "schema_version": 1, + "status": "ready" +} diff --git a/research/native-lattice-retiming/arithmetic.py b/research/native-lattice-retiming/arithmetic.py new file mode 100644 index 0000000000..ea5fb38dfb --- /dev/null +++ b/research/native-lattice-retiming/arithmetic.py @@ -0,0 +1,136 @@ +"""Complete changed invoice, paid tails, rank and outer consumer. +Apache-2.0. Substantial OpenAI Codex assistance. Credits: PR4359/4433, +Cinna Davis PR4440/4441, and Jacob Alan Sussman's mixed-target flow. +""" +from collections import Counter +from fractions import Fraction as Q +from pathlib import Path +import ast +import json +import native + +HERE=Path(__file__).resolve().parent +ROOT=HERE.parents[1] +KAPPA,TESTED=Q('.00300120'),Q('.00300122') +LOW,HIGH=Q('.0030012390170'),Q('.0030012390173') +need=native.need + +def encoded(x): + if isinstance(x,Q):return str(x) + if isinstance(x,dict):return {str(k):encoded(v) for k,v in x.items()} + if isinstance(x,(tuple,list)):return [encoded(v) for v in x] + return x + +def uniform(E,v,theta,power,kappa): + t=1-TESTED + eta=E.scale(E.power(153,-v*TESTED),t) + need(18**16<22**15 and 2*(18**v)**16<=(153**v)**15,'Strict shifted logarithm contraction') + need(eta[0]>theta**power and E.power(153,v*TESTED)[1]<2**power,'Both logarithmic induction conditions') + gap=(TESTED-kappa)/7 + step=gap.denominator + def passes(j):return (step*j+1)**power<2**(gap.numerator*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 + H=step*hi + need(H>8*v and passes(hi) and not passes(hi-1),'Effective winning integer rank and prior-grid control') + return dict(theta=theta,logarithm_power=power,eta=E.display(eta),gap=gap, + uniform_saving=TESTED-gap,H=H,N='2^'+str(H),integer_exponent=gap.numerator*hi, + word_materialized=False) + +def legacy(params,outer): + source=ROOT/'research/higher-moment-strictification/vendor/check_ledger.py' + parsed=ast.parse(source.read_bytes()) + fn=next(n for n in parsed.body if isinstance(n,ast.FunctionDef) and n.name=='ledger') + constants=[n for n in parsed.body if isinstance(n,ast.Assign) and any(isinstance(t,ast.Name) and t.id.startswith('KAPPA_') for t in n.targets)] + d=params['d'];eps,beta,q,a=(params[k] for k in ('epsilon','beta','q','a')) + grid=10**10;backoff=Q((eps*q*grid).__floor__(),grid)-KAPPA + need(backoff>0,'Positive exact legacy grid backoff') + env={'Q':Q,'R0':params['r0'],'ZETA':Q(1,10**8),'SLACK':d,'STOP':d,'FLOOR':grid,'BACKOFF':backoff, + 'EPS':eps,'BETA':beta,'THETA_POWER':Q(2),'HALO_POWER':48,'CORE_POWER':128,'STRASSEN_TAU':Q(45,16), + 'b':params['b'],'q':q,'a':a,'bit':params['bit_saving'], + 'online':Q('0.001730970419199163702738'),'old':Q('0.001730970419199163702738')} + exec(compile(ast.fix_missing_locations(ast.Module(body=constants+[fn],type_ignores=[])),'pinned legacy outer','exec'),env) + result=env['ledger']('native_lattice') + need(result['kappa']==KAPPA and result['margins']==outer['margins'],'Nine outer rows agree independently') + need(len(result['strict_checks'])==63 and all(x>0 for x in result['strict_checks'].values()),'All 63 legacy predicates') + return dict(checks=result['strict_checks'],grid=grid,backoff=backoff) + +def run(local): + E=native.load(ROOT/'research/higher-moment-strictification/verify.py','lattice_exact_intervals') + C=native.load(ROOT/'research/query-thinned-controllers/controller.py','lattice_query_controller') + word=native.read(ROOT/'research/query-thinned-controllers/COMPLEX-CONTROLLER.json') + need(json.loads(json.dumps(C.run('complex',17,8)))==word,'Exact unchanged source physical word and Laurent boundaries') + H={int(k):v for k,v in local['helpers'].items()};N={int(k):v for k,v in local['paid'].items()} + T,P=Counter(),Counter();full=thin=idle=0 + for e in word['physical_events']: + if e[0]=='LOCAL':full+=1;T.update(H);P.update(N) + elif e[0]=='QUERY_SHEAR':thin+=1;P[1]+=112 + elif e[0]=='IDLE':P[8*len(e[2])]+=224;idle+=224 + for term in word['diagonal']:T[1+8*sum(term[1:])]+=112 + need((full,thin,idle)==(19,16,3584),'Every native, query and whole idle') + predecessor=native.read(ROOT/'research/fresh-helper-thinned/RESULT.json') + oldT=Counter({int(k):v for k,v in predecessor['targets'].items()});oldP=Counter({int(k):v for k,v in predecessor['paid'].items()}) + need(T==oldT and P==oldP+Counter({1:19,4:19})-Counter({2:19,3:19}),'Independent complete profile substitution') + need(sum(T.values())==11560 and sum(P.values())==69273,'Complete field and call counts') + need((sum(r*n for r,n in T.items()),sum(r*n for r,n in P.items()))==(260798,259998),'Unchanged rank masses and surplus 800') + 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(LOW)[0]>0 and margin(HIGH)[1]<0,'Exact changed raw-root bracket') + # Positive decreasing on [0,.01], sufficient to isolate this first root. + derivative=sum(n*E.mul(E.power(r,Q('.99')),E.log_bounds(r))[0] for r,n in T.items())-sum(n*E.mul(E.power(r,1),E.log_bounds(r))[1] for r,n in P.items()) + need(derivative>0,'Strictly decreasing throughout C in [0,.01]') + other=native.load(ROOT/'research/kappa-rebuild/architecture/mixed_target_probe.py','lattice_other_intervals') + tl,th=other.moment(T,TESTED);pl,ph=other.moment(P,TESTED) + t=1-TESTED;target=E.moment(T,t);paid=E.moment(P,t) + need(tl>ph and max(tl,target[0])<=min(th,target[1]),'Second exact raw moment engine') + alpha=E.divide(paid,target);u=Q(3,25);v=675;c=18;b=22 + 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)) + ag,g,d=Q(19,10**9),Q(491,500),Q(391,400) + need(t+u>=1 and alpha[1]<1-ag and gamma[1]1,'Short-product bound negative control') + rank=uniform(E,v,Q(15,16),160,KAPPA) + same=uniform(E,v,Q(15,16),160,Q('.00300105')) + bit=native.read(ROOT/'research/query-thinned-controllers/RESULT.json')['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,'Retain the entire stronger ordinary BIT admission') + gap=(TESTED-KAPPA)/7 + params=dict(kappa=KAPPA,tested_saving=TESTED,complex_uniform_saving=rank['uniform_saving'], + 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) + L=native.load(ROOT/'research/pr4359-p7-padding/dependencies/compiler-refill/endpoint.py','lattice_outer') + 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,'Full current consumer predicates') + need(all(x>0 for group in ('strict_checks','functional_checks') for x in outer[group].values()),'Every current outer predicate') + oldchecks=legacy(params,outer) + source_kappa=Q('.00300105');sg=(TESTED-source_kappa)/7 + sp=dict(kappa=source_kappa,tested_saving=TESTED,complex_uniform_saving=same['uniform_saving'], + b=source_kappa+5*sg,a=source_kappa+4*sg,q=source_kappa+3*sg,bit_saving=admitted, + epsilon=1-sg,beta=1-3*sg,r0=sg/10,stop=sg,layout=sg,d=sg) + same_outer=L.ledger(sp);same_outer['functional_checks']['actual_new_BIT_stock_sublinear']=sp['beta']*(1-atom) + need(all(x>0 for group in ('strict_checks','functional_checks') for x in same_outer[group].values()),'Same-kappa full outer comparison') + controls={} + for name,patch in [('old_BIT',{'bit_saving':Q('.0027')}),('closed_uniform',{'complex_uniform_saving':params['b']}),('unfunded_kappa',{'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 + local_scalar=max(x['real_scalar_allowance'] for x in local['native'].values()) + routes=(sum(N.values())+2*408)*1000 + need(local_scalar+routes<10**7,'All unchanged scalar and changed physical route costs fit') + raw=19*10**7+16*1792+32*112*(len(word['physical_events'])+sum(len(word['boundaries'][k+'_program']) for k in ('left','right'))) + need(raw<10**9,'Complete nonrecursive raw budget') + return encoded(dict(status='PASS_CONDITIONAL_NEW_NATIVE_PROFILE_KAPPA',kappa=KAPPA,kappa_decimal='0.00300120', + gain_over_PR4441=KAPPA-Q('.00300105'),targets=dict(sorted(T.items())),paid=dict(sorted(P.items())), + rank_surplus=800,raw_root=[LOW,HIGH],raw_root_scope='Unique crossing on [0,.01]; no universal or global mechanism ceiling.', + derivative_negative_upper=-derivative,raw_moment_margin=E.display(margin(TESTED)), + strictification=dict(tested=TESTED,power=v,cutoff=c,floor=b,u=u,alpha=E.display(alpha),gamma=E.display(gamma),delta=E.display(delta),limits=[1-ag,g,d],normalized_paid_upper=bound), + compiler=rank,same_predecessor_kappa_compiler=same, + rank_exponent_reduction=Q(int(predecessor['compiler']['H']),rank['H']),same_kappa_rank_exponent_reduction=Q(int(predecessor['compiler']['H']),same['H']), + ordinary_BIT=bit,outer=outer,same_predecessor_kappa_outer=same_outer,legacy_outer=oldchecks,negative_controls=controls, + nonrecursive=dict(local_scalar=local_scalar,route_bound=routes,raw_upper=raw,budget=10**9))) diff --git a/research/native-lattice-retiming/discover-lattice.cpp b/research/native-lattice-retiming/discover-lattice.cpp new file mode 100644 index 0000000000..1798964ac4 --- /dev/null +++ b/research/native-lattice-retiming/discover-lattice.cpp @@ -0,0 +1,68 @@ +// 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 +#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 Frame{int dim;array bits;}; +bool sub(const Frame&a,const Frame&b){for(int k=0;k<8;k++)if(a.bits[k]&~b.bits[k])return false;return true;} +bool contains(const Frame&f,int v){return(f.bits[v/64]>>(v%64))&1;} +Frame mapped(const Frame&f,int v,bool join){Frame g=f;if(join){if(contains(f,v))return g;g.dim++;for(int x=0;x<512;x++)if(contains(f,x))g.bits[(x^v)/64]|=1ULL<<((x^v)%64);}else{bool changed=false;for(int x=0;x<512;x++)if(contains(f,x)&&(__builtin_popcount(unsigned(x&v))&1)){g.bits[x/64]&=~(1ULL<<(x%64));changed=true;}if(changed)g.dim--;}return g;} +struct Node{bool mut;int oldf,newf;}; +int main(int argc,char**argv){ + if(argc!=2)return 2; + int F,N,E;cin>>F>>N>>E;vectorframes(F);map,int>lookup; + for(int f=0;f>frames[f].dim;for(auto&x:frames[f].bits)cin>>x;lookup[frames[f].bits]=f;} + vectornodes(N);vectoridx(N,-1),rev; + for(int i=0;i>m>>nodes[i].oldf>>nodes[i].newf;nodes[i].mut=m;} + vector>edges(E);for(auto&[a,b]:edges)cin>>a>>b; + int H;cin>>H;vector>helpers(H);for(auto&[a,b]:helpers)cin>>a>>b; + for(int i=0;iused;for(auto n:nodes){used.insert(n.oldf);used.insert(n.newf);}vectorproposal(frames.size()); + for(int f:used)proposal[f]=mapped(frames[f],v,join); + Flow flow(V+2);vectorunary(V,0);int s=V,t=V+1; + for(auto[a,b]:edges){int fa=nodes[a].newf,fb=nodes[b].oldf;auto A=frames[fa],B=frames[fb],GA=proposal[fa],GB=proposal[fb]; + if(!sub(A,B)){cerr<<"bad baseline edge"<=0&&i==j){unary[i]+=e11-e00;continue;} + if(i>=0&&j>=0){double w=e10+e01-e00-e11;if(w<-1e-7){cerr<<"nonsubmodular "<=0)unary[i]+=e10-e00;else if(j>=0)unary[j]+=e01-e00; + } + for(auto[a,b]:helpers){auto A=frames[nodes[a].newf],B=frames[nodes[b].oldf],GA=proposal[nodes[a].newf],GB=proposal[nodes[b].oldf]; + unary[idx[a]]+=powers[B.dim-A.dim]-powers[GB.dim-GA.dim]; + } + for(int i=0;i=0&&reach[idx[a]]?proposal[fa]:A,GB=idx[b]>=0&&reach[idx[b]]?proposal[fb]:B; + if(!sub(GA,GB)){legal=false;break;}delta+=powers[GB.dim-GA.dim]-powers[B.dim-A.dim]; + } + for(auto[a,b]:helpers)if(reach[idx[a]]){auto A=frames[nodes[a].newf],B=frames[nodes[b].oldf],GA=proposal[nodes[a].newf],GB=proposal[nodes[b].oldf];delta+=powers[B.dim-A.dim]-powers[GB.dim-GA.dim];} + if(legal&&delta < -1e-8){int count=0,h=0;for(auto[a,b]:helpers)if(reach[idx[a]])h++; + vectortranslated(frames.size(),-1); + for(int f:used){auto G=proposal[f];auto it=lookup.find(G.bits);if(it==lookup.end()){int k=frames.size();lookup[G.bits]=k;frames.push_back(G);translated[f]=k;}else translated[f]=it->second;} + for(int k=0;k=0&&reach[idx[k]]){nodes[k].oldf=translated[nodes[k].oldf];nodes[k].newf=translated[nodes[k].newf];count++;} + gain+=delta;cerr<<"ACCEPT round "<=-1e-8)break; + } +} diff --git a/research/native-lattice-retiming/discover.py b/research/native-lattice-retiming/discover.py new file mode 100644 index 0000000000..425a74925c --- /dev/null +++ b/research/native-lattice-retiming/discover.py @@ -0,0 +1,59 @@ +"""Optional floating discovery; never mathematical acceptance. +Apache-2.0, Codex assistance. Min-cut base credited to Cinna Davis PR4441. +""" +import argparse +import json +from pathlib import Path +import subprocess +import native + +def main(output): + output.mkdir(parents=True,exist_ok=False) + N,c,_,baseline=native.build() + c['frames'].pop() # The explicit candidate must not seed its own discovery. + program=baseline['forward'];nodes=[];paths=[[] for _ in range(632)] + def contact(old,new,roles,mutable=False,index=-1): + i=len(nodes);nodes.append(dict(old=old,new=new,roles=roles,mutable=mutable,index=index)) + for r in roles:paths[r].append(i) + for r,f in enumerate(c['start']):contact(f,f,[r],r>=224) + for i,e in enumerate(program): + if e[0]=='scalar': + g=e[1];rr=g[1:3] if g[0] in ('add','copy') else g[1:2];roles=[r[1] for r in rr if r[0]=='L'] + if roles:contact(e[2],e[2],roles,all(r[0]=='L' for r in rr),i) + elif e[0]=='warp':contact(e[3],e[4],[e[1][1]],False,i) + last=len(nodes) + for r,f in enumerate(c['final']):contact(f,f,[r],r>=224) + edges=[(a,b) for path in paths for a,b in zip(path,path[1:])] + graph=output/'input.graph' + with graph.open('w') as out: + print(len(c['frames']),len(nodes),len(edges),file=out) + for basis in c['frames']: + sp=N.span(basis) + print(len(basis),*[sum(1<<(v%64) for v in sp if v//64==b) for b in range(8)],file=out) + for n in nodes:print(int(n['mutable']),n['old'],n['new'],file=out) + for a,b in edges:print(a,b,file=out) + print(408,file=out) + for r in range(224,632):print(r,last+r,file=out) + executable=output/'discover-lattice';solution=output/'solution.txt' + subprocess.run(['c++','-O3','-std=c++20',str(native.HERE/'discover-lattice.cpp'),'-o',str(executable)],check=True,timeout=120) + with graph.open() as inp,(output/'discovery.log').open('w') as log: + subprocess.run([str(executable),str(solution)],stdin=inp,stdout=log,stderr=log,check=True,timeout=600) + native.need(solution.exists(),'No improved candidate found') + lines=solution.read_text().splitlines();F,M=map(int,lines[0].split());native.need(M==len(nodes),'Discovery dimensions') + spaces=[] + for line in lines[1:F+1]: + d,*chunks=map(int,line.split());sp=frozenset(x for x in range(512) if chunks[x//64]>>(x%64)&1) + native.need(len(sp)==1<=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))