diff --git a/research/pr4568-arithmetic-check/.gitattributes b/research/pr4568-arithmetic-check/.gitattributes new file mode 100644 index 0000000000..2e38d3688c --- /dev/null +++ b/research/pr4568-arithmetic-check/.gitattributes @@ -0,0 +1 @@ +PR4568-RESULT.json -text diff --git a/research/pr4568-arithmetic-check/PR4568-RESULT.json b/research/pr4568-arithmetic-check/PR4568-RESULT.json new file mode 100644 index 0000000000..540ffb9516 --- /dev/null +++ b/research/pr4568-arithmetic-check/PR4568-RESULT.json @@ -0,0 +1,271 @@ +{ + "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_evaluation_N": "2^100000000000000", + "cost_margin_lower": "418/15", + "logA_upper": "11588535078387598648766751054204368156120388952774219/850705917302346158658436518579420528640000000000000", + "log_threshold": 100000000000000, + "margin_evaluation_log_N": 100000000000000, + "margin_lower": "62512649175114201706254157498695754664126611047225781/850705917302346158658436518579420528640000000000000", + "margin_scope": "margin_lower is evaluated at log(N)=log_threshold; cost_margin_lower is the conservative certified margin at primary_certified_N. The two margins use different cutoffs.", + "positive_gap": "1/1000000000000", + "primary_certified_N": "2^100000000000000", + "secondary_conservative_N_cutoff": "2^200000000000000" + }, + "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": 20000000000000, + "class_envelope": "C_N <= W0*(W0+P0+1)^(G_depth+1) < 2^340000000000031", + "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": 340000000000031, + "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^100000000000000", + "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": "302016597/100000000000", + "minimum_outer_margin_above_kappa": "2996979834027/1000000000000000000000000", + "outer_checks": 54, + "outer_parameters": { + "a": "1510082987/500000000000", + "b": "120806639/40000000000", + "beta": "999999999997/1000000000000", + "bit_saving": "17/5000", + "complex_uniform_saving": "377520747/125000000000", + "d": "1/1000000000000", + "epsilon": "999999999999/1000000000000", + "kappa": "302016597/100000000000", + "layout": "1/1000000000000", + "q": "3020165973/1000000000000", + "r0": "1/10000000000000", + "stop": "1/1000000000000", + "tested_saving": "3020165977/1000000000000" + }, + "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/critical-root-multiplication/PROOF.md": "870cc213c847175f3717db057539686de638594e8c509b2a2daf8d8e72497102", + "research/critical-root-multiplication/RESULT.json": "e830f4cab30e70ab02d2ecca283969bd97f3a6925948b61d0eb15df3be831b14", + "research/critical-root-multiplication/verify.py": "9604516d64ad845ac0d28423ddeed55a5782b6093f88edc031aeef3e74d8d346", + "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": "377520747/125000000000" +} diff --git a/research/pr4568-arithmetic-check/README.md b/research/pr4568-arithmetic-check/README.md new file mode 100644 index 0000000000..4acef453d0 --- /dev/null +++ b/research/pr4568-arithmetic-check/README.md @@ -0,0 +1,44 @@ +# Independent arithmetic check of #4568 (conditional κ = 0.00302016597) + +**Task:** independent-moment (independent source-bound coverage). **Base:** canonical main `f626db5c`. **No new κ** of my own. + +hexapode's #4568 (head `b269a729`) raises #4535's conditional κ by 9.7·10⁻¹⁰, to **0.00302016597**. It uses my #4564's outer slack `d = 10^−12` together with the unchanged #4470 profile, #4535's critical-root bracket and #4532's majorant. The new outer point is `z = .996979834024`, with `q, a, b = κ + 3d, 4d, 5d`, `s_C = κ + 6d` and tested saving `κ + 7d`. The frozen word is at `N = 2^(10^14)`. #4568's `RESULT.json` is vendored (blob `540ffb95`, SHA256-pinned). + +## Results + +All checked claims are confirmed. + +- **Outer ledger.** I replayed the exact source that #4535 and #4568 pin (`pr4359-p7-padding/.../endpoint.py`, SHA256-checked) at #4568's parameters, which are confirmed to be exactly `κ + jd`. + - All 54 strict predicates, the 4 functional guards and the 9 margins above κ pass. + - The minimum margin is `2996979834027/10^24`, matching #4568's record. +- **Saving order.** `κ < s_C < tested saving = 1 − θ_hi < 1 − θ`. The tested saving equals the bracket endpoint `1 − θ_hi` exactly. It stays strictly below the root's saving only because the certified root lies strictly inside #4535's open bracket, which the bracket certificate guarantees. The absorption gap is `z − θ_hi = 10^−12` exactly. +- **Absorption.** At `N = 2^(10^14)`, my certified margin is 42.94 nats, above #4568's conservative 418/15. The least certified ranks at #4568's κ are: + +| majorant | least `K` (`N = 2^K`) | vs #4568's `10^14` | +|---|---|---| +| #4532 witness, #4568's coarse `ln A` | 37,477,695,815,212 | 2.67× smaller | +| #4532 witness, `A`'s own definition | 32,523,485,165,724 | 3.07× smaller | +| **my #4565 retuned witness** (`M = 2^24`, `ℓ0 = 64`, `p = 3/10`, `c = 101`) | **14,562,291,820,122** | **6.87× smaller** | + +So #4568's frozen word can be built at a rank exponent at least 6.9× smaller, at the same κ, by combining it with #4565. Each `K` is the least certified one, and the inequality holds monotonically beyond it. + +I also replayed #4568's registered package: `PASS_REGISTERED_RESEARCH_PACKAGE research/critical-slack-multiplication outcome=completed` in 8.4 s. + +## Verify + +```text +python3 -B research/pr4568-arithmetic-check/verify.py +``` + +This runs in about 3 s with the standard library only. + +## Limitations + +- **Not covered.** The critical-root bracket, mirror and #4532 gates are #4535's and are not recomputed here; my #4536 and #4569 cover them. Native, physical and outer-cutoff premises are out of scope, as in #4568. +- **Admission.** Whether a κ gain obtained by retuning outer slack against the same raw root counts as a hill-climb step is a maintainer decision. Per #4568 itself, the native paid profile and raw root are unchanged. This package takes no position. + +## Open next questions + +- None new from the arithmetic. Whether a slack-retuned κ is admitted is for the maintainers. + +Credit: hexapode (#4568, #4535), Dillon (#4532), Cinna Davis (#4470), zxv and Jacob Alan Sussman. Prepared by Ryanson Jonathan with substantial Claude Code (Claude Opus 5.5) assistance. diff --git a/research/pr4568-arithmetic-check/SOURCES.json b/research/pr4568-arithmetic-check/SOURCES.json new file mode 100644 index 0000000000..b58b96ca8e --- /dev/null +++ b/research/pr4568-arithmetic-check/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "f626db5c3a3d781d8f7695038776c621651f75e1", + "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" + }, + { + "path": "research/pr4359-p7-padding/dependencies/compiler-refill/endpoint.py", + "usage": "input", + "git_blob": "340e1f0ffb8a1a9c38fbbd9119580b6d23e01b59", + "sha256": "d097e55f06c3f244f2074ffd7c1a0a5f3c4b4b6a6accf9619d1dde5c0ae85e15" + } + ] +} diff --git a/research/pr4568-arithmetic-check/TASK.json b/research/pr4568-arithmetic-check/TASK.json new file mode 100644 index 0000000000..86a0b9f693 --- /dev/null +++ b/research/pr4568-arithmetic-check/TASK.json @@ -0,0 +1,100 @@ +{ + "schema_version": 1, + "task_id": "independent-moment", + "priority_revision": 7, + "base_commit": "f626db5c3a3d781d8f7695038776c621651f75e1", + "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": "unchanged", + "actual_scope": "Does a new paid-profile or mixture-ceiling claim have independent source-bound coverage of its actual changed ledger?", + "scope_change_reason": null, + "bottleneck_link": "Independent arithmetic coverage of the newest open conditional kappa (#4568), plus a 6.9x smaller certified frozen rank at that kappa via #4565.", + "budget_minutes": 30, + "stop_rule": "Stop at #4568's arithmetic.", + "outcome": "completed", + "evidence": "Pinned outer ledger at #4568's exact kappa+jd parameters: 54/4/9 pass, recorded minimum margin reproduced; saving order and gap 1e-12 exact; certified absorption margin 42.94 nats at 2^(10^14); least certified K 3.75e13 / 3.25e13 / 1.456e13 (retuned); #4568 package replays.", + "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": "None new; maintainers to decide admission of slack-retuned kappa.", + "why_it_matters": "Hill-climb rules distinguish profile changes from root digits.", + "first_step": "Maintainer review.", + "blocked_by": "Maintainer decision." + } + ] +} diff --git a/research/pr4568-arithmetic-check/VERIFY.json b/research/pr4568-arithmetic-check/VERIFY.json new file mode 100644 index 0000000000..6be2eb2078 --- /dev/null +++ b/research/pr4568-arithmetic-check/VERIFY.json @@ -0,0 +1,21 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/compact-joint-compiler/arithmetic/RESULT.json", + "research/pr4359-p7-padding/dependencies/compiler-refill/endpoint.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Pinned outer ledger at #4568's parameters (54 predicates, guards, margins, recorded minimum); saving order and gap; certified absorption margin and least ranks for three majorants; binding to vendored #4568 RESULT.json." + } + ] +} diff --git a/research/pr4568-arithmetic-check/verify.py b/research/pr4568-arithmetic-check/verify.py new file mode 100644 index 0000000000..d41d70b075 --- /dev/null +++ b/research/pr4568-arithmetic-check/verify.py @@ -0,0 +1,137 @@ +#!/usr/bin/env python3 +"""Independent arithmetic check of PR #4568 (hexapode): conditional kappa = 0.00302016597 (+9.7e-10 over #4535). + +#4568 (head b269a729; RESULT.json vendored, sha256-pinned) keeps #4535's native profile, critical-root bracket and +#4532 majorant, and moves the outer point to d = 10^-12 with z = .996979834024, kappa = .00302016597, q, a, b = +kappa + 3d, 4d, 5d, tested saving kappa + 7d and complex uniform saving s_C = 1 - z = kappa + 6d. This verifier: + * replays the outer ledger source that #4535/#4568 pin (research/pr4359-p7-padding/dependencies/compiler-refill/ + endpoint.py, sha256-checked) with the ordinary BIT admission (research/compact-joint-compiler/arithmetic/RESULT.json) + at #4568's exact parameters: 54 strict predicates, 4 functional guards, 9 margins above kappa, the recorded minimum + margin and the full outer_parameters encoding; + * checks the saving order kappa < s_C < tested saving < 1 - theta (theta in #4535's bracket, open at theta_hi) and + the absorption gap z - theta_hi = 10^-12 exactly; + * with own certified logarithms, checks absorption at #4568's N = 2^(10^14) and finds the least certified rank K for + (i) #4532's p16 witness with #4568's coarse ln A, (ii) the same witness with A's own definition, and (iii) my #4565 + retuned witness (M = 2^24, ell0 = 64, p = 3/10, c = 101), monotone beyond K. +Ryanson Jonathan with Claude Code (Claude Opus 5.5) assistance. Apache-2.0. +""" +from fractions import Fraction as Fr +import hashlib +import json +from pathlib import Path +import sys + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +LEDGER = ROOT / "research/pr4359-p7-padding/dependencies/compiler-refill/endpoint.py" +LEDGER_SHA256 = "d097e55f06c3f244f2074ffd7c1a0a5f3c4b4b6a6accf9619d1dde5c0ae85e15" +COMPILER = ROOT / "research/compact-joint-compiler/arithmetic/RESULT.json" +COMPILER_SHA256 = "a6caaa2a6d6460a8c1ef7e48c4853bb27976be33a52b96a4216dfa90d96c9091" +RESULT = HERE / "PR4568-RESULT.json" # #4568 head b269a729, research/critical-slack-multiplication/RESULT.json, blob 540ffb95 +RESULT_SHA256 = "b55c34dd733ed09472c487ea21df1f7c102c3427bcb05222e60b218242715abb" +THETA = (Fr(9969798340229, 10 ** 13), Fr(996979834023, 10 ** 12)) # #4535's isolated root bracket +TERMS = 60 + + +def need(condition, message): + if not condition: + raise AssertionError(message) + + +def atanh_bounds(x): + s, p = Fr(0), x + for j in range(TERMS): + s += p / (2 * j + 1) + p *= x * x + return s, s + p / ((2 * TERMS + 1) * (1 - x * x)) + + +LN2 = tuple(2 * v for v in atanh_bounds(Fr(1, 3))) + + +def ln_bounds(y): + y = Fr(y) + k = y.numerator.bit_length() - y.denominator.bit_length() + m = y / Fr(2) ** k + while m >= 2: + m /= 2 + k += 1 + while m < 1: + m *= 2 + k -= 1 + lo, hi = atanh_bounds((m - 1) / (m + 1)) + lo, hi = 2 * lo, 2 * hi + return (k * LN2[0] + lo, k * LN2[1] + hi) if k >= 0 else (k * LN2[1] + lo, k * LN2[0] + hi) + + +def coarse(v, den=10 ** 30): + return Fr(-((-v.numerator * den) // v.denominator), den) + + + +def least_rank(lnA, p, c, gap, K_max=10 ** 15): + def margin(K): + return gap * K * LN2[0] - lnA - p * ln_bounds(c + coarse(K * LN2[1]))[1] + + lo, hi = 1, K_max + need(margin(hi) > 0, "certifies at K_max") + while hi - lo > 1: + mid = (lo + hi) // 2 + lo, hi = (lo, mid) if margin(mid) > 0 else (mid, hi) + need(margin(hi) > 0 and margin(hi - 1) <= 0, "least certified K") + need(gap - p / (c + hi * LN2[0]) > 0, "monotone beyond K") + return hi, margin + + +def main(): + raw = RESULT.read_bytes() + need(hashlib.sha256(raw).hexdigest() == RESULT_SHA256, "vendored #4568 RESULT.json") + res = json.loads(raw) + ledger_raw = LEDGER.read_bytes() + need(hashlib.sha256(ledger_raw).hexdigest() == LEDGER_SHA256, "pinned outer ledger") + ns = {"__file__": str(LEDGER), "__name__": "outer_exact"} + exec(compile(ledger_raw, str(LEDGER), "exec"), ns) + comp_raw = COMPILER.read_bytes() + need(hashlib.sha256(comp_raw).hexdigest() == COMPILER_SHA256, "pinned compiler result") + comp = json.loads(comp_raw) + k = Fr(res["kappa"]) + d = Fr(1, 10 ** 12) + need(k == Fr("0.00302016597"), "kappa") + a = {"kappa": k, "tested_saving": k + 7 * d, "complex_uniform_saving": k + 6 * d, "b": k + 5 * d, "a": k + 4 * d, + "q": k + 3 * d, "bit_saving": Fr(comp["ordinary_BIT"]["admitted"]), "epsilon": 1 - d, "beta": 1 - 3 * d, + "r0": d / 10, "stop": d, "layout": d, "d": d} + need(ns["encode"](a) == res["outer_parameters"], "outer parameters are kappa + jd at d = 1e-12") + out = ns["ledger"](a) + out["functional_checks"]["actual_new_BIT_stock_sublinear"] = a["beta"] * (1 - Fr(comp["ordinary_BIT"]["atom"])) + need(len(out["strict_checks"]) == 54 and all(v > 0 for v in out["strict_checks"].values()), "54 strict predicates") + need(len(out["functional_checks"]) == 4 and all(v > 0 for v in out["functional_checks"].values()), "4 guards") + need(len(out["margins"]) == 9 and all(v > k for v in out["margins"].values()), "9 margins above kappa") + min_margin = min(out["margins"].values()) - k + need(min_margin == Fr(res["minimum_outer_margin_above_kappa"]), "recorded minimum outer margin") + s_C, tested = a["complex_uniform_saving"], a["tested_saving"] + need(s_C == Fr(res["uniform_saving"]), "uniform saving") + need(k < s_C < tested == 1 - THETA[1] < 1 - THETA[0], "saving order (the root theta < theta_hi strictly)") + z = 1 - s_C + gap = z - THETA[1] + need(gap == Fr(1, 10 ** 12), "absorption gap 1e-12") + ln_n0 = ln_bounds(145 * 1024 ** 650) + lnA_coarse = coarse((1 - THETA[0]) * ln_n0[1]) + need(lnA_coarse <= coarse(Fr(res["absorption"]["logA_upper"])) + Fr(1, 10 ** 20), "coarse ln A as #4568") + lnA_exact = coarse((1 - THETA[0]) * ln_n0[1] - Fr(2, 5) * ln_bounds(133 + ln_n0[0])[0]) + ln_n0r = ln_bounds(145 * (1 << 24) ** 64) + lnA_retuned = coarse((1 - THETA[0]) * ln_n0r[1] - Fr(3, 10) * ln_bounds(101 + ln_n0r[0])[0]) + K1, margin1 = least_rank(lnA_coarse, Fr(2, 5), 133, gap) + K2, _ = least_rank(lnA_exact, Fr(2, 5), 133, gap) + K3, _ = least_rank(lnA_retuned, Fr(3, 10), 101, gap) + m_at = margin1(10 ** 14) + need(m_at > Fr(418, 15), "absorption margin at N = 2^(10^14) exceeds #4568's certified 418/15") + report = {"status": "PASS_PR4568_ARITHMETIC_CHECK", "kappa": str(k), + "outer": {"strict": 54, "guards": 4, "margins": 9, "min_margin_above_kappa": str(min_margin)}, + "absorption_gap": str(gap), "margin_at_N=2^10^14_nats": float(m_at), + "least_K": {"4532_witness_coarse_lnA": K1, "4532_witness_exact_A": K2, "4565_retuned": K3}, + "rank_exponent_ratio_10^14_over_retuned": round(10 ** 14 / K3, 2), "new_kappa_claimed": False} + print(json.dumps(report, indent=1)) + + +if __name__ == "__main__": + sys.exit(main())