FormulaTransformEngine

FormulaTransformEngine is a Wolfram Language paclet for replayable theorem application and relation-safe formula transformation in mathematical analysis. It discovers canonical theorem families, named variants, and family-scoped preparation heuristics while preserving assumptions and unresolved proof obligations.

It complements Wolfram's native algebra, integration, region, and tensor operations; it does not reimplement them.

Native inert integral and sum inputs keep their presentation form in returned expressions, relations, and candidates; the replay derivation uses the common measure-space IR internally.

Installation

Install a checkout or a built .paclet archive, then load the package:

PacletInstall["path/to/FormulaTransformEngine"]
Needs["Lightmarey`FormulaTransformEngine`"]

The package is now available from the Wolfram Language Paclet Repository, the install target is PacletInstall["Lightmarey/FormulaTransformEngine"].

The installed paclet includes English and Simplified Chinese reference pages for every operation function and mathematical primitive. Search for FormulaTransformEngine in the Documentation Center to open the main guide, the end-to-end workflow, or the .ftr.md rule-authoring guide.

Human: shortest call

Needs["Lightmarey`FormulaTransformEngine`"];

ApplyFormulaTransform[
  Abs[MeasureIntegral[f g, x, mu]]
]

Automatic application succeeds only when one candidate has a uniquely best semantic score. Otherwise it returns AmbiguousTransform or NoApplicableTransform.

For a genuine ambiguity, inspect the concise explanations and replay exactly the chosen candidate—without rewriting the request by hand:

found = FindFormulaTransforms[expr];
found["Candidates"][[All, {"CandidateId", "Summary", "Differences"}]]

FormulaTransform[found["Candidates"][[1]]["SelectionRequest"]]

The same candidate id can be passed as TransformationPreference -> id. A stale id fails with PreferredCandidateNotFound; it never silently falls back to another rule.

Human and Association calls return Wolfram Failure[tag, data] objects for unsuccessful operations, so FailureQ[result] and the native failure display work as expected. The JSON-string transport returns a serializable Association with "Status" -> "Failure" and "FailureType" -> tag instead.

Successful results separate "Conditions", "DischargedConditions", typed "Evidence", and pending "Obligations". The same fields occur on candidates and replay steps, so missing conditions cannot disappear inside a presentation-only trace. result["ContextTemplate"] partitions pending native assumptions from analytic declarations into a copyable <|"Assumptions" -> ..., "Context" -> ...|> request patch.

Expert: explicit theorem and context

context = CreateFormulaTransformContext[
  MemLp[f, 2, mu],
  MemLp[g, 2, mu]
];

result = ApplyFormulaTransform[
  Abs[MeasureIntegral[f g, x, mu]],
  TransformationFamily -> "Holder",
  TransformationVariant -> "AbsoluteUpper",
  TransformationParameters -> <|"p" -> 2, "q" -> 2|>,
  TransformationContext -> context
];

result["Relation"]
ValidateFormulaTransformDerivation[result["Derivation"]]
FormulaTransformSteps[result]

FormulaTransformSteps[result] displays a native Dataset with theorem, input, output, direction, part path, relation lifting, conditions, obligations, and cost. Use the property forms FormulaTransformSteps[result, "Rows"] and FormulaTransformSteps[result, "Raw"] for summary Associations and complete replay records respectively.

Target-directed parameter inference uses Reduce, retains conditions, and commits an omitted parameter only when the constrained target has one solution:

PlanFormulaTransform[
  Abs[a b],
  TransformationFamily -> "CauchySchwarz",
  TransformationVariant -> "EpsilonCauchy",
  TargetRelation -> (Abs[a b] <= delta a^2 + b^2/(4 delta))
]

Target completion is automatic: structural search runs first, followed—only when needed— by one final, time-bounded algebraic bridge when a rule-derived endpoint is mathematically equal to the requested target but has a different syntax:

ApplyFormulaTransform[
  Abs[a b],
  TransformationFamily -> "Young",
  TargetRelation -> (Abs[a b] <= (Abs[a]^2 + Abs[b]^2)/2)
]

This fallback is attempted only after structural search fails, never as a rule matcher or an unrecorded rewrite. A successful bridge is a ComputationalEquivalence step whose safe FullSimplify check is recomputed during derivation replay. Set TargetEquivalence -> "Structural" to disable the bridge for deterministic or performance-sensitive workloads.

An inequality theorem is navigable from either recoverable endpoint. Without a final target, humans can ask specifically for an upper or lower transformation:

FindFormulaTransforms[expr, TransformationDirection -> All]
ApplyFormulaTransform[expr, TransformationDirection -> "Upper"]
ApplyFormulaTransform[expr, TransformationDirection -> "Lower"]

Automatic derives direction from TargetRelation when present. A conflicting explicit direction fails with IncompatibleDirection; without a target, candidates from different directions remain an explicit ambiguity.

An inequality may be transformed inside a larger expression only when the outer path has replayable monotonicity evidence. Addition preserves direction; multiplication uses the scalar sign and reverses direction when negative; supported scalar functions use Wolfram's FunctionMonotonicity; measure integration emits PositiveMeasure and IntegrableOn obligations. Unknown scalar sign produces explicit upper and lower candidates rather than a guess.

Agent: the same request model

Agents do not use a separate engine. FormulaTransform normalizes an Association or JSON object into the same request evaluated by the human API. Request keys use the documented PascalCase spelling; unknown keys are errors rather than ignored defaults.

