Symbolic mathematics

The Symbolic workbench provides guided calculation creation and explicit native expression, solution and derivation inspection over these same language operations.

Grid symbolic mathematics is part of the ordinary reactive language. It is not a quoted expression language, a string evaluator, or a second compiler. Declare unknowns with contextual symbol statements, then compose them with ordinary Grid operators, references, literals, and admitted mathematical functions.

symbol x
input A1 = 2

polynomial = x^2 + 2*x + 1
reactive = A1*x^2 + 1

x is an immutable symbolic_variable. Its identity includes the authority of the module that declared it; importing or aliasing it does not rename it. A1 is still an ordinary reactive input. Editing A1 rebuilds reactive and its dependants, while unrelated symbolic values retain their identities.

The compiler evaluates a purely ordinary subtree before lifting its result. In (A1 + B1) * x, A1 + B1 is one ordinary coefficient with both dependency edges; it does not turn either cell into an unknown. Values that cannot cross the exact symbolic boundary—strings, blanks, booleans, errors, units, lossy coercions, volatile results, and effectful results—fail closed.

Transformations return records

Constructors return symbolic values directly. Transformations return an atomic record so status, conditions, work, completeness, and certificate cannot be silently separated from the answer.

canonical_result = SYMBOLIC.CANONICALIZE(polynomial)
canonical = canonical_result.expression

expanded_result = SYMBOLIC.EXPAND(polynomial)
collected_result = SYMBOLIC.COLLECT(polynomial, x)
factored_result = SYMBOLIC.FACTOR(polynomial)
derivative_result = SYMBOLIC.D(polynomial, x)

An expression-operation result contains:

Field	Meaning
status	:complete, :conditional, :not_applicable, :limit, or :invalid
expression	The completed symbolic expression, or BLANK when no answer was certified
conditions	Normalized unresolved propositions required by the result
changed	Whether the returned expression differs structurally from the input
complete	Whether the named operation completed its declared algorithm
work	Deterministic bounded kernel and certificate-adapter work charged by the operation
certificate	A certificate-bound Tree derivation handle that is replayable with the exact operation input

The public record and its bounded WHY projection can verify that the handle binds the visible output, conditions, operation/version, input fingerprint, and stated work coordinate. They deliberately do not retain the operation input, so that inspection-only check is not itself a replay or an independent proof of the adapter-work amount. Authoritative validation supplies the exact input, recomputes its portable bytes and every adapter charge, and reconstructs the handle byte for byte. For SOLVE, it also validates the result and all branch certificates as one cumulative batch.

Operators may enable that validation at the publication boundary; in that verification mode, every completed expression, decision, and solution reruns its closed native operation before publication. The mode is off by default because it deliberately performs a second kernel run. It is not a fallback, a second evaluator, or part of ordinary symbolic execution.

:complete means the named deterministic algorithm completed. It does not claim that SIMPLIFY found a globally smallest expression. A limit or unsupported domain never publishes a plausible uncertified partial answer.

The initial exact transformation family is:

Function	Contract
SYMBOLIC.CANONICALIZE(f)	Deterministic structural canonical form
SYMBOLIC.SIMPLIFY(f, assumptions?)	Assumption-aware deterministic simplification
SYMBOLIC.EXPAND(f)	Exact polynomial expansion
SYMBOLIC.COLLECT(f, x)	Exact coefficient collection by variable
SYMBOLIC.FACTOR(f)	Complete admitted univariate factorization over the rationals
SYMBOLIC.CANCEL(f, assumptions?)	Rational-factor cancellation with nonzero obligations
SYMBOLIC.TOGETHER(f, assumptions?)	Exact common-denominator combination
SYMBOLIC.APART(f, x, assumptions?)	Exact univariate partial fractions
SYMBOLIC.D(f, x, assumptions?)	Symbolic differentiation with branch conditions

Existing unqualified EXPAND, SOLVE, DERIVATIVE, and numeric root functions retain their existing array, matrix, and numeric meanings.

Ordered calculations

SYMBOLIC.CALCULATE(expression, steps, assumptions?) evaluates 1–64 ordered steps under one immutable local assumption set and one cumulative work budget. Use it when later transformations must preserve the domains of earlier steps.

symbol x

# Cancellation retains the excluded point through differentiation.
steps = [{operation: :cancel}, {operation: :differentiate, variable: x}]
derivative = SYMBOLIC.CALCULATE(x / x, steps)

The expression is 0, with the retained condition x != 0. Supplying SYMBOLIC.ASSUMPTIONS(SYMBOLIC.DOMAIN(x, :real), x > 0) discharges that condition for the entire calculation. Conditions are obligations, never new assumptions.

