// Tors. Canon strings ride <sexpr!>; ops consume linearly.
//
// Literal / trusted parse: π, e, 2*π, √(2), (π+e), 1/3...
// `expr` spells expression syntax at the callsite — authored math, not
// quoted text. Runtime text goes through ingest/parse instead.
~pub tor lit { expr: Expression }
| exact string<sexpr!>
| bad

// External boundary: outside text -> <sexpr-external!>, only parse discharges.
~pub tor ingest { s: string } -> string<sexpr-external!>

~pub tor parse { s: string<!sexpr-external> }
| exact string<sexpr!>
| bad string<std.io:allocated!>

~pub tor add { a: string<!sexpr>, b: string<!sexpr> } -> string<sexpr!>

~pub tor sub { a: string<!sexpr>, b: string<!sexpr> } -> string<sexpr!>

~pub tor mul { a: string<!sexpr>, b: string<!sexpr> } -> string<sexpr!>

~pub tor div { a: string<!sexpr>, b: string<!sexpr> }
| exact string<sexpr!>
| div-zero

~pub tor neg { a: string<!sexpr> } -> string<sexpr!>

~pub tor sqrt { a: string<!sexpr> }
| exact string<sexpr!>
| neg-root

// Equivalence is canonical string equality — borrows both.
~pub tor equiv { a: string<sexpr>, b: string<sexpr> }
| same
| diff

~pub tor free { n: string<!sexpr> }

~pub tor render { n: string<!sexpr> } -> string<std.io:allocated!>

~pub tor dup { n: string<!sexpr> } -> { a: string<sexpr!>, b: string<sexpr!> }

// Cross-tower lanes
//
// Re-issue a canonical decimal as a symbolic leaf. The bytes are already
// canonical sexpr — numeric leaves share the decimal alphabet — so this is
// a mark move, not a conversion.
~pub tor of-dec { n: string<std.num:!exact> } -> string<sexpr!>

// Integer power by repeated symbolic multiply: pow(x,3) -> (x*x*x),
// pow(x,-2) -> inv((x*x)), pow(x,0) -> 1e0. pow(0,-1) -> | div-zero,
// riding inv's own zero guard.
~pub tor pow { a: string<!sexpr>, n: i64 }
| exact string<sexpr!>
| div-zero

// d/dx of a canonical sexpr — structural rules over the NF, result
// normalized through the same norm, so deriv lands canon.
~pub tor deriv { a: string<!sexpr> } -> string<sexpr!>

// Series of a canonical sexpr at x=0 — `terms` coefficients as
// `terms=L:c0,c1,...` over exact rationals.
~pub tor series { a: string<!sexpr>, terms: i64 }
| exact string<std.io:allocated!>
| non-analytic
| non-rational
| bad

// SupGen derive: bounded holonomic ODE discovery. Enumerates
// (order, degree) up to the declared bounds, solves the series-residual
// linear system exactly, verifies the residual on terms the solve never
// used, and emits a certificate — or | not-found (within bounds).
~pub tor derive-ode { a: string<!sexpr>, max-order: i64, max-deg: i64 }
| exact string<std.io:allocated!>
| not-found
| non-analytic
| non-rational
| bad

// Integral closure — HolonomicCertificate.integralShift, proven in Lean
// (HolonomicClosure.integral_closure_shift): prepend p0=0, order+1. A
// theorem application, not a search — consumes the cert string.
~pub tor cert-shift { c: string<std.io:!allocated> }
| exact string<std.io:allocated!>
| bad-cert string<std.io:allocated!>

// Abstract-term seed — declares a cert body `p0=[..]|p1=[..]|...` as
// data; truth is GIVEN, not discovered. This is the entry point for
// holonomy over terms the grammar does not close over: register the
// law, everything above it is algebra (cert-shift, later compose).
~pub tor cert-seed { body: string }
| exact string<std.io:allocated!>
| bad-cert string<std.io:allocated!>

