import java.math.BigInteger;
import java.nio.charset.StandardCharsets;
import java.util.ArrayList;
import java.util.Arrays;
import java.util.Collections;
import java.util.LinkedHashMap;
import java.util.List;
import java.util.Map;
import java.util.TreeMap;

/**
 * OMEGA NAUGHT: exact symbolic certificates and finite audits.
 * Java 17+, standard library only. Uses BigInteger and reduced rationals.
 * No floating-point arithmetic or Java assert statements.
 * General theorems and the scope of each audit are in the companion Markdown.
 */
public final class OmegaUnifiedProof {
    static final BigInteger ZERO = BigInteger.ZERO;
    static final BigInteger ONE = BigInteger.ONE;
    static final BigInteger Q = new BigInteger("339949771344778");
    static final BigInteger S = new BigInteger("1000000000000000");
    static final int MAX_SEED = 32767;
    static final int HORIZON = 23;
    static final int MAX_FIBER = 50000;

    static BigInteger b(long n) { return BigInteger.valueOf(n); }

    static void require(boolean condition, String message) {
        // Always active, even when Java assertions are disabled.
        if (!condition) throw new IllegalStateException(message);
    }

    static void natural(BigInteger n, String name) {
        if (n == null || n.signum() < 0)
            throw new IllegalArgumentException(name + " must be nonnegative");
    }

    static BigInteger ceilDiv(BigInteger n, BigInteger d) {
        natural(n, "numerator");
        if (d == null || d.signum() <= 0)
            throw new IllegalArgumentException("positive denominator required");
        return n.add(d).subtract(ONE).divide(d);
    }

    static BigInteger boundary(BigInteger y) {
        natural(y, "output");
        return ceilDiv(S.multiply(y), Q);
    }

    record Step(BigInteger output, BigInteger remainder, int rank) {}

    static Step forward(BigInteger d) {
        natural(d, "state");
        BigInteger[] qr = Q.multiply(d).divideAndRemainder(S);
        int rank = d.subtract(boundary(qr[0])).intValueExact();
        require(qr[1].signum() >= 0 && qr[1].compareTo(S) < 0
                && rank >= 0 && rank <= 2, "forward invariant");
        return new Step(qr[0], qr[1], rank);
    }

    static BigInteger inverseRemainder(BigInteger y, BigInteger r) {
        natural(y, "output");
        natural(r, "remainder");
        if (r.compareTo(S) >= 0)
            throw new IllegalArgumentException("remainder outside [0,S)");
        BigInteger[] qr = S.multiply(y).add(r).divideAndRemainder(Q);
        if (qr[1].signum() != 0)
            throw new IllegalArgumentException("record is not divisible by Q");
        BigInteger[] check = Q.multiply(qr[0]).divideAndRemainder(S);
        if (!check[0].equals(y) || !check[1].equals(r))
            throw new IllegalArgumentException("inconsistent remainder record");
        return qr[0];
    }

    static BigInteger inverseRank(BigInteger y, int w) {
        natural(y, "output");
        if (w < 0 || w > 2)
            throw new IllegalArgumentException("rank must be 0, 1, or 2");
        BigInteger d = boundary(y).add(b(w));
        if (!Q.multiply(d).divide(S).equals(y))
            throw new IllegalArgumentException("rank not present in this fiber");
        return d;
    }

    static List<BigInteger> recoverRemainders(BigInteger terminal,
                                              List<BigInteger> witnesses) {
        natural(terminal, "terminal state");
        List<BigInteger> history = new ArrayList<>();
        history.add(terminal);
        for (int i = witnesses.size() - 1; i >= 0; --i) {
            terminal = inverseRemainder(terminal, witnesses.get(i));
            history.add(terminal);
        }
        Collections.reverse(history);
        return history;
    }

    static List<BigInteger> recoverRanks(BigInteger terminal, List<Integer> witnesses) {
        natural(terminal, "terminal state");
        List<BigInteger> history = new ArrayList<>();
        history.add(terminal);
        for (int i = witnesses.size() - 1; i >= 0; --i) {
            terminal = inverseRank(terminal, witnesses.get(i));
            history.add(terminal);
        }
        Collections.reverse(history);
        return history;
    }