Steps accept :canonicalize, :simplify, :expand, :collect, :factor, :cancel, :together, :apart, :differentiate (also :d), :integrate and :evaluate. Collect, apart, differentiation, integration and evaluation require a declared native variable; other steps reject that field. Unknown commands and extra fields produce GRID_SYMBOLIC_CALCULATION_STEPS. Solving, general substitution and definite integration remain separate operations with their own domain contracts.

An :evaluate step takes both variable and value. Direct literal worksheet records admit exact integer/fraction syntax for value, such as 2/3, through the existing native exact-rational input policy. Named values and shared or computed step lists must already carry native exact values; for example, define point = SYMBOLIC.RATIONAL(2, 3) and use value: point. Ordinary numeric results are not rationalized. This worksheet profile accepts an exact rational point and checks every affected retained condition and assumption independently at that point. A violated restriction returns invalid; a restriction that cannot be decided exactly within this profile returns not_applicable. Neither publishes an expression or certificate. Conditions on other variables remain attached.

slopeAtPoint = SYMBOLIC.CALCULATE(x^3, [
  {operation: :d, variable: x},
  {operation: :evaluate, variable: x, value: 2/3}
]) /* exact 4/3 */

Cancel x/x and then evaluate at 0: the worksheet refuses the excluded point, even though its intermediate expression is 1. If a positive assumption discharged the hole earlier, evaluating at -1 still refuses. A valid point discharges only the conditions checked there. Integer domains and refuted or contradictory evidence are checked too. Symbolic or irrational replacement values and unresolved predicates involving other variables are outside this worksheet profile; standalone SYMBOLIC.EVALUATE retains its broader input contract.

:integrate admits exact univariate polynomials with rational coefficients and returns one antiderivative with integration constant zero. Its exact derivative is checked before publication, within the same work budget. It does not invent an arbitrary constant, integrate rational poles or elementary functions, or admit another symbolic coefficient. Unsupported inputs return not_applicable.

# Retain the original input and verify the primitive by differentiation.
roundTrip = SYMBOLIC.CALCULATE((x + 1)^2, [
  {operation: :expand},
  {operation: :integrate, variable: x},
  {operation: :d, variable: x}
])

The fixed symbolic_calculation_result_v1 record has status, expression, conditions, changed, complete, work, certificate, schema, evidence and reason. A completed calculation publishes its native expression and one certificate binding the original input, ordered steps, assumptions and result. An incomplete outcome has no expression or certificate and explains the refusal in reason. Differentiation or integration after a contextual rewrite requires an admitted open domain: an assumption such as x == 0 cannot justify calculus on a result that was simplified only at that point. Cancelled holes remain obligations through polynomial antiderivatives and later derivatives.

Save the original expression, steps and assumptions in model source to retain the recipe. A result's .expression remains usable as mathematics, but extracting it does not carry its conditions or assumptions into another operation. Extend the original steps for a context-preserving continuation. Display captures and certificates alone do not reconstruct missing source inputs.

Substitution, evaluation, and approximation

A substitution is a typed immutable binding. Its selector is a symbolic_variable value, never identifier text.

at_three = SYMBOLIC.SUBSTITUTION(x, 3)
value_result = SYMBOLIC.EVALUATE(polynomial, at_three)
value = value_result.expression             /* 16 */

SYMBOLIC.EVALUATE(f, binding, assumptions?) substitutes, performs exact ground arithmetic, and then consumes the optional assumptions while simplifying the result and discharging supported conditions. The assumptions are semantic input to the operation and its certificate; they are not merely validated metadata. Evaluation does not imply an approximate conversion. Use SYMBOLIC.APPROXIMATE explicitly for a ground expression:

third = SYMBOLIC.RATIONAL(1, 3)
approx_result = SYMBOLIC.APPROXIMATE(third, 128, :nearest_even)
approx = approx_result.expression

The precision is in bits. Supported rounding symbols are :nearest_even, :toward_negative, :toward_positive, :toward_zero, and :away_from_zero. The result retains its effective precision, rounding policy, representative value, and outward exact enclosure. Effective precision is the requested precision capped by the authority of any approximate source—for example, a machine-real input cannot acquire more than its 53 source bits merely by requesting a larger result. Approximate values remain explicitly approximate and cannot satisfy an exact proof obligation.

Assumptions and decisions

Assumptions are immutable, fingerprinted four-state evidence values. They are local inputs to an operation; they do not mutate the expression or global model truth.

positive_real = SYMBOLIC.ASSUMPTIONS(
  SYMBOLIC.DOMAIN(x, :real),
  x > 0
)

cancelled_result = SYMBOLIC.CANCEL(x / x, positive_real)
decision_result = SYMBOLIC.DECIDE(x > 0, positive_real)

