Skip to content
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
12 changes: 12 additions & 0 deletions research/fine-prime-root160/CLAIM.json
Original file line number Diff line number Diff line change
@@ -0,0 +1,12 @@
{
"status": "VERIFIED_CONDITIONAL_FINITE_ADMISSION",
"kappa": "839877478062772260667835496960351288499155719251290147730163760081432274130162819413152828066422316137225658454293110486035224060082706071385650318346478357849999999999999999998998320245043374455478664329006079297423/500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
"kappa_decimal": "0.001679754956125544521335670993920702576998311438502580295460327520162864548260325638826305656132844632274451316908586220972070448120165412142771300636692956715699999999999999999997996640490086748910957328658012158594846",
"previous_pr": 1839,
"previous_head": "836ef6a1a550f439e42be65423cffd624658af6a",
"previous_kappa": "8398774780627722606678354969603512884991557192512901477301637600814322741301628194131524999999998998320245043374455478664329006079297/5000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
"gain": "328066422416305201154116847562619602323452153006071385650318346478357849999999999999999998998320245043374455478664329006079297423/500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
"gain_decimal": "6.56132844832610402308233695125239204646904306012142771300636692956715699999999999999999997996640490086748910957328658012158594846E-91",
"scope": "Conditional on all inherited PR1800/1786/1758/1673 compiler, common-label/mutable-source, hosting, semantic online precision C1=1, fixed-tape/prime-packing, interchange, recovery and analytic assumptions, plus the cited Trudgian prime theorem. Finite arithmetic does not establish the written all-size prime/precision/locality or accretive-circuit arguments. No unconditional theorem, practical cutoff, independent human review or maintainer acceptance is claimed.",
"verification_receipt": "evidence/FULL-RESULT.json"
}
383 changes: 383 additions & 0 deletions research/fine-prime-root160/DEPENDENCY-MANIFEST.json

Large diffs are not rendered by default.

