A-normalization to purify's input form (doc/eidos.md §6): every reactive definition body becomes a let chain over simple right-hand sides ending in an atom (or a jump), by the spec's small ordered ruleset — eta-expansion (definitions reach their signature arity, parameters in the telescope), argument naming (the computed arguments of spines — definition calls, constructor applications, cases — are let-bound), subject naming (case scrutinees are atoms), head reduction (a residual beta-redex becomes a let), let-flattening (no lets in right-hand sides), and alternative flattening (alternative bodies are themselves ANF). Primitive applications are transparent: a primitive-headed argument is not named but normalized in place, so the pure data path stays an expression tree of primitives over atoms (the fold lowers it inline, and pattern-matches its idioms — bit slices, finite literals — where they stand).

The *reactive* fragment is the deliberate exemption — it is what purify consumes, and its structure must survive:

• a spine whose type mentions the reactive stack stays a spine; its computed arguments are named, its lambda arguments (bind continuations, like the higher-order primitives' function arguments) stay in place with A-normalized bodies, and its reactive arguments normalize recursively in place (a pure let may wrap them);
• a case with a reactive result type stays in tail position (its scrutinee is named, its alternatives normalize as tails) — purify turns it into a terminator case; a pure-resulted case is let-bound like any other computation.

Runs after the partial evaluator (ReWire.ModCache pass 6), immediately before purify.