    /** Reduced exact rational with positive denominator. */
    static final class Rat implements Comparable<Rat> {
        final BigInteger n;
        final BigInteger d;
        Rat(BigInteger numerator, BigInteger denominator) {
            if (denominator.signum() == 0)
                throw new IllegalArgumentException("zero denominator");
            if (denominator.signum() < 0) {
                numerator = numerator.negate();
                denominator = denominator.negate();
            }
            BigInteger gcd = numerator.gcd(denominator);
            n = numerator.divide(gcd);
            d = denominator.divide(gcd);
        }
        Rat(long numerator, long denominator) { this(b(numerator), b(denominator)); }
        static Rat of(long n) { return new Rat(b(n), ONE); }
        static Rat of(BigInteger n) { return new Rat(n, ONE); }
        Rat add(Rat other) {
            return new Rat(n.multiply(other.d).add(other.n.multiply(d)), d.multiply(other.d));
        }
        Rat neg() { return new Rat(n.negate(), d); }
        Rat sub(Rat other) { return add(other.neg()); }
        Rat mul(Rat other) { return new Rat(n.multiply(other.n), d.multiply(other.d)); }
        Rat div(Rat other) {
            if (other.n.signum() == 0) throw new IllegalArgumentException("division by zero");
            return new Rat(n.multiply(other.d), d.multiply(other.n));
        }
        Rat square() { return new Rat(n.multiply(n), d.multiply(d)); }
        public int compareTo(Rat other) {
            return n.multiply(other.d).compareTo(other.n.multiply(d));
        }
        boolean lt(Rat other) { return compareTo(other) < 0; }
        boolean le(Rat other) { return compareTo(other) <= 0; }
        @Override public boolean equals(Object other) {
            return other instanceof Rat r && n.equals(r.n) && d.equals(r.d);
        }
        @Override public int hashCode() { return 31*n.hashCode()+d.hashCode(); }
        @Override public String toString() { return n + "/" + d; }
    }

    static Rat[] distances(Rat a, Rat x, Rat y) {
        return new Rat[]{x.add(a).square().add(y.square()),
                         x.sub(a).square().add(y.square()),
                         x.square().add(y.sub(a).square())};
    }

    static Rat[] recoverPoint(Rat a, Rat[] delta) {
        if (a.compareTo(Rat.of(0)) <= 0 || delta.length != 3)
            throw new IllegalArgumentException("positive scale and three distances required");
        for (Rat r : delta)
            if (r.compareTo(Rat.of(0)) < 0)
                throw new IllegalArgumentException("negative squared distance");
        Rat denominator = Rat.of(4).mul(a);
        Rat x = delta[0].sub(delta[1]).div(denominator);
        Rat y = delta[0].add(delta[1]).sub(Rat.of(2).mul(delta[2])).div(denominator);
        if (!Arrays.equals(distances(a, x, y), delta))
            throw new IllegalArgumentException("inconsistent planar distance record");
        return new Rat[]{x, y};
    }

    static BigInteger encodeMessage(byte[] message) {
        byte[] marked = new byte[message.length + 1];
        marked[0] = 1;
        System.arraycopy(message, 0, marked, 1, message.length);
        return new BigInteger(1, marked);
    }

    static byte[] decodeMessage(BigInteger n) {
        natural(n, "message integer");
        if (n.signum() == 0) throw new IllegalArgumentException("zero has no marker");
        byte[] raw = n.toByteArray();
        // A valid marker is 0x01, so a valid code needs no leading sign byte.
        if (raw[0] != 1) throw new IllegalArgumentException("invalid message marker");
        return Arrays.copyOfRange(raw, 1, raw.length);
    }

    static Rat encodeBounded(byte[] message) {
        return Rat.of(1).add(new Rat(ONE, encodeMessage(message).add(ONE)));
    }

    static byte[] decodeBounded(Rat a) {
        if (!Rat.of(1).lt(a) || !a.le(new Rat(3, 2)))
            throw new IllegalArgumentException("bounded scale must lie in (1,3/2]");
        Rat n = Rat.of(1).div(a.sub(Rat.of(1))).sub(Rat.of(1));
        if (!n.d.equals(ONE)) throw new IllegalArgumentException("noninteger message code");
        return decodeMessage(n.n);
    }