8 changes: 8 additions & 0 deletions research/fine-prime-root160/DEPENDENCY.json
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
{
"pr": 1800,
"head": "46d865ab92e58098538b8c5348b6a131c99abf45",
"repository": "jeremykothe2/integer-mult-bounds",
"package": "research/capped-fusion-t74-k554",
"manifest_sha256": "b8dba5524f8603e1848c73a8dd675404a0d3d9eed3b0285e9f0cfccde38fd15f",
"scope": "Unchanged supplier and analytic construction; refine positive free slack parameters only."
}
17 changes: 17 additions & 0 deletions research/fine-prime-root160/ENDPOINT.json
Original file line number Diff line number Diff line change
@@ -0,0 +1,17 @@
{
"lower": "16797549561255445213356709939207025769983114385025802954603275201628645482603256388263056561328446322744513169085862209720704481201654121427713006366929567157/10000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
"upper": "8398774780627722606678354969603512884991557192512901477301637600814322741301628194131528280664223161372256584542931104860352240600827060713856503183464783579/5000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
"grid_digits": 160,
"source_endpoint": "4199387390313861303339177484801756442495778596256450738650818800407/2500000000000000000000000000000000000000000000000000000000000000000000",
"profile": {
"1": 1560432,
"2": 336336,
"3": 278724,
"4": 84912,
"5": 54612,
"8": 5328,
"48": 22748
},
"m": 73,
"live": 66304
}
37 changes: 37 additions & 0 deletions research/fine-prime-root160/MANIFEST.json
Original file line number Diff line number Diff line change
@@ -0,0 +1,37 @@
{
"CLAIM.json": "dce0ef1b5313632e9ccb241f1213752461a29a69e957a8fc3690ba7006b5fd60",
"DEPENDENCY-MANIFEST.json": "b8dba5524f8603e1848c73a8dd675404a0d3d9eed3b0285e9f0cfccde38fd15f",
"DEPENDENCY.json": "57b6fe18ea819cca8860e65b1f9d7de83438dd3f1a309661ea5aad6932ef8213",
"ENDPOINT.json": "0d856fe6025bab483009716ba8a1702437b4c51e87ce69b487dc01ec720e8802",
"MATH-BINDING.json": "62387bb60f7d5801c0e0e7570e5bb199ad6f77b60e434e4fb51d47d796579373",
"NOTICE": "e71adf89004057245bb473b955ba4936d821fa84af06c3e689fb0f7390893ca8",
"PARAMETERS.json": "d50de1b4aacb682f03ca5f061722a99830f8e96644931df4edc6cfee42c79bce",
"PROOF.md": "4a7523d2152cb7eb0b6edf7cca8d49afc10817fcfd4c4f0578a481c8864a2872",
"README.md": "3b81889e53de65062f6ddf4b2e4eec8fbf69894e04983b6e4100649472dd5f2e",
"RELEASE-BINDING.json": "a1e09aca4a2bb5a036ab95156b9612a99670c8865d7157780a0fb9d664253843",
"certify_endpoint.py": "22980cd3aacdf96cddbbbe2b93d42c07ec91d169977c6129624f5ec9f274ea17",
"check_ledger.py": "8bc0d4f4bae9b8f600cdef06e0dbb0854be7c09320d5c9695f049fefb8c72c73",
"evidence/ARITHMETIC-RESULT.json": "81d7b14c352a574cd40f04191480bdd5f172f889b712bd07179f987dda9f5080",
"evidence/ARITHMETIC-STAGES.json": "fa481d7c95faa18ec01347cdc546981733e46f96170c25f73014edf7396d96ad",
"evidence/ENDPOINT-REPLAY.json": "91a200b87c6001ea13e5df8bafa07c2231cdc0bcc9dbfdc90f5858597347b6b7",
"evidence/FULL-RESULT.json": "c7aa5698dbbf2ae9fc7f73fe9169a213d863d7221826c6997f1ea7d7150a3b60",
"evidence/FULL-STAGES.json": "2eb8dc4180489cfc4511cdff1ec7579d38a8623222e1f1b7a66c7f4576698aaf",
"evidence/INDEPENDENT.json": "030a8fec46ae0b6118a2ab2edb9f5a43e26c85a578f0d2b05ebd5388e0c9c11c",
"evidence/LEDGER.json": "cab2db1d5dcd75daed32c924726b969608991c4c915434b88f7c50e87781af8f",
"evidence/SUPPLIER-RESULT.json": "3c56933877227901b38df4570f5edafd69972024faa9a68aa1cbd20e5e3f5cbf",
"evidence/SUPPLIER-STAGES.json": "ca8f78413d6222b055de3783ce23dd77ea502c93ec6c962e6d353f9acdf402ba",
"evidence/VERIFIED-SOURCE-MANIFEST.json": "6868006d3acded8df5d6e0be42695302f36b268c226d1b6657667ff8ac90bb1b",
"independent_check.py": "9434771a3f73ebb7a58e7bf162aba2eef05e380ebd6a40a2f67273a32df4c9ee",
"inputs/B.json": "2ba272fe3036774ea32a9cbab76a96c7cbb0bee4595b03898e44b496373a9f6a",
"inputs/CLAIM1800.json": "1dd5490597ead36a31634f6008b1cd5ce0b51c4acd48a541b13306212e3f52f1",
"inputs/LEADER1839.json": "1cc459f3c79046a2dc025f7e004958d178b886a3b541d64d886e4628f77fc252",
"inputs/OUTER-CLAIM1800.json": "c10ff0673ee9152d2efee792fb3532ca25a5edee0bf52c5b700bf86735752779",
"inputs/SOURCE-SPEC.json": "41d7bd51c18eb354c6a785780ddefd35b3a8e2513daa2c4f585b236b7173e943",
"inputs/SPEC.json": "985ddc29fcd43663b1099a6a7129b50e555c5feee183deb775a308bb62ec7e18",
"reference/check_ledger.py": "58162da8e9e7c02de50a9e63649c05ddc4fc5026b7f9173c9058018d093b9603",
"reference/fine_mercator.py": "c0bbb95baff4f301413778c6c595049a0f3fca4ca2cdc86351898137c53e1658",
"reference/fine_moment.py": "feaf1d3b6bf0e3b8eaeb22c40bea3a04ca63a98c08534fa5c28ae913c8ed70c2",
"reference/independent_check.py": "791c0bd5b1b634e20952914c8946bd8402415f4b1163ed83e94e7881fb657a5e",
"replay_outer.py": "f3bef0ca5139984faf357861283f7ed914f236d5a31b9f0dfcf88dcd93183026",
"verify.py": "e38c9f73316847a0b8700086d79d473ad4cff1e779dfed72bf50d3d3072a9c1f"
}
24 changes: 24 additions & 0 deletions research/fine-prime-root160/MATH-BINDING.json
Original file line number Diff line number Diff line change
@@ -0,0 +1,24 @@
{
"kappa": "839877478062772260667835496960351288499155719251290147730163760081432274130162819413152828066422316137225658454293110486035224060082706071385650318346478357849999999999999999998998320245043374455478664329006079297423/500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
"sha256": {
"DEPENDENCY-MANIFEST.json": "b8dba5524f8603e1848c73a8dd675404a0d3d9eed3b0285e9f0cfccde38fd15f",
"DEPENDENCY.json": "57b6fe18ea819cca8860e65b1f9d7de83438dd3f1a309661ea5aad6932ef8213",
"ENDPOINT.json": "0d856fe6025bab483009716ba8a1702437b4c51e87ce69b487dc01ec720e8802",
"PARAMETERS.json": "d50de1b4aacb682f03ca5f061722a99830f8e96644931df4edc6cfee42c79bce",
"certify_endpoint.py": "22980cd3aacdf96cddbbbe2b93d42c07ec91d169977c6129624f5ec9f274ea17",
"check_ledger.py": "8bc0d4f4bae9b8f600cdef06e0dbb0854be7c09320d5c9695f049fefb8c72c73",
"independent_check.py": "9434771a3f73ebb7a58e7bf162aba2eef05e380ebd6a40a2f67273a32df4c9ee",
"inputs/B.json": "2ba272fe3036774ea32a9cbab76a96c7cbb0bee4595b03898e44b496373a9f6a",
"inputs/CLAIM1800.json": "1dd5490597ead36a31634f6008b1cd5ce0b51c4acd48a541b13306212e3f52f1",
"inputs/LEADER1839.json": "1cc459f3c79046a2dc025f7e004958d178b886a3b541d64d886e4628f77fc252",
"inputs/OUTER-CLAIM1800.json": "c10ff0673ee9152d2efee792fb3532ca25a5edee0bf52c5b700bf86735752779",
"inputs/SOURCE-SPEC.json": "41d7bd51c18eb354c6a785780ddefd35b3a8e2513daa2c4f585b236b7173e943",
"inputs/SPEC.json": "985ddc29fcd43663b1099a6a7129b50e555c5feee183deb775a308bb62ec7e18",
"reference/check_ledger.py": "58162da8e9e7c02de50a9e63649c05ddc4fc5026b7f9173c9058018d093b9603",
"reference/fine_mercator.py": "c0bbb95baff4f301413778c6c595049a0f3fca4ca2cdc86351898137c53e1658",
"reference/fine_moment.py": "feaf1d3b6bf0e3b8eaeb22c40bea3a04ca63a98c08534fa5c28ae913c8ed70c2",
"reference/independent_check.py": "791c0bd5b1b634e20952914c8946bd8402415f4b1163ed83e94e7881fb657a5e",
"replay_outer.py": "f3bef0ca5139984faf357861283f7ed914f236d5a31b9f0dfcf88dcd93183026",
"verify.py": "e38c9f73316847a0b8700086d79d473ad4cff1e779dfed72bf50d3d3072a9c1f"
}
}
10 changes: 10 additions & 0 deletions research/fine-prime-root160/NOTICE
Original file line number Diff line number Diff line change
@@ -0,0 +1,10 @@
New research prepared by Rohan Arun with substantial OpenAI Codex assistance. Apache-2.0. Parent words and build recipe method derive from Jeremy Kothe PR1274 and Rohan Arun PR1218, with lineage credited in README.md. All inherited mathematical qualifications are retained.
Additional pivot555 and567 composition by Rohan Arun with substantial OpenAI Codex assistance.

