ch:normalization: ch:normalization

Problem and invariant. Normalize the full finite $T_{\mathsf{impl}}$ slice without trusting a raw rewrite loop or the normal-form shape checker as a type checker. Maintain two invariants: semantic values are reified only at their supplied semantic type, and type quotation differs from universe-code quotation exactly where the signature’s lift equations differ.

Two representations. Terms use de Bruijn indices. Semantic functions are defunctionalized closures containing syntax and an environment; semantic dependent pairs store both components, and neutrals record stuck applications, projections, and the four eliminators. Metatheoretic functions would make the logical construction more direct, but Kappa could neither compare nor print them. An intrinsically typed value family would reject cross-type readback by construction; the extrinsic domain instead makes that boundary observable through wrong-readback and the separate shape rechecker.

First complete version. Implement environments, evaluation, semantic application, and reflection first. Reification at $\mathrm{\Pi }$ reflects the next level, applies the closure, and wraps the recursively reified result in an eta-long lambda. Reification at $\mathrm{\Sigma }$ projects a neutral or semantic pair at the first component and then reifies the second at the instantiated codomain. The $\mathbf{1}$ clause always returns star. Add the Boolean, natural, identity, and vector eliminators in formation–introduction–elimination–computation order, retaining a neutral node when the scrutinee or equality proof is stuck.

Add type quotation and code quotation separately. Type quotation erases a lift through Lift-El; code quotation retains a lift unless a displayed code equation removes it. In particular the signature has no Lift-Vec equation. Only after these operations pass should conversion compare normal forms and the partial rechecker validate their outer shape.

Add the cases in semantic groups. Begin with eta at products, sums, and Unit. Add the four stuck eliminators, then their constructor computations. Separate type quotation from code quotation before adding lift probes. Finally add symbolic-level normalization, schema equality, conversion, head inversion, wrong-type readback, shape, and idempotence cases. Appendix E owns the exact expected output and hashes; the grouping here is the construction order.

A failing version. Return the first projection twice from the $\mathrm{\Sigma }$ reifier. Kappa still checks the program and the shallow normal-shape oracle still passes, but sigma-eta fails. This is why the rechecker cannot replace the type-indexed semantic argument. Independently, erase binder metadata in type quotation to break meta-kept, or retain the lift in type quotation to break lift-vec-type; these mutations distinguish syntax shape, metadata coherence, and the type/code lift boundary.

Acceptance test. Run the four commands in appendix E. Require a silent check, a passing inline test, the exact Appendix E output, and an empty audit. Replay every recorded semantic mutant independently, require its named oracle and the computed aggregate to fail, restore the accepted source, and repeat all four commands.

Mathematical boundary. Fuel makes the Kappa evaluator total and does not prove that every well-typed term normalizes within the fixed bound. The corpus is a normalizer and partial normal-form rechecker, not a type checker; its semantic input type is trusted. It does not infer that type or check universe formation. Symbolic level comparison retains parameters and decides schema equality without selecting an ambient numeric assignment. Running it proves none of theorem 111.76, theorem 49.18 or corollary 49.20; those results depend on the chapter’s Kripke logical relation and fundamental lemma.