✓
Passing This code compiles and runs correctly.
Code
import std/io
import std/sym
// theorem-derived cert for sqrt(1+x): 2(1+x)g' - g = 0
std/sym:lit(√((1e0+x)))
| exact a |> std/sym:cert-of(a)
| exact c |> std/io:print.ln("{{ c:s }}")
| not-holonomic m |> std/io:print.ln("nh:{{ m:s }}")
| bad m |> std/io:print.ln("bad:{{ m:s }}")
| bad |> std/io:print.ln("bad-lit")
// certified series: seeds exact, tail generated by the recurrence
std/sym:lit(√((1e0+x)))
| exact a |> std/sym:cert-series(a, terms: 8)
| exact c |> std/io:print.ln("{{ c:s }}")
| under-determined m |> std/io:print.ln("ud:{{ m:s }}")
| not-holonomic m |> std/io:print.ln("nh:{{ m:s }}")
| non-rational |> std/io:print.ln("nr")
| non-analytic |> std/io:print.ln("na")
| bad |> std/io:print.ln("bad")
| bad |> std/io:print.ln("bad-lit")
// independent witness: plain series must agree
std/sym:lit(√((1e0+x)))
| exact a |> std/sym:series(a, terms: 8)
| exact s |> std/io:print.ln("{{ s:s }}")
| non-rational |> std/io:print.ln("nr")
| non-analytic |> std/io:print.ln("na")
| bad |> std/io:print.ln("bad")
| bad |> std/io:print.ln("bad-lit")
// 1/(1-x) through the poly-inv lane, 8 certified terms
std/sym:lit(inv((1e0+(-1e0*x))))
| exact a |> std/sym:cert-series(a, terms: 8)
| exact c |> std/io:print.ln("{{ c:s }}")
| under-determined m |> std/io:print.ln("ud:{{ m:s }}")
| not-holonomic m |> std/io:print.ln("nh:{{ m:s }}")
| non-rational |> std/io:print.ln("nr")
| non-analytic |> std/io:print.ln("na")
| bad |> std/io:print.ln("bad")
| bad |> std/io:print.ln("bad-lit")
// x alone: the recurrence cannot determine a_1 -> under-determined
std/sym:lit((x))
| exact a |> std/sym:cert-series(a, terms: 5)
| exact c |> std/io:print.ln("{{ c:s }}")
| under-determined m |> std/io:print.ln("ud:{{ m:s }}")
| not-holonomic m |> std/io:print.ln("nh:{{ m:s }}")
| non-rational |> std/io:print.ln("nr")
| non-analytic |> std/io:print.ln("na")
| bad |> std/io:print.ln("bad")
| bad |> std/io:print.ln("bad-lit")
// sqrt of a non-polynomial -> named refusal
std/sym:lit(√(inv(x)))
| exact a |> std/sym:cert-of(a)
| exact c |> std/io:print.ln("{{ c:s }}")
| not-holonomic m |> std/io:print.ln("nh:{{ m:s }}")
| bad m |> std/io:print.ln("bad:{{ m:s }}")
| bad |> std/io:print.ln("bad-lit")
Actual
ode(k=1,d=1,via=of)|p0=[-1]|p1=[2,2]
cser(terms=8,det=1)|a=[1,1/2,-1/8,1/16,-5/128,7/256,-21/1024,33/2048]|ode=ode(k=1,d=1,via=of)|p0=[-1]|p1=[2,2]|rec=rec(k=2,d=1,via=bridge,det=1)|p0=[0]|p1=[1,2]|p2=[4,2]
terms=8:1,1/2,-1/8,1/16,-5/128,7/256,-21/1024,33/2048
cser(terms=8,det=1)|a=[1,1,1,1,1,1,1,1]|ode=ode(k=1,d=1,via=of)|p0=[-1]|p1=[1,-1]|rec=rec(k=2,d=1,via=bridge,det=1)|p0=[0]|p1=[-2,-1]|p2=[2,1]
ud:rec(k=1,d=1,via=bridge,det=0)|p0=[0]|p1=[0,1]
nh:not-generally-holonomic:sqrt-nonpoly
Expected output
ode(k=1,d=1,via=of)|p0=[-1]|p1=[2,2]
cser(terms=8,det=1)|a=[1,1/2,-1/8,1/16,-5/128,7/256,-21/1024,33/2048]|ode=ode(k=1,d=1,via=of)|p0=[-1]|p1=[2,2]|rec=rec(k=2,d=1,via=bridge,det=1)|p0=[0]|p1=[1,2]|p2=[4,2]
terms=8:1,1/2,-1/8,1/16,-5/128,7/256,-21/1024,33/2048
cser(terms=8,det=1)|a=[1,1,1,1,1,1,1,1]|ode=ode(k=1,d=1,via=of)|p0=[-1]|p1=[1,-1]|rec=rec(k=2,d=1,via=bridge,det=1)|p0=[0]|p1=[-2,-1]|p2=[2,1]
ud:rec(k=1,d=1,via=bridge,det=0)|p0=[0]|p1=[0,1]
nh:not-generally-holonomic:sqrt-nonpoly
Flows
flow ~lit click a branch to expand · @labels scroll to their anchor
lit (expr: √((1e0+x)))
flow ~lit click a branch to expand · @labels scroll to their anchor
lit (expr: √((1e0+x)))
flow ~lit click a branch to expand · @labels scroll to their anchor
lit (expr: √((1e0+x)))
flow ~lit click a branch to expand · @labels scroll to their anchor
lit (expr: inv((1e0+(-1e0*x))))
flow ~lit click a branch to expand · @labels scroll to their anchor
lit (expr: (x))
flow ~lit click a branch to expand · @labels scroll to their anchor
lit (expr: √(inv(x)))
Test Configuration
MUST_RUN