diff --git a/research/pr4412-pr4414-moment-check/README.md b/research/pr4412-pr4414-moment-check/README.md new file mode 100644 index 000000000..64d07fe64 --- /dev/null +++ b/research/pr4412-pr4414-moment-check/README.md @@ -0,0 +1,75 @@ +# Independent check of the strictification inequalities in #4412 and #4414 + +**Claim type: an independent certified finite check. No new κ.** This +accepts neither PR. It checks none of their native audits, outer ledgers or +inherited premises. + +## Object + +1337isnot1337's two predecessors of #4416 (whose check is +[#4420](https://github.com/CrocSwap/integer-mult-bounds/pull/4420)) each +tensor a native mixed unit, then split paid jobs at a cutoff `J`. With +`α = P_τ/T_τ`, `γ = P_1/(b^C T_τ)` and `X_τ = Σ n_r r^τ`: + +| PR | conditional κ | saving `C` | cutoff | needs | +| --- | --- | --- | --- | --- | +| [#4412](https://github.com/CrocSwap/integer-mult-bounds/pull/4412) | 0.00247755 | `0.00247756` | `J = 4^n` | `α < 1 − 10⁻⁹`, `γ < 999/1000`; with `n = 15000`, `1/(1+n/10⁹) + 2(999/1000)^n < 1` | +| [#4414](https://github.com/CrocSwap/integer-mult-bounds/pull/4414) | 0.00267987 | `0.00267988` | `J = ⌊(19/4)^v⌋` | `α < 1 − 10⁻⁸`, `γ < 9999/10000`; with `v = 150000`, `1/(1+v/10⁸) + 4/2¹⁵ < 1` | + +No outside check existed for either. + +## Results + +Every link holds, recomputed with exact rationals and enclosure widths below +`10⁻³⁰`. The enclosures overlap each PR's recorded intervals. + +| | #4412 | #4414 | +| --- | --- | --- | +| Invoice: targets / paid calls, rank-one moments | 3,528 / 25,774; 47,075 vs 46,851 | 6,648 / 48,442; 108,769 vs 108,257 | +| `α` | `0.999999996840`; `1 − α = 3.16·10⁻⁹` | `0.999999982435`; `1 − α = 1.76·10⁻⁸` | +| `γ` | `0.9989653420` (base 4) | `0.9998629803` (base 19/4) | +| Closing bound | surplus `1.4392544772·10⁻⁵`, inside the recorded interval | exactly `16386003/16408576`, gap `22573/16408576` | +| **Limit saving `C*` (α = 1)** | `0.002477561641`, **`1.6·10⁻⁹` above the tested saving** | `0.002679889969`, **`1.0·10⁻⁸` above** | + +`γ` stays below 1 at each `C*`. So, as at #4416, each tested saving sits at +its own invoice's ceiling. Larger powers cannot raise either κ; only a +different invoice can. + +Other checks: + +- #4414's `(9999/10000)^10000 < 1/2` is exact. +- #4414's control holds: the integer cutoff base 4 fails the tail, since + `γ > 1` there. +- #4412's cutoff base 4 lies below its minimum target rank 5. + +## Not covered + +- The native audits behind `T` and `P`. **Tightest margin:** #4412's `α` + clears `1 − 10⁻⁹` by only `2.2·10⁻⁹`. +- The tensor and splitting proofs, the compiler ranks, the outer rows and + every inherited premise. + +## Reproduce + +```sh +python3.12 -B research/pr4412-pr4414-moment-check/verify.py +``` + +It prints `PASS_PR4412_PR4414_MOMENT_CHECK` in about 2 minutes, using only +the standard library. + +## Open next questions + +1. **Rebuild the three p6/p7 invoices from their native words** (#4412, + #4414 and #4416). + - *Why it matters:* every `α` margin is below `10⁻⁸`, while one paid call + moves `α` by more than `10⁻⁶`. + - *First step:* census the native words with separate code. + - *Blocked by:* nothing. + +## Credit + +The constructions and invoices are 1337isnot1337's (#4412, #4414, with +OpenAI Codex assistance), building on zxv's #4359, #4405 and Jacob Alan +Sussman's Theorem 1G. Prepared by Ryanson Jonathan with substantial Claude +Code (Claude Opus 5.5) assistance. Apache-2.0. diff --git a/research/pr4412-pr4414-moment-check/SOURCES.json b/research/pr4412-pr4414-moment-check/SOURCES.json new file mode 100644 index 000000000..fcfba8aa3 --- /dev/null +++ b/research/pr4412-pr4414-moment-check/SOURCES.json @@ -0,0 +1,18 @@ +{ + "schema_version": 1, + "base_commit": "12fa8c5c844be21bfefb38a19503fbd867a11244", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81", + "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "64bfc5af6709ed9811171e0a2108f05e1219cb65", + "sha256": "352a6184713b8843d96fd2c2071eb7aeaa655906b7c51d45ad444912666c8a96" + } + ] +} diff --git a/research/pr4412-pr4414-moment-check/TASK.json b/research/pr4412-pr4414-moment-check/TASK.json new file mode 100644 index 000000000..4a6309e7b --- /dev/null +++ b/research/pr4412-pr4414-moment-check/TASK.json @@ -0,0 +1,100 @@ +{ + "schema_version": 1, + "task_id": "independent-moment", + "priority_revision": 7, + "base_commit": "12fa8c5c844be21bfefb38a19503fbd867a11244", + "original_card": { + "id": "independent-moment", + "question": "Does a new paid-profile or mixture-ceiling claim have independent source-bound coverage of its actual changed ledger?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/staged544-mixed-fourth-entry/README.md", + "research/staged-fourth-mixture-ceiling/README.md", + "research/r437-two-window-carrier/README.md" + ], + "methods": [ + "Independently reconstruct one changed paid ledger or pooled dual with exact source and model binding.", + "Check a genuinely uncovered moment implication with a different enclosure method and semantic controls." + ], + "acceptance_gate": "Demonstrate independence, source binding, positive cases and semantic failure controls. Name the existing checks and the missing coverage. More digits or another equivalent evaluation of an unchanged root is not by itself new verification coverage.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Choose one uncovered implication in #4088 literal mixed fill, #4091 pooled dual/model binding or #4067 changed frame/host bill. #4091 pins an earlier #4088 head: validate word, capacity and stock equivalence before applying that ceiling to the later fill.", + "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately." + }, + "first_experiment": "Independently reconstruct one changed ledger or pooled certificate with a positive case and a semantic failure control. Compare exact sources and name what existing checks miss. Keep this separate from supplier-boundary-audit (ordinary/outer dispatch) and uniform-transfer-audit (all-size proof). Stop after the chosen implication; more digits of an unchanged root are not additional mechanism coverage.", + "bottleneck_link": "Independent pricing prevents unsupported frontier claims and can reveal genuine accounting slack.", + "allowed_variations": [ + "Reconstruct either a source ledger or a numeric enclosure with a different method." + ], + "scope_change_triggers": [ + "Importing the primary function and calling its output independent verification.", + "Calling an aggregate histogram or source archive an independently accepted physical supplier." + ], + "overlap_terms": [ + "independent moment", + "rank histogram", + "exact enclosure", + "2979", + "rank7 joint endframes", + "paired extraction", + "joint lowering", + "4088", + "4091", + "4067", + "staged544-mixed-fourth-entry", + "staged-fourth-mixture-ceiling", + "r437-two-window-carrier" + ], + "existing_checks": [ + { + "scope": "PR #4088: mixed local/owner/phase ledger and moment reported.", + "evidence": "research/staged544-mixed-fourth-entry/README.md", + "remaining": "Independent binding of changed construction to paid histogram, distinct from full admission.", + "status": "author-checked", + "source_commit": "72d7efc181edb21806a878f174847c96dd410ab0", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4091: sharp pooled ceiling proposed for fixed THREE/FOUR words and inventory.", + "evidence": "research/staged-fourth-mixture-ceiling/README.md", + "remaining": "Validate dual, exhaustive pattern scope and exact source equivalence before applying to newer fills.", + "status": "author-checked", + "source_commit": "a29bdd8f56cd18b805917775cdec09ff935eddc4", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4067: paid (2,2) to (1,3) exchange and fixed OQ4 host reported.", + "evidence": "research/r437-two-window-carrier/README.md", + "remaining": "Independent full cost delta; remaining caller/precision/stock obligations are separate.", + "status": "author-checked", + "source_commit": "a95f11c52e3ca1e4c5171b3c20d8f4b0815aee2e", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "refined", + "actual_scope": "Independently certify the strictification inequalities of #4412 (saving 0.00247756) and #4414 (saving 0.00267988) from their recorded native invoices, and compute each invoice's limit saving.", + "scope_change_reason": "The card asks for independent coverage of new moment claims; #4412 and #4414 are open conditional-kappa predecessors of #4416 with no outside check.", + "bottleneck_link": "Each raises the conditional kappa; their moment inequalities must hold before their native and outer premises are worth review.", + "budget_minutes": 30, + "stop_rule": "Stop once every stated inequality of both PRs is certified or fails.", + "outcome": "completed", + "evidence": "verify.py: invoices bound to each native inventory; #4412 alpha = 0.99999999684 < 1-1e-9, gamma = 0.99897 < 999/1000, closing surplus 1.4392544772e-5 inside its interval; #4414 alpha = 0.99999998243 < 1-1e-8, gamma = 0.99986 < 9999/10000, bound 16386003/16408576 and gap exact, base-4 control fails; limit savings 0.002477561641 and 0.002679889969, 1.6e-9 and 1.0e-8 above the tested savings, with gamma < 1 there.", + "author": "Ryanson Jonathan, with Claude Code (Claude Opus 5.5) assistance", + "ai_assistance": "Substantial Claude Code (Claude Opus 5.5) assistance in reading, verifier implementation and writing; no independent human or proof-kernel review.", + "open_questions": [ + { + "question": "Rebuild the p6/p7 native invoices of #4412, #4414 and #4416 with separate code.", + "why_it_matters": "Every alpha margin is below 1e-8 while one paid call moves alpha by more than 1e-6.", + "first_step": "Census the native words independently.", + "blocked_by": "None." + } + ] +} diff --git a/research/pr4412-pr4414-moment-check/VERIFY.json b/research/pr4412-pr4414-moment-check/VERIFY.json new file mode 100644 index 000000000..f1b97919d --- /dev/null +++ b/research/pr4412-pr4414-moment-check/VERIFY.json @@ -0,0 +1,18 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 600, + "checks": "Vendored TENSOR.md and RESULT.json hashes and phrases for both PRs; invoice binding and aggregates; certified alpha and gamma at each tested saving overlapping the recorded intervals; closing bounds and gaps; #4414 decay comparison and base-4 control; limit savings with gamma < 1 there." + } + ] +} diff --git a/research/pr4412-pr4414-moment-check/vendor/4412-RESULT.json b/research/pr4412-pr4414-moment-check/vendor/4412-RESULT.json new file mode 100644 index 000000000..d9f027061 --- /dev/null +++ b/research/pr4412-pr4414-moment-check/vendor/4412-RESULT.json @@ -0,0 +1,266 @@ +{ + "endpoint": { + "compiler": { + "H0": 2508580090000, + "H1": 8701218254312470001, + "N_encoding": "2^8701218254312470001", + "delta": "1/1400000000", + "exit_coefficient_log2_upper": "41250", + "final_strict_power_gap": "1/1400000000", + "h": "1/8", + "materialized_tensor_rule_or_uniform_word": false, + "negative_log2_eta_upper": "31357247/140000", + "paid_max_bound_encoding": "4^15000", + "rank_one_induction": "47075^n > 46851^n, and splitting preserves total rank", + "t": "24938061/25000000", + "target_max_encoding": "57^15000", + "target_min_encoding": "5^15000", + "tensor_power": 15000, + "theta_upper": "7/8", + "z": "698265709/700000000", + "z0": "1396531417/1400000000" + }, + "gain_over_PR4359": "3551/20000000", + "gain_over_PR4405": "8623/50000000", + "kappa": "49551/20000000", + "ledger_source_sha256": "d097e55f06c3f244f2074ffd7c1a0a5f3c4b4b6a6accf9619d1dde5c0ae85e15", + "minimum_outer_margin": "131141607/30625000000000000", + "negative_controls": { + "closed_epsilon": { + "actual_logarithmic_gamma_guard": "0", + "epsilon_below_one": "0", + "gaussian_above_main": "-325179/30625000000000000", + "global_gamma_power_slack": "-1/7000000000", + "new_semantic_guard_with_C1_one": "0", + "source_axis_superpolynomial": "0" + }, + "closed_uniform_gap": { + "new_complex_uniform_saving_above_b": "0" + }, + "insufficient_BIT": { + "actual_bit_above_effective": "-124289/700000000" + }, + "unfunded_outer_point": { + "boundary_algebraic_matrix_above_kappa": "-131358393/30625000000000000", + "fused_gaussian_above_kappa": "-131575179/30625000000000000", + "global_coordinate_router_above_kappa": "-3/700000000", + "group_bit_router_above_kappa": "-1405202867/490000000000000000", + "main_transform_above_kappa": "-175108393/30625000000000000" + } + }, + "outer": { + "functional_checks": { + "fixed_halo_explicit_metadata_branch": "13475000001/175000000", + "new_BIT_row_stock_sublinear_in_active_group": "697899997009/700000000000", + "new_semantic_group_guard": "3/700000000" + }, + "margins": { + "boundary_algebraic_matrix": "75875143641607/30625000000000000", + "fused_gaussian": "75875143424821/30625000000000000", + "global_coordinate_router": "1734289/700000000", + "group_bit_router": "1214002994797133/490000000000000000", + "group_scans": "349999999/350000000", + "main_transform": "75875099891607/30625000000000000", + "microbox_face_corrections": "13475000001/175000000", + "polynomial_products": "699999999/700000000", + "sparse_union_movement": "12517281393641607/30625000000000000" + }, + "parameters": { + "a": "1734289/700000000", + "b": "173429/70000000", + "beta": "699999997/700000000", + "bit_saving": "27/10000", + "cap_xi": "27829781349891607/30625000000000000", + "complex_uniform_saving": "1734291/700000000", + "d": "1/700000000", + "epsilon": "699999999/700000000", + "kappa": "49551/20000000", + "lambda_": "199504489/200000000", + "lambda_prime": "43641607/43750000", + "layout": "1/700000000", + "q": "108393/43750000", + "r0": "1/7000000000", + "stop": "1/700000000", + "tested_saving": "61939/25000000" + }, + "strict_checks": { + "actual_bit_above_effective": "155711/700000000", + "actual_logarithmic_gamma_guard": "1/700000000", + "actual_logarithmic_group_guard": "2795218715733393/15312500000000000", + "alpha_logarithm_absorption": "1/7000000000", + "boundary_algebraic_matrix_above_kappa": "174891607/30625000000000000", + "cap_above_band": "12517281349891607/30625000000000000", + "cap_below_cell": "2795218606358393/30625000000000000", + "cap_below_phase_cell_power": "33420218650108393/30625000000000000", + "complex_above_effective": "1/700000000", + "complex_below_one_over_32": "2014071/70000000", + "complex_endpoint": "1/350000000", + "epsilon_below_one": "1/700000000", + "epsilon_positive": "699999999/700000000", + "fine_prime_halo_umbrella": "7/2", + "fused_gaussian_above_kappa": "174674821/30625000000000000", + "gaussian_above_main": "21766607/15312500000000000", + "global_coordinate_router_above_kappa": "1/175000000", + "global_gamma_power_slack": "9/7000000000", + "group_below_dimension": "1/350000000", + "group_bit_router_above_kappa": "3494797133/490000000000000000", + "group_gauge_power_slack": "2795218713545893/15312500000000000", + "group_key_fits_record": "1/350000000", + "group_positive": "699999997/700000000", + "group_scans_above_kappa": "698265713/700000000", + "halo_covers_generic_inverse_radius": "5", + "improvement_over_user_baseline": "373289790400418148631/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": "139826571/49000000000000000", + "leaf_saving_above_effective": "69826571/49000000000000000", + "main_transform_above_kappa": "131141607/30625000000000000", + "membership_arithmetic_fits_record": "1/700000000", + "microbox_face_corrections_above_kappa": "53898265719/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": "349132857/350000000", + "positive_layout_slack": "1/700000000", + "q_below_effective": "1/700000000", + "q_below_internal": "1/700000000", + "q_below_leaf": "139826571/49000000000000000", + "q_positive": "108393/43750000", + "short_record_fallback": "69826571/70000000", + "source_axis_superpolynomial": "1/700000000", + "sparse_union_movement_above_kappa": "12441406424891607/30625000000000000", + "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" + } + }, + "schema": "native-tensor-strictification-outer-endpoint/1", + "scope": "Source-bound native edits, a finite tensor recipe, exact moment and outer inequalities, and a specified finite uniform rank. Native tensor closure and the PR4359 inherited precision, storage, analytic, fixed-tape and recovery hypotheses are written premises, not a full formal theorem certificate.", + "status": "PASS_CONDITIONAL_TENSOR_OUTER_POINT", + "strictification_source_sha256": "87570ae4bfa02bec87bb1ff55c8429c5b8c6de1934f8088fe3dfb4f3317ceb93", + "tested_saving": "61939/25000000" + }, + "independent_interval_crosscheck": true, + "scope": "Conditional native construction and exact finite arithmetic. The finite word and inherited physical, precision, analytic and fixed-tape proofs are not formally verified or materialized by this checker.", + "source_files": 18, + "status": "PASS_SOURCE_BOUND_CONDITIONAL_NATIVE_TENSOR_IMPROVEMENT", + "strictification": { + "alpha_interval": { + "lower": "0.99999999684043347848885218633343164", + "upper": "0.99999999684043347848885218633343165" + }, + "alpha_upper": "999999999/1000000000", + "controls": { + "gamma_one_rejected": true, + "power_10000_fails_this_conservative_bound": true, + "raw_saving_003_rejected": true, + "unstrictified_native_tariff_rejected": true + }, + "cutoff_base": 4, + "exponent": 15000, + "gamma_interval": { + "lower": "0.99896534203150283241622972954856204", + "upper": "0.99896534203150283241622972954856205" + }, + "gamma_upper": "999/1000", + "materialized_tensor_word": false, + "native_inventory": { + "ambient_rank": 57, + "controls": { + "raw_rule_not_strictly_separated": true, + "whole_idle_missing_phase_rejected_count": 224, + "wrong_intermediate_center_rejected": true + }, + "fresh_helper_fields": 2856, + "main_fields": 672, + "native_scalar_allowance": 1147304, + "paid": { + "1": 17409, + "16": 448, + "2": 4991, + "3": 1568, + "4": 714, + "5": 140, + "8": 504 + }, + "paid_calls": 25774, + "productive_fields": 3528, + "rank_surplus": 224, + "restored_native_centers": 56, + "schema": "native-all-fresh-full-idle-inventory/1", + "scope": "Exact finite all-fresh controller inventory. Native all-column closure is inherited; the raw rule requires the separate tensor strictification before the old strict compiler applies.", + "source_head": "da637c87c89482bc4c86be36bd0071b3d400dbed", + "source_sha256": { + "research/kappa-0023-productive-jobs/dependencies/kappa-next-regime/direct-decoder/sources/DATA-PHASES.json": "c5916ff312678f12aba403847643fbbc29f643acec60bdf836fa56cd3e8251fa", + "research/kappa-rebuild/complex/fresh-certificates/THREE-base-HELPER-BOUNDARIES.json.gz": "f90517e395bde58c72cacd5d3481c4ea31d459fe4535384ac16547ac40460555", + "research/kappa-rebuild/complex/full-identity-certificates/RESULT.json": "943d5fad2fc529f470df05a35446e07ecaef7344abfce450d2c2eb2c9b3798f6", + "research/kappa-rebuild/complex/full-identity-certificates/THREE-base-FULL-IDENTITY-CANONICAL.json.gz": "6418ec3da24d548a57f5c3fe5b9062c26c9478e638504a61c387f5cfb5f4ed61", + "research/kappa-rebuild/complex/full-identity-certificates/THREE-base-FULL-IDENTITY-NATIVE.json.gz": "c54b0a3e129d28e6dbf74fa731fc3bb70fe3c6705f07256750fbecddcc842d39", + "research/kappa-rebuild/complex/full_identity_rebuild.py": "9af2ffbb0038c92e2a7d281081b0daaeadce75b11b566e5427845dc1af91e33d", + "research/kappa-rebuild/controller/P3-NATIVE-COVER.json.gz": "facfc6d6ecde151afb7e6a167776f3fdaac1c816e785a21a39f7f0bfd9140f3f", + "research/kappa-rebuild/controller/p3_native_cover.py": "fae71fcbbd20b9ee73b049cf6f43ea1d048217fb15feb6055a007e47da3363fe", + "research/kappa-rebuild/transfer-audit/p3_cover_audit.py": "a0fe9a26f77556e83b31b0c91fea909d6f3d8209d0f9f7ad4e5bc1375d33615e" + }, + "status": "PASS_ACTUAL_ARBITRARY_HELPERS_AND_COMPLETE_PHASE_CORRECT_IDLE_JOBS", + "targets": { + "25": 448, + "5": 196, + "57": 224, + "6": 126, + "7": 392, + "8": 651, + "9": 1491 + }, + "whole_idle_profile": { + "16": 448, + "8": 448 + } + }, + "new_max_paid_encoding": "4^15000", + "new_max_target_encoding": "57^15000", + "new_min_target_encoding": "5^15000", + "normalized_strict_moment_upper": { + "lower": "0.99998560745522845202872016550689448", + "upper": "0.99998560745522845202872016550689449" + }, + "paid": { + "1": 17409, + "16": 448, + "2": 4991, + "3": 1568, + "4": 714, + "5": 140, + "8": 504 + }, + "paid_rank_one_moment": 46851, + "schema": "native-tensor-cutoff-strictification/1", + "scope": "The exact finite construction is specified by synchronized native substitution and paid-axis splitting. This receipt proves its sufficient moment and separation inequalities, conditional on the documented native interfaces; it is not a formal whole-word or multiplication-theorem verification.", + "source_sha256": { + "research/kappa-rebuild/architecture/mixed_target_probe.py": "011c3c9d0cf81103dc84d709a0e36793eb7c5ae3f23c85eac27650ef13afa04a" + }, + "status": "PASS_SOURCE_BOUND_TENSOR_STRICTIFICATION", + "strict_moment_verified": true, + "strictification_gap": { + "lower": "0.00001439254477154797127983449310551", + "upper": "0.00001439254477154797127983449310552" + }, + "target_rank_one_moment": 47075, + "targets": { + "25": 448, + "5": 196, + "57": 224, + "6": 126, + "7": 392, + "8": 651, + "9": 1491 + }, + "tested_saving": "61939/25000000", + "theta_upper": "7/8" + } +} diff --git a/research/pr4412-pr4414-moment-check/vendor/4412-TENSOR.md b/research/pr4412-pr4414-moment-check/vendor/4412-TENSOR.md new file mode 100644 index 000000000..c7c28b4d2 --- /dev/null +++ b/research/pr4412-pr4414-moment-check/vendor/4412-TENSOR.md @@ -0,0 +1,247 @@ +# Native tensor composition followed by strict rank cutoff + +This note constructs a new finite mixed supplier from the source-bound native +inventory in [NATIVE.md](NATIVE.md). It then restores the strict rank separation +required by PR4359's compiler. The native program and interfaces come from +PR4359 at `da637c87c89482bc4c86be36bd0071b3d400dbed`; its integer lockstep +compiler builds on Jacob Alan Sussman's Theorem 1G. Apache-2.0; substantial +OpenAI/Codex assistance. + +The result is conditional on the source arbitrary-input native words, +whole-job adapters, complete spectators, scalar and movement primitives, and +finite-program closure. It does not infer native correctness from a moment +histogram. The large new word is defined by finite algorithms and is not +materialized here. + +## 1. A native product of two mixed units + +Let a unit U have productive roles indexed by i, with canonical target ranks +`k_i`, and a chronological list of paid ranks `r_l`. Let a second unit V have +roles indexed by j, target ranks `h_j`, and chronological paid ranks `s_a`. +Every role is a distinct arbitrary complete array. Owned work fields have +separate identities and are not counted as productive inputs. +As in the source unit and its products, assume each native ambient rank is +its maximum productive rank and every paid rank fits that ambient space. + +For each productive V role j, instantiate one U word at column multiplicity +`h_j`. Its productive arrays are the grid `(i,j)`. Use one common ambient +space of rank `max_i(k_i)*max_j(h_j)`, with the source whole-job embeddings +and complete spectators. Each U copy receives its own owned work fields. + +Execute these U copies in lockstep through their common chronological paid +list. The all-column word has the same list of operations at every positive +column count. At paid position l, pause every U copy. Copy j requests one +complete canonical job of rank `r_l*h_j` on its designated physical owner. +These owners are distinct across j, since they belong to distinct U copies. +They may be productive fields or U-owned centers holding correlated data. + +Use them as the productive roles of one V invocation at column multiplicity +`r_l`. Its j-th target is exactly the required rank `h_j*r_l`. Apply the +permitted complete-job coordinate matchers before the V call and undo them +after its completed endpoint. These matchers align arbitrary equal-rank axis +subsets; they do not relabel intermediate scalar contacts. The V call is +correct on all its distinct arbitrary input arrays, including correlated +values. Its own owned fields are fresh and distinct from every U field. + +Complete V, restore all its whole-job adapters, and only then resume the +paused U copies. Never mix early and late requests of the same U copy in one +V invocation. This establishes chronology and excludes cyclic dependencies. + +At the end, each `(i,j)` field has received the canonical rank `k_i*h_j` +job. The remaining paid calls, in the actual nested order, have ranks +`r_l*s_a`. Consequently, for any exponent tau, + +``` +target_moment(U product V) = target_moment(U)*target_moment(V), +paid_moment(U product V) = paid_moment(U)*paid_moment(V). +``` + +This is explicit substitution of complete array programs. Scalar gates +remain scalar gates on roles. No claim that tensor power distributes over +matrix addition is used. + +All intermediate U and V work fields persist until their actual owners clear +them. A safe allocation is one full bank per instantiated unit; every bank +is supplied, initialized, parked, and erased, with no productive credit. +There are only finitely many banks and operations in a fixed product word. +The source finite closure theorem must be applied with these new constants. + +Iterating this construction n times gives exactly `B^n` productive roles, +target moments `T_tau^n`, and paid moments `P_tau^n`. The minimum and maximum +target ranks become `k_min^n` and `m^n`. Each finite word accepts all further +positive tensor multiplicities: lift every coordinate and every whole-job +matcher, while retaining the same chronological scalar word. + +## 2. Restore strict separation by splitting only paid jobs + +Write `tau=1-C`, where `0J`, write `R=q*J+r`, with `0<=rJ`. The zero-remainder case omits the last call. +Unsplit lower-rank calls retain their original charge. If `P_1` is the base +unit's paid rank-one moment, the n-fold word therefore has complete paid +tau-moment at most + +``` +P_tau^n + 2*P_1^n/J^C. +``` + +This deliberately overcounts the original cost of the replaced large jobs. +It includes all paid calls, including those made on owned centers. + +Choose `J=b^n` for an integer `1max(1/(1-a),3/(1-g))`. The elementary bound +`x^n<=1/(1+n*(1-x))` gives `a^n<1/2` and `g^n<1/4`. The present certificate +is much smaller because it retains the exact rational power of g instead. + +## 3. Exact source-bound application + +The audited native construction gives each local helper its own arbitrary +productive field and pays each retained main idle window in full, as proved +in NATIVE.md. Its complete invoice is + +``` +targets = {5:196, 6:126, 7:392, 8:651, 9:1491, 25:448, 57:224}, +paid = {1:17409, 2:4991, 3:1568, 4:714, 5:140, 8:504, 16:448}. +``` + +There are 3,528 productive fields. The exact rank-one moments are +`T_1=47075`, `P_1=46851`, leaving the original surplus 224. The raw unit has +paid rank 16 and productive rank 5, so it cannot directly use the source +compiler's strict separation condition. + +At tested saving `C=0.00247756=61939/25000000`, exact rational elementary +function enclosures prove + +``` +alpha < 999999999/1000000000, +gamma = P_1/(4^C*T_tau) < 999/1000. +``` + +Use `n=15000`, `J=4^15000`. A directly verified rational inequality is + +``` +1/(1+15000/10^9) + 2*(999/1000)^15000 < 1. +``` + +The certified surplus is greater than `0.00001439`. Thus this finite word +has a strict mixed moment at the tested saving, with + +``` +minimum productive rank = 5^15000, +maximum productive rank = 57^15000, +maximum paid rank <= 4^15000. +``` + +The compiler's exit exponent satisfies +`theta<=log(4)/log(5)<7/8`, by the exact integer inequality `4^8<5^7`. +Unlike a cutoff only one below `5^15000`, this construction retains a fixed +gap `h=1/8` for the subsequent compiler bound. + +Run the source-bound arithmetic certificate from the repository root: + +```sh +python3 -I -B research/pr4359-tensor-strictification/strictification.py +``` + +The program first rechecks the native invoice. It then verifies both ratio +bounds and the complete power inequality, rejects a failed smaller trial +power under these particular conservative bounds, rejects gamma equal to +one, and rejects the unsupported raw saving 0.003. These are scoped checks +of the construction's sufficient inequalities; no minimal power is claimed. + +## 4. Applying the existing uniform compiler + +The new finite unit satisfies the same arbitrary-input, whole-job adapter, +spectator, chronological, and owned-storage contracts, together with strict +separation and a strict tested superpotential. Its positive rank-one surplus +is `47075^15000-46851^15000`; paid splitting preserves that total. The source +uniform compiler therefore applies at every strictly smaller positive saving. + +For an effective explicit bound, let `t=1-C`, choose a desired uniform +exponent `z>t`, and put `z0=(t+z)/2`, `delta=z0-t`, and `h=1/8`. The source +exit estimate with the new m and r_max gives, for `x>=m`, + +``` +m*E(x)/x <= 4^n*57^(n/8)*x^(-1/8) + < 2^((11/4)*n)*x^(-1/8), +-log2(z0*m^(z0-1)) < 1+6*n*(1-z0), +``` + +where the second inequality uses `z0>1/2`. It follows that + +``` +H0 = ceil(((11/4)*n*delta+1+6*n*(1-z0))/(h*delta)), +H1 = floor(H0*(1-z0)/(z-z0))+1, +N = 2^H1 +``` + +is sufficient, provided `H0>=6*n` covers the finite base range. The endpoint +certificate checks this condition and both strict inequalities at its chosen +uniform saving. The proof is the same complement induction with the actual +complement coefficient; it does not reuse the old exit constant 16. + +After choosing N, recalculate the finite unit count, productive width, paid +leaf count, scalar word, owned storage, and precision/row constants from this +new exact word. Every such quantity is fixed before the eventual input grows. +The inherited analytic decomposition, permitted physical primitives, +fixed-tape model, and outer transfer remain conditional premises. + +In particular, count raw native instances through both the tensor +substitution and the final uniform compiler, rather than counting each +large tensor macro as one unit. If this expanded count is `U_raw`, allocate +`O=U_raw` complete owned center banks. Let `W` and `P` be the final uniform +productive width and rank-one paid count. Count every non-scalar native +record and complete normalization in the new expanded word as `R`; this +includes the additional whole idle-window calls and every compiler/product +adapter. The unchanged scalar words have allowance `1147304*U_raw`. +Whole-job coordinate permutations and unit phases add no coefficient +height, but the source's conservative eight-per-record allowance gives +the safe new charge `G=1147304*U_raw+8*R`. All actual route work is charged +separately. This uses the new count R instead of reusing the old 460 paid +completion normalizers or old numerical G envelope. Substitute + +``` +Z = W+O, +E = 64*(Z+N+P+G+1)^3, +B = P+E, +C0 = 32*N*B^2. +``` + +The source completed-child semantic recurrence is then +`A(e)<=A(floor(e/N))+P*floor(e/N)+E`, giving `A(e)<=2*B*e` and the +same form of linear outer guard. No single center per tensor macro is +assumed. Allocated bank count, finite movement cost, and borrowed row stock +all use the fully expanded word. Reusing the source small-word numerical +constants without this substitution would not establish the precision or +storage interface. + +Open next questions are to optimize the cutoff base and finite tensor power, +reduce the effective uniform rank, and certify stronger native mergers. A +favorable histogram alone would not justify any such native change. diff --git a/research/pr4412-pr4414-moment-check/vendor/4414-RESULT.json b/research/pr4412-pr4414-moment-check/vendor/4414-RESULT.json new file mode 100644 index 000000000..e3bc60a35 --- /dev/null +++ b/research/pr4412-pr4414-moment-check/vendor/4414-RESULT.json @@ -0,0 +1,283 @@ +{ + "endpoint": { + "compiler": { + "H0": 126106333450000, + "H1": 473129651134046950001, + "N_encoding": "2^473129651134046950001", + "delta": "1/1400000000", + "exit_coefficient_log2_upper": "740625/2", + "final_strict_power_gap": "1/1400000000", + "h": "1/32", + "materialized_tensor_rule_or_uniform_word": false, + "negative_log2_eta_upper": "11259493/4000", + "paid_max_bound_encoding": "floor((19/4)^150000)", + "rank_one_induction": "108769^n > 108257^n, and splitting preserves total rank", + "t": "24933003/25000000", + "target_max_encoding": "105^150000", + "target_min_encoding": "5^150000", + "tensor_power": 150000, + "theta_upper": "31/32", + "z": "139624817/140000000", + "z0": "1396248169/1400000000" + }, + "gain_over_PR4359": "37987/100000000", + "gain_over_PR4405": "18739/50000000", + "gain_over_allfresh_p3": "2529/12500000", + "kappa": "267987/100000000", + "ledger_source_sha256": "d097e55f06c3f244f2074ffd7c1a0a5f3c4b4b6a6accf9619d1dde5c0ae85e15", + "minimum_outer_margin": "262265511/61250000000000000", + "negative_controls": { + "closed_epsilon": { + "actual_logarithmic_gamma_guard": "0", + "epsilon_below_one": "0", + "gaussian_above_main": "-703467/61250000000000000", + "global_gamma_power_slack": "-1/7000000000", + "new_semantic_guard_with_C1_one": "0", + "source_axis_superpolynomial": "0" + }, + "closed_uniform_gap": { + "new_complex_uniform_saving_above_b": "0" + }, + "insufficient_BIT": { + "actual_bit_above_effective": "-265913/700000000" + }, + "unfunded_outer_point": { + "boundary_algebraic_matrix_above_kappa": "-262734489/61250000000000000", + "fused_gaussian_above_kappa": "-263203467/61250000000000000", + "global_coordinate_router_above_kappa": "-3/700000000", + "group_bit_router_above_kappa": "-1405627739/490000000000000000", + "main_transform_above_kappa": "-350234489/61250000000000000" + } + }, + "outer": { + "functional_checks": { + "fixed_halo_explicit_metadata_branch": "13475000001/175000000", + "new_BIT_row_stock_sublinear_in_active_group": "697899997009/700000000000", + "new_semantic_group_guard": "3/700000000" + }, + "margins": { + "boundary_algebraic_matrix": "164142387265511/61250000000000000", + "fused_gaussian": "164142386796533/61250000000000000", + "global_coordinate_router": "1875913/700000000", + "group_bit_router": "1313139794372261/490000000000000000", + "group_scans": "349999999/350000000", + "main_transform": "164142299765511/61250000000000000", + "microbox_face_corrections": "13475000001/175000000", + "polynomial_products": "699999999/700000000", + "sparse_union_movement": "25046954887265511/61250000000000000" + }, + "parameters": { + "a": "1875913/700000000", + "b": "937957/350000000", + "beta": "699999997/700000000", + "bit_saving": "27/10000", + "cap_xi": "55671954799765511/61250000000000000", + "complex_uniform_saving": "375183/140000000", + "d": "1/700000000", + "epsilon": "699999999/700000000", + "kappa": "267987/100000000", + "lambda_": "7978561/8000000", + "lambda_prime": "87265511/87500000", + "layout": "1/700000000", + "q": "234489/87500000", + "r0": "1/7000000000", + "stop": "1/700000000", + "tested_saving": "66997/25000000" + }, + "strict_checks": { + "actual_bit_above_effective": "14087/700000000", + "actual_logarithmic_gamma_guard": "1/700000000", + "actual_logarithmic_group_guard": "5578045331484489/30625000000000000", + "alpha_logarithm_absorption": "1/7000000000", + "boundary_algebraic_matrix_above_kappa": "349765511/61250000000000000", + "cap_above_band": "25046954799765511/61250000000000000", + "cap_below_cell": "5578045112734489/61250000000000000", + "cap_below_phase_cell_power": "66828045200234489/61250000000000000", + "complex_above_effective": "1/700000000", + "complex_below_one_over_32": "9999543/350000000", + "complex_endpoint": "1/350000000", + "epsilon_below_one": "1/700000000", + "epsilon_positive": "699999999/700000000", + "fine_prime_halo_umbrella": "7/2", + "fused_gaussian_above_kappa": "349296533/61250000000000000", + "gaussian_above_main": "43515511/30625000000000000", + "global_coordinate_router_above_kappa": "1/175000000", + "global_gamma_power_slack": "9/7000000000", + "group_below_dimension": "1/350000000", + "group_bit_router_above_kappa": "3494372261/490000000000000000", + "group_gauge_power_slack": "5578045327109489/30625000000000000", + "group_key_fits_record": "1/350000000", + "group_positive": "699999997/700000000", + "group_scans_above_kappa": "698124089/700000000", + "halo_covers_generic_inverse_radius": "5", + "improvement_over_user_baseline": "474449790400418148631/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": "699062043/245000000000000000", + "leaf_saving_above_effective": "349062043/245000000000000000", + "main_transform_above_kappa": "262265511/61250000000000000", + "membership_arithmetic_fits_record": "1/700000000", + "microbox_face_corrections_above_kappa": "10779624819/140000000", + "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": "69812409/70000000", + "positive_layout_slack": "1/700000000", + "q_below_effective": "1/700000000", + "q_below_internal": "1/700000000", + "q_below_leaf": "699062043/245000000000000000", + "q_positive": "234489/87500000", + "short_record_fallback": "349062043/350000000", + "source_axis_superpolynomial": "1/700000000", + "sparse_union_movement_above_kappa": "24882812849765511/61250000000000000", + "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" + } + }, + "schema": "native-p6-tensor-strictification-outer-endpoint/1", + "scope": "Source-bound native edits, a finite tensor recipe, exact moment and outer inequalities, and a specified finite uniform rank. Native tensor closure and the PR4359 inherited precision, storage, analytic, fixed-tape and recovery hypotheses are written premises, not a full formal theorem certificate.", + "status": "PASS_CONDITIONAL_P6_OUTER_POINT", + "strictification_source_sha256": "ea90705f895a896f29b0107e37b781ca05d40a1caef9e959838dbf07318624a0", + "tested_saving": "66997/25000000" + }, + "independent_interval_crosscheck": true, + "scope": "Conditional native construction and exact finite arithmetic. The finite word and inherited physical, precision, analytic and fixed-tape proofs are not formally verified or materialized by this checker.", + "source_files": 21, + "status": "PASS_SOURCE_BOUND_CONDITIONAL_P6_NATIVE_TENSOR_IMPROVEMENT", + "strictification": { + "alpha_interval": { + "lower": "0.99999998243467076019221523488048225", + "upper": "0.99999998243467076019221523488048226" + }, + "alpha_upper": "99999999/100000000", + "controls": { + "integer_cutoff_four_rejected": true, + "one_decay_block_rejected": true, + "undamped_tail_rejected": true + }, + "cutoff_denominator": 4, + "cutoff_encoding": "floor((19/4)^150000)", + "cutoff_numerator": 19, + "decay_block_count": 15, + "decay_block_length": 10000, + "exponent": 150000, + "gamma_interval": { + "lower": "0.99986298028286378831364421899719657", + "upper": "0.99986298028286378831364421899719658" + }, + "gamma_upper": "9999/10000", + "materialized_tensor_word": false, + "native_inventory": { + "artifact_hash_encoding": "Uncompressed UTF-8 JSON, sort_keys=True, separators=(comma,colon)", + "artifact_sha256": "7302f2e16e26ddf67d9880621d27dd3eb292524a65b2147194f7ef36a50529b1", + "contacts": 5824, + "dimension": 105, + "fresh_helper_fields": 5304, + "keep": 25279, + "limits": "Finite exact physical controller admission; inherited all-column local word, tensor strictification, new full-word precision/stock and outer transfer remain written proof obligations.", + "main_fields": 1344, + "native_scalar_allowance": 2166056, + "native_source_gate": "PASS_ACTUAL_ARBITRARY_HELPERS_AND_COMPLETE_PHASE_CORRECT_IDLE_JOBS", + "negative_controls": { + "omitted_endpoint_translation_rejected": 672, + "wrong_native_orientation_rejected": true + }, + "p": 6, + "paid": { + "1": 32331, + "16": 448, + "2": 9269, + "3": 2912, + "32": 448, + "4": 1326, + "48": 224, + "5": 260, + "8": 1224 + }, + "paid_calls": 48442, + "productive_fields": 6648, + "rank_margin": 512, + "scalar_allowance": 2166056, + "schema": "source-bound-p6-all-fresh-complete-native-controller/1", + "source_sha256": { + "research/kappa-0023-productive-jobs/dependencies/kappa-next-regime/direct-decoder/sources/DATA-PHASES.json": "c5916ff312678f12aba403847643fbbc29f643acec60bdf836fa56cd3e8251fa", + "research/kappa-rebuild/bit/COMPLEX-CONTROLLER-FACTOR-P6.json": "573e797a4d1a37c6a9e419216ff53c7d9e2fe4e8a8384e01d2cc344f87d6d05e", + "research/kappa-rebuild/complex/fresh-certificates/THREE-base-HELPER-BOUNDARIES.json.gz": "f90517e395bde58c72cacd5d3481c4ea31d459fe4535384ac16547ac40460555", + "research/kappa-rebuild/complex/full-identity-certificates/RESULT.json": "943d5fad2fc529f470df05a35446e07ecaef7344abfce450d2c2eb2c9b3798f6", + "research/kappa-rebuild/complex/full-identity-certificates/THREE-base-FULL-IDENTITY-CANONICAL.json.gz": "6418ec3da24d548a57f5c3fe5b9062c26c9478e638504a61c387f5cfb5f4ed61", + "research/kappa-rebuild/complex/full-identity-certificates/THREE-base-FULL-IDENTITY-NATIVE.json.gz": "c54b0a3e129d28e6dbf74fa731fc3bb70fe3c6705f07256750fbecddcc842d39", + "research/kappa-rebuild/complex/full_identity_rebuild.py": "9af2ffbb0038c92e2a7d281081b0daaeadce75b11b566e5427845dc1af91e33d", + "research/kappa-rebuild/controller/P3-NATIVE-COVER.json.gz": "facfc6d6ecde151afb7e6a167776f3fdaac1c816e785a21a39f7f0bfd9140f3f", + "research/kappa-rebuild/controller/p3_native_cover.py": "fae71fcbbd20b9ee73b049cf6f43ea1d048217fb15feb6055a007e47da3363fe", + "research/kappa-rebuild/transfer-audit/p3_cover_audit.py": "a0fe9a26f77556e83b31b0c91fea909d6f3d8209d0f9f7ad4e5bc1375d33615e", + "research/kappa-rebuild/transfer-audit/p3_native_audit.py": "5504a55a50546418d10c522984438cdeedb44993f7c1dab7bd4aa1ae0515d902" + }, + "status": "PASS_EXACT_LAURENT_ALL_MAIN_CONTACTS_ENDPOINTS_AND_FULL_IDLE_PHASES", + "targets": { + "105": 224, + "25": 448, + "41": 448, + "5": 364, + "57": 224, + "6": 234, + "7": 728, + "8": 1209, + "9": 2769 + }, + "whole_idle_profile": { + "16": 448, + "32": 448, + "48": 224, + "8": 1120 + } + }, + "new_max_target_encoding": "105^150000", + "new_min_target_encoding": "5^150000", + "normalized_moment_upper_rational": "16386003/16408576", + "paid": { + "1": 32331, + "16": 448, + "2": 9269, + "3": 2912, + "32": 448, + "4": 1326, + "48": 224, + "5": 260, + "8": 1224 + }, + "paid_rank_one_moment": 108257, + "schema": "p6-rational-cutoff-tensor-certificate/1", + "scope": "Exact sufficient moment inequalities for the documented finite native substitution and floor-cutoff construction. The native audit and inherited all-column, precision, storage, analytic and fixed-tape premises remain separate; no full multiplication theorem is formally verified.", + "source_sha256": { + "research/kappa-rebuild/architecture/mixed_target_probe.py": "011c3c9d0cf81103dc84d709a0e36793eb7c5ae3f23c85eac27650ef13afa04a" + }, + "status": "PASS_EXACT_P6_RATIONAL_CUTOFF_STRICTIFICATION", + "strict_moment_verified": true, + "strictification_gap": { + "lower": "0.00137568305744508237643534697953070", + "upper": "0.00137568305744508237643534697953071" + }, + "strictification_gap_rational": "22573/16408576", + "target_rank_one_moment": 108769, + "targets": { + "105": 224, + "25": 448, + "41": 448, + "5": 364, + "57": 224, + "6": 234, + "7": 728, + "8": 1209, + "9": 2769 + }, + "tested_saving": "66997/25000000", + "theta_upper": "31/32" + } +} diff --git a/research/pr4412-pr4414-moment-check/vendor/4414-TENSOR.md b/research/pr4412-pr4414-moment-check/vendor/4414-TENSOR.md new file mode 100644 index 000000000..897c0c27a --- /dev/null +++ b/research/pr4412-pr4414-moment-check/vendor/4414-TENSOR.md @@ -0,0 +1,205 @@ +# Native tensor substitution with a rational rank cutoff + +This argument applies to the actual all-fresh p6/keep25279 native word in +NATIVE.md, at ambient rank105. It retains PR4359's all-column arbitrary-input +word, complete spectators, permitted whole-job adapters, finite-program +closure, and uniform compiler. The integer compiler is attributed to Jacob +Alan Sussman's Theorem1G; the controller and native local word come from +zxv's PR4359. Apache-2.0; substantial OpenAI/Codex assistance. + +The moment bounds below certify a finite construction under these native +premises. The large word is specified by exact algorithms; its instruction +list has not been materialized. The selected frontier is unchanged. + +## 1. Actual native product and field ownership + +Let native mixed unit U have target roles i of ranks k_i and chronological +paid ranks r_l. Let V have target roles j of ranks h_j and paid ranks s_a. +As in the present word and its products, each ambient rank equals the +maximum target rank, and all its paid ranks fit that ambient space. + +For every V target role j, instantiate a separate U copy at column count h_j. +Its productive fields have labels(i,j), all distinct arbitrary complete +arrays. Work in the common product ambient space, completing all unused +coordinates as arbitrary spectators. Give every copy its own owned center +banks. These are initialized and erased, and receive no productive credit. + +Run the U copies in lockstep through their common scalar and paid-call list. +At paid position l, pause every copy. Copy j requests a rank r_l*h_j job +on its current physical owner. These owners are distinct across the copies; +some may be owned centers containing correlated values. One V invocation at +column count r_l receives those fields as its j-indexed productive roles. +Wrap this complete invocation with the permitted role-specific whole-job +axis matchers. Its endpoints provide exactly the requested ranks h_j*r_l. +Its own centers have separate identities. + +Finish V, undo all its complete-job matchers, and only then resume U. +Never combine different paid positions of the same U copy. This is a finite +acyclic chronological program, and arbitrary-input correctness permits +correlated values in distinct physical input slots. No scalar input is +copied to manufacture additional productive credit. + +The final independent(i,j) endpoints have ranks k_i*h_j; the remaining +paid calls have ranks r_l*s_a. Thus target and paid moments multiply. +Iterating v times gives target moment T_tau^v and paid moment P_tau^v, +with minimum target5^v and maximum target105^v. This is substitution of +whole native programs; it never tensors a sum of matrix operators. + +The same recipe works at every further positive column multiplicity by +lifting each fixed coordinate/phase generator and matcher. The scalar word +remains unchanged. One owned bank per raw unit instance is a safe finite +allocation, retaining every bank until its actual owner clears it. + +## 2. Integer splitting at a rationally specified cutoff + +Write tau=1-C with0J by consecutive +jobs on disjoint axes of ranks J,...,J,r, where R=qJ+r and0<=r1. It also rejects an undamped +tail and a single10000-step decay block under these sufficient inequalities. +No minimal tensor power or optimal cutoff is claimed. + +## 4. Effective uniformization bound + +The new mixed unit has m=105^v, k_min=5^v and r_max<=J. Exact integer tests + +``` +19^32 < 4^32*5^31, +19^4 < 4^4*2^9, +105 < 2^7 +``` + +give theta<31/32. Put h=1/32. For x>=m, the compiler exit-rank estimate is + +``` +m*E(x)/x <= r_max*m^h*x^(-h) + < 2^((79/32)*v)*x^(-h). +``` + +For a desired uniform exponent z>t=1-C, put z0=(t+z)/2 and delta=z0-t. +When z0>1/2, the actual complement coefficient eta=z0*m^(z0-1) obeys + +``` +-log2(eta) < 1+7*v*(1-z0). +``` + +Consequently the fully rational sufficient formulas are + +``` +H0 = ceil((((79/32)*v)*delta+1+7*v*(1-z0))/(h*delta)), +H1 = floor(H0*(1-z0)/(z-z0))+1, +N = 2^H1. +``` + +Check H0>=7v so that the threshold covers every base rank. Below this +threshold the positive rank-one surplus gives L(x)<=x. Above it, the source +complement induction gives L(x)<=A*x^z0, with A=(2^H0)^(1-z0), and the +strict H1 inequality proves L(N)1/4 estimate are not reused. + +## 5. New owned-field, coefficient and physical constants + +Expand both the native tensor product and the final uniform compiler. +Let U_raw count the resulting actual raw p6-unit instances. Allocate +O=U_raw full owned-center banks, regardless of the number of tensor macros. +Let W be the final productive width, P the final rank-one paid count, and R +the count of non-scalar native records and complete normalizations in the +expanded word, including every new product/compiler route. + +The audited raw scalar allowance is2166056. A conservative coefficient +envelope is G=2166056*U_raw+8R, retaining the source's allowance for +non-scalar records; actual coordinate movement is paid separately. Unit +phases and coordinate permutations have zero coefficient height. Substitute + +``` +Z=W+O, +E=64*(Z+N+P+G+1)^3, +B=P+E, +C0=32*N*B^2. +``` + +The completed-child semantic recurrence then has the original valid form +`A(e)<=A(floor(e/N))+P*floor(e/N)+E`, implying A(e)<=2B*e. Its use requires +the source completed-child semantics and common fine-grid implementation. +All allocated fields, scalar/phase records, role routes, parking and borrowed +stock are computed from the expanded word. No source small-word numerical +reserve is substituted for this count. + +These finite constants may be enormous, but they are fixed before the +eventual multiplication input varies. The inherited physical primitive, +analytic, prime-padding, fixed-tape and exact-recovery premises remain +conditional. A finite exact tariff certificate is not a full formal +integer-multiplication theorem proof. + +Open next questions are to reduce the sufficient tensor power or cutoff +constant, derive smaller uniform ranks, and construct a better native +controller with independently audited contacts, phases and helper ownership. diff --git a/research/pr4412-pr4414-moment-check/vendor/NOTICE.md b/research/pr4412-pr4414-moment-check/vendor/NOTICE.md new file mode 100644 index 000000000..2eca7b474 --- /dev/null +++ b/research/pr4412-pr4414-moment-check/vendor/NOTICE.md @@ -0,0 +1,14 @@ +# Vendored files + +Byte-identical copies, checked by SHA256 in `verify.py`. They are copied because these PR heads +are not reachable from canonical main. + +| Vendored file | Source | Head | Git blob | +| --- | --- | --- | --- | +| `4412-TENSOR.md` | [#4412](https://github.com/CrocSwap/integer-mult-bounds/pull/4412) `research/pr4359-tensor-strictification/TENSOR.md` | `9f0df9bf6f49942faf5f31389e7e387fdfe511b3` | `c7c28b4d2590a6fa06383fbdf1c7b56084269013` | +| `4412-RESULT.json` | same package, `RESULT.json` | same | `d9f027061d2a899b50883813c56b08ca5cc746d0` | +| `4414-TENSOR.md` | [#4414](https://github.com/CrocSwap/integer-mult-bounds/pull/4414) `research/pr4359-p6-fresh/TENSOR.md` | `90da4b0ab894350ca12cac9110cc6da2225d18af` | `897c0c27a74c4121f940e3a50e2262434520d7e6` | +| `4414-RESULT.json` | same package, `RESULT.json` | same | `e3bc60a3541266142f0204a2ee36456f64e7cf37` | + +1337isnot1337's work with OpenAI Codex assistance, building on zxv's #4359; Apache-2.0, as those +packages state. diff --git a/research/pr4412-pr4414-moment-check/verify.py b/research/pr4412-pr4414-moment-check/verify.py new file mode 100644 index 000000000..291b97cc9 --- /dev/null +++ b/research/pr4412-pr4414-moment-check/verify.py @@ -0,0 +1,172 @@ +#!/usr/bin/env python3 +"""Independent certified check of the strictification inequalities in #4412 and #4414. + +Both build a tensor power of a native mixed unit with target invoice T and paid invoice P, split paid jobs +at a cutoff J, and need, at saving C (tau = 1 - C), alpha = P_tau/T_tau < 1 and gamma = P_1/(b^C T_tau) < 1: + #4412: J = 4^n, alpha < 1 - 1e-9, gamma < 999/1000, n = 15000, 1/(1+n/1e9) + 2 (999/1000)^n < 1; + #4414: J = floor((19/4)^v), alpha < 1 - 1e-8, gamma < 9999/10000, v = 150000, 1/(1+v/1e8) + 4/2^15 < 1. +X_tau = sum_r n_r r^tau. Exact rational enclosures: ln by atanh after reducing by powers of two, exp by +Taylor with a remainder. Each invoice's limit saving C* (alpha = 1) is also computed. The four inputs are +vendored byte-identically. No code from #4412 or #4414. +Ryanson Jonathan with Claude Code (Claude Opus 5.5) assistance. Apache-2.0. +""" +from fractions import Fraction as Q +import hashlib +import json +from pathlib import Path +import sys + +HERE = Path(__file__).resolve().parent +VENDORED = { + "vendor/4412-TENSOR.md": "d65a39979a0d44ba85123f9e323614caf8efe5585f3b5ea2cb6091c11ce1acc5", + "vendor/4412-RESULT.json": "4b0bbf35d51e25c167327ceba9f969eba2a80bd359d5a92964e1c47ba5bce15d", + "vendor/4414-TENSOR.md": "96e4593ff213a51defba0bcd394deffaa2b9c69292da895cf02d8e33469c27eb", + "vendor/4414-RESULT.json": "d9a04cbbc4235a187c863a463dc2105c71a6b3bffd2129ca082759d9257845cf", +} +PHRASES = { + "4412": ["targets = {5:196, 6:126, 7:392, 8:651, 9:1491, 25:448, 57:224},", + "paid = {1:17409, 2:4991, 3:1568, 4:714, 5:140, 8:504, 16:448}.", + "alpha < 999999999/1000000000,", "gamma = P_1/(4^C*T_tau) < 999/1000.", + "Use `n=15000`, `J=4^15000`.", "1/(1+15000/10^9) + 2*(999/1000)^15000 < 1.", + "The certified surplus is greater than `0.00001439`."], + "4414": ["T = {5:364,6:234,7:728,8:1209,9:2769,25:448,41:448,57:224,105:224},", + "P = {1:32331,2:9269,3:2912,4:1326,5:260,8:1224,16:448,32:448,48:224}.", + "gamma < 9999/10000.", "Take v=150000. The exact finite inequality", + "`(9999/10000)^10000<1/2` gives gamma^v<2^-15.", "1/(1+150000/10^8) + 4/2^15 < 1.", + "<= alpha^v+2^(1+C)*gamma^v < alpha^v+4*gamma^v."], +} + + +def need(condition, message): + if not condition: + raise AssertionError(message) + + +def atanh_ln(x, terms=60): + z = (x - 1) / (x + 1) + s = 2 * sum(z ** (2 * k + 1) / (2 * k + 1) for k in range(terms + 1)) + return s, s + 2 * z ** (2 * terms + 3) / ((2 * terms + 3) * (1 - z * z)) + + +LN2 = atanh_ln(Q(2)) + + +def ln_bounds(x): + """x >= 1 rational""" + k = (x.numerator // x.denominator).bit_length() - 1 + c, d = atanh_ln(x / 2 ** k) + return k * LN2[0] + c, k * LN2[1] + d + + +def exp_bounds(y, terms=40): + """0 <= y <= 1""" + s, term = Q(0), Q(1) + for k in range(terms + 1): + s += term + term = term * y / (k + 1) + return s, s + 3 * term + + +def power_moment(inv, C): + """sum n r^(1-C) = sum n r exp(-C ln r), enclosed""" + lo = hi = Q(0) + for r, n in inv.items(): + if r == 1: + lo, hi = lo + n, hi + n + continue + l_lo, l_hi = ln_bounds(Q(r)) + lo += n * r / exp_bounds(C * l_hi)[1] + hi += n * r / exp_bounds(C * l_lo)[0] + return lo, hi + + + +def ratios(T, P, C, b): + t_lo, t_hi = power_moment(T, C) + p_lo, p_hi = power_moment(P, C) + l_lo, l_hi = ln_bounds(Q(b)) + bc_lo, bc_hi = exp_bounds(C * l_lo)[0], exp_bounds(C * l_hi)[1] + P1 = sum(r * n for r, n in P.items()) + return {"alpha": (p_lo / t_hi, p_hi / t_lo), "gamma": (P1 / (bc_hi * t_hi), P1 / (bc_lo * t_lo))} + + +def limit_saving(T, P, lo, hi): + for _ in range(30): + mid = (lo + hi) / 2 + if ratios(T, P, mid, 4)["alpha"][1] < 1: + lo = mid + else: + hi = mid + return lo, hi + + +def load(tag): + text = (HERE / f"vendor/{tag}-TENSOR.md").read_text() + for p in PHRASES[tag]: + need(p in text, f"#{tag} TENSOR.md: {p[:40]}") + s = json.loads((HERE / f"vendor/{tag}-RESULT.json").read_text())["strictification"] + T = {int(k): v for k, v in s["targets"].items()} + P = {int(k): v for k, v in s["paid"].items()} + ni = s["native_inventory"] + need({int(k): v for k, v in ni["targets"].items()} == T and {int(k): v for k, v in ni["paid"].items()} == P, + f"#{tag}: strictification invoice is the native inventory's") + return s, T, P + + +def check_interval(tag, s, R): + for k in ("alpha", "gamma"): + lo, hi = R[k] + cl = (Q(s[f"{k}_interval"]["lower"]), Q(s[f"{k}_interval"]["upper"])) + need(hi - lo < Q(1, 10**30) and not (hi < cl[0] or lo > cl[1]), f"#{tag} {k} overlaps the recorded interval") + + +def main(): + for rel, digest in VENDORED.items(): + need(hashlib.sha256((HERE / rel).read_bytes()).hexdigest() == digest, f"vendored {rel}") + out = {} + + # #4412 + s, T, P = load("4412") + need((sum(T.values()), sum(r * n for r, n in T.items()), sum(r * n for r, n in P.items()), sum(P.values())) == (3528, 47075, 46851, 25774), "#4412 invoice aggregates") + C = Q(s["tested_saving"]) + need(C == Q(61939, 25000000), "#4412 tested saving 0.00247756") + R = ratios(T, P, C, 4) + need(R["alpha"][1] < Q(999999999, 10**9) and R["gamma"][1] < Q(999, 1000), "#4412 alpha < 1 - 1e-9, gamma < 999/1000") + check_interval("4412", s, R) + n = 15000 + bound = 1 / (1 + n * Q(1, 10**9)) + 2 * Q(999, 1000) ** n + need(bound < 1 and 1 - bound > Q(1439, 10**8), "#4412 closing bound and surplus > 0.00001439") + g = s["strictification_gap"] + need(Q(g["lower"]) <= 1 - bound <= Q(g["upper"]), "#4412 gap inside the recorded interval") + need(max(P) == 16 and min(T) == 5, "#4412 cutoff base 4 lies below the minimum target 5") + Cs = limit_saving(T, P, C, Q(3, 1000)) + need(ratios(T, P, Cs[1], 4)["gamma"][1] < 1, "#4412 gamma < 1 at the limit saving") + out["4412"] = {"alpha": f"{float(R['alpha'][1]):.12f}", "one_minus_alpha": f"{float(1 - R['alpha'][1]):.4e}", + "gamma": f"{float(R['gamma'][1]):.10f}", "gap": f"{float(1 - bound):.10e}", + "limit_saving": f"{float(Cs[0]):.12f}", "headroom": f"{float(Cs[0] - C):.4e}"} + + # #4414 + s, T, P = load("4414") + need((sum(T.values()), sum(r * n for r, n in T.items()), sum(r * n for r, n in P.items()), sum(P.values())) == (6648, 108769, 108257, 48442), "#4414 invoice aggregates") + C = Q(s["tested_saving"]) + need(C == Q(66997, 25000000), "#4414 tested saving 0.00267988") + R = ratios(T, P, C, Q(19, 4)) + need(R["alpha"][1] < 1 - Q(1, 10**8) and R["gamma"][1] < Q(9999, 10000), "#4414 alpha < 1 - 1e-8, gamma < 9999/10000") + check_interval("4414", s, R) + v = 150000 + need(v == 15 * 10000 and Q(9999, 10000) ** 10000 < Q(1, 2), "#4414 (9999/10000)^10000 < 1/2") + need(Q(19, 4) < 5 and Q(2) ** 2 == 4, "#4414 floor cutoff below the minimum target 5^v; 2^(1+C) < 4") + bound = 1 / (1 + v * Q(1, 10**8)) + 4 * Q(1, 2**15) + need(bound == Q(s["normalized_moment_upper_rational"]) == Q(16386003, 16408576) and 1 - bound == Q(s["strictification_gap_rational"]), "#4414 normalized bound and gap") + need(ratios(T, P, C, 4)["gamma"][0] > 1, "#4414 control: integer cutoff base 4 fails the tail (gamma > 1)") + Cs = limit_saving(T, P, C, Q(3, 1000)) + need(ratios(T, P, Cs[1], Q(19, 4))["gamma"][1] < 1, "#4414 gamma < 1 at the limit saving") + out["4414"] = {"alpha": f"{float(R['alpha'][1]):.12f}", "one_minus_alpha": f"{float(1 - R['alpha'][1]):.4e}", + "gamma": f"{float(R['gamma'][1]):.10f}", "gap": str(1 - bound), + "limit_saving": f"{float(Cs[0]):.12f}", "headroom": f"{float(Cs[0] - C):.4e}"} + + print(json.dumps({"status": "PASS_PR4412_PR4414_MOMENT_CHECK", **out, "new_kappa_claimed": False}, indent=1)) + + +if __name__ == "__main__": + sys.exit(main())