Evidence states are :neither, :supported, :refuted, and :both. Contradictory evidence remains :both; it is never coerced to true. Domain evidence follows the mathematical refinement lattice: integer implies real, and real implies complex, subject to the same four-state rules.

The four states are the same canonical evidence type used by Grid Predicate. Here, predicate_proposition means the operation-local symbolic relation/domain adapter accepted by SYMBOLIC.ASSUMPTIONS; it is not a publication into the global Predicate program. Constructing an assumption therefore does not add a model fact or run Predicate inference. The adapter retains local provenance-shaped records and ordinary Grid dependency edges for the symbolic operation that consumes it.

Without supported nonzero evidence, cancelling x/x returns an explicit condition. With supported and unrefuted x > 0, the condition is discharged. Branch-sensitive identities for radicals, logarithms, and noninteger powers retain their real/complex and sign obligations instead of assuming generic values or principal branches.

SYMBOLIC.SAME(left, right) is only structural Tree identity. Build a symbolic relation with ordinary comparison syntax and use SYMBOLIC.DECIDE when asking for mathematical truth. A symbolic expression or relation cannot be used as an IF, AND, OR, or NOT condition.

Ordinary function calls use one closed, default-deny Tree policy shared by the compiler and resident evaluator. Explicit Tree consumers and reviewed value carriers may receive a mathematical Tree in payload positions; every other position rejects it with GRID_SYMBOLIC_CALL_TYPE, and every implicit Boolean position rejects it with GRID_SYMBOLIC_TRUTHINESS. The runtime check also covers a Tree that materializes from a callable union or is nested inside an array or native collection, before a fast path or function bridge can coerce or ignore it. Models with no symbolic authority do not run this scan.

Exact solving

SYMBOLIC.SOLVE solves an exact univariate polynomial relation in the selected domain:

roots = SYMBOLIC.SOLVE(polynomial == 0, x, :complex)
constrained = SYMBOLIC.SOLVE(polynomial == 0, x, :complex, positive_real)

The domain argument is optional. An assumptions value may occupy the third argument when no domain is written, or the fourth argument after an explicit domain. Assumptions are consumed by the solve: a certified exact branch is removed only when its binding is refuted without simultaneous support. :both, unknown, and non-scalar algebraic candidates are retained rather than guessed away.

The result contains status, canonical branches, domain, complete, work, and a result-level certificate. Every branch contains typed bindings, conditions, an exact multiplicity, and its own certificate. Rational roots are returned directly; other algebraic roots use canonical root_of values with certified real intervals or complex rectangles.

:none is used only with a complete no-solution certificate in the named domain. :unknown and :limit are distinct and never presented as no solution. Over the complex domain, branch multiplicities account for the full polynomial degree within the admitted limits.

Linear and quadratic equations also admit coefficients in a real quadratic field a + b*SQRT(d), with exact rational a, b, and positive rational d. Compatible radicals (such as SQRT(8) and SQRT(2)) share that field. These roots are exact radical expressions, with multiplicity preserved; real-root decisions use exact arithmetic. SYMBOLIC.EVALUATE reduces closed arithmetic in the same field, including division by nonzero field elements. For example, substituting 12*(SQRT(SYMBOLIC.RATIONAL(6,1))-2) into the companion threshold polynomial now gives exact zero. This extension does not admit arbitrary higher-degree equations over multiple independent radical fields.

Hybrid exact and certified operations

Grid's hybrid symbolic-numeric surface is deliberately limited to four problem classes: polynomial decomposition, polynomial systems, large exact linear algebra, and definite-integration/differential-equation preparation. FLINT is a private optional backend for admitted kernels. It does not own Grid source semantics, result records, numeric matrix operations, the ordinary ODE solver, or publication authority.

Capability selection is fixed by the operation name and arity:

Grid-owned without FLINT	Requires an admitted FLINT capability
Two-argument univariate SYMBOLIC.GCD	Ordered-variable multivariate SYMBOLIC.GCD
One-argument univariate SYMBOLIC.FACTOR	Ordered-variable multivariate SYMBOLIC.FACTOR
SYMBOLIC.MATRIX construction	SYMBOLIC.GROEBNER_BASIS and SYMBOLIC.SOLVE_SYSTEM
SYMBOLIC.DEFINITE_INTEGRAL	All SYMBOLIC.MATRIX.* operations
SYMBOLIC.ODE_SOLVE_PREPARED over an already verified series	SYMBOLIC.CERTIFIED_INTEGRAL and SYMBOLIC.LINEAR_ODE_SERIES

