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.

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.