generate_reference_docs.wls

#!/usr/bin/env wolframscript

root = DirectoryName[$InputFileName];
Get[FileNameJoin[{root, "FormulaTransformEngine", "FormulaTransformEngine.wl"}]];

apiSymbols = {
  "ApplyFormulaTransform", "PlanFormulaTransform", "FindFormulaTransforms", "FormulaTransform",
  "CompileFormulaTransformFamily", "CompileFormulaTransformMonotonicityDescriptor",
  "CompileFormulaTransformSource", "CreateFormulaTransformRegistry", "LoadFormulaTransformRegistry",
  "InspectFormulaTransformRegistry", "CreateFormulaTransformContext",
  "ValidateFormulaTransformDerivation", "CreateFormulaTransformCertificate",
  "FormulaTransformSteps", "CheckFormulaTransformEquivalence"
};

primitiveSpecs = Association@KeyValueMap[
  SymbolName[Unevaluated[#1]] -> #2 &,
  Lightmarey`FormulaTransformEngine`Private`$FTPrimitiveSpecs
];
primitiveSymbols = Keys[primitiveSpecs];
symbols = Join[apiSymbols, primitiveSymbols];

bi[english_, chinese_] := <|"English" -> english, "ChineseSimplified" -> chinese|>;
localized[value_Association, language_String] := Lookup[value, language];
example[english_, chinese_, input_, output_] := <|
  "Text" -> bi[english, chinese], "Input" -> input, "Output" -> output
|>;

referenceURI[name_String] := "paclet:Lightmarey/FormulaTransformEngine/ref/" <> name;
guideURI[name_String] := "paclet:Lightmarey/FormulaTransformEngine/guide/" <> name;
referenceLink[name_String] := ButtonBox[
  StyleBox[name, "InlineFormula"], BaseStyle -> "Link", ButtonData -> referenceURI[name]
];
guideLink[name_String, label_String] := ButtonBox[
  StyleBox[label, "InlineFormula"], BaseStyle -> "Link", ButtonData -> guideURI[name]
];

apiDescriptions = <|
  "ApplyFormulaTransform" -> bi["apply the unique best replayable transformation", "\:5e94\:7528\:552f\:4e00\:6700\:4f18\:4e14\:53ef\:91cd\:653e\:7684\:516c\:5f0f\:53d8\:6362"],
  "PlanFormulaTransform" -> bi["plan a complete or best partial bounded transformation", "\:5728\:9884\:7b97\:5185\:89c4\:5212\:5b8c\:6574\:6216\:6700\:4f73\:90e8\:5206\:53d8\:6362"],
  "FindFormulaTransforms" -> bi["find direct and family-scoped preparation candidates", "\:67e5\:627e\:76f4\:63a5\:5019\:9009\:548c\:5b9a\:7406\:65cf\:5185\:7684\:51c6\:5907\:5019\:9009"],
  "FormulaTransform" -> bi["execute the unified Association or structural JSON request model", "\:6267\:884c\:7edf\:4e00\:7684 Association \:6216\:7ed3\:6784\:5316 JSON \:8bf7\:6c42"],
  "CompileFormulaTransformFamily" -> bi["validate and elaborate strict TransformFamily IR", "\:9a8c\:8bc1\:5e76\:7cbe\:5316\:4e25\:683c\:7684 TransformFamily IR"],
  "CompileFormulaTransformMonotonicityDescriptor" -> bi["compile a replayable analytic monotonicity descriptor", "\:7f16\:8bd1\:53ef\:91cd\:653e\:7684\:5206\:6790\:5355\:8c03\:6027\:63cf\:8ff0\:7b26"],
  "CompileFormulaTransformSource" -> bi["compile a restricted Markdown and YAML rule source", "\:7f16\:8bd1\:53d7\:9650\:7684 Markdown \:4e0e YAML \:89c4\:5219\:6e90"],
  "CreateFormulaTransformRegistry" -> bi["create an immutable registry from rule values", "\:4ece\:89c4\:5219\:503c\:521b\:5efa\:4e0d\:53ef\:53d8 registry"],
  "LoadFormulaTransformRegistry" -> bi["load JSON IR files into an immutable registry", "\:5c06 JSON IR \:6587\:4ef6\:52a0\:8f7d\:4e3a\:4e0d\:53ef\:53d8 registry"],
  "InspectFormulaTransformRegistry" -> bi["inspect registry contents, digests, and index status", "\:68c0\:67e5 registry \:5185\:5bb9\:3001\:6458\:8981\:548c\:7d22\:5f15\:72b6\:6001"],
  "CreateFormulaTransformContext" -> bi["create or extend an immutable mathematical context", "\:521b\:5efa\:6216\:6269\:5c55\:4e0d\:53ef\:53d8\:6570\:5b66\:4e0a\:4e0b\:6587"],
  "ValidateFormulaTransformDerivation" -> bi["replay and validate every recorded transformation step", "\:9010\:6b65\:91cd\:653e\:5e76\:9a8c\:8bc1\:53d8\:6362\:63a8\:5bfc"],
  "CreateFormulaTransformCertificate" -> bi["create a certificate from an unconditional valid replay", "\:4ece\:65e0\:6761\:4ef6\:6709\:6548\:7684\:91cd\:653e\:63a8\:5bfc\:521b\:5efa\:8bc1\:4e66"],
  "FormulaTransformSteps" -> bi["display concise replay steps or return their records", "\:663e\:793a\:7b80\:6d01\:7684\:91cd\:653e\:6b65\:9aa4\:6216\:8fd4\:56de\:6b65\:9aa4\:8bb0\:5f55"],
  "CheckFormulaTransformEquivalence" -> bi["check restricted algebraic equivalence within a time bound", "\:5728\:65f6\:95f4\:9650\:5236\:5185\:68c0\:67e5\:53d7\:9650\:4ee3\:6570\:7b49\:4ef7\:6027"]
|>;

apiForms = <|
  "ApplyFormulaTransform" -> {"ApplyFormulaTransform[expr]", "ApplyFormulaTransform[expr, opts]"},
  "PlanFormulaTransform" -> {"PlanFormulaTransform[expr]", "PlanFormulaTransform[expr, opts]"},
  "FindFormulaTransforms" -> {"FindFormulaTransforms[expr]", "FindFormulaTransforms[expr, opts]"},
  "FormulaTransform" -> {"FormulaTransform[request_Association]", "FormulaTransform[json_String]"},
  "CompileFormulaTransformFamily" -> {"CompileFormulaTransformFamily[ir_Association]"},
  "CompileFormulaTransformMonotonicityDescriptor" -> {"CompileFormulaTransformMonotonicityDescriptor[ir_Association]"},
  "CompileFormulaTransformSource" -> {"CompileFormulaTransformSource[path_String]"},
  "CreateFormulaTransformRegistry" -> {"CreateFormulaTransformRegistry[rule1, rule2, ...]"},
  "LoadFormulaTransformRegistry" -> {"LoadFormulaTransformRegistry[path_String]"},
  "InspectFormulaTransformRegistry" -> {"InspectFormulaTransformRegistry[]", "InspectFormulaTransformRegistry[registry]"},
  "CreateFormulaTransformContext" -> {"CreateFormulaTransformContext[]", "CreateFormulaTransformContext[decls]", "CreateFormulaTransformContext[context, decls]"},
  "ValidateFormulaTransformDerivation" -> {"ValidateFormulaTransformDerivation[derivation]", "ValidateFormulaTransformDerivation[derivation, opts]"},
  "CreateFormulaTransformCertificate" -> {"CreateFormulaTransformCertificate[derivation]", "CreateFormulaTransformCertificate[derivation, opts]"},
  "FormulaTransformSteps" -> {"FormulaTransformSteps[value]", "FormulaTransformSteps[value, \"Rows\"]", "FormulaTransformSteps[value, \"Raw\"]"},
  "CheckFormulaTransformEquivalence" -> {"CheckFormulaTransformEquivalence[lhs, rhs]", "CheckFormulaTransformEquivalence[lhs, rhs, opts]"}
|>;

transformOptions = {
  "TransformationFamily", "TransformationVariant", "TransformationDirection", "TargetRelation",
  "TargetEquivalence", "TransformationScope", "TransformationContext", "TransformationRegistry",
  "Assumptions", "TransformationParameters", "TransformationTags", "TransformationPreference",
  "TraceLevel", "MaxDepth", "MaxStates", "TimeConstraint"
};

optionDescriptions = <|
  "TransformationFamily" -> bi["Automatic, or the canonical family name to search.", "Automatic\:ff0c\:6216\:8981\:641c\:7d22\:7684\:89c4\:8303\:5b9a\:7406\:65cf\:540d\:79f0\:3002"],
  "TransformationVariant" -> bi["Automatic, or a variant name scoped by an explicit family.", "Automatic\:ff0c\:6216\:7531\:663e\:5f0f\:5b9a\:7406\:65cf\:9650\:5b9a\:7684\:53d8\:4f53\:540d\:79f0\:3002"],
  "TransformationDirection" -> bi["Automatic, All, \"Upper\", \"Lower\", or \"Equivalent\".", "Automatic\:3001All\:3001\"Upper\"\:3001\"Lower\" \:6216 \"Equivalent\"\:3002"],
  "TargetRelation" -> bi["Automatic, or a binary native relation containing the source expression as one endpoint.", "Automatic\:ff0c\:6216\:4ee5\:6e90\:8868\:8fbe\:5f0f\:4e3a\:4e00\:7aef\:7684\:4e8c\:5143\:539f\:751f\:5173\:7cfb\:3002"],
  "TargetEquivalence" -> bi["Automatic enables one recorded terminal computational bridge after structural search; \"Structural\" disables it.", "Automatic \:5141\:8bb8\:7ed3\:6784\:641c\:7d22\:5931\:8d25\:540e\:8ffd\:52a0\:4e00\:6b21\:6709\:8bb0\:5f55\:7684\:7ec8\:7aef\:8ba1\:7b97\:7b49\:4ef7\:6865\:ff1b\"Structural\" \:7981\:7528\:8be5\:6865\:3002"],
  "TransformationScope" -> bi["\"Whole\", All, or an explicit part path.", "\"Whole\"\:3001All \:6216\:663e\:5f0f\:90e8\:4ef6\:8def\:5f84\:3002"],
  "TransformationContext" -> bi["An immutable value created by CreateFormulaTransformContext.", "\:7531 CreateFormulaTransformContext \:521b\:5efa\:7684\:4e0d\:53ef\:53d8\:503c\:3002"],
  "TransformationRegistry" -> bi["Automatic for built-ins, or an immutable custom registry.", "Automatic \:8868\:793a\:5185\:7f6e\:89c4\:5219\:ff0c\:6216\:4f20\:5165\:4e0d\:53ef\:53d8\:81ea\:5b9a\:4e49 registry\:3002"],
  "Assumptions" -> bi["Safe native logical assumptions; defaults to $Assumptions.", "\:5b89\:5168\:7684\:539f\:751f\:903b\:8f91\:5047\:8bbe\:ff1b\:9ed8\:8ba4\:4f7f\:7528 $Assumptions\:3002"],
  "TransformationParameters" -> bi["An Association of named theorem parameter values.", "\:5b9a\:7406\:547d\:540d\:53c2\:6570\:503c\:7ec4\:6210\:7684 Association\:3002"],
  "TransformationTags" -> bi["A list of discovery tags; explicit family calls are not narrowed by tags.", "\:7528\:4e8e\:53d1\:73b0\:7684\:6807\:7b7e\:5217\:8868\:ff1b\:663e\:5f0f\:5b9a\:7406\:65cf\:8c03\:7528\:4e0d\:53d7\:6807\:7b7e\:7f29\:7a84\:3002"],
  "TransformationPreference" -> bi["Automatic, or a stable CandidateId returned by discovery.", "Automatic\:ff0c\:6216\:53d1\:73b0\:9636\:6bb5\:8fd4\:56de\:7684\:7a33\:5b9a CandidateId\:3002"],
  "TraceLevel" -> bi["\"Steps\" records a derivation; None omits it from the returned presentation.", "\"Steps\" \:8bb0\:5f55\:63a8\:5bfc\:ff1bNone \:4ece\:8fd4\:56de\:8868\:793a\:4e2d\:7701\:7565\:63a8\:5bfc\:3002"],
  "MaxDepth" -> bi["Maximum target-search depth; the default is 4.", "\:76ee\:6807\:641c\:7d22\:6700\:5927\:6df1\:5ea6\:ff1b\:9ed8\:8ba4\:503c\:4e3a 4\:3002"],
  "MaxStates" -> bi["Maximum visited search states; the default is 256.", "\:6700\:591a\:8bbf\:95ee\:7684\:641c\:7d22\:72b6\:6001\:6570\:ff1b\:9ed8\:8ba4\:503c\:4e3a 256\:3002"],
  "TimeConstraint" -> bi["One request-wide positive time limit in seconds; the default is 5.", "\:8986\:76d6\:6574\:4e2a\:8bf7\:6c42\:7684\:6b63\:79d2\:6570\:65f6\:9650\:ff1b\:9ed8\:8ba4\:503c\:4e3a 5\:3002"]
|>;

optionsFor = AssociationThread[apiSymbols, ConstantArray[{}, Length[apiSymbols]]];
Scan[(optionsFor[#] = transformOptions) &, {"ApplyFormulaTransform", "PlanFormulaTransform", "FindFormulaTransforms"}];
optionsFor["ValidateFormulaTransformDerivation"] = {"TransformationRegistry", "TimeConstraint"};
optionsFor["CreateFormulaTransformCertificate"] = {"TransformationRegistry", "TimeConstraint"};
optionsFor["CheckFormulaTransformEquivalence"] = {"Assumptions", "TimeConstraint"};

apiReturns = <|
  "ApplyFormulaTransform" -> bi["Returns a FormulaTransformResult Association only for a unique complete candidate; pending hypotheses remain in Obligations.", "\:4ec5\:5f53\:5b58\:5728\:552f\:4e00\:5b8c\:6574\:5019\:9009\:65f6\:8fd4\:56de FormulaTransformResult Association\:ff1b\:672a\:89e3\:51b3\:524d\:63d0\:4fdd\:7559\:5728 Obligations \:4e2d\:3002"],
  "PlanFormulaTransform" -> bi["Returns a FormulaTransformPlan Association. Complete may be False, in which case the best partial replay remains explicit.", "\:8fd4\:56de FormulaTransformPlan Association\:3002Complete \:53ef\:4ee5\:4e3a False\:ff0c\:6b64\:65f6\:6700\:4f73\:90e8\:5206\:91cd\:653e\:4ecd\:88ab\:663e\:5f0f\:4fdd\:7559\:3002"],
  "FindFormulaTransforms" -> bi["Returns a FormulaTransformCandidates Association containing replayable candidates and stable CandidateId values.", "\:8fd4\:56de FormulaTransformCandidates Association\:ff0c\:5176\:4e2d\:5305\:542b\:53ef\:91cd\:653e\:5019\:9009\:548c\:7a33\:5b9a CandidateId\:3002"],
  "FormulaTransform" -> bi["Association input returns the native result contract. JSON-string input returns a JSON-serializable Association, including serializable failure data.", "Association \:8f93\:5165\:8fd4\:56de\:539f\:751f\:7ed3\:679c\:5951\:7ea6\:ff1bJSON \:5b57\:7b26\:4e32\:8f93\:5165\:8fd4\:56de\:53ef JSON \:5e8f\:5217\:5316\:7684 Association\:ff0c\:5305\:62ec\:53ef\:5e8f\:5217\:5316\:5931\:8d25\:6570\:636e\:3002"],
  "CompileFormulaTransformFamily" -> bi["Returns a compiled CoreRule family Association with matchers, BindingId values, and semantic, execution, record, and source digests.", "\:8fd4\:56de\:5df2\:7f16\:8bd1\:7684 CoreRule \:5b9a\:7406\:65cf Association\:ff0c\:5305\:542b matcher\:3001BindingId \:4ee5\:53ca\:8bed\:4e49\:3001\:6267\:884c\:3001\:8bb0\:5f55\:548c\:6e90\:6458\:8981\:3002"],
  "CompileFormulaTransformMonotonicityDescriptor" -> bi["Returns a compiled CoreRule descriptor used to lift relations through an analytic outer operator.", "\:8fd4\:56de\:7528\:4e8e\:5c06\:5173\:7cfb\:63d0\:5347\:7a7f\:8fc7\:5206\:6790\:5916\:5c42\:7b97\:5b50\:7684\:5df2\:7f16\:8bd1 CoreRule \:63cf\:8ff0\:7b26\:3002"],
  "CompileFormulaTransformSource" -> bi["Returns a compiled family or descriptor with SourceFile and exact FormulaSpans attached.", "\:8fd4\:56de\:9644\:5e26 SourceFile \:548c\:7cbe\:786e FormulaSpans \:7684\:5df2\:7f16\:8bd1\:5b9a\:7406\:65cf\:6216\:63cf\:8ff0\:7b26\:3002"],
  "CreateFormulaTransformRegistry" -> bi["Returns an immutable FormulaTransformRegistry Association whose matcher data and index are rebuilt from validated inputs.", "\:8fd4\:56de\:4e0d\:53ef\:53d8 FormulaTransformRegistry Association\:ff1bmatcher \:6570\:636e\:548c\:7d22\:5f15\:7531\:5df2\:9a8c\:8bc1\:8f93\:5165\:91cd\:5efa\:3002"],
  "LoadFormulaTransformRegistry" -> bi["Returns an immutable registry compiled from the supported JSON IR files in path.", "\:8fd4\:56de\:7531\:6307\:5b9a\:8def\:5f84\:4e2d\:53d7\:652f\:6301 JSON IR \:6587\:4ef6\:7f16\:8bd1\:51fa\:7684\:4e0d\:53ef\:53d8 registry\:3002"],
  "InspectFormulaTransformRegistry" -> bi["Returns a FormulaTransformRegistryInspection Association with concise family, rule, digest, and index information.", "\:8fd4\:56de FormulaTransformRegistryInspection Association\:ff0c\:5305\:542b\:7b80\:6d01\:7684\:5b9a\:7406\:65cf\:3001\:89c4\:5219\:3001\:6458\:8981\:548c\:7d22\:5f15\:4fe1\:606f\:3002"],
  "CreateFormulaTransformContext" -> bi["Returns an immutable FormulaTransformContext Association. Logical relations go to Assumptions; analytic declarations go to Declarations.", "\:8fd4\:56de\:4e0d\:53ef\:53d8 FormulaTransformContext Association\:3002\:903b\:8f91\:5173\:7cfb\:8fdb\:5165 Assumptions\:ff0c\:5206\:6790\:58f0\:660e\:8fdb\:5165 Declarations\:3002"],
  "ValidateFormulaTransformDerivation" -> bi["Returns an Association whose ValidationStatus is Valid, ConditionallyValid, or Invalid.", "\:8fd4\:56de ValidationStatus \:4e3a Valid\:3001ConditionallyValid \:6216 Invalid \:7684 Association\:3002"],
  "CreateFormulaTransformCertificate" -> bi["Returns a FormulaTransformCertificate only when replay validation is unconditionally Valid.", "\:4ec5\:5f53\:91cd\:653e\:9a8c\:8bc1\:4e3a\:65e0\:6761\:4ef6 Valid \:65f6\:8fd4\:56de FormulaTransformCertificate\:3002"],
  "FormulaTransformSteps" -> bi["Returns a Dataset by default, concise row Associations for \"Rows\", or complete replay records for \"Raw\".", "\:9ed8\:8ba4\:8fd4\:56de Dataset\:ff1b\"Rows\" \:8fd4\:56de\:7b80\:6d01\:884c Association\:ff1b\"Raw\" \:8fd4\:56de\:5b8c\:6574\:91cd\:653e\:8bb0\:5f55\:3002"],
  "CheckFormulaTransformEquivalence" -> bi["Returns an Association with Result equal to Proved, Disproved, or Unknown, together with method and timeout data.", "\:8fd4\:56de Result \:4e3a Proved\:3001Disproved \:6216 Unknown \:7684 Association\:ff0c\:5e76\:9644\:65b9\:6cd5\:548c\:8d85\:65f6\:4fe1\:606f\:3002"]
|>;

apiFailures = <|
  "ApplyFormulaTransform" -> bi["Returns Failure for no match, ambiguity, incompatible direction, incomplete target search, unsafe input, or timeout.", "\:65e0\:5339\:914d\:3001\:6b67\:4e49\:3001\:65b9\:5411\:51b2\:7a81\:3001\:76ee\:6807\:641c\:7d22\:4e0d\:5b8c\:6574\:3001\:4e0d\:5b89\:5168\:8f93\:5165\:6216\:8d85\:65f6\:65f6\:8fd4\:56de Failure\:3002"],
  "PlanFormulaTransform" -> bi["Returns Failure for malformed requests, unsafe input, replay failure, or timeout; an ordinary incomplete search is a successful partial plan.", "\:8bf7\:6c42\:9519\:8bef\:3001\:4e0d\:5b89\:5168\:8f93\:5165\:3001\:91cd\:653e\:5931\:8d25\:6216\:8d85\:65f6\:65f6\:8fd4\:56de Failure\:ff1b\:666e\:901a\:7684\:4e0d\:5b8c\:6574\:641c\:7d22\:662f\:6210\:529f\:7684\:90e8\:5206\:8ba1\:5212\:3002"],
  "FindFormulaTransforms" -> bi["Returns Failure when the request is invalid or no transformation is applicable; multiple candidates are returned rather than treated as failure.", "\:8bf7\:6c42\:65e0\:6548\:6216\:65e0\:53ef\:7528\:53d8\:6362\:65f6\:8fd4\:56de Failure\:ff1b\:591a\:4e2a\:5019\:9009\:4f1a\:88ab\:8fd4\:56de\:ff0c\:800c\:4e0d\:662f\:89c6\:4e3a\:5931\:8d25\:3002"],
  "FormulaTransform" -> bi["Unknown request keys and malformed held ExpressionJSON are rejected. JSON transport reports failures with Status -> \"Failure\".", "\:672a\:77e5\:8bf7\:6c42\:952e\:548c\:975e\:6cd5 held ExpressionJSON \:4f1a\:88ab\:62d2\:7edd\:ff1bJSON \:4f20\:8f93\:7528 Status -> \"Failure\" \:62a5\:544a\:5931\:8d25\:3002"],
  "CompileFormulaTransformFamily" -> bi["Returns Failure with Path for unknown keys, invalid field types, malformed formulas, undeclared symbols, bad primitive applications, or inconsistent generated parameters.", "\:672a\:77e5\:952e\:3001\:5b57\:6bb5\:7c7b\:578b\:9519\:8bef\:3001\:516c\:5f0f\:975e\:6cd5\:3001\:672a\:58f0\:660e\:7b26\:53f7\:3001\:539f\:8bed\:5e94\:7528\:9519\:8bef\:6216\:751f\:6210\:53c2\:6570\:4e0d\:4e00\:81f4\:65f6\:ff0c\:8fd4\:56de\:5e26 Path \:7684 Failure\:3002"],
  "CompileFormulaTransformMonotonicityDescriptor" -> bi["Returns Failure for an invalid matcher, endpoint condition, argument position, direction, strictness, metadata type, or digest.", "matcher\:3001\:7aef\:70b9\:6761\:4ef6\:3001\:53c2\:6570\:4f4d\:7f6e\:3001\:65b9\:5411\:3001\:4e25\:683c\:6027\:3001\:5143\:6570\:636e\:7c7b\:578b\:6216\:6458\:8981\:65e0\:6548\:65f6\:8fd4\:56de Failure\:3002"],
  "CompileFormulaTransformSource" -> bi["Returns a source-located Failure with File, Line, Column, Span, and schema Path whenever possible.", "\:5931\:8d25\:65f6\:5c3d\:53ef\:80fd\:8fd4\:56de\:5305\:542b File\:3001Line\:3001Column\:3001Span \:548c schema Path \:7684\:6e90\:7801\:5b9a\:4f4d Failure\:3002"],
  "CreateFormulaTransformRegistry" -> bi["Returns Failure when source IR is invalid or supplied compiled data is internally inconsistent.", "\:6e90 IR \:65e0\:6548\:6216\:4f20\:5165\:7684\:5df2\:7f16\:8bd1\:6570\:636e\:5185\:90e8\:4e0d\:4e00\:81f4\:65f6\:8fd4\:56de Failure\:3002"],
  "LoadFormulaTransformRegistry" -> bi["Returns Failure for an invalid path, unreadable JSON, unsupported rule kind, duplicate rule identity, or invalid IR.", "\:8def\:5f84\:65e0\:6548\:3001JSON \:4e0d\:53ef\:8bfb\:3001\:89c4\:5219 Kind \:4e0d\:53d7\:652f\:6301\:3001\:89c4\:5219\:6807\:8bc6\:91cd\:590d\:6216 IR \:65e0\:6548\:65f6\:8fd4\:56de Failure\:3002"],
  "InspectFormulaTransformRegistry" -> bi["Returns Failure[\"MalformedRegistry\", ...] for values not created by the registry constructors.", "\:5bf9\:4e8e\:4e0d\:662f\:7531 registry \:6784\:9020\:51fd\:6570\:521b\:5efa\:7684\:503c\:ff0c\:8fd4\:56de Failure[\"MalformedRegistry\", ...]\:3002"],
  "CreateFormulaTransformContext" -> bi["Rejects text notes, unverified evidence records, malformed context values, and non-list context patches.", "\:62d2\:7edd\:6587\:672c\:5907\:6ce8\:3001\:672a\:7ecf\:9a8c\:8bc1\:7684 evidence \:8bb0\:5f55\:3001\:975e\:6cd5 context \:503c\:548c\:975e\:5217\:8868 context patch\:3002"],
  "ValidateFormulaTransformDerivation" -> bi["Malformed or stale derivations normally return ValidationStatus -> \"Invalid\" rather than claiming a valid replay.", "\:975e\:6cd5\:6216\:8fc7\:671f\:63a8\:5bfc\:901a\:5e38\:8fd4\:56de ValidationStatus -> \"Invalid\"\:ff0c\:4e0d\:4f1a\:58f0\:79f0\:91cd\:653e\:6709\:6548\:3002"],
  "CreateFormulaTransformCertificate" -> bi["Returns Failure[\"UnverifiedDerivation\", ...] for conditional or invalid replay.", "\:6761\:4ef6\:6709\:6548\:6216\:65e0\:6548\:91cd\:653e\:4f1a\:8fd4\:56de Failure[\"UnverifiedDerivation\", ...]\:3002"],
  "FormulaTransformSteps" -> bi["Returns Failure[\"InvalidProperty\", ...] for an unknown property; a value without a derivation yields an empty step sequence.", "\:672a\:77e5\:5c5e\:6027\:8fd4\:56de Failure[\"InvalidProperty\", ...]\:ff1b\:4e0d\:542b\:63a8\:5bfc\:7684\:503c\:4ea7\:751f\:7a7a\:6b65\:9aa4\:5e8f\:5217\:3002"],
  "CheckFormulaTransformEquivalence" -> bi["Unsafe syntax, unsafe assumptions, or timeout returns Result -> \"Unknown\"; the function does not treat Unknown as proof.", "\:4e0d\:5b89\:5168\:8bed\:6cd5\:3001\:4e0d\:5b89\:5168\:5047\:8bbe\:6216\:8d85\:65f6\:8fd4\:56de Result -> \"Unknown\"\:ff1bUnknown \:4e0d\:4f1a\:88ab\:5f53\:4f5c\:8bc1\:660e\:3002"]
|>;

commonTransformNotes = {
  bi["Input is held, audited, and converted to the common semantic measure representation before matching; returned expressions preserve recognized native inert presentation.", "\:8f93\:5165\:5148\:88ab\:4fdd\:6301\:548c\:5ba1\:8ba1\:ff0c\:518d\:8f6c\:6362\:4e3a\:516c\:5171\:7684\:6d4b\:5ea6\:8bed\:4e49\:8868\:793a\:8fdb\:884c\:5339\:914d\:ff1b\:8fd4\:56de\:8868\:8fbe\:5f0f\:4f1a\:6062\:590d\:53ef\:8bc6\:522b\:7684\:539f\:751f\:60f0\:6027\:8868\:793a\:3002"],
  bi["Conditions, DischargedConditions, Evidence, and Obligations remain separate in candidates, steps, and results.", "Conditions\:3001DischargedConditions\:3001Evidence \:548c Obligations \:5728\:5019\:9009\:3001\:6b65\:9aa4\:4e0e\:7ed3\:679c\:4e2d\:59cb\:7ec8\:5206\:5f00\:3002"]
};

apiNotes = AssociationThread[apiSymbols, ConstantArray[{}, Length[apiSymbols]]];
Scan[(apiNotes[#] = commonTransformNotes) &, {"ApplyFormulaTransform", "PlanFormulaTransform", "FindFormulaTransforms"}];
apiNotes["FormulaTransform"] = {bi["Request keys are PascalCase. Association and JSON calls are normalized into the same internal request.", "\:8bf7\:6c42\:952e\:4f7f\:7528 PascalCase\:ff1bAssociation \:4e0e JSON \:8c03\:7528\:4f1a\:89c4\:8303\:5316\:4e3a\:540c\:4e00\:4e2a\:5185\:90e8\:8bf7\:6c42\:3002"]};
apiNotes["CompileFormulaTransformFamily"] = {bi["The compiler elaborates SourceRule data into held CoreRule data; compiled Associations are current-process values, not a compatibility ABI.", "\:7f16\:8bd1\:5668\:628a SourceRule \:6570\:636e\:7cbe\:5316\:4e3a held CoreRule \:6570\:636e\:ff1b\:5df2\:7f16\:8bd1 Association \:662f\:5f53\:524d\:8fdb\:7a0b\:503c\:ff0c\:4e0d\:662f\:517c\:5bb9\:6027 ABI\:3002"]};
apiNotes["CompileFormulaTransformMonotonicityDescriptor"] = {bi["The reserved endpoints from and to may appear in Conditions. Other condition symbols must be bound by Match.", "\:4fdd\:7559\:7aef\:70b9 from \:548c to \:53ef\:4ee5\:51fa\:73b0\:5728 Conditions \:4e2d\:ff1b\:5176\:4ed6\:6761\:4ef6\:7b26\:53f7\:5fc5\:987b\:7531 Match \:7ed1\:5b9a\:3002"]};
apiNotes["CompileFormulaTransformSource"] = {bi["Only YAML frontmatter is executable rule data. The Markdown body is explanatory text and may contain LaTeX.", "\:53ea\:6709 YAML frontmatter \:662f\:53ef\:6267\:884c\:89c4\:5219\:6570\:636e\:ff1bMarkdown \:6b63\:6587\:662f\:8bf4\:660e\:6587\:5b57\:ff0c\:53ef\:4ee5\:5305\:542b LaTeX\:3002"]};
apiNotes["CreateFormulaTransformRegistry"] = {bi["Creating a registry does not mutate the built-in registry or any other request.", "\:521b\:5efa registry \:4e0d\:4f1a\:4fee\:6539\:5185\:7f6e registry \:6216\:5176\:4ed6\:8bf7\:6c42\:3002"]};
apiNotes["LoadFormulaTransformRegistry"] = {bi["Use the same returned registry for execution and replay validation because derivations record RegistryDigest.", "\:6267\:884c\:548c\:91cd\:653e\:9a8c\:8bc1\:5e94\:4f7f\:7528\:540c\:4e00\:4e2a\:8fd4\:56de registry\:ff0c\:56e0\:4e3a\:63a8\:5bfc\:4f1a\:8bb0\:5f55 RegistryDigest\:3002"]};
apiNotes["InspectFormulaTransformRegistry"] = {bi["Inspection omits executable matcher internals and exposes stable author-facing metadata and counts.", "\:68c0\:67e5\:7ed3\:679c\:7701\:7565\:53ef\:6267\:884c matcher \:5185\:90e8\:7ed3\:6784\:ff0c\:53ea\:66b4\:9732\:7a33\:5b9a\:7684\:4f5c\:8005\:5143\:6570\:636e\:548c\:8ba1\:6570\:3002"]};
apiNotes["CreateFormulaTransformContext"] = {bi["A context is data, not asserted proof evidence. A later request must still discharge every condition through supported replayable methods.", "context \:662f\:6570\:636e\:ff0c\:4e0d\:662f\:8c03\:7528\:8005\:81ea\:884c\:65ad\:8a00\:7684\:8bc1\:660e evidence\:ff1b\:540e\:7eed\:8bf7\:6c42\:4ecd\:987b\:901a\:8fc7\:53d7\:652f\:6301\:7684\:53ef\:91cd\:653e\:65b9\:6cd5\:89e3\:9664\:6bcf\:4e2a\:6761\:4ef6\:3002"]};
apiNotes["ValidateFormulaTransformDerivation"] = {bi["Replay checks registry and rule digests, step continuity, match bindings, relation lifting, conditions, obligations, and cumulative cost.", "\:91cd\:653e\:4f1a\:68c0\:67e5 registry \:4e0e\:89c4\:5219\:6458\:8981\:3001\:6b65\:9aa4\:8fde\:7eed\:6027\:3001\:5339\:914d\:7ed1\:5b9a\:3001\:5173\:7cfb\:63d0\:5347\:3001\:6761\:4ef6\:3001\:4e49\:52a1\:548c\:7d2f\:8ba1\:6210\:672c\:3002"]};
apiNotes["CreateFormulaTransformCertificate"] = {bi["A certificate is intentionally stricter than a useful conditional derivation: no pending obligations may remain.", "\:8bc1\:4e66\:6709\:610f\:6bd4\:6709\:7528\:7684\:6761\:4ef6\:63a8\:5bfc\:66f4\:4e25\:683c\:ff1a\:4e0d\:80fd\:6b8b\:7559\:5f85\:89e3\:51b3\:4e49\:52a1\:3002"]};
apiNotes["FormulaTransformSteps"] = {bi["Rows are for reading; Raw records are for exact replay-oriented inspection.", "Rows \:7528\:4e8e\:9605\:8bfb\:ff1bRaw \:8bb0\:5f55\:7528\:4e8e\:9762\:5411\:7cbe\:786e\:91cd\:653e\:7684\:68c0\:67e5\:3002"]};
apiNotes["CheckFormulaTransformEquivalence"] = {bi["This is a bounded proof step over an audited algebraic whitelist, not a general evaluator or matcher.", "\:8fd9\:662f\:5728\:5ba1\:8ba1\:540e\:7684\:4ee3\:6570\:767d\:540d\:5355\:4e0a\:8fd0\:884c\:7684\:6709\:754c\:8bc1\:660e\:6b65\:9aa4\:ff0c\:4e0d\:662f\:901a\:7528\:6c42\:503c\:5668\:6216 matcher\:3002"]};

apiExamples = <|
  "ApplyFormulaTransform" -> {
    example["Apply a named Holder variant.", "\:5e94\:7528\:6307\:5b9a\:7684 Holder \:53d8\:4f53\:3002", "ApplyFormulaTransform[Abs[MeasureIntegral[f g, x, mu]], TransformationFamily -> \"Holder\", TransformationVariant -> \"AbsoluteUpper\"]", "<|\"Status\" -> \"Success\", \"Kind\" -> \"FormulaTransformResult\", \"Relation\" -> Abs[MeasureIntegral[f g, x, mu]] <= LpNorm[f, p, mu] LpNorm[g, q, mu], \"Obligations\" -> {...}, ...|>"],
    example["A missing family is an explicit failure.", "\:4e0d\:5b58\:5728\:7684\:5b9a\:7406\:65cf\:4f1a\:4ea7\:751f\:663e\:5f0f\:5931\:8d25\:3002", "ApplyFormulaTransform[x, TransformationFamily -> \"Missing\"]", "Failure[\"NoApplicableTransform\", <|...|>]" ]},
  "PlanFormulaTransform" -> {
    example["Plan toward an algebraically equivalent target.", "\:5411\:4ee3\:6570\:7b49\:4ef7\:76ee\:6807\:8fdb\:884c\:89c4\:5212\:3002", "PlanFormulaTransform[Abs[a b], TransformationFamily -> \"CauchySchwarz\", TransformationVariant -> \"EpsilonCauchy\", TargetRelation -> (Abs[a b] <= delta a^2 + b^2/(4 delta))]", "<|\"Status\" -> \"Success\", \"Kind\" -> \"FormulaTransformPlan\", \"Complete\" -> True, ...|>"],
    example["A bounded search can return its best partial plan.", "\:6709\:754c\:641c\:7d22\:53ef\:4ee5\:8fd4\:56de\:6700\:4f73\:90e8\:5206\:8ba1\:5212\:3002", "PlanFormulaTransform[expr, TargetRelation -> (expr <= target), MaxDepth -> 1]", "<|\"Status\" -> \"Success\", \"Complete\" -> False, \"Derivation\" -> <|...|>, ...|>" ]},
  "FindFormulaTransforms" -> {
    example["Discover Holder candidates without choosing one.", "\:53d1\:73b0 Holder \:5019\:9009\:800c\:4e0d\:81ea\:52a8\:9009\:62e9\:3002", "FindFormulaTransforms[Abs[MeasureIntegral[f g, x, mu]], TransformationFamily -> \"Holder\"]", "<|\"Kind\" -> \"FormulaTransformCandidates\", \"CandidateCount\" -> 1, \"Candidates\" -> {<|\"CandidateId\" -> ..., ...|>}, ...|>"],
    example["Ask for both recoverable inequality directions.", "\:67e5\:8be2\:4e24\:4e2a\:53ef\:6062\:590d\:7684\:4e0d\:7b49\:5f0f\:65b9\:5411\:3002", "FindFormulaTransforms[expr, TransformationDirection -> All]", "<|\"Status\" -> \"Success\", \"Candidates\" -> {...}|>" ]},
  "FormulaTransform" -> {
    example["Use the unified Association request.", "\:4f7f\:7528\:7edf\:4e00\:7684 Association \:8bf7\:6c42\:3002", "FormulaTransform[<|\"Action\" -> \"Find\", \"Expression\" -> HoldComplete[Abs[a b]], \"Family\" -> \"Young\"|>]", "<|\"Status\" -> \"Success\", \"Kind\" -> \"FormulaTransformCandidates\", ...|>"],
    example["Unknown keys are not silently ignored.", "\:672a\:77e5\:952e\:4e0d\:4f1a\:88ab\:9759\:9ed8\:5ffd\:7565\:3002", "FormulaTransform[<|\"Action\" -> \"Find\", \"Expression\" -> HoldComplete[x], \"Famliy\" -> \"Young\"|>]", "Failure[\"InvalidRequest\", <|\"Keys\" -> {\"Famliy\"}, ...|>]" ]},
  "CompileFormulaTransformFamily" -> {
    example["Compile a minimal equality family.", "\:7f16\:8bd1\:4e00\:4e2a\:6700\:5c0f\:7b49\:5f0f\:5b9a\:7406\:65cf\:3002", "CompileFormulaTransformFamily[<|\"SchemaVersion\" -> 1, \"Kind\" -> \"TransformFamily\", \"Name\" -> \"Square\", \"Variants\" -> {<|\"Name\" -> \"Expand\", \"Match\" -> \"(a_ + b_)^2\", \"Result\" -> \"(a + b)^2 == a^2 + 2 a b + b^2\"|>}|>]", "<|\"Status\" -> \"Compiled\", \"Stage\" -> \"CoreRule\", \"Kind\" -> \"TransformFamily\", ...|>"],
    example["Wrong field types retain their schema path.", "\:9519\:8bef\:5b57\:6bb5\:7c7b\:578b\:4f1a\:4fdd\:7559 schema \:8def\:5f84\:3002", "CompileFormulaTransformFamily[<|\"SchemaVersion\" -> 1, \"Kind\" -> \"TransformFamily\", \"Name\" -> \"Bad\", \"Conditions\" -> {}, \"Variants\" -> {}|>]", "Failure[\"InvalidRuleIR\", <|\"Path\" -> \"Conditions\", ...|>]" ]},
  "CompileFormulaTransformMonotonicityDescriptor" -> {
    example["Compile a positive-measure integral lift.", "\:7f16\:8bd1\:6b63\:6d4b\:5ea6\:79ef\:5206\:7684\:5173\:7cfb\:63d0\:5347\:3002", "CompileFormulaTransformMonotonicityDescriptor[<|\"SchemaVersion\" -> 1, \"Kind\" -> \"MonotonicityDescriptor\", \"Name\" -> \"PositiveIntegral\", \"Match\" -> \"MeasureIntegral[body_, x_, mu_]\", \"ArgumentPosition\" -> 1, \"Direction\" -> \"Increasing\", \"Strict\" -> False, \"Conditions\" -> \"{PositiveMeasure[mu], IntegrableOn[from, mu], IntegrableOn[to, mu]}\"|>]", "<|\"Status\" -> \"Compiled\", \"Kind\" -> \"MonotonicityDescriptor\", ...|>"],
    example["An out-of-range argument position is rejected.", "\:8d8a\:754c\:7684\:53c2\:6570\:4f4d\:7f6e\:4f1a\:88ab\:62d2\:7edd\:3002", "CompileFormulaTransformMonotonicityDescriptor[<|\"SchemaVersion\" -> 1, \"Kind\" -> \"MonotonicityDescriptor\", \"Name\" -> \"Bad\", \"Match\" -> \"Abs[x_]\", \"ArgumentPosition\" -> 2, \"Direction\" -> \"Increasing\", \"Strict\" -> False, \"Conditions\" -> \"{}\"|>]", "Failure[\"InvalidRuleIR\", <|\"Path\" -> \"ArgumentPosition\", ...|>]" ]},
  "CompileFormulaTransformSource" -> {
    example["Compile one tracked author source.", "\:7f16\:8bd1\:4e00\:4e2a\:53d7\:7248\:672c\:7ba1\:7406\:7684\:4f5c\:8005\:6e90\:6587\:4ef6\:3002", "CompileFormulaTransformSource[\"Registry/Sources/Holder.ftr.md\"]", "<|\"Status\" -> \"Compiled\", \"SourceFile\" -> \"Registry/Sources/Holder.ftr.md\", \"Variants\" -> {...}, ...|>"],
    example["Diagnostics point back to the source file.", "\:8bca\:65ad\:4f1a\:6307\:56de\:6e90\:6587\:4ef6\:3002", "CompileFormulaTransformSource[\"Tests/Fixtures/InvalidResultSyntax.ftr.md\"]", "Failure[\"InvalidRuleIR\", <|\"File\" -> ..., \"Line\" -> ..., \"Column\" -> ..., \"Path\" -> \"Variants[1].Result\", ...|>]" ]},
  "CreateFormulaTransformRegistry" -> {
    example["Create a registry from compiled families.", "\:4ece\:5df2\:7f16\:8bd1\:5b9a\:7406\:65cf\:521b\:5efa registry\:3002", "CreateFormulaTransformRegistry[family1, family2]", "<|\"Kind\" -> \"FormulaTransformRegistry\", \"RegistryDigest\" -> ..., \"Families\" -> <|...|>, ...|>"],
    example["Invalid input is rejected instead of stored.", "\:65e0\:6548\:8f93\:5165\:4f1a\:88ab\:62d2\:7edd\:800c\:4e0d\:662f\:88ab\:5b58\:50a8\:3002", "CreateFormulaTransformRegistry[<||>]", "Failure[\"InvalidRuleIR\", <|...|>]" ]},
  "LoadFormulaTransformRegistry" -> {
    example["Load the tracked JSON IR directory.", "\:52a0\:8f7d\:53d7\:7248\:672c\:7ba1\:7406\:7684 JSON IR \:76ee\:5f55\:3002", "registry = LoadFormulaTransformRegistry[\"Registry/IR\"]", "<|\"Kind\" -> \"FormulaTransformRegistry\", \"RegistryDigest\" -> ..., ...|>"],
    example["A missing directory fails explicitly.", "\:4e0d\:5b58\:5728\:7684\:76ee\:5f55\:4f1a\:663e\:5f0f\:5931\:8d25\:3002", "LoadFormulaTransformRegistry[\"missing\"]", "Failure[\"RegistryLoadFailed\", <|...|>]" ]},
  "InspectFormulaTransformRegistry" -> {
    example["Inspect the built-in registry.", "\:68c0\:67e5\:5185\:7f6e registry\:3002", "InspectFormulaTransformRegistry[]", "<|\"Status\" -> \"Success\", \"Families\" -> {...}, \"Index\" -> <|\"Ready\" -> True, ...|>, ...|>"],
    example["Ordinary Associations are not registries.", "\:666e\:901a Association \:4e0d\:662f registry\:3002", "InspectFormulaTransformRegistry[<||>]", "Failure[\"MalformedRegistry\", <|...|>]" ]},
  "CreateFormulaTransformContext" -> {
    example["Collect analytic declarations immutably.", "\:4ee5\:4e0d\:53ef\:53d8\:65b9\:5f0f\:6536\:96c6\:5206\:6790\:58f0\:660e\:3002", "CreateFormulaTransformContext[MemLp[f, 2, mu], MemLp[g, 2, mu]]", "<|\"Kind\" -> \"FormulaTransformContext\", \"Assumptions\" -> {}, \"Declarations\" -> {MemLp[f, 2, mu], MemLp[g, 2, mu]}|>"],
    example["Text notes are not mathematical declarations.", "\:6587\:672c\:5907\:6ce8\:4e0d\:662f\:6570\:5b66\:58f0\:660e\:3002", "CreateFormulaTransformContext[\"f is square integrable\"]", "Failure[\"InvalidContextDeclaration\", <|...|>]" ]},
  "ValidateFormulaTransformDerivation" -> {
    example["Replay a recorded derivation.", "\:91cd\:653e\:5df2\:8bb0\:5f55\:63a8\:5bfc\:3002", "ValidateFormulaTransformDerivation[result[\"Derivation\"]]", "<|\"ValidationStatus\" -> \"Valid\", ...|>"],
    example["Malformed data is invalid, not conditionally accepted.", "\:975e\:6cd5\:6570\:636e\:662f\:65e0\:6548\:7684\:ff0c\:4e0d\:4f1a\:88ab\:6761\:4ef6\:63a5\:53d7\:3002", "ValidateFormulaTransformDerivation[<||>]", "<|\"ValidationStatus\" -> \"Invalid\", \"Reason\" -> \"MalformedDerivation\"|>" ]},
  "CreateFormulaTransformCertificate" -> {
    example["Certify an unconditional replay.", "\:4e3a\:65e0\:6761\:4ef6\:91cd\:653e\:521b\:5efa\:8bc1\:4e66\:3002", "CreateFormulaTransformCertificate[result[\"Derivation\"]]", "<|\"Kind\" -> \"FormulaTransformCertificate\", \"Validation\" -> <|\"ValidationStatus\" -> \"Valid\", ...|>, ...|>"],
    example["Pending obligations prevent certification.", "\:5f85\:89e3\:51b3\:4e49\:52a1\:4f1a\:963b\:6b62\:8bc1\:4e66\:751f\:6210\:3002", "CreateFormulaTransformCertificate[conditionalDerivation]", "Failure[\"UnverifiedDerivation\", <|...|>]" ]},
  "FormulaTransformSteps" -> {
    example["Display readable replay rows.", "\:663e\:793a\:6613\:8bfb\:7684\:91cd\:653e\:884c\:3002", "FormulaTransformSteps[ApplyFormulaTransform[Abs[MeasureIntegral[f g, x, mu]]]]", "Dataset[{<|\"Rule\" -> \"Holder/AbsoluteUpper\", \"Input\" -> ..., \"Output\" -> ..., ...|>}]"],
    example["Request complete replay records.", "\:8bf7\:6c42\:5b8c\:6574\:91cd\:653e\:8bb0\:5f55\:3002", "FormulaTransformSteps[result, \"Raw\"]", "{<|\"RuleId\" -> ..., \"Bindings\" -> ..., \"Conditions\" -> ..., \"Obligations\" -> ..., ...|>}" ]},
  "CheckFormulaTransformEquivalence" -> {
    example["Prove a bounded algebraic equivalence.", "\:8bc1\:660e\:4e00\:4e2a\:6709\:754c\:4ee3\:6570\:7b49\:4ef7\:3002", "CheckFormulaTransformEquivalence[a/b + c, (a + b c)/b, Assumptions -> b != 0]", "<|\"Result\" -> \"Proved\", \"Method\" -> \"FullSimplify\", \"TimedOut\" -> False, ...|>"],
    example["Unsupported executable syntax is not evaluated.", "\:4e0d\:53d7\:652f\:6301\:7684\:53ef\:6267\:884c\:8bed\:6cd5\:4e0d\:4f1a\:88ab\:6c42\:503c\:3002", "CheckFormulaTransformEquivalence[Run[\"command\"], 0]", "<|\"Result\" -> \"Unknown\", \"Method\" -> \"HeldASTAudit\", \"Reason\" -> \"UnsafeExpression\"|>" ]}
|>;

apiSeeAlso = <|
  "ApplyFormulaTransform" -> {"FindFormulaTransforms", "PlanFormulaTransform", "FormulaTransformSteps"},
  "PlanFormulaTransform" -> {"ApplyFormulaTransform", "FindFormulaTransforms", "CheckFormulaTransformEquivalence"},
  "FindFormulaTransforms" -> {"ApplyFormulaTransform", "PlanFormulaTransform", "FormulaTransform"},
  "FormulaTransform" -> {"ApplyFormulaTransform", "FindFormulaTransforms", "PlanFormulaTransform"},
  "CompileFormulaTransformFamily" -> {"CompileFormulaTransformSource", "CreateFormulaTransformRegistry"},
  "CompileFormulaTransformMonotonicityDescriptor" -> {"CompileFormulaTransformSource", "CreateFormulaTransformRegistry"},
  "CompileFormulaTransformSource" -> {"CompileFormulaTransformFamily", "CompileFormulaTransformMonotonicityDescriptor", "LoadFormulaTransformRegistry"},
  "CreateFormulaTransformRegistry" -> {"LoadFormulaTransformRegistry", "InspectFormulaTransformRegistry"},
  "LoadFormulaTransformRegistry" -> {"CreateFormulaTransformRegistry", "InspectFormulaTransformRegistry"},
  "InspectFormulaTransformRegistry" -> {"CreateFormulaTransformRegistry", "LoadFormulaTransformRegistry"},
  "CreateFormulaTransformContext" -> {"ApplyFormulaTransform", "MemLp", "IntegrableOn"},
  "ValidateFormulaTransformDerivation" -> {"CreateFormulaTransformCertificate", "FormulaTransformSteps"},
  "CreateFormulaTransformCertificate" -> {"ValidateFormulaTransformDerivation", "FormulaTransformSteps"},
  "FormulaTransformSteps" -> {"ValidateFormulaTransformDerivation", "CreateFormulaTransformCertificate"},
  "CheckFormulaTransformEquivalence" -> {"PlanFormulaTransform", "ApplyFormulaTransform"}
|>;

primitiveDescriptions = <|
  "MeasureIntegral" -> bi["an inert integral over a measure", "\:5173\:4e8e\:6d4b\:5ea6\:7684\:60f0\:6027\:79ef\:5206"],
  "LpNorm" -> bi["an inert L-p norm over a measure", "\:5173\:4e8e\:6d4b\:5ea6\:7684\:60f0\:6027 L-p \:8303\:6570"],
  "CountingMeasure" -> bi["the counting measure induced by a sum iterator", "\:7531\:6c42\:548c\:8fed\:4ee3\:5668\:8bf1\:5bfc\:7684\:8ba1\:6570\:6d4b\:5ea6"],
  "RegionMeasureObject" -> bi["the measure induced by a Wolfram region", "\:7531 Wolfram \:533a\:57df\:8bf1\:5bfc\:7684\:6d4b\:5ea6"],
  "LebesgueMeasure" -> bi["one-dimensional Lebesgue measure on an interval", "\:533a\:95f4\:4e0a\:7684\:4e00\:7ef4 Lebesgue \:6d4b\:5ea6"],
  "EuclideanMeasure" -> bi["Lebesgue measure on Euclidean n-space", "\:6b27\:6c0f n \:7ef4\:7a7a\:95f4\:4e0a\:7684 Lebesgue \:6d4b\:5ea6"],
  "AlmostEverywhere" -> bi["an almost-everywhere proposition with respect to a measure", "\:76f8\:5bf9\:4e8e\:6d4b\:5ea6\:7684\:51e0\:4e4e\:5904\:5904\:547d\:9898"],
  "RiemannianVolumeMeasure" -> bi["the volume measure determined by a manifold and metric", "\:7531\:6d41\:5f62\:548c\:5ea6\:91cf\:786e\:5b9a\:7684\:4f53\:79ef\:6d4b\:5ea6"],
  "RiemannianGradientEnergy" -> bi["the scalar Dirichlet energy of an expression", "\:8868\:8fbe\:5f0f\:7684\:6807\:91cf Dirichlet \:80fd\:91cf"],
  "SmoothCompactRiemannianManifold" -> bi["a smooth compact Riemannian-manifold premise", "\:5149\:6ed1\:7d27 Riemann \:6d41\:5f62\:524d\:63d0"],
  "Boundaryless" -> bi["a no-boundary proposition for a manifold", "\:6d41\:5f62\:65e0\:8fb9\:754c\:547d\:9898"],
  "BoundaryPairing" -> bi["the inert boundary term produced by integration by parts", "\:5206\:90e8\:79ef\:5206\:4ea7\:751f\:7684\:60f0\:6027\:8fb9\:754c\:9879"],
  "TransformParameter" -> bi["an unresolved named rule parameter in engine output", "\:5f15\:64ce\:8f93\:51fa\:4e2d\:7684\:672a\:89e3\:6790\:547d\:540d\:89c4\:5219\:53c2\:6570"],
  "TheoremConstant" -> bi["a stable opaque constant introduced by a theorem", "\:7531\:5b9a\:7406\:5f15\:5165\:7684\:7a33\:5b9a\:4e0d\:900f\:660e\:5e38\:6570"],
  "PositiveMeasure" -> bi["the proposition that a measure preserves nonnegative inequalities under integration", "\:6d4b\:5ea6\:5728\:79ef\:5206\:4e0b\:4fdd\:6301\:975e\:8d1f\:4e0d\:7b49\:5f0f\:7684\:547d\:9898"],
  "MemLp" -> bi["finite L-p membership stated as a proposition", "\:4ee5\:547d\:9898\:8868\:793a\:7684\:6709\:9650 L-p \:53ef\:79ef\:6027"],
  "MemSobolev" -> bi["Sobolev regularity stated without constructing a space object", "\:4e0d\:6784\:9020\:7a7a\:95f4\:5bf9\:8c61\:800c\:9648\:8ff0\:7684 Sobolev \:6b63\:5219\:6027"],
  "IntegrableOn" -> bi["integrability of an expression with respect to a measure", "\:8868\:8fbe\:5f0f\:76f8\:5bf9\:4e8e\:6d4b\:5ea6\:7684\:53ef\:79ef\:6027"],
  "IntegrationByPartsAdmissible" -> bi["the combined analytic premise required for integration by parts", "\:5206\:90e8\:79ef\:5206\:6240\:9700\:7684\:7efc\:5408\:5206\:6790\:524d\:63d0"],
  "BoundaryValue" -> bi["an inert trace or boundary value", "\:60f0\:6027\:7684\:8ff9\:6216\:8fb9\:754c\:503c"],
  "Convolution" -> bi["an inert continuous convolution value", "\:60f0\:6027\:8fde\:7eed\:5377\:79ef\:503c"],
  "DiscreteConvolution" -> bi["an inert discrete convolution value", "\:60f0\:6027\:79bb\:6563\:5377\:79ef\:503c"],
  "MeasureOf" -> bi["the measure of a predicate-defined set", "\:7531\:8c13\:8bcd\:5b9a\:4e49\:96c6\:5408\:7684\:6d4b\:5ea6"],
  "AEMeasurable" -> bi["almost-everywhere measurability with respect to a measure", "\:76f8\:5bf9\:4e8e\:6d4b\:5ea6\:7684\:51e0\:4e4e\:5904\:5904\:53ef\:6d4b\:6027"]
|>;

primitiveForms = <|
  "MeasureIntegral" -> "MeasureIntegral[f, x, mu]", "LpNorm" -> "LpNorm[f, p, mu]",
  "CountingMeasure" -> "CountingMeasure[iterator]", "RegionMeasureObject" -> "RegionMeasureObject[region]",
  "LebesgueMeasure" -> "LebesgueMeasure[x, a, b]", "EuclideanMeasure" -> "EuclideanMeasure[n]",
  "AlmostEverywhere" -> "AlmostEverywhere[mu, proposition]",
  "RiemannianVolumeMeasure" -> "RiemannianVolumeMeasure[M, g]",
  "RiemannianGradientEnergy" -> "RiemannianGradientEnergy[u, M, g]",
  "SmoothCompactRiemannianManifold" -> "SmoothCompactRiemannianManifold[M, g, n]",
  "Boundaryless" -> "Boundaryless[M]", "BoundaryPairing" -> "BoundaryPairing[expr, x, mu]",
  "TransformParameter" -> "TransformParameter[family, name]",
  "TheoremConstant" -> "TheoremConstant[family, name, dependencies]",
  "PositiveMeasure" -> "PositiveMeasure[mu]", "MemLp" -> "MemLp[f, p, mu]",
  "MemSobolev" -> "MemSobolev[f, k, p, mu]", "IntegrableOn" -> "IntegrableOn[f, mu]",
  "IntegrationByPartsAdmissible" -> "IntegrationByPartsAdmissible[u, v, x, mu]",
  "BoundaryValue" -> "BoundaryValue[f, point]", "Convolution" -> "Convolution[f, g, x]",
  "DiscreteConvolution" -> "DiscreteConvolution[a, b, n]", "MeasureOf" -> "MeasureOf[condition, x, mu]",
  "AEMeasurable" -> "AEMeasurable[f, mu]"
|>;

primitiveUseExamples = <|
  "MeasureIntegral" -> "Abs[MeasureIntegral[f g, x, mu]]",
  "LpNorm" -> "LpNorm[f, p, mu] LpNorm[g, q, mu]",
  "CountingMeasure" -> "MeasureIntegral[a[i], i, CountingMeasure[{i, 1, n}]]",
  "RegionMeasureObject" -> "MeasureIntegral[f, x, RegionMeasureObject[region]]",
  "LebesgueMeasure" -> "MeasureIntegral[f, x, LebesgueMeasure[x, 0, 1]]",
  "EuclideanMeasure" -> "LpNorm[f, 2, EuclideanMeasure[n]]",
  "AlmostEverywhere" -> "AlmostEverywhere[mu, Element[f, Reals] && f >= 0]",
  "RiemannianVolumeMeasure" -> "LpNorm[u, 2, RiemannianVolumeMeasure[M, g]]",
  "RiemannianGradientEnergy" -> "RiemannianGradientEnergy[u, M, g] >= 0",
  "SmoothCompactRiemannianManifold" -> "SmoothCompactRiemannianManifold[M, g, n]",
  "Boundaryless" -> "Boundaryless[M]",
  "BoundaryPairing" -> "BoundaryPairing[u v, x, mu]",
  "TransformParameter" -> "TransformParameter[\"Holder\", \"p\"]",
  "TheoremConstant" -> "TheoremConstant[\"Sobolev\", \"A\", {M, g}]",
  "PositiveMeasure" -> "CreateFormulaTransformContext[PositiveMeasure[mu]]",
  "MemLp" -> "CreateFormulaTransformContext[MemLp[f, 2, mu]]",
  "MemSobolev" -> "CreateFormulaTransformContext[MemSobolev[u, 1, 2, mu]]",
  "IntegrableOn" -> "CreateFormulaTransformContext[IntegrableOn[f, mu]]",
  "IntegrationByPartsAdmissible" -> "IntegrationByPartsAdmissible[u, v, x, mu]",
  "BoundaryValue" -> "BoundaryValue[u, 0] == 0",
  "Convolution" -> "LpNorm[Convolution[f, g, x], r, mu]",
  "DiscreteConvolution" -> "LpNorm[DiscreteConvolution[a, b, n], r, CountingMeasure[n]]",
  "MeasureOf" -> "MeasureIntegral[MeasureOf[f > t, x, mu], t, LebesgueMeasure[t, 0, Infinity]]",
  "AEMeasurable" -> "CreateFormulaTransformContext[AEMeasurable[f, mu]]"
|>;

primitiveSpecialNotes = AssociationThread[primitiveSymbols, ConstantArray[{}, Length[primitiveSymbols]]];
primitiveSpecialNotes["MeasureIntegral"] = {bi["The second argument is a lexical binder. Repeated uses of the same author slot are unified by the compiler.", "\:7b2c\:4e8c\:4e2a\:53c2\:6570\:662f\:8bcd\:6cd5 binder\:ff1b\:540c\:4e00\:4f5c\:8005 slot \:7684\:91cd\:590d\:51fa\:73b0\:7531\:7f16\:8bd1\:5668\:7edf\:4e00\:3002"]};
primitiveSpecialNotes["MeasureOf"] = {bi["The second argument binds the variable occurring in the predicate, mirroring measure-theory set-builder statements.", "\:7b2c\:4e8c\:4e2a\:53c2\:6570\:7ed1\:5b9a\:8c13\:8bcd\:4e2d\:7684\:53d8\:91cf\:ff0c\:5bf9\:5e94\:6d4b\:5ea6\:8bba\:7684\:96c6\:5408\:6784\:9020\:9648\:8ff0\:3002"]};
primitiveSpecialNotes["LpNorm"] = {bi["LpNorm is a scalar functional, never a constructor for a function-space object.", "LpNorm \:662f\:6807\:91cf\:6cdb\:51fd\:ff0c\:7edd\:4e0d\:662f\:51fd\:6570\:7a7a\:95f4\:5bf9\:8c61\:7684\:6784\:9020\:5668\:3002"]};
primitiveSpecialNotes["MemLp"] = {bi["Use MemLp in Conditions or a context when the theorem needs finite L-p norm; do not encode membership as LpNorm[f,p,mu] < Infinity.", "\:5b9a\:7406\:9700\:8981\:6709\:9650 L-p \:8303\:6570\:65f6\:ff0c\:5728 Conditions \:6216 context \:4e2d\:4f7f\:7528 MemLp\:ff1b\:4e0d\:8981\:5199\:6210 LpNorm[f,p,mu] < Infinity\:3002"]};
primitiveSpecialNotes["MemSobolev"] = {bi["The engine transforms numbers, functions, and functionals; this proposition records regularity without manipulating a Sobolev-space object.", "\:5f15\:64ce\:4e3b\:8981\:53d8\:6362\:6570\:3001\:51fd\:6570\:548c\:6cdb\:51fd\:ff1b\:8be5\:547d\:9898\:8bb0\:5f55\:6b63\:5219\:6027\:ff0c\:800c\:4e0d\:64cd\:4f5c Sobolev \:7a7a\:95f4\:5bf9\:8c61\:3002"]};
primitiveSpecialNotes["TransformParameter"] = {bi["This head is normally produced by the engine when a parameter remains unresolved; rule authors declare parameters in YAML instead of writing this head in Match or Result.", "\:8be5 head \:901a\:5e38\:7531\:5f15\:64ce\:5728\:53c2\:6570\:672a\:89e3\:6790\:65f6\:4ea7\:751f\:ff1b\:89c4\:5219\:4f5c\:8005\:5e94\:5728 YAML \:4e2d\:58f0\:660e\:53c2\:6570\:ff0c\:800c\:4e0d\:662f\:5728 Match \:6216 Result \:4e2d\:624b\:5199\:6b64 head\:3002"]};
primitiveSpecialNotes["TheoremConstant"] = {bi["This head is normally produced from GeneratedParameters. It preserves theorem identity and dependencies without guessing a numeric value.", "\:8be5 head \:901a\:5e38\:7531 GeneratedParameters \:4ea7\:751f\:ff1b\:5b83\:4fdd\:7559\:5b9a\:7406\:8eab\:4efd\:548c\:4f9d\:8d56\:ff0c\:800c\:4e0d\:731c\:6d4b\:6570\:503c\:3002"]};
primitiveSpecialNotes["CountingMeasure"] = {bi["The one-argument form is the author-facing form. The three-argument form is reserved for normalized native sum adapters.", "\:5355\:53c2\:6570\:5f62\:5f0f\:9762\:5411\:89c4\:5219\:4f5c\:8005\:ff1b\:4e09\:53c2\:6570\:5f62\:5f0f\:4fdd\:7559\:7ed9\:89c4\:8303\:5316\:540e\:7684\:539f\:751f\:6c42\:548c\:9002\:914d\:5668\:3002"]};
primitiveSpecialNotes["IntegrationByPartsAdmissible"] = {bi["This premise intentionally combines regularity, integrability, measure compatibility, and trace requirements that the engine cannot infer safely.", "\:8be5\:524d\:63d0\:6709\:610f\:5408\:5e76\:5f15\:64ce\:65e0\:6cd5\:5b89\:5168\:63a8\:65ad\:7684\:6b63\:5219\:6027\:3001\:53ef\:79ef\:6027\:3001\:6d4b\:5ea6\:517c\:5bb9\:6027\:548c\:8ff9\:8981\:6c42\:3002"]};

roleNames = <|
  "English" -> <|"Expression" -> "expression", "Binder" -> "binder", "Measure" -> "measure", "Scalar" -> "scalar", "NonnegativeScalar" -> "nonnegative scalar", "Exponent" -> "exponent", "Iterator" -> "iterator", "Region" -> "region", "Coordinate" -> "coordinate", "Endpoint" -> "endpoint", "Dimension" -> "dimension", "Proposition" -> "proposition", "Manifold" -> "manifold", "Metric" -> "metric", "Name" -> "name", "Dependencies" -> "dependencies", "Order" -> "order", "Index" -> "index", "Unknown" -> "unspecified"|>,
  "ChineseSimplified" -> <|"Expression" -> "\:8868\:8fbe\:5f0f", "Binder" -> "binder", "Measure" -> "\:6d4b\:5ea6", "Scalar" -> "\:6807\:91cf", "NonnegativeScalar" -> "\:975e\:8d1f\:6807\:91cf", "Exponent" -> "\:6307\:6570", "Iterator" -> "\:8fed\:4ee3\:5668", "Region" -> "\:533a\:57df", "Coordinate" -> "\:5750\:6807", "Endpoint" -> "\:7aef\:70b9", "Dimension" -> "\:7ef4\:6570", "Proposition" -> "\:547d\:9898", "Manifold" -> "\:6d41\:5f62", "Metric" -> "\:5ea6\:91cf", "Name" -> "\:540d\:79f0", "Dependencies" -> "\:4f9d\:8d56", "Order" -> "\:9636\:6570", "Index" -> "\:7d22\:5f15", "Unknown" -> "\:672a\:6307\:5b9a"|>
|>;
roleLabel[role_String, language_String] := Lookup[Lookup[roleNames, language], role, role];

usageCell[name_String, forms_List, summary_String] := Cell[
  TextData@Join[
    Flatten@Riffle[({referenceLink[name], StyleBox[StringDrop[#, StringLength[name]], "InlineFormula"]} & /@ forms), {"\n"}],
    {" \[LongDash] " <> summary <> "."}
  ],
  "Usage"
];

loadCells[language_String] := {
  Cell[If[language === "English", "Load the paclet.", "\:8f7d\:5165 Paclet\:3002"], "ExampleText"],
  Cell[BoxData["Needs[\"Lightmarey`FormulaTransformEngine`\"]"], "Input"],
  Cell[BoxData["Null"], "Output"]
};

exampleCells[examples_List, language_String] := Flatten[
  ({Cell[localized[Lookup[#, "Text"], language], "ExampleText"],
     Cell[BoxData[Lookup[#, "Input"]], "Input"], Cell[BoxData[Lookup[#, "Output"]], "Output"]} &) /@ examples
];

optionCells[names_List, language_String] := If[names === {}, {}, Join[
  {Cell[If[language === "English", "Options", "\:9009\:9879"], "NotesSection"]},
  (Cell[TextData[{StyleBox[#, "InlineFormula"], " \[LongDash] " <> localized[optionDescriptions[#], language]}], "Notes"] & /@ names)
]];

seeAlsoCells[names_List, language_String] := If[names === {}, {}, {
  Cell[If[language === "English", "See Also", "\:53c2\:89c1"], "SeeAlsoSection"],
  Cell[TextData@Riffle[referenceLink /@ names, "   "], "SeeAlso"]
}];

categorizationCells[name_String] := CellGroupData[{
  Cell["Categorization", "CategorizationSection"],
  Cell["Symbol", "Categorization", CellLabel -> "Entity Type"],
  Cell["Lightmarey/FormulaTransformEngine", "Categorization", CellLabel -> "Paclet Name"],
  Cell["Lightmarey`FormulaTransformEngine`", "Categorization", CellLabel -> "Context"],
  Cell["Lightmarey/FormulaTransformEngine/ref/" <> name, "Categorization", CellLabel -> "URI"]
}, Closed];

apiPage[name_String, language_String] := Notebook[Join[
  {Cell[categorizationCells[name]], Cell[name, "ObjectName"],
   usageCell[name, apiForms[name], localized[apiDescriptions[name], language]],
   Cell[If[language === "English", "Details", "\:8be6\:7ec6\:4fe1\:606f"], "NotesSection"],
   Cell[(If[language === "English", "Return contract: ", "\:8fd4\:56de\:5951\:7ea6\:ff1a"]) <> localized[apiReturns[name], language], "Notes", CellTags -> "ReturnContract"],
   Cell[(If[language === "English", "Failure contract: ", "\:5931\:8d25\:5951\:7ea6\:ff1a"]) <> localized[apiFailures[name], language], "Notes", CellTags -> "FailureContract"]},
  (Cell[localized[#, language], "Notes"] & /@ apiNotes[name]),
  optionCells[optionsFor[name], language],
  {Cell[If[language === "English", "Examples", "\:8303\:4f8b"], "PrimaryExamplesSection"]},
  loadCells[language], exampleCells[apiExamples[name], language], seeAlsoCells[apiSeeAlso[name], language]
], TaggingRules -> <|"Paclet" -> "Lightmarey/FormulaTransformEngine", "Language" -> language|>,
  StyleDefinitions -> FrontEnd`FileName[{"Wolfram"}, "FunctionPageStylesExt.nb", CharacterEncoding -> "UTF-8"]];

primitiveArityNote[name_String, language_String] := Module[{spec = primitiveSpecs[name], arities, arguments, result, binders},
  arities = StringRiffle[ToString /@ Lookup[spec, "Arity"], If[language === "English", " or ", " \:6216 "]];
  arguments = roleLabel[#, language] & /@ Lookup[spec, "Arguments", {}];
  result = roleLabel[Lookup[spec, "Result", "Unknown"], language];
  binders = Lookup[spec, "BinderPositions", {}];
  If[language === "English",
    "Primitive specification: accepted arity " <> arities <> "; argument roles " <> ToString[arguments, InputForm] <>
      "; result role " <> result <> If[binders === {}, ".", "; binder position " <> StringRiffle[ToString /@ binders, ", "] <> "."],
    "\:539f\:8bed\:89c4\:683c\:ff1a\:63a5\:53d7\:53c2\:6570\:4e2a\:6570 " <> arities <> "\:ff1b\:53c2\:6570\:89d2\:8272 " <> ToString[arguments, InputForm] <>
      "\:ff1b\:7ed3\:679c\:89d2\:8272 " <> result <> If[binders === {}, "\:3002", "\:ff1bbinder \:4f4d\:7f6e " <> StringRiffle[ToString /@ binders, "\:3001"] <> "\:3002"]
  ]
];

primitiveSeeAlso[name_String] := DeleteCases[Switch[name,
  "MeasureIntegral", {"LpNorm", "MeasureOf", "PositiveMeasure", "IntegrableOn"},
  "LpNorm", {"MeasureIntegral", "MemLp", "MemSobolev"},
  "MeasureOf", {"MeasureIntegral", "LebesgueMeasure", "AEMeasurable"},
  "Convolution" | "DiscreteConvolution", {"LpNorm", "MemLp"},
  "TransformParameter" | "TheoremConstant", {"CompileFormulaTransformFamily", "FormulaTransformSteps"},
  "BoundaryPairing" | "BoundaryValue" | "IntegrationByPartsAdmissible", {"MeasureIntegral", "IntegrableOn"},
  "RiemannianVolumeMeasure" | "RiemannianGradientEnergy" | "SmoothCompactRiemannianManifold" | "Boundaryless", {"LpNorm", "MemSobolev"},
  _, {"CreateFormulaTransformContext", "ApplyFormulaTransform"}
], name];

primitivePage[name_String, language_String] := Notebook[Join[
  {Cell[categorizationCells[name]], Cell[name, "ObjectName"],
   usageCell[name, {primitiveForms[name]}, localized[primitiveDescriptions[name], language]],
   Cell[If[language === "English", "Details", "\:8be6\:7ec6\:4fe1\:606f"], "NotesSection"],
   Cell[primitiveArityNote[name, language], "Notes", CellTags -> "PrimitiveSpecification"],
   Cell[If[language === "English",
      "The head is inert: it records mathematical meaning for compilation, matching, replay, and display, but does not evaluate the represented operation.",
      "\:8be5 head \:662f\:60f0\:6027\:7684\:ff1a\:5b83\:4e3a\:7f16\:8bd1\:3001\:5339\:914d\:3001\:91cd\:653e\:548c\:663e\:793a\:8bb0\:5f55\:6570\:5b66\:542b\:4e49\:ff0c\:4f46\:4e0d\:4f1a\:8ba1\:7b97\:6240\:8868\:793a\:7684\:8fd0\:7b97\:3002"], "Notes"],
   Cell[If[language === "English",
      "Compiler and runtime legality checks use the same primitive specification. Wrong arity or a known role contradiction is rejected.",
      "\:7f16\:8bd1\:671f\:548c\:8fd0\:884c\:671f\:5408\:6cd5\:6027\:68c0\:67e5\:4f7f\:7528\:540c\:4e00\:4efd\:539f\:8bed\:89c4\:683c\:ff1b\:53c2\:6570\:4e2a\:6570\:9519\:8bef\:6216\:5df2\:77e5\:89d2\:8272\:77db\:76fe\:4f1a\:88ab\:62d2\:7edd\:3002"], "Notes", CellTags -> "FailureContract"]},
  (Cell[localized[#, language], "Notes"] & /@ primitiveSpecialNotes[name]),
  {Cell[If[language === "English", "Examples", "\:8303\:4f8b"], "PrimaryExamplesSection"]},
  loadCells[language],
  exampleCells[{
    example["Construct the inert mathematical object.", "\:6784\:9020\:60f0\:6027\:6570\:5b66\:5bf9\:8c61\:3002", primitiveForms[name], primitiveForms[name]],
    example["Use the primitive in a formula, condition, or context.", "\:5728\:516c\:5f0f\:3001\:6761\:4ef6\:6216 context \:4e2d\:4f7f\:7528\:8be5\:539f\:8bed\:3002", primitiveUseExamples[name], primitiveUseExamples[name]]
  }, language],
  seeAlsoCells[primitiveSeeAlso[name], language]
], TaggingRules -> <|"Paclet" -> "Lightmarey/FormulaTransformEngine", "Language" -> language|>,
  StyleDefinitions -> FrontEnd`FileName[{"Wolfram"}, "FunctionPageStylesExt.nb", CharacterEncoding -> "UTF-8"]];

guideCategorization[name_String] := CellGroupData[{
  Cell["Categorization", "CategorizationSection"],
  Cell["Guide", "Categorization", CellLabel -> "Entity Type"],
  Cell["Lightmarey/FormulaTransformEngine", "Categorization", CellLabel -> "Paclet Name"],
  Cell["Lightmarey`FormulaTransformEngine`", "Categorization", CellLabel -> "Context"],
  Cell["Lightmarey/FormulaTransformEngine/guide/" <> name, "Categorization", CellLabel -> "URI"]
}, Closed];

guideNotebook[name_String, title_String, abstract_String, cells_List, language_String] := Notebook[Join[
  {Cell[guideCategorization[name]], Cell[title, "GuideTitle"], Cell[abstract, "GuideAbstract"]}, cells
], TaggingRules -> <|"Paclet" -> "Lightmarey/FormulaTransformEngine", "Language" -> language|>,
  StyleDefinitions -> FrontEnd`FileName[{"Wolfram"}, "GuidePageStylesExt.nb", CharacterEncoding -> "UTF-8"]];

mainGuide[language_String] := guideNotebook[
  "FormulaTransformEngine", "FormulaTransformEngine",
  If[language === "English",
    "Replayable theorem application for analysis formulas, with bounded search, explicit obligations, immutable registries, and one request model for humans and agents.",
    "\:9762\:5411\:5206\:6790\:516c\:5f0f\:7684\:53ef\:91cd\:653e\:5b9a\:7406\:5e94\:7528\:ff0c\:63d0\:4f9b\:6709\:754c\:641c\:7d22\:3001\:663e\:5f0f\:4e49\:52a1\:3001\:4e0d\:53ef\:53d8 registry\:ff0c\:4ee5\:53ca\:4eba\:7c7b\:4e0e Agent \:5171\:7528\:7684\:4e00\:5957\:8bf7\:6c42\:6a21\:578b\:3002"],
  Join[
    {Cell[If[language === "English", "Start here", "\:4ece\:8fd9\:91cc\:5f00\:59cb"], "GuideFunctionsSection"],
     Cell[TextData[{guideLink["FormulaTransformWorkflow", If[language === "English", "Formula transform workflow", "\:516c\:5f0f\:53d8\:6362\:5de5\:4f5c\:6d41"]],
       If[language === "English", " \[LongDash] choose discovery, application, planning, replay, and certification calls.", " \[LongDash] \:9009\:62e9\:53d1\:73b0\:3001\:5e94\:7528\:3001\:89c4\:5212\:3001\:91cd\:653e\:548c\:8bc1\:4e66\:8c03\:7528\:3002"]}], "GuideText"],
     Cell[TextData[{guideLink["AuthoringFormulaTransformRules", If[language === "English", "Authoring .ftr.md rules", "\:7f16\:5199 .ftr.md \:89c4\:5219"]],
       If[language === "English", " \[LongDash] write, lint, compile, test, and register theorem families.", " \[LongDash] \:7f16\:5199\:3001lint\:3001\:7f16\:8bd1\:3001\:6d4b\:8bd5\:5e76\:6ce8\:518c\:5b9a\:7406\:65cf\:3002"]}], "GuideText"],
     Cell[If[language === "English", "Transformation and replay", "\:53d8\:6362\:4e0e\:91cd\:653e"], "GuideFunctionsSection"]},
    (Cell[TextData[{referenceLink[#], " \[LongDash] " <> localized[apiDescriptions[#], language]}], "GuideText"] & /@ apiSymbols),
    {Cell[If[language === "English", "Mathematical primitives", "\:6570\:5b66\:539f\:8bed"], "GuideFunctionsSection"]},
    (Cell[TextData[{referenceLink[#], " \[LongDash] " <> localized[primitiveDescriptions[#], language]}], "GuideText"] & /@ primitiveSymbols)
  ], language
];

workflowGuide[language_String] := guideNotebook[
  "FormulaTransformWorkflow",
  If[language === "English", "Formula Transform Workflow", "\:516c\:5f0f\:53d8\:6362\:5de5\:4f5c\:6d41"],
  If[language === "English", "A practical route from an expression to candidate selection, target planning, replay validation, and optional certification.", "\:4ece\:8868\:8fbe\:5f0f\:51fa\:53d1\:ff0c\:7ecf\:8fc7\:5019\:9009\:9009\:62e9\:3001\:76ee\:6807\:89c4\:5212\:3001\:91cd\:653e\:9a8c\:8bc1\:ff0c\:5e76\:5728\:9002\:7528\:65f6\:751f\:6210\:8bc1\:4e66\:7684\:5b9e\:7528\:6d41\:7a0b\:3002"],
  {
    Cell[If[language === "English", "1. Discover before choosing", "1. \:5148\:53d1\:73b0\:ff0c\:518d\:9009\:62e9"], "GuideFunctionsSection"],
    Cell[TextData[{If[language === "English", "Use ", "\:4f7f\:7528 "], referenceLink["FindFormulaTransforms"], If[language === "English", " when more than one theorem or direction may apply. Inspect CandidateId, Summary, Differences, Conditions, and Obligations.", " \:67e5\:770b\:53ef\:80fd\:9002\:7528\:7684\:591a\:4e2a\:5b9a\:7406\:6216\:65b9\:5411\:ff1b\:68c0\:67e5 CandidateId\:3001Summary\:3001Differences\:3001Conditions \:548c Obligations\:3002"]}], "GuideText"],
    Cell[BoxData["found = FindFormulaTransforms[expr];\nfound[\"Candidates\"][[All, {\"CandidateId\", \"Summary\", \"Differences\", \"Obligations\"}]]"], "Input"],
    Cell[If[language === "English", "2. Apply one step or plan to a target", "2. \:5e94\:7528\:4e00\:6b65\:6216\:89c4\:5212\:5230\:76ee\:6807"], "GuideFunctionsSection"],
    Cell[TextData[{referenceLink["ApplyFormulaTransform"], If[language === "English", " requires a unique best complete result. ", " \:8981\:6c42\:552f\:4e00\:6700\:4f73\:5b8c\:6574\:7ed3\:679c\:3002"], referenceLink["PlanFormulaTransform"], If[language === "English", " may return Complete -> False with the best partial replay.", " \:53ef\:4ee5\:8fd4\:56de Complete -> False\:ff0c\:5e76\:4fdd\:7559\:6700\:4f73\:90e8\:5206\:91cd\:653e\:3002"]}], "GuideText"],
    Cell[BoxData["plan = PlanFormulaTransform[expr, TargetRelation -> (expr <= target), MaxDepth -> 4, MaxStates -> 256]"], "Input"],
    Cell[If[language === "English", "3. Supply mathematical context", "3. \:63d0\:4f9b\:6570\:5b66\:4e0a\:4e0b\:6587"], "GuideFunctionsSection"],
    Cell[TextData[{If[language === "English", "Build structured declarations with ", "\:4f7f\:7528 "], referenceLink["CreateFormulaTransformContext"], If[language === "English", ". Native inequalities belong in Assumptions; analytic predicates such as ", " \:6784\:9020\:7ed3\:6784\:5316\:58f0\:660e\:3002\:539f\:751f\:4e0d\:7b49\:5f0f\:5c5e\:4e8e Assumptions\:ff1b\:8bf8\:5982 "], referenceLink["MemLp"], If[language === "English", " belong in the context.", " \:7684\:5206\:6790\:8c13\:8bcd\:5c5e\:4e8e context\:3002"]}], "GuideText"],
    Cell[BoxData["context = CreateFormulaTransformContext[MemLp[f, 2, mu], PositiveMeasure[mu]]"], "Input"],
    Cell[If[language === "English", "4. Understand target equivalence", "4. \:7406\:89e3\:76ee\:6807\:7b49\:4ef7"], "GuideFunctionsSection"],
    Cell[If[language === "English", "TargetEquivalence -> Automatic first performs structural search. Only if needed, it appends one time-bounded ComputationalEquivalence step and replays that step during validation. Use \"Structural\" when this bridge is undesirable.", "TargetEquivalence -> Automatic \:5148\:6267\:884c\:7ed3\:6784\:641c\:7d22\:ff1b\:4ec5\:5728\:9700\:8981\:65f6\:8ffd\:52a0\:4e00\:6b21\:6709\:65f6\:9650\:7684 ComputationalEquivalence \:6b65\:9aa4\:ff0c\:5e76\:5728\:9a8c\:8bc1\:65f6\:91cd\:653e\:8be5\:6b65\:9aa4\:3002\:4e0d\:9700\:8981\:6b64\:6865\:65f6\:4f7f\:7528 \"Structural\"\:3002"], "GuideText"],
    Cell[If[language === "English", "5. Inspect and validate", "5. \:68c0\:67e5\:5e76\:9a8c\:8bc1"], "GuideFunctionsSection"],
    Cell[TextData[{If[language === "English", "Read with ", "\:4f7f\:7528 "], referenceLink["FormulaTransformSteps"], If[language === "English", ", then replay with ", " \:9605\:8bfb\:6b65\:9aa4\:ff0c\:518d\:7528 "], referenceLink["ValidateFormulaTransformDerivation"], If[language === "English", ". Only a Valid replay can be passed to ", " \:91cd\:653e\:3002\:53ea\:6709 Valid \:91cd\:653e\:53ef\:4ee5\:4f20\:7ed9 "], referenceLink["CreateFormulaTransformCertificate"], "."}], "GuideText"],
    Cell[BoxData["FormulaTransformSteps[result]\nValidateFormulaTransformDerivation[result[\"Derivation\"]]"], "Input"],
    Cell[If[language === "English", "Result checklist", "\:7ed3\:679c\:68c0\:67e5\:6e05\:5355"], "GuideFunctionsSection"],
    Cell[If[language === "English", "Check Status, Complete, Relation, Conditions, DischargedConditions, Evidence, Obligations, ContextTemplate, Search, and Derivation. A successful transformation may still be conditional.", "\:68c0\:67e5 Status\:3001Complete\:3001Relation\:3001Conditions\:3001DischargedConditions\:3001Evidence\:3001Obligations\:3001ContextTemplate\:3001Search \:548c Derivation\:3002\:6210\:529f\:53d8\:6362\:4ecd\:53ef\:80fd\:662f\:6761\:4ef6\:6709\:6548\:7684\:3002"], "GuideText"]
  }, language
];

authoringGuide[language_String] := guideNotebook[
  "AuthoringFormulaTransformRules",
  If[language === "English", "Authoring .ftr.md Rules", "\:7f16\:5199 .ftr.md \:89c4\:5219"],
  If[language === "English", "The shortest reliable path for writing theorem families and monotonicity descriptors that remain readable, diagnosable, and replayable.", "\:7f16\:5199\:53ef\:8bfb\:3001\:53ef\:8bca\:65ad\:4e14\:53ef\:91cd\:653e\:7684\:5b9a\:7406\:65cf\:548c\:5355\:8c03\:6027\:63cf\:8ff0\:7b26\:7684\:6700\:77ed\:53ef\:9760\:8def\:5f84\:3002"],
  {
    Cell[If[language === "English", "Source layout", "\:6e90\:6587\:4ef6\:5e03\:5c40"], "GuideFunctionsSection"],
    Cell[If[language === "English", "Use YAML frontmatter for compiled data and Markdown body text for exposition. Match, Result, Conditions, Applicability, and Rewrite contain Wolfram InputForm block scalars. LaTeX in the body is explanatory and is not compiled.", "YAML frontmatter \:5b58\:653e\:7f16\:8bd1\:6570\:636e\:ff0cMarkdown \:6b63\:6587\:7528\:4e8e\:8bf4\:660e\:3002Match\:3001Result\:3001Conditions\:3001Applicability \:548c Rewrite \:4f7f\:7528 Wolfram InputForm \:5757\:5b57\:7b26\:4e32\:ff1b\:6b63\:6587\:4e2d\:7684 LaTeX \:53ea\:4f5c\:8bf4\:660e\:ff0c\:4e0d\:53c2\:4e0e\:7f16\:8bd1\:3002"], "GuideText"],
    Cell[BoxData["---\nSchemaVersion: 1\nKind: TransformFamily\nName: Example\nTags: [Inequality, MeasureSpace]\nConditions: |\n  {}\nVariants:\n  - Name: Upper\n    Match: |\n      Abs[MeasureIntegral[f_, x_, mu_]]\n    Result: |\n      Abs[MeasureIntegral[f, x, mu]] <= LpNorm[f, 1, mu]\n---"], "Input"],
    Cell[If[language === "English", "Write natural patterns", "\:81ea\:7136\:5730\:7f16\:5199 pattern"], "GuideFunctionsSection"],
    Cell[TextData[{If[language === "English", "Write ordinary Wolfram multiplication and slots such as x_. Binder positions come from the primitive specification; repeated named slots are unified. See ", "\:4f7f\:7528\:666e\:901a Wolfram \:4e58\:6cd5\:548c x_ \:8fd9\:6837\:7684 slot\:3002binder \:4f4d\:7f6e\:6765\:81ea\:539f\:8bed\:89c4\:683c\:ff1b\:540c\:540d slot \:4f1a\:88ab\:7edf\:4e00\:3002\:53c2\:89c1 "], referenceLink["MeasureIntegral"], If[language === "English", " and ", " \:548c "], referenceLink["MeasureOf"], "."}], "GuideText"],
    Cell[If[language === "English", "Parameters and premises", "\:53c2\:6570\:4e0e\:524d\:63d0"], "GuideFunctionsSection"],
    Cell[TextData[{If[language === "English", "Declare rule parameters in Parameters and mathematical hypotheses in Conditions. Use propositions such as ", "\:5728 Parameters \:4e2d\:58f0\:660e\:89c4\:5219\:53c2\:6570\:ff0c\:5728 Conditions \:4e2d\:58f0\:660e\:6570\:5b66\:524d\:63d0\:3002\:4f7f\:7528\:8bf8\:5982 "], referenceLink["MemLp"], ", ", referenceLink["IntegrableOn"], ", ", referenceLink["AEMeasurable"], If[language === "English", ", and ", " \:548c "], referenceLink["IntegrationByPartsAdmissible"], If[language === "English", "; do not construct function-space objects.", "\:ff1b\:4e0d\:8981\:6784\:9020\:51fd\:6570\:7a7a\:95f4\:5bf9\:8c61\:3002"]}], "GuideText"],
    Cell[If[language === "English", "Generated values", "\:751f\:6210\:503c"], "GuideFunctionsSection"],
    Cell[TextData[{If[language === "English", "Use GeneratedParameters for theorem constants. The runtime represents them with ", "\:5b9a\:7406\:5e38\:6570\:4f7f\:7528 GeneratedParameters\:ff1b\:8fd0\:884c\:65f6\:7528 "], referenceLink["TheoremConstant"], If[language === "English", ". Result-only binders are inferred when they are lexically scoped.", " \:8868\:793a\:3002\:53ea\:51fa\:73b0\:5728 Result \:4e2d\:4e14\:5177\:6709\:8bcd\:6cd5\:4f5c\:7528\:57df\:7684 binder \:4f1a\:88ab\:63a8\:65ad\:3002"]}], "GuideText"],
    Cell[If[language === "English", "Heuristics and normalization", "\:542f\:53d1\:5f0f\:4e0e\:89c4\:8303\:5316"], "GuideFunctionsSection"],
    Cell[If[language === "English", "A Heuristic is a family-scoped, equality-valued Preparation step with a total structural Applicability predicate. Representation normalization stays in the compiler/runtime canonicalizer; mathematical bridges remain ordinary theorem variants.", "Heuristic \:662f\:5b9a\:7406\:65cf\:5185\:3001\:7b49\:5f0f\:503c\:7684 Preparation \:6b65\:9aa4\:ff0c\:5e76\:5e26\:6709\:5168\:7ed3\:6784 Applicability \:8c13\:8bcd\:3002\:8868\:793a\:89c4\:8303\:5316\:7559\:5728\:7f16\:8bd1\:5668/\:8fd0\:884c\:65f6 canonicalizer \:4e2d\:ff1b\:6570\:5b66\:6865\:63a5\:4ecd\:662f\:666e\:901a\:5b9a\:7406\:53d8\:4f53\:3002"], "GuideText"],
    Cell[If[language === "English", "Compile and diagnose", "\:7f16\:8bd1\:4e0e\:8bca\:65ad"], "GuideFunctionsSection"],
    Cell[TextData[{If[language === "English", "Run lint_ftr.wls while editing. ", "\:7f16\:8f91\:65f6\:8fd0\:884c lint_ftr.wls\:3002"], referenceLink["CompileFormulaTransformSource"], If[language === "English", " returns exact source locations; ", " \:8fd4\:56de\:7cbe\:786e\:6e90\:7801\:4f4d\:7f6e\:ff1b"], referenceLink["CompileFormulaTransformFamily"], If[language === "English", " and ", " \:548c "], referenceLink["CompileFormulaTransformMonotonicityDescriptor"], If[language === "English", " validate the two strict schemas.", " \:9a8c\:8bc1\:4e24\:79cd\:4e25\:683c schema\:3002"]}], "GuideText"],
    Cell[BoxData["wolframscript -file .\\lint_ftr.wls .\\Registry\\Sources\\Example.ftr.md\nwolframscript -file .\\compile_rules.wls\nwolframscript -file .\\build_rules.wls\nwolframscript -file .\\run_tests.wls"], "Input"],
    Cell[If[language === "English", "Author checklist", "\:4f5c\:8005\:68c0\:67e5\:6e05\:5355"], "GuideFunctionsSection"],
    Cell[If[language === "English", "Keep names stable; use only declared symbols; prefer native inert Wolfram heads; add a package primitive only for a real missing semantic boundary; state hypotheses explicitly; keep Meta nonsemantic; add positive, negative, compilation, and replay tests.", "\:4fdd\:6301\:540d\:79f0\:7a33\:5b9a\:ff1b\:53ea\:4f7f\:7528\:5df2\:58f0\:660e\:7b26\:53f7\:ff1b\:4f18\:5148\:4f7f\:7528 Wolfram \:539f\:751f\:60f0\:6027 head\:ff1b\:53ea\:6709\:786e\:5b9e\:7f3a\:5c11\:8bed\:4e49\:8fb9\:754c\:65f6\:624d\:6dfb\:52a0\:5305\:539f\:8bed\:ff1b\:663e\:5f0f\:9648\:8ff0\:524d\:63d0\:ff1bMeta \:4fdd\:6301\:975e\:8bed\:4e49\:ff1b\:8865\:5145\:6b63\:5411\:3001\:53cd\:5411\:3001\:7f16\:8bd1\:548c\:91cd\:653e\:6d4b\:8bd5\:3002"], "GuideText"]
  }, language
];

requiredData = {apiDescriptions, apiForms, apiReturns, apiFailures, apiNotes, apiExamples, apiSeeAlso};
If[! AllTrue[requiredData, Sort[Keys[#]] === Sort[apiSymbols] &] ||
   ! AllTrue[{primitiveDescriptions, primitiveForms, primitiveUseExamples, primitiveSpecialNotes},
     Sort[Keys[#]] === Sort[primitiveSymbols] &],
  Print["Documentation metadata does not cover the public API and primitive specification."];
  Exit[1]
];

writeNotebook[path_, notebook_] := Module[{stream},
  stream = OpenWrite[path, CharacterEncoding -> "ASCII"];
  WriteString[stream, ToString[notebook, InputForm, PageWidth -> Infinity], "\n"];
  Close[stream]
];

Do[
  languageRoot = FileNameJoin[{root, "Documentation", language}];
  symbolRoot = FileNameJoin[{languageRoot, "ReferencePages", "Symbols"}];
  guideRoot = FileNameJoin[{languageRoot, "Guides"}];
  If[! DirectoryQ[symbolRoot], CreateDirectory[symbolRoot, CreateIntermediateDirectories -> True]];
  If[! DirectoryQ[guideRoot], CreateDirectory[guideRoot, CreateIntermediateDirectories -> True]];
  Scan[DeleteFile, FileNames["*.nb", symbolRoot]];
  Scan[DeleteFile, FileNames["*.nb", guideRoot]];
  Do[
    writeNotebook[FileNameJoin[{symbolRoot, name <> ".nb"}],
      If[MemberQ[apiSymbols, name], apiPage[name, language], primitivePage[name, language]]],
    {name, symbols}
  ];
  writeNotebook[FileNameJoin[{guideRoot, "FormulaTransformEngine.nb"}], mainGuide[language]];
  writeNotebook[FileNameJoin[{guideRoot, "FormulaTransformWorkflow.nb"}], workflowGuide[language]];
  writeNotebook[FileNameJoin[{guideRoot, "AuthoringFormulaTransformRules.nb"}], authoringGuide[language]],
  {language, {"English", "ChineseSimplified"}}
];

Print["Generated ", 2 Length[symbols], " reference pages and 6 guides."];