"""Complete exact algebra/domain checker for the final rank/capacity iteration."""
from fractions import Fraction as F
from pathlib import Path
import sys,runpy,json
ROOT=Path(__file__).resolve().parent
sys.path.insert(0,str(ROOT))
sys.path.insert(0,str(Path(__file__).parent))
from localize import bound,ns
G=F(866807,2000000);AB=G;old=F(23,53)
for target in [G,AB]:
    assert 2*target>F(110,127) and 2*target>1-F(65,484)
    assert 2*target>1-F(17,127)
    # Entry only needs a fixed positive m to absorb finite packing errors.
    assert 2*(F(7,8)-2*target)<F(25,1296)  # m>1/9, not the obsolete1/8 gate.
    assert F(42503599,100000000)<target  # Exact y>=z optimized branch replaces obsolete .001 gap.
common=[
 ('r>=1/10',[0,0,0,0,0,1],-F(1,10)),
 ('w>=1/10',[0,0,0,1,0,0],-F(1,10)),
 ('z>=1/5',[0,0,1,0,0,0],-F(1,5)),
 ('y>=187m/1000',[-F(187,2000),1,0,0,F(187,1000),0],0),
 ('y<=w',[0,-1,0,1,0,0],0),
 ('2y<=z',[0,-2,1,0,0,0],0),
 ('y<=3z/8',[0,-1,F(3,8),0,0,0],0),
 ('r+z<=6w',[0,0,-1,6,0,-1],0),
 ('h<=5m/4',[F(5,8),0,0,0,-F(13,4),0],0),
]
exclusions=json.loads(Path(__file__).with_name('exclusion-certificate.json').read_text())
exception_bounds={case['name']:F(case['gamma']) for case in exclusions['cases']}
assert exception_bounds['y_ge_z']<G
covered={'y<=3z/8':'y_ge_3z8','y<=13m/20':'y_ge_13m20'}
def check_condition(args):
    if args[0] in covered:assert exception_bounds[covered[args[0]]]<G
    else:assert bound(*args)>2*(old-G)
for args in common:check_condition(args)
dd=[
 ('y<=m',[F(1,2),-1,0,0,-1,0],0),
 ('y<=13m/20',[F(13,40),-1,0,0,-F(13,20),0],0),
 ('z<=3m',[F(3,2),0,-1,0,-3,0],0),
]
# The y/q and z/q conditions also apply to AB; all previous matrices
# depend on m=min(d,q) and are independent of family orientation.
for args in dd:check_condition(args)
runpy.run_path(str(Path(__file__).with_name('verify_exclusions.py')))
# First establish the positive imbalance without any top-capacity assumption.
runpy.run_path(str(Path(__file__).with_name('verify_small_imbalance.py')),run_name='__main__')
small_imbalance=json.loads(Path(__file__).with_name('small-imbalance-certificate.json').read_text())
assert len(small_imbalance['cases'])==4 and {(v['orientation'],v['capacity'])for v in small_imbalance['cases']}=={(o,c)for o in ['AB','CD']for c in ['r_le_2w','r_ge_2w']}
assert all(F(row['gamma'])<G for row in small_imbalance['cases'])
# Therefore h>=3m/10. All other common domains hold. The next two
# oriented comparisons exclude m>=2w without assuming r<=2w or m<=2w.
runpy.run_path(str(Path(__file__).with_name('verify_ab_boundary.py')),run_name='__main__')
runpy.run_path(str(Path(__file__).with_name('verify_cd_boundary.py')),run_name='__main__')
ab_boundary=json.loads(Path(__file__).with_name('ab-boundary-certificate.json').read_text())
assert len(ab_boundary['cases'])==2 and {v['kind']for v in ab_boundary['cases']}=={'r_le_2w','r_ge_2w'}
assert all(F(row['gamma'])<G for row in ab_boundary['cases'])
assert F(json.loads(Path(__file__).with_name('cd-boundary-certificate.json').read_text())['gamma'])<G
# Thus m<=2w in both orientations and r<=m<=2w.

old_domains=runpy.run_path(str(Path(__file__).with_name('verify_ab_good_domains.py')))
old_domains['verify'](['r_le_7q8'])
runpy.run_path(str(Path(__file__).with_name('verify_high_c.py')),run_name='__main__')
assert F(43321,100000)<G
runpy.run_path(str(Path(__file__).with_name('verify_z_domain.py')),run_name='__main__')
runpy.run_path(str(Path(__file__).with_name('verify_good_domain_new.py')),run_name='__main__')
runpy.run_path(str(Path(__file__).with_name('verify_cp_large.py')),run_name='__main__')
runpy.run_path(str(Path(__file__).with_name('verify_cp_small.py')),run_name='__main__')
runpy.run_path(str(Path(__file__).with_name('verify_swap_cap.py')),run_name='__main__')
runpy.run_path(str(Path(__file__).with_name('verify_cd_domain.py')),run_name='__main__')
assert AB<=G
for filename in ['cd-domain-certificate.json','swap-cap-certificate.json','good-domain-new-certificate.json','z-domain-certificate.json']:
    assert F(json.loads(Path(__file__).with_name(filename).read_text())['gamma'])<=G
for filename in ['cp-large-certificate.json','cp-small-certificate.json','ab-good-domains-certificate.json']:
    data=json.loads(Path(__file__).with_name(filename).read_text())
    if 'gamma' in data:assert F(data['gamma'])<=G
    else:assert all(F(row['gamma'])<=G for row in data['cases'] if row['name']=='r_le_7q8')
assert 1/(1+F(3,10))<F(4,5)
assert F(13,4)<8
assert F(1,5)*F(8)==F(12,5)-F(4,5)
print('PASS: full universal gamma(4)<=',G,'=',float(G))