back to table · edit · history · where entries came from · files · download
4523 bytes, as of the version from 2026-10-30 02:35 (current). Recorded here, not run.
"""Check the two T615 prose repairs with SageMath; performs no writes.
Run: sage -python repair_checks.py
Requires numberdb and the attached generate.py and solver.py alongside it.
Set NUMBERDB_API_KEY for live draft reads, or provide downloaded API documents
as T615-before.json and T614-before.json alongside this script.
Only the analytic n=0,1 controls are recomputed; nonlinear values are unchanged.
"""
import hashlib
import json
from pathlib import Path
import platform
import numberdb.sage as numberdb
# The symbolic checks require full Sage's initialized Maxima interface.
# This is a SageMath check script, not a portable production generator.
from sage.all import SR, sin, sqrt, pi, Infinity, QQ, RealBallField
from sage.version import version as sage_version
from generate import LaneEmdenDensityRatio
base = Path(__file__).resolve().parent
def document(tid):
snapshot = base / (tid + '-before.json')
return json.loads(snapshot.read_text()) if snapshot.exists() else numberdb.table(tid)
def exact_decimal(text):
whole, fraction = text.split('.')
return QQ(int(whole + fraction)) / QQ(10)**len(fraction), QQ(1) / QQ(10)**len(fraction)
def interval_check(text, value):
midpoint, ulp = exact_decimal(text)
B = value.parent()
assert value.is_finite()
assert B(value.rad()) < B(ulp) / 10**20
assert value > B(midpoint - ulp) and value < B(midpoint + ulp)
assert not (value > B(midpoint + 9*ulp) and value < B(midpoint + 11*ulp))
return {'absolute_error_ulps': str(abs(value - B(midpoint)) / B(ulp)),
'stored_interval_contains_ball': True, 'shifted_control_rejected': True}
x = SR.var('x')
theta1 = sin(x) / x
residual1 = (theta1.diff(x, 2) + 2*theta1.diff(x)/x + theta1).simplify_full()
assert residual1 == 0
assert theta1.limit(x=0) == 1
assert theta1.diff(x).limit(x=0) == 0
curvature = theta1.diff(x, 2).limit(x=0)
assert curvature == -QQ(1)/3
assert theta1.subs(x=pi) == 0
mass1 = (-x**2 * theta1.diff(x)).subs(x=pi).simplify_full()
assert mass1 == pi
ratio1 = (pi**3 / (3*mass1)).simplify_full()
assert (ratio1 - pi**2/3).simplify_full() == 0
theta5 = (1 + x**2/3)**(-QQ(1)/2)
residual5 = (theta5.diff(x, 2) + 2*theta5.diff(x)/x + theta5**5).simplify_full()
assert residual5 == 0
assert theta5.limit(x=0) == 1
assert theta5.diff(x).limit(x=0) == 0
mass5 = -x**2*theta5.diff(x)
assert (mass5.diff(x) - x**2*theta5**5).simplify_full() == 0
assert mass5.limit(x=0) == 0
assert (mass5.limit(x=Infinity) - sqrt(3)).simplify_full() == 0
density, mass = document('T615'), document('T614')
g = LaneEmdenDensityRatio()
selected = list(g.enumerate())
assert selected == [{'n': n} for n in density['Numbers']]
assert g.value({'n':'0'}, 100)['number'] == QQ(1)
one = g.value({'n':'1'}, 100)
assert one['comment'] == density['Numbers']['1']['comment'].replace('The linear profile ', 'The index-one profile ')
B = RealBallField(600)
assert one['number'].overlaps(B.pi()**2/3)
row5 = mass['Numbers']['5']
row5 = row5['number'] if isinstance(row5, dict) else row5
evidence = {
'table': 'T615',
'scope': 'Analytic checks for two prose repairs only; no nonlinear ODE recomputation or precision upgrade.',
'skill_manifest': 'agents/runs/20261030T022722Z-repair-skills/manifest.json',
'skill_sha256': {'local': '28ecbeeccb0c5e5d6eb541b5a5b0f88aec47b154374d909085116d34f5629199',
'live': '28ecbeeccb0c5e5d6eb541b5a5b0f88aec47b154374d909085116d34f5629199'},
'source': 'https://arxiv.org/html/1611.07202v1#S2, equations (7)-(10)',
'n1': {'ODE_residual': str(residual1), 'central_second_derivative': str(curvature),
'mass': str(mass1), 'ratio': str(ratio1),
**interval_check(density['Numbers']['1']['number'], B.pi()**2/3)},
'n5': {'ODE_residual': str(residual5), 'mass_at_infinity': str(mass5.limit(x=Infinity)),
'finite_surface': False,
'positivity_reason': 'theta5=(1+x^2/3)^(-1/2)>0 for every finite real x; the positive denominator never vanishes.',
**interval_check(row5, B(3).sqrt())},
'generator': {'enumeration': selected, 'analytic_controls_pass': True,
'n1_comment': one['comment'],
'sha256': hashlib.sha256((base/'generate.py').read_bytes()).hexdigest()},
'argument_uncertainty': 'Exact rational indices. Pi and sqrt(3) are 600-bit Arb enclosures; all arithmetic propagates their uncertainty.',
'versions': {'sage': sage_version, 'python': platform.python_version()},
}
print(json.dumps(evidence, indent=2))