FormulaTransform[<|
  "Action" -> "Plan",
  "Expression" -> Abs[a b],
  "Family" -> "CauchySchwarz",
  "Variant" -> "EpsilonCauchy",
  "TargetRelation" -> (Abs[a b] <= delta a^2 + b^2/(4 delta)),
  "MaxDepth" -> 4,
  "MaxStates" -> 256,
  "TraceLevel" -> "Steps"
|>]

JSON expressions use Wolfram's native ExpressionJSON representation rather than Wolfram code strings or a package-specific head/arguments codec. Expression fields must have a HoldComplete root and are audited before entering the engine:

{
  "Action": "Find",
  "Expression": ["HoldComplete", ["Abs", ["Times", "a", "b"]]],
  "Family": "Young"
}

"TargetRelation", "Assumptions", context assumptions/declarations, and symbolic parameter values use the same held ExpressionJSON representation. JSON text notes are rejected rather than interpreted as mathematical evidence. Numeric parameter values remain ordinary JSON numbers.

Rule authoring

Human-authored rules live in Registry/Sources/*.ftr.md: YAML frontmatter carries the schema and Wolfram InputForm block scalars carry executable formulas. Markdown body text may use LaTeX for exposition, but it is not compiled theorem data. Deterministic JSON IR is tracked in Registry/IR; compile_rules.wls regenerates it and build_rules.wls verifies semantic, execution, record, metadata, and exact source-digest equality. Authors write ordinary Wolfram multiplication; the compiler preserves explicit heuristic factors in a held native representation rather than requiring a package-specific product head. Authors also write natural slots such as x_. The compiler infers true binder positions, constrains them internally to symbols, and unifies every repeated occurrence of the same slot. Rule sources therefore do not need internal _Symbol annotations, while a formula such as MeasureIntegral[f_, x_, LebesgueMeasure[x, 0, 1]] still requires both occurrences of x to agree at match time. Result-only binders are inferred too: a level variable introduced by an outer MeasureIntegral[..., t, ...] needs no extra schema field, is rejected if it leaks from that scope, and receives a stable capture-avoiding binding during replay. Declared parameters may also occur naturally in Match. The compiler captures and unifies those occurrences, infers the value from the input when omitted, and rejects a supplied value that conflicts with the matched expression. Internally, one native Orderless matcher view replaces factorial permutation expansion. The derived registry index covers direct, reverse-orientation, and family-scoped heuristic entry heads.

Parsing happens in an isolated RuleSource`` namespace. Elaboration then produces CoreRulerecords with rule-localBindingIdvalues, so a Notebook value assigned to an author variable such asf` cannot change compilation. Formula fields retain exact start/end spans for diagnostics. These records are current-process compiler data, not an ABI or compatibility format.

wolframscript -file .\lint_ftr.wls
wolframscript -file .\lint_ftr.wls .\Registry\Sources\Holder.ftr.md
wolframscript -file .\compile_rules.wls
wolframscript -file .\build_rules.wls
wolframscript -file .\run_tests.wls
powershell -NoProfile -File .\build_and_smoke_paclet.ps1

The compiler rejects YAML aliases/tags/duplicate keys, undeclared formula symbols, executable heads, malformed execution metadata, and invalid generated theorem parameters. Meta is open and nonsemantic; missing and recursively empty metadata never block compilation. lint_ftr.wls accepts one or more source files, or all tracked sources when invoked without arguments. Diagnostics include the source file, the exact formula-value span, and the nearest schema path such as Variants[1].Result. After linting, compile_rules.wls regenerates all tracked IR and refuses to leave stale generated files; build_rules.wls remains the synchronization gate.

Parameter domains are enforced mathematical data. Reals, Integers, and PositiveReals compile into replayed conditions; an unsupported domain is rejected. Integration by parts similarly emits an explicit IntegrationByPartsAdmissible obligation instead of assuming regularity, measure compatibility, and trace behavior.

Tags are lightweight discovery and dispatch labels, not theorem assumptions. Use a relation tag (Equality or Inequality) together with stable subject tags such as Algebra, Calculus, Integral, MeasureSpace, Convolution, HarmonicAnalysis, Sobolev, or Manifold; introduce a new subject tag only when it will group multiple families. Mathematical variable domains remain under parameter Domain, so the two concepts are not overloaded.

Analytic outer operators are extensible through separately compiled MonotonicityDescriptor sources. A descriptor declares a held outer matcher, argument position, increasing/decreasing direction, strictness, and conditions using the reserved from/to endpoints. The tracked positive-measure integral descriptor is the reference implementation; custom descriptors enter the same immutable registry and replay digest.

Compiled extensions use immutable registry values; loading or creating one never changes the built-in registry or another request:

registry = LoadFormulaTransformRegistry["path/to/Registry/IR"];
ApplyFormulaTransform[expr, TransformationRegistry -> registry]
ValidateFormulaTransformDerivation[derivation, TransformationRegistry -> registry]

CreateFormulaTransformRegistry[family1, family2] accepts strict source IR. A supplied compiled Association is consistency-checked and its matcher/index data is rebuilt; this detects accidental stale or edited derived fields, but is not presented as a security boundary against someone who can edit package code. InspectFormulaTransformRegistry exposes the registry digest, families, variants, heuristics, and index status.

See PRIMITIVES_AND_SYNTAX.md for the complete schema, semantic primitives, relation rules, obligations, and AST whitelist.

License

FormulaTransformEngine 2.0.1 is licensed under BUSL-1.1. See LICENSE.