Symbolic mathematics

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:

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:

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

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:

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.