import java.math.BigInteger;
import java.util.*;

/** Exact reproduction in Q and Q(sqrt(5)); Java 17+, standard library only. */
public final class Verify {
    static void require(boolean ok, String label) {
        if (!ok) throw new IllegalArgumentException(label);
    }
    static final class Q implements Comparable<Q> {
        final BigInteger n, d;
        Q(BigInteger n, BigInteger d) {
            if (d.signum()==0) throw new ArithmeticException("zero denominator");
            if (d.signum()<0) { n=n.negate(); d=d.negate(); }
            BigInteger g=n.gcd(d); this.n=n.divide(g); this.d=d.divide(g);
        }
        Q add(Q x) { return new Q(n.multiply(x.d).add(x.n.multiply(d)),d.multiply(x.d)); }
        Q neg() { return new Q(n.negate(),d); }
        Q sub(Q x) { return add(x.neg()); }
        Q mul(Q x) { return new Q(n.multiply(x.n),d.multiply(x.d)); }
        Q div(Q x) { return new Q(n.multiply(x.d),d.multiply(x.n)); }
        Q pow(int j) { require(j>=0,"exponent"); return new Q(n.pow(j),d.pow(j)); }
        Q add(long x) { return add(q(x)); } Q sub(long x) { return sub(q(x)); }
        Q mul(long x) { return mul(q(x)); } Q div(long x) { return div(q(x)); }
        int sign() { return n.signum(); }
        BigInteger floor() {
            BigInteger[] qr=n.divideAndRemainder(d);
            return n.signum()<0 && qr[1].signum()!=0 ? qr[0].subtract(BigInteger.ONE) : qr[0];
        }
        public int compareTo(Q x) { return n.multiply(x.d).compareTo(x.n.multiply(d)); }
        public boolean equals(Object x) { return x instanceof Q y && n.equals(y.n) && d.equals(y.d); }
        public int hashCode() { return Objects.hash(n,d); }
        public String toString() { return n+"/"+d; }
    }
    static Q q(long n) { return q(n,1); }
    static Q q(long n,long d) { return new Q(BigInteger.valueOf(n),BigInteger.valueOf(d)); }
    static Q q(BigInteger n) { return new Q(n,BigInteger.ONE); }
    static final class K {
        final Q a,b;
        K(Q a,Q b) { this.a=a;this.b=b; }
        K add(K x) { return new K(a.add(x.a),b.add(x.b)); }
        K neg() { return new K(a.neg(),b.neg()); }
        K sub(K x) { return add(x.neg()); }
        K mul(K x) { return new K(a.mul(x.a).add(b.mul(x.b).mul(5)),a.mul(x.b).add(b.mul(x.a))); }
        K div(K x) {
            Q den=x.a.pow(2).sub(x.b.pow(2).mul(5));
            return mul(new K(x.a.div(den),x.b.neg().div(den)));
        }
        K add(long n) { return add(k(n)); } K sub(long n) { return sub(k(n)); }
        K mul(long n) { return mul(k(n)); } K div(long n) { return div(k(n)); }
        K pow(int n) { require(n>=0,"exponent");K out=k(1);for(int i=0;i<n;i++)out=out.mul(this);return out; }
        int sign() {
            if(b.sign()==0)return a.sign();if(a.sign()==0)return b.sign();
            if(a.sign()*b.sign()>0)return a.sign();
            return a.pow(2).sub(b.pow(2).mul(5)).sign()>0 ? a.sign() : b.sign();
        }
        public boolean equals(Object x) { return x instanceof K y && a.equals(y.a) && b.equals(y.b); }
        public int hashCode() { return Objects.hash(a,b); }
        public String toString() { return a+";"+b; }
    }
    static K k(long n) { return new K(q(n),q(0)); }
    static K k(Q x) { return new K(x,q(0)); }
    static K k(long n,long d) { return k(q(n,d)); }
    static K sum(List<K> xs) { K out=k(0);for(K x:xs)out=out.add(x);return out; }
    static void emit(String name,K x) { System.out.println("VALUE\t"+name+"\t"+x); }
    record Monomial(int i,int j) implements Comparable<Monomial> {
        public int compareTo(Monomial x) { int c=Integer.compare(i,x.i);return c!=0?c:Integer.compare(j,x.j); }
    }
    static Map<Monomial,Q> mono(int i,int j) { var p=new TreeMap<Monomial,Q>();p.put(new Monomial(i,j),q(1));return p; }
    @SafeVarargs static Map<Monomial,Q> add(Map<Monomial,Q>... ps) {
        var out=new TreeMap<Monomial,Q>();
        for(var p:ps)for(var e:p.entrySet())out.merge(e.getKey(),e.getValue(),Q::add);
        out.values().removeIf(x->x.sign()==0);return out;
    }
    static Map<Monomial,Q> scale(Map<Monomial,Q> p,Q c) {
        var out=new TreeMap<Monomial,Q>();
        for(var e:p.entrySet()){Q x=e.getValue().mul(c);if(x.sign()!=0)out.put(e.getKey(),x);}return out;
    }
    @SafeVarargs static Map<Monomial,Q> mul(Map<Monomial,Q>... ps) {
        Map<Monomial,Q> out=mono(0,0);
        for(var p:ps){var next=new TreeMap<Monomial,Q>();
            for(var a:out.entrySet())for(var b:p.entrySet())
                next.merge(new Monomial(a.getKey().i+b.getKey().i,a.getKey().j+b.getKey().j),a.getValue().mul(b.getValue()),Q::add);
            next.values().removeIf(x->x.sign()==0);out=next;
        }return out;
    }
    static List<K> masses(K a,K b) {
        K ga=b.mul(5).sub(1).mul(2).div(b.sub(a).mul(k(1).sub(a)).mul(15));
        K gb=k(1).sub(a.mul(5)).mul(2).div(b.sub(a).mul(k(1).sub(b)).mul(15));
        K gc=k(3).sub(a.add(b).mul(5)).add(a.mul(b).mul(15)).div(k(1).sub(a).mul(k(1).sub(b)).mul(15));
        return List.of(ga,gb,gc);
    }
    record Decomposition(BigInteger quotient,Q residual) {}
    static Decomposition decompose(Q x,Q h) {
        require(h.sign()>0,"positive scale");BigInteger n=x.div(h).floor();return new Decomposition(n,x.sub(h.mul(q(n))));
    }
    static BigInteger reverseStep(BigInteger Q,BigInteger S,BigInteger nxt,BigInteger rho) {
        require(Q.signum()>0 && S.signum()>0 && rho.signum()>=0 && rho.compareTo(S)<0,"ledger range");
        BigInteger[] qr=S.multiply(nxt).add(rho).divideAndRemainder(Q);
        require(qr[1].signum()==0,"ledger divisibility");return qr[0];
    }
    static List<K> solve(List<List<K>> matrix,List<K> rhs) {
        require(!matrix.isEmpty() && matrix.size()==rhs.size(),"system rows");int cols=matrix.get(0).size();
        require(cols>0 && matrix.stream().allMatch(x->x.size()==cols),"system columns");
        var a=new ArrayList<List<K>>();
        for(int i=0;i<matrix.size();i++){var row=new ArrayList<>(matrix.get(i));row.add(rhs.get(i));a.add(row);}
        int row=0;
        for(int col=0;col<cols;col++){
            int pivot=-1;for(int j=row;j<a.size();j++)if(a.get(j).get(col).sign()!=0){pivot=j;break;}
            if(pivot<0)return null;Collections.swap(a,row,pivot);K factor=a.get(row).get(col);
            for(int j=0;j<=cols;j++)a.get(row).set(j,a.get(row).get(j).div(factor));
            for(int j=0;j<a.size();j++)if(j!=row){factor=a.get(j).get(col);
                for(int t=0;t<=cols;t++)a.get(j).set(t,a.get(j).get(t).sub(factor.mul(a.get(row).get(t))));}
            row++;
        }
        for(var line:a){boolean zero=true;for(int j=0;j<cols;j++)zero &= line.get(j).sign()==0;
            if(zero && line.get(cols).sign()!=0)return null;}
        var out=new ArrayList<K>();for(int j=0;j<cols;j++)out.add(a.get(j).get(cols));return out;
    }
    static List<K> moments(int degree) {
        require(0<=degree && degree<=6,"degree 0..6");var out=new ArrayList<K>();
        for(int j=0;j<=degree;j++)out.add(j%2==0?k(1,j+1):k(0));return out;
    }
    static boolean distinct(List<K> nodes) { return new HashSet<>(nodes).size()==nodes.size(); }
    static List<List<K>> momentMatrix(List<K> nodes,int d) {
        var out=new ArrayList<List<K>>();for(int j=0;j<=d;j++){var row=new ArrayList<K>();for(K x:nodes)row.add(x.pow(j));out.add(row);}return out;
    }
    static K weighted(List<K> weights,List<K> nodes,int degree) {
        K out=k(0);for(int i=0;i<nodes.size();i++)out=out.add(weights.get(i).mul(nodes.get(i).pow(degree)));return out;
    }
    static List<K> positiveRule(List<K> nodes,int degree) {
        require(nodes.size()==6 && distinct(nodes),"six distinct nodes");var target=moments(degree);
        for(int size=1;size<=Math.min(6,degree+1);size++)for(int mask=1;mask<64;mask++){
            if(Integer.bitCount(mask)!=size)continue;var idx=new ArrayList<Integer>();var selected=new ArrayList<K>();
            for(int i=0;i<6;i++)if((mask & (1<<i))!=0){idx.add(i);selected.add(nodes.get(i));}
            var w=solve(momentMatrix(selected,degree),target);
            if(w!=null && w.stream().allMatch(x->x.sign()>=0)){
                var out=new ArrayList<>(Collections.nCopies(6,k(0)));for(int j=0;j<idx.size();j++)out.set(idx.get(j),w.get(j));return out;
            }
        }return null;
    }
    static List<List<K>> copyRecords(List<List<K>> records) {
        var out=new ArrayList<List<K>>();for(var row:records)out.add(row==null?null:new ArrayList<>(row));return out;
    }
    static List<List<K>> recoverAffine(List<K> nodes,List<List<K>> records,int errors) {
        require(nodes.size()==6 && records.size()==6,"six labeled records");require(errors>=0,"error budget");
        require(distinct(nodes),"distinct nodes");var good=new ArrayList<Integer>();
        for(int i=0;i<6;i++)if(records.get(i)!=null)good.add(i);
        require(2L*errors+6-good.size()<=4,"recovery budget");int dim=records.get(good.get(0)).size();
        require(dim>0 && good.stream().allMatch(i->records.get(i).size()==dim),"coordinate dimension");
        var candidates=new ArrayList<List<List<K>>>();
        for(int ii=0;ii<good.size();ii++)for(int jj=ii+1;jj<good.size();jj++){
            int i=good.get(ii),j=good.get(jj);var m=new ArrayList<K>();var qv=new ArrayList<K>();
            for(int z=0;z<dim;z++){K q=records.get(j).get(z).sub(records.get(i).get(z)).div(nodes.get(j).sub(nodes.get(i)));
                qv.add(q);m.add(records.get(i).get(z).sub(nodes.get(i).mul(q)));}
            var pred=new ArrayList<List<K>>();for(K t:nodes){var row=new ArrayList<K>();for(int z=0;z<dim;z++)row.add(m.get(z).add(t.mul(qv.get(z))));pred.add(row);}
            int mismatch=0;for(int t:good)if(!pred.get(t).equals(records.get(t)))mismatch++;
            if(mismatch<=errors && !candidates.contains(pred))candidates.add(pred);
        }
        require(candidates.size()==1,"unique affine recovery");return candidates.get(0);
    }
    static Q[] atanInterval(int d) {
        Q partial=q(0);for(int j=0;j<24;j++)partial=partial.add(new Q(BigInteger.valueOf(j%2==0?1:-1),BigInteger.valueOf(d).pow(2*j+1).multiply(BigInteger.valueOf(2*j+1))));
        Q other=partial.add(new Q(BigInteger.ONE,BigInteger.valueOf(d).pow(49).multiply(BigInteger.valueOf(49))));
        return partial.compareTo(other)<0?new Q[]{partial,other}:new Q[]{other,partial};
    }
    static boolean rejected(Runnable f) { try{f.run();return false;}catch(IllegalArgumentException|ArithmeticException e){return true;} }
    static K crossRatio(List<K> y) { return y.get(2).sub(y.get(0)).mul(y.get(3).sub(y.get(1))).div(y.get(2).sub(y.get(1)).mul(y.get(3).sub(y.get(0)))); }
    static void additionalChecks(List<String> labels) {
        for(Q c:List.of(q(-3,2),q(0),q(1)))for(Q r:List.of(q(-2,3),q(0),q(1,3),q(2,3)))for(Q x:List.of(c.sub(2),c,c.add(3))){
            Q z=x;for(int n=0;n<19;n++){require(z.equals(c.add(r.pow(n).mul(x.sub(c)))),"affine closed form");Q nxt=c.add(r.mul(z.sub(c)));
                if(r.sign()>0 && r.compareTo(q(1))<0)require(nxt.sub(z).mul(c.sub(z)).sign()>=0,"affine monotonicity");z=nxt;}}
        labels.add("affine iteration and monotonicity");
        for(Q h:List.of(q(1,3),q(1),q(7,2)))for(Q x:List.of(new Q(BigInteger.TEN.pow(50).negate(),BigInteger.valueOf(3)),q(-3,2),q(0),q(5,4),q(BigInteger.TWO.pow(160).add(BigInteger.ONE)))){
            var e=decompose(x,h);require(x.equals(h.mul(q(e.quotient)).add(e.residual)) && e.residual.sign()>=0 && e.residual.compareTo(h)<0,"floor decomposition");}
        require(q(-3,2).floor().equals(BigInteger.valueOf(-2)),"floor versus truncation");labels.add("signed floor decomposition and large integers");
        for(Q r:List.of(q(1,3),q(2,3)))for(Q h:List.of(q(1,5),q(1)))for(Q x:List.of(q(-17,3),q(0),q(399,7))){
            Q z=x;var history=new ArrayList<Q>();for(int n=1;n<24;n++){
                Q nxt=h.mul(q(r.mul(z).div(h).floor()));history.add(r.mul(z).sub(nxt));z=nxt;Q err=q(0);
                for(int j=0;j<history.size();j++)err=err.add(r.pow(n-1-j).mul(history.get(j)));
                require(r.pow(n).mul(x).equals(z.add(err)),"unrolled residual identity");Q bound=h.mul(q(1).sub(r.pow(n))).div(q(1).sub(r));
                require(err.sign()>=0 && err.compareTo(bound)<0 && bound.compareTo(h.div(q(1).sub(r)))<0,"residual bound");}}
        labels.add("quantized recurrence and geometric error bounds");
        BigInteger Q=new BigInteger("339949771344778"),S=BigInteger.TEN.pow(15);
        for(BigInteger seed:List.of(BigInteger.valueOf(-32767),BigInteger.ZERO,BigInteger.valueOf(399),BigInteger.valueOf(32767),BigInteger.TWO.pow(160).add(BigInteger.ONE))){
            BigInteger d=seed;var ledger=new ArrayList<BigInteger>();for(int i=0;i<23;i++){
                BigInteger nxt=new Verify.Q(Q.multiply(d),S).floor(),rho=Q.multiply(d).subtract(S.multiply(nxt));ledger.add(rho);
                require(reverseStep(Q,S,nxt,rho).equals(d),"integer reverse step");d=nxt;}
            for(int i=ledger.size()-1;i>=0;i--)d=reverseStep(Q,S,d,ledger.get(i));require(d.equals(seed),"complete ledger reverse");}
        require(rejected(()->reverseStep(Q,S,BigInteger.ZERO,S)),"reject remainder bound");
        require(rejected(()->reverseStep(Q,S,BigInteger.ZERO,BigInteger.ONE)),"reject nondivisible reverse");labels.add("integer ledgers and invalid-witness rejection");
        var nodes=List.of(k(-3),k(-2),k(-1),k(1),k(2),k(3));
        for(int degree=0;degree<6;degree++){
            var coeff=new ArrayList<K>();for(int j=0;j<=degree;j++)coeff.add(k((j%2==0?1:-1)*(j+1),j+2));
            var matrix=new ArrayList<List<K>>();var values=new ArrayList<K>();
            for(K t:nodes){var row=new ArrayList<K>();K val=k(0);for(int j=0;j<=degree;j++){row.add(t.pow(j));val=val.add(t.pow(j).mul(coeff.get(j)));}matrix.add(row);values.add(val);}
            require(Objects.equals(solve(matrix,values),coeff),"polynomial coefficient recovery");}
        var m=List.of(k(2),k(-1),k(7));var qv=List.of(k(3),k(2),k(-2));var original=new ArrayList<List<K>>();
        for(K t:nodes){var row=new ArrayList<K>();for(int j=0;j<3;j++)row.add(m.get(j).add(t.mul(qv.get(j))));original.add(row);}
        var corrupt=copyRecords(original);corrupt.get(0).set(0,corrupt.get(0).get(0).add(100));corrupt.get(5).set(2,corrupt.get(5).get(2).sub(200));
        require(recoverAffine(nodes,corrupt,2).equals(original),"two errors");var erased=copyRecords(original);
        for(int i=0;i<6;i++)if(i!=1 && i!=4)erased.set(i,null);require(recoverAffine(nodes,erased,0).equals(original),"four erasures");
        var mixed=copyRecords(original);mixed.set(1,null);mixed.set(4,null);mixed.get(0).set(1,mixed.get(0).get(1).add(123));
        require(recoverAffine(nodes,mixed,1).equals(original),"mixed errors and erasures");var malformed=copyRecords(original);malformed.set(0,List.of(malformed.get(0).get(0)));
        require(rejected(()->recoverAffine(nodes,malformed,0)),"reject truncated coordinate");require(rejected(()->recoverAffine(nodes,original,3)),"reject excess budget");
        labels.add("polynomial interpolation and affine record recovery");
        K phi=new K(q(1,2),q(1,2)),root=new K(q(0),q(1)),star=root.sub(1).div(4);
        for(K s:List.of(k(1,4),star,k(1,2))){
            K A=s.add(phi.pow(2)),B=s.add(1),u=s.div(A),v=B.div(A);var x=List.of(k(-1),v.neg(),u.neg(),u,v,k(1));var g=masses(u.pow(2),v.pow(2));
            var w=List.of(g.get(2).div(2),g.get(1).div(2),g.get(0).div(2),g.get(0).div(2),g.get(1).div(2),g.get(2).div(2));
            require(Objects.equals(solve(momentMatrix(x,5),moments(5)),w),"independent moment solve");
            for(int degree:new int[]{3,4,5,6}){var result=positiveRule(x,degree);boolean expected=degree==3 || (degree<=5 && s.sub(star).sign()>=0);
                require((result!=null)==expected,"positive support feasibility");if(result!=null)for(int j=0;j<=degree;j++)require(weighted(result,x,j).equals(moments(degree).get(j)),"returned positive-rule witness");}
            var scaled=new ArrayList<K>();for(K t:x)scaled.add(A.mul(t));
            for(int j=0;j<6;j++)require(weighted(w,scaled,j).equals(j%2!=0?k(0):A.pow(j).div(j+1)),"interval transport");
            var outer=List.of(A.neg(),B.neg(),B,A);var image=new ArrayList<K>();for(K t:outer)image.add(t.mul(2).add(1).div(t.add(10)));
            K ratio=crossRatio(outer);require(crossRatio(image).equals(ratio),"projective invariance");K pr=A.add(B).div(A.sub(B));
            require(pr.sign()>0 && pr.pow(2).equals(ratio.div(ratio.sub(1))),"positive root branch");require(phi.div(2).mul(pr.sub(root)).equals(s),"seed inverse");}
        labels.add("independent quadrature solve and positive support search");labels.add("interval rescaling and projective parameter recovery");
        Q[] a=atanInterval(5),b=atanInterval(239);Q piL=a[0].mul(16).sub(b[1].mul(4)),piU=a[1].mul(16).sub(b[0].mul(4));
        Q xL=piL.div(1296000),xU=piU.div(1296000),sL=xL.sub(xL.pow(3).div(6)),sU=xU;
        require(xL.sign()>0 && xL.compareTo(xU)<0 && xU.compareTo(q(1))<0,"sine-bound domain");
        require(sL.sign()>0 && sL.compareTo(sU)<0 && sU.compareTo(q(1,4))<0,"one-arcsecond seed enclosure");
        require(k(sU).sub(star).sign()<0,"canonical seed below threshold");BigInteger scale=BigInteger.TEN.pow(24),iroot=scale.pow(2).multiply(BigInteger.valueOf(5)).sqrt();
        BigInteger radicand=scale.pow(2).multiply(BigInteger.valueOf(5));
        require(iroot.pow(2).compareTo(radicand)<=0 && iroot.add(BigInteger.ONE).pow(2).compareTo(radicand)>0,"integer square-root witness");
        Q phiL=new Q(iroot,scale).add(1).div(2),phiU=new Q(iroot.add(BigInteger.ONE),scale).add(1).div(2);
        Q lo=phiL.div(phiL.add(piU)),hi=phiU.div(phiU.add(piL));
        require(lo.sign()>0 && lo.compareTo(hi)<0 && hi.compareTo(q(1))<0 && hi.sub(lo).compareTo(new Q(BigInteger.ONE,BigInteger.TEN.pow(24)))<0,"contraction interval");
        emit("canonical_seed_lower",k(sL));emit("canonical_seed_upper",k(sU));emit("contraction_lower",k(lo));emit("contraction_upper",k(hi));
        labels.add("certified transcendental seed and contraction enclosures");
        require(rejected(()->decompose(q(1),q(0))),"reject zero grid");require(rejected(()->positiveRule(Collections.nCopies(6,k(0)),3)),"reject duplicate nodes");
        require(rejected(()->moments(-1)),"reject invalid degree");require(rejected(()->k(1).div(k(0))),"reject zero field divisor");labels.add("input-domain rejection");
        double p=(1+Math.sqrt(5))/2,s=Math.sin(Math.PI/1296000),aa=Math.pow(s/(s+p*p),2),bb=Math.pow((s+1)/(s+p*p),2);
        double amplification=1-4*(5*bb-1)/(15*(bb-aa)*(1-aa));require(Math.abs(amplification-1.4944217144773972)<1e-12,"numerical illustration only");
        System.out.printf(Locale.ROOT,"APPROX\tcanonical_amplification\t%.8f%n",amplification);
    }
    public static void main(String[] args) {
        var labels=new ArrayList<String>();var one=mono(0,0);var a=mono(1,0);var b=mono(0,1);
        var da=add(one,scale(a,q(-1)));var db=add(one,scale(b,q(-1)));var gap=add(b,scale(a,q(-1)));
        var den=scale(mul(gap,da,db),q(15));var na=scale(mul(add(scale(b,q(5)),scale(one,q(-1))),db),q(2));
        var nb=scale(mul(add(one,scale(a,q(-5))),da),q(2));var nc=mul(add(scale(one,q(3)),scale(add(a,b),q(-5)),scale(mul(a,b),q(15))),gap);
        for(int j=0;j<3;j++)require(add(mul(na,mono(j,0)),mul(nb,mono(0,j)),nc).equals(scale(den,q(1,2*j+1))),"formal moment identity");
        labels.add("formal degree-five moment identities");
        var sixth=add(scale(one,q(1,7)),scale(add(one,a,b),q(-1,5)),scale(add(a,b,mul(a,b)),q(1,3)),scale(mul(a,b),q(-1)));
        require(sixth.equals(scale(add(scale(one,q(3)),scale(add(a,b),q(-7)),scale(mul(a,b),q(35))),q(-2,105))),"formal sixth-degree obstruction");
        labels.add("formal sixth-degree obstruction");var fourth=add(scale(one,q(1,5)),scale(add(one,b),q(-1,3)),b);
        require(fourth.equals(scale(add(scale(b,q(5)),scale(one,q(-1))),q(2,15))),"formal fourth-degree obstruction");labels.add("formal fourth-degree obstruction");
        K phi=new K(q(1,2),q(1,2)),root=new K(q(0),q(1)),star=root.sub(1).div(4),rstar=root.mul(3).add(5).div(10);
        require(phi.pow(2).equals(phi.add(1)),"golden identity");require(phi.pow(2).add(1).pow(2).equals(phi.pow(2).mul(5)),"endpoint bound");
        require(k(3).sub(k(7).div(phi.pow(2))).sign()>0,"uniform obstruction bound");require(k(2,3).sub(k(1).div(phi.pow(2))).sign()>0,"positive cubic rule bound");labels.add("exact field identities and endpoint bounds");
        var cases=List.of(k(1,1000000),k(1,10),k(1,4),star,k(1,2),k(3,4),k(999999,1000000));
        for(int number=0;number<cases.size();number++){
            K s=cases.get(number),A=s.add(phi.pow(2)),B=s.add(1),u=s.div(A),v=B.div(A),alpha=u.pow(2),beta=v.pow(2);var g=masses(alpha,beta);
            require(g.get(0).sign()==s.sub(star).sign(),"inner mass sign");require(g.get(1).sign()>0 && g.get(2).sign()>0,"other mass signs");
            for(int j=0;j<3;j++)require(g.get(0).mul(alpha.pow(j)).add(g.get(1).mul(beta.pow(j))).add(g.get(2)).equals(k(1,2*j+1)),"exact field moment");
            K sv=k(-2,105).mul(k(3).sub(alpha.add(beta).mul(7)).add(alpha.mul(beta).mul(35)));require(sv.sign()<0,"sixth moment obstruction");
            K t=k(2).div(k(2).sub(alpha).sub(beta).mul(3));require(t.sign()>0 && k(1).sub(t.mul(2)).sign()>0,"cubic positivity");
            require(t.mul(alpha).add(t.mul(beta)).add(1).sub(t.mul(2)).equals(k(1,3)),"cubic moment");K ratio=v.add(1).pow(2).div(v.mul(4));
            require(rstar.sub(ratio).sign()==s.sub(star).sign(),"cross-ratio threshold");K tv=k(0);for(K x:g)tv=tv.add(x.mul(x.sign()));
            require(tv.equals(k(1).add(g.get(0).sign()>=0?k(0):g.get(0).mul(-2))),"amplification formula and attaining error signs");
            String prefix="case_"+number+"_";emit(prefix+"s",s);emit(prefix+"inner",g.get(0));emit(prefix+"middle",g.get(1));emit(prefix+"outer",g.get(2));emit(prefix+"cross_ratio",ratio);emit(prefix+"amplification",tv);
            if(s.equals(star)){require(beta.equals(k(1,5)),"boundary location");require(g.equals(List.of(k(0),k(5,6),k(1,6))),"boundary masses");require(ratio.equals(rstar),"boundary cross-ratio");}
        }
        labels.addAll(List.of("field moments and mass signs on seven seeds","strictly positive cubic rules on seven seeds","degree-six failure on seven seeds","cross-ratio threshold on seven seeds","sharp amplification on seven seeds","exact boundary weights and cross-ratio"));
        var limiting=masses(k(0),k(1).div(phi.pow(4)));require(limiting.get(0).equals(k(-2).div(phi.mul(5))),"limiting negative mass");
        require(k(1).sub(limiting.get(0).mul(2)).equals(k(1).add(k(4).div(phi.mul(5)))),"limiting amplification");labels.add("one-sided small-seed amplification limit");
        Q c=q(1,2),h=q(1),r=q(1,2),x=q(3,4),T=c.add(r.mul(x.sub(c)));
        require(h.mul(q(T.div(h).floor())).sub(c).equals(q(-1,2)),"unaligned grid counterexample");
        require(h.mul(q(r.mul(x.sub(c)).div(h).floor())).equals(q(0)),"recentered comparison");
        require(c.add(h.mul(q(T.sub(c).div(h).floor()))).sub(c).equals(h.mul(q(r.mul(x.sub(c)).div(h).floor()))),"aligned grid");
        labels.add("grid-origin compatibility counterexample");additionalChecks(labels);
        for(String label:labels)System.out.println("PASS\t"+label);System.out.println("TOTAL\t"+labels.size()+"\tPASS");
    }
}