T74 exact-fill owner construction by Rohan Arun with substantial OpenAI Codex assistance.

PR1377 grid refinement credited to Jeremy Kothe. Outer witness refinement by Rohan Arun with OpenAI Codex assistance; construction unchanged.

Pivot-566 kernel, words, edits, rebuild.py and rebind.py: PR1625 (mdumitrean). Endpoint/outer-witness stacking, fine_cache.py and oracle stage by jeremykothe2 with oh-my-pi assistance.

This refinement also credits Jeremy Kothe and PR1839 contributors for the finer endpoint recertification, and Rohan Arun PR1828 for parameterized positive-slack replay. Original retained enclosure engines and predecessor files are unchanged in reference/. New endpoint, parameters, binding checker and documentation prepared by Rohan Arun with substantial OpenAI Codex assistance. No independent human review is claimed.
13 changes: 13 additions & 0 deletions research/fine-prime-root160/PARAMETERS.json
Original file line number Diff line number Diff line change
@@ -0,0 +1,13 @@
{
"root_digits": 160,
"slack_digits": 180,
"zeta_digits": 182,
"stop_digits": 186,
"backoff_digits": 192,
"kappa_grid_digits": 220,
"moment_grid_digits": 240,
"log_terms": 280,
"exp_terms": 100,
"mercator_bits": 1024,
"mercator_log_terms": 1024
}
11 changes: 11 additions & 0 deletions research/fine-prime-root160/PROOF.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,11 @@
# Finer endpoint with fixed positive slacks