// Tors.
//
// Sum closure: h = f + g. Companion-basis elimination over Q(x);
// HolonomicClosure's sum theorem — structural, not a finite witness.
~pub tor cert-sum { a: string<std.io:!allocated>, b: string<std.io:!allocated> }
| exact string<std.io:allocated!>
| bad-cert string<std.io:allocated!>

// Product closure: h = f * g, dim <= m*n companion basis.
~pub tor cert-prod { a: string<std.io:!allocated>, b: string<std.io:!allocated> }
| exact string<std.io:allocated!>
| bad-cert string<std.io:allocated!>

// Function composition f(g(x)) — proven not holonomic in general
// (exp_exp_not_holonomic / Stanley 1980 growth bound). This is a named
// theorem refusal, never a search: inputs are validated, then refused.
~pub tor cert-compose {
    outer: string<std.io:!allocated>,
    inner: string<std.io:!allocated>
}
| not-holonomic string<std.io:allocated!>
| bad-cert string<std.io:allocated!>

// D-finite -> P-recursive projection (HolonomicBridge.lean): emits a
// rec(...) object — coefficients are polynomials in the index n, not x.
// det=1 marks q_{K,0} != 0: the recurrence's leading coefficient then
// never vanishes for n >= 0, so the coefficient sequence is determined
// by its first k terms — Lean's toPRecursiveCertificate packaging
// condition. A projection of a cert, not a search.
~pub tor cert-bridge { c: string<std.io:!allocated> }
| exact string<std.io:allocated!>
| bad-cert string<std.io:allocated!>

// Tors.
//
// An empty registry blob.
~pub tor cert-reg-new {} -> string<std.io:allocated!>

// Append a raw cert text as the next G entry. Validates the registry
// blob AND the cert — nothing unvalidated enters the store.
~pub tor cert-reg-put {
    reg: string<std.io:!allocated>,
    cert: string<std.io:!allocated>
}
| exact string<std.io:allocated!>
| bad-cert string<std.io:allocated!>

// Register a declared law body — the abstract-term path, appended as
// the next G entry with via=seed.
~pub tor cert-reg-seed { reg: string<std.io:!allocated>, body: string }
| exact string<std.io:allocated!>
| bad-cert string<std.io:allocated!>

// integralShift at registry level: G_new = shift(G_key), via=shift(Gk).
~pub tor cert-reg-shift { reg: string<std.io:!allocated>, key: string }
| exact string<std.io:allocated!>
| not-found
| bad-cert string<std.io:allocated!>

// Sum closure at registry level: G_new = sum(G_a, G_b), via=sum(Ga,Gb).
~pub tor cert-reg-sum { reg: string<std.io:!allocated>, a: string, b: string }
| exact string<std.io:allocated!>
| not-found
| bad-cert string<std.io:allocated!>

// Product closure at registry level, via=prod(Ga,Gb).
~pub tor cert-reg-prod { reg: string<std.io:!allocated>, a: string, b: string }
| exact string<std.io:allocated!>
| not-found
| bad-cert string<std.io:allocated!>

// Discovery at registry level (Python register_from_expr): run the
// bounded SupGen search, append via=verified=N on success.
~pub tor cert-reg-derive {
    reg: string<std.io:!allocated>,
    a: string<!sexpr>,
    max-order: i64,
    max-deg: i64
}
| exact string<std.io:allocated!>
| not-found
| non-analytic
| non-rational
| bad
| bad-cert string<std.io:allocated!>

// Composition at registry level: validate both keys resolve to certs,
// then refuse by name — the impossibility is a theorem.
~pub tor cert-reg-compose {
    reg: string<std.io:!allocated>,
    outer: string,
    inner: string
}
| not-holonomic string<std.io:allocated!>
| not-found
| bad-cert string<std.io:allocated!>

