From 7db8ee8d97d456f120cb534d8cf356a1b8b02ca8 Mon Sep 17 00:00:00 2001 From: pinterbanget Date: Thu, 22 Oct 2026 13:54:06 +0700 Subject: [PATCH] =?UTF-8?q?Certify=20#4535=20at=20a=2013x=20smaller=20fini?= =?UTF-8?q?te=20rank:=20N=20=3D=202^77,014,944,503=20instead=20of=202^10^1?= =?UTF-8?q?2=20(same=20=CE=BA=20=3D=200.003020165)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-Authored-By: Claude Opus 5.5 --- research/pr4535-smaller-rank/.gitattributes | 1 + .../pr4535-smaller-rank/PR4535-RESULT.json | 268 ++++++++++++++++++ research/pr4535-smaller-rank/README.md | 50 ++++ research/pr4535-smaller-rank/SOURCES.json | 18 ++ research/pr4535-smaller-rank/TASK.json | 106 +++++++ research/pr4535-smaller-rank/VERIFY.json | 18 ++ research/pr4535-smaller-rank/verify.py | 143 ++++++++++ 7 files changed, 604 insertions(+) create mode 100644 research/pr4535-smaller-rank/.gitattributes create mode 100644 research/pr4535-smaller-rank/PR4535-RESULT.json create mode 100644 research/pr4535-smaller-rank/README.md create mode 100644 research/pr4535-smaller-rank/SOURCES.json create mode 100644 research/pr4535-smaller-rank/TASK.json create mode 100644 research/pr4535-smaller-rank/VERIFY.json create mode 100644 research/pr4535-smaller-rank/verify.py diff --git a/research/pr4535-smaller-rank/.gitattributes b/research/pr4535-smaller-rank/.gitattributes new file mode 100644 index 0000000000..c1d01eaff4 --- /dev/null +++ b/research/pr4535-smaller-rank/.gitattributes @@ -0,0 +1 @@ +PR4535-RESULT.json -text diff --git a/research/pr4535-smaller-rank/PR4535-RESULT.json b/research/pr4535-smaller-rank/PR4535-RESULT.json new file mode 100644 index 0000000000..1c7af6e350 --- /dev/null +++ b/research/pr4535-smaller-rank/PR4535-RESULT.json @@ -0,0 +1,268 @@ +{ + "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^1000000000000", + "cost_margin_lower": "646/3", + "logA_upper": "11588535078387598648766751054204368156120388952774219/850705917302346158658436518579420528640000000000000", + "log_threshold": 1000000000000, + "margin_evaluation_log_N": 1000000000000, + "margin_lower": "299725246478781048809002279469549139266283611047225781/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": "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-smaller-rank/README.md b/research/pr4535-smaller-rank/README.md new file mode 100644 index 0000000000..1dec76e1da --- /dev/null +++ b/research/pr4535-smaller-rank/README.md @@ -0,0 +1,50 @@ +# A 13× smaller certified finite rank for #4535's critical-root compiler (same κ) + +**Task:** independent-moment. **Base:** canonical main `f626db5c`. **No new κ.** κ = 0.003020165 is unchanged, as are the parameters, the root bracket, the mirror and the outer ledger. + +hexapode's #4535 (head `a6d7237f`) freezes its finite compiler word at `N = 2^(10^12)` and certifies absorption `L(N) < N^z` from #4532's funded majorant `L(n) ≤ A n^θ (c + ln n)^p`. The parameters are `p = 2/5`, `c = 133` and `n0 = 145·1024^650`, with `z − θ_hi = 377/10^12`. Absorption needs only + +```text +ln A + p·ln(c + ln N) < (z − θ_hi)·ln N. +``` + +The left side grows like `ln ln N`. At `ln N ≈ 6.9·10^11` it is about 24 nats, while the right side is about 261. **The rank is therefore about 13× larger, in exponent, than the certificate needs.** + +## Result + +| Quantity | #4535 | This package | +|---|---|---| +| Frozen rank `N` | `2^(10^12)` | **`2^77,014,944,503`** | +| `ln A` bound used | 13.6223, from `(1−θ_lo) ln n0` | **10.2450**, from #4535's own `A = n0^(1−θ)/(c+ln n0)^p` | +| Height envelope `G_depth` | 2·10^11 | **1.540·10^10** | +| Class-count envelope `log₂ C_N` | 3,400,000,000,031 | **261,850,811,331** | + +- **Same `ln A` bound.** With #4535's coarser `ln A` bound, the least certified rank is already `2^90,180,626,561`, an 11.1× smaller exponent. +- **Minimality.** Both ranks are the **least** integers `K` for which the inequality is certified at `N = 2^K`. The verifier also shows that the inequality fails at `K − 1000`, even with the most favourable bounds, so `K` is minimal for these parameters up to 1,000. +- **Larger ranks.** It holds at every larger `N`, because `z − θ_hi > p/(c + ln N)`. +- **Base cutoff.** `N` exceeds `n0`. +- **Consistency.** At `K = 10^12` the margin is 240.17 nats (236.79 with the coarse `ln A`), consistent with #4535 and my #4536. + +**Why it matters.** #4535 freezes the finite word at `N` before the multiplication input grows. Its height, class count, divisible widths (`B_N < C_N^N`), record envelopes and, with them, the eventual input cutoff all grow with `N`. A 13× smaller `log N` shrinks the class-count exponent 13× and the width bound `C_N^N` correspondingly. Nothing physical is materialised or claimed here. + +All logarithms come from my own certified bounds: atanh series with explicit remainders in exact rationals, with `ln 2` enclosed to `10^−50`. #4535's `RESULT.json` is vendored (blob `1c7af6e3`, SHA256-pinned) for the bracket, gap, saving and κ. + +## Verify + +```text +python3 -B research/pr4535-smaller-rank/verify.py +``` + +This runs in about 2 s with the standard library only. + +## Limitations + +- **Scope.** This uses #4535's certificate as given: its root bracket, gap and #4532's funded majorant. It changes only the frozen rank `N`. Physical constants, the outer cutoff and selection are untouched and not claimed. +- **Not re-optimised here.** `p`, `c`, `n0`, `M` and `g` are not retuned. See the open questions. + +## Open next questions + +- **Outer slack `d`.** The gap `z − θ_hi = (1 − θ_hi) − κ − 6d` uses `d = 10^−10`. Halving `d` would raise the gap to `6.77·10^−10`, shrinking `K` by a further 1.8×. This needs a fresh 54-predicate outer replay at the new `(a, b, q, ε, β)`. First step: rerun #4535's outer ledger at `d = 5·10^−11`. +- **Majorant retune.** A smaller `ln A`, via a smaller `n0`, or a smaller `p` needs #4532's tail and funding gates rechecked at `θ`. First step: tabulate the gate margins of #4532's p16 witness against `ℓ0` and `p`. + +Credit: hexapode (#4535); Dillon (#4532); zxv and Jacob Alan Sussman (#4483 compiler and majorant lineage); Cinna Davis (#4470 supplier). Prepared by Ryanson Jonathan with substantial Claude Code (Claude Opus 5.5) assistance. diff --git a/research/pr4535-smaller-rank/SOURCES.json b/research/pr4535-smaller-rank/SOURCES.json new file mode 100644 index 0000000000..a2a5ea8bbd --- /dev/null +++ b/research/pr4535-smaller-rank/SOURCES.json @@ -0,0 +1,18 @@ +{ + "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" + } + ] +} diff --git a/research/pr4535-smaller-rank/TASK.json b/research/pr4535-smaller-rank/TASK.json new file mode 100644 index 0000000000..ac91b23662 --- /dev/null +++ b/research/pr4535-smaller-rank/TASK.json @@ -0,0 +1,106 @@ +{ + "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": "Answers part of the 'funded cutoff' open question of #4532/#4535: the frozen finite word can be built at a 13x smaller rank exponent, shrinking every finite-word envelope.", + "budget_minutes": 40, + "stop_rule": "Stop at the absorption rank with unchanged parameters.", + "outcome": "completed", + "evidence": "Least certified K = 77,014,944,503 (90,180,626,561 with #4535's coarse ln A) vs 10^12; fails at K-1000 even favourably; monotone beyond; envelopes G_depth 1.54e10 and log2 C_N 2.6185e11 vs 2e11 and 3.4e12; own certified logarithms.", + "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": "Does a smaller outer slack d keep all 54 outer predicates and shrink K further?", + "why_it_matters": "Halving d gives a 1.8x smaller K.", + "first_step": "Rerun #4535's outer ledger at d = 5e-11.", + "blocked_by": "None." + }, + { + "question": "Can n0 or p be reduced while #4532's gates still hold at theta?", + "why_it_matters": "ln A and p ln(c+ln N) set K.", + "first_step": "Tabulate #4532 p16 gate margins against ell0 and p.", + "blocked_by": "None." + } + ] +} diff --git a/research/pr4535-smaller-rank/VERIFY.json b/research/pr4535-smaller-rank/VERIFY.json new file mode 100644 index 0000000000..3f1b383257 --- /dev/null +++ b/research/pr4535-smaller-rank/VERIFY.json @@ -0,0 +1,18 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Certified least absorption rank K for #4535's unchanged certificate (both ln A bounds), minimality up to 1000, monotonicity, base cutoff, envelopes at both ranks; binding to vendored #4535 RESULT.json (sha256)." + } + ] +} diff --git a/research/pr4535-smaller-rank/verify.py b/research/pr4535-smaller-rank/verify.py new file mode 100644 index 0000000000..430885de4c --- /dev/null +++ b/research/pr4535-smaller-rank/verify.py @@ -0,0 +1,143 @@ +#!/usr/bin/env python3 +"""A smaller certified finite rank for PR #4535's critical-root compiler, at the same kappa and parameters. + +#4535 (head a6d7237f, vendored RESULT.json, sha256-pinned) freezes its finite compiler word at N = 2^(10^12) and +certifies L(N) < N^z from the funded majorant L(n) <= A n^theta (c + ln n)^p, with p = 2/5, c = 133, +n0 = 145*1024^650, A <= n0^(1-theta_lo), the critical-root bracket [theta_lo, theta_hi] and z = 1 - s_C, +z - theta_hi = 377/10^12. Absorption needs only + + ln A + p ln(c + ln N) < (z - theta_hi) ln N, + +whose left side grows like ln ln N. #4535 bounds ln A by (1 - theta_lo) ln n0; its own definition +A = n0^(1-theta)/(c + ln n0)^p gives a sharper certified bound, and both are used. This verifier, with its own certified logarithms (atanh series with explicit +remainders, exact rationals), finds the least integer K with the inequality certified at N = 2^K, certifies that it +holds at every larger N (the derivative condition z - theta_hi > p/(c + ln N)), and that it fails at K - 1000 even +with the most favourable bounds (so K is minimal for these parameters, up to 1000), recomputes #4535's margin at K = 10^12, and +recomputes the frozen word's height and class-count envelopes at both ranks with #4535's own formulas +(G_depth <= 2 floor(log_1024 floor(N/145)), C_N < 2^(17 G_depth + 31)). Nothing about kappa, the mirror, the root +bracket or the outer ledger changes. +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 +RESULT = HERE / "PR4535-RESULT.json" # #4535 head a6d7237f, research/critical-root-multiplication/RESULT.json, blob 1c7af6e3 +RESULT_SHA256 = "e830f4cab30e70ab02d2ecca283969bd97f3a6925948b61d0eb15df3be831b14" +TERMS = 60 + + +def need(condition, message): + if not condition: + raise AssertionError(message) + + +def atanh_bounds(x): + """Bounds on atanh(x) for rational 0 <= x < 1: partial sum and remainder <= x^(2J+1)/((2J+1)(1-x^2)).""" + 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))) # ln 2 = 2 atanh(1/3) + + +def ln_bounds(y): + """Certified [lo, hi] for ln y, rational y > 0: y = 2^k m with m in [1, 2), ln m = 2 atanh((m-1)/(m+1)).""" + 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): + """Round a rational up to a multiple of 1/den (keeps fractions small).""" + return Fr(-((-v.numerator * den) // v.denominator), den) + + +def main(): + raw = RESULT.read_bytes() + need(hashlib.sha256(raw).hexdigest() == RESULT_SHA256, "vendored #4535 RESULT.json") + res = json.loads(raw) + theta_lo, theta_hi = (Fr(v) for v in res["critical_root"]["critical_root_interval"]) + s_C = Fr(res["uniform_saving"]) + z = 1 - s_C + gap = z - theta_hi + need(gap == Fr(res["absorption"]["positive_gap"]) == Fr(377, 10 ** 12), "z - theta_hi = 377/10^12") + need(Fr(res["kappa"]) == Fr(604033, 200000000), "kappa unchanged") + p, c = Fr(2, 5), 133 + n0 = 145 * 1024 ** 650 + ln_n0 = ln_bounds(n0) + # #4535 bounds ln A by (1 - theta_lo) ln n0, dropping the factor (c + ln n0)^(-p) <= 1. Its own definition + # A = n0^(1-theta)/(c + ln n0)^p gives the sharper certified bound used here; both are reported. + lnA_coarse = coarse((1 - theta_lo) * ln_n0[1]) + need(lnA_coarse <= coarse(Fr(res["absorption"]["logA_upper"])) + Fr(1, 10 ** 20), "coarse ln A agrees with #4535") + lnA_hi = coarse((1 - theta_lo) * ln_n0[1] - p * ln_bounds(c + ln_n0[0])[0]) + need(LN2[1] - LN2[0] < Fr(1, 10 ** 50), "ln 2 enclosure") + + def margin_lo(K, lnA=None): + lnN_lo, lnN_hi = K * LN2[0], K * LN2[1] + return gap * lnN_lo - (lnA_hi if lnA is None else lnA) - p * ln_bounds(c + coarse(lnN_hi))[1] + + def margin_hi(K): # most favourable: smallest A term (A >= n0^(1-theta_hi)/(c + ln n0)^p), lower log bounds + lnN_lo, lnN_hi = K * LN2[0], K * LN2[1] + lnA_lo = (1 - theta_hi) * ln_n0[0] - p * ln_bounds(c + ln_n0[1])[1] + return gap * lnN_hi - lnA_lo - p * ln_bounds(c + K * LN2[0])[0] + + def least(lnA=None): + lo, hi = 1, 10 ** 12 + need(margin_lo(hi, lnA) > 0, "#4535's rank certifies") + while hi - lo > 1: + mid = (lo + hi) // 2 + if margin_lo(mid, lnA) > 0: + hi = mid + else: + lo = mid + need(margin_lo(hi, lnA) > 0 and margin_lo(hi - 1, lnA) <= 0, "least certified K") + return hi + + K_coarse = least(lnA_coarse) + K = least() + # For this certificate (same A, p, c, theta bracket and gap) no materially smaller K can work: below the + # most favourable crossing the inequality fails outright. + K_fail = K - 1000 + need(margin_hi(K_fail) < 0, "the inequality genuinely fails well below K") + # Monotone beyond K: d/dlnN [gap lnN - p ln(c + lnN)] = gap - p/(c + lnN) > 0. + need(gap - p / (c + K * LN2[0]) > 0, "absorption holds at every larger N") + need(K > n0.bit_length() and K_coarse > K, "N above the base cutoff n0") + + def envelopes(K): + # floor(N/145) for N = 2^K has bit length K - 7; log_1024 floor(N/145) < (K - 7)/10 + 1. + G = 2 * ((K - 8) // 10 + 1) + return G, 17 * G + 31 + + G_old, logC_old = envelopes(10 ** 12) + G_new, logC_new = envelopes(K) + need(G_old <= 200000000000 and logC_old <= 3400000000031, "#4535's envelopes reproduced") + report = {"status": "PASS_PR4535_SMALLER_RANK", "kappa": "604033/200000000 (unchanged)", + "least_certified_K_with_4535_coarse_lnA": K_coarse, + "least_certified_K": K, "ratio_10^12_over_K": round(10 ** 12 / K, 3), + "lnA_upper": {"coarse_as_4535": float(lnA_coarse), "exact_formula": float(lnA_hi)}, + "margin_at_K_nats": float(margin_lo(K)), "margin_at_10^12_nats": float(margin_lo(10 ** 12)), + "fails_at_K_minus_1000_even_favourably": True, + "G_depth_bound": {"N=2^10^12": G_old, "N=2^K": G_new}, + "log2_class_envelope": {"N=2^10^12": logC_old, "N=2^K": logC_new}, + "new_kappa_claimed": False} + print(json.dumps(report, indent=1)) + + +if __name__ == "__main__": + sys.exit(main())