Fix #446: reject a substitution that drops the symbol's assumptions

[petlenz]

Closes #446.

A fold can consume a symbol's assumption and erase the operation that used it — skew(S) folds to 0 for symmetric S, abs(p) folds to p for positive p — so substituting a replacement that does not carry the same assumption left the folded result behind:

Call	Before	Now
substitute(skew(S), S, G)	0{2}	throws
substitute(sym(S), S, G)	G	throws
substitute(abs(p), p, q)	q	throws
substitute(abs(p), p, -2)	-2 (true value 2)	throws

The scalar case is not in the issue text; it was found while probing and has the same shape.

Rule

substitute(expr, old, new) now requires the replacement to provably carry every assumption asserted on the symbol it replaces, and throws invalid_expression_error naming the missing fact. Tensor space tags and algebra assumptions go through the existing predicates, so implications are honoured (PD ⇒ symmetric, MinorMajor ⇒ symmetric, proper/improper rotation ⇒ orthogonal); payload-carrying tags with no predicate (Young, PartialTraceTag) require the same tag. Scalar and t2s facts compare the assumption sets after inference; a t2s symbol is a wrapped scalar, so the check unwraps to the scalar it carries.

Unprovable counts as not carried. This is the crux, and it is what fixes the reported case: the replacement there is an unannotated general tensor, so treating "unknown" as acceptable would leave the bug in place. The fold is already gone by the time substitution runs, so there is nothing left to re-justify — refusing to answer beats answering wrongly. Option 3 in the issue (record the justifying assumption on the folded node) would be the more precise fix, but it does not help here: the fold left no node behind.

Legitimate workflows still pass, verified by probe:

Replacement for positive p / symmetric S	Result
constant 2, exp(q)	allowed (inference proves positive)
identity_tensor, tensor_zero, trans(X)*X, sym(X), S+S	allowed
dev(X) for a deviatoric symbol	allowed
q*q + 1	rejected — positive in fact, unprovable here

The last row is the cost of the conservative rule. The opt-out is the explicit typed call substitute(std::type_identity<E>{}, std::type_identity<T>{}, expr, old, new), which skips the check — the issue's Option 2, and the only escape for a provably-fine compound, since assumption() rejects non-symbols.

Internal callers

The typed call is also how the substitution visitors recurse into children, so the check runs once per public call rather than per node, and how tensor_solver performs its X = 0 probe to read off the constant term — that is not a claim that zero satisfies X's assumptions. Without that bypass, solve(c*X - B, X) with a PD-annotated X throws instead of returning; SubstitutionAssumptions.SolverProbeIsNotValidated pins it, and I confirmed it fails if the bypass is removed.

The ergonomic overload lost its constexpr/noexcept specification, since validation throws — a noexcept spec there would have turned a rejection into std::terminate. No caller depended on it (checked).

Tests

Five tests in SubstitutionAssumptions: tensor space tags, tensor algebra assumptions (PD, orthogonal), scalar facts, the t2s wrapper, and the solver probe. Each covers a rejection, a provably-satisfying replacement that still folds, and an unannotated symbol as target (unaffected).

Negative control: with core/substitute.h restored from main, 9 assertions across 4 tests fail; all pass with the fix. Full suite 2410/2410 (gcc-14 Debug), clang-format and clang-tidy clean.

Note for the reviewer: this touches apply_scalar/apply_tensor in tensor_to_scalar_substitution.h, which PR #456 also edits — expect a small conflict in those two lines, resolved by keeping #456's if constexpr condition with the typed call inside.

Rebased onto main (which now contains #456). The two PRs both changed apply_tensor, and the conflict was load-bearing: #456's fix for #448 is precisely that the descent became unconditional, while this branch still carried the old if constexpr (tensor || scalar) guard around its typed call. Taking either side alone loses a fix. The resolution keeps both — unconditional descent with the typed (unchecked) call, so a t2s needle inside a tensor child is still found and recursion does not re-validate what the public entry point already checked.

Verified: T2sNeedleInsideTensorChild and T2sNeedleInsideTensorIfThenElse (#456's own tests for #448) pass, and restoring the conditional form fails all 6 of them across the three dimensions — so the wrong resolution cannot land silently. SubstitutionAssumptions.* 5/5. Full suite 2430/2430.