// Fetch a cert's text by key. Borrows the registry — the blob's
// allocated! obligation stays with the caller.
~pub tor cert-reg-get { reg: string<*>, key: string }
| exact string<std.io:allocated!>
| not-found
| bad-cert string<std.io:allocated!>

// The key of the most recent entry ("G{n}"), for threading chains.
// Borrows the registry.
~pub tor cert-reg-last { reg: string<*> }
| exact string<std.io:allocated!>
| empty
| bad-cert string<std.io:allocated!>

// Tors.
//
// Structural ODE derivation — theorem-level, no series witness.
~pub tor cert-of { a: string<!sexpr> }
| exact string<std.io:allocated!>
| not-holonomic string<std.io:allocated!>
| bad string<std.io:allocated!>

// Certified series: the theorem upgrade. cert-of -> bridge -> det ->
// exact seeds -> recurrence-generated tail. The emitted coefficients
// are FORCED by the annihilating ODE (residual zero for all n >= 0 by
// the closure theorems), so the tail is theorem-correct — the finite
// window only seeds it.
~pub tor cert-series { a: string<!sexpr>, terms: i64 }
| exact string<std.io:allocated!>
| under-determined string<std.io:allocated!>
| not-holonomic string<std.io:allocated!>
| non-rational
| non-analytic
| bad

// decide-integral: elementary construction for polynomial integrands;
// otherwise the holonomic-special lane — structural cert-of preferred
// (theorem-grade), bounded derive-ode as the discovery fallback
// (witness-grade seed, flagged). Matches the artifact's layer order:
// elementary-construct first, certified antiderivative via
// integral-shift second, unresolved with named evidence last.
~pub tor decide-integral { a: string<!sexpr>, max-order: i64, max-deg: i64 }
| elementary string<std.io:allocated!>
| holonomic-special string<std.io:allocated!>
| unresolved string<std.io:allocated!>
| not-holonomic string<std.io:allocated!>
| non-rational
| non-analytic
| bad

// decide-ode: Kovacic pole-structure classification for y'' = r(x) y.
// Ported faithfully: poles = roots of den(r) — over C any non-constant
// denominator has roots — so bounded iff den is constant and
// deg(num) <= deg(den), i.e. r is a constant. No dsolve engine: the
// bounded arm emits the constant-coefficient solution FORM as text.
~pub tor decide-ode { r: string<!sexpr> }
| liouvillian string<std.io:allocated!>
| holonomic-special string<std.io:allocated!>
| unclassifiable string<std.io:allocated!>
| bad string<std.io:allocated!>

// Generic `|name=` segment extractor over decision/cert blobs — the
// composition seam that lets decide-* outputs feed cert-reg-put without
// record-payload arms.
~pub tor decide-field { blob: string<*>, name: string }
| exact string<std.io:allocated!>
| not-found

~pub tor rel-new {} -> string<std.io:allocated!>

// Declare a generator name (lawless until rel-law attaches a law).
~pub tor rel-seed { name: Expression, reg: string<std.io:!allocated> }
| exact string<std.io:allocated!>
| dup
| full
| bad

// Attach (or replace) the derivative law for a declared generator. The law
// is a sexpr over x and generator names — self- and mutual references
// resolve since the name set is complete at attach time.
~pub tor rel-law {
    name: Expression,
    reg: string<std.io:!allocated>,
    source: Source
}
| exact string<std.io:allocated!>
| unknown-generator
| bad

// d/dx of expr under the declared laws — theorem-grade: every rewrite step
// is a derivative rule or a declared-law substitution.
~pub tor rel-derive { reg: string<*>, source: Source }
| exact string<std.io:allocated!>
| unknown-generator
| lawless
| bad

// Canonical normal form of expr under the registry's name set — the
// caller-side equality primitive: canon-equal texts are provably equal.
~pub tor rel-norm { reg: string<*>, source: Source }
| exact string<std.io:allocated!>
| unknown-generator
| bad