The physical supplier and paid rank profile are unchanged from PR1800 at its pinned head. This package re-certifies that profile's moment root on a 10^-160 rational grid. The input source specification is preserved byte for byte as inputs/SOURCE-SPEC.json. The derived SPEC differs only in expected.complex_lower. Both retained enclosure algorithms independently prove M(B)<1<M(B+10^-160), with outward rounding and explicit tails. M is strictly increasing because every child rank lies strictly between zero and the parent dimension. No floating-point root finder is used by verification.

Write h=10^-180, b=B-h, q=B-2h, a=B-3h/2, delta=2h, epsilon=1-delta, beta=1-3delta, r0=slack=h, stop=10^-186 and zeta=10^-182. As in PR1800 and PR1828, c=3/32 and xi=epsilon*(1+q)-c+slack. The source-axis absorption gap is delta-r0=h>0; the membership gap is delta>0; the Gaussian gap is delta*(1-2q)>0; the effective-router gap is h/2>0. The stopping condition stop*b<h/2 is checked exactly. The remaining inherited inequalities and nine cost powers are regenerated as exact rationals with 17 rejecting controls.

K=floor(epsilon*q*10^220)/10^220-10^-192. Both independently implemented balance calculations must agree on this exact rational. K must strictly exceed the exact PR1839 rational pinned in inputs/LEADER1839.json. Decimal displays play no role in comparison.

The full replay checks the immutable PR1800 dependency, all inherited outer replays and complete supplier admission. The actual assembly must match the preserved original specification and exactly the re-certified profile, dimension, live count and bit endpoint. The endpoint certificate binds that same profile to the new derived specification; it does not rely on changing an old receipt's number. The original native admission's lower endpoint is a weaker valid endpoint, not an upper ceiling.

