"""D1259 exact verification. All arithmetic is symbolic or rational.
Run without -O. No external data, network calls, floating-point tolerance, or
claim of equivalence to unavailable frozen programme arrays is used.
"""
import sympy as S
import platform
if not __debug__:
    raise SystemExit("Assertions require a run without -O.")
def report(key, value):
    print(key + " = " + str(value))
report("environment", "Python " + platform.python_version() + "; SymPy " + S.__version__)
report("arithmetic", "exact rationals / symbolic polynomials / algebraic radicals")

q=S.Rational
phi=(1+S.sqrt(5))/2
# Route A uses inverse-pair symmetry, separately from Route B's number field.
r=S.symbols('r',positive=True)
normsum=r**2+1+r**-2
assert S.expand((normsum**2-16)*r**4-(r**4-3*r**2+1)*(r**4+5*r**2+1))==0
assert S.simplify(phi**4-3*phi**2+1)==0
report("route_A_polynomial","(r^4-3*r^2+1)*(r^4+5*r^2+1)")
report("route_A_positive_gram_condition","r^2 + r^(-2) = 3")
# Integer recurrence, not approximate powers of phi.
def A(k):
    if k<0: k=-k
    u,v=2,3
    for _ in range(k): u,v=v,3*v-u
    return u
def F(p,q): return 3+A(p)+A(q)+A(p+q)
def exponents(p,q):
    if (p+2*q)%3: return None
    return ((2*p+q)//3,(q-p)//3,-(p+2*q)//3)
def Fexp(ns):
    return 3+sum(A(abs(ns[i]-ns[j])) for i in range(3) for j in range(i+1,3))
report("A_0_through_6",[A(k) for k in range(7)])
x=S.symbols("x")
recurrence=S.expand(x**2-3*x+1)
assert S.simplify(recurrence.subs(x,phi**2))==0
assert A(1)>A(0)>0
# The analytic induction: if v>u>0 then (3v-u)-v = 2v-u>0.
cases=[(p,n-p) for n in range(4) for p in range(n+1) if exponents(p,n-p) is not None]
report("admissible_gaps_with_sum_at_most_3",cases)
assert cases==[(0,0),(1,1),(0,3),(3,0)]
assert [F(*c) for c in cases]==[9,16,41,41]
report("F_for_those_gaps",[F(*c) for c in cases])
# All remaining admissible gaps have p+q >=4, hence bound A4+3+2+2.
tail_bound=A(4)+7
assert tail_bound==54>41
report("tail_lower_bound_for_gap_sum_at_least_4",tail_bound)
# Finite exact control supplements but does not replace the analytic proof.
bound=18
scan=[(p,j,exponents(p,j),F(p,j)) for p in range(bound+1)
      for j in range(bound+1) if exponents(p,j) is not None]
gold=[ns for p,j,ns,f in scan if f==16]
other=[f for p,j,ns,f in scan if (p,j) not in ((0,0),(1,1))]
assert gold==[(1,0,-1)] and min(other)==41
report("finite_control_gap_bound",bound)
report("finite_control_admissible_cases",len(scan))
report("finite_control_F16_exponents",gold)
report("finite_control_other_minimum",min(other))
report("next_gap_value",sorted(set(f for *_,f in scan))[3])
assert Fexp((5,0,-5))==15376 and Fexp((6,-3,-3))==11561
report("rejected_spread_monotonicity_values",(Fexp((5,0,-5)),Fexp((6,-3,-3))))
# Full actual Albert norm from its explicit Cayley-Dickson formula.
# Minimal multiplication suffices for the norm; no frozen arrays imported.
def add(v,w): return tuple(x+y for x,y in zip(v,w))
def neg(v): return tuple(-x for x in v)
def qm(p,r):
    a,b,c,d=p; e,f,g,h=r
    return (a*e-b*f-c*g-d*h,a*f+b*e+c*h-d*g,
            a*g-b*h+c*e+d*f,a*h+b*g-c*f+d*e)
def bar(p): return (p[0],)+neg(p[1:])
def om(x,y):
    p=x[:4];u=(x[7],)+neg(x[4:7]); r=y[:4];v=(y[7],)+neg(y[4:7])
    first=add(qm(p,r),qm(bar(v),u));second=add(qm(v,p),qm(u,bar(r)))
    return first+neg(second[1:])+(second[0],)
def n(x): return sum(v*v for v in x[:4])-sum(v*v for v in x[4:])
X=S.symbols("x0:27")
a,b,c=X[:3];z=X[3:11];y=X[11:19];x=X[19:27]
N=S.expand(a*b*c-a*n(x)-b*n(y)-c*n(z)+2*om(om(z,x),y)[0])
I={v:S.Integer(i<3) for i,v in enumerate(X)}
grad=S.Matrix([S.diff(N,v).subs(I) for v in X])
H=S.hessian((N-1)**2,X).subs(I)
assert H==2*grad*grad.T and H.rank()==1
assert N.subs(I)==1
report("norm_only_test_object","S(X)=(N_Albert(X)-1)^2 at the Albert identity")
report("norm_only_hessian_rank",H.rank())
report("norm_only_hessian_nullity",len(X)-H.rank())
report("frame_orbit_count_and_stronger_variational_pointer","NOT VERIFIED: not computed by this script")
report("result","PASS: analytic-gap control and actual Albert norm-only Hessian")