- Positive-cone transport certificates (p28_positive_cone.py, POSITIVE_CONE_CERTIFICATE.md, POSITIVE_CONE_MANUSCRIPT_SECTION.tex) - Optimized differential gauge (p28_optimized_gauge.py, OPTIMIZED_GAUGE_CERTIFICATE.md) - Adversarial provenance supplements (p28_mutation_sensitivity.py, solution_pre_positive_cone.tex) - FAMM SCARS advisory records (FAMM_SCARS.md, p28_famm_scars.json, p28_famm_scars_validator.py) - Overview documentation (OPTIONAL_IMPROVEMENTS.md, ADVERSARIAL_AUDIT.md) These are independent, replayable supplements developed after the original exact closure. They can be verified independently with 'bash run_checks.sh' in the certificates directory.
663 lines
20 KiB
Python
663 lines
20 KiB
Python
#!/usr/bin/env python3
|
|
"""Dependency-free positive-cone certificate for Problem 2.8.
|
|
|
|
This verifier constructs the authoritative deformed transfer matrix exactly
|
|
at x=1/R, balances it, and conjugates it by the Pascal matrix:
|
|
|
|
T_m = P * B_m * P^(-1).
|
|
|
|
With k=m-1 and s=R-4, every entry is checked coefficientwise against an
|
|
explicit rational function N_ij(k,s)/D_ij(m,R). Every coefficient of every
|
|
N_ij and D_ij is strictly positive, proving T_m>0 for m>=1 and R>=4.
|
|
|
|
The script also checks:
|
|
|
|
* both official seed rows enter this cone after the first transfer;
|
|
* the displayed positive limiting matrix is the exact limit of T_m; and
|
|
* specialization at the official R reproduces both official integer rows.
|
|
|
|
Only ``fractions.Fraction`` and sparse coefficient dictionaries are used.
|
|
There is no polynomial division, factorization, simplifier, root finder,
|
|
eigenvalue routine, numerical approximation, or finite sampling.
|
|
"""
|
|
|
|
from fractions import Fraction as F
|
|
|
|
|
|
class Poly:
|
|
"""Sparse polynomials in (k,s), represented by exponent pairs."""
|
|
|
|
__slots__ = ("terms",)
|
|
|
|
def __init__(self, terms=None):
|
|
normalized = {}
|
|
source = terms or {}
|
|
items = source.items() if hasattr(source, "items") else source
|
|
for exponent, coefficient in items:
|
|
coefficient = F(coefficient)
|
|
if coefficient:
|
|
normalized[tuple(exponent)] = (
|
|
normalized.get(tuple(exponent), F(0)) + coefficient
|
|
)
|
|
self.terms = {
|
|
exponent: coefficient
|
|
for exponent, coefficient in normalized.items()
|
|
if coefficient
|
|
}
|
|
|
|
@staticmethod
|
|
def constant(value):
|
|
value = F(value)
|
|
return Poly({(0, 0): value}) if value else Poly()
|
|
|
|
def __add__(self, other):
|
|
other = as_poly(other)
|
|
return Poly(list(self.terms.items()) + list(other.terms.items()))
|
|
|
|
__radd__ = __add__
|
|
|
|
def __neg__(self):
|
|
return Poly({exponent: -coefficient for exponent, coefficient in self.terms.items()})
|
|
|
|
def __sub__(self, other):
|
|
return self + (-as_poly(other))
|
|
|
|
def __rsub__(self, other):
|
|
return as_poly(other) - self
|
|
|
|
def __mul__(self, other):
|
|
if isinstance(other, Rat):
|
|
return other * self
|
|
other = as_poly(other)
|
|
terms = {}
|
|
for (ak, ass), ac in self.terms.items():
|
|
for (bk, bss), bc in other.terms.items():
|
|
exponent = (ak + bk, ass + bss)
|
|
terms[exponent] = terms.get(exponent, F(0)) + ac * bc
|
|
return Poly(terms)
|
|
|
|
__rmul__ = __mul__
|
|
|
|
def __pow__(self, exponent):
|
|
if exponent < 0:
|
|
return Rat(1, self ** (-exponent))
|
|
result = Poly.constant(1)
|
|
base = self
|
|
power = exponent
|
|
while power:
|
|
if power & 1:
|
|
result = result * base
|
|
base = base * base
|
|
power //= 2
|
|
return result
|
|
|
|
def __truediv__(self, other):
|
|
return Rat(self, as_poly(other))
|
|
|
|
def __rtruediv__(self, other):
|
|
return Rat(as_poly(other), self)
|
|
|
|
def __eq__(self, other):
|
|
return self.terms == as_poly(other).terms
|
|
|
|
def all_coefficients_positive(self):
|
|
return bool(self.terms) and all(value > 0 for value in self.terms.values())
|
|
|
|
def evaluate(self, k_value, s_value):
|
|
k_value = F(k_value)
|
|
s_value = F(s_value)
|
|
return sum(
|
|
coefficient * k_value**k_degree * s_value**s_degree
|
|
for (k_degree, s_degree), coefficient in self.terms.items()
|
|
)
|
|
|
|
def leading_in_k(self):
|
|
if not self.terms:
|
|
return -1, Poly()
|
|
degree = max(exponent[0] for exponent in self.terms)
|
|
coefficient = Poly(
|
|
{
|
|
(0, s_degree): value
|
|
for (k_degree, s_degree), value in self.terms.items()
|
|
if k_degree == degree
|
|
}
|
|
)
|
|
return degree, coefficient
|
|
|
|
|
|
def as_poly(value):
|
|
if isinstance(value, Poly):
|
|
return value
|
|
if isinstance(value, Rat):
|
|
if value.denominator == Poly.constant(1):
|
|
return value.numerator
|
|
raise TypeError("cannot coerce a non-polynomial rational function to Poly")
|
|
return Poly.constant(value)
|
|
|
|
|
|
class Rat:
|
|
"""Unsimplified rational functions; equality is by cross multiplication."""
|
|
|
|
__slots__ = ("numerator", "denominator")
|
|
|
|
def __init__(self, numerator=0, denominator=1):
|
|
if isinstance(numerator, Rat):
|
|
if denominator != 1:
|
|
raise TypeError("nested rational denominator")
|
|
self.numerator = numerator.numerator
|
|
self.denominator = numerator.denominator
|
|
return
|
|
self.numerator = as_poly(numerator)
|
|
self.denominator = as_poly(denominator)
|
|
if not self.denominator.terms:
|
|
raise ZeroDivisionError("zero polynomial denominator")
|
|
|
|
def __add__(self, other):
|
|
other = as_rat(other)
|
|
if self.denominator == other.denominator:
|
|
return Rat(self.numerator + other.numerator, self.denominator)
|
|
return Rat(
|
|
self.numerator * other.denominator
|
|
+ other.numerator * self.denominator,
|
|
self.denominator * other.denominator,
|
|
)
|
|
|
|
__radd__ = __add__
|
|
|
|
def __neg__(self):
|
|
return Rat(-self.numerator, self.denominator)
|
|
|
|
def __sub__(self, other):
|
|
return self + (-as_rat(other))
|
|
|
|
def __rsub__(self, other):
|
|
return as_rat(other) - self
|
|
|
|
def __mul__(self, other):
|
|
other = as_rat(other)
|
|
return Rat(
|
|
self.numerator * other.numerator,
|
|
self.denominator * other.denominator,
|
|
)
|
|
|
|
__rmul__ = __mul__
|
|
|
|
def __truediv__(self, other):
|
|
other = as_rat(other)
|
|
return Rat(
|
|
self.numerator * other.denominator,
|
|
self.denominator * other.numerator,
|
|
)
|
|
|
|
def __rtruediv__(self, other):
|
|
return as_rat(other) / self
|
|
|
|
def __pow__(self, exponent):
|
|
if exponent < 0:
|
|
return Rat(
|
|
self.denominator ** (-exponent),
|
|
self.numerator ** (-exponent),
|
|
)
|
|
return Rat(self.numerator**exponent, self.denominator**exponent)
|
|
|
|
def __eq__(self, other):
|
|
other = as_rat(other)
|
|
return (
|
|
self.numerator * other.denominator
|
|
== other.numerator * self.denominator
|
|
)
|
|
|
|
def evaluate(self, k_value, s_value):
|
|
denominator = self.denominator.evaluate(k_value, s_value)
|
|
if not denominator:
|
|
raise ZeroDivisionError("specialized denominator vanishes")
|
|
return self.numerator.evaluate(k_value, s_value) / denominator
|
|
|
|
def limit_in_k(self):
|
|
numerator_degree, numerator_lead = self.numerator.leading_in_k()
|
|
denominator_degree, denominator_lead = self.denominator.leading_in_k()
|
|
if numerator_degree < denominator_degree:
|
|
return Rat(0)
|
|
if numerator_degree > denominator_degree:
|
|
raise AssertionError("rational function diverges as k tends to infinity")
|
|
return Rat(numerator_lead, denominator_lead)
|
|
|
|
|
|
def as_rat(value):
|
|
return value if isinstance(value, Rat) else Rat(value)
|
|
|
|
|
|
def matrix_multiply(left, right):
|
|
rows = len(left)
|
|
inner = len(right)
|
|
columns = len(right[0])
|
|
assert all(len(row) == inner for row in left)
|
|
return [
|
|
[
|
|
sum(
|
|
(as_rat(left[i][h]) * as_rat(right[h][j]) for h in range(inner)),
|
|
Rat(0),
|
|
)
|
|
for j in range(columns)
|
|
]
|
|
for i in range(rows)
|
|
]
|
|
|
|
|
|
def row_matrix_multiply(row, matrix):
|
|
return matrix_multiply([row], matrix)[0]
|
|
|
|
|
|
def polynomial_from_coefficient_rows(rows):
|
|
"""Rows are indexed by k-degree; entries by s-degree."""
|
|
return Poly(
|
|
{
|
|
(k_degree, s_degree): coefficient
|
|
for k_degree, row in enumerate(rows)
|
|
for s_degree, coefficient in enumerate(row)
|
|
if coefficient
|
|
}
|
|
)
|
|
|
|
|
|
k = Poly({(1, 0): 1})
|
|
s = Poly({(0, 1): 1})
|
|
m = k + 1
|
|
R = s + 4
|
|
|
|
|
|
def authoritative_matrix(u, parameter_R):
|
|
"""The exact Problem 2.8 transfer at x=1/R."""
|
|
omega = u * (3 * u - 2) * (3 * u + 2)
|
|
|
|
a1 = parameter_R * (144*u**5 - 288*u**4 + 144*u**3) + (
|
|
-99*u**5 + 333*u**4 - 229*u**3 - 114*u**2 + 40*u + 64
|
|
)
|
|
a2 = parameter_R * (432*u**4 - 864*u**3 + 432*u**2) + (
|
|
-243*u**4 + 909*u**3 - 868*u**2 - 80*u + 272
|
|
)
|
|
a3 = parameter_R * (432*u**3 - 864*u**2 + 432*u) + (
|
|
-153*u**3 + 648*u**2 - 860*u + 360
|
|
)
|
|
a4 = parameter_R * 144 * (u - 1)**2
|
|
|
|
b1 = parameter_R * (-144*u**3) + (
|
|
9*u**4 + 63*u**3 + 158*u**2 + 168*u + 64
|
|
)
|
|
b2 = parameter_R * (216*u**2) + (
|
|
36*u**3 - 189*u**2 - 316*u - 168
|
|
)
|
|
b3 = parameter_R * (108*u) + (54*u**2 - 189*u - 158)
|
|
|
|
c1 = (
|
|
parameter_R**2 * (-288*u**3)
|
|
+ parameter_R * (54*u**4 + 378*u**3 + 948*u**2 + 1008*u + 384)
|
|
+ (18*u**5 + 45*u**4 - 251*u**3 - 1086*u**2 - 1384*u - 576)
|
|
)
|
|
c2 = (
|
|
parameter_R**2 * (-432*u**2)
|
|
+ parameter_R * (153*u**4 - 657*u**3 + 1292*u**2 + 2064*u + 1072)
|
|
+ (-72*u**4 + 702*u**3 - 1069*u**2 - 2508*u - 1512)
|
|
)
|
|
c3 = (
|
|
parameter_R**2 * (-216*u)
|
|
+ parameter_R * (180*u**3 - 891*u**2 + 1450*u + 1116)
|
|
+ (-108*u**3 + 864*u**2 - 1385*u - 1422)
|
|
)
|
|
c4 = (
|
|
parameter_R**2 * (-4)
|
|
+ parameter_R * (6*u**2 - 33*u + F(536, 9))
|
|
+ (-4*u**2 + 32*u - 63)
|
|
)
|
|
|
|
return [
|
|
[a1/omega, a2/omega, a3/omega, a4/omega],
|
|
[-u**3, -3*u**2, -3*u, -1],
|
|
[
|
|
b1/(144*parameter_R),
|
|
-b2/(72*parameter_R),
|
|
-b3/(36*parameter_R),
|
|
(-2*parameter_R-(2*u-7))/(2*parameter_R),
|
|
],
|
|
[
|
|
c1/(288*parameter_R**2),
|
|
c2/(144*parameter_R**2),
|
|
c3/(72*parameter_R**2),
|
|
c4/(4*parameter_R**2),
|
|
],
|
|
]
|
|
|
|
|
|
PASCAL = [
|
|
[1, 0, 0, 0],
|
|
[1, 1, 0, 0],
|
|
[1, 2, 1, 0],
|
|
[1, 3, 3, 1],
|
|
]
|
|
PASCAL_INVERSE = [
|
|
[1, 0, 0, 0],
|
|
[-1, 1, 0, 0],
|
|
[1, -2, 1, 0],
|
|
[-1, 3, -3, 1],
|
|
]
|
|
|
|
|
|
OBLIGATIONS = {}
|
|
|
|
|
|
def obligation(group, condition):
|
|
if not condition:
|
|
raise AssertionError("failed obligation in group: " + group)
|
|
OBLIGATIONS[group] = OBLIGATIONS.get(group, 0) + 1
|
|
|
|
|
|
obligation(
|
|
"Pascal inverse",
|
|
matrix_multiply(PASCAL, PASCAL_INVERSE)
|
|
== [[Rat(int(i == j)) for j in range(4)] for i in range(4)],
|
|
)
|
|
|
|
|
|
# Build B_m and T_m=P*B_m*P^(-1) exactly with m=k+1 and R=s+4.
|
|
M = authoritative_matrix(2*m + 3, R)
|
|
balanced = [
|
|
[
|
|
as_rat(M[i][j]) * (m+1)**j / m**i / (m+1)**2
|
|
for j in range(4)
|
|
]
|
|
for i in range(4)
|
|
]
|
|
T = matrix_multiply(matrix_multiply(PASCAL, balanced), PASCAL_INVERSE)
|
|
|
|
|
|
# Explicit coefficient arrays for N_ij(k,s). The outer list is indexed by
|
|
# k-degree and each inner list by s-degree.
|
|
NUMERATOR_COEFFICIENTS = [
|
|
[
|
|
[
|
|
[209067, 62208],
|
|
[409482, 124416],
|
|
[318165, 98496],
|
|
[122806, 38592],
|
|
[23580, 7488],
|
|
[1800, 576],
|
|
],
|
|
[
|
|
[216214, 62208],
|
|
[351120, 103680],
|
|
[210784, 63936],
|
|
[55584, 17280],
|
|
[5472, 1728],
|
|
],
|
|
[
|
|
[76079, 20736],
|
|
[98882, 27648],
|
|
[41796, 12096],
|
|
[5688, 1728],
|
|
],
|
|
[
|
|
[18432, 4608],
|
|
[27648, 6912],
|
|
[13824, 3456],
|
|
[2304, 576],
|
|
],
|
|
],
|
|
[
|
|
[
|
|
[44808, 15552],
|
|
[93312, 31104],
|
|
[62208, 20736],
|
|
[17280, 5760],
|
|
[1728, 576],
|
|
],
|
|
[
|
|
[186379, 62208],
|
|
[511210, 165888],
|
|
[519853, 167616],
|
|
[250678, 81216],
|
|
[58140, 19008],
|
|
[5256, 1728],
|
|
],
|
|
[
|
|
[66134, 20736],
|
|
[159568, 48384],
|
|
[131792, 39744],
|
|
[45216, 13824],
|
|
[5472, 1728],
|
|
],
|
|
[
|
|
[16222, 4608],
|
|
[42291, 11520],
|
|
[39050, 10368],
|
|
[15444, 4032],
|
|
[2232, 576],
|
|
],
|
|
],
|
|
[
|
|
[
|
|
[12995117, 8841456, 1492992],
|
|
[58685630, 37561608, 5971968],
|
|
[103594644, 64078200, 9828864],
|
|
[94855680, 57551496, 8640000],
|
|
[49440456, 29668248, 4396032],
|
|
[14835888, 8843664, 1299456],
|
|
[2392416, 1419552, 207360],
|
|
[160704, 95040, 13824],
|
|
],
|
|
[
|
|
[39423757, 27038952, 4478976],
|
|
[166410214, 105688080, 16422912],
|
|
[262665540, 160189416, 24012288],
|
|
[203963976, 121854816, 17915904],
|
|
[83704320, 49549824, 7216128],
|
|
[17449344, 10295424, 1492992],
|
|
[1461888, 860544, 124416],
|
|
],
|
|
[
|
|
[6744221, 4650768, 746496],
|
|
[26619818, 16612236, 2488320],
|
|
[37076724, 21985452, 3172608],
|
|
[23503608, 13602888, 1928448],
|
|
[6902496, 3967056, 559872],
|
|
[756864, 438048, 62208],
|
|
],
|
|
[
|
|
[87786, 60468, 9216],
|
|
[369593, 226474, 32256],
|
|
[559242, 320520, 43776],
|
|
[393892, 216608, 28800],
|
|
[131832, 70560, 9216],
|
|
[16992, 8928, 1152],
|
|
],
|
|
],
|
|
[
|
|
[
|
|
[33051981, 55702072, 23898528, 2985984],
|
|
[327240514, 376865532, 134112240, 14929920],
|
|
[930970540, 937602272, 303903216, 31601664],
|
|
[1279073232, 1205376648, 370469520, 36937728],
|
|
[994303368, 902431272, 268543536, 26072064],
|
|
[461588688, 409453104, 119369664, 11390976],
|
|
[127105056, 111089760, 31948032, 3013632],
|
|
[19185984, 16597440, 4727808, 442368],
|
|
[1223424, 1050624, 297216, 27648],
|
|
],
|
|
[
|
|
[124354341, 177927470, 72724752, 8957952],
|
|
[1045995002, 1120727784, 383156784, 41803776],
|
|
[2641611740, 2536092136, 794391552, 80870400],
|
|
[3164847768, 2875298832, 858173328, 83856384],
|
|
[2060023392, 1815713424, 527093136, 50264064],
|
|
[748445184, 648617760, 185300064, 17418240],
|
|
[142860672, 122627520, 34706880, 3234816],
|
|
[11197440, 9548928, 2685312, 248832],
|
|
],
|
|
[
|
|
[26276833, 32297441, 12409344, 1492992],
|
|
[188851718, 188046502, 61107192, 6469632],
|
|
[420585148, 383136068, 114774408, 11321856],
|
|
[431847432, 375502536, 107664480, 10202112],
|
|
[225990144, 191691072, 53691264, 4976640],
|
|
[58320000, 48926592, 13561344, 1244160],
|
|
[5847552, 4904064, 1358208, 124416],
|
|
],
|
|
[
|
|
[3759202, 4035454, 1433736, 165888],
|
|
[25198317, 23609115, 7287084, 746496],
|
|
[57385334, 50066438, 14346252, 1368576],
|
|
[62533980, 52200252, 14310108, 1306368],
|
|
[35688168, 28926216, 7710120, 684288],
|
|
[10310976, 8188128, 2142288, 186624],
|
|
[1192320, 933120, 241056, 20736],
|
|
],
|
|
],
|
|
]
|
|
|
|
N = [
|
|
[polynomial_from_coefficient_rows(NUMERATOR_COEFFICIENTS[i][j]) for j in range(4)]
|
|
for i in range(4)
|
|
]
|
|
|
|
g = (2*m+3) * (6*m+7) * (6*m+11)
|
|
D = [
|
|
[(m+1)**2*g, (m+1)*g, g, g],
|
|
[m*g, m*(m+1)*g, m*g, m*g],
|
|
[
|
|
24*m**2*(m+1)**2*g*R,
|
|
72*m**2*(m+1)*g*R,
|
|
36*m**2*g*R,
|
|
2*m**2*g*R,
|
|
],
|
|
[
|
|
48*m**3*(m+1)**2*g*R**2,
|
|
144*m**3*(m+1)*g*R**2,
|
|
72*m**3*g*R**2,
|
|
36*m**3*g*R**2,
|
|
],
|
|
]
|
|
|
|
for i in range(4):
|
|
for j in range(4):
|
|
obligation("16 transfer identities", T[i][j] == Rat(N[i][j], D[i][j]))
|
|
obligation("16 positive numerators", N[i][j].all_coefficients_positive())
|
|
obligation("16 positive denominators", D[i][j].all_coefficients_positive())
|
|
|
|
|
|
# Exact positive limiting matrix P*S*P^(-1).
|
|
LIMIT = [
|
|
[8*R-7, 4*(6*R-5), 24*R-17, 8*R],
|
|
[8*(R-1), 24*R-23, 4*(6*R-5), 8*R-1],
|
|
[
|
|
(R-1)*(8*R-1)/R,
|
|
2*(R-1)*(12*R-1)/R,
|
|
24*R-23,
|
|
2*(4*R**2-R-1)/R,
|
|
],
|
|
[
|
|
2*(R-1)*(4*R**2-R-1)/R**2,
|
|
(R-1)*(24*R**2-5*R-4)/R**2,
|
|
2*(R-1)*(12*R-1)/R,
|
|
(8*R**3-3*R**2-4)/R**2,
|
|
],
|
|
]
|
|
|
|
for i in range(4):
|
|
for j in range(4):
|
|
actual_limit = T[i][j].limit_in_k()
|
|
expected_limit = as_rat(LIMIT[i][j])
|
|
obligation("16 limiting-matrix identities", actual_limit == expected_limit)
|
|
obligation(
|
|
"16 positive limiting entries",
|
|
expected_limit.numerator.all_coefficients_positive()
|
|
and expected_limit.denominator.all_coefficients_positive(),
|
|
)
|
|
|
|
|
|
# Official seed rows and their first positive-cone states.
|
|
CHUD_A = 13_591_409
|
|
CHUD_B = 545_140_134
|
|
CHUD_S = 426_880
|
|
|
|
compact_denominator = [
|
|
18*R + F(159, 4),
|
|
54*R + F(131, 2),
|
|
54*R + 27,
|
|
18*R,
|
|
]
|
|
h0 = [CHUD_A+CHUD_B, CHUD_B, 0, 0]
|
|
seed_a1 = [CHUD_S*entry for entry in compact_denominator]
|
|
seed_a0 = [
|
|
CHUD_A*compact_denominator[index] - F(5, 4)*h0[index]
|
|
for index in range(4)
|
|
]
|
|
|
|
M0 = authoritative_matrix(Poly.constant(3), R)
|
|
cone_a1 = row_matrix_multiply(row_matrix_multiply(seed_a1, M0), PASCAL_INVERSE)
|
|
cone_a0 = row_matrix_multiply(row_matrix_multiply(seed_a0, M0), PASCAL_INVERSE)
|
|
|
|
EXPECTED_CONE_A1 = [
|
|
Rat(320160*polynomial_from_coefficient_rows([[451657, 259168, 36864]]), 77),
|
|
Rat(213440*polynomial_from_coefficient_rows([[1045771, 591288, 82944]]), 77),
|
|
Rat(3841920*polynomial_from_coefficient_rows([[30075, 16706, 2304]]), 77),
|
|
Rat(7683840*polynomial_from_coefficient_rows([[2612, 1421, 192]]), 77),
|
|
]
|
|
EXPECTED_CONE_A0 = [
|
|
Rat(polynomial_from_coefficient_rows([[13563858344917, 18828949838688, 4509303312384]]), 924),
|
|
Rat(2*polynomial_from_coefficient_rows([[2606908232573, 3613607517834, 845494371072]]), 231),
|
|
Rat(polynomial_from_coefficient_rows([[3584820267815, 4955797147464, 1127325828096]]), 308),
|
|
Rat(3*polynomial_from_coefficient_rows([[103400761441, 142363659388, 31314606336]]), 154),
|
|
]
|
|
|
|
for actual, expected in zip(cone_a1, EXPECTED_CONE_A1):
|
|
obligation("8 seed-cone identities", actual == expected)
|
|
obligation(
|
|
"8 positive seed coordinates",
|
|
expected.numerator.all_coefficients_positive()
|
|
and expected.denominator.all_coefficients_positive(),
|
|
)
|
|
for actual, expected in zip(cone_a0, EXPECTED_CONE_A0):
|
|
obligation("8 seed-cone identities", actual == expected)
|
|
obligation(
|
|
"8 positive seed coordinates",
|
|
expected.numerator.all_coefficients_positive()
|
|
and expected.denominator.all_coefficients_positive(),
|
|
)
|
|
|
|
|
|
R_OFFICIAL = 151_931_373_056_001
|
|
S_OFFICIAL = R_OFFICIAL - 4
|
|
OFFICIAL_A0 = [
|
|
37169305760442252761441,
|
|
111507917281327441564208,
|
|
111507917281327599720129,
|
|
37169305760442410917362,
|
|
]
|
|
OFFICIAL_A1 = [
|
|
1167416361542639692320,
|
|
3502249084627896132160,
|
|
3502249084627879697280,
|
|
1167416361542622723840,
|
|
]
|
|
|
|
obligation(
|
|
"official coefficient relation",
|
|
9*236_337_691_420_383 == 14*R_OFFICIAL - 567,
|
|
)
|
|
obligation(
|
|
"2 official seed specializations",
|
|
[as_rat(entry).evaluate(0, S_OFFICIAL) for entry in seed_a0] == OFFICIAL_A0,
|
|
)
|
|
obligation(
|
|
"2 official seed specializations",
|
|
[as_rat(entry).evaluate(0, S_OFFICIAL) for entry in seed_a1] == OFFICIAL_A1,
|
|
)
|
|
|
|
|
|
total = sum(OBLIGATIONS.values())
|
|
print("PASS: exact positive-cone certificate")
|
|
for group, count in OBLIGATIONS.items():
|
|
print(f"PASS: {group}: {count}")
|
|
print(f"PASS: {total} exact obligations")
|
|
print("T_m=P*B_m*P^(-1) is entrywise positive for every m>=1 and R>=4")
|
|
print("Both official seed rows enter the same positive cone after one transfer")
|
|
print("No sampling, factorizer, simplifier, root finder, or eigenvalue routine was used")
|