diff --git a/research/native-transpose-owned/NATIVE-CERTIFICATE.json b/research/native-transpose-owned/NATIVE-CERTIFICATE.json new file mode 100644 index 0000000000..fedb291f72 --- /dev/null +++ b/research/native-transpose-owned/NATIVE-CERTIFICATE.json @@ -0,0 +1 @@ +{"axes":9,"peak_expanded_terms":24664,"problem_sha256":"a4c901e27b21dc7033ff8ace1217165eabb5e59ecd301dba321f76940db8be05","residual_terms":0,"roles":641,"schema":"native-tensor-cutoff/v1","status":"IDENTITY_ALL_POSITIVE_WIDTHS","window":[22,25]} diff --git a/research/native-transpose-owned/NATIVE-PROBLEM.json.gz b/research/native-transpose-owned/NATIVE-PROBLEM.json.gz new file mode 100644 index 0000000000..f2137b4174 Binary files /dev/null and b/research/native-transpose-owned/NATIVE-PROBLEM.json.gz differ diff --git a/research/native-transpose-owned/PHASES.json.gz b/research/native-transpose-owned/PHASES.json.gz new file mode 100644 index 0000000000..159b1c026d Binary files /dev/null and b/research/native-transpose-owned/PHASES.json.gz differ diff --git a/research/native-transpose-owned/README.md b/research/native-transpose-owned/README.md new file mode 100644 index 0000000000..def61111b8 --- /dev/null +++ b/research/native-transpose-owned/README.md @@ -0,0 +1,273 @@ +# Conditional kappa 0.00302725 by transposing an owned supplier + +This construction gives **conditional kappa = 12109/4000000 = 0.00302725**. +It improves the selected PR4610 value 0.0030217758 by 0.0000054742. It improves +the eight-relation PR5383 value 0.00302666 by 0.00000059. The paid profile changes; +the gain does not come from more digits of an unchanged root. +It also exceeds the later [PR #5387](https://github.com/CrocSwap/integer-mult-bounds/pull/5387) +compiler refinement, 0.003026674765, by 0.000000575235. That refinement is related +work; it is not a source dependency. + +The new result transfers a completed backward supplier to the forward +interface. It applies the classical transposition principle to the complete +linear circuit, including owned COPY and CLEAR operations. Exact monomial +corrections then restore the required forward map. Thus the two forward calls +can use the same reduced paid and helper profiles as the sixteen backward +calls. The construction also gives a reusable rule for later suppliers with +this interface and clean owned storage. + +[RESULT.json](RESULT.json) gives the complete evidence and bill. +[WORD.json.gz](WORD.json.gz) gives the emitted finite word and its boundary +corrections. [PHASES.json.gz](PHASES.json.gz) gives every transposed paid +operator recipe. [SOURCES.json](SOURCES.json) pins all consumed bytes. +The selected frontier is unchanged. + +## Exact source and separate scope + +The scientific base is canonical main +`1ec1119972c9aefe42525172d07b332fcff81cb4`, priority revision 7. +The source is Ali Romman's eight-relation +[PR #5383](https://github.com/CrocSwap/integer-mult-bounds/pull/5383), fixed at +`4bd6efa51a495a7c7b7754915cf0244e7e60969e`. Its published word, after canonical +JSON serialization with a final newline, has SHA256 +`2aee5e997df99726fc763e510d9cb69fbe4f86114dc8d2cd33ad26c6c462a21d`. +The verifier reconstructs and checks that exact word before transposition. +It does not consume a later PR head or an unpublished helper relation. +The exact source files are retained in commit +`5eb314069417db1f4305430b6b14f20e9251e509` in this branch. The live pins use +that ancestor; each `source_pin` retains the original PR source and hash. +A clean checkout does not need either pending PR commit in its object store. + +PR5383 prepares eight owned pivots from independent cold helpers. It removes +eight rank-eight centers and eight rank-one jobs, and debits eight rank-nine +productive targets. Its unchanged input is Cao Yifan's final +[PR #4610](https://github.com/CrocSwap/integer-mult-bounds/pull/4610) word, with +payload SHA256 +`cfcd36b40326d7a5815e1db5313444379b3fb756b27d5201c561574c085cc0dd`. +This package retains that backward construction and changes only the forward +supplier and its full cost calculation. + +The [scoped claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/5125#discussioncomment-19154367) +first tested the one-relation source. After PR5383 published and released its +eight-relation construction, this work pinned that stronger completed source. +No search or priority claim for the source relations is part of this result. Native map changes, +finite contact searches and no-snapshot relation screens that gave no gain +are not included in this PR. + +## 1. Transpose a complete linear circuit + +Let a source circuit act on independent fields x and owned fields z. Assume +that its complete map, with both x and z initially arbitrary, is + +```math +(x,z) \longmapsto (Bx,0). +``` + +In particular, every owned input column and output row is zero in the complete +matrix. Reverse the instruction order and transpose each instruction matrix. +The resulting circuit has complete map `(x,z) -> (B^T x,0)`. The transpose is +bilinear transpose over the complex numbers. It is not conjugate transpose. + +The emitted scalar rules are: + +| Source instruction | Transposed instruction | +| --- | --- | +| `d += c*s` | `s += c*d` | +| `d *= c` | `d *= c` | +| owned `CLEAR d` | owned `CLEAR d` | +| owned `COPY d <- s` | `s += d`, then owned `CLEAR d` | + +All coefficients stay unchanged. Every new CLEAR targets a field that was +already owned. The procedure uses the same physical slots. It does not invert +a CLEAR or assume that an erased value is available. A source COPY costs one +extra ADD under transposition; that cost is included below. + +A native monomial U has monomial transpose. If its action is +`U e_x = i^p(x) e_(Ax+t)`, its transpose sends `e_(Ax+t)` to `i^p(x) e_x`. +Its permutation is the inverse affine map, with the same entry phase at the +inverse address. The affine-quadratic grammar is closed under this operation. +Equivalently, `U^T = conjugate(U^-1)`. + +A standard Gaussian child C_r is symmetric. A source child with the exact +factorization `L C_r R` therefore transposes to `R^T C_r L^T`. Both new boundary +maps are native monomials. It has the same paid rank r, including its absolute +phase. This gives a direct finite lowering algorithm for every source child. +It does not require a new Gaussian supplier or a new assumption about general +Clifford identities. + +These identities hold at every positive tensor width f. Transposition commutes +with tensor powers, and scalar coefficients stay outside tensor powers. The +new native checker verifies the concrete monomial logical normalization by +its complete four-width criterion. The separate transposition argument and +Gaussian factorization establish the paid circuit statement. + +## 2. The zero-row frame marker requires no reverse zero assumption + +The source replaces eight paid jobs by physical identity. At each such job, +the data row is zero under the prepared helper relations. It records this with `zero_retag`. +The transpose of physical identity is identity. It is omitted from the emitted +physical word. The reverse data row need not be zero. + +For a second endpoint check, insert a distinct fresh free operator at each corresponding +reverse coordinate boundary. The exact rational replay cancels every term +that contains this operator at all returned fields. It checks all 641 entry +columns, including the seventeen owned fields. This is a proof in free operator +words, so it also holds for the actual nonmonomial frame quotient. The proof +symbol is not an emitted gate, an unpaid Gaussian call, or a presumed native +recipe. The complete matrix transposition theorem is the physical argument. + +The new forward artifact lists source indices for transposed paid operators +and source markers. A paid reference resolves through the exact source pair +and PHASES.json.gz. A native warp reverses its signed map and its frame pair. +Source entry and exit normalizers are transposed in reverse order, at whole +invocation boundaries. The inherited whole-job normalizer contract remains +explicit; no internal partial job is normalized for free. + +## 3. Restore the required forward interface + +Use the source controller's normalized complex local interfaces, stated in +`research/query-thinned-controllers/PROOF.md`. On each port, Q is the central +rank-one Gaussian and D is its commuting stage multiplier. Both are symmetric +in these coordinates and `Q^4=I`. For later stages D acts on eight fresh axes. +At stage zero it is the source nine-axis Gaussian times `Q^-1`; the same +symmetry and commutation statements hold. Spectator axes are unchanged. + +```math +F=\begin{pmatrix}D&0\\DQ^{-1}&D\end{pmatrix},\qquad +B=\begin{pmatrix}D&-DQ\\0&D\end{pmatrix},\qquad +J=\begin{pmatrix}Q^2&0\\0&-I\end{pmatrix}. +``` + +Direct multiplication gives `F = J B^T J`. Apply J before and after the +transposed normalized backward circuit. The Q squared operation is the exact +native translation, with no paid Gaussian job. The Y sign is scalar `-1` +on the complete field. It is not native phase two raised to tensor width f. +The verifier rejects that phase substitution with an all-width counterexample. + +The backward helper normalizer gives `conjugate(C_r)`. Transposition leaves it +unchanged because it is symmetric. Append `C_r^2`, the native translation on +its r active axes, to obtain C_r. Charge one such pass on every retained helper. +The word records all 400 helper ranks and translation offsets. These wrappers +restore the original forward main contract and the 400 independent productive +helper contracts. The eight pivot fields and C0 through C8 remain owned and return zero. + +This argument applies to any completed supplier with the same normalized B +interface, standard productive Gaussian helpers, native boundary maps and +clean owned storage. It does not classify other interfaces or justify a +source construction whose own endpoint or bill is incomplete. + +## 4. Complete bill and conditional exponent + +Both directions now have + +```text +paid: {1:2193, 2:412, 3:510, 4:127, 5:40} +helpers: {4:28, 7:7, 8:47, 9:318} +``` + +Relative to PR5383, the two forward calls remove sixteen H1 and sixteen H8 +paid jobs, and debit sixteen H9 productive targets. For every `00`. This adds 12.5 percent to the +source's sixteen-call moment gain. Relative to final PR4610, the full p16 +change is minus 144 H1, minus 144 H8 and minus 144 H9 targets. + +The full bill has **64,116 paid jobs and 10,784 productive fields**. The rank +surplus stays 752. Both main targets, all 15 query shears, all idle jobs and +both completion tails are included. Two independently assembled invoices and +two rational interval engines agree. + +The fixed-profile crossing lies in +**(0.00302728824993, 0.00302728824994)**. The claimed saving 0.00302725 leaves +more than 0.00000003824993 raw headroom. The tested saving is 0.00302726. +The exact completion uses power 1024, cutoff 20, floor 21, tail offset 1/5 +and reserve 1e-9. Both tail ratios are below 0.97. The finite compiler has +`H=31385200000000`, `N=2^H`, gap `1/700000000` and logarithm power 1000. +The exact integer threshold test passes. All 54 strict and four functional +outer predicates pass, with the retained ordinary BIT saving 0.0034. + +The forward scalar allowance is 159,320, including the sixteen transposed COPY +rules and both Y sign layers. The route allowance is 10,292,000. It includes +224 main native passes and 400 helper translation passes. It conservatively +doubles the source route allowance because COPY becomes ADD then CLEAR. +Eight additional physical private slots relative to PR4610 suffice, as in +PR5383. Each direction has seventeen owned fields, including eight old helper +slots. +The local allowance remains below 2*10^7 and the complete raw nonrecursive +allowance is **361,098,496 < 10^9**. The forward formal prefix L1 maximum is +442, below the original forward maximum 457. The denominator is at most 32, +equal to the original bound. + +## 5. Reproduce and assess the limits + +Use standard-library Python 3.12. From the repository root: + +```sh +python3 -B scripts/research_package.py --package research/native-transpose-owned +``` + +The normal and optimized commands must end with + +```text +PASS_CONDITIONAL_KAPPA_00302725_OWNED_TRANSPOSE +``` + +For a standalone replay, run: + +```sh +python3 -I -B research/native-transpose-owned/verify.py +``` The separate `--write` authoring +mode writes only this package's artifacts after all mathematical gates pass. +Normal verification compares every regenerated artifact with committed data. + +Checks cover the exact published source word, 641 independent/owned entry +columns, the arbitrary frame-bridge cancellation, the complete native +four-width certificate and its separate checker, all 2,847 transposed paid +phase classes, all 180 native warp classes on 92,160 literal columns, all 112 +Q-squared port phases, four productive helper ranks, the literal p16 +controller, the full cost calculation, completion, compiler and outer ledger. +Controls reject a wrong ADD transpose, missing owned cleanup, wrong native +inverse, wrong prepared relation, wrong absolute phase, omitted Q-squared +correction, scalar/tensor sign confusion, unearned helper credit and invalid +outer parameters. + +The complete bound retains the selected framework's native/all-column source, +owned erasure, whole-job normalizers, finite-template closure, precision and +fixed-tape, analytic decomposition, prime avoidance and exact recovery +assumptions. The source and new finite algebra/phase obligations are checked; +physical tape execution, numerical precision execution, ordinary BIT native +replay, Lean, Docker, analytic decomposition and integer recovery are not rerun. +The huge uniform compiled word is specified by a finite algorithm and is not +materialized. This is an author-checked conditional construction. It is not an +unconditional multiplication theorem, a practical speedup, independent human +acceptance or proof-kernel acceptance. + +## Credit + +Prepared by Ali Romman with substantial OpenAI Codex assistance; Apache-2.0. +Ali Romman's separate PR5377 and PR5383 contributions supply the owned +relations, actual saved values, zero-row replacements and backward word. The new +contribution is the transpose construction, its exact forward normalizer, +physical phase receipts and complete additional gain. No credit is claimed +for discovering the source relations. + +Cao Yifan / intqwq supplies final PR4610. Cinna Davis / 1337isnot1337 supplies +the PR4470 controller and native lineage. Dugongue supplies transported-frame +work; zxv supplies native, owned-cache and compiler interfaces; Jacob Alan +Sussman supplies mixed-target recursion. The source notices retain their +predecessors. The classical transposition principle is not new here. + +[PR #5369](https://github.com/CrocSwap/integer-mult-bounds/pull/5369), at +`18354f41de4dc7bfda4692e814cf1d91a6d619ef`, supplies the complete native tensor +criterion, producer and separate checker. The four code files are copied +without changes. Its native and classical mathematical attribution remains in +that linked proof. [source/NOTICE.md](source/NOTICE.md) gives the exact source +links and copied-file scope. The pricing code is adapted from the attributed +PR5377 engine, which retains Cao Yifan, Cinna Davis, zxv and Jacob Alan Sussman. + +## Open next questions + +Apply the construction to a stronger, published and independently verified +backward supplier. First check its complete normalized interface, owned +columns and productive targets. Then transpose the actual word and recompute +the complete bill. This package does not reserve or assess unpublished source +constructions. [TASK.json](TASK.json) records the scope and first gate. diff --git a/research/native-transpose-owned/RESULT.json b/research/native-transpose-owned/RESULT.json new file mode 100644 index 0000000000..32d9851bca --- /dev/null +++ b/research/native-transpose-owned/RESULT.json @@ -0,0 +1 @@ +{"arithmetic":{"PR5383_raw_root_upper":"37833434601/12500000000000","compiler":{"H":31385200000000,"N":"2^31385200000000","eta":{"lower":"0.000000198896818191972299783809","upper":"0.000000198896818191972299783810"},"gap":"1/700000000","integer_test_exponent":44836,"logarithm_power":1000,"theta":"63/64","uniform_saving":"2119081/700000000","word_materialized":false},"fixed_profile_ceiling":{"decreasing_through":"1/20","derivative_upper":{"lower":"-195429.853549519051730354837623051264","upper":"-195429.853549519051730354837623051263"},"remaining_interval_moment_upper":{"lower":"-6817.813214098317476830090331963946","upper":"-6817.813214098317476830090331963945"}},"full_backward":16,"full_forward":2,"gain_over_PR4610":"27371/5000000000","gain_over_PR5383":"59/100000000","kappa":"12109/4000000","kappa_decimal":".00302725","margin_at_PR5383_raw_root_upper":{"lower":"0.151387988317648054643094222493","upper":"0.151387988317648054643094222494"},"margin_at_previous_kappa":{"lower":"1.360313469048365037022624303111","upper":"1.360313469048365037022624303112"},"margin_at_previous_root_upper":{"lower":"1.360296002377893907536683455026","upper":"1.360296002377893907536683455027"},"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":["new_complex_uniform_saving_above_b"],"old_BIT":["actual_bit_above_effective"],"unearned_helper_credit":"Rejected by the independent complete census","unfunded_endpoint":["main_transform_above_kappa","global_coordinate_router_above_kappa","fused_gaussian_above_kappa","group_bit_router_above_kappa","boundary_algebraic_matrix_above_kappa"]},"nonrecursive":{"additional_private_slots":8,"local_routes":10292000,"local_scalar":159320,"owned_slots_per_direction":17,"raw_budget":1000000000,"raw_scalar_upper":361098496},"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":"174299999253/175000000000","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":"741677648940461/245000000000000000","fused_gaussian":"741677646821383/245000000000000000","global_coordinate_router":"2119079/700000000","group_bit_router":"1483355993642763/490000000000000000","group_scans":"349999999/350000000","main_transform":"741677298940461/245000000000000000","microbox_face_corrections":"13475000001/175000000","polynomial_products":"699999999/700000000","sparse_union_movement":"100272927648940461/245000000000000000"},"parameters":{"a":"2119079/700000000","b":"52977/17500000","beta":"699999997/700000000","bit_saving":"17/5000","cap_xi":"222772927298940461/245000000000000000","complex_uniform_saving":"2119081/700000000","d":"1/700000000","epsilon":"699999999/700000000","kappa":"12109/4000000","lambda_":"199394549/200000000","lambda_prime":"348940461/350000000","layout":"1/700000000","q":"1059539/350000000","r0":"1/7000000000","stop":"1/700000000","tested_saving":"151363/50000000"},"strict_checks":{"actual_bit_above_effective":"260921/700000000","actual_logarithmic_gamma_guard":"1/700000000","actual_logarithmic_group_guard":"22227073226059539/122500000000000000","alpha_logarithm_absorption":"1/7000000000","boundary_algebraic_matrix_above_kappa":"1398940461/245000000000000000","cap_above_band":"100272927298940461/245000000000000000","cap_below_cell":"22227072351059539/245000000000000000","cap_below_phase_cell_power":"267227072701059539/245000000000000000","complex_above_effective":"1/700000000","complex_below_one_over_32":"246949/8750000","complex_endpoint":"1/350000000","epsilon_below_one":"1/700000000","epsilon_positive":"699999999/700000000","fine_prime_halo_umbrella":"7/2","fused_gaussian_above_kappa":"1396821383/245000000000000000","gaussian_above_main":"173940461/122500000000000000","global_coordinate_router_above_kappa":"1/175000000","global_gamma_power_slack":"9/7000000000","group_below_dimension":"1/350000000","group_bit_router_above_kappa":"3493642763/490000000000000000","group_gauge_power_slack":"22227073208559539/122500000000000000","group_key_fits_record":"1/350000000","group_positive":"699999997/700000000","group_scans_above_kappa":"697880923/700000000","halo_covers_generic_inverse_radius":"5","improvement_over_user_baseline":"648139790400418148631/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":"34947023/12250000000000000","leaf_saving_above_effective":"17447023/12250000000000000","main_transform_above_kappa":"1048940461/245000000000000000","membership_arithmetic_fits_record":"1/700000000","microbox_face_corrections_above_kappa":"53897880929/700000000","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":"174470231/175000000","positive_layout_slack":"1/700000000","q_below_effective":"1/700000000","q_below_internal":"1/700000000","q_below_leaf":"34947023/12250000000000000","q_positive":"1059539/350000000","short_record_fallback":"17447023/17500000","source_axis_superpolynomial":"1/700000000","sparse_union_movement_above_kappa":"99531251398940461/245000000000000000","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":41154,"16":448,"2":7416,"24":448,"3":9180,"32":448,"4":2286,"40":448,"48":448,"5":720,"56":448,"64":448,"72":224},"paid_calls":64116,"productive_fields":10784,"query_shears":15,"rank_mass_surplus":752,"raw_headroom":["3824993/100000000000000","1912497/50000000000000"],"raw_root_interval":["302728824993/100000000000000","151364412497/50000000000000"],"strictification":{"alpha":{"lower":"0.999999970464534591128115679621","upper":"0.999999970464534591128115679622"},"cutoff":20,"delta":{"lower":"0.950818834663934748568486126695","upper":"0.950818834663934748568486126696"},"floor":21,"gamma":{"lower":"0.957062946439347991413082521771","upper":"0.957062946439347991413082521772"},"normalized_paid_upper":"2097152001953127/2097154147483648","power":1024,"reserve":"1/1000000000","tail_offset":"1/5","tested":"151363/50000000"},"targets":{"145":224,"17":448,"25":448,"33":448,"4":504,"41":448,"49":448,"57":448,"65":448,"7":126,"73":224,"8":846,"9":5724}},"interface":{"D_exponent_is_formal":true,"Q_exponents_modulus":4,"copy_and_clear_checked":true,"identity":"F = J B^T J; J = diag(Q^2,-I)","missing_transpose_rejected":true,"scalar_coefficients_checked":5,"scalar_sign_counterexample":{"axes":9,"character":[0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0],"discrepancy":["2","0"],"input_points":[0,1,2,4,8,16,32,64,128,256,1,2,4,8,16,32,64,128,256,511,511,0,0,0],"input_role":0,"output_points":[0,1,2,4,8,16,32,64,128,256,1,2,4,8,16,32,64,128,256,511,511,0,0,0],"output_role":0,"peak_expanded_terms":1,"problem_sha256":"21a755f2a34d1a25e602dd888bb935c67dae506c5a2fd326d0178e554e5866bb","residual_terms":2,"roles":1,"schema":"native-tensor-cutoff/v1","status":"COUNTEREXAMPLE","window":[22,25]},"wrong_Q_correction_rejected":true},"native":{"controls":{"missing_owned_clear":"('Endpoint', 112, 3, {(112, ()): Fraction(1, 1), (0, ()): Fraction(-1, 1), (633, ()): Fraction(1, 4)})","wrong_native_transpose":"('Endpoint', 400, 12, {(411, ()): Fraction(-1, 2), (400, ()): Fraction(1, 2), (15, ()): Fraction(-1, 2), (410, ()): Fraction(1, 2), (406, ()): Fraction(-1, 2), (53, ()): Fraction(-","wrong_prepared_relation":"('Endpoint', 384, 151, {(384, ()): Fraction(1, 1), (388, ()): Fraction(-1, 1), (398, ()): Fraction(-1, 1), (253, ()): Fraction(1, 1), (239, ()): Fraction(1, 1), (81, ()): Fraction(","wrong_transposed_add":"('Endpoint', 382, 1, {(383, ()): Fraction(-1, 1)})"},"literal_word_sha256":"737caaf8ed380ec2bdac2452839c3fb8a3ddf68136a8f6fee8c4419cfccdc076","native":{"axes":9,"peak_expanded_terms":24664,"problem_sha256":"a4c901e27b21dc7033ff8ace1217165eabb5e59ecd301dba321f76940db8be05","residual_terms":0,"roles":641,"schema":"native-tensor-cutoff/v1","status":"IDENTITY_ALL_POSITIVE_WIDTHS","window":[22,25]},"native_sign_counterexample":{"axes":9,"character":[0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0],"discrepancy":["-1/2","0"],"input_points":[0,1,2,4,8,16,32,64,128,256,1,2,4,8,16,32,64,128,256,511,511,0,0,0],"input_role":411,"output_points":[0,1,2,4,8,16,32,64,128,256,1,2,4,8,16,32,64,128,256,511,511,0,0,0],"output_role":400,"peak_expanded_terms":24746,"problem_sha256":"e2134063e1fb9a6073200d9f298253829c96d767d46aa7a77d17ae0977ed450a","residual_terms":84,"roles":641,"schema":"native-tensor-cutoff/v1","status":"COUNTEREXAMPLE","window":[22,25]},"new_monomial_passes_bound":624,"paid":{"1":2193,"2":412,"3":510,"4":127,"5":40},"real_scalar_allowance":159320,"real_scalar_allowance_before_wrappers":158872,"source_counts":{"adapter":448,"climb":3282,"phase":10,"scalar":17563,"warp":240,"zero_retag":8},"source_replay":{"helpers":{"4":28,"7":7,"8":47,"9":318},"independent_owned_entry_columns":17,"independent_persistent_columns":624,"max_denominator":64,"max_formal_prefix_l1":"163","owned_outputs_zero":true,"paid":{"1":2193,"2":412,"3":510,"4":127,"5":40},"real_scalar_allowance":158744,"zero_identities":8},"source_word_sha256":"2aee5e997df99726fc763e510d9cb69fbe4f86114dc8d2cd33ad26c6c462a21d","transpose":{"all_entry_columns":641,"ghost_terms_at_return":0,"max_denominator":32,"max_formal_prefix_l1":"442"}},"physical":{"Q_squared_ports":112,"literal_native_transpose_columns":92160,"native_warp_classes":180,"paid_classes":2847,"source_clifford_sha256":"2982ead07721e83358dc67c6f49c2b4c16a236a6bebdfd72f58221be1f5d0962","symmetric_helper_ranks":[4,7,8,9],"wrong_absolute_phase_rejected":"Transposed paid absolute phase"},"status":"PASS_CONDITIONAL_KAPPA_00302725_OWNED_TRANSPOSE"} diff --git a/research/native-transpose-owned/SOURCES.json b/research/native-transpose-owned/SOURCES.json new file mode 100644 index 0000000000..2c282a0239 --- /dev/null +++ b/research/native-transpose-owned/SOURCES.json @@ -0,0 +1,134 @@ +{ + "schema_version": 1, + "base_commit": "1ec1119972c9aefe42525172d07b332fcff81cb4", + "files": [ + { + "path": "research/kappa-round3-warp-20261022/ACTUAL-WORD.json.gz", + "usage": "input", + "git_blob": "46d929df83817b85a5387bcdb9745e0627d6366e", + "sha256": "7679daa4ec6a40f56fc7f0202379a6f454310e94945aba4f48beaaaafb838d05" + }, + { + "path": "research/kappa-round3-warp-20261022/PHASE-VALIDATION.json.gz", + "usage": "input", + "git_blob": "ac77b78547d6dbf2e6bd102e1047c5b16c1bca88", + "sha256": "6eae66ed3cfa8a1533e89b9660a57276908e6646640a12f8b1e3489f4ea1354b" + }, + { + "path": "research/joint-helper-lattice/CONTROLLER.json", + "usage": "input", + "git_blob": "49a2f0675819f9deeea27ed77be2c2b6ff2e87e5", + "sha256": "1f5d6aa267e4e66048818714b5d3b5eae17a58abe91d15deeaa34574f7391a5f" + }, + { + "path": "research/kappa-round6-compiler-tightening-20261022/ARITHMETIC.json", + "usage": "input", + "git_blob": "0fdb65f946d557c13d8e2781b9151e2a8ddee5c3", + "sha256": "b4f720a7ccbb5b46e472eaf85dc8739a40598986f19b37d26c4f9ecfbd31f0de" + }, + { + "path": "research/higher-moment-strictification/verify.py", + "usage": "input", + "git_blob": "4b24a5096154736ce060474eb8c72dc64c303699", + "sha256": "0ce7e7137422d5ffeda22085c81fa88471bbe963100fdad62e659f1e3bf89326" + }, + { + "path": "research/kappa-rebuild/architecture/mixed_target_probe.py", + "usage": "input", + "git_blob": "4fc05ab08138218ba9f09e5c89b649afae7c914e", + "sha256": "011c3c9d0cf81103dc84d709a0e36793eb7c5ae3f23c85eac27650ef13afa04a" + }, + { + "path": "research/query-thinned-controllers/RESULT.json", + "usage": "input", + "git_blob": "e0695152c98d727edfd0d2034b58a1c7e8682c0c", + "sha256": "6ebfc8c0f09166f4834e9d7427410cb31aefff2cd4d4ce588c8e52c9c70e9a0f" + }, + { + "path": "research/pr4359-p7-padding/dependencies/compiler-refill/endpoint.py", + "usage": "input", + "git_blob": "340e1f0ffb8a1a9c38fbbd9119580b6d23e01b59", + "sha256": "d097e55f06c3f244f2074ffd7c1a0a5f3c4b4b6a6accf9619d1dde5c0ae85e15" + }, + { + "path": "research/t74-native-fast/vendor/native/new/code/borrow/vendor/clifford/clifford_exact.py", + "usage": "input", + "git_blob": "166841a037f069249f6f7f6dedb89248812f59e2", + "sha256": "2982ead07721e83358dc67c6f49c2b4c16a236a6bebdfd72f58221be1f5d0962" + }, + { + "path": "research/native-transpose-owned/source/cutoff/native.py", + "usage": "input", + "git_blob": "8872f540e108010cdf6d143fa9d89729693a3ed6", + "sha256": "9e30aa82ce17e41d04db81f140475b6f782f274e017c2a32996bd71e4aa9c751", + "pin": "head:5eb314069417db1f4305430b6b14f20e9251e509:research/native-transpose-owned/source/cutoff/native.py", + "source_pin": "head:18354f41de4dc7bfda4692e814cf1d91a6d619ef:research/native-tensor-cutoff/native.py" + }, + { + "path": "research/native-transpose-owned/source/cutoff/native_identity.py", + "usage": "input", + "git_blob": "85376a935d1e9b19202d773c78d09c9025e8a899", + "sha256": "3ca738030aedad5c173579f99254b88aa5edccd02e575945511679ef7b44d452", + "pin": "head:5eb314069417db1f4305430b6b14f20e9251e509:research/native-transpose-owned/source/cutoff/native_identity.py", + "source_pin": "head:18354f41de4dc7bfda4692e814cf1d91a6d619ef:research/native-tensor-cutoff/native_identity.py" + }, + { + "path": "research/native-transpose-owned/source/cutoff/exact.py", + "usage": "input", + "git_blob": "4f8514d1a2ab211b46e820e030e2feda36a4882c", + "sha256": "6d918d23200b7603b620fbe0a3efefd5d05a20d0b99ad8bb9a43b8fcb9e39130", + "pin": "head:5eb314069417db1f4305430b6b14f20e9251e509:research/native-transpose-owned/source/cutoff/exact.py", + "source_pin": "head:18354f41de4dc7bfda4692e814cf1d91a6d619ef:research/native-tensor-cutoff/exact.py" + }, + { + "path": "research/native-transpose-owned/source/cutoff/check_certificate.py", + "usage": "input", + "git_blob": "929ccceeff54218a6b834a838ffb05c18aff4aad", + "sha256": "a6d73b8cefb3c26e39661e6d6eedabfe2c15df123695ba19386daa11d93142aa", + "pin": "head:5eb314069417db1f4305430b6b14f20e9251e509:research/native-transpose-owned/source/cutoff/check_certificate.py", + "source_pin": "head:18354f41de4dc7bfda4692e814cf1d91a6d619ef:research/native-tensor-cutoff/check_certificate.py" + }, + { + "path": "research/native-transpose-owned/source/owned/native.py", + "usage": "input", + "git_blob": "cbff46fe6e7d71c10fe439610f1916ad07fa3cd8", + "sha256": "3c8efab1f830868c054d33391ee2f8bc74f9bae9c134edf5b455790eb674c1c4", + "pin": "head:5eb314069417db1f4305430b6b14f20e9251e509:research/native-transpose-owned/source/owned/native.py", + "source_pin": "head:4bd6efa51a495a7c7b7754915cf0244e7e60969e:research/kappa-joint-relations-20261023/native.py" + }, + { + "path": "research/native-transpose-owned/source/owned/WITNESS.json", + "usage": "input", + "git_blob": "19665f9eac2238d709758e0296eb6016e71b2b1a", + "sha256": "24599011da06325e1012619b2b84a4dd3aceb90ab42d3caaf6414879e7d16591", + "pin": "head:5eb314069417db1f4305430b6b14f20e9251e509:research/native-transpose-owned/source/owned/WITNESS.json", + "source_pin": "head:4bd6efa51a495a7c7b7754915cf0244e7e60969e:research/kappa-joint-relations-20261023/WITNESS.json" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "b288ae44032fd84dd5564243422836cbcd29835e", + "sha256": "f9ed52bb642cd1e1486cf2743557ac5fa23cf1514a3277d786a644e39a565038" + }, + { + "path": "research/query-thinned-controllers/PROOF.md", + "usage": "provenance", + "git_blob": "9068f429896112082664455ab00bab083c99d1d8", + "sha256": "5ade59641f2ed70d045d6f60e89db7d979b1d1e9967f3acbe5c56eac81312841" + }, + { + "path": "research/native-transpose-owned/source/owned/RESULT.json", + "usage": "input", + "git_blob": "b6c9cd0da1889ed92f3f1066127a203246f303d8", + "sha256": "d6a99bd75c6b7a2146b0fc4cfa038890aaf1d4adcdef42d767fdb40b687e61aa", + "pin": "head:5eb314069417db1f4305430b6b14f20e9251e509:research/native-transpose-owned/source/owned/RESULT.json", + "source_pin": "head:4bd6efa51a495a7c7b7754915cf0244e7e60969e:research/kappa-joint-relations-20261023/RESULT.json" + } + ] +} diff --git a/research/native-transpose-owned/TASK.json b/research/native-transpose-owned/TASK.json new file mode 100644 index 0000000000..c400de8086 --- /dev/null +++ b/research/native-transpose-owned/TASK.json @@ -0,0 +1,67 @@ +{ + "schema_version": 1, + "task_id": "complex-new-helper-inventory", + "priority_revision": 7, + "base_commit": "1ec1119972c9aefe42525172d07b332fcff81cb4", + "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": "Transpose the fixed PR5383 owned backward circuit into a forward supplier with the same reduced bill; prove its native phases, complete endpoint and kappa 0.00302725.", + "scope_change_reason": "The donor requested a meaningful complete improvement from the native theorem. The new work transports an existing owned construction between orientations. It does not search the separately claimed eight-center system; it consumes the released source.", + "bottleneck_link": "The p16 controller still pays for two unreduced forward calls. Native transposition removes their extra eight H1 and eight H8 jobs while debiting their eight H9 helpers.", + "budget_minutes": 180, + "stop_rule": "Publish only after exact complete native, physical phase, completion, compiler and outer gates pass. The donor requested continued work until a verified improvement.", + "outcome": "completed", + "evidence": "641-column transpose and native checks, 2847 paid phase classes, 180 native warp classes, complete p16 census and exact outer admission.", + "author": "Ali Romman", + "ai_assistance": "Substantial OpenAI Codex assistance. No subagents, independent human review or proof-kernel acceptance.", + "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/5125#discussioncomment-19154367", + "open_questions": [ + { + "question": "Apply the transposition construction to a new, independently verified backward supplier.", + "why_it_matters": "Every later backward-only saving can also reduce the two forward bills if its complete interface and owned fields satisfy this theorem.", + "first_step": "Pin the published complete backward word and verify its normalized interface before transposition.", + "blocked_by": "A stronger source word needs its own admission and complete pricing. No claim is made about unpublished sources." + } + ] +} diff --git a/research/native-transpose-owned/VERIFY.json b/research/native-transpose-owned/VERIFY.json new file mode 100644 index 0000000000..3711f7a1ef --- /dev/null +++ b/research/native-transpose-owned/VERIFY.json @@ -0,0 +1,51 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/kappa-round3-warp-20261022/ACTUAL-WORD.json.gz", + "research/kappa-round3-warp-20261022/PHASE-VALIDATION.json.gz", + "research/joint-helper-lattice/CONTROLLER.json", + "research/kappa-round6-compiler-tightening-20261022/ARITHMETIC.json", + "research/higher-moment-strictification/verify.py", + "research/kappa-rebuild/architecture/mixed_target_probe.py", + "research/query-thinned-controllers/RESULT.json", + "research/pr4359-p7-padding/dependencies/compiler-refill/endpoint.py", + "research/t74-native-fast/vendor/native/new/code/borrow/vendor/clifford/clifford_exact.py", + "research/native-transpose-owned/source/cutoff/native.py", + "research/native-transpose-owned/source/cutoff/native_identity.py", + "research/native-transpose-owned/source/cutoff/exact.py", + "research/native-transpose-owned/source/cutoff/check_certificate.py", + "research/native-transpose-owned/source/owned/native.py", + "research/native-transpose-owned/source/owned/WITNESS.json", + "research/native-transpose-owned/source/owned/RESULT.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 550, + "checks": "Complete owned transpose, separate native checker, all physical phase classes and full compiler/outer arithmetic." + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 550, + "checks": "Complete owned transpose, separate native checker, all physical phase classes and full compiler/outer arithmetic." + } + ] +} diff --git a/research/native-transpose-owned/WORD.json.gz b/research/native-transpose-owned/WORD.json.gz new file mode 100644 index 0000000000..0e7e5a84ad Binary files /dev/null and b/research/native-transpose-owned/WORD.json.gz differ diff --git a/research/native-transpose-owned/interface.py b/research/native-transpose-owned/interface.py new file mode 100644 index 0000000000..77596f3122 --- /dev/null +++ b/research/native-transpose-owned/interface.py @@ -0,0 +1,60 @@ +"""Check the complete local interface and scalar transposition rules. + +The normalized interfaces are retained from query-thinned-controllers. +The scalar transpose is classical. Apache-2.0; OpenAI Codex assistance. +""" +from fractions import Fraction as Q +from support import need + +def add(a,b): + out=dict(a) + for k,v in b.items(): + out[k]=out.get(k,0)+v + if not out[k]:del out[k] + return out + +def mul(a,b): + out={} + for (d,q),v in a.items(): + for (e,r),w in b.items():out=add(out,{(d+e,(q+r)%4):v*w}) + return out + +def matmul(a,b):return [[add(mul(a[i][0],b[0][j]),mul(a[i][1],b[1][j])) for j in range(2)] for i in range(2)] +def transpose(a):return [list(r) for r in zip(*a)] + +def run(): + zero={};one={(0,0):1};D={(1,0):1} + F=[[D,zero],[{(1,3):1},D]] + B=[[D,{(1,1):-1}],[zero,D]] + J=[[{(0,2):1},zero],[zero,{(0,0):-1}]] + need(matmul(matmul(J,transpose(B)),J)==F,'Exact complete forward interface') + wrong=[[one,zero],[zero,{(0,0):-1}]] + need(matmul(matmul(wrong,transpose(B)),wrong)!=F,'Q squared correction is necessary') + need(matmul(matmul(J,B),J)!=F,'Circuit order and linear transpose are necessary') + # Check overwritten COPY, CLEAR and ADD as complete two-register maps. + def product(a,b):return [[sum(a[i][k]*b[k][j] for k in range(2)) for j in range(2)] for i in range(2)] + clear=[[0,0],[0,1]];copy=[[0,1],[0,1]] + clearT=transpose(clear) + need(clearT==clear,'Owned CLEAR transpose') + samples=0 + for c in (Q(-3,4),Q(-1),Q(1,4),Q(1),Q(2)): + A=[[1,c],[0,1]];T=[[1,0],[c,1]] + need(transpose(A)==T,'ADD transpose coefficient') + S=[[c,0],[0,1]];need(transpose(S)==S,'SCALE transpose') + samples+=1 + need(product(clear,[[1,0],[1,1]])==transpose(copy),'COPY transpose is ADD then CLEAR') + from native import Native + from native_identity import decide + from check_certificate import check + phase=Native.identity(9).json();phase['phase']=2 + problem={'axes':9,'roles':1,'generators':{'minus':phase}, + 'program':[{'op':'apply','dst':0,'generator':'minus'}], + 'reference':[{'op':'scale','dst':0,'coefficient':-1}]} + certificate=decide(problem) + need(certificate['status']=='COUNTEREXAMPLE','Scalar sign must stay outside tensor powers') + check(problem,certificate) + # The matrix polynomial is valid for every commuting symmetric Q,D with Q^4=I. + return {'identity':'F = J B^T J; J = diag(Q^2,-I)', + 'Q_exponents_modulus':4,'D_exponent_is_formal':True, + 'scalar_coefficients_checked':samples,'copy_and_clear_checked':True, + 'wrong_Q_correction_rejected':True,'missing_transpose_rejected':True,'scalar_sign_counterexample':certificate} diff --git a/research/native-transpose-owned/phases.py b/research/native-transpose-owned/phases.py new file mode 100644 index 0000000000..ea31c96324 --- /dev/null +++ b/research/native-transpose-owned/phases.py @@ -0,0 +1,103 @@ +"""Check physical transposition and exact phase recipes on source classes. + +Uses the credited exact Clifford compiler. Ali Romman with OpenAI Codex +assistance. Apache-2.0. +""" +from collections import Counter +from hashlib import sha256 +from copy import deepcopy +import json +from support import HERE,ROOT,read,need,load,CE,packed +ce=load(CE,'transpose_exact_clifford') + +def primitive(n,e,conjugate=False): + tag=e[0] + if tag=='P':return ce.perm(n,tuple(e[1])) + if tag=='D':return ce.diag(n,tuple(e[1]),tuple((-v)%4 for v in e[2]) if conjugate else tuple(e[2])) + if tag=='C':return ce.cgate(n,e[1],-e[2] if conjugate else e[2]) + if tag=='X':return ce.xgate(n,e[1]) + if tag=='phase': + k=(-e[1] if conjugate else e[1])%4 + return ce.Op(n,ce.identity(n),[('phase',k)]) + raise ValueError(tag) + +def conj(op): + ans=ce.ident(op.n) + for e in op.circuit:ans=ans.then(primitive(op.n,e,True)) + return ans + +def trans(op): + ans=ce.ident(op.n) + for e in reversed(op.circuit): + if e[0]=='P':e=('P',ce.inv(tuple(e[1]),op.n)) + ans=ans.then(primitive(op.n,e)) + return ans + +def decode(r): + from native import Native + Native.parse({k:list(v) if isinstance(v,tuple) else v for k,v in r.items()},9) + n=len(r['matrix_rows']) + q=tuple(r['quadratic_rows']);a=r['linear_Z4'] + need(ce.transpose(q,n)==q and all(a[i]%2==((q[i]>>i)&1) for i in range(n)),'Valid symmetric Gaussian phase recipe') + return ce.diag(n,tuple(r['quadratic_rows']),tuple(r['linear_Z4'])).then(ce.perm(n,tuple(r['matrix_rows']))).then(ce.xgate(n,r['offset'])).then(primitive(n,('phase',r['phase']))) + + +def run(x): + c=x['canonical'];p=x['programs']['backward'] + from word import base + candidate=base.construct(x)['programs']['backward'] + expected=sorted({(e[3],e[4],e[5]) for e in candidate if e[0]=='climb'}|{(e[2],e[3],e[4]) for e in candidate if e[0]=='center'}) + receipts=read(HERE/'PHASES.json.gz') + need([(r['old'],r['new'],r['rank']) for r in receipts]==expected,'Every transposed paid class exactly once') + frames={} + def frame(i): + if i not in frames:frames[i]=ce.canonical_frame(9,c['frames'][i]) + return frames[i] + def check_paid(row): + a,b,r=row['old'],row['new'],row['rank'] + want=trans(conj(frame(a).adjoint().then(frame(b)))) + physical=decode(row['right']).then(ce.fourier(9,range(r))).then(decode(row['left'])) + need(physical.tab==want.tab and physical.zero_state()==want.zero_state(),'Transposed paid absolute phase') + need(ce.rank([a for a,b,p in want.tab[9:]])==r,'Exact transposed paid rank') + for i,row in enumerate(receipts): + check_paid(row) + if i%500==0:print('PAID_PHASES',i+1,len(receipts),flush=True) + maps={} + for w in c['warps']: + G=ce.transpose(tuple(w['G_columns']),9);tr=ce.transpose(ce.inv(G,9),9) + q=tuple((1<0 else maps[abs(op)].adjoint() + old=conj(frame(a).adjoint().then(K).then(frame(b))) + want=trans(old) + new=frame(b).adjoint().then(K.adjoint()).then(frame(a)) + need(want.tab==new.tab and want.zero_state()==new.zero_state(),'Exact inverse primal native warp') + _,original=ce.monomial(old);_,changed=ce.monomial(want) + def parse(r):return Native.parse({k:list(v) if isinstance(v,tuple) else v for k,v in r.items()},9) + oldn,newn=parse(original),parse(changed) + for a0 in range(512): + b0=oldn.image(a0) + need(newn.image(b0)==a0 and newn.exponent(b0)==oldn.exponent(a0),'Literal transpose entry and phase') + columns+=1 + bad=deepcopy(receipts[0]);bad['left']['phase']=(bad['left']['phase']+2)%4 + try:check_paid(bad) + except ValueError as error:control=str(error) + else:raise ValueError('Wrong absolute phase accepted') + # C_q is symmetric and C_q squared is the exact native translation X_q. + for q in c['ports']: + Q=ce.cgate(9,q);square=Q.then(Q);native=ce.xgate(9,q) + need(square.tab==native.tab and square.zero_state()==native.zero_state(),'All actual port Q squared phases') + need(trans(Q).tab==Q.tab and trans(Q).zero_state()==Q.zero_state(),'Symmetric port Gaussian') + for rank in (4,7,8,9): + C=ce.fourier(9,range(rank));T=trans(C) + need(C.tab==T.tab and C.zero_state()==T.zero_state(),'Every productive standard Gaussian is symmetric') + fixed=conj(C).then(ce.xgate(9,(1< 0, 'Changed invoice beats the prior raw root upper endpoint') + source_open_T,source_open_P=Counter(T),Counter(P) + source_open_T[9]+=16;source_open_P[1]+=16;source_open_P[8]+=16 + source_open=read(HERE / 'source/owned/RESULT.json')['arithmetic'] + source_open_upper=Q(source_open['raw_root_interval'][1]) + need(Q(source_open['kappa'])==Q('.00302666') and source_open_upper==Q('0.00302667476808'), 'Pinned PR5383 complete bound') + need(source_open_T==Counter({int(r): n for r,n in source_open['targets'].items()}) and source_open_P==Counter({int(r): n for r,n in source_open['paid'].items()}), 'Exact complete PR5383 profile') + need(E.moment(source_open_T,1-source_open_upper)[1] < E.moment(source_open_P,1-source_open_upper)[0], 'Published PR5383 root upper sign') + need(margin(source_open_upper)[0]>0,'New complete profile beats PR5383 raw crossing') + lo, hi, grid = 0, 10**12, 10**14 + while hi - lo > 1: + mid = (lo + hi) // 2 + if margin(Q(mid, grid))[0] > 0: lo = mid + else: hi = mid + root_low, root_high = Q(lo, grid), Q(hi, grid) + need(margin(root_low)[0] > 0 and margin(root_high)[1] < 0, 'Strict rational root enclosure') + need(PREVIOUS < KAPPA < TESTED < root_low, 'New bound and explicit compiler headroom') + # The complete signed profile decreases on [0, .05], and stays negative + # on [.05, 1]. This proves a fixed-profile ceiling, not a circuit ceiling. + signed = {r: T[r] - P[r] for r in T.keys() | P.keys()} + derivative, upper = None, 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) + for i in range(128): + l, r = Q(1, 20) + Q(19 * i, 2560), Q(1, 20) + Q(19 * (i + 1), 2560) + value = 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 = value if upper is None else max(upper, value) + need(derivative > 0 and upper < 0, 'Fixed-profile ceiling on all 0 < kappa < 1') + t, u, v, c, b = 1 - TESTED, Q(1, 5), 1024, 20, 21 + target, paid = E.moment(T, t), E.moment(P, t) + tl, th = other.moment(T, TESTED); pl, ph = other.moment(P, TESTED) + need(tl > ph and max(tl, target[0]) <= min(th, target[1]) and max(pl, paid[0]) <= min(ph, paid[1]), 'Two exact interval engines agree') + alpha = E.divide(paid, target) + 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)) + reserve = Q(1, 10**9); g = d = Q(97, 100) + need(alpha[1] < 1 - reserve and gamma[1] < g and delta[1] < d, 'Original and completion tails charged') + need(g**128 < Q(1, 16) and d**128 < Q(1, 16), 'Two strict tail decay blocks') + normalized = 1 / (1 + v * reserve) + Q(4, 2**32) + need(normalized < 1 and c**64 < b**63, 'Paid completion, splitting and rounding') + theta, power = Q(63, 64), 1000 + eta = E.scale(E.power(145, -v * TESTED), t) + need(2 * (20**v)**64 <= (145**v)**63 and eta[0] > theta**power, 'Shifted exits and complement capacity') + need(E.power(145, v * TESTED)[1] < 2**power, 'Compiler initial range') + gap = (TESTED - KAPPA) / 7; need(gap.numerator == 1, 'Finite integer grid') + step = gap.denominator + def wins(j): return (step * j + 1)**power < 2**j + left, right = 1, 2 + while not wins(right): left, right = right, 2 * right + while right - left > 1: + mid = (left + right) // 2 + if wins(mid): right = mid + else: left = mid + height = step * right + need(height > 8 * v and wins(right) and not wins(right - 1), 'Finite uniform-rank threshold') + local_scalar = max(x['real_scalar_allowance'] for x in native.values()) + # Double the source route allowance, including all owned field lifetimes. + # COPY splits into ADD and CLEAR. Add each boundary and helper pass. + routes = (2 * (sum(OLD_PAID.values()) + 2 * 408 + 688 + 32) + 2 * 112 + 400) * 1000 + need(local_scalar + routes < 2 * 10**7, 'All new preparation, COPY, CLEAR and fixed routes fit') + scalar_upper = 18 * 2 * 10**7 + 15 * 1792 + 32 * 112 * (len(word['physical_events']) + sum(len(word['boundaries'][k + '_program']) for k in ('left', 'right'))) + need(scalar_upper < 10**9, 'Complete raw nonrecursive bound') + bit = 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, 'Retained stronger BIT admission and stock') + L = load('research/pr4359-p7-padding/dependencies/compiler-refill/endpoint.py', 'owned_relation_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': 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 outer inequality is strict') + 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 outer patch ' + name); controls[name] = failed + bad_native = {d: dict(x) for d, x in native.items()} + bad_native['backward']['helpers'] = OLD_HELPERS + try: assemble(bad_native, word) + except ValueError: controls['unearned_helper_credit'] = 'Rejected by the independent complete census' + else: raise ValueError('Unowned helper credit was accepted') + return encode({'kappa': KAPPA, 'kappa_decimal': '.00302725', 'gain_over_PR4610': KAPPA - PREVIOUS, 'gain_over_PR5383': KAPPA-Q('.00302666'), + 'PR5383_raw_root_upper': source_open_upper, 'margin_at_PR5383_raw_root_upper': E.display(margin(source_open_upper)), + 'raw_root_interval': [root_low, root_high], 'raw_headroom': [root_low - KAPPA, root_high - KAPPA], + 'margin_at_previous_kappa': E.display(margin(PREVIOUS)), + 'margin_at_previous_root_upper': E.display(margin(OLD_ROOT_UPPER)), + 'fixed_profile_ceiling': {'decreasing_through': Q(1, 20), 'derivative_upper': E.display((-derivative,) * 2), 'remaining_interval_moment_upper': E.display((upper,) * 2)}, + 'targets': T, 'paid': P, 'productive_fields': sum(T.values()), 'paid_calls': sum(P.values()), 'rank_mass_surplus': 752, + 'full_backward': 16, 'full_forward': 2, 'query_shears': 15, + 'strictification': {'tested': TESTED, 'power': v, 'cutoff': c, 'floor': b, 'tail_offset': u, 'reserve': reserve, 'alpha': E.display(alpha), 'gamma': E.display(gamma), 'delta': E.display(delta), 'normalized_paid_upper': normalized}, + 'compiler': {'theta': theta, 'logarithm_power': power, 'eta': E.display(eta), 'gap': gap, 'uniform_saving': params['complex_uniform_saving'], 'H': height, 'N': '2^' + str(height), 'integer_test_exponent': right, 'word_materialized': False}, + 'nonrecursive': {'local_scalar': local_scalar, 'local_routes': routes, 'raw_scalar_upper': scalar_upper, 'raw_budget': 10**9, 'additional_private_slots': 8, 'owned_slots_per_direction': 17}, + 'ordinary_BIT': bit, 'outer': outer, 'negative_controls': controls}) diff --git a/research/native-transpose-owned/source/NOTICE.md b/research/native-transpose-owned/source/NOTICE.md new file mode 100644 index 0000000000..97dacf2cd0 --- /dev/null +++ b/research/native-transpose-owned/source/NOTICE.md @@ -0,0 +1,10 @@ +# Copied source files + +Apache-2.0. Preserve the source headers. No copied source file is modified. + +- `owned/native.py` and its unchanged `WITNESS.json`: Ali Romman's [PR5383 native construction](https://github.com/aliromman/integer-mult-bounds/blob/4bd6efa51a495a7c7b7754915cf0244e7e60969e/research/kappa-joint-relations-20261023/native.py). Only its pure construction, scalar allowance and exact row replay functions are called. The package's independent pins bind its source inputs. Its original notices credit Cao Yifan, Cinna Davis and zxv. +- `cutoff/exact.py`, `cutoff/native.py`, `cutoff/native_identity.py` and `cutoff/check_certificate.py`: Ali Romman's [PR5369 native tensor package](https://github.com/aliromman/integer-mult-bounds/tree/18354f41de4dc7bfda4692e814cf1d91a6d619ef/research/native-tensor-cutoff). The [complete proof and source credit](https://github.com/aliromman/integer-mult-bounds/blob/18354f41de4dc7bfda4692e814cf1d91a6d619ef/research/native-tensor-cutoff/PROOF.md) retain the native recipe lineage of Jose Manuel/jmbarrancoml, Douglas Colkitt and the listed contributors, plus the classical Fourier, binary Gram factorization, finite-group, Cook and Barrington results. This package uses the positive identity decision and the separately implemented certificate checker. It does not claim those results as new. + +The local `price.py` is an adapted version of the [PR5377 complete price engine](https://github.com/aliromman/integer-mult-bounds/blob/c448d13c71908647f968b06cddb795ce7d288139/research/kappa-owned-relation-20261023/price.py). Its notice credits Cao Yifan, Cinna Davis, zxv and Jacob Alan Sussman. The new census debits the eight owned helpers in all 18 full calls and includes every forward transpose wrapper. + +Substantial OpenAI Codex assistance was used in both source packages and in this contribution. Source links are fixed commits; SOURCES.json records each copied blob and byte hash. diff --git a/research/native-transpose-owned/source/cutoff/check_certificate.py b/research/native-transpose-owned/source/cutoff/check_certificate.py new file mode 100644 index 0000000000..929ccceeff --- /dev/null +++ b/research/native-transpose-owned/source/cutoff/check_certificate.py @@ -0,0 +1,244 @@ +"""Check certificates without importing the producer or its native algebra.""" +import argparse +import hashlib +import json +from pathlib import Path +import sys +sys.path.insert(0, str(Path(__file__).resolve().parent)) +from exact import QI, need, scalar, unit + + +def dot(row, x): + return (row & x).bit_count() % 2 + + +def image(g, x): + return sum(dot(row, x) << i for i, row in enumerate(g[0])) ^ g[1] + + +def exponent(g, x): + return (g[2] + sum(g[3][i] for i in range(len(g[0])) if x & (1 << i)) + + 2 * sum(1 for i in range(len(g[0])) for j in range(i + 1, len(g[0])) + if x & (1 << i) and x & (1 << j) and g[4][i] & (1 << j))) % 4 + + +def invert_matrix(rows): + size = len(rows) + a, b = list(rows), [1 << i for i in range(size)] + for col in range(size): + choices = [i for i in range(col, size) if a[i] & (1 << col)] + need(bool(choices), 'checker: singular matrix') + i = choices[0] + a[col], a[i], b[col], b[i] = a[i], a[col], b[i], b[col] + for row in range(size): + if row != col and a[row] & (1 << col): + a[row] ^= a[col] + b[row] ^= b[col] + return tuple(b) + + +def normalize(data, n): + need(isinstance(data, dict) and set(data) == {'matrix_rows', 'offset', 'phase', 'linear_Z4', 'quadratic_rows'}, + 'checker: native fields') + a, p, q = data['matrix_rows'], data['linear_Z4'], data['quadratic_rows'] + need(all(isinstance(x, list) and len(x) == n for x in (a, p, q)), 'checker: native dimensions') + need(all(type(x) is int and 0 <= x < (1 << n) for x in a + q), 'checker: binary rows') + need(all(type(x) is int and 0 <= x < 4 for x in p), 'checker: linear phases') + need(type(data['offset']) is int and 0 <= data['offset'] < (1 << n), 'checker: offset') + need(type(data['phase']) is int and 0 <= data['phase'] < 4, 'checker: phase') + invert_matrix(a) + return (tuple(a), data['offset'], data['phase'], tuple(p), + tuple(q[i] & ~((1 << (i + 1)) - 1) for i in range(n))) + + +def problem_data(problem): + need(isinstance(problem, dict) and set(problem) == {'axes', 'roles', 'generators', 'program', 'reference'}, + 'checker: problem fields') + n, r = problem['axes'], problem['roles'] + need(type(n) is int and 1 <= n <= 256 and type(r) is int and 1 <= r <= 4096, + 'checker: dimensions') + need(isinstance(problem['generators'], dict), 'checker: generator table') + gs = {} + for name, value in problem['generators'].items(): + need(isinstance(name, str) and bool(name), 'checker: generator name') + gs[name] = normalize(value, n) + fields = {'add': {'op', 'src', 'dst', 'coefficient'}, + 'query': {'op', 'src', 'dst', 'coefficient', 'generator', 'inverse'}, + 'apply': {'op', 'dst', 'generator', 'inverse'}, + 'scale': {'op', 'dst', 'coefficient'}, 'swap': {'op', 'src', 'dst'}} + for code in (problem['program'], problem['reference']): + need(isinstance(code, list), 'checker: instruction list') + for ins in code: + need(isinstance(ins, dict), 'checker: instruction object') + op = ins.get('op') + need(isinstance(op, str) and op in fields and set(ins) <= fields[op], 'checker: instruction fields') + for key in (('src', 'dst') if op in ('add', 'query', 'swap') else ('dst',)): + need(type(ins.get(key)) is int and 0 <= ins[key] < r, 'checker: role') + if op in ('apply', 'query'): + need(isinstance(ins.get('generator'), str) and ins['generator'] in gs, 'checker: generator') + need(type(ins.get('inverse', False)) is bool, 'checker: inverse flag') + if 'coefficient' in ins: + scalar(ins['coefficient']) + return gs + + +def compose(g, h): + """Expand affine Boolean forms modulo four, without interpolation.""" + n = len(g[0]) + a = [] + for row in g[0]: + out = 0 + for j in range(n): + if row & (1 << j): + out ^= h[0][j] + a.append(out) + constant = h[2] + g[2] + linear = list(h[3]) + quad = [[2 * ((h[4][j] >> k) & 1) for k in range(n)] for j in range(n)] + bits = [[(row >> j) & 1 for j in range(n)] for row in h[0]] + shifts = [(h[1] >> i) & 1 for i in range(n)] + for i in range(n): + coefficient, t = g[3][i], shifts[i] + constant += coefficient * t + for j in range(n): + linear[j] += coefficient * (1 - 2 * t) * bits[i][j] + for k in range(j + 1, n): + quad[j][k] -= 2 * coefficient * bits[i][j] * bits[i][k] + for l in range(i + 1, n): + if not (g[4][i] >> l & 1): + continue + u = shifts[l] + constant += 2 * t * u + for j in range(n): + linear[j] += 2 * (t * bits[l][j] + u * bits[i][j] + bits[i][j] * bits[l][j]) + for k in range(j + 1, n): + quad[j][k] += 2 * (bits[i][j] * bits[l][k] + bits[i][k] * bits[l][j]) + return (tuple(a), image(g, h[1]), constant % 4, tuple(x % 4 for x in linear), + tuple(sum(((quad[j][k] % 4) // 2) << k for k in range(j + 1, n)) for j in range(n))) + + +def inverse(g): + n = len(g[0]) + rows = invert_matrix(g[0]) + offset = sum(dot(row, g[1]) << i for i, row in enumerate(rows)) + h = (rows, offset, 0, (0,) * n, (0,) * n) + phase = compose(g, h) + return (rows, offset, -phase[2] % 4, tuple(-x % 4 for x in phase[3]), phase[4]) + + +def accumulate(row, key, value): + if key in row: + value = value + row[key] + if value: + row[key] = value + elif key in row: + del row[key] + + +def algebra_endpoint(problem, code, generators, max_terms): + n, r = problem['axes'], problem['roles'] + need(type(max_terms) is int and max_terms >= r, 'checker: expanded-term limit; no decision') + identity = (tuple(1 << i for i in range(n)), 0, 0, (0,) * n, (0,) * n) + state = [{(i, identity): QI(1)} for i in range(r)] + for ins in code: + op, d = ins['op'], ins['dst'] + if op == 'swap': + s = ins['src'] + state[s], state[d] = state[d], state[s] + elif op == 'scale': + c = scalar(ins.get('coefficient', 1)) + state[d] = {k: c * v for k, v in state[d].items()} if c else {} + else: + s = d if op == 'apply' else ins['src'] + old = list(state[s].items()) + if op != 'add': + g = generators[ins['generator']] + if ins.get('inverse', False): + g = inverse(g) + old = [((i, compose(g, h)), c) for (i, h), c in old] + if op == 'apply': + state[d] = {} + c = scalar(ins.get('coefficient', 1)) + for key, value in old: + accumulate(state[d], key, c * value) + need(sum(len(row) for row in state) <= max_terms, 'checker: expanded-term limit; no decision') + return state + + +def literal_endpoint(problem, code, generators, input_role, points, max_terms): + """Run literal tensor basis actions. No group products or Gram factors are used.""" + state = [{} for _ in range(problem['roles'])] + state[input_role][tuple(points)] = QI(1) + for ins in code: + op, d = ins['op'], ins['dst'] + if op == 'swap': + s = ins['src'] + state[s], state[d] = state[d], state[s] + elif op == 'scale': + c = scalar(ins.get('coefficient', 1)) + state[d] = {k: c * v for k, v in state[d].items()} if c else {} + else: + s = d if op == 'apply' else ins['src'] + old = list(state[s].items()) + if op != 'add': + g = generators[ins['generator']] + if ins.get('inverse', False): + rows = invert_matrix(g[0]) + moved = [] + for xs, value in old: + ys = tuple(sum(dot(row, x ^ g[1]) << j for j, row in enumerate(rows)) for x in xs) + moved.append((ys, value * unit(-sum(exponent(g, y) for y in ys)))) + else: + moved = [(tuple(image(g, x) for x in xs), value * unit(sum(exponent(g, x) for x in xs))) + for xs, value in old] + old = moved + if op == 'apply': + state[d] = {} + c = scalar(ins.get('coefficient', 1)) + for xs, value in old: + accumulate(state[d], xs, c * value) + need(sum(map(len, state)) <= max_terms, 'checker: literal-term limit; no decision') + return state + + +def check(problem, certificate, max_terms=100000): + need(isinstance(certificate, dict), 'checker: certificate object') + need(type(max_terms) is int and max_terms >= 1, 'checker: positive term limit') + generators = problem_data(problem) + digest = hashlib.sha256(json.dumps(problem, sort_keys=True, separators=(',', ':')).encode()).hexdigest() + need(certificate.get('schema') == 'native-tensor-cutoff/v1' and certificate.get('problem_sha256') == digest, + 'checker: certificate binding') + n, r = problem['axes'], problem['roles'] + need(certificate.get('axes') == n and certificate.get('roles') == r and + certificate.get('window') == [2 * n + 4, 2 * n + 7], 'checker: certificate dimensions') + if certificate.get('status') == 'IDENTITY_ALL_POSITIVE_WIDTHS': + a = algebra_endpoint(problem, problem['program'], generators, max_terms) + b = algebra_endpoint(problem, problem['reference'], generators, max_terms) + need(a == b and certificate.get('residual_terms') == 0, 'checker: complete native endpoints differ') + return 'PASS_NATIVE_IDENTITY_ALL_POSITIVE_WIDTHS' + need(certificate.get('status') == 'COUNTEREXAMPLE', 'checker: status') + xs, ys = certificate.get('input_points'), certificate.get('output_points') + need(isinstance(xs, list) and isinstance(ys, list) and len(xs) == len(ys) and + 2 * n + 4 <= len(xs) <= 2 * n + 7, 'checker: witness width') + need(all(type(x) is int and 0 <= x < 1 << n for x in xs + ys), 'checker: witness coordinates') + i, o = certificate.get('input_role'), certificate.get('output_role') + need(type(i) is int and 0 <= i < r and type(o) is int and 0 <= o < r, 'checker: witness roles') + a = literal_endpoint(problem, problem['program'], generators, i, xs, max_terms) + b = literal_endpoint(problem, problem['reference'], generators, i, xs, max_terms) + observed = a[o].get(tuple(ys), QI()) - b[o].get(tuple(ys), QI()) + need(bool(observed) and observed == scalar(certificate.get('discrepancy')), 'checker: witness discrepancy') + return 'PASS_NATIVE_TENSOR_COUNTEREXAMPLE' + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('problem', type=Path) + parser.add_argument('certificate', type=Path) + parser.add_argument('--max-terms', type=int, default=100000) + args = parser.parse_args() + need(args.max_terms >= 1, 'positive checker term limit') + print(check(json.loads(args.problem.read_text()), json.loads(args.certificate.read_text()), args.max_terms)) + + +if __name__ == '__main__': + main() diff --git a/research/native-transpose-owned/source/cutoff/exact.py b/research/native-transpose-owned/source/cutoff/exact.py new file mode 100644 index 0000000000..4f8514d1a2 --- /dev/null +++ b/research/native-transpose-owned/source/cutoff/exact.py @@ -0,0 +1,68 @@ +"""Exact Gaussian rational arithmetic shared by the two checkers.""" +from fractions import Fraction +import re + + +class QI: + __slots__ = ('real', 'imag') + + def __init__(self, real=0, imag=0): + if isinstance(real, QI): + self.real, self.imag = real.real, real.imag + else: + self.real, self.imag = Fraction(real), Fraction(imag) + + def __add__(self, other): + other = QI(other) + return QI(self.real + other.real, self.imag + other.imag) + + __radd__ = __add__ + + def __neg__(self): + return QI(-self.real, -self.imag) + + def __sub__(self, other): + return self + -QI(other) + + def __mul__(self, other): + other = QI(other) + return QI(self.real * other.real - self.imag * other.imag, + self.real * other.imag + self.imag * other.real) + + __rmul__ = __mul__ + + def __eq__(self, other): + if not isinstance(other, (QI, int, Fraction)): + return False + other = QI(other) + return self.real == other.real and self.imag == other.imag + + def __bool__(self): + return bool(self.real or self.imag) + + def json(self): + return [str(self.real), str(self.imag)] + + +def scalar(value): + """Accept integers, rational strings, or two such components. Reject floats.""" + def component(x): + if type(x) is int: + return Fraction(x) + if isinstance(x, str) and re.fullmatch(r'[+-]?[0-9]+(?:/[+-]?[0-9]+)?', x): + return Fraction(x) + raise ValueError('explicit integer or rational component required') + if type(value) is int or isinstance(value, str): + return QI(component(value)) + if isinstance(value, list) and len(value) == 2: + return QI(component(value[0]), component(value[1])) + raise ValueError('exact Gaussian coefficient required') + + +def unit(power): + return (QI(1), QI(0, 1), QI(-1), QI(0, -1))[power % 4] + + +def need(condition, message): + if not condition: + raise ValueError(message) diff --git a/research/native-transpose-owned/source/cutoff/native.py b/research/native-transpose-owned/source/cutoff/native.py new file mode 100644 index 0000000000..8872f540e1 --- /dev/null +++ b/research/native-transpose-owned/source/cutoff/native.py @@ -0,0 +1,193 @@ +"""Canonical affine maps with quadratic Gaussian phases.""" +from dataclasses import dataclass +from exact import need + + +def parity(x): + return x.bit_count() & 1 + + +def act(rows, x): + return sum(parity(row & x) << j for j, row in enumerate(rows)) + + +def inverse(rows): + n = len(rows) + work = [row | (1 << (n + i)) for i, row in enumerate(rows)] + for j in range(n): + p = next((k for k in range(j, n) if work[k] >> j & 1), None) + need(p is not None, 'invertible binary matrix required') + work[j], work[p] = work[p], work[j] + for k in range(n): + if k != j and work[k] >> j & 1: + work[k] ^= work[j] + return tuple(x >> n for x in work) + + +def matrix_product(left, right): + result = [] + for row in left: + value = 0 + for j, other in enumerate(right): + if row >> j & 1: + value ^= other + result.append(value) + return tuple(result) + + +@dataclass(frozen=True) +class Native: + rows: tuple + offset: int + phase: int + linear: tuple + quadratic: tuple + + @property + def n(self): + return len(self.rows) + + @classmethod + def identity(cls, n): + return cls(tuple(1 << j for j in range(n)), 0, 0, (0,) * n, (0,) * n) + + @classmethod + def parse(cls, data, n): + need(isinstance(data, dict), 'native recipe object required') + need(set(data) == {'matrix_rows', 'offset', 'phase', 'linear_Z4', 'quadratic_rows'}, + 'exact native recipe fields required') + rows, linear, quadratic = (data[k] for k in ('matrix_rows', 'linear_Z4', 'quadratic_rows')) + need(all(isinstance(x, list) and len(x) == n for x in (rows, linear, quadratic)), + 'native recipe dimension') + need(all(type(x) is int and 0 <= x < 1 << n for x in rows + quadratic), + 'binary row extent') + need(all(type(x) is int and 0 <= x < 4 for x in linear), 'linear phase extent') + need(type(data['offset']) is int and 0 <= data['offset'] < 1 << n, 'offset extent') + need(type(data['phase']) is int and 0 <= data['phase'] < 4, 'constant phase extent') + inverse(rows) + # The source convention ignores diagonal and lower quadratic entries. + quadratic = tuple(row & ~((1 << (j + 1)) - 1) for j, row in enumerate(quadratic)) + return cls(tuple(rows), data['offset'], data['phase'], tuple(linear), quadratic) + + def json(self): + return {'matrix_rows': list(self.rows), 'offset': self.offset, 'phase': self.phase, + 'linear_Z4': list(self.linear), 'quadratic_rows': list(self.quadratic)} + + def image(self, x): + return act(self.rows, x) ^ self.offset + + def exponent(self, x): + return (self.phase + sum(self.linear[i] for i in range(self.n) if x >> i & 1) + + 2 * sum(parity(self.quadratic[i] & x) for i in range(self.n) if x >> i & 1)) % 4 + + @classmethod + def from_function(cls, rows, offset, phase_function): + n = len(rows) + c = phase_function(0) % 4 + a = tuple((phase_function(1 << i) - c) % 4 for i in range(n)) + quadratic = [] + for i in range(n): + row = 0 + for j in range(i + 1, n): + delta = (phase_function((1 << i) | (1 << j)) - c - a[i] - a[j]) % 4 + need(delta in (0, 2), 'quadratic phase parity') + row |= (delta // 2) << j + quadratic.append(row) + return cls(tuple(rows), offset, c, a, tuple(quadratic)) + + def compose(self, right): + """Apply right first, then this map. Scalars stay outside this operation.""" + need(self.n == right.n, 'composition dimension') + return Native.from_function(matrix_product(self.rows, right.rows), + act(self.rows, right.offset) ^ self.offset, + lambda x: right.exponent(x) + self.exponent(right.image(x))) + + def inv(self): + rows = inverse(self.rows) + offset = act(rows, self.offset) + return Native.from_function(rows, offset, lambda x: -self.exponent(act(rows, x) ^ offset)) + + def phase_key(self): + return ((self.phase,) + self.linear + + tuple((self.quadratic[i] >> j) & 1 for i in range(self.n) for j in range(i + 1, self.n))) + + +def gram_factor(rows): + """Return at most n+1 columns whose binary outer products sum to rows.""" + n = len(rows) + need(all(0 <= r < 1 << n for r in rows), 'Gram row extent') + need(all(((rows[i] >> j) & 1) == ((rows[j] >> i) & 1) + for i in range(n) for j in range(n)), 'symmetric Gram matrix') + + def pair(x, y): + return parity(x & act(rows, y)) + + pending = [1 << i for i in range(n)] + singles, pairs = [], [] + while pending: + p = next((i for i, v in enumerate(pending) if pair(v, v)), None) + if p is not None: + v = pending.pop(p) + singles.append(v) + pending = [w ^ (v if pair(v, w) else 0) for w in pending] + continue + hit = next(((i, j) for i in range(len(pending)) for j in range(i + 1, len(pending)) + if pair(pending[i], pending[j])), None) + if hit is None: + break + i, j = hit + v, w = pending[i], pending[j] + pairs.append((v, w)) + pending = [u ^ (v if pair(u, w) else 0) ^ (w if pair(u, v) else 0) + for k, u in enumerate(pending) if k not in (i, j)] + + basis = singles + [v for pair_ in pairs for v in pair_] + pending + a, b = len(singles), len(pairs) + rank = a + 2 * b + width = rank + bool(b) + # Even-weight vectors in odd dimension have a nonsingular alternating form. + even = [(1 << i) | (1 << (2 * b)) for i in range(2 * b)] + hyperbolic = [] + while even: + v = even.pop(0) + j = next(j for j, w in enumerate(even) if parity(v & w)) + w = even.pop(j) + hyperbolic.extend((v, w)) + even = [u ^ (v if parity(u & w) else 0) ^ (w if parity(u & v) else 0) for u in even] + canonical = ([1 << i for i in range(a)] + [v << a for v in hyperbolic] + + [0] * len(pending)) + undo = inverse(basis) + vectors = [] + for row in undo: + value = 0 + for j in range(n): + if row >> j & 1: + value ^= canonical[j] + vectors.append(value) + return [sum(((vectors[i] >> j) & 1) << i for i in range(n)) for j in range(width)] + + +def character_tuple(n, character, floor=None): + """Realize one phase character on an affinely spanning tuple.""" + need(len(character) == 1 + n + n * (n - 1) // 2, 'phase character dimension') + need(all(type(x) is int and 0 <= x < 4 for x in character[:n + 1]) and + all(type(x) is int and x in (0, 1) for x in character[n + 1:]), 'phase character extent') + floor = 2 * n + 4 if floor is None else floor + need(type(floor) is int and floor >= 2 * n + 4, 'tensor window floor') + c, a = character[0], character[1:n + 1] + rows = [((a[i] & 1) ^ 1) << i for i in range(n)] + k = n + 1 + for i in range(n): + for j in range(i + 1, n): + rows[i] |= character[k] << j + rows[j] |= character[k] << i + k += 1 + points = [0] + [1 << i for i in range(n)] + gram_factor(rows) + counts = [sum((x >> i) & 1 for x in points) % 4 for i in range(n)] + need(all((a[i] - counts[i]) % 2 == 0 for i in range(n)), 'Gram parity invariant') + z = sum((((a[i] - counts[i]) % 4) // 2) << i for i in range(n)) + if z: + points.extend((z, z)) + f = floor + (c - floor) % 4 + need(len(points) <= f, 'proved tensor cutoff') + return points + [0] * (f - len(points)) diff --git a/research/native-transpose-owned/source/cutoff/native_identity.py b/research/native-transpose-owned/source/cutoff/native_identity.py new file mode 100644 index 0000000000..85376a935d --- /dev/null +++ b/research/native-transpose-owned/source/cutoff/native_identity.py @@ -0,0 +1,159 @@ +"""Decide complete dirty endpoints and produce a short native tensor witness.""" +import argparse +import hashlib +import json +from pathlib import Path +import sys +sys.path.insert(0, str(Path(__file__).resolve().parent)) +from exact import QI, need, scalar, unit +from native import Native, character_tuple + + +def digest(problem): + return hashlib.sha256(json.dumps(problem, sort_keys=True, separators=(',', ':')).encode()).hexdigest() + + +def validate(problem): + need(isinstance(problem, dict) and set(problem) == {'axes', 'roles', 'generators', 'program', 'reference'}, + 'exact problem fields required') + n, r = problem['axes'], problem['roles'] + need(type(n) is int and 1 <= n <= 256, 'axes must be in 1..256') + need(type(r) is int and 1 <= r <= 4096, 'roles must be in 1..4096') + need(isinstance(problem['generators'], dict), 'generator table required') + generators = {} + for name, data in problem['generators'].items(): + need(isinstance(name, str) and bool(name), 'generator name required') + generators[name] = Native.parse(data, n) + for program in (problem['program'], problem['reference']): + need(isinstance(program, list), 'instruction list required') + for instruction in program: + need(isinstance(instruction, dict), 'instruction object required') + op = instruction.get('op') + fields = {'add': {'op', 'src', 'dst', 'coefficient'}, + 'query': {'op', 'src', 'dst', 'coefficient', 'generator', 'inverse'}, + 'apply': {'op', 'dst', 'generator', 'inverse'}, + 'scale': {'op', 'dst', 'coefficient'}, + 'swap': {'op', 'src', 'dst'}} + need(isinstance(op, str) and op in fields and set(instruction) <= fields[op], 'instruction fields') + need('dst' in instruction, 'destination required') + if op in ('add', 'query', 'swap'): + need('src' in instruction, 'source required') + for key in ('src', 'dst'): + if key in instruction: + need(type(instruction[key]) is int and 0 <= instruction[key] < r, 'role index') + if op in ('query', 'apply'): + need(isinstance(instruction.get('generator'), str) and instruction['generator'] in generators, + 'known native generator required') + need(type(instruction.get('inverse', False)) is bool, 'inverse flag') + if 'coefficient' in instruction: + scalar(instruction['coefficient']) + return generators + + +def add_term(row, key, value): + new = row.get(key, QI()) + value + if new: + row[key] = new + else: + row.pop(key, None) + + +def endpoint(problem, instructions, generators, max_terms=100000): + need(type(max_terms) is int and max_terms >= problem['roles'], 'expanded-term limit exceeded; no decision') + identity = Native.identity(problem['axes']) + state = [{(i, identity): QI(1)} for i in range(problem['roles'])] + inverses = {} + peak = len(state) + for instruction in instructions: + op, d = instruction['op'], instruction['dst'] + if op == 'swap': + s = instruction['src'] + state[s], state[d] = state[d], state[s] + elif op == 'scale': + c = scalar(instruction.get('coefficient', 1)) + state[d] = {key: c * value for key, value in state[d].items()} if c else {} + else: + s = d if op == 'apply' else instruction['src'] + old = list(state[s].items()) + c = scalar(instruction.get('coefficient', 1)) + if op in ('apply', 'query'): + name = instruction['generator'] + g = generators[name] + if instruction.get('inverse', False): + if name not in inverses: + inverses[name] = g.inv() + g = inverses[name] + old = [((i, g.compose(h)), value) for (i, h), value in old] + if op == 'apply': + state[d] = {} + for key, value in old: + add_term(state[d], key, c * value) + size = sum(map(len, state)) + need(size <= max_terms, 'expanded-term limit exceeded; no decision') + peak = max(peak, size) + return state, peak + + +def choose_character(table, n): + """Choose a nonzero finite Fourier value without enumerating all characters.""" + moduli = [4] * (n + 1) + [2] * (n * (n - 1) // 2) + chosen = [] + for modulus in moduli: + for k in range(modulus): + reduced = {} + for key, coefficient in table.items(): + add_term(reduced, key[1:], coefficient * unit((4 // modulus) * k * key[0])) + if reduced: + table = reduced + chosen.append(k) + break + else: + raise ValueError('nonzero Fourier invariant failed') + need(set(table) == {()}, 'complete Fourier projection') + return chosen, table[()] + + +def decide(problem, max_terms=100000): + need(type(max_terms) is int and max_terms >= 1, 'positive expanded-term limit') + generators = validate(problem) + left, p = endpoint(problem, problem['program'], generators, max_terms) + right, q = endpoint(problem, problem['reference'], generators, max_terms) + residual = [] + for a, b in zip(left, right): + row = dict(a) + for key, value in b.items(): + add_term(row, key, -value) + residual.append(row) + n = problem['axes'] + result = {'schema': 'native-tensor-cutoff/v1', 'problem_sha256': digest(problem), + 'axes': n, 'roles': problem['roles'], 'window': [2 * n + 4, 2 * n + 7], + 'peak_expanded_terms': max(p, q), 'residual_terms': sum(map(len, residual))} + if not any(residual): + result['status'] = 'IDENTITY_ALL_POSITIVE_WIDTHS' + return result + o = next(i for i, row in enumerate(residual) if row) + source, g = next(iter(residual[o])) + table = {h.phase_key(): value for (i, h), value in residual[o].items() + if i == source and h.rows == g.rows and h.offset == g.offset} + character, amplitude = choose_character(table, n) + points = character_tuple(n, character) + result.update(status='COUNTEREXAMPLE', input_role=source, output_role=o, + input_points=points, output_points=[g.image(x) for x in points], + character=character, discrepancy=amplitude.json()) + return result + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('problem', type=Path) + parser.add_argument('--output', type=Path, required=True) + parser.add_argument('--max-terms', type=int, default=100000) + args = parser.parse_args() + need(args.max_terms >= 1, 'positive expanded-term limit') + result = decide(json.loads(args.problem.read_text()), args.max_terms) + args.output.write_text(json.dumps(result, indent=2) + '\n') + print(result['status']) + + +if __name__ == '__main__': + main() diff --git a/research/native-transpose-owned/source/owned/RESULT.json b/research/native-transpose-owned/source/owned/RESULT.json new file mode 100644 index 0000000000..b6c9cd0da1 --- /dev/null +++ b/research/native-transpose-owned/source/owned/RESULT.json @@ -0,0 +1,961 @@ +{ + "arithmetic": { + "PR5377_raw_root_upper": "75559684087/25000000000000", + "compiler": { + "H": 31385200000000, + "N": "2^31385200000000", + "eta": { + "lower": "0.000000199495867924466542600392", + "upper": "0.000000199495867924466542600393" + }, + "gap": "1/700000000", + "integer_test_exponent": 44836, + "logarithm_power": 1000, + "theta": "63/64", + "uniform_saving": "529667/175000000", + "word_materialized": false + }, + "fixed_profile_ceiling": { + "decreasing_through": "1/20", + "derivative_upper": { + "lower": "-195473.450610684184815935477074865515", + "upper": "-195473.450610684184815935477074865514" + }, + "remaining_interval_moment_upper": { + "lower": "-6820.155255095433991980526890420873", + "upper": "-6820.155255095433991980526890420872" + } + }, + "full_backward": 16, + "full_forward": 2, + "gain_over_PR4610": "24421/5000000000", + "gain_over_PR5377": "431/100000000", + "kappa": "151333/50000000", + "kappa_decimal": ".00302666", + "margin_at_previous_kappa": { + "lower": "1.209169472215494738857340795394", + "upper": "1.209169472215494738857340795395" + }, + "margin_at_previous_root_upper": { + "lower": "1.209152002019805295008574084544", + "upper": "1.209152002019805295008574084545" + }, + "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": [ + "new_complex_uniform_saving_above_b" + ], + "old_BIT": [ + "actual_bit_above_effective" + ], + "unearned_helper_credit": "Rejected by the independent complete census", + "unfunded_endpoint": [ + "main_transform_above_kappa", + "global_coordinate_router_above_kappa", + "fused_gaussian_above_kappa", + "group_bit_router_above_kappa", + "boundary_algebraic_matrix_above_kappa" + ] + }, + "nonrecursive": { + "additional_private_slots": 8, + "local_routes": 4834000, + "local_scalar": 158744, + "owned_slots_backward": 17, + "raw_budget": 1000000000, + "raw_scalar_upper": 181098496 + }, + "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": "174299999253/175000000000", + "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": "296613239576267/98000000000000000", + "fused_gaussian": "296613238728801/98000000000000000", + "global_coordinate_router": "1059333/350000000", + "group_bit_router": "741533446822001/245000000000000000", + "group_scans": "349999999/350000000", + "main_transform": "296613099576267/98000000000000000", + "microbox_face_corrections": "13475000001/175000000", + "polynomial_products": "699999999/700000000", + "sparse_union_movement": "40109113239576267/98000000000000000" + }, + "parameters": { + "a": "1059333/350000000", + "b": "2118667/700000000", + "beta": "699999997/700000000", + "bit_saving": "17/5000", + "cap_xi": "89109113099576267/98000000000000000", + "complex_uniform_saving": "529667/175000000", + "d": "1/700000000", + "epsilon": "699999999/700000000", + "kappa": "151333/50000000", + "lambda_": "199394667/200000000", + "lambda_prime": "139576267/140000000", + "layout": "1/700000000", + "q": "423733/140000000", + "r0": "1/7000000000", + "stop": "1/700000000", + "tested_saving": "302667/100000000" + }, + "strict_checks": { + "actual_bit_above_effective": "130667/350000000", + "actual_logarithmic_gamma_guard": "1/700000000", + "actual_logarithmic_group_guard": "8890887110423733/49000000000000000", + "alpha_logarithm_absorption": "1/7000000000", + "boundary_algebraic_matrix_above_kappa": "559576267/98000000000000000", + "cap_above_band": "40109113099576267/98000000000000000", + "cap_below_cell": "8890886760423733/98000000000000000", + "cap_below_phase_cell_power": "106890886900423733/98000000000000000", + "complex_above_effective": "1/700000000", + "complex_below_one_over_32": "19756333/700000000", + "complex_endpoint": "1/350000000", + "epsilon_below_one": "1/700000000", + "epsilon_positive": "699999999/700000000", + "fine_prime_halo_umbrella": "7/2", + "fused_gaussian_above_kappa": "558728801/98000000000000000", + "gaussian_above_main": "69576267/49000000000000000", + "global_coordinate_router_above_kappa": "1/175000000", + "global_gamma_power_slack": "9/7000000000", + "group_below_dimension": "1/350000000", + "group_bit_router_above_kappa": "1746822001/245000000000000000", + "group_gauge_power_slack": "8890887103423733/49000000000000000", + "group_key_fits_record": "1/350000000", + "group_positive": "699999997/700000000", + "group_scans_above_kappa": "87235167/87500000", + "halo_covers_generic_inverse_radius": "5", + "improvement_over_user_baseline": "647844790400418148631/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": "1397881333/490000000000000000", + "leaf_saving_above_effective": "697881333/490000000000000000", + "main_transform_above_kappa": "419576267/98000000000000000", + "membership_arithmetic_fits_record": "1/700000000", + "microbox_face_corrections_above_kappa": "26948940671/350000000", + "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": "697881337/700000000", + "positive_layout_slack": "1/700000000", + "q_below_effective": "1/700000000", + "q_below_internal": "1/700000000", + "q_below_leaf": "1397881333/490000000000000000", + "q_positive": "423733/140000000", + "short_record_fallback": "697881333/700000000", + "source_axis_superpolynomial": "1/700000000", + "sparse_union_movement_above_kappa": "39812500559576267/98000000000000000", + "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": 41170, + "16": 448, + "2": 7416, + "24": 448, + "3": 9180, + "32": 448, + "4": 2286, + "40": 448, + "48": 448, + "5": 720, + "56": 448, + "64": 448, + "72": 224, + "8": 16 + }, + "paid_calls": 64148, + "productive_fields": 10800, + "query_shears": 15, + "rank_mass_surplus": 752, + "raw_headroom": [ + "1476807/100000000000000", + "184601/12500000000000" + ], + "raw_root_interval": [ + "302667476807/100000000000000", + "37833434601/12500000000000" + ], + "strictification": { + "alpha": { + "lower": "0.999999995016963387587258118166", + "upper": "0.999999995016963387587258118167" + }, + "cutoff": 20, + "delta": { + "lower": "0.951652473261883819699264316643", + "upper": "0.951652473261883819699264316644" + }, + "floor": 21, + "gamma": { + "lower": "0.956968564096059991841792406781", + "upper": "0.956968564096059991841792406782" + }, + "normalized_paid_upper": "2097152001953127/2097154147483648", + "power": 1024, + "reserve": "1/1000000000", + "tail_offset": "1/5", + "tested": "302667/100000000" + }, + "targets": { + "145": 224, + "17": 448, + "25": 448, + "33": 448, + "4": 504, + "41": 448, + "49": 448, + "57": 448, + "65": 448, + "7": 126, + "73": 224, + "8": 846, + "9": 5740 + } + }, + "candidate_native": { + "backward": { + "helpers": { + "4": 28, + "7": 7, + "8": 47, + "9": 318 + }, + "independent_owned_entry_columns": 17, + "independent_persistent_columns": 624, + "max_denominator": 64, + "max_formal_prefix_l1": "163", + "owned_outputs_zero": true, + "paid": { + "1": 2193, + "2": 412, + "3": 510, + "4": 127, + "5": 40 + }, + "real_scalar_allowance": 158744, + "zero_identities": 8 + }, + "forward": { + "helpers": { + "4": 28, + "7": 7, + "8": 47, + "9": 326 + }, + "independent_owned_entry_columns": 1, + "independent_persistent_columns": 632, + "max_denominator": 32, + "max_formal_prefix_l1": "457", + "owned_outputs_zero": true, + "paid": { + "1": 2201, + "2": 412, + "3": 510, + "4": 127, + "5": 40, + "8": 8 + }, + "real_scalar_allowance": 158120, + "zero_identities": 0 + } + }, + "independent_source_identities": { + "checked": [ + [ + "center", + 11332 + ], + [ + "center", + 11358 + ], + [ + "center", + 11384 + ], + [ + "center", + 11410 + ], + [ + "center", + 11436 + ], + [ + "center", + 11462 + ], + [ + "center", + 11488 + ], + [ + "center", + 11514 + ], + [ + "zero", + 15584 + ], + [ + "zero", + 15870 + ], + [ + "zero", + 15876 + ], + [ + "zero", + 17245 + ], + [ + "zero", + 17256 + ], + [ + "zero", + 17264 + ], + [ + "zero", + 17580 + ], + [ + "zero", + 17722 + ] + ], + "owned_pivots": [ + 225, + 227, + 229, + 230, + 241, + 245, + 257, + 288 + ], + "reduced_basis": { + "225": { + "225": "1", + "384": "-1", + "388": "-1", + "390": "1", + "391": "1", + "392": "1", + "397": "-1" + }, + "227": { + "227": "1", + "231": "1", + "232": "-1", + "234": "1", + "235": "1", + "237": "1", + "238": "-1", + "239": "-1", + "324": "-1/2", + "326": "1/2", + "328": "1/2", + "333": "-1/2" + }, + "229": { + "229": "1", + "231": "-1", + "236": "-1", + "238": "1", + "324": "-1/2", + "326": "1/2", + "328": "1/2", + "333": "-1/2" + }, + "230": { + "230": "1", + "324": "-1", + "326": "1", + "328": "1", + "333": "-1" + }, + "241": { + "241": "1", + "243": "-1", + "253": "-1", + "255": "1", + "324": "1/2", + "326": "-1/2", + "328": "-1/2", + "333": "1/2" + }, + "245": { + "245": "1", + "247": "-1", + "252": "-1", + "254": "1", + "324": "-1/2", + "326": "1/2", + "328": "1/2", + "333": "-1/2" + }, + "257": { + "257": "1", + "259": "-1", + "261": "1", + "263": "-1", + "268": "-1", + "269": "-1", + "270": "1", + "271": "1" + }, + "288": { + "288": "1", + "294": "-1", + "296": "-1", + "297": "-1", + "300": "1", + "303": "1" + } + }, + "relation_rank": 8, + "snapshot_terms_before_substitution": { + "11205": 61, + "11218": 63, + "11231": 73, + "11244": 68, + "11257": 64, + "11270": 75, + "11283": 64, + "11306": 62 + }, + "source_event_indices_are_zero_based": true, + "witnesses": [ + { + "cached_event": 11205, + "cached_role": 92, + "copy_factor": "1", + "difference_factor": "1/4", + "event": 11332, + "frame": 254, + "relation": [ + [ + 230, + "1" + ], + [ + 324, + "-1" + ], + [ + 326, + "1" + ], + [ + 328, + "1" + ], + [ + 333, + "-1" + ] + ], + "zero_event": 15584, + "zero_factor": "-1/4", + "zero_role": 92 + }, + { + "cached_event": 11218, + "cached_role": 57, + "copy_factor": "1", + "difference_factor": "1/4", + "event": 11358, + "frame": 274, + "relation": [ + [ + 225, + "1" + ], + [ + 384, + "-1" + ], + [ + 388, + "-1" + ], + [ + 390, + "1" + ], + [ + 391, + "1" + ], + [ + 392, + "1" + ], + [ + 397, + "-1" + ] + ], + "zero_event": 17264, + "zero_factor": "-1/4", + "zero_role": 57 + }, + { + "cached_event": 11231, + "cached_role": 81, + "copy_factor": "1", + "difference_factor": "1/4", + "event": 11384, + "frame": 619, + "relation": [ + [ + 225, + "1" + ], + [ + 227, + "-1" + ], + [ + 229, + "1" + ], + [ + 231, + "-2" + ], + [ + 232, + "1" + ], + [ + 234, + "-1" + ], + [ + 235, + "-1" + ], + [ + 236, + "-1" + ], + [ + 237, + "-1" + ], + [ + 238, + "2" + ], + [ + 239, + "1" + ], + [ + 384, + "-1" + ], + [ + 388, + "-1" + ], + [ + 390, + "1" + ], + [ + 391, + "1" + ], + [ + 392, + "1" + ], + [ + 397, + "-1" + ] + ], + "zero_event": 17256, + "zero_factor": "-1/4", + "zero_role": 81 + }, + { + "cached_event": 11244, + "cached_role": 224, + "copy_factor": "1", + "difference_factor": "-1/4", + "event": 11410, + "frame": 279, + "relation": [ + [ + 227, + "1" + ], + [ + 229, + "1" + ], + [ + 232, + "-1" + ], + [ + 234, + "1" + ], + [ + 235, + "1" + ], + [ + 236, + "-1" + ], + [ + 237, + "1" + ], + [ + 239, + "-1" + ], + [ + 324, + "-1" + ], + [ + 326, + "1" + ], + [ + 328, + "1" + ], + [ + 333, + "-1" + ] + ], + "zero_event": 17722, + "zero_factor": "1/4", + "zero_role": 224 + }, + { + "cached_event": 11257, + "cached_role": 11, + "copy_factor": "1", + "difference_factor": "1/4", + "event": 11436, + "frame": 621, + "relation": [ + [ + 241, + "1" + ], + [ + 243, + "-1" + ], + [ + 245, + "1" + ], + [ + 247, + "-1" + ], + [ + 252, + "-1" + ], + [ + 253, + "-1" + ], + [ + 254, + "1" + ], + [ + 255, + "1" + ] + ], + "zero_event": 15876, + "zero_factor": "-1/4", + "zero_role": 11 + }, + { + "cached_event": 11270, + "cached_role": 240, + "copy_factor": "1", + "difference_factor": "-1/4", + "event": 11462, + "frame": 280, + "relation": [ + [ + 225, + "1" + ], + [ + 241, + "-1" + ], + [ + 243, + "1" + ], + [ + 245, + "1" + ], + [ + 247, + "-1" + ], + [ + 252, + "-1" + ], + [ + 253, + "1" + ], + [ + 254, + "1" + ], + [ + 255, + "-1" + ], + [ + 324, + "-1" + ], + [ + 326, + "1" + ], + [ + 328, + "1" + ], + [ + 333, + "-1" + ], + [ + 384, + "-1" + ], + [ + 388, + "-1" + ], + [ + 390, + "1" + ], + [ + 391, + "1" + ], + [ + 392, + "1" + ], + [ + 397, + "-1" + ] + ], + "zero_event": 17245, + "zero_factor": "1/4", + "zero_role": 240 + }, + { + "cached_event": 11283, + "cached_role": 9, + "copy_factor": "1", + "difference_factor": "1/4", + "event": 11488, + "frame": 624, + "relation": [ + [ + 257, + "1" + ], + [ + 259, + "-1" + ], + [ + 261, + "1" + ], + [ + 263, + "-1" + ], + [ + 268, + "-1" + ], + [ + 269, + "-1" + ], + [ + 270, + "1" + ], + [ + 271, + "1" + ] + ], + "zero_event": 15870, + "zero_factor": "-1/4", + "zero_role": 9 + }, + { + "cached_event": 11306, + "cached_role": 288, + "copy_factor": "1", + "difference_factor": "1/4", + "event": 11514, + "frame": 281, + "relation": [ + [ + 288, + "1" + ], + [ + 294, + "-1" + ], + [ + 296, + "-1" + ], + [ + 297, + "-1" + ], + [ + 300, + "1" + ], + [ + 303, + "1" + ] + ], + "zero_event": 17580, + "zero_factor": "-1/4", + "zero_role": 288 + } + ] + }, + "native_negative_controls": { + "missing_owned_input_clear": "Every independent main/helper endpoint: 0", + "uncleared_owned_output": "Every owned entry column is erased at return", + "under_or_overstated_paid_rank": "Exact paid rank and frame", + "wrong_copy_gauge": "Exact scalar destination frame", + "wrong_relation_sign": "Every independent main/helper endpoint: 0", + "wrong_snapshot_source": "Zero identity requires an identically zero full row", + "wrong_zero_input_frame": "Declared zero identity" + }, + "phase_inheritance": { + "absolute_phase_receipt_reused": "research/kappa-round3-warp-20261022/PHASE-VALIDATION.json.gz", + "all_retained_paid_events_and_warps_from_source": true, + "new_gaussian_operators": 0, + "new_native_maps": 0, + "new_operations": "Same-frame COPY, owned CLEAR/ADD, and physical identity on a proved zero row.", + "source_amplitudes_and_phase_lowering_freshly_replayed": false + }, + "scope": "Exact finite word, full all-column endpoints, ownership, p16 bill and compiler arithmetic. Retains source native phase, allowed owned erasure, mixed-target all-size, analytic, precision, tape, prime and exact-recovery contracts. No selected-frontier update.", + "source_native": { + "backward": { + "helpers": { + "4": 28, + "7": 7, + "8": 47, + "9": 326 + }, + "independent_owned_entry_columns": 1, + "independent_persistent_columns": 632, + "max_denominator": 64, + "max_formal_prefix_l1": "169", + "owned_outputs_zero": true, + "paid": { + "1": 2201, + "2": 412, + "3": 510, + "4": 127, + "5": 40, + "8": 8 + }, + "real_scalar_allowance": 158168, + "zero_identities": 0 + }, + "forward": { + "helpers": { + "4": 28, + "7": 7, + "8": 47, + "9": 326 + }, + "independent_owned_entry_columns": 1, + "independent_persistent_columns": 632, + "max_denominator": 32, + "max_formal_prefix_l1": "457", + "owned_outputs_zero": true, + "paid": { + "1": 2201, + "2": 412, + "3": 510, + "4": 127, + "5": 40, + "8": 8 + }, + "real_scalar_allowance": 158120, + "zero_identities": 0 + } + }, + "source_payload_sha256": "cfcd36b40326d7a5815e1db5313444379b3fb756b27d5201c561574c085cc0dd", + "status": "PASS_CONDITIONAL_KAPPA_00302666_EIGHT_JOINT_RELATIONS", + "word_payload_sha256": "2aee5e997df99726fc763e510d9cb69fbe4f86114dc8d2cd33ad26c6c462a21d" +} diff --git a/research/native-transpose-owned/source/owned/WITNESS.json b/research/native-transpose-owned/source/owned/WITNESS.json new file mode 100644 index 0000000000..19665f9eac --- /dev/null +++ b/research/native-transpose-owned/source/owned/WITNESS.json @@ -0,0 +1,434 @@ +[ + { + "relation": [ + [ + 230, + "1" + ], + [ + 324, + "-1" + ], + [ + 326, + "1" + ], + [ + 328, + "1" + ], + [ + 333, + "-1" + ] + ], + "event": 11332, + "frame": 254, + "cached_event": 11205, + "cached_role": 92, + "zero_event": 15584, + "zero_role": 92, + "copy_factor": "1", + "difference_factor": "1/4", + "zero_factor": "-1/4" + }, + { + "relation": [ + [ + 225, + "1" + ], + [ + 384, + "-1" + ], + [ + 388, + "-1" + ], + [ + 390, + "1" + ], + [ + 391, + "1" + ], + [ + 392, + "1" + ], + [ + 397, + "-1" + ] + ], + "event": 11358, + "frame": 274, + "cached_event": 11218, + "cached_role": 57, + "zero_event": 17264, + "zero_role": 57, + "copy_factor": "1", + "difference_factor": "1/4", + "zero_factor": "-1/4" + }, + { + "relation": [ + [ + 225, + "1" + ], + [ + 227, + "-1" + ], + [ + 229, + "1" + ], + [ + 231, + "-2" + ], + [ + 232, + "1" + ], + [ + 234, + "-1" + ], + [ + 235, + "-1" + ], + [ + 236, + "-1" + ], + [ + 237, + "-1" + ], + [ + 238, + "2" + ], + [ + 239, + "1" + ], + [ + 384, + "-1" + ], + [ + 388, + "-1" + ], + [ + 390, + "1" + ], + [ + 391, + "1" + ], + [ + 392, + "1" + ], + [ + 397, + "-1" + ] + ], + "event": 11384, + "frame": 619, + "cached_event": 11231, + "cached_role": 81, + "zero_event": 17256, + "zero_role": 81, + "copy_factor": "1", + "difference_factor": "1/4", + "zero_factor": "-1/4" + }, + { + "relation": [ + [ + 227, + "1" + ], + [ + 229, + "1" + ], + [ + 232, + "-1" + ], + [ + 234, + "1" + ], + [ + 235, + "1" + ], + [ + 236, + "-1" + ], + [ + 237, + "1" + ], + [ + 239, + "-1" + ], + [ + 324, + "-1" + ], + [ + 326, + "1" + ], + [ + 328, + "1" + ], + [ + 333, + "-1" + ] + ], + "event": 11410, + "frame": 279, + "cached_event": 11244, + "cached_role": 224, + "zero_event": 17722, + "zero_role": 224, + "copy_factor": "1", + "difference_factor": "-1/4", + "zero_factor": "1/4" + }, + { + "relation": [ + [ + 241, + "1" + ], + [ + 243, + "-1" + ], + [ + 245, + "1" + ], + [ + 247, + "-1" + ], + [ + 252, + "-1" + ], + [ + 253, + "-1" + ], + [ + 254, + "1" + ], + [ + 255, + "1" + ] + ], + "event": 11436, + "frame": 621, + "cached_event": 11257, + "cached_role": 11, + "zero_event": 15876, + "zero_role": 11, + "copy_factor": "1", + "difference_factor": "1/4", + "zero_factor": "-1/4" + }, + { + "relation": [ + [ + 225, + "1" + ], + [ + 241, + "-1" + ], + [ + 243, + "1" + ], + [ + 245, + "1" + ], + [ + 247, + "-1" + ], + [ + 252, + "-1" + ], + [ + 253, + "1" + ], + [ + 254, + "1" + ], + [ + 255, + "-1" + ], + [ + 324, + "-1" + ], + [ + 326, + "1" + ], + [ + 328, + "1" + ], + [ + 333, + "-1" + ], + [ + 384, + "-1" + ], + [ + 388, + "-1" + ], + [ + 390, + "1" + ], + [ + 391, + "1" + ], + [ + 392, + "1" + ], + [ + 397, + "-1" + ] + ], + "event": 11462, + "frame": 280, + "cached_event": 11270, + "cached_role": 240, + "zero_event": 17245, + "zero_role": 240, + "copy_factor": "1", + "difference_factor": "-1/4", + "zero_factor": "1/4" + }, + { + "relation": [ + [ + 257, + "1" + ], + [ + 259, + "-1" + ], + [ + 261, + "1" + ], + [ + 263, + "-1" + ], + [ + 268, + "-1" + ], + [ + 269, + "-1" + ], + [ + 270, + "1" + ], + [ + 271, + "1" + ] + ], + "event": 11488, + "frame": 624, + "cached_event": 11283, + "cached_role": 9, + "zero_event": 15870, + "zero_role": 9, + "copy_factor": "1", + "difference_factor": "1/4", + "zero_factor": "-1/4" + }, + { + "relation": [ + [ + 288, + "1" + ], + [ + 294, + "-1" + ], + [ + 296, + "-1" + ], + [ + 297, + "-1" + ], + [ + 300, + "1" + ], + [ + 303, + "1" + ] + ], + "event": 11514, + "frame": 281, + "cached_event": 11306, + "cached_role": 288, + "zero_event": 17580, + "zero_role": 288, + "copy_factor": "1", + "difference_factor": "1/4", + "zero_factor": "-1/4" + } +] diff --git a/research/native-transpose-owned/source/owned/native.py b/research/native-transpose-owned/source/owned/native.py new file mode 100644 index 0000000000..cbff46fe6e --- /dev/null +++ b/research/native-transpose-owned/source/owned/native.py @@ -0,0 +1,344 @@ +"""Eight prepared helpers remove sixteen paid jobs in the PR4610 backward word. + +Ali Romman, with substantial OpenAI Codex assistance. Apache-2.0. +This extends Ali Romman's one-relation PR5377 at c448d13c71908647f968b06cddb795ce7d288139. +The source word is by Cao Yifan. The row convention and scalar allowance +follow the credited native work of Cinna Davis and zxv. +""" +from collections import Counter +from copy import deepcopy +from fractions import Fraction as Q +from hashlib import sha1, sha256 +from pathlib import Path +import gzip +import importlib.util +import json +import sys + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +SOURCE = 'research/kappa-round3-warp-20261022/ACTUAL-WORD.json.gz' +PHASE = 'research/kappa-round3-warp-20261022/PHASE-VALIDATION.json.gz' +PAYLOAD = 'cfcd36b40326d7a5815e1db5313444379b3fb756b27d5201c561574c085cc0dd' +WITNESSES = json.loads((HERE / 'WITNESS.json').read_text(encoding='utf-8')) +COUNT = 8 +OLD_PAID = {1: 2201, 2: 412, 3: 510, 4: 127, 5: 40, 8: 8} +NEW_PAID = dict(OLD_PAID) +NEW_PAID[1] -= COUNT +NEW_PAID.pop(8) +OLD_HELPERS = {4: 28, 7: 7, 8: 47, 9: 326} + + +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 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 load(relative, name): + spec = importlib.util.spec_from_file_location(name, ROOT / relative) + module = importlib.util.module_from_spec(spec) + sys.modules[name] = module + spec.loader.exec_module(module) + return module + + +def authenticate(): + pins = read(HERE / 'SOURCES.json') + for row in pins['files']: + if row['usage'] != 'input': + continue + p = ROOT + for part in Path(row['path']).parts: + p /= part + need(not p.is_symlink(), 'No source aliases') + raw = p.read_bytes() + 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'], 'Source Git blob') + need(sha256(gzip.decompress((ROOT / SOURCE).read_bytes())).hexdigest() == PAYLOAD, 'Exact source payload') + return pins + + +def span(basis): + out = {0} + for vector in basis: + need(isinstance(vector, int) and 0 <= vector < 512, 'Binary frame coordinate') + out |= {v ^ vector for v in tuple(out)} + need(len(out) == 2 ** len(basis), 'Independent frame basis') + return out + + +def add(dst, src, q): + for k, v in tuple(src.items()): + value = dst.get(k, Q(0)) + q * v + if value: + dst[k] = value + else: + dst.pop(k, None) + + +def allowance(g): + if g[0] in ('clear', 'copy'): + return 2 + q = Q(*g[3:]) if g[0] == 'add' else Q(*g[2:]) + n, d = abs(q.numerator), q.denominator + need(n > 0 and d & (d - 1) == 0, 'Nonzero dyadic scalar') + if g[0] == 'scale': + need(n & (n - 1) == 0, 'Dyadic unit SCALE') + return 2 * (abs(n.bit_length() - d.bit_length()) + int(q < 0)) + need(g[0] == 'add', 'Known scalar operation') + return 2 * (3 + n.bit_length() - 1 + n.bit_count() + d.bit_length() - 1) + + +def relation_system(): + """Find exact independent pivots and eliminate all other pivot columns.""" + basis = {} + need(len(WITNESSES) == COUNT, 'Eight declared witnesses') + for witness in WITNESSES: + pairs = witness['relation'] + row = {h: Q(q) for h, q in pairs} + need(len(row) == len(pairs) and all(224 <= h < 632 and q for h, q in row.items()), 'Distinct helper coefficients') + for pivot, prior in sorted(basis.items()): + add(row, prior, -row.get(pivot, Q(0))) + need(row, 'Independent helper relations') + pivot = min(row); scale = row[pivot] + row = {h: q / scale for h, q in row.items()} + for prior in basis.values(): + add(prior, row, -prior.get(pivot, Q(0))) + basis[pivot] = row + need(len(basis) == COUNT, 'Eight paid helper outputs removed') + for pivot, row in basis.items(): + need(all(row.get(h, 0) == int(h == pivot) for h in basis), 'Reduced pivot columns') + return dict(sorted(basis.items())) + + +BASIS = relation_system() + + +def construct(source): + c = source['canonical']; old = source['programs']['backward'] + all_helpers = {h for x in WITNESSES for h, _ in x['relation']} + need(all(c['start'][h] == 0 and c['final'][h] == 1 for h in all_helpers), 'Every relation uses cold full-ended helpers') + snapshots, centers, zeros = {}, {}, {} + for slot, x in enumerate(WITNESSES, 1): + frame, role = x['frame'], x['cached_role'] + need(old[x['event']] == ['center', 0, 0, frame, 8], 'Exact source center') + event = old[x['cached_event']] + need(event[0] == 'climb' and event[2] == role and event[4] == frame, 'Exact snapshot source') + need(old[x['zero_event']] == ['climb', 'warp_retimed', x['zero_role'], frame, 1, 1], 'Exact zero source job') + need(x['cached_event'] < x['event'] < x['zero_event'] and Q(x['copy_factor']) == 1, 'Snapshot chronology and COPY coefficient') + snapshots[x['cached_event']] = (slot, x) + centers[x['event']] = (slot, x) + zeros[x['zero_event']] = x + need(len(snapshots) == len(centers) == len(zeros) == COUNT, 'Distinct replacement sites') + word = [] + for pivot, row in BASIS.items(): + word.append(['scalar', ['clear', ['L', pivot]], 0]) + for h, q in sorted(row.items()): + if h != pivot: + word.append(['scalar', ['add', ['L', pivot], ['L', h], -q.numerator, q.denominator], 0]) + for index, event in enumerate(old): + if index in centers: + slot, x = centers[index]; f = x['frame'] + word += [['scalar', ['clear', ['C', 0]], f], + ['scalar', ['copy', ['C', 0], ['C', slot]], f], + ['scalar', ['clear', ['C', slot]], f]] + elif index in zeros: + x = zeros[index] + word.append(['zero_retag', ['L', x['zero_role']], x['frame'], 1]) + else: + word.append(deepcopy(event)) + if index in snapshots: + slot, x = snapshots[index]; f = x['frame'] + word += [['scalar', ['clear', ['C', slot]], f], + ['scalar', ['copy', ['C', slot], ['L', x['cached_role']]], f]] + word += [['scalar', ['clear', ['L', h]], 1] for h in BASIS] + physical = deepcopy(c); physical.pop('local_profile') + return {'schema': 'joint-helper-relations-word/1', 'canonical': physical, + 'relation_basis': encode(BASIS), + 'paid_profiles': {'forward': OLD_PAID, 'backward': NEW_PAID}, + 'owned': {'forward': [['C', 0]], 'backward': [['C', i] for i in range(COUNT + 1)] + [['L', h] for h in BASIS]}, + 'programs': {'forward': deepcopy(source['programs']['forward']), 'backward': word}} + + +def replay(c, program, backward, specialized): + """Run every event on all independent entry columns and exact frames.""" + owned = {('C', 0)} | ({('C', i) for i in range(1, COUNT + 1)} | {('L', h) for h in BASIS} if specialized else set()) + roles = {('L', i) for i in range(632)} | owned + rows = {r: {(r, ()): Q(1)} for r in roles} + frames = {('L', i): f for i, f in enumerate(c['start'])} + frames.update({r: None for r in owned if r[0] == 'C'}) + spaces = [span(b) for b in c['frames']] + paid = Counter() + cost, max_l1, denominator, zero_count = 0, Q(1), 1, 0 + for e in program: + kind, touched = e[0], None + if kind == 'scalar': + g, frame = e[1:] + dst = tuple(g[1]); touched = dst + need(dst in rows and 0 <= frame < len(spaces), 'Declared scalar destination and frame') + cost += allowance(g) + if g[0] == 'clear': + need(dst in owned, 'Only owned fields can be erased') + rows[dst] = {}; frames[dst] = frame + else: + need(frames[dst] == frame, 'Exact scalar destination frame') + if g[0] in ('add', 'copy'): + src = tuple(g[2]) + need(src in rows and frames[src] == frame and dst != src, 'Exact scalar source frame') + if g[0] == 'copy': + need(dst in owned and not rows[dst], 'COPY into cleared owned storage') + rows[dst] = dict(rows[src]) + else: + add(rows[dst], rows[src], Q(g[3], g[4])) + else: + need(g[0] == 'scale', 'Known scalar operation') + rows[dst] = {k: Q(g[2], g[3]) * v for k, v in rows[dst].items()} + elif kind == 'warp': + _, role, op, old, new = e + dst = tuple(role); touched = dst + need(frames[dst] == old and 1 <= abs(op) <= len(c['warps']), 'Exact warp input') + symbol = (1 if op > 0 else -1) * (abs(op) + (10**6 if backward else 0)) + rows[dst] = {(r, w[1:] if w and w[0] == -symbol else (symbol,) + w): q + for (r, w), q in rows[dst].items()} + frames[dst] = new + elif kind in ('climb', 'center'): + if kind == 'climb': + _, _, i, old, new, rank = e + dst = ('L', i) + need(spaces[old] < spaces[new], 'Ascending paid climb') + else: + _, i, old, new, rank = e + dst = ('C', i) + need(spaces[old] < spaces[new] or spaces[new] < spaces[old], 'Nested paid center') + need(frames[dst] == old and rank == abs(len(c['frames'][new]) - len(c['frames'][old])), 'Exact paid rank and frame') + frames[dst] = new; paid[rank] += 1 + elif kind == 'zero_retag': + _, role, old, new = e + dst = tuple(role) + need(specialized and backward and any(dst == ('L', x['zero_role']) and (old, new) == (x['frame'], 1) for x in WITNESSES), 'Declared zero identity') + need(frames[dst] == old and not rows[dst], 'Zero identity requires an identically zero full row') + frames[dst] = new; zero_count += 1 + else: + need(kind in ('phase', 'adapter'), 'Known inert source marker') + if touched is not None: + max_l1 = max(max_l1, sum(map(abs, rows[touched].values()), Q(0))) + denominator = max(denominator, max((q.denominator for q in rows[touched].values()), default=1)) + need([frames['L', i] for i in range(632)] == c['final'], 'Every final native frame') + for i in range(632): + r = ('L', i) + if r in owned: + continue + expected = {(r, ()): Q(1)} + if i < 112 if backward else 112 <= i < 224: + expected[(('L', i + 112 if backward else i - 112), ())] = Q(-1 if backward else 1) + need(rows[r] == expected, 'Every independent main/helper endpoint: ' + str(i)) + need(all(not rows[r] for r in owned), 'Every owned entry column is erased at return') + need(zero_count == COUNT * int(specialized), 'All eight zero identities checked') + helpers = Counter() + for i in range(224, 632): + if ('L', i) in owned: + continue + a, b = c['start'][i], c['final'][i] + need(spaces[a] < spaces[b], 'Strict independent productive helper') + helpers[len(c['frames'][b]) - len(c['frames'][a])] += 1 + return {'paid': dict(sorted(paid.items())), 'helpers': dict(sorted(helpers.items())), + 'independent_persistent_columns': 632 - COUNT if specialized else 632, + 'independent_owned_entry_columns': len(owned), 'owned_outputs_zero': True, + 'real_scalar_allowance': cost, 'max_formal_prefix_l1': str(max_l1), + 'max_denominator': denominator, 'zero_identities': zero_count} + + +def independent_source_identities(source): + """Check unrestricted source identities with the predecessor row engine.""" + v = load('research/kappa-causal-continuation/buffer-borrowing/verify_buffers.py', 'joint_relation_source_rows') + rows = {('L', i): v.identity(('L', i)) for i in range(632)} + rows['C', 0] = v.identity(('C', 0)); saved = {}; checked = [] + for index, e in enumerate(source['programs']['backward']): + if e[0] == 'scalar': + g = e[1]; dst = tuple(g[1]) + if g[0] == 'clear': rows[dst] = {} + elif g[0] == 'copy': rows[dst] = dict(rows[tuple(g[2])]) + elif g[0] == 'scale': rows[dst] = {k: Q(g[2], g[3]) * a for k, a in rows[dst].items()} + else: v.add(rows[dst], rows[tuple(g[2])], Q(g[3], g[4])) + elif e[0] == 'warp': + dst = tuple(e[1]); rows[dst] = v.warp(rows[dst], e[2], True) + for x in WITNESSES: + delta = {(('L', h), ()): Q(q) for h, q in x['relation']} + if index == x['cached_event']: + saved[index] = dict(rows['L', x['cached_role']]) + if index == x['event']: + diff = dict(rows['C', 0]); v.add(diff, saved[x['cached_event']], -Q(x['copy_factor'])) + need(diff == {k: Q(x['difference_factor']) * q for k, q in delta.items()}, 'Independent exact center minus snapshot identity') + checked.append(('center', index)) + if index == x['zero_event']: + need(rows['L', x['zero_role']] == {k: Q(x['zero_factor']) * q for k, q in delta.items()}, 'Independent exact zero-site row identity') + checked.append(('zero', index)) + need(len(checked) == 2 * COUNT, 'Sixteen unrestricted source identities') + need(all(rows['L', i] == v.expected(('L', i), [], True, False) for i in range(632)), 'Independent unrestricted source endpoints') + return {'source_event_indices_are_zero_based': True, 'witnesses': WITNESSES, + 'relation_rank': COUNT, 'owned_pivots': list(BASIS), 'reduced_basis': BASIS, + 'snapshot_terms_before_substitution': {i: len(row) for i, row in saved.items()}, + 'checked': checked} + + +def phase_inheritance(source, candidate): + receipt = read(ROOT / PHASE) + need(receipt['status'] == 'PASS_JOINT_HELPER_MAPS_ALL_ACTUAL_ABSOLUTE_PHASES' and + receipt['actual_word_canonical_sha256'] == PAYLOAD, 'Authenticated source absolute-phase receipt') + physical = deepcopy(source['canonical']); physical.pop('local_profile') + need(candidate['canonical'] == physical, 'Every frame, native map and main adapter unchanged') + for direction, program in candidate['programs'].items(): + old = source['programs'][direction] + for kind in ('warp', 'adapter', 'phase'): + need([e for e in program if e[0] == kind] == [e for e in old if e[0] == kind], 'Exact inherited ' + kind + ' sequence') + old_paid = Counter(tuple(e) for e in old if e[0] in ('climb', 'center')) + new_paid = Counter(tuple(e) for e in program if e[0] in ('climb', 'center')) + expected = Counter() if direction == 'forward' else Counter(tuple(old[i]) for x in WITNESSES for i in (x['event'], x['zero_event'])) + need(old_paid - new_paid == expected and not new_paid - old_paid, 'Only the sixteen proved jobs are removed') + return {'new_gaussian_operators': 0, 'new_native_maps': 0, + 'all_retained_paid_events_and_warps_from_source': True, + 'absolute_phase_receipt_reused': PHASE, + 'source_amplitudes_and_phase_lowering_freshly_replayed': False, + 'new_operations': 'Same-frame COPY, owned CLEAR/ADD, and physical identity on a proved zero row.'} + + +def controls(c, candidate): + controls = {} + base = candidate['programs']['backward'] + variants = {} + bad = deepcopy(base); bad[1][1][3] *= -1; variants['wrong_relation_sign'] = bad + variants['missing_owned_input_clear'] = deepcopy(base[1:]) + bad = deepcopy(base) + next(e for e in bad if e[0] == 'scalar' and e[1][:2] == ['copy', ['C', 1]])[1][2] = ['L', 63] + variants['wrong_snapshot_source'] = bad + bad = deepcopy(base); next(e for e in bad if e[0] == 'zero_retag')[2] = 0 + variants['wrong_zero_input_frame'] = bad + bad = deepcopy(base); next(e for e in bad if e[0] == 'climb')[5] += 1 + variants['under_or_overstated_paid_rank'] = bad + bad = deepcopy(base) + next(e for e in bad if e[0] == 'scalar' and e[1][:2] == ['copy', ['C', 0]])[2] = 0 + variants['wrong_copy_gauge'] = bad + variants['uncleared_owned_output'] = deepcopy(base[:-1]) + for name, program in variants.items(): + try: + replay(c, program, True, True) + except ValueError as err: + controls[name] = str(err) + else: + raise ValueError('Control accepted: ' + name) + return controls diff --git a/research/native-transpose-owned/support.py b/research/native-transpose-owned/support.py new file mode 100644 index 0000000000..f126e462ba --- /dev/null +++ b/research/native-transpose-owned/support.py @@ -0,0 +1,41 @@ +"""Read pinned inputs and load the exact source modules. Apache-2.0.""" +from pathlib import Path +from fractions import Fraction +from hashlib import sha1,sha256 +import gzip,importlib.util,json,sys +HERE=Path(__file__).resolve().parent +ROOT=HERE.parents[1] +OLD_PAID={1:2201,2:412,3:510,4:127,5:40,8:8} +OLD_HELPERS={4:28,7:7,8:47,9:326} +SOURCE='research/kappa-round3-warp-20261022/ACTUAL-WORD.json.gz' +PAYLOAD='cfcd36b40326d7a5815e1db5313444379b3fb756b27d5201c561574c085cc0dd' +CE='research/t74-native-fast/vendor/native/new/code/borrow/vendor/clifford/clifford_exact.py' +def need(ok,why): + if not ok:raise ValueError(why) +def read(path): + data=Path(path).read_bytes() + return json.loads(gzip.decompress(data) if str(path).endswith('.gz') else data) +def load(relative,name): + spec=importlib.util.spec_from_file_location(name,ROOT/relative) + module=importlib.util.module_from_spec(spec);sys.modules[name]=module + spec.loader.exec_module(module) + return module +def encode(x): + if isinstance(x,Fraction):return str(x) + if isinstance(x,dict):return {str(k):encode(v) for k,v in x.items()} + if isinstance(x,(tuple,list)):return [encode(v) for v in x] + return x +def packed(x):return (json.dumps(encode(x),sort_keys=True,separators=(',',':'))+'\n').encode() +def authenticate(): + pins=read(HERE/'SOURCES.json') + for row in pins['files']: + if row['usage']!='input':continue + p=ROOT + for part in Path(row['path']).parts: + p/=part;need(not p.is_symlink(),'No source alias') + data=p.read_bytes() + need(sha256(data).hexdigest()==row['sha256'],'Source bytes: '+row['path']) + need(sha1(b'blob '+str(len(data)).encode()+b'\0'+data).hexdigest()==row['git_blob'],'Source Git blob') + raw=gzip.decompress((ROOT/SOURCE).read_bytes()) + need(sha256(raw).hexdigest()==PAYLOAD,'Final PR4610 payload') + return json.loads(raw) diff --git a/research/native-transpose-owned/verify.py b/research/native-transpose-owned/verify.py new file mode 100644 index 0000000000..b3c1c49706 --- /dev/null +++ b/research/native-transpose-owned/verify.py @@ -0,0 +1,46 @@ +"""Check the owned transpose, physical phases and complete conditional bound. + +Ali Romman with substantial OpenAI Codex assistance. Apache-2.0. +""" +from pathlib import Path +import argparse,gzip,json,sys +sys.dont_write_bytecode=True +HERE=Path(__file__).resolve().parent +sys.path.insert(0,str(HERE)) +from support import authenticate,read,need,packed + +def run(): + source=authenticate() + import word,interface,phases,price + from check_certificate import check + native,emitted,problem=word.run(source) + check(problem,native['native']) + print('PASS_TRANSPOSE_ALL_INPUTS_AND_NATIVE_CHECKER',flush=True) + boundary=interface.run() + physical=phases.run(source) + print('PASS_TRANSPOSE_ALL_PHYSICAL_CLASSES',flush=True) + b=native['source_replay'] + f=dict(b,real_scalar_allowance=native['real_scalar_allowance'], + max_formal_prefix_l1=native['transpose']['max_formal_prefix_l1'], + max_denominator=native['transpose']['max_denominator']) + arithmetic=price.run({'forward':f,'backward':b}) + result={'status':'PASS_CONDITIONAL_KAPPA_00302725_OWNED_TRANSPOSE', + 'native':native,'interface':boundary,'physical':physical,'arithmetic':arithmetic} + return result,emitted,problem + +def main(): + parser=argparse.ArgumentParser(description=__doc__) + parser.add_argument('--write',action='store_true',help='Write this package after every check passes') + args=parser.parse_args() + result,emitted,problem=run() + artifacts={'RESULT.json':result,'WORD.json.gz':emitted,'NATIVE-PROBLEM.json.gz':problem, + 'NATIVE-CERTIFICATE.json':result['native']['native']} + for name,value in artifacts.items(): + path=HERE/name + if args.write: + data=packed(value) + path.write_bytes(gzip.compress(data,mtime=0) if name.endswith('.gz') else data) + else:need(read(path)==json.loads(packed(value)),'Exact committed artifact: '+name) + print(result['status'],flush=True) + return 0 +if __name__=='__main__':raise SystemExit(main()) diff --git a/research/native-transpose-owned/word.py b/research/native-transpose-owned/word.py new file mode 100644 index 0000000000..df11d06f64 --- /dev/null +++ b/research/native-transpose-owned/word.py @@ -0,0 +1,144 @@ +"""Check the literal transpose and its formal bridge cancellation. + +The bridge is a coordinate proof symbol, not an emitted physical operation. +The source zero_retag is physical identity. Its transpose is identity. +Credit the classical transposition principle and PR5383 by Ali Romman, +Cao Yifan's word, Cinna Davis and the retained native authors. Apache-2.0. +Prepared by Ali Romman with OpenAI Codex assistance. +""" +from fractions import Fraction as Q +from collections import Counter +from hashlib import sha256 +from pathlib import Path +import json,sys +from support import HERE,ROOT,need,load,packed +sys.path.insert(0,str(HERE/'source/cutoff')) +from native_identity import decide +base=load('research/native-transpose-owned/source/owned/native.py','transpose_owned_source') +ROLES=632+base.COUNT+1 +OWNED=set(base.BASIS)|set(range(632,ROLES)) + +def recipes(c): + from phases import ce + from native import Native + out={} + for w in c['warps']: + rows=ce.transpose(tuple(w['G_columns']),9) + tr=ce.transpose(ce.inv(rows,9),9) + q=tuple((1<