    /** Sparse Z-polynomials. Sorted strings represent commutative monomials. */
    static final class Poly {
        final Map<String, BigInteger> terms;
        Poly(Map<String, BigInteger> input) {
            terms = new TreeMap<>();
            input.forEach((key, value) -> { if (value.signum() != 0) terms.put(key, value); });
        }
        static Poly number(long n) { return new Poly(Map.of("", b(n))); }
        static Poly variable(String name) {
            if (name.length() != 1 || !Character.isLetter(name.charAt(0)))
                throw new IllegalArgumentException("one-letter variable required");
            return new Poly(Map.of(name, ONE));
        }
        Poly add(Poly other) {
            Map<String, BigInteger> result = new TreeMap<>(terms);
            other.terms.forEach((key, value) -> result.merge(key, value, BigInteger::add));
            return new Poly(result);
        }
        Poly neg() {
            Map<String, BigInteger> result = new TreeMap<>();
            terms.forEach((key, value) -> result.put(key, value.negate()));
            return new Poly(result);
        }
        Poly sub(Poly other) { return add(other.neg()); }
        Poly mul(Poly other) {
            Map<String, BigInteger> result = new TreeMap<>();
            for (Map.Entry<String, BigInteger> left : terms.entrySet()) {
                for (Map.Entry<String, BigInteger> right : other.terms.entrySet()) {
                    char[] key = (left.getKey()+right.getKey()).toCharArray();
                    Arrays.sort(key);
                    result.merge(new String(key), left.getValue().multiply(right.getValue()),
                                 BigInteger::add);
                }
            }
            return new Poly(result);
        }
        Poly scale(long n) { return mul(number(n)); }
        Poly pow(int n) {
            if (n < 0) throw new IllegalArgumentException("negative polynomial exponent");
            Poly result = number(1);
            for (int k = 0; k < n; ++k) result = result.mul(this);
            return result;
        }
    }

    static Poly[] symbolicDistances(Poly a, Poly x, Poly y) {
        return new Poly[]{x.add(a).pow(2).add(y.pow(2)),
                          x.sub(a).pow(2).add(y.pow(2)),
                          x.pow(2).add(y.sub(a).pow(2))};
    }

    static int symbolicCertificates() {
        Poly a=Poly.variable("a"), x=Poly.variable("x"), y=Poly.variable("y");
        Poly u=Poly.variable("u"), v=Poly.variable("v"), p=Poly.variable("p");
        Poly q=Poly.variable("q"), d=Poly.variable("d"), e=Poly.variable("e");
        Poly h=Poly.variable("h"), f=Poly.variable("f"), c=Poly.variable("c");
        Poly r=Poly.variable("r"), l=Poly.variable("l"), z=Poly.variable("z");
        Poly j=Poly.variable("j");
        Poly t=q.mul(d).sub(e), nxt=q.mul(t).sub(j), lam=q.add(h);
        Poly[] dx=symbolicDistances(a,x,y), du=symbolicDistances(a,u,v);
        Poly first=dx[0].sub(dx[1]).sub(du[0]).add(du[1]);
        Poly second=dx[0].add(dx[1]).sub(dx[2].scale(2))
                .sub(du[0]).sub(du[1]).add(du[2].scale(2));
        List<Poly> certificates = List.of(
            a.mul(f).mul(f.add(c)).sub(f.mul(a.mul(f).add(a.mul(c)))),
            a.mul(x).sub(a.mul(u)).pow(2).add(a.mul(y).sub(a.mul(v)).pow(2))
                .sub(a.pow(2).mul(x.sub(u).pow(2).add(y.sub(v).pow(2)))),
            r.add(l.mul(a)).sub(r.add(l.mul(r.add(a).sub(r)))),
            q.mul(d).mul(p).sub(t.mul(p).add(e.mul(p))),
            lam.mul(d).mul(p).sub(t.mul(p).add(e.add(h.mul(d)).mul(p))),
            dx[0].sub(dx[1]).sub(a.mul(x).scale(4)),
            dx[0].add(dx[1]).sub(dx[2].scale(2)).sub(a.mul(y).scale(4)),
            x.add(a).pow(2).add(y.pow(2)).add(z.pow(2)).sub(dx[0]).sub(z.pow(2)),
            a.pow(2).mul(x.sub(u).pow(2).add(y.sub(v).pow(2))).scale(16)
                .sub(first.pow(2)).sub(second.pow(2)),
            q.pow(2).mul(d).sub(nxt).sub(q.mul(e)).sub(j),
            lam.pow(2).mul(d).sub(nxt).sub(lam.mul(e.add(h.mul(d))))
                .sub(j.add(h.mul(t)))
        );
        for (int k=0; k<certificates.size(); ++k)
            require(certificates.get(k).terms.isEmpty(), "symbolic certificate " + (k+1));
        require(!x.mul(x).add(Poly.number(1)).sub(x.mul(x)).terms.isEmpty(),
                "normalizer negative control");
        return certificates.size();
    }