All slacks are fixed positive constants. The predecessor's eventual polynomial and polylogarithmic absorption arguments therefore transfer with a potentially larger unspecified cutoff if those written arguments are valid. No limit point epsilon=1, uniform cutoff as h tends to zero, new physical supplier, or practical speedup is claimed. All inherited compiler, hosting, online precision, fixed-tape, source-prime, locality, recovery, interchange and analytic hypotheses remain. Finite replay does not prove those all-size hypotheses.
21 changes: 21 additions & 0 deletions research/fine-prime-root160/README.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,21 @@
Locally verified conditional arithmetic refinement of [PR #1839](https://github.com/CrocSwap/integer-mult-bounds/pull/1839) at `836ef6a1a550f439e42be65423cffd624658af6a`.

**Kappa:** `0.001679754956125544521335670993920702576998311438502580295460327520162864548260325638826305656132844632274451316908586220972070448120165412142771300636692956715699999999999999999997996640490086748910957328658012158594846`.

**Exact gain:** `6.56132844832610402308233695125239204646904306012142771300636692956715699999999999999999997996640490086748910957328658012158594846E-91`. This is an extremely small numerical improvement of the same conditional construction. The physical supplier and paid profile are unchanged; no practical speedup or new construction is claimed.

The supplier moment is enclosed on a 10^-160 grid by two independently implemented rational algorithms. Positive slacks use h=10^-180, epsilon=1-2h and beta=1-6h. The endpoint upper neighbour is rejected, and the two ledger calculations must agree on the exact candidate. Arithmetic replay passed: both endpoint enclosures, 57 strict rational inequalities, 17 rejecting controls, and the separate nine-cost balance derivation agree. Full finite replay passed locally, including fresh native supplier admission. No hosted CI pass is claimed.

Reproduce arithmetic: `PYTHONINTMAXSTRDIGITS=0 python3 -B research/fine-prime-root160/verify.py --work /absolute/new/work --arithmetic-only`.

For full replay, omit `--arithmetic-only`. The immutable 381-file PR1800 dependency is fetched and checked, or supplied with `--dependency`. The actual assembly profile is bound to the new two-engine certificate; the old supplier admission endpoint is retained as a weaker valid value. All outputs stay under the explicit work directory. Full replay receipts and the exact source manifest are included in evidence/.

Conditional on all inherited PR1800/1786/1758/1673 compiler, common-label/mutable-source, hosting, semantic online precision C1=1, fixed-tape/prime-packing, interchange, recovery and analytic assumptions, plus the cited Trudgian prime theorem. Finite arithmetic does not establish the written all-size prime/precision/locality or accretive-circuit arguments. No unconditional theorem, practical cutoff, independent human review or maintainer acceptance is claimed.

Credits: Jeremy Kothe and contributors, PR1839 endpoint refinement and PR1800 composition; Rohan Arun PR1828 slack replay; Chafik Boukhalfa / chafreaky PR1786 and Tim Trudgian's prime theorem; Vlado Vojdanovski PR1673; PR1758 contributors, LeverRank, mdumitrean, midhatn, and all retained PR1319/1297 supplier authors. Full predecessor notices and original checker sources are preserved. Prepared by Rohan Arun with substantial OpenAI Codex assistance. Apache-2.0; no independent human review claimed.


Concurrent comparison: PR #1875 at `5b06a3fd5f80a6ca3d62f28e04cd650897a5b47a` reports a higher 300-digit candidate, approximately 3.49625273906229277168487776095E-161 above this PR. Its body reports arithmetic passes with full native replay pending. This PR is a locally verified refinement over PR1839 and does not claim the current lead.


Local verification result: `PASS_CONDITIONAL_SLACK_REFINEMENT_FINITE_ADMISSION`. The fresh replay passed both exact endpoint engines, the 57 strict inequalities and 17 rejecting controls, the independent balance calculation, inherited outer checks, the native supplier and strict T74 admission, and the final assembly-to-ledger bindings. The release changes only status metadata and documentation and adds receipts; all mathematical inputs, parameters and verifier code remain byte-identical to the replayed source. Hosted CI remains separate.
11 changes: 11 additions & 0 deletions research/fine-prime-root160/RELEASE-BINDING.json
Original file line number Diff line number Diff line change
@@ -0,0 +1,11 @@
{
"replayed_manifest": "6868006d3acded8df5d6e0be42695302f36b268c226d1b6657667ff8ac90bb1b",
"replayed_head": "da74579387c2511dc2ca98c05aa7133c8e7f9956",
"changed_existing_files": [
"CLAIM.json",
"README.md"
],
"unchanged_code_parameters_inputs": true,
"full_receipt_sha256": "c7aa5698dbbf2ae9fc7f73fe9169a213d863d7221826c6997f1ea7d7150a3b60",
"scope": "Only status metadata and documentation changed after replay; evidence added. Exact claim and hypotheses unchanged."
}
25 changes: 25 additions & 0 deletions research/fine-prime-root160/certify_endpoint.py
Original file line number Diff line number Diff line change
@@ -0,0 +1,25 @@
"""Exact outward-rounded moment bracket using two retained algorithms.
The proposed endpoint is data. No floating point or root finder runs here.
"""
from pathlib import Path
from fractions import Fraction as Q
from functools import lru_cache
import json,sys,hashlib,importlib.util,copy
P=Path(__file__).resolve().parent
if not __debug__:raise RuntimeError('Assertions required')
def read(n):return json.loads((P/n).read_text())
def load(name):
s=importlib.util.spec_from_file_location(name,P/'reference'/(name+'.py'));m=importlib.util.module_from_spec(s);s.loader.exec_module(m);return m
param=read('PARAMETERS.json');ep=read('ENDPOINT.json');source=read('inputs/SOURCE-SPEC.json');derived=read('inputs/SPEC.json');expected=copy.deepcopy(source);expected['expected']['complex_lower']=ep['lower'];assert derived==expected
H={int(k):int(v)for k,v in source['expected']['global_profile'].items()};m=source['geometry']['dimension'];W=source['expected']['live'];lo,hi=Q(ep['lower']),Q(ep['upper'])
assert ep['profile']=={str(k):v for k,v in H.items()}and ep['m']==m and ep['live']==W
assert 0<Q(source['expected']['complex_lower'])<lo<hi and hi-lo==Q(1,10**param['root_digits'])
A=load('fine_mercator');B=load('fine_moment');A.DYAD=1<<param['mercator_bits'];A.LOGN=param['mercator_log_terms']+1;A.EXPN=param['exp_terms'];B.GRID=10**param['moment_grid_digits'];B.LOG_TERMS=param['log_terms'];B.EXP_TERMS=param['exp_terms'];B.log_bounds=lru_cache(None)(B.log_bounds)
assert (A.LOGN-1)%2==0
rows={}
for name,fn in [('alternating_mercator',lambda x:A.moment(H,m,W,x)),('base_two_atanh',lambda x:B.moment(m,W,list(H.items()),x))]:
l,u=fn(lo);rl,ru=fn(hi);assert 0<l<=u<1<rl<=ru
rows[name]=dict(lower_endpoint_interval=[str(l),str(u)],upper_endpoint_interval=[str(rl),str(ru)],acceptance_margin=str(1-u),upper_rejection_margin=str(rl-1))
leader=read('inputs/LEADER1839.json');assert Q(leader['kappa_rational'])<lo
result=dict(status='PASS_TWO_ENGINE_ENDPOINT_BRACKET',lower=str(lo),upper=str(hi),engines=rows,profile=H,m=m,live=W,monotonicity='Every positive child term (n*r/(m*W))*(m/r)^b is strictly increasing in b because 0<r<m. The accepted lower and rejected upper therefore enclose the same unique positive moment root.',scope='Exact finite moment recertification of the unchanged supplier profile; full native admission and all inherited theorem hypotheses are separate.',source_hashes={f:hashlib.sha256((P/f).read_bytes()).hexdigest()for f in ['inputs/SOURCE-SPEC.json','inputs/SPEC.json','PARAMETERS.json','ENDPOINT.json','reference/fine_mercator.py','reference/fine_moment.py']})
Path(sys.argv[1]).write_text(json.dumps(result,indent=2)+'\n');print(result['status'])
Loading
Loading