s1000.py

from research import *
s=begin(1000,'Verify fixed-pivot domains','Do the declared residue classes preserve integrality at both stages?',{},['C999'])
rows=json.loads((ROOT/'model/fixed_pivot_key_domains.json').read_text());ks={'E':E,'P':P,'J':J};checks=[]
for r in rows:
 if r['nonempty']:
  n1,n2=r['pair'].split('→')
  for t in [-1,0,1]:
   x=r['residue']+r['period']*t;y=14006+ks[n1]*(x-14006);z=4836+ks[n2]*(y-4836);checks.append(y.denominator==z.denominator==1)
finish(s,{'nonempty_class_checks':len(checks),'pivot_difference_mod3':(4836-14006)%3,'J_to_P_reason':'gcd(300,69)=3 does not divide−9170'},'All nonempty class formulas pass exact staged substitution. J→P fails because the two fixed pivots differ modulo3; no endpoint choice repairs that within the declared integer domain.','Extend the congruence result from one point to an entire labelled field.',{'all_substitutions':all(checks),'obstruction':(4836-14006)%3==1})