    static Rat atanSum(int inverse, int terms) {
        Rat total=Rat.of(0);
        for (int k=0; k<terms; ++k) {
            BigInteger denominator=b(2L*k+1).multiply(b(inverse).pow(2*k+1));
            total=total.add(new Rat(k%2==0 ? ONE : ONE.negate(), denominator));
        }
        return total;
    }

    static Rat[] lambdaBracket() {
        BigInteger base=BigInteger.TEN.pow(30), n=b(5).multiply(base.multiply(base));
        BigInteger root=n.sqrt();
        require(root.multiply(root).compareTo(n)<0
                && n.compareTo(root.add(ONE).pow(2))<0, "strict sqrt(5) bracket");
        Rat phiLow=new Rat(base.add(root), b(2).multiply(base));
        Rat phiHigh=new Rat(base.add(root).add(ONE), b(2).multiply(base));
        Rat piLow=Rat.of(16).mul(atanSum(5,18)).sub(Rat.of(4).mul(atanSum(239,9)));
        Rat piHigh=Rat.of(16).mul(atanSum(5,19)).sub(Rat.of(4).mul(atanSum(239,8)));
        require(Rat.of(3).lt(piLow) && piLow.lt(piHigh) && piHigh.lt(new Rat(22,7)),
                "pi bracket");
        Rat low=phiLow.div(phiLow.add(piHigh)), high=phiHigh.div(phiHigh.add(piLow));
        Rat q=new Rat(Q,S);
        require(q.lt(low) && low.lt(high)
                && high.lt(q.add(new Rat(ONE,BigInteger.TEN.pow(14)))),
                "lambda bracket ordering");
        require(new Rat(b(9295),BigInteger.TEN.pow(19)).lt(low.sub(q))
                && high.sub(q).lt(new Rat(b(9297),BigInteger.TEN.pow(19))), "delta bracket");
        return new Rat[]{low,high};
    }

    record History(List<BigInteger> states, List<BigInteger> remainders, List<Integer> ranks) {}

    static History auditHistory(BigInteger seed, int horizon) {
        natural(seed,"seed");
        if (horizon<0) throw new IllegalArgumentException("negative horizon");
        List<BigInteger> states=new ArrayList<>(), remainders=new ArrayList<>();
        List<Integer> ranks=new ArrayList<>();
        states.add(seed);
        BigInteger qPower=ONE, sPower=ONE, weightedSum=ZERO;
        for (int k=0;k<horizon;++k) {
            BigInteger prior=states.get(states.size()-1);
            Step step=forward(prior);
            require(Q.multiply(prior).equals(S.multiply(step.output()).add(step.remainder())),
                    "step identity");
            require(inverseRemainder(step.output(),step.remainder()).equals(prior),
                    "one-step remainder inverse");
            require(inverseRank(step.output(),step.rank()).equals(prior),
                    "one-step rank inverse");
            weightedSum=Q.multiply(weightedSum).add(step.remainder().multiply(sPower));
            qPower=qPower.multiply(Q);
            sPower=sPower.multiply(S);
            require(qPower.multiply(seed).equals(sPower.multiply(step.output()).add(weightedSum)),
                    "full telescoping prefix identity");
            states.add(step.output());
            remainders.add(step.remainder());
            ranks.add(step.rank());
        }
        BigInteger terminal=states.get(states.size()-1);
        require(recoverRemainders(terminal,remainders).equals(states),
                "complete remainder-history inverse");
        require(recoverRanks(terminal,ranks).equals(states), "complete rank-history inverse");
        return new History(states,remainders,ranks);
    }

