From 26502792b9d46fc353fc7b092de070a675264fd8 Mon Sep 17 00:00:00 2001 From: pinterbanget Date: Thu, 22 Oct 2026 11:40:30 +0700 Subject: [PATCH 1/2] =?UTF-8?q?Independently=20check=20#4535's=20arithmeti?= =?UTF-8?q?c=20(=CE=BA=20=3D=200.003020165):=20critical=20root,=20gap=2037?= =?UTF-8?q?7e-12,=20mirror,=20absorption,=20binding=20outer=20row=20(no=20?= =?UTF-8?q?new=20=CE=BA)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-Authored-By: Claude Opus 5.5 --- .../pr4535-arithmetic-check/.gitattributes | 1 + research/pr4535-arithmetic-check/README.md | 74 +++++ .../pr4535-arithmetic-check/RESULT-4535.json | 265 ++++++++++++++++++ research/pr4535-arithmetic-check/SOURCES.json | 24 ++ research/pr4535-arithmetic-check/TASK.json | 100 +++++++ research/pr4535-arithmetic-check/VERIFY.json | 20 ++ research/pr4535-arithmetic-check/verify.py | 214 ++++++++++++++ 7 files changed, 698 insertions(+) create mode 100644 research/pr4535-arithmetic-check/.gitattributes create mode 100644 research/pr4535-arithmetic-check/README.md create mode 100644 research/pr4535-arithmetic-check/RESULT-4535.json create mode 100644 research/pr4535-arithmetic-check/SOURCES.json create mode 100644 research/pr4535-arithmetic-check/TASK.json create mode 100644 research/pr4535-arithmetic-check/VERIFY.json create mode 100644 research/pr4535-arithmetic-check/verify.py diff --git a/research/pr4535-arithmetic-check/.gitattributes b/research/pr4535-arithmetic-check/.gitattributes new file mode 100644 index 0000000000..f35e2cd035 --- /dev/null +++ b/research/pr4535-arithmetic-check/.gitattributes @@ -0,0 +1 @@ +RESULT-4535.json -text diff --git a/research/pr4535-arithmetic-check/README.md b/research/pr4535-arithmetic-check/README.md new file mode 100644 index 0000000000..6604f42322 --- /dev/null +++ b/research/pr4535-arithmetic-check/README.md @@ -0,0 +1,74 @@ +# Independent arithmetic check of #4535 (conditional κ = 0.003020165) + +**Claim type:** an independent arithmetic check with certified intervals. **No new κ.** It covers hexapode's +[#4535](https://github.com/CrocSwap/integer-mult-bounds/pull/4535) (head `cca1112d`). That PR combines +dillona's #4532 critical-root compiler with #4470's unchanged p16 supplier, and proposes conditional κ += 0.003020165, up from 0.00302015. #4535's `RESULT.json` is vendored here (SHA256-pinned, `-text`). The p16 +profile is read from main. + +## What is checked + +1. **The critical exponent.** `[θ_lo, θ_hi] = [0.9969798340229, 0.996979834023]` brackets the crossing + `T_θ = P_θ`, certified on both sides. It equals exactly 1 minus the raw-root bracket + `(0.0030201659770, 0.0030201659771)` that my #4478 certified for #4470. +2. **The saving order.** κ = 604033/200000000 is below the uniform saving 3775207/1250000000, and + `t − θ_hi = 377/10¹²` exactly, with `t = 1 − uniform saving`. +3. **The mirror condition at θ.** `E_J(θ_hi) ≤ β·S_J(θ_lo)` holds on every elementary window, with + `β = 141/250`. The worst ratio is **0.56281**, in the window (1/48, 1/41), matching #4535's maximizing cell. +4. **Absorption.** `A·N^θ(133 + ln N)^{2/5} ≤ N^t`, with `ln A ≤ (1 − θ_lo)·ln(145·1024^{650}) = 13.6223`, + which is #4535's `logA_upper`: + + | evaluation point | margin (lower) | + | --- | ---: | + | `ln N = 10¹²`, #4535's `log_threshold` | 352.33 | + | the stated `N = 2^{10¹²}` | 236.79 | + + It is monotone beyond both points, since `t − θ > p/(133 + ln N)`. + + **Labelling note.** #4535's `margin_lower`, 352.33, is computed at `ln N = 10¹²`, while its + `primary_certified_N` is `2^{10¹²}`, which has the smaller `ln N ≈ 6.93·10¹¹`. The inequality still holds + there, with margin 236.79, so the conclusion is unaffected. +5. **The outer rows.** Seven of the nine rows exceed κ: + + | Row | Formula | + | --- | --- | + | main transform | `εq` | + | global router | `a` | + | fused Gaussian | `1−ε+qβ` | + | group bit router | `1−ε+aβ` | + | group scans | `1−ε+β` | + | polynomial products | `ε` | + | micro-box faces | `79−ε−β` | + + The **binding main-transform margin is exactly the reported 29969798347/10²⁰**. The parameters follow the + schedule `κ + 7d, 6d, 5d, 4d, 3d` and `1 − d`, `1 − 3d`, with `d = 10⁻¹⁰`. The two ξ rows are not recomputed, + because ξ is not printed among #4535's outer parameters. + +## Not covered + +- #4532's critical-root theorem: the leaf bound `L(n) ≤ A n^θ(c + log n)^p` and its gate criterion. +- The finite envelope, owned storage, routing, precision, stock and tape bounds. +- The native and physical premises. +- The two ξ outer rows. + +## Reproduce + +```sh +python3.12 -B scripts/research_package.py --package research/pr4535-arithmetic-check --check-only +python3.12 -B scripts/research_package.py --package research/pr4535-arithmetic-check +``` + +The verifier prints `PASS_PR4535_ARITHMETIC_CHECK` in about 10 seconds, using only the standard library. + +## Open next questions + +1. **Print ξ (`cap_xi`) in #4535's outer parameters, so all nine rows can be recomputed.** +2. **An independent check of #4532's critical-root leaf bound.** + +## Credit + +- The construction is hexapode's (#4535). +- The critical-root compiler is dillona's (#4532). The profile comes from #4470. + +Prepared by Ryanson Jonathan with substantial Claude Code (Claude Opus 5.5) assistance. +Apache-2.0. diff --git a/research/pr4535-arithmetic-check/RESULT-4535.json b/research/pr4535-arithmetic-check/RESULT-4535.json new file mode 100644 index 0000000000..7665be4201 --- /dev/null +++ b/research/pr4535-arithmetic-check/RESULT-4535.json @@ -0,0 +1,265 @@ +{ + "BIT_admission": { + "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" + }, + "absorption": { + "conclusion": "A*N^theta*(133+logN)^(2/5)<=N^t above this finite cutoff; physical implementation overhead not inferred", + "cost_all_larger_N_monotonicity": true, + "cost_margin_lower": "646/3", + "logA_upper": "11588535078387598648766751054204368156120388952774219/850705917302346158658436518579420528640000000000000", + "log_threshold": 1000000000000, + "margin_lower": "299725246478781048809002279469549139266283611047225781/850705917302346158658436518579420528640000000000000", + "positive_gap": "377/1000000000000", + "primary_certified_N": "2^1000000000000", + "secondary_conservative_N_cutoff": "2^2000000000000" + }, + "critical_root": { + "beta": "141/250", + "conclusion": "Unique crossing on this bracket; critical-root hypotheses hold.", + "critical_root_interval": [ + "9969798340229/10000000000000", + "996979834023/1000000000000" + ], + "derivative_floor": "1", + "endpoint_target_minus_paid": [ + [ + "-1/1000000", + "0" + ], + [ + "0", + "1/1000000" + ] + ], + "funded_mirror_cells": [ + { + "left": "1/72", + "right": "1/65", + "upper_ratio": "141309/500000" + }, + { + "left": "1/65", + "right": "1/64", + "upper_ratio": "37509/250000" + }, + { + "left": "1/64", + "right": "1/57", + "upper_ratio": "477989/1000000" + }, + { + "left": "1/57", + "right": "1/56", + "upper_ratio": "303319/1000000" + }, + { + "left": "1/56", + "right": "1/49", + "upper_ratio": "135741/250000" + }, + { + "left": "1/49", + "right": "1/48", + "upper_ratio": "187981/500000" + }, + { + "left": "1/48", + "right": "1/41", + "upper_ratio": "562811/1000000" + }, + { + "left": "1/41", + "right": "1/40", + "upper_ratio": "25767/62500" + }, + { + "left": "1/40", + "right": "1/33", + "upper_ratio": "140197/250000" + }, + { + "left": "1/33", + "right": "1/32", + "upper_ratio": "430399/1000000" + }, + { + "left": "1/32", + "right": "1/25", + "upper_ratio": "68367/125000" + }, + { + "left": "1/25", + "right": "1/24", + "upper_ratio": "220287/500000" + }, + { + "left": "1/24", + "right": "1/17", + "upper_ratio": "52779/100000" + }, + { + "left": "1/17", + "right": "1/16", + "upper_ratio": "450273/1000000" + }, + { + "left": "1/16", + "right": "1/9", + "upper_ratio": "101799/200000" + }, + { + "left": "1/9", + "right": "1/8", + "upper_ratio": "60647/1000000" + }, + { + "left": "1/8", + "right": "1/7", + "upper_ratio": "9019/500000" + }, + { + "left": "1/7", + "right": "1/5", + "upper_ratio": "3127/250000" + }, + { + "left": "1/5", + "right": "1/4", + "upper_ratio": "13237/1000000" + } + ], + "maximizing_cell": [ + "1/48", + "1/41" + ], + "mirror_upper": "562811/1000000", + "scope": "Rank-inventory admission criterion; native and outer obligations inherited.", + "source_capacity_lower": "491053/500000", + "uniform_mean_gap_lower": "521143/500000" + }, + "finite_envelope": { + "G_depth_upper": 200000000000, + "class_envelope": "C_N <= W0*(W0+P0+1)^(G_depth+1) < 2^3400000000031", + "divisible_width_bound": "B_N < C_N^N", + "full_call_centre_episodes_per_raw_unit": 144, + "height_base": 1024, + "height_multiplier": 2, + "log2_C_N_strict_upper": 3400000000031, + "owned_space_scope": "144U and1680U bound separate raw episodes, not total live scratch. Actual compiler/parking allocations require their own O ledger.", + "primary_N": "2^1000000000000", + "proof_scope": "Height/class recurrence, denominator clearing and positive-surplus occurrence inequalities are inherited proof premises. Only their displayed integer arithmetic is checked; no gigantic word or B_N is materialized.", + "raw_occurrence_bound": "U <= B_N*N/752", + "raw_paid_jobs": 64620, + "raw_productive_fields": 10928, + "raw_rank_surplus": 752, + "thin_query_episodes_per_raw_unit": 1680 + }, + "functional_checks": 4, + "kappa": "604033/200000000", + "minimum_outer_margin_above_kappa": "29969798347/100000000000000000000", + "outer_checks": 54, + "outer_parameters": { + "a": "15100827/5000000000", + "b": "6040331/2000000000", + "beta": "9999999997/10000000000", + "bit_saving": "17/5000", + "complex_uniform_saving": "3775207/1250000000", + "d": "1/10000000000", + "epsilon": "9999999999/10000000000", + "kappa": "604033/200000000", + "layout": "1/10000000000", + "q": "30201653/10000000000", + "r0": "1/100000000000", + "stop": "1/10000000000", + "tested_saving": "30201657/10000000000" + }, + "physical_bridge": "Conditional proof premise: retained native, movement, precision, stock and fixed-tape closure must apply to the fixed expanded word; this arithmetic check does not establish physical admission.", + "rejected_mutations": { + "closedrootgap": "closed root gap", + "kappa_equals_uniform": "raw kappa lacks uniform slack", + "log_absorption_failure": "log absorption derivative", + "nativeprofile": "native profile altered" + }, + "retained_root_applications_replayed": [ + "p7", + "p16" + ], + "source_sha256": { + "research/adaptive-gate-existence/PROOF.md": "340d637feef40f44a808c718207c0fede12cc483e2c979b86c56bb736b9c1ef5", + "research/adaptive-gate-existence/SOURCES.json": "ca5f833fd92acd6fac36fef73692550f4250b39f24760840e72b5868884048d9", + "research/adaptive-gate-existence/WITNESS.json": "f1fa3d91efe8fb32e038941776f9db54a6d935eeb2b28bd2b3168aa8f70251e4", + "research/adaptive-gate-existence/root_application.py": "e656ef12f73a8dd3bdb256eca95a712de1269facb18a652fc4068ba718619b4d", + "research/adaptive-gate-existence/verify.py": "9f0c0fbddbba2d9c38a73097db911fc5cdacf8ea1d182e037f4779577dca253a", + "research/compact-joint-compiler/PROOF.md": "3f337fba12288d3b5e51af9541e2a645f79c8668fabf48b212672285fe6150b4", + "research/compact-joint-compiler/arithmetic/RESULT.json": "a6caaa2a6d6460a8c1ef7e48c4853bb27976be33a52b96a4216dfa90d96c9091", + "research/direct-mixed-flow/README.md": "78351e2419eb1ff1d645addd411158b91b381b23a962a91b6deeebeacd5192a8", + "research/fresh-helper-boundary/ARITHMETIC-RESULT.json": "5d25fec9ac4b036c93846a50dccfa4af030e2982f5cec02e28702193bf157cf7", + "research/fresh-helper-boundary/CHANGES.json": "cde73b8ff5b3c0d06e69e2293b991b24fd14a16dd4ccab7ff6b3439074a94624", + "research/fresh-helper-boundary/NATIVE-RESULT.json.gz": "37d0848458b289eb50271c47adef6e74014ae30be6363d09394b2337b566b839", + "research/fresh-helper-boundary/RESULT.json": "34163eeeef1cd712de457d7fd3b0435f98a12ac456b82256b078f33225456fbd", + "research/fresh-helper-boundary/SOURCES.json": "01998e9b86222d10811fc0114dcd5c946ff9e95025a7cacd00e67a3eefe543d0", + "research/fresh-helper-boundary/arithmetic.py": "212bae96d0ddcbc25076afe2589a47736c66b77420057f28c44c937ad087fc07", + "research/fresh-helper-boundary/native.py": "9b55a2d3c3972148fae9d112e745d9244968166bd89bd900c938f429fc76ab29", + "research/fresh-helper-boundary/verify.py": "4c18851214400cf955e10565d89357029d9e765140233831472ce23f0c3ee7bf", + "research/fresh-helper-thinned/PROOF.md": "9883b3329fef7624d3471e27bb55258cd9dc18bb6d37779a3939de99add87347", + "research/fresh-helper-thinned/README.md": "70c1c872c2327c3f71918e218d5f1ecb7a00037771a5dd1b8ae415b84cc90dc2", + "research/fresh-helper-thinned/RESULT.json": "8e7db2fed5f4be6a7f944bc59e7942ccbcc3e6c36130b5671331540c183ada21", + "research/fresh-helper-thinned/SOURCES.json": "5aec5df5096ee8a3e90618d311640b4bdfba42be5bc4bc5fab55e8be858ab2cb", + "research/fresh-helper-thinned/verify.py": "c841265ccee9b6f79045ad818ce9d27cfd7ee1f60047525a75d491f0dd8b997a", + "research/higher-moment-strictification/README.md": "ebe80b68ff026ce90f71f274c31744f4c0b36132d15ebb7e39cf2d5df4df270d", + "research/higher-moment-strictification/RESULT.json": "ad79e3c0459e7b495a0ca34010553b12147779a007389e1695cc1336f123c156", + "research/higher-moment-strictification/verify.py": "0ce7e7137422d5ffeda22085c81fa88471bbe963100fdad62e659f1e3bf89326", + "research/joint-helper-lattice/RESULT.json": "c7b2388f6511c19976b337d8c8ac374610af616866a249d75dace704eb5d9e21", + "research/joint-helper-lattice/SOURCES.json": "4045942a3b3516380c980b547e80ac254bc22e4c21c74ac16e48d3f0e46955f6", + "research/joint-helper-lattice/VERIFY.json": "1d004a782ff9d8264e4f3f6e6fbee729047ec7a24874fb03728695ef527786a8", + "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-0023-productive-jobs/dependencies/kappa-next-regime/direct-decoder/sources/DATA-PHASES.json": "c5916ff312678f12aba403847643fbbc29f643acec60bdf836fa56cd3e8251fa", + "research/kappa-causal-continuation/buffer-borrowing/verify_buffers.py": "106b4d5e052427230df452f0c901d5390a0583782960b80a8af94d9a984022c7", + "research/kappa-function-composition/complex/prune_native.py": "f2b37c183a10922eabc8e0436b426a08866430e96bd0adc7e178951c7fbb5257", + "research/kappa-rebuild/architecture/mixed_target_probe.py": "011c3c9d0cf81103dc84d709a0e36793eb7c5ae3f23c85eac27650ef13afa04a", + "research/kappa-rebuild/bit/BIT-ALLSIZE-PARAMETERS.json": "edb273f59a27356ad89f38791590c3c806b228c3510eb508e01e89f2caba95ef", + "research/kappa-rebuild/bit/BIT-P3-NATIVE-BINDING.json": "9ece46fdfda6182e757e9a3b1f513fb3d029d730f3bafdcd6ed59180a14175b0", + "research/kappa-rebuild/bit/DELAYED-COVER-BRIDGE.md": "9731b93026717f5fa15851e3633cbb4bdc76eba2bffb9d6b4a3b69f7dd502443", + "research/kappa-rebuild/bit/MIXED-PRODUCTIVE-BIT.json": "2f69a19f417c0e0d141c180f9b2fae3d358391b9a230f5848ee07c45450e70bf", + "research/kappa-rebuild/bit/bit_native_binding.py": "bf6374225f388e7531fa6475cc255bd430100ff62c38d582c41601f0739de7b7", + "research/kappa-rebuild/bit/complex_controller_factor.py": "1de9aaf918e6a4f2f5448754c1f3c3da3b85e6257849ebd097af09859c4e5497", + "research/kappa-rebuild/bit/mixed_productive_bit.py": "b32291b0db7fc0d332ec444c70746ab0fb03351d2e50546f8bcb64060e3ff95e", + "research/kappa-rebuild/complex/FULL-IDENTITY.md": "c4aa88c4943ef041e9542c519b7600ecf26ed6caff92558fdb07ac88ace64c17", + "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/native_extensions.py": "50ad007d9c386393657e86c99a96ae0a63a8fbc52872579b185002cc626e88e3", + "research/kappa-rebuild/complex/power_two_balance.py": "76929bb3887911ccf100c4593574b8a1c82ee64e96f939a8aca196869438b424", + "research/kappa-rebuild/complex/rebuild_native.py": "f94c527cc02215de49350d477618188c4c0da48bc8fb05b4e37b24c482cad7d5", + "research/kappa-rebuild/transfer-audit/FINITE-TEMPLATE-CLOSURE.md": "3f8508c63862dd83968bd30df91b08ba5afcee1e10db15ca546cdff0caef95d9", + "research/kappa-rebuild/transfer-audit/p3_native_audit.py": "5504a55a50546418d10c522984438cdeedb44993f7c1dab7bd4aa1ae0515d902", + "research/missing-join-frame/NATIVE.json.gz": "96718b257db24f4f62d3b86b36cdd514e67d2cb99947ddd7bdcb9b55a2c17841", + "research/missing-join-frame/PATCH.json": "9ab5328245ff02c9d0be21d39bcc375f50bc5d7909e9f7b9a3a9a6f812f5bd6e", + "research/missing-join-frame/PROOF.md": "50061c25d379ff5733135dbed53e8721bbd4dbee6766d1609d8a2ecdebb7dc06", + "research/missing-join-frame/RESULT.json": "25f2cbcde988847ff86f44e804982069863ec99ff68097f16e9bb7a1a17c4cd0", + "research/missing-join-frame/verify.py": "21429dd9c1b9c93ebb57e5fbb8ef674d0e4146ac8c25cc7c097c3352c02366a4", + "research/pr4359-p7-padding/P7-FACTOR.json": "6f96f6be5d8441f71cbe6ebb1657c69b543eb085b848b92b591b7ac01d6e6598", + "research/pr4359-p7-padding/TENSOR.md": "b2eba86cb979b4dc2a045f2e74bbd29e4d9e5ec87d6a2bc23ba7b54f1f58e3e3", + "research/pr4359-p7-padding/dependencies/compiler-refill/endpoint.py": "d097e55f06c3f244f2074ffd7c1a0a5f3c4b4b6a6accf9619d1dde5c0ae85e15", + "research/pr4359-p7-padding/native_inventory.py": "65539acaf45bdfe8c5aee6830f9c9b3d1107c442a60842ef803fdd7688de8f32", + "research/query-thinned-controllers/BIT-CONTROLLER.json": "39ac84fb848b908f7ba051fae4556d507900c421dc5d23501a9c0cb1d61fd08d", + "research/query-thinned-controllers/COMPLEX-CONTROLLER.json": "bf1143325d8380fab40cd5a85449f9a5412f0340deba7f4693714c92ae320088", + "research/query-thinned-controllers/RESULT.json": "6ebfc8c0f09166f4834e9d7427410cb31aefff2cd4d4ce588c8e52c9c70e9a0f", + "research/query-thinned-controllers/SOURCES.json": "74b73563d9f78a4562d376b6f33528d652e41097f65747667f112a3e1fa81d29", + "research/query-thinned-controllers/controller.py": "8b462d660487b1be4940357c4c7522967b1bfaede3c02b1c66109b85acae0fd2", + "research/query-thinned-controllers/verify.py": "07dea601d6bbaa4d90e576f20c8607c37fb01e8778c798d919fa9df435049950", + "research/rank-convergence/BENCHMARKS.json": "513efe2fe74af82891c1918e462ba8338b1bbd06403cbfcec284bcf3b4f8f850", + "research/rank-convergence/PROOF.md": "3c971c5670669cb36312815b111e64c83e1490a10ee82f5412bd9aee01e9c376", + "research/rank-convergence/README.md": "e77af882d3f02a9d3f2dd19dce889052f63892a1c8f39fdbe0813ff5fab5e8c1", + "research/t74-native-fast/vendor/native/new/code/borrow/vendor/clifford/clifford_exact.py": "2982ead07721e83358dc67c6f49c2b4c16a236a6bebdfd72f58221be1f5d0962" + }, + "status": "PASS_EXACT_CONDITIONAL_PARAMETER_CERTIFICATE", + "uniform_saving": "3775207/1250000000" +} diff --git a/research/pr4535-arithmetic-check/SOURCES.json b/research/pr4535-arithmetic-check/SOURCES.json new file mode 100644 index 0000000000..a422a260e8 --- /dev/null +++ b/research/pr4535-arithmetic-check/SOURCES.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "base_commit": "f9f85c1e4fa1e955ff39f10fca447e3e2a4e4adc", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ed33caef5c5827693e9572d252a66f99cbb73d40", + "sha256": "5732707cc1e460b090b53f2463162749ad860de878a18f7408938671d295a9d9" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "64bfc5af6709ed9811171e0a2108f05e1219cb65", + "sha256": "352a6184713b8843d96fd2c2071eb7aeaa655906b7c51d45ad444912666c8a96" + }, + { + "path": "research/compact-joint-compiler/arithmetic/RESULT.json", + "usage": "input", + "git_blob": "514d12ce4d2d824a4e0a418022bba610c8aed8ff", + "sha256": "a6caaa2a6d6460a8c1ef7e48c4853bb27976be33a52b96a4216dfa90d96c9091" + } + ] +} diff --git a/research/pr4535-arithmetic-check/TASK.json b/research/pr4535-arithmetic-check/TASK.json new file mode 100644 index 0000000000..3a24255b1c --- /dev/null +++ b/research/pr4535-arithmetic-check/TASK.json @@ -0,0 +1,100 @@ +{ + "schema_version": 1, + "task_id": "independent-moment", + "priority_revision": 7, + "base_commit": "f9f85c1e4fa1e955ff39f10fca447e3e2a4e4adc", + "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": "Independent arithmetic check of #4535 (conditional kappa 0.003020165).", + "scope_change_reason": "Independent coverage of a new conditional kappa claim.", + "bottleneck_link": "Independent coverage of the newest kappa improvement.", + "budget_minutes": 45, + "stop_rule": "Stop at the arithmetic; #4532's theorem out of scope.", + "outcome": "completed", + "evidence": "Critical root = 1 - raw-root bracket; gap 377/1e12; mirror worst 0.56281; lnA 13.6223 matches; absorption margin 352.33 at ln N=1e12 and 236.79 at N=2^(1e12); binding outer margin 29969798347/1e20 matches; schedule kappa + k d.", + "author": "Ryanson Jonathan, with Claude Code (Claude Opus 5.5) assistance", + "ai_assistance": "Substantial Claude Code (Claude Opus 5.5) assistance; no independent human review.", + "open_questions": [ + { + "question": "Print xi in #4535's outer parameters and recompute all nine rows.", + "why_it_matters": "Completes outer coverage.", + "first_step": "Ask the author to export cap_xi.", + "blocked_by": "Author data." + } + ] +} diff --git a/research/pr4535-arithmetic-check/VERIFY.json b/research/pr4535-arithmetic-check/VERIFY.json new file mode 100644 index 0000000000..2bab0e950e --- /dev/null +++ b/research/pr4535-arithmetic-check/VERIFY.json @@ -0,0 +1,20 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/compact-joint-compiler/arithmetic/RESULT.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 300, + "checks": "#4535 arithmetic: critical-root bracket = 1 - #4478 raw-root bracket, gap 377/1e12, mirror at theta (worst 0.56281 <= 141/250), absorption margins at ln N = 1e12 and N = 2^(1e12), seven outer rows with binding margin 29969798347/1e20, parameter schedule." + } + ] +} diff --git a/research/pr4535-arithmetic-check/verify.py b/research/pr4535-arithmetic-check/verify.py new file mode 100644 index 0000000000..89085673b8 --- /dev/null +++ b/research/pr4535-arithmetic-check/verify.py @@ -0,0 +1,214 @@ +#!/usr/bin/env python3 +"""Independent arithmetic check of #4535: conditional kappa 0.003020165 via critical-root transfer. + +Reads #4535's RESULT.json (vendored as RESULT-4535.json, sha256 pinned to head cca1112d) and the unchanged p16 +profile on main (research/compact-joint-compiler/arithmetic/RESULT.json; 10,928 fields, 64,620 paid jobs). With its +own certified intervals (helpers of research/rank-convergence-gates) it checks: + * the critical-root interval [theta_lo, theta_hi] brackets the T_t = P_t crossing and equals 1 minus #4478's raw-root + bracket (0.0030201659770, 0.0030201659771); + * kappa < uniform saving and t - theta_hi = 377/10^12 exactly (t = 1 - uniform saving); + * the mirror windows at theta: E_J(theta_hi) <= beta S_J(theta_lo) with beta = 141/250 (worst 0.56281); + * absorption A N^theta (133 + ln N)^(2/5) <= N^t with ln A <= (1 - theta_lo) ln(145 * 1024^650), at ln N = 10^12 + (#4535's log_threshold) and at the stated N = 2^(10^12), and its monotonicity (gap > p/(c + ln N)); + * seven of the nine outer rows (main transform eps*q, global router a, fused Gaussian 1-eps+q*beta, group bit router + 1-eps+a*beta, group scans 1-eps+beta, polynomial products eps, micro-box faces 79-eps-beta) exceed kappa; the + binding main-transform margin equals the reported minimum 29969798347/10^20; the parameter schedule is kappa + k d. +xi is not printed in #4535's outer parameters, so the two xi rows are not recomputed. +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 +ROOT = HERE.parents[1] +RESULT_SHA = "85f6e8a659c53c49acfde141eaae3ece0b7d8c5c1750b82674bc7292e7d630e8" + + +def need(condition, message): + if not condition: + raise AssertionError(message) + + +GRID = Q(1, 10**50) + + + + +def down(x): + return (x / GRID).__floor__() * GRID + + +def up(x): + return (x / GRID).__ceil__() * GRID + + +def ln_bounds(n): + """certified ln n for integer n >= 1 (reduction to [1, 2) and the atanh series)""" + if n == 1: + return Q(0), Q(0) + k = n.bit_length() - 1 + y = Q(n, 2 ** k) + out = [Q(0), Q(0)] + for part, scale in ((y, 1), (Q(2), k)): + if part == 1 or scale == 0: + continue + u = (part - 1) / (part + 1) + s, term, j = Q(0), u, 0 + while True: + s += term / (2 * j + 1) + j += 1 + term *= u * u + tail = term / (2 * j + 1) / (1 - u * u) + if tail < GRID: + break + out[0] += scale * down(2 * s) + out[1] += scale * up(2 * (s + tail)) + return out[0], out[1] + + +def exp_bounds(x_lo, x_hi): + """certified exp on a small interval (|x| < 1)""" + def series(x): + s, term = Q(0), Q(1) + for i in range(70): + s += term + term = term * x / (i + 1) + return s, abs(term) * 2 + a, ea = series(x_lo) + b, eb = series(x_hi) + return down(a - ea), up(b + eb) + + +LN = {} + + +def ln(n): + if n not in LN: + LN[n] = ln_bounds(n) + return LN[n] + + +def moment(hist, C): + """bounds of sum count * k^(1-C)""" + lo = hi = Q(0) + for k, w in hist.items(): + e = exp_bounds(-C * ln(k)[1], -C * ln(k)[0]) + lo, hi = lo + w * k * e[0], hi + w * k * e[1] + return lo, hi + + +def lnq(x): + a, b = ln(x.numerator), ln(x.denominator) + return a[0] - b[1], a[1] - b[0] + + +def powq(base, e): + """certified base^e for integer base >= 1 and rational exponent e (|e ln base| < 1.2)""" + l = ln(base) + lo, hi = (e * l[0], e * l[1]) if e >= 0 else (e * l[1], e * l[0]) + return exp_bounds(lo, hi) + + + + +def rat(x): + return Q(x) + + +def ln_real(lo, hi): + """certified ln on a positive rational interval [lo, hi]""" + return lnq(Q(lo))[0], lnq(Q(hi))[1] + + +def expi(lo, hi): + """certified exp on an interval, reducing large |x| by halving and squaring""" + k = 0 + while max(abs(lo), abs(hi)) > Q(1, 2): + lo, hi, k = lo / 2, hi / 2, k + 1 + a, b = exp_bounds(lo, hi) + for _ in range(k): + a, b = down(a * a), up(b * b) + return a, b + + +def mgf(h, t): + """certified sum_k w k^t""" + lo = hi = Q(0) + for k, w in h.items(): + l = ln(k) + a, b = expi(t * l[0], t * l[1]) + lo, hi = lo + w * a, hi + w * b + return lo, hi + + +def logmean(h, t): + nlo = nhi = Q(0) + for k, w in h.items(): + l = ln(k) + a, b = expi(t * l[0], t * l[1]) + nlo, nhi = nlo + w * a * l[0], nhi + w * b * l[1] + dlo, dhi = mgf(h, t) + return nlo / dhi, nhi / dlo + + + + +def main(): + for row in json.loads((HERE / "SOURCES.json").read_text(encoding="utf-8"))["files"]: + need(hashlib.sha256((ROOT / row["path"]).read_bytes()).hexdigest() == row["sha256"], row["path"]) + raw = (HERE / "RESULT-4535.json").read_bytes() + need(hashlib.sha256(raw).hexdigest() == RESULT_SHA, "#4535 RESULT.json bytes") + R = json.loads(raw) + pr=json.loads((ROOT / 'research/compact-joint-compiler/arithmetic/RESULT.json').read_text(encoding='utf-8')); T={int(k):v for k,v in pr['targets'].items()}; P={int(k):v for k,v in pr['paid'].items()} + need(sum(T.values())==10928 and sum(P.values())==64620,"p16 invoice") + th_lo,th_hi=(Q(x) for x in R['critical_root']['critical_root_interval']) + # raw root: T_t - P_t changes sign across [th_lo, th_hi] + a=mgf(T,th_lo); b=mgf(P,th_lo); need(a[1]b[1],"T > P at theta_hi") + us=Q(R['uniform_saving']); kap=Q(R['kappa']); t=1-us + need(kapth_hi and t-th_hi==Q(377,10**12),"saving order and gap 377/1e12") + need(1-th_hi==Q(30201659770,10**13) and 1-th_lo==Q(30201659771,10**13),"theta interval = 1 - raw-root bracket (#4478)") + # mirror at theta (pointwise): E_J(theta_hi) <= beta S_J(theta_lo) + beta=Q(R['critical_root']['beta']); pts=sorted({Q(1,x) for x in list(T)+list(P)}); worst=Q(0) + pw={} + for r in P: + for k in T: + l=ln(r*k); pw[r,k]=(expi(th_lo*l[0],th_lo*l[1])[0],expi(th_hi*l[0],th_hi*l[1])[1]) + for lo,hi in zip(pts,pts[1:]): + mid=(lo+hi)/2 + E=sum(P[r]*T[k]*pw[r,k][1] for r in P for k in T if r>k and Q(1,r)r and Q(1,k)0 and E<=beta*S,"mirror"); worst=max(worst,E/S) + print("mirror worst",float(worst),"beta",float(beta)) + # absorption: (t - theta) lnN - lnA - p ln(c + lnN) > 0 with lnA <= (1-theta_lo) ln n0, n0 = 145*1024^650 + p=Q(2,5); c=Q(133); l1024=ln(1024); l145=ln(145) + ln_n0_hi=l145[1]+650*l1024[1] + lnA_hi=(1-th_lo)*ln_n0_hi + print("lnA upper (mine)",float(lnA_hi),"theirs",float(Q(R['absorption']['logA_upper']))) + for label,lnN in (("ln N = 1e12",(Q(10**12),Q(10**12))),("N = 2^(1e12)",(10**12*ln(2)[0],10**12*ln(2)[1]))): + lc=lnq(up(c+lnN[1]))[1] + margin=(t-th_hi)*lnN[0]-lnA_hi-p*lc + need(margin>0 and (t-th_hi)>p/(c+lnN[0]),label) + print(label,"margin lower",float(margin)) + # outer rows + op={k:Q(v) for k,v in R['outer_parameters'].items()} + e,q,a_,be,ka=op['epsilon'],op['q'],op['a'],op['beta'],op['kappa'] + print(sorted(op)) + rows={"main_transform":e*q,"global_coordinate_router":a_,"fused_gaussian":1-e+q*be,"group_bit_router":1-e+a_*be, + "group_scans":1-e+be,"polynomial_products":e,"microbox_face_corrections":1-(e+be+48-128+2)} + for k,v in rows.items(): need(v>ka,k) + mn=min(rows,key=rows.get); print("binding",mn,rows[mn]-ka, rows[mn]-ka==Q(R['minimum_outer_margin_above_kappa'])) + need(op['complex_uniform_saving']==us and op['kappa']==ka,"outer point binds uniform saving and kappa") + d=op['d']; need(op['tested_saving']==ka+7*d and us==ka+6*d and op['b']==ka+5*d and a_==ka+4*d and q==ka+3*d and e==1-d and be==1-3*d,"parameter schedule kappa + k d") + print("schedule ok") + + print(json.dumps({"status": "PASS_PR4535_ARITHMETIC_CHECK", "kappa": str(ka), "uniform_saving": str(us), + "mirror_worst": f"{float(worst):.6f}", "binding_margin": str(rows[mn] - ka), + "new_kappa_claimed": False}, indent=1)) + + +if __name__ == "__main__": + sys.exit(main()) From 4617b96cb4020dd6f36ccff3f0832381b62ba512 Mon Sep 17 00:00:00 2001 From: pinterbanget Date: Thu, 22 Oct 2026 12:56:06 +0700 Subject: [PATCH 2/2] #4535 check: finite envelope arithmetic Co-Authored-By: Claude Opus 5.5 --- research/pr4535-arithmetic-check/README.md | 10 +++++++++- research/pr4535-arithmetic-check/verify.py | 14 ++++++++++++++ 2 files changed, 23 insertions(+), 1 deletion(-) diff --git a/research/pr4535-arithmetic-check/README.md b/research/pr4535-arithmetic-check/README.md index 6604f42322..6a58b5074a 100644 --- a/research/pr4535-arithmetic-check/README.md +++ b/research/pr4535-arithmetic-check/README.md @@ -44,10 +44,18 @@ profile is read from main. schedule `κ + 7d, 6d, 5d, 4d, 3d` and `1 − d`, `1 − 3d`, with `d = 10⁻¹⁰`. The two ξ rows are not recomputed, because ξ is not printed among #4535's outer parameters. +6. **The finite envelope.** + - The height `G = 2⌊log₁₀₂₄⌊N/145⌋⌋` is at most `2·10¹¹` at `N = 2^{10¹²}`. + - Since `W₀ = 10,928 < 2¹⁴` and `W₀ + P₀ + 1 = 75,549 < 2¹⁷`, the class envelope is + `C_N < 2^{17G+31} ≤ 2^{3400000000031}`. + - The episode counts are 144 = 18·8 (centre) and 1,680 = 15·112 (thin queries). + + All of this matches #4535's `finite_envelope`. + ## Not covered - #4532's critical-root theorem: the leaf bound `L(n) ≤ A n^θ(c + log n)^p` and its gate criterion. -- The finite envelope, owned storage, routing, precision, stock and tape bounds. +- Owned storage, routing, precision, stock and tape bounds, beyond the displayed envelope arithmetic. - The native and physical premises. - The two ξ outer rows. diff --git a/research/pr4535-arithmetic-check/verify.py b/research/pr4535-arithmetic-check/verify.py index 89085673b8..73c91431c9 100644 --- a/research/pr4535-arithmetic-check/verify.py +++ b/research/pr4535-arithmetic-check/verify.py @@ -14,6 +14,8 @@ 1-eps+a*beta, group scans 1-eps+beta, polynomial products eps, micro-box faces 79-eps-beta) exceed kappa; the binding main-transform margin equals the reported minimum 29969798347/10^20; the parameter schedule is kappa + k d. xi is not printed in #4535's outer parameters, so the two xi rows are not recomputed. + * the finite envelope arithmetic: height G <= 2e11 at N = 2^(10^12), W0 < 2^14, W0+P0+1 < 2^17, C_N < 2^(17G+31) = + 2^3400000000031, and the episode counts 144 = 18*8 and 1680 = 15*112. Ryanson Jonathan with Claude Code (Claude Opus 5.5) assistance. Apache-2.0. """ from fractions import Fraction as Q @@ -205,6 +207,18 @@ def main(): d=op['d']; need(op['tested_saving']==ka+7*d and us==ka+6*d and op['b']==ka+5*d and a_==ka+4*d and q==ka+3*d and e==1-d and be==1-3*d,"parameter schedule kappa + k d") print("schedule ok") + # finite envelope (#4535 RESULT finite_envelope): height, class-count and episode arithmetic + fe = R["finite_envelope"] + W0, P0, M_, g_ = 10928, 64620, fe["height_base"], fe["height_multiplier"] + need((fe["raw_productive_fields"], fe["raw_paid_jobs"], fe["raw_rank_surplus"]) == (W0, P0, 752), "raw counts") + logN = 10 ** 12 # N = 2^(10^12) + # ell = floor(log_M floor(N/145)); floor(N/145) lies in [2^(logN-8), 2^logN) since 145 < 2^8 + ell_hi = logN // 10 # M = 1024 = 2^10 + need(M_ == 1024 and g_ * ell_hi <= fe["G_depth_upper"] == 2 * 10 ** 11, "height G = g * ell <= 2e11") + need(W0 < 2 ** 14 and W0 + P0 + 1 < 2 ** 17, "W0 < 2^14 and W0 + P0 + 1 < 2^17") + need(17 * fe["G_depth_upper"] + 31 == fe["log2_C_N_strict_upper"] == 3400000000031, "C_N < 2^(17 G + 31)") + need(fe["full_call_centre_episodes_per_raw_unit"] == 18 * 8 and fe["thin_query_episodes_per_raw_unit"] == 15 * 112, + "episodes 144 = 18 * 8 and 1680 = 15 * 112") print(json.dumps({"status": "PASS_PR4535_ARITHMETIC_CHECK", "kappa": str(ka), "uniform_saving": str(us), "mirror_worst": f"{float(worst):.6f}", "binding_margin": str(rows[mn] - ka), "new_kappa_claimed": False}, indent=1))