The language, compiler, result carriers, independent verifiers, and package contract are implemented. Native availability is package- and target-specific: a Pro package advertises FLINT methods only after loading a valid packaged capability record whose recipe is marked qualified, then passing the exact ABI, dependency, loader, lifecycle, and method-envelope self-tests. The current checked-in Linux recipe remains candidate, macOS remains development-only pending legal review, and Windows remains blocked pending its MSVC/CRT recipe. Consequently, do not assume that an arbitrary 0.65 Server or Desktop binary contains the native methods merely because the functions appear in the language catalog. A missing capability fails model admission explicitly; it never falls back to another symbolic or numeric lane.

symbol x
symbol y

p = (y + 1) * (x + y + 1)
q = (y + 2) * (x + y + 1)

gcd_result = SYMBOLIC.GCD(p, q, [x, y])
basis_result = SYMBOLIC.GROEBNER_BASIS([p, q], [x, y], :lex)
system_result = SYMBOLIC.SOLVE_SYSTEM([p == 0, q == 0], [x, y], :real)

matrix = SYMBOLIC.MATRIX([1, 2; 3, 4])
determinant_result = SYMBOLIC.MATRIX.DETERMINANT(matrix)
inverse_result = SYMBOLIC.MATRIX.INVERSE(matrix)

exact_integral = SYMBOLIC.DEFINITE_INTEGRAL(x^2, x, 0, 1)
certified_integral = SYMBOLIC.CERTIFIED_INTEGRAL(SIN(x), x, 0, 1, 1 / 1000)

series = SYMBOLIC.LINEAR_ODE_SERIES(SYMBOLIC.MATRIX([0]), [1], x, 0, 8)
trajectory = SYMBOLIC.ODE_SOLVE_PREPARED(series, 1.0, 101)

The ordered-variable arguments make multivariate capability requirements statically visible. The first nonmonomial decomposition profile accepts exact integer polynomials in two variables with degree at most one in the first variable; general sparse-multivariate modular and Hensel profiles remain future work. SYMBOLIC.MATRIX is a pure exact constructor; .DETERMINANT, .RANK, .RREF, .SOLVE, .INVERSE, and .NULLSPACE use the admitted exact-matrix profile. Existing floating-point, sparse, iterative, GPU, and distributed matrix owners are unchanged. Exact polynomial definite integration is Grid-owned. Certified finite-path integration and formal local series may use the selected FLINT capability; SYMBOLIC.ODE_SOLVE_PREPARED then hands a verified series seed to the existing approximate grid-ode trajectory owner.

A backend proposes a bounded candidate. Grid independently verifies it, constructs the canonical result and replay certificate, and checks the resident revision again before publication. Missing capability, an unsupported domain, a resource limit, nonconvergence, and a certified no-solution or singular classification remain distinct. None silently falls back to a weaker numeric or alternate symbolic lane.

These operations do not imply unrestricted computer algebra. Broader multivariate algebra beyond the admitted profiles, piecewise reasoning, dimensional symbolic analysis, and general equation-rearrangement search remain explicit future work—not incomplete behavior hidden behind a shipped name. Exact public signatures, admitted result types, and availability metadata are listed in the function catalog.

One resident Tree value

Symbolic expressions and relations refine Grid's portable syntax_tree value under the shipped math.expression authority. The internal prefix grammar is only a validation and hydration contract; it is not author syntax.

Consequently the same resident value works with TREE.RENDER, structural Tree inspection, GRAPH, history, and WHY. Display text is bounded and is never used to reconstruct or compare a symbolic value. Persistence hydrates the Tree and derivation identities directly. A canary or restart audit re-evaluates the resident operation with input-bearing replay; the inspection-only projection does not validate the operation's input or charged work.

Limits and refusal

Symbolic construction and algorithms enforce bounded term size, depth, coefficient bits, polynomial degree, precision, encoded bytes, assumptions, branches, and deterministic work. A breached bound returns an explicit :limit result or a GRID_SYMBOLIC_* diagnostic without partially publishing an answer.

See the complete function signatures in the function catalog and the diagnostics in Errors and diagnostics. Worked recipes live in the cookbook.

For a local Mac development runtime, prepare the pinned native libraries with node tools/prepare-flint.mjs, then select symbolic-flint-qualification-package alongside the host's usual features. When running outside Cargo, place the prepared libraries at the runtime's ../lib/grid/flint path (a local development symlink is sufficient), or set DYLD_LIBRARY_PATH to that prepared lib directory. This existing development selection executes the backend without advertising production availability. The Mac manifest remains development_only_pending_legal_review; production packaging must retain that restriction until the release/legal review is complete. The maintained companion_multivariate_gcd_runs_with_selected_flint_backend test is part of test:native:flint:profile-acceptance and checks the original GCD against x+y+1 exactly.