From 99007ce1bb6a3d2889ddeb763bbc7546724e1f52 Mon Sep 17 00:00:00 2001 From: lm1909 Date: Thu, 22 Oct 2026 15:54:51 +0200 Subject: [PATCH] Independently check #4635's native kappa step: profile-only delta (no new kappa) Binds the #4630 -> #4635 changed paid ledger to #4610 round-three and the unchanged main controller, recomputes both critical roots (Decimal), finite absorption, both nine-row native ledgers and #4630's five controls. Co-Authored-By: Claude Opus 5.5 --- .../.gitattributes | 1 + .../native-lift-4635-delta-check/README.md | 86 ++++ .../native-lift-4635-delta-check/SOURCES.json | 93 ++++ .../native-lift-4635-delta-check/TASK.json | 106 +++++ .../native-lift-4635-delta-check/VERIFY.json | 22 + .../vendor/pr4610/ARITHMETIC.json | 241 +++++++++++ .../vendor/pr4630/critical_check.py.txt | 49 +++ .../vendor/pr4630/native_ledger.py.txt | 63 +++ .../vendor/pr4630/raw-profile.json | 274 ++++++++++++ .../vendor/pr4635/ARITHMETIC.json | 241 +++++++++++ .../vendor/pr4635/NATIVE-LIFT.md | 104 +++++ .../vendor/pr4635/PARAMETERS.json | 49 +++ .../pr4635/critical_provider_check.py.txt | 71 ++++ .../native-lift-4635-delta-check/verify.py | 402 ++++++++++++++++++ 14 files changed, 1802 insertions(+) create mode 100644 research/native-lift-4635-delta-check/.gitattributes create mode 100644 research/native-lift-4635-delta-check/README.md create mode 100644 research/native-lift-4635-delta-check/SOURCES.json create mode 100644 research/native-lift-4635-delta-check/TASK.json create mode 100644 research/native-lift-4635-delta-check/VERIFY.json create mode 100644 research/native-lift-4635-delta-check/vendor/pr4610/ARITHMETIC.json create mode 100644 research/native-lift-4635-delta-check/vendor/pr4630/critical_check.py.txt create mode 100644 research/native-lift-4635-delta-check/vendor/pr4630/native_ledger.py.txt create mode 100644 research/native-lift-4635-delta-check/vendor/pr4630/raw-profile.json create mode 100644 research/native-lift-4635-delta-check/vendor/pr4635/ARITHMETIC.json create mode 100644 research/native-lift-4635-delta-check/vendor/pr4635/NATIVE-LIFT.md create mode 100644 research/native-lift-4635-delta-check/vendor/pr4635/PARAMETERS.json create mode 100644 research/native-lift-4635-delta-check/vendor/pr4635/critical_provider_check.py.txt create mode 100644 research/native-lift-4635-delta-check/verify.py diff --git a/research/native-lift-4635-delta-check/.gitattributes b/research/native-lift-4635-delta-check/.gitattributes new file mode 100644 index 0000000000..66a5224c92 --- /dev/null +++ b/research/native-lift-4635-delta-check/.gitattributes @@ -0,0 +1 @@ +vendor/** -text diff --git a/research/native-lift-4635-delta-check/README.md b/research/native-lift-4635-delta-check/README.md new file mode 100644 index 0000000000..eee8e1fc43 --- /dev/null +++ b/research/native-lift-4635-delta-check/README.md @@ -0,0 +1,86 @@ +# Independent check: where #4635's +0.0000016099 comes from + +**No new κ.** This package checks Dugongue's native Word RAM line: +#4630 (κ = 0.0030201655, head `f4b974db1f651250a252721cf127d0491a802699`) and #4635 +(κ = 0.0030217754, head `898b0c8e2ca23897c312230988515c2553154f30`). The question: +what changes between them? And does the +0.0000016099 step come from the paid profile +and critical root, or from a native transfer/absorption term? + +## Result + +**The step comes entirely from the changed paid profile, which #4610 supplies. No transfer or absorption term changes.** + +1. **Changed ledger.** The targets (10,928 fields), the helper census {4:28, 7:7, 8:47, 9:326} and the controller are byte-identical across the two PRs. The controller blob `49a2f067…` equals main's `research/joint-helper-lattice/CONTROLLER.json` and has 18 LOCAL calls. #4635's `ARITHMETIC.json` is byte-identical to the one in #4610's round-three package at head `1eb8da6c`. The only change is the local paid profile, by {1:−36, 2:+24, 3:+16, 4:−20, 5:+4} per LOCAL call. That is 18× this change globally: {1:−648, 2:+432, 3:+288, 4:−360, 5:+72}. The local rank mass stays 5,327 and the surplus stays 752. #4630's profile equals main's p16 profile in `compact-joint-compiler/arithmetic/RESULT.json`. +2. **Critical roots.** These were recomputed by an independent method: Decimal ln/exp at 60 digits with bisection, rather than the 2^-128 outward grid of Dillon's engine. The root solves Σ targets·k^θ = Σ paid·r^θ, with one sign change on a grid of (0, 1]. + - #4630 (p16 profile): 1−θ = 0.00302016597701562… + - #4635 (#4610 profile): 1−θ = 0.00302177587077658… + - The raw step is 1.60989376e-6. Both stated brackets are confirmed. +3. **Decomposition.** The κ step 1.6099e-6 exceeds the raw step by only 6.24e-12. The gap between raw saving and κ is 4.770e-10 for #4630 and 4.708e-10 for #4635. The 6.24e-12 is paid from #4630's slightly larger slack. The native lift in NATIVE-LIFT.md is lossless: every κ < min(q_C, 3/32). It therefore contributes nothing numerically. #4635's README already says it does not rediscover the profile or the root. This check confirms that nothing else changes the number. +4. **Finite absorption at N = 2^(10^12).** The proof needs log-margin > 0. Using the true root: + - #4630: margin ≥ 236.8 (stated 646/3) + - #4635: margin ≥ 232.5 (stated 164) + - The largest q_C this N supports is ≈ 0.0030217758354 for #4635 and ≈ 0.0030201659416 for #4630. The stated q_C values are conservative. +5. **Mirror and capacity at the #4635 root.** The worst mirror ratio is 0.56281093, below the stated 0.562811 and below β = 0.564. The capacity is η = 0.98209726, above the stated 0.982097. +6. **#4635 nine-row ledger.** I re-implemented NATIVE-LIFT.md's parameter formulas with Fraction. All of PARAMETERS.json reproduces exactly: q, stop, δ, ε, β, r, layout, ξ, all nine savings and all guards/excesses. The minimum excess is in the main-transform row: 80181306527/1604834840720000000000 ≈ 5.0e-11. Four controls reject: + - κ = q_C + - κ ≥ 3/32 + - #4635's κ on #4630's provider + - an unfused O(Td) Gaussian row, whose saving δ ≈ 1.2e-11 is below κ +7. **#4630 nine-row ledger.** It reproduces: the minimum excess is 1.97983445e-11, in the main row. Each of the five rejecting controls fails for its stated reason: + - `epsilon_one` breaks ε < 1. + - `unfunded_outer_target` breaks the main row. + - `membership_at_edge` breaks the membership guard. + - `normalization_at_edge` breaks the global γ guard. + - `key_fills_whole_word_power` breaks the key guard. + + **Observation:** the group-key guard 1−(β+1−ε) is the same expression as `beta_below_epsilon` (ε−β). It is also strictly weaker than the membership guard (ε−β) − (1−ε). So the key control is implied by the membership control, and the five controls test four independent conditions. This is redundancy, not an error. +8. **Selected frontier.** The selected κ = 0.00302015 (#4470) lies below the p16 raw root 0.0030201659770. This is consistent with #4630's statement that it does not change the p16 root. + +## What is NOT covered + +- Whether #4610's changed word is an admitted canonical provider. This includes the all-fiber identity, the 20 changed native maps, the 26 helper interfaces and absolute phases. #4610 is open and unselected, so #4635's number depends on it. +- The shifted-logarithmic majorant guards U, V, Q, d and the recurrence funding (.048546 > .04282). +- The retained analytic, compiler and recovery proofs, and the native algorithms themselves (fused Gaussian circuits, record products, boundary solver). +- #4635's frame-bridge and transporter lemmas. #4635 attributes no gain to them. + +## Reproduce + +From the repository root (Python 3.12, stdlib only, under 1 s): + +```sh +python3.12 -B research/native-lift-4635-delta-check/verify.py +python3.12 scripts/research_package.py --package research/native-lift-4635-delta-check +``` + +PR-head inputs are vendored under `vendor/` and pinned as `head::` provenance rows in SOURCES.json. The verifier checks every vendored byte against those SHA256 pins. Its four negative controls reject: + +- the #4630 profile against #4635's q_C +- a q_C above the raw root +- a one-byte tamper of the vendored profile +- the #4630 bracket applied to the #4635 profile + +Metadata validation of head pins needs the PR-head commits to be present locally, for example via `git fetch origin pull/4630/head pull/4635/head pull/4610/head`. + +## Open next questions + +The structured list is in [TASK.json](TASK.json). + +1. Is #4610 head `1eb8da6c`'s round-three word an admitted canonical provider? A first step is an independent replay of its 20 changed native maps and 26 helper interfaces on all 632 columns. +2. Do the funded-majorant guards hold for the changed profile under an independent enclosure? + +## Credit + +Credit goes to the predecessors who did the work: + +- Dugongue, for #4630, #4635 and the #4554 native assembly +- Cao Yifan, for the #4610 round-three joint-helper and native-map profile, which supplies the whole numerical step +- Cinna Davis and the #4470 joint-helper/controller lineage +- Dillon (#4532/#4535), for the critical-root criterion and engine +- zxv and Jacob Alan Sussman, for the compiler and integer matching +- Ryanson Jonathan, for mirror windows and the #4614–#4616 checks of an earlier #4610 head +- Vlado Vojdanovski (#1673), the #1758 gauge-free authors, Chafik Boukhalfa (#1786) and Tim Trudgian +- Harvey and van der Hoeven + +No predecessor code is imported or executed. Vendored files are read as data, and the two `.py.txt` files only to bind stated constants. + +Prepared by lm1909 with Claude Code (Claude Opus 5.5) assistance. New code is Apache-2.0. Vendored files keep their original Apache-2.0 notices and authorship. diff --git a/research/native-lift-4635-delta-check/SOURCES.json b/research/native-lift-4635-delta-check/SOURCES.json new file mode 100644 index 0000000000..b46237335c --- /dev/null +++ b/research/native-lift-4635-delta-check/SOURCES.json @@ -0,0 +1,93 @@ +{ + "schema_version": 1, + "base_commit": "fbc9ea0249746acca4f504d4fda2b84e0e36cf0d", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "input", + "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395", + "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "research/compact-joint-compiler/arithmetic/RESULT.json", + "usage": "input", + "git_blob": "514d12ce4d2d824a4e0a418022bba610c8aed8ff", + "sha256": "a6caaa2a6d6460a8c1ef7e48c4853bb27976be33a52b96a4216dfa90d96c9091" + }, + { + "path": "research/joint-helper-lattice/CONTROLLER.json", + "usage": "input", + "git_blob": "49a2f0675819f9deeea27ed77be2c2b6ff2e87e5", + "sha256": "1f5d6aa267e4e66048818714b5d3b5eae17a58abe91d15deeaa34574f7391a5f" + }, + { + "path": "research/native-kappa-30201655/raw-profile.json", + "usage": "provenance", + "pin": "head:f4b974db1f651250a252721cf127d0491a802699:research/native-kappa-30201655/raw-profile.json", + "git_blob": "edf41a49a0350862c23378f837c7397fc5dc7596", + "sha256": "c7b2388f6511c19976b337d8c8ac374610af616866a249d75dace704eb5d9e21" + }, + { + "path": "research/native-kappa-30201655/native_ledger.py", + "usage": "provenance", + "pin": "head:f4b974db1f651250a252721cf127d0491a802699:research/native-kappa-30201655/native_ledger.py", + "git_blob": "e1faa0cf22d82d55ce76ee13acc3793fd9ee4b47", + "sha256": "cf3ededf5c980e272deb4647bdae76b1132aa1aa164c89af92eb58ac2597f3c2" + }, + { + "path": "research/native-kappa-30201655/critical_check.py", + "usage": "provenance", + "pin": "head:f4b974db1f651250a252721cf127d0491a802699:research/native-kappa-30201655/critical_check.py", + "git_blob": "fe6cb22e2f634eb06efafd565e97c451e4ea2f26", + "sha256": "41fa69948c5e20faa7245f441c7487e0a7f89ccaffc778849d80187ba012eb28" + }, + { + "path": "research/native-provider-lift/ARITHMETIC.json", + "usage": "provenance", + "pin": "head:898b0c8e2ca23897c312230988515c2553154f30:research/native-provider-lift/ARITHMETIC.json", + "git_blob": "c89e009ca4a5ad316c69f0371d885d72045ba415", + "sha256": "ab10f6a4a8a4f589d4b094aac663e002c43ec44774e6bd181c51915c7fa7e521" + }, + { + "path": "research/native-provider-lift/PARAMETERS.json", + "usage": "provenance", + "pin": "head:898b0c8e2ca23897c312230988515c2553154f30:research/native-provider-lift/PARAMETERS.json", + "git_blob": "0ec8027ed7cb6a2213e0513d177bb84ad8a1c246", + "sha256": "95bb0399057fd1c83687c8f51e47799cced99e0a112575bca486fb922a606a9e" + }, + { + "path": "research/native-provider-lift/critical_provider_check.py", + "usage": "provenance", + "pin": "head:898b0c8e2ca23897c312230988515c2553154f30:research/native-provider-lift/critical_provider_check.py", + "git_blob": "76f58548ffc7baf5a5db01b03b6647adae9aecc4", + "sha256": "593fbf957e9049bcdfcee198cf4f47f1b4eb4cc40f05f216f983a9c4d8486faa" + }, + { + "path": "research/native-provider-lift/NATIVE-LIFT.md", + "usage": "provenance", + "pin": "head:898b0c8e2ca23897c312230988515c2553154f30:research/native-provider-lift/NATIVE-LIFT.md", + "git_blob": "a900a66392f6486d439234a858c8127af56d138c", + "sha256": "66188d374905361062d30710b2cd0510defcf50d3786c1e54323847c3d9f9d08" + }, + { + "path": "research/native-provider-lift/CONTROLLER.json", + "usage": "provenance", + "pin": "head:898b0c8e2ca23897c312230988515c2553154f30:research/native-provider-lift/CONTROLLER.json", + "git_blob": "49a2f0675819f9deeea27ed77be2c2b6ff2e87e5", + "sha256": "1f5d6aa267e4e66048818714b5d3b5eae17a58abe91d15deeaa34574f7391a5f" + }, + { + "path": "research/kappa-round3-warp-20261022/ARITHMETIC.json", + "usage": "provenance", + "pin": "head:1eb8da6cfb35512c0cc2533413e5ca42f48e13c6:research/kappa-round3-warp-20261022/ARITHMETIC.json", + "git_blob": "c89e009ca4a5ad316c69f0371d885d72045ba415", + "sha256": "ab10f6a4a8a4f589d4b094aac663e002c43ec44774e6bd181c51915c7fa7e521" + } + ] +} diff --git a/research/native-lift-4635-delta-check/TASK.json b/research/native-lift-4635-delta-check/TASK.json new file mode 100644 index 0000000000..d4e81768fe --- /dev/null +++ b/research/native-lift-4635-delta-check/TASK.json @@ -0,0 +1,106 @@ +{ + "schema_version": 1, + "task_id": "independent-moment", + "priority_revision": 7, + "base_commit": "fbc9ea0249746acca4f504d4fda2b84e0e36cf0d", + "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": "For Dugongue's native Word RAM line, independently determine what changes between #4630 (kappa 0.0030201655, head f4b974db) and #4635 (kappa 0.0030217754, head 898b0c8e): bind the changed paid ledger to its #4610 source and the unchanged main controller, recompute both critical roots with a different enclosure method, recompute the finite-absorption margins, and recompute both nine-row native cost ledgers and their rejecting controls exactly.", + "scope_change_reason": "The card asks for independent coverage of a changed paid ledger; the changed ledger here is #4610's round-three local profile as consumed by the #4635 native lift, so the check is refined to that ledger plus the native transfer terms that could otherwise explain the +1.6099e-6 step.", + "bottleneck_link": "Separates a machine-model transfer contribution from a paid-profile contribution, so the #4635 headline is attributed to the right (still unselected) #4610 profile and not counted as an independent Word RAM advance.", + "budget_minutes": 60, + "stop_rule": "Stop after the #4630->#4635 delta is fully attributed and both nine-row ledgers and the five #4630 controls are recomputed; do not review the inherited all-fiber/analytic proofs.", + "outcome": "completed", + "evidence": "python3.12 -B research/native-lift-4635-delta-check/verify.py prints PASS_4635_DELTA_IS_PROFILE_ONLY: only the 18x local paid profile changes ({1:-36,2:+24,3:+16,4:-20,5:+4} per LOCAL call); raw savings 0.00302016597702 -> 0.00302177587078 (step 1.60989376e-6); kappa step 1.6099e-6 exceeds raw step by 6.24e-12, paid from #4630's larger transfer slack; nine-row ledgers reproduce exactly; four negative controls reject.", + "author": "lm1909", + "ai_assistance": "Prepared by lm1909 with Claude Code (Claude Opus 5.5) assistance.", + "open_questions": [ + { + "question": "Is #4610's round-three word (local paid profile {1:2201,2:412,3:510,4:127,5:40,8:8}) an admitted canonical provider under the all-fiber identity and absolute-phase contracts that #4635's NATIVE-LIFT.md requires?", + "why_it_matters": "The entire +1.6099e-6 of #4635 rests on this profile; the native lift adds no saving of its own.", + "first_step": "Independently replay #4610 head 1eb8da6c's changed 20 native maps and 26 helper interfaces on the 632 formal columns in both orientations, without importing its interpreters.", + "blocked_by": "#4610 is open and not maintainer-reviewed; #4614-#4616 covered an earlier head." + }, + { + "question": "Do the funded critical-majorant guards (U, V, Q, d, recurrence funding .048546 > .04282) hold for the changed profile under an independent enclosure?", + "why_it_matters": "This package recomputes the root, mirror ratio and capacity, but not the shifted-logarithmic majorant that turns the root into L(N) < N^(1-q_C).", + "first_step": "Re-implement the critical_guards inequalities of PR #4532/#4535 from their PROOF.md with Decimal intervals and evaluate them on the #4610 profile.", + "blocked_by": "None; needs a careful reading of the #4532 majorant statement." + } + ] +} diff --git a/research/native-lift-4635-delta-check/VERIFY.json b/research/native-lift-4635-delta-check/VERIFY.json new file mode 100644 index 0000000000..6f3194d39d --- /dev/null +++ b/research/native-lift-4635-delta-check/VERIFY.json @@ -0,0 +1,22 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "certificates/selected-result.json", + "research/compact-joint-compiler/arithmetic/RESULT.json", + "research/joint-helper-lattice/CONTROLLER.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Head-pinned vendored bytes and main inputs; #4630->#4635 changed paid ledger bound to #4610 and the unchanged main controller; Decimal critical roots for both profiles; finite absorption; both nine-row native ledgers and #4630 five controls; four negative controls (old profile vs new q_C, q_C above root, tampered vendored byte, wrong bracket)." + } + ] +} diff --git a/research/native-lift-4635-delta-check/vendor/pr4610/ARITHMETIC.json b/research/native-lift-4635-delta-check/vendor/pr4610/ARITHMETIC.json new file mode 100644 index 0000000000..c89e009ca4 --- /dev/null +++ b/research/native-lift-4635-delta-check/vendor/pr4610/ARITHMETIC.json @@ -0,0 +1,241 @@ +{ + "compiler": { + "H": 31385200000000, + "N": "2^31385200000000", + "eta": { + "lower": "0.000000204541256425394083726654", + "upper": "0.000000204541256425394083726655" + }, + "gap": "1/700000000", + "integer_test_exponent": 44836, + "logarithm_power": 1000, + "theta": "63/64", + "uniform_saving": "1057619/350000000", + "word_materialized": false + }, + "gain_over_PR4535": "319/200000000", + "kappa": "9443/3125000", + "local_helpers": { + "4": 28, + "7": 7, + "8": 47, + "9": 326 + }, + "local_paid": { + "1": 2201, + "2": 412, + "3": 510, + "4": 127, + "5": 40, + "8": 8 + }, + "margin_at_old_root_upper": [ + "78072058023577019965454984044224523228758899702419408235/196159429230833773869868419475239575503198607639501078528", + "1249152928377232319447279744707592371660142395238823308861/3138550867693340381917894711603833208051177722232017256448" + ], + "native_receipt_sha256": "eec3b14241430b6c9f5de3cbf0e3d45a172d8071d2dccd2b59d56a1fbac3d428", + "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" + ], + "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": { + "local_routes": 4802000, + "local_scalar": 158168, + "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": "296133039576953/98000000000000000", + "fused_gaussian": "296133038730859/98000000000000000", + "global_coordinate_router": "528809/175000000", + "group_bit_router": "370166473413573/122500000000000000", + "group_scans": "349999999/350000000", + "main_transform": "296132899576953/98000000000000000", + "microbox_face_corrections": "13475000001/175000000", + "polynomial_products": "699999999/700000000", + "sparse_union_movement": "40108633039576953/98000000000000000" + }, + "parameters": { + "a": "528809/175000000", + "b": "2115237/700000000", + "beta": "699999997/700000000", + "bit_saving": "17/5000", + "cap_xi": "89108632899576953/98000000000000000", + "complex_uniform_saving": "1057619/350000000", + "d": "1/700000000", + "epsilon": "699999999/700000000", + "kappa": "9443/3125000", + "lambda_": "199395647/200000000", + "lambda_prime": "139576953/140000000", + "layout": "1/700000000", + "q": "423047/140000000", + "r0": "1/7000000000", + "stop": "1/700000000", + "tested_saving": "302177/100000000" + }, + "strict_checks": { + "actual_bit_above_effective": "66191/175000000", + "actual_logarithmic_gamma_guard": "1/700000000", + "actual_logarithmic_group_guard": "8891367310423047/49000000000000000", + "alpha_logarithm_absorption": "1/7000000000", + "boundary_algebraic_matrix_above_kappa": "559576953/98000000000000000", + "cap_above_band": "40108632899576953/98000000000000000", + "cap_below_cell": "8891366960423047/98000000000000000", + "cap_below_phase_cell_power": "106891367100423047/98000000000000000", + "complex_above_effective": "1/700000000", + "complex_below_one_over_32": "19759763/700000000", + "complex_endpoint": "1/350000000", + "epsilon_below_one": "1/700000000", + "epsilon_positive": "699999999/700000000", + "fine_prime_halo_umbrella": "7/2", + "fused_gaussian_above_kappa": "558730859/98000000000000000", + "gaussian_above_main": "69576953/49000000000000000", + "global_coordinate_router_above_kappa": "1/175000000", + "global_gamma_power_slack": "9/7000000000", + "group_below_dimension": "1/350000000", + "group_bit_router_above_kappa": "873413573/122500000000000000", + "group_gauge_power_slack": "8891367303423047/49000000000000000", + "group_key_fits_record": "1/350000000", + "group_positive": "699999997/700000000", + "group_scans_above_kappa": "348942383/350000000", + "halo_covers_generic_inverse_radius": "5", + "improvement_over_user_baseline": "645394790400418148631/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": "1397884763/490000000000000000", + "leaf_saving_above_effective": "697884763/490000000000000000", + "main_transform_above_kappa": "419576953/98000000000000000", + "membership_arithmetic_fits_record": "1/700000000", + "microbox_face_corrections_above_kappa": "13474471193/175000000", + "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": "697884767/700000000", + "positive_layout_slack": "1/700000000", + "q_below_effective": "1/700000000", + "q_below_internal": "1/700000000", + "q_below_leaf": "1397884763/490000000000000000", + "q_positive": "423047/140000000", + "short_record_fallback": "697884763/700000000", + "source_axis_superpolynomial": "1/700000000", + "sparse_union_movement_above_kappa": "39812500559576953/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": 41298, + "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": 144 + }, + "paid_calls": 64404, + "productive_fields": 10928, + "rank_mass_surplus": 752, + "raw_root_interval": [ + "15108879/5000000000", + "30217759/10000000000" + ], + "scope": "Exact changed-profile arithmetic only. Requires separately admitted changed native programs, paid transports and absolute phases. Retained compiler/native/precision/tape/analytic/recovery assumptions.", + "source_sha256": { + "research/fresh-helper-boundary/native.py": "9b55a2d3c3972148fae9d112e745d9244968166bd89bd900c938f429fc76ab29", + "research/higher-moment-strictification/verify.py": "0ce7e7137422d5ffeda22085c81fa88471bbe963100fdad62e659f1e3bf89326", + "research/joint-helper-lattice/CONTROLLER.json": "1f5d6aa267e4e66048818714b5d3b5eae17a58abe91d15deeaa34574f7391a5f", + "research/joint-helper-lattice/native_joint.py": "50869b1bcad7493e6b4cb2a4cd5d2fd9a193a5921100483fa2c3f2c999ddfd46", + "research/joint-helper-lattice/verify.py": "8eb13f77a94315f811612cb557a17edeecb6b9d9a75dfa238b112dd6520c336f", + "research/kappa-0023-productive-jobs/dependencies/kappa-next-regime/bit-compression/carrier-reuse/reference/joint_pair_dag.py": "8a0de761642d21919e969475c3f13e5d01a4bae7343c1e1f37c586d94b676a85", + "research/kappa-interface-round2-20261022/price_profile.py": "adde619968d3ac37147d239e25145b28150650e9ce0f76035f680f22589adcbb", + "research/kappa-rebuild/architecture/mixed_target_probe.py": "011c3c9d0cf81103dc84d709a0e36793eb7c5ae3f23c85eac27650ef13afa04a", + "research/kappa-rebuild/bit/complex_controller_factor.py": "1de9aaf918e6a4f2f5448754c1f3c3da3b85e6257849ebd097af09859c4e5497", + "research/kappa-rebuild/bit/mixed_productive_bit.py": "b32291b0db7fc0d332ec444c70746ab0fb03351d2e50546f8bcb64060e3ff95e", + "research/pr4359-p7-padding/dependencies/compiler-refill/endpoint.py": "d097e55f06c3f244f2074ffd7c1a0a5f3c4b4b6a6accf9619d1dde5c0ae85e15", + "research/query-thinned-controllers/RESULT.json": "6ebfc8c0f09166f4834e9d7427410cb31aefff2cd4d4ce588c8e52c9c70e9a0f", + "research/query-thinned-controllers/controller.py": "8b462d660487b1be4940357c4c7522967b1bfaede3c02b1c66109b85acae0fd2" + }, + "status": "PASS_CHANGED_PROFILE_ARITHMETIC_NATIVE_ADMISSION_SEPARATE", + "strictification": { + "alpha": { + "lower": "0.999999993884252622740095906769", + "upper": "0.999999993884252622740095906770" + }, + "cutoff": 20, + "delta": { + "lower": "0.958285305508943939401236992035", + "upper": "0.958285305508943939401236992036" + }, + "floor": 21, + "gamma": { + "lower": "0.956217506703714253758457710273", + "upper": "0.956217506703714253758457710274" + }, + "normalized_paid_upper": "2097152001953127/2097154147483648", + "power": 1024, + "tail_offset": "1/5", + "tested": "302177/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": 5868 + } +} diff --git a/research/native-lift-4635-delta-check/vendor/pr4630/critical_check.py.txt b/research/native-lift-4635-delta-check/vendor/pr4630/critical_check.py.txt new file mode 100644 index 0000000000..fe6cb22e2f --- /dev/null +++ b/research/native-lift-4635-delta-check/vendor/pr4630/critical_check.py.txt @@ -0,0 +1,49 @@ +"""Exact p16 critical majorant and finite native-provider absorption replay. +Apache-2.0; Dugongue with substantial OpenAI Codex assistance. +Credits: Dillon's retained critical engine, zxv/Sussman/compiler lineage. +""" +from pathlib import Path +from fractions import Fraction as F +import json + +HERE=Path(__file__).resolve().parent + + +def need(ok,why): + if not ok:raise ValueError(why) + + +def check(): + path=HERE/'critical_engine.py';E={'__name__':'frozen_critical_engine','__file__':str(path)} + exec(compile(path.read_bytes(),str(path),'exec'),E) + profile=json.loads((HERE/'raw-profile.json').read_text()) + benchmarks=json.loads((HERE/'majorant-benchmarks.json').read_text()) + old=next(row['witness'] for row in benchmarks['cases'] if row['name']=='p16') + witness={key:old[key] for key in ('a','b','height_base','ell0','s','lambda','p','c')} + witness['guards']={key:old['guards'][key] for key in ('U','V','Q','d','beta')} + witness['upper_exponent']='.997067' + lo,hi=F('.9969798340229'),F('.9969798340230') + root=E['certify'](profile,lo,hi,F('.564'),F(1)) + majorant=E['critical_guards'](profile,lo,hi,witness) + need(witness['height_base']==1024 and witness['ell0']==650 and F(witness['c'])==133 and F(witness['p'])==F(2,5),'exact retained majorant parameters') + log=lambda n:tuple(F(x,E['GRID']) for x in E['logarithm'](n)) + need(log(2)[0]>F(2,3) and log(2)[1]<1,'log2 bracket') + need(log(145)[1]<8,'log145 bracket') + log_A_upper=F('.003021')*(8+6500) + need(log_A_upper<20 and 133+10**12<2**40,'normalization/logarithmic overhead below36') + uniform=F('.0030201656');gap=(1-hi)-uniform;H=10**12 + margin=gap*H*F(2,3)-36 + need(margin==F(646,3) and margin>0,'finite word absorption') + need(gap-F(2,5)/(133+F(2,3)*H)>0,'all-larger-rank absorption monotonicity') + rejected=False + try:E['certify'](profile,lo,hi,F(0),F(1)) + except ValueError:rejected=True + need(rejected,'unfunded mirror control') + return dict(status='PASS',critical_root=root,critical_majorant=majorant, + fixed_rank_encoding='2^1000000000000',fixed_rank_materialized=False, + native_provider_saving=str(uniform),finite_absorption_log_margin=str(margin), + unfunded_mirror_rejected=True, + scope='Exact source critical-majorant arithmetic and finite absorption; all-column algebraic word identity remains a cited mathematical proof, not this replay') + + +if __name__=='__main__':print(json.dumps(check(),indent=2)) diff --git a/research/native-lift-4635-delta-check/vendor/pr4630/native_ledger.py.txt b/research/native-lift-4635-delta-check/vendor/pr4630/native_ledger.py.txt new file mode 100644 index 0000000000..e1faa0cf22 --- /dev/null +++ b/research/native-lift-4635-delta-check/vendor/pr4630/native_ledger.py.txt @@ -0,0 +1,63 @@ +"""Exact native Word RAM assembly ledger; Apache-2.0. +Dugongue with substantial OpenAI Codex assistance. +Arithmetic checks support the separate source-bound proof; they do not prove its identities. +""" +from fractions import Fraction as F +import json + +PROVIDER=F('0.0030201656') +Q=F('0.00302016555') +STOP=F(1,10**9) +TARGET=F('0.0030201655') + +def check(epsilon=1-F(1,10**8), beta=1-F(3,10**8), target=TARGET, r=F(1,10**9)): + q=Q + xi=epsilon*(1+q)-F(3,32)+F(1,10**10) + savings={ + 'main_transform':epsilon*q, + 'complete_address_routing':F(1), + 'fused_gaussian':1-epsilon+q*beta, + 'selected_bit_gather_restore':F(1), + 'group_scans_and_lookup':1-epsilon+beta, + 'boundary_algebra_and_couplings':F(3,32)+xi-epsilon, + 'indexed_sparse_axis_visits':F(1,2)+xi-epsilon, + 'global_precision_record_products':epsilon, + 'core_face_recovery':1-(epsilon+beta+48-128+2)} + guards={ + 'positive_saving':target, + 'source_provider_stopped_margin':PROVIDER*(1-STOP)-q, + 'below_packed_output_limit':1-target, + 'epsilon_below_one':1-epsilon, + 'beta_positive':beta, + 'beta_below_epsilon':epsilon-beta, + 'cap_above_band':xi-F(1,2), + 'cap_below_dimension':epsilon-xi, + 'global_gamma_guard':1-epsilon-r, + 'shifted_group_chirp_guard':1-(beta+2*xi-2+r), + 'group_support_and_key_guard':1-(beta+1-epsilon), + 'membership_guard':1-(beta+2*(1-epsilon)), + 'positive_spare_alpha_exponent':r, + 'strassen_integer_certificate':F(2**45-7**16)} + guards.update({name+'_excess':value-target for name,value in savings.items()}) + if not all(v>0 for v in guards.values()): + raise ValueError('failed strict guards: '+','.join(k for k,v in guards.items() if v<=0)) + return {'kappa':str(target),'effective_provider_saving':str(q),'source_provider_saving':str(PROVIDER),'stop':str(STOP),'epsilon':str(epsilon),'beta':str(beta),'r':str(r),'xi':str(xi), + 'nine_native_savings':{k:str(v) for k,v in savings.items()}, + 'strict_guards':{k:str(v) for k,v in guards.items()}, + 'minimum_excess':str(min(v-target for v in savings.values()))} + +def main(): + result=check() + controls={} + for name,kwargs in [('epsilon_one',{'epsilon':F(1)}),('unfunded_outer_target',{'target':Q}), + ('key_fills_whole_word_power',{'beta':1-F(1,10**8)}), + ('membership_at_edge',{'beta':1-F(2,10**8)}), + ('normalization_at_edge',{'r':F(1,10**8)})]: + try:check(**kwargs) + except ValueError:controls[name]='REJECTED' + else:raise AssertionError('control accepted: '+name) + result.update(status='PASS',rejecting_controls=controls, + scope='Exact native exponent/guard arithmetic only; retained algebraic/analytic identities and full implementation are separate evidence.') + print(json.dumps(result,indent=2)) + +if __name__=='__main__':main() diff --git a/research/native-lift-4635-delta-check/vendor/pr4630/raw-profile.json b/research/native-lift-4635-delta-check/vendor/pr4630/raw-profile.json new file mode 100644 index 0000000000..edf41a49a0 --- /dev/null +++ b/research/native-lift-4635-delta-check/vendor/pr4630/raw-profile.json @@ -0,0 +1,274 @@ +{ + "compiler": { + "H": 64215200000000, + "N": "2^64215200000000", + "eta": { + "lower": "0.000000206231977820868640096499", + "upper": "0.000000206231977820868640096500" + }, + "gap": "1/1400000000", + "integer_test_exponent": 45868, + "logarithm_power": 1000, + "theta": "63/64", + "uniform_saving": "528527/175000000", + "word_materialized": false + }, + "fixed_profile_ceiling": { + "decreasing_through_C": "1/20", + "headroom": [ + "15977/1000000000000", + "159771/10000000000000" + ], + "negative_derivative_upper": { + "lower": "-195970.145588045890401261885812812963", + "upper": "-195970.145588045890401261885812812962" + }, + "remaining_interval_moment_upper": { + "lower": "-6847.019825166589746262304732988153", + "upper": "-6847.019825166589746262304732988152" + }, + "root": [ + "3020165977/1000000000000", + "30201659771/10000000000000" + ] + }, + "full_calls": 18, + "gain_over_PR4416": "4171/12500000", + "gain_over_PR4440": "1203/20000000", + "gain_over_PR4441": "191/10000000", + "gain_over_PR4447": "473/25000000", + "kappa": "60403/20000000", + "kappa_decimal": "0.00302015", + "local_helpers": { + "4": 28, + "7": 7, + "8": 47, + "9": 326 + }, + "local_paid": { + "1": 2237, + "2": 388, + "3": 494, + "4": 147, + "5": 36, + "8": 8 + }, + "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" + ], + "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": { + "local_route_bound": 4814000, + "local_scalar_allowance": 158168, + "raw_budget": 1000000000, + "raw_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": "348599999253/350000000000", + "fixed_halo_explicit_metadata_branch": "26950000001/350000000", + "new_BIT_row_stock_sublinear_in_active_group": "1395799997009/1400000000000", + "new_semantic_group_guard": "3/1400000000" + }, + "margins": { + "boundary_algebraic_matrix": "5919499595771787/1960000000000000000", + "fused_gaussian": "5919499587315361/1960000000000000000", + "global_coordinate_router": "2114107/700000000", + "group_bit_router": "2959750493657679/980000000000000000", + "group_scans": "699999999/700000000", + "main_transform": "5919498195771787/1960000000000000000", + "microbox_face_corrections": "26950000001/350000000", + "polynomial_products": "1399999999/1400000000", + "sparse_union_movement": "802169499595771787/1960000000000000000" + }, + "parameters": { + "a": "2114107/700000000", + "b": "845643/280000000", + "beta": "1399999997/1400000000", + "bit_saving": "17/5000", + "cap_xi": "1782169498195771787/1960000000000000000", + "complex_uniform_saving": "528527/175000000", + "d": "1/1400000000", + "epsilon": "1399999999/1400000000", + "kappa": "60403/20000000", + "lambda_": "398791939/400000000", + "lambda_prime": "1395771787/1400000000", + "layout": "1/1400000000", + "q": "4228213/1400000000", + "r0": "1/14000000000", + "stop": "1/1400000000", + "tested_saving": "604031/200000000" + }, + "strict_checks": { + "actual_bit_above_effective": "265893/700000000", + "actual_logarithmic_gamma_guard": "1/1400000000", + "actual_logarithmic_group_guard": "177830503904228213/980000000000000000", + "alpha_logarithm_absorption": "1/14000000000", + "boundary_algebraic_matrix_above_kappa": "5595771787/1960000000000000000", + "cap_above_band": "802169498195771787/1960000000000000000", + "cap_below_cell": "177830500404228213/1960000000000000000", + "cap_below_phase_cell_power": "2137830501804228213/1960000000000000000", + "complex_above_effective": "1/1400000000", + "complex_below_one_over_32": "7904357/280000000", + "complex_endpoint": "1/700000000", + "epsilon_below_one": "1/1400000000", + "epsilon_positive": "1399999999/1400000000", + "fine_prime_halo_umbrella": "7/2", + "fused_gaussian_above_kappa": "5587315361/1960000000000000000", + "gaussian_above_main": "695771787/980000000000000000", + "global_coordinate_router_above_kappa": "1/350000000", + "global_gamma_power_slack": "9/14000000000", + "group_below_dimension": "1/700000000", + "group_bit_router_above_kappa": "3493657679/980000000000000000", + "group_gauge_power_slack": "177830503834228213/980000000000000000", + "group_key_fits_record": "1/700000000", + "group_positive": "1399999997/1400000000", + "group_scans_above_kappa": "348942947/350000000", + "halo_covers_generic_inverse_radius": "5", + "improvement_over_user_baseline": "644589790400418148631/500000000000000000000000", + "lambda_above_internal": "1/2800000000", + "lambda_above_sigma": "3/2800000000", + "lambda_above_tau": "1/2800000000", + "lambda_prime_above_lambda": "1/2800000000", + "lambda_prime_above_leaf": "559154357/392000000000000000", + "leaf_saving_above_effective": "279154357/392000000000000000", + "main_transform_above_kappa": "4195771787/1960000000000000000", + "membership_arithmetic_fits_record": "1/1400000000", + "microbox_face_corrections_above_kappa": "53897885897/700000000", + "microbox_halo_volume": "110600000003/1400000000", + "new_complex_uniform_saving_above_b": "1/1400000000", + "new_semantic_guard_with_C1_one": "1/1400000000", + "polynomial_products_above_kappa": "1395771789/1400000000", + "positive_layout_slack": "1/1400000000", + "q_below_effective": "1/1400000000", + "q_below_internal": "1/1400000000", + "q_below_leaf": "559154357/392000000000000000", + "q_positive": "4228213/1400000000", + "short_record_fallback": "279154357/280000000", + "source_axis_superpolynomial": "1/1400000000", + "sparse_union_movement_above_kappa": "796250005595771787/1960000000000000000", + "stop_below_one": "1399999999/1400000000", + "stop_positive": "1/1400000000", + "strassen_integer_power_gap": "1951441519231", + "support_router_span": "3/1400000000", + "theta_positive_polynomial_power": "2", + "union_header_fits_record": "3/1400000000", + "union_tag_work_per_visit_fits_record": "3/1400000000" + } + }, + "paid": { + "1": 41946, + "16": 448, + "2": 6984, + "24": 448, + "3": 8892, + "32": 448, + "4": 2646, + "40": 448, + "48": 448, + "5": 648, + "56": 448, + "64": 448, + "72": 224, + "8": 144 + }, + "paid_calls": 64620, + "pairs": 16, + "prefix_pairs": 7, + "productive_fields": 10928, + "query_shears": 15, + "scope": "Author-checked conditional construction; retained native/all-column, owned-erasure, whole-job, analytic, precision, tape, prime and recovery contracts. No selected promotion or formal/human acceptance.", + "source_heads": { + "PR4440": "40e22a83ed660d3d6074c4f2dbf14bfb621eee51", + "PR4441_combination": "5f9d871c6bd1b9e34db5a7ea5ef08a908e94db39", + "PR4447": "322e0ec764aa7ef7801383feb1f656e460dd8bed", + "helper_retiming": "ccdae89b2ab9ced24ee3e7adfdb670ef80d223d9" + }, + "source_inputs": 51, + "status": "PASS_CONDITIONAL_JOINT_HELPER_KAPPA_00302015", + "strictification": { + "alpha": { + "lower": "0.999999988558808354139963023136", + "upper": "0.999999988558808354139963023137" + }, + "cutoff": 20, + "delta": { + "lower": "0.958284435309221389866479909583", + "upper": "0.958284435309221389866479909584" + }, + "floor": 21, + "gamma": { + "lower": "0.956176646497545264598139374323", + "upper": "0.956176646497545264598139374324" + }, + "limits": [ + "999999999/1000000000", + "97/100", + "97/100" + ], + "normalized_paid_upper": "2097152001953127/2097154147483648", + "power": 1024, + "tail_offset": "1/5", + "tested": "604031/200000000" + }, + "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": 5868 + }, + "uniform_local_gain": { + "coefficients": { + "1": 17, + "2": 126, + "3": -50, + "4": -42, + "5": 2, + "7": -22, + "8": 5, + "9": 17 + }, + "derivative_upper": { + "lower": "-16.327581880492435373215953558618", + "upper": "-16.327581880492435373215953558617" + }, + "intervals": 128, + "vanishes_at_one": true + } +} diff --git a/research/native-lift-4635-delta-check/vendor/pr4635/ARITHMETIC.json b/research/native-lift-4635-delta-check/vendor/pr4635/ARITHMETIC.json new file mode 100644 index 0000000000..c89e009ca4 --- /dev/null +++ b/research/native-lift-4635-delta-check/vendor/pr4635/ARITHMETIC.json @@ -0,0 +1,241 @@ +{ + "compiler": { + "H": 31385200000000, + "N": "2^31385200000000", + "eta": { + "lower": "0.000000204541256425394083726654", + "upper": "0.000000204541256425394083726655" + }, + "gap": "1/700000000", + "integer_test_exponent": 44836, + "logarithm_power": 1000, + "theta": "63/64", + "uniform_saving": "1057619/350000000", + "word_materialized": false + }, + "gain_over_PR4535": "319/200000000", + "kappa": "9443/3125000", + "local_helpers": { + "4": 28, + "7": 7, + "8": 47, + "9": 326 + }, + "local_paid": { + "1": 2201, + "2": 412, + "3": 510, + "4": 127, + "5": 40, + "8": 8 + }, + "margin_at_old_root_upper": [ + "78072058023577019965454984044224523228758899702419408235/196159429230833773869868419475239575503198607639501078528", + "1249152928377232319447279744707592371660142395238823308861/3138550867693340381917894711603833208051177722232017256448" + ], + "native_receipt_sha256": "eec3b14241430b6c9f5de3cbf0e3d45a172d8071d2dccd2b59d56a1fbac3d428", + "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" + ], + "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": { + "local_routes": 4802000, + "local_scalar": 158168, + "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": "296133039576953/98000000000000000", + "fused_gaussian": "296133038730859/98000000000000000", + "global_coordinate_router": "528809/175000000", + "group_bit_router": "370166473413573/122500000000000000", + "group_scans": "349999999/350000000", + "main_transform": "296132899576953/98000000000000000", + "microbox_face_corrections": "13475000001/175000000", + "polynomial_products": "699999999/700000000", + "sparse_union_movement": "40108633039576953/98000000000000000" + }, + "parameters": { + "a": "528809/175000000", + "b": "2115237/700000000", + "beta": "699999997/700000000", + "bit_saving": "17/5000", + "cap_xi": "89108632899576953/98000000000000000", + "complex_uniform_saving": "1057619/350000000", + "d": "1/700000000", + "epsilon": "699999999/700000000", + "kappa": "9443/3125000", + "lambda_": "199395647/200000000", + "lambda_prime": "139576953/140000000", + "layout": "1/700000000", + "q": "423047/140000000", + "r0": "1/7000000000", + "stop": "1/700000000", + "tested_saving": "302177/100000000" + }, + "strict_checks": { + "actual_bit_above_effective": "66191/175000000", + "actual_logarithmic_gamma_guard": "1/700000000", + "actual_logarithmic_group_guard": "8891367310423047/49000000000000000", + "alpha_logarithm_absorption": "1/7000000000", + "boundary_algebraic_matrix_above_kappa": "559576953/98000000000000000", + "cap_above_band": "40108632899576953/98000000000000000", + "cap_below_cell": "8891366960423047/98000000000000000", + "cap_below_phase_cell_power": "106891367100423047/98000000000000000", + "complex_above_effective": "1/700000000", + "complex_below_one_over_32": "19759763/700000000", + "complex_endpoint": "1/350000000", + "epsilon_below_one": "1/700000000", + "epsilon_positive": "699999999/700000000", + "fine_prime_halo_umbrella": "7/2", + "fused_gaussian_above_kappa": "558730859/98000000000000000", + "gaussian_above_main": "69576953/49000000000000000", + "global_coordinate_router_above_kappa": "1/175000000", + "global_gamma_power_slack": "9/7000000000", + "group_below_dimension": "1/350000000", + "group_bit_router_above_kappa": "873413573/122500000000000000", + "group_gauge_power_slack": "8891367303423047/49000000000000000", + "group_key_fits_record": "1/350000000", + "group_positive": "699999997/700000000", + "group_scans_above_kappa": "348942383/350000000", + "halo_covers_generic_inverse_radius": "5", + "improvement_over_user_baseline": "645394790400418148631/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": "1397884763/490000000000000000", + "leaf_saving_above_effective": "697884763/490000000000000000", + "main_transform_above_kappa": "419576953/98000000000000000", + "membership_arithmetic_fits_record": "1/700000000", + "microbox_face_corrections_above_kappa": "13474471193/175000000", + "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": "697884767/700000000", + "positive_layout_slack": "1/700000000", + "q_below_effective": "1/700000000", + "q_below_internal": "1/700000000", + "q_below_leaf": "1397884763/490000000000000000", + "q_positive": "423047/140000000", + "short_record_fallback": "697884763/700000000", + "source_axis_superpolynomial": "1/700000000", + "sparse_union_movement_above_kappa": "39812500559576953/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": 41298, + "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": 144 + }, + "paid_calls": 64404, + "productive_fields": 10928, + "rank_mass_surplus": 752, + "raw_root_interval": [ + "15108879/5000000000", + "30217759/10000000000" + ], + "scope": "Exact changed-profile arithmetic only. Requires separately admitted changed native programs, paid transports and absolute phases. Retained compiler/native/precision/tape/analytic/recovery assumptions.", + "source_sha256": { + "research/fresh-helper-boundary/native.py": "9b55a2d3c3972148fae9d112e745d9244968166bd89bd900c938f429fc76ab29", + "research/higher-moment-strictification/verify.py": "0ce7e7137422d5ffeda22085c81fa88471bbe963100fdad62e659f1e3bf89326", + "research/joint-helper-lattice/CONTROLLER.json": "1f5d6aa267e4e66048818714b5d3b5eae17a58abe91d15deeaa34574f7391a5f", + "research/joint-helper-lattice/native_joint.py": "50869b1bcad7493e6b4cb2a4cd5d2fd9a193a5921100483fa2c3f2c999ddfd46", + "research/joint-helper-lattice/verify.py": "8eb13f77a94315f811612cb557a17edeecb6b9d9a75dfa238b112dd6520c336f", + "research/kappa-0023-productive-jobs/dependencies/kappa-next-regime/bit-compression/carrier-reuse/reference/joint_pair_dag.py": "8a0de761642d21919e969475c3f13e5d01a4bae7343c1e1f37c586d94b676a85", + "research/kappa-interface-round2-20261022/price_profile.py": "adde619968d3ac37147d239e25145b28150650e9ce0f76035f680f22589adcbb", + "research/kappa-rebuild/architecture/mixed_target_probe.py": "011c3c9d0cf81103dc84d709a0e36793eb7c5ae3f23c85eac27650ef13afa04a", + "research/kappa-rebuild/bit/complex_controller_factor.py": "1de9aaf918e6a4f2f5448754c1f3c3da3b85e6257849ebd097af09859c4e5497", + "research/kappa-rebuild/bit/mixed_productive_bit.py": "b32291b0db7fc0d332ec444c70746ab0fb03351d2e50546f8bcb64060e3ff95e", + "research/pr4359-p7-padding/dependencies/compiler-refill/endpoint.py": "d097e55f06c3f244f2074ffd7c1a0a5f3c4b4b6a6accf9619d1dde5c0ae85e15", + "research/query-thinned-controllers/RESULT.json": "6ebfc8c0f09166f4834e9d7427410cb31aefff2cd4d4ce588c8e52c9c70e9a0f", + "research/query-thinned-controllers/controller.py": "8b462d660487b1be4940357c4c7522967b1bfaede3c02b1c66109b85acae0fd2" + }, + "status": "PASS_CHANGED_PROFILE_ARITHMETIC_NATIVE_ADMISSION_SEPARATE", + "strictification": { + "alpha": { + "lower": "0.999999993884252622740095906769", + "upper": "0.999999993884252622740095906770" + }, + "cutoff": 20, + "delta": { + "lower": "0.958285305508943939401236992035", + "upper": "0.958285305508943939401236992036" + }, + "floor": 21, + "gamma": { + "lower": "0.956217506703714253758457710273", + "upper": "0.956217506703714253758457710274" + }, + "normalized_paid_upper": "2097152001953127/2097154147483648", + "power": 1024, + "tail_offset": "1/5", + "tested": "302177/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": 5868 + } +} diff --git a/research/native-lift-4635-delta-check/vendor/pr4635/NATIVE-LIFT.md b/research/native-lift-4635-delta-check/vendor/pr4635/NATIVE-LIFT.md new file mode 100644 index 0000000000..a900a66392 --- /dev/null +++ b/research/native-lift-4635-delta-check/vendor/pr4635/NATIVE-LIFT.md @@ -0,0 +1,104 @@ +# A supplier-to-native-multiplication theorem below 3/32 + +Prepared for Dugongue with substantial OpenAI Codex assistance. Apache-2.0. + +## Scope and precise sufficient conclusion + +Retain the actual algebraic and analytic source results, scalar instructions and paid native algorithms of PR #4630, pinned at head f4b974db1f651250a252721cf127d0491a802699. These are the explicit all-column chronological finite-word identities, finite compiler, fine-padding Gaussian/Poisson reduction, capped gauge-free Toeplitz tensor circuits, batched boundary factors and integer recovery theorem enumerated in its NATIVE-ASSEMBLY.md. They are mathematical dependencies, not permission to replace a missing identity by an oracle. + +Assume a fixed, algorithmically specified uniform provider word with productive width W, complete paid leaf count P and rank N satisfies + + P/W < N^(1-q_C), 0 < q_C < 1. + +A purported larger q_C may first be weakened to 1/2. Its exact endpoint must be the required canonical selected-axis Gaussian operator on every independent productive field, with literal phase charts, restored owned storage, actual all-column/fiber lift, and the coefficient/prefix bounds required by the native finite-word lowering. The moment inequality alone is insufficient. Fixed N and all its instructions may be enormous; they must be effective finite constructions independent of the growing input. + +Then, for every real target + + 0 < kappa < min(q_C, 3/32), + +these retained constructions multiply packed n-bit integers on a standard Word RAM in + + O(n/(log n)^kappa) + +operations, with word width C log n for a sufficiently large fixed C. No Turing-machine algorithm, BIT transform supplier, or tape-to-RAM simulation is a premise. For real endpoints, choose rational interior q and kappa first; the explicit rational formulas below suffice for every rational target and therefore for every strictly smaller real target. This is a source-bound sufficient theorem, not an unconditional record claim or a new paid supplier profile. + +## Explicit universal parameter choice + +Put c=3/32 and Q=min(q_C,c). For rational 0 0. + +Here stop is the harmless strict loss used by the provider recurrence/base policy; it is not a license to omit paid exits or owned work. The finite provider lowering is unchanged. Only the dimension, grouping and cap parameters in the actual native caller vary. + +## All interface guards, with universal proofs + +We have 0=97/100>0, beta0. The global gamma guard is + + 1-epsilon-r = 9delta/10 > 0. + +The full-coordinate group key has size + + K=O(p^(beta+1-epsilon)+p^beta log p), + +where beta+1-epsilon=1-2delta<1. Hence K=o(p), and explicitly enumerating the actual coefficient/address/classification functions on every K-bit key costs n^o(1). It is important that the key includes coarse coordinates, not only a local membership header. The separate retained membership guard is + + 1-beta-2(1-epsilon)=delta>0. + +Since epsilon>=99/100, + + xi > 99/100 - 3/32 > 1/2. + +The cap lies below the axis exponent because + + epsilon-xi = c-epsilon*q-layout + >= c-q-delta/100 > 0; + +indeed delta<=(c-q)/16. The actual chirp/conditioning guard simplifies exactly to + + 1-(beta+2xi-2+r) + = 2(c-q) + delta(122/25+2q) > 0. + +Thus the group guard bits remain o(p). This explicitly preserves the two potentially restrictive analytic inequalities while allowing q up to c. Fixed polynomial setup remains polynomial(s_i,p)=n^o(1), and all online coefficients remain O(p) bits under the retained conditioning bounds. + +## Every paid native row + +The actual algorithms and complete accounting are those in PR #4630. Here p=Theta(log n), d=Theta(p^epsilon), g=Theta(p^beta), cap B=Theta(p^xi), boundary width W_band=O(sqrt(p) polylog p), and T p=Theta(n). Every row is O(T p^(1-saving) polylog p): + +| Actual native operation | Saving | Strict comparison with kappa | +|---|---:|---| +| Main simultaneous transform | epsilon*q | q-delta*q > kappa | +| Standalone complete-address routing | 1 | 1>kappa | +| Fused Gaussian circuits | 1-epsilon+q*beta | q+delta(1-3q)>q>kappa | +| Additional standalone addressing passes | 1 | 1>kappa | +| Extra group scans and lookups | 1-epsilon+beta=1-2delta | >=98/100>kappa | +| Boundary algebra, both couplings and periodic closure | c+xi-epsilon=epsilon*q+layout | >epsilon*q>kappa | +| Indexed sparse-axis visits | 1/2+xi-epsilon=13/32+epsilon*q+layout | >13/32>kappa | +| Global-precision polynomial record products | epsilon | >=99/100>kappa | +| Core-face recovery | 79-epsilon-beta | >77>kappa | + +For the first row, delta <= (q-kappa)/(4(q+1)) implies delta*q < (q-kappa)/4. Its saving exceeds kappa by more than 3(q-kappa)/4. This proves all nine strict comparisons without numerical optimization. + +The boundary exponent uses Strassen's explicit seven-product recursion and the exact integer certificate 7^16<2^45, giving c=3/32 conservatively. It includes factorization setup, batched solves, both coupling directions and periodic closure. The fused Gaussian row uses the actual shallow tensor circuits; unfused O(Td) Gaussian evaluation does not satisfy this theorem. The record-product row uses global O(p)-bit words on r coefficients; switching to a fresh O(log(rp))-bit local machine would invalidate its tariff. Per-call gathers and restoration are charged in their calls, and extra group scans have their own row. No recurring pass is silently assigned a one-time cost. + +Every polylog(p) factor is absorbed by the fixed positive margins just proved. Native preparation is n^o(1), below the claimed work bound. The retained recovery theorem then gives exact packed integer multiplication. This completes the sufficient assembly argument. + +## Meaning of the 3/32 endpoint + +This theorem establishes the open range below min(q_C,3/32). It does not establish equality at either endpoint. The number 3/32 comes from this caller's cap inequality xiF(2,3) and log(145)[1]<8,'exact logarithms') + # log A < (1-theta)*(log145+650 log1024) < .003022*(8+6500)<20. + # (2/5)*log(133+log N)<(2/5)*40 log2 <16. + need(F('.003022')*(8+6500)<20 and 133+H<2**40,'overhead below36') + margin=gap*H*F(2,3)-36 + need(gap==F(3,10**10) and margin==164,'finite critical-root absorption') + need(gap-F(2,5)/(133+F(2,3)*H)>0,'monotone continuation above cutoff') + controls={} + for name,kwargs in [('unfunded_mirror',dict(beta=F(0))),('wrong_root',dict(lo=F('.9969798340229'),hi=F('.9969798340230')))]: + k=dict(lo=lo,hi=hi,beta=F('.564'),derivative_floor=F(1));k.update(kwargs) + try:E['certify'](profile,**k) + except ValueError:controls[name]=True + else:raise ValueError('negative control accepted: '+name) + return dict(status='PASS_SOURCE_BOUND_CRITICAL_PROVIDER',source_pr=4610,source_head='1eb8da6cfb35512c0cc2533413e5ca42f48e13c6', + critical_root=root,critical_majorant=majorant,uniform_saving=str(qC),fixed_rank_encoding='2^1000000000000', + fixed_rank_materialized=False,finite_absorption_log_margin=str(margin),negative_controls=controls, + scope='Exact profile arithmetic and funded critical majorant; actual all-fiber algebraic supplier and whole-job normalizers are explicitly inherited proofs, not finite tests.') +if __name__=='__main__': print(json.dumps(check(),indent=2)) diff --git a/research/native-lift-4635-delta-check/verify.py b/research/native-lift-4635-delta-check/verify.py new file mode 100644 index 0000000000..b9f5aca6b2 --- /dev/null +++ b/research/native-lift-4635-delta-check/verify.py @@ -0,0 +1,402 @@ +#!/usr/bin/env python3 +"""Independent check of the #4630 -> #4635 native Word RAM kappa step. + +Question: what exactly changes between Dugongue's #4630 (kappa 0.0030201655) +and #4635 (kappa 0.0030217754), and does the +0.0000016099 step come from the +paid profile / critical root or from the native transfer/absorption terms? + +Stdlib only. No predecessor code is imported or executed; vendored PR-head files +are read as data (and two .py files as text, to bind the constants they state). +lm1909 with Claude Code (Claude Opus 5.5) assistance. Apache-2.0. +""" +from collections import Counter +from decimal import Decimal as D, getcontext +from fractions import Fraction as F +from hashlib import sha256 +from pathlib import Path +import json +import sys + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +getcontext().prec = 60 + +H4630 = 'f4b974db1f651250a252721cf127d0491a802699' +H4635 = '898b0c8e2ca23897c312230988515c2553154f30' +H4610 = '1eb8da6cfb35512c0cc2533413e5ca42f48e13c6' +VENDOR = { # vendored copy -> (pinned head, original path) + 'vendor/pr4630/raw-profile.json': (H4630, 'research/native-kappa-30201655/raw-profile.json'), + 'vendor/pr4630/native_ledger.py.txt': (H4630, 'research/native-kappa-30201655/native_ledger.py'), + 'vendor/pr4630/critical_check.py.txt': (H4630, 'research/native-kappa-30201655/critical_check.py'), + 'vendor/pr4635/ARITHMETIC.json': (H4635, 'research/native-provider-lift/ARITHMETIC.json'), + 'vendor/pr4635/PARAMETERS.json': (H4635, 'research/native-provider-lift/PARAMETERS.json'), + 'vendor/pr4635/critical_provider_check.py.txt': (H4635, 'research/native-provider-lift/critical_provider_check.py'), + 'vendor/pr4635/NATIVE-LIFT.md': (H4635, 'research/native-provider-lift/NATIVE-LIFT.md'), + 'vendor/pr4610/ARITHMETIC.json': (H4610, 'research/kappa-round3-warp-20261022/ARITHMETIC.json'), +} +MAIN = { + 'cjc': 'research/compact-joint-compiler/arithmetic/RESULT.json', + 'controller': 'research/joint-helper-lattice/CONTROLLER.json', + 'selected': 'certificates/selected-result.json', +} + + +def need(ok, why): + if not ok: + raise ValueError(why) + + +# ---------------------------------------------------------------- binding +def load_sources(sources=None, vendor_bytes=None): + sources = sources if sources is not None else json.loads((HERE/'SOURCES.json').read_text()) + rows = {(r.get('pin') or 'base:'+r['path']): r for r in sources['files']} + blobs = {} + for rel, (head, path) in VENDOR.items(): + row = rows.get('head:%s:%s' % (head, path)) + need(row is not None and row['usage'] == 'provenance', 'missing head pin for '+path) + raw = vendor_bytes[rel] if vendor_bytes and rel in vendor_bytes else (HERE/rel).read_bytes() + need(sha256(raw).hexdigest() == row['sha256'], 'vendored bytes differ from pin: '+rel) + blobs[rel] = raw + for key, path in MAIN.items(): + row = rows['base:'+path] + raw = (ROOT/path).read_bytes() + need(row['usage'] == 'input' and sha256(raw).hexdigest() == row['sha256'], 'main input drift: '+path) + blobs[key] = raw + ctl4635 = rows['head:%s:research/native-provider-lift/CONTROLLER.json' % H4635] + return blobs, ctl4635['sha256'] + + +def hist(d): + return {int(k): v for k, v in d.items()} + + +# ---------------------------------------------------------------- part A +def delta_ledger(blobs, ctl4635_sha): + p30 = json.loads(blobs['vendor/pr4630/raw-profile.json']) + p35 = json.loads(blobs['vendor/pr4635/ARITHMETIC.json']) + main = json.loads(blobs['cjc']) + need(blobs['vendor/pr4635/ARITHMETIC.json'] == blobs['vendor/pr4610/ARITHMETIC.json'], + '#4635 ARITHMETIC.json is not byte-identical to #4610 round-three ARITHMETIC.json') + need(ctl4635_sha == sha256(blobs['controller']).hexdigest(), '#4635 controller differs from main') + ctl = json.loads(blobs['controller']) + kinds = Counter(e[0] for e in ctl['physical_events']) + need(kinds['LOCAL'] == 18, 'expected 18 LOCAL calls in the unchanged controller') + for key in ('targets', 'paid', 'local_paid', 'local_helpers'): + need(hist(p30[key]) == hist(main[key]), '#4630 profile is not main p16: '+key) + need(hist(p30['targets']) == hist(p35['targets']), 'targets changed') + need(hist(p30['local_helpers']) == hist(p35['local_helpers']), 'helper census changed') + old, new = Counter(hist(p30['local_paid'])), Counter(hist(p35['local_paid'])) + dloc = {r: new[r]-old[r] for r in sorted(set(old) | set(new)) if new[r] != old[r]} + need(dloc == {1: -36, 2: 24, 3: 16, 4: -20, 5: 4}, 'unexpected local paid delta %r' % dloc) + need(sum(r*c for r, c in old.items()) == sum(r*c for r, c in new.items()) == 5327, 'local rank mass') + P0, P1 = hist(p30['paid']), hist(p35['paid']) + gdelta = {r: P1.get(r, 0)-P0.get(r, 0) for r in set(P0) | set(P1) if P1.get(r, 0) != P0.get(r, 0)} + need(gdelta == {r: kinds['LOCAL']*c for r, c in dloc.items()}, 'global paid delta != 18 x local delta') + T = hist(p30['targets']) + need(sum(P1.values()) == 64404 and sum(T.values()) == 10928, '#4635 inventory counts') + need(sum(P0.values()) == 64404 + 12*18, '#4630 paid count') + need(sum(k*c for k, c in T.items()) - sum(r*c for r, c in P1.items()) == 752 == + sum(k*c for k, c in T.items()) - sum(r*c for r, c in P0.items()), 'rank-mass surplus 752 both') + return dict(T=T, P0=P0, P1=P1, dloc=dloc, gdelta=gdelta, p35=p35, p30=p30) + + +# ---------------------------------------------------------------- part B +LN = {} + + +def ln(k): + if k not in LN: + LN[k] = D(k).ln() + return LN[k] + + +def moment(h, t): + return sum(c*(ln(k)*t).exp() for k, c in h.items()) + + +def f(T, P, t): + return moment(T, t) - moment(P, t) + + +TOL = D('1e-35') # far above accumulated rounding of ~1e5 correctly rounded terms at 60 digits + + +def root(T, P, lo=D('0.99'), hi=D(1)): + need(f(T, P, lo) < -TOL and f(T, P, hi) > TOL, 'no bracketed crossing') + for _ in range(140): + mid = (lo+hi)/2 + if f(T, P, mid) < 0: + lo = mid + else: + hi = mid + return lo, hi + + +def sign_at(T, P, t): + v = f(T, P, D(t)) + need(abs(v) > TOL, 'sign not resolved at %s' % t) + return v > 0 + + +def mirror_max(T, P, t): + pts = sorted({F(0), *(F(1, k) for k in T), *(F(1, r) for r in P)}) + worst = D(0) + for a, b in zip(pts, pts[1:]): + x = (a+b)/2 + src, ext = Counter(), Counter() + for k, w in T.items(): + for r, c in P.items(): + if k > r and F(1, k) < x <= F(1, r): + src[k*r] += w*c + if r > k and F(1, r) < x <= F(1, k): + ext[k*r] += w*c + if ext: + worst = max(worst, moment(ext, t)/moment(src, t)) + return worst + + +def roots(A): + T, P0, P1 = A['T'], A['P0'], A['P1'] + out = {} + for name, P, (blo, bhi) in (('4630', P0, ('.9969798340229', '.9969798340230')), + ('4635', P1, ('.9969782241', '.9969782242'))): + lo, hi = root(T, P) + need(not sign_at(T, P, blo) and sign_at(T, P, bhi), name+' stated root bracket rejected') + # single crossing on a coarse grid of (0,1]: f<0 then f>0 exactly once + signs = [sign_at(T, P, D(j)/100) for j in range(1, 101)] + need(sum(1 for u, v in zip(signs, signs[1:]) if u != v) == 1, name+' grid sign changes') + out[name] = dict(theta=lo, saving=1-hi, saving_hi=1-lo) + return out + + +# ---------------------------------------------------------------- part C: finite absorption +LN2_LO, LN2_HI = F('0.6931471805'), F('0.6931471806') + + +def ln_upper(x): + return F(D(x.numerator).ln() - D(x.denominator).ln() + D('1e-40')) + + +def absorption_margin(theta_lo, qC, H=10**12): + """Lower bound on (1-theta-q_C)log N - log A - (2/5)log(133+log N) with + N=2^H, n0=145*1024^650, A=n0^(1-theta)/(133+log n0)^(2/5) <= n0^(1-theta), + and theta < theta_hi(=1-saving_lo). Uses the true root, not the rounded bracket.""" + one_minus_theta_hi = 1-F(theta_lo) # upper bound for (1-theta) + log_n0_hi = ln_upper(F(145)) + 6500*LN2_HI + logA_hi = one_minus_theta_hi*log_n0_hi + over_hi = F(2, 5)*ln_upper(133 + H*LN2_HI) + return (1-F(theta_lo)-qC), logA_hi, over_hi + + +def absorption(R): + res = {} + for name, qC, kappa in (('4630', F('0.0030201656'), F('0.0030201655')), + ('4635', F('0.0030217755'), F('0.0030217754'))): + r = R[name] + th_hi = F(r['theta']) + F(1, 10**40) + gap = 1 - th_hi - qC + _, logA, over = absorption_margin(r['theta'], qC) + margin = gap*10**12*LN2_LO - logA - over + need(margin > 0, name+' finite absorption fails') + need(F(r['saving']) > qC > kappa, name+' order raw saving > q_C > kappa') + qmax = F(r['saving']) - (logA+over)/(10**12*LN2_LO) + res[name] = dict(margin=margin, qC_max_at_this_N=qmax) + return res + + +# ---------------------------------------------------------------- part D: native ledgers +C32 = F(3, 32) + + +def ledger(kappa, q, eps, beta, r, xi, provider, stop, strassen=2**45-7**16): + sav = { + 'main': eps*q, 'standalone_routing': F(1), 'fused_gaussian': 1-eps+q*beta, + 'standalone_addressing': F(1), 'group_scans': 1-eps+beta, 'boundary': C32+xi-eps, + 'sparse_visits': F(1, 2)+xi-eps, 'record_products': eps, 'core_face_recovery': 79-eps-beta} + guards = { + 'positive_kappa': kappa, 'stopped_provider': provider*(1-stop)-q, 'stop_positive': stop, + 'stop_below_one': 1-stop, 'epsilon_below_one': 1-eps, 'beta_positive': beta, + 'beta_below_epsilon': eps-beta, 'cap_above_band': xi-F(1, 2), 'cap_below_dimension': eps-xi, + 'global_gamma': 1-eps-r, 'group_chirp': 1-(beta+2*xi-2+r), 'group_key': 1-(beta+1-eps), + 'membership': 1-beta-2*(1-eps), 'spare_positive': r, 'strassen_integer_certificate': F(strassen)} + excess = {k: v-kappa for k, v in sav.items()} + failed = sorted([k for k, v in guards.items() if v <= 0] + [k+'_excess' for k, v in excess.items() if v <= 0]) + return sav, guards, excess, failed + + +def lift_params(kappa, qC): + """NATIVE-LIFT.md 'Explicit universal parameter choice', re-implemented.""" + Q = min(qC, C32) + need(0 < kappa < Q, 'kappa outside (0, min(q_C,3/32))') + q = (kappa+Q)/2 + stop = (qC-q)/(2*qC) + delta = min(F(1, 100), (q-kappa)/(4*(q+1)), (C32-q)/16) + eps, beta = 1-delta, 1-3*delta + r, layout = delta/10, delta/100 + xi = eps*(1+q)-C32+layout + return dict(q=q, stop=stop, delta=delta, eps=eps, beta=beta, r=r, layout=layout, xi=xi) + + +def check_4635(blobs): + P = json.loads(blobs['vendor/pr4635/PARAMETERS.json']) + kappa, qC = F(P['target']), F(P['provider']) + need(kappa == F('0.0030217754') and qC == F('0.0030217755'), 'stated #4635 target/provider') + x = lift_params(kappa, qC) + for k_mine, k_theirs in (('q', 'q'), ('stop', 'stop'), ('delta', 'delta'), ('r', 'spare'), + ('layout', 'layout'), ('xi', 'xi')): + need(x[k_mine] == F(P[k_theirs]), 'parameter mismatch '+k_theirs) + need(x['eps'] == F(P['epsilon']) and x['beta'] == F(P['beta']), 'epsilon/beta mismatch') + sav, guards, excess, failed = ledger(kappa, x['q'], x['eps'], x['beta'], x['r'], x['xi'], qC, x['stop']) + need(not failed, '#4635 ledger fails: %r' % failed) + need(sav == {k: F(v) for k, v in P['savings'].items()}, 'nine savings differ from PARAMETERS.json') + stored = {k: F(v) for k, v in P['guards'].items()} + mine = dict(guards) + for k, v in excess.items(): + mine[k+'_excess'] = v + for k, v in stored.items(): + need(k in mine and mine[k] == v, 'guard differs from PARAMETERS.json: '+k) + need(min(excess.values()) == F(P['minimum_excess']) == excess['main'], 'minimum excess') + # rejecting controls, each must fail for the stated reason + ctl = {} + try: + lift_params(qC, qC) + except ValueError as e: + ctl['kappa_equals_provider'] = str(e) + try: + lift_params(F(1, 10), F(1, 2)) + except ValueError as e: + ctl['kappa_above_3_32'] = str(e) + try: + lift_params(kappa, F('0.0030201656')) + except ValueError as e: + ctl['4635_kappa_on_4630_provider'] = str(e) + s2 = ledger(kappa, x['q'], x['eps'], x['beta'], x['r'], x['xi'], qC, x['stop'])[0] + unfused = 1-x['eps'] # O(T d) Gaussian evaluation saves only 1-epsilon = delta + ctl['unfused_gaussian_row'] = 'saving %s <= kappa' % float(unfused) if unfused <= kappa else None + need(len([v for v in ctl.values() if v]) == 4 and s2 == sav, '#4635 controls') + return dict(kappa=kappa, qC=qC, params=x, excess=excess, controls=ctl) + + +def check_4630(blobs): + src = blobs['vendor/pr4630/native_ledger.py.txt'].decode() + for lit in ("PROVIDER=F('0.0030201656')", "Q=F('0.00302016555')", "STOP=F(1,10**9)", + "TARGET=F('0.0030201655')", "epsilon=1-F(1,10**8), beta=1-F(3,10**8)", + "r=F(1,10**9)", "xi=epsilon*(1+q)-F(3,32)+F(1,10**10)"): + need(lit in src, '#4630 ledger constant not found: '+lit) + base = dict(kappa=F('0.0030201655'), q=F('0.00302016555'), eps=1-F(1, 10**8), + beta=1-F(3, 10**8), r=F(1, 10**9), provider=F('0.0030201656'), stop=F(1, 10**9)) + + def run(**kw): + a = dict(base, **kw) + xi = a['eps']*(1+a['q'])-C32+F(1, 10**10) + return ledger(a['kappa'], a['q'], a['eps'], a['beta'], a['r'], xi, a['provider'], a['stop']) + sav, guards, excess, failed = run() + need(not failed, '#4630 ledger fails') + need(min(excess.values()) == excess['main'] == F('0.0000000000197983445'), '#4630 minimum excess') + ctl = {} + for name, kw, expect in ( + ('epsilon_one', dict(eps=F(1)), {'epsilon_below_one'}), + ('unfunded_outer_target', dict(kappa=F('0.00302016555')), {'main_excess'}), + ('key_fills_whole_word_power', dict(beta=1-F(1, 10**8)), {'group_key'}), + ('membership_at_edge', dict(beta=1-F(2, 10**8)), {'membership'}), + ('normalization_at_edge', dict(r=F(1, 10**8)), {'global_gamma'})): + failed = set(run(**kw)[3]) + need(expect <= failed, '#4630 control %s did not fail for its stated reason: %r' % (name, failed)) + ctl[name] = sorted(failed) + return dict(excess=excess, controls=ctl) + + +# ---------------------------------------------------------------- main +def main(): + blobs, ctl_sha = load_sources() + A = delta_ledger(blobs, ctl_sha) + R = roots(A) + ABS = absorption(R) + L35 = check_4635(blobs) + L30 = check_4630(blobs) + sel = json.loads(blobs['selected']) + kap_sel = F(sel['kappa']) + need(kap_sel == F('0.00302015') and kap_sel < F(R['4630']['saving']), 'selected kappa vs p16 root') + # bind stated brackets / q_C in the vendored provider checks (text only) + need("lo,hi=F('.9969798340229'),F('.9969798340230')" in blobs['vendor/pr4630/critical_check.py.txt'].decode(), + '#4630 stated root bracket not found') + need("lo,hi=F('.9969782241'),F('.9969782242')" in blobs['vendor/pr4635/critical_provider_check.py.txt'].decode() + and "qC=F('.0030217755')" in blobs['vendor/pr4635/critical_provider_check.py.txt'].decode(), + '#4635 stated root bracket / q_C not found') + T, P1 = A['T'], A['P1'] + th = R['4635']['theta'] + eta = th*(ln(145)*(th-1)).exp() + mir = mirror_max(T, P1, th) + need(mir < D('0.562811') < D('0.564') < D('0.982097') < eta, '#4635 stated mirror/capacity bounds') + # local paid moment change g(t) = sum dloc_r r^t, negative at the new root + g = sum(c*(ln(r)*th).exp() for r, c in A['dloc'].items()) + need(g < 0, 'local paid moment change must be negative at the root') + dk = F('0.0030217754') - F('0.0030201655') + need(dk == F('0.0000016099'), 'stated kappa step') + ds = D(R['4635']['saving']) - D(R['4630']['saving']) + slack30 = D(R['4630']['saving']) - D('0.0030201655') + slack35 = D(R['4635']['saving']) - D('0.0030217754') + need(abs((D(dk.numerator)/D(dk.denominator) - ds) - (slack30 - slack35)) < D('1e-30'), 'decomposition') + # negative controls on the roots / absorption + rej = {} + try: # old #4630 profile cannot support #4635's provider q_C + need(F(R['4630']['saving_hi']) > F('0.0030217755'), 'old p16 root below #4635 q_C') + except ValueError as e: + rej['4630_profile_with_4635_qC'] = str(e) + try: # q_C above the true raw root is not absorbed + gap, logA, over = absorption_margin(th, F('0.0030217759')) + need(gap*10**12*LN2_HI - logA - over > 0, 'q_C above raw root not absorbed') + except ValueError as e: + rej['qC_above_root'] = str(e) + try: # a tampered vendored input is rejected by its head pin + bad = dict(blobs) + bad['vendor/pr4635/ARITHMETIC.json'] = blobs['vendor/pr4635/ARITHMETIC.json'].replace(b'"5": 40', b'"5": 41', 1) + load_sources(vendor_bytes=bad) + except ValueError as e: + rej['tampered_vendored_profile'] = str(e) + try: # bracket from #4630 applied to the #4635 profile is rejected + need(not sign_at(T, P1, '.9969798340229') and sign_at(T, P1, '.9969798340230'), 'wrong bracket') + except ValueError as e: + rej['4630_bracket_on_4635_profile'] = str(e) + need(len(rej) == 4, 'a negative control was accepted: %r' % rej) + + s = lambda x, n=22: str(x)[:n] + out = { + 'status': 'PASS_4635_DELTA_IS_PROFILE_ONLY', + 'changed_inputs': { + 'local_paid_delta_per_LOCAL_call': A['dloc'], + 'global_paid_delta': dict(sorted(A['gdelta'].items())), + 'LOCAL_calls': 18, 'targets_helpers_controller': 'unchanged (controller blob = main joint-helper-lattice/CONTROLLER.json)', + 'pr4635_ARITHMETIC_equals_pr4610_round3': True, + 'local_rank_mass': 5327, 'rank_mass_surplus_both': 752, + 'local_paid_moment_change_at_new_root': s(g), + }, + 'raw_saving_1_minus_theta': {k: s(v['saving'], 24) for k, v in R.items()}, + 'raw_saving_step': s(ds, 24), + 'stated_kappa_step': str(dk), + 'transfer_slack_raw_minus_kappa': {'4630': '%.12e' % slack30, '4635': '%.12e' % slack35}, + 'kappa_step_minus_raw_step': '%.12e' % (D(dk.numerator)/D(dk.denominator) - ds), + 'group_key_guard_equals_beta_below_epsilon': L35['params']['eps'] - L35['params']['beta'] == 2*L35['params']['delta'], + 'finite_absorption_log_margin_lower': {k: float(v['margin']) for k, v in ABS.items()}, + 'largest_qC_this_N_supports': {k: float(v['qC_max_at_this_N']) for k, v in ABS.items()}, + 'mirror_max_at_root_4635': s(mir, 10), 'capacity_eta_4635': s(eta, 10), + 'ledger_4635_min_excess': str(min(L35['excess'].values())), + 'ledger_4635_params': {k: str(v) for k, v in L35['params'].items()}, + 'ledger_4635_controls': L35['controls'], + 'ledger_4630_min_excess': str(min(L30['excess'].values())), + 'ledger_4630_controls_fail_reasons': L30['controls'], + 'selected_kappa_below_p16_root': str(kap_sel), + 'negative_controls': rej, + 'scope': 'Profile delta, critical roots, finite-absorption and native-ledger arithmetic only. ' + 'Not covered: all-fiber algebraic identity of the #4610 word, retained analytic/compiler proofs, ' + 'the funded-majorant U/V/Q/d guards, the native algorithms themselves.', + } + print(json.dumps(out, indent=2, default=str)) + + +if __name__ == '__main__': + try: + main() + except ValueError as e: + print('FAIL:', e) + sys.exit(1)