    static void expectRejection(Runnable action) {
        try { action.run(); }
        catch (IllegalArgumentException expected) { return; }
        throw new IllegalStateException("malformed input was accepted");
    }

    static LinkedHashMap<String,Long> run() {
        LinkedHashMap<String,Long> result=new LinkedHashMap<>();
        result.put("symbolic_polynomial_identities",(long)symbolicCertificates());
        require(Q.multiply(b(3)).compareTo(S)>0 && Q.multiply(b(2)).compareTo(S)<0,
                "canonical ratio range");
        Rat[] bracket=lambdaBracket();
        Rat low=bracket[0], high=bracket[1];
        for (int i=0;i<=MAX_SEED;++i) {
            BigInteger d=b(i), t=Q.multiply(d).divide(S);
            require(t.multiply(low.d).compareTo(low.n.multiply(d))<=0, "lambda lower floor");
            require(high.n.multiply(d).compareTo(t.add(ONE).multiply(high.d))<0,
                    "lambda upper floor");
        }
        result.put("certified_lambda_floor_states",(long)MAX_SEED+1);
        BigInteger counterexample=b(42189065), t=Q.multiply(counterexample).divide(S);
        require(t.equals(b(14342162)),"counterexample rational floor");
        require(t.add(ONE).multiply(low.d).compareTo(low.n.multiply(counterexample))<=0,
                "counterexample lower bound");
        require(high.n.multiply(counterexample).compareTo(t.add(b(2)).multiply(high.d))<0,
                "counterexample upper bound");
        result.put("out_of_domain_disagreement_examples",1L);

        long predecessorCount=0;
        BigInteger firstTwo=null;
        for (int i=0;i<=MAX_FIBER;++i) {
            BigInteger y=b(i), lo=boundary(y), hi=boundary(y.add(ONE));
            int size=hi.subtract(lo).intValueExact();
            require(size==2 || size==3,"floor fiber cardinality");
            if (size==2 && firstTwo==null) firstTwo=y;
            for (BigInteger d=lo;d.compareTo(hi)<0;d=d.add(ONE)) {
                Step step=forward(d);
                require(step.output().equals(y),"fiber membership");
                require(inverseRank(y,step.rank()).equals(d),"fiber rank inverse");
                require(inverseRemainder(y,step.remainder()).equals(d),"fiber remainder inverse");
                ++predecessorCount;
            }
        }
        for (int i=0;i<3;++i)
            require(forward(b(i)).output().equals(ZERO),"two-bit lower-bound example");
        result.put("consecutive_output_fibers",(long)MAX_FIBER+1);
        result.put("fiber_predecessors",predecessorCount);
        result.put("maximum_fiber_cardinality_proved",3L);
        result.put("optimal_fixed_width_witness_bits_proved",2L);

        int maxExtinction=0;
        int[][] points={{-1,0},{1,0},{0,1},{3,5}};
        for (int i=0;i<=MAX_SEED;++i) {
            BigInteger seed=b(i);
            Step step=forward(seed);
            for (int[] point:points) {
                for (int coordinate:point) {
                    BigInteger p=b(coordinate);
                    require(Q.multiply(seed).multiply(p).equals(
                        S.multiply(step.output()).multiply(p).add(step.remainder().multiply(p))),
                        "geometric coordinate discrepancy");
                }
            }
            if (i>0) {
                Rat a=Rat.of(seed), x=new Rat(seed.multiply(b(2)),b(3));
                Rat y=new Rat(seed.multiply(b(-5)),b(7));
                require(Arrays.equals(recoverPoint(a,distances(a,x,y)),new Rat[]{x,y}),
                        "positive-scale planar recovery");
            }
            History history=auditHistory(seed,HORIZON);
            require(history.states().get(HORIZON).equals(ZERO), "canonical extinction by 23");
            maxExtinction=Math.max(maxExtinction,history.states().indexOf(ZERO));
        }
        result.put("geometric_scale_cases_including_zero",(long)MAX_SEED+1);
        result.put("marked_point_vector_identities",((long)MAX_SEED+1)*points.length);
        result.put("positive_scale_planar_recoveries",(long)MAX_SEED);
        result.put("canonical_transition_checks",((long)MAX_SEED+1)*HORIZON);
        result.put("canonical_telescoping_prefix_checks",((long)MAX_SEED+1)*HORIZON);
        result.put("canonical_full_history_roundtrips_per_witness_type",(long)MAX_SEED+1);
        result.put("maximum_extinction_horizon_observed",(long)maxExtinction);

        for (BigInteger seed:List.of(ZERO,ONE,b(MAX_SEED),ONE.shiftLeft(256).add(b(123))))
            auditHistory(seed,0);
        result.put("zero_horizon_roundtrips",4L);

        long messageCount=0;
        for (int length=0;length<=2;++length) {
            int limit=1<<(8*length);
            for (int value=0;value<limit;++value) {
                byte[] message=new byte[length];
                for (int j=0;j<length;++j) message[length-1-j]=(byte)(value >>> (8*j));
                require(Arrays.equals(decodeMessage(encodeMessage(message)),message),
                        "integer message code");
                require(Arrays.equals(decodeBounded(encodeBounded(message)),message),
                        "bounded-scale code");
                ++messageCount;
            }
        }
        result.put("messages_of_lengths_zero_through_two_per_codec",messageCount);
        byte[] allBytes=new byte[256];
        for (int i=0;i<allBytes.length;++i) allBytes[i]=(byte)i;
        List<byte[]> samples=List.of(new byte[0],new byte[]{0},new byte[]{0,0},
            new byte[]{0,1,(byte)255},"OMEGA".getBytes(StandardCharsets.US_ASCII),
            allBytes,new byte[64]);
        for (byte[] message:samples) {
            History history=auditHistory(encodeMessage(message),HORIZON);
            BigInteger terminal=history.states().get(HORIZON);
            BigInteger nr=recoverRemainders(terminal,history.remainders()).get(0);
            BigInteger nw=recoverRanks(terminal,history.ranks()).get(0);
            require(Arrays.equals(decodeMessage(nr),message),"message remainder pipeline");
            require(Arrays.equals(decodeMessage(nw),message),"message rank pipeline");
        }
        result.put("composed_message_history_roundtrips_per_witness_type",(long)samples.size());

        require(firstTwo!=null,"two-element fiber encountered");
        final BigInteger twoFiber=firstTwo;
        List<Runnable> rejects=List.of(
            ()->forward(b(-1)), ()->inverseRemainder(b(-1),ZERO),
            ()->inverseRemainder(ZERO,b(-1)), ()->inverseRemainder(ZERO,S),
            ()->inverseRemainder(ZERO,ONE), ()->inverseRank(b(-1),0),
            ()->inverseRank(ZERO,-1), ()->inverseRank(ZERO,3),
            ()->inverseRank(twoFiber,2),
            ()->recoverPoint(Rat.of(0),new Rat[]{Rat.of(1),Rat.of(1),Rat.of(1)}),
            ()->recoverPoint(Rat.of(1),new Rat[]{Rat.of(0),Rat.of(0),Rat.of(0)}),
            ()->decodeMessage(ZERO), ()->decodeMessage(b(2)),
            ()->decodeBounded(Rat.of(1)), ()->decodeBounded(Rat.of(2))
        );
        rejects.forEach(OmegaUnifiedProof::expectRejection);
        result.put("malformed_input_cases_rejected",(long)rejects.size());
        return result;
    }

    public static void main(String[] args) {
        if (args.length!=0) throw new IllegalArgumentException("Usage: java OmegaUnifiedProof");
        LinkedHashMap<String,Long> report=run();
        System.out.println("OMEGA_UNIFIED_EXACT_CHECK_V2");
        report.forEach((key,value)->System.out.println(key+"="+value));
        System.out.println("status=PASS");
    }
}