s873.py

from research import *
s=begin(873,'Derive the exact lattice-preservation criterion','When does a reduced Key p/q preserve hZ?',{'keys':{'E':E,'P':P,'J':J}},['C872 declared domains'])
from math import gcd
proof={'assume':'s=h*m with integer m; gcd(p,q)=1','reduce':'(p/q)*s in hZ iff p*m/q is integer','necessity':'q divides p*m; coprimality implies q divides m','sufficiency':'m=q*t gives output h*p*t','domain':'h*q*Z'}
a=artifact('model/one_key_grid_theorem.json',json.dumps(proof,indent=2)+'\n')
finish(s,{'theorem':a,'reduced_denominators':{n:k.denominator for n,k in [('E',E),('P',P),('J',J)]}},'A Key preserves a declared grid exactly on hqZ. This is an input-domain condition, not a demand to round rational outputs or a license to apply a Key to every chronology.','Classify integer and Rounded domains for all three Keys and their intersection.',{'coprime':all(gcd(k.numerator,k.denominator)==1 for k in [E,P,J]),'grid_cancels':proof['reduce'].endswith('integer')})