TFPT scientific source excerpt
Original repository path: experiments/theory-contracts/elliptic-moebius-source-bridge-20261026/check_real_boundary_and_modular.py
Original file SHA-256: 03fe91a722026292a2e7a5e59f5fe70ca57cb4fb5d8ad417da3bb17d8268ef05
Inclusive original lines: 1-165
Line numbers below refer to the original source.
This bounded excerpt is source evidence; it is not a new proof/checker run.
Conversation metadata and personal execution details are omitted where indicated.

000001 | """Decisive exact identities for the actual boundary and modular source.
000002 | 
000003 | Analytic boundedness/range and compact bump RP proofs remain in the reports.
000004 | The theta and elliptic evaluations below are diagnostics of those proofs.
000005 | """
000006 | import itertools
000007 | import json
000008 | import sympy as s
000009 | import mpmath as mp
000010 | 
000011 | checks = []
000012 | 
000013 | 
000014 | def need(name, value):
000015 |     if not bool(value):
000016 |         raise RuntimeError(name)
000017 |     checks.append(name)
000018 | 
000019 | 
000020 | x, t, b, y = s.symbols('x t b y')
000021 | I = s.I
000022 | AS = s.Matrix([[0,0,1], [0,1,0], [1,0,0]])
000023 | AT = s.Matrix([[I,0,0], [0,0,1], [0,1,0]])
000024 | U, M = -I*AT, I*AS*AT
000025 | a, bb, c = M**2, M*U**-1, U
000026 | need('finite modular target and marked generators',
000027 |      a**3 == s.eye(3) and bb**2 == s.eye(3)
000028 |      and c**4 == s.eye(3) and a*bb*c == s.eye(3))
000029 | d = bb*c*bb**-1
000030 | need('actual second cusp conjugate word', s.simplify(d-(U*M)**-1) == s.zeros(3))
000031 | need('quotient four puncture Hurwitz product', c*a**2*bb**2*d == s.eye(3))
000032 | phi = -(t-1)**2/(4*t)
000033 | need('degree two source map branch values', s.factor(phi-1) == -(t+1)**2/(4*t))
000034 | need('degree two source map complete critical law',
000035 |      s.simplify(s.diff(phi,t)+(t-1)*(t+1)/(4*t*t)) == 0)
000036 | J = phi.subs(t,x**4)
000037 | need('composed degree eight critical law',
000038 |      s.simplify(s.diff(J,x)+(x**4-1)*(x**4+1)/x**5) == 0)
000039 | need('source map is the original D4 invariant',
000040 |      s.simplify(J.subs(x,I*x)-J) == 0 and s.simplify(J.subs(x,1/x)-J) == 0)
000041 | angle = s.symbols('angle',real=True)
000042 | need('actual marked equator image',
000043 |      s.trigsimp((1-s.cos(4*angle))/2-s.sin(2*angle)**2) == 0)
000044 | need('degree eight full ramification sum', 4+4+2*3 == 2*8-2)
000045 | prod = s.eye(3)
000046 | for k in range(4):
000047 |     prod = s.simplify(prod*U**k*M*U**(-k))
000048 | need('all four Schreier peripheral matrices', prod == s.eye(3))
000049 | Tfull = s.Matrix([[1,1], [0,1]])
000050 | need('full modular cusp remains nontrivial', Tfull**4 != s.eye(2))
000051 | 
000052 | # Rigidity test in the expressly specified genuine unitary D4 orbifold class.
000053 | omega = (-1+I*s.sqrt(3))/2
000054 | root_traces = {s.simplify(e[0]+e[1]*omega**2+e[2]*omega)
000055 |                for e in [(1,1,1),(1,-1,-1),(-1,1,-1),(-1,-1,1)]}
000056 | need('four determinant one half meridian branches',
000057 |      root_traces == {s.Integer(0),s.Integer(2),-1+I*s.sqrt(3),-1-I*s.sqrt(3)})
000058 | need('nonzero trace branches are impossible or reducible',
000059 |      (s.re(s.Integer(2))+1)/2 > 1
000060 |      and (s.re(-1+I*s.sqrt(3))+1)/2 == 0
000061 |      and (s.re(-1-I*s.sqrt(3))+1)/2 == 0)
000062 | v0 = s.Matrix([1/s.sqrt(2),s.Rational(1,2),s.Rational(1,2)])
000063 | b0 = 2*v0*v0.H-s.eye(3)
000064 | targetU = s.diag(1,I,-I)
000065 | a0 = (b0*targetU)**-1
000066 | need('forced irreducible branch representative',
000067 |      s.simplify(b0**2) == s.eye(3) and s.simplify(a0**3) == s.eye(3))
000068 | D = s.diag(1,-(1+I)/s.sqrt(2),(1-I)/s.sqrt(2))
000069 | targetM = s.Matrix([[0,-(1+I)/2,(1-I)/2],
000070 |                     [-(1+I)/2,-I/2,-s.Rational(1,2)],
000071 |                     [(1-I)/2,-s.Rational(1,2),I/2]])
000072 | need('forced representative has exact original marked v117 pair',
000073 |      s.simplify(D*a0**2*D.H-targetM) == s.zeros(3)
000074 |      and s.simplify(D*targetU*D.H-targetU) == s.zeros(3))
000075 | 
000076 | # Tate normal form and its actual critical law, not a fitted j value.
000077 | F = y*y+(x+b)*y-x*x*(x+b)
000078 | critical = 16*x*x+(16*b+3)*x+4*b
000079 | need('Tate critical substitution',
000080 |      s.factor(F.subs(y,4*x*(x+b))-x*(x+b)*critical) == 0)
000081 | need('triple critical point parameter',
000082 |      s.factor(s.discriminant(critical,x)) == (16*b-9)*(16*b-1))
000083 | b0 = s.Rational(9,16)
000084 | c4 = 1-16*b+16*b*b
000085 | delta = b**4*(1-16*b)
000086 | jval = s.factor((c4**3/delta).subs(b,b0))
000087 | need('unique smooth branch and distinct elliptic invariant',
000088 |      delta.subs(b,s.Rational(1,16)) == 0
000089 |      and delta.subs(b,b0) != 0
000090 |      and jval == s.Rational(207646,6561) and jval != 1728)
000091 | special = {b:b0,x:-s.Rational(3,8),y:-s.Rational(9,32)}
000092 | need('actual triple branch point and value',
000093 |      F.subs(special) == 0
000094 |      and (y*y/(x+b)).subs(special) == s.Rational(27,64))
000095 | 
000096 | 
000097 | def compose(p,q):
000098 |     return tuple(p[q[i]] for i in range(4))
000099 | 
000100 | 
000101 | def inv(p):
000102 |     return tuple(p.index(i) for i in range(4))
000103 | 
000104 | 
000105 | def ctype(p):
000106 |     unseen, lengths = set(range(4)), []
000107 |     while unseen:
000108 |         start = next(iter(unseen))
000109 |         cur, count = start, 0
000110 |         while cur in unseen:
000111 |             unseen.remove(cur)
000112 |             count += 1
000113 |             cur = p[cur]
000114 |         lengths.append(count)
000115 |     return sorted(lengths)
000116 | 
000117 | 
000118 | perms = list(itertools.permutations(range(4)))
000119 | four = [p for p in perms if ctype(p)==[4]]
000120 | three = [p for p in perms if ctype(p)==[1,3]]
000121 | triples = [(p,q,inv(compose(p,q))) for p in four for q in three
000122 |            if ctype(inv(compose(p,q)))==[4]]
000123 | first = triples[0]
000124 | orbit = {tuple(compose(compose(k,p),inv(k)) for p in first) for k in perms}
000125 | need('unique ordered S4 Nielsen class', len(triples)==24 and set(triples)==orbit)
000126 | need('elliptic source and normal closure genus',
000127 |      -8+3+2+3 == 0 and 24*(-2+s.Rational(3,4)+s.Rational(2,3)+s.Rational(3,4)) == 4)
000128 | 
000129 | # Exact beta moment: gamma recurrence first, reflection identity afterwards.
000130 | r = s.Rational
000131 | moment0 = s.gamma(r(1,4))*s.gamma(r(3,4))/s.pi
000132 | moment2 = (s.gamma(r(3,4))*s.gamma(r(5,4))
000133 |            -s.gamma(r(7,4))*s.gamma(r(1,4)))/s.pi
000134 | need('nonorthogonality Fourier coefficient by beta recurrence',
000135 |      s.simplify(s.expand_func(moment2/moment0)) == -s.Rational(1,2))
000136 | need('reflection formula gives exact nonzero overlap',
000137 |      s.simplify((-s.Rational(1,2))/s.sin(s.pi/4)+1/s.sqrt(2)) == 0)
000138 | L = s.beta(r(1,4),r(1,2))/4
000139 | edge_length = s.beta(r(1,4),r(1,2))/(8*L)
000140 | need('intrinsic edge and full face lengths', edge_length == r(1,2) and 4*edge_length == 2)
000141 | need('intrinsic speed fails fixed base winding Ward', s.sqrt(2)/2 != 1)
000142 | 
000143 | mp.mp.dps = 70
000144 | nome = mp.exp(-mp.pi)
000145 | theta = lambda w: (1j/2)*mp.jtheta(3,mp.pi*w,nome)*mp.jtheta(1,0,nome,1)/(mp.jtheta(3,0,nome)*mp.jtheta(1,mp.pi*w,nome))
000146 | tt = mp.mpf(1)/4
000147 | sp, sm = theta(1j*tt), theta(-1j*tt)
000148 | fourier = sum(mp.exp(-tt*(2*mp.pi*(mp.mpf(n)+mp.mpf('.5'))))/(1+mp.exp(-2*mp.pi*(mp.mpf(n)+mp.mpf('.5')))) for n in range(-100,101))
000149 | if abs(sp-fourier)>mp.mpf('1e-60') or abs(sm+sp)>mp.mpf('1e-60'):
000150 |     raise RuntimeError('actual theta and NS Fourier diagnostic')
000151 | if not (abs(sp.imag)<mp.mpf('1e-60') and sp.real>0 and sm.real<0):
000152 |     raise RuntimeError('charged reflection sign diagnostic')
000153 | cc = 2*mp.ellipk(-1)*(1+1j)
000154 | pts = [mp.mpc('.375','.5'),mp.mpc('.125','0')]
000155 | absx = [abs(mp.ellipfun('sn',cc*z,-1)) for z in pts]
000156 | if not all(v<1 for v in absx):
000157 |     raise RuntimeError('checker face point positions')
000158 | 
000159 | print(json.dumps(dict(verdict='PASS_SCOPED',exact_checks=len(checks),checks=checks,
000160 |     theta_fourier_error=mp.nstr(abs(sp-fourier),8),
000161 |     neutral_reflection_point_diagnostic=mp.nstr((sp*sm).real,16),
000162 |     actual_inside_face_abs_x=[mp.nstr(v,12) for v in absx],
000163 |     j_of_degree_four_source=str(jval),
000164 |     compact_bump_and_outer_proofs='analytical reports; not finite grid extrapolation',
000165 |     complete_TFPT_